diff --git a/src/Cryptol/Eval/Env.hs b/src/Cryptol/Eval/Env.hs index e14fa3b5..417366b8 100644 --- a/src/Cryptol/Eval/Env.hs +++ b/src/Cryptol/Eval/Env.hs @@ -9,9 +9,11 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Safe #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE CPP #-} module Cryptol.Eval.Env where import Cryptol.Eval.Value +import Cryptol.ModuleSystem.Name import Cryptol.TypeCheck.AST import Cryptol.Utils.PP @@ -29,7 +31,7 @@ import Data.Monoid (Monoid(..)) type ReadEnv = EvalEnv data EvalEnv = EvalEnv - { envVars :: Map.Map QName Value + { envVars :: NameMap Value , envTypes :: Map.Map TVar TValue } deriving (Generic) diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs index fc19dd01..8a416341 100644 --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -354,8 +354,8 @@ lookupRecord f rec = case lookup f (fromVRecord rec) of -- this value, if we can determine it. -- -- XXX: View patterns would probably clean up this definition a lot. -toExpr :: Type -> Value -> Maybe Expr -toExpr ty val = case (ty, val) of +toExpr :: PrimMap -> Type -> Value -> Maybe Expr +toExpr prims ty val = case (ty, val) of (TRec tfs, VRecord vfs) -> do let fns = map fst vfs guard (map fst tfs == fns) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index d2c9b356..d8b01ec3 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -29,9 +29,14 @@ module Cryptol.ModuleSystem.Name ( -- * Name Maps , NameMap() , emptyNM + , nullNM , insertNM + , alterNM , lookupNM , findWithDefaultNM + , unionWithNM + , toListNM + , mapMaybeWithKeyNM ) where import Cryptol.Parser.Position (Range) @@ -205,15 +210,41 @@ mkParameter nIdent nLoc s = newtype NameMap a = NameMap { nmElems :: I.IntMap (Name,a) } deriving (Functor,Foldable,Traversable,Show) +toListNM :: NameMap a -> [(Name,a)] +toListNM NameMap { .. } = I.elems nmElems + emptyNM :: NameMap a emptyNM = NameMap { nmElems = I.empty } +nullNM :: NameMap a -> Bool +nullNM NameMap { .. } = I.null nmElems + insertNM :: Name -> a -> NameMap a -> NameMap a insertNM n a (NameMap ns) = NameMap (I.insert (nUnique n) (n,a) ns) lookupNM :: Name -> NameMap a -> Maybe a lookupNM Name { .. } (NameMap m) = snd `fmap` I.lookup nUnique m +alterNM :: Name -> (Maybe a -> Maybe a) -> NameMap a -> NameMap a +alterNM k f (NameMap m) = NameMap (I.alter f' (nUnique k) m) + where + f' (Just (n,a)) = do a' <- f (Just a) + return (n,a') + f' Nothing = do a <- f Nothing + return (k,a) + findWithDefaultNM :: a -> Name -> NameMap a -> a findWithDefaultNM a Name { .. } (NameMap m) = snd (I.findWithDefault (undefined,a) nUnique m) + +unionWithNM :: (a -> a -> a) -> NameMap a -> NameMap a -> NameMap a +unionWithNM combine (NameMap a) (NameMap b) = NameMap (I.unionWith combine' a b) + where + -- As the uniques were the same, the name values will also be the same. + combine' (n,x) (_,y) = (n,combine x y) + +mapMaybeWithKeyNM :: (Name -> a -> Maybe b) -> NameMap a -> NameMap b +mapMaybeWithKeyNM f (NameMap m) = NameMap (I.mapMaybeWithKey f' m) + where + f' _ (n,a) = do b <- f n a + return (n,b) diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 6024b962..ddd7517a 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -61,7 +61,7 @@ simpleBind x e = Bind { bName = x, bParams = [] , bDoc = Nothing } -sel :: Pattern PName -> PName -> Selector PName -> Bind PName +sel :: Pattern PName -> PName -> Selector -> Bind PName sel p x s = let (a,ts) = splitSimpleP p in simpleBind a (foldl ETyped (ESel (EVar x) s) ts) diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 92e6c64d..316b1d58 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -163,7 +163,7 @@ mkFixity assoc tok qns = (errorMessage (srcRange tok) "Fixity levels must be between 0 and 20") return (DFixity (Fixity assoc (fromInteger l)) qns) -mkTupleSel :: Range -> Integer -> ParseM (Located (Selector PName)) +mkTupleSel :: Range -> Integer -> ParseM (Located Selector) mkTupleSel pos n | n < 0 = errorMessage pos (show n ++ " is not a valid tuple selector (they start from 0).") @@ -280,7 +280,7 @@ changeExport e = map change change (TDNewtype n) = TDNewtype n { tlExport = e } change td@Include{} = td -mkTypeInst :: Named PName (Type PName) -> TypeInst PName +mkTypeInst :: Named (Type PName) -> TypeInst PName mkTypeInst x | nullIdent (getIdent (thing (name x))) = PosInst (value x) | otherwise = NamedInst x diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index 6e292915..c36e1793 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -74,6 +74,7 @@ {-# LANGUAGE PatternGuards, FlexibleInstances, MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE CPP #-} module Cryptol.Transform.MonoValues (rewModule) where import Cryptol.Parser.AST (Pass(MonoValues)) @@ -81,7 +82,6 @@ import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.TypeMap import Data.List(sortBy,groupBy) import Data.Either(partitionEithers) -import Data.Map (Map) import MonadLib #if __GLASGOW_HASKELL__ < 710 @@ -90,10 +90,10 @@ import Control.Applicative {- (f,t,n) |--> x means that when we spot instantiations of `f` with `ts` and `n` proof argument, we should replace them with `Var x` -} -newtype RewMap' a = RM (Map QName (TypesMap (Map Int a))) -type RewMap = RewMap' QName +newtype RewMap' a = RM (NameMap (TypesMap (Map Int a))) +type RewMap = RewMap' Name -instance TrieMap RewMap' (QName,[Type],Int) where +instance TrieMap RewMap' (Name,[Type],Int) where emptyTM = RM emptyTM nullTM (RM m) = nullTM m diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index cd065a5d..c8cf8231 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -13,6 +13,7 @@ {-# LANGUAGE DeriveGeneric #-} module Cryptol.TypeCheck.AST ( module Cryptol.TypeCheck.AST + , Name() , TFun(..) , Selector(..) , Import(..) diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index c76b63ac..53d7722a 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -21,10 +21,10 @@ import Data.Map ( Map ) import qualified Data.Map as Map -tcExpr :: Map QName Schema -> Expr -> Either Error (Schema, [ ProofObligation ]) +tcExpr :: Map Name Schema -> Expr -> Either Error (Schema, [ ProofObligation ]) tcExpr env e = runTcM env (exprSchema e) -tcDecls :: Map QName Schema -> [DeclGroup] -> Either Error [ ProofObligation ] +tcDecls :: Map Name Schema -> [DeclGroup] -> Either Error [ ProofObligation ] tcDecls env ds0 = case runTcM env (go ds0) of Left err -> Left err Right (_,ps) -> Right ps @@ -33,7 +33,7 @@ tcDecls env ds0 = case runTcM env (go ds0) of go (d : ds) = do xs <- checkDeclGroup d withVars xs (go ds) -tcModule :: Map QName Schema -> Module -> Either Error [ ProofObligation ] +tcModule :: Map Name Schema -> Module -> Either Error [ ProofObligation ] tcModule env m = tcDecls env (mDecls m) @@ -351,7 +351,7 @@ convertible t1 t2 = go t1 t2 -------------------------------------------------------------------------------- -- | Check a declaration. The boolean indicates if we should check the siganture -checkDecl :: Bool -> Decl -> TcM (QName, Schema) +checkDecl :: Bool -> Decl -> TcM (Name, Schema) checkDecl checkSig d = case dDefinition d of @@ -367,7 +367,7 @@ checkDecl checkSig d = reportError $ TypeMismatch s s1 return (dName d, s) -checkDeclGroup :: DeclGroup -> TcM [(QName, Schema)] +checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)] checkDeclGroup dg = case dg of NonRecursive d -> do x <- checkDecl True d @@ -379,7 +379,7 @@ checkDeclGroup dg = withVars xs $ mapM (checkDecl False) ds -checkMatch :: Match -> TcM ((QName, Schema), Type) +checkMatch :: Match -> TcM ((Name, Schema), Type) checkMatch ma = case ma of From x t e -> @@ -396,7 +396,7 @@ checkMatch ma = Let d -> do x <- checkDecl True d return (x, tNum (1 :: Int)) -checkArm :: [Match] -> TcM ([(QName, Schema)], Type) +checkArm :: [Match] -> TcM ([(Name, Schema)], Type) checkArm [] = reportError EmptyArm checkArm [m] = do (x,l) <- checkMatch m return ([x], l) @@ -416,7 +416,7 @@ checkArm (m : ms) = data RO = RO { roTVars :: Map Int TParam , roAsmps :: [Prop] - , roVars :: Map QName Schema + , roVars :: Map Name Schema } type ProofObligation = Schema -- but the type is of kind Prop @@ -441,7 +441,7 @@ instance Monad TcM where let TcM m1 = f a m1) -runTcM :: Map QName Schema -> TcM a -> Either Error (a, [ProofObligation]) +runTcM :: Map Name Schema -> TcM a -> Either Error (a, [ProofObligation]) runTcM env (TcM m) = case runM m ro rw of (Left err, _) -> Left err @@ -476,7 +476,7 @@ data Error = | BadMatch Type | EmptyArm | UndefinedTypeVaraible TVar - | UndefinedVariable QName + | UndefinedVariable Name deriving Show reportError :: Error -> TcM a @@ -492,10 +492,10 @@ withAsmp p (TcM m) = TcM $ do ro <- ask local ro { roAsmps = p : roAsmps ro } m -withVar :: QName -> Type -> TcM a -> TcM a +withVar :: Name -> Type -> TcM a -> TcM a withVar x t = withVars [(x,tMono t)] -withVars :: [(QName, Schema)] -> TcM a -> TcM a +withVars :: [(Name, Schema)] -> TcM a -> TcM a withVars xs (TcM m) = TcM $ do ro <- ask local ro { roVars = Map.union (Map.fromList xs) (roVars ro) } m @@ -519,7 +519,7 @@ lookupTVar x = | otherwise -> reportError $ KindMismatch (kindOf tp) k Nothing -> reportError $ UndefinedTypeVaraible x -lookupVar :: QName -> TcM Schema +lookupVar :: Name -> TcM Schema lookupVar x = do ro <- TcM ask case Map.lookup x (roVars ro) of diff --git a/src/Cryptol/TypeCheck/TypeMap.hs b/src/Cryptol/TypeCheck/TypeMap.hs index 862acf19..f21a18d0 100644 --- a/src/Cryptol/TypeCheck/TypeMap.hs +++ b/src/Cryptol/TypeCheck/TypeMap.hs @@ -19,6 +19,7 @@ module Cryptol.TypeCheck.TypeMap , List(..) ) where +import Cryptol.ModuleSystem.Name import Cryptol.TypeCheck.AST import qualified Data.Map as Map @@ -168,3 +169,12 @@ updSub k f = Just . alterTM k f . fromMaybe emptyTM instance Show a => Show (TypeMap a) where showsPrec p xs = showsPrec p (toListTM xs) + +instance TrieMap NameMap Name where + emptyTM = emptyNM + nullTM = nullNM + lookupTM = lookupNM + alterTM = alterNM + unionTM = unionWithNM + toListTM = toListNM + mapMaybeWithKeyTM = mapMaybeWithKeyNM diff --git a/src/Cryptol/TypeCheck/TypeOf.hs b/src/Cryptol/TypeCheck/TypeOf.hs index 68909365..cdcf7bd8 100644 --- a/src/Cryptol/TypeCheck/TypeOf.hs +++ b/src/Cryptol/TypeCheck/TypeOf.hs @@ -25,7 +25,7 @@ import qualified Data.Map as Map -- | Given a typing environment and an expression, compute the type of -- the expression as quickly as possible, assuming that the expression -- is well formed with correct type annotations. -fastTypeOf :: Map QName Schema -> Expr -> Type +fastTypeOf :: Map Name Schema -> Expr -> Type fastTypeOf tyenv expr = case expr of -- Monomorphic fragment @@ -55,7 +55,7 @@ fastTypeOf tyenv expr = _ -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf" [ "unexpected polymorphic type" ] -fastSchemaOf :: Map QName Schema -> Expr -> Schema +fastSchemaOf :: Map Name Schema -> Expr -> Schema fastSchemaOf tyenv expr = case expr of -- Polymorphic fragment