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

module Hydra.Reduction where

import Hydra.Basics
import Hydra.Strip
import Hydra.Compute
import Hydra.Core
import Hydra.Schemas
import Hydra.Extras
import Hydra.Graph
import Hydra.Annotations
import Hydra.Lexical
import Hydra.Rewriting
import Hydra.Tier1
import Hydra.Tier2
import qualified Hydra.Dsl.Expect as Expect
import qualified Hydra.Dsl.Terms as Terms

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


alphaConvert :: Name -> Term -> Term -> Term
alphaConvert :: Name -> Term -> Term -> Term
alphaConvert Name
vold Term
tnew = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
rewrite
  where
    rewrite :: (Term -> Term) -> Term -> Term
rewrite Term -> Term
recurse Term
term = case Term
term of
      TermFunction (FunctionLambda (Lambda Name
v Maybe Type
_ Term
_)) -> if Name
v Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
vold
        then Term
term
        else Term -> Term
recurse Term
term
      TermVariable Name
v -> if Name
v Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
vold then Term
tnew else Name -> Term
TermVariable Name
v
      Term
_ -> Term -> Term
recurse Term
term

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

-- A term evaluation function which is alternatively lazy or eager
reduceTerm :: Bool -> M.Map Name Term -> Term -> Flow Graph Term
reduceTerm :: Bool -> Map Name Term -> Term -> Flow Graph Term
reduceTerm Bool
eager Map Name Term
env = ((Term -> Flow Graph Term) -> Term -> Flow Graph Term)
-> Term -> Flow Graph Term
forall s.
((Term -> Flow s Term) -> Term -> Flow s Term)
-> Term -> Flow s Term
rewriteTermM (Term -> Flow Graph Term) -> Term -> Flow Graph Term
mapping
  where
    reduce :: Bool -> Term -> Flow Graph Term
reduce Bool
eager = Bool -> Map Name Term -> Term -> Flow Graph Term
reduceTerm Bool
eager Map Name Term
forall k a. Map k a
M.empty

    mapping :: (Term -> Flow Graph Term) -> Term -> Flow Graph Term
mapping Term -> Flow Graph Term
recurse Term
mid = do
      Term
inner <- if Bool -> Term -> Bool
doRecurse Bool
eager Term
mid then Term -> Flow Graph Term
recurse Term
mid else Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
mid
      Bool -> Term -> [Term] -> Flow Graph Term
applyIfNullary Bool
eager Term
inner []

    doRecurse :: Bool -> Term -> Bool
doRecurse Bool
eager Term
term = Bool
eager Bool -> Bool -> Bool
&& case Term
term of
      TermFunction (FunctionLambda Lambda
_) -> Bool
False
      Term
_ -> Bool
True

    -- Reduce an argument only if evaluation is lazy (i.e. the argument may not already have been reduced)
    reduceArg :: Bool -> Term -> Flow Graph Term
reduceArg Bool
eager Term
arg = if Bool
eager then Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
arg else Bool -> Term -> Flow Graph Term
reduce Bool
False Term
arg

    applyToArguments :: Term -> [Term] -> Term
applyToArguments Term
fun [Term]
args = case [Term]
args of
      [] -> Term
fun
      (Term
h:[Term]
r) -> Term -> [Term] -> Term
applyToArguments (Term -> Term -> Term
Terms.apply Term
fun Term
h) [Term]
r

    replaceFreeName :: Name -> Term -> Term -> Term
replaceFreeName Name
toReplace Term
replacement = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
mapping
      where
        mapping :: (Term -> Term) -> Term -> Term
mapping Term -> Term
recurse Term
inner = case Term
inner of
          TermFunction (FunctionLambda (Lambda Name
param Maybe Type
_ Term
_)) -> if Name
param Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
toReplace then Term
inner else Term -> Term
recurse Term
inner
          TermVariable Name
name -> if Name
name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
toReplace then Term
replacement else Term
inner
          Term
