{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedStrings #-}

module IR.Constraint.Constrain.Expression where

import qualified Common.Identifiers as Ident
import Control.Monad (forM, zipWithM)
import Data.Foldable (foldrM)
import qualified Data.Map.Strict as Map
import IR.Constraint.Canonical ((-->))
import qualified IR.Constraint.Canonical as Can
import qualified IR.Constraint.Constrain.Annotation as Ann
import qualified IR.Constraint.Constrain.Pattern as Pattern
import IR.Constraint.Monad (TC, freshAnnVar, getExtern, throwError)
import IR.Constraint.Type as Type
import qualified IR.IR as I
import IR.SegmentLets (segmentDefs')


-- | HELPER ALIASES
type Def = (I.VarId, [I.Annotation], Variable, I.Expr Attachment)


type BinderDef = (I.Binder Attachment, I.Expr Attachment)


-- | DEFS
constrainBinderDefs :: [BinderDef] -> Constraint -> TC Constraint
constrainBinderDefs :: [BinderDef] -> Constraint -> TC Constraint
constrainBinderDefs [BinderDef]
binderDefs Constraint
finalConstraint = do
  [(VarId, [Annotation], Variable, Expr Attachment)]
defs <- [BinderDef]
-> (BinderDef
    -> StateT
         TCState
         (ExceptT Error (WriterT (Doc String) IO))
         (VarId, [Annotation], Variable, Expr Attachment))
-> StateT
     TCState
     (ExceptT Error (WriterT (Doc String) IO))
     [(VarId, [Annotation], Variable, Expr Attachment)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [BinderDef]
binderDefs \(Binder Attachment
binder, Expr Attachment
expr) -> do
    -- TODO: these binders will also contain annotations; we need to do
    -- something with them!

    -- resolved I think?
    VarId
name <- Binder Attachment -> TC VarId
forall t. Binder t -> TC VarId
Type.binderToVarId Binder Attachment
binder
    let ([Annotation]
anns, Variable
uvar) = Binder Attachment -> ([Annotation], Variable)
forall (c :: * -> *).
Carrier c =>
c Attachment -> ([Annotation], Variable)
uncarryAttachment Binder Attachment
binder
    (VarId, [Annotation], Variable, Expr Attachment)
-> StateT
     TCState
     (ExceptT Error (WriterT (Doc String) IO))
     (VarId, [Annotation], Variable, Expr Attachment)
forall (m :: * -> *) a. Monad m => a -> m a
return (VarId
name, [Annotation]
anns, Variable
uvar, Expr Attachment
expr)
  [(VarId, [Annotation], Variable, Expr Attachment)]
-> Constraint -> TC Constraint
constrainDefs [(VarId, [Annotation], Variable, Expr Attachment)]
defs Constraint
finalConstraint


constrainDefs :: [Def] -> Constraint -> TC Constraint
constrainDefs :: [(VarId, [Annotation], Variable, Expr Attachment)]
-> Constraint -> TC Constraint
constrainDefs [(VarId, [Annotation], Variable, Expr Attachment)]
defs Constraint
finalConstraint = do
  let segments :: [[(VarId, [Annotation], Variable, Expr Attachment)]]
segments = [(VarId, [Annotation], Variable, Expr Attachment)]
-> [[(VarId, [Annotation], Variable, Expr Attachment)]]
forall t a b. [Def' t a b] -> [[Def' t a b]]
segmentDefs' [(VarId, [Annotation], Variable, Expr Attachment)]
defs
  ([(VarId, [Annotation], Variable, Expr Attachment)]
 -> Constraint -> TC Constraint)
-> Constraint
-> [[(VarId, [Annotation], Variable, Expr Attachment)]]
-> TC Constraint
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM [(VarId, [Annotation], Variable, Expr Attachment)]
-> Constraint -> TC Constraint
constrainRecDefs Constraint
finalConstraint [[(VarId, [Annotation], Variable, Expr Attachment)]]
segments


constrainRecDefs :: [Def] -> Constraint -> TC Constraint
constrainRecDefs :: [(VarId, [Annotation], Variable, Expr Attachment)]
-> Constraint -> TC Constraint
constrainRecDefs [(VarId, [Annotation], Variable, Expr Attachment)]
defs Constraint
finalConstraint = do
  let flexVars :: [Variable]
flexVars = [Variable
uvar | (VarId
_, [Annotation]
_, Variable
uvar, Expr Attachment
_) <- [(VarId, [Annotation], Variable, Expr Attachment)]
defs]
      flexHeader :: Map Identifier Type
flexHeader = [(Identifier, Type)] -> Map Identifier Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(VarId -> Identifier
forall a b. (Identifiable a, Identifiable b) => a -> b
Ident.fromId VarId
name, Variable -> Type
TVarN Variable
uvar) | (VarId
name, [Annotation]
_, Variable
uvar, Expr Attachment
_) <- [(VarId, [Annotation], Variable, Expr Attachment)]
defs]
  [Constraint]
headerConstraints <- [(VarId, [Annotation], Variable, Expr Attachment)]
-> ((VarId, [Annotation], Variable, Expr Attachment)
    -> TC Constraint)
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) [Constraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(VarId, [Annotation], Variable, Expr Attachment)]
defs \(VarId
_, [Annotation]
anns, Variable
uvar, Expr Attachment
e) -> do
    [Annotation] -> Type -> (Type -> TC Constraint) -> TC Constraint
