module Hydra.Inference.AltInference where

import Hydra.Basics
import Hydra.Core
import Hydra.Compute
import Hydra.Mantle
import qualified Hydra.Flows as F
import qualified Hydra.Tier1 as Tier1
import qualified Hydra.Lib.Flows as Flows
import qualified Hydra.Dsl.Types as Types

import qualified Data.List as L
import qualified Data.Map as M


--------------------------------------------------------------------------------
-- Graphs

showType :: Type -> String
showType :: Type -> String
showType (TypeFunction (FunctionType Type
dom Type
cod)) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
dom String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"→" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
cod String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
showType (TypeList Type
etyp) = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
etyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
showType (TypeLiteral LiteralType
lit) = LiteralType -> String
forall a. Show a => a -> String
show LiteralType
lit
showType (TypeMap (MapType Type
keyTyp Type
valTyp)) = String
"map<" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
keyTyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"," String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
valTyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">"
showType (TypeProduct [Type]
types) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"," ((Type -> String) -> [Type] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> String
showType [Type]
types)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
showType (TypeVariable (Name String
name)) = String
name

showTypeScheme :: TypeScheme -> String
showTypeScheme :: TypeScheme -> String
showTypeScheme (TypeScheme [Name]
vars Type
body) = String
"∀[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"," ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Name String
name) -> String
name) [Name]
vars)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
body

showConstraint :: TypeConstraint -> String
showConstraint :: TypeConstraint -> String
showConstraint (TypeConstraint Type
ltyp Type
rtyp Maybe String
_) = Type -> String
showType Type
ltyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"≡" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
rtyp

--------------------------------------------------------------------------------
-- Unification

type UnificationContext = Maybe String

data SUnificationError
  = SUnificationErrorCannotUnify Type Type UnificationContext
  | SUnificationErrorOccursCheckFailed Name Type UnificationContext
  deriving (SUnificationError -> SUnificationError -> Bool
(SUnificationError -> SUnificationError -> Bool)
-> (SUnificationError -> SUnificationError -> Bool)
-> Eq SUnificationError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SUnificationError -> SUnificationError -> Bool
== :: SUnificationError -> SUnificationError -> Bool
$c/= :: SUnificationError -> SUnificationError -> Bool
/= :: SUnificationError -> SUnificationError -> Bool
Eq, Eq SUnificationError
Eq SUnificationError =>
(SUnificationError -> SUnificationError -> Ordering)
-> (SUnificationError -> SUnificationError -> Bool)
-> (SUnificationError -> SUnificationError -> Bool)
-> (SUnificationError -> SUnificationError -> Bool)
-> (SUnificationError -> SUnificationError -> Bool)
-> (SUnificationError -> SUnificationError -> SUnificationError)
-> (SUnificationError -> SUnificationError -> SUnificationError)
-> Ord SUnificationError
SUnificationError -> SUnificationError -> Bool
SUnificationError -> SUnificationError -> Ordering
SUnificationError -> SUnificationError -> SUnificationError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SUnificationError -> SUnificationError -> Ordering
compare :: SUnificationError -> SUnificationError -> Ordering
$c< :: SUnificationError -> SUnificationError -> Bool
< :: SUnificationError -> SUnificationError -> Bool
$c<= :: SUnificationError -> SUnificationError -> Bool
<= :: SUnificationError -> SUnificationError -> Bool
$c> :: SUnificationError -> SUnificationError -> Bool
> :: SUnificationError -> SUnificationError -> Bool
$c>= :: SUnificationError -> SUnificationError -> Bool
>= :: SUnificationError -> SUnificationError -> Bool
$cmax :: SUnificationError -> SUnificationError -> SUnificationError
max :: SUnificationError -> SUnificationError -> SUnificationError
$cmin :: SUnificationError -> SUnificationError -> SUnificationError
min :: SUnificationError -> SUnificationError -> SUnificationError
Ord, Int -> SUnificationError -> String -> String
[SUnificationError] -> String -> String
SUnificationError -> String
(Int -> SUnificationError -> String -> String)
-> (SUnificationError -> String)
-> ([SUnificationError] -> String -> String)
-> Show SUnificationError
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> SUnificationError -> String -> String
showsPrec :: Int -> SUnificationError -> String -> String
$cshow :: SUnificationError -> String
show :: SUnificationError -> String
$cshowList :: [SUnificationError] -> String -> String
showList :: [SUnificationError] -> String -> String
Show)

sOccursIn :: Name -> Type -> Bool
sOccursIn :: Name -> Type -> Bool
sOccursIn Name
var Type
typ = case Type
typ of
  TypeFunction (FunctionType Type
domTyp Type
codTyp) -> Name -> Type -> Bool
sOccursIn Name
var Type
domTyp Bool -> Bool -> Bool
|| Name -> Type -> Bool
sOccursIn Name
var Type
codTyp
  TypeList Type
etyp -> Name -> Type -> Bool
sOccursIn Name
var Type
etyp
  TypeLiteral LiteralType
_ -> Bool
False
  TypeMap (MapType Type
keyTyp Type
valTyp) -> Name -> Type -> Bool
sOccursIn Name
var Type
keyTyp Bool -> Bool -> Bool
|| Name -> Type -> Bool
sOccursIn Name
var Type
valTyp
  TypeProduct [Type]
types -> (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Type -> Bool
sOccursIn Name
var) [Type]
types
  TypeVariable Name
name -> Name
var Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name

-- sComposeSubst :: SSubst -> SSubst -> SSubst
-- sComposeSubst s1 s2 = ...

{-
Robinson's algorithm, following https://www.cs.cornell.edu/courses/cs6110/2017sp/lectures/lec23.pdf
Specifically this is an implementation of the following rules:
 * Unify({(x, t)} ∪ E) = {t/x} Unify(E{t/x}) if x ∉ FV(t)
 * Unify(∅) = I (the identity substitution x ↦ x)
 * Unify({(x, x)} ∪ E) = Unify(E)
 * Unify({(f(s1, ..., sn), f(t1, ..., tn))} ∪ E) = Unify({(s1, t1), ..., (sn, tn)} ∪ E)
-}
uUnify :: [TypeConstraint] -> Either SUnificationError SSubst
-- uUnify = L.foldl helper sEmptySubst
--   where
--     helper s (TypeConstraint t1 t2 ctx) = case t1 of
--       TypeVariable v1 -> case t2 of
--         TypeVariable v2 -> if v1 == v2
--           then Right s
--           else uBind v1 t2
--         _ -> unifyVar s v1 t2
--       _ -> case t2 of
--         TypeVariable v2 -> unifyVar v2 t1
--         _ -> unifyOther s t1 t2
--     unifyVar s v t = if sOccursIn v t -- TODO: expensive occurs check
--       then Left $ SUnificationErrorOccursCheckFailed v t ctx
--       else Right $ M.singleton v t
--     unifyOther s t1 t2 = ...
uUnify :: [TypeConstraint] -> Either SUnificationError SSubst
uUnify [TypeConstraint]
constraints = case [TypeConstraint]
constraints of
    [] -> SSubst -> Either SUnificationError SSubst
forall a b. b -> Either a b
Right SSubst
sEmptySubst
    ((TypeConstraint Type
t1 Type
t2 Maybe String
ctx):[TypeConstraint]
rest) -> case Type
t1 of
        TypeVariable Name
v1 -> case Type
t2 of
          TypeVariable Name
v2 -> if Name
v1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
v2
            then [TypeConstraint] -> Either SUnificationError SSubst
uUnify [TypeConstraint]
rest
            else Name -> Type -> Either SUnificationError SSubst
uBind Name
v1 Type
t2
          Type
_ -> Name -> Type -> Either SUnificationError SSubst
uBind Name
v1 Type
t2
        Type
_ -> case Type
t2 of
          TypeVariable Name
v2 -> Name -> Type -> Either SUnificationError SSubst
uBind Name
v2 Type
t1
          Type
_ -> Type -> Type -> Either SUnificationError SSubst
uUnifyOther Type
t1 Type
t2
      where
        -- TODO: this occurs check is expensive; consider delaying it until the time of substitution
        uBind :: Name -> Type -> Either SUnificationError SSubst
uBind Name
v Type
t = if Name -> Type -> Bool
sOccursIn Name
v Type
t
            then SUnificationError -> Either SUnificationError SSubst
