-- | Functions for type and term rewriting

module Hydra.Rewriting where

import Hydra.Basics
import Hydra.Strip
import Hydra.Coders
import Hydra.Compute
import Hydra.Core
import Hydra.CoreEncoding
import Hydra.Extras
import Hydra.Graph
import Hydra.Module
import Hydra.Lexical
import Hydra.Mantle
import Hydra.Tools.Sorting
import Hydra.Tier1
import Hydra.Tier2
import Hydra.Tools.Debug

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


-- beneathTermAnnotations :: (Term -> Term) -> Term -> Term
-- beneathTermAnnotations f term = case term of
--   TermAnnotated (AnnotatedTerm term1 ann) ->
--     TermAnnotated (AnnotatedTerm (beneathTermAnnotations f term1) ann)
--   TermTyped (TypedTerm term1 typ) ->
--     TermTyped $ TypedTerm (beneathTermAnnotations f term1) typ
--   _ -> f term
--
-- beneathTermAnnotationsM :: (Term -> Flow s Term) -> Term -> Flow s Term
-- beneathTermAnnotationsM f term = case term of
--   TermAnnotated (AnnotatedTerm term1 ann) ->
--     TermAnnotated <$> (AnnotatedTerm <$> beneathTermAnnotationsM f term1 <*> pure ann)
--   TermTyped (TypedTerm term1 typ) ->
--     TermTyped <$> (TypedTerm <$> beneathTermAnnotationsM f term1 <*> pure typ)
--   _ -> f term

-- | Apply a transformation to the first type beneath a chain of annotations
beneathTypeAnnotations :: (Type -> Type) -> Type -> Type
beneathTypeAnnotations :: (Type -> Type) -> Type -> Type
beneathTypeAnnotations Type -> Type
f Type
t = case Type
t of
  TypeAnnotated (AnnotatedType Type
t1 Map Name Term
ann) -> AnnotatedType -> Type
TypeAnnotated (Type -> Map Name Term -> AnnotatedType
AnnotatedType ((Type -> Type) -> Type -> Type
beneathTypeAnnotations Type -> Type
f Type
t1) Map Name Term
ann)
  Type
_ -> Type -> Type
f Type
t

elementsWithDependencies :: [Element] -> Flow Graph [Element]
elementsWithDependencies :: [Element] -> Flow Graph [Element]
elementsWithDependencies [Element]
original = (Name -> Flow Graph Element) -> [Name] -> Flow Graph [Element]
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 Name -> Flow Graph Element
requireElement [Name]
allDepNames
  where
    depNames :: Element -> [Name]
depNames = Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> [Name]) -> (Element -> Set Name) -> Element -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool -> Bool -> Term -> Set Name
termDependencyNames Bool
True Bool
False Bool
False (Term -> Set Name) -> (Element -> Term) -> Element -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Element -> Term
elementData
    allDepNames :: [Name]
