module Symantic.Optimize where

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

import Symantic.Lang
import Symantic.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 :: SomeData repr a -> SomeData repr a
normalOrderReduction = SomeData repr a -> SomeData repr a
forall b. SomeData repr b -> SomeData repr b
nor
  where
  -- | normal-order reduction
  nor :: SomeData repr b -> SomeData repr b
  nor :: SomeData repr b -> SomeData repr b
nor = \case
    Data (Lam f) -> (SomeData repr a -> SomeData repr b) -> SomeData repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam (SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor (SomeData repr b -> SomeData repr b)
-> (SomeData repr a -> SomeData repr b)
-> SomeData repr a
-> SomeData repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. SomeData repr a -> SomeData repr b
f)
    Data (Lam1 f) -> (SomeData repr a -> SomeData repr b) -> SomeData repr (a -> b)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam1 (SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor (SomeData repr b -> SomeData repr b)
-> (SomeData repr a -> SomeData repr b)
-> SomeData repr a
-> SomeData repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. SomeData repr a -> SomeData repr b
f)
    Data (x :@ y) -> case SomeData repr (a -> b) -> SomeData repr (a -> b)
forall b. SomeData repr b -> SomeData repr b
whnf SomeData repr (a -> b)
x of
      Data (Lam1 f) -> SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor (SomeData repr a -> SomeData repr b
f SomeData repr a
SomeData repr a
y)
      SomeData repr (a -> b)
x' -> SomeData repr (a -> b) -> SomeData repr (a -> b)
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr (a -> b)
x' SomeData repr (a -> b) -> SomeData repr a -> SomeData repr b
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr a -> SomeData repr a
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr a
y
    Data (IfThenElse test ok ko) ->
      case SomeData repr Bool -> SomeData repr Bool
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr Bool
test of
        Data (Constant b :: Data (Constantable Bool) repr Bool) ->
          if Bool
b then SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr b
ok else SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr b
ko
        SomeData repr Bool
t -> SomeData repr Bool
-> SomeData repr b -> SomeData repr b -> SomeData repr b
forall (repr :: * -> *) a.
IfThenElseable repr =>
repr Bool -> repr a -> repr a -> repr a
ifThenElse (SomeData repr Bool -> SomeData repr Bool
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr Bool
t) (SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr b
ok) (SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
nor SomeData repr b
ko)
    SomeData repr b
x -> SomeData repr b
x
  -- | weak-head normal-form
  whnf :: SomeData repr b -> SomeData repr b
  whnf :: SomeData repr b -> SomeData repr b
whnf = \case
    Data (x :@ y) -> case SomeData repr (a -> b) -> SomeData repr (a -> b)
forall b. SomeData repr b -> SomeData repr b
whnf SomeData repr (a -> b)
x of
      Data (Lam1 f) -> SomeData repr b -> SomeData repr b
forall b. SomeData repr b -> SomeData repr b
whnf (SomeData repr a -> SomeData repr b
f SomeData repr a
SomeData repr a
y)
      SomeData repr (a -> b)
x' -> SomeData repr (a -> b)
x' SomeData repr (a -> b) -> SomeData repr a -> SomeData repr b
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
.@ SomeData repr a
y
    SomeData repr b
x -> SomeData repr b
x