src/Symantic/Univariant/Optim.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE KindSignatures #-}
   5 {-# LANGUAGE LambdaCase #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE PatternSynonyms #-}
   8 {-# LANGUAGE QuantifiedConstraints #-}
   9 {-# LANGUAGE RankNTypes #-}
  10 {-# LANGUAGE ScopedTypeVariables #-}
  11 {-# LANGUAGE TypeApplications #-}
  12 {-# LANGUAGE TypeFamilies #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 {-# LANGUAGE ViewPatterns #-}
  15 module Symantic.Univariant.Optim where
  16
  17 import Data.Kind
  18 import Type.Reflection
  19 import Data.Char (Char)
  20 import Data.Bool (Bool(..))
  21 import Data.Maybe (Maybe(..))
  22 import Data.Functor.Identity (Identity(..))
  23 import Data.String (String)
  24 import Prelude (undefined)
  25 import Text.Show (Show(..))
  26 import qualified Data.Eq as Eq
  27 import qualified Data.Function as Fun
  28
  29 import Symantic.Univariant.Trans
  30 import Symantic.Univariant.Lang
  31 import Symantic.Univariant.Data
  32
  33 -- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
  34 -- but to avoid duplication of work, only those manually marked
  35 -- as using their variable at most once.
  36 --
  37 -- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
  38 -- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
  39 normalOrderReduction :: forall repr a.
  40   Abstractable repr =>
  41   SomeData repr a -> SomeData repr a
  42 normalOrderReduction = nor
  43   where
  44   -- | normal-order reduction
  45   nor :: SomeData repr b -> SomeData repr b
  46   nor = \case
  47     Data (Lam f) -> lam (nor Fun.. f)
  48     Data (Lam1 f) -> lam1 (nor Fun.. f)
  49     Data (x :@ y) -> case whnf x of
  50       Data (Lam1 f) -> nor (f y)
  51       x' -> nor x' .@ nor y
  52     x -> x
  53   -- | weak-head normal-form
  54   whnf :: SomeData repr b -> SomeData repr b
  55   whnf = \case
  56     Data (x :@ y) -> case whnf x of
  57       Data (Lam1 f) -> whnf (f y)
  58       x' -> x' .@ y
  59     x -> x