{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Univariant.Optim where

import Data.Kind
import Type.Reflection
import Data.Char (Char)
import Data.Bool (Bool(..))
import Data.Maybe (Maybe(..))
import Data.Functor.Identity (Identity(..))
import Data.String (String)
import Prelude (undefined)
import Text.Show (Show(..))
import qualified Data.Eq as Eq
import qualified Data.Function as Fun

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