Merge branch 'master' of cryptol into new-eval

cryptol.cabal

@@ -51,7 +51,6 @@ library
                        directory         >= 1.2,
                        filepath          >= 1.3,
                        gitrev            >= 1.0,
-                       generic-trie      >= 0.3.0.1,
                        GraphSCC          >= 1.0.4,
                        heredoc           >= 0.2,
                        monad-control     >= 1.0,
@@ -168,8 +167,6 @@ library
                        GitRev
 
   GHC-options:         -Wall -O2 -fsimpl-tick-factor=140
-  -- the `fsimpl-tick-factor` is needed to finish optimizing the
-  -- generic trie.
   ghc-prof-options:    -fprof-auto -prof
 
   if flag(relocatable)

examples/MiniLock/prim/SHA256.cry

@@ -82,7 +82,6 @@ SHA256MessageSchedule : [16][32] -> [64][32]
 SHA256MessageSchedule M = W where
     W = M # [ s1 (W@(j-2)) + (W@(j-7)) + s0 (W@(j-15)) + (W@(j-16)) | j <- [16 .. 63]:[_][8] ]
 
-
 SHA256Compress : [8][32] -> [64][32] -> [8][32]
 SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4, fs!0 + H@5, gs!0 + H@6, hs!0 + H@7] where
     T1 = [h + S1 e + Ch e f g  + k + w | h <- hs | e <- es | f <- fs | g <- gs | k <- K | w <- W]
@@ -99,7 +98,7 @@ SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4
 /*
  * The SHA256' function hashes a preprocessed sequence of blocks with the
  * compression function.  The SHA256 function hashes a sequence of bytes, and
- * is more likely the function that will be similar to those seein in an
+ * is more likely the function that will be similar to those see in in an
  * implementation to be verified.
  */
 
@@ -108,7 +107,7 @@ SHA256' blocks = hash!0 where
     hash = [H0] # [SHA256Compress h (SHA256MessageSchedule b) | h <- hash | b <- blocks]
 
 SHA256 : {a} (fin a, 64 >= width (8*a)) => [a][8] -> [256]
-SHA256 msg =   join (SHA256' [ split x | x <- preprocess(join msg)])
+SHA256 msg = join (SHA256' [ split x | x <- preprocess(join msg)])
 
 property katsPass = ~zero == [test == kat | (test,kat) <- kats ]
 

src/Cryptol/ModuleSystem/Base.hs

@@ -84,11 +84,6 @@ renameModule :: P.Module PName
              -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)
 renameModule m = do
   (decls,menv) <- importIfaces (map thing (P.mImports m))
-  let (es,ws) = R.checkNamingEnv menv
-
-  renamerWarnings ws
-  unless (null es) (renamerErrors es)
-
   (declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m)
   return (decls,declsEnv,rm)
 

src/Cryptol/ModuleSystem/Renamer.hs

@@ -39,7 +39,7 @@ import Cryptol.Utils.PP
 import qualified Data.Foldable as F
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
-import           MonadLib hiding (mapM)
+import           MonadLib hiding (mapM, mapM_)
 
 import GHC.Generics (Generic)
 import Control.DeepSeq
@@ -77,8 +77,11 @@ data RenamerError
   | InvalidConstraint (Type PName) NameDisp
     -- ^ When it's not possible to produce a Prop from a Type.
 
-  | MalformedConstraint (Located (Type PName)) NameDisp
+  | MalformedBuiltin (Type PName) PName NameDisp
-    -- ^ When a constraint appears within another constraint
+    -- ^ When a builtin type/type-function is used incorrectly.
+
+  | BoundReservedType PName (Maybe Range) Doc NameDisp
+    -- ^ When a builtin type is named in a binder.
     deriving (Show,Generic)
 
 instance NFData RenamerError where rnf = genericRnf
@@ -125,10 +128,15 @@ instance PP RenamerError where
       hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
          4 (fsep [ pp ty, text "is not a valid constraint" ])
 
-    MalformedConstraint t disp -> fixNameDisp disp $
+    MalformedBuiltin ty pn disp -> fixNameDisp disp $
-      hang (text "[error] at" <+> pp (srcRange t))
+      hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
-         4 (sep [ quotes (pp (thing t))
+         4 (fsep [ text "invalid use of built-in type", pp pn
-                , text "is not a valid argument to a constraint" ])
+                 , text "in type", pp ty ])
+
+    BoundReservedType n loc src disp -> fixNameDisp disp $
+      hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) loc)
+         4 (fsep [ text "built-in type", quotes (pp n), text "shadowed in", src ])
+
 
 -- Warnings --------------------------------------------------------------------
 