_ -> Term -> Term
recurse Term
inner

    applyIfNullary :: Bool -> Term -> [Term] -> Flow Graph Term
applyIfNullary Bool
eager Term
original [Term]
args = case Term -> Term
stripTerm Term
original of
      TermApplication (Application Term
fun Term
arg) -> Bool -> Term -> [Term] -> Flow Graph Term
applyIfNullary Bool
eager Term
fun (Term
argTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
args)
      TermFunction Function
fun -> case Function
fun of
        FunctionElimination Elimination
elm -> case [Term]
args of
          [] -> Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
original
          -- Reduce the argument prior to application, regardless of laziness
          (Term
arg:[Term]
remainingArgs) -> do
            Term
reducedArg <- Bool -> Term -> Flow Graph Term
reduceArg Bool
eager (Term -> Flow Graph Term) -> Term -> Flow Graph Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
stripTerm Term
arg
            Term
reducedResult <- Elimination -> Term -> Flow Graph Term
forall {s}. Elimination -> Term -> Flow s Term
applyElimination Elimination
elm Term
reducedArg Flow Graph Term -> (Term -> Flow Graph Term) -> Flow Graph Term
forall a b. Flow Graph a -> (a -> Flow Graph b) -> Flow Graph b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Term -> Flow Graph Term
reduce Bool
eager
            Bool -> Term -> [Term] -> Flow Graph Term
applyIfNullary Bool
eager Term
reducedResult [Term]
remainingArgs
        FunctionLambda (Lambda Name
param Maybe Type
_ Term
body) -> case [Term]
args of
          [] -> Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
original
          (Term
arg:[Term]
remainingArgs) -> do
            Term
reducedArg <- Bool -> Term -> Flow Graph Term
reduce Bool
eager (Term -> Flow Graph Term) -> Term -> Flow Graph Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
stripTerm Term
arg
            Term
reducedResult <- Bool -> Term -> Flow Graph Term
reduce Bool
eager (Term -> Flow Graph Term) -> Term -> Flow Graph Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Term -> Term
replaceFreeName Name
param Term
reducedArg Term
body
            Bool -> Term -> [Term] -> Flow Graph Term
applyIfNullary Bool
eager Term
reducedResult [Term]
remainingArgs
        FunctionPrimitive Name
name -> do
          Primitive
prim <- Name -> Flow Graph Primitive
requirePrimitive Name
name
          let arity :: Int
arity = Primitive -> Int
primitiveArity Primitive
prim
          if Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Term]
args
            -- Not enough arguments available; back out
            then Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Flow Graph Term) -> Term -> Flow Graph Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
applyToArguments Term
original [Term]
args
            else do
              let argList :: [Term]
argList = Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
L.take Int
arity [Term]
args
              let remainingArgs :: [Term]
remainingArgs = Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
L.drop Int
arity [Term]
args
              [Term]
reducedArgs <- (Term -> Flow Graph Term) -> [Term] -> Flow Graph [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM (Bool -> Term -> Flow Graph Term
reduceArg Bool
eager) [Term]
argList
              Term
reducedResult <- Primitive -> [Term] -> Flow Graph Term
primitiveImplementation Primitive
prim [Term]
reducedArgs Flow Graph Term -> (Term -> Flow Graph Term) -> Flow Graph Term
forall a b. Flow Graph a -> (a -> Flow Graph b) -> Flow Graph b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Term -> Flow Graph Term
reduce Bool
eager
              Bool -> Term -> [Term] -> Flow Graph Term
applyIfNullary Bool
eager Term
reducedResult [Term]
remainingArgs
      TermVariable Name
_ -> Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Flow Graph Term) -> Term -> Flow Graph Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
applyToArguments Term
original [Term]
args -- TODO: dereference variables
      Term
_ -> Term -> Flow Graph Term
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Flow Graph Term) -> Term -> Flow Graph Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
applyToArguments Term
original [Term]
args

    applyElimination :: Elimination -> Term -> Flow s Term
