Checkpoint, adding constraints

src/Cryptol/ModuleSystem/Env.hs

@@ -145,7 +145,8 @@ focusedEnv me = fold $
      let (ifaces,names) = unzip deps
          Iface { .. }   = lmInterface lm
          localDecls     = ifPublic `mappend` ifPrivate
-         localNames     = R.unqualifiedEnv localDecls
+         localNames     = R.unqualifiedEnv localDecls `mappend`
+                          R.modParamsNamingEnv ifParams
          namingEnv      = localNames `R.shadowing` mconcat names
 
      return (mconcat (localDecls:ifaces), namingEnv, R.toNameDisp namingEnv)

src/Cryptol/ModuleSystem/Interface.hs

@@ -45,7 +45,7 @@ data Iface = Iface
   } deriving (Show, Generic, NFData)
 
 data IfaceParams = IfaceParams
-  { ifParamTypes :: Map.Map Name TParam     -- ^ Uninterpreted types
+  { ifParamTypes :: [TParam]     -- ^ Uninterpreted types
   , ifParamConstraints :: [Prop]            -- ^ Constraints on param. types
   , ifParamFuns  :: Map.Map Name IfaceDecl  -- ^ Uninterpreted value constants
   } deriving (Show, Generic, NFData)

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -21,11 +21,12 @@ import Cryptol.ModuleSystem.Interface
 import Cryptol.ModuleSystem.Name
 import Cryptol.Parser.AST
 import Cryptol.Parser.Position
+import qualified Cryptol.TypeCheck.Type as T
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic (panic)
 
 import Data.List (nub)
-import Data.Maybe (catMaybes,fromMaybe)
+import Data.Maybe (catMaybes,fromMaybe,mapMaybe)
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 import MonadLib (runId,Id)
@@ -258,6 +259,27 @@ unqualifiedEnv IfaceDecls { .. } =
               | d    <- Map.elems ifDecls ]
 
 
+-- | Compute an unqualified naming environment from the parameters of a module
+modParamsNamingEnv :: IfaceParams -> NamingEnv
+modParamsNamingEnv IfaceParams { .. } =
+  NamingEnv { neExprs = Map.fromList $ map fromFu $ Map.keys ifParamFuns
+            , neTypes = Map.fromList $ mapMaybe fromTy ifParamTypes
+            , neFixity = Map.fromList $ mapMaybe toFix $ Map.toList ifParamFuns
+            }
+
+  where
+  toPName n = mkUnqual (nameIdent n)
+
+  fromTy tp = do nm <- T.tpName tp
+                 return (toPName nm, [nm])
+
+  fromFu f  = (toPName f, [f])
+
+  toFix (f,x) = do d <- ifDeclFixity x
+                   return (f, d)
+
+
+
 data ImportIface = ImportIface Import Iface
 
 -- | Produce a naming environment from an interface file, that contains a

src/Cryptol/TypeCheck/AST.hs