forall a b. a -> Either a b
Left (SUnificationError -> Either SUnificationError SSubst)
-> SUnificationError -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Maybe String -> SUnificationError
SUnificationErrorOccursCheckFailed Name
v Type
t Maybe String
ctx
            else case [TypeConstraint] -> Either SUnificationError SSubst
uUnify ((TypeConstraint -> TypeConstraint)
-> [TypeConstraint] -> [TypeConstraint]
forall a b. (a -> b) -> [a] -> [b]
L.map (Name -> Type -> TypeConstraint -> TypeConstraint
uSubstInConstraint Name
v Type
t) [TypeConstraint]
rest) of
              Left SUnificationError
err -> SUnificationError -> Either SUnificationError SSubst
forall a b. a -> Either a b
Left SUnificationError
err
              Right SSubst
subst -> SSubst -> Either SUnificationError SSubst
forall a b. b -> Either a b
Right (SSubst -> Either SUnificationError SSubst)
-> SSubst -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ Map Name Type -> SSubst
SSubst (Map Name Type -> SSubst) -> Map Name Type -> SSubst
forall a b. (a -> b) -> a -> b
$ Map Name Type -> Map Name Type -> Map Name Type
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union (Name -> Type -> Map Name Type
forall k a. k -> a -> Map k a
M.singleton Name
v (Type -> Map Name Type) -> Type -> Map Name Type
forall a b. (a -> b) -> a -> b
$ SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
t) (Map Name Type -> Map Name Type) -> Map Name Type -> Map Name Type
forall a b. (a -> b) -> a -> b
$ SSubst -> Map Name Type
sUnSubst SSubst
subst
        uUnifyOther :: Type -> Type -> Either SUnificationError SSubst
