module Hydra.Reduction where

import Hydra.Core
import Hydra.Monads
import Hydra.Compute
import Hydra.Rewriting
import Hydra.Basics
import Hydra.Lexical
import Hydra.Lexical
import Hydra.CoreDecoding
import Hydra.Util.Context

import qualified Control.Monad as CM
import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Set as S


alphaConvert :: Ord m => Variable -> Term m -> Term m -> Term m
alphaConvert :: forall m. Ord m => Variable -> Term m -> Term m -> Term m
alphaConvert Variable
vold Term m
tnew = forall b a.
Ord b =>
((Term a -> Term b) -> Term a -> Term b)
-> (a -> b) -> Term a -> Term b
rewriteTerm (Term m -> Term m) -> Term m -> Term m
rewrite forall a. a -> a
id
  where
    rewrite :: (Term m -> Term m) -> Term m -> Term m
rewrite Term m -> Term m
recurse Term m
term = case Term m
term of
      TermFunction (FunctionLambda (Lambda Variable
v Term m
body)) -> if Variable
v forall a. Eq a => a -> a -> Bool
== Variable
vold
        then Term m
term
        else Term m -> Term m
recurse Term m
term
      TermVariable Variable
v -> if Variable
v forall a. Eq a => a -> a -> Bool
== Variable
vold then Term m
tnew else forall m. Variable -> Term m
TermVariable Variable
v
      Term m
_ -> Term m -> Term m
recurse Term m
term

-- For demo purposes. This should be generalized to enable additional side effects of interest.
countPrimitiveFunctionInvocations :: Bool
countPrimitiveFunctionInvocations :: Bool
countPrimitiveFunctionInvocations = Bool
True

-- | A beta reduction function which is designed for safety, not speed.
--   This function does not assume that term to be evaluated is in a normal form,
--   and will provide an informative error message if evaluation fails.
--   Type checking is assumed to have already occurred.
betaReduceTerm :: (Ord m, Show m) => Term m -> GraphFlow m (Term m)
betaReduceTerm :: forall m. (Ord m, Show m) => Term m -> GraphFlow m (Term m)
betaReduceTerm = forall {m}.
(Ord m, Show m) =>
Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce forall k a. Map k a
M.empty
  where
    reduce :: Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings Term m
term = do
      Context m
cx <- forall s. Flow s s
getState
      if forall m. EvaluationStrategy -> Term m -> Bool
termIsOpaque (forall m. Context m -> EvaluationStrategy
contextStrategy Context m
cx) Term m
term
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure Term m
term
        else case forall m. Term m -> Term m
stripTerm Term m
term of
          TermApplication (Application Term m
func Term m
arg) -> Term m -> Flow (Context m) (Term m)
reduceb Term m
func forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings [Term m
arg]
          TermLiteral Literal
_ -> Flow (Context m) (Term m)
done
          TermElement Name
_ -> Flow (Context m) (Term m)
done
          TermFunction Function m
f -> Function m -> Flow (Context m) (Term m)
reduceFunction Function m
f
          TermList [Term m]
terms -> forall m. [Term m] -> Term m
TermList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM Term m -> Flow (Context m) (Term m)
reduceb [Term m]
terms
          TermMap Map (Term m) (Term m)
map -> forall m. Map (Term m) (Term m) -> Term m
TermMap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM (Term m, Term m) -> Flow (Context m) (Term m, Term m)
reducePair forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map (Term m) (Term m)
map)
            where
              reducePair :: (Term m, Term m) -> Flow (Context m) (Term m, Term m)
reducePair (Term m
k, Term m
v) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term m -> Flow (Context m) (Term m)
reduceb Term m
k forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term m -> Flow (Context m) (Term m)
reduceb Term m
v
          TermNominal (Named Name
name Term m
term') -> (\Term m
t -> forall m. Named m -> Term m
TermNominal (forall m. Name -> Term m -> Named m
Named Name
name Term m
t)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings Term m
term'
          TermOptional Maybe (Term m)
m -> forall m. Maybe (Term m) -> Term m
TermOptional forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM Term m -> Flow (Context m) (Term m)
reduceb Maybe (Term m)
m
          TermRecord (Record Name
n [Field m]
fields) -> forall m. Record m -> Term m
TermRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall m. Name -> [Field m] -> Record m
Record Name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM Field m -> Flow (Context m) (Field m)
reduceField [Field m]
fields)
          TermSet Set (Term m)
