Fix type checker
This commit is contained in:
parent
cc5755c3a9
commit
0d6c5920a9
1 changed files with 13 additions and 4 deletions
|
|
@ -12,18 +12,18 @@ import Control.Applicative (Alternative, Applicative (liftA2),
|
||||||
import Control.Monad.Except (ExceptT, MonadError (throwError),
|
import Control.Monad.Except (ExceptT, MonadError (throwError),
|
||||||
liftEither, runExceptT, unless,
|
liftEither, runExceptT, unless,
|
||||||
zipWithM, zipWithM_)
|
zipWithM, zipWithM_)
|
||||||
import Control.Monad.State (MonadState (get, put), State,
|
import Control.Monad.State (MonadState, State, evalState, gets,
|
||||||
evalState, gets, modify)
|
modify)
|
||||||
import Data.Coerce (coerce)
|
import Data.Coerce (coerce)
|
||||||
import Data.Foldable (foldrM)
|
import Data.Foldable (foldrM)
|
||||||
import Data.Function (on)
|
import Data.Function (on)
|
||||||
import Data.List (intercalate, partition)
|
import Data.List (intercalate, partition)
|
||||||
import Data.List.Extra (allSame)
|
|
||||||
import Data.Map (Map)
|
import Data.Map (Map)
|
||||||
import qualified Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
import Data.Maybe (fromMaybe, isNothing)
|
import Data.Maybe (fromMaybe, isNothing)
|
||||||
import Data.Sequence (Seq (..))
|
import Data.Sequence (Seq (..))
|
||||||
import qualified Data.Sequence as S
|
import qualified Data.Sequence as S
|
||||||
|
import qualified Data.Set as Set
|
||||||
import Data.Tuple.Extra (second, secondM)
|
import Data.Tuple.Extra (second, secondM)
|
||||||
import Debug.Trace (trace)
|
import Debug.Trace (trace)
|
||||||
import Grammar.Abs
|
import Grammar.Abs
|
||||||
|
|
@ -72,11 +72,20 @@ initCxt defs = Cxt
|
||||||
| DBind' name vars rhs <- defs
|
| DBind' name vars rhs <- defs
|
||||||
]
|
]
|
||||||
, next_tevar = 0
|
, next_tevar = 0
|
||||||
, data_injs = Map.fromList [ (name, t)
|
, data_injs = Map.fromList [ (name, foldr TAll t $ unboundedTVars t)
|
||||||
| DData (Data _ injs) <- defs
|
| DData (Data _ injs) <- defs
|
||||||
, Inj name t <- injs
|
, Inj name t <- injs
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
|
where
|
||||||
|
unboundedTVars = uncurry (Set.\\) . go (mempty, mempty)
|
||||||
|
where
|
||||||
|
go (unbounded, bounded) = \case
|
||||||
|
TAll tvar t -> go (unbounded, Set.insert tvar bounded) t
|
||||||
|
TVar tvar -> (Set.insert tvar unbounded, bounded)
|
||||||
|
TFun t1 t2 -> foldl go (unbounded, bounded) [t1, t2]
|
||||||
|
TData _ typs -> foldl go (unbounded, bounded) typs
|
||||||
|
_ -> (unbounded, bounded)
|
||||||
|
|
||||||
typecheck :: Program -> Err (T.Program' Type)
|
typecheck :: Program -> Err (T.Program' Type)
|
||||||
typecheck (Program defs) = do
|
typecheck (Program defs) = do
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue