-- | Wrapper for @wisnesky's Algorithm W implementation which makes it into an alternative inferencer for Hydra

module Hydra.Inference.AlgorithmWBridge where

import Hydra.Inference.AlgorithmW

import qualified Hydra.Core as Core
import qualified Hydra.Graph as Graph
import qualified Hydra.Dsl.Literals as Literals
import qualified Hydra.Dsl.LiteralTypes as LiteralTypes
import qualified Hydra.Dsl.Terms as Terms
import qualified Hydra.Dsl.Types as Types
import Hydra.Sources.Libraries
import Hydra.Basics
import Hydra.Strip
import Hydra.Tier1
import Hydra.Coders
import Hydra.Inference.Substitution
import Hydra.Rewriting

import qualified Data.List as L
import qualified Data.Map as M
import qualified Control.Monad as CM

import Control.Monad.Except
import Control.Monad.State


-- A minimal Hydra graph container for use in these translation functions
data HydraContext = HydraContext (M.Map Core.Name Graph.Primitive)

----------------------------------------

-- | Find all of the bound variables in the type annotations within a System F term.
--   This function considers the types in "typed terms" (term:type), domain types on lambdas (\v:type.term),
--   and also type abstractions (/\v.term) to provide bound type variables.
boundTypeVariablesInSystemFTerm :: Core.Term -> [Core.Name]
boundTypeVariablesInSystemFTerm :: Term -> [Name]
boundTypeVariablesInSystemFTerm = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> (Term -> [Name]) -> Term -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraversalOrder
-> ([Name] -> Term -> [Name]) -> [Name] -> Term -> [Name]
forall x. TraversalOrder -> (x -> Term -> x) -> x -> Term -> x
foldOverTerm TraversalOrder
TraversalOrderPost [Name] -> Term -> [Name]
addTypeVars []
  where
    addTypeVars :: [Name] -> Term -> [Name]
