Almost complete module instantiation

src/Cryptol/ModuleSystem/InstantiateModule.hs

@@ -8,8 +8,9 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Map (Map)
 import qualified Data.Map as Map
-import           MonadLib(Id,ReaderT,runReaderT,runId,ask)
+import           MonadLib(ReaderT,runReaderT,ask)
 
+import Cryptol.Parser.Position(Located(..))
 import Cryptol.ModuleSystem.Name
 import Cryptol.ModuleSystem.Exports(ExportSpec(..))
 import Cryptol.TypeCheck.AST
@@ -29,16 +30,15 @@ especially when working with dictionaries.
 -- | Convert a module instantiation into a partial module.
 -- The resulting module is incomplete because it is missing the definitions
 -- from the instantiation.
-instantiateModule :: Supply           {- ^ To generate fresh names -} ->
+instantiateModule :: FreshM m =>
                      Module           {- ^ Parametrized module -} ->
                      ModName          {- ^ Name of the new module -} ->
                      Map TParam Type  {- ^ Type params -} ->
                      Map Name Expr    {- ^ Value parameters -} ->
-                     ([Prop], Module, Supply)
+                     m ([Located Prop], Module)
                      -- ^ Instantiated constraints, fresh module, new supply
-instantiateModule s func newName tpMap vpMap = (ps, m, s1)
-  where
-  ((ps,m),s1) = runInstM newName s $
+instantiateModule func newName tpMap vpMap =
+  runReaderT newName $
     do let oldVpNames = Map.keys vpMap
        -- XXX: If the defining Expr is already just a name, we should
        -- just use that name directly.
@@ -53,7 +53,7 @@ instantiateModule s func newName tpMap vpMap = (ps, m, s1)
            su = listSubst
                   [ (TVBound tp, t) | (tp,t) <- Map.toList (tyParamMap env) ]
 
-           goals = apSubst su (mParamConstraints func)
+           goals = map (fmap (apSubst su)) (mParamConstraints func)
            -- Constraints to discharge about the type instances
 
        let renamedDecls = inst env (mDecls func)
@@ -72,6 +72,7 @@ instantiateModule s func newName tpMap vpMap = (ps, m, s1)
                  , mDecls             = paramDecls ++ renamedDecls
                  } )
 
