Continue plumbing new names through

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)
 

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)

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)

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)
 

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
 

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

src/Cryptol/TypeCheck/AST.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE DeriveGeneric                       #-}
 module Cryptol.TypeCheck.AST
   ( module Cryptol.TypeCheck.AST
+  , Name()
   , TFun(..)
   , Selector(..)
   , Import(..)

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

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

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