addTypeVars [Name]
vars Term
term = Term -> [Name]
typeVarsIn Term
term [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
vars
    typeVarsIn :: Term -> [Name]
typeVarsIn Term
term = case Term
term of
      Core.TermFunction (Core.FunctionLambda (Core.Lambda Name
_ (Just Type
typ) Term
_)) -> Type -> [Name]
boundVariablesInTypeOrdered Type
typ
      Core.TermTypeAbstraction (Core.TypeAbstraction Name
v Term
_) -> [Name
v]
      Core.TermTyped (Core.TypedTerm Term
term Type
typ) -> Type -> [Name]
boundVariablesInTypeOrdered Type
typ
      Term
_ -> []

boundTypeVariablesInTermOrdered :: Core.Term -> [Core.Name]
boundTypeVariablesInTermOrdered :: Term -> [Name]
boundTypeVariablesInTermOrdered = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> (Term -> [Name]) -> Term -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraversalOrder
-> ([Name] -> Term -> [Name]) -> [Name] -> Term -> [Name]
forall x. TraversalOrder -> (x -> Term -> x) -> x -> Term -> x
foldOverTerm TraversalOrder
TraversalOrderPre [Name] -> Term -> [Name]
fld []
  where
    fld :: [Name] -> Term -> [Name]
fld [Name]
vars Term
term = case Term
term of
      Core.TermTyped (Core.TypedTerm Term
_ Type
typ) -> Bool -> Type -> [Name]
variablesInTypeOrdered Bool
False Type
typ [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
vars
      Term
_ -> [Name]
vars

-- | Finds all of the universal type variables in a type expression, in the order in which they appear.
-- Note: this function assumes that there are no shadowed type variables, as in (forall a. forall a. a)
-- TODO: redundant with variablesInTypeOrdered
boundVariablesInTypeOrdered :: Core.Type -> [Core.Name]
boundVariablesInTypeOrdered :: Type -> [Name]
boundVariablesInTypeOrdered Type
typ = case Type
typ of
  Core.TypeLambda (Core.LambdaType Name
var Type
body) -> Name
varName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:(Type -> [Name]
boundVariablesInTypeOrdered Type
body)
  Type
t -> [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (Type -> [Name]
boundVariablesInTypeOrdered (Type -> [Name]) -> [Type] -> [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [Type]
subtypes Type
t)

-- | Replace arbitrary bound type variables like v, a, v_12 with the systematic type variables t0, t1, t2, ...
--   following a canonical ordering in the term.
--   This function assumes that the bound variables do not also appear free in the type expressions of the term,
--   which in Hydra is made less likely by using the unusual naming convention tv_0, tv_1, etc. for temporary variables.
normalizeBoundTypeVariablesInSystemFTerm :: Core.Term -> Core.Term
normalizeBoundTypeVariablesInSystemFTerm :: Term -> Term
normalizeBoundTypeVariablesInSystemFTerm Term
term = Map Name Name -> Term -> Term
replaceTypeVariablesInSystemFTerm Map Name Name
subst Term
term
  where
    actualVars :: [Name]
actualVars = Term -> [Name]
boundTypeVariablesInSystemFTerm Term
term
    subst :: Map Name Name
subst = [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, Name)] -> Map Name Name)
-> [(Name, Name)] -> Map Name Name
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
L.zip [Name]
actualVars [Name]
normalVariables

replaceTypeVariables :: M.Map Core.Name Core.Name -> Core.Type -> Core.Type
replaceTypeVariables :: Map Name Name -> Type -> Type
replaceTypeVariables Map Name Name
subst = ((Type -> Type) -> Type -> Type) -> Type -> Type
rewriteType (((Type -> Type) -> Type -> Type) -> Type -> Type)
-> ((Type -> Type) -> Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ \Type -> Type
recurse Type
t -> case Type -> Type
recurse Type
t of
    Core.TypeVariable Name
v -> Name -> Type
Core.TypeVariable (Name -> Type) -> Name -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Name
replace Name
v
    Core.TypeLambda (Core.LambdaType Name
v Type
body) -> LambdaType -> Type
Core.TypeLambda (LambdaType -> Type) -> LambdaType -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> LambdaType
Core.LambdaType (Name -> Name
replace Name
v) Type
body
    Type
t1 -> Type
t1
  where
    replace :: Name -> Name
replace Name
v = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Name
v Name
v Map Name Name
subst

-- Note: this will replace all occurrences, regardless of boundness or shadowing
replaceTypeVariablesInSystemFTerm :: M.Map Core.Name Core.Name -> Core.Term -> Core.Term
replaceTypeVariablesInSystemFTerm :: Map Name Name -> Term -> Term
replaceTypeVariablesInSystemFTerm Map Name Name
subst = ((Term -> Term) -> Term -> Term) -> Term -> Term
rewriteTerm (((Term -> Term) -> Term -> Term) -> Term -> Term)
-> ((Term -> Term) -> Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ \Term -> Term
recurse Term
term ->
  case Term -> Term
recurse Term
term of
    Core.TermFunction (Core.FunctionLambda (Core.Lambda Name
v (Just Type
mt) Term
body)) ->
        Function -> Term
Core.TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Lambda -> Function
Core.FunctionLambda (Lambda -> Function) -> Lambda -> Function
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Type -> Term -> Lambda
Core.Lambda Name
v (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
mt2) Term
body
      where
        mt2 :: Type
mt2 = Map Name Name -> Type -> Type
replaceTypeVariables Map Name Name
subst Type
mt
    Core.TermTypeAbstraction (Core.TypeAbstraction Name
v Term
body) -> TypeAbstraction -> Term
Core.TermTypeAbstraction (TypeAbstraction -> Term) -> TypeAbstraction -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> TypeAbstraction
Core.TypeAbstraction Name
v2 Term
body
      where
        v2 :: Name
v2 = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Name
v Name
v Map Name Name
subst
    Core.TermTyped (Core.TypedTerm Term
term Type
typ) -> TypedTerm -> Term
Core.TermTyped (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
Core.TypedTerm Term
term (Map Name Name -> Type -> Type
replaceTypeVariables Map Name Name
subst Type
typ)
    Term
t -> Term
t

-- | Find the variables (both bound and free) in a type expression, following a preorder traversal of the expression.
variablesInTypeOrdered :: Bool -> Core.Type -> [Core.Name]
variablesInTypeOrdered :: Bool -> Type -> [Name]
variablesInTypeOrdered Bool
onlyBound = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
L.nub ([Name] -> [Name]) -> (Type -> [Name]) -> Type -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Name]
vars -- Note: we rely on the fact that 'nub' keeps the first occurrence
  where
    vars :: Type -> [Name]
vars Type
t = case Type
t of
      Core.TypeLambda (Core.LambdaType Name
v Type
body) -> Name
vName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:(Type -> [Name]
vars Type
body)
      Core.TypeVariable Name
v -> if Bool
onlyBound then [] else [Name
v]
      Type
_ -> [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
L.concat (Type -> [Name]
vars (Type -> [Name]) -> [Type] -> [[Name]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [Type]
subtypes Type
t)

----------------------------------------

-- Note: no support for @wisnesky's Prim constructors other than PrimStr, PrimNat, Cons, and Nil
hydraTermToStlc :: HydraContext -> Core.Term -> Either String Expr
hydraTermToStlc :: HydraContext -> Term -> Either String Expr
hydraTermToStlc HydraContext
context Term
term = case Term
term of
    Core.TermApplication (Core.Application Term
t1 Term
t2) -> Expr -> Expr -> Expr
App (Expr -> Expr -> Expr)
-> Either String Expr -> Either String (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Either String Expr
toStlc Term
t1 Either String (Expr -> Expr)
-> Either String Expr -> Either String Expr
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Either String Expr
toStlc Term
t2
    Core.TermFunction Function
f -> case Function
f of
      Core.FunctionLambda (Core.Lambda (Core.Name String
v) Maybe Type
_ Term
body) -> String -> Expr -> Expr
Abs (String -> Expr -> Expr)
-> Either String String -> Either String (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Either String String
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
v Either String (Expr -> Expr)
-> Either String Expr -> Either String Expr
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Either String Expr
toStlc Term
body
      Core.FunctionPrimitive Name
name -> do
        Primitive
prim <- case Name -> Map Name Primitive -> Maybe Primitive
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
name Map Name Primitive
prims of
          Maybe Primitive
Nothing -> String -> Either String Primitive
forall a b. a -> Either a b
Left (String -> Either String Primitive)
-> String -> Either String Primitive
forall a b. (a -> b) -> a -> b
$ String
"no such primitive: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
Core.unName Name
name
          Just Primitive
p -> Primitive -> Either String Primitive
forall a b. b -> Either a b
Right Primitive
p
        TypSch
ts <- TypeScheme -> Either String TypSch
hydraTypeSchemeToStlc (TypeScheme -> Either String TypSch)
-> TypeScheme -> Either String TypSch
forall a b. (a -> b) -> a -> b
$ Primitive -> TypeScheme
Graph.primitiveType Primitive
prim
        Expr -> Either String Expr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Either String Expr) -> Expr -> Either String Expr
forall a b. (a -> b) -> a -> b
$ Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ TypedPrimitive -> Prim
TypedPrim (TypedPrimitive -> Prim) -> TypedPrimitive -> Prim
forall a b. (a -> b) -> a -> b
$ Name -> TypSch -> TypedPrimitive
TypedPrimitive Name
name TypSch
ts
    Core.TermLet (Core.Let [LetBinding]
bindings Term
env) -> [(String, Expr)] -> Expr -> Expr
Letrec ([(String, Expr)] -> Expr -> Expr)
-> Either String [(String, Expr)] -> Either String (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LetBinding -> Either String (String, Expr))
-> [LetBinding] -> Either String [(String, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM LetBinding -> Either String (String, Expr)
bindingToStlc [LetBinding]
bindings Either String (Expr -> Expr)
-> Either String Expr -> Either String Expr
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Either String Expr
toStlc Term
env
      where
        bindingToStlc :: LetBinding -> Either String (String, Expr)
bindingToStlc (Core.LetBinding (Core.Name String
v) Term
term Maybe TypeScheme
_) = do
          Expr
s <- Term -> Either String Expr
toStlc Term
term
          (String, Expr) -> Either String (String, Expr)
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
v, Expr
s)
    Core.TermList [Term]
els -> do
      [Expr]
sels <- (Term -> Either String Expr) -> [Term] -> Either String [Expr]
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 -> Either String Expr
toStlc [Term]
els
      Expr -> Either String Expr
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Either String Expr) -> Expr -> Either String Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Expr
el Expr
acc -> Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Cons) Expr
el) Expr
acc) (Prim -> Expr
Const Prim
Nil) [Expr]
sels
    Core.TermLiteral Literal
lit -> Expr -> Either String Expr
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> Either String Expr) -> Expr -> Either String Expr
forall a b. (a -> b) -> a -> b
$ Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Literal -> Prim
Lit Literal
lit
    Core.TermProduct [Term]
els -> [Expr] -> Expr
Tuple ([Expr] -> Expr) -> Either String [Expr] -> Either String Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> Either String Expr) -> [Term] -> Either String [Expr]
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 -> Either String Expr
toStlc [Term]
els)
    Core.TermVariable (Core.Name String
v) -> Expr -> Either String Expr
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> Either String Expr) -> Expr -> Either String Expr
forall a b. (a -> b) -> a -> b
$ String -> Expr
Var String
v
    Term