+  where
   mkParamDecl vpNames (x,e) =
       NonRecursive Decl
         { dName        = vpNames Map.! x
@@ -105,24 +106,21 @@ instance Defines DeclGroup where
 
 --------------------------------------------------------------------------------
 
-type InstM = ReaderT ModName (SupplyT Id)
-
-runInstM :: ModName -> Supply -> InstM a -> (a, Supply)
-runInstM mn s = runId . runSupplyT s . runReaderT mn
-
+type InstM = ReaderT ModName
 
 -- | Generate a new instance of a declared name.
-freshenName :: Name -> InstM Name
+freshenName :: FreshM m => Name -> InstM m Name
 freshenName x =
   do m <- ask
      liftSupply (mkDeclared m (nameIdent x) (nameFixity x) (nameLoc x))
 
 -- | Compute renaming environment from a module instantiation.
 -- computeEnv :: ModInst -> InstM Env
-computeEnv :: Module {- ^ Functor being instantiated -} ->
+computeEnv :: FreshM m =>
+              Module {- ^ Functor being instantiated -} ->
               Map TParam Type {- replace type params by type -} ->
               Map Name Name {- replace value parameters by other names -} ->
-              InstM Env
+              InstM m Env
 computeEnv m tpMap vpMap =
   do tss <- mapM freshTy (Map.toList (mTySyns m))
      nts <- mapM freshTy (Map.toList (mNewtypes m))

src/Cryptol/ModuleSystem/Interface.hs

@@ -26,6 +26,7 @@ module Cryptol.ModuleSystem.Interface (
 import           Cryptol.ModuleSystem.Name
 import           Cryptol.TypeCheck.AST
 import           Cryptol.Utils.Ident (ModName)
+import           Cryptol.Parser.Position(Located)
 
 import qualified Data.Map as Map
 
@@ -46,7 +47,7 @@ data Iface = Iface
 
 data IfaceParams = IfaceParams
   { ifParamTypes :: [TParam]     -- ^ Uninterpreted types
-  , ifParamConstraints :: [Prop]            -- ^ Constraints on param. types
+  , ifParamConstraints :: [Located Prop] -- ^ Constraints on param. types
   , ifParamFuns  :: Map.Map Name IfaceDecl  -- ^ Uninterpreted value constants
   } deriving (Show, Generic, NFData)
 

src/Cryptol/ModuleSystem/Renamer.hs

@@ -365,7 +365,12 @@ instance Rename TopDecl where
     DParameterFun f  -> DParameterFun  <$> rename f
     DParameterType f -> DParameterType <$> rename f
 
-    DParameterConstraint d -> DParameterConstraint <$> mapM rename d
+    DParameterConstraint d -> DParameterConstraint <$> mapM renameLocated d
+
+renameLocated :: Rename f => Located (f PName) -> RenameM (Located (f Name))
+renameLocated x =
+  do y <- rename (thing x)
+     return x { thing = y }
 
 instance Rename ParameterType where
   rename a =

src/Cryptol/Parser.y

@@ -268,7 +268,7 @@ par_decls                            :: { [TopDecl PName] }
 par_decl                         :: { TopDecl PName }
   : mbDoc        name ':' schema    { mkParFun $1 $2 $4 }
   | mbDoc 'type' name ':' kind      { mkParType $1 $3 $5 }
-  | mbDoc 'type' 'constraint' type  {% fmap (DParameterConstraint . thing)
+  | mbDoc 'type' 'constraint' type  {% fmap (DParameterConstraint . distrLoc)
                                             (mkProp $4) }
 
 

src/Cryptol/Parser/AST.hs

@@ -129,7 +129,8 @@ data TopDecl name =
   | TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t
   | Include (Located FilePath)          -- ^ @include File@
   | DParameterType (ParameterType name) -- ^ @parameter type T : #@
-  | DParameterConstraint [Prop name]    -- ^ @parameter type constraint (fin T)@
+  | DParameterConstraint [Located (Prop name)]
+                                        -- ^ @parameter type constraint (fin T)@
   | DParameterFun  (ParameterFun name)  -- ^ @parameter someVal : [256]@
                     deriving (Show, Generic, NFData)
 

src/Cryptol/Parser/ParserUtils.hs

@@ -426,6 +426,11 @@ mkDoc ltxt = ltxt { thing = docStr }
         Nothing     -> False
 
 
+distrLoc :: Located [a] -> [Located a]
+distrLoc x = [ Located { srcRange = r, thing = a } | a <- thing x ]
+  where r = srcRange x
+
+
 mkProp :: Type PName -> ParseM (Located [Prop PName])
 mkProp ty =
   case ty of

src/Cryptol/TypeCheck/AST.hs

@@ -28,6 +28,7 @@ module Cryptol.TypeCheck.AST
   , module Cryptol.TypeCheck.Type
   ) where
 
+import Cryptol.Parser.Position(Located)
 import Cryptol.ModuleSystem.Name
 import Cryptol.ModuleSystem.Exports(ExportSpec(..)
                                    , isExportedBind, isExportedType)
@@ -53,7 +54,7 @@ data Module = Module { mName        :: !ModName
                      , mTySyns      :: Map Name TySyn
                      , mNewtypes    :: Map Name Newtype
                      , mParamTypes  :: [ TParam ]
-                     , mParamConstraints :: [Prop]
+                     , mParamConstraints :: [Located Prop]
                      , mParamFuns   :: Map Name Schema
                      , mDecls       :: [DeclGroup]
                      } deriving (Show, Generic, NFData)

src/Cryptol/TypeCheck/CheckModuleInstance.hs

@@ -0,0 +1,165 @@
+module Cryptol.TypeCheck.CheckModuleInstance (inferModuleInstance) where
+
+import           Data.Map ( Map )
+import qualified Data.Map as Map
+import           Control.Monad(unless)
+
+import Cryptol.Parser.Position(Located(..))
+import qualified Cryptol.Parser.AST as P
+import Cryptol.ModuleSystem.Name(Name,nameIdent,nameLoc)
+import Cryptol.ModuleSystem.InstantiateModule(instantiateModule)
+import Cryptol.TypeCheck.AST
+import Cryptol.TypeCheck.Monad
+import Cryptol.TypeCheck.Infer
+import Cryptol.Utils.PP
+import Cryptol.Utils.Panic
+
+
+
+inferModuleInstance :: Module {- ^ type-checked functor -} ->
+                       Module {- ^ type-checked instance -} ->
+                       InferM Module -- ^ Instantiated module
+inferModuleInstance func inst =
+  do tMap <- checkTyParams func inst
+     vMap <- checkValParams func inst
+     (ctrs, m) <- instantiateModule func (mName inst) tMap vMap
+     let toG p = Goal { goal = thing p
+                      , goalRange = srcRange p
+                      , goalSource = CtModuleInstance (mName inst)
+                      }
+     addGoals (map toG ctrs)
+     return Module { mName = mName m
+                   , mExports = mExports m
+                   , mImports = mImports inst ++ mImports m
+                                -- Note that this is just here to record
+                                -- the full dependencies, the actual imports
+                                -- might be ambiguous, but that shouldn't
+                                -- matters as names have been already resolved
+                   , mTySyns = Map.union (mTySyns inst) (mTySyns m)
+                   , mNewtypes = Map.union (mNewtypes inst) (mNewtypes m)
+                   , mParamTypes       = mParamTypes inst
+                   , mParamConstraints = mParamConstraints inst
+                   , mParamFuns        = mParamFuns inst
+                   , mDecls            = mDecls inst ++ mDecls m
+                   }
+
+-- | Check that the type parameters of the functors all have appropriate
+-- definitions.
+checkTyParams :: Module -> Module -> InferM (Map TParam Type)
+checkTyParams func inst =
+  Map.fromList <$> mapM checkTParamDefined (mParamTypes func)
+
+  where
+  -- Maps to lookup things by identifier (i.e., lexical name)
+  -- rather than using the name unique.
+  identMap f m = Map.fromList [ (f x, ts) | (x,ts) <- Map.toList m ]
+  tySyns       = identMap nameIdent (mTySyns inst)
+  newTys       = identMap nameIdent (mNewtypes inst)
+  tParams      = Map.fromList [ (tpId x, x) | x <- mParamTypes inst ]
+
+  tpId x       = case tpName x of
+                   Just n  -> nameIdent n
+                   Nothing -> panic "inferModuleInstance.tpId" ["Missing name"]
+
+  -- Find a definition for a given type parameter
+  checkTParamDefined tp =
+    let x = tpId tp
+    in case Map.lookup x tySyns of
+         Just ts -> checkTySynDef tp ts
+         Nothing ->
+           case Map.lookup x newTys of
+             Just nt -> checkNewTyDef tp nt
+             Nothing ->
+               case Map.lookup x tParams of
+                 Just tp1 -> checkTP tp tp1
+                 Nothing ->
+                   do recordError $ ErrorMsg $
+                        text "Missing definition for type parameter:" <+> pp x
+                      return (tp, TVar (TVBound tp)) -- hm, maybe just stop!
+
+  -- Check that a type parameter defined as a type synonym is OK
+  checkTySynDef tp ts =
+    do let k1 = kindOf tp
+           k2 = kindOf ts
+       unless (k1 == k2) (recordError (KindMismatch k1 k2))
+
+       let nm  = tsName ts
+           src = CtPartialTypeFun (UserTyFun nm)
+       mapM_ (newGoal src) (tsConstraints ts)
+
+       return (tp, TUser nm [] (tsDef ts))
+
+  -- Check that a type parameter defined a newtype is OK
+  -- This one is a bit weird: since the newtype is deinfed in the
+  -- instantiation, it will not be exported, and so won't be usable
+  -- in type signatures, directly.   This could be worked around
+  -- if the parametrized module explictly exported a parameter via
+  -- a type synonym like this: `type T = p`, where `p` is one of
+  -- the parametersm and the declartion for `T` is public.
+  checkNewTyDef tp nt =
+    do let k1 = kindOf tp
+           k2 = kindOf nt
+       unless (k1 == k2) (recordError (KindMismatch k1 k2))
+
+       let nm = ntName nt
+           src = CtPartialTypeFun (UserTyFun nm)
+       mapM_ (newGoal src) (ntConstraints nt)
+
+       return (tp, TCon (TC (TCNewtype (UserTC nm k2))) [])
+
+  -- Check that a type parameter defined as another type parameter is OK
+  checkTP tp tp1 =
+    do let k1 = kindOf tp
+           k2 = kindOf tp1
+       unless (k1 == k2) (recordError (KindMismatch k1 k2))
+
+       return (tp, TVar (TVBound tp1))
+
+
+
+
+checkValParams :: Module -> Module -> InferM (Map Name Expr)
+checkValParams func inst =
+  Map.fromList <$> mapM checkParam (Map.toList (mParamFuns func))
+  where
+  valMap = Map.fromList [ (nameIdent (dName d), (dName d, dSignature d))
+                          | dg <- mDecls inst, d <- groupDecls dg ]
+
+  checkParam (x,sP) =
+    case Map.lookup (nameIdent x) valMap of
+      Just (n,sD) -> do e <- makeValParamDef n sD sP
+                        return (n,e)
+      Nothing -> do recordError $ ErrorMsg
+                                $ text "Mising definition for value parameter"
+                                    <+> pp x
+                    return (x, panic "checkValParams" ["Should not use this"])
+
+
+
+-- | Given a parameter definition, compute an appropriate instantiation
+-- that will match the actual schema for the parameter.
+makeValParamDef :: Name   {- ^ Definition of parameter -} ->
+                   Schema {- ^ Schema for parameter definition -} ->
+                   Schema {- ^ Schema for parameter -} ->
+                   InferM Expr {- ^ Expression to use for param definition -}
+
+makeValParamDef x sDef pDef =
+  withVar x sDef $ do DExpr e <- dDefinition <$> checkSigB bnd (pDef,[])
+                      return e
+  where
+  bnd = P.Bind { P.bName      = loc x
+               , P.bParams    = []
+               , P.bDef       = loc (P.DExpr (P.EVar x))
+
+                -- unused
+               , P.bSignature = Nothing
+               , P.bInfix     = False
+               , P.bFixity    = Nothing
+               , P.bPragmas   = []
+               , P.bMono      = False
+               , P.bDoc       = Nothing
+               }
+  loc a = P.Located { P.srcRange = nameLoc x, P.thing = a }
+
+
+

src/Cryptol/TypeCheck/Depends.hs

@@ -106,7 +106,7 @@ orderBinds bs = mkScc [ (b, map thing defs, Set.toList uses)
 class FromDecl d where
   toBind             :: d -> Maybe (P.Bind Name)
   toParamFun         :: d -> Maybe (P.ParameterFun Name)
-  toParamConstraints :: d -> [P.Prop Name]
+  toParamConstraints :: d -> [P.Located (P.Prop Name)]
   toTyDecl           :: d -> Maybe TyDecl
   isTopDecl          :: d -> Bool
 

src/Cryptol/TypeCheck/InferTypes.hs

@@ -25,7 +25,7 @@ import qualified Cryptol.Parser.AST as P
 import           Cryptol.Utils.PP
 import           Cryptol.ModuleSystem.Name (asPrim,nameLoc)
 import           Cryptol.TypeCheck.PP
-import           Cryptol.Utils.Ident (Ident,identText)
+import           Cryptol.Utils.Ident (Ident,identText,ModName)
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.Misc(anyJust)
 
@@ -192,6 +192,7 @@ data ConstraintSource
   | CtPartialTypeFun TyFunName -- ^ Use of a partial type function.
   | CtImprovement
   | CtPattern Doc         -- ^ Constraints arising from type-checking patterns
+  | CtModuleInstance ModName -- ^ Instantiating a parametrized module
     deriving (Show, Generic, NFData)
 
 data TyFunName = UserTyFun Name | BuiltInTyFun TFun
@@ -215,6 +216,7 @@ instance TVars ConstraintSource where
       CtPartialTypeFun _ -> src
       CtImprovement    -> src
       CtPattern _      -> src
+      CtModuleInstance _ -> src
 
 instance TVars Warning where
   apSubst su warn =
@@ -543,6 +545,7 @@ instance PP ConstraintSource where
       CtPartialTypeFun f -> text "use of partial type function" <+> pp f
       CtImprovement   -> text "examination of collected goals"
       CtPattern desc  -> text "checking a pattern:" <+> desc
+      CtModuleInstance n -> text "module instantiation" <+> pp n
 
 ppUse :: Expr -> Doc
 ppUse expr =

src/Cryptol/TypeCheck/Kind.hs

@@ -127,11 +127,13 @@ checkType t k =
   do (_, t1) <- withTParams True schemaParam {-no params-} [] $ doCheckType t k
      return (tRebuild t1)
 
-checkParameterConstraints :: [P.Prop Name] -> InferM [Prop]
+checkParameterConstraints :: [Located (P.Prop Name)] -> InferM [Located Prop]
 checkParameterConstraints ps =
-  do (_, cs) <- withTParams False schemaParam {-no params-}[]
-                                                        (mapM checkProp ps)
-     return (map tRebuild cs)
+  do (_, cs) <- withTParams False schemaParam {-no params-}[] (mapM checkL ps)
+     return cs
+  where
+  checkL x = do p <- checkProp (thing x)
+                return x { thing = tRebuild p }
 
 
 {- | Check something with type parameters.

src/Cryptol/TypeCheck/Monad.hs

@@ -201,7 +201,7 @@ data RO = RO
   , iParamTypes :: Map Name TParam
     -- ^ Parameter types
 
-  , iParamConstraints :: [Prop]
+  , iParamConstraints :: [Located Prop]
     -- ^ Constraints on the type parameters
 
   , iParamFuns :: Map Name Schema
@@ -597,7 +597,7 @@ getParamFuns = IM $ asks iParamFuns
 getParamTypes :: InferM (Map Name TParam)
 getParamTypes = IM $ asks iParamTypes
 
-getParamConstraints :: InferM [Prop]
+getParamConstraints :: InferM [Located Prop]
 getParamConstraints = IM $ asks iParamConstraints
 
 -- | Get the set of bound type variables that are in scope.
@@ -696,7 +696,7 @@ withParamFuns xs (IM m) =
   add (x,s) = Map.insert x s
 
 -- | Add some assumptions for an entire module
-withParameterConstraints :: [Prop] -> InferM a -> InferM a
+withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
 withParameterConstraints ps (IM m) =
   IM $ mapReader (\r -> r { iParamConstraints = ps ++ iParamConstraints r }) m
 

src/Cryptol/TypeCheck/Solve.hs

@@ -18,6 +18,7 @@ module Cryptol.TypeCheck.Solve
   , defaultReplExpr
   ) where
 
+import           Cryptol.Parser.Position(thing)
 import           Cryptol.TypeCheck.PP(pp)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Monad
@@ -178,7 +179,7 @@ proveModuleTopLevel =
        [] -> return ()
        _  -> do as <- Map.elems <$> getParamTypes
                 gs <- getGoals
-                su <- proveImplication Nothing as cs gs
+                su <- proveImplication Nothing as (map thing cs) gs
                 extendSubst su
 
 
@@ -186,7 +187,7 @@ proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
 proveImplication lnam as ps gs =
   do evars <- varsWithAsmps
      solver <- getSolver
-     extra <- getParamConstraints
+     extra <- map thing <$> getParamConstraints
      (mbErr,su) <- io (proveImplicationIO solver lnam evars as (extra ++ ps) gs)
      case mbErr of
        Right ws -> mapM_ recordWarning ws