@@ -51,7 +51,7 @@ data Module = Module { mName        :: !ModName
                      , mImports     :: [Import]
                      , mTySyns      :: Map Name TySyn
                      , mNewtypes    :: Map Name Newtype
-                     , mParamTypes  :: Map Name TParam
+                     , mParamTypes  :: [ TParam ]
                      , mParamConstraints :: [Prop]
                      , mParamFuns   :: Map Name Schema
                      , mDecls       :: [DeclGroup]
@@ -305,5 +305,5 @@ instance PP (WithNames Module) where
     vcat (map pp mImports) $$
     -- XXX: Print tysyns
     -- XXX: Print abstarct types/functions
-    vcat (map (ppWithNames nm) mDecls)
+    vcat (map (ppWithNames (addTNames mParamTypes nm)) mDecls)
 

src/Cryptol/TypeCheck/Infer.hs

@@ -48,7 +48,7 @@ import           Control.Monad(when,zipWithM)
 inferModule :: P.Module Name -> InferM Module
 inferModule m =
   inferDs (P.mDecls m) $ \ds1 ->
-    do simplifyAllConstraints
+    do proveModuleTopLevel
        ts <- getTSyns
        nts <- getNewtypes
        pTs <- getParamTypes
@@ -59,7 +59,7 @@ inferModule m =
                      , mImports   = map thing (P.mImports m)
                      , mTySyns    = Map.mapMaybe onlyLocal ts
                      , mNewtypes  = Map.mapMaybe onlyLocal nts
-                     , mParamTypes= pTs
+                     , mParamTypes= Map.elems pTs
                      , mParamConstraints = pCs
                      , mParamFuns = pFuns
                      , mDecls     = ds1
@@ -791,7 +791,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
 
      asmps1 <- applySubst asmps0
 
-     defSu1 <- proveImplication (thing (P.bName b)) as asmps1 now
+     defSu1 <- proveImplication (Just (thing (P.bName b))) as asmps1 now
      let later = apSubst defSu1 later0
          asmps = apSubst defSu1 asmps1
 

src/Cryptol/TypeCheck/InferTypes.hs

@@ -86,7 +86,8 @@ data HasGoal = HasGoal
 
 -- | Delayed implication constraints, arising from user-specified type sigs.
 data DelayedCt = DelayedCt
-  { dctSource :: Name   -- ^ Signature that gave rise to this constraint
+  { dctSource :: Maybe Name   -- ^ Signature that gave rise to this constraint
+                              -- Nothing means module top-level
   , dctForall :: [TParam]
   , dctAsmps  :: [Prop]
   , dctGoals  :: [Goal]
@@ -564,8 +565,10 @@ instance PP (WithNames DelayedCt) where
   ppPrec _ (WithNames d names) =
     sig $$ nest 2 (vars $$ asmps $$ vcat (map (ppWithNames ns1) (dctGoals d)))
     where
-    sig = text "In the definition of" <+> quotes (pp name) <>
-          comma <+> text "at" <+> pp (nameLoc name) <> colon
+    sig = case name of
+            Just n -> text "In the definition of" <+> quotes (pp n) <>
+                          comma <+> text "at" <+> pp (nameLoc n) <> colon
+            Nothing -> text "When checking the module's parameters."
 
     name  = dctSource d
     vars = case dctForall d of

src/Cryptol/TypeCheck/Solve.hs

@@ -11,6 +11,7 @@
 module Cryptol.TypeCheck.Solve
   ( simplifyAllConstraints
   , proveImplication
+  , proveModuleTopLevel
   , wfType
   , wfTypeFunction
   , improveByDefaultingWith
@@ -172,9 +173,22 @@ simpHasGoals = go False [] =<< getHasGoals
        changes' `seq` unsolved `seq` go changes' unsolved' todo
 
 
+-- | Try to clean-up any left-over constraints after we've checked everything
+-- in a module.  Typically these are either trivial things, or constraints
+-- on the module's type parameters.
+proveModuleTopLevel :: InferM ()
+proveModuleTopLevel =
+  do simplifyAllConstraints
+     cs <- getParamConstraints
+     case cs of
+       [] -> return ()
+       _  -> do as <- Map.elems <$> getParamTypes
+                gs <- getGoals
+                su <- proveImplication Nothing as cs gs
+                extendSubst su
 
 
-proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
+proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
 proveImplication lnam as ps gs =
   do evars <- varsWithAsmps
      solver <- getSolver
@@ -222,10 +236,10 @@ proveImplicationIO s f varsInEnv ps asmps0 gs0 =
   err us =  Left $ cleanupError
                  $ UnsolvedDelayedCt
                  $ DelayedCt { dctSource = f
-                              , dctForall = ps
-                              , dctAsmps  = asmps0
-                              , dctGoals  = us
-                              }
+                             , dctForall = ps
+                             , dctAsmps  = asmps0
+                             , dctGoals  = us
+                             }
 
 
   asmps1 = concatMap pSplitAnd asmps0