_ -> String -> Either String Expr
forall a b. a -> Either a b
Left (String -> Either String Expr) -> String -> Either String Expr
forall a b. (a -> b) -> a -> b
$ String
"Unsupported term: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
term
  where
    HydraContext Map Name Primitive
prims = HydraContext
context
    toStlc :: Term -> Either String Expr
toStlc = HydraContext -> Term -> Either String Expr
hydraTermToStlc HydraContext
context
    pair :: Expr -> Expr -> Expr
pair Expr
a Expr
b = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Pair) Expr
a) Expr
b

hydraTypeSchemeToStlc :: Core.TypeScheme -> Either String TypSch
hydraTypeSchemeToStlc :: TypeScheme -> Either String TypSch
hydraTypeSchemeToStlc (Core.TypeScheme [Name]
vars Type
body) = do
    MTy
sbody <- Type -> Either String MTy
toStlc Type
body
    TypSch -> Either String TypSch
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either String TypSch) -> TypSch -> Either String TypSch
forall a b. (a -> b) -> a -> b
$ [String] -> MTy -> TypSch
Forall (Name -> String
Core.unName (Name -> String) -> [Name] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
vars) MTy
sbody
  where
    toStlc :: Type -> Either String MTy
toStlc Type
typ = case Type -> Type
stripType Type
typ of
      Core.TypeFunction (Core.FunctionType Type
dom Type
cod) -> MTy -> MTy -> MTy
TyFn (MTy -> MTy -> MTy)
-> Either String MTy -> Either String (MTy -> MTy)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Either String MTy
toStlc Type
dom Either String (MTy -> MTy)
-> Either String MTy -> Either String MTy
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Either String MTy
toStlc Type
cod
      Core.TypeList Type
