-- | Inference rules

module Hydra.Inference.Rules where

import Hydra.Basics
import Hydra.Strip
import Hydra.Compute
import Hydra.Core
import Hydra.Schemas
import Hydra.CoreEncoding
import Hydra.Graph
import Hydra.Lexical
import Hydra.Mantle
import Hydra.Rewriting
import Hydra.Inference.Substitution
import Hydra.Unification
import Hydra.Tools.Debug
import Hydra.Annotations
import Hydra.Tier1
import Hydra.Tier2
import qualified Hydra.Dsl.Types as Types

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


data Inferred a = Inferred {
  -- The original term, possibly annotated with the inferred type
  forall a. Inferred a -> a
inferredObject :: a,
  -- The inferred type
  forall a. Inferred a -> Type
inferredType :: Type,
  -- Any constraints introduced by the inference process
  forall a. Inferred a -> [TypeConstraint]
inferredConstraints :: [TypeConstraint]
} deriving Int -> Inferred a -> ShowS
[Inferred a] -> ShowS
Inferred a -> String
(Int -> Inferred a -> ShowS)
-> (Inferred a -> String)
-> ([Inferred a] -> ShowS)
-> Show (Inferred a)
forall a. Show a => Int -> Inferred a -> ShowS
forall a. Show a => [Inferred a] -> ShowS
forall a. Show a => Inferred a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Inferred a -> ShowS
showsPrec :: Int -> Inferred a -> ShowS
$cshow :: forall a. Show a => Inferred a -> String
show :: Inferred a -> String
$cshowList :: forall a. Show a => [Inferred a] -> ShowS
showList :: [Inferred a] -> ShowS
Show

key_vcount :: Name
key_vcount = String -> Name
Name String
"vcount"

constraint :: Type -> Type -> TypeConstraint
constraint :: Type -> Type -> TypeConstraint
constraint Type
t1 Type
t2 = Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
t1 Type
t2 Maybe String
forall a. Maybe a
Nothing

fieldType :: Field -> FieldType
fieldType :: Field -> FieldType
fieldType (Field Name
fname Term
term) = Name -> Type -> FieldType
FieldType Name
fname (Type -> FieldType) -> Type -> FieldType
forall a b. (a -> b) -> a -> b
$ Term -> Type
termType Term
term

findMatchingField :: Name -> [FieldType] -> Flow Graph FieldType
findMatchingField :: Name -> [FieldType] -> Flow Graph FieldType
findMatchingField Name
fname [FieldType]
sfields = case (FieldType -> Bool) -> [FieldType] -> [FieldType]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (\FieldType
f -> FieldType -> Name
fieldTypeName FieldType
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
fname) [FieldType]
sfields of
  []    -> String -> Flow Graph FieldType
forall a. String -> Flow Graph a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow Graph FieldType) -> String -> Flow Graph FieldType
forall a b. (a -> b) -> a -> b
$ String
"no such field: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
fname
  (FieldType
h:[FieldType]
_) -> FieldType -> Flow Graph FieldType
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return FieldType
h

freshName :: Flow Graph Name
freshName :: Flow Graph Name
freshName = Int -> Name
normalVariable (Int -> Name) -> Flow Graph Int -> Flow Graph Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Flow Graph Int
forall s. Name -> Flow s Int
nextCount Name
key_vcount

freshVariableType :: Flow Graph Type
freshVariableType :: Flow Graph Type
freshVariableType = Name -> Type
TypeVariable (Name -> Type) -> Flow Graph Name -> Flow Graph Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Flow Graph Name
freshName

generalize :: M.Map Name TypeScheme -> Type -> TypeScheme
generalize :: Map Name TypeScheme -> Type -> TypeScheme
generalize Map Name TypeScheme
env Type
t  = [Name] -> Type -> TypeScheme
TypeScheme [Name]
vars Type
t
  where
    vars :: [Name]
vars = Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.difference
      (Type -> Set Name
freeVariablesInType Type
t)
      ((TypeScheme -> Set Name -> Set Name)
-> Set Name -> [TypeScheme] -> Set Name
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
L.foldr (Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set Name -> Set Name -> Set Name)
-> (TypeScheme -> Set Name) -> TypeScheme -> Set Name -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeScheme -> Set Name
freeVariablesInScheme) Set Name
forall a. Set a
S.empty ([TypeScheme] -> Set Name) -> [TypeScheme] -> Set Name
forall a b. (a -> b) -> a -> b
$ Map Name TypeScheme -> [TypeScheme]
forall k a. Map k a -> [a]
M.elems Map Name TypeScheme
env)

infer :: Term -> Flow Graph (Inferred Term)
infer :: Term -> Flow Graph (Inferred Term)
infer Term
term = String -> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall s a. String -> Flow s a -> Flow s a
withTrace (String
"infer for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TermVariant -> String
forall a. Show a => a -> String
show (Term -> TermVariant
termVariant Term
term)) (Flow Graph (Inferred Term) -> Flow Graph (Inferred Term))
-> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall a b. (a -> b) -> a -> b
$ case Term
term of
    TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
