diff options
Diffstat (limited to 'src/HSVIS')
-rw-r--r-- | src/HSVIS/AST.hs | 6 | ||||
-rw-r--r-- | src/HSVIS/Pretty.hs | 7 | ||||
-rw-r--r-- | src/HSVIS/Typecheck.hs | 32 |
3 files changed, 40 insertions, 5 deletions
diff --git a/src/HSVIS/AST.hs b/src/HSVIS/AST.hs index a789c82..f95a3cc 100644 --- a/src/HSVIS/AST.hs +++ b/src/HSVIS/AST.hs @@ -141,6 +141,12 @@ data Operator = OAdd | OSub | OMul | ODiv | OMod | OEqu | OPow instance Pretty Name where prettysPrec _ (Name n) = showString ("\"" ++ n ++ "\"") +instance (X Kind s ~ (), Pretty (E Kind s)) => Pretty (Kind s) where + prettysPrec _ (KType ()) = showString "Type" + prettysPrec d (KFun () a b) = + showParen (d > -1) $ prettysPrec 0 a . showString " -> " . prettysPrec 0 b + prettysPrec d (KExt () e) = prettysPrec d e + instance HasExt DataDef where type HasXField DataDef = 'True type HasECon DataDef = 'False diff --git a/src/HSVIS/Pretty.hs b/src/HSVIS/Pretty.hs index ffde90e..0f98da3 100644 --- a/src/HSVIS/Pretty.hs +++ b/src/HSVIS/Pretty.hs @@ -1,11 +1,16 @@ module HSVIS.Pretty where +import Data.Void + class Pretty a where prettysPrec :: Int -> a -> ShowS +instance Pretty Void where + prettysPrec _ = absurd + prettyPrec :: Pretty a => Int -> a -> String prettyPrec d x = prettysPrec d x "" pretty :: Pretty a => a -> String -pretty x = prettyPrec 0 x +pretty x = prettyPrec minBound x diff --git a/src/HSVIS/Typecheck.hs b/src/HSVIS/Typecheck.hs index 2b05793..de9d7db 100644 --- a/src/HSVIS/Typecheck.hs +++ b/src/HSVIS/Typecheck.hs @@ -7,10 +7,10 @@ module HSVIS.Typecheck where import Control.Monad -import Data.Bifunctor (first) +import Data.Bifunctor (first, second) import Data.Foldable (toList) -import Data.List (partition) import Data.Map.Strict (Map) +import Data.Monoid (First(..)) import qualified Data.Map.Strict as Map import Data.Bag @@ -78,8 +78,11 @@ typecheck fp source prog = in (toList (ds1 <> ds2), substProg sub progtc) data Constr - = CEq CType CType Range -- ^ These types must be equal because of the expression here - | CEqK CKind CKind Range -- ^ These kinds must be equal because of the type here + -- Equality constraints: "left" must be equal to "right" because of the thing + -- at the given range. "left" is the expected thing; "right" is the observed + -- thing. + = CEq CType CType Range + | CEqK CKind CKind Range deriving (Show) data Env = Env (Map Name CKind) (Map Name CType) @@ -268,6 +271,27 @@ tcFunDef (FunDef _ name msig eqs) = do tcFunEq :: CType -> PFunEq -> TCM CFunEq tcFunEq = _ +solveKindVars :: Bag (CKind, CKind, Range) -> TCM () +solveKindVars = + mapM_ $ \(a, b, rng) -> do + let (subst, First merr) = reduce a b + forM_ merr $ \(erra, errb) -> + raise rng $ + "Kind mismatch:\n\ + \- Expected: " ++ pretty a ++ "\n\ + \- Observed: " ++ pretty b ++ "\n\ + \because '" ++ pretty erra ++ "' and '" ++ pretty errb ++ "' don't match" + let collected :: [(Int, Bag CKind)] + collected = Map.assocs $ Map.fromListWith (<>) (fmap (second pure) (toList subst)) + _ + where + reduce :: CKind -> CKind -> (Bag (Int, CKind), First (CKind, CKind)) + reduce (KType ()) (KType ()) = mempty + reduce (KFun () a b) (KFun () c d) = reduce a c <> reduce b d + reduce (KExt () (KUniVar i)) k = (pure (i, k), mempty) + reduce k (KExt () (KUniVar i)) = (pure (i, k), mempty) + reduce k1 k2 = (mempty, pure (k1, k2)) + allEq :: (Eq a, Foldable t) => t a -> Bool allEq l = case toList l of [] -> True |