allDepNames = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Element -> Name
elementName (Element -> Name) -> [Element] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Element]
original) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ([[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ([[Name]] -> [Name]) -> [[Name]] -> [Name]
forall a b. (a -> b) -> a -> b
$ Element -> [Name]
depNames (Element -> [Name]) -> [Element] -> [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Element]
original)

-- | Recursively transform arbitrary terms like 'add 42' into terms like '\x.add 42 x',
--   whose arity (in the absence of application terms) is equal to the depth of nested lambdas.
--   This is useful for targets like Java with weaker support for currying.
expandTypedLambdas :: Term -> Term
expandTypedLambdas :: Term -> Term
expandTypedLambdas = ((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 -> Maybe ([Type], Type)
getFunType Term
term of
        Maybe ([Type], Type)
Nothing -> Term -> Term
recurse Term
term
        Just ([Type]
doms, Type
cod) -> [Type] -> Type -> Term -> Term
expand [Type]
doms Type
cod Term
term
      where
        toNaryFunType :: Type -> ([Type], Type)
toNaryFunType Type
typ = case Type -> Type
stripType Type
typ of
          TypeFunction (FunctionType Type
dom0 Type
cod0) -> (Type
dom0 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
doms, Type
cod1)
            where
              ([Type]
doms, Type
cod1) = Type -> ([Type], Type)
toNaryFunType Type
cod0
          Type
d -> ([], Type
d)
        getFunType :: Term -> Maybe ([Type], Type)
getFunType Term
term = Type -> ([Type], Type)
toNaryFunType (Type -> ([Type], Type)) -> Maybe Type -> Maybe ([Type], Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Type
getTermType Term
term

        expand :: [Type] -> Type -> Term -> Term
expand [Type]
doms Type
cod Term
term = case Term
term of
          TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
ann) -> AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> AnnotatedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm ([Type] -> Type -> Term -> Term
expand [Type]
doms Type
cod Term
term1) Map Name Term
ann
          TermApplication (Application Term
lhs Term
rhs) -> case Term -> Maybe Type
getTermType Term
rhs of
            Maybe Type
Nothing -> Term -> Term
recurse Term
term
            Just Type
typ -> Application -> Term
TermApplication (Application -> Term) -> Application -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Application
Application ([Type] -> Type -> Term -> Term
expand (Type
typType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
doms) Type
cod Term
lhs) (Term -> Application) -> Term -> Application
forall a b. (a -> b) -> a -> b
$ Term -> Term
expandTypedLambdas Term
rhs
          TermFunction Function
f -> case Function
f of
            FunctionLambda (Lambda Name
var Maybe Type
d Term
body) -> Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Lambda Name
var Maybe Type
d (Term -> Lambda) -> Term -> Lambda
forall a b. (a -> b) -> a -> b
$
              [Type] -> Type -> Term -> Term
expand ([Type] -> [Type]
forall a. HasCallStack => [a] -> [a]
L.tail [Type]
doms) Type
cod Term
body
            Function
_ -> Integer -> [Type] -> Type -> Term -> Term
forall {t}. (Num t, Show t) => t -> [Type] -> Type -> Term -> Term
pad Integer
1 [Type]
doms Type
cod Term
term
          TermLet (Let [LetBinding]
bindings Term
env) -> Let -> Term
TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Let (LetBinding -> LetBinding
expandBinding (LetBinding -> LetBinding) -> [LetBinding] -> [LetBinding]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings) (Term -> Let) -> Term -> Let
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> Term -> Term
expand [Type]
doms Type
cod Term
env
            where
              expandBinding :: LetBinding -> LetBinding
expandBinding (LetBinding Name
name Term
term1 Maybe TypeScheme
typ) = Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
name (Term -> Term
expandTypedLambdas Term
term1) Maybe TypeScheme
typ
          TermTyped (TypedTerm Term
term1 Type
typ) -> TypedTerm -> Term
TermTyped (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
TypedTerm ([Type] -> Type -> Term -> Term
expand [Type]
doms Type
cod Term
term1) Type
typ
          Term
_ -> Term -> Term
recurse Term
term

        pad :: t -> [Type] -> Type -> Term -> Term
pad t
i [Type]
doms Type
cod Term
term = if [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Type]
doms
            then Term
term
            else Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Lambda Name
var (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
dom) (Term -> Lambda) -> Term -> Lambda
forall a b. (a -> b) -> a -> b
$
              t -> [Type] -> Type -> Term -> Term
pad (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) ([Type] -> [Type]
forall a. HasCallStack => [a] -> [a]
L.tail [Type]
doms) Type
cod (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
              -- TODO: omit this type annotation if practical; a type annotation on application terms
              --       shouldn't really be necessary.
              Type -> Term -> Term
typed ([Type] -> Type -> Type
forall {t :: * -> *}. Foldable t => t Type -> Type -> Type
toFunctionType ([Type] -> [Type]
forall a. HasCallStack => [a] -> [a]
L.tail [Type]
doms) Type
cod) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
              Application -> Term
TermApplication (Application -> Term) -> Application -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Application
Application (Type -> Term -> Term
typed ([Type] -> Type -> Type
forall {t :: * -> *}. Foldable t => t Type -> Type -> Type
toFunctionType [Type]
doms Type
cod) Term
term) (Term -> Application) -> Term -> Application
forall a b. (a -> b) -> a -> b
$ Name -> Term
TermVariable Name
var
          where
            dom :: Type
dom = [Type] -> Type
forall a. HasCallStack => [a] -> a
L.head [Type]
doms
            typed :: Type -> Term -> Term
typed Type
typ Term
term = TypedTerm -> Term
TermTyped (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
TypedTerm Term
term Type
typ
            toFunctionType :: t Type -> Type -> Type
toFunctionType t Type
doms Type
cod = (Type -> Type -> Type) -> Type -> t Type -> Type
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 (\Type
c Type
d -> FunctionType -> Type
TypeFunction (FunctionType -> Type) -> FunctionType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> FunctionType
FunctionType Type
d Type
c) Type
cod t Type
doms
            var :: Name
var = String -> Name
Name (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"v" String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i

flattenLetTerms :: Term -> Term
flattenLetTerms :: Term -> Term
flattenLetTerms = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
forall {t}. (t -> Term) -> t -> Term
flatten
  where
    flatten :: (t -> Term) -> t -> Term
flatten t -> Term
recurse t
term = case t -> Term
recurse t
term of
      TermLet (Let [LetBinding]
bindings Term
body) -> Let -> Term
TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Let [LetBinding]
newBindings Term
body
        where
          newBindings :: [LetBinding]
newBindings = [[LetBinding]] -> [LetBinding]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((LetBinding, [LetBinding]) -> [LetBinding]
forall {a}. (a, [a]) -> [a]
forResult ((LetBinding, [LetBinding]) -> [LetBinding])
-> (LetBinding -> (LetBinding, [LetBinding]))
-> LetBinding
-> [LetBinding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> (LetBinding, [LetBinding])
rewriteBinding (LetBinding -> [LetBinding]) -> [LetBinding] -> [[LetBinding]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings)
            where
              forResult :: (a, [a]) -> [a]
forResult (a
h, [a]
rest) = (a
ha -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rest)
          rewriteBinding :: LetBinding -> (LetBinding, [LetBinding])
rewriteBinding (LetBinding Name
k0 Term
v0 Maybe TypeScheme
t) = case Term
v0 of
            TermAnnotated (AnnotatedTerm Term
v1 Map Name Term
ann) -> ((Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k0 (AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> AnnotatedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm Term
v2 Map Name Term
ann) Maybe TypeScheme
t), [LetBinding]
deps)
              where
                ((LetBinding Name
_ Term
v2 Maybe TypeScheme
_), [LetBinding]
deps) = LetBinding -> (LetBinding, [LetBinding])
rewriteBinding (Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k0 Term
v1 Maybe TypeScheme
t)
            TermLet (Let [LetBinding]
bindings1 Term
body1) -> ((Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k0 Term
newBody Maybe TypeScheme
t), LetBinding -> LetBinding
newBinding (LetBinding -> LetBinding) -> [LetBinding] -> [LetBinding]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings1)
              where
                newBody :: Term
newBody = Term -> Term
replaceVars Term
body1
                newBinding :: LetBinding -> LetBinding
newBinding (LetBinding Name
kn Term
vn Maybe TypeScheme
t) = Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding (Name -> Name
qualify Name
kn) (Term -> Term
replaceVars Term
vn) Maybe TypeScheme
t
                qualify :: Name -> Name
qualify Name
n = String -> Name
Name (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
n
                replaceVars :: Term -> Term
replaceVars = Map Name Name -> Term -> Term
substituteVariables Map Name Name
subst
                subst :: Map Name Name
subst = [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (LetBinding -> (Name, Name)
toSubstPair (LetBinding -> (Name, Name)) -> [LetBinding] -> [(Name, Name)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings1)
                  where
                    toSubstPair :: LetBinding -> (Name, Name)
toSubstPair (LetBinding Name
n Term
_ Maybe TypeScheme
_) = (Name
n, Name -> Name
qualify Name
n)
                prefix :: String
prefix = Name -> String
unName Name
k0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_"
            Term
v1 -> ((Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k0 Term
v1 Maybe TypeScheme
t), [])
      Term
term0 -> Term
term0

freeVariablesInScheme :: TypeScheme -> S.Set Name
freeVariablesInScheme :: TypeScheme -> Set Name
freeVariablesInScheme (TypeScheme [Name]
vars Type
t) = Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.difference (Type -> Set Name
freeVariablesInType Type
t) ([Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList [Name]
vars)

-- | Inline all type variables in a type using the provided schema.
--   Note: this function is only appropriate for nonrecursive type definitions.
inlineType :: M.Map Name Type -> Type -> Flow s Type
inlineType :: forall s. Map Name Type -> Type -> Flow s Type
inlineType Map Name Type
schema = ((Type -> Flow s Type) -> Type -> Flow s Type)
-> Type -> Flow s Type
forall s.
((Type -> Flow s Type) -> Type -> Flow s Type)
-> Type -> Flow s Type
rewriteTypeM (Type -> Flow s Type) -> Type -> Flow s Type
forall {t} {s}. (t -> Flow s Type) -> t -> Flow s Type
f
  where
    f :: (t -> Flow s Type) -> t -> Flow s Type
f t -> Flow s Type
recurse t
typ = do
      Type
tr <- t -> Flow s Type
recurse t
typ
      case Type
tr of
        TypeVariable Name
v -> case Name -> Map Name Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v Map Name Type
schema of
          Just Type
t -> Map Name Type -> Type -> Flow s Type
forall s. Map Name Type -> Type -> Flow s Type
inlineType Map Name Type
schema Type
t
          Maybe Type
Nothing -> String -> Flow s Type
forall a. String -> Flow s a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow s Type) -> String -> Flow s Type
forall a b. (a -> b) -> a -> b
$ String
"No such type in schema: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
v
        Type
t -> Type -> Flow s Type
forall a. a -> Flow s a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t

isFreeIn :: Name -> Term -> Bool
isFreeIn :: Name -> Term -> Bool
isFreeIn Name
v Term
term = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Name
v (Set Name -> Bool) -> Set Name -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Set Name
freeVariablesInTerm Term
term

-- | Recursively remove term annotations, including within subterms
removeTermAnnotations :: Term -> Term
removeTermAnnotations :: Term -> Term
removeTermAnnotations = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
forall {t}. (t -> Term) -> t -> Term
remove
  where
    remove :: (t -> Term) -> t -> Term
remove t -> Term
recurse t
term = case t -> Term
recurse t
term of
      TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
_) -> Term
term1
      TermTyped (TypedTerm Term
term1 Type
_) -> Term
term1
      Term
t -> Term
t

-- | Recursively remove type annotations, including within subtypes
removeTypeAnnotations :: Type -> Type
removeTypeAnnotations :: Type -> Type
removeTypeAnnotations = ((Type -> Type) -> Type -> Type) -> Type -> Type
rewriteType (Type -> Type) -> Type -> Type
forall {t}. (t -> Type) -> t -> Type
remove
  where
    remove :: (t -> Type) -> t -> Type
remove t -> Type
recurse t
typ = case t -> Type
recurse t
typ of
      TypeAnnotated (AnnotatedType Type
typ' Map Name Term
_) -> Type
typ'
      Type
t -> Type
t

replaceFreeName :: Name -> Type -> Type -> Type
replaceFreeName :: Name -> Type -> Type -> Type
replaceFreeName Name
v Type
rep = ((Type -> Type) -> Type -> Type) -> Type -> Type
rewriteType (Type -> Type) -> Type -> Type
mapExpr
  where
    mapExpr :: (Type -> Type) -> Type -> Type
mapExpr Type -> Type
recurse Type
t = case Type
t of
      TypeLambda (LambdaType Name
v' Type
body) -> if Name
v Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
v'
        then Type
t
        else LambdaType -> Type
TypeLambda (LambdaType -> Type) -> LambdaType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> LambdaType
LambdaType Name
v' (Type -> LambdaType) -> Type -> LambdaType
forall a b. (a -> b) -> a -> b
$ Type -> Type
recurse Type
body
      TypeVariable Name
v' -> if Name
v Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
v' then Type
rep else Type
t
      Type
_ -> Type -> Type
recurse Type
t

rewrite :: ((x -> y) -> x -> y) -> ((x -> y) -> x -> y) -> x -> y
rewrite :: forall x y. ((x -> y) -> x -> y) -> ((x -> y) -> x -> y) -> x -> y
rewrite (x -> y) -> x -> y
fsub (x -> y) -> x -> y
f = x -> y
recurse
  where
    recurse :: x -> y
recurse = (x -> y) -> x -> y
f ((x -> y) -> x -> y
fsub x -> y
recurse)

rewriteTerm :: ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm :: ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
f = ((Term -> Term) -> Term -> Term)
-> ((Term -> Term) -> Term -> Term) -> Term -> Term
forall x y. ((x -> y) -> x -> y) -> ((x -> y) -> x -> y) -> x -> y
rewrite (Term -> Term) -> Term -> Term
fsub (Term -> Term) -> Term -> Term
f
  where
    fsub :: (Term -> Term) -> Term -> Term
fsub Term -> Term
recurse Term
term = case Term
term of
        TermAnnotated (AnnotatedTerm Term
ex Map Name Term
ann) -> AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> AnnotatedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm (Term -> Term
recurse Term
ex) Map Name Term
ann
        TermApplication (Application Term
lhs Term
rhs) -> Application -> Term
TermApplication (Application -> Term) -> Application -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Application
Application (Term -> Term
recurse Term
lhs) (Term -> Term
recurse Term
rhs)
        TermFunction Function
fun -> Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ case Function
fun of
          FunctionElimination Elimination
e -> Elimination -> Function
FunctionElimination (Elimination -> Function) -> Elimination -> Function
forall a b. (a -> b) -> a -> b
$ case Elimination
e of
            EliminationList Term
fld -> Term -> Elimination
EliminationList (Term -> Elimination) -> Term -> Elimination
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse Term
fld
            EliminationOptional (OptionalCases Term
nothing Term
just) -> OptionalCases -> Elimination
EliminationOptional
              (Term -> Term -> OptionalCases
OptionalCases (Term -> Term
recurse Term
nothing) (Term -> Term
recurse Term
just))
            EliminationProduct TupleProjection
tp -> TupleProjection -> Elimination
EliminationProduct TupleProjection
tp
            EliminationRecord Projection
p -> Projection -> Elimination
EliminationRecord Projection
p
            EliminationUnion (CaseStatement Name
n Maybe Term
def [Field]
cases) -> CaseStatement -> Elimination
EliminationUnion (CaseStatement -> Elimination) -> CaseStatement -> Elimination
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Term -> [Field] -> CaseStatement
CaseStatement Name
n (Term -> Term
recurse (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Term
def) (Field -> Field
forField (Field -> Field) -> [Field] -> [Field]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Field]
cases)
            EliminationWrap Name
name -> Name -> Elimination
EliminationWrap Name
name
          FunctionLambda (Lambda Name
v Maybe Type
d Term
body) -> Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Lambda Name
v Maybe Type
d (Term -> Lambda) -> Term -> Lambda
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse Term
body
          FunctionPrimitive Name
name -> Name -> Function
FunctionPrimitive Name
name
        TermLet (Let [LetBinding]
bindings Term
env) -> Let -> Term
TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Let (LetBinding -> LetBinding
mapBinding (LetBinding -> LetBinding) -> [LetBinding] -> [LetBinding]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings) (Term -> Term
recurse Term
env)
          where
            mapBinding :: LetBinding -> LetBinding
mapBinding (LetBinding Name
k Term
v Maybe TypeScheme
t) = Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k (Term -> Term
recurse Term
v) Maybe TypeScheme
t
        TermList [Term]
els -> [Term] -> Term
TermList ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse (Term -> Term) -> [Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
els
        TermLiteral Literal
v -> Literal -> Term
TermLiteral Literal
v
        TermMap Map Term Term
m -> Map Term Term -> Term
TermMap (Map Term Term -> Term) -> Map Term Term -> Term
forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Map Term Term
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Term, Term)] -> Map Term Term)
-> [(Term, Term)] -> Map Term Term
forall a b. (a -> b) -> a -> b
$ (\(Term
k, Term
v) -> (Term -> Term
recurse Term
k, Term -> Term
recurse Term
v)) ((Term, Term) -> (Term, Term)) -> [(Term, Term)] -> [(Term, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Term Term -> [(Term, Term)]
forall k a. Map k a -> [(k, a)]
M.toList Map Term Term
m
        TermWrap (WrappedTerm Name
name Term
t) -> WrappedTerm -> Term
TermWrap (Name -> Term -> WrappedTerm
WrappedTerm Name
name (Term -> WrappedTerm) -> Term -> WrappedTerm
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse Term
t)
        TermOptional Maybe Term
m -> Maybe Term -> Term
TermOptional (Maybe Term -> Term) -> Maybe Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Term
m
        TermProduct [Term]
tuple -> [Term] -> Term
TermProduct (Term -> Term
recurse (Term -> Term) -> [Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
tuple)
        TermRecord (Record Name
n [Field]
fields) -> Record -> Term
TermRecord (Record -> Term) -> Record -> Term
forall a b. (a -> b) -> a -> b
$ Name -> [Field] -> Record
Record Name
n ([Field] -> Record) -> [Field] -> Record
forall a b. (a -> b) -> a -> b
$ Field -> Field
forField (Field -> Field) -> [Field] -> [Field]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Field]
fields
        TermSet Set Term
s -> Set Term -> Term
TermSet (Set Term -> Term) -> Set Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Set Term
forall a. Ord a => [a] -> Set a
S.fromList ([Term] -> Set Term) -> [Term] -> Set Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse (Term -> Term) -> [Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Term -> [Term]
forall a. Set a -> [a]
S.toList Set Term
s
        TermSum (Sum Int
i Int
s Term
trm) -> Sum -> Term
TermSum (Sum -> Term) -> Sum -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Term -> Sum
Sum Int
i Int
s (Term -> Sum) -> Term -> Sum
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse Term
trm
        TermTypeAbstraction (TypeAbstraction Name
v Term
t) -> TypeAbstraction -> Term
TermTypeAbstraction (TypeAbstraction -> Term) -> TypeAbstraction -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> TypeAbstraction
TypeAbstraction Name
v (Term -> TypeAbstraction) -> Term -> TypeAbstraction
forall a b. (a -> b) -> a -> b
$ Term -> Term
recurse Term
t
        TermTypeApplication (TypedTerm Term
term1 Type
type2) -> TypedTerm -> Term
TermTypeApplication (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
TypedTerm (Term -> Term
recurse Term
term1) Type
type2
        TermTyped (TypedTerm Term
term1 Type
type2) -> TypedTerm -> Term
TermTyped (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
TypedTerm (Term -> Term
recurse Term
term1) Type
type2
        TermUnion (Injection Name
n Field
field) -> Injection -> Term
TermUnion (Injection -> Term) -> Injection -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Field -> Injection
Injection Name
n (Field -> Injection) -> Field -> Injection
forall a b. (a -> b) -> a -> b
$ Field -> Field
forField Field
field
        TermVariable Name
v -> Name -> Term
TermVariable Name
v
      where
        forField :: Field -> Field
forField Field
f = Field
f {fieldTerm = recurse (fieldTerm f)}

rewriteTermM ::
  ((Term -> Flow s Term) -> Term -> (Flow s Term)) -> Term -> Flow s Term
rewriteTermM :: forall s.
((Term -> Flow s Term) -> Term -> Flow s Term)
-> Term -> Flow s Term
rewriteTermM (Term -> Flow s Term) -> Term -> Flow s Term
f = ((Term -> Flow s Term) -> Term -> Flow s Term)
-> ((Term -> Flow s Term) -> Term -> Flow s Term)
-> Term
-> Flow s Term
forall x y. ((x -> y) -> x -> y) -> ((x -> y) -> x -> y) -> x -> y
rewrite (Term -> Flow s Term) -> Term -> Flow s Term
forall {f :: * -> *}. Monad f => (Term -> f Term) -> Term -> f Term
fsub (Term -> Flow s Term) -> Term -> Flow s Term
f
  where
    fsub :: (Term -> f Term) -> Term -> f Term
fsub Term -> f Term
recurse Term
term = case Term
term of
        TermAnnotated (AnnotatedTerm Term
ex Map Name Term
ma) -> AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> f AnnotatedTerm -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm (Term -> Map Name Term -> AnnotatedTerm)
-> f Term -> f (Map Name Term -> AnnotatedTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
ex f (Map Name Term -> AnnotatedTerm)
-> f (Map Name Term) -> f AnnotatedTerm
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Name Term -> f (Map Name Term)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Name Term
ma)
        TermApplication (Application Term
lhs Term
rhs) -> Application -> Term
TermApplication (Application -> Term) -> f Application -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Term -> Application
Application (Term -> Term -> Application) -> f Term -> f (Term -> Application)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
lhs f (Term -> Application) -> f Term -> f Application
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> f Term
recurse Term
rhs)
        TermFunction Function
fun -> Function -> Term
TermFunction (Function -> Term) -> f Function -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Function
fun of
          FunctionElimination Elimination
e -> Elimination -> Function
FunctionElimination (Elimination -> Function) -> f Elimination -> f Function
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Elimination
e of
            EliminationList Term
fld -> Term -> Elimination
EliminationList (Term -> Elimination) -> f Term -> f Elimination
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
fld
            EliminationOptional (OptionalCases Term
nothing Term
just) -> OptionalCases -> Elimination
EliminationOptional (OptionalCases -> Elimination) -> f OptionalCases -> f Elimination
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
              (Term -> Term -> OptionalCases
OptionalCases (Term -> Term -> OptionalCases)
-> f Term -> f (Term -> OptionalCases)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
nothing f (Term -> OptionalCases) -> f Term -> f OptionalCases
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> f Term
recurse Term
just)
            EliminationProduct TupleProjection
tp -> Elimination -> f Elimination
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elimination -> f Elimination) -> Elimination -> f Elimination
forall a b. (a -> b) -> a -> b
$ TupleProjection -> Elimination
EliminationProduct TupleProjection
tp
            EliminationRecord Projection
p -> Elimination -> f Elimination
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elimination -> f Elimination) -> Elimination -> f Elimination
forall a b. (a -> b) -> a -> b
$ Projection -> Elimination
EliminationRecord Projection
p
            EliminationUnion (CaseStatement Name
n Maybe Term
def [Field]
cases) -> do
              Maybe Term
rdef <- case Maybe Term
def of
                Maybe Term
Nothing -> Maybe Term -> f (Maybe Term)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Term
forall a. Maybe a
Nothing
                Just Term
t -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> f Term -> f (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
t
              CaseStatement -> Elimination
EliminationUnion (CaseStatement -> Elimination) -> f CaseStatement -> f Elimination
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Maybe Term -> [Field] -> CaseStatement
CaseStatement Name
n Maybe Term
rdef ([Field] -> CaseStatement) -> f [Field] -> f CaseStatement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Field -> f Field) -> [Field] -> f [Field]
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 Field -> f Field
forField [Field]
cases))
            EliminationWrap Name
name -> Elimination -> f Elimination
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Elimination -> f Elimination) -> Elimination -> f Elimination
forall a b. (a -> b) -> a -> b
$ Name -> Elimination
EliminationWrap Name
name
          FunctionLambda (Lambda Name
v Maybe Type
d Term
body) -> Lambda -> Function
FunctionLambda (Lambda -> Function) -> f Lambda -> f Function
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Maybe Type -> Term -> Lambda
Lambda Name
v Maybe Type
d (Term -> Lambda) -> f Term -> f Lambda
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
body)
          FunctionPrimitive Name
name -> Function -> f Function
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Function -> f Function) -> Function -> f Function
forall a b. (a -> b) -> a -> b
$ Name -> Function
FunctionPrimitive Name
name
        TermLet (Let [LetBinding]
bindings Term
env) -> Let -> Term
TermLet (Let -> Term) -> f Let -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([LetBinding] -> Term -> Let
Let ([LetBinding] -> Term -> Let) -> f [LetBinding] -> f (Term -> Let)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((LetBinding -> f LetBinding) -> [LetBinding] -> f [LetBinding]
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 LetBinding -> f LetBinding
mapBinding [LetBinding]
bindings) f (Term -> Let) -> f Term -> f Let
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> f Term
recurse Term
env)
          where
            mapBinding :: LetBinding -> f LetBinding
mapBinding (LetBinding Name
k Term
v Maybe TypeScheme
t) = do
              Term
v' <- Term -> f Term
recurse Term
v
              LetBinding -> f LetBinding
forall a. a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return (LetBinding -> f LetBinding) -> LetBinding -> f LetBinding
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k Term
v' Maybe TypeScheme
t
        TermList [Term]
els -> [Term] -> Term
TermList ([Term] -> Term) -> f [Term] -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> f Term) -> [Term] -> f [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 Term -> f Term
recurse [Term]
els)
        TermLiteral Literal
v -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> f Term) -> Term -> f Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
TermLiteral Literal
v
        TermMap Map Term Term
m -> Map Term Term -> Term
TermMap (Map Term Term -> Term) -> f (Map Term Term) -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Term, Term)] -> Map Term Term
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Term, Term)] -> Map Term Term)
-> f [(Term, Term)] -> f (Map Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term, Term) -> f (Term, Term))
-> [(Term, Term)] -> f [(Term, 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 (Term, Term) -> f (Term, Term)
forPair (Map Term Term -> [(Term, Term)]
forall k a. Map k a -> [(k, a)]
M.toList Map Term Term
m))
          where
            forPair :: (Term, Term) -> f (Term, Term)
forPair (Term
k, Term
v) = do
              Term
km <- Term -> f Term
recurse Term
k
              Term
vm <- Term -> f Term
recurse Term
v
              (Term, Term) -> f (Term, Term)
forall a. a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
km, Term
vm)
        TermOptional Maybe Term
