module Symantic.Typed.Optim where

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 =>
  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
    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