et -> MTy -> MTy
TyList (MTy -> MTy) -> Either String MTy -> Either String MTy
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Either String MTy
toStlc Type
et
      Core.TypeLiteral LiteralType
lt -> MTy -> Either String MTy
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy -> Either String MTy) -> MTy -> Either String MTy
forall a b. (a -> b) -> a -> b
$ LiteralType -> MTy
TyLit LiteralType
lt
--      TypeMap MapType |
--      TypeOptional Type |
      Core.TypeProduct [Type]
types -> [MTy] -> MTy
TyTuple ([MTy] -> MTy) -> Either String [MTy] -> Either String MTy
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type -> Either String MTy) -> [Type] -> Either String [MTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM Type -> Either String MTy
toStlc [Type]
types)
--      TypeRecord RowType |
--      TypeSet Type |
--      TypeStream Type |
      Core.TypeSum [Type]
types -> if [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Type]
types Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
        then MTy -> Either String MTy
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MTy
TyVoid
        else if [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [Type]
types Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
          then String -> Either String MTy
forall a b. a -> Either a b
Left (String -> Either String MTy) -> String -> Either String MTy
forall a b. (a -> b) -> a -> b
$ String
"unary sums are not yet supported"
          else do
            [MTy]
stypes <- (Type -> Either String MTy) -> [Type] -> Either String [MTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM Type -> Either String MTy
toStlc [Type]
types
            let rev :: [MTy]
rev = [MTy] -> [MTy]
forall a. [a] -> [a]
L.reverse [MTy]
stypes
            MTy -> Either String MTy
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy -> Either String MTy) -> MTy -> Either String MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy) -> MTy -> [MTy] -> MTy
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\MTy
a MTy
e -> MTy -> MTy -> MTy
TySum MTy
e MTy
a) (MTy -> MTy -> MTy
TySum ([MTy]
rev [MTy] -> Int -> MTy
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) ([MTy]
rev [MTy] -> Int -> MTy
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)) ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ Int -> [MTy] -> [MTy]
forall a. Int -> [a] -> [a]
L.drop Int
2 [MTy]
rev
--      TypeUnion RowType |
      Core.TypeVariable Name
name -> MTy -> Either String MTy
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy -> Either String MTy) -> MTy -> Either String MTy
forall a b. (a -> b) -> a -> b
$ String -> MTy
TyVar (String -> MTy) -> String -> MTy
forall a b. (a -> b) -> a -> b
$ Name -> String
Core.unName Name
name
--      TypeWrap (Nominal Type)
      Type