m -> Maybe Term -> Term
TermOptional (Maybe Term -> Term) -> f (Maybe Term) -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> f Term) -> Maybe Term -> f (Maybe 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) -> Maybe a -> m (Maybe b)
CM.mapM Term -> f Term
recurse Maybe Term
m)
        TermProduct [Term]
tuple -> [Term] -> Term
TermProduct ([Term] -> Term) -> f [Term] -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> f Term) -> [Term] -> f [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 Term -> f Term
recurse [Term]
tuple)
        TermRecord (Record Name
n [Field]
fields) -> Record -> Term
TermRecord (Record -> Term) -> f Record -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> [Field] -> Record
Record Name
n ([Field] -> Record) -> f [Field] -> f Record
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Field -> f Field) -> [Field] -> f [Field]
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 Field -> f Field
forField [Field]
fields))
        TermSet Set Term
s -> Set Term -> Term
TermSet (Set Term -> Term) -> f (Set Term) -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Term] -> Set Term
forall a. Ord a => [a] -> Set a
S.fromList ([Term] -> Set Term) -> f [Term] -> f (Set Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> f Term) -> [Term] -> f [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 Term -> f Term
recurse ([Term] -> f [Term]) -> [Term] -> f [Term]
forall a b. (a -> b) -> a -> b
$ Set Term -> [Term]
forall a. Set a -> [a]
S.toList Set Term
s))
        TermSum (Sum Int
i Int
s Term
trm) -> Sum -> Term
TermSum (Sum -> Term) -> f Sum -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Int -> Term -> Sum
Sum Int
i Int
s (Term -> Sum) -> f Term -> f Sum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
trm)
        TermTyped (TypedTerm Term
term1 Type
type2) -> TypedTerm -> Term
TermTyped (TypedTerm -> Term) -> f TypedTerm -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Type -> TypedTerm
TypedTerm (Term -> Type -> TypedTerm) -> f Term -> f (Type -> TypedTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
term1 f (Type -> TypedTerm) -> f Type -> f TypedTerm
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
type2)
        TermUnion (Injection Name
n Field
field) -> Injection -> Term
TermUnion (Injection -> Term) -> f Injection -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Field -> Injection
Injection Name
n (Field -> Injection) -> f Field -> f Injection
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field -> f Field
forField Field
field)
        TermVariable Name