terms -> forall m. Set (Term m) -> Term m
TermSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Ord a => [a] -> Set a
S.fromList (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM Term m -> Flow (Context m) (Term m)
reduceb forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (Term m)
terms)
          TermUnion (Union Name
n Field m
f) -> forall m. Union m -> Term m
TermUnion forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall m. Name -> Field m -> Union m
Union Name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field m -> Flow (Context m) (Field m)
reduceField Field m
f)
          TermVariable var :: Variable
var@(Variable String
v) -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Variable
var Map Variable (Term m)
bindings of
            Maybe (Term m)
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"cannot reduce free variable " forall a. [a] -> [a] -> [a]
++ String
v
            Just Term m
t -> Term m -> Flow (Context m) (Term m)
reduceb Term m
t
      where
        done :: Flow (Context m) (Term m)
done = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term m
term
        reduceb :: Term m -> Flow (Context m) (Term m)
reduceb = Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings
        reduceField :: Field m -> Flow (Context m) (Field m)
reduceField (Field FieldName
n Term m
t) = forall m. FieldName -> Term m -> Field m
Field FieldName
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term m -> Flow (Context m) (Term m)
reduceb Term m
t
        reduceFunction :: Function m -> Flow (Context m) (Term m)
reduceFunction Function m
f = case Function m
f of
          FunctionElimination Elimination m
el -> case Elimination m
el of
            Elimination m
EliminationElement -> Flow (Context m) (Term m)
done
            EliminationOptional (OptionalCases Term m
nothing Term m
just) -> forall m. Function m -> Term m
TermFunction forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Elimination m -> Function m
FunctionElimination forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. OptionalCases m -> Elimination m
EliminationOptional forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
              (forall m. Term m -> Term m -> OptionalCases m
OptionalCases forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term m -> Flow (Context m) (Term m)
reduceb Term m
nothing forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term m -> Flow (Context m) (Term m)
reduceb Term m
just)
            EliminationRecord Projection
_ -> Flow (Context m) (Term m)
done
            EliminationUnion (CaseStatement Name
n [Field m]
cases) ->
              forall m. Function m -> Term m
TermFunction forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Elimination m -> Function m
FunctionElimination forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. CaseStatement m -> Elimination m
EliminationUnion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Name -> [Field m] -> CaseStatement m
CaseStatement Name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
CM.mapM Field m -> Flow (Context m) (Field m)
reduceField [Field m]
cases
          FunctionCompareTo Term m
other -> forall m. Function m -> Term m
TermFunction forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Term m -> Function m
FunctionCompareTo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term m -> Flow (Context m) (Term m)
reduceb Term m
other
          FunctionLambda (Lambda Variable
v Term m
body) -> forall m. Function m -> Term m
TermFunction forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Lambda m -> Function m
FunctionLambda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Variable -> Term m -> Lambda m
Lambda Variable
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term m -> Flow (Context m) (Term m)
reduceb Term m
body
          FunctionPrimitive Name
_ -> Flow (Context m) (Term m)
done

        -- Assumes that the function is closed and fully reduced. The arguments may not be.
        reduceApplication :: Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings [Term m]
args Term m
f = if forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Term m]
args then forall (f :: * -> *) a. Applicative f => a -> f a
pure Term m
f else case forall m. Term m -> Term m
stripTerm Term m
f of
          TermApplication (Application Term m
func Term m
arg) -> Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings Term m
func
             forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings (Term m
argforall a. a -> [a] -> [a]
:[Term m]
args)

          TermFunction Function m
f -> case Function m
f of
            FunctionElimination Elimination m
e -> case Elimination m
e of
              Elimination m
EliminationElement -> do
                Term m
arg <- Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
L.head [Term m]
args
                case forall m. Term m -> Term m
stripTerm Term m
arg of
                  TermElement Name
name -> forall m. Name -> GraphFlow m (Term m)
dereferenceElement Name
name
                    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings
                    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings (forall a. [a] -> [a]
L.tail [Term m]
args)
                  Term m
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"tried to apply data (delta) to a non- element reference"

              EliminationOptional (OptionalCases Term m
nothing Term m
just) -> do
                Term m
arg <- (Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
L.head [Term m]
args) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall m. Term m -> GraphFlow m (Term m)
deref
                case forall m. Term m -> Term m
stripTerm Term m
arg of
                  TermOptional Maybe (Term m)
m -> case Maybe (Term m)
m of
                    Maybe (Term m)
Nothing -> Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings Term m
nothing
                    Just Term m
