-- | Inference rules

module Hydra.Rules where

import Hydra.Basics
import Hydra.Strip
import Hydra.Compute
import Hydra.Core
import Hydra.CoreDecoding
import Hydra.CoreEncoding
import Hydra.Graph
import Hydra.Lexical
import Hydra.Mantle
import Hydra.Rewriting
import Hydra.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 InferenceContext = InferenceContext {
  InferenceContext -> Graph
inferenceContextGraph :: Graph,
  InferenceContext -> TypingEnvironment
inferenceContextEnvironment :: TypingEnvironment}

type TypingEnvironment = M.Map Name TypeScheme

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 InferenceContext (FieldType)
findMatchingField :: Name -> [FieldType] -> Flow InferenceContext 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 InferenceContext FieldType
forall a. String -> Flow InferenceContext a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow InferenceContext FieldType)
-> String -> Flow InferenceContext FieldType
forall a b. (a -> b) -> a -> b
$ String
"no such field: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
fname
  (FieldType
h:[FieldType]
_) -> FieldType -> Flow InferenceContext FieldType
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return FieldType
h

freshName :: Flow InferenceContext (Type)
freshName :: Flow InferenceContext Type
freshName = Name -> Type
TypeVariable (Name -> Type) -> (Int -> Name) -> Int -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
normalVariable (Int -> Type)
-> Flow InferenceContext Int -> Flow InferenceContext Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Flow InferenceContext Int
forall s. String -> Flow s Int
nextCount String
"hyInf"

generalize :: TypingEnvironment -> Type -> TypeScheme
generalize :: TypingEnvironment -> Type -> TypeScheme
generalize TypingEnvironment
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
$ TypingEnvironment -> [TypeScheme]
forall k a. Map k a -> [a]
M.elems TypingEnvironment
env)

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

    TermTyped (TypedTerm Term
term1 Type
typ) -> do
      (Term
i, [Constraint]
c) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
term1
      (Term, [Constraint]) -> Flow InferenceContext (Term, [Constraint])
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> Term -> Term
setTermType (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typ) Term
i, [Constraint]
c [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [(Type
typ, Term -> Type
termType Term
i)])

    TermApplication (Application Term
fun Term
arg) -> do
      (Term
ifun, [Constraint]
funconst) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
fun
      (Term
iarg, [Constraint]
argconst) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
arg
      Type
cod <- Flow InferenceContext Type
freshName
      let constraints :: [Constraint]
constraints = [Constraint]
funconst [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
argconst [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [(Term -> Type
termType Term
ifun, Type -> Type -> Type
Types.function (Term -> Type
termType Term
iarg) Type
cod)]
      Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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 [Constraint]
constraints

    TermFunction Function
f -> case Function
f of

      FunctionElimination Elimination
e -> case Elimination
e of

        EliminationList Term
fun -> do
          Type
a <- Flow InferenceContext Type
freshName
          Type
b <- Flow InferenceContext Type
freshName
          let expected :: Type
expected = [Type] -> Type
Types.functionN [Type
b, Type
a, Type
b]
          (Term
i, [Constraint]
c) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
fun
          let elim :: Type
elim = [Type] -> Type
Types.functionN [Type
b, Type -> Type
Types.list Type
a, Type
b]
          Elimination
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yieldElimination (Term -> Elimination
EliminationList Term
i) Type
elim ([Constraint]
c [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [(Type
expected, Term -> Type
termType Term
i)])

        EliminationOptional (OptionalCases Term
n Term
j) -> do
          Type
dom <- Flow InferenceContext Type
freshName
          Type
cod <- Flow InferenceContext Type
freshName
          (Term
ni, [Constraint]
nconst) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
n
          (Term
ji, [Constraint]
jconst) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
j
          let t :: Type
t = Type -> Type -> Type
Types.function (Type -> Type
Types.optional Type
dom) Type
cod
          let constraints :: [Constraint]
constraints = [Constraint]
nconst [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
jconst
                              [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [(Type
cod, Term -> Type
termType Term
ni), (Type -> Type -> Type
Types.function Type
dom Type
cod, Term -> Type
termType Term
ji)]
          Elimination
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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 [Constraint]
constraints

        EliminationProduct (TupleProjection Int
arity Int
idx) -> do
          [Type]
types <- Int -> Flow InferenceContext Type -> Flow InferenceContext [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
CM.replicateM Int
arity Flow InferenceContext Type
freshName
          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
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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 <- Flow Graph RowType -> Flow InferenceContext RowType
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph RowType -> Flow InferenceContext RowType)
-> Flow Graph RowType -> Flow InferenceContext RowType
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Flow Graph RowType
requireRecordType Bool
True Name
name
          FieldType
sfield <- Name -> [FieldType] -> Flow InferenceContext FieldType
findMatchingField Name
fname (RowType -> [FieldType]
rowTypeFields RowType
rt)
          Elimination
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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, [Constraint]
dfltConstraints) <- case Maybe Term
def of
              Maybe Term
Nothing -> (Maybe Term, [Constraint])
-> Flow InferenceContext (Maybe Term, [Constraint])
forall a. a -> Flow InferenceContext a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Term
forall a. Maybe a
Nothing, [])
              Just Term
d -> do
                (Term
i, [Constraint]
c) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
d
                (Maybe Term, [Constraint])
-> Flow InferenceContext (Maybe Term, [Constraint])
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
i, [Constraint]
c)

            -- Cases
            [(Field, [Constraint])]
icases' <- (Field -> Flow InferenceContext (Field, [Constraint]))
-> [Field] -> Flow InferenceContext [(Field, [Constraint])]
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 InferenceContext (Field, [Constraint])
inferFieldType [Field]
cases
            let icases :: [Field]
icases = (Field, [Constraint]) -> Field
forall a b. (a, b) -> a
fst ((Field, [Constraint]) -> Field)
-> [(Field, [Constraint])] -> [Field]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Field, [Constraint])]
icases'
            let casesconst :: [[Constraint]]