v -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> f Term) -> Term -> f Term
forall a b. (a -> b) -> a -> b
$ Name -> Term
TermVariable Name
v
        TermWrap (WrappedTerm Name
name Term
t) -> WrappedTerm -> Term
TermWrap (WrappedTerm -> Term) -> f WrappedTerm -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Term -> WrappedTerm
WrappedTerm Name
name (Term -> WrappedTerm) -> f Term -> f WrappedTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Term
recurse Term
t)
      where
        forField :: Field -> f Field
forField Field
f = do
          Term
t <- Term -> f Term
recurse (Field -> Term
fieldTerm Field
f)
          Field -> f Field
forall a. a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return Field
f {fieldTerm = t}

rewriteTermMeta :: (M.Map Name Term -> M.Map Name Term) -> Term -> Term
rewriteTermMeta :: (Map Name Term -> Map Name Term) -> Term -> Term
rewriteTermMeta Map Name Term -> Map Name Term
mapping = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
forall {t}. (t -> Term) -> t -> Term
rewrite
  where
    rewrite :: (t -> Term) -> t -> Term
rewrite t -> Term
recurse t
term = case t -> Term
recurse t
term of
      TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
ann) -> AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> AnnotatedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm Term
term1 (Map Name Term -> AnnotatedTerm) -> Map Name Term -> AnnotatedTerm
forall a b. (a -> b) -> a -> b
$ Map Name Term -> Map Name Term
mapping Map Name Term
ann
      Term
