src/Symantic/Typed/Optimize.hs

   1 module Symantic.Typed.Optimize where
   2
   3 import Data.Bool (Bool)
   4 import qualified Data.Function as Fun
   5
   6 import Symantic.Typed.Lang
   7 import Symantic.Typed.Data
   8
   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.
  12 --
  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.
  16   Abstractable repr =>
  17   IfThenElseable repr =>
  18   SomeData repr a -> SomeData repr a
  19 normalOrderReduction = nor
  20   where
  21   -- | normal-order reduction
  22   nor :: SomeData repr b -> SomeData repr b
  23   nor = \case
  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)
  28       x' -> nor x' .@ nor y
  29     Data (IfThenElse test ok ko) ->
  30       case nor test of
  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)
  34     x -> x
  35   -- | weak-head normal-form
  36   whnf :: SomeData repr b -> SomeData repr b
  37   whnf = \case
  38     Data (x :@ y) -> case whnf x of
  39       Data (Lam1 f) -> whnf (f y)
  40       x' -> x' .@ y
  41     x -> x