applyElimination Elimination
elm Term
reducedArg = case Elimination
elm of
      EliminationList Term
_ -> String -> Flow s Term
forall a. String -> Flow s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"list eliminations are unsupported"
      EliminationOptional OptionalCases
_ -> String -> Flow s Term
forall a. String -> Flow s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"optional eliminations are unsupported"
      EliminationRecord Projection
proj -> do
        [Field]
fields <- Name -> Term -> Flow s [Field]
forall s. Name -> Term -> Flow s [Field]
Expect.recordWithName (Projection -> Name
projectionTypeName Projection
proj) (Term -> Flow s [Field]) -> Term -> Flow s [Field]
forall a b. (a -> b) -> a -> b
$ Term -> Term
stripTerm Term
reducedArg
        let matchingFields :: [Field]
matchingFields = (Field -> Bool) -> [Field] -> [Field]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (\Field
f -> Field -> Name
fieldName Field
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Projection -> Name
projectionField Projection
proj) [Field]
fields
        if [Field] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Field]
matchingFields
          then String -> Flow s Term
forall a. String -> Flow s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow s Term) -> String -> Flow s Term
forall a b. (a -> b) -> a -> b
$ String
"no such field: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName (Projection -> Name
projectionField Projection
proj) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName (Projection -> Name
projectionTypeName Projection
proj) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" record"
          else Term -> Flow s Term
forall a. a -> Flow s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Flow s Term) -> Term -> Flow s Term
forall a b. (a -> b) -> a -> b
$ Field -> Term
fieldTerm (Field -> Term) -> Field -> Term
forall a b. (a -> b) -> a -> b
$ [Field] -> Field
forall a. HasCallStack => [a] -> a
L.head [Field]
matchingFields
      EliminationUnion (CaseStatement Name
name Maybe Term
def [Field]
fields) -> do
        Field
field <- Name -> Term -> Flow s Field
forall s. Name -> Term -> Flow s Field
Expect.injectionWithName Name
name Term
reducedArg
        let matchingFields :: [Field]
matchingFields = (Field -> Bool) -> [Field] -> [Field]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (\Field
f -> Field -> Name
fieldName Field
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Field -> Name
fieldName Field
field) [Field]
fields
        if [Field] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Field]
matchingFields
          then case Maybe Term
def of
            Just Term
d -> Term -> Flow s Term
forall a. a -> Flow s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
d
            Maybe Term
Nothing -> String -> Flow s Term
forall a. String -> Flow s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow s Term) -> String -> Flow s Term
forall a b. (a -> b) -> a -> b
$ String
"no such field " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName (Field -> Name
fieldName Field
field) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" case statement"
          else Term -> Flow s Term
forall a. a -> Flow s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Flow s Term) -> Term -> Flow s Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Terms.apply (Field -> Term
fieldTerm (Field -> Term) -> Field -> Term
forall a b. (a -> b) -> a -> b
$ [Field] -> Field
forall a. HasCallStack => [a] -> a
L.head [Field]
matchingFields) (Field -> Term
fieldTerm Field
field)
      EliminationWrap Name
name -> Name -> Term -> Flow s Term
forall s. Name -> Term -> Flow s Term
Expect.wrap Name
name Term
reducedArg

-- 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 :: Type -> Flow Graph (Type)
betaReduceType :: Type -> Flow Graph Type
betaReduceType Type
typ = do
    Graph
g <- Flow Graph Graph
forall s. Flow s s
getState :: Flow Graph Graph
    ((Type -> Flow Graph Type) -> Type -> Flow Graph Type)
-> Type -> Flow Graph Type
forall s.
((Type -> Flow s Type) -> Type -> Flow s Type)
-> Type -> Flow s Type
rewriteTypeM (Type -> Flow Graph Type) -> Type -> Flow Graph Type
forall {t}. (t -> Flow Graph Type) -> t -> Flow Graph Type
mapExpr Type
typ
  where
    mapExpr :: (t -> Flow Graph Type) -> t -> Flow Graph Type