t -> Term
t

rewriteTermMetaM :: (M.Map Name Term -> Flow s (M.Map Name Term)) -> Term -> Flow s Term
rewriteTermMetaM :: forall s.
(Map Name Term -> Flow s (Map Name Term)) -> Term -> Flow s Term
rewriteTermMetaM Map Name Term -> Flow s (Map Name Term)
mapping = ((Term -> Flow s Term) -> Term -> Flow s Term)
-> Term -> Flow s Term
forall s.
((Term -> Flow s Term) -> Term -> Flow s Term)
-> Term -> Flow s Term
rewriteTermM (Term -> Flow s Term) -> Term -> Flow s Term
forall {t}. (t -> Flow s Term) -> t -> Flow s Term
rewrite
  where
    rewrite :: (t -> Flow s Term) -> t -> Flow s Term
rewrite t -> Flow s Term
recurse t
term = do
      Term
r <- t -> Flow s Term
recurse t
term
      case Term
r of
        TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
ann) -> AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> Flow s AnnotatedTerm -> Flow s Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm (Term -> Map Name Term -> AnnotatedTerm)
-> Flow s Term -> Flow s (Map Name Term -> AnnotatedTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Flow s Term
forall a. a -> Flow s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
term1 Flow s (Map Name Term -> AnnotatedTerm)
-> Flow s (Map Name Term) -> Flow s AnnotatedTerm
forall a b. Flow s (a -> b) -> Flow s a -> Flow s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Name Term -> Flow s (Map Name Term)
mapping Map Name Term
ann)
        Term