casesconst = (Field, [Constraint]) -> [Constraint]
forall a b. (a, b) -> b
snd ((Field, [Constraint]) -> [Constraint])
-> [(Field, [Constraint])] -> [[Constraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Field, [Constraint])]
icases'
            let icasesMap :: Map Name Term
icasesMap = [Field] -> Map Name Term
fieldMap [Field]
icases
            RowType
rt <- Flow Graph RowType -> Flow InferenceContext RowType
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph RowType -> Flow InferenceContext RowType)
-> Flow Graph RowType -> Flow InferenceContext RowType
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Flow Graph RowType
requireUnionType Bool
True 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 InferenceContext ()
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 InferenceContext Type
freshName
            let outerConstraints :: [Constraint]
outerConstraints = (\(Term
d, Type
s) -> (Term -> Type
termType Term
d, Type -> Type -> Type
Types.function Type
s Type
cod)) ((Term, Type) -> Constraint) -> [(Term, Type)] -> [Constraint]
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 :: [Constraint]
innerConstraints = [Constraint]
dfltConstraints [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat [[Constraint]]
casesconst

            Elimination
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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)
              ([Constraint]
innerConstraints [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
tname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": "
                  String -> String -> String
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 <- Flow Graph Type -> Flow InferenceContext Type
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph Type -> Flow InferenceContext Type)
-> Flow Graph Type -> Flow InferenceContext Type
forall a b. (a -> b) -> a -> b
$ Name -> Flow Graph Type
requireWrappedType Name
name
          Elimination
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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 Term
body) -> do
        Type
tv <- Flow InferenceContext Type
freshName
        (Term
i, [Constraint]
iconst) <- Name
-> TypeScheme
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall x.
Name
-> TypeScheme -> Flow InferenceContext x -> Flow InferenceContext x
withBinding Name
v (Type -> TypeScheme
monotype Type
tv) (Flow InferenceContext (Term, [Constraint])
 -> Flow InferenceContext (Term, [Constraint]))
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall a b. (a -> b) -> a -> b
$ Term -> Flow InferenceContext (Term, [Constraint])
infer Term
body
        Function
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yieldFunction (Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Lambda
Lambda Name
v Term
i) (Type -> Type -> Type
Types.function Type
tv (Term -> Type
termType Term
i)) [Constraint]
iconst

      FunctionPrimitive Name
name -> do
          Type