t -> Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings Term m
just forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings (Term m
tforall a. a -> [a] -> [a]
:forall a. [a] -> [a]
L.tail [Term m]
args)
                  Term m
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"tried to apply an optional case statement to a non-optional term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term m
arg

              EliminationUnion (CaseStatement Name
_ [Field m]
cases) -> do
                Term m
arg <- (Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
L.head [Term m]
args) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall m. Term m -> GraphFlow m (Term m)
deref
                case forall m. Term m -> Term m
stripTerm Term m
arg of
                  TermUnion (Union Name
_ (Field FieldName
fname Term m
t)) -> if forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Field m]
matching
                      then forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"no case for field named " forall a. [a] -> [a] -> [a]
++ FieldName -> String
unFieldName FieldName
fname
                      else Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings (forall m. Field m -> Term m
fieldTerm forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
L.head [Field m]
matching)
                        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings (Term m
tforall a. a -> [a] -> [a]
:forall a. [a] -> [a]
L.tail [Term m]
args)
                    where
                      matching :: [Field m]
matching = forall a. (a -> Bool) -> [a] -> [a]
L.filter (\Field m
c -> forall m. Field m -> FieldName
fieldName Field m
c forall a. Eq a => a -> a -> Bool
== FieldName
fname) [Field m]
cases
                  Term m
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"tried to apply a case statement to a non- union term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term m
arg

            -- TODO: FunctionCompareTo

            FunctionPrimitive Name
name -> do
                 PrimitiveFunction m
prim <- forall m. Name -> GraphFlow m (PrimitiveFunction m)
requirePrimitiveFunction Name
name
                 let arity :: Int
arity = forall m. PrimitiveFunction m -> Int
primitiveFunctionArity PrimitiveFunction m
prim
                 if forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Term m]
args forall a. Ord a => a -> a -> Bool
>= Int
arity
                   then do
                     if Bool
countPrimitiveFunctionInvocations
                       then forall s. String -> Flow s Int
nextCount (String
"count_" forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
name)
                       else forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
                     (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
L.take Int
arity [Term m]
args)
                     forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall m.
PrimitiveFunction m -> [Term m] -> Flow (Context m) (Term m)
primitiveFunctionImplementation PrimitiveFunction m
prim
                     forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce Map Variable (Term m)
bindings
                     forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings (forall a. Int -> [a] -> [a]
L.drop Int
arity [Term m]
args)
                   else Flow (Context m) (Term m)
unwind
               where
                 unwind :: Flow (Context m) (Term m)
unwind = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Term m
l Term m
r -> forall m. Application m -> Term m
TermApplication forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> Application m
Application Term m
l Term m
r) (forall m. Function m -> Term m
TermFunction Function m
f) [Term m]
args

            FunctionLambda (Lambda Variable
v Term m
body) -> Map Variable (Term m) -> Term m -> Flow (Context m) (Term m)
reduce (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Variable
v (forall a. [a] -> a
L.head [Term m]
args) Map Variable (Term m)
bindings) Term m
body
              forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Map Variable (Term m)
-> [Term m] -> Term m -> Flow (Context m) (Term m)
reduceApplication Map Variable (Term m)
bindings (forall a. [a] -> [a]
L.tail [Term m]
args)

            -- TODO: FunctionProjection

            Function m
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"unsupported function variant: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall m. Function m -> FunctionVariant
functionVariant Function m
f)

          Term m
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"tried to apply a non-function: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall m. Term m -> TermVariant
termVariant Term m
f)

-- Note: this is eager beta reduction, in that we always descend into subtypes,
--       and always reduce the right-hand side of an application prior to substitution
betaReduceType :: (Ord m, Show m) => Type m -> GraphFlow m (Type m)
betaReduceType :: forall m. (Ord m, Show m) => Type m -> GraphFlow m (Type m)
betaReduceType Type m
typ = do
    Context m
cx <- forall s. Flow s s
getState :: GraphFlow m (Context m)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b.
((Type a -> Type b) -> Type a -> Type b)
-> (a -> b) -> Type a -> Type b
rewriteType (forall {m} {t}.
(Ord m, Show m) =>
Context m -> (t -> Type m) -> t -> Type m
mapExpr Context m
cx) forall a. a -> a
id Type m
typ
  where
    mapExpr :: Context m -> (t -> Type m) -> t -> Type m
mapExpr Context m
cx t -> Type m
rec t
t = case t -> Type m
rec t
t of
        TypeApplication ApplicationType m
a -> ApplicationType m -> Type m
reduceApp ApplicationType m
a
        Type m
t' -> Type m
t'
      where
        reduceApp :: ApplicationType m -> Type m