t -> Term -> Flow s Term
forall a. a -> Flow s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
t

rewriteType :: ((Type -> Type) -> Type -> Type) -> Type -> Type
rewriteType :: ((Type -> Type) -> Type -> Type) -> Type -> Type
rewriteType (Type -> Type) -> Type -> Type
f = ((Type -> Type) -> Type -> Type)
-> ((Type -> Type) -> Type -> Type) -> Type -> Type
forall x y. ((x -> y) -> x -> y) -> ((x -> y) -> x -> y) -> x -> y
rewrite (Type -> Type) -> Type -> Type
fsub (Type -> Type) -> Type -> Type
f
  where
    fsub :: (Type -> Type) -> Type -> Type
fsub Type -> Type
recurse Type
typ = case Type
typ of
        TypeAnnotated (AnnotatedType Type
t Map Name Term
ann) -> AnnotatedType -> Type
TypeAnnotated (AnnotatedType -> Type) -> AnnotatedType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Map Name Term -> AnnotatedType
AnnotatedType (Type -> Type
recurse Type
t) Map Name Term
ann
        TypeApplication (ApplicationType Type
lhs Type
rhs) -> ApplicationType -> Type
TypeApplication (ApplicationType -> Type) -> ApplicationType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> ApplicationType
ApplicationType (Type -> Type
recurse Type
lhs) (Type -> Type
recurse Type
rhs)
        TypeFunction (FunctionType Type
dom Type
cod) -> FunctionType -> Type
TypeFunction (Type -> Type -> FunctionType
FunctionType (Type -> Type
recurse Type
dom) (Type -> Type
recurse Type
cod))
        TypeLambda (LambdaType Name
v Type
b) -> LambdaType -> Type
TypeLambda (Name -> Type -> LambdaType
LambdaType Name
v (Type -> LambdaType) -> Type -> LambdaType
forall a b. (a -> b) -> a -> b
$ Type -> Type
recurse Type
b)
        TypeList Type