Ann.withAnnotations [Annotation]
anns (Variable -> Type
TVarN Variable
uvar) ((Type -> TC Constraint) -> TC Constraint)
-> (Type -> TC Constraint) -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
e
  if Bool
shouldGeneralize
    then
      Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$
        [Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet
          []
          [Variable]
flexVars
          Map Identifier Type
flexHeader
          ([Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet [] [] Map Identifier Type
flexHeader Constraint
CTrue ([Constraint] -> Constraint
CAnd [Constraint]
headerConstraints))
          Constraint
finalConstraint
    else
      Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$
        [Variable] -> Constraint -> Constraint
exists [Variable]
flexVars (Constraint -> Constraint) -> Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$
          [Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet
            []
            []
            Map Identifier Type
flexHeader
            ([Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet [] [] Map Identifier Type
flexHeader Constraint
CTrue ([Constraint] -> Constraint
CAnd [Constraint]
headerConstraints))
            Constraint
finalConstraint
 where
  shouldGeneralize :: Bool
shouldGeneralize = ((VarId, [Annotation], Variable, Expr Attachment) -> Bool)
-> [(VarId, [Annotation], Variable, Expr Attachment)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(VarId
_, [Annotation]
_, Variable
_, Expr Attachment
e) -> Expr Attachment -> Bool
forall t. Expr t -> Bool
I.isValue Expr Attachment
e) [(VarId, [Annotation], Variable, Expr Attachment)]
defs -- see concept: value restriction


-- | CONSTRAIN EXPRESSIONS
constrainExprAttached :: I.Expr Attachment -> Type -> TC Constraint
constrainExprAttached :: Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
expr Type
expected = do
  let ([Annotation]
anns, Variable
u) = Expr Attachment -> ([Annotation], Variable)
forall (c :: * -> *).
Carrier c =>
c Attachment -> ([Annotation], Variable)
uncarryAttachment Expr Attachment
expr
  Constraint
constraint <- [Annotation] -> Type -> (Type -> TC Constraint) -> TC Constraint
Ann.withAnnotations [Annotation]
anns Type
expected ((Type -> TC Constraint) -> TC Constraint)
-> (Type -> TC Constraint) -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Expr Attachment -> Type -> TC Constraint
constrainExpr Expr Attachment
expr
  Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ [Variable] -> Constraint -> Constraint
exists [Variable
u] (Constraint -> Constraint) -> Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ [Constraint] -> Constraint
CAnd [Type -> Type -> Constraint
CEqual (Variable -> Type
TVarN Variable
u) Type
expected, Constraint
constraint]


constrainExprAnnotated
  :: I.Expr Attachment -> [Can.Annotation] -> Type -> TC Constraint
constrainExprAnnotated :: Expr Attachment -> [Annotation] -> Type -> TC Constraint
constrainExprAnnotated Expr Attachment
expr [] Type
expected = Expr Attachment -> Type -> TC Constraint
constrainExpr Expr Attachment
expr Type
expected
constrainExprAnnotated Expr Attachment
expr (Can.AnnDCon DConId
_ [Annotation]
_ : [Annotation]
anns) Type
expected =
  Expr Attachment -> [Annotation] -> Type -> TC Constraint
constrainExprAnnotated Expr Attachment
expr [Annotation]
anns Type
expected
constrainExprAnnotated Expr Attachment
expr (Annotation
ann : [Annotation]
anns) Type
expected = do
  Identifier
dummyId <- VarId -> Identifier
forall a b. (Identifiable a, Identifiable b) => a -> b
Ident.fromId (VarId -> Identifier)
-> TC VarId
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) Identifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TC VarId
freshAnnVar
  (Ann.State RigidMap
rigidMap [Variable]
flexs, Type
tipe) <- Annotation -> TC (State, Type)
Ann.add Annotation
ann
  Constraint
innerConstraint <- Expr Attachment -> [Annotation] -> Type -> TC Constraint
constrainExprAnnotated Expr Attachment
expr [Annotation]
anns Type
tipe
  Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$
    CLet :: [Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet
      { _rigidVars :: [Variable]
_rigidVars = RigidMap -> [Variable]
forall k a. Map k a -> [a]
Map.elems RigidMap
rigidMap
      , _flexVars :: [Variable]
_flexVars = [Variable]
flexs
      , _header :: Map Identifier Type
_header = Identifier -> Type -> Map Identifier Type
forall k a. k -> a -> Map k a
Map.singleton Identifier
dummyId Type
tipe
      , _headerCon :: Constraint
_headerCon = Constraint
innerConstraint
      , _bodyCon :: Constraint
_bodyCon = Identifier -> Type -> Constraint
CLocal Identifier
dummyId Type
expected
      }


constrainExpr :: I.Expr Attachment -> Type -> TC Constraint
constrainExpr :: Expr Attachment -> Type -> TC Constraint
constrainExpr Expr Attachment
expr Type
expected = do
  case Expr Attachment
expr of
    I.Var VarId
name Attachment
_ -> Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Identifier -> Type -> Constraint
CLocal (VarId -> Identifier
forall a b. (Identifiable a, Identifiable b) => a -> b
Ident.fromId VarId
name) Type
expected
    I.Data DConId
name Attachment
_ -> Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Identifier -> Type -> Constraint
CLocal (DConId -> Identifier
forall a b. (Identifiable a, Identifiable b) => a -> b
Ident.fromId DConId
name) Type
expected
    I.Lit Literal
lit Attachment
_ -> Literal -> Type -> TC Constraint
constrainLit Literal
lit Type
expected
    I.App Expr Attachment
func Expr Attachment
arg Attachment
_ -> Expr Attachment -> Expr Attachment -> Type -> TC Constraint
constrainApp Expr Attachment
func Expr Attachment
arg Type
expected
    I.Lambda Binder Attachment
binder Expr Attachment
body Attachment
_ -> Binder Attachment -> Expr Attachment -> Type -> TC Constraint
constrainLambda Binder Attachment
binder Expr Attachment
body Type
expected
    I.Let [BinderDef]
binderDefs Expr Attachment
body Attachment
_ -> do
      [BinderDef] -> Constraint -> TC Constraint
constrainBinderDefs [BinderDef]
binderDefs (Constraint -> TC Constraint) -> TC Constraint -> TC Constraint
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
body Type
expected
    I.Match Expr Attachment
e [(Alt Attachment, Expr Attachment)]
branches Attachment
_ -> Expr Attachment
-> [(Alt Attachment, Expr Attachment)] -> Type -> TC Constraint
constrainMatch Expr Attachment
e [(Alt Attachment, Expr Attachment)]
branches Type
expected
    I.Prim Primitive
prim [Expr Attachment]
args Attachment
_ -> Primitive -> [Expr Attachment] -> Type -> TC Constraint
constrainPrim Primitive
prim [Expr Attachment]
args Type
expected
    I.Exception ExceptType
_ Attachment
_ ->
      let scheme :: Scheme
scheme = Type -> Scheme
Can.schemeOf (Type -> Scheme) -> Type -> Scheme
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a"
       in Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Scheme -> Type -> Constraint
CForeign Scheme
scheme Type
expected


constrainLit :: I.Literal -> Type -> TC Constraint
constrainLit :: Literal -> Type -> TC Constraint
constrainLit (I.LitIntegral Integer
_) Type
expected = Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEqual Type
Type.i32 Type
expected
constrainLit Literal
I.LitEvent Type
expected = Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Constraint
CEqual Type
Type.unit Type
expected


constrainApp :: I.Expr Attachment -> I.Expr Attachment -> Type -> TC Constraint
constrainApp :: Expr Attachment -> Expr Attachment -> Type -> TC Constraint
constrainApp Expr Attachment
func Expr Attachment
arg Type
resultType = do
  Variable
argVar <- TC Variable
mkFlexVar
  let argType :: Type
argType = Variable -> Type
TVarN Variable
argVar
      funcType :: Type
funcType = Type
argType Type -> Type -> Type
==> Type
resultType
  Constraint
funcCon <- Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
func Type
funcType
  Constraint
argCon <- Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
arg Type
argType
  Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ [Variable] -> Constraint -> Constraint
exists [Variable
argVar] ([Constraint] -> Constraint
CAnd [Constraint
funcCon, Constraint
argCon])


constrainLambda :: I.Binder Attachment -> I.Expr Attachment -> Type -> TC Constraint
constrainLambda :: Binder Attachment -> Expr Attachment -> Type -> TC Constraint
constrainLambda Binder Attachment
binder Expr Attachment
body Type
expected = do
  VarId
argName <- Binder Attachment -> TC VarId
forall t. Binder t -> TC VarId
binderToVarId Binder Attachment
binder
  Variable
resultVar <- TC Variable
mkFlexVar
  let ([Annotation]
anns, Variable
argVar) = Binder Attachment -> ([Annotation], Variable)
forall (c :: * -> *).
Carrier c =>
c Attachment -> ([Annotation], Variable)
uncarryAttachment Binder Attachment
binder
      resultType :: Type
resultType = Variable -> Type
TVarN Variable
resultVar

  [Variable] -> Constraint -> Constraint
exists [Variable
argVar, Variable
resultVar] (Constraint -> Constraint) -> TC Constraint -> TC Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Annotation] -> Type -> (Type -> TC Constraint) -> TC Constraint
Ann.withAnnotations [Annotation]
anns (Variable -> Type
TVarN Variable
argVar) \Type
argExpected -> do
    Constraint
bodyCon <- Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
body Type
resultType

    Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$
      [Constraint] -> Constraint
CAnd
        [ [Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet [] [] (Identifier -> Type -> Map Identifier Type
forall k a. k -> a -> Map k a
Map.singleton (VarId -> Identifier
forall a b. (Identifiable a, Identifiable b) => a -> b
Ident.fromId VarId
argName) Type
argExpected) Constraint
CTrue Constraint
bodyCon
        , Type -> Type -> Constraint
CEqual (Type
argExpected Type -> Type -> Type
==> Type
resultType) Type
expected
        ]


constrainMatch
  :: I.Expr Attachment -> [(I.Alt Attachment, I.Expr Attachment)] -> Type -> TC Constraint
constrainMatch :: Expr Attachment
-> [(Alt Attachment, Expr Attachment)] -> Type -> TC Constraint
constrainMatch Expr Attachment
expr [(Alt Attachment, Expr Attachment)]
branches Type
expected = do
  Variable
exprVar <- TC Variable
mkFlexVar
  let exprType :: Type
exprType = Variable -> Type
TVarN Variable
exprVar
  Constraint
exprCon <- Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
expr Type
exprType

  [Constraint]
branchCons <- [(Alt Attachment, Expr Attachment)]
-> ((Alt Attachment, Expr Attachment) -> TC Constraint)
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) [Constraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Alt Attachment, Expr Attachment)]
branches \(Alt Attachment
alt, Expr Attachment
branchExpr) -> Alt Attachment -> Expr Attachment -> Type -> Type -> TC Constraint
constrainBranch Alt Attachment
alt Expr Attachment
branchExpr Type
exprType Type
expected

  Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ [Variable] -> Constraint -> Constraint
exists [Variable
exprVar] (Constraint -> Constraint) -> Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ [Constraint] -> Constraint
CAnd [Constraint
exprCon, [Constraint] -> Constraint
CAnd [Constraint]
branchCons]


constrainBranch :: I.Alt Attachment -> I.Expr Attachment -> Type -> Type -> TC Constraint
constrainBranch :: Alt Attachment -> Expr Attachment -> Type -> Type -> TC Constraint
constrainBranch Alt Attachment
alt Expr Attachment
expr Type
pExpect Type
bExpect = do
  (Pattern.State Map Identifier Type
headers [Variable]
pvars [Constraint]
revCons) <- Alt Attachment -> Type -> State -> TC State
Pattern.add Alt Attachment
alt Type
pExpect State
Pattern.emptyState
  [Variable]
-> [Variable]
-> Map Identifier Type
-> Constraint
-> Constraint
-> Constraint
CLet [] [Variable]
pvars Map Identifier Type
headers ([Constraint] -> Constraint
CAnd ([Constraint] -> [Constraint]
forall a. [a] -> [a]
reverse [Constraint]
revCons))
    (Constraint -> Constraint) -> TC Constraint -> TC Constraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr Attachment -> Type -> TC Constraint
constrainExprAttached Expr Attachment
expr Type
bExpect


constrainPrim :: I.Primitive -> [I.Expr Attachment] -> Type -> TC Constraint
constrainPrim :: Primitive -> [Expr Attachment] -> Type -> TC Constraint
constrainPrim Primitive
prim [Expr Attachment]
args Type
expected = do
  [Variable]
argVars <- (Expr Attachment -> TC Variable)
-> [Expr Attachment]
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) [Variable]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TC Variable -> Expr Attachment -> TC Variable
forall a b. a -> b -> a
const TC Variable
mkFlexVar) [Expr Attachment]
args
  let argTypes :: [Type]