_ -> String -> Either String MTy
forall a b. a -> Either a b
Left (String -> Either String MTy) -> String -> Either String MTy
forall a b. (a -> b) -> a -> b
$ String
"unsupported type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
typ


-- hydraTypeToTypeScheme :: Core.Type -> Either String TypSch
-- hydraTypeToTypeScheme typ = do
--     let (boundVars, baseType) = splitBoundVars [] typ
--     ty <- toStlc baseType
--     return $ Forall (Core.unName <$> boundVars) ty
--   where
--     splitBoundVars vars typ = case stripType typ of
--       Core.TypeLambda (Core.LambdaType v body) -> (v:vars', typ')
--         where
--           (vars', typ') = splitBoundVars vars body
--       _ -> (vars, typ)

systemFExprToHydra :: FExpr -> Either String Core.Term
systemFExprToHydra :: FExpr -> Either String Term
systemFExprToHydra FExpr
expr = case FExpr
expr of
  FConst Prim
prim -> case Prim
prim of
    Lit Literal
lit -> Term -> Either String Term
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Core.TermLiteral Literal
lit
    TypedPrim (TypedPrimitive Name
name TypSch
_) -> Term -> Either String Term
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ Function -> Term
Core.TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Function
Core.FunctionPrimitive Name
name
    Prim
Nil -> Term -> Either String Term
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
Core.TermList []
    Prim
_ -> String -> Either String Term
forall a b. a -> Either a b
Left (String -> Either String Term) -> String -> Either String Term
forall a b. (a -> b) -> a -> b
$ String
"Unsupported primitive: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Prim -> String
forall a. Show a => a -> String
show Prim
prim
    -- Note: other prims are unsupported
  FVar String
v -> Term -> Either String Term
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ Name -> Term
Core.TermVariable (Name -> Term) -> Name -> Term
forall a b. (a -> b) -> a -> b
$ String -> Name
Core.Name String
v
  FApp FExpr
e1 FExpr
e2 -> case FExpr
e1 of
    FApp (FTyApp (FConst Prim
Cons) [FTy]
_) FExpr
hd -> do
        [Term]
els <- (FExpr -> Either String Term) -> [FExpr] -> Either String [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM FExpr -> Either String Term
systemFExprToHydra (FExpr
hdFExpr -> [FExpr] -> [FExpr]
forall a. a -> [a] -> [a]
:(FExpr -> [FExpr]
gather FExpr
e2))
        Term -> Either String Term
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
Core.TermList [Term]
els -- TODO: include inferred type
      where
        gather :: FExpr -> [FExpr]
gather FExpr
e = case FExpr
e of
          FTyApp (FConst Prim
Nil) [FTy]
_ -> []
          FApp (FApp (FTyApp (FConst Prim
Cons) [FTy]
_) FExpr
hd) FExpr
tl -> FExpr
hdFExpr -> [FExpr] -> [FExpr]
forall a. a -> [a] -> [a]
:(FExpr -> [FExpr]
gather FExpr
tl)
    FTyApp (FConst Prim
Pair) [FTy]
_ -> do
--        els <- CM.mapM systemFExprToHydra (gather expr)
        [Term]
els <- [Term] -> Either String [Term]
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        Term -> Either String Term
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
Core.TermProduct [Term]
els -- TODO: include inferred type
      where
        gather :: FExpr -> [FExpr]
gather FExpr
e = case FExpr
e of
          FApp (FApp (FTyApp (FConst Prim
Pair) [FTy]
_) FExpr
el) FExpr
arg -> FExpr
elFExpr -> [FExpr] -> [FExpr]
forall a. a -> [a] -> [a]
:(FExpr -> [FExpr]
gather FExpr
arg)
          FExpr
_ -> [FExpr
e]
    FExpr
_ -> Application -> Term
Core.TermApplication (Application -> Term)
-> Either String Application -> Either String Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Term -> Application
Core.Application (Term -> Term -> Application)
-> Either String Term -> Either String (Term -> Application)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FExpr -> Either String Term
systemFExprToHydra FExpr
e1 Either String (Term -> Application)
-> Either String Term -> Either String Application
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FExpr -> Either String Term
systemFExprToHydra FExpr
e2)
  FAbs String
v FTy
dom FExpr
e -> do
    Term
term <- FExpr -> Either String Term
systemFExprToHydra FExpr
e
    Type