reduceApp (ApplicationType Type m
lhs Type m
rhs) = case Type m
lhs of
          TypeAnnotated (Annotated Type m
t' m
ann) -> forall m. Annotated (Type m) m -> Type m
TypeAnnotated (forall a m. a -> m -> Annotated a m
Annotated (ApplicationType m -> Type m
reduceApp (forall m. Type m -> Type m -> ApplicationType m
ApplicationType Type m
t' Type m
rhs)) m
ann)
          TypeLambda (LambdaType VariableType
v Type m
body) -> forall s a. s -> Flow s a -> a
fromFlow Context m
cx forall a b. (a -> b) -> a -> b
$ forall m. (Ord m, Show m) => Type m -> GraphFlow m (Type m)
betaReduceType forall a b. (a -> b) -> a -> b
$ forall m. Ord m => VariableType -> Type m -> Type m -> Type m
replaceFreeVariableType VariableType
v Type m
rhs Type m
body
          -- nominal types are transparent
          TypeNominal Name
name -> forall s a. s -> Flow s a -> a
fromFlow Context m
cx forall a b. (a -> b) -> a -> b
$ forall m. (Ord m, Show m) => Type m -> GraphFlow m (Type m)
betaReduceType forall a b. (a -> b) -> a -> b
$ forall m. ApplicationType m -> Type m
TypeApplication forall a b. (a -> b) -> a -> b
$ forall m. Type m -> Type m -> ApplicationType m
ApplicationType Type m
t' Type m
rhs
            where
              t' :: Type m
t' = forall s a. s -> Flow s a -> a
fromFlow Context m
cx forall a b. (a -> b) -> a -> b
$ forall m. Show m => Name -> GraphFlow m (Type m)
requireType Name
name

-- | Apply the special rules:
--     ((\x.e1) e2) == e1, where x does not appear free in e1
--   and
--     ((\x.e1) e2) = e1[x/e2]
--  These are both limited forms of beta reduction which help to "clean up" a term without fully evaluating it.
contractTerm :: Ord m => Term m -> Term m
contractTerm :: forall m. Ord m => Term m -> Term m
contractTerm = forall b a.
Ord b =>
((Term a -> Term b) -> Term a -> Term b)
-> (a -> b) -> Term a -> Term b
rewriteTerm forall {m} {p}. Ord m => (p -> Term m) -> p -> Term m
rewrite forall a. a -> a
id
  where
    rewrite :: (p -> Term m) -> p -> Term m
rewrite p -> Term m
recurse p
term = case Term m
rec of
        TermApplication (Application Term m
lhs Term m
rhs) -> case forall m. Term m -> Term m
stripTerm Term m
lhs of
          TermFunction (FunctionLambda (Lambda Variable
v Term m
body)) -> if forall m. Variable -> Term m -> Bool
isFreeIn Variable
v Term m
body
            then Term m
body
            else forall m. Ord m => Variable -> Term m -> Term m -> Term m
alphaConvert Variable
v Term m
rhs Term m
body
          Term m
_ -> Term m
rec
        Term m
_ -> Term m
rec
      where
        rec :: Term m
rec = p -> Term m
recurse p
term

-- Note: unused / untested
etaReduceTerm :: Term m -> Term m
etaReduceTerm :: forall m. Term m -> Term m
etaReduceTerm Term m
term = case Term m
term of
    TermAnnotated (Annotated Term m
term1 m
ann) -> forall m. Annotated (Term m) m -> Term m
TermAnnotated (forall a m. a -> m -> Annotated a m
Annotated (forall m. Term m -> Term m
etaReduceTerm Term m
term1) m
ann)
    TermFunction (FunctionLambda Lambda m
l) -> Lambda m -> Term m
reduceLambda Lambda m
l
    Term m
_ -> Term m
noChange
  where
    reduceLambda :: Lambda m -> Term m
reduceLambda (Lambda Variable
v Term m
body) = case forall m. Term m -> Term m
etaReduceTerm Term m
body of
      TermAnnotated (Annotated Term m
body1 m
ann) -> Lambda m -> Term m
reduceLambda (forall m. Variable -> Term m -> Lambda m
Lambda Variable
v Term m
body1)
      TermApplication Application m
a -> Application m -> Term m
reduceApplication Application m
a
        where
          reduceApplication :: Application m -> Term m
