module Symantic.Typed.Optimize where

import Data.Bool (Bool)
import qualified Data.Function as Fun

import Symantic.Typed.Lang
import Symantic.Typed.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