argTypes = (Variable -> Type) -> [Variable] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Type
TVarN [Variable]
argVars
  [Constraint]
argCons <- (Expr Attachment -> Type -> TC Constraint)
-> [Expr Attachment]
-> [Type]
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) [Constraint]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Expr Attachment -> Type -> TC Constraint
constrainExprAttached [Expr Attachment]
args [Type]
argTypes
  let fromArgs :: Type
fromArgs = ([Type], Type) -> Type
foldArrow ([Type]
argTypes, Type
expected)
  Scheme
fromPrim <- Int -> Primitive -> TC Scheme
lookupPrim ([Expr Attachment] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr Attachment]
args) Primitive
prim
  Constraint -> TC Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> TC Constraint) -> Constraint -> TC Constraint
forall a b. (a -> b) -> a -> b
$ [Variable] -> Constraint -> Constraint
exists [Variable]
argVars (Constraint -> Constraint) -> Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ [Constraint] -> Constraint
CAnd (Scheme -> Type -> Constraint
CForeign Scheme
fromPrim Type
fromArgs Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: [Constraint]
argCons)


lookupPrim :: Int -> I.Primitive -> TC Can.Scheme
lookupPrim :: Int -> Primitive -> TC Scheme
lookupPrim Int
len Primitive
prim = do
  Type -> Scheme