t <- (Flow Graph Type -> Flow InferenceContext Type
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph Type -> Flow InferenceContext Type)
-> Flow Graph Type -> Flow InferenceContext Type
forall a b. (a -> b) -> a -> b
$ Name -> Flow Graph Type
typeOfPrimitive Name
name) Flow InferenceContext Type
-> (Type -> Flow InferenceContext Type)
-> Flow InferenceContext Type
forall a b.
Flow InferenceContext a
-> (a -> Flow InferenceContext b) -> Flow InferenceContext b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Flow InferenceContext Type
replaceFreeVariables
          Function
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yieldFunction (Name -> Function
FunctionPrimitive Name
name) Type
t []
        where
          -- This prevents type variables from being reused across multiple instantiations of a primitive within a single element,
          -- which would lead to false unification.
          replaceFreeVariables :: Type -> Flow InferenceContext Type
replaceFreeVariables Type
t = do
              [(Name, Type)]
pairs <- (Name -> Flow InferenceContext (Name, Type))
-> [Name] -> Flow InferenceContext [(Name, 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 Name -> Flow InferenceContext (Name, Type)
forall {a}. a -> Flow InferenceContext (a, Type)
toPair ([Name] -> Flow InferenceContext [(Name, Type)])
-> [Name] -> Flow InferenceContext [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
S.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ Type -> Set Name
freeVariablesInType Type
t
              Type -> Flow InferenceContext Type
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Flow InferenceContext Type)
-> Type -> Flow InferenceContext Type
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)]
pairs) Type
t
            where
              toPair :: a -> Flow InferenceContext (a, Type)
toPair a
v = do
                Type
v' <- Flow InferenceContext Type
freshName
                (a, Type) -> Flow InferenceContext (a, Type)
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
v, Type
v')

    TermLet Let
lt -> Let -> Flow InferenceContext (Term, [Constraint])
inferLet Let
lt

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

    TermLiteral Literal
l -> Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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 InferenceContext Type
freshName
        Type
vv <- Flow InferenceContext Type
freshName
        if Map Term Term -> Bool
forall k a. Map k a -> Bool
M.null Map Term Term
m
          then Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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, [Constraint])]
triples <- ((Term, Term) -> Flow InferenceContext (Term, Term, [Constraint]))
-> [(Term, Term)]
-> Flow InferenceContext [(Term, Term, [Constraint])]
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 InferenceContext (Term, Term, [Constraint])
toTriple ([(Term, Term)]
 -> Flow InferenceContext [(Term, Term, [Constraint])])
-> [(Term, Term)]
-> Flow InferenceContext [(Term, Term, [Constraint])]
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, [Constraint]
_) -> (Term
k, Term
v)) ((Term, Term, [Constraint]) -> (Term, Term))
-> [(Term, Term, [Constraint])] -> [(Term, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, Term, [Constraint])]
triples
            let co :: [Constraint]
co = [[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((\(Term
k, Term
v, [Constraint]
c) -> [Constraint]
c [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [(Type
kv, Term -> Type
termType Term
k), (Type
vv, Term -> Type
termType Term
v)]) ((Term, Term, [Constraint]) -> [Constraint])
-> [(Term, Term, [Constraint])] -> [[Constraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, Term, [Constraint])]
triples)
            Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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) [Constraint]
co
      where
        toTriple :: (Term, Term) -> Flow InferenceContext (Term, Term, [Constraint])
toTriple (Term
k, Term
v) = do
          (Term
ik, [Constraint]
kc) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
k
          (Term
iv, [Constraint]
vc) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
v
          (Term, Term, [Constraint])
-> Flow InferenceContext (Term, Term, [Constraint])
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
ik, Term
iv, [Constraint]
kc [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
vc)

    TermOptional Maybe Term
m -> do
      Type
v <- Flow InferenceContext Type
freshName
      case Maybe Term
m of
        Maybe Term
Nothing -> Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yield (Maybe Term -> Term
TermOptional Maybe Term
forall a. Maybe a
Nothing) (Type -> Type
Types.optional Type
v) []
        Just Term
e -> do
          (Term
i, [Constraint]
ci) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
e
          Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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
v, Term -> Type
termType Term
i)Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:[Constraint]
ci)

    TermProduct [Term]
tuple -> do
      [(Term, [Constraint])]
is' <- (Term -> Flow InferenceContext (Term, [Constraint]))
-> [Term] -> Flow InferenceContext [(Term, [Constraint])]
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 InferenceContext (Term, [Constraint])
infer [Term]
tuple
      let is :: [Term]
is = (Term, [Constraint]) -> Term
forall a b. (a, b) -> a
fst ((Term, [Constraint]) -> Term) -> [(Term, [Constraint])] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, [Constraint])]
is'
      let co :: [Constraint]