t -> Type -> Type
TypeList (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
recurse Type
t
        TypeLiteral LiteralType
lt -> LiteralType -> Type
TypeLiteral LiteralType
lt
        TypeMap (MapType Type
kt Type
vt) -> MapType -> Type
TypeMap (Type -> Type -> MapType
MapType (Type -> Type
recurse Type
kt) (Type -> Type
recurse Type
vt))
        TypeOptional Type
t -> Type -> Type
TypeOptional (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
recurse Type
t
        TypeProduct [Type]
types -> [Type] -> Type
TypeProduct (Type -> Type
recurse (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
types)
        TypeRecord (RowType Name
name [FieldType]
fields) -> RowType -> Type
TypeRecord (RowType -> Type) -> RowType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> [FieldType] -> RowType
RowType Name
name (FieldType -> FieldType
forField (FieldType -> FieldType) -> [FieldType] -> [FieldType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType]
fields)
        TypeSet Type
t -> Type -> Type
TypeSet (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
recurse Type
t
        TypeSum [Type]
types -> [Type] -> Type
TypeSum (Type -> Type
recurse (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
types)
        TypeUnion (RowType Name
name [FieldType]
fields) -> RowType -> Type
TypeUnion (RowType -> Type) -> RowType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> [FieldType] -> RowType
RowType Name
name (FieldType -> FieldType
forField (FieldType -> FieldType) -> [FieldType] -> [FieldType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldType]
fields)
        TypeVariable Name
v -> Name -> Type
TypeVariable Name
v
        TypeWrap (WrappedType Name
name Type
t) -> WrappedType -> Type
TypeWrap (WrappedType -> Type) -> WrappedType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> WrappedType
WrappedType Name
name (Type -> WrappedType) -> Type -> WrappedType
forall a b. (a -> b) -> a -> b
$ Type -> Type
recurse Type
t
      where
        forField :: FieldType -> FieldType
forField FieldType
f = FieldType
f {fieldTypeType = recurse (fieldTypeType f)}

rewriteTypeM ::
  ((Type -> Flow s Type) -> Type -> (Flow s Type)) ->
  Type ->
  Flow s Type
rewriteTypeM :: forall s.
((Type -> Flow s Type) -> Type -> Flow s Type)
-> Type -> Flow s Type
rewriteTypeM (Type -> Flow s Type) -> Type -> Flow s Type
f = ((Type -> Flow s Type) -> Type -> Flow s Type)
-> ((Type -> Flow s Type) -> Type -> Flow s Type)
-> Type
-> Flow s Type
forall x y. ((x -> y) -> x -> y) -> ((x -> y) -> x -> y) -> x -> y
rewrite (Type -> Flow s Type) -> Type -> Flow s Type
forall {f :: * -> *}. Monad f => (Type -> f Type) -> Type -> f Type
fsub (Type -> Flow s Type) -> Type -> Flow s Type
f
  where
    fsub :: (Type -> f Type) -> Type -> f Type
fsub Type -> f Type
recurse Type
typ = case Type
typ of
        TypeAnnotated (AnnotatedType Type
t Map Name Term
ann) -> AnnotatedType -> Type
TypeAnnotated (AnnotatedType -> Type) -> f AnnotatedType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Map Name Term -> AnnotatedType
AnnotatedType (Type -> Map Name Term -> AnnotatedType)
-> f Type -> f (Map Name Term -> AnnotatedType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
t f (Map Name Term -> AnnotatedType)
-> f (Map Name Term) -> f AnnotatedType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Name Term -> f (Map Name Term)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map Name Term
ann)
        TypeApplication (ApplicationType Type
lhs Type
rhs) -> ApplicationType -> Type
TypeApplication (ApplicationType -> Type) -> f ApplicationType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Type -> ApplicationType
ApplicationType (Type -> Type -> ApplicationType)
-> f Type -> f (Type -> ApplicationType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
lhs f (Type -> ApplicationType) -> f Type -> f ApplicationType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> f Type
recurse Type
rhs)
        TypeFunction (FunctionType Type
dom Type
cod) -> FunctionType -> Type
TypeFunction (FunctionType -> Type) -> f FunctionType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Type -> FunctionType
FunctionType (Type -> Type -> FunctionType)
-> f Type -> f (Type -> FunctionType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
dom f (Type -> FunctionType) -> f Type -> f FunctionType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> f Type
recurse Type
cod)
        TypeLambda (LambdaType Name
v Type
b) -> LambdaType -> Type
TypeLambda (LambdaType -> Type) -> f LambdaType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Type -> LambdaType
LambdaType (Name -> Type -> LambdaType) -> f Name -> f (Type -> LambdaType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
v f (Type -> LambdaType) -> f Type -> f LambdaType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> f Type
recurse Type
b)
        TypeList Type
t -> Type -> Type
TypeList (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
t
        TypeLiteral LiteralType
lt -> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ LiteralType -> Type
TypeLiteral LiteralType
lt
        TypeMap (MapType Type
kt Type
vt) -> MapType -> Type
TypeMap (MapType -> Type) -> f MapType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Type -> MapType
MapType (Type -> Type -> MapType) -> f Type -> f (Type -> MapType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
kt f (Type -> MapType) -> f Type -> f MapType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> f Type
recurse Type
vt)
        TypeOptional Type
t -> Type -> Type
TypeOptional (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
t
        TypeProduct [Type]
types -> [Type] -> Type
TypeProduct ([Type] -> Type) -> f [Type] -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> [Type] -> f [Type]
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 Type -> f Type
recurse [Type]
types
        TypeRecord (RowType Name
name [FieldType]
fields) ->
          RowType -> Type
TypeRecord (RowType -> Type) -> f RowType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> [FieldType] -> RowType
RowType (Name -> [FieldType] -> RowType)
-> f Name -> f ([FieldType] -> RowType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
name f ([FieldType] -> RowType) -> f [FieldType] -> f RowType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (FieldType -> f FieldType) -> [FieldType] -> f [FieldType]
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 FieldType -> f FieldType
forField [FieldType]
fields)
        TypeSet Type
t -> Type -> Type
TypeSet (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Type
recurse Type
t
        TypeSum [Type]
types -> [Type] -> Type
TypeSum ([Type] -> Type) -> f [Type] -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> [Type] -> f [Type]
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 Type -> f Type
recurse [Type]
types
        TypeUnion (RowType Name
name [FieldType]
fields) ->
          RowType -> Type
TypeUnion (RowType -> Type) -> f RowType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> [FieldType] -> RowType
RowType (Name -> [FieldType] -> RowType)
-> f Name -> f ([FieldType] -> RowType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
name f ([FieldType] -> RowType) -> f [FieldType] -> f RowType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (FieldType -> f FieldType) -> [FieldType] -> f [FieldType]
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 FieldType -> f FieldType
forField [FieldType]
fields)
        TypeVariable Name
v -> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
v
        TypeWrap (WrappedType Name
name Type
t) -> WrappedType -> Type
TypeWrap (WrappedType -> Type) -> f WrappedType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Type -> WrappedType
WrappedType (Name -> Type -> WrappedType) -> f Name -> f (Type -> WrappedType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
name f (Type -> WrappedType) -> f Type -> f WrappedType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> f Type
recurse Type
t)
      where
        forField :: FieldType -> f FieldType
forField FieldType
f = do
          Type
t <- Type -> f Type
recurse (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ FieldType -> Type
fieldTypeType FieldType
f
          FieldType -> f FieldType
forall a. a -> f a
forall (m :: * -> *) a. Monad m => a -> m a
return FieldType
f {fieldTypeType = t}

rewriteTypeMeta :: (M.Map Name Term -> M.Map Name Term) -> Type -> Type
rewriteTypeMeta :: (Map Name Term -> Map Name Term) -> Type -> Type
rewriteTypeMeta Map Name Term -> Map Name Term
mapping = ((Type -> Type) -> Type -> Type) -> Type -> Type
rewriteType (Type -> Type) -> Type -> Type
forall {t}. (t -> Type) -> t -> Type
rewrite
  where
    rewrite :: (t -> Type) -> t -> Type
rewrite t -> Type
recurse t
typ = case t -> Type
recurse t
typ of
      TypeAnnotated (AnnotatedType Type
typ1 Map Name Term
ann) -> AnnotatedType -> Type
TypeAnnotated (AnnotatedType -> Type) -> AnnotatedType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Map Name Term -> AnnotatedType
AnnotatedType Type
typ1 (Map Name Term -> AnnotatedType) -> Map Name Term -> AnnotatedType
forall a b. (a -> b) -> a -> b
$ Map Name Term -> Map Name Term
mapping Map Name Term
ann
      Type
t -> Type
t

simplifyTerm :: Term -> Term
simplifyTerm :: Term -> Term
simplifyTerm = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
forall {b}. (Term -> b) -> Term -> b
simplify
  where
    simplify :: (Term -> b) -> Term -> b
simplify Term -> b
recurse Term
term = Term -> b
recurse (Term -> b) -> Term -> b
forall a b. (a -> b) -> a -> b
$ case Term -> Term
fullyStripTerm Term
term of
      TermApplication (Application Term
lhs Term
rhs) -> case Term -> Term
fullyStripTerm Term
lhs of
        TermFunction (FunctionLambda (Lambda Name
var Maybe Type
d Term
body)) ->
          if Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Name
var (Term -> Set Name
freeVariablesInTerm Term
body)
            then case Term -> Term
fullyStripTerm Term
rhs of
              TermVariable Name
v -> Term -> Term
simplifyTerm (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Name -> Term -> Term
substituteVariable Name
var Name
v Term
body
              Term
_ -> Term
term
            else Term -> Term
simplifyTerm Term
body
        Term
_ -> Term
term
      Term
_ -> Term
term

stripTermRecursive :: Term -> Term
stripTermRecursive :: Term -> Term
stripTermRecursive = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
forall {t}. (t -> Term) -> t -> Term
strip
  where
    strip :: (t -> Term) -> t -> Term
strip t -> Term
recurse t
term = case t -> Term
recurse t
term of
      TermAnnotated (AnnotatedTerm Term
t Map Name Term
_) -> Term
t
      TermTyped (TypedTerm Term
t Type
_) -> Term
t
      Term
t -> Term
t

substituteVariable :: Name -> Name -> Term -> Term
substituteVariable :: Name -> Name -> Term -> Term
substituteVariable Name
from Name
to = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
replace
  where
    replace :: (Term -> Term) -> Term -> Term
replace Term -> Term
recurse Term
term = case Term
term of
      TermVariable Name
x -> (Name -> Term
TermVariable (Name -> Term) -> Name -> Term
forall a b. (a -> b) -> a -> b
$ if Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
from then Name
to else Name
x)
      TermFunction (FunctionLambda (Lambda Name
var Maybe Type
_ Term
_)) -> if Name
var Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
from
        then Term
term
        else Term -> Term
recurse Term
term
      Term
_ -> Term -> Term
recurse Term
term

substituteVariables :: M.Map Name Name -> Term -> Term
substituteVariables :: Map Name Name -> Term -> Term
substituteVariables Map Name Name
subst = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (Term -> Term) -> Term -> Term
replace
  where
    replace :: (Term -> Term) -> Term -> Term
replace Term -> Term
recurse Term
term = case Term
term of
      TermVariable Name
n -> Name -> Term
TermVariable (Name -> Term) -> Name -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
Y.fromMaybe Name
n (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Map Name Name
subst
      TermFunction (FunctionLambda (Lambda Name
v Maybe Type
_ Term
_ )) -> case Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v Map Name Name
subst of
        Maybe Name
Nothing -> Term -> Term
recurse Term
term
        Just Name
_ -> Term
term
      Term
_ -> Term -> Term
recurse Term
term

-- Note: does not distinguish between bound and free variables; use freeVariablesInTerm for that
termDependencyNames :: Bool -> Bool -> Bool -> Term -> S.Set Name
termDependencyNames :: Bool -> Bool -> Bool -> Term -> Set Name
termDependencyNames Bool
withVars Bool
withPrims Bool
withNoms = TraversalOrder
-> (Set Name -> Term -> Set Name) -> Set Name -> Term -> Set Name
forall x. TraversalOrder -> (x -> Term -> x) -> x -> Term -> x
foldOverTerm TraversalOrder
TraversalOrderPre Set Name -> Term -> Set Name
addNames Set Name
forall a. Set a
S.empty
  where
    addNames :: Set Name -> Term -> Set Name
addNames Set Name
names Term
term = case Term
term of
        TermFunction Function
f -> case Function
f of
          FunctionPrimitive Name
name -> Name -> Set Name
prim Name
name
          FunctionElimination Elimination
e -> case Elimination
e of
            EliminationRecord (Projection Name
name Name
_) -> Name -> Set Name
nominal Name
name
            EliminationUnion (CaseStatement Name
name Maybe Term
_ [Field]
_) -> Name -> Set Name
nominal Name
name
            EliminationWrap Name
name -> Name -> Set Name
nominal Name
name
            Elimination
_ -> Set Name
names
          Function
_ -> Set Name
names
        TermRecord (Record Name
name [Field]
_) -> Name -> Set Name
nominal Name
name
        TermUnion (Injection Name
name Field
_) -> Name -> Set Name
nominal Name
name
        TermVariable Name
name -> Name -> Set Name
var Name
name
        TermWrap (WrappedTerm Name
name Term
_) -> Name -> Set Name
nominal Name
name
        Term
_ -> Set Name
names
      where
        nominal :: Name -> Set Name
nominal Name
name = if Bool
withNoms then Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
name Set Name
names else Set Name
names
        prim :: Name -> Set Name
prim Name
name = if Bool
withPrims then Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
name Set Name
names else Set Name
names
        var :: Name -> Set Name
var Name
name = if Bool
withVars then Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
S.insert Name
name Set Name
names else Set Name
names

-- Topological sort of connected components, in terms of dependencies between varable/term binding pairs
topologicalSortBindings :: M.Map Name Term -> [[(Name, Term)]]
topologicalSortBindings :: Map Name Term -> [[(Name, Term)]]
topologicalSortBindings Map Name Term
bindingMap = ([Name] -> [(Name, Term)]) -> [[Name]] -> [[(Name, Term)]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> (Name, Term)) -> [Name] -> [(Name, Term)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> (Name, Term)
toPair) ([(Name, [Name])] -> [[Name]]
forall a. Ord a => [(a, [a])] -> [[a]]
topologicalSortComponents ((Name, Term) -> (Name, [Name])
forall {a}. (a, Term) -> (a, [Name])
depsOf ((Name, Term) -> (Name, [Name]))
-> [(Name, Term)] -> [(Name, [Name])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Name, Term)]
bindings))
  where
    bindings :: [(Name, Term)]
bindings = Map Name Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name Term
bindingMap
    keys :: Set Name
keys = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList ((Name, Term) -> Name
forall a b. (a, b) -> a
fst ((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Name, Term)]
bindings)
    depsOf :: (a, Term) -> (a, [Name])
depsOf (a
name, Term
term) = (a
name, if Term -> Bool
hasTypeAnnotation Term
term
      then []
      else Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set Name
keys (Set Name -> Set Name) -> Set Name -> Set Name
forall a b. (a -> b) -> a -> b
$ Term -> Set Name
freeVariablesInTerm Term
term))
    toPair :: Name -> (Name, Term)
toPair Name
name = (Name
name, Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
Y.fromMaybe (Literal -> Term
TermLiteral (Literal -> Term) -> Literal -> Term
forall a b. (a -> b) -> a -> b
$ String -> Literal
LiteralString String
"Impossible!") (Maybe Term -> Term) -> Maybe Term -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Map Name Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
name Map Name Term
bindingMap)
    hasTypeAnnotation :: Term -> Bool
hasTypeAnnotation Term
term = case Term
term of
      TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
_) -> Term -> Bool
hasTypeAnnotation Term
term1
      TermTyped TypedTerm
_ -> Bool
True
      Term
_ -> Bool
False

topologicalSortElements :: [Element] -> Either [[Name]] [Name]
topologicalSortElements :: [Element] -> Either [[Name]] [Name]
topologicalSortElements [Element]
els = [(Name, [Name])] -> Either [[Name]] [Name]
forall a. Ord a => [(a, [a])] -> Either [[a]] [a]
topologicalSort ([(Name, [Name])] -> Either [[Name]] [Name])
-> [(Name, [Name])] -> Either [[Name]] [Name]
forall a b. (a -> b) -> a -> b
$ Element -> (Name, [Name])
adjlist (Element -> (Name, [Name])) -> [Element] -> [(Name, [Name])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Element]
els
  where
    adjlist :: Element -> (Name, [Name])
adjlist Element
e = (Element -> Name
elementName Element
e, Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool -> Term -> Set Name
termDependencyNames Bool
False Bool
True Bool
True (Term -> Set Name) -> Term -> Set Name
forall a b. (a -> b) -> a -> b
$ Element -> Term
elementData Element
e)

typeDependencyNames :: Type -> S.Set Name
typeDependencyNames :: Type -> Set Name
typeDependencyNames = Type -> Set Name
freeVariablesInType