Can.schemeOf (Type -> Scheme)
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
-> TC Scheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
primType
 where
  primType :: TC Can.Type
  primType :: StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
primType = case Primitive
prim of
    Primitive
I.New -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a" Type -> Type -> Type
--> Type -> Type
Can.Ref (TVarId -> Type
Can.TVar TVarId
"a")
    Primitive
I.Dup -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a" Type -> Type -> Type
--> TVarId -> Type
Can.TVar TVarId
"a"
    Primitive
I.Drop -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a" Type -> Type -> Type
--> Type
Can.Unit
    Primitive
I.Deref -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Can.Ref (TVarId -> Type
Can.TVar TVarId
"a") Type -> Type -> Type
--> TVarId -> Type
Can.TVar TVarId
"a"
    Primitive
I.Assign -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Can.Ref (TVarId -> Type
Can.TVar TVarId
"a") Type -> Type -> Type
--> TVarId -> Type
Can.TVar TVarId
"a" Type -> Type -> Type
--> Type
Can.Unit
    Primitive
I.After ->
      Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ Type
Can.I32 Type -> Type -> Type
--> Type -> Type
Can.Ref (TVarId -> Type
Can.TVar TVarId
"a") Type -> Type -> Type
--> TVarId -> Type
Can.TVar TVarId
"a" Type -> Type -> Type
--> Type
Can.Unit
    Primitive