co = [[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((Term, [Constraint]) -> [Constraint]
forall a b. (a, b) -> b
snd ((Term, [Constraint]) -> [Constraint])
-> [(Term, [Constraint])] -> [[Constraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, [Constraint])]
is')
      Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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) [Constraint]
co

    TermRecord (Record Name
n [Field]
fields) -> do
        RowType
rt <- Flow Graph RowType -> Flow InferenceContext RowType
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph RowType -> Flow InferenceContext RowType)
-> Flow Graph RowType -> Flow InferenceContext RowType
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Flow Graph RowType
requireRecordType Bool
True Name
n
        [(Field, [Constraint])]
ifields' <- (Field -> Flow InferenceContext (Field, [Constraint]))
-> [Field] -> Flow InferenceContext [(Field, [Constraint])]
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 InferenceContext (Field, [Constraint])
inferFieldType [Field]
fields
        let ifields :: [Field]
ifields = (Field, [Constraint]) -> Field
forall a b. (a, b) -> a
fst ((Field, [Constraint]) -> Field)
-> [(Field, [Constraint])] -> [Field]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Field, [Constraint])]
ifields'
        let ci :: [Constraint]
ci = [[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((Field, [Constraint]) -> [Constraint]
forall a b. (a, b) -> b
snd ((Field, [Constraint]) -> [Constraint])
-> [(Field, [Constraint])] -> [[Constraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Field, [Constraint])]
ifields')
        let irt :: Type
irt = RowType -> Type
TypeRecord (RowType -> Type) -> RowType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Name -> [FieldType] -> RowType
RowType Name
n Maybe Name
forall a. Maybe a
Nothing (Field -> FieldType
fieldType (Field -> FieldType) -> [Field] -> [FieldType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Field]
ifields)
        Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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 ((RowType -> Type
TypeRecord RowType
rt, Type
irt)Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:[Constraint]
ci)

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

    TermSum (Sum Int
i Int
s Term
trm) -> do
        (Term
it, [Constraint]
co) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
trm
        [Type]
types <- [Flow InferenceContext Type] -> Flow InferenceContext [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 (Term -> Int -> Flow InferenceContext Type
varOrTerm Term
it (Int -> Flow InferenceContext Type)
-> [Int] -> [Flow InferenceContext 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
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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) [Constraint]
co
      where
        varOrTerm :: Term -> Int -> Flow InferenceContext Type
varOrTerm Term
it Int
j = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
          then Type -> Flow InferenceContext Type
forall a. a -> Flow InferenceContext a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Flow InferenceContext Type)
-> Type -> Flow InferenceContext Type
forall a b. (a -> b) -> a -> b
$ Term -> Type
termType Term
it
          else Flow InferenceContext Type
freshName

    TermUnion (Injection Name
n Field
field) -> do
        RowType
rt <- Flow Graph RowType -> Flow InferenceContext RowType
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph RowType -> Flow InferenceContext RowType)
-> Flow Graph RowType -> Flow InferenceContext RowType
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> Flow Graph RowType
requireUnionType Bool
True Name
n
        FieldType
sfield <- Name -> [FieldType] -> Flow InferenceContext FieldType
findMatchingField (Field -> Name
fieldName Field
field) (RowType -> [FieldType]
rowTypeFields RowType
rt)
        (Field
ifield, [Constraint]
ci) <- Field -> Flow InferenceContext (Field, [Constraint])
inferFieldType Field
field
        let co :: Constraint
co = (Term -> Type
termType (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Field -> Term
fieldTerm Field
ifield, FieldType -> Type
fieldTypeType FieldType
sfield)

        Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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) (Constraint
coConstraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:[Constraint]
ci)

    TermVariable Name
v -> do
      Type
t <- Name -> Flow InferenceContext Type
requireName Name
v
      Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yield (Name -> Term
TermVariable Name
v) Type
t []

    TermWrap (WrappedTerm Name
name Term
term1) -> do
      Type
typ <- Flow Graph Type -> Flow InferenceContext Type
forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext (Flow Graph Type -> Flow InferenceContext Type)
-> Flow Graph Type -> Flow InferenceContext Type
forall a b. (a -> b) -> a -> b
$ Name -> Flow Graph Type
requireWrappedType Name
name
      (Term
i, [Constraint]
ci) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
term1
      Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
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) ([Constraint]
ci [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [(Type
typ, Term -> Type
termType Term
i)])

inferFieldType :: Field -> Flow InferenceContext (Field, [Constraint])
inferFieldType :: Field -> Flow InferenceContext (Field, [Constraint])
inferFieldType (Field Name
fname Term
term) = do
  (Term
i, [Constraint]
c) <- Term -> Flow InferenceContext (Term, [Constraint])
infer Term
term
  (Field, [Constraint])
-> Flow InferenceContext (Field, [Constraint])
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Term -> Field
Field Name
fname Term
i, [Constraint]
c)

inferLet :: Let -> Flow InferenceContext (Term, [Constraint])
inferLet :: Let -> Flow InferenceContext (Term, [Constraint])
inferLet (Let [LetBinding]
bindings Term
env) = String
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall s a. String -> Flow s a -> Flow s a
withTrace (String
"let(" String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") (Flow InferenceContext (Term, [Constraint])
 -> Flow InferenceContext (Term, [Constraint]))
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall a b. (a -> b) -> a -> b
$ do
    InferenceContext
state0 <- Flow InferenceContext InferenceContext
forall s. Flow s s
getState
    let e :: TypingEnvironment
e = [LetBinding] -> TypingEnvironment -> TypingEnvironment
forall {t :: * -> *}.
Foldable t =>
t LetBinding -> TypingEnvironment -> TypingEnvironment
preExtendEnv [LetBinding]
bindings (TypingEnvironment -> TypingEnvironment)
-> TypingEnvironment -> TypingEnvironment
forall a b. (a -> b) -> a -> b
$ InferenceContext -> TypingEnvironment
inferenceContextEnvironment InferenceContext
state0
    let state1 :: InferenceContext
state1 = InferenceContext
state0 {inferenceContextEnvironment = e}
    InferenceContext
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState InferenceContext
state1 (Flow InferenceContext (Term, [Constraint])
 -> Flow InferenceContext (Term, [Constraint]))
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
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
      [(Term, [Constraint])]
ivalues' <- (Term -> Flow InferenceContext (Term, [Constraint]))
-> [Term] -> Flow InferenceContext [(Term, [Constraint])]
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 InferenceContext (Term, [Constraint])
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 = (Term, [Constraint]) -> Term
forall a b. (a, b) -> a
fst ((Term, [Constraint]) -> Term) -> [(Term, [Constraint])] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, [Constraint])]
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 :: [Constraint]
bc = [[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ((Term, [Constraint]) -> [Constraint]
forall a b. (a, b) -> b
snd ((Term, [Constraint]) -> [Constraint])
-> [(Term, [Constraint])] -> [[Constraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Term, [Constraint])]
ivalues')

      let tbindings :: TypingEnvironment
tbindings = [(Name, TypeScheme)] -> TypingEnvironment
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, TypeScheme)] -> TypingEnvironment)
-> [(Name, TypeScheme)] -> TypingEnvironment
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
      (Term
ienv, [Constraint]
cenv) <- TypingEnvironment
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall x.
TypingEnvironment
-> Flow InferenceContext x -> Flow InferenceContext x
withBindings TypingEnvironment
tbindings (Flow InferenceContext (Term, [Constraint])
 -> Flow InferenceContext (Term, [Constraint]))
