-- | Functions for reducing terms and types, i.e. performing computations

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.Meta

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