src/Symantic/Typed/Optim.hs

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