mapExpr t -> Flow Graph Type
recurse t
t = do
        Type
r <- t -> Flow Graph Type
recurse t
t
        case Type
r of
          TypeApplication ApplicationType
a -> ApplicationType -> Flow Graph Type
reduceApp ApplicationType
a
          Type
t' -> Type -> Flow Graph Type
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t'
      where
        reduceApp :: ApplicationType -> Flow Graph Type
reduceApp (ApplicationType Type
lhs Type
rhs) = case Type
lhs of
          TypeAnnotated (AnnotatedType Type
t' Map Name Term
ann) -> do
            Type
a <- ApplicationType -> Flow Graph Type
reduceApp (ApplicationType -> Flow Graph Type)
-> ApplicationType -> Flow Graph Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> ApplicationType
ApplicationType Type
t' Type
rhs
            Type -> Flow Graph Type
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Flow Graph Type) -> Type -> Flow Graph Type
forall a b. (a -> b) -> a -> b
$ AnnotatedType -> Type
TypeAnnotated (AnnotatedType -> Type) -> AnnotatedType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Map Name Term -> AnnotatedType
AnnotatedType Type
a Map Name Term
ann
          TypeLambda (LambdaType Name
v Type
body) -> Type -> Flow Graph Type
betaReduceType (Type -> Flow Graph Type) -> Type -> Flow Graph Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Type -> Type
replaceFreeName Name
v Type
rhs Type
body
          -- nominal types are transparent
          TypeVariable Name
name -> do
            Type
t' <- Name -> Flow Graph Type
requireType Name
name
            Type -> Flow Graph Type
betaReduceType (Type -> Flow Graph Type) -> Type -> Flow Graph Type
forall a b. (a -> b) -> a -> b
$ ApplicationType -> Type
TypeApplication (ApplicationType -> Type) -> ApplicationType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> ApplicationType
ApplicationType Type
t' Type
rhs

-- | 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 :: Term -> Term
contractTerm :: Term -> Term
contractTerm = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
forall {p}. (p -> Term) -> p -> Term
rewrite
  where
    rewrite :: (p -> Term) -> p -> Term
rewrite p -> Term
recurse p
term = case Term
rec of
        TermApplication (Application Term
lhs Term
rhs) -> case Term -> Term
fullyStripTerm Term
lhs of
          TermFunction (FunctionLambda (Lambda Name
v Maybe Type
_ Term
body)) -> if Name -> Term -> Bool
isFreeIn Name
v Term
body
            then Term
body
            else Name -> Term -> Term -> Term
alphaConvert Name
v Term
rhs Term
body
          Term
_ -> Term
rec
        Term
_ -> Term
rec
      where
        rec :: Term
rec = p -> Term
recurse p
term

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

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

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

    functionIsValue :: Function -> Bool
functionIsValue Function
f = case Function
f of
      FunctionElimination Elimination
e -> case Elimination
e of
        EliminationWrap Name
_ -> Bool
True
        EliminationOptional (OptionalCases Term
nothing Term
just) -> Graph -> Term -> Bool
termIsValue Graph
g Term
nothing
          Bool -> Bool -> Bool
&& Graph -> Term -> Bool
termIsValue Graph
g Term
just
        EliminationRecord Projection
_ -> Bool
True
        EliminationUnion (CaseStatement Name
_ Maybe Term
def [Field]
cases) -> [Field] -> Bool
checkFields [Field]
cases Bool -> Bool -> Bool
&& (Bool -> (Term -> Bool) -> Maybe Term -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
Y.maybe Bool
True (Graph -> Term -> Bool
termIsValue Graph
g) Maybe Term
def)
      FunctionLambda (Lambda Name
_ Maybe Type
_ Term
body) -> Graph -> Term -> Bool
termIsValue Graph
g Term
body
      FunctionPrimitive Name
_ -> Bool
True