module IR.Constraint.Elaborate where

import qualified IR.Constraint.Canonical as Can
import IR.Constraint.Monad (TC)
import IR.Constraint.Type as Type
import qualified IR.IR as I


run :: I.Program Variable -> TC (I.Program Can.Type)
run :: Program Variable -> TC (Program Type)
run Program Variable
pVar = do
  let ([Binder Variable]
names, [Expr Variable]
exprs) = [(Binder Variable, Expr Variable)]
-> ([Binder Variable], [Expr Variable])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Binder Variable, Expr Variable)]
 -> ([Binder Variable], [Expr Variable]))
-> [(Binder Variable, Expr Variable)]
-> ([Binder Variable], [Expr Variable])
forall a b. (a -> b) -> a -> b
$ Program Variable -> [(Binder Variable, Expr Variable)]
forall t. Program t -> [(Binder t, Expr t)]
I.programDefs Program Variable
pVar
  [Expr Type]
exprs' <- (Expr Variable
 -> StateT
      TCState (ExceptT Error (WriterT (Doc String) IO)) (Expr Type))
-> [Expr Variable]
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) [Expr Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Variable
 -> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type)
-> Expr Variable
-> StateT
     TCState (ExceptT Error (WriterT (Doc String) IO)) (Expr Type)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Variable
-> StateT TCState (ExceptT Error (WriterT (Doc String) IO)) Type
Type.toCanType) [Expr Variable]
exprs
  let reattachBinders :: Binder t -> c t -> (Binder t, c t)
reattachBinders (I.BindVar VarId
v t
_) c t
expr = (VarId -> t -> Binder t
forall t. VarId -> t -> Binder t
I.BindVar VarId
v (t -> Binder t) -> t -> Binder t
forall a b. (a -> b) -> a -> b
$ c t -> t
forall (c :: * -> *) a. Carrier c => c a -> a
I.extract c t
expr, c t
expr)
      reattachBinders (I.BindAnon t
_) c t
expr = (t -> Binder t
forall t. t -> Binder t
I.BindAnon (t -> Binder t) -> t -> Binder t
forall a b. (a -> b) -> a -> b
$ c t -> t
forall (c :: * -> *) a. Carrier c => c a -> a
I.extract c t
expr, c t
expr)
  Program Type -> TC (Program Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Program Type -> TC (Program Type))
-> Program Type -> TC (Program Type)
forall a b. (a -> b) -> a -> b
$ Program Variable
pVar{programDefs :: [(Binder Type, Expr Type)]
I.programDefs = (Binder Variable -> Expr Type -> (Binder Type, Expr Type))
-> [Binder Variable] -> [Expr Type] -> [(Binder Type, Expr Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Binder Variable -> Expr Type -> (Binder Type, Expr Type)
forall (c :: * -> *) t t.
Carrier c =>
Binder t -> c t -> (Binder t, c t)
reattachBinders [Binder Variable]
names [Expr Type]
exprs', symTable :: Map VarId (SymInfo Type)
I.symTable = Map VarId (SymInfo Type)
forall t. Map VarId (SymInfo t)
I.uninitializedSymTable }