1 module Symantic.Optimize where
3 import Data.Bool (Bool)
4 import qualified Data.Function as Fun
6 import Symantic.Classes
9 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
10 -- but to avoid duplication of work, only those manually marked
11 -- as using their variable at most once.
13 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
14 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
15 normalOrderReduction :: forall repr a.
17 IfThenElseable repr =>
18 SomeData repr a -> SomeData repr a
19 normalOrderReduction = nor
21 -- | normal-order reduction
22 nor :: SomeData repr b -> SomeData repr b
24 Data (Lam f) -> lam (nor Fun.. f)
25 Data (Lam1 f) -> lam1 (nor Fun.. f)
26 Data (x :@ y) -> case whnf x of
27 Data (Lam1 f) -> nor (f y)
29 Data (IfThenElse test ok ko) ->
31 Data (Constant b :: Data (Constantable Bool) repr Bool) ->
32 if b then nor ok else nor ko
33 t -> ifThenElse (nor t) (nor ok) (nor ko)
35 -- | weak-head normal-form
36 whnf :: SomeData repr b -> SomeData repr b
38 Data (x :@ y) -> case whnf x of
39 Data (Lam1 f) -> whnf (f y)