-> Flow InferenceContext (Term, [Constraint])
-> Flow InferenceContext (Term, [Constraint])
forall a b. (a -> b) -> a -> b
$ Term -> Flow InferenceContext (Term, [Constraint])
infer Term
env

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

instantiate :: TypeScheme -> Flow InferenceContext (Type)
instantiate :: TypeScheme -> Flow InferenceContext Type
instantiate (TypeScheme [Name]
vars Type
t) = do
    [Type]
vars1 <- (Name -> Flow InferenceContext Type)
-> [Name] -> Flow InferenceContext [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]
mapM (Flow InferenceContext Type -> Name -> Flow InferenceContext Type
forall a b. a -> b -> a
const Flow InferenceContext Type
freshName) [Name]
vars
    Type -> Flow InferenceContext Type
forall a. a -> Flow InferenceContext a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Flow InferenceContext Type)
-> Type -> Flow InferenceContext Type
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)]
zip [Name]
vars [Type]
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 InferenceContext (Type)
requireName :: Name -> Flow InferenceContext Type
requireName Name
v = do
  TypingEnvironment
env <- InferenceContext -> TypingEnvironment
inferenceContextEnvironment (InferenceContext -> TypingEnvironment)
-> Flow InferenceContext InferenceContext
-> Flow InferenceContext TypingEnvironment
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Flow InferenceContext InferenceContext
forall s. Flow s s
getState
  case Name -> TypingEnvironment -> Maybe TypeScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v TypingEnvironment