reduceApplication (Application Term m
lhs Term m
rhs) = case forall m. Term m -> Term m
etaReduceTerm Term m
rhs of
            TermAnnotated (Annotated Term m
rhs1 m
ann) -> Application m -> Term m
reduceApplication (forall m. Term m -> Term m -> Application m
Application Term m
lhs Term m
rhs1)
            TermVariable Variable
v1 -> if Variable
v forall a. Eq a => a -> a -> Bool
== Variable
v1 Bool -> Bool -> Bool
&& forall m. Variable -> Term m -> Bool
isFreeIn Variable
v Term m
lhs
              then forall m. Term m -> Term m
etaReduceTerm Term m
lhs
              else Term m
noChange
            Term m
_ -> Term m
noChange
      Term m
_ -> Term m
noChange
    noChange :: Term m
noChange = Term m
term

-- | Whether a term is closed, i.e. represents a complete program
termIsClosed :: Term m -> Bool
termIsClosed :: forall m. Term m -> Bool
termIsClosed = forall a. Set a -> Bool
S.null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Term m -> Set Variable
freeVariablesInTerm

-- | Whether a term is opaque to reduction, i.e. need not be reduced
termIsOpaque :: EvaluationStrategy -> Term m -> Bool
termIsOpaque :: forall m. EvaluationStrategy -> Term m -> Bool
termIsOpaque EvaluationStrategy
strategy Term m
term = forall a. Ord a => a -> Set a -> Bool
S.member (forall m. Term m -> TermVariant
termVariant Term m
term) (EvaluationStrategy -> Set TermVariant
evaluationStrategyOpaqueTermVariants EvaluationStrategy
strategy)

-- | Whether a term has been fully reduced to a "value"
termIsValue :: Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue :: forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
term = forall m. EvaluationStrategy -> Term m -> Bool
termIsOpaque EvaluationStrategy
strategy Term m
term Bool -> Bool -> Bool
|| case forall m. Term m -> Term m
stripTerm Term m
term of
    TermApplication Application m
_ -> Bool
False
    TermLiteral Literal
_ -> Bool
True
    TermElement Name
_ -> Bool
True
    TermFunction Function m
f -> Function m -> Bool
functionIsValue Function m
f
    TermList [Term m]
els -> forall {t :: * -> *}. Foldable t => t (Term m) -> Bool
forList [Term m]
els
    TermMap Map (Term m) (Term m)
map -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl
      (\Bool
b (Term m
k, Term m
v) -> Bool
b Bool -> Bool -> Bool
&& forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
k Bool -> Bool -> Bool
&& forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
v)
      Bool
True forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map (Term m) (Term m)
map
    TermOptional Maybe (Term m)
m -> case Maybe (Term m)
m of
      Maybe (Term m)
Nothing -> Bool
True
      Just Term m
term -> forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
term
    TermRecord (Record Name
_ [Field m]
fields) -> [Field m] -> Bool
checkFields [Field m]
fields
    TermSet Set (Term m)
els -> forall {t :: * -> *}. Foldable t => t (Term m) -> Bool
forList forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
S.toList Set (Term m)
els
    TermUnion (Union Name
_ Field m
field) -> Field m -> Bool
checkField Field m
field
    TermVariable Variable
_ -> Bool
False
  where
    forList :: t (Term m) -> Bool
forList t (Term m)
els = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Bool
b Term m
t -> Bool
b Bool -> Bool -> Bool
&& forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
t) Bool
True t (Term m)
els
    checkField :: Field m -> Bool
checkField = forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Field m -> Term m
fieldTerm
    checkFields :: [Field m] -> Bool
checkFields = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Bool
b Field m
f -> Bool
b Bool -> Bool -> Bool
&& Field m -> Bool
checkField Field m
f) Bool
True

    functionIsValue :: Function m -> Bool
functionIsValue Function m
f = case Function m
f of
      FunctionCompareTo Term m
other -> forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
other
      FunctionElimination Elimination m
e -> case Elimination m
e of
        Elimination m
EliminationElement -> Bool
True
        EliminationNominal Name
_ -> Bool
True
        EliminationOptional (OptionalCases Term m
nothing Term m
just) -> forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
nothing
          Bool -> Bool -> Bool
&& forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
just
        EliminationRecord Projection
_ -> Bool
True
        EliminationUnion (CaseStatement Name
_ [Field m]
cases) -> [Field m] -> Bool
checkFields [Field m]
cases
      FunctionLambda (Lambda Variable
_ Term m
body) -> forall m. Context m -> EvaluationStrategy -> Term m -> Bool
termIsValue Context m
cx EvaluationStrategy
strategy Term m
body
      FunctionPrimitive Name
_ -> Bool
True