diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c7d20e18..52e16c6e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -31,10 +31,6 @@ jobs: ghc: "9.2.5" os: ubuntu-latest - - cabal: "3.2" - ghc: "8.10.7" - os: ubuntu-latest - # latest GHC, non-default OS - cabal: "3.8" ghc: "9.6" diff --git a/examples/non-examples/kind-occurs-check.golden b/examples/non-examples/kind-occurs-check.golden new file mode 100644 index 00000000..0c822001 --- /dev/null +++ b/examples/non-examples/kind-occurs-check.golden @@ -0,0 +1,2 @@ +Infinite kind detected: + (KindVar 55708) = (META(KindVar 55708) → META(KindVar 55701)) diff --git a/examples/non-examples/kind-occurs-check.kl b/examples/non-examples/kind-occurs-check.kl new file mode 100644 index 00000000..dd380347 --- /dev/null +++ b/examples/non-examples/kind-occurs-check.kl @@ -0,0 +1,17 @@ +#lang "prelude.kl" + +(datatype (Phantom A) + (mk-phantom)) + +-- causes the kind equality ?1 ~ ?2 to be unified twice, which previously +-- caused ?2 to point to itself, thus causing zonking ?2 to run forever. +-- should be accepted. +(example + (with-unknown-type [A] + (the (Phantom A) + (mk-phantom)))) + +-- causes the kind equality ?1 ~ (-> ?1 *). +-- should be accepted by the occurs-check. +(datatype (InfiniteKind A) + (mk-infinite-kind (Phantom (A A)))) diff --git a/examples/non-examples/type-occurs-check.golden b/examples/non-examples/type-occurs-check.golden new file mode 100644 index 00000000..b25ba10e --- /dev/null +++ b/examples/non-examples/type-occurs-check.golden @@ -0,0 +1 @@ +Infinite type detected: (MetaPtr 57868) = (List META(MetaPtr 57868)) diff --git a/examples/non-examples/type-occurs-check.kl b/examples/non-examples/type-occurs-check.kl new file mode 100644 index 00000000..00815c5b --- /dev/null +++ b/examples/non-examples/type-occurs-check.kl @@ -0,0 +1,13 @@ +#lang "prelude.kl" + +-- accepted, thanks to let-generalization +(example + (let [xs (nil)] + (:: xs -- (the (List A) xs) + xs -- (the (List (List A)) xs) + ))) + +-- causes the type equality ?1 ~ List ?1, which must be rejected by the +-- occurs-check. +(defun infinite-type (xs) + (:: xs xs)) diff --git a/klister.cabal b/klister.cabal index 13ce70fa..1527fbb6 100644 --- a/klister.cabal +++ b/klister.cabal @@ -81,6 +81,7 @@ library PartialType Phase Pretty + Pretty.Renumber Scope ScopeSet ShortShow diff --git a/src/Expander.hs b/src/Expander.hs index ff581681..93e7d11a 100644 --- a/src/Expander.hs +++ b/src/Expander.hs @@ -544,15 +544,17 @@ initializeKernel outputChannel = do | (name, fun) <- [("<", (<)), ("<=", (<=)), (">", (>)), (">=", (>=)), ("=", (==)), ("/=", (/=))] ] ++ [ ("pure-IO" - , Scheme [KStar, KStar] $ tFun [tSchemaVar 0 []] (tIO (tSchemaVar 0 [])) + , let a = tSchemaVar firstSchemeVar [] + in Scheme [KStar, KStar] $ tFun [a] (tIO a) , ValueClosure $ HO $ \v -> ValueIOAction (pure v) ) , ("bind-IO" - , Scheme [KStar, KStar] $ - tFun [ tIO (tSchemaVar 0 []) - , tFun [tSchemaVar 0 []] (tIO (tSchemaVar 1 [])) - ] - (tIO (tSchemaVar 1 [])) + , let a:b:_ = [tSchemaVar i [] | i <- [firstSchemeVar..]] + in Scheme [KStar, KStar] $ + tFun [ tIO a + , tFun [a] (tIO b) + ] + (tIO b) , ValueClosure $ HO $ \(ValueIOAction mx) -> do ValueClosure $ HO $ \(ValueClosure f) -> do ValueIOAction $ do @@ -596,22 +598,25 @@ initializeKernel outputChannel = do , ("Unit", [], [("unit", [])]) , ("Bool", [], [("true", []), ("false", [])]) , ("Problem", [], [("module", []), ("declaration", []), ("type", []), ("expression", [tType]), ("pattern", []), ("type-pattern", [])]) - , ("Maybe", [KStar], [("nothing", []), ("just", [tSchemaVar 0 []])]) - , ("List" - , [KStar] - , [ ("nil", []) - , ("::", [tSchemaVar 0 [], Prims.primitiveDatatype "List" [tSchemaVar 0 []]]) - ] - ) + , let a = tSchemaVar firstSchemeVar [] + in ("Maybe", [KStar], [("nothing", []), ("just", [a])]) + , let a = tSchemaVar firstSchemeVar [] + in ("List" + , [KStar] + , [ ("nil", []) + , ("::", [a, Prims.primitiveDatatype "List" [a]]) + ] + ) , ("Syntax-Contents" , [KStar] - , [ ("list-contents", [Prims.primitiveDatatype "List" [tSchemaVar 0 []]]) - , ("integer-contents", [tInteger]) - , ("string-contents", [tString]) - , ("identifier-contents", [tString]) - -- if you add a constructor here, remember to also add a - -- corresponding pattern in close-syntax! - ] + , let a = tSchemaVar firstSchemeVar [] + in [ ("list-contents", [Prims.primitiveDatatype "List" [a]]) + , ("integer-contents", [tInteger]) + , ("string-contents", [tString]) + , ("identifier-contents", [tString]) + -- if you add a constructor here, remember to also add a + -- corresponding pattern in close-syntax! + ] ) ] @@ -1211,8 +1216,9 @@ expandOneForm prob stx case prob of ExprDest t dest -> do argTys <- traverse makeTypeMeta argKinds + let tyStore = S.fromList $ zip [firstSchemeVar..] argTys unify dest t $ tDatatype dt argTys - args' <- for args \a -> inst dest (Scheme argKinds a) argTys + args' <- for args \a -> inst dest (Scheme argKinds a) tyStore Stx _ _ (foundName, foundArgs) <- mustBeCons stx _ <- mustBeIdent foundName argDests <- @@ -1225,8 +1231,9 @@ expandOneForm prob stx PatternDest patTy dest -> do Stx _ loc (_cname, subPats) <- mustBeCons stx tyArgs <- traverse makeTypeMeta argKinds + let tyStore = S.fromList $ zip [firstSchemeVar..] tyArgs argTypes <- for args \ a -> - inst loc (Scheme argKinds a) tyArgs + inst loc (Scheme argKinds a) tyStore unify loc (tDatatype dt tyArgs) patTy if length subPats /= length argTypes then throwError $ WrongArgCount stx ctor (length argTypes) (length subPats) diff --git a/src/Expander/Error.hs b/src/Expander/Error.hs index c4134733..30b13c8f 100644 --- a/src/Expander/Error.hs +++ b/src/Expander/Error.hs @@ -6,6 +6,7 @@ module Expander.Error ( ExpansionErr(..) , SyntacticCategory(..) , TypeCheckError(..) + , KindCheckError(..) , Tenon, tenon, Mortise, mortise , notRightLength ) where @@ -63,10 +64,10 @@ data ExpansionErr (Mortise SyntacticCategory) | NotValidType Syntax | TypeCheckError TypeCheckError + | KindCheckError KindCheckError | WrongArgCount Syntax Constructor Int Int | NotAConstructor Syntax | WrongTypeArity Syntax TypeConstructor Natural Int - | KindMismatch (Maybe SrcLoc) Kind Kind | CircularImports ModuleName [ModuleName] deriving (Show) @@ -97,6 +98,10 @@ data TypeCheckError | OccursCheckFailed MetaPtr Ty deriving (Show) +data KindCheckError + = KindMismatch (Maybe SrcLoc) Kind Kind + | KindOccursCheckFailed KindVar Kind + deriving (Show) data SyntacticCategory = ModuleCat @@ -216,6 +221,7 @@ instance Pretty VarInfo ExpansionErr where pp env (NotValidType stx) = hang 2 $ group $ vsep [text "Not a type:", pp env stx] pp env (TypeCheckError err) = pp env err + pp env (KindCheckError err) = pp env err pp env (WrongArgCount stx ctor wanted got) = hang 2 $ vsep [ text "Wrong number of arguments for constructor" <+> pp env ctor @@ -231,11 +237,6 @@ instance Pretty VarInfo ExpansionErr where , text "Got" <+> viaShow got , text "In" <+> align (pp env stx) ] - pp env (KindMismatch loc k1 k2) = - hang 2 $ group $ vsep [ text "Kind mismatch at" <+> - maybe (text "unknown location") (pp env) loc <> text "." - , group $ vsep [pp env k1, text "≠", pp env k2] - ] pp env (CircularImports current stack) = hang 2 $ vsep [ group $ vsep [ text "Circular imports while importing", pp env current] , group $ hang 2 $ vsep (text "Context:" : map (pp env) stack)] @@ -265,10 +266,21 @@ instance Pretty VarInfo TypeCheckError where ] pp env (OccursCheckFailed ptr ty) = - hang 2 $ group $ vsep [ text "Occurs check failed:" - , group (vsep [viaShow ptr, "≠", pp env ty]) + hang 2 $ group $ vsep [ text "Infinite type detected:" + , group (vsep [viaShow ptr, "=", pp env ty]) ] +instance Pretty VarInfo KindCheckError where + pp env (KindMismatch loc k1 k2) = + hang 2 $ group $ vsep [ text "Kind mismatch at" <+> + maybe (text "unknown location") (pp env) loc <> text "." + , group $ vsep [pp env k1, text "≠", pp env k2] + ] + + pp env (KindOccursCheckFailed v k) = + hang 2 $ group $ vsep [ text "Infinite kind detected:" + , group (vsep [viaShow v, "=", pp env k]) + ] instance Pretty VarInfo SyntacticCategory where pp _env ExpressionCat = text "an expression" diff --git a/src/Expander/Monad.hs b/src/Expander/Monad.hs index 7a8c34c4..3e375810 100644 --- a/src/Expander/Monad.hs +++ b/src/Expander/Monad.hs @@ -240,7 +240,7 @@ data EValue | EPrimPatternMacro (Either (Ty, PatternPtr) TypePatternPtr -> Syntax -> Expand ()) | EPrimUniversalMacro (MacroDest -> Syntax -> Expand ()) | EVarMacro !Var -- ^ For bound variables (the Unique is the binding site of the var) - | ETypeVar !Kind !Natural + | ETypeVar !Kind !SchemeVar -- ^ For bound type variables (user-written Skolem variables or in datatype definitions) | EUserMacro !MacroVar -- ^ For user-written macros | EIncompleteMacro !MacroVar !Ident !SplitCorePtr -- ^ Macros that are themselves not yet ready to go diff --git a/src/Expander/Primitives.hs b/src/Expander/Primitives.hs index b8c5b8f8..08657ae9 100644 --- a/src/Expander/Primitives.hs +++ b/src/Expander/Primitives.hs @@ -68,7 +68,6 @@ import Control.Monad.Except import Data.Text (Text) import qualified Data.Text as T import Data.Traversable -import Numeric.Natural import Binding import Core @@ -130,7 +129,7 @@ datatype dest outScopesDest stx = do Stx scs loc (_ :: Syntax, more) <- mustBeCons stx Stx _ _ (nameAndArgs, ctorSpecs) <- mustBeCons (Syntax (Stx scs loc (List more))) Stx _ _ (name, args) <- mustBeCons nameAndArgs - typeArgs <- for (zip [0..] args) $ \(i, a) -> + typeArgs <- for (zip [firstSchemeVar..] args) $ \(i, a) -> prepareTypeVar i a sc <- freshScope $ T.pack $ "For datatype at " ++ shortShow (stxLoc stx) let typeScopes = map (view _1) typeArgs ++ [sc] @@ -712,7 +711,7 @@ scheduleTypePattern exprTy (Stx _ _ (patStx, rhsStx@(Syntax (Stx _ loc _)))) = d forkExpanderTask $ AwaitingTypePattern dest exprTy rhsDest rhsStx return (dest, rhsDest) -prepareTypeVar :: Natural -> Syntax -> Expand (Scope, Ident, Kind) +prepareTypeVar :: SchemeVar -> Syntax -> Expand (Scope, Ident, Kind) prepareTypeVar i varStx = do (sc, α, b) <- varPrepHelper varStx k <- KMetaVar <$> liftIO newKindVar diff --git a/src/Expander/Syntax.hs b/src/Expander/Syntax.hs index 2a3202b5..5a7ccb80 100644 --- a/src/Expander/Syntax.hs +++ b/src/Expander/Syntax.hs @@ -3,6 +3,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} -- | Utilities for analyzing the form of syntax in the expander monad module Expander.Syntax where diff --git a/src/Expander/TC.hs b/src/Expander/TC.hs index f6fdf1b7..2af0fd0d 100644 --- a/src/Expander/TC.hs +++ b/src/Expander/TC.hs @@ -14,6 +14,7 @@ import Control.Monad import Control.Monad.Except import Control.Monad.State import Data.Foldable +import Data.Traversable (for) import Numeric.Natural import Expander.Monad @@ -107,12 +108,14 @@ freshMeta kind = do return ptr -inst :: UnificationErrorBlame blame => blame -> Scheme Ty -> [Ty] -> Expand Ty +inst :: UnificationErrorBlame blame => blame -> Scheme Ty -> Store SchemeVar Ty -> Expand Ty inst blame (Scheme argKinds ty) ts | length ts /= length argKinds = throwError $ InternalError "Mismatch in number of type vars" | otherwise = do - traverse_ (uncurry $ checkKind blame) (zip argKinds ts) + let tys :: [Ty] + tys = fmap snd $ St.toAscList ts + traverse_ (uncurry $ checkKind blame) (zip argKinds tys) instTy ty where instTy :: Ty -> Expand Ty @@ -131,13 +134,17 @@ inst blame (Scheme argKinds ty) ts pure $ TyF ctor' (tArgsPrefix ++ tArgsSuffix) instCtor :: TypeConstructor -> TyF Ty - instCtor (TSchemaVar i) = unTy $ ts !! fromIntegral i + instCtor (TSchemaVar v) = unTy $ ts St.! v instCtor ctor = TyF ctor [] specialize :: UnificationErrorBlame blame => blame -> Scheme Ty -> Expand Ty specialize blame sch@(Scheme argKinds _) = do - freshVars <- traverse makeTypeMeta argKinds + pairs <- for (zip [firstSchemeVar..] argKinds) $ \(v, k) -> do + meta <- makeTypeMeta k + pure (v, meta) + let freshVars :: Store SchemeVar Ty + freshVars = St.fromList pairs inst blame sch freshVars varType :: Var -> Expand (Maybe (Scheme Ty)) @@ -162,35 +169,35 @@ notFreeInCtx var = do generalizeType :: Ty -> Expand (Scheme Ty) generalizeType ty = do canGeneralize <- filterM notFreeInCtx =<< metas ty - (body, (_, _, argKinds)) <- flip runStateT (0, mempty, []) $ do + (body, (_, _, argKinds)) <- flip runStateT (firstSchemeVar, mempty, []) $ do genTyVars canGeneralize ty pure $ Scheme argKinds body where genTyVars :: [MetaPtr] -> Ty -> - StateT (Natural, Store MetaPtr Natural, [Kind]) Expand Ty + StateT (SchemeVar, Store MetaPtr SchemeVar, [Kind]) Expand Ty genTyVars vars t = do (Ty t') <- lift $ normType t Ty <$> genVarsTyF vars t' genVarsTyF :: [MetaPtr] -> TyF Ty -> - StateT (Natural, Store MetaPtr Natural, [Kind]) Expand (TyF Ty) + StateT (SchemeVar, Store MetaPtr SchemeVar, [Kind]) Expand (TyF Ty) genVarsTyF vars (TyF ctor args) = TyF <$> genVarsCtor vars ctor <*> traverse (genTyVars vars) args genVarsCtor :: [MetaPtr] -> TypeConstructor -> - StateT (Natural, Store MetaPtr Natural, [Kind]) Expand TypeConstructor + StateT (SchemeVar, Store MetaPtr SchemeVar, [Kind]) Expand TypeConstructor genVarsCtor vars (TMetaVar v) | v `elem` vars = do (i, indices, argKinds) <- get case St.lookup v indices of Nothing -> do k <- lift $ typeVarKind v - put (i + 1, St.insert v i indices, argKinds ++ [k]) + put (succ i, St.insert v i indices, argKinds ++ [k]) pure $ TSchemaVar i Just j -> pure $ TSchemaVar j | otherwise = pure $ TMetaVar v @@ -306,15 +313,57 @@ typeVarKind ptr = Just v -> pure $ view varKind v -setKindVar :: KindVar -> Kind -> Expand () -setKindVar v k@(KMetaVar v') = - (view (expanderKindStore . at v') <$> getState) >>= - \case - Nothing -> modifyState $ set (expanderKindStore . at v) (Just k) - -- Path compression step - Just k' -> setKindVar v k' -setKindVar v k = modifyState $ set (expanderKindStore . at v) (Just k) +kindMetas :: Kind -> Expand [KindVar] +kindMetas k = do + k' <- zonkKind k + case k' of + KMetaVar v' -> + (view (expanderKindStore . at v') <$> getState) >>= + \case + Nothing -> pure [v'] + Just k'' -> kindMetas k'' + KStar -> pure [] + KFun k1 k2 -> (++) <$> kindMetas k1 <*> kindMetas k2 + + +-- pre-condition: 'v' zonks to itself. +-- post-condition: 'k' zonks to a kind which does not contain 'v'. +kindOccursCheck :: KindVar -> Kind -> Expand () +kindOccursCheck v k = do + free <- kindMetas k + if v `elem` free + then do + k' <- zonkKind k + throwError $ KindCheckError $ KindOccursCheckFailed v k' + else pure () +-- pre-condition: 'v' zonks to itself. +-- post-condition: @KMetaVar v@, 'k', and the return value all zonk to the same +-- kind. +setKindVar :: KindVar -> Kind -> Expand Kind +setKindVar v k@(KMetaVar v') + | v == v' = + pure k + | otherwise = + (view (expanderKindStore . at v') <$> getState) >>= + \case + Nothing -> do + kindOccursCheck v k + modifyState $ set (expanderKindStore . at v) (Just k) + pure k + Just k' -> do + -- Recur to the root, both to compress the path from 'v' and to + -- make sure we don't make 'v' point indirectly to itself. + k'' <- setKindVar v k' + -- Also compress v' + modifyState $ set (expanderKindStore . at v') (Just k'') + pure k'' +setKindVar v k = do + kindOccursCheck v k + modifyState $ set (expanderKindStore . at v) (Just k) + pure k + +-- post-condition: 'kind1' and 'kind2' both zonk to the same kind. equateKinds :: UnificationErrorBlame blame => blame -> Kind -> Kind -> Expand () equateKinds blame kind1 kind2 = equateKinds' kind1 kind2 >>= @@ -324,7 +373,7 @@ equateKinds blame kind1 kind2 = k1' <- zonkKind kind1 k2' <- zonkKind kind2 loc <- getBlameLoc blame - throwError $ KindMismatch loc k1' k2' + throwError $ KindCheckError $ KindMismatch loc k1' k2' where -- Rigid-rigid cases equateKinds' KStar KStar = pure True diff --git a/src/Pretty.hs b/src/Pretty.hs index 238d37c5..422ba7de 100644 --- a/src/Pretty.hs +++ b/src/Pretty.hs @@ -311,14 +311,14 @@ instance Pretty VarInfo (Scheme Ty) where text "∀" <> (align $ group $ vsep [ group $ - vsep (zipWith ppArgKind typeVarNames argKinds) <> text "." + vsep (zipWith ppArgKind schemeVarNames argKinds) <> text "." , pp env t ]) where ppArgKind varName kind = parens (text varName <+> text ":" <+> pp env kind) -typeVarNames :: [Text] -typeVarNames = +schemeVarNames :: [Text] +schemeVarNames = greek ++ [ base <> T.pack (show i) | (base, i) <- greekNum @@ -332,6 +332,8 @@ typeVarNames = , base <- greek ] +schemeVarName :: SchemeVar -> Text +schemeVarName (SchemeVar n) = schemeVarNames !! fromIntegral n instance Pretty VarInfo TypeConstructor where pp _ TSyntax = text "Syntax" @@ -343,7 +345,7 @@ instance Pretty VarInfo TypeConstructor where pp _ TIO = text "IO" pp _ TType = text "Type" pp env (TDatatype t) = pp env t - pp _ (TSchemaVar n) = text $ typeVarNames !! fromIntegral n + pp _ (TSchemaVar v) = text $ schemeVarName v pp _ (TMetaVar v) = text "META" <> viaShow v -- TODO instance Pretty VarInfo a => Pretty VarInfo (TyF a) where @@ -390,7 +392,7 @@ instance (Pretty VarInfo s, Pretty VarInfo t, PrettyBinder VarInfo a, Pretty Var (hang 2 $ group $ vsep ( text "data" <+> text x <+> hsep [ parens (text α <+> ":" <+> pp env k) - | α <- typeVarNames + | α <- schemeVarNames | k <- argKinds ] <+> text "=" diff --git a/src/Pretty/Renumber.hs b/src/Pretty/Renumber.hs new file mode 100644 index 00000000..67663f2c --- /dev/null +++ b/src/Pretty/Renumber.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Pretty.Renumber where + +import Control.Lens +import Control.Monad.State + +import Type +import Util.Store (Store) +import Util.Store qualified as Store +import Kind (KindVar) + + +newtype Renumbered = Renumbered + { unRenumbered :: Int } + +-- | The goal is to give a small, unique number to the few unification variables +-- which are present in a particular error message, in order to turn +-- +-- > Infinite type detected: (MetaPtr 57868) = (List META(MetaPtr 57868)) +-- +-- into something more readable, like +-- +-- > Infinite type detected: ?1 = (List ?1) +-- +-- In order to do this, it is important to call 'renumber' _once_, on all the +-- unification variables in the error message, rather than calling 'renumber' on +-- separate components of the message and combining them. +renumber + :: forall s t u + . Traversal s t MetaPtr Renumbered + -> Traversal t u KindVar Renumbered + -> s -> u +renumber typeVars kindVars s = u + where + (t, n) = flip evalState Store.empty $ do + t_ <- traverseOf typeVars renumberTypeVar s + store <- get + let n_ = Store.size store + pure (t_, n_) + u = flip evalState Store.empty $ do + traverseOf kindVars renumberKindVar t + + renumberTypeVar :: MetaPtr -> State (Store MetaPtr Renumbered) Renumbered + renumberTypeVar metaPtr = do + store <- get + case Store.lookup metaPtr store of + Just renumbered -> do + pure renumbered + Nothing -> do + let i = Store.size store + let r = Renumbered i + put $ Store.insert metaPtr r store + pure r + + renumberKindVar :: KindVar -> State (Store KindVar Renumbered) Renumbered + renumberKindVar kindVar = do + store <- get + case Store.lookup kindVar store of + Just renumbered -> do + pure renumbered + Nothing -> do + let i = n + Store.size store + let r = Renumbered i + put $ Store.insert kindVar r store + pure r diff --git a/src/Type.hs b/src/Type.hs index cc5d377f..5b4de6e7 100644 --- a/src/Type.hs +++ b/src/Type.hs @@ -36,6 +36,13 @@ newMetaPtr = MetaPtr <$> newUnique instance Show MetaPtr where show (MetaPtr i) = "(MetaPtr " ++ show (hashUnique i) ++ ")" +newtype SchemeVar = SchemeVar Natural + deriving newtype (Enum, Eq, HasKey, Ord, Show) + deriving stock Data + +firstSchemeVar :: SchemeVar +firstSchemeVar = SchemeVar 0 + data TypeConstructor = TSyntax | TInteger @@ -46,7 +53,7 @@ data TypeConstructor | TIO | TType | TDatatype Datatype - | TSchemaVar Natural + | TSchemaVar SchemeVar | TMetaVar MetaPtr deriving (Data, Eq, Show) makePrisms ''TypeConstructor @@ -115,7 +122,7 @@ class TyLike a arg | a -> arg where tIO :: arg -> a tType :: a tDatatype :: Datatype -> [arg] -> a - tSchemaVar :: Natural -> [arg] -> a + tSchemaVar :: SchemeVar -> [arg] -> a tMetaVar :: MetaPtr -> a instance TyLike (TyF a) a where diff --git a/src/Util/Key.hs b/src/Util/Key.hs index fba1b3d2..9f010887 100644 --- a/src/Util/Key.hs +++ b/src/Util/Key.hs @@ -4,6 +4,8 @@ module Util.Key (HasKey(..) ) where +import Numeric.Natural + class HasKey a where getKey :: a -> Int fromKey :: Int -> a @@ -11,3 +13,7 @@ class HasKey a where instance HasKey Int where getKey = id fromKey = id + +instance HasKey Natural where + getKey = fromIntegral + fromKey = fromIntegral \ No newline at end of file diff --git a/src/Util/Store.hs b/src/Util/Store.hs index 26960169..d8834043 100644 --- a/src/Util/Store.hs +++ b/src/Util/Store.hs @@ -10,19 +10,24 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeOperators #-} -- | wrapper over IntMap for our purposes module Util.Store ( lookup + , (!) , singleton , insert , toList + , toAscList , fromList , Store , unionWith , mapKeys , mapMaybeWithKey + , empty + , size ) where @@ -70,6 +75,11 @@ instance (c ~ d) => Each (Store c a) (Store d b) a b where lookup :: HasKey p => p -> Store p v -> Maybe v lookup ptr graph = getKey ptr `IM.lookup` unStore graph +(!) :: HasKey p => Store p v -> p -> v +graph ! ptr = case lookup ptr graph of + Just v -> v + Nothing -> error "Store.!!: key not found" + singleton :: HasKey p => p -> v -> Store p v singleton ptr val = Store $! IM.singleton (getKey ptr) val @@ -79,6 +89,9 @@ insert k v str = Store $! IM.insert (getKey k) v (unStore str) toList :: HasKey p => Store p v -> [(p,v)] toList str = map (first fromKey) $ IM.toList (unStore str) +toAscList :: HasKey p => Store p v -> [(p,v)] +toAscList str = map (first fromKey) $ IM.toAscList (unStore str) + fromList :: HasKey p => [(p,v)] -> Store p v fromList ps = Store $! IM.fromList $ map (first getKey) ps @@ -94,3 +107,9 @@ mapMaybeWithKey f s = Store $! IM.mapMaybeWithKey (f . fromKey) (unStore s) mapKeys :: HasKey p => (p -> p) -> Store p v -> Store p v mapKeys f s = Store $! IM.mapKeys (getKey . f . fromKey) (unStore s) + +empty :: Store p v +empty = Store IM.empty + +size :: Store p v -> Int +size = IM.size . unStore \ No newline at end of file