env of
    Maybe TypeScheme
Nothing -> String -> Flow InferenceContext Type
forall a. String -> Flow InferenceContext a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Flow InferenceContext Type)
-> String -> Flow InferenceContext Type
forall a b. (a -> b) -> a -> b
$ String
"variable not bound in environment: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". Environment: "
      String -> String -> String
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
<$> TypingEnvironment -> [Name]
forall k a. Map k a -> [k]
M.keys TypingEnvironment
env)
    Just TypeScheme
s  -> TypeScheme -> Flow InferenceContext Type
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) (Type)
typeOfPrimitive :: Name -> Flow Graph Type
typeOfPrimitive Name
name = Primitive -> Type
primitiveType (Primitive -> Type) -> Flow Graph Primitive -> Flow Graph Type
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 String 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 InferenceContext x -> Flow InferenceContext x
withBinding :: forall x.
Name
-> TypeScheme -> Flow InferenceContext x -> Flow InferenceContext x
withBinding Name
n TypeScheme
ts = (TypingEnvironment -> TypingEnvironment)
-> Flow InferenceContext x -> Flow InferenceContext x
forall x.
(TypingEnvironment -> TypingEnvironment)
-> Flow InferenceContext x -> Flow InferenceContext x
withEnvironment (Name -> TypeScheme -> TypingEnvironment -> TypingEnvironment
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 InferenceContext x -> Flow InferenceContext x
withBindings :: forall x.
TypingEnvironment
-> Flow InferenceContext x -> Flow InferenceContext x
withBindings TypingEnvironment
bindings = (TypingEnvironment -> TypingEnvironment)
-> Flow InferenceContext x -> Flow InferenceContext x
forall x.
(TypingEnvironment -> TypingEnvironment)
-> Flow InferenceContext x -> Flow InferenceContext x
withEnvironment (\TypingEnvironment
e -> TypingEnvironment -> TypingEnvironment -> TypingEnvironment
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union TypingEnvironment
bindings TypingEnvironment
e)

withEnvironment :: (TypingEnvironment -> TypingEnvironment) -> Flow InferenceContext x -> Flow InferenceContext x
withEnvironment :: forall x.
(TypingEnvironment -> TypingEnvironment)
-> Flow InferenceContext x -> Flow InferenceContext x
withEnvironment TypingEnvironment -> TypingEnvironment
m Flow InferenceContext x
flow = do
  InferenceContext Graph
g TypingEnvironment
e <- Flow InferenceContext InferenceContext
forall s. Flow s s
getState
  InferenceContext
-> Flow InferenceContext x -> Flow InferenceContext x
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState (Graph -> TypingEnvironment -> InferenceContext
InferenceContext Graph
g (TypingEnvironment -> TypingEnvironment
m TypingEnvironment
e)) Flow InferenceContext x
flow

withGraphContext :: Flow (Graph) x -> Flow InferenceContext x
withGraphContext :: forall x. Flow Graph x -> Flow InferenceContext x
withGraphContext Flow Graph x
f = do
  Graph
cx <- InferenceContext -> Graph
inferenceContextGraph (InferenceContext -> Graph)
-> Flow InferenceContext InferenceContext
-> Flow InferenceContext Graph
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Flow InferenceContext InferenceContext
forall s. Flow s s
getState
  Graph -> Flow Graph x -> Flow InferenceContext x
forall s1 a s2. s1 -> Flow s1 a -> Flow s2 a
withState Graph
cx Flow Graph x
f

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

yieldFunction :: Function -> Type -> [Constraint] -> Flow InferenceContext (Term, [Constraint])
yieldFunction :: Function
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yieldFunction Function
fun = Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yield (Function -> Term
TermFunction Function
fun)

yieldElimination :: Elimination -> Type -> [Constraint] -> Flow InferenceContext (Term, [Constraint])
yieldElimination :: Elimination
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yieldElimination Elimination
e = Term
-> Type
-> [Constraint]
-> Flow InferenceContext (Term, [Constraint])
yield (Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Elimination -> Function
FunctionElimination Elimination
e)