@@ -267,8 +275,8 @@ shadowNames' check names m = do
   do env <- liftSupply (namingEnv' names)
      RenameM $
        do ro  <- ask
-          sets_ (checkEnv (roDisp ro) check env (roNames ro))
+          env' <- sets (checkEnv (roDisp ro) check env (roNames ro))
-          let ro' = ro { roNames = env `shadowing` roNames ro }
+          let ro' = ro { roNames = env' `shadowing` roNames ro }
           local ro' (unRenameM m)
 
 shadowNamesNS :: BindsNames (InModule env) => env -> RenameM a -> RenameM a
@@ -280,25 +288,30 @@ shadowNamesNS names m =
 -- | Generate warnings when the left environment shadows things defined in
 -- the right.  Additionally, generate errors when two names overlap in the
 -- left environment.
-checkEnv :: NameDisp -> EnvCheck -> NamingEnv -> NamingEnv -> RW -> RW
+checkEnv :: NameDisp -> EnvCheck -> NamingEnv -> NamingEnv -> RW -> (NamingEnv,RW)
-checkEnv _    CheckNone _ _ rw = rw
+checkEnv disp check l r rw
-checkEnv disp check     l r rw = rw''
+  | check == CheckNone = (l',rw)
+  | otherwise          = (l',rw'')
 
   where
 
-  rw'  = Map.foldlWithKey (step neExprs) rw (neExprs l)
+  l' = l { neExprs = es, neTypes = ts }
-  rw'' = Map.foldlWithKey (step neTypes) rw' (neTypes l)
 
-  step prj acc k ns = acc
+  (rw',es)  = Map.mapAccumWithKey (step neExprs) rw  (neExprs l)
-    { rwWarnings =
+  (rw'',ts) = Map.mapAccumWithKey (step neTypes) rw' (neTypes l)
-        if check == CheckAll
-           then case Map.lookup k (prj r) of
-                  Nothing -> rwWarnings acc
-                  Just os -> rwWarnings acc Seq.|> SymbolShadowed (head ns) os disp
 
-           else rwWarnings acc
+  step prj acc k ns = (acc', [head ns])
-    , rwErrors   = rwErrors acc Seq.>< containsOverlap disp ns
+    where
-    }
+    acc' = acc
+      { rwWarnings =
+          if check == CheckAll
+             then case Map.lookup k (prj r) of
+                    Nothing -> rwWarnings acc
+                    Just os -> rwWarnings acc Seq.|> SymbolShadowed (head ns) os disp
+
+             else rwWarnings acc
+      , rwErrors   = rwErrors acc Seq.>< containsOverlap disp ns
+      }
 
 -- | Check the RHS of a single name rewrite for conflicting sources.
 containsOverlap :: NameDisp -> [Name] -> Seq.Seq RenamerError
@@ -446,7 +459,12 @@ instance Rename Schema where
 -- into scope.
 renameSchema :: Schema PName -> RenameM (NamingEnv,Schema Name)
 renameSchema (Forall ps p ty loc) =
-  do env <- liftSupply (namingEnv' ps)
+  do -- check that the parameters don't shadow any built-in types
+     let reserved = filter (isReserved . getIdent . tpName) ps
+         mkErr tp = BoundReservedType (tpName tp) (tpRange tp) (text "schema")
+     unless (null reserved) (mapM_ (record . mkErr) reserved)
+
+     env <- liftSupply (namingEnv' ps)
      s'  <- shadowNames env $ Forall <$> traverse rename ps
                                      <*> traverse rename p
                                      <*> rename ty
@@ -494,6 +512,33 @@ translateProp ty = go ty
          CType <$> rename t
 
 
+
+-- | Fixed names for type functions and built-in types.
+reservedTypeNames :: Map.Map Ident ([Type Name] -> Maybe (Type Name))
+reservedTypeNames  = Map.fromList
+  [ (packIdent "inf", typeConst TInf)
+  , (packIdent "Bit", typeConst TBit)
+
+  , (packIdent "min",              arity 2 TCMin)
+  , (packIdent "max",              arity 2 TCMax)
+  , (packIdent "lengthFromThen",   arity 3 TCLenFromThen)
+  , (packIdent "lengthFromThenTo", arity 3 TCLenFromThenTo)
+  , (packIdent "width",            arity 1 TCWidth)
+  ]
+
+  where
+  typeConst c ps =
+    do guard (null ps)
+       return c
+
+  arity n op ps =
+    do guard (length ps == n)
+       return (TApp op ps)
+
+-- | Check to see if this identifier is a reserved type/type-function.
+isReserved :: Ident -> Bool
+isReserved k = Map.member k reservedTypeNames
+
 -- | Resolve fixity, then rename the resulting type.
 instance Rename Type where
   rename ty0 = go =<< resolveTypeFixity ty0
@@ -507,17 +552,12 @@ instance Rename Type where
     go  TInf         = return TInf
 
     go (TUser pn ps)
-      | i == packIdent "inf", null ps     = return TInf
+      | Just mk <- Map.lookup (getIdent pn) reservedTypeNames =
-      | i == packIdent "Bit", null ps     = return TBit
+        do ps' <- traverse go ps
-
+           case mk ps' of
-      | i == packIdent "min"              = TApp TCMin           <$> traverse go ps
+             Just ty -> return ty
-      | i == packIdent "max"              = TApp TCMax           <$> traverse go ps
+             Nothing -> do record (MalformedBuiltin ty0 pn)
-      | i == packIdent "lengthFromThen"   = TApp TCLenFromThen   <$> traverse go ps
+                           TUser <$> renameType pn <*> pure ps'
-      | i == packIdent "lengthFromThenTo" = TApp TCLenFromThenTo <$> traverse go ps
-      | i == packIdent "width"            = TApp TCWidth         <$> traverse go ps
-
-      where
-      i = getIdent pn
 
     go (TUser qn ps)   = TUser    <$> renameType qn <*> traverse go ps
     go (TApp f xs)     = TApp f   <$> traverse go xs
@@ -670,7 +710,9 @@ instance Rename Expr where
     EInfFrom a b  -> EInfFrom<$> rename a  <*> traverse rename b
     EComp e' bs   -> do arms' <- traverse renameArm bs
                         let (envs,bs') = unzip arms'
-                        shadowNames envs (EComp <$> rename e' <*> pure bs')
+                        -- NOTE: renameArm will generate shadowing warnings; we only
+                        -- need to check for repeated names across multiple arms
+                        shadowNames' CheckOverlap envs (EComp <$> rename e' <*> pure bs')
     EApp f x      -> EApp    <$> rename f  <*> rename x
     EAppT f ti    -> EAppT   <$> rename f  <*> traverse rename ti
     EIf b t f     -> EIf     <$> rename b  <*> rename t  <*> rename f
@@ -732,7 +774,9 @@ renameArm :: [Match PName] -> RenameM (NamingEnv,[Match Name])
 
 renameArm (m:ms) =
   do (me,m') <- renameMatch m
-     shadowNames me $
+     -- NOTE: renameMatch will generate warnings, so we don't
+     -- need to duplicate them here
+     shadowNames' CheckNone me $
        do (env,rest) <- renameArm ms
 
           -- NOTE: the inner environment shadows the outer one, for examples
@@ -774,22 +818,30 @@ renamePats  = loop
     [] -> return (mempty, [])
 
 patternEnv :: Pattern PName -> RenameM NamingEnv
-patternEnv p0 = go p0
+patternEnv  = go
   where
   go (PVar Located { .. }) =
     do n <- liftSupply (mkParameter (getIdent thing) srcRange)
        return (singletonE thing n)
 
   go PWild            = return mempty
-  go (PTuple ps)      = foldMap go ps
+  go (PTuple ps)      = bindVars ps
-  go (PRecord fs)     = foldMap (foldMap go) fs
+  go (PRecord fs)     = bindVars (map value fs)
   go (PList ps)       = foldMap go ps
   go (PTyped p ty)    = go p `mappend` typeEnv ty
   go (PSplit a b)     = go a `mappend` go b
   go (PLocated p loc) = withLoc loc (go p)
 
-  typeEnv (TFun a b) = typeEnv a `mappend` typeEnv b
+  bindVars []     = return mempty
-  typeEnv (TSeq a b) = typeEnv a `mappend` typeEnv b
+  bindVars (p:ps) =
+    do env <- go p
+       shadowNames env $
+         do rest <- bindVars ps
+            return (env `mappend` rest)
+
+
+  typeEnv (TFun a b) = bindTypes [a,b]
+  typeEnv (TSeq a b) = bindTypes [a,b]
 
   typeEnv TBit       = return mempty
   typeEnv TNum{}     = return mempty
@@ -801,7 +853,7 @@ patternEnv p0 = go p0
        case mb of
 
          -- The type is already bound, don't introduce anything.
-         Just _ -> foldMap typeEnv ps
+         Just _ -> bindTypes ps
 
          Nothing
            -- The type isn't bound, and has no parameters, so it names a portion
@@ -819,13 +871,21 @@ patternEnv p0 = go p0
                 n   <- liftSupply (mkParameter (getIdent pn) loc)
                 return (singletonT pn n)
 
-  typeEnv (TApp _ ts)       = foldMap typeEnv ts
+  typeEnv (TApp _ ts)       = bindTypes ts
-  typeEnv (TRecord fs)      = foldMap (foldMap typeEnv) fs
+  typeEnv (TRecord fs)      = bindTypes (map value fs)
-  typeEnv (TTuple ts)       = foldMap typeEnv ts
+  typeEnv (TTuple ts)       = bindTypes ts
   typeEnv TWild             = return mempty
   typeEnv (TLocated ty loc) = withLoc loc (typeEnv ty)
   typeEnv (TParens ty)      = typeEnv ty
-  typeEnv (TInfix a _ _ b)  = typeEnv a `mappend` typeEnv b
+  typeEnv (TInfix a _ _ b)  = bindTypes [a,b]
+
+  bindTypes [] = return mempty
+  bindTypes (t:ts) =
+    do env' <- typeEnv t
+       shadowNames env' $
+         do res <- bindTypes ts
+            return (env' `mappend` res)
+
 
 instance Rename Match where
   rename m = case m of
@@ -834,9 +894,12 @@ instance Rename Match where
 
 instance Rename TySyn where
   rename (TySyn n ps ty) =
-     shadowNames ps $ TySyn <$> rnLocated renameType n
+    do when (isReserved (getIdent (thing n)))
-                            <*> traverse rename ps
+            (record (BoundReservedType (thing n) (getLoc n) (text "type synonym")))
-                            <*> rename ty
+
+       shadowNames ps $ TySyn <$> rnLocated renameType n
+                              <*> traverse rename ps
+                              <*> rename ty
 
 
 -- Utilities -------------------------------------------------------------------

src/Cryptol/REPL/Command.hs

@@ -401,7 +401,7 @@ cmdProveSat isSat "" =
                      then rPutStr $ ":sat "   ++ str ++ "\n\t"
                      else rPutStr $ ":prove " ++ str ++ "\n\t"
                   cmdProveSat isSat str
-cmdProveSat isSat expr = do
+cmdProveSat isSat str = do
   let cexStr | isSat = "satisfying assignment"
              | otherwise = "counterexample"
   EnvString proverName <- getUser "prover"
@@ -409,7 +409,7 @@ cmdProveSat isSat expr = do
   let mfile = if fileName == "-" then Nothing else Just fileName
   case proverName of
     "offline" -> do
-      result <- offlineProveSat isSat expr mfile
+      result <- offlineProveSat isSat str mfile
       case result of
         Left msg -> rPutStrLn msg
         Right smtlib -> do
@@ -425,7 +425,7 @@ cmdProveSat isSat expr = do
             Just path -> io $ writeFile path smtlib
             Nothing -> rPutStr smtlib
     _ -> do
-      result <- onlineProveSat isSat expr mfile
+      result <- onlineProveSat isSat str mfile
       ppOpts <- getPPValOpts
       case result of
         Symbolic.EmptyResult         ->
@@ -439,7 +439,7 @@ cmdProveSat isSat expr = do
           let tess = map (map $ \(t,e,_) -> (t,e)) tevss
               vss  = map (map $ \(_,_,v) -> v)     tevss
               ppvs vs = do
-                parseExpr <- replParseExpr expr
+                parseExpr <- replParseExpr str
                 docs <- mapM (io . E.runEval . E.ppValue ppOpts) vs
                 let -- function application has precedence 3
                     doc = ppPrec 3 parseExpr
@@ -549,13 +549,14 @@ typeOfCmd :: String -> REPL ()
 typeOfCmd str = do
 
   expr         <- replParseExpr str
-  (re,def,sig) <- replCheckExpr expr
+  (_re,def,sig) <- replCheckExpr expr
 
   -- XXX need more warnings from the module system
   --io (mapM_ printWarning ws)
   whenDebug (rPutStrLn (dump def))
   (_,_,names) <- getFocusedEnv
-  rPrint $ runDoc names $ pp re <+> text ":" <+> pp sig
+  -- type annotation ':' has precedence 2
+  rPrint $ runDoc names $ ppPrec 2 expr <+> text ":" <+> pp sig
 
 readFileCmd :: FilePath -> REPL ()
 readFileCmd fp = do
@@ -849,7 +850,7 @@ moduleCmdResult (res,ws0) = do
           ys -> Just (M.TypeCheckWarnings ys)
       filterDefaults w = Just w
 
-      isShadowWarn (M.SymbolShadowed _ _ _) = True
+      isShadowWarn (M.SymbolShadowed {}) = True
 
       filterShadowing w | warnShadowing = Just w
       filterShadowing (M.RenamerWarnings xs) =

src/Cryptol/TypeCheck/Depends.hs

@@ -29,7 +29,7 @@ import qualified Data.Set as Set
 data TyDecl = TS (P.TySyn Name) | NT (P.Newtype Name)
 
 -- | Check for duplicate and recursive type synonyms.
--- Returns the type-synonyms in dependecy order.
+-- Returns the type-synonyms in dependency order.
 orderTyDecls :: [TyDecl] -> InferM [TyDecl]
 orderTyDecls ts =
   do vs <- getTVars

src/Cryptol/TypeCheck/Solver/InfNat.hs

@@ -16,15 +16,12 @@ module Cryptol.TypeCheck.Solver.InfNat where
 import Data.Bits
 import Cryptol.Utils.Panic
 
-import Data.GenericTrie(TrieKey)
 import GHC.Generics(Generic)
 
 -- | Natural numbers with an infinity element
 data Nat' = Nat Integer | Inf
             deriving (Show,Eq,Ord,Generic)
 
-instance TrieKey Nat'
-
 fromNat :: Nat' -> Maybe Integer
 fromNat n' =
   case n' of

tests/issues/issue256.icry.stdout

@@ -1,4 +1,4 @@
 Loading module Cryptol
-[True] == [False] : Bit
+([True] == [False]) : Bit
-\x -> True != x : Bit -> Bit
+(\x -> True != x) : Bit -> Bit
-\x -> True && x : Bit -> Bit
+(\x -> True && x) : Bit -> Bit

tests/issues/issue304.cry

@@ -0,0 +1,5 @@
+x : [64]
+x = 10
+
+a : [16]
+a # b = x

tests/issues/issue304.icry

@@ -0,0 +1,4 @@
+:l issue304.cry
+:t x
+:t a
+:t b

tests/issues/issue304.icry.stdout

@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+x : [64]
+a : [16]
+b : [48]

tests/issues/issue335.icry

@@ -0,0 +1,2 @@
+:t \ (x: (Bit,Bit)) -> x.0
+:t \ (x:a) (y:a) -> x

tests/issues/issue335.icry.stdout

@@ -0,0 +1,3 @@
+Loading module Cryptol
+(\(x : (Bit, Bit)) -> x.0) : (Bit, Bit) -> Bit
+(\(x : a) (y : a) -> x) : {a} a -> a -> a

tests/renamer/comp02.icry.stdout

@@ -6,7 +6,3 @@ Loading module comp02
     Overlapping symbols defined:
     (at ./comp02.cry:4:12--4:13, a)
     (at ./comp02.cry:5:12--5:13, a)
-[error] at ./comp02.cry:4:8--4:9
-    Multiple definitions for symbol: a
-    (at ./comp02.cry:4:12--4:13, a)
-    (at ./comp02.cry:5:12--5:13, a)