uUnifyOther Type
t1 Type
t2 = case Type
t1 of
            TypeFunction (FunctionType Type
dom1 Type
cod1) -> case Type
t2 of
              TypeFunction (FunctionType Type
dom2 Type
cod2) -> [TypeConstraint] -> Either SUnificationError SSubst
uUnify ([TypeConstraint] -> Either SUnificationError SSubst)
-> [TypeConstraint] -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ [
                (Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
dom1 Type
dom2 Maybe String
ctx), (Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
cod1 Type
cod2 Maybe String
ctx)] [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
rest
              Type
_ -> Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
            TypeList Type
l1 -> case Type
t2 of
              TypeList Type
l2 -> [TypeConstraint] -> Either SUnificationError SSubst
uUnify ([TypeConstraint] -> Either SUnificationError SSubst)
-> [TypeConstraint] -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ [(Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
l1 Type
l2 Maybe String
ctx)] [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
rest
              Type
_ -> Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
            TypeLiteral LiteralType
lit1 -> case Type
t2 of
              TypeLiteral LiteralType
lit2 -> if LiteralType
lit1 LiteralType -> LiteralType -> Bool
forall a. Eq a => a -> a -> Bool
== LiteralType
lit2
                then [TypeConstraint] -> Either SUnificationError SSubst
uUnify [TypeConstraint]
rest
                else Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
              Type
_ -> Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
            TypeMap (MapType Type
key1 Type
val1) -> case Type
t2 of
              TypeMap (MapType Type
key2 Type
val2) -> [TypeConstraint] -> Either SUnificationError SSubst
uUnify ([TypeConstraint] -> Either SUnificationError SSubst)
-> [TypeConstraint] -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ [
                (Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
key1 Type
key2 Maybe String
ctx), (Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
val1 Type
val2 Maybe String
ctx)] [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
rest
              Type
_ -> Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
            TypeProduct [Type]
types1 -> case Type
t2 of
              TypeProduct [Type]
types2 -> if [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Type]
types1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Type]
types2
                then Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
                else [TypeConstraint] -> Either SUnificationError SSubst
uUnify ([TypeConstraint] -> Either SUnificationError SSubst)
-> [TypeConstraint] -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> TypeConstraint)
-> [Type] -> [Type] -> [TypeConstraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
L.zipWith (\Type
t1 Type
t2 -> Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
t1 Type
t2 Maybe String
ctx) [Type]
types1 [Type]
types2 [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
rest
              Type
_ -> Either SUnificationError SSubst
forall {b}. Either SUnificationError b
cannotUnify
          where
            cannotUnify :: Either SUnificationError b
cannotUnify = SUnificationError -> Either SUnificationError b
forall a b. a -> Either a b
Left (SUnificationError -> Either SUnificationError b)
-> SUnificationError -> Either SUnificationError b
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Maybe String -> SUnificationError
SUnificationErrorCannotUnify Type
t1 Type
t2 Maybe String
ctx

-- TODO: substituting one variable at a time is inefficient
uSubst :: Name -> Type -> Type -> Type
uSubst :: Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
typ = case Type
typ of
  TypeFunction (FunctionType Type
dom Type
cod) -> FunctionType -> Type
TypeFunction (FunctionType -> Type) -> FunctionType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> FunctionType
FunctionType (Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
dom) (Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
cod)
  TypeList Type
etyp -> Type -> Type
TypeList (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
etyp
  TypeLiteral LiteralType
_ -> Type
typ
  TypeMap (MapType Type
key Type
val) -> MapType -> Type
TypeMap (MapType -> Type) -> MapType -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> MapType
MapType (Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
key) (Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
val)
  TypeProduct [Type]
types -> [Type] -> Type
TypeProduct ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Type -> Type -> Type
uSubst Name
v Type
t) [Type]
types
  TypeVariable Name
name -> if Name
name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
v then Type
t else Type
typ

uSubstInConstraint :: Name -> Type -> TypeConstraint -> TypeConstraint
uSubstInConstraint :: Name -> Type -> TypeConstraint -> TypeConstraint
uSubstInConstraint Name
v Type
t (TypeConstraint Type
t1 Type
t2 Maybe String
ctx) = Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
t1) (Name -> Type -> Type -> Type
uSubst Name
v Type
t Type
t2) Maybe String
ctx

--------------------------------------------------------------------------------
-- Substitution

data SSubst = SSubst { SSubst -> Map Name Type
sUnSubst :: M.Map Name Type }

instance Show SSubst where
  show :: SSubst -> String
show (SSubst Map Name Type
subst) = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
", " (((Name, Type) -> String) -> [(Name, Type)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((Name String
k), Type
v) -> String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showType Type
v) ([(Name, Type)] -> [String]) -> [(Name, Type)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map Name Type -> [(Name, Type)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name Type
subst) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

sEmptySubst :: SSubst
sEmptySubst = Map Name Type -> SSubst
SSubst Map Name Type
forall k a. Map k a
M.empty

sSubstituteTypeVariables :: SSubst -> Type -> Type
sSubstituteTypeVariables :: SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
typ = case Type
typ of
  TypeFunction (FunctionType Type
dom Type
cod) -> FunctionType -> Type
TypeFunction (FunctionType -> Type) -> FunctionType -> Type
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> FunctionType
FunctionType (SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
dom) (SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
cod)
  TypeList Type
etyp -> Type -> Type
TypeList (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
etyp
  TypeLiteral LiteralType
_ -> Type
typ
  TypeMap (MapType Type
key Type
val) -> MapType -> Type
TypeMap (MapType -> Type) -> MapType -> Type
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> MapType
MapType (SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
key) (SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
val)
  TypeProduct [Type]
types -> [Type] -> Type
TypeProduct ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst) [Type]
types
  TypeVariable Name
name -> case Name -> Map Name Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
name (SSubst -> Map Name Type
sUnSubst SSubst
subst) of
    Just Type
styp -> Type
styp
    Maybe Type
Nothing -> Type
typ

-- TODO: remove unused bound type variables
sSubstituteTypeVariablesInScheme :: SSubst -> TypeScheme -> TypeScheme
sSubstituteTypeVariablesInScheme :: SSubst -> TypeScheme -> TypeScheme
sSubstituteTypeVariablesInScheme SSubst
subst (TypeScheme [Name]
vars Type
typ) = [Name] -> Type -> TypeScheme
TypeScheme [Name]
vars (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst Type
typ


--------------------------------------------------------------------------------
-- Inference

data SInferenceContext
  = SInferenceContext {
    SInferenceContext -> Map Name TypeScheme
sInferenceContextLexicon :: M.Map Name TypeScheme,
    SInferenceContext -> Int
sInferenceContextVariableCount :: Int,
    SInferenceContext -> Map Name TypeScheme
sInferenceContextTypingEnvironment :: M.Map Name TypeScheme}
  deriving (SInferenceContext -> SInferenceContext -> Bool
(SInferenceContext -> SInferenceContext -> Bool)
-> (SInferenceContext -> SInferenceContext -> Bool)
-> Eq SInferenceContext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SInferenceContext -> SInferenceContext -> Bool
== :: SInferenceContext -> SInferenceContext -> Bool
$c/= :: SInferenceContext -> SInferenceContext -> Bool
/= :: SInferenceContext -> SInferenceContext -> Bool
Eq, Eq SInferenceContext
Eq SInferenceContext =>
(SInferenceContext -> SInferenceContext -> Ordering)
-> (SInferenceContext -> SInferenceContext -> Bool)
-> (SInferenceContext -> SInferenceContext -> Bool)
-> (SInferenceContext -> SInferenceContext -> Bool)
-> (SInferenceContext -> SInferenceContext -> Bool)
-> (SInferenceContext -> SInferenceContext -> SInferenceContext)
-> (SInferenceContext -> SInferenceContext -> SInferenceContext)
-> Ord SInferenceContext
SInferenceContext -> SInferenceContext -> Bool
SInferenceContext -> SInferenceContext -> Ordering
SInferenceContext -> SInferenceContext -> SInferenceContext
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SInferenceContext -> SInferenceContext -> Ordering
compare :: SInferenceContext -> SInferenceContext -> Ordering
$c< :: SInferenceContext -> SInferenceContext -> Bool
< :: SInferenceContext -> SInferenceContext -> Bool
$c<= :: SInferenceContext -> SInferenceContext -> Bool
<= :: SInferenceContext -> SInferenceContext -> Bool
$c> :: SInferenceContext -> SInferenceContext -> Bool
> :: SInferenceContext -> SInferenceContext -> Bool
$c>= :: SInferenceContext -> SInferenceContext -> Bool
>= :: SInferenceContext -> SInferenceContext -> Bool
$cmax :: SInferenceContext -> SInferenceContext -> SInferenceContext
max :: SInferenceContext -> SInferenceContext -> SInferenceContext
$cmin :: SInferenceContext -> SInferenceContext -> SInferenceContext
min :: SInferenceContext -> SInferenceContext -> SInferenceContext
Ord, Int -> SInferenceContext -> String -> String
[SInferenceContext] -> String -> String
SInferenceContext -> String
(Int -> SInferenceContext -> String -> String)
-> (SInferenceContext -> String)
-> ([SInferenceContext] -> String -> String)
-> Show SInferenceContext
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> SInferenceContext -> String -> String
showsPrec :: Int -> SInferenceContext -> String -> String
$cshow :: SInferenceContext -> String
show :: SInferenceContext -> String
$cshowList :: [SInferenceContext] -> String -> String
showList :: [SInferenceContext] -> String -> String
Show)

data SInferenceResult
  = SInferenceResult {
    SInferenceResult -> TypeScheme
sInferenceResultScheme :: TypeScheme,
    SInferenceResult -> [TypeConstraint]
sInferenceResultConstraints :: [TypeConstraint]}
  deriving (SInferenceResult -> SInferenceResult -> Bool
(SInferenceResult -> SInferenceResult -> Bool)
-> (SInferenceResult -> SInferenceResult -> Bool)
-> Eq SInferenceResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SInferenceResult -> SInferenceResult -> Bool
== :: SInferenceResult -> SInferenceResult -> Bool
$c/= :: SInferenceResult -> SInferenceResult -> Bool
/= :: SInferenceResult -> SInferenceResult -> Bool
Eq, Eq SInferenceResult
Eq SInferenceResult =>
(SInferenceResult -> SInferenceResult -> Ordering)
-> (SInferenceResult -> SInferenceResult -> Bool)
-> (SInferenceResult -> SInferenceResult -> Bool)
-> (SInferenceResult -> SInferenceResult -> Bool)
-> (SInferenceResult -> SInferenceResult -> Bool)
-> (SInferenceResult -> SInferenceResult -> SInferenceResult)
-> (SInferenceResult -> SInferenceResult -> SInferenceResult)
-> Ord SInferenceResult
SInferenceResult -> SInferenceResult -> Bool
SInferenceResult -> SInferenceResult -> Ordering
SInferenceResult -> SInferenceResult -> SInferenceResult
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SInferenceResult -> SInferenceResult -> Ordering
compare :: SInferenceResult -> SInferenceResult -> Ordering
$c< :: SInferenceResult -> SInferenceResult -> Bool
< :: SInferenceResult -> SInferenceResult -> Bool
$c<= :: SInferenceResult -> SInferenceResult -> Bool
<= :: SInferenceResult -> SInferenceResult -> Bool
$c> :: SInferenceResult -> SInferenceResult -> Bool
> :: SInferenceResult -> SInferenceResult -> Bool
$c>= :: SInferenceResult -> SInferenceResult -> Bool
>= :: SInferenceResult -> SInferenceResult -> Bool
$cmax :: SInferenceResult -> SInferenceResult -> SInferenceResult
max :: SInferenceResult -> SInferenceResult -> SInferenceResult
$cmin :: SInferenceResult -> SInferenceResult -> SInferenceResult
min :: SInferenceResult -> SInferenceResult -> SInferenceResult
Ord)
instance Show SInferenceResult where
  show :: SInferenceResult -> String
show (SInferenceResult TypeScheme
scheme [TypeConstraint]
constraints) = String
"{type= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeScheme -> String
showTypeScheme TypeScheme
scheme String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", constraints= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [TypeConstraint] -> String
forall a. Show a => a -> String
show [TypeConstraint]
constraints String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

sInferType :: Term -> Flow SInferenceContext TypeScheme
sInferType :: Term -> Flow SInferenceContext TypeScheme
sInferType Term
term = Flow SInferenceContext SInferenceResult
-> (SInferenceResult -> Flow SInferenceContext TypeScheme)
-> Flow SInferenceContext TypeScheme
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
term) SInferenceResult -> Flow SInferenceContext TypeScheme
unifyAndSubst
  where
    unifyAndSubst :: SInferenceResult -> Flow SInferenceContext TypeScheme
    unifyAndSubst :: SInferenceResult -> Flow SInferenceContext TypeScheme
unifyAndSubst SInferenceResult
result = Flow SInferenceContext SSubst
-> (SSubst -> Flow SInferenceContext TypeScheme)
-> Flow SInferenceContext TypeScheme
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Either SUnificationError SSubst -> Flow SInferenceContext SSubst
forall e a c. Show e => Either e a -> Flow c a
F.fromEither (Either SUnificationError SSubst -> Flow SInferenceContext SSubst)
-> Either SUnificationError SSubst -> Flow SInferenceContext SSubst
forall a b. (a -> b) -> a -> b
$ [TypeConstraint] -> Either SUnificationError SSubst
uUnify ([TypeConstraint] -> Either SUnificationError SSubst)
-> [TypeConstraint] -> Either SUnificationError SSubst
forall a b. (a -> b) -> a -> b
$ SInferenceResult -> [TypeConstraint]
sInferenceResultConstraints SInferenceResult
result) SSubst -> Flow SInferenceContext TypeScheme
doSubst
      where
        doSubst :: SSubst -> Flow SInferenceContext TypeScheme
        doSubst :: SSubst -> Flow SInferenceContext TypeScheme
doSubst SSubst
subst = TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiateAndNormalize (TypeScheme -> Flow SInferenceContext TypeScheme)
-> TypeScheme -> Flow SInferenceContext TypeScheme
forall a b. (a -> b) -> a -> b
$ SSubst -> TypeScheme -> TypeScheme
sSubstituteTypeVariablesInScheme SSubst
subst (TypeScheme -> TypeScheme) -> TypeScheme -> TypeScheme
forall a b. (a -> b) -> a -> b
$ SInferenceResult -> TypeScheme
sInferenceResultScheme SInferenceResult
result

sInferTypeInternal :: Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal :: Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
term = case Term
term of

    TermApplication (Application Term
lterm Term
rterm) -> Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withVar1
      where
        withVar1 :: Name -> Flow SInferenceContext SInferenceResult
withVar1 Name
dom = Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withVar2
          where
            withVar2 :: Name -> Flow SInferenceContext SInferenceResult
withVar2 Name
cod = Flow SInferenceContext SInferenceResult
-> (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
lterm) SInferenceResult -> Flow SInferenceContext SInferenceResult
withLeft
              where
                withLeft :: SInferenceResult -> Flow SInferenceContext SInferenceResult
withLeft SInferenceResult
lresult = Flow SInferenceContext SInferenceResult
-> (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
rterm) SInferenceResult -> Flow SInferenceContext SInferenceResult
forall {s}. SInferenceResult -> Flow s SInferenceResult
withRight
                  where
                    withRight :: SInferenceResult -> Flow s SInferenceResult
withRight SInferenceResult
rresult = SInferenceResult -> Flow s SInferenceResult
forall x s. x -> Flow s x
Flows.pure (SInferenceResult -> Flow s SInferenceResult)
-> SInferenceResult -> Flow s SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> [TypeConstraint] -> SInferenceResult
SInferenceResult ([Name] -> Type -> TypeScheme
TypeScheme [Name]
tvars (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
cod) ([TypeConstraint] -> SInferenceResult)
-> [TypeConstraint] -> SInferenceResult
forall a b. (a -> b) -> a -> b
$ [
                        Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Type -> Type -> Type
Types.function (Name -> Type
TypeVariable Name
dom) (Name -> Type
TypeVariable Name
cod)) Type
ltyp Maybe String
ctx,
                        Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Name -> Type
TypeVariable Name
dom) Type
rtyp Maybe String
ctx]
                        [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ SInferenceResult -> [TypeConstraint]
sInferenceResultConstraints SInferenceResult
lresult [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ SInferenceResult -> [TypeConstraint]
sInferenceResultConstraints SInferenceResult
rresult
                      where
                        ctx :: Maybe String
ctx = String -> Maybe String
forall a. a -> Maybe a
Just String
"application"
                        ltyp :: Type
ltyp = TypeScheme -> Type
typeSchemeType (TypeScheme -> Type) -> TypeScheme -> Type
forall a b. (a -> b) -> a -> b
$ SInferenceResult -> TypeScheme
sInferenceResultScheme SInferenceResult
lresult
                        rtyp :: Type
rtyp = TypeScheme -> Type
typeSchemeType (TypeScheme -> Type) -> TypeScheme -> Type
forall a b. (a -> b) -> a -> b
$ SInferenceResult -> TypeScheme
sInferenceResultScheme SInferenceResult
rresult
                        tvars :: [Name]
tvars = TypeScheme -> [Name]
typeSchemeVariables (SInferenceResult -> TypeScheme
sInferenceResultScheme SInferenceResult
lresult) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ TypeScheme -> [Name]
typeSchemeVariables (SInferenceResult -> TypeScheme
sInferenceResultScheme SInferenceResult
rresult)

    TermFunction (FunctionLambda (Lambda Name
var Maybe Type
_ Term
body)) -> Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withVar
     where
        withVar :: Name -> Flow SInferenceContext SInferenceResult
withVar Name
tvar = Name
-> TypeScheme
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall a.
Name
-> TypeScheme
-> Flow SInferenceContext a
-> Flow SInferenceContext a
sWithTypeBinding Name
var (Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
tvar) (Flow SInferenceContext SInferenceResult
 -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ (SInferenceResult -> SInferenceResult)
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map SInferenceResult -> SInferenceResult
withBodyType (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
body)
          where
            -- TODO: prove that tvar will never appear in vars
            withBodyType :: SInferenceResult -> SInferenceResult
withBodyType (SInferenceResult (TypeScheme [Name]
vars Type
t) [TypeConstraint]
constraints)
              = TypeScheme -> [TypeConstraint] -> SInferenceResult
SInferenceResult ([Name] -> Type -> TypeScheme
TypeScheme (Name
tvarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
vars) (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.function (Name -> Type
TypeVariable Name
tvar) Type
t) [TypeConstraint]
constraints

    -- TODO: propagate rawValueVars and envVars into the final result, possibly after substitution
    -- TODO: recursive and mutually recursive let
    TermLet (Let [LetBinding]
bindings Term
env) -> if [LetBinding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [LetBinding]
bindings Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2
        then Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal (Term -> Flow SInferenceContext SInferenceResult)
-> Term -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ Let -> Term
TermLet ([LetBinding] -> Term -> Let
Let [[LetBinding] -> LetBinding
forall a. HasCallStack => [a] -> a
L.head [LetBinding]
bindings] (Term -> Let) -> Term -> Let
forall a b. (a -> b) -> a -> b
$ Let -> Term
TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Let ([LetBinding] -> [LetBinding]
forall a. HasCallStack => [a] -> [a]
L.tail [LetBinding]
bindings) Term
env)
        else LetBinding -> Flow SInferenceContext SInferenceResult
forSingleBinding (LetBinding -> Flow SInferenceContext SInferenceResult)
-> LetBinding -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> LetBinding
forall a. HasCallStack => [a] -> a
L.head [LetBinding]
bindings
      where
        forSingleBinding :: LetBinding -> Flow SInferenceContext SInferenceResult
forSingleBinding (LetBinding Name
key Term
value Maybe TypeScheme
_) = Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withVar
          where
            -- Create a temporary type variable for the binding
            withVar :: Name -> Flow SInferenceContext SInferenceResult
withVar Name
var = Name
-> TypeScheme
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall a.
Name
-> TypeScheme
-> Flow SInferenceContext a
-> Flow SInferenceContext a
sWithTypeBinding Name
key (Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
var) (Flow SInferenceContext SInferenceResult
 -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$
                Flow SInferenceContext SInferenceResult
-> (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
value) SInferenceResult -> Flow SInferenceContext SInferenceResult
withValueType
              where
                -- Unify and substitute over the value constraints
                -- TODO: save the substitution and pass it along, instead of the original set of constraints
                withValueType :: SInferenceResult -> Flow SInferenceContext SInferenceResult
withValueType (SInferenceResult TypeScheme
rawValueScheme [TypeConstraint]
valueConstraints) = Flow SInferenceContext SSubst
-> (SSubst -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Either SUnificationError SSubst -> Flow SInferenceContext SSubst
forall e a c. Show e => Either e a -> Flow c a
F.fromEither (Either SUnificationError SSubst -> Flow SInferenceContext SSubst)
-> Either SUnificationError SSubst -> Flow SInferenceContext SSubst
forall a b. (a -> b) -> a -> b
$ [TypeConstraint] -> Either SUnificationError SSubst
uUnify [TypeConstraint]
kvConstraints) SSubst -> Flow SInferenceContext SInferenceResult
afterUnification
                  where
                    rawValueVars :: [Name]
rawValueVars = TypeScheme -> [Name]
typeSchemeVariables TypeScheme
rawValueScheme
                    kvConstraints :: [TypeConstraint]
kvConstraints = TypeConstraint
keyConstraintTypeConstraint -> [TypeConstraint] -> [TypeConstraint]
forall a. a -> [a] -> [a]
:[TypeConstraint]
valueConstraints
                    keyConstraint :: TypeConstraint
keyConstraint = Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Name -> Type
TypeVariable Name
var) (TypeScheme -> Type
typeSchemeType TypeScheme
rawValueScheme) (Maybe String -> TypeConstraint) -> Maybe String -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"let binding"
                    -- Now update the type binding to use the inferred type
                    afterUnification :: SSubst -> Flow SInferenceContext SInferenceResult
afterUnification SSubst
subst = Name
-> TypeScheme
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall a.
Name
-> TypeScheme
-> Flow SInferenceContext a
-> Flow SInferenceContext a
sWithTypeBinding Name
key TypeScheme
valueScheme
                        (Flow SInferenceContext SInferenceResult
 -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ (SInferenceResult -> SInferenceResult)
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map SInferenceResult -> SInferenceResult
withEnvType (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
env)
                      where
                        valueScheme :: TypeScheme
valueScheme = SSubst -> TypeScheme -> TypeScheme
sSubstituteTypeVariablesInScheme SSubst
subst TypeScheme
rawValueScheme
                        withEnvType :: SInferenceResult -> SInferenceResult
withEnvType (SInferenceResult TypeScheme
envScheme [TypeConstraint]
envConstraints) = TypeScheme -> [TypeConstraint] -> SInferenceResult
SInferenceResult TypeScheme
envScheme [TypeConstraint]
constraints
                          where
                            constraints :: [TypeConstraint]
constraints = [TypeConstraint]
kvConstraints [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
envConstraints
                            envVars :: [Name]
envVars = TypeScheme -> [Name]
typeSchemeVariables TypeScheme
envScheme

    TermList [Term]
els -> Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withVar
      where
        withVar :: Name -> Flow SInferenceContext SInferenceResult
withVar Name
tvar = if [Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Term]
els
            then SInferenceResult -> Flow SInferenceContext SInferenceResult
forall x s. x -> Flow s x
Flows.pure (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> SInferenceResult -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> [TypeConstraint] -> SInferenceResult
yield ([Name] -> Type -> TypeScheme
TypeScheme [Name
tvar] (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type
Types.list (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
tvar) []
            else ([SInferenceResult] -> SInferenceResult)
-> Flow SInferenceContext [SInferenceResult]
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map [SInferenceResult] -> SInferenceResult
fromResults ([Flow SInferenceContext SInferenceResult]
-> Flow SInferenceContext [SInferenceResult]
forall s x. [Flow s x] -> Flow s [x]
Flows.sequence (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal (Term -> Flow SInferenceContext SInferenceResult)
-> [Term] -> [Flow SInferenceContext SInferenceResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
els))
          where
            fromResults :: [SInferenceResult] -> SInferenceResult
fromResults [SInferenceResult]
results = TypeScheme -> [TypeConstraint] -> SInferenceResult
yield ([Name] -> Type -> TypeScheme
TypeScheme [Name]
vars (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type
Types.list (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
tvar) [TypeConstraint]
constraints
              where
                uctx :: Maybe String
uctx = String -> Maybe String
forall a. a -> Maybe a
Just String
"list element"
                constraints :: [TypeConstraint]
constraints = [TypeConstraint]
cinner [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
couter
                cinner :: [TypeConstraint]
cinner = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (SInferenceResult -> [TypeConstraint]
sInferenceResultConstraints (SInferenceResult -> [TypeConstraint])
-> [SInferenceResult] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SInferenceResult]
results)
                couter :: [TypeConstraint]
couter = (Type -> TypeConstraint) -> [Type] -> [TypeConstraint]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Type
t -> Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Name -> Type
TypeVariable Name
tvar) Type
t Maybe String
uctx) [Type]
types
                types :: [Type]
types = TypeScheme -> Type
typeSchemeType (TypeScheme -> Type)
-> (SInferenceResult -> TypeScheme) -> SInferenceResult -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInferenceResult -> TypeScheme
sInferenceResultScheme (SInferenceResult -> Type) -> [SInferenceResult] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SInferenceResult]
results
                vars :: [Name]
vars = [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (TypeScheme -> [Name]
typeSchemeVariables (TypeScheme -> [Name])
-> (SInferenceResult -> TypeScheme) -> SInferenceResult -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInferenceResult -> TypeScheme
sInferenceResultScheme (SInferenceResult -> [Name]) -> [SInferenceResult] -> [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SInferenceResult]
results)

    TermLiteral Literal
lit -> SInferenceResult -> Flow SInferenceContext SInferenceResult
forall x s. x -> Flow s x
Flows.pure (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> SInferenceResult -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> SInferenceResult
yieldWithoutConstraints (TypeScheme -> SInferenceResult) -> TypeScheme -> SInferenceResult
forall a b. (a -> b) -> a -> b
$ Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ LiteralType -> Type
TypeLiteral (LiteralType -> Type) -> LiteralType -> Type
forall a b. (a -> b) -> a -> b
$ Literal -> LiteralType
literalType Literal
lit

    TermMap Map Term Term
m -> Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withKeyVar
      where
        withKeyVar :: Name -> Flow SInferenceContext SInferenceResult
withKeyVar Name
kvar = Flow SInferenceContext Name
-> (Name -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind Flow SInferenceContext Name
sNewVar Name -> Flow SInferenceContext SInferenceResult
withValueVar
          where
            withValueVar :: Name -> Flow SInferenceContext SInferenceResult
withValueVar Name
vvar = if Map Term Term -> Bool
forall k a. Map k a -> Bool
M.null Map Term Term
m
               then SInferenceResult -> Flow SInferenceContext SInferenceResult
forall x s. x -> Flow s x
Flows.pure (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> SInferenceResult -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> [TypeConstraint] -> SInferenceResult
yield ([Name] -> Type -> TypeScheme
TypeScheme [Name
kvar, Name
vvar] (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.map (Name -> Type
TypeVariable Name
kvar) (Name -> Type
TypeVariable Name
vvar)) []
               else ([([Name], [TypeConstraint])] -> SInferenceResult)
-> Flow SInferenceContext [([Name], [TypeConstraint])]
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map [([Name], [TypeConstraint])] -> SInferenceResult
forall {t :: * -> *}.
(Foldable t, Functor t) =>
t ([Name], [TypeConstraint]) -> SInferenceResult
withResults ([Flow SInferenceContext ([Name], [TypeConstraint])]
-> Flow SInferenceContext [([Name], [TypeConstraint])]
forall s x. [Flow s x] -> Flow s [x]
Flows.sequence ([Flow SInferenceContext ([Name], [TypeConstraint])]
 -> Flow SInferenceContext [([Name], [TypeConstraint])])
-> [Flow SInferenceContext ([Name], [TypeConstraint])]
-> Flow SInferenceContext [([Name], [TypeConstraint])]
forall a b. (a -> b) -> a -> b
$ ((Term, Term) -> Flow SInferenceContext ([Name], [TypeConstraint]))
-> [(Term, Term)]
-> [Flow SInferenceContext ([Name], [TypeConstraint])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Flow SInferenceContext ([Name], [TypeConstraint])
fromPair ([(Term, Term)]
 -> [Flow SInferenceContext ([Name], [TypeConstraint])])
-> [(Term, Term)]
-> [Flow SInferenceContext ([Name], [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)
              where
                fromPair :: (Term, Term) -> Flow SInferenceContext ([Name], [TypeConstraint])
fromPair (Term
k, Term
v) = Flow SInferenceContext SInferenceResult
-> (SInferenceResult
    -> Flow SInferenceContext ([Name], [TypeConstraint]))
-> Flow SInferenceContext ([Name], [TypeConstraint])
forall s x y. Flow s x -> (x -> Flow s y) -> Flow s y
Flows.bind (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
k) SInferenceResult
-> Flow SInferenceContext ([Name], [TypeConstraint])
withKeyType
                  where
                    withKeyType :: SInferenceResult
-> Flow SInferenceContext ([Name], [TypeConstraint])
withKeyType (SInferenceResult (TypeScheme [Name]
kvars Type
kt) [TypeConstraint]
kconstraints) = (SInferenceResult -> ([Name], [TypeConstraint]))
-> Flow SInferenceContext SInferenceResult
-> Flow SInferenceContext ([Name], [TypeConstraint])
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map SInferenceResult -> ([Name], [TypeConstraint])
withValueType (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
v)
                      where
                        withValueType :: SInferenceResult -> ([Name], [TypeConstraint])
withValueType (SInferenceResult (TypeScheme [Name]
vvars Type
vt) [TypeConstraint]
vconstraints)
                          = ([Name]
kvars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
vvars,
                             [Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Name -> Type
TypeVariable Name
kvar) Type
kt (Maybe String -> TypeConstraint) -> Maybe String -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"map key",
                              Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint (Name -> Type
TypeVariable Name
vvar) Type
vt (Maybe String -> TypeConstraint) -> Maybe String -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"map value"]
                              [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
kconstraints [TypeConstraint] -> [TypeConstraint] -> [TypeConstraint]
forall a. [a] -> [a] -> [a]
++ [TypeConstraint]
vconstraints)
                withResults :: t ([Name], [TypeConstraint]) -> SInferenceResult
withResults t ([Name], [TypeConstraint])
pairs = TypeScheme -> [TypeConstraint] -> SInferenceResult
yield ([Name] -> Type -> TypeScheme
TypeScheme (t [Name] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (([Name], [TypeConstraint]) -> [Name]
forall a b. (a, b) -> a
fst (([Name], [TypeConstraint]) -> [Name])
-> t ([Name], [TypeConstraint]) -> t [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t ([Name], [TypeConstraint])
pairs)) (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.map (Name -> Type
TypeVariable Name
kvar) (Name -> Type
TypeVariable Name
vvar)) ([TypeConstraint] -> SInferenceResult)
-> [TypeConstraint] -> SInferenceResult
forall a b. (a -> b) -> a -> b
$
                  t [TypeConstraint] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (([Name], [TypeConstraint]) -> [TypeConstraint]
forall a b. (a, b) -> b
snd (([Name], [TypeConstraint]) -> [TypeConstraint])
-> t ([Name], [TypeConstraint]) -> t [TypeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t ([Name], [TypeConstraint])
pairs)

    TermFunction (FunctionPrimitive Name
name) -> (SInferenceContext
 -> Trace -> FlowState SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x. (s -> Trace -> FlowState s x) -> Flow s x
Flow ((SInferenceContext
  -> Trace -> FlowState SInferenceContext SInferenceResult)
 -> Flow SInferenceContext SInferenceResult)
-> (SInferenceContext
    -> Trace -> FlowState SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ \SInferenceContext
ctx Trace
t -> case Name -> Map Name TypeScheme -> Maybe TypeScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
name (SInferenceContext -> Map Name TypeScheme
sInferenceContextLexicon SInferenceContext
ctx) of
      Just TypeScheme
scheme -> Flow SInferenceContext SInferenceResult
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext SInferenceResult
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow ((TypeScheme -> SInferenceResult)
-> Flow SInferenceContext TypeScheme
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map TypeScheme -> SInferenceResult
withoutConstraints (Flow SInferenceContext TypeScheme
 -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext TypeScheme
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiate TypeScheme
scheme) SInferenceContext
ctx Trace
t
      Maybe TypeScheme
Nothing -> Flow SInferenceContext SInferenceResult
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext SInferenceResult
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow (String -> Flow SInferenceContext SInferenceResult
forall s x. String -> Flow s x
Flows.fail (String -> Flow SInferenceContext SInferenceResult)
-> String -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ String
"No such primitive: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
name) SInferenceContext
ctx Trace
t

    TermProduct [Term]
els -> if [Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Term]
els
      then SInferenceResult -> Flow SInferenceContext SInferenceResult
forall x s. x -> Flow s x
Flows.pure (SInferenceResult -> Flow SInferenceContext SInferenceResult)
-> SInferenceResult -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> [TypeConstraint] -> SInferenceResult
yield (Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
Types.product []) []
      else ([SInferenceResult] -> SInferenceResult)
-> Flow SInferenceContext [SInferenceResult]
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map [SInferenceResult] -> SInferenceResult
fromResults ([Flow SInferenceContext SInferenceResult]
-> Flow SInferenceContext [SInferenceResult]
forall s x. [Flow s x] -> Flow s [x]
Flows.sequence (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal (Term -> Flow SInferenceContext SInferenceResult)
-> [Term] -> [Flow SInferenceContext SInferenceResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
els))
      where
        fromResults :: [SInferenceResult] -> SInferenceResult
fromResults [SInferenceResult]
results = TypeScheme -> [TypeConstraint] -> SInferenceResult
yield ([Name] -> Type -> TypeScheme
TypeScheme [Name]
tvars (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
TypeProduct [Type]
tbodies) [TypeConstraint]
constraints
          where
            tvars :: [Name]
tvars = [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ([[Name]] -> [Name]) -> [[Name]] -> [Name]
forall a b. (a -> b) -> a -> b
$ TypeScheme -> [Name]
typeSchemeVariables (TypeScheme -> [Name])
-> (SInferenceResult -> TypeScheme) -> SInferenceResult -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInferenceResult -> TypeScheme
sInferenceResultScheme (SInferenceResult -> [Name]) -> [SInferenceResult] -> [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SInferenceResult]
results
            tbodies :: [Type]
tbodies = TypeScheme -> Type
typeSchemeType (TypeScheme -> Type)
-> (SInferenceResult -> TypeScheme) -> SInferenceResult -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInferenceResult -> TypeScheme
sInferenceResultScheme (SInferenceResult -> Type) -> [SInferenceResult] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SInferenceResult]
results
            constraints :: [TypeConstraint]
constraints = [[TypeConstraint]] -> [TypeConstraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ([[TypeConstraint]] -> [TypeConstraint])
-> [[TypeConstraint]] -> [TypeConstraint]
forall a b. (a -> b) -> a -> b
$ SInferenceResult -> [TypeConstraint]
sInferenceResultConstraints (SInferenceResult -> [TypeConstraint])
-> [SInferenceResult] -> [[TypeConstraint]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SInferenceResult]
results

    TermVariable Name
var -> (SInferenceContext
 -> Trace -> FlowState SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall s x. (s -> Trace -> FlowState s x) -> Flow s x
Flow ((SInferenceContext
  -> Trace -> FlowState SInferenceContext SInferenceResult)
 -> Flow SInferenceContext SInferenceResult)
-> (SInferenceContext
    -> Trace -> FlowState SInferenceContext SInferenceResult)
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ \SInferenceContext
ctx Trace
t -> case Name -> Map Name TypeScheme -> Maybe TypeScheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
var (SInferenceContext -> Map Name TypeScheme
sInferenceContextTypingEnvironment SInferenceContext
ctx) of
      Just TypeScheme
scheme -> Flow SInferenceContext SInferenceResult
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext SInferenceResult
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow ((TypeScheme -> SInferenceResult)
-> Flow SInferenceContext TypeScheme
-> Flow SInferenceContext SInferenceResult
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map TypeScheme -> SInferenceResult
withoutConstraints (Flow SInferenceContext TypeScheme
 -> Flow SInferenceContext SInferenceResult)
-> Flow SInferenceContext TypeScheme
-> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiate TypeScheme
scheme) SInferenceContext
ctx Trace
t
      Maybe TypeScheme
Nothing -> Flow SInferenceContext SInferenceResult
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext SInferenceResult
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow (String -> Flow SInferenceContext SInferenceResult
forall s x. String -> Flow s x
Flows.fail (String -> Flow SInferenceContext SInferenceResult)
-> String -> Flow SInferenceContext SInferenceResult
forall a b. (a -> b) -> a -> b
$ String
"Variable not bound to type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
unName Name
var) SInferenceContext
ctx Trace
t

  where
    unsupported :: Flow s x
unsupported = String -> Flow s x
forall s x. String -> Flow s x
Flows.fail String
"Not yet supported"
    yield :: TypeScheme -> [TypeConstraint] -> SInferenceResult
yield = TypeScheme -> [TypeConstraint] -> SInferenceResult
SInferenceResult
    yieldWithoutConstraints :: TypeScheme -> SInferenceResult
yieldWithoutConstraints TypeScheme
scheme = TypeScheme -> [TypeConstraint] -> SInferenceResult
yield TypeScheme
scheme []
    withoutConstraints :: TypeScheme -> SInferenceResult
withoutConstraints TypeScheme
scheme = TypeScheme -> [TypeConstraint] -> SInferenceResult
SInferenceResult TypeScheme
scheme []

sInstantiate :: TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiate :: TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiate TypeScheme
scheme = ([Name] -> TypeScheme)
-> Flow SInferenceContext [Name]
-> Flow SInferenceContext TypeScheme
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map [Name] -> TypeScheme
doSubst (Int -> Flow SInferenceContext [Name]
sNewVars (Int -> Flow SInferenceContext [Name])
-> Int -> Flow SInferenceContext [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Name]
oldVars)
    where
      doSubst :: [Name] -> TypeScheme
doSubst [Name]
newVars = [Name] -> Type -> TypeScheme
TypeScheme [Name]
newVars (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Type
typeSchemeType TypeScheme
scheme
        where
          subst :: SSubst
subst = Map Name Type -> SSubst
SSubst (Map Name Type -> SSubst) -> Map Name Type -> SSubst
forall a b. (a -> b) -> a -> b
$ [(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]
oldVars (Name -> Type
TypeVariable (Name -> Type) -> [Name] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
newVars)
      oldVars :: [Name]
oldVars = [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
L.intersect ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ TypeScheme -> [Name]
typeSchemeVariables TypeScheme
scheme) (Type -> [Name]
sFreeTypeVariables (Type -> [Name]) -> Type -> [Name]
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Type
typeSchemeType TypeScheme
scheme)

sInstantiateAndNormalize :: TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiateAndNormalize :: TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiateAndNormalize TypeScheme
scheme = (TypeScheme -> TypeScheme)
-> Flow SInferenceContext TypeScheme
-> Flow SInferenceContext TypeScheme
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map TypeScheme -> TypeScheme
sNormalizeTypeVariables (TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiate TypeScheme
scheme)

sFreeTypeVariables :: Type -> [Name]
sFreeTypeVariables :: Type -> [Name]
sFreeTypeVariables Type
typ = case Type
typ of
  TypeFunction (FunctionType Type
dom Type
cod) -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Type -> [Name]
sFreeTypeVariables Type
dom [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Type -> [Name]
sFreeTypeVariables Type
cod
  TypeList Type
t -> Type -> [Name]
sFreeTypeVariables Type
t
  TypeLiteral LiteralType
_ -> []
  TypeMap (MapType Type
k Type
v) -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Type -> [Name]
sFreeTypeVariables Type
k [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Type -> [Name]
sFreeTypeVariables Type
v
  TypeProduct [Type]
types -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat ([[Name]] -> [Name]) -> [[Name]] -> [Name]
forall a b. (a -> b) -> a -> b
$ Type -> [Name]
sFreeTypeVariables (Type -> [Name]) -> [Type] -> [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
types
  TypeVariable Name
name -> [Name
name]

sNormalizeTypeVariables :: TypeScheme -> TypeScheme
sNormalizeTypeVariables :: TypeScheme -> TypeScheme
sNormalizeTypeVariables TypeScheme
scheme = [Name] -> Type -> TypeScheme
TypeScheme [Name]
newVars (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ SSubst -> Type -> Type
sSubstituteTypeVariables SSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Type
typeSchemeType TypeScheme
scheme
  where
    normalVariables :: [Name]
normalVariables = (\Integer
n -> String -> Name
Name (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n) (Integer -> Name) -> [Integer] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0..]
    oldVars :: [Name]
oldVars = TypeScheme -> [Name]
typeSchemeVariables TypeScheme
scheme
    newVars :: [Name]
newVars = Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
L.take ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Name]
oldVars) [Name]
normalVariables
    subst :: SSubst
subst =Map Name Type -> SSubst
SSubst (Map Name Type -> SSubst) -> Map Name Type -> SSubst
forall a b. (a -> b) -> a -> b
$ [(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]
oldVars (Name -> Type
TypeVariable (Name -> Type) -> [Name] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
newVars)

sNewVar :: Flow SInferenceContext Name
sNewVar :: Flow SInferenceContext Name
sNewVar = ([Name] -> Name)
-> Flow SInferenceContext [Name] -> Flow SInferenceContext Name
forall x y s. (x -> y) -> Flow s x -> Flow s y
Flows.map [Name] -> Name
forall a. HasCallStack => [a] -> a
L.head (Int -> Flow SInferenceContext [Name]
sNewVars Int
1)

sNewVars :: Int -> Flow SInferenceContext [Name]
sNewVars :: Int -> Flow SInferenceContext [Name]
sNewVars Int
n = (SInferenceContext -> Trace -> FlowState SInferenceContext [Name])
-> Flow SInferenceContext [Name]
forall s x. (s -> Trace -> FlowState s x) -> Flow s x
Flow SInferenceContext -> Trace -> FlowState SInferenceContext [Name]
helper
  where
    helper :: SInferenceContext -> Trace -> FlowState SInferenceContext [Name]
helper SInferenceContext
ctx Trace
t = Maybe [Name]
-> SInferenceContext -> Trace -> FlowState SInferenceContext [Name]
forall s x. Maybe x -> s -> Trace -> FlowState s x
FlowState Maybe [Name]
value SInferenceContext
ctx' Trace
t
      where
        value :: Maybe [Name]
value = [Name] -> Maybe [Name]
forall a. a -> Maybe a
Just ((\Int
n -> String -> Name
Name (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) (Int -> Name) -> [Int] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
L.take Int
n [(SInferenceContext -> Int
sInferenceContextVariableCount SInferenceContext
ctx)..]))
        ctx' :: SInferenceContext
ctx' = SInferenceContext
ctx {sInferenceContextVariableCount = n + sInferenceContextVariableCount ctx}

sVarScheme :: Name -> TypeScheme
sVarScheme :: Name -> TypeScheme
sVarScheme Name
v = [Name] -> Type -> TypeScheme
TypeScheme [Name
v] (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Name -> Type
TypeVariable Name
v

-- | Temporarily add a (term variable, type scheme) to the typing environment
sWithTypeBinding :: Name -> TypeScheme -> Flow SInferenceContext a -> Flow SInferenceContext a
sWithTypeBinding :: forall a.
Name
-> TypeScheme
-> Flow SInferenceContext a
-> Flow SInferenceContext a
sWithTypeBinding Name
name TypeScheme
scheme Flow SInferenceContext a
f = (SInferenceContext -> Trace -> FlowState SInferenceContext a)
-> Flow SInferenceContext a
forall s x. (s -> Trace -> FlowState s x) -> Flow s x
Flow SInferenceContext -> Trace -> FlowState SInferenceContext a
helper
  where
    helper :: SInferenceContext -> Trace -> FlowState SInferenceContext a
helper SInferenceContext
ctx0 Trace
t0 = Maybe a
-> SInferenceContext -> Trace -> FlowState SInferenceContext a
forall s x. Maybe x -> s -> Trace -> FlowState s x
FlowState Maybe a
e SInferenceContext
ctx3 Trace
t1
      where
        env :: Map Name TypeScheme
env = SInferenceContext -> Map Name TypeScheme
sInferenceContextTypingEnvironment SInferenceContext
ctx0
        ctx1 :: SInferenceContext
ctx1 = SInferenceContext
ctx0 {sInferenceContextTypingEnvironment = M.insert name scheme env}
        FlowState Maybe a
e SInferenceContext
ctx2 Trace
t1 = Flow SInferenceContext a
-> SInferenceContext -> Trace -> FlowState SInferenceContext a
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow Flow SInferenceContext a
f SInferenceContext
ctx1 Trace
t0
        ctx3 :: SInferenceContext
ctx3 = SInferenceContext
ctx2 {sInferenceContextTypingEnvironment = env}


--------------------------------------------------------------------------------
-- Testing

_app :: Term -> Term -> Term
_app Term
l Term
r = Application -> Term
TermApplication (Application -> Term) -> Application -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Application
Application Term
l Term
r
_int :: Int -> Term
_int = Literal -> Term
TermLiteral (Literal -> Term) -> (Int -> Literal) -> Int -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntegerValue -> Literal
LiteralInteger (IntegerValue -> Literal)
-> (Int -> IntegerValue) -> Int -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntegerValue
IntegerValueInt32
_lambda :: String -> Term -> Term
_lambda String
v Term
b = Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Lambda (String -> Name
Name String
v) Maybe Type
forall a. Maybe a
Nothing Term
b
_list :: [Term] -> Term
_list = [Term] -> Term
TermList
_map :: Map Term Term -> Term
_map = Map Term Term -> Term
TermMap
_pair :: Term -> Term -> Term
_pair Term
l Term
r = [Term] -> Term
TermProduct [Term
l, Term
r]
_str :: String -> Term
_str = Literal -> Term
TermLiteral (Literal -> Term) -> (String -> Literal) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Literal
LiteralString
_var :: String -> Term
_var = Name -> Term
TermVariable (Name -> Term) -> (String -> Name) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
Name

(@@) :: Term -> Term -> Term
Term
f @@ :: Term -> Term -> Term
@@ Term
x = Application -> Term
TermApplication (Application -> Term) -> Application -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Application
Application Term
f Term
x

infixr 0 >:
(>:) :: String -> Term -> (Name, Term)
String
n >: :: String -> Term -> (Name, Term)
>: Term
t = (String -> Name
Name String
n, Term
t)

int32 :: Int -> Term
int32 = Literal -> Term
TermLiteral (Literal -> Term) -> (Int -> Literal) -> Int -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntegerValue -> Literal
LiteralInteger (IntegerValue -> Literal)
-> (Int -> IntegerValue) -> Int -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntegerValue
IntegerValueInt32
lambda :: String -> Term -> Term
lambda String
v Term
b = Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Lambda -> Function
FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Lambda (String -> Name
Name String
v) Maybe Type
forall a. Maybe a
Nothing Term
b
list :: [Term] -> Term
list = [Term] -> Term
TermList
map :: Map Term Term -> Term
map = Map Term Term -> Term
TermMap
pair :: Term -> Term -> Term
pair Term
l Term
r = [Term] -> Term
TermProduct [Term
l, Term
r]
string :: String -> Term
string = Literal -> Term
TermLiteral (Literal -> Term) -> (String -> Literal) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Literal
LiteralString
var :: String -> Term
var = Name -> Term
TermVariable (Name -> Term) -> (String -> Name) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
Name
with :: Term -> t (Name, Term) -> Term
with Term
env t (Name, Term)
bindings = (Term -> (Name, Term) -> Term) -> Term -> t (Name, Term) -> Term
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Term
e (Name
k, Term
v) -> Let -> Term
TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Let [Name -> Term -> Maybe TypeScheme -> LetBinding
LetBinding Name
k Term
v Maybe TypeScheme
forall a. Maybe a
Nothing] Term
e) Term
env t (Name, Term)
bindings




infixr 0 ===
(===) :: Type -> Type -> TypeConstraint
Type
t1 === :: Type -> Type -> TypeConstraint
=== Type
t2 = Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
t1 Type
t2 (Maybe String -> TypeConstraint) -> Maybe String -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"some context"


_add :: Term
_add = Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Function
FunctionPrimitive (Name -> Function) -> Name -> Function
forall a b. (a -> b) -> a -> b
$ String -> Name
Name String
"add"
primPred :: Term
primPred = Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Function
FunctionPrimitive (Name -> Function) -> Name -> Function
forall a b. (a -> b) -> a -> b
$ String -> Name
Name String
"primPred"
primSucc :: Term
primSucc = Function -> Term
TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Function
FunctionPrimitive (Name -> Function) -> Name -> Function
forall a b. (a -> b) -> a -> b
$ String -> Name
Name String
"primSucc"

_unify :: Type -> Type -> Either SUnificationError SSubst
_unify Type
t1 Type
t2 = [TypeConstraint] -> Either SUnificationError SSubst
uUnify [Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
t1 Type
t2 (Maybe String -> TypeConstraint) -> Maybe String -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"ctx"]

sTestLexicon :: Map Name TypeScheme
sTestLexicon = [(Name, TypeScheme)] -> Map Name TypeScheme
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
  (String -> Name
Name String
"add", Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.function Type
Types.int32 Type
Types.int32),
  (String -> Name
Name String
"primPred", Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.function Type
Types.int32 Type
Types.int32),
  (String -> Name
Name String
"primSucc", Type -> TypeScheme
Types.mono (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Types.function Type
Types.int32 Type
Types.int32)]

sInitialContext :: SInferenceContext
sInitialContext = Map Name TypeScheme
-> Int -> Map Name TypeScheme -> SInferenceContext
SInferenceContext Map Name TypeScheme
sTestLexicon Int
0 Map Name TypeScheme
forall k a. Map k a
M.empty

_infer :: Term -> Maybe TypeScheme
_infer Term
term = FlowState SInferenceContext TypeScheme -> Maybe TypeScheme
forall s x. FlowState s x -> Maybe x
flowStateValue (FlowState SInferenceContext TypeScheme -> Maybe TypeScheme)
-> FlowState SInferenceContext TypeScheme -> Maybe TypeScheme
forall a b. (a -> b) -> a -> b
$ Flow SInferenceContext TypeScheme
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext TypeScheme
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow (Term -> Flow SInferenceContext TypeScheme
sInferType Term
term) SInferenceContext
sInitialContext Trace
Tier1.emptyTrace

_inferRaw :: Term -> Maybe SInferenceResult
_inferRaw Term
term = FlowState SInferenceContext SInferenceResult
-> Maybe SInferenceResult
forall s x. FlowState s x -> Maybe x
flowStateValue (FlowState SInferenceContext SInferenceResult
 -> Maybe SInferenceResult)
-> FlowState SInferenceContext SInferenceResult
-> Maybe SInferenceResult
forall a b. (a -> b) -> a -> b
$ Flow SInferenceContext SInferenceResult
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext SInferenceResult
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow (Term -> Flow SInferenceContext SInferenceResult
sInferTypeInternal Term
term) SInferenceContext
sInitialContext Trace
Tier1.emptyTrace

_instantiate :: TypeScheme -> Maybe TypeScheme
_instantiate TypeScheme
scheme = FlowState SInferenceContext TypeScheme -> Maybe TypeScheme
forall s x. FlowState s x -> Maybe x
flowStateValue (FlowState SInferenceContext TypeScheme -> Maybe TypeScheme)
-> FlowState SInferenceContext TypeScheme -> Maybe TypeScheme
forall a b. (a -> b) -> a -> b
$ Flow SInferenceContext TypeScheme
-> SInferenceContext
-> Trace
-> FlowState SInferenceContext TypeScheme
forall s x. Flow s x -> s -> Trace -> FlowState s x
unFlow (TypeScheme -> Flow SInferenceContext TypeScheme
sInstantiate TypeScheme
scheme) SInferenceContext
sInitialContext Trace
Tier1.emptyTrace

_con :: Type -> Type -> TypeConstraint
_con Type
t1 Type
t2 = Type -> Type -> Maybe String -> TypeConstraint
TypeConstraint Type
t1 Type
t2 (Maybe String -> TypeConstraint) -> Maybe String -> TypeConstraint
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"ctx"



{-

----------------------------------------
-- Unification

_unify (Types.var "a") (Types.var "b")
_unify (Types.var "a") (Types.list $ Types.var "b")

_unify (Types.var "a") Types.int32

_unify (Types.list Types.string) (Types.list $ Types.var "a")

_unify (Types.map (Types.var "a") Types.int32) (Types.map Types.string (Types.var "b"))

sUnifyAll [Types.var "t1" === Types.var "t0", Types.var "t1" === Types.int32]

-- Failure cases

_unify Types.string Types.int32

_unify (Types.var "a") (Types.list $ Types.var "a")

ctx = Just "ctx"
uUnify [(TypeConstraint (Types.var "t1") (Types.var "t0") ctx), (TypeConstraint (Types.var "t1") Types.int32 ctx)]


----------------------------------------
-- Inference

_infer $ _str "hello"

_infer _add

_infer $ _list [_add]

_infer $ _lambda "x" $ _int 42

_infer $ _list [_int 42]




_inferRaw (_list [_int 42])



:module
import Hydra.NewInference

-- System F cases
_inferRaw (lambda "x" $ var "x")                                                           -- (Types.poly ["t0"] $ Types.function (Types.var "t0") (Types.var "t0"))
_inferRaw (int32 32 `with` ["foo">: lambda "x" $ var "x"])                                 -- (Types.mono Types.int32)
_inferRaw ((var "f" @@ int32 0) `with` ["f">: lambda "x" $ var "x"])                       -- (Types.mono Types.int32)
_inferRaw (var "f" `with` ["f">: (lambda "x" $ var "x") @@ int32 0])                       -- (Types.mono Types.int32)
_inferRaw (lambda "x" $ list [var "x"])                                                    -- (Types.poly ["t0"] $ Types.function (Types.var "t0") (Types.list (Types.var "t0")))
_inferRaw (var "sng" `with` ["sng">: lambda "x" $ list [var "x"]])                         -- (Types.poly ["t0"] $ Types.function (Types.var "t0") (Types.list (Types.var "t0")))
_inferRaw ((var "+" @@ (primSucc @@ (primSucc @@ int32 0)) @@ (primSucc @@ int32 0)) `with` ["+">: lambda "x" $ lambda "y" (primSucc @@ (var "+" @@ (primPred @@ var "x") @@ var "y"))]) -- (Types.mono Types.int32)
_inferRaw (var "f" `with` ["f">: lambda "x" $ lambda "y" (var "f" @@ int32 0 @@ var "x")]) -- (Types.poly ["t0"] $ Types.function Types.int32 (Types.function Types.int32 (Types.var "t0")))



_inferRaw (var "f" `with` ["f">: lambda "x" $ lambda "y" (var "f" @@ int32 0 @@ var "x")]) -- (Types.poly ["t0"] $ Types.function Types.int32 (Types.function Types.int32 (Types.var "t0")))



:set +m

constraints = [
  _con (Types.function (Types.var "t5") (Types.var "t6")) (Types.var "t0"),
  _con (Types.var "t5") Types.int32,
  _con (Types.function (Types.var "t3") (Types.var "t4")) (Types.var "t6"),
  _con (Types.var "t3") (Types.var "t1"),
  _con (Types.var "t0") (Types.function (Types.var "t1") (Types.function (Types.var "t2") (Types.var "t4")))]

uUnify constraints




_inferRaw (_lambda "x" $ _list [_var "x", _int 42])

_inferRaw (_lambda "y" (_a (_lambda "x" $ _list [_var "x"]) (_var "y")))




_inferRaw (var "sng" `with` ["sng">: lambda "x" $ list [var "x"]])


----------------------------------------
-- Instantiation

sInstantiate (Types.poly ["t0", "t1"] $ Types.function (Types.var "t1") (Types.var "t1")) sInitialContext



-}