ann) -> do
      (Inferred Term
term2 Type
typ [TypeConstraint]
constraints) <- Term -> Flow Graph (Inferred Term)
infer Term
term1
      Inferred Term -> Flow Graph (Inferred Term)
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Type -> [TypeConstraint] -> Inferred Term
forall a. a -> Type -> [TypeConstraint] -> Inferred a
Inferred (AnnotatedTerm -> Term
TermAnnotated (AnnotatedTerm -> Term) -> AnnotatedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Map Name Term -> AnnotatedTerm
AnnotatedTerm Term
term2 Map Name Term
ann) Type
typ [TypeConstraint]
constraints)

    TermApplication (Application Term
fun Term
arg) -> do
      (Inferred Term
ifun Type
ityp [TypeConstraint]
funconst) <- Term -> Flow Graph (Inferred Term)
infer Term
fun
      (Inferred Term
iarg Type
atyp [TypeConstraint]
argconst) <- Term -> Flow Graph (Inferred Term)
infer Term
arg
      Type
cod <- Flow Graph Type
freshVariableType
      let constraints :: [TypeConstraint]
constraints = [TypeConstraint]
funconst [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
argconst [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [Type -> Type -> TypeConstraint
constraint Type
ityp (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.function Type
atyp Type
cod]
      Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Application -> Term
TermApplication (Application -> Term) -> Application -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Application
Application Term
ifun Term
iarg) Type
cod [TypeConstraint]
constraints

    TermFunction Function
f -> case Function
f of

      FunctionElimination Elimination
e -> case Elimination
e of

        EliminationList Term
fun -> do
          Type
a <- Flow Graph Type
freshVariableType
          Type
b <- Flow Graph Type
freshVariableType
          let expected :: Type
expected = [Type] -> Type
Types.functionN [Type
b, Type
a, Type
b]
          (Inferred Term
i Type
t [TypeConstraint]
c) <- Term -> Flow Graph (Inferred Term)
infer Term
fun
          let elim :: Type
elim = [Type] -> Type
Types.functionN [Type
b, Type -> Type
Types.list Type
a, Type
b]
          Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination (Term -> Elimination
EliminationList Term
i) Type
elim ([TypeConstraint]
c [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [Type -> Type -> TypeConstraint
constraint Type
expected Type
t])

        EliminationOptional (OptionalCases Term
n Term
j) -> do
          Type
dom <- Flow Graph Type
freshVariableType
          Type
cod <- Flow Graph Type
freshVariableType
          (Inferred Term
ni Type
nt [TypeConstraint]
nconst) <- Term -> Flow Graph (Inferred Term)
infer Term
n
          (Inferred Term
ji Type
jt [TypeConstraint]
jconst) <- Term -> Flow Graph (Inferred Term)
infer Term
j
          let t :: Type
t = Type -> Type -> Type
Types.function (Type -> Type
Types.optional Type
dom) Type
cod
          let constraints :: [TypeConstraint]
constraints = [TypeConstraint]
nconst [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
jconst
                              [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [Type -> Type -> TypeConstraint
constraint Type
cod Type
nt, Type -> Type -> TypeConstraint
constraint (Type -> Type -> Type
Types.function Type
dom Type
cod) Type
jt]
          Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination (OptionalCases -> Elimination
EliminationOptional (OptionalCases -> Elimination) -> OptionalCases -> Elimination
forall a b. (a -> b) -> a -> b
$ Term -> Term -> OptionalCases
OptionalCases Term
ni Term
ji) Type
t [TypeConstraint]
constraints

        EliminationProduct (TupleProjection Int
arity Int
idx) -> do
          [Type]
types <- Int -> Flow Graph Type -> Flow Graph [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
CM.replicateM Int
arity Flow Graph Type
freshVariableType
          let cod :: Type
cod = [Type]
types [Type] -> Int -> Type
forall a. HasCallStack => [a] -> Int -> a
!! Int
idx
          let t :: Type
t = Type -> Type -> Type
Types.function ([Type] -> Type
Types.product [Type]
types) Type
cod
          Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination (TupleProjection -> Elimination
EliminationProduct (TupleProjection -> Elimination) -> TupleProjection -> Elimination
forall a b. (a -> b) -> a -> b
$ Int -> Int -> TupleProjection
TupleProjection Int
arity Int
idx) Type
t []

        EliminationRecord (Projection Name
name Name
fname) -> do
          RowType
rt <- Name -> Flow Graph RowType
requireRecordType Name
name
          FieldType
sfield <- Name -> [FieldType] -> Flow Graph FieldType
findMatchingField Name
fname (RowType -> [FieldType]
rowTypeFields RowType
rt)
          Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination (Projection -> Elimination
EliminationRecord (Projection -> Elimination) -> Projection -> Elimination
forall a b. (a -> b) -> a -> b
$ Name -> Name -> Projection
Projection Name
name Name
fname)
            (Type -> Type -> Type
Types.function (RowType -> Type
TypeRecord RowType
rt) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ FieldType -> Type
fieldTypeType FieldType
sfield) []

        EliminationUnion (CaseStatement Name
tname Maybe Term
def [Field]
cases) -> do
            -- Default value
            (Maybe Term
idef, [TypeConstraint]
dfltConstraints) <- case Maybe Term
def of
              Maybe Term
Nothing -> (Maybe Term, [TypeConstraint])
-> Flow Graph (Maybe Term, [TypeConstraint])
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Term
forall a. Maybe a
Nothing, [])
              Just Term
d -> do
                (Inferred Term
i Type
_ [TypeConstraint]
c) <- Term -> Flow Graph (Inferred Term)
infer Term
d
                (Maybe Term, [TypeConstraint])
-> Flow Graph (Maybe Term, [TypeConstraint])
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
i, [TypeConstraint]
c)

            -- Cases
            [Inferred Field]
icases' <- (Field -> Flow Graph (Inferred Field))
-> [Field] -> Flow Graph [Inferred 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 -> Flow Graph (Inferred Field)
inferFieldType [Field]
cases
            let icases :: [Field]
icases = Inferred Field -> Field
forall a. Inferred a -> a
inferredObject (Inferred Field -> Field) -> [Inferred Field] -> [Field]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Field]
icases'
            let casesconst :: [[TypeConstraint]]
casesconst = Inferred Field -> [TypeConstraint]
forall a. Inferred a -> [TypeConstraint]
inferredConstraints (Inferred Field -> [TypeConstraint])
-> [Inferred Field] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Field]
icases'
            let icasesMap :: Map Name Term
icasesMap = [Field] -> Map Name Term
fieldMap [Field]
icases
            RowType
rt <- Name -> Flow Graph RowType
requireUnionType Name
tname
            let sfields :: Map Name Type
sfields = [FieldType] -> Map Name Type
fieldTypeMap  ([FieldType] -> Map Name Type) -> [FieldType] -> Map Name Type
forall a b. (a -> b) -> a -> b
$ RowType -> [FieldType]
rowTypeFields RowType
rt
            Name -> Map Name Term -> Map Name Type -> Flow Graph ()
forall {f :: * -> *} {a} {b}.
MonadFail f =>
Name -> Map Name a -> Map Name b -> f ()
checkCasesAgainstSchema Name
tname Map Name Term
icasesMap Map Name Type
sfields
            let pairMap :: Map Name (Term, Type)
pairMap = Map Name Term -> Map Name Type -> Map Name (Term, Type)
forall k l r. Ord k => Map k l -> Map k r -> Map k (l, r)
productOfMaps Map Name Term
icasesMap Map Name Type
sfields

            Type
cod <- Flow Graph Type
freshVariableType
            let outerConstraints :: [TypeConstraint]
outerConstraints = (\(Term
d, Type
s) -> Type -> Type -> TypeConstraint
constraint (Term -> Type
termType Term
d) (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.function Type
s Type
cod) ((Term, Type) -> TypeConstraint)
-> [(Term, Type)] -> [TypeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name (Term, Type) -> [(Term, Type)]
forall k a. Map k a -> [a]
M.elems Map Name (Term, Type)
pairMap
            let innerConstraints :: [TypeConstraint]
innerConstraints = [TypeConstraint]
dfltConstraints [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat [[TypeConstraint]]
casesconst

            Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination (CaseStatement -> Elimination
EliminationUnion (Name -> Maybe Term -> [Field] -> CaseStatement
CaseStatement Name
tname Maybe Term
idef [Field]
icases))
              (Type -> Type -> Type
Types.function (RowType -> Type
TypeUnion RowType
rt) Type
cod)
              ([TypeConstraint]
innerConstraints [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
outerConstraints)
          where
            checkCasesAgainstSchema :: Name -> Map Name a -> Map Name b -> f ()
checkCasesAgainstSchema Name
tname Map Name a
icases Map Name b
sfields = if Map Name a -> Bool
forall k a. Map k a -> Bool
M.null Map Name a
diff
                then () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                else String -> f ()
forall a. String -> f a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> f ()) -> String -> f ()
forall a b. (a -> b) -> a -> b
$ String
"case(s) in case statement which do not exist in type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
tname String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": "
                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
", " (Name -> String
unName (Name -> String) -> [Name] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name a -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name a
diff)
              where
                diff :: Map Name a
diff = Map Name a -> Map Name b -> Map Name a
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Map Name a
icases Map Name b
sfields

        EliminationWrap Name
name -> do
          Type
typ <- Name -> Flow Graph Type
requireWrappedType Name
name
          Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination (Name -> Elimination
EliminationWrap Name
name) (Type -> Type -> Type
Types.function (WrappedType -> Type
TypeWrap (WrappedType -> Type) -> WrappedType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> WrappedType
WrappedType Name
name Type
typ) Type
typ) []

      FunctionLambda (Lambda Name
v Maybe Type
_ Term
body) -> do
        Type
tv <- Flow Graph Type
freshVariableType
        (Inferred Term
i Type
t [TypeConstraint]
iconst) <- Name
-> TypeScheme
-> Flow Graph (Inferred Term)
-> Flow Graph (Inferred Term)
forall x. Name -> TypeScheme -> Flow Graph x -> Flow Graph x
withBinding Name
v (Type -> TypeScheme
monotype Type
tv) (Flow Graph (Inferred Term) -> Flow Graph (Inferred Term))
-> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall a b. (a -> b) -> a -> b
$ Term -> Flow Graph (Inferred Term)
infer Term
body
        Function -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldFunction (Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Lambda Name
v (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
tv) Term
i) (Type -> Type -> Type
Types.function Type
tv Type
t) [TypeConstraint]
iconst

      FunctionPrimitive Name
name -> do
          TypeScheme
ts <- (Name -> Flow Graph TypeScheme
typeOfPrimitive Name
name) Flow Graph TypeScheme
-> (TypeScheme -> Flow Graph TypeScheme) -> Flow Graph TypeScheme
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
>>= TypeScheme -> Flow Graph TypeScheme
instantiate
          -- TODO: propagate the entire type scheme, not only the body
          Function -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldFunction (Name -> Function
FunctionPrimitive Name
name) (TypeScheme -> Type
typeSchemeType TypeScheme
ts) []

    TermLet Let
lt -> Let -> Flow Graph (Inferred Term)
inferLet Let
lt

    TermList [Term]
els -> do
        Type
v <- Flow Graph Type
freshVariableType
        if [Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Term]
els
          then Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield ([Term] -> Term
TermList []) (Type -> Type
Types.list Type
v) []
          else do
            [Inferred Term]
iels' <- (Term -> Flow Graph (Inferred Term))
-> [Term] -> Flow Graph [Inferred 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 -> Flow Graph (Inferred Term)
infer [Term]
els
            let iels :: [Term]
iels = Inferred Term -> Term
forall a. Inferred a -> a
inferredObject (Inferred Term -> Term) -> [Inferred Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
iels'
            let elsconst :: [[TypeConstraint]]
elsconst = Inferred Term -> [TypeConstraint]
forall a. Inferred a -> [TypeConstraint]
inferredConstraints (Inferred Term -> [TypeConstraint])
-> [Inferred Term] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
iels'
            let co :: [TypeConstraint]
co = (\Term
e -> Type -> Type -> TypeConstraint
constraint Type
v (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ Term -> Type
termType Term
e) (Term -> TypeConstraint) -> [Term] -> [TypeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
iels
            let ci :: [TypeConstraint]
ci = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat [[TypeConstraint]]
elsconst
            Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield ([Term] -> Term
TermList [Term]
iels) (Type -> Type
Types.list Type
v) ([TypeConstraint]
co [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
ci)

    TermLiteral Literal
l -> Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Literal -> Term
TermLiteral Literal
l) (LiteralType -> Type
Types.literal (LiteralType -> Type) -> LiteralType -> Type
forall a b. (a -> b) -> a -> b
$ Literal -> LiteralType
literalType Literal
l) []

    TermMap Map Term Term
m -> do
        Type
kv <- Flow Graph Type
freshVariableType
        Type
vv <- Flow Graph Type
freshVariableType
        if Map Term Term -> Bool
forall k a. Map k a -> Bool
M.null Map Term Term
m
          then Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Map Term Term -> Term
TermMap Map Term Term
forall k a. Map k a
M.empty) (Type -> Type -> Type
Types.map Type
kv Type
vv) []
          else do
            [(Term, Term, [TypeConstraint])]
triples <- ((Term, Term) -> Flow Graph (Term, Term, [TypeConstraint]))
-> [(Term, Term)] -> Flow Graph [(Term, Term, [TypeConstraint])]
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) -> Flow Graph (Term, Term, [TypeConstraint])
toTriple ([(Term, Term)] -> Flow Graph [(Term, Term, [TypeConstraint])])
-> [(Term, Term)] -> Flow Graph [(Term, Term, [TypeConstraint])]
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
m
            let pairs :: [(Term, Term)]
pairs = (\(Term
k, Term
v, [TypeConstraint]
_) -> (Term
k, Term
v)) ((Term, Term, [TypeConstraint]) -> (Term, Term))
-> [(Term, Term, [TypeConstraint])] -> [(Term, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, Term, [TypeConstraint])]
triples
            let co :: [TypeConstraint]
co = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((\(Term
k, Term
v, [TypeConstraint]
c) -> [TypeConstraint]
c [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [Type -> Type -> TypeConstraint
constraint Type
kv (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ Term -> Type
termType Term
k, Type -> Type -> TypeConstraint
constraint Type
vv (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ Term -> Type
termType Term
v]) ((Term, Term, [TypeConstraint]) -> [TypeConstraint])
-> [(Term, Term, [TypeConstraint])] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, Term, [TypeConstraint])]
triples)
            Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (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)]
pairs) (Type -> Type -> Type
Types.map Type
kv Type
vv) [TypeConstraint]
co
      where
        toTriple :: (Term, Term) -> Flow Graph (Term, Term, [TypeConstraint])
toTriple (Term
k, Term
v) = do
          (Inferred Term
ik Type
_ [TypeConstraint]
kc) <- Term -> Flow Graph (Inferred Term)
infer Term
k
          (Inferred Term
iv Type
_ [TypeConstraint]
vc) <- Term -> Flow Graph (Inferred Term)
infer Term
v
          (Term, Term, [TypeConstraint])
-> Flow Graph (Term, Term, [TypeConstraint])
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
ik, Term
iv, [TypeConstraint]
kc [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
vc)

    TermOptional Maybe Term
m -> do
      Type
v <- Flow Graph Type
freshVariableType
      case Maybe Term
m of
        Maybe Term
Nothing -> Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Maybe Term -> Term
TermOptional Maybe Term
forall a. Maybe a
Nothing) (Type -> Type
Types.optional Type
v) []
        Just Term
e -> do
          (Inferred Term
i Type
t [TypeConstraint]
ci) <- Term -> Flow Graph (Inferred Term)
infer Term
e
          Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Maybe Term -> Term
TermOptional (Maybe Term -> Term) -> Maybe Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just Term
i) (Type -> Type
Types.optional Type
v) ((Type -> Type -> TypeConstraint
constraint Type
v Type
t)TypeConstraint -> [TypeConstraint] -> [TypeConstraint]
forall a. a -> [a] -> [a]
:[TypeConstraint]
ci)

    TermProduct [Term]
tuple -> do
      [Inferred Term]
is' <- (Term -> Flow Graph (Inferred Term))
-> [Term] -> Flow Graph [Inferred 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 -> Flow Graph (Inferred Term)
infer [Term]
tuple
      let is :: [Term]
is = Inferred Term -> Term
forall a. Inferred a -> a
inferredObject (Inferred Term -> Term) -> [Inferred Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
is'
      let co :: [TypeConstraint]
co = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (Inferred Term -> [TypeConstraint]
forall a. Inferred a -> [TypeConstraint]
inferredConstraints (Inferred Term -> [TypeConstraint])
-> [Inferred Term] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
is')
      Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield ([Term] -> Term
TermProduct [Term]
is) ([Type] -> Type
TypeProduct ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Term -> Type) -> [Term] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Type
termType [Term]
is) [TypeConstraint]
co

    TermRecord (Record Name
n [Field]
fields) -> do
        RowType
rt <- Name -> Flow Graph RowType
requireRecordType Name
n
        [Inferred Field]
ifields' <- (Field -> Flow Graph (Inferred Field))
-> [Field] -> Flow Graph [Inferred 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 -> Flow Graph (Inferred Field)
inferFieldType [Field]
fields
        let ifields :: [Field]
ifields = Inferred Field -> Field
forall a. Inferred a -> a
inferredObject (Inferred Field -> Field) -> [Inferred Field] -> [Field]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Field]
ifields'
        let ci :: [TypeConstraint]
ci = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (Inferred Field -> [TypeConstraint]
forall a. Inferred a -> [TypeConstraint]
inferredConstraints (Inferred Field -> [TypeConstraint])
-> [Inferred Field] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Field]
ifields')
        let irt :: Type
irt = RowType -> Type
TypeRecord (RowType -> Type) -> RowType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> [FieldType] -> RowType
RowType Name
n (Field -> FieldType
fieldType (Field -> FieldType) -> [Field] -> [FieldType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Field]
ifields)
        Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Record -> Term
TermRecord (Record -> Term) -> Record -> Term
forall a b. (a -> b) -> a -> b
$ Name -> [Field] -> Record
Record Name
n [Field]
ifields) Type
irt ((Type -> Type -> TypeConstraint
constraint Type
irt (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ RowType -> Type
TypeRecord RowType
rt)TypeConstraint -> [TypeConstraint] -> [TypeConstraint]
forall a. a -> [a] -> [a]
:[TypeConstraint]
ci)

    TermSet Set Term
els -> do
      Type
v <- Flow Graph Type
freshVariableType
      if Set Term -> Bool
forall a. Set a -> Bool
S.null Set Term
els
        then Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Set Term -> Term
TermSet Set Term
forall a. Set a
S.empty) (Type -> Type
Types.set Type
v) []
        else do
          [Inferred Term]
iels' <- (Term -> Flow Graph (Inferred Term))
-> [Term] -> Flow Graph [Inferred 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 -> Flow Graph (Inferred Term)
infer ([Term] -> Flow Graph [Inferred Term])
-> [Term] -> Flow Graph [Inferred Term]
forall a b. (a -> b) -> a -> b
$ Set Term -> [Term]
forall a. Set a -> [a]
S.toList Set Term
els
          let iels :: [Term]
iels = Inferred Term -> Term
forall a. Inferred a -> a
inferredObject (Inferred Term -> Term) -> [Inferred Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
iels'
          let co :: [TypeConstraint]
co = (\Term
e -> (Type -> Type -> TypeConstraint
constraint Type
v (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ Term -> Type
termType Term
e)) (Term -> TypeConstraint) -> [Term] -> [TypeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
iels
          let ci :: [TypeConstraint]
ci = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (Inferred Term -> [TypeConstraint]
forall a. Inferred a -> [TypeConstraint]
inferredConstraints (Inferred Term -> [TypeConstraint])
-> [Inferred Term] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
iels')
          Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (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]
iels) (Type -> Type
Types.set Type
v) ([TypeConstraint]
co [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
ci)

    TermSum (Sum Int
i Int
s Term
trm) -> do
        (Inferred Term
it Type
t [TypeConstraint]
co) <- Term -> Flow Graph (Inferred Term)
infer Term
trm
        [Type]
types <- [Flow Graph Type] -> Flow Graph [Type]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
CM.sequence (Type -> Int -> Flow Graph Type
varOrTerm Type
t (Int -> Flow Graph Type) -> [Int] -> [Flow Graph Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)])
        Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Sum -> Term
TermSum (Sum -> Term) -> Sum -> Term
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Term -> Sum
Sum Int
i Int
s Term
it) ([Type] -> Type
TypeSum [Type]
types) [TypeConstraint]
co
      where
        varOrTerm :: Type -> Int -> Flow Graph Type
varOrTerm Type
t Int
j = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
          then Type -> Flow Graph Type
forall a. a -> Flow Graph a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
          else Flow Graph Type
freshVariableType

    TermTyped (TypedTerm Term
term1 Type
typ) -> do
      (Inferred Term
i Type
t [TypeConstraint]
c) <- Term -> Flow Graph (Inferred Term)
infer Term
term1
      Inferred Term -> Flow Graph (Inferred Term)
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Inferred Term -> Flow Graph (Inferred Term))
-> Inferred Term -> Flow Graph (Inferred Term)
forall a b. (a -> b) -> a -> b
$ Term -> Type -> [TypeConstraint] -> Inferred Term
forall a. a -> Type -> [TypeConstraint] -> Inferred a
Inferred (Maybe Type -> Term -> Term
setTermType (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typ) Term
i) Type
typ ([TypeConstraint] -> Inferred Term)
-> [TypeConstraint] -> Inferred Term
forall a b. (a -> b) -> a -> b
$ [TypeConstraint]
c [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [Type -> Type -> TypeConstraint
constraint Type
typ Type
t]

    TermUnion (Injection Name
n Field
field) -> do
        RowType
rt <- Name -> Flow Graph RowType
requireUnionType Name
n
        FieldType
sfield <- Name -> [FieldType] -> Flow Graph FieldType
findMatchingField (Field -> Name
fieldName Field
field) (RowType -> [FieldType]
rowTypeFields RowType
rt)
        (Inferred Field
ifield Type
t [TypeConstraint]
ci) <- Field -> Flow Graph (Inferred Field)
inferFieldType Field
field
        let co :: TypeConstraint
co = Type -> Type -> TypeConstraint
constraint Type
t (Type -> TypeConstraint) -> Type -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ FieldType -> Type
fieldTypeType FieldType
sfield

        Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Injection -> Term
TermUnion (Injection -> Term) -> Injection -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Field -> Injection
Injection Name
n Field
ifield) (RowType -> Type
TypeUnion RowType
rt) (TypeConstraint
coTypeConstraint -> [TypeConstraint] -> [TypeConstraint]
forall a. a -> [a] -> [a]
:[TypeConstraint]
ci)

    TermVariable Name
v -> do
      TypeScheme
ts <- Name -> Flow Graph TypeScheme
requireName Name
v
      -- TODO: propagate the entire type scheme, not only the body
      Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Name -> Term
TermVariable Name
v) (TypeScheme -> Type
typeSchemeType TypeScheme
ts) []

    TermWrap (WrappedTerm Name
name Term
term1) -> do
      Type
typ <- Name -> Flow Graph Type
requireWrappedType Name
name
      (Inferred Term
i Type
t [TypeConstraint]
ci) <- Term -> Flow Graph (Inferred Term)
infer Term
term1
      Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (WrappedTerm -> Term
TermWrap (WrappedTerm -> Term) -> WrappedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> WrappedTerm
WrappedTerm Name
name Term
i) (WrappedType -> Type
TypeWrap (WrappedType -> Type) -> WrappedType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> WrappedType
WrappedType Name
name Type
typ) ([TypeConstraint]
ci [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [Type -> Type -> TypeConstraint
constraint Type
typ Type
t])

inferFieldType :: Field -> Flow Graph (Inferred Field)
inferFieldType :: Field -> Flow Graph (Inferred Field)
inferFieldType (Field Name
fname Term
term) = do
  (Inferred Term
i Type
t [TypeConstraint]
c) <- Term -> Flow Graph (Inferred Term)
infer Term
term
  Inferred Field -> Flow Graph (Inferred Field)
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Field -> Type -> [TypeConstraint] -> Inferred Field
forall a. a -> Type -> [TypeConstraint] -> Inferred a
Inferred (Name -> Term -> Field
Field Name
fname Term
i) Type
t [TypeConstraint]
c)

inferLet :: Let -> Flow Graph (Inferred Term)
inferLet :: Let -> Flow Graph (Inferred Term)
inferLet (Let [LetBinding]
bindings Term
env) = String -> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall s a. String -> Flow s a -> Flow s a
withTrace (String
"let(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"," (Name -> String
unName (Name -> String) -> (LetBinding -> Name) -> LetBinding -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> Name
letBindingName (LetBinding -> String) -> [LetBinding] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")") (Flow Graph (Inferred Term) -> Flow Graph (Inferred Term))
-> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall a b. (a -> b) -> a -> b
$ do
    Graph
state0 <- Flow Graph Graph
forall s. Flow s s
getState
    let e :: Map Name TypeScheme
e = [LetBinding] -> Map Name TypeScheme -> Map Name TypeScheme
forall {t :: * -> *}.
Foldable t =>
t LetBinding -> Map Name TypeScheme -> Map Name TypeScheme
preExtendEnv [LetBinding]
bindings (Map Name TypeScheme -> Map Name TypeScheme)
-> Map Name TypeScheme -> Map Name TypeScheme
forall a b. (a -> b) -> a -> b
$ Graph -> Map Name TypeScheme
graphTypes Graph
state0
    let state1 :: Graph
state1 = Graph
state0 {graphTypes = e}
    Graph -> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState Graph
state1 (Flow Graph (Inferred Term) -> Flow Graph (Inferred Term))
-> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall a b. (a -> b) -> a -> b
$ do
      -- TODO: perform a topological sort on the bindings; this process should be unified with that of elements in a graph

      -- Infer types of bindings in the pre-extended environment
      [Inferred Term]
ivalues' <- (Term -> Flow Graph (Inferred Term))
-> [Term] -> Flow Graph [Inferred 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 -> Flow Graph (Inferred Term)
infer (LetBinding -> Term
letBindingTerm (LetBinding -> Term) -> [LetBinding] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LetBinding]
bindings)
      let ivalues :: [Term]
ivalues = Inferred Term -> Term
forall a. Inferred a -> a
inferredObject (Inferred Term -> Term) -> [Inferred Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
ivalues'
      let ibindings :: [LetBinding]
ibindings = (LetBinding -> Term -> LetBinding)
-> [LetBinding] -> [Term] -> [LetBinding]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith (\(LetBinding Name
k Term
v Maybe TypeScheme
t) Term
i -> Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k Term
i Maybe TypeScheme
t) [LetBinding]
bindings [Term]
ivalues
      let bc :: [TypeConstraint]
bc = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (Inferred Term -> [TypeConstraint]
forall a. Inferred a -> [TypeConstraint]
inferredConstraints (Inferred Term -> [TypeConstraint])
-> [Inferred Term] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Inferred Term]
ivalues')

      let tbindings :: Map Name TypeScheme
tbindings = [(Name, TypeScheme)] -> Map Name TypeScheme
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, TypeScheme)] -> Map Name TypeScheme)
-> [(Name, TypeScheme)] -> Map Name TypeScheme
forall a b. (a -> b) -> a -> b
$ (LetBinding -> (Name, TypeScheme))
-> [LetBinding] -> [(Name, TypeScheme)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(LetBinding Name
k Term
i Maybe TypeScheme
t) -> (Name
k, Term -> TypeScheme
termTypeScheme Term
i)) [LetBinding]
ibindings
      (Inferred Term
ienv Type
t [TypeConstraint]
cenv) <- Map Name TypeScheme
-> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall x. Map Name TypeScheme -> Flow Graph x -> Flow Graph x
withBindings Map Name TypeScheme
tbindings (Flow Graph (Inferred Term) -> Flow Graph (Inferred Term))
-> Flow Graph (Inferred Term) -> Flow Graph (Inferred Term)
forall a b. (a -> b) -> a -> b
$ Term -> Flow Graph (Inferred Term)
infer Term
env

      Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Let -> Term
TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Let [LetBinding]
ibindings Term
ienv) Type
t ([TypeConstraint]
bc [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
cenv)
  where
    -- Add any manual type annotations for the bindings to the environment, enabling type inference over recursive definitions
    preExtendEnv :: t LetBinding -> Map Name TypeScheme -> Map Name TypeScheme
preExtendEnv t LetBinding
bindings Map Name TypeScheme
e = (Map Name TypeScheme -> LetBinding -> Map Name TypeScheme)
-> Map Name TypeScheme -> t LetBinding -> Map Name TypeScheme
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map Name TypeScheme -> LetBinding -> Map Name TypeScheme
addPair Map Name TypeScheme
e t LetBinding
bindings
      where
        addPair :: Map Name TypeScheme -> LetBinding -> Map Name TypeScheme
addPair Map Name TypeScheme
e (LetBinding Name
name Term
term Maybe TypeScheme
_) = case Term -> Maybe Type
typeOfTerm Term
term of
          Maybe Type
Nothing -> Map Name TypeScheme
e
          Just Type
typ -> Name -> TypeScheme -> Map Name TypeScheme -> Map Name TypeScheme
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
name (Type -> TypeScheme
monotype Type
typ) Map Name TypeScheme
e

instantiate :: TypeScheme -> Flow Graph TypeScheme
instantiate :: TypeScheme -> Flow Graph TypeScheme
instantiate (TypeScheme [Name]
vars Type
t) = do
    [Name]
vars1 <- (Name -> Flow Graph Name) -> [Name] -> Flow Graph [Name]
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]
mapM (Flow Graph Name -> Name -> Flow Graph Name
forall a b. a -> b -> a
const Flow Graph Name
freshName) [Name]
vars
    TypeScheme -> Flow Graph TypeScheme
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeScheme -> Flow Graph TypeScheme)
-> TypeScheme -> Flow Graph TypeScheme
forall a b. (a -> b) -> a -> b
$ [Name] -> Type -> TypeScheme
TypeScheme [Name]
vars1 (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Map Name Type -> Type -> Type
substituteInType ([(Name, Type)] -> Map Name Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, Type)] -> Map Name Type)
-> [(Name, Type)] -> Map Name Type
forall a b. (a -> b) -> a -> b
$ [Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
L.zip [Name]
vars (Name -> Type
TypeVariable (Name -> Type) -> [Name] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
vars1)) Type
t

monotype :: Type -> TypeScheme
monotype :: Type -> TypeScheme
monotype Type
typ = [Name] -> Type -> TypeScheme
TypeScheme [] Type
typ

productOfMaps :: Ord k => M.Map k l -> M.Map k r -> M.Map k (l, r)
productOfMaps :: forall k l r. Ord k => Map k l -> Map k r -> Map k (l, r)
productOfMaps Map k l
ml Map k r
mr = [(k, (l, r))] -> Map k (l, r)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(k, (l, r))] -> Map k (l, r)) -> [(k, (l, r))] -> Map k (l, r)
forall a b. (a -> b) -> a -> b
$ [Maybe (k, (l, r))] -> [(k, (l, r))]
forall a. [Maybe a] -> [a]
Y.catMaybes ((k, r) -> Maybe (k, (l, r))
forall {b}. (k, b) -> Maybe (k, (l, b))
toPair ((k, r) -> Maybe (k, (l, r))) -> [(k, r)] -> [Maybe (k, (l, r))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map k r -> [(k, r)]
forall k a. Map k a -> [(k, a)]
M.toList Map k r
mr)
  where
    toPair :: (k, b) -> Maybe (k, (l, b))
toPair (k
k, b
vr) = (\l
vl -> (k
k, (l
vl, b
vr))) (l -> (k, (l, b))) -> Maybe l -> Maybe (k, (l, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> Map k l -> Maybe l
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
k Map k l
ml

reduceType :: Type -> Type
reduceType :: Type -> Type
reduceType Type
t = Type
t -- betaReduceType cx t

requireName :: Name -> Flow Graph TypeScheme
requireName :: Name -> Flow Graph TypeScheme
requireName Name
v = do
  Map Name TypeScheme
env <- Graph -> Map Name TypeScheme
graphTypes (Graph -> Map Name TypeScheme)
-> Flow Graph Graph -> Flow Graph (Map Name TypeScheme)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Flow Graph Graph
forall s. Flow s s
getState
  case Name -> Map Name TypeScheme -> Maybe TypeScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v Map Name TypeScheme
env of
    Maybe TypeScheme
Nothing -> String -> Flow Graph TypeScheme
forall a. String -> Flow Graph a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow Graph TypeScheme)
-> String -> Flow Graph TypeScheme
forall a b. (a -> b) -> a -> b
$ String
"variable not bound in environment: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". Environment: "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
", " (Name -> String
unName (Name -> String) -> [Name] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name TypeScheme -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name TypeScheme
env)
    Just TypeScheme
s -> TypeScheme -> Flow Graph TypeScheme
instantiate TypeScheme
s

termType :: Term -> Type
termType :: Term -> Type
termType Term
term = case Term -> Term
stripTerm Term
term of
  (TermTyped (TypedTerm Term
_ Type
typ)) -> Type
typ

-- TODO: limited and temporary
termTypeScheme :: Term -> TypeScheme
termTypeScheme :: Term -> TypeScheme
termTypeScheme = Type -> TypeScheme
monotype (Type -> TypeScheme) -> (Term -> Type) -> Term -> TypeScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Type
termType

typeOfPrimitive :: Name -> Flow Graph TypeScheme
typeOfPrimitive :: Name -> Flow Graph TypeScheme
typeOfPrimitive Name
name = Primitive -> TypeScheme
primitiveType (Primitive -> TypeScheme)
-> Flow Graph Primitive -> Flow Graph TypeScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Flow Graph Primitive
requirePrimitive Name
name

typeOfTerm :: Term -> Maybe Type
typeOfTerm :: Term -> Maybe Type
typeOfTerm Term
term = case Term
term of
  TermAnnotated (AnnotatedTerm Term
term1 Map Name Term
_) -> Term -> Maybe Type
typeOfTerm Term
term1
  TermTyped (TypedTerm Term
term1 Type
typ) -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typ
  Term
_ -> Maybe Type
forall a. Maybe a
Nothing

withBinding :: Name -> TypeScheme -> Flow Graph x -> Flow Graph x
withBinding :: forall x. Name -> TypeScheme -> Flow Graph x -> Flow Graph x
withBinding Name
n TypeScheme
ts = (Map Name TypeScheme -> Map Name TypeScheme)
-> Flow Graph x -> Flow Graph x
forall x.
(Map Name TypeScheme -> Map Name TypeScheme)
-> Flow Graph x -> Flow Graph x
withEnvironment (Name -> TypeScheme -> Map Name TypeScheme -> Map Name TypeScheme
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Name
n TypeScheme
ts)

withBindings :: M.Map Name TypeScheme -> Flow Graph x -> Flow Graph x
withBindings :: forall x. Map Name TypeScheme -> Flow Graph x -> Flow Graph x
withBindings Map Name TypeScheme
bindings = (Map Name TypeScheme -> Map Name TypeScheme)
-> Flow Graph x -> Flow Graph x
forall x.
(Map Name TypeScheme -> Map Name TypeScheme)
-> Flow Graph x -> Flow Graph x
withEnvironment (\Map Name TypeScheme
e -> Map Name TypeScheme -> Map Name TypeScheme -> Map Name TypeScheme
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Name TypeScheme
bindings Map Name TypeScheme
e)

withEnvironment :: (M.Map Name TypeScheme -> M.Map Name TypeScheme) -> Flow Graph x -> Flow Graph x
withEnvironment :: forall x.
(Map Name TypeScheme -> Map Name TypeScheme)
-> Flow Graph x -> Flow Graph x
withEnvironment Map Name TypeScheme -> Map Name TypeScheme
m Flow Graph x
flow = do
  Graph
g <- Flow Graph Graph
forall s. Flow s s
getState
  Graph -> Flow Graph x -> Flow Graph x
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState (Graph
g {graphTypes = m (graphTypes g)}) Flow Graph x
flow

yield :: Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield :: Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield Term
term Type
typ [TypeConstraint]
constraints = do
  Inferred Term -> Flow Graph (Inferred Term)
forall a. a -> Flow Graph a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Type -> [TypeConstraint] -> Inferred Term
forall a. a -> Type -> [TypeConstraint] -> Inferred a
Inferred (TypedTerm -> Term
TermTyped (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
TypedTerm Term
term Type
typ) Type
typ [TypeConstraint]
constraints)

yieldFunction :: Function -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldFunction :: Function -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldFunction Function
fun = Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Function -> Term
TermFunction Function
fun)

yieldElimination :: Elimination -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination :: Elimination
-> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yieldElimination Elimination
e = Term -> Type -> [TypeConstraint] -> Flow Graph (Inferred Term)
yield (Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Elimination -> Function
FunctionElimination Elimination
e)