module Symantic.Optimize where import Data.Bool (Bool) import qualified Data.Function as Fun import Symantic.Lang import Symantic.Data -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction), -- but to avoid duplication of work, only those manually marked -- as using their variable at most once. -- -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001, -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf normalOrderReduction :: forall repr a. Abstractable repr => IfThenElseable repr => SomeData repr a -> SomeData repr a normalOrderReduction = nor where -- | normal-order reduction nor :: SomeData repr b -> SomeData repr b nor = \case Data (Lam f) -> lam (nor Fun.. f) Data (Lam1 f) -> lam1 (nor Fun.. f) Data (x :@ y) -> case whnf x of Data (Lam1 f) -> nor (f y) x' -> nor x' .@ nor y Data (IfThenElse test ok ko) -> case nor test of Data (Constant b :: Data (Constantable Bool) repr Bool) -> if b then nor ok else nor ko t -> ifThenElse (nor t) (nor ok) (nor ko) x -> x -- | weak-head normal-form whnf :: SomeData repr b -> SomeData repr b whnf = \case Data (x :@ y) -> case whnf x of Data (Lam1 f) -> whnf (f y) x' -> x' .@ y x -> x