hdom <- TypeScheme -> Type
Core.typeSchemeType (TypeScheme -> Type)
-> Either String TypeScheme -> Either String Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTy -> Either String TypeScheme
systemFTypeToHydra FTy
dom
    Term -> Either String Term
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ Function -> Term
Core.TermFunction (Function -> Term) -> Function -> Term
forall a b. (a -> b) -> a -> b
$ Lambda -> Function
Core.FunctionLambda (Name -> Maybe Type -> Term -> Lambda
Core.Lambda (String -> Name
Core.Name String
v) (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
hdom) Term
term)
  FTyAbs [String]
params FExpr
body -> do
    Term
hbody <- FExpr -> Either String Term
systemFExprToHydra FExpr
body
    Term -> Either String Term
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ (Term -> String -> Term) -> Term -> [String] -> Term
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Term
t String
v -> TypeAbstraction -> Term
Core.TermTypeAbstraction (TypeAbstraction -> Term) -> TypeAbstraction -> Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> TypeAbstraction
Core.TypeAbstraction (String -> Name
Core.Name String
v) Term
t) Term
hbody ([String] -> Term) -> [String] -> Term
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
L.reverse [String]
params
  FTyApp FExpr
fun [FTy]
args -> do
    Term
hfun <- FExpr -> Either String Term
systemFExprToHydra FExpr
fun
    [Type]
hargs <- (FTy -> Either String Type) -> [FTy] -> Either String [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 (\FTy
t -> TypeScheme -> Type
Core.typeSchemeType (TypeScheme -> Type)
-> Either String TypeScheme -> Either String Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTy -> Either String TypeScheme
systemFTypeToHydra FTy
t) [FTy]
args
    Term -> Either String Term
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Either String Term) -> Term -> Either String Term
forall a b. (a -> b) -> a -> b
$ (Term -> Type -> Term) -> Term -> [Type] -> Term
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\Term
t Type
a -> TypedTerm -> Term
Core.TermTypeApplication (TypedTerm -> Term) -> TypedTerm -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypedTerm
Core.TypedTerm Term
t Type
a) Term
hfun ([Type] -> Term) -> [Type] -> Term
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type]
forall a. [a] -> [a]
L.reverse [Type]
hargs
  FLetrec [(String, FTy, FExpr)]
bindings FExpr
env -> Let -> Term
Core.TermLet (Let -> Term) -> Either String Let -> Either String Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      ([LetBinding] -> Term -> Let
Core.Let ([LetBinding] -> Term -> Let)
-> Either String [LetBinding] -> Either String (Term -> Let)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((String, FTy, FExpr) -> Either String LetBinding)
-> [(String, FTy, FExpr)] -> Either String [LetBinding]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM (String, FTy, FExpr) -> Either String LetBinding
bindingToHydra [(String, FTy, FExpr)]
bindings Either String (Term -> Let)
-> Either String Term -> Either String Let
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FExpr -> Either String Term
systemFExprToHydra FExpr
env)
    where
      bindingToHydra :: (String, FTy, FExpr) -> Either String LetBinding
bindingToHydra (String
v, FTy
ty, FExpr
term) = do
        Term
hterm <- FExpr -> Either String Term
systemFExprToHydra FExpr
term
        TypeScheme
hts <- FTy -> Either String TypeScheme
systemFTypeToHydra FTy
ty
        LetBinding -> Either String LetBinding
forall a. a -> Either String a
forall (m :: * -> *) a. Monad m => a -> m a
return (LetBinding -> Either String LetBinding)
-> LetBinding -> Either String LetBinding
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Maybe TypeScheme -> LetBinding
Core.LetBinding (String -> Name
Core.Name String
v) Term
hterm (Maybe TypeScheme -> LetBinding) -> Maybe TypeScheme -> LetBinding
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Maybe TypeScheme
forall a. a -> Maybe a
Just TypeScheme
hts
  FTuple [FExpr]