I.Now -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
Can.U64
    Primitive
I.Last -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
Can.Ref (TVarId -> Type
Can.TVar TVarId
"a") Type -> Type -> Type
--> Type
Can.U64
    I.CQuote String
_ -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a"
    Primitive
I.Loop -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a" Type -> Type -> Type
--> Type
Can.Unit
    Primitive
I.Break -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
Can.Unit
    I.FfiCall VarId
name -> do
      Maybe Type
maybeType <- VarId -> TC (Maybe Type)
getExtern VarId
name
      case Maybe Type
maybeType of
        Just Type
canType -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
canType
        Maybe Type
Nothing -> String
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a. String -> TC a
throwError (String
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> String
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ String
"Unknown ffi call: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarId -> String
forall a. Show a => a -> String
show VarId
name
    I.CCall CSym
_ -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
Can.TVar TVarId
"a"
    I.PrimOp PrimOp
primOp -> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ PrimOp -> Type
primOpType PrimOp
primOp
    Primitive
I.Par ->
      let tvs :: [TVarId]
tvs = Int -> [TVarId] -> [TVarId]
forall a. Int -> [a] -> [a]
take Int
len ([TVarId] -> [TVarId]) -> [TVarId] -> [TVarId]
forall a b. (a -> b) -> a -> b
$ (Int -> TVarId) -> [Int] -> [TVarId]
forall a b. (a -> b) -> [a] -> [b]
map ((TVarId
"a" TVarId -> TVarId -> TVarId
forall a. Semigroup a => a -> a -> a
<>) (TVarId -> TVarId) -> (Int -> TVarId) -> Int -> TVarId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TVarId
forall a b. (Show a, Identifiable b) => a -> b
Ident.showId) [(Int
1 :: Int) ..]
          args :: [Type]
args = (TVarId -> Type) -> [TVarId] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TVarId -> Type
Can.TVar [TVarId]
tvs
          ret :: Type
ret = [Type] -> Type
Can.tuple [Type]
args
       in Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ ([Type], Type) -> Type
Can.foldArrow ([Type]
args, Type
ret)
    Primitive
I.Wait ->
      let tvs :: [TVarId]
tvs = Int -> [TVarId] -> [TVarId]
forall a. Int -> [a] -> [a]
take Int
len ([TVarId] -> [TVarId]) -> [TVarId] -> [TVarId]
forall a b. (a -> b) -> a -> b
$ (Int -> TVarId) -> [Int] -> [TVarId]
forall a b. (a -> b) -> [a] -> [b]
map ((TVarId
"a" TVarId -> TVarId -> TVarId
forall a. Semigroup a => a -> a -> a
<>) (TVarId -> TVarId) -> (Int -> TVarId) -> Int -> TVarId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TVarId
forall a b. (Show a, Identifiable b) => a -> b
Ident.showId) [(Int
1 :: Int) ..]
          args :: [Type]
args = (TVarId -> Type) -> [TVarId] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TVarId -> Type
Can.TVar [TVarId]
tvs
          ret :: Type
ret = Type
Can.Unit
       in Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Type
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
forall a b. (a -> b) -> a -> b
$ ([Type], Type) -> Type
Can.foldArrow ([Type]
args, Type
ret)

  primOpType :: I.PrimOp -> Can.Type
  primOpType :: PrimOp -> Type
primOpType PrimOp
primOp = case PrimOp
primOp of
    PrimOp
I.PrimNeg -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimNot -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimBitNot -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimAdd -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimSub -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimMul -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimDiv -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimMod -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimBitAnd -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimBitOr -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimEq -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimNeq -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimGt -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimGe -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimLt -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32
    PrimOp
I.PrimLe -> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32 Type -> Type -> Type
--> Type
Can.I32