els -> [Term] -> Term
Core.TermProduct ([Term] -> Term) -> Either String [Term] -> Either String Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((FExpr -> Either String Term) -> [FExpr] -> Either String [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM FExpr -> Either String Term
systemFExprToHydra [FExpr]
els)
  FInj Int
i [FTy]
types FExpr
e -> Sum -> Term
Core.TermSum (Sum -> Term) -> Either String Sum -> Either String Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Int -> Term -> Sum
Core.Sum Int
i ([FTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [FTy]
types) (Term -> Sum) -> Either String Term -> Either String Sum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FExpr -> Either String Term
systemFExprToHydra FExpr
e)

systemFTypeToHydra :: FTy -> Either String Core.TypeScheme
systemFTypeToHydra :: FTy -> Either String TypeScheme
systemFTypeToHydra FTy
ty = case FTy
ty of
    FForall [String]
vars FTy
body -> [Name] -> Type -> TypeScheme
Core.TypeScheme (String -> Name
Core.Name (String -> Name) -> [String] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
vars) (Type -> TypeScheme)
-> Either String Type -> Either String TypeScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTy -> Either String Type
forall {f :: * -> *}. Monad f => FTy -> f Type
toHydra FTy
body
    FTy
_ -> [Name] -> Type -> TypeScheme
Core.TypeScheme [] (Type -> TypeScheme)
-> Either String Type -> Either String TypeScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTy -> Either String Type
forall {f :: * -> *}. Monad f => FTy -> f Type
toHydra FTy
ty
  where
    toHydra :: FTy -> f Type
toHydra FTy
ty = case FTy
ty of
      FTyVar String
v -> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
Core.TypeVariable (Name -> Type) -> Name -> Type
forall a b. (a -> b) -> a -> b
$ String -> Name
Core.Name String
v
      FTyLit LiteralType
lt -> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ LiteralType -> Type
Core.TypeLiteral LiteralType
lt
      FTyList FTy
lt -> Type -> Type
Core.TypeList (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTy -> f Type
toHydra FTy
lt
      FTyFn FTy
dom FTy
cod -> FunctionType -> Type
Core.TypeFunction (FunctionType -> Type) -> f FunctionType -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> Type -> FunctionType
Core.FunctionType (Type -> Type -> FunctionType)
-> f Type -> f (Type -> FunctionType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FTy -> f Type
toHydra FTy
dom f (Type -> FunctionType) -> f Type -> f FunctionType
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTy -> f Type
toHydra FTy
cod)
      FTyProd FTy
t1 FTy
t2 -> [Type] -> Type
Core.TypeProduct ([Type] -> Type) -> f [Type] -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FTy -> f Type) -> [FTy] -> f [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM FTy -> f Type
toHydra (FTy
t1FTy -> [FTy] -> [FTy]
forall a. a -> [a] -> [a]
:(FTy -> [FTy]
componentsTypesOf FTy
t2))
        where
          componentsTypesOf :: FTy -> [FTy]
componentsTypesOf FTy
t = case FTy
t of
            FTyProd FTy
t1 FTy
t2 -> FTy
t1FTy -> [FTy] -> [FTy]
forall a. a -> [a] -> [a]
:(FTy -> [FTy]
componentsTypesOf FTy
t2)
            FTy
_ -> [FTy
t]
      FTySum FTy
t1 FTy
t2 -> [Type] -> Type
Core.TypeSum ([Type] -> Type) -> f [Type] -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FTy -> f Type) -> [FTy] -> f [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM FTy -> f Type
toHydra (FTy
t1FTy -> [FTy] -> [FTy]
forall a. a -> [a] -> [a]
:(FTy -> [FTy]
componentsTypesOf FTy
t2))
        where
          componentsTypesOf :: FTy -> [FTy]
componentsTypesOf FTy
t = case FTy
t of
            FTySum FTy
t1 FTy
t2 -> FTy
t1FTy -> [FTy] -> [FTy]
forall a. a -> [a] -> [a]
:(FTy -> [FTy]
componentsTypesOf FTy
t2)
            FTy
_ -> [FTy
t]
      FTy
FTyUnit -> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
Core.TypeProduct []
      FTy
FTyVoid -> Type -> f Type
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> f Type) -> Type -> f Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
Core.TypeSum []
      FTyTuple [FTy]
tys -> [Type] -> Type
Core.TypeProduct ([Type] -> Type) -> f [Type] -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((FTy -> f Type) -> [FTy] -> f [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM FTy -> f Type
toHydra [FTy]
tys)
      FTyVariant [FTy]
tys -> [Type] -> Type
Core.TypeSum ([Type] -> Type) -> f [Type] -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((FTy -> f Type) -> [FTy] -> f [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
CM.mapM FTy -> f Type
toHydra [FTy]
tys)

inferWithAlgorithmW :: HydraContext -> Core.Term -> IO Core.Term
inferWithAlgorithmW :: HydraContext -> Term -> IO Term
inferWithAlgorithmW HydraContext
context Term
term = do
    Expr
stlc <- case HydraContext -> Term -> Either String Expr
hydraTermToStlc HydraContext
context (Term -> Term
wrap Term
term) of
       Left String
err -> String -> IO Expr
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
       Right Expr
t -> Expr -> IO Expr
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
t
    (FExpr
fexpr, FTy
_) <- Expr -> IO (FExpr, FTy)
inferExpr Expr
stlc
    case FExpr -> Either String Term
systemFExprToHydra FExpr
fexpr of
      Left String
err -> String -> IO Term
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
      Right Term
t -> Term -> Term
normalizeBoundTypeVariablesInSystemFTerm (Term -> Term) -> IO Term -> IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> IO Term
forall {f :: * -> *}. MonadFail f => Term -> f Term
unwrap Term
t
  where
    sFieldName :: Name
sFieldName = String -> Name
Core.Name String
"tempVar"
    wrap :: Term -> Term
wrap Term
term = Let -> Term
Core.TermLet (Let -> Term) -> Let -> Term
forall a b. (a -> b) -> a -> b
$ [LetBinding] -> Term -> Let
Core.Let ([Name -> Term -> Maybe TypeScheme -> LetBinding
Core.LetBinding Name
sFieldName Term
term Maybe TypeScheme
forall a. Maybe a
Nothing]) (Term -> Let) -> Term -> Let
forall a b. (a -> b) -> a -> b
$
      Literal -> Term
Core.TermLiteral (Literal -> Term) -> Literal -> Term
forall a b. (a -> b) -> a -> b
$ String -> Literal
Core.LiteralString String
"tempEnvironment"
    unwrap :: Term -> f Term
unwrap Term
term = case Term
term of
      Core.TermLet (Core.Let [LetBinding]
bindings Term
_) -> case [LetBinding]
bindings of
        [(Core.LetBinding Name
fname Term
t Maybe TypeScheme
_)] -> if Name
fname Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sFieldName
          then Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
t
          else String -> f Term
forall a. String -> f a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected let binding matching input"
        [LetBinding]
_ -> String -> f Term
forall a. String -> f a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected let bindings"

inferExpr :: Expr -> IO (FExpr, FTy)
inferExpr :: Expr -> IO (FExpr, FTy)
inferExpr Expr
t = case ((Either String (Subst, (MTy, FExpr)), ([String], Integer))
-> Either String (Subst, (MTy, FExpr))
forall a b. (a, b) -> a
fst ((Either String (Subst, (MTy, FExpr)), ([String], Integer))
 -> Either String (Subst, (MTy, FExpr)))
-> (Either String (Subst, (MTy, FExpr)), ([String], Integer))
-> Either String (Subst, (MTy, FExpr))
forall a b. (a -> b) -> a -> b
$ State ([String], Integer) (Either String (Subst, (MTy, FExpr)))
-> ([String], Integer)
-> (Either String (Subst, (MTy, FExpr)), ([String], Integer))
forall s a. State s a -> s -> (a, s)
runState (ExceptT
  String (StateT ([String], Integer) Identity) (Subst, (MTy, FExpr))
-> State ([String], Integer) (Either String (Subst, (MTy, FExpr)))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Int
-> ADTs
-> Ctx
-> Expr
-> ExceptT
     String (StateT ([String], Integer) Identity) (Subst, (MTy, FExpr))
w Int
0 [] [] Expr
t)) ([],Integer
0)) of
  Left String
e -> String -> IO (FExpr, FTy)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (FExpr, FTy)) -> String -> IO (FExpr, FTy)
forall a b. (a -> b) -> a -> b
$ String
"inference error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
  Right (Subst
_, (MTy
ty, FExpr
f)) -> case (ADTs -> [String] -> [(String, FTy)] -> FExpr -> Either String FTy
typeOf [] [] [] FExpr
f) of
    Left String
err -> String -> IO (FExpr, FTy)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (FExpr, FTy)) -> String -> IO (FExpr, FTy)
forall a b. (a -> b) -> a -> b
$ String
"type error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
    Right FTy
tt -> if FTy
tt FTy -> FTy -> Bool
forall a. Eq a => a -> a -> Bool
== MTy -> FTy
mTyToFTy MTy
ty
      then (FExpr, FTy) -> IO (FExpr, FTy)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FExpr
f, FTy
tt)
      else String -> IO (FExpr, FTy)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"no match"