cryptol 2.7.0 → 2.8.0

raw patch · 59 files changed

+1884/−1534 lines, 59 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +44/−0
• LICENSE +1/−1
• cryptol.cabal +5/−5
• cryptol/Main.hs +2/−1
• cryptol/REPL/Haskeline.hs +3/−8
• lib/Cryptol.cry +161/−20
• src/Cryptol/Eval.hs +8/−5
• src/Cryptol/Eval/Monad.hs +18/−5
• src/Cryptol/Eval/Reference.lhs +17/−0
• src/Cryptol/Eval/Type.hs +24/−8
• src/Cryptol/Eval/Value.hs +7/−3
• src/Cryptol/ModuleSystem.hs +5/−5
• src/Cryptol/ModuleSystem/Base.hs +43/−23
• src/Cryptol/ModuleSystem/Env.hs +41/−7
• src/Cryptol/ModuleSystem/Exports.hs +1/−0
• src/Cryptol/ModuleSystem/InstantiateModule.hs +14/−2
• src/Cryptol/ModuleSystem/Interface.hs +14/−4
• src/Cryptol/ModuleSystem/Monad.hs +21/−15
• src/Cryptol/ModuleSystem/NamingEnv.hs +22/−39
• src/Cryptol/ModuleSystem/Renamer.hs +100/−170
• src/Cryptol/Parser.y +125/−98
• src/Cryptol/Parser/AST.hs +95/−120
• src/Cryptol/Parser/Fixity.hs +5/−1
• src/Cryptol/Parser/Lexer.x +6/−1
• src/Cryptol/Parser/LexerUtils.hs +5/−4
• src/Cryptol/Parser/Names.hs +52/−99
• src/Cryptol/Parser/NoInclude.hs +1/−0
• src/Cryptol/Parser/NoPat.hs +120/−54
• src/Cryptol/Parser/ParserUtils.hs +137/−52
• src/Cryptol/Parser/Selector.hs +1/−3
• src/Cryptol/Parser/Unlit.hs +9/−4
• src/Cryptol/Parser/Utils.hs +5/−6
• src/Cryptol/Prelude.hs +5/−18
• src/Cryptol/Prims/Eval.hs +26/−12
• src/Cryptol/Prims/Syntax.hs +0/−444
• src/Cryptol/REPL/Command.hs +95/−32
• src/Cryptol/REPL/Monad.hs +16/−9
• src/Cryptol/Symbolic.hs +1/−0
• src/Cryptol/Symbolic/Prims.hs +3/−6
• src/Cryptol/Symbolic/Value.hs +1/−1
• src/Cryptol/Testing/Concrete.hs +2/−0
• src/Cryptol/Testing/Random.hs +20/−21
• src/Cryptol/Transform/Specialize.hs +0/−14
• src/Cryptol/TypeCheck/AST.hs +1/−1
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +5/−4
• src/Cryptol/TypeCheck/Depends.hs +46/−19
• src/Cryptol/TypeCheck/Error.hs +5/−5
• src/Cryptol/TypeCheck/Infer.hs +45/−37
• src/Cryptol/TypeCheck/InferTypes.hs +1/−8
• src/Cryptol/TypeCheck/Instantiate.hs +51/−24
• src/Cryptol/TypeCheck/Kind.hs +40/−44
• src/Cryptol/TypeCheck/Monad.hs +25/−0
• src/Cryptol/TypeCheck/Sanity.hs +2/−2
• src/Cryptol/TypeCheck/Solve.hs +0/−43
• src/Cryptol/TypeCheck/Solver/Class.hs +6/−1
• src/Cryptol/TypeCheck/Solver/Selector.hs +1/−1
• src/Cryptol/TypeCheck/TCon.hs +314/−0
• src/Cryptol/TypeCheck/Type.hs +51/−22
• src/Cryptol/Utils/PP.hs +10/−3

@@ -1,3 +1,47 @@+# 2.8.0 (September 4, 2019)++## New features++* Added support for indexing on the left-hand sides of declarations,+  record field constructors, and record updaters (issue #577). This+  builds on a new primitive function called `generate`, where the new+  syntax `x @ i = e` is sugar for `x = generate (\i -> e)`.++* Added support for element type ascriptions on sequence enumerations.+  The syntax `[a,b..c:t]` indicates that the elements should be of type+  `t`.++* Added support for wildcards in sequence enumerations. For example, the+  syntax `[1 .. _] : [3][8]` yields `[0x01, 0x02, 0x03]`. It can also be+  used polymorphically. For example, the most general type of `[1 .. _]`+  is `{n, a} (n >= 1, Literal n a, fin n) => [n]a`++* Changed the syntax of type signatures to allow multiple constraint+  arrows in type schemas (issue #599). The following are now equivalent:++        f : {a} (fin a, a >= 1) => [a] -> [a]++        f : {a} (fin a) => (a >= 1) => [a] -> [a]+        +* Added a mechanism for user-defined type constraint operators, and use+  this to define the new type constraint synonyms (<) and (>) (issues+  #400, #618).++* Added support for primitive type declarations. The prelude now uses+  this mechanism to declare all of the basic types.++* Added support for Haskell-style "block arguments", reducing the need+  for parentheses in some cases. For example, `generate (\i -> i +1)`+  can now be written `generate \i -> i + 1`.++* Improved shadowing errors (part of the fix for issue #569).++## Bug fixes++* Closed many issues, including #265, #367, #437, #508, #522, #549,+  #557, #559, #569, #578, #590, #595, #596, #601, #607, #608, #610,+  #615, #621, and #636.+ # 2.7.0 (April 30, 2019)  ## New features

@@ -1,4 +1,4 @@-Copyright (c) 2013-2018 Galois Inc.+Copyright (c) 2013-2019 Galois Inc. All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -1,5 +1,5 @@ Name:                cryptol-Version:             2.7.0+Version:             2.8.0 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD3@@ -8,7 +8,7 @@ Maintainer:          cryptol@galois.com Homepage:            http://www.cryptol.net/ Bug-reports:         https://github.com/GaloisInc/cryptol/issues-Copyright:           2013-2018 Galois Inc.+Copyright:           2013-2019 Galois Inc. Category:            Language Build-type:          Simple Cabal-version:       1.18@@ -25,7 +25,7 @@ source-repository this   type:     git   location: https://github.com/GaloisInc/cryptol.git-  tag:      2.7.0+  tag:      2.8.0  flag static   default: False@@ -74,8 +74,7 @@   Build-tools:         alex, happy   hs-source-dirs:      src -  Exposed-modules:     Cryptol.Prims.Syntax,-                       Cryptol.Prims.Eval,+  Exposed-modules:     Cryptol.Prims.Eval,                         Cryptol.Parser,                        Cryptol.Parser.Lexer,@@ -113,6 +112,7 @@                         Cryptol.TypeCheck,                        Cryptol.TypeCheck.Type,+                       Cryptol.TypeCheck.TCon,                        Cryptol.TypeCheck.TypePat,                        Cryptol.TypeCheck.SimpType,                        Cryptol.TypeCheck.AST,

@@ -17,6 +17,7 @@ import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,                    io,prependSearchPath,setSearchPath) import qualified Cryptol.REPL.Monad as REPL+import Cryptol.ModuleSystem.Env(ModulePath(..))  import REPL.Haskeline import REPL.Logo@@ -276,6 +277,6 @@              REPL.setEditPath l              REPL.setLoadedMod REPL.LoadedModule                { REPL.lName = Nothing-               , REPL.lPath = l+               , REPL.lPath = InFile l                }     _   -> io $ putStrLn "Only one file may be loaded at the command line."

@@ -12,13 +12,12 @@  module REPL.Haskeline where -import           Cryptol.Prims.Syntax (primTyList, primTyIdent) import           Cryptol.REPL.Command import           Cryptol.REPL.Monad import           Cryptol.REPL.Trie import           Cryptol.Utils.PP import           Cryptol.Utils.Logger(stdoutLogger)-import           Cryptol.Utils.Ident(modNameToText, interactiveName, isInfixIdent)+import           Cryptol.Utils.Ident(modNameToText, interactiveName)  import qualified Control.Exception as X import           Control.Monad (guard, join)@@ -267,9 +266,8 @@ completeHelp (l, _) = do   ns1 <- getExprNames   ns2 <- getTypeNames-  let ns3 = primTyNames-  let ns4 = concatMap cNames (nub (findCommand ":"))-  let ns = Set.toAscList (Set.fromList (ns1 ++ ns2 ++ ns3)) ++ ns4+  let ns3 = concatMap cNames (nub (findCommand ":"))+  let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3   let n    = reverse l   case break isSpace n of     (":set", _ : n') ->@@ -280,9 +278,6 @@       do let vars = filter (n `isPrefixOf`) ns          return (l, map (nameComp n) vars) -primTyNames :: [String]-primTyNames = map (showIdent . primTyIdent) primTyList-  where showIdent i = show (optParens (isInfixIdent i) (pp i))  -- | Complete a name from the list of loaded modules. completeModName :: CompletionFunc REPL

@@ -27,50 +27,178 @@ infixr 60 # infixl 70 <<, <<<, >>, >>>, >>$ infixl 80 +, --infixl 90 *, /, %, /$, %$+infixl 90 *, /, %, /$, %$, %^, /^ infixr 95 ^^ infixl 100 @, @@, !, !! +// -----------------------------------------------------------------------------++/** A numeric type representing infinity. */+primitive type inf : #++/** The type of boolean values. */+primitive type Bit : *++/** The type of unbounded integers. */+primitive type Integer : *++/** 'Z n' is the type of integers, modulo 'n'. */+primitive type {n : #} (fin n, n >= 1) => Z n : *++++/** Assert that two numeric types are equal. */+primitive type (==) : # -> # -> Prop++/** Assert that two numeric types are different. */+primitive type (!=) : # -> # -> Prop++/** Assert that the first numeric type is larger than, or equal to the second.*/+primitive type (>=) : # -> # -> Prop++/** Assert that a numeric type is a proper natural number (not 'inf'). */+primitive type fin : * -> Prop++/** Value types that have a notion of 'zero'. */+primitive type Zero : * -> Prop++/** Value types that support logical operations. */+primitive type Logic : * -> Prop++/** Value types that support arithmetic. */+primitive type Arith : * -> Prop++/** Value types that support unsigned comparisons. */+primitive type Cmp : * -> Prop++/** Value types that support signed comparisons. */+primitive type SignedCmp : * -> Prop++/** 'Literal n a' asserts that type 'a' contains the number 'n'. */+primitive type Literal : # -> * -> Prop++++/** Add numeric types. */+primitive type (+) : # -> # -> #++/** Subtract numeric types. */+primitive type+  {m : #, n : # }+  (fin n, m >= n) =>+  m - n : #++/** Multiply numeric types. */+primitive type (*) : # -> # -> #++/** Divide numeric types, rounding down. */+primitive type+  { m : #, n : # }+  (fin m, n >= 1) =>+  m / n : #++/** Remainder of numeric type division. */+primitive type+  { m : #, n : # }+  (fin m, n >= 1) =>+  m % n : #++/** Exponentiate numeric types. */+primitive type (^^) : # -> # -> #++/** The number of bits required to represent the value of a numeric type. */+primitive type width : # -> #++/** The smaller of two numeric types. */+primitive type min : # -> # -> #++/** The larger of two numeric types. */+primitive type max : # -> # -> #++/** Divide numeric types, rounding up. */+primitive type+  { m : #, n : # }+  (fin m, fin n, n >= 1) =>+  m /^ n : #++/** How much we need to add to make a proper multiple of the second argument. */+primitive type+  { m : #, n : # }+  (fin m, fin n, n >= 1) =>+  m %^ n : #++/** The length of an enumeration. */+primitive type+  { start : #, next : #, last : # }+  (fin start, fin next, fin last, start != next) =>+  lengthFromThenTo start next last : #+++++// -----------------------------------------------------------------------------+ /**+ * Assert that the first numeric type is less than or equal to the second.+ */+type constraint i <= j = (j >= i)++/**+ * Assert that the first numeric type is greater than the second.+ */+type constraint i > j = i >= j + 1++/**+ * Assert that the first numeric type is less than the second.+ */+type constraint i < j = j >= i + 1++/**  * Add two values.- *  * For words, addition uses modulo arithmetic.+ *  * For type [n], addition is modulo 2^^n.  *  * Structured values are added element-wise.  */ primitive (+) : {a} (Arith a) => a -> a -> a  /**- * For words, subtraction uses modulo arithmetic.- * Structured values are subtracted element-wise. Defined as:- * a - b = a + negate b- * See also: `negate'.+ * Subtract two values.+ *  * For type [n], subtraction is modulo 2^^n.+ *  * Structured values are subtracted element-wise.+ *  * Satisfies 'a - b = a + negate b'.+ * See also: 'negate'.  */ primitive (-) : {a} (Arith a) => a -> a -> a  /**- * For words, multiplies two words, modulus 2^^a.- * Structured values are multiplied element-wise.+ * Multiply two values.+ *  * For type [n], multiplication is modulo 2^^n.+ *  * Structured values are multiplied element-wise.  */ primitive (*) : {a} (Arith a) => a -> a -> a  /**- * For words, divides two words, modulus 2^^a.- * Structured values are divided element-wise.+ * Divide two values, rounding down.+ *  * For type [n], the arguments are treated as unsigned.+ *  * Structured values are divided element-wise.+ *  * Division by zero is undefined.  */ primitive (/) : {a} (Arith a) => a -> a -> a  /**- * For words, takes the modulus of two words, modulus 2^^a.- * Over structured values, operates element-wise.- * Be careful, as this will often give unexpected results due to interaction of- * the two moduli.+ * Compute the remainder from dividing two values.+ *  * For type [n], the arguments are treated as unsigned.+ *  * Structured values are combined element-wise.+ *  * Remainder of division by zero is undefined.+ *  * Satisfies 'x % y == x - (x / y) * y'.  */ primitive (%) : {a} (Arith a) => a -> a -> a  /**- * For words, takes the exponent of two words, modulus 2^^a.- * Over structured values, operates element-wise.- * Be careful, due to its fast-growing nature, exponentiation is prone to- * interacting poorly with defaulting.+ * Compute the exponentiation of two values.+ *  * For type [n], the exponent is treated as unsigned,+ *    and the result is reduced modulo 2^^n.+ *  * For type Integer, negative powers are undefined.+ *  * Structured values are combined element-wise.  */ primitive (^^) : {a} (Arith a) => a -> a -> a @@ -96,9 +224,11 @@ primitive False : Bit  /**- * Returns the twos complement of its argument.+ * Returns the two's complement of its argument.  * Over structured values, operates element-wise.- * negate a = ~a + 1+ * The prefix notation '- x' is syntactic sugar+ * for 'negate x'.+ * Satisfies 'negate a = ~a + 1'.  */ primitive negate : {a} (Arith a) => a -> a @@ -483,6 +613,17 @@  * '[x,y...]' is syntactic sugar for 'infFromThen x y'.  */ primitive infFromThen : {a} (Arith a) => a -> a -> [inf]a++/**+ * Produce a sequence using a generating function.+ * Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.+ *+ * Declarations of the form 'x @ i = e' are syntactic sugar for+ * 'x = generate (\i -> e)'.+ */+generate : {n, ix, a}+  (fin ix, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a+generate f = [ f i | i <- [0 .. n-1] ]  primitive error : {a, len} (fin len) => [len][8] -> a 

@@ -373,7 +373,9 @@                 | (f,t) <- fs                 ] +      TVAbstract {} -> x + declHole :: Decl          -> Eval (Name, Schema, Eval (GenValue b w i), Eval (GenValue b w i) -> Eval ()) declHole d =@@ -403,7 +405,10 @@          -> Eval (GenEvalEnv b w i) evalDecl renv env d =   case dDefinition d of-    DPrim   -> return $ bindVarDirect (dName d) (evalPrim d) env+    DPrim   -> case evalPrim d of+                 Just v  -> pure (bindVarDirect (dName d) v env)+                 Nothing -> bindVar (dName d) (cryNoPrimError (dName d)) env+     DExpr e -> bindVar (dName d) (evalExpr renv e) env  @@ -456,7 +461,7 @@   case x of     TupleSel n _  -> setTuple n     RecordSel n _ -> setRecord n-    ListSel ix _  -> setList (fromIntegral ix)+    ListSel ix _  -> setList (toInteger ix)    where   bad msg =@@ -624,7 +629,5 @@     where       f env =           case dDefinition d of-            -- Primitives here should never happen, I think...-            --    perhaps this should be converted to an error.-            DPrim   -> return $ evalPrim d+            DPrim   -> evalPanic "evalMatch" ["Unexpected local primitive"]             DExpr e -> evalExpr env e

@@ -32,6 +32,7 @@ , wordTooWide , cryUserError , cryLoopError+, cryNoPrimError , invalidIndex ) where @@ -47,7 +48,7 @@ import Cryptol.Utils.Panic import Cryptol.Utils.PP import Cryptol.Utils.Logger(Logger)-import Cryptol.TypeCheck.AST(Type)+import Cryptol.TypeCheck.AST(Type,Name)  -- | A computation that returns an already-evaluated value. ready :: a -> Eval a@@ -75,7 +76,9 @@ data ThunkState a   = Unforced        -- ^ This thunk has not yet been forced   | BlackHole       -- ^ This thunk is currently being evaluated-  | Forced !a       -- ^ This thunk has previously been forced, and has the given value+  | Forced !(Either EvalError a)+    -- ^ This thunk has previously been forced,+    -- and has the given value, or evaluation resulted in an error.   -- | Access the evaluation options.@@ -126,15 +129,20 @@ unDelay retry r x = do   rval <- io $ readIORef r   case rval of-    Forced val -> return val+    Forced val -> io (toVal val)     BlackHole  ->       retry     Unforced -> io $ do       writeIORef r BlackHole-      val <- x+      val <- X.try x       writeIORef r (Forced val)-      return val+      toVal val +  where+  toVal mbV = case mbV of+                Right a -> pure a+                Left e  -> X.throwIO e+ -- | Execute the given evaluation action. runEval :: EvalOpts -> Eval a -> IO a runEval _ (Ready a) = return a@@ -196,6 +204,7 @@   | WordTooWide Integer           -- ^ Bitvector too large   | UserError String              -- ^ Call to the Cryptol @error@ primitive   | LoopError String              -- ^ Detectable nontermination+  | NoPrim Name                   -- ^ Primitive with no implementation     deriving (Typeable,Show)  instance PP EvalError where@@ -209,6 +218,7 @@       text "word too wide for memory:" <+> integer w <+> text "bits"     UserError x -> text "Run-time error:" <+> text x     LoopError x -> text "<<loop>>" <+> text x+    NoPrim x -> text "unimplemented primitive:" <+> pp x  instance X.Exception EvalError @@ -237,6 +247,9 @@ -- | For the Cryptol @error@ function. cryUserError :: String -> Eval a cryUserError msg = io (X.throwIO (UserError msg))++cryNoPrimError :: Name -> Eval a+cryNoPrimError x = io (X.throwIO (NoPrim x))  -- | For cases where we can detect tight loops. cryLoopError :: String -> Eval a

@@ -176,6 +176,7 @@ >         TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val))) >         TVRec fields -> VRecord [ (f, go fty (lookupRecord f val)) | (f, fty) <- fields ] >         TVFun _ bty  -> VFun (\v -> go bty (fromVFun val v))+>         TVAbstract {} -> val > > copyStream :: [a] -> [a] > copyStream xs = head xs : copyStream (tail xs)@@ -755,6 +756,8 @@ >     go (TVTuple tys)  = VTuple (map go tys) >     go (TVRec fields) = VRecord [ (f, go fty) | (f, fty) <- fields ] >     go (TVFun _ bty)  = VFun (\_ -> go bty)+>     go (TVAbstract {}) =+>        evalPanic "logicUnary" ["Abstract type not in `Logic`"] > > logicUnary :: (Bool -> Bool) -> TValue -> Value -> Value > logicUnary op = go@@ -770,6 +773,8 @@ >         TVTuple etys -> VTuple (zipWith go etys (fromVTuple val)) >         TVRec fields -> VRecord [ (f, go fty (lookupRecord f val)) | (f, fty) <- fields ] >         TVFun _ bty  -> VFun (\v -> go bty (fromVFun val v))+>         TVAbstract {} ->+>           evalPanic "logicUnary" ["Abstract type not in `Logic`"] > > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value > logicBinary op = go@@ -786,6 +791,8 @@ >         TVRec fields -> VRecord [ (f, go fty (lookupRecord f l) (lookupRecord f r)) >                                 | (f, fty) <- fields ] >         TVFun _ bty  -> VFun (\v -> go bty (fromVFun l v) (fromVFun r v))+>         TVAbstract {} ->+>           evalPanic "logicBinary" ["Abstract type not in `Logic`"]   Arithmetic@@ -823,6 +830,8 @@ >           VTuple (map go tys) >         TVRec fs -> >           VRecord [ (f, go fty) | (f, fty) <- fs ]+>         TVAbstract {} ->+>           evalPanic "arithNullary" ["Absrat type not in `Arith`"] > > arithUnary :: (Integer -> Either EvalError Integer) >            -> TValue -> Value -> Value@@ -854,6 +863,8 @@ >           VTuple (zipWith go tys (fromVTuple val)) >         TVRec fs -> >           VRecord [ (f, go fty (lookupRecord f val)) | (f, fty) <- fs ]+>         TVAbstract {} ->+>           evalPanic "arithUnary" ["Absrat type not in `Arith`"] > > arithBinary :: (Integer -> Integer -> Either EvalError Integer) >             -> TValue -> Value -> Value -> Value@@ -906,6 +917,8 @@ >           VTuple (zipWith3 go tys (fromVTuple l) (fromVTuple r)) >         TVRec fs -> >           VRecord [ (f, go fty (lookupRecord f l) (lookupRecord f r)) | (f, fty) <- fs ]+>         TVAbstract {} ->+>           evalPanic "arithBinary" ["Abstract type not in class `Arith`"]  Signed bitvector division (`/$`) and remainder (`%$`) are defined so that division rounds toward zero, and the remainder `x %$ y` has the@@ -968,6 +981,8 @@ >           ls     = map snd (sortBy (comparing fst) (fromVRecord l)) >           rs     = map snd (sortBy (comparing fst) (fromVRecord r)) >        in lexList (zipWith3 lexCompare tys ls rs)+>     TVAbstract {} ->+>       evalPanic "lexCompare" ["Abstract type not in `Cmp`"] > > lexList :: [Either EvalError Ordering] -> Either EvalError Ordering > lexList [] = Right EQ@@ -1017,6 +1032,8 @@ >           ls     = map snd (sortBy (comparing fst) (fromVRecord l)) >           rs     = map snd (sortBy (comparing fst) (fromVRecord r)) >        in lexList (zipWith3 lexSignedCompare tys ls rs)+>     TVAbstract {} ->+>       evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]   Sequences

@@ -27,14 +27,15 @@ -- | An evaluated type of kind *. -- These types do not contain type variables, type synonyms, or type functions. data TValue-  = TVBit                    -- ^ @ Bit @-  | TVInteger                -- ^ @ Integer @-  | TVIntMod Integer         -- ^ @ Z n @-  | TVSeq Integer TValue     -- ^ @ [n]a @-  | TVStream TValue          -- ^ @ [inf]t @-  | TVTuple [TValue]         -- ^ @ (a, b, c )@-  | TVRec [(Ident, TValue)]  -- ^ @ { x : a, y : b, z : c } @-  | TVFun TValue TValue      -- ^ @ a -> b @+  = TVBit                     -- ^ @ Bit @+  | TVInteger                 -- ^ @ Integer @+  | TVIntMod Integer          -- ^ @ Z n @+  | TVSeq Integer TValue      -- ^ @ [n]a @+  | TVStream TValue           -- ^ @ [inf]t @+  | TVTuple [TValue]          -- ^ @ (a, b, c )@+  | TVRec [(Ident, TValue)]   -- ^ @ { x : a, y : b, z : c } @+  | TVFun TValue TValue       -- ^ @ a -> b @+  | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type     deriving (Generic, NFData)  -- | Convert a type value back into a regular type@@ -49,7 +50,13 @@     TVTuple ts  -> tTuple (map tValTy ts)     TVRec fs    -> tRec [ (f, tValTy t) | (f, t) <- fs ]     TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)+    TVAbstract u vs -> tAbstract u (map arg vs)+      where arg x = case x of+                      Left Inf     -> tInf+                      Left (Nat n) -> tNum n+                      Right v      -> tValTy v + instance Show TValue where   showsPrec p v = showsPrec p (tValTy v) @@ -103,6 +110,15 @@         (TCTuple _, _)  -> Right $ TVTuple (map val ts)         (TCNum n, [])   -> Left $ Nat n         (TCInf, [])     -> Left $ Inf+        (TCAbstract u,vs) ->+            case kindOf ty of+              KType -> Right $ TVAbstract u (map (evalType env) vs)+              k -> evalPanic "evalType"+                [ "Unsupported"+                , "*** Abstract type of kind: " ++ show (pp k)+                , "*** Name: " ++ show (pp u)+                ]+         -- FIXME: What about TCNewtype?         _ -> evalPanic "evalType" ["not a value type", show ty]     TCon (TF f) ts      -> Left $ evalTF f (map num ts)

@@ -541,8 +541,9 @@ -- | This class defines additional operations necessary to define generic evaluation --   functions. class BitWord b w i => EvalPrims b w i where-  -- | Eval prim binds primitive declarations to the primitive values that implement them.-  evalPrim :: Decl -> GenValue b w i+  -- | Eval prim binds primitive declarations to the primitive values that implement them.  Returns 'Nothing' for abstract primitives (i.e., once that are+  -- not implemented by this backend).+  evalPrim :: Decl -> Maybe (GenValue b w i)    -- | if/then/else operation.  Choose either the 'then' value or the 'else' value depending   --   on the value of the test bit.@@ -628,7 +629,10 @@  -- | Create a packed word of n bits. word :: BitWord b w i => Integer -> Integer -> GenValue b w i-word n i = VWord n $ ready $ WordVal $ wordLit n i+word n i+  | n >= Arch.maxBigIntWidth = wordTooWide n+  | otherwise                = VWord n $ ready $ WordVal $ wordLit n i+  lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i lam  = VFun

@@ -57,19 +57,19 @@ getPrimMap me = runModuleM me Base.getPrimMap  -- | Find the file associated with a module name in the module search path.-findModule :: P.ModName -> ModuleCmd FilePath+findModule :: P.ModName -> ModuleCmd ModulePath findModule n env = runModuleM env (Base.findModule n)  -- | Load the module contained in the given file.-loadModuleByPath :: FilePath -> ModuleCmd (FilePath,T.Module)+loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module) loadModuleByPath path (evo,env) = runModuleM (evo,resetModuleEnv env) $ do-  unloadModule ((path ==) . lmFilePath)+  unloadModule ((InFile path ==) . lmFilePath)   m <- Base.loadModuleByPath path   setFocusedModule (T.mName m)-  return (path,m)+  return (InFile path,m)  -- | Load the given parsed module.-loadModuleByName :: P.ModName -> ModuleCmd (FilePath,T.Module)+loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module) loadModuleByName n env = runModuleM env $ do   unloadModule ((n ==) . lmName)   (path,m') <- Base.loadModuleFrom (FromModule n)

@@ -21,7 +21,8 @@ import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap) import Cryptol.ModuleSystem.Env (lookupModule                                 , LoadedModule(..)-                                , meCoreLint, CoreLint(..))+                                , meCoreLint, CoreLint(..)+                                , ModulePath(..), modulePathLabel) import qualified Cryptol.Eval                 as E import qualified Cryptol.Eval.Value           as E import           Cryptol.Prims.Eval ()@@ -45,7 +46,7 @@ import Cryptol.Utils.Panic (panic) import Cryptol.Utils.Logger(logPutStrLn, logPrint) -import Cryptol.Prelude (writePreludeContents)+import Cryptol.Prelude (preludeContents)  import Cryptol.Transform.MonoValues (rewModule) @@ -105,23 +106,34 @@  -- Parsing --------------------------------------------------------------------- -parseModule :: FilePath -> ModuleM (Fingerprint, P.Module PName)+parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName) parseModule path = do -  bytesRes <- io (X.try (B.readFile path))+  bytesRes <- case path of+                InFile p -> io (X.try (B.readFile p))+                InMem _ bs -> pure (Right bs)    bytes <- case bytesRes of     Right bytes -> return bytes-    Left exn | IOE.isDoesNotExistError exn -> cantFindFile path-             | otherwise                   -> otherIOError path exn+    Left exn ->+      case path of+        InFile p+          | IOE.isDoesNotExistError exn -> cantFindFile p+          | otherwise                   -> otherIOError p exn+        InMem p _ -> panic "parseModule"+                       [ "IOError for in-memory contetns???"+                       , "Label: " ++ show p+                       , "Exception: " ++ show exn ]    txt <- case decodeUtf8' bytes of     Right txt -> return txt     Left e    -> badUtf8 path e    let cfg = P.defaultConfig-              { P.cfgSource  = path-              , P.cfgPreProc = P.guessPreProc path+              { P.cfgSource  = case path of+                                 InFile p -> p+                                 InMem l _ -> l+              , P.cfgPreProc = P.guessPreProc (modulePathLabel path)               }    case P.parseModule cfg txt of@@ -137,25 +149,26 @@ loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do   let fileName = takeFileName path   foundPath <- findFile fileName-  (fp, pm) <- parseModule foundPath+  (fp, pm) <- parseModule (InFile foundPath)   let n = thing (P.mName pm)    -- Check whether this module name has already been loaded from a different file   env <- getModuleEnv   -- path' is the resolved, absolute path, used only for checking   -- whether it's already been loaded-  path' <- io $ canonicalizePath foundPath+  path' <- io (canonicalizePath foundPath)+   case lookupModule n env of     -- loadModule will calculate the canonical path again-    Nothing -> doLoadModule (FromModule n) foundPath fp pm+    Nothing -> doLoadModule (FromModule n) (InFile foundPath) fp pm     Just lm      | path' == loaded -> return (lmModule lm)      | otherwise       -> duplicateModuleName n path' loaded-     where loaded = lmCanonicalPath lm+     where loaded = lmModuleId lm   -- | Load a module, unless it was previously loaded.-loadModuleFrom :: ImportSource -> ModuleM (FilePath,T.Module)+loadModuleFrom :: ImportSource -> ModuleM (ModulePath,T.Module) loadModuleFrom isrc =   do let n = importedModule isrc      mb <- getLoadedMaybe n@@ -171,7 +184,7 @@ -- | Load dependencies, typecheck, and add to the eval environment. doLoadModule ::   ImportSource ->-  FilePath ->+  ModulePath ->   Fingerprint ->   P.Module PName ->   ModuleM T.Module@@ -186,8 +199,7 @@       -- extend the eval env, unless a functor.      unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv tcm)-     canonicalPath <- io (canonicalizePath path)-     loadedModule path canonicalPath fp tcm+     loadedModule path fp tcm       return tcm   where@@ -224,8 +236,9 @@ moduleFile :: ModName -> String -> FilePath moduleFile n = addExtension (joinPath (modNameChunks n)) + -- | Discover a module.-findModule :: ModName -> ModuleM FilePath+findModule :: ModName -> ModuleM ModulePath findModule n = do   paths <- getSearchPath   loop (possibleFiles paths)@@ -234,13 +247,13 @@      path:rest -> do       b <- io (doesFileExist path)-      if b then return path else loop rest+      if b then return (InFile path) else loop rest      [] -> handleNotFound    handleNotFound =     case n of-      m | m == preludeName -> io writePreludeContents+      m | m == preludeName -> pure (InMem "Cryptol" preludeContents)       _ -> moduleNotFound n =<< getSearchPath    -- generate all possible search paths@@ -359,7 +372,7 @@                   [ "Unable to find the prelude" ]  -- | Load a module, be it a normal module or a functor instantiation.-checkModule :: ImportSource -> FilePath -> P.Module PName -> ModuleM T.Module+checkModule :: ImportSource -> ModulePath -> P.Module PName -> ModuleM T.Module checkModule isrc path m =   case P.mInstance m of     Nothing -> checkSingleModule T.tcModule isrc path m@@ -373,7 +386,7 @@ checkSingleModule ::   Act (P.Module Name) T.Module {- ^ how to check -} ->   ImportSource                 {- ^ why are we loading this -} ->-  FilePath                     {- path -} ->+  ModulePath                   {- path -} ->   P.Module PName               {- ^ module to check -} ->   ModuleM T.Module checkSingleModule how isrc path m = do@@ -383,8 +396,14 @@   unless (notParamInstModName nm == thing (P.mName m))          (moduleNameMismatch nm (mName m)) -  -- remove includes first-  e   <- io (removeIncludesModule path m)+  -- remove includes first; we only do this for actual files.+  -- it is less clear what should happen for in-memory things, and since+  -- this is a more-or-less obsolete feature, we are just not doing+  -- ot for now.+  e   <- case path of+           InFile p -> io (removeIncludesModule p m)+           InMem {} -> pure (Right m)+   nim <- case e of            Right nim  -> return nim            Left ierrs -> noIncludeErrors ierrs@@ -502,6 +521,7 @@     , T.inpVars      = Map.map ifDeclSig (ifDecls env)     , T.inpTSyns     = ifTySyns env     , T.inpNewtypes  = ifNewtypes env+    , T.inpAbstractTypes = ifAbstractTypes env     , T.inpNameSeeds = seeds     , T.inpMonoBinds = monoBinds     , T.inpSolverConfig = cfg

@@ -25,8 +25,9 @@ import Cryptol.Parser.AST import qualified Cryptol.TypeCheck as T import qualified Cryptol.TypeCheck.AST as T-import Cryptol.Utils.PP (NameDisp)+import Cryptol.Utils.PP (PP(..),text,parens,NameDisp) +import Data.ByteString(ByteString) import Control.Monad (guard,mplus) import qualified Control.Exception as X import Data.Function (on)@@ -222,6 +223,36 @@  -- Loaded Modules -------------------------------------------------------------- +-- | The location of a module+data ModulePath = InFile FilePath+                | InMem String ByteString -- ^ Label, content+    deriving (Show, Generic, NFData)++-- | In-memory things are compared by label.+instance Eq ModulePath where+  p1 == p2 =+    case (p1,p2) of+      (InFile x, InFile y) -> x == y+      (InMem a _, InMem b _) -> a == b+      _ -> False++instance PP ModulePath where+  ppPrec _ e =+    case e of+      InFile p  -> text p+      InMem l _ -> parens (text l)++++-- | The name of the content---either the file path, or the provided label.+modulePathLabel :: ModulePath -> String+modulePathLabel p =+  case p of+    InFile path -> path+    InMem lab _ -> lab+++ data LoadedModules = LoadedModules   { lmLoadedModules      :: [LoadedModule]     -- ^ Invariants:@@ -250,10 +281,12 @@  data LoadedModule = LoadedModule   { lmName              :: ModName-  , lmFilePath          :: FilePath+  , lmFilePath          :: ModulePath     -- ^ The file path used to load this module (may not be canonical)-  , lmCanonicalPath     :: FilePath-    -- ^ The canonical version of the path of this module+  , lmModuleId          :: String+    -- ^ An identifier used to identify the source of the bytes for the module.+    -- For files we just use the cononical path, for in memory things we+    -- use their label.   , lmInterface         :: Iface   , lmModule            :: T.Module   , lmFingerprint       :: Fingerprint@@ -277,8 +310,8 @@ -- | Add a freshly loaded module.  If it was previously loaded, then -- the new version is ignored. addLoadedModule ::-  FilePath -> FilePath -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules-addLoadedModule path canonicalPath fp tm lm+  ModulePath -> String -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules+addLoadedModule path ident fp tm lm   | isLoaded (T.mName tm) lm  = lm   | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :                                                 lmLoadedParamModules lm }@@ -288,7 +321,7 @@   loaded = LoadedModule     { lmName            = T.mName tm     , lmFilePath        = path-    , lmCanonicalPath   = canonicalPath+    , lmModuleId        = ident     , lmInterface       = genIface tm     , lmModule          = tm     , lmFingerprint     = fp@@ -341,6 +374,7 @@   mconcat [ IfaceDecls             { ifTySyns   = Map.empty             , ifNewtypes = Map.empty+            , ifAbstractTypes = Map.empty             , ifDecls    = Map.singleton (ifDeclName ifd) ifd             }           | decl <- concatMap T.groupDecls dgs

@@ -18,6 +18,7 @@    exportedNames (Decl td) = map exportBind  (names  namesD td)                          ++ map exportType (names tnamesD td)+  exportedNames (DPrimType t) = [ exportType (thing . primTName <$> t) ]   exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt)   exportedNames (Include {})  = []   exportedNames (DParameterFun {}) = []

@@ -50,6 +50,7 @@            renamedExports  = inst env (mExports func)            renamedTySyns   = rnMp tsName (mTySyns func)            renamedNewtypes = rnMp ntName (mNewtypes func)+           renamedPrimTys  = rnMp atName (mPrimTypes func)             su = listParamSubst (Map.toList (tyParamMap env)) @@ -66,6 +67,7 @@                  , mImports           = mImports func                  , mTySyns            = renamedTySyns                  , mNewtypes          = renamedNewtypes+                 , mPrimTypes         = renamedPrimTys                  , mParamTypes        = Map.empty                  , mParamConstraints  = []                  , mParamFuns         = Map.empty@@ -250,8 +252,9 @@ instance Inst TC where   inst env tc =     case tc of-      TCNewtype x -> TCNewtype (inst env x)-      _           -> tc+      TCNewtype x  -> TCNewtype (inst env x)+      TCAbstract x -> TCAbstract (inst env x)+      _            -> tc  instance Inst UserTC where   inst env (UserTC x t) = UserTC y t@@ -281,6 +284,15 @@                         , ntDoc = ntDoc nt                         }     where x = ntName nt++instance Inst AbstractType where+  inst env a = AbstractType { atName    = instTyName env (atName a)+                            , atKind    = atKind a+                            , atCtrs    = case atCtrs a of+                                            (xs,ps) -> (xs, inst env ps)+                            , atFixitiy = atFixitiy a+                            , atDoc     = atDoc a+                            }  instTyName :: Env -> Name -> Name instTyName env x = Map.findWithDefault x x (tyNameMap env)

@@ -61,24 +61,27 @@   }  data IfaceDecls = IfaceDecls-  { ifTySyns   :: Map.Map Name IfaceTySyn-  , ifNewtypes :: Map.Map Name IfaceNewtype-  , ifDecls    :: Map.Map Name IfaceDecl+  { ifTySyns        :: Map.Map Name IfaceTySyn+  , ifNewtypes      :: Map.Map Name IfaceNewtype+  , ifAbstractTypes :: Map.Map Name IfaceAbstractType+  , ifDecls         :: Map.Map Name IfaceDecl   } deriving (Show, Generic, NFData)  instance Semigroup IfaceDecls where   l <> r = IfaceDecls     { ifTySyns   = Map.union (ifTySyns l)   (ifTySyns r)     , ifNewtypes = Map.union (ifNewtypes l) (ifNewtypes r)+    , ifAbstractTypes = Map.union (ifAbstractTypes l) (ifAbstractTypes r)     , ifDecls    = Map.union (ifDecls l)    (ifDecls r)     }  instance Monoid IfaceDecls where-  mempty      = IfaceDecls Map.empty Map.empty Map.empty+  mempty      = IfaceDecls Map.empty Map.empty Map.empty Map.empty   mappend l r = l <> r   mconcat ds  = IfaceDecls     { ifTySyns   = Map.unions (map ifTySyns   ds)     , ifNewtypes = Map.unions (map ifNewtypes ds)+    , ifAbstractTypes = Map.unions (map ifAbstractTypes ds)     , ifDecls    = Map.unions (map ifDecls    ds)     } @@ -88,6 +91,7 @@ ifTySynName = tsName  type IfaceNewtype = Newtype+type IfaceAbstractType = AbstractType  data IfaceDecl = IfaceDecl   { ifDeclName    :: !Name          -- ^ Name of thing@@ -116,12 +120,14 @@   , ifPublic      = IfaceDecls     { ifTySyns    = tsPub     , ifNewtypes  = ntPub+    , ifAbstractTypes = atPub     , ifDecls     = dPub     }    , ifPrivate = IfaceDecls     { ifTySyns    = tsPriv     , ifNewtypes  = ntPriv+    , ifAbstractTypes = atPriv     , ifDecls     = dPriv     } @@ -139,6 +145,10 @@   (ntPub,ntPriv) =       Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )                            (mNewtypes m)++  (atPub,atPriv) =+    Map.partitionWithKey (\qn _ -> qn `isExportedType` mExports m)+                         (mPrimTypes m)    (dPub,dPriv) =       Map.partitionWithKey (\ qn _ -> qn `isExportedBind` mExports m)

@@ -40,6 +40,7 @@ import Data.Maybe (isJust) import Data.Text.Encoding.Error (UnicodeException) import MonadLib+import System.Directory (canonicalizePath)  import GHC.Generics (Generic) import Control.DeepSeq@@ -47,6 +48,7 @@ import Prelude () import Prelude.Compat + -- Errors ----------------------------------------------------------------------  data ImportSource@@ -78,11 +80,11 @@     -- ^ Unable to find the module given, tried looking in these paths   | CantFindFile FilePath     -- ^ Unable to open a file-  | BadUtf8 FilePath UnicodeException+  | BadUtf8 ModulePath UnicodeException     -- ^ Bad UTF-8 encoding in while decoding this file   | OtherIOError FilePath IOException     -- ^ Some other IO error occurred while reading this file-  | ModuleParseError FilePath Parser.ParseError+  | ModuleParseError ModulePath Parser.ParseError     -- ^ Generated this parse error when parsing the file for module m   | RecursiveModules [ImportSource]     -- ^ Recursive module group discovered@@ -106,7 +108,7 @@     -- ^ Failed to add the module parameters to all definitions in a module.   | NotAParameterizedModule P.ModName -  | ErrorInFile FilePath ModuleError+  | ErrorInFile ModulePath ModuleError     -- ^ This is just a tag on the error, indicating the file containing it.     -- It is convenient when we had to look for the module, and we'd like     -- to communicate the location of pthe problematic module to the handler.@@ -153,7 +155,7 @@      BadUtf8 path _ue ->       text "[error]" <+>-      text "bad utf-8 encoding:" <+> text path+      text "bad utf-8 encoding:" <+> pp path      OtherIOError path exn ->       hang (text "[error]" <+>@@ -207,13 +209,13 @@ cantFindFile :: FilePath -> ModuleM a cantFindFile path = ModuleT (raise (CantFindFile path)) -badUtf8 :: FilePath -> UnicodeException -> ModuleM a+badUtf8 :: ModulePath -> UnicodeException -> ModuleM a badUtf8 path ue = ModuleT (raise (BadUtf8 path ue))  otherIOError :: FilePath -> IOException -> ModuleM a otherIOError path exn = ModuleT (raise (OtherIOError path exn)) -moduleParseError :: FilePath -> Parser.ParseError -> ModuleM a+moduleParseError :: ModulePath -> Parser.ParseError -> ModuleM a moduleParseError path err =   ModuleT (raise (ModuleParseError path err)) @@ -260,7 +262,7 @@  -- | Run the computation, and if it caused and error, tag the error -- with the given file.-errorInFile :: FilePath -> ModuleM a -> ModuleM a+errorInFile :: ModulePath -> ModuleM a -> ModuleM a errorInFile file (ModuleT m) = ModuleT (m `handle` h)   where h e = raise $ case e of                         ErrorInFile {} -> e@@ -414,11 +416,11 @@     _      -> return (FromModule noModuleName)  getIface :: P.ModName -> ModuleM Iface-getIface mn = ModuleT $ do-  env <- get-  case lookupModule mn env of-    Just lm -> return (lmInterface lm)-    Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)]+getIface mn =+  do env <- ModuleT get+     case lookupModule mn env of+       Just lm -> return (lmInterface lm)+       Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)]  getLoaded :: P.ModName -> ModuleM T.Module getLoaded mn = ModuleT $@@ -456,10 +458,14 @@   env <- get   set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) } -loadedModule :: FilePath -> FilePath -> Fingerprint -> T.Module -> ModuleM ()-loadedModule path canonicalPath fp m = ModuleT $ do+loadedModule :: ModulePath -> Fingerprint -> T.Module -> ModuleM ()+loadedModule path fp m = ModuleT $ do   env <- get-  set $! env { meLoadedModules = addLoadedModule path canonicalPath fp m (meLoadedModules env) }+  ident <- case path of+             InFile p  -> unModuleT $ io (canonicalizePath p)+             InMem l _ -> pure l++  set $! env { meLoadedModules = addLoadedModule path ident fp m (meLoadedModules env) }  modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM () modifyEvalEnv f = ModuleT $ do

@@ -27,7 +27,7 @@ import Cryptol.Utils.Panic (panic)  import Data.List (nub)-import Data.Maybe (catMaybes,fromMaybe,mapMaybe)+import Data.Maybe (fromMaybe) import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Semigroup@@ -48,8 +48,6 @@                              -- ^ Expr renaming environment                            , neTypes :: !(Map.Map PName [Name])                              -- ^ Type renaming environment-                           , neFixity:: !(Map.Map Name Fixity)-                             -- ^ Expression-level fixity environment                            } deriving (Show, Generic, NFData)  -- | Return a list of value-level names to which this parsed name may refer.@@ -65,23 +63,18 @@ instance Semigroup NamingEnv where   l <> r   =     NamingEnv { neExprs  = Map.unionWith merge (neExprs  l) (neExprs  r)-              , neTypes  = Map.unionWith merge (neTypes  l) (neTypes  r)-              , neFixity = Map.union           (neFixity l) (neFixity r) }+              , neTypes  = Map.unionWith merge (neTypes  l) (neTypes  r) }  instance Monoid NamingEnv where   mempty        =     NamingEnv { neExprs  = Map.empty-              , neTypes  = Map.empty-              , neFixity = Map.empty }+              , neTypes  = Map.empty } -  -- NOTE: merging the fixity maps is a special case that just prefers the left-  -- entry, as they're already keyed by a name with a unique   mappend l r   = l <> r    mconcat envs  =     NamingEnv { neExprs  = Map.unionsWith merge (map neExprs  envs)-              , neTypes  = Map.unionsWith merge (map neTypes  envs)-              , neFixity = Map.unions           (map neFixity envs) }+              , neTypes  = Map.unionsWith merge (map neTypes  envs) }    {-# INLINE mempty #-}   {-# INLINE mappend #-}@@ -174,11 +167,10 @@ shadowing :: NamingEnv -> NamingEnv -> NamingEnv shadowing l r = NamingEnv   { neExprs  = Map.union (neExprs  l) (neExprs  r)-  , neTypes  = Map.union (neTypes  l) (neTypes  r)-  , neFixity = Map.union (neFixity l) (neFixity r) }+  , neTypes  = Map.union (neTypes  l) (neTypes  r) }  travNamingEnv :: Applicative f => (Name -> f Name) -> NamingEnv -> f NamingEnv-travNamingEnv f ne = NamingEnv <$> neExprs' <*> neTypes' <*> pure (neFixity ne)+travNamingEnv f ne = NamingEnv <$> neExprs' <*> neTypes'   where     neExprs' = traverse (traverse f) (neExprs ne)     neTypes' = traverse (traverse f) (neTypes ne)@@ -268,28 +260,23 @@ -- the names are qualified. unqualifiedEnv :: IfaceDecls -> NamingEnv unqualifiedEnv IfaceDecls { .. } =-  mconcat [ exprs, tySyns, ntTypes, ntExprs-          , mempty { neFixity = Map.fromList fixity } ]+  mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs ]   where   toPName n = mkUnqual (nameIdent n)    exprs   = mconcat [ singletonE (toPName n) n | n <- Map.keys ifDecls ]   tySyns  = mconcat [ singletonT (toPName n) n | n <- Map.keys ifTySyns ]   ntTypes = mconcat [ singletonT (toPName n) n | n <- Map.keys ifNewtypes ]+  absTys  = mconcat [ singletonT (toPName n) n | n <- Map.keys ifAbstractTypes ]   ntExprs = mconcat [ singletonE (toPName n) n | n <- Map.keys ifNewtypes ] -  fixity =-    catMaybes [ do f <- ifDeclFixity d; return (ifDeclName d,f)-              | d    <- Map.elems ifDecls ] - -- | Compute an unqualified naming environment, containing the various module -- parameters. modParamsNamingEnv :: IfaceParams -> NamingEnv modParamsNamingEnv IfaceParams { .. } =   NamingEnv { neExprs = Map.fromList $ map fromFu $ Map.keys ifParamFuns             , neTypes = Map.fromList $ map fromTy $ Map.elems ifParamTypes-            , neFixity = Map.fromList $ mapMaybe toFix $ Map.elems ifParamFuns             }    where@@ -300,11 +287,8 @@    fromFu f  = (toPName f, [f]) -  toFix x = do d <- T.mvpFixity x-               return (T.mvpName x, d)  - data ImportIface = ImportIface Import Iface  -- | Produce a naming environment from an interface file, that contains a@@ -320,11 +304,7 @@     do let Located { .. } = bName b        n <- newTop ns thing (bFixity b) srcRange -       let fixity = case bFixity b of-             Just f  -> mempty { neFixity = Map.singleton n f }-             Nothing -> mempty--       return (singletonE thing n `mappend` fixity)+       return (singletonE thing n)  -- | Generate the naming environment for a type parameter. instance BindsNames (TParam PName) where@@ -344,12 +324,20 @@   namingEnv (InModule ns td) =     case td of       Decl d           -> namingEnv (InModule ns (tlValue d))+      DPrimType d      -> namingEnv (InModule ns (tlValue d))       TDNewtype d      -> namingEnv (InModule ns (tlValue d))       DParameterType d -> namingEnv (InModule ns d)       DParameterConstraint {} -> mempty       DParameterFun  d -> namingEnv (InModule ns d)       Include _   -> mempty +instance BindsNames (InModule (PrimType PName)) where+  namingEnv (InModule ns PrimType { .. }) =+    BuildNamingEnv $+      do let Located { .. } = primTName+         nm <- newTop ns thing primTFixity srcRange+         pure (singletonT thing nm)+ instance BindsNames (InModule (ParameterFun PName)) where   namingEnv (InModule ns ParameterFun { .. }) = BuildNamingEnv $     do let Located { .. } = pfName@@ -377,12 +365,12 @@   namingEnv (InModule pfx d) = case d of     DBind b -> BuildNamingEnv $       do n <- mkName (bName b) (bFixity b)-         return (singletonE (thing (bName b)) n `mappend` fixity n b)+         return (singletonE (thing (bName b)) n)      DSignature ns _sig      -> foldMap qualBind ns     DPragma ns _p           -> foldMap qualBind ns-    DType (TySyn lqn _ _)   -> qualType lqn-    DProp (PropSyn lqn _ _) -> qualType lqn+    DType syn               -> qualType (tsName syn) (tsFixity syn)+    DProp syn               -> qualType (psName syn) (psFixity syn)     DLocated d' _           -> namingEnv (InModule pfx d')     DPatBind _pat _e        -> panic "ModuleSystem" ["Unexpected pattern binding"]     DFixity{}               -> panic "ModuleSystem" ["Unexpected fixity declaration"]@@ -395,11 +383,6 @@       do n <- mkName ln Nothing          return (singletonE (thing ln) n) -    qualType ln = BuildNamingEnv $-      do n <- mkName ln Nothing+    qualType ln f = BuildNamingEnv $+      do n <- mkName ln f          return (singletonT (thing ln) n)--    fixity n b =-      case bFixity b of-        Just f  -> mempty { neFixity = Map.singleton n f }-        Nothing -> mempty

@@ -31,16 +31,14 @@ import Cryptol.ModuleSystem.Name import Cryptol.ModuleSystem.NamingEnv import Cryptol.ModuleSystem.Exports-import Cryptol.Prims.Syntax import Cryptol.Parser.AST import Cryptol.Parser.Position import Cryptol.Parser.Selector(ppNestedSels,selName)-import Cryptol.TypeCheck.Type (TCon(..))-import Cryptol.Utils.Ident (packInfix) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP  import Data.List(find)+import Data.Maybe (fromMaybe) import qualified Data.Foldable as F import           Data.Map.Strict ( Map ) import qualified Data.Map.Strict as Map@@ -78,7 +76,7 @@     -- ^ When a type is missing from the naming environment, but one or more     -- values exist with the same name. -  | FixityError (Located Name) (Located Name) NameDisp+  | FixityError (Located Name) Fixity (Located Name) Fixity NameDisp     -- ^ When the fixity of two operators conflict    | InvalidConstraint (Type PName) NameDisp@@ -126,11 +124,14 @@          4 (fsep [ text "Expected a type named", quotes (pp (thing lqn))                  , text "but found a value instead" ]) -    FixityError o1 o2 disp -> fixNameDisp disp $-      hang (text "[error]")-         4 (fsep [ text "The fixities of", pp o1, text "and", pp o2-                 , text "are not compatible.  "-                 , text "You may use explicit parenthesis to disambiguate" ])+    FixityError o1 f1 o2 f2 disp -> fixNameDisp disp $+      hang (text "[error] at" <+> pp (srcRange o1) <+> text "and" <+> pp (srcRange o2))+         4 (fsep [ text "The fixities of"+                 , nest 2 $ vcat+                   [ "•" <+> pp (thing o1) <+> parens (pp f1)+                   , "•" <+> pp (thing o2) <+> parens (pp f2) ]+                 , text "are not compatible."+                 , text "You may use explicit parentheses to disambiguate." ])      InvalidConstraint ty disp -> fixNameDisp disp $       hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))@@ -162,9 +163,10 @@ instance PP RenamerWarning where   ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $     hang (text "[warning] at" <+> loc)-       4 $ fsep [ text "This binding for" <+> sym-                , (text "shadows the existing binding" <.> plural) <+> text "from" ]-        $$ vcat (map ppLocName originals)+       4 $ fsep [ text "This binding for" <+> backticks sym+                , text "shadows the existing binding" <.> plural <+>+                  text "at" ]+        $$ vcat (map (pp . nameLoc) originals)      where     plural | length originals > 1 = char 's'@@ -396,6 +398,7 @@ instance Rename TopDecl where   rename td     = case td of     Decl d      -> Decl      <$> traverse rename d+    DPrimType d -> DPrimType <$> traverse rename d     TDNewtype n -> TDNewtype <$> traverse rename n     Include n   -> return (Include n)     DParameterFun f  -> DParameterFun  <$> rename f@@ -408,6 +411,13 @@   do y <- rename (thing x)      return x { thing = y } +instance Rename PrimType where+  rename pt =+    do x <- rnLocated renameType (primTName pt)+       let (as,ps) = primTCts pt+       (_,cts) <- renameQual as ps $ \as' ps' -> pure (as',ps')+       pure pt { primTCts = cts, primTName = x }+ instance Rename ParameterType where   rename a =     do n' <- rnLocated renameType (ptName a)@@ -531,18 +541,20 @@ -- into scope. renameSchema :: Schema PName -> RenameM (NamingEnv,Schema Name) renameSchema (Forall ps p ty loc) =-  do -- check that the parameters don't shadow any built-in types-     let reserved = filter (isReserved . 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-                                     <*> pure loc+  renameQual ps p $ \ps' p' ->+    do ty' <- rename ty+       pure (Forall ps' p' ty' loc) -     return (env,s')+-- | Rename a qualified thing.+renameQual :: [TParam PName] -> [Prop PName] ->+              ([TParam Name] -> [Prop Name] -> RenameM a) ->+              RenameM (NamingEnv, a)+renameQual as ps k =+  do env <- liftSupply (namingEnv' as)+     res <- shadowNames env $ do as' <- traverse rename as+                                 ps' <- traverse rename ps+                                 k as' ps'+     pure (env,res)  instance Rename TParam where   rename TParam { .. } =@@ -550,53 +562,7 @@        return TParam { tpName = n, .. }  instance Rename Prop where-  rename p      = case p of-    CFin t        -> CFin       <$> rename t-    CEqual l r    -> CEqual     <$> rename l <*> rename r-    CNeq l r      -> CNeq       <$> rename l <*> rename r-    CGeq l r      -> CGeq       <$> rename l <*> rename r-    CZero t       -> CZero      <$> rename t-    CLogic t      -> CLogic     <$> rename t-    CArith t      -> CArith     <$> rename t-    CCmp t        -> CCmp       <$> rename t-    CSignedCmp t  -> CSignedCmp <$> rename t-    CLiteral l r  -> CLiteral   <$> rename l <*> rename r-    CUser qn ps   -> CUser      <$> renameType qn <*> traverse rename ps-    CLocated p' r -> withLoc r-                   $ CLocated <$> rename p' <*> pure r--    -- here, we rename the type and then require that it produces something that-    -- looks like a Prop-    CType t -> translateProp =<< resolveTypeFixity t--translateProp :: Type PName -> RenameM (Prop Name)-translateProp ty = go ty-  where-  go t = case t of--    TLocated t' r -> (`CLocated` r) <$> go t'--    TApp (PC x) [l,r]-      | PEqual <- x -> CEqual <$> rename l <*> rename r-      | PNeq   <- x -> CNeq   <$> rename l <*> rename r-      | PGeq   <- x -> CGeq   <$> rename l <*> rename r--    TUser n [l,r]-      | isLeq n -> CGeq <$> rename r <*> rename l--    TUser n ts -> CUser <$> renameType n <*> traverse rename ts--    -- record an error, but continue renaming to gather any other errors-    _ ->-      do record (InvalidConstraint ty)-         CType <$> rename t----- | Check to see if this identifier is a reserved type/type-function.-isReserved :: PName -> Bool-isReserved pn = case primTyFromPName pn of-                  Just _ -> True-                  _      -> False+  rename (CType t) = CType <$> rename t   -- | Resolve fixity, then rename the resulting type.@@ -610,14 +576,7 @@     go (TNum c)      = return (TNum c)     go (TChar c)     = return (TChar c) -    go (TUser pn ps)--      | Just pt <- primTyFromPName pn =-        do ps' <- traverse go ps-           return (TApp (primTyCon pt) ps')-     go (TUser qn ps)   = TUser    <$> renameType qn <*> traverse go ps-    go (TApp f xs)     = TApp f   <$> traverse go xs     go (TRecord fs)    = TRecord  <$> traverse (rnNamed go) fs     go (TTuple fs)     = TTuple   <$> traverse go fs     go  TWild          = return TWild@@ -640,7 +599,6 @@     TFun a b     -> TFun     <$> go a  <*> go b     TSeq n a     -> TSeq     <$> go n  <*> go a     TUser pn ps  -> TUser pn <$> traverse go ps-    TApp f xs    -> TApp f   <$> traverse go xs     TRecord fs   -> TRecord  <$> traverse (traverse go) fs     TTuple fs    -> TTuple   <$> traverse go fs @@ -649,7 +607,7 @@     TParens t'   -> TParens <$> go t'      TInfix a o _ b ->-      do let op = lookupFixity o+      do op <- lookupFixity o          a' <- go a          b' <- go b          mkTInfix a' op b'@@ -667,11 +625,8 @@ mkTInfix t op@(o2,f2) z =   case t of     TLocated t1 _ -> mkTInfix t1 op z--    TUser op1 [x,y] | isLeq op1 -> doFixity (TUser op1) leqFixity x y-    TApp tc [x,y]-      | Just pt <- primTyFromTC tc-      , Just f1 <- primTyFixity pt -> doFixity (TApp tc) f1 x y+    TInfix x ln f1 y ->+      doFixity (\a b -> TInfix a ln f1 b) f1 x y      _ -> return (o2 t z) @@ -680,7 +635,7 @@     case compareFixity f1 f2 of       FCLeft  -> return (o2 t z)       FCRight -> do r <- mkTInfix y op z-                    return (mk [x,r])+                    return (mk x r)        -- As the fixity table is known, and this is a case where the fixity came       -- from that table, it's a real error if the fixities didn't work out.@@ -691,35 +646,16 @@  -- | When possible, rewrite the type operator to a known constructor, otherwise -- return a 'TOp' that reconstructs the original term, and a default fixity.-lookupFixity :: Located PName -> (TOp,Fixity)+lookupFixity :: Located PName -> RenameM (TOp, Fixity) lookupFixity op =-  case lkp of-    Just res -> res--    -- unknown type operator, just use default fixity-    -- NOTE: this works for the props defined above, as all other operators-    -- are defined with a higher precedence.-    Nothing    -> (\x y -> TUser sym [x,y], Fixity NonAssoc 0)+  do n <- renameType sym+     let fi = fromMaybe defaultFixity (nameFixity n)+     return (\x y -> TInfix x op fi y, fi)    where   sym = thing op-  lkp = do pt <- primTyFromPName (thing op)-           fi <- primTyFixity pt-           return (\x y -> TApp (primTyCon pt) [x,y], fi)-        `mplus`-        do guard (isLeq sym)-           return (\x y -> TUser sym [x,y], leqFixity) -leqFixity :: Fixity-leqFixity = Fixity NonAssoc 30 -leqIdent :: Ident-leqIdent  = packInfix "<="--isLeq :: PName -> Bool-isLeq x = getIdent x == leqIdent-- -- | Rename a binding. instance Rename Bind where   rename b      = do@@ -754,7 +690,7 @@     PLocated p' loc -> withLoc loc                      $ PLocated <$> rename p'    <*> pure loc --- | Note that after this point the @->@ updates have an explicit funciton+-- | Note that after this point the @->@ updates have an explicit function -- and there are no more nested updates. instance Rename UpdField where   rename (UpdField h ls e) =@@ -777,47 +713,50 @@  instance Rename Expr where   rename expr = case expr of-    EVar n        -> EVar <$> renameVar n-    ELit l        -> return (ELit l)-    ENeg e        -> ENeg    <$> rename e-    EComplement e -> EComplement-                             <$> rename e-    ETuple es     -> ETuple  <$> traverse rename es-    ERecord fs    -> ERecord <$> traverse (rnNamed rename) fs-    ESel e' s     -> ESel    <$> rename e' <*> pure s-    EUpd mb fs    -> do checkLabels fs-                        EUpd <$> traverse rename mb <*> traverse rename fs-    EList es      -> EList   <$> traverse rename es-    EFromTo s n e'-> EFromTo <$> rename s-                             <*> traverse rename n-                             <*> rename e'-    EInfFrom a b  -> EInfFrom<$> rename a  <*> traverse rename b-    EComp e' bs   -> do arms' <- traverse renameArm bs-                        let (envs,bs') = unzip arms'-                        -- 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-    EWhere e' ds  -> do ns <- getNS-                        shadowNames (map (InModule ns) ds) $-                          EWhere <$> rename e' <*> traverse rename ds-    ETyped e' ty  -> ETyped  <$> rename e' <*> rename ty-    ETypeVal ty   -> ETypeVal<$> rename ty-    EFun ps e'    -> do (env,ps') <- renamePats ps-                        -- NOTE: renamePats will generate warnings, so we don't-                        -- need to duplicate them here-                        shadowNames' CheckNone env (EFun ps' <$> rename e')-    ELocated e' r -> withLoc r-                   $ ELocated <$> rename e' <*> pure r+    EVar n          -> EVar <$> renameVar n+    ELit l          -> return (ELit l)+    ENeg e          -> ENeg    <$> rename e+    EComplement e   -> EComplement+                               <$> rename e+    EGenerate e     -> EGenerate+                               <$> rename e+    ETuple es       -> ETuple  <$> traverse rename es+    ERecord fs      -> ERecord <$> traverse (rnNamed rename) fs+    ESel e' s       -> ESel    <$> rename e' <*> pure s+    EUpd mb fs      -> do checkLabels fs+                          EUpd <$> traverse rename mb <*> traverse rename fs+    EList es        -> EList   <$> traverse rename es+    EFromTo s n e t -> EFromTo <$> rename s+                               <*> traverse rename n+                               <*> rename e+                               <*> traverse rename t+    EInfFrom a b    -> EInfFrom<$> rename a  <*> traverse rename b+    EComp e' bs     -> do arms' <- traverse renameArm bs+                          let (envs,bs') = unzip arms'+                          -- 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+    EWhere e' ds    -> do ns <- getNS+                          shadowNames (map (InModule ns) ds) $+                            EWhere <$> rename e' <*> traverse rename ds+    ETyped e' ty    -> ETyped  <$> rename e' <*> rename ty+    ETypeVal ty     -> ETypeVal<$> rename ty+    EFun ps e'      -> do (env,ps') <- renamePats ps+                          -- NOTE: renamePats will generate warnings, so we don't+                          -- need to duplicate them here+                          shadowNames' CheckNone env (EFun ps' <$> rename e')+    ELocated e' r   -> withLoc r+                     $ ELocated <$> rename e' <*> pure r -    ESplit e      -> ESplit  <$> rename e-    EParens p     -> EParens <$> rename p-    EInfix x y _ z-> do op <- renameOp y-                        x' <- rename x-                        z' <- rename z-                        mkEInfix x' op z'+    ESplit e        -> ESplit  <$> rename e+    EParens p       -> EParens <$> rename p+    EInfix x y _ z  -> do op <- renameOp y+                          x' <- rename x+                          z' <- rename z+                          mkEInfix x' op z'   checkLabels :: [UpdField PName] -> RenameM ()@@ -859,7 +798,7 @@      FCRight -> do r <- mkEInfix y op z                    return (EInfix x o1 f1 r) -     FCError -> do record (FixityError o1 o2)+     FCError -> do record (FixityError o1 f1 o2 f2)                    return (EInfix e o2 f2 z)  mkEInfix (ELocated e' _) op z =@@ -872,8 +811,7 @@ renameOp :: Located PName -> RenameM (Located Name,Fixity) renameOp ln = withLoc ln $   do n  <- renameVar (thing ln)-     ro <- RenameM ask-     case Map.lookup n (neFixity (roNames ro)) of+     case nameFixity n of        Just fixity -> return (ln { thing = n },fixity)        Nothing     -> return (ln { thing = n },defaultFixity) @@ -977,9 +915,6 @@          Just _ -> bindTypes ps           Nothing-           -- Just ignore reserved names, as they'll be resolved when renaming.-           | isReserved pn ->-             bindTypes ps             -- The type isn't bound, and has no parameters, so it names a portion            -- of the type of the pattern.@@ -996,7 +931,6 @@                 n   <- liftSupply (mkParameter (getIdent pn) loc)                 return (singletonT pn n) -  typeEnv (TApp _ ts)       = bindTypes ts   typeEnv (TRecord fs)      = bindTypes (map value fs)   typeEnv (TTuple ts)       = bindTypes ts   typeEnv TWild             = return mempty@@ -1018,22 +952,18 @@     MatchLet b -> shadowNamesNS b (MatchLet <$> rename b)  instance Rename TySyn where-  rename (TySyn n ps ty) =-    do when (isReserved (thing n))-            (record (BoundReservedType (thing n) (getLoc n) (text "type synonym")))--       shadowNames ps $ TySyn <$> rnLocated renameType n-                              <*> traverse rename ps-                              <*> rename ty+  rename (TySyn n f ps ty) =+    shadowNames ps $ TySyn <$> rnLocated renameType n+                           <*> pure f+                           <*> traverse rename ps+                           <*> rename ty  instance Rename PropSyn where-  rename (PropSyn n ps cs) =-    do when (isReserved (thing n))-            (record (BoundReservedType (thing n) (getLoc n) (text "constraint synonym")))--       shadowNames ps $ PropSyn <$> rnLocated renameType n-                                <*> traverse rename ps-                                <*> traverse rename cs+  rename (PropSyn n f ps cs) =+    shadowNames ps $ PropSyn <$> rnLocated renameType n+                             <*> pure f+                             <*> traverse rename ps+                             <*> traverse rename cs   -- Utilities -------------------------------------------------------------------

@@ -31,7 +31,6 @@ import qualified Data.Text as T import           Control.Monad(liftM2,msum) -import Cryptol.Prims.Syntax(TFun(..)) import Cryptol.Parser.AST import Cryptol.Parser.Position import Cryptol.Parser.LexerUtils hiding (mkIdent)@@ -42,7 +41,15 @@ import Paths_cryptol } +{- state 196 contains 1 shift/reduce conflicts.+     `_` identifier conflicts with `_` in record update.+    We have `_` as an identifier for the cases where we parse types as+    expressions, for example `[ 12 .. _ ]`.+-} +%expect 1++ %token   NUM         { $$@(Located _ (Token (Num   {}) _))}   STRLIT      { $$@(Located _ (Token (StrLit {}) _))}@@ -74,6 +81,7 @@    'primitive' { Located $$ (Token (KW KW_primitive) _)}   'constraint'{ Located $$ (Token (KW KW_constraint) _)}+  'Prop'      { Located $$ (Token (KW KW_Prop) _)}    '['         { Located $$ (Token (Sym BracketL) _)}   ']'         { Located $$ (Token (Sym BracketR) _)}@@ -112,6 +120,7 @@   '~'         { Located $$ (Token (Op Complement) _)}    '#'         { Located $$ (Token (Op Hash) _)}+  '@'         { Located $$ (Token (Op At) _)}    OP          { $$@(Located _ (Token (Op (Other [] _)) _))}   QOP         { $$@(Located _ (Token (Op  Other{}   )  _))}@@ -137,19 +146,8 @@ {- If you add additional operators, please update the corresponding    tables in the pretty printer. -} -%nonassoc '=>' %right '->'-%left     'where'-%nonassoc 'then' 'else'-%nonassoc ':'-%nonassoc '=='-%nonassoc '<=' '>=' %right '#'-%left  '+' '-'-%left  '*' '/' '%'-%right '^^'-%right NEG '~'-%left OP QOP %%  @@ -252,7 +250,7 @@ prim_bind               :: { [TopDecl PName] }   : mbDoc 'primitive' name  ':' schema       { mkPrimDecl $1 $3 $5 }   | mbDoc 'primitive' '(' op ')' ':' schema  { mkPrimDecl $1 $4 $7 }-+  | mbDoc 'primitive' 'type' schema ':' kind {% mkPrimTypeDecl $1 $4 $6 }   parameter_decls                      :: { [TopDecl PName] }@@ -284,17 +282,8 @@   : vars_comma ':' schema  { at (head $1,$3) $ DSignature (reverse $1) $3   }   | ipat '=' expr          { at ($1,$3) $ DPatBind $1 $3                    }   | '(' op ')' '=' expr    { at ($1,$5) $ DPatBind (PVar $2) $5             }-  | var apats '=' expr     { at ($1,$4) $-                             DBind $ Bind { bName      = $1-                                          , bParams    = reverse $2-                                          , bDef       = at $4 (Located emptyRange (DExpr $4))-                                          , bSignature = Nothing-                                          , bPragmas   = []-                                          , bMono      = False-                                          , bInfix     = False-                                          , bFixity    = Nothing-                                          , bDoc       = Nothing-                                          } }+  | var apats_indices '=' expr+                           { at ($1,$4) $ mkIndexedDecl $1 $2 $4 }    | apat pat_op apat '=' expr                            { at ($1,$5) $@@ -312,11 +301,15 @@   | 'type' name '=' type   {% at ($1,$4) `fmap` mkTySyn $2 [] $4 }   | 'type' name tysyn_params '=' type                            {% at ($1,$5) `fmap` mkTySyn $2 (reverse $3) $5  }+  | 'type' tysyn_param op tysyn_param '=' type+                           {% at ($1,$6) `fmap` mkTySyn $3 [$2, $4] $6 }    | 'type' 'constraint' name '=' type                            {% at ($2,$5) `fmap` mkPropSyn $3 [] $5 }   | 'type' 'constraint' name tysyn_params '=' type                            {% at ($2,$6) `fmap` mkPropSyn $3 (reverse $4) $6 }+  | 'type' 'constraint' tysyn_param op tysyn_param '=' type+                           {% at ($2,$7) `fmap` mkPropSyn $4 [$3, $5] $7 }    | 'infixl' NUM ops       {% mkFixity LeftAssoc  $2 (reverse $3) }   | 'infixr' NUM ops       {% mkFixity RightAssoc $2 (reverse $3) }@@ -325,17 +318,7 @@  let_decl                :: { Decl PName }   : 'let' ipat '=' expr          { at ($2,$4) $ DPatBind $2 $4                    }-  | 'let' name apats '=' expr    { at ($2,$5) $-                                   DBind $ Bind { bName      = $2-                                                , bParams    = reverse $3-                                                , bDef       = at $5 (Located emptyRange (DExpr $5))-                                                , bSignature = Nothing-                                                , bPragmas   = []-                                                , bMono      = False-                                                , bInfix     = False-                                                , bFixity    = Nothing-                                                , bDoc       = Nothing-                                                } }+  | 'let' name apats_indices '=' expr    { at ($2,$5) $ mkIndexedDecl $2 $3 $5 }  newtype                 :: { Newtype PName }   : 'newtype' qname '=' newtype_body@@ -355,14 +338,22 @@   : name                      { $1 }   | '(' op ')'                { $2 } -apats                     :: { [Pattern PName] }+apats                   :: { [Pattern PName] }   : apat                   { [$1] }-  | apats1 apat            { $2 : $1 }+  | apats apat             { $2 : $1 } -apats1                   :: { [Pattern PName]  }-  : apat                    { [$1]       }-  | apats1 apat             { $2 : $1    }+indices                 :: { [Pattern PName] }+  : '@' indices1           { $2 }+  | {- empty -}            { [] } +indices1                :: { [Pattern PName] }+  : apat                   { [$1] }+  | indices1 '@' apat      { $3 : $1 }++apats_indices           :: { ([Pattern PName], [Pattern PName]) }+  : apats indices          { ($1, $2) }+  | '@' indices1           { ([], $2) }+ decls                   :: { [Decl PName] }   : decl ';'               { [$1] }   | decls decl ';'         { $2 : $1 }@@ -380,43 +371,9 @@   : expr                   { ExprInput $1 }   | let_decl               { LetInput $1 } ------------------------------------------------------------------------------------ if a then b else c : [10] --expr                             :: { Expr PName }-  : cexpr                           { $1 }-  | expr 'where' '{' '}'            { at ($1,$4) $ EWhere $1 []           }-  | expr 'where' '{' decls '}'      { at ($1,$5) $ EWhere $1 (reverse $4) }-  | expr 'where' 'v{' 'v}'          { at ($1,$2) $ EWhere $1 []           }-  | expr 'where' 'v{' vdecls 'v}'   { at ($1,$4) $ EWhere $1 (reverse $4) }-  | error                           {% expected "an expression" }--ifBranches                       :: { [(Expr PName, Expr PName)] }-  : ifBranch                        { [$1] }-  | ifBranches '|' ifBranch         { $3 : $1 }--ifBranch                         :: { (Expr PName, Expr PName) }-  : expr 'then' expr                { ($1, $3) }--cexpr                            :: { Expr PName }-  : sig_expr                        { $1 }-  | 'if' ifBranches 'else' cexpr    { at ($1,$4) $ mkIf (reverse $2) $4 }-  | '\\' apats '->' cexpr           { at ($1,$4) $ EFun (reverse $2) $4 }--sig_expr                         :: { Expr PName }-  : iexpr                           { $1 }-  | iexpr ':' type                  { at ($1,$3) $ ETyped $1 $3 }--iexpr                            :: { Expr PName }-  : expr10                          { $1 }-  | iexpr qop expr10                { binOp $1 $2 $3 }--expr10                           :: { Expr PName }-  : aexprs                          { mkEApp $1 }--  | '-' expr10 %prec NEG            { at ($1,$2) $ ENeg $2 }-  | '~' expr10                      { at ($1,$2) $ EComplement $2 }+--------------------------------------------------------------------------------+-- Operators  qop                              :: { LPName }   : op                              { $1 }@@ -426,6 +383,7 @@ op                               :: { LPName }   : pat_op                          { $1 }   | '#'                             { Located $1 $ mkUnqual $ mkInfix "#" }+  | '@'                             { Located $1 $ mkUnqual $ mkInfix "@" }  pat_op                           :: { LPName }   : other_op                        { $1 }@@ -442,15 +400,81 @@   : OP                              { let Token (Op (Other [] str)) _ = thing $1                                        in mkUnqual (mkInfix str) A.<$ $1 } - ops                     :: { [LPName] }   : op                     { [$1] }   | ops ',' op             { $3 : $1 } +++--------------------------------------------------------------------------------+-- Expressions+++expr                          :: { Expr PName }+  : exprNoWhere                  { $1 }+  | expr 'where' whereClause     { at ($1,$3) (EWhere $1 (thing $3)) }++-- | An expression without a `where` clause+exprNoWhere                    :: { Expr PName }+  : simpleExpr qop longRHS        { at ($1,$3) (binOp $1 $2 $3) }+  | longRHS                       { $1 }+  | typedExpr                     { $1 }++whereClause                    :: { Located [Decl PName] }+  : '{' '}'                       { Located (rComb $1 $2) [] }+  | '{' decls '}'                 { Located (rComb $1 $3) (reverse $2) }+  | 'v{' 'v}'                     { Located (rComb $1 $2) [] }+  | 'v{' vdecls 'v}'              { let l2 = fromMaybe $3 (getLoc $2)+                                    in Located (rComb $1 l2) (reverse $2) }++-- An expression with a type annotation+typedExpr                      :: { Expr PName }+  : simpleExpr ':' type           { at ($1,$3) (ETyped $1 $3) }++-- A possibly infix expression (no where, no long application, no type annot)+simpleExpr                     :: { Expr PName }+  : simpleExpr qop simpleRHS      { at ($1,$3) (binOp $1 $2 $3) }+  | simpleRHS                     { $1 }++-- An expression without an obvious end marker+longExpr                       :: { Expr PName }+  : 'if' ifBranches 'else' exprNoWhere   { at ($1,$4) $ mkIf (reverse $2) $4 }+  | '\\' apats '->' exprNoWhere          { at ($1,$4) $ EFun (reverse $2) $4 }++ifBranches                     :: { [(Expr PName, Expr PName)] }+  : ifBranch                      { [$1] }+  | ifBranches '|' ifBranch       { $3 : $1 }++ifBranch                       :: { (Expr PName, Expr PName) }+  : expr 'then' expr              { ($1, $3) }++simpleRHS                      :: { Expr PName }+  : '-' simpleApp                 { at ($1,$2) (ENeg $2) }+  | '~' simpleApp                 { at ($1,$2) (EComplement $2) }+  | simpleApp                     { $1 }++longRHS                        :: { Expr PName }+  : '-' longApp                   { at ($1,$2) (ENeg $2) }+  | '~' longApp                   { at ($1,$2) (EComplement $2) }+  | longApp                       { $1 }+++-- Prefix application expression, ends with an atom.+simpleApp                      :: { Expr PName }+  : aexprs                        { mkEApp $1 }++-- Prefix application expression, may end with a long expression+longApp                        :: { Expr PName }+  : simpleApp longExpr            { at ($1,$2) (EApp $1 $2) }+  | longExpr                      { $1 }+  | simpleApp                     { $1 }+ aexprs                         :: { [Expr PName] }-  : aexpr                         { [$1]    }+  : aexpr                         { [$1] }   | aexprs aexpr                  { $2 : $1 } ++-- Expression atom (needs no parens) aexpr                          :: { Expr PName }   : no_sel_aexpr                  { $1 }   | sel_expr                      { $1 }@@ -461,6 +485,7 @@   | NUM                           { at $1 $ numLit (tokenType (thing $1))  }   | STRLIT                        { at $1 $ ELit $ ECString $ getStr $1    }   | CHARLIT                       { at $1 $ ELit $ ECNum (getNum $1) CharLit }+  | '_'                           { at $1 $ EVar $ mkUnqual $ mkIdent "_" }    | '(' expr ')'                  { at ($1,$3) $ EParens $2                }   | '(' tuple_exprs ')'           { at ($1,$3) $ ETuple (reverse $2)       }@@ -476,9 +501,6 @@   | '<|'            '|>'          {% mkPoly (rComb $1 $2) [] }   | '<|' poly_terms '|>'          {% mkPoly (rComb $1 $3) $2 } --  -- | error                           {%^ customError "expr" }- sel_expr                       :: { Expr PName }   : no_sel_aexpr '.' selector     { at ($1,$3) $ ESel $1 (thing $3)        }   | sel_expr '.' selector         { at ($1,$3) $ ESel $1 (thing $3)        }@@ -512,8 +534,10 @@ field_expr             :: { UpdField PName }   : selector field_how expr     { UpdField $2 [$1] $3 }   | sels field_how expr         { UpdField $2 $1 $3 }-  | sels apats field_how expr   { UpdField $3 $1 (EFun (reverse $2) $4) }-  | selector apats field_how expr   { UpdField $3 [$1] (EFun (reverse $2) $4) }+  | sels apats_indices field_how expr+                                { UpdField $3 $1 (mkIndexedExpr $2 $4) }+  | selector apats_indices field_how expr+                                { UpdField $3 [$1] (mkIndexedExpr $2 $4) }  field_how :: { UpdHow }   : '='                          { UpdSet }@@ -602,12 +626,17 @@   | '{' schema_params '}'         { Located (rComb $1 $3) (reverse $2) }  schema_quals                   :: { Located [Prop PName] }+  : schema_quals schema_qual      { at ($1,$2) $ fmap (++ thing $2) $1 }+  | schema_qual                   { $1 }++schema_qual                    :: { Located [Prop PName] }   : type '=>'                     {% fmap (\x -> at (x,$2) x) (mkProp $1) } -kind                             :: { Located Kind      }-  : '#'                             { Located $1 KNum   }-  | '*'                             { Located $1 KType  }-  | kind '->' kind                  { combLoc KFun $1 $3 }+kind                           :: { Located Kind      }+  : '#'                           { Located $1 KNum   }+  | '*'                           { Located $1 KType  }+  | 'Prop'                        { Located $1 KProp  }+  | kind '->' kind                { combLoc KFun $1 $3 }  schema_param                   :: { TParam PName }   : ident                         {% mkTParam $1 Nothing           }@@ -625,18 +654,15 @@   : tysyn_param                  { [$1]      }   | tysyn_params tysyn_param     { $2 : $1   } -type                           :: { Type PName                                                 }-  : app_type '->' type            { at ($1,$3) $ TFun $1 $3                                    }-  | type op app_type              { at ($1,$3) $ TInfix $1 $2 defaultFixity $3 }-  | app_type                      { $1                                                         }+type                           :: { Type PName              }+  : infix_type '->' type          { at ($1,$3) $ TFun $1 $3 }+  | infix_type                    { $1                      } -app_type                       :: { Type PName }-  -- : 'lg2'   atype                 { at ($1,$2) $ TApp TCLg2   [$2]    }-  -- | 'lengthFromThenTo' atype atype-  --                      atype      { at ($1,$4) $ TApp TCLenFromThenTo [$2,$3,$4] }-  -- | 'min'   atype atype           { at ($1,$3) $ TApp TCMin   [$2,$3] }-  -- | 'max'   atype atype           { at ($1,$3) $ TApp TCMax   [$2,$3] }+infix_type                     :: { Type PName }+  : infix_type op app_type        { at ($1,$3) $ TInfix $1 $2 defaultFixity $3 }+  | app_type                      { $1                                         } +app_type                       :: { Type PName }   : dimensions atype              { at ($1,$2) $ foldr TSeq $2 (reverse (thing $1)) }   | qname atypes                  { at ($1,head $2)                                      $ TUser (thing $1) (reverse $2) }@@ -644,6 +670,7 @@  atype                          :: { Type PName }   : qname                         { at $1 $ TUser (thing $1) []        }+  | '(' qop ')'                   { at $1 $ TUser (thing $2) []        }   | NUM                           { at $1 $ TNum  (getNum $1)          }   | CHARLIT                       { at $1 $ TChar (toEnum $ fromInteger                                                           $ getNum $1) }@@ -678,7 +705,7 @@ ident              :: { Located Ident }   : IDENT             { let Token (Ident _ str) _ = thing $1                          in $1 { thing = mkIdent str } }-  | 'x'               { Located { srcRange = $1, thing = mkIdent "x" }}+  | 'x'               { Located { srcRange = $1, thing = mkIdent "x" } }   | 'private'         { Located { srcRange = $1, thing = mkIdent "private" } }   | 'as'              { Located { srcRange = $1, thing = mkIdent "as" } }   | 'hiding'          { Located { srcRange = $1, thing = mkIdent "hiding" } }

@@ -31,6 +31,10 @@   , Kind(..)   , Type(..)   , Prop(..)+  , tsName+  , psName+  , tsFixity+  , psFixity      -- * Declarations   , Module(..)@@ -48,6 +52,7 @@   , TopLevel(..)   , Import(..), ImportSpec(..)   , Newtype(..)+  , PrimType(..)   , ParameterType(..)   , ParameterFun(..) @@ -77,7 +82,6 @@ import Cryptol.Parser.Name import Cryptol.Parser.Position import Cryptol.Parser.Selector-import Cryptol.TypeCheck.Type (TCon(..)) import Cryptol.Utils.Ident import Cryptol.Utils.PP @@ -128,6 +132,7 @@  data TopDecl name =     Decl (TopLevel (Decl name))+  | DPrimType (TopLevel (PrimType name))   | TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t   | Include (Located FilePath)          -- ^ @include File@   | DParameterType (ParameterType name) -- ^ @parameter type T : #@@@ -180,12 +185,26 @@                 | Only   [Ident]                   deriving (Eq, Show, Generic, NFData) -data TySyn n  = TySyn (Located n) [TParam n] (Type n)+-- The 'Maybe Fixity' field is filled in by the NoPat pass.+data TySyn n = TySyn (Located n) (Maybe Fixity) [TParam n] (Type n)                 deriving (Eq, Show, Generic, NFData, Functor) -data PropSyn n = PropSyn (Located n) [TParam n] [Prop n]+-- The 'Maybe Fixity' field is filled in by the NoPat pass.+data PropSyn n = PropSyn (Located n) (Maybe Fixity) [TParam n] [Prop n]                  deriving (Eq, Show, Generic, NFData, Functor) +tsName :: TySyn name -> Located name+tsName (TySyn lqn _ _ _) = lqn++psName :: PropSyn name -> Located name+psName (PropSyn lqn _ _ _) = lqn++tsFixity :: TySyn name -> Maybe Fixity+tsFixity (TySyn _ f _ _) = f++psFixity :: PropSyn name -> Maybe Fixity+psFixity (PropSyn _ f _ _) = f+ {- | Bindings.  Notes:      * The parser does not associate type signatures and pragmas with@@ -225,6 +244,15 @@                             , nBody   :: [Named (Type name)] -- ^ Constructor                             } deriving (Eq, Show, Generic, NFData) +-- | A declaration for a type with no implementation.+data PrimType name = PrimType { primTName :: Located name+                              , primTKind :: Located Kind+                              , primTCts  :: ([TParam name], [Prop name])+                                -- ^ parameters are in the order used+                                -- by the type constructor.+                              , primTFixity :: Maybe Fixity+                              } deriving (Show,Generic,NFData)+ -- | Input at the REPL, which can either be an expression or a @let@ -- statement. data ReplInput name = ExprInput (Expr name)@@ -262,12 +290,14 @@               | ELit Literal                    -- ^ @ 0x10 @               | ENeg (Expr n)                   -- ^ @ -1 @               | EComplement (Expr n)            -- ^ @ ~1 @+              | EGenerate (Expr n)              -- ^ @ generate f @               | ETuple [Expr n]                 -- ^ @ (1,2,3) @               | ERecord [Named (Expr n)]        -- ^ @ { x = 1, y = 2 } @               | ESel (Expr n) Selector          -- ^ @ e.l @               | EUpd (Maybe (Expr n)) [ UpdField n ]  -- ^ @ { r | x = e } @               | EList [Expr n]                  -- ^ @ [1,2,3] @-              | EFromTo (Type n) (Maybe (Type n)) (Type n) -- ^ @[1, 5 ..  117 ] @+              | EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n))+                                                -- ^ @ [1, 5 .. 117 : t] @               | EInfFrom (Expr n) (Maybe (Expr n))-- ^ @ [1, 3 ...] @               | EComp (Expr n) [[Match n]]      -- ^ @ [ 1 | x <- xs ] @               | EApp (Expr n) (Expr n)          -- ^ @ f x @@@ -315,7 +345,7 @@ data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range)   deriving (Eq, Show, Generic, NFData, Functor) -data Kind = KNum | KType | KFun Kind Kind+data Kind = KProp | KNum | KType | KFun Kind Kind   deriving (Eq, Show, Generic, NFData)  data TParam n = TParam { tpName  :: n@@ -330,16 +360,6 @@             | TNum Integer            -- ^ @10@             | TChar Char              -- ^ @'a'@             | TUser n [Type n]        -- ^ A type variable or synonym--            | TApp TCon [Type n]-              -- ^ @2 + x@-              -- Note that the parser never produces these; instead it-              -- produces a "TUser" value.  The "TApp" is introduced by-              -- the renamer when it spots built-in functions.-              -- XXX: We should just add primitive declarations for the-              -- built-in type functions, and simplify all this.--             | TRecord [Named (Type n)]-- ^ @{ x : [8], y : [32] }@             | TTuple [Type n]         -- ^ @([8], [32])@             | TWild                   -- ^ @_@, just some type.@@ -348,21 +368,9 @@             | TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @               deriving (Eq, Show, Generic, NFData, Functor) --data Prop n   = CFin (Type n)             -- ^ @ fin x   @-              | CEqual (Type n) (Type n)  -- ^ @ x == 10 @-              | CNeq (Type n) (Type n)    -- ^ @ x != 10 @-              | CGeq (Type n) (Type n)    -- ^ @ x >= 10 @-              | CZero (Type n)            -- ^ @ Zero a  @-              | CLogic (Type n)           -- ^ @ Logic a @-              | CArith (Type n)           -- ^ @ Arith a @-              | CCmp (Type n)             -- ^ @ Cmp a @-              | CSignedCmp (Type n)       -- ^ @ SignedCmp a @-              | CLiteral (Type n) (Type n)-- ^ @ Literal val a @-              | CUser n [Type n]          -- ^ Constraint synonym-              | CLocated (Prop n) Range   -- ^ Location information-              | CType (Type n)            -- ^ After parsing-                deriving (Eq, Show, Generic, NFData, Functor)+-- | A 'Prop' is a 'Type' that represents a type constraint.+newtype Prop n = CType (Type n)+  deriving (Eq, Show, Generic, NFData, Functor)   --------------------------------------------------------------------------------@@ -397,16 +405,6 @@   dropLoc (TLocated e _) = dropLoc e   dropLoc e              = e -instance HasLoc (Prop name) where-  getLoc (CLocated _ r) = Just r-  getLoc _              = Nothing--instance AddLoc (Prop name) where-  addLoc = CLocated--  dropLoc (CLocated e _) = dropLoc e-  dropLoc e              = e- instance AddLoc (Pattern name) where   addLoc = PLocated @@ -452,12 +450,16 @@ instance HasLoc (TopDecl name) where   getLoc td = case td of     Decl tld    -> getLoc tld+    DPrimType pt -> getLoc pt     TDNewtype n -> getLoc n     Include lfp -> getLoc lfp     DParameterType d -> getLoc d     DParameterFun d  -> getLoc d     DParameterConstraint d -> getLoc d +instance HasLoc (PrimType name) where+  getLoc pt = Just (rComb (srcRange (primTName pt)) (srcRange (primTKind pt)))+ instance HasLoc (ParameterType name) where   getLoc a = getLoc (ptName a) @@ -511,6 +513,7 @@   ppPrec _ top_decl =     case top_decl of       Decl    d   -> pp d+      DPrimType p -> pp p       TDNewtype n -> pp n       Include l   -> text "include" <+> text (show (thing l))       DParameterFun d -> pp d@@ -522,6 +525,10 @@                        []  -> "()"                        xs  -> parens (hsep (punctuate comma xs)) +instance (Show name, PPName name) => PP (PrimType name) where+  ppPrec _ pt =+    "primitive" <+> "type" <+> pp (primTName pt) <+> ":" <+> pp (primTKind pt)+ instance (Show name, PPName name) => PP (ParameterType name) where   ppPrec _ a = text "parameter" <+> text "type" <+>                ppPrefixName (ptName a) <+> text ":" <+> pp (ptKind a)@@ -603,11 +610,12 @@   instance PPName name => PP (TySyn name) where-  ppPrec _ (TySyn x xs t) = text "type" <+> ppL x <+> fsep (map (ppPrec 1) xs)-                                        <+> text "=" <+> pp t+  ppPrec _ (TySyn x _ xs t) =+    text "type" <+> ppL x <+> fsep (map (ppPrec 1) xs)+                <+> text "=" <+> pp t  instance PPName name => PP (PropSyn name) where-  ppPrec _ (PropSyn x xs ps) =+  ppPrec _ (PropSyn x _ xs ps) =     text "constraint" <+> ppL x <+> fsep (map (ppPrec 1) xs)                       <+> text "=" <+> parens (commaSep (map pp ps)) @@ -684,12 +692,14 @@        ENeg x        -> wrap n 3 (text "-" <.> ppPrec 4 x)       EComplement x -> wrap n 3 (text "~" <.> ppPrec 4 x)+      EGenerate x   -> wrap n 3 (text "generate" <+> ppPrec 4 x)        ETuple es     -> parens (commaSep (map pp es))       ERecord fs    -> braces (commaSep (map (ppNamed "=") fs))       EList es      -> brackets (commaSep (map pp es))-      EFromTo e1 e2 e3 -> brackets (pp e1 <.> step <+> text ".." <+> pp e3)+      EFromTo e1 e2 e3 t1 -> brackets (pp e1 <.> step <+> text ".." <+> end)         where step = maybe empty (\e -> comma <+> pp e) e2+              end = maybe (pp e3) (\t -> pp e3 <+> colon <+> pp t) t1       EInfFrom e1 e2 -> brackets (pp e1 <.> step <+> text "...")         where step = maybe empty (\e -> comma <+> pp e) e2       EComp e mss   -> brackets (pp e <+> vcat (map arm mss))@@ -774,22 +784,24 @@ instance PP Kind where   ppPrec _ KType  = text "*"   ppPrec _ KNum   = text "#"+  ppPrec _ KProp  = text "@"   ppPrec n (KFun k1 k2) = wrap n 1 (ppPrec 1 k1 <+> "->" <+> ppPrec 0 k2)  -- | "Conversational" printing of kinds (e.g., to use in error messages) cppKind :: Kind -> Doc cppKind KType     = text "a value type" cppKind KNum      = text "a numeric type"+cppKind KProp     = text "a constraint type" cppKind (KFun {}) = text "a type-constructor type"  instance PPName name => PP (TParam name) where   ppPrec n (TParam p Nothing _)   = ppPrec n p   ppPrec n (TParam p (Just k) _)  = wrap n 1 (pp p <+> text ":" <+> pp k) --- 4: wrap [_] t--- 3: wrap application--- 2: wrap function--- 1:+-- 4: atomic type expression+-- 3: [_]t or application+-- 2: infix type+-- 1: function type instance PPName name => PP (Type name) where   ppPrec n ty =     case ty of@@ -803,16 +815,9 @@       TSeq t1 t2     -> optParens (n > 3)                       $ brackets (pp t1) <.> ppPrec 3 t2 -      _ | Just tinf <- isInfix ty ->-              optParens (n > 2)-              $ ppInfix 2 isInfix tinf--      TApp f ts      -> optParens (n > 2)-                      $ pp f <+> fsep (map (ppPrec 4) ts)-       TUser f []     -> ppPrefixName f -      TUser f ts     -> optParens (n > 2)+      TUser f ts     -> optParens (n > 3)                       $ ppPrefixName f <+> fsep (map (ppPrec 4) ts)        TFun t1 t2     -> optParens (n > 1)@@ -822,32 +827,12 @@        TParens t      -> parens (pp t) -      TInfix t1 o _ t2 -> optParens (n > 0)-                        $ sep [ppPrec 2 t1 <+> ppInfixName o, ppPrec 1 t2]+      TInfix t1 o _ t2 -> optParens (n > 2)+                        $ sep [ppPrec 2 t1 <+> ppInfixName o, ppPrec 3 t2] -   where-   isInfix (TApp ieOp [ieLeft, ieRight]) = do-     (ieAssoc,iePrec) <- ppNameFixity ieOp-     return Infix { .. }-   isInfix _ = Nothing  instance PPName name => PP (Prop name) where-  ppPrec n prop =-    case prop of-      CFin t         -> text "fin"   <+> ppPrec 4 t-      CZero t        -> text "Zero"  <+> ppPrec 4 t-      CLogic t       -> text "Logic" <+> ppPrec 4 t-      CArith t       -> text "Arith" <+> ppPrec 4 t-      CCmp t         -> text "Cmp"   <+> ppPrec 4 t-      CSignedCmp t   -> text "SignedCmp" <+> ppPrec 4 t-      CLiteral t1 t2 -> text "Literal" <+> ppPrec 4 t1 <+> ppPrec 4 t2-      CEqual t1 t2   -> ppPrec 2 t1 <+> text "==" <+> ppPrec 2 t2-      CNeq t1 t2     -> ppPrec 2 t1 <+> text "!=" <+> ppPrec 2 t2-      CGeq t1 t2     -> ppPrec 2 t1 <+> text ">=" <+> ppPrec 2 t2-      CUser f ts     -> optParens (n > 2)-                      $ ppPrefixName f <+> fsep (map (ppPrec 4) ts)-      CLocated c _   -> ppPrec n c-      CType t        -> ppPrec n t+  ppPrec n (CType t) = ppPrec n t   --------------------------------------------------------------------------------@@ -881,12 +866,16 @@   noPos decl =     case decl of       Decl    x   -> Decl     (noPos x)+      DPrimType t -> DPrimType (noPos t)       TDNewtype n -> TDNewtype(noPos n)       Include x   -> Include  (noPos x)       DParameterFun d  -> DParameterFun (noPos d)       DParameterType d -> DParameterType (noPos d)       DParameterConstraint d -> DParameterConstraint (noPos d) +instance NoPos (PrimType name) where+  noPos x = x+ instance NoPos (ParameterType name) where   noPos a = a @@ -933,38 +922,39 @@   instance NoPos (TySyn name) where-  noPos (TySyn x y z) = TySyn (noPos x) (noPos y) (noPos z)+  noPos (TySyn x f y z) = TySyn (noPos x) f (noPos y) (noPos z)  instance NoPos (PropSyn name) where-  noPos (PropSyn x y z) = PropSyn (noPos x) (noPos y) (noPos z)+  noPos (PropSyn x f y z) = PropSyn (noPos x) f (noPos y) (noPos z)  instance NoPos (Expr name) where   noPos expr =     case expr of-      EVar x        -> EVar     x-      ELit x        -> ELit     x-      ENeg x        -> ENeg     (noPos x)-      EComplement x -> EComplement (noPos x)-      ETuple x      -> ETuple   (noPos x)-      ERecord x     -> ERecord  (noPos x)-      ESel x y      -> ESel     (noPos x) y-      EUpd x y      -> EUpd     (noPos x) (noPos y)-      EList x       -> EList    (noPos x)-      EFromTo x y z -> EFromTo  (noPos x) (noPos y) (noPos z)-      EInfFrom x y  -> EInfFrom (noPos x) (noPos y)-      EComp x y     -> EComp    (noPos x) (noPos y)-      EApp  x y     -> EApp     (noPos x) (noPos y)-      EAppT x y     -> EAppT    (noPos x) (noPos y)-      EIf   x y z   -> EIf      (noPos x) (noPos y) (noPos z)-      EWhere x y    -> EWhere   (noPos x) (noPos y)-      ETyped x y    -> ETyped   (noPos x) (noPos y)-      ETypeVal x    -> ETypeVal (noPos x)-      EFun x y      -> EFun     (noPos x) (noPos y)-      ELocated x _  -> noPos x+      EVar x          -> EVar     x+      ELit x          -> ELit     x+      ENeg x          -> ENeg     (noPos x)+      EComplement x   -> EComplement (noPos x)+      EGenerate x     -> EGenerate (noPos x)+      ETuple x        -> ETuple   (noPos x)+      ERecord x       -> ERecord  (noPos x)+      ESel x y        -> ESel     (noPos x) y+      EUpd x y        -> EUpd     (noPos x) (noPos y)+      EList x         -> EList    (noPos x)+      EFromTo x y z t -> EFromTo  (noPos x) (noPos y) (noPos z) (noPos t)+      EInfFrom x y    -> EInfFrom (noPos x) (noPos y)+      EComp x y       -> EComp    (noPos x) (noPos y)+      EApp  x y       -> EApp     (noPos x) (noPos y)+      EAppT x y       -> EAppT    (noPos x) (noPos y)+      EIf   x y z     -> EIf      (noPos x) (noPos y) (noPos z)+      EWhere x y      -> EWhere   (noPos x) (noPos y)+      ETyped x y      -> ETyped   (noPos x) (noPos y)+      ETypeVal x      -> ETypeVal (noPos x)+      EFun x y        -> EFun     (noPos x) (noPos y)+      ELocated x _    -> noPos x -      ESplit x      -> ESplit (noPos x)-      EParens e     -> EParens (noPos e)-      EInfix x y f z-> EInfix (noPos x) y f (noPos z)+      ESplit x        -> ESplit (noPos x)+      EParens e       -> EParens (noPos e)+      EInfix x y f z  -> EInfix (noPos x) y f (noPos z)  instance NoPos (UpdField name) where   noPos (UpdField h xs e) = UpdField h xs (noPos e)@@ -999,7 +989,6 @@   noPos ty =     case ty of       TWild         -> TWild-      TApp x y      -> TApp     x         (noPos y)       TUser x y     -> TUser    x         (noPos y)       TRecord x     -> TRecord  (noPos x)       TTuple x      -> TTuple   (noPos x)@@ -1013,18 +1002,4 @@       TInfix x y f z-> TInfix (noPos x) y f (noPos z)  instance NoPos (Prop name) where-  noPos prop =-    case prop of-      CEqual  x y   -> CEqual  (noPos x) (noPos y)-      CNeq x y      -> CNeq (noPos x) (noPos y)-      CGeq x y      -> CGeq (noPos x) (noPos y)-      CFin x        -> CFin (noPos x)-      CZero x       -> CZero  (noPos x)-      CLogic x      -> CLogic (noPos x)-      CArith x      -> CArith (noPos x)-      CCmp x        -> CCmp   (noPos x)-      CSignedCmp x  -> CSignedCmp (noPos x)-      CLiteral x y  -> CLiteral (noPos x) (noPos y)-      CUser x y     -> CUser x (noPos y)-      CLocated c _  -> noPos c-      CType t       -> CType (noPos t)+  noPos (CType t) = CType (noPos t)

@@ -17,7 +17,7 @@   , compareFixity   ) where -import Cryptol.Utils.PP (Assoc(..))+import Cryptol.Utils.PP  import GHC.Generics (Generic) import Control.DeepSeq@@ -44,3 +44,7 @@ -- | The fixity used when none is provided. defaultFixity :: Fixity defaultFixity = Fixity LeftAssoc 100++instance PP Fixity where+  ppPrec _ (Fixity assoc level) =+    text "precedence" <+> int level <.> comma <+> pp assoc

@@ -121,6 +121,8 @@ "parameter"               { emit $ KW KW_parameter } "constraint"              { emit $ KW KW_constraint } +"Prop"                    { emit $ KW KW_Prop }+ @num2                     { emitS (numToken 2  . Text.drop 2) } @num8                     { emitS (numToken 8  . Text.drop 2) } @num10                    { emitS (numToken 10 . Text.drop 0) }@@ -164,6 +166,9 @@ -- hash is used as a kind, and as a pattern "#"                       { emit  (Op   Hash ) } +-- at-sign is used in declaration bindings+"@"                       { emit  (Op   At   ) }+ -- ~ is used for unary complement "~"                       { emit  (Op   Complement) } @@ -240,7 +245,7 @@           , alexPos i')       AlexSkip i' _ -> run i' s       AlexToken i' l act ->-        let txt         = Text.take (fromIntegral l) (input i)+        let txt         = Text.take l (input i)             (mtok,s')   = act cfg (alexPos i) txt s             (rest,pos)  = run i' $! s'         in case mtok of

@@ -214,15 +214,15 @@  -------------------------------------------------------------------------------- numToken :: Integer -> Text -> TokenT-numToken rad ds = Num (toVal ds') (fromInteger rad) (fromIntegral (T.length ds'))+numToken rad ds = Num (toVal ds') (fromInteger rad) (T.length ds')   where   ds' = T.filter (/= '_') ds   toVal = T.foldl' (\x c -> rad * x + fromDigit c) 0  fromDigit :: Char -> Integer fromDigit x'-  | 'a' <= x && x <= 'z'  = fromIntegral (10 + fromEnum x - fromEnum 'a')-  | otherwise             = fromIntegral (fromEnum x - fromEnum '0')+  | 'a' <= x && x <= 'z'  = toInteger (10 + fromEnum x - fromEnum 'a')+  | otherwise             = toInteger (fromEnum x - fromEnum '0')   where x                 = toLower x'  -------------------------------------------------------------------------------@@ -393,13 +393,14 @@               | KW_primitive               | KW_parameter               | KW_constraint+              | KW_Prop                 deriving (Eq, Show, Generic, NFData)  -- | The named operators are a special case for parsing types, and 'Other' is -- used for all other cases that lexed as an operator. data TokenOp  = Plus | Minus | Mul | Div | Exp | Mod               | Equal | LEQ | GEQ-              | Complement | Hash+              | Complement | Hash | At               | Other [T.Text] T.Text                 deriving (Eq, Show, Generic, NFData) 

@@ -23,7 +23,7 @@  -- | The names defined and used by a group of mutually recursive declarations. namesDs :: Ord name => [Decl name] -> ([Located name], Set name)-namesDs ds = (defs, boundNames defs (Set.unions frees))+namesDs ds = (defs, boundLNames defs (Set.unions frees))   where   defs          = concat defss   (defss,frees) = unzip (map namesD ds)@@ -57,15 +57,9 @@     DProp ps        -> [psName ps]     DLocated d _    -> allNamesD d -tsName :: TySyn name -> Located name-tsName (TySyn lqn _ _) = lqn--psName :: PropSyn name -> Located name-psName (PropSyn lqn _ _) = lqn- -- | The names defined and used by a single binding. namesB :: Ord name => Bind name -> ([Located name], Set name)-namesB b = ([bName b], boundNames (namesPs (bParams b)) (namesDef (thing (bDef b))))+namesB b = ([bName b], boundLNames (namesPs (bParams b)) (namesDef (thing (bDef b))))   namesDef :: Ord name => BindDef name -> Set name@@ -81,25 +75,26 @@     ELit _        -> Set.empty     ENeg e        -> namesE e     EComplement e -> namesE e+    EGenerate e   -> namesE e     ETuple es     -> Set.unions (map namesE es)     ERecord fs    -> Set.unions (map (namesE . value) fs)     ESel e _      -> namesE e     EUpd mb fs    -> let e = maybe Set.empty namesE mb                      in Set.unions (e : map namesUF fs)     EList es      -> Set.unions (map namesE es)-    EFromTo _ _ _ -> Set.empty+    EFromTo{}     -> Set.empty     EInfFrom e e' -> Set.union (namesE e) (maybe Set.empty namesE e')     EComp e arms  -> let (dss,uss) = unzip (map namesArm arms)-                     in Set.union (boundNames (concat dss) (namesE e))+                     in Set.union (boundLNames (concat dss) (namesE e))                                   (Set.unions uss)     EApp e1 e2    -> Set.union (namesE e1) (namesE e2)     EAppT e _     -> namesE e     EIf e1 e2 e3  -> Set.union (namesE e1) (Set.union (namesE e2) (namesE e3))     EWhere  e ds  -> let (bs,xs) = namesDs ds-                     in Set.union (boundNames bs (namesE e)) xs+                     in Set.union (boundLNames bs (namesE e)) xs     ETyped e _    -> namesE e     ETypeVal _    -> Set.empty-    EFun ps e     -> boundNames (namesPs ps) (namesE e)+    EFun ps e     -> boundLNames (namesPs ps) (namesE e)     ELocated e _  -> namesE e      ESplit e      -> namesE e@@ -136,60 +131,25 @@ namesArm = foldr combine ([],Set.empty) . map namesM   where combine (ds1,fs1) (ds2,fs2) =           ( filter ((`notElem` map thing ds2) . thing) ds1 ++ ds2-          , Set.union fs1 (boundNames ds1 fs2)+          , Set.union fs1 (boundLNames ds1 fs2)           )  -- | Remove some defined variables from a set of free variables.-boundNames :: Ord name => [Located name] -> Set name -> Set name-boundNames bs xs = Set.difference xs (Set.fromList (map thing bs))+boundLNames :: Ord name => [Located name] -> Set name -> Set name+boundLNames = boundNames . map thing +-- | Remove some defined variables from a set of free variables.+boundNames :: Ord name => [name] -> Set name -> Set name+boundNames = boundNamesSet . Set.fromList --- | Given the set of type variables that are in scope,--- compute the type synonyms used by a type.-namesT :: Ord name => Set name -> Type name -> Set name-namesT vs = go-  where-  go ty =-    case ty of-      TWild         -> Set.empty-      TFun t1 t2    -> Set.union (go t1) (go t2)-      TSeq t1 t2    -> Set.union (go t1) (go t2)-      TBit          -> Set.empty-      TNum _        -> Set.empty-      TChar _       -> Set.empty-      TApp _ ts     -> Set.unions (map go ts)-      TTuple ts     -> Set.unions (map go ts)-      TRecord fs    -> Set.unions (map (go . value) fs)-      TLocated t _  -> go t-      TUser x [] | x `Set.member` vs-                    -> Set.empty-      TUser x ts    -> Set.insert x (Set.unions (map go ts))+-- | Remove some defined variables from a set of free variables.+boundNamesSet :: Ord name => Set name -> Set name -> Set name+boundNamesSet bs xs = Set.difference xs bs -      TParens t     -> namesT vs t-      TInfix a _ _ b-> Set.union (namesT vs a) (namesT vs b) --- | Given the set of type variables that are in scope,--- compute the type/constraint synonyms used by a prop.-namesC :: Ord name => Set name -> Prop name -> Set name-namesC vs prop =-  case prop of-    CFin t        -> namesT vs t-    CEqual t1 t2  -> Set.union (namesT vs t1) (namesT vs t2)-    CNeq   t1 t2  -> Set.union (namesT vs t1) (namesT vs t2)-    CGeq t1 t2    -> Set.union (namesT vs t1) (namesT vs t2)-    CZero t       -> namesT vs t-    CLogic t      -> namesT vs t-    CArith t      -> namesT vs t-    CCmp t        -> namesT vs t-    CSignedCmp t  -> namesT vs t-    CLiteral t1 t2-> Set.union (namesT vs t1) (namesT vs t2)-    CUser x ts    -> Set.insert x (Set.unions (map (namesT vs) ts))-    CLocated p _  -> namesC vs p-    CType t       -> namesT vs t- -- | The type names defined and used by a group of mutually recursive declarations. tnamesDs :: Ord name => [Decl name] -> ([Located name], Set name)-tnamesDs ds = (defs, boundNames defs (Set.unions frees))+tnamesDs ds = (defs, boundLNames defs (Set.unions frees))   where   defs          = concat defss   (defss,frees) = unzip (map tnamesD ds)@@ -204,8 +164,10 @@     DBind b              -> ([], tnamesB b)     DPatBind _ e         -> ([], tnamesE e)     DLocated d _         -> tnamesD d-    DType (TySyn n ps t) -> ([n], Set.difference (tnamesT t) (Set.fromList (map tpName ps)))-    DProp (PropSyn n ps cs)+    DType (TySyn n _ ps t)+                         -> ([n], Set.difference (tnamesT t)+                                  (Set.fromList (map tpName ps)))+    DProp (PropSyn n _ ps cs)                          -> ([n], Set.difference (Set.unions (map tnamesC cs))                                   (Set.fromList (map tpName ps))) @@ -225,33 +187,36 @@ tnamesE :: Ord name => Expr name -> Set name tnamesE expr =   case expr of-    EVar _        -> Set.empty-    ELit _        -> Set.empty-    ENeg e        -> tnamesE e-    EComplement e -> tnamesE e-    ETuple es     -> Set.unions (map tnamesE es)-    ERecord fs    -> Set.unions (map (tnamesE . value) fs)-    ESel e _      -> tnamesE e-    EUpd mb fs    -> let e = maybe Set.empty tnamesE mb-                     in Set.unions (e : map tnamesUF fs)-    EList es      -> Set.unions (map tnamesE es)-    EFromTo a b c -> Set.union (tnamesT a)-                     (Set.union (maybe Set.empty tnamesT b) (tnamesT c))-    EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e')-    EComp e mss   -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss)))-    EApp e1 e2    -> Set.union (tnamesE e1) (tnamesE e2)-    EAppT e fs    -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs))-    EIf e1 e2 e3  -> Set.union (tnamesE e1) (Set.union (tnamesE e2) (tnamesE e3))-    EWhere  e ds  -> let (bs,xs) = tnamesDs ds-                     in Set.union (boundNames bs (tnamesE e)) xs-    ETyped e t    -> Set.union (tnamesE e) (tnamesT t)-    ETypeVal t    -> tnamesT t-    EFun ps e     -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e)-    ELocated e _  -> tnamesE e+    EVar _          -> Set.empty+    ELit _          -> Set.empty+    ENeg e          -> tnamesE e+    EComplement e   -> tnamesE e+    EGenerate e     -> tnamesE e+    ETuple es       -> Set.unions (map tnamesE es)+    ERecord fs      -> Set.unions (map (tnamesE . value) fs)+    ESel e _        -> tnamesE e+    EUpd mb fs      -> let e = maybe Set.empty tnamesE mb+                       in Set.unions (e : map tnamesUF fs)+    EList es        -> Set.unions (map tnamesE es)+    EFromTo a b c t -> tnamesT a+                       `Set.union` maybe Set.empty tnamesT b+                       `Set.union` tnamesT c+                       `Set.union` maybe Set.empty tnamesT t+    EInfFrom e e'   -> Set.union (tnamesE e) (maybe Set.empty tnamesE e')+    EComp e mss     -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss)))+    EApp e1 e2      -> Set.union (tnamesE e1) (tnamesE e2)+    EAppT e fs      -> Set.union (tnamesE e) (Set.unions (map tnamesTI fs))+    EIf e1 e2 e3    -> Set.union (tnamesE e1) (Set.union (tnamesE e2) (tnamesE e3))+    EWhere  e ds    -> let (bs,xs) = tnamesDs ds+                       in Set.union (boundLNames bs (tnamesE e)) xs+    ETyped e t      -> Set.union (tnamesE e) (tnamesT t)+    ETypeVal t      -> tnamesT t+    EFun ps e       -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e)+    ELocated e _    -> tnamesE e -    ESplit e      -> tnamesE e-    EParens e     -> tnamesE e-    EInfix a _ _ b-> Set.union (tnamesE a) (tnamesE b)+    ESplit e        -> tnamesE e+    EParens e       -> tnamesE e+    EInfix a _ _ b  -> Set.union (tnamesE a) (tnamesE b)  tnamesUF :: Ord name => UpdField name -> Set name tnamesUF (UpdField _ _ e) = tnamesE e@@ -288,18 +253,6 @@ tnamesC :: Ord name => Prop name -> Set name tnamesC prop =   case prop of-    CFin t         -> tnamesT t-    CEqual t1 t2   -> Set.union (tnamesT t1) (tnamesT t2)-    CNeq   t1 t2   -> Set.union (tnamesT t1) (tnamesT t2)-    CGeq t1 t2     -> Set.union (tnamesT t1) (tnamesT t2)-    CZero t        -> tnamesT t-    CLogic t       -> tnamesT t-    CArith t       -> tnamesT t-    CCmp t         -> tnamesT t-    CSignedCmp t   -> tnamesT t-    CLiteral t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)-    CUser x ts     -> Set.insert x (Set.unions (map tnamesT ts))-    CLocated p _   -> tnamesC p     CType t        -> tnamesT t  -- | Compute the type synonyms/type variables used by a type.@@ -312,10 +265,10 @@     TBit          -> Set.empty     TNum _        -> Set.empty     TChar __      -> Set.empty-    TApp _ ts     -> Set.unions (map tnamesT ts)     TTuple ts     -> Set.unions (map tnamesT ts)     TRecord fs    -> Set.unions (map (tnamesT . value) fs)     TLocated t _  -> tnamesT t     TUser x ts    -> Set.insert x (Set.unions (map tnamesT ts))     TParens t     -> tnamesT t-    TInfix a _ _ c-> Set.union (tnamesT a) (tnamesT c)+    TInfix a x _ c-> Set.insert (thing x)+                                (Set.union (tnamesT a) (tnamesT c))

@@ -155,6 +155,7 @@ noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName] noIncTopDecl td = case td of   Decl _     -> return [td]+  DPrimType {} -> pure [td]   TDNewtype _-> return [td]   DParameterType {} -> return [td]   DParameterConstraint {} -> return [td]

@@ -96,7 +96,7 @@          x <- newName          r <- getRange          let len      = length ps-             ty       = TSeq (TNum (fromIntegral len)) TWild+             ty       = TSeq (TNum (toInteger len)) TWild              getN a n = sel a x (ListSel n (Just len))          return (pTy r x ty, zipWith getN as [0..] ++ concat dss) @@ -113,7 +113,7 @@       do (a,ds) <- noPat p          return (PTyped a t, ds) -    -- XXX: Ww can do more with type annotations here+    -- XXX: We can do more with type annotations here     PSplit p1 p2 ->       do (a1,ds1) <- noPat p1          (a2,ds2) <- noPat p2@@ -148,6 +148,7 @@     ELit {}       -> return expr     ENeg e        -> ENeg    <$> noPatE e     EComplement e -> EComplement <$> noPatE e+    EGenerate e   -> EGenerate <$> noPatE e     ETuple es     -> ETuple  <$> mapM noPatE es     ERecord es    -> ERecord <$> mapM noPatF es     ESel e s      -> ESel    <$> noPatE e <*> return s@@ -241,21 +242,28 @@ noPatDs :: [Decl PName] -> NoPatM [Decl PName] noPatDs ds =   do ds1 <- concat <$> mapM noMatchD ds-     let pragmaMap = Map.fromListWith (++) $ concatMap toPragma ds1-         sigMap    = Map.fromListWith (++) $ concatMap toSig ds1-         fixMap    = Map.fromListWith (++) $ concatMap toFixity ds1-     (ds2, (pMap,sMap,fMap,_)) <- runStateT (pragmaMap, sigMap, fixMap, Map.empty)-                                            (annotDs ds1)+     let fixes = Map.fromListWith (++) $ concatMap toFixity ds1+         amap = AnnotMap+           { annPragmas = Map.fromListWith (++) $ concatMap toPragma ds1+           , annSigs    = Map.fromListWith (++) $ concatMap toSig ds1+           , annValueFs = fixes+           , annTypeFs  = fixes+           , annDocs    = Map.empty+           } -     forM_ (Map.toList pMap) $ \(n,ps) ->+     (ds2, AnnotMap { .. }) <- runStateT amap (annotDs ds1)++     forM_ (Map.toList annPragmas) $ \(n,ps) ->        forM_ ps $ \p -> recordError $ PragmaNoBind (p { thing = n }) (thing p) -     forM_ (Map.toList sMap) $ \(n,ss) ->+     forM_ (Map.toList annSigs) $ \(n,ss) ->        do _ <- checkSigs n ss           forM_ ss $ \s -> recordError $ SignatureNoBind (s { thing = n })                                                          (thing s) -     forM_ (Map.toList fMap) $ \(n,fs) ->+     -- Generate an error if a fixity declaration is not used for+     -- either a value-level or type-level operator.+     forM_ (Map.toList (Map.intersection annValueFs annTypeFs)) $ \(n,fs) ->        forM_ fs $ \f -> recordError $ FixityNoBind f { thing = n }       return ds2@@ -267,23 +275,29 @@   do desugared <- concat <$> mapM desugar tds       let allDecls  = map tlValue (decls desugared)-         pragmaMap = Map.fromListWith (++) $ concatMap toPragma allDecls-         sigMap    = Map.fromListWith (++) $ concatMap toSig    allDecls-         fixMap    = Map.fromListWith (++) $ concatMap toFixity allDecls-         docMap    = Map.fromListWith (++) $ concatMap toDocs   (decls tds)+         fixes     = Map.fromListWith (++) $ concatMap toFixity allDecls -     (tds', (pMap,sMap,fMap,_)) <- runStateT (pragmaMap,sigMap,fixMap,docMap)-                                             (annotTopDs desugared)+     let ann = AnnotMap+           { annPragmas = Map.fromListWith (++) $ concatMap toPragma allDecls+           , annSigs    = Map.fromListWith (++) $ concatMap toSig    allDecls+           , annValueFs = fixes+           , annTypeFs  = fixes+           , annDocs    = Map.fromListWith (++) $ concatMap toDocs $ decls tds+          } -     forM_ (Map.toList pMap) $ \(n,ps) ->+     (tds', AnnotMap { .. }) <- runStateT ann (annotTopDs desugared)++     forM_ (Map.toList annPragmas) $ \(n,ps) ->        forM_ ps $ \p -> recordError $ PragmaNoBind (p { thing = n }) (thing p) -     forM_ (Map.toList sMap) $ \(n,ss) ->+     forM_ (Map.toList annSigs) $ \(n,ss) ->        do _ <- checkSigs n ss           forM_ ss $ \s -> recordError $ SignatureNoBind (s { thing = n })                                                          (thing s) -     forM_ (Map.toList fMap) $ \(n,fs) ->+     -- Generate an error if a fixity declaration is not used for+     -- either a value-level or type-level operator.+     forM_ (Map.toList (Map.intersection annValueFs annTypeFs)) $ \(n,fs) ->        forM_ fs $ \f -> recordError $ FixityNoBind f { thing = n }       return tds'@@ -308,19 +322,23 @@  -------------------------------------------------------------------------------- -type AnnotMap = ( Map.Map PName [Located  Pragma       ]-                , Map.Map PName [Located (Schema PName)]-                , Map.Map PName [Located  Fixity       ]-                , Map.Map PName [Located  String       ]-                )+data AnnotMap = AnnotMap+  { annPragmas  :: Map.Map PName [Located  Pragma       ]+  , annSigs     :: Map.Map PName [Located (Schema PName)]+  , annValueFs  :: Map.Map PName [Located  Fixity       ]+  , annTypeFs   :: Map.Map PName [Located  Fixity       ]+  , annDocs     :: Map.Map PName [Located  String       ]+  } +type Annotates a = a -> StateT AnnotMap NoPatM a+ -- | Add annotations to exported declaration groups. -- -- XXX: This isn't quite right: if a signature and binding have different -- export specifications, this will favor the specification of the binding. -- This is most likely the intended behavior, so it's probably fine, but it does -- smell a bit.-annotTopDs :: [TopDecl PName] -> StateT AnnotMap NoPatM [TopDecl PName]+annotTopDs :: Annotates [TopDecl PName] annotTopDs tds =   case tds of @@ -332,18 +350,26 @@                Left _   -> annotTopDs ds                Right d2 -> (Decl (d1 { tlValue = d2 }) :) <$> annotTopDs ds -        -- XXX: Add fixity once we support type-level fixities-        DParameterType {} -> (d :) <$> annotTopDs ds+        DPrimType tl ->+          do pt <- annotPrimType (tlValue tl)+             let d1 = DPrimType tl { tlValue = pt }+             (d1 :) <$> annotTopDs ds++        DParameterType p ->+          do p1 <- annotParameterType p+             (DParameterType p1 :) <$> annotTopDs ds+         DParameterConstraint {} -> (d :) <$> annotTopDs ds+         DParameterFun p ->-          do (ps,ss,fs,ds') <- get+          do AnnotMap { .. } <- get              let rm _ _ = Nothing                  name = thing (pfName p)-             case Map.updateLookupWithKey rm name fs of+             case Map.updateLookupWithKey rm name annValueFs of                (Nothing,_)  -> (d :) <$> annotTopDs ds                (Just f,fs1) ->                  do mbF <- lift (checkFixs name f)-                    set (ps,ss,fs1,ds')+                    set AnnotMap { annValueFs = fs1, .. }                     let p1 = p { pfFixity = mbF }                     (DParameterFun p1 :) <$> annotTopDs ds @@ -354,8 +380,8 @@     [] -> return []  --- | Add annotations, keeping track of which annotation are not yet used up.-annotDs :: [Decl PName] -> StateT AnnotMap NoPatM [Decl PName]+-- | Add annotations, keeping track of which annotations are not yet used up.+annotDs :: Annotates [Decl PName] annotDs (d : ds) =   do ignore <- runExceptionT (annotD d)      case ignore of@@ -363,7 +389,7 @@        Right d1  -> (d1 :) <$> annotDs ds annotDs [] = return [] --- | Add annotations, keeping track of which annotation are not yet used up.+-- | Add annotations, keeping track of which annotations are not yet used up. -- The exception indicates which declarations are no longer needed. annotD :: Decl PName -> ExceptionT () (StateT AnnotMap NoPatM) (Decl PName) annotD decl =@@ -373,34 +399,74 @@     DFixity{}     -> raise ()     DPragma {}    -> raise ()     DPatBind {}   -> raise ()-    DType {}      -> return decl-    DProp {}      -> return decl+    DType tysyn   -> DType <$> lift (annotTySyn tysyn)+    DProp propsyn -> DProp <$> lift (annotPropSyn propsyn)     DLocated d r  -> (`DLocated` r) <$> annotD d  -- | Add pragma/signature annotations to a binding.-annotB :: Bind PName -> StateT AnnotMap NoPatM (Bind PName)+annotB :: Annotates (Bind PName) annotB Bind { .. } =-  do (ps,ss,fs,ds) <- get+  do AnnotMap { .. } <- get      let name       = thing bName          remove _ _ = Nothing-     case ( Map.updateLookupWithKey remove name ps-          , Map.updateLookupWithKey remove name ss-          , Map.updateLookupWithKey remove name fs-          , Map.updateLookupWithKey remove name ds-          ) of-           ( (thisPs, pragmas1), (thisSigs, sigs1), (thisFixes, fixes1), (thisDocs, docs1)) ->-                do s <- lift $ checkSigs name (jn thisSigs)-                   f <- lift $ checkFixs name (jn thisFixes)-                   d <- lift $ checkDocs name (jn thisDocs)-                   set (pragmas1,sigs1,fixes1,docs1)-                   return Bind { bSignature = s-                               , bPragmas = map thing (jn thisPs) ++ bPragmas-                               , bFixity = f-                               , bDoc = d-                               , ..-                               }+         (thisPs    , ps') = Map.updateLookupWithKey remove name annPragmas+         (thisSigs  , ss') = Map.updateLookupWithKey remove name annSigs+         (thisFixes , fs') = Map.updateLookupWithKey remove name annValueFs+         (thisDocs  , ds') = Map.updateLookupWithKey remove name annDocs+     s <- lift $ checkSigs name $ jn thisSigs+     f <- lift $ checkFixs name $ jn thisFixes+     d <- lift $ checkDocs name $ jn thisDocs+     set AnnotMap { annPragmas = ps'+                  , annSigs    = ss'+                  , annValueFs = fs'+                  , annDocs    = ds'+                  , ..+                  }+     return Bind { bSignature = s+                 , bPragmas = map thing (jn thisPs) ++ bPragmas+                 , bFixity = f+                 , bDoc = d+                 , ..+                 }   where jn x = concat (maybeToList x) +annotTyThing :: PName -> StateT AnnotMap NoPatM (Maybe Fixity)+annotTyThing name =+  do AnnotMap { .. } <- get+     let remove _ _ = Nothing+         (thisFixes, ts') = Map.updateLookupWithKey remove name annTypeFs+     f <- lift $ checkFixs name $ concat $ maybeToList thisFixes+     set AnnotMap { annTypeFs = ts', .. }+     pure f+++-- | Add fixity annotations to a type synonym binding.+annotTySyn :: Annotates (TySyn PName)+annotTySyn (TySyn ln _ params rhs) =+  do f <- annotTyThing (thing ln)+     pure (TySyn ln f params rhs)++-- | Add fixity annotations to a constraint synonym binding.+annotPropSyn :: Annotates (PropSyn PName)+annotPropSyn (PropSyn ln _ params rhs) =+  do f <- annotTyThing (thing ln)+     pure (PropSyn ln f params rhs)++-- | Annotate a primitive type declaration.+annotPrimType :: Annotates (PrimType PName)+annotPrimType pt =+  do f <- annotTyThing (thing (primTName pt))+     pure pt { primTFixity = f }++-- | Annotate a module's type parameter.+annotParameterType :: Annotates (ParameterType PName)+annotParameterType pt =+  do f <- annotTyThing (thing (ptName pt))+     pure pt { ptFixity = f }++++ -- | Check for multiple signatures. checkSigs :: PName -> [Located (Schema PName)] -> NoPatM (Maybe (Schema PName)) checkSigs _ []             = return Nothing@@ -517,7 +583,7 @@       SignatureNoBind x s ->         text "At" <+> pp (srcRange x) <.> colon <+>         text "Type signature without a matching binding:"-         $$ nest 2 (pp s)+         $$ nest 2 (pp (thing x) <+> colon <+> pp s)        PragmaNoBind x s ->         text "At" <+> pp (srcRange x) <.> colon <+>

@@ -15,20 +15,12 @@ {-# LANGUAGE OverloadedStrings #-} module Cryptol.Parser.ParserUtils where -import Cryptol.Parser.AST-import Cryptol.Parser.Lexer-import Cryptol.Parser.Position-import Cryptol.Parser.Utils (translateExprToNumT,widthIdent)-import Cryptol.Utils.Ident(packModName)-import Cryptol.Utils.PP-import Cryptol.Utils.Panic- import Data.Maybe(fromMaybe) import Data.Bits(testBit,setBit)-import Control.Monad(liftM,ap,unless)+import Control.Monad(liftM,ap,unless,guard) import           Data.Text(Text) import qualified Data.Text as T-+import qualified Data.Map as Map  import GHC.Generics (Generic) import Control.DeepSeq@@ -36,6 +28,16 @@ import Prelude () import Prelude.Compat ++import Cryptol.Parser.AST+import Cryptol.Parser.Lexer+import Cryptol.Parser.Position+import Cryptol.Parser.Utils (translateExprToNumT,widthIdent)+import Cryptol.Utils.Ident(packModName)+import Cryptol.Utils.PP+import Cryptol.Utils.Panic++ parseString :: Config -> ParseM a -> String -> Either ParseError a parseString cfg p cs = parse cfg p (T.pack cs) @@ -182,7 +184,7 @@ getNum :: Located Token -> Integer getNum l = case thing l of              Token (Num x _ _) _ -> x-             Token (ChrLit x) _  -> fromIntegral (fromEnum x)+             Token (ChrLit x) _  -> toInteger (fromEnum x)              _ -> panic "[Parser] getNum" ["not a number:", show l]  getStr :: Located Token -> String@@ -239,7 +241,6 @@     TChar {}     -> ok     TWild        -> bad "Wildcard types"     TUser {}     -> ok-    TApp {}      -> ok      TParens t    -> validDemotedType rng t     TInfix{}     -> ok@@ -247,6 +248,7 @@   where bad x = errorMessage rng (x ++ " cannot be demoted.")         ok    = return $ at rng ty +-- | Input expression are reversed mkEApp :: [Expr PName] -> Expr PName mkEApp es@(eLast : _) = at (eFirst,eLast) $ foldl EApp f xs   where@@ -284,11 +286,28 @@ binOp :: Expr PName -> Located PName -> Expr PName -> Expr PName binOp x f y = at (x,y) $ EInfix x f defaultFixity y +-- An element type ascription is allowed to appear on one of the arguments. eFromTo :: Range -> Expr PName -> Maybe (Expr PName) -> Expr PName -> ParseM (Expr PName)-eFromTo r e1 e2 e3 = EFromTo <$> exprToNumT r e1-                             <*> mapM (exprToNumT r) e2-                             <*> exprToNumT r e3+eFromTo r e1 e2 e3 =+  case (asETyped e1, asETyped =<< e2, asETyped e3) of+    (Just (e1', t), Nothing, Nothing) -> eFromToType r e1' e2 e3 (Just t)+    (Nothing, Just (e2', t), Nothing) -> eFromToType r e1 (Just e2') e3 (Just t)+    (Nothing, Nothing, Just (e3', t)) -> eFromToType r e1 e2 e3' (Just t)+    (Nothing, Nothing, Nothing) -> eFromToType r e1 e2 e3 Nothing+    _ -> errorMessage r "A sequence enumeration may have at most one element type annotation."+  where+    asETyped (ELocated e _) = asETyped e+    asETyped (ETyped e t) = Just (e, t)+    asETyped _ = Nothing +eFromToType ::+  Range -> Expr PName -> Maybe (Expr PName) -> Expr PName -> Maybe (Type PName) -> ParseM (Expr PName)+eFromToType r e1 e2 e3 t =+  EFromTo <$> exprToNumT r e1+          <*> mapM (exprToNumT r) e2+          <*> exprToNumT r e3+          <*> pure t+ exprToNumT :: Range -> Expr PName -> ParseM (Type PName) exprToNumT r expr =   case translateExprToNumT expr of@@ -297,11 +316,7 @@   where   bad = errorMessage (fromMaybe r (getLoc expr)) $ unlines         [ "The boundaries of .. sequences should be valid numeric types."-        , "The expression `" ++ show (pp expr) ++ "` is not."-        , ""-        , "If you were trying to specify the width of the elements,"-        , "you may add a type annotation outside the sequence. For example:"-        , "   [ 1 .. 10 ] : [_][16]"+        , "The expression `" ++ show expr ++ "` is not."         ]  @@ -352,6 +367,7 @@ changeExport e = map change   where   change (Decl d)      = Decl      d { tlExport = e }+  change (DPrimType t) = DPrimType t { tlExport = e }   change (TDNewtype n) = TDNewtype n { tlExport = e }   change td@Include{}  = td   change (DParameterType {}) = panic "changeExport" ["private type parameter?"]@@ -375,7 +391,7 @@     errorMessage (srcRange ln) "`width` is not a valid type synonym name."    | otherwise =-    return $ DType $ TySyn ln ps b+    return $ DType $ TySyn ln Nothing ps b  mkPropSyn :: Located PName -> [TParam PName] -> Type PName -> ParseM (Decl PName) mkPropSyn ln ps b@@ -383,7 +399,7 @@     errorMessage (srcRange ln) "`width` is not a valid constraint synonym name."    | otherwise =-    DProp . PropSyn ln ps . thing <$> mkProp b+    DProp . PropSyn ln Nothing ps . thing <$> mkProp b  polyTerm :: Range -> Integer -> Integer -> ParseM (Bool, Integer) polyTerm rng k p@@ -420,6 +436,34 @@                                , bDoc        = Nothing                                } +-- NOTE: The lists of patterns are reversed!+mkIndexedDecl ::+  LPName -> ([Pattern PName], [Pattern PName]) -> Expr PName -> Decl PName+mkIndexedDecl f (ps, ixs) e =+  DBind Bind { bName       = f+             , bParams     = reverse ps+             , bDef        = at e (Located emptyRange (DExpr rhs))+             , bSignature  = Nothing+             , bPragmas    = []+             , bMono       = False+             , bInfix      = False+             , bFixity     = Nothing+             , bDoc        = Nothing+             }+  where+    rhs :: Expr PName+    rhs = mkGenerate (reverse ixs) e++-- NOTE: The lists of patterns are reversed!+mkIndexedExpr :: ([Pattern PName], [Pattern PName]) -> Expr PName -> Expr PName+mkIndexedExpr (ps, ixs) body+  | null ps = mkGenerate (reverse ixs) body+  | otherwise = EFun (reverse ps) (mkGenerate (reverse ixs) body)++mkGenerate :: [Pattern PName] -> Expr PName -> Expr PName+mkGenerate pats body =+  foldr (\pat e -> EGenerate (EFun [pat] e)) body pats+ mkIf :: [(Expr PName, Expr PName)] -> Expr PName -> Expr PName mkIf ifThens theElse = foldr addIfThen theElse ifThens     where@@ -431,7 +475,8 @@ -- pass.  This is also the reason we add the doc to the TopLevel constructor, -- instead of just place it on the binding directly.  A better solution might be -- to just have a different constructor for primitives.-mkPrimDecl :: Maybe (Located String) -> LPName -> Schema PName -> [TopDecl PName]+mkPrimDecl ::+  Maybe (Located String) -> LPName -> Schema PName -> [TopDecl PName] mkPrimDecl mbDoc ln sig =   [ exportDecl mbDoc Public     $ DBind Bind { bName      = ln@@ -448,6 +493,73 @@     $ DSignature [ln] sig   ] +mkPrimTypeDecl ::+  Maybe (Located String) ->+  Schema PName ->+  Located Kind ->+  ParseM [TopDecl PName]+mkPrimTypeDecl mbDoc (Forall as qs st ~(Just schema_rng)) finK =+  case splitT schema_rng st of+    Just (n,xs) ->+      do vs <- mapM tpK as+         unless (distinct (map fst vs)) $+            errorMessage schema_rng "Repeated parameterms."+         let kindMap = Map.fromList vs+             lkp v = case Map.lookup (thing v) kindMap of+                       Just (k,tp)  -> pure (k,tp)+                       Nothing ->+                        errorMessage+                            (srcRange v)+                            ("Undefined parameter: " ++ show (pp (thing v)))+         (as',ins) <- unzip <$> mapM lkp xs+         unless (length vs == length xs) $+           errorMessage schema_rng "All parameters should appear in the type."++         let ki = finK { thing = foldr KFun (thing finK) ins }++         pure [ DPrimType TopLevel+                  { tlExport = Public+                  , tlDoc    = mbDoc+                  , tlValue  = PrimType { primTName   = n+                                        , primTKind   = ki+                                        , primTCts    = (as',qs)+                                        , primTFixity = Nothing+                                        }+                 }+              ]++    Nothing -> errorMessage schema_rng "Invalid primitive signature"++  where+  splitT r ty = case ty of+                  TLocated t r1 -> splitT r1 t+                  TUser n ts -> mkT r Located { srcRange = r, thing = n } ts+                  TInfix t1 n _ t2  -> mkT r n [t1,t2]+                  _ -> Nothing++  mkT r n ts = do ts1 <- mapM (isVar r) ts+                  guard (distinct (map thing ts1))+                  pure (n,ts1)++  isVar r ty = case ty of+                 TLocated t r1  -> isVar r1 t+                 TUser n []     -> Just Located { srcRange = r, thing = n }+                 _              -> Nothing++  -- inefficient, but the lists should be small+  distinct xs = case xs of+                  [] -> True+                  x : ys -> not (x `elem` ys) && distinct ys++  tpK tp = case tpKind tp of+             Just k  -> pure (tpName tp, (tp,k))+             Nothing ->+              case tpRange tp of+                Just r -> errorMessage r "Parameters need a kind annotation"+                Nothing -> panic "mkPrimTypeDecl"+                              [ "Missing range on schema parameter." ]++ -- | Fix-up the documentation strings by removing the comment delimiters on each -- end, and stripping out common prefixes on all the remaining lines. mkDoc :: Located Text -> Located String@@ -504,13 +616,12 @@    props r t =     case t of-      TInfix{}       -> infixProp t-      TUser f xs     -> prefixProp r f xs+      TInfix{}       -> return [CType t]+      TUser{}        -> return [CType t]       TTuple ts      -> concat `fmap` mapM (props r) ts       TParens t'     -> props r  t'       TLocated t' r' -> props r' t' -      TApp{}    -> err       TFun{}    -> err       TSeq{}    -> err       TBit{}    -> err@@ -521,32 +632,6 @@      where     err = errorMessage r "Invalid constraint"--  -- we have to delay these until renaming, when we have the fixity table-  -- present-  infixProp t = return [CType t]--  -- these can be translated right away-  prefixProp r f xs-    | i == zeroIdent,      [x] <- xs = return [CLocated (CZero x) r]-    | i == logicIdent,     [x] <- xs = return [CLocated (CLogic x) r]-    | i == arithIdent,     [x] <- xs = return [CLocated (CArith x) r]-    | i == finIdent,       [x] <- xs = return [CLocated (CFin x) r]-    | i == cmpIdent,       [x] <- xs = return [CLocated (CCmp x) r]-    | i == signedCmpIdent, [x] <- xs = return [CLocated (CSignedCmp x) r]-    | i == literalIdent, [x,y] <- xs = return [CLocated (CLiteral x y) r]-    | otherwise                      = return [CLocated (CType (TUser f xs)) r]-    where-    i = getIdent f--zeroIdent, logicIdent, arithIdent, finIdent, cmpIdent, signedCmpIdent, literalIdent :: Ident-zeroIdent      = mkIdent "Zero"-logicIdent     = mkIdent "Logic"-arithIdent     = mkIdent "Arith"-finIdent       = mkIdent "fin"-cmpIdent       = mkIdent "Cmp"-signedCmpIdent = mkIdent "SignedCmp"-literalIdent   = mkIdent "Literal"  -- | Make an ordinary module mkModule :: Located ModName ->

@@ -76,12 +76,10 @@     TupleSel n _  -> packIdent ("_" ++ show n)     ListSel n _   -> packIdent ("__" ++ show n) --- | Show a list of selectors as they appear in a nested selector in an updae+-- | Show a list of selectors as they appear in a nested selector in an update. ppNestedSels :: [Selector] -> Doc ppNestedSels = hcat . intersperse "." . map ppS   where ppS s = case s of                   RecordSel i _ -> text (unpackIdent i)                   TupleSel n _ -> int n                   ListSel n _  -> brackets (int n) -- not in source--

@@ -99,12 +99,17 @@     | otherwise         = fenced op (l : current) ls  -  isOpenFence l  | "```cryptol" == l'         = Just Code-                 | "```"        == l'         = Just Code-                 | "```" `Text.isPrefixOf` l' = Just Comment-                 | otherwise                  = Nothing+  isOpenFence l+    | "```" `Text.isPrefixOf` l' =+      Just $ case Text.drop 3 l' of+               l'' | "cryptol" `Text.isPrefixOf` l'' -> Code+                   | isBlank l''                     -> Code+                   | otherwise                       -> Comment++    | otherwise = Nothing     where     l' = Text.dropWhile isSpace l+   isCloseFence l = "```" `Text.isPrefixOf` l   isBlank l      = Text.all isSpace l   isCodeLine l   = "\t" `Text.isPrefixOf` l || "    " `Text.isPrefixOf` l

@@ -17,18 +17,20 @@   ) where  import Cryptol.Parser.AST-import Cryptol.Prims.Syntax-import Cryptol.TypeCheck.Type (TCon(TF))   widthIdent :: Ident widthIdent  = mkIdent "width" +underIdent :: Ident+underIdent = mkIdent "_"+ translateExprToNumT :: Expr PName -> Maybe (Type PName) translateExprToNumT expr =   case expr of     ELocated e r -> (`TLocated` r) `fmap` translateExprToNumT e-    EVar n | getIdent n == widthIdent -> mkFun TCWidth+    EVar n | getIdent n == widthIdent -> pure (TUser n [])+           | getIdent n == underIdent -> pure TWild     EVar x       -> return (TUser x [])     ELit x       -> cvtLit x     EApp e1 e2   -> do t1 <- translateExprToNumT e1@@ -48,11 +50,8 @@   tApp ty t =     case ty of       TLocated t1 r -> (`TLocated` r) `fmap` tApp t1 t-      TApp f ts     -> return (TApp f (ts ++ [t]))       TUser f ts    -> return (TUser f (ts ++ [t]))       _             -> Nothing--  mkFun f = return (TApp (TF f) [])    cvtLit (ECNum n CharLit)  = return (TChar $ toEnum $ fromInteger n)   cvtLit (ECNum n _)        = return (TNum n)

@@ -13,28 +13,15 @@ {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE OverloadedStrings #-} -module Cryptol.Prelude (-  writePreludeContents,-  cryptolTcContents-  ) where+module Cryptol.Prelude (preludeContents,cryptolTcContents) where  -import System.Directory (getTemporaryDirectory)-import System.IO (hClose, hPutStr, openTempFile)+import Data.ByteString(ByteString)+import qualified Data.ByteString.Char8 as B import Text.Heredoc (there) -preludeContents :: String-preludeContents = [there|lib/Cryptol.cry|]---- | Write the contents of the Prelude to a temporary file so that--- Cryptol can load the module.-writePreludeContents :: IO FilePath-writePreludeContents = do-  tmpdir <- getTemporaryDirectory-  (path, h) <- openTempFile tmpdir "Cryptol.cry"-  hPutStr h preludeContents-  hClose h-  return path+preludeContents :: ByteString+preludeContents = B.pack [there|lib/Cryptol.cry|]  cryptolTcContents :: String cryptolTcContents = [there|lib/CryptolTC.z3|]

@@ -24,7 +24,6 @@  import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),fromNat,genLog, nMul)-import qualified Cryptol.Eval.Arch as Arch import Cryptol.Eval.Monad import Cryptol.Eval.Type import Cryptol.Eval.Value@@ -49,11 +48,9 @@ -- Primitives ------------------------------------------------------------------  instance EvalPrims Bool BV Integer where-  evalPrim Decl { dName = n, .. }-    | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val--  evalPrim Decl { .. } =-      panic "Eval" [ "Unimplemented primitive", show dName ]+  evalPrim Decl { dName = n, .. } =+    do prim <- asPrim n+       Map.lookup prim primTable    iteValue b t f = if b then t else f @@ -222,9 +219,7 @@   case ty of     TVInteger                    -> VInteger . integerLit     TVIntMod _                   -> VInteger . integerLit-    TVSeq w TVBit-      | w >= Arch.maxBigIntWidth -> wordTooWide w-      | otherwise                -> word w+    TVSeq w TVBit                -> word w     _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"                                     [ "Invalid type for number" ] @@ -432,6 +427,9 @@                  ]          return $ VRecord fs' +    TVAbstract {} ->+      evalPanic "arithBinary" ["Abstract type not in `Arith`"]+ type UnaryArith w = Integer -> w -> Eval w  liftUnaryArith :: (Integer -> Integer) -> UnaryArith BV@@ -487,6 +485,8 @@                  ]          return $ VRecord fs' +    TVAbstract {} -> evalPanic "arithUnary" ["Abstract type not in `Arith`"]+ arithNullary ::   forall b w i.   BitWord b w i =>@@ -518,6 +518,9 @@          TVRec fs -> VRecord [ (f, ready (loop a)) | (f, a) <- fs ] +        TVAbstract {} ->+          evalPanic "arithNullary" ["Abstract type not in `Arith`"]+ lg2 :: Integer -> Integer lg2 i = case genLog i 2 of   Just (i',isExact) | isExact   -> i'@@ -580,6 +583,8 @@                             cmpValues tys                               (vals (fromVRecord v1))                               (vals (fromVRecord v2)) k+        TVAbstract {} -> evalPanic "cmpValue"+                          [ "Abstract type not in `Cmp`" ]      cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =       do x1' <- x1@@ -652,7 +657,7 @@ signedBV (BV i x) = signedValue i x  signedValue :: Integer -> Integer -> Integer-signedValue i x = if testBit x (fromIntegral (i-1)) then x - (1 `shiftL` (fromIntegral i)) else x+signedValue i x = if testBit x (fromInteger (i-1)) then x - (1 `shiftL` (fromInteger i)) else x  bvSlt :: Integer -> Integer -> Integer -> Eval Value bvSlt _sz x y = return . VBit $! (x < y)@@ -671,7 +676,7 @@   nlam $ \_k ->   wlam $ \(BV i x) -> return $   wlam $ \y ->-   let signx = testBit x (fromIntegral (i-1))+   let signx = testBit x (fromInteger (i-1))        amt   = fromInteger (bvVal y)        negv  = (((-1) `shiftL` amt) .|. x) `shiftR` amt        posv  = x `shiftR` amt@@ -742,6 +747,8 @@   TVRec fields ->     VRecord [ (f,ready $ zeroV fty) | (f,fty) <- fields ] +  TVAbstract {} -> evalPanic "zeroV" [ "Abstract type not in `Zero`" ]+ --  | otherwise = evalPanic "zeroV" ["invalid type for zero"]  @@ -1121,7 +1128,10 @@                    ]            return $ VRecord fs +    TVAbstract {} -> evalPanic "logicBinary"+                        [ "Abstract type not in `Logic`" ] + wordValUnaryOp :: BitWord b w i                => (b -> b)                -> (w -> w)@@ -1177,7 +1187,9 @@                  ]          return $ VRecord fs +    TVAbstract {} -> evalPanic "logicUnary" [ "Abstract type not in `Logic`" ] + logicShift :: (Integer -> Integer -> Integer -> Integer)               -- ^ The function may assume its arguments are masked.               -- It is responsible for masking its result if needed.@@ -1466,7 +1478,7 @@     Just gen ->       -- unpack the seed into four Word64s       let mask64 = 0xFFFFFFFFFFFFFFFF-          unpack s = fromIntegral (s .&. mask64) : unpack (s `shiftR` 64)+          unpack s = fromInteger (s .&. mask64) : unpack (s `shiftR` 64)           [a, b, c, d] = take 4 (unpack seed)       in fst $ gen 100 $ seedTFGen (a, b, c, d) @@ -1503,3 +1515,5 @@   -- records   TVRec fields ->     return $ VRecord [ (f,errorV fty msg) | (f,fty) <- fields ]++  TVAbstract {} -> cryUserError msg

@@ -1,444 +0,0 @@-{-# Language DeriveGeneric, DeriveAnyClass #-}-module Cryptol.Prims.Syntax where--import GHC.Generics (Generic)-import Control.DeepSeq-import qualified Data.Map as Map--import Cryptol.Parser.Name-import Cryptol.Parser.Selector-import Cryptol.Parser.Fixity-import qualified Cryptol.ModuleSystem.Name as M-import Cryptol.Utils.Ident-import Cryptol.Utils.PP---- | Information about a user visible built-in type.-data PrimTy = PrimTy-  { primTyCon     :: !TCon            -- ^ Use this ty-con (renamer)-  , primTyIdent   :: !Ident           -- ^ This is what it's called-  , primTyDoc     :: !String          -- ^ Documentation-  , primTyFixity  :: !(Maybe Fixity)  -- ^ Precedence, for infix ones-  }--instance Eq PrimTy where-  x == y = primTyCon x == primTyCon y--instance Ord PrimTy where-  compare x y = compare (primTyCon x) (primTyCon y)----- | This list should contain all user-visible built-in types.-primTyList :: [ PrimTy ]-primTyList =-  [ -- Value type constructors ---------------------------------------------------    tPrefix "inf"             TC TCInf-    "A numeric type representing infinity."--  , tPrefix "Bit"             TC TCBit-    "The type of boolean values."--  , tPrefix "Integer"         TC TCInteger-    "The type of unbounded integers."--  , tPrefix "Z"               TC TCIntMod-    "'Z n' is the type of integers, modulo 'n'."---    -- Predicate constructors ----------------------------------------------------  , tInfix "=="                PC PEqual      (n 20)-    "Assert that two numeric types are equal."--  , tInfix "!="                PC PNeq        (n 20)-    "Assert that two numeric types are different."--  , tInfix ">="                PC PGeq        (n 30)-    "Assert that the first numeric type is larger than, or equal to the second."--  , tPrefix "fin"              PC PFin-    "Assert that a numeric type is a proper natural number (not 'inf')."--  , tPrefix "Zero"             PC PZero-    "Value types that have a notion of 'zero'."--  , tPrefix "Logic"            PC PLogic-    "Value types that support logical operations."--  , tPrefix "Arith"            PC PArith-    "Value types that support arithmetic."--  , tPrefix "Cmp"              PC PCmp-    "Value types that support unsigned comparisons."--  , tPrefix "SignedCmp"        PC PSignedCmp-    "Value types that support signed comparisons."--  , tPrefix "Literal"         PC PLiteral-    "'Literal n a' asserts that type 'a' contains the number 'n'."----    -- Type functions --------------------------------------------------  , tInfix  "+"                TF TCAdd       (l 80)-    "Add numeric types."--  , tInfix  "-"                TF TCSub       (l 80)-    "Subtract numeric types."--  , tInfix  "*"                TF TCMul       (l 90)-    "Multiply numeric types."--  , tInfix  "/"                TF TCDiv       (l 90)-    "Divide numeric types, rounding down."--  , tInfix  "%"                TF TCMod       (l 90)-    "Remainder of numeric type division."--  , tInfix  "^^"               TF TCExp       (r 95)-    "Exponentiate numeric types."--  , tPrefix "width"            TF TCWidth-    "The number of bits required to represent the value of a numeric type."--  , tPrefix "min"              TF TCMin-    "The smaller of two numeric types."--  , tPrefix "max"              TF TCMax-    "The larger of two numeric types."--  , tInfix  "/^"               TF TCCeilDiv    (l 90)-    "Divide numeric types, rounding up."--  , tInfix  "%^"               TF TCCeilMod    (l 90)-    "How much we need to add to make a proper multiple of the second argument."--  , tPrefix "lengthFromThenTo" TF TCLenFromThenTo-    "The length of an enumeration."-  ]-  where-  r x = Fixity { fAssoc = RightAssoc, fLevel = x }-  l x = Fixity { fAssoc = LeftAssoc,  fLevel = x }-  n x = Fixity { fAssoc = NonAssoc,   fLevel = x }--  tPrefix x mk tc d =-    PrimTy { primTyCon    = mk tc-           , primTyIdent  = packIdent x-           , primTyDoc    = d-           , primTyFixity = Nothing-           }--  tInfix x mk tc f d =-    PrimTy { primTyCon    = mk tc-           , primTyIdent  = packInfix x-           , primTyDoc    = d-           , primTyFixity = Just f-           }------------------------------------------------------------------------------------- Indexes for quick access---- | Construct an index for quick lookup of primtys.-primTyIx :: Ord a => (PrimTy -> Maybe a) -> a -> Maybe PrimTy-primTyIx toKey = \x -> Map.lookup x mp-  where mp = Map.fromList [ (k,x) | x <- primTyList, Just k <- [ toKey x ] ]-{-# Inline primTyIx #-}----- | Lookup a prim type by a parser name.-primTyFromPName :: PName -> Maybe PrimTy-primTyFromPName = primTyIx $ \t -> Just (mkUnqual (primTyIdent t))----- | Lookup if a ty con is a primitive.-primTyFromTC :: TCon -> Maybe PrimTy-primTyFromTC = primTyIx $ \t -> Just (primTyCon t)---- | Lookup a 'TFun' prim type.-primTyFromTF :: TFun -> Maybe PrimTy-primTyFromTF = primTyIx $ \t ->-  case primTyCon t of-    TF tf -> Just tf-    _     -> Nothing----- | Lookup a 'PC' prim type.-primTyFromPC :: PC -> Maybe PrimTy-primTyFromPC = primTyIx $ \t ->-  case primTyCon t of-    PC tf -> Just tf-    _     -> Nothing--------------------------------------------------------------------------------------infixr 5 :->---- | Kinds, classify types.-data Kind   = KType-            | KNum-            | KProp-            | Kind :-> Kind-              deriving (Eq, Ord, Show, Generic, NFData)--class HasKind t where-  kindOf :: t -> Kind--instance HasKind TCon where-  kindOf (TC tc)      = kindOf tc-  kindOf (PC pc)      = kindOf pc-  kindOf (TF tf)      = kindOf tf-  kindOf (TError k _) = k--instance HasKind UserTC where-  kindOf (UserTC _ k) = k--instance HasKind TC where-  kindOf tcon =-    case tcon of-      TCNum _   -> KNum-      TCInf     -> KNum-      TCBit     -> KType-      TCInteger -> KType-      TCIntMod  -> KNum :-> KType-      TCSeq     -> KNum :-> KType :-> KType-      TCFun     -> KType :-> KType :-> KType-      TCTuple n -> foldr (:->) KType (replicate n KType)-      TCNewtype x -> kindOf x--instance HasKind PC where-  kindOf pc =-    case pc of-      PEqual     -> KNum :-> KNum :-> KProp-      PNeq       -> KNum :-> KNum :-> KProp-      PGeq       -> KNum :-> KNum :-> KProp-      PFin       -> KNum :-> KProp-      PHas _     -> KType :-> KType :-> KProp-      PZero      -> KType :-> KProp-      PLogic     -> KType :-> KProp-      PArith     -> KType :-> KProp-      PCmp       -> KType :-> KProp-      PSignedCmp -> KType :-> KProp-      PLiteral   -> KNum :-> KType :-> KProp-      PAnd       -> KProp :-> KProp :-> KProp-      PTrue      -> KProp--instance HasKind TFun where-  kindOf tfun =-    case tfun of-      TCWidth   -> KNum :-> KNum--      TCAdd     -> KNum :-> KNum :-> KNum-      TCSub     -> KNum :-> KNum :-> KNum-      TCMul     -> KNum :-> KNum :-> KNum-      TCDiv     -> KNum :-> KNum :-> KNum-      TCMod     -> KNum :-> KNum :-> KNum-      TCExp     -> KNum :-> KNum :-> KNum-      TCMin     -> KNum :-> KNum :-> KNum-      TCMax     -> KNum :-> KNum :-> KNum-      TCCeilDiv -> KNum :-> KNum :-> KNum-      TCCeilMod -> KNum :-> KNum :-> KNum--      TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum------ | Type constants.-data TCon   = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage-              deriving (Show, Eq, Ord, Generic, NFData)----- | Predicate symbols.--- If you add additional user-visible constructors, please update 'primTys'.-data PC     = PEqual        -- ^ @_ == _@-            | PNeq          -- ^ @_ /= _@-            | PGeq          -- ^ @_ >= _@-            | PFin          -- ^ @fin _@--            -- classes-            | PHas Selector -- ^ @Has sel type field@ does not appear in schemas-            | PZero         -- ^ @Zero _@-            | PLogic        -- ^ @Logic _@-            | PArith        -- ^ @Arith _@-            | PCmp          -- ^ @Cmp _@-            | PSignedCmp    -- ^ @SignedCmp _@-            | PLiteral      -- ^ @Literal _ _@--            | PAnd          -- ^ This is useful when simplifying things in place-            | PTrue         -- ^ Ditto-              deriving (Show, Eq, Ord, Generic, NFData)---- | 1-1 constants.--- If you add additional user-visible constructors, please update 'primTys'.-data TC     = TCNum Integer            -- ^ Numbers-            | TCInf                    -- ^ Inf-            | TCBit                    -- ^ Bit-            | TCInteger                -- ^ Integer-            | TCIntMod                 -- ^ @Z _@-            | TCSeq                    -- ^ @[_] _@-            | TCFun                    -- ^ @_ -> _@-            | TCTuple Int              -- ^ @(_, _, _)@-            | TCNewtype UserTC         -- ^ user-defined, @T@-              deriving (Show, Eq, Ord, Generic, NFData)---data UserTC = UserTC M.Name Kind-              deriving (Show, Generic, NFData)--instance Eq UserTC where-  UserTC x _ == UserTC y _ = x == y--instance Ord UserTC where-  compare (UserTC x _) (UserTC y _) = compare x y-----data TCErrorMessage = TCErrorMessage-  { tcErrorMessage :: !String-    -- XXX: Add location?-  } deriving (Show, Eq, Ord, Generic, NFData)----- | Built-in type functions.--- If you add additional user-visible constructors,--- please update 'primTys' in "Cryptol.Prims.Types".-data TFun--  = TCAdd                 -- ^ @ : Num -> Num -> Num @-  | TCSub                 -- ^ @ : Num -> Num -> Num @-  | TCMul                 -- ^ @ : Num -> Num -> Num @-  | TCDiv                 -- ^ @ : Num -> Num -> Num @-  | TCMod                 -- ^ @ : Num -> Num -> Num @-  | TCExp                 -- ^ @ : Num -> Num -> Num @-  | TCWidth               -- ^ @ : Num -> Num @-  | TCMin                 -- ^ @ : Num -> Num -> Num @-  | TCMax                 -- ^ @ : Num -> Num -> Num @-  | TCCeilDiv             -- ^ @ : Num -> Num -> Num @-  | TCCeilMod             -- ^ @ : Num -> Num -> Num @--  -- Computing the lengths of explicit enumerations-  | TCLenFromThenTo       -- ^ @ : Num -> Num -> Num -> Num@-    -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@--    deriving (Show, Eq, Ord, Bounded, Enum, Generic, NFData)--------------------------------------------------------------------------------------- Pretty printing--instance PP Kind where-  ppPrec p k = case k of-    KType   -> char '*'-    KNum    -> char '#'-    KProp   -> text "Prop"-    l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r])--instance PP TCon where-  ppPrec _ (TC tc)        = pp tc-  ppPrec _ (PC tc)        = pp tc-  ppPrec _ (TF tc)        = pp tc-  ppPrec _ (TError _ msg) = pp msg--instance PPName TCon where-  ppNameFixity (TC _)       = Nothing-  ppNameFixity (PC _)       = Nothing-  ppNameFixity (TF tf)      = ppNameFixity tf-  ppNameFixity (TError _ _) = Nothing--  ppPrefixName (TC tc) = pp tc-  ppPrefixName (PC pc) = pp pc-  ppPrefixName (TF tf) = ppPrefixName tf-  ppPrefixName (TError _ msg) = pp msg--  ppInfixName (TC tc) = pp tc-  ppInfixName (PC pc) = pp pc-  ppInfixName (TF tf) = ppInfixName tf-  ppInfixName (TError _ msg) = pp msg--instance PP TCErrorMessage where-  ppPrec _ tc = parens (text "error:" <+> text (tcErrorMessage tc))--instance PP PC where-  ppPrec _ x =-    case x of-      PEqual     -> text "(==)"-      PNeq       -> text "(/=)"-      PGeq       -> text "(>=)"-      PFin       -> text "fin"-      PHas sel   -> parens (ppSelector sel)-      PZero      -> text "Zero"-      PLogic     -> text "Logic"-      PArith     -> text "Arith"-      PCmp       -> text "Cmp"-      PSignedCmp -> text "SignedCmp"-      PLiteral   -> text "Literal"-      PTrue      -> text "True"-      PAnd       -> text "(&&)"--instance PP TC where-  ppPrec _ x =-    case x of-      TCNum n   -> integer n-      TCInf     -> text "inf"-      TCBit     -> text "Bit"-      TCInteger -> text "Integer"-      TCIntMod  -> text "Z"-      TCSeq     -> text "[]"-      TCFun     -> text "(->)"-      TCTuple 0 -> text "()"-      TCTuple 1 -> text "(one tuple?)"-      TCTuple n -> parens $ hcat $ replicate (n-1) comma-      TCNewtype u -> pp u--instance PP UserTC where-  ppPrec p (UserTC x _) = ppPrec p x-----instance PPName TFun where--  ppNameFixity f =-    do pt <- primTyFromTF f-       fi <- primTyFixity pt-       return (fAssoc fi, fLevel fi)--  ppPrefixName TCAdd     = text "(+)"-  ppPrefixName TCSub     = text "(-)"-  ppPrefixName TCMul     = text "(*)"-  ppPrefixName TCDiv     = text "(/)"-  ppPrefixName TCMod     = text "(%)"-  ppPrefixName TCExp     = text "(^^)"-  ppPrefixName TCCeilDiv = text "(/^)"-  ppPrefixName TCCeilMod = text "(%^)"-  ppPrefixName f         = pp f--  ppInfixName TCAdd     = text "+"-  ppInfixName TCSub     = text "-"-  ppInfixName TCMul     = text "*"-  ppInfixName TCDiv     = text "/"-  ppInfixName TCMod     = text "%"-  ppInfixName TCExp     = text "^^"-  ppInfixName TCCeilDiv = text "/^"-  ppInfixName TCCeilMod = text "%^"-  ppInfixName f         = error $ "Not a prefix type function: " ++ show (pp f)--instance PP TFun where-  ppPrec _ tcon =-    case tcon of-      TCAdd             -> text "+"-      TCSub             -> text "-"-      TCMul             -> text "*"-      TCDiv             -> text "/"-      TCMod             -> text "%"-      TCExp             -> text "^^"-      TCWidth           -> text "width"-      TCMin             -> text "min"-      TCMax             -> text "max"-      TCCeilDiv         -> text "/^"-      TCCeilMod         -> text "%^"-      TCLenFromThenTo   -> text "lengthFromThenTo"

@@ -19,6 +19,7 @@   , findCommand   , findCommandExact   , findNbCommand+  , commandList    , moduleCmd, loadCmd, loadPrelude, setOptionCmd @@ -71,7 +72,7 @@ import qualified Cryptol.TypeCheck.Subst as T import           Cryptol.TypeCheck.Solve(defaultReplExpr) import qualified Cryptol.TypeCheck.Solver.SMT as SMT-import Cryptol.TypeCheck.PP (dump)+import Cryptol.TypeCheck.PP (dump,ppWithNames,emptyNameMap,backticks) import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) import qualified Cryptol.Parser.AST as P@@ -81,21 +82,26 @@  import qualified Control.Exception as X import Control.Monad hiding (mapM, mapM)+import Control.Monad.IO.Class(liftIO)+import Data.ByteString (ByteString) import qualified Data.ByteString as BS+import qualified Data.ByteString.Char8 as BS8 import Data.Bits ((.&.))-import Data.Char (isSpace,isPunctuation,isSymbol)+import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii) import Data.Function (on)-import Data.List (intercalate, nub, sortBy, partition, isPrefixOf)+import Data.List (intercalate, nub, sortBy, partition, isPrefixOf,intersperse) import Data.Maybe (fromMaybe,mapMaybe,isNothing) import System.Environment (lookupEnv) import System.Exit (ExitCode(ExitSuccess)) import System.Process (shell,createProcess,waitForProcess) import qualified System.Process as Process(runCommand) import System.FilePath((</>), isPathSeparator)-import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist)+import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist+                       ,getTemporaryDirectory,setPermissions,removeFile+                       ,emptyPermissions,setOwnerReadable) import qualified Data.Map as Map import qualified Data.Set as Set-import System.IO(hFlush,stdout)+import System.IO(hFlush,stdout,openTempFile,hClose) import System.Random.TF(newTFGen) import Numeric (showFFloat) import qualified Data.Text as T@@ -311,7 +317,11 @@      ppopts <- getPPValOpts      testNum <- getKnownUser "tests" :: REPL Int      g <- io newTFGen-     tests <- io $ TestR.returnTests g evo ty val testNum+     gens <-+       case TestR.dumpableType ty of+         Nothing -> raise (TypeNotTestable ty)+         Just gens -> return gens+     tests <- io $ TestR.returnTests g evo gens val testNum      out <- forM tests $             \(args, x) ->               do argOut <- mapM (rEval . E.ppValue ppopts) args@@ -420,7 +430,7 @@   lg2 :: Integer -> Integer   lg2 x | x >= 2^(1024::Int) = 1024 + lg2 (x `div` 2^(1024::Int))         | x == 0       = 0-        | otherwise    = let valNumD = fromIntegral x :: Double+        | otherwise    = let valNumD = fromInteger x :: Double                          in round $ logBase 2 valNumD :: Integer    prt msg   = rPutStr msg >> io (hFlush stdout)@@ -777,7 +787,9 @@     Just lm  ->       case lName lm of         Just m | M.isParamInstModName m -> loadHelper (M.loadModuleByName m)-        _ -> loadCmd (lPath lm)+        _ -> case lPath lm of+               M.InFile f -> loadCmd f+               _ -> return ()     Nothing -> return ()  @@ -787,18 +799,43 @@      mbL <- getLoadedMod      if not (null path)         then do when (isNothing mbL)-                  $ setLoadedMod LoadedModule { lName = Nothing, lPath = path }+                  $ setLoadedMod LoadedModule { lName = Nothing+                                              , lPath = M.InFile path }                 doEdit path-        else case msum [ mbE, lPath <$> mbL ] of+        else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of                Nothing -> rPutStrLn "No filed to edit."-               Just p  -> doEdit p+               Just p  ->+                  case p of+                    M.InFile f   -> doEdit f+                    M.InMem l bs -> withROTempFile l bs replEdit >> pure ()   where   doEdit p =     do setEditPath p        _ <- replEdit p        reloadCmd +withROTempFile :: String -> ByteString -> (FilePath -> REPL a) -> REPL a+withROTempFile name cnt k =+  do (path,h) <- mkTmp+     do mkFile path h+        k path+      `finally` liftIO (do hClose h+                           removeFile path)+  where+  mkTmp =+    liftIO $+    do tmp <- getTemporaryDirectory+       let esc c = if isAscii c && isAlphaNum c then c else '_'+       openTempFile tmp (map esc name ++ ".cry") +  mkFile path h =+    liftIO $+    do BS8.hPutStrLn h cnt+       hFlush h+       setPermissions path (setOwnerReadable True emptyPermissions)+++ moduleCmd :: String -> REPL () moduleCmd modString   | null modString = return ()@@ -817,11 +854,11 @@   -- when `:load`, the edit and focused paths become the parameter   | otherwise = do setEditPath path                    setLoadedMod LoadedModule { lName = Nothing-                                             , lPath = path+                                             , lPath = M.InFile path                                              }                    loadHelper (M.loadModuleByPath path) -loadHelper :: M.ModuleCmd (FilePath,T.Module) -> REPL ()+loadHelper :: M.ModuleCmd (M.ModulePath,T.Module) -> REPL () loadHelper how =   do clearLoadedMod      (path,m) <- liftModuleCmd how@@ -831,7 +868,9 @@         , lPath = path         }      -- after a successful load, the current module becomes the edit target-     setEditPath path+     case path of+       M.InFile f -> setEditPath f+       M.InMem {} -> clearEditPath      setDynEnv mempty  quitCmd :: REPL ()@@ -867,6 +906,7 @@    browseMParams  visibleType visibleDecl params disp   browseTSyns    visibleType             iface disp+  browsePrimTys  visibleType             iface disp   browseNewtypes visibleType             iface disp   browseVars     visibleDecl             iface disp @@ -888,6 +928,13 @@                $ filter (vis . nm) $ Map.elems mp  +browsePrimTys :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL ()+browsePrimTys isVisible M.IfaceDecls { .. } names =+  do let pts = sortBy (M.cmpNameDisplay names `on` T.atName)+               [ ts | ts <- Map.elems ifAbstractTypes, isVisible (T.atName ts) ]+     ppBlock names ppA "Primitive Types" pts+  where+  ppA a = pp (T.atName a) <+> ":" <+> pp (T.atKind a)  browseTSyns :: (M.Name -> Bool) -> M.IfaceDecls -> NameDisp -> REPL () browseTSyns isVisible M.IfaceDecls { .. } names = do@@ -983,13 +1030,14 @@         do (params,env,rnEnv,nameEnv) <- getFocusedEnv            let vNames = M.lookupValNames  qname rnEnv                tNames = M.lookupTypeNames qname rnEnv-               pNames = T.primTyFromPName qname -           mapM_ (showTypeHelp params env nameEnv) tNames-           mapM_ (showValHelp params env nameEnv qname) vNames-           mapM_ (showPrimTyHelp nameEnv) pNames+           let helps = map (showTypeHelp params env nameEnv) tNames +++                       map (showValHelp params env nameEnv qname) vNames -           when (null (vNames ++ tNames) && pNames == Nothing) $+               separ = rPutStrLn "            ~~~ * ~~~"+           sequence_ (intersperse separ helps)++           when (null (vNames ++ tNames)) $              rPrint $ "Undefined name:" <+> pp qname       Nothing ->            rPutStrLn ("Unable to parse name: " ++ cmd)@@ -1001,21 +1049,11 @@                       rPrint $runDoc nameEnv ("Name defined in module" <+> pp m)       M.Parameter  -> rPutStrLn "// No documentation is available." -  showPrimTyHelp nameEnv pt =-    do rPutStrLn ""-       let i    = T.primTyIdent pt-           nm   = pp (T.primTyIdent pt)-           pnam = if P.isInfixIdent i then parens nm else nm-           sig  = "primitive type" <+> pnam <+> ":" <+> pp (T.kindOf (T.primTyCon pt))-       rPrint $ runDoc nameEnv $ nest 4 sig-       doShowFix (T.primTyFixity pt)-       rPutStrLn ""-       rPutStrLn (T.primTyDoc pt)-       rPutStrLn "" +   showTypeHelp params env nameEnv name =     fromMaybe (noInfo nameEnv name) $-    msum [ fromTySyn, fromNewtype, fromTyParam ]+    msum [ fromTySyn, fromPrimType, fromNewtype, fromTyParam ]      where     fromTySyn =@@ -1027,6 +1065,31 @@          let decl = pp nt $$ (pp name <+> text ":" <+> pp (T.newtypeConType nt))          return $ doShowTyHelp nameEnv decl (T.ntDoc nt) +    fromPrimType =+      do a <- Map.lookup name (M.ifAbstractTypes env)+         pure $ do rPutStrLn ""+                   rPrint $ runDoc nameEnv $ nest 4+                          $ "primitive type" <+> pp (T.atName a)+                                     <+> ":" <+> pp (T.atKind a)++                   let (vs,cs) = T.atCtrs a+                   unless (null cs) $+                     do let example = T.TCon (T.abstractTypeTC a)+                                             (map (T.TVar . T.tpVar) vs)+                            ns = T.addTNames vs emptyNameMap+                            rs = [ "•" <+> ppWithNames ns c | c <- cs ]+                        rPutStrLn ""+                        rPrint $ runDoc nameEnv $ nest 4 $+                                    backticks (ppWithNames ns example) <+>+                                    "requires:" $$ nest 2 (vcat rs)++                   doShowFix (T.atFixitiy a)++                   case T.atDoc a of+                     Nothing -> pure ()+                     Just d -> do rPutStrLn ""+                                  rPutStrLn d+     fromTyParam =       do p <- Map.lookup name (M.ifParamTypes params)          let uses c = T.TVBound (T.mtpParam p) `Set.member` T.fvs c@@ -1215,7 +1278,7 @@     Right (a,me') -> setModuleEnv me' >> return a     Left err      ->       do e <- case err of-                M.ErrorInFile file e ->+                M.ErrorInFile (M.InFile file) e ->                   -- on error, the file with the error becomes the edit                   -- target.  Note, however, that the focused module is not                   -- changed.

@@ -22,6 +22,7 @@   , raise   , stop   , catch+  , finally   , rPutStrLn   , rPutStr   , rPrint@@ -42,7 +43,7 @@   , getPropertyNames   , getModNames   , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod-  , setEditPath, getEditPath+  , setEditPath, getEditPath, clearEditPath   , setSearchPath, prependSearchPath   , getPrompt   , shouldContinue@@ -122,8 +123,8 @@  -- | This indicates what the user would like to work on. data LoadedModule = LoadedModule-  { lName :: Maybe P.ModName -- ^ Working on this module.-  , lPath :: FilePath        -- ^ Working on this file.+  { lName :: Maybe P.ModName  -- ^ Working on this module.+  , lPath :: M.ModulePath     -- ^ Working on this file.   }  -- | REPL RW Environment.@@ -185,7 +186,7 @@    modLn   =     case lName =<< eLoadedMod rw of-      Nothing -> "cryptol"+      Nothing -> show (pp I.preludeName)       Just m         | M.isLoadedParamMod m (M.meLoadedModules (eModuleEnv rw)) ->                  modName ++ "(parameterized)"@@ -196,15 +197,15 @@     case eLoadedMod rw of       Nothing -> modLn       Just m ->-        case lName m of-          Nothing -> ":r to reload " ++ lPath m ++ "\n" ++ modLn-          Just _ -> modLn+        case (lName m, lPath m) of+          (Nothing, M.InFile f) -> ":r to reload " ++ show f ++ "\n" ++ modLn+          _ -> modLn    withEdit =     case eEditFile rw of       Nothing -> withFocus       Just e-        | Just f <- lPath <$> eLoadedMod rw+        | Just (M.InFile f) <- lPath <$> eLoadedMod rw         , f == e -> withFocus         | otherwise -> ":e to edit " ++ e ++ "\n" ++ withFocus @@ -308,7 +309,10 @@ catch :: REPL a -> (REPLException -> REPL a) -> REPL a catch m k = REPL (\ ref -> rethrowEvalError (unREPL m ref) `X.catch` \ e -> unREPL (k e) ref) +finally :: REPL a -> REPL b -> REPL a+finally m1 m2 = REPL (\ref -> unREPL m1 ref `X.finally` unREPL m2 ref) + rethrowEvalError :: IO a -> IO a rethrowEvalError m = run `X.catch` rethrow   where@@ -365,6 +369,9 @@ getEditPath :: REPL (Maybe FilePath) getEditPath = eEditFile <$> getRW +clearEditPath :: REPL ()+clearEditPath = modifyRW_ $ \rw -> rw { eEditFile = Nothing }+ setSearchPath :: [FilePath] -> REPL () setSearchPath path = do   me <- getModuleEnv@@ -786,7 +793,7 @@     "Enable type-checker debugging output." $     \case EnvNum n -> do me <- getModuleEnv                          let cfg = M.meSolverConfig me-                         setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = fromIntegral n } }+                         setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = n } }           _        -> return ()   , OptionDescr "core-lint" (EnvBool False)     noCheck

@@ -326,6 +326,7 @@     Eval.TVSeq n t        -> FTSeq <$> numType n <*> finType t     Eval.TVTuple ts       -> FTTuple <$> traverse finType ts     Eval.TVRec fields     -> FTRecord <$> traverse (traverseSnd finType) fields+    Eval.TVAbstract {}    -> Nothing     _                     -> Nothing  unFinType :: FinType -> Type

@@ -45,7 +45,6 @@ import Cryptol.Symbolic.Value import Cryptol.TypeCheck.AST (Decl(..)) import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)-import Cryptol.Utils.Panic import Cryptol.ModuleSystem.Name (asPrim) import Cryptol.Utils.Ident (Ident,mkIdent) @@ -64,11 +63,9 @@ -- Primitives ------------------------------------------------------------------  instance EvalPrims SBool SWord SInteger where-  evalPrim Decl { dName = n, .. }-    | Just prim <- asPrim n, Just val <- Map.lookup prim primTable = val--  evalPrim Decl { .. } =-      panic "Eval" [ "Unimplemented primitive", show dName ]+  evalPrim Decl { dName = n, .. } =+    do prim <- asPrim n+       Map.lookup prim primTable    iteValue b x1 x2     | Just b' <- SBV.svAsBool b = if b' then x1 else x2

@@ -193,7 +193,7 @@   wordLit n x = svInteger (KBounded False (fromInteger n)) x   integerLit x = svInteger KUnbounded x -  wordBit x idx = svTestBit x (intSizeOf x - 1 - fromIntegral idx)+  wordBit x idx = svTestBit x (intSizeOf x - 1 - fromInteger idx)    wordUpdate x idx b = svSymbolicMerge (kindOf x) False b wtrue wfalse     where

@@ -99,6 +99,7 @@         (TCSeq, _)       -> Nothing         (TCFun, _)       -> Nothing         (TCTuple _, els) -> product <$> mapM typeSize els+        (TCAbstract _, _) -> Nothing         (TCNewtype _, _) -> Nothing      TCon _ _ -> Nothing@@ -142,6 +143,7 @@         TCTuple _   -> [ VTuple (map ready xs)                        | xs <- sequence (map typeValues ts)                        ]+        TCAbstract _ -> []         TCNewtype _ -> []      TCon _ _ -> []

@@ -9,17 +9,17 @@ -- This module generates random values for Cryptol types.  {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ScopedTypeVariables #-} module Cryptol.Testing.Random where  import Cryptol.Eval.Monad     (ready,runEval,EvalOpts) import Cryptol.Eval.Value     (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..), BitWord(..)) import qualified Cryptol.Testing.Concrete as Conc-import Cryptol.TypeCheck.AST  (Type(..),TCon(..),TC(..),tNoUser)+import Cryptol.TypeCheck.AST  (Type(..), TCon(..), TC(..), tNoUser, tIsFun) import Cryptol.TypeCheck.SimpType(tRebuild')  import Cryptol.Utils.Ident    (Ident) import Cryptol.Utils.Panic    (panic)-import Cryptol.Utils.PP       (pp)  import Control.Monad          (forM,join) import Data.List              (unfoldr, genericTake, genericIndex)@@ -63,28 +63,20 @@      return (args, result, g1)    where      go (VFun f) (v : vs) = join (go <$> (f (ready v)) <*> pure vs)-     go (VFun _) [] = panic "Not enough arguments to function while generating tests" []-     go v@(VBit _) [] = return v-     go v@(VSeq _ _) [] = return v-     go v@(VWord _ _) [] = return v-     go v@(VRecord _) [] = return v-     go v@(VTuple _) [] = return v-     go _ _ = panic "Cryptol.Testing.Random" ["Unsupported return value for testing"]+     go (VFun _) [] = panic "Cryptol.Testing.Random" ["Not enough arguments to function while generating tests"]+     go _ (_ : _) = panic "Cryptol.Testing.Random" ["Too many arguments to function while generating tests"]+     go v [] = return v   -- | Return a collection of random tests. returnTests :: RandomGen g          => g -- ^ The random generator state          -> EvalOpts -- ^ How to evaluate things-         -> Type -- ^ The type of the function for which tests are to be generated+         -> [Gen g Bool BV Integer] -- ^ Generators for the function arguments          -> Value -- ^ The function itself          -> Int -- ^ How many tests?          -> IO [([Value], Value)] -- ^ A list of pairs of random arguments and computed outputs-returnTests g evo ty fun num =-    case argGens ty of-      Nothing -> panic "Cryptol.Testing.Random" ["Can't generate test inputs for type", show (pp ty)]-      Just args ->-        do go args g 0+returnTests g evo gens fun num = go gens g 0   where     go args g0 n       | n >= num = return []@@ -94,12 +86,19 @@            more <- go args g1 (n + 1)            return ((inputs, output) : more) -    argGens t =-      case tNoUser t of-        TCon (TC TCFun) [t1, t2] ->-          (:) <$> randomValue t1 <*> argGens t2-        _ -> pure []-+{- | Given a (function) type, compute generators for the function's+arguments. This is like @testableType@, but allows the result to be+any finite type instead of just @Bit@. -}+dumpableType :: forall g. RandomGen g => Type -> Maybe [Gen g Bool BV Integer]+dumpableType ty =+  case tIsFun ty of+    Just (t1, t2) ->+      do g  <- randomValue t1+         as <- testableType t2+         return (g : as)+    Nothing ->+      do (_ :: Gen g Bool BV Integer) <- randomValue ty+         return []  {- | Given a (function) type, compute generators for the function's arguments. Currently we do not support polymorphic functions.

@@ -337,20 +337,6 @@     concatMap mDecls   . M.loadedModules -allLoadedModules :: M.ModuleEnv -> [M.LoadedModule]-allLoadedModules =-    M.getLoadedModules-  . M.meLoadedModules--allPublicNames :: M.ModuleEnv -> [Name]-allPublicNames =-    concatMap-      ( Map.keys-      . M.ifDecls-      . M.ifPublic-      . M.lmInterface-      )-  . allLoadedModules  traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c) traverseSnd f (x, y) = (,) x <$> f y

@@ -33,7 +33,6 @@ import Cryptol.ModuleSystem.Name import Cryptol.ModuleSystem.Exports(ExportSpec(..)                                    , isExportedBind, isExportedType)-import Cryptol.Prims.Syntax import Cryptol.Parser.AST ( Selector(..),Pragma(..)                           , Import(..), ImportSpec(..), ExportType(..)                           , Fixity(..))@@ -59,6 +58,7 @@                        -- of a module.                       , mNewtypes         :: Map Name Newtype+                     , mPrimTypes        :: Map Name AbstractType                      , mParamTypes       :: Map Name ModTParam                      , mParamConstraints :: [Located Prop]                      , mParamFuns        :: Map Name ModVParam

@@ -37,8 +37,9 @@                                 -- 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)+                   , mTySyns      = Map.union (mTySyns inst) (mTySyns m)+                   , mNewtypes    = Map.union (mNewtypes inst) (mNewtypes m)+                   , mPrimTypes   = Map.union (mPrimTypes inst) (mPrimTypes m)                    , mParamTypes       = mParamTypes inst                    , mParamConstraints = mParamConstraints inst                    , mParamFuns        = mParamFuns inst@@ -88,7 +89,7 @@        unless (k1 == k2) (recordError (KindMismatch k1 k2))         let nm  = tsName ts-           src = CtPartialTypeFun (UserTyFun nm)+           src = CtPartialTypeFun nm        mapM_ (newGoal src) (tsConstraints ts)         return (tp, TUser nm [] (tsDef ts))@@ -106,7 +107,7 @@        unless (k1 == k2) (recordError (KindMismatch k1 k2))         let nm = ntName nt-           src = CtPartialTypeFun (UserTyFun nm)+           src = CtPartialTypeFun nm        mapM_ (newGoal src) (ntConstraints nt)         return (tp, TCon (TC (TCNewtype (UserTC nm k2))) [])

@@ -13,7 +13,8 @@ import           Cryptol.ModuleSystem.Name (Name) import qualified Cryptol.Parser.AST as P import           Cryptol.Parser.Position(Range, Located(..), thing)-import           Cryptol.Parser.Names (namesB, namesT, namesC)+import           Cryptol.Parser.Names (namesB, tnamesT, tnamesC,+                                      boundNamesSet, boundNames) import           Cryptol.TypeCheck.Monad( InferM, recordError, getTVars ) import           Cryptol.TypeCheck.Error(Error(..)) import           Cryptol.Utils.Panic(panic)@@ -27,10 +28,13 @@ import qualified Data.Map as Map import qualified Data.Set as Set -data TyDecl = TS (P.TySyn Name) (Maybe String)              -- ^ Type synonym-            | NT (P.Newtype Name) (Maybe String)            -- ^ Newtype-            | AT (P.ParameterType Name) (Maybe String)      -- ^ Parameter type-            | PS (P.PropSyn Name) (Maybe String)            -- ^ Property synonym+data TyDecl =+    TS (P.TySyn Name) (Maybe String)          -- ^ Type synonym+  | NT (P.Newtype Name) (Maybe String)        -- ^ Newtype+  | AT (P.ParameterType Name) (Maybe String)  -- ^ Parameter type+  | PS (P.PropSyn Name) (Maybe String)        -- ^ Property synonym+  | PT (P.PrimType Name) (Maybe String)       -- ^ A primitive/abstract typee+    deriving Show  setDocString :: Maybe String -> TyDecl -> TyDecl setDocString x d =@@ -38,7 +42,8 @@     TS a _ -> TS a x     PS a _ -> PS a x     NT a _ -> NT a x-    AT a _  -> AT a x+    AT a _ -> AT a x+    PT a _ -> PT a x  -- | Check for duplicate and recursive type synonyms. -- Returns the type-synonyms in dependency order.@@ -51,6 +56,20 @@      concat `fmap` mapM check ordered    where+  toMap vs ty@(PT p _) =+    let x       = P.primTName p+        (as,cs) = P.primTCts p+    in  ( thing x+        , x { thing = (ty, Set.toList $+                           boundNamesSet vs $+                           boundNames (map P.tpName as) $+                           Set.unions $+                           map tnamesC cs+                      )+             }+        )++   toMap _ ty@(AT a _) =     let x = P.ptName a     in ( thing x, x { thing = (ty, []) } )@@ -58,32 +77,39 @@   toMap vs ty@(NT (P.Newtype x as fs) _) =     ( thing x     , x { thing = (ty, Set.toList $-                       Set.difference-                         (Set.unions (map (namesT vs . P.value) fs))-                         (Set.fromList (map P.tpName as))+                       boundNamesSet vs $+                       boundNames (map P.tpName as) $+                       Set.unions $+                       map (tnamesT . P.value) fs                   )         }     ) -  toMap vs ty@(TS (P.TySyn x as t) _) =+  toMap vs ty@(TS (P.TySyn x _ as t) _) =         (thing x         , x { thing = (ty, Set.toList $-                           Set.difference (namesT vs t)-                                          (Set.fromList (map P.tpName as)))+                           boundNamesSet vs $+                           boundNames (map P.tpName as) $+                           tnamesT t+                      )              }         ) -  toMap vs ty@(PS (P.PropSyn x as ps) _) =+  toMap vs ty@(PS (P.PropSyn x _ as ps) _) =         (thing x         , x { thing = (ty, Set.toList $-                           Set.difference (Set.unions (map (namesC vs) ps))-                                          (Set.fromList (map P.tpName as)))+                           boundNamesSet vs $+                           boundNames (map P.tpName as) $+                           Set.unions $+                           map tnamesC ps+                      )              }         )-  getN (TS (P.TySyn x _ _) _)   = thing x-  getN (PS (P.PropSyn x _ _) _) = thing x-  getN (NT x _)                 = thing (P.nName x)-  getN (AT x _)                 = thing (P.ptName x)+  getN (TS x _) = thing (P.tsName x)+  getN (PS x _) = thing (P.psName x)+  getN (NT x _) = thing (P.nName x)+  getN (AT x _) = thing (P.ptName x)+  getN (PT x _) = thing (P.primTName x)    check (AcyclicSCC x) = return [x] @@ -121,6 +147,7 @@   toParamConstraints (P.DParameterConstraint xs) = xs   toParamConstraints _                           = [] +  toTyDecl (P.DPrimType p)      = Just (PT (P.tlValue p) (thing <$> P.tlDoc p))   toTyDecl (P.DParameterType d) = Just (AT d (P.ptDoc d))   toTyDecl (P.TDNewtype d)      = Just (NT (P.tlValue d) (thing <$> P.tlDoc d))   toTyDecl (P.Decl x)           = setDocString (thing <$> P.tlDoc x)

@@ -71,8 +71,8 @@               | TooManyTySynParams Name Int                 -- ^ Type-synonym, number of extra params -              | TooFewTySynParams Name Int-                -- ^ Type-synonym, number of missing params+              | TooFewTyParams Name Int+                -- ^ Who is missing params, number of missing params                | RecursiveTypeDecls [Name]                 -- ^ The type synonym declarations are recursive@@ -137,7 +137,7 @@       TooManyTypeParams {}      -> err       TyVarWithParams           -> err       TooManyTySynParams {}     -> err-      TooFewTySynParams {}      -> err+      TooFewTyParams {}         -> err       RecursiveTypeDecls {}     -> err       TypeMismatch t1 t2        -> TypeMismatch (apSubst su t1) (apSubst su t2)       RecursiveType t1 t2       -> RecursiveType (apSubst su t1) (apSubst su t2)@@ -161,7 +161,7 @@       TooManyTypeParams {}      -> Set.empty       TyVarWithParams           -> Set.empty       TooManyTySynParams {}     -> Set.empty-      TooFewTySynParams {}      -> Set.empty+      TooFewTyParams {}         -> Set.empty       RecursiveTypeDecls {}     -> Set.empty       TypeMismatch t1 t2        -> fvs (t1,t2)       RecursiveType t1 t2       -> fvs (t1,t2)@@ -240,7 +240,7 @@           ("Type synonym" <+> nm t <+> "was applied to" <+>             pl extra "extra parameters" <.> text ".") -      TooFewTySynParams t few ->+      TooFewTyParams t few ->         addTVarsDescsAfter names err $         nested "Malformed type."           ("Type" <+> nm t <+> "is missing" <+> int few <+> text "parameters.")

@@ -35,6 +35,7 @@ import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,                                         checkPropSyn,checkNewtype,                                         checkParameterType,+                                        checkPrimType,                                         checkParameterConstraints) import           Cryptol.TypeCheck.Instantiate import           Cryptol.TypeCheck.Depends@@ -63,6 +64,7 @@     do proveModuleTopLevel        ts <- getTSyns        nts <- getNewtypes+       ats <- getAbstractTypes        pTs <- getParamTypes        pCs <- getParamConstraints        pFuns <- getParamFuns@@ -71,6 +73,7 @@                      , mImports   = map thing (P.mImports m)                      , mTySyns    = Map.mapMaybe onlyLocal ts                      , mNewtypes  = Map.mapMaybe onlyLocal nts+                     , mPrimTypes = Map.mapMaybe onlyLocal ats                      , mParamTypes = pTs                      , mParamConstraints = pCs                      , mParamFuns = pFuns@@ -123,13 +126,14 @@            P.PolyLit _n  -> [ ("rep", P.TSeq P.TWild P.TBit) ]         P.ECString s ->-          P.ETyped (P.EList [ P.ELit (P.ECNum (fromIntegral (fromEnum c))+          P.ETyped (P.EList [ P.ELit (P.ECNum (toInteger (fromEnum c))                             P.CharLit) | c <- s ])                    (P.TSeq P.TWild (P.TSeq (P.TNum 8) P.TBit))  + -- | Infer the type of an expression with an explicit instantiation.-appTys :: P.Expr Name -> [Located (Maybe Ident,Type)] -> Type -> InferM Expr+appTys :: P.Expr Name -> [TypeArg] -> Type -> InferM Expr appTys expr ts tGoal =   case expr of     P.EVar x ->@@ -146,9 +150,7 @@                    appTys e ts tGoal  -    P.EAppT e fs ->-      do ps <- mapM inferTyParam fs-         appTys e (ps ++ ts) tGoal+    P.EAppT e fs -> appTys e (map uncheckedTypeArg fs ++ ts) tGoal      -- Here is an example of why this might be useful:     -- f ` { x = T } where type T = ...@@ -162,6 +164,7 @@      P.ENeg        {} -> mono     P.EComplement {} -> mono+    P.EGenerate   {} -> mono      P.ETuple    {} -> mono     P.ERecord   {} -> mono@@ -185,33 +188,23 @@                   checkNoParams ts                   return e' -checkNoParams :: [Located (Maybe Ident,Type)] -> InferM ()+checkNoParams :: [TypeArg] -> InferM () checkNoParams ts =   case pos of-    p : _ -> inRange (srcRange p) (recordError TooManyPositionalTypeParams)-    []    -> mapM_ badNamed named+    p : _ -> do r <- case tyArgType p of+                       Unchecked t | Just r <- getLoc t -> pure r+                       _ -> curRange+                inRange r (recordError TooManyPositionalTypeParams)+    _ -> mapM_ badNamed named   where   badNamed l =-    case fst (thing l) of-      Just i -> recordError (UndefinedTypeParameter l { thing = i })+    case tyArgName l of+      Just i  -> recordError (UndefinedTypeParameter i)       Nothing -> return () -  (named,pos) = partition (isJust . fst . thing) ts+  (named,pos) = partition (isJust . tyArgName) ts  -inferTyParam :: P.TypeInst Name -> InferM (Located (Maybe Ident, Type))-inferTyParam (P.NamedInst param) =-  do let loc = srcRange (P.name param)-     t <- inRange loc $ checkType (P.value param) Nothing-     return $ Located loc (Just (thing (P.name param)), t)--inferTyParam (P.PosInst param) =-  do t   <- checkType param Nothing-     rng <- case getLoc param of-              Nothing -> curRange-              Just r  -> return r-     return Located { srcRange = rng, thing = (Nothing, t) }- checkTypeOfKind :: P.Type Name -> Kind -> InferM Type checkTypeOfKind ty k = checkType ty (Just k) @@ -238,6 +231,10 @@       do prim <- mkPrim "complement"          checkE (P.EApp prim e) tGoal +    P.EGenerate e ->+      do prim <- mkPrim "generate"+         checkE (P.EApp prim e) tGoal+     P.ELit l@(P.ECNum _ P.DecLit) ->       do e <- desugarLiteral False l          -- NOTE: When 'l' is a decimal literal, 'desugarLiteral' does@@ -246,7 +243,10 @@          -- instantiate 'rep' to 'tGoal' in this case to avoid          -- generating an unnecessary unification variable.          loc <- curRange-         appTys e [Located loc (Just (packIdent "rep"), tGoal)] tGoal+         let arg = TypeArg { tyArgName = Just (Located loc (packIdent "rep"))+                           , tyArgType = Checked tGoal+                           }+         appTys e [arg] tGoal      P.ELit l -> (`checkE` tGoal) =<< desugarLiteral False l @@ -279,14 +279,18 @@          es' <- mapM (`checkE` a) es          return (EList es' a) -    P.EFromTo t1 mbt2 t3 ->+    P.EFromTo t1 mbt2 t3 mety ->       do l <- curRange+         let fs0 =+               case mety of+                 Just ety -> [("a", ety)]+                 Nothing -> []          let (c,fs) =                case mbt2 of                  Nothing ->-                    ("fromTo", [ ("last", t3) ])+                    ("fromTo", ("last", t3) : fs0)                  Just t2 ->-                    ("fromThenTo", [ ("next",t2), ("last",t3) ])+                    ("fromThenTo", ("next",t2) : ("last",t3) : fs0)           prim <- mkPrim c          let e' = P.EAppT prim@@ -314,9 +318,7 @@          e'     <- withMonoTypes ds (checkE e a)          return (EComp len a e' mss') -    P.EAppT e fs ->-      do ts <- mapM inferTyParam fs-         appTys e ts tGoal+    P.EAppT e fs -> appTys e (map uncheckedTypeArg fs) tGoal      P.EApp fun@(dropLoc -> P.EApp (dropLoc -> P.EVar c) _)            arg@(dropLoc -> P.ELit l)@@ -637,7 +639,7 @@               , Type                   -- length of sequence               ) -inferCArm _ [] = panic "inferCArm" [ "Empty comprahension arm" ]+inferCArm _ [] = panic "inferCArm" [ "Empty comprehension arm" ] inferCArm _ [m] =   do (m1, x, t, n) <- inferMatch m      return ([m1], Map.singleton x t, n)@@ -649,7 +651,10 @@      return (m1 : ms', Map.insertWith (\_ old -> old) x t ds, tMul n n')  -- | @inferBinds isTopLevel isRec binds@ performs inference for a--- strongly-connected component of 'P.Bind's. If @isTopLevel@ is true,+-- strongly-connected component of 'P.Bind's.+-- If any of the members of the recursive group are already marked+-- as monomorphic, then we don't do generalzation.+-- If @isTopLevel@ is true, -- any bindings without type signatures will be generalized. If it is -- false, and the mono-binds flag is enabled, no bindings without type -- signatures will be generalized, but bindings with signatures will@@ -660,12 +665,11 @@      -- declarations, mark all bindings lacking signatures as monomorphic      monoBinds <- getMonoBinds      let (sigs,noSigs) = partition (isJust . P.bSignature) binds-         monos         = [ b { P.bMono = True } | b <- noSigs ]-         binds' | monoBinds && not isTopLevel = sigs ++ monos+         monos         = sigs ++ [ b { P.bMono = True } | b <- noSigs ]+         binds' | any P.bMono binds           = monos+                | monoBinds && not isTopLevel = monos                 | otherwise                   = binds --          check exprMap =         {- Guess type is here, because while we check user supplied signatures            we may generate additional constraints. For example, `x - y` would@@ -948,6 +952,10 @@   checkTyDecls (NT t mbD : ts) =     do t1 <- checkNewtype t mbD        withNewtype t1 (checkTyDecls ts)++  checkTyDecls (PT p mbD : ts) =+    do p1 <- checkPrimType p mbD+       withPrimType p1 (checkTyDecls ts)    -- We checked all type synonyms, now continue with value-level definitions:   checkTyDecls [] =

@@ -153,20 +153,13 @@   | CtExactType   | CtEnumeration   | CtDefaulting          -- ^ Just defaulting on the command line-  | CtPartialTypeFun TyFunName -- ^ Use of a partial type function.+  | CtPartialTypeFun Name -- ^ 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 | BuiltInTC TC-                deriving (Show, Generic, NFData) --instance PP TyFunName where-  ppPrec c (UserTyFun x)    = ppPrec c x-  ppPrec c (BuiltInTyFun x) = ppPrec c x-  ppPrec c (BuiltInTC x)    = ppPrec c x  instance TVars ConstraintSource where   apSubst su src =

@@ -6,16 +6,23 @@ -- Stability   :  provisional -- Portability :  portable {-# Language OverloadedStrings #-}-module Cryptol.TypeCheck.Instantiate (instantiateWith) where+module Cryptol.TypeCheck.Instantiate+  ( instantiateWith+  , TypeArg(..)+  , uncheckedTypeArg+  , MaybeCheckedType(..)+  ) where  import Cryptol.ModuleSystem.Name (nameIdent) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)+import Cryptol.TypeCheck.Kind(checkType) import Cryptol.TypeCheck.Error import Cryptol.Parser.Position (Located(..)) import Cryptol.Utils.Ident (Ident) import Cryptol.Utils.Panic(panic)+import qualified Cryptol.Parser.AST as P  import Control.Monad(zipWithM) import Data.Function (on)@@ -25,9 +32,37 @@ import qualified Data.Set as Set  +data TypeArg = TypeArg+  { tyArgName :: Maybe (Located Ident)+  , tyArgType :: MaybeCheckedType+  } -instantiateWith :: Name -> Expr -> Schema -> [Located (Maybe Ident,Type)]-                -> InferM (Expr,Type)+uncheckedTypeArg :: P.TypeInst Name -> TypeArg+uncheckedTypeArg a =+  case a of+    P.NamedInst x ->+      TypeArg { tyArgName = Just (P.name x), tyArgType = Unchecked (P.value x) }+    P.PosInst t ->+      TypeArg { tyArgName = Nothing, tyArgType = Unchecked t }+++data MaybeCheckedType = Checked Type | Unchecked (P.Type Name)++++checkTyParam :: TVarSource -> Kind -> MaybeCheckedType -> InferM Type+checkTyParam src k mb =+  case mb of+    Checked t+      | k == k'   -> pure t+      | otherwise -> do recordError (KindMismatch k k')+                        newType src k+        where k' = kindOf t+    Unchecked t -> checkType t (Just k)++++instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr,Type) instantiateWith nm e s ts   | null named      = instantiateWithPos nm e s positional   | null positional = instantiateWithNames nm e s named@@ -36,27 +71,25 @@    where   (named,positional) = partitionEithers (map classify ts)-  classify t = case thing t of-                 (Just n,ty)  -> Left t { thing = (n,ty) }-                 (Nothing,ty) -> Right ty+  classify t = case tyArgName t of+                 Just n  -> Left n { thing = (thing n, tyArgType t) }+                 Nothing -> Right (tyArgType t)  -instantiateWithPos :: Name -> Expr -> Schema -> [Type] -> InferM (Expr,Type)++instantiateWithPos ::+  Name -> Expr -> Schema -> [MaybeCheckedType] -> InferM (Expr,Type) instantiateWithPos nm e (Forall as ps t) ts =   do su <- makeSu (1::Int) [] as ts      doInst su e ps t   where   isNamed q = isJust (tpName q) -  makeSu n su (q : qs) (ty : tys)+  makeSu n su (q : qs) (mbty : tys)     | not (isNamed q) = do r <- unnamed n q-                           makeSu (n+1) (r : su) qs (ty : tys)-    | k1 == k2        = makeSu (n+1) ((q, ty) : su) qs tys-    | otherwise       = do recordError (KindMismatch k1 k2)-                           r <- unnamed n q-                           makeSu (n+1) (r : su) qs tys-      where k1 = kindOf q-            k2 = kindOf ty+                           makeSu (n+1) (r : su) qs (mbty : tys)+    | otherwise = do ty <- checkTyParam (TypeParamInstPos nm n) (kindOf q) mbty+                     makeSu (n+1) ((q,ty) : su) qs tys    makeSu _ su [] []       = return (reverse su)   makeSu n su (q : qs) [] = do r <- unnamed n q@@ -79,7 +112,6 @@   - {- | Instantiate an expression of the given polymorphic type. The arguments that are provided will be instantiated as requested, the rest will be instantiated with fresh type variables.@@ -90,7 +122,8 @@   - There will be one `ETApp t` for each insantiated type parameter;   - there will be one `EProofApp` for each constraint on the schema; -}-instantiateWithNames :: Name -> Expr -> Schema -> [Located (Ident,Type)]+instantiateWithNames ::+  Name -> Expr -> Schema -> [Located (Ident,MaybeCheckedType)]                      -> InferM (Expr,Type) instantiateWithNames nm e (Forall as ps t) xs =   do sequence_ repeatedParams@@ -109,13 +142,7 @@                    Just na -> TypeParamInstNamed nm (nameIdent na)                    Nothing -> TypeParamInstPos nm n        ty <- case lkp =<< tpName x of-               Just lty-                 | k1 == k   -> return ty-                 | otherwise -> inRange (srcRange lty) $-                                  do recordError (KindMismatch k k1)-                                     newType src k-                  where ty = snd (thing lty)-                        k1 = kindOf ty+               Just lty -> checkTyParam src k (snd (thing lty))                Nothing -> newType src k        return (x, ty) 

@@ -12,6 +12,7 @@   ( checkType   , checkSchema   , checkNewtype+  , checkPrimType   , checkTySyn   , checkPropSyn   , checkParameterType@@ -26,15 +27,15 @@ import           Cryptol.TypeCheck.Monad hiding (withTParams) import           Cryptol.TypeCheck.SimpType(tRebuild) import           Cryptol.TypeCheck.SimpleSolver(simplify)-import           Cryptol.TypeCheck.Solve (simplifyAllConstraints-                                         ,wfTypeFunction,wfTC)+import           Cryptol.TypeCheck.Solve (simplifyAllConstraints)+import           Cryptol.TypeCheck.Subst(listSubst,apSubst) import           Cryptol.Utils.Panic (panic)  import qualified Data.Map as Map import           Data.List(sortBy,groupBy) import           Data.Maybe(fromMaybe) import           Data.Function(on)-import           Control.Monad(unless,forM)+import           Control.Monad(unless,forM,when)   @@ -74,7 +75,7 @@  -- | Check a type-synonym declaration. checkTySyn :: P.TySyn Name -> Maybe String -> InferM TySyn-checkTySyn (P.TySyn x as t) mbD =+checkTySyn (P.TySyn x _ as t) mbD =   do ((as1,t1),gs) <- collectGoals                     $ inRange (srcRange x)                     $ do r <- withTParams NoWildCards tySynParam as@@ -90,7 +91,7 @@  -- | Check a constraint-synonym declaration. checkPropSyn :: P.PropSyn Name -> Maybe String -> InferM TySyn-checkPropSyn (P.PropSyn x as ps) mbD =+checkPropSyn (P.PropSyn x _ as ps) mbD =   do ((as1,t1),gs) <- collectGoals                     $ inRange (srcRange x)                     $ do r <- withTParams NoWildCards propSynParam as@@ -126,7 +127,17 @@                     , ntDoc = mbD                     } -+checkPrimType :: P.PrimType Name -> Maybe String -> InferM AbstractType+checkPrimType p mbD =+  do let (as,cs) = P.primTCts p+     (as',cs') <- withTParams NoWildCards (TPOther . Just) as $+                    mapM checkProp cs+     pure AbstractType { atName = thing (P.primTName p)+                       , atKind = cvtK (thing (P.primTKind p))+                       , atFixitiy = P.primTFixity p+                       , atCtrs = (as',cs')+                       , atDoc = mbD+                       }  checkType :: P.Type Name -> Maybe Kind -> InferM Type checkType t k =@@ -211,6 +222,7 @@ cvtK :: P.Kind -> Kind cvtK P.KNum  = KNum cvtK P.KType = KType+cvtK P.KProp = KProp cvtK (P.KFun k1 k2) = cvtK k1 :-> cvtK k2  @@ -224,10 +236,11 @@   do (ts1,k1) <- appTy ts0 (kindOf tc)      checkKind (TCon tc ts1) k k1 + -- | Check a type application of a non built-in type or type variable. checkTUser ::   Name          {- ^ The name that is being applied to some arguments. -} ->-  [P.Type Name] {- ^ Type synonym parameters -} ->+  [P.Type Name] {- ^ Parameters to the type -} ->   Maybe Kind    {- ^ Expected kind -} ->   KindM Type    {- ^ Resulting type -} checkTUser x ts k =@@ -235,6 +248,7 @@   mcase kLookupTSyn       checkTySynUse $   mcase kLookupNewtype    checkNewTypeUse $   mcase kLookupParamType  checkModuleParamUse $+  mcase kLookupAbstractType checkAbstractTypeUse $   checkScopedVarUse -- none of the above, must be a scoped type variable,                     -- if the renamer did its job correctly.   where@@ -244,7 +258,7 @@        ts2 <- checkParams as ts1        let su = zip as ts2        ps1 <- mapM (`kInstantiateT` su) (tsConstraints tysyn)-       kNewGoals (CtPartialTypeFun (UserTyFun (tsName tysyn))) ps1+       kNewGoals (CtPartialTypeFun (tsName tysyn)) ps1        t1  <- kInstantiateT (tsDef tysyn) su        checkKind (TUser x ts1 t1) k k1 @@ -254,10 +268,24 @@        ts2 <- checkParams (ntParams nt) ts1        return (TCon tc ts2) +  checkAbstractTypeUse absT =+    do let tc   = abstractTypeTC absT+       (ts1,k1) <- appTy ts (kindOf tc)+       let (as,ps) = atCtrs absT+       case ps of+          [] -> pure ()   -- common case+          _ -> do let need = length as+                      have = length ts1+                  when (need > have) $+                     kRecordError (TooFewTyParams (atName absT) (need - have))+                  let su = listSubst (map tpVar as `zip` ts1)+                  kNewGoals (CtPartialTypeFun (atName absT)) (apSubst su <$> ps)+       checkKind (TCon tc ts1) k k1+   checkParams as ts1     | paramHave == paramNeed = return ts1     | paramHave < paramNeed  =-                   do kRecordError (TooFewTySynParams x (paramNeed-paramHave))+                   do kRecordError (TooFewTyParams x (paramNeed-paramHave))                       let src = TypeErrorPlaceHolder                       fake <- mapM (kNewType src . kindOf . tpVar)                                    (drop paramHave as)@@ -344,24 +372,8 @@     P.TSeq t1 t2    -> tcon (TC TCSeq)                 [t1,t2] k     P.TBit          -> tcon (TC TCBit)                 [] k     P.TNum n        -> tcon (TC (TCNum n))             [] k-    P.TChar n       -> tcon (TC (TCNum $ fromIntegral $ fromEnum n)) [] k-    P.TApp tc ts    ->-      do it <- tcon tc ts k--         -- Now check for additional well-formedness-         -- constraints.-         case it of-           TCon (TF f) ts' ->-              case wfTypeFunction f ts' of-                 [] -> return ()-                 ps -> kNewGoals (CtPartialTypeFun (BuiltInTyFun f)) ps-           TCon (TC f) ts' ->-              case wfTC f ts' of-                 [] -> return ()-                 ps -> kNewGoals (CtPartialTypeFun (BuiltInTC f)) ps-           _ -> return ()+    P.TChar n       -> tcon (TC (TCNum $ toInteger $ fromEnum n)) [] k -         return it     P.TTuple ts     -> tcon (TC (TCTuple (length ts))) ts k      P.TRecord fs    -> do t1 <- TRec `fmap` mapM checkF fs@@ -372,9 +384,7 @@      P.TParens t     -> doCheckType t k -    P.TInfix{}      -> panic "KindCheck"-                       [ "TInfix not removed by the renamer", show ty ]-+    P.TInfix t x _ u-> doCheckType (P.TUser (thing x) [t, u]) k    where   checkF f = do t <- kInRange (srcRange (name f))@@ -386,21 +396,7 @@ -- | Validate a parsed proposition. checkProp :: P.Prop Name      -- ^ Proposition that need to be checked           -> KindM Type       -- ^ Checked representation-checkProp prop =-  case prop of-    P.CFin t1        -> tcon (PC PFin)           [t1]    (Just KProp)-    P.CEqual t1 t2   -> tcon (PC PEqual)         [t1,t2] (Just KProp)-    P.CNeq t1 t2     -> tcon (PC PNeq)           [t1,t2] (Just KProp)-    P.CGeq t1 t2     -> tcon (PC PGeq)           [t1,t2] (Just KProp)-    P.CZero t1       -> tcon (PC PZero)          [t1]    (Just KProp)-    P.CLogic t1      -> tcon (PC PLogic)         [t1]    (Just KProp)-    P.CArith t1      -> tcon (PC PArith)         [t1]    (Just KProp)-    P.CCmp t1        -> tcon (PC PCmp)           [t1]    (Just KProp)-    P.CSignedCmp t1  -> tcon (PC PSignedCmp)     [t1]    (Just KProp)-    P.CLiteral t1 t2 -> tcon (PC PLiteral)       [t1,t2] (Just KProp)-    P.CUser x ts     -> checkTUser x ts (Just KProp)-    P.CLocated p r1  -> kInRange r1 (checkProp p)-    P.CType _        -> panic "checkProp" [ "Unexpected CType", show prop ]+checkProp (P.CType t) = doCheckType t (Just KProp)   -- | Check that a type has the expected kind.

@@ -61,6 +61,7 @@   , inpVars      :: Map Name Schema   -- ^ Variables that are in scope   , inpTSyns     :: Map Name TySyn    -- ^ Type synonyms that are in scope   , inpNewtypes  :: Map Name Newtype  -- ^ Newtypes in scope+  , inpAbstractTypes :: Map Name AbstractType -- ^ Abstract types in scope      -- When typechecking a module these start off empty.     -- We need them when type-checking an expression at the command@@ -121,6 +122,7 @@                          , iTVars         = []                          , iTSyns         = fmap mkExternal (inpTSyns info)                          , iNewtypes      = fmap mkExternal (inpNewtypes info)+                         , iAbstractTypes = mkExternal <$> inpAbstractTypes info                          , iParamTypes    = inpParamTypes info                          , iParamFuns     = inpParamFuns info                          , iParamConstraints = inpParamConstraints info@@ -202,6 +204,7 @@    -- So, either a type-synonym shadows a newtype, or it was declared    -- at the top-level, but then there can't be a newtype with the    -- same name (this should be caught by the renamer).+  , iAbstractTypes :: Map Name (DefLoc, AbstractType)    , iParamTypes :: Map Name ModTParam     -- ^ Parameter types@@ -615,6 +618,9 @@ lookupNewtype :: Name -> InferM (Maybe Newtype) lookupNewtype x = fmap (fmap snd . Map.lookup x) getNewtypes +lookupAbstractType :: Name -> InferM (Maybe AbstractType)+lookupAbstractType x = fmap (fmap snd . Map.lookup x) getAbstractTypes+ -- | Lookup the kind of a parameter type lookupParamType :: Name -> InferM (Maybe ModTParam) lookupParamType x = Map.lookup x <$> getParamTypes@@ -637,6 +643,7 @@            [] ->               do recordError $ ErrorMsg                              $ text "Undefined type" <+> quotes (pp x)+                                    <+> text (show x)                  newType TypeErrorPlaceHolder k             sc : more ->@@ -653,6 +660,10 @@ getNewtypes :: InferM (Map Name (DefLoc,Newtype)) getNewtypes = IM $ asks iNewtypes +-- | Returns the abstract type declarations that are in scope.+getAbstractTypes :: InferM (Map Name (DefLoc,AbstractType))+getAbstractTypes = IM $ asks iAbstractTypes+ -- | Returns the parameter functions declarations getParamFuns :: InferM (Map Name ModVParam) getParamFuns = IM $ asks iParamFuns@@ -733,6 +744,14 @@   IM $ mapReader         (\r -> r { iNewtypes = Map.insert (ntName t) (IsLocal,t)                                                      (iNewtypes r) }) m++withPrimType :: AbstractType -> InferM a -> InferM a+withPrimType t (IM m) =+  IM $ mapReader+      (\r -> r { iAbstractTypes = Map.insert (atName t) (IsLocal,t)+                                                        (iAbstractTypes r) }) m++ withParamType :: ModTParam -> InferM a -> InferM a withParamType a (IM m) =   IM $ mapReader@@ -870,6 +889,9 @@ kRecordWarning :: Warning -> KindM () kRecordWarning w = kInInferM $ recordWarning w +kIO :: IO a -> KindM a+kIO m = KM $ lift $ lift $ io m+ -- | Generate a fresh unification variable of the given kind. -- NOTE:  We do not simplify these, because we end up with bottom. -- See `Kind.hs`@@ -890,6 +912,9 @@  kLookupParamType :: Name -> KindM (Maybe ModTParam) kLookupParamType x = kInInferM (lookupParamType x)++kLookupAbstractType :: Name -> KindM (Maybe AbstractType)+kLookupAbstractType x = kInInferM $ lookupAbstractType x  kExistTVar :: Name -> Kind -> KindM Type kExistTVar x k = kInInferM $ existVar x k

@@ -256,7 +256,7 @@            (_,_)      -> reportError (BadProofTyVars as)  -    -- XXX: Check that defined things are disitnct?+    -- XXX: Check that defined things are distinct?     EWhere e dgs ->       let go []       = exprSchema e           go (d : ds) = do xs <- checkDeclGroup d@@ -326,7 +326,7 @@                Just len ->                  case tNoUser n of                    TCon (TC (TCNum m)) []-                     | m == fromIntegral len -> return ()+                     | m == toInteger len -> return ()                    _ -> reportError $ UnexpectedSequenceShape len n               return elT

@@ -12,9 +12,6 @@   ( simplifyAllConstraints   , proveImplication   , proveModuleTopLevel-  , wfType-  , wfTypeFunction-  , wfTC   , defaultAndSimplify   , defaultReplExpr   ) where@@ -50,46 +47,6 @@   -{- | Add additional constraints that ensure validity of type function.-Note that these constraints do not introduce additional malformed types,-so the well-formedness constraints are guaranteed to be well-formed.-This assumes that the parameters are well-formed. -}-wfTypeFunction :: TFun -> [Type] -> [Prop]-wfTypeFunction TCSub [a,b]             = [ a >== b, pFin b]-wfTypeFunction TCDiv [a,b]             = [ b >== tOne, pFin a ]-wfTypeFunction TCMod [a,b]             = [ b >== tOne, pFin a ]-wfTypeFunction TCCeilDiv [a,b]         = [ pFin a, pFin b, b >== tOne ]-wfTypeFunction TCCeilMod [a,b]         = [ pFin a, pFin b, b >== tOne ]-wfTypeFunction TCLenFromThenTo [a,b,c] = [ pFin a, pFin b, pFin c, a =/= b ]-wfTypeFunction _ _                     = []---- | Add additional constraints that ensure validity of a type--- constructor application. Note that the constraints do not use any--- partial type functions, so the new constraints are guaranteed to be--- well-formed. This assumes that the parameters are well-formed.-wfTC :: TC -> [Type] -> [Prop]-wfTC TCIntMod [n] = [ pFin n, n >== tOne ]-wfTC _ _          = []---- | Add additional constraints that ensure the validity of a type.-wfType :: Type -> [Prop]-wfType t =-  case t of-    TCon c ts ->-      let ps = concatMap wfType ts-      in case c of-           TF f -> wfTypeFunction f ts ++ ps-           TC f -> wfTC f ts ++ ps-           _    -> ps--    TVar _      -> []-    TUser _ _ s -> wfType s-    TRec fs     -> concatMap (wfType . snd) fs-------------------------------------------------------------------------------------   quickSolverIO :: Ctxt -> [Goal] -> IO (Either Goal (Subst,[Goal]))

@@ -129,7 +129,12 @@   TCon (TC TCBit) [] -> SolvedIf [ pFin n ]    -- variables are not solvable.-  TVar {} -> Unsolved+  TVar {} -> case tNoUser n of+                {- We are sure that the lenght is not `fin`, so the+                special case for `Bit` does not apply.+                Arith ty => Arith [n]ty -}+                TCon (TC TCInf) [] -> SolvedIf [ pArith ty ]+                _                  -> Unsolved    -- Arith ty => Arith [n]ty   _ -> SolvedIf [ pArith ty ]

@@ -76,7 +76,7 @@                    Nothing -> return Nothing                    Just t  ->                      do let su = listParamSubst (zip (ntParams nt) ts)-                        newGoals (CtPartialTypeFun $ UserTyFun x)+                        newGoals (CtPartialTypeFun x)                           $ apSubst su $ ntConstraints nt                         return $ Just $ apSubst su t         _ -> return Nothing

@@ -0,0 +1,314 @@+{-# Language DeriveGeneric, DeriveAnyClass #-}+module Cryptol.TypeCheck.TCon where++import qualified Data.Map as Map+import GHC.Generics (Generic)+import Control.DeepSeq++import Cryptol.Parser.Selector+import Cryptol.Parser.Fixity+import qualified Cryptol.ModuleSystem.Name as M+import Cryptol.Utils.Ident+import Cryptol.Utils.PP++-- | This is used for pretty prinitng.+-- XXX: it would be nice to just rely in the info from the Prelude.+infixPrimTy :: TCon -> Maybe (Ident,Fixity)+infixPrimTy = \tc -> Map.lookup tc mp+  where+  mp = Map.fromList+          [ tInfix "=="  PC PEqual    (n 20)+          , tInfix "!="  PC PNeq      (n 20)+          , tInfix ">="  PC PGeq      (n 30)+          , tInfix  "+"  TF TCAdd     (l 80)+          , tInfix  "-"  TF TCSub     (l 80)+          , tInfix  "*"  TF TCMul     (l 90)+          , tInfix  "/"  TF TCDiv     (l 90)+          , tInfix  "%"  TF TCMod     (l 90)+          , tInfix  "^^" TF TCExp     (r 95)+          , tInfix  "/^" TF TCCeilDiv (l 90)+          , tInfix  "%^" TF TCCeilMod (l 90)+          ]++  r x = Fixity { fAssoc = RightAssoc, fLevel = x }+  l x = Fixity { fAssoc = LeftAssoc,  fLevel = x }+  n x = Fixity { fAssoc = NonAssoc,   fLevel = x }++  tInfix x mk tc f = (mk tc, (packIdent x, f))+++builtInType :: M.Name -> Maybe TCon+builtInType nm =+  case M.nameInfo nm of+    M.Declared m _+      | m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes+    _ -> Nothing++  where+  x ~> y = (packIdent x, y)++  builtInTypes = Map.fromList+    [ -- Types+      "inf"               ~> TC TCInf+    , "Bit"               ~> TC TCBit+    , "Integer"           ~> TC TCInteger+    , "Z"                 ~> TC TCIntMod++      -- Predicate contstructors+    , "=="                ~> PC PEqual+    , "!="                ~> PC PNeq+    , ">="                ~> PC PGeq+    , "fin"               ~> PC PFin+    , "Zero"              ~> PC PZero+    , "Logic"             ~> PC PLogic+    , "Arith"             ~> PC PArith+    , "Cmp"               ~> PC PCmp+    , "SignedCmp"         ~> PC PSignedCmp+    , "Literal"           ~> PC PLiteral++    -- Type functions+    , "+"                ~> TF TCAdd+    , "-"                ~> TF TCSub+    , "*"                ~> TF TCMul+    , "/"                ~> TF TCDiv+    , "%"                ~> TF TCMod+    , "^^"               ~> TF TCExp+    , "width"            ~> TF TCWidth+    , "min"              ~> TF TCMin+    , "max"              ~> TF TCMax+    , "/^"               ~> TF TCCeilDiv+    , "%^"               ~> TF TCCeilMod+    , "lengthFromThenTo" ~> TF TCLenFromThenTo+    ]+++++--------------------------------------------------------------------------------++infixr 5 :->++-- | Kinds, classify types.+data Kind   = KType+            | KNum+            | KProp+            | Kind :-> Kind+              deriving (Eq, Ord, Show, Generic, NFData)++class HasKind t where+  kindOf :: t -> Kind++instance HasKind TCon where+  kindOf (TC tc)      = kindOf tc+  kindOf (PC pc)      = kindOf pc+  kindOf (TF tf)      = kindOf tf+  kindOf (TError k _) = k++instance HasKind UserTC where+  kindOf (UserTC _ k) = k++instance HasKind TC where+  kindOf tcon =+    case tcon of+      TCNum _   -> KNum+      TCInf     -> KNum+      TCBit     -> KType+      TCInteger -> KType+      TCIntMod  -> KNum :-> KType+      TCSeq     -> KNum :-> KType :-> KType+      TCFun     -> KType :-> KType :-> KType+      TCTuple n -> foldr (:->) KType (replicate n KType)+      TCNewtype x -> kindOf x+      TCAbstract x -> kindOf x++instance HasKind PC where+  kindOf pc =+    case pc of+      PEqual     -> KNum :-> KNum :-> KProp+      PNeq       -> KNum :-> KNum :-> KProp+      PGeq       -> KNum :-> KNum :-> KProp+      PFin       -> KNum :-> KProp+      PHas _     -> KType :-> KType :-> KProp+      PZero      -> KType :-> KProp+      PLogic     -> KType :-> KProp+      PArith     -> KType :-> KProp+      PCmp       -> KType :-> KProp+      PSignedCmp -> KType :-> KProp+      PLiteral   -> KNum :-> KType :-> KProp+      PAnd       -> KProp :-> KProp :-> KProp+      PTrue      -> KProp++instance HasKind TFun where+  kindOf tfun =+    case tfun of+      TCWidth   -> KNum :-> KNum++      TCAdd     -> KNum :-> KNum :-> KNum+      TCSub     -> KNum :-> KNum :-> KNum+      TCMul     -> KNum :-> KNum :-> KNum+      TCDiv     -> KNum :-> KNum :-> KNum+      TCMod     -> KNum :-> KNum :-> KNum+      TCExp     -> KNum :-> KNum :-> KNum+      TCMin     -> KNum :-> KNum :-> KNum+      TCMax     -> KNum :-> KNum :-> KNum+      TCCeilDiv -> KNum :-> KNum :-> KNum+      TCCeilMod -> KNum :-> KNum :-> KNum++      TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum++++-- | Type constants.+data TCon   = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage+              deriving (Show, Eq, Ord, Generic, NFData)+++-- | Predicate symbols.+-- If you add additional user-visible constructors, please update 'primTys'.+data PC     = PEqual        -- ^ @_ == _@+            | PNeq          -- ^ @_ /= _@+            | PGeq          -- ^ @_ >= _@+            | PFin          -- ^ @fin _@++            -- classes+            | PHas Selector -- ^ @Has sel type field@ does not appear in schemas+            | PZero         -- ^ @Zero _@+            | PLogic        -- ^ @Logic _@+            | PArith        -- ^ @Arith _@+            | PCmp          -- ^ @Cmp _@+            | PSignedCmp    -- ^ @SignedCmp _@+            | PLiteral      -- ^ @Literal _ _@++            | PAnd          -- ^ This is useful when simplifying things in place+            | PTrue         -- ^ Ditto+              deriving (Show, Eq, Ord, Generic, NFData)++-- | 1-1 constants.+-- If you add additional user-visible constructors, please update 'primTys'.+data TC     = TCNum Integer            -- ^ Numbers+            | TCInf                    -- ^ Inf+            | TCBit                    -- ^ Bit+            | TCInteger                -- ^ Integer+            | TCIntMod                 -- ^ @Z _@+            | TCSeq                    -- ^ @[_] _@+            | TCFun                    -- ^ @_ -> _@+            | TCTuple Int              -- ^ @(_, _, _)@+            | TCAbstract UserTC        -- ^ An abstract type+            | TCNewtype UserTC         -- ^ user-defined, @T@+              deriving (Show, Eq, Ord, Generic, NFData)+++data UserTC = UserTC M.Name Kind+              deriving (Show, Generic, NFData)++instance Eq UserTC where+  UserTC x _ == UserTC y _ = x == y++instance Ord UserTC where+  compare (UserTC x _) (UserTC y _) = compare x y+++++data TCErrorMessage = TCErrorMessage+  { tcErrorMessage :: !String+    -- XXX: Add location?+  } deriving (Show, Eq, Ord, Generic, NFData)+++-- | Built-in type functions.+-- If you add additional user-visible constructors,+-- please update 'primTys' in "Cryptol.Prims.Types".+data TFun++  = TCAdd                 -- ^ @ : Num -> Num -> Num @+  | TCSub                 -- ^ @ : Num -> Num -> Num @+  | TCMul                 -- ^ @ : Num -> Num -> Num @+  | TCDiv                 -- ^ @ : Num -> Num -> Num @+  | TCMod                 -- ^ @ : Num -> Num -> Num @+  | TCExp                 -- ^ @ : Num -> Num -> Num @+  | TCWidth               -- ^ @ : Num -> Num @+  | TCMin                 -- ^ @ : Num -> Num -> Num @+  | TCMax                 -- ^ @ : Num -> Num -> Num @+  | TCCeilDiv             -- ^ @ : Num -> Num -> Num @+  | TCCeilMod             -- ^ @ : Num -> Num -> Num @++  -- Computing the lengths of explicit enumerations+  | TCLenFromThenTo       -- ^ @ : Num -> Num -> Num -> Num@+    -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@++    deriving (Show, Eq, Ord, Bounded, Enum, Generic, NFData)++++--------------------------------------------------------------------------------+-- Pretty printing++instance PP Kind where+  ppPrec p k = case k of+    KType   -> char '*'+    KNum    -> char '#'+    KProp   -> text "Prop"+    l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r])++instance PP TCon where+  ppPrec _ (TC tc)        = pp tc+  ppPrec _ (PC tc)        = pp tc+  ppPrec _ (TF tc)        = pp tc+  ppPrec _ (TError _ msg) = pp msg+++instance PP TCErrorMessage where+  ppPrec _ tc = parens (text "error:" <+> text (tcErrorMessage tc))++instance PP PC where+  ppPrec _ x =+    case x of+      PEqual     -> text "(==)"+      PNeq       -> text "(/=)"+      PGeq       -> text "(>=)"+      PFin       -> text "fin"+      PHas sel   -> parens (ppSelector sel)+      PZero      -> text "Zero"+      PLogic     -> text "Logic"+      PArith     -> text "Arith"+      PCmp       -> text "Cmp"+      PSignedCmp -> text "SignedCmp"+      PLiteral   -> text "Literal"+      PTrue      -> text "True"+      PAnd       -> text "(&&)"++instance PP TC where+  ppPrec _ x =+    case x of+      TCNum n   -> integer n+      TCInf     -> text "inf"+      TCBit     -> text "Bit"+      TCInteger -> text "Integer"+      TCIntMod  -> text "Z"+      TCSeq     -> text "[]"+      TCFun     -> text "(->)"+      TCTuple 0 -> text "()"+      TCTuple 1 -> text "(one tuple?)"+      TCTuple n -> parens $ hcat $ replicate (n-1) comma+      TCNewtype u -> pp u+      TCAbstract u -> pp u++instance PP UserTC where+  ppPrec p (UserTC x _) = ppPrec p x++instance PP TFun where+  ppPrec _ tcon =+    case tcon of+      TCAdd             -> text "+"+      TCSub             -> text "-"+      TCMul             -> text "*"+      TCDiv             -> text "/"+      TCMod             -> text "%"+      TCExp             -> text "^^"+      TCWidth           -> text "width"+      TCMin             -> text "min"+      TCMax             -> text "max"+      TCCeilDiv         -> text "/^"+      TCCeilMod         -> text "%^"+      TCLenFromThenTo   -> text "lengthFromThenTo"

@@ -4,7 +4,7 @@ {-# Language OverloadedStrings #-} module Cryptol.TypeCheck.Type   ( module Cryptol.TypeCheck.Type-  , module Cryptol.Prims.Syntax+  , module Cryptol.TypeCheck.TCon   ) where  @@ -21,8 +21,8 @@ import Cryptol.Parser.Fixity import Cryptol.Parser.Position(Range,emptyRange) import Cryptol.ModuleSystem.Name-import Cryptol.Prims.Syntax import Cryptol.Utils.Ident (Ident)+import Cryptol.TypeCheck.TCon import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Solver.InfNat import Cryptol.Utils.Panic(panic)@@ -186,8 +186,18 @@                         } deriving (Show, Generic, NFData)  +-- | Information about an abstract type.+data AbstractType = AbstractType+  { atName    :: Name+  , atKind    :: Kind+  , atCtrs    :: ([TParam], [Prop])+  , atFixitiy :: Maybe Fixity+  , atDoc     :: Maybe String+  } deriving (Show, Generic, NFData)  ++ --------------------------------------------------------------------------------  @@ -278,6 +288,12 @@   as = ntParams nt  +abstractTypeTC :: AbstractType -> TCon+abstractTypeTC at =+  case builtInType (atName at) of+    Just tcon -> tcon+    _         -> TC $ TCAbstract $ UserTC (atName at) (atKind at)+ instance Eq TVar where   TVBound x       == TVBound y       = x == y   TVFree  x _ _ _ == TVFree  y _ _ _ = x == y@@ -433,7 +449,7 @@   tNum     :: Integral a => a -> Type-tNum n    = TCon (TC (TCNum (fromIntegral n))) []+tNum n    = TCon (TC (TCNum (toInteger n))) []  tZero     :: Type tZero     = tNum (0 :: Int)@@ -452,6 +468,9 @@               Inf   -> tInf               Nat n -> tNum n +tAbstract :: UserTC -> [Type] -> Type+tAbstract u ts = TCon (TC (TCAbstract u)) ts+ tBit     :: Type tBit      = TCon (TC TCBit) [] @@ -499,8 +518,12 @@  -- | Make a malformed numeric type. tBadNumber :: TCErrorMessage -> Type-tBadNumber msg = TCon (TError KNum msg) []+tBadNumber = tError KNum +-- | Make an error value of the given type.+tError :: Kind -> TCErrorMessage -> Type+tError k msg = TCon (TError k msg) []+ tf1 :: TFun -> Type -> Type tf1 f x = TCon (TF f) [x] @@ -510,14 +533,6 @@ tf3 :: TFun -> Type -> Type -> Type -> Type tf3 f x y z = TCon (TF f) [x,y,z] -{--tAdd :: Type -> Type -> Type-tAdd x y-  | Just x' <- tIsNum x-  , Just y' <- tIsNum y = error (show x' ++ " + " ++ show y')-  | otherwise = tf2 TCAdd x y--}- tSub :: Type -> Type -> Type tSub = tf2 TCSub @@ -716,13 +731,17 @@  instance PP (WithNames TySyn) where   ppPrec _ (WithNames ts ns) =-    text "type" <+> ctr <+> pp (tsName ts) <+>-      sep (map (ppWithNames ns1) (tsParams ts)) <+> char '='-                <+> ppWithNames ns1 (tsDef ts)+    text "type" <+> ctr <+> lhs <+> char '=' <+> ppWithNames ns1 (tsDef ts)     where ns1 = addTNames (tsParams ts) ns           ctr = case kindResult (kindOf ts) of                   KProp -> text "constraint"                   _     -> empty+          n = tsName ts+          lhs = case (nameFixity n, tsParams ts) of+                  (Just _, [x, y]) ->+                    ppWithNames ns1 x <+> pp (nameIdent n) <+> ppWithNames ns1 y+                  (_, ps) ->+                    pp n <+> sep (map (ppWithNames ns1) ps)  instance PP Newtype where   ppPrec = ppWithNamesPrec IntMap.empty@@ -739,8 +758,12 @@       TVar a  -> ppWithNames nmMap a       TRec fs -> braces $ fsep $ punctuate comma                     [ pp l <+> text ":" <+> go 0 t | (l,t) <- fs ]++      _ | Just tinf <- isTInfix ty0 -> optParens (prec > 2)+                                     $ ppInfix 2 isTInfix tinf++      TUser c [] _ -> pp c       TUser c ts _ -> optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts)-      -- TUser _ _ t -> ppPrec prec t -- optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts)        TCon (TC tc) ts ->         case (tc,ts) of@@ -777,23 +800,29 @@            (_, _)              -> pp pc <+> fsep (map (go 4) ts) -      _ | Just tinf <- isTInfix ty0 -> optParens (prec > 2)-                                     $ ppInfix 2 isTInfix tinf-       TCon f ts -> optParens (prec > 3)                 $ pp f <+> fsep (map (go 4) ts)      where     go p t = ppWithNamesPrec nmMap p t -    isTInfix (WithNames (TCon (TF ieOp) [ieLeft',ieRight']) _) =+    isTInfix (WithNames (TCon tc [ieLeft',ieRight']) _) =       do let ieLeft  = WithNames ieLeft' nmMap              ieRight = WithNames ieRight' nmMap-         pt <- primTyFromTF ieOp-         fi <- primTyFixity pt+         (ieOp,fi) <- infixPrimTy tc          let ieAssoc = fAssoc fi              iePrec  = fLevel fi          return Infix { .. }++    isTInfix (WithNames (TUser n [ieLeft',ieRight'] _) _) =+      do let ieLeft  = WithNames ieLeft' nmMap+             ieRight = WithNames ieRight' nmMap+         fi <- nameFixity n+         let ieAssoc = fAssoc fi+             iePrec  = fLevel fi+             ieOp    = nameIdent n+         return Infix { .. }+     isTInfix _ = Nothing  

@@ -10,7 +10,7 @@  {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE OverloadedStrings #-} module Cryptol.Utils.PP where  import           Cryptol.Utils.Ident@@ -149,7 +149,7 @@ data Infix op thing = Infix   { ieOp    :: op       -- ^ operator   , ieLeft  :: thing    -- ^ left argument-  , ieRight :: thing    -- ^ right argumrnt+  , ieRight :: thing    -- ^ right argument   , iePrec  :: Int      -- ^ operator precedence   , ieAssoc :: Assoc    -- ^ operator associativity   }@@ -177,7 +177,7 @@   --- | Display a numeric values as an ordinar (e.g., 2nd)+-- | Display a numeric value as an ordinal (e.g., 2nd) ordinal :: (Integral a, Show a, Eq a) => a -> Doc ordinal x = text (show x) <.> text (ordSuffix x) @@ -256,6 +256,9 @@ quotes :: Doc -> Doc quotes  = liftPJ1 PJ.quotes +backticks :: Doc -> Doc+backticks d = hcat [ "`", d, "`" ]+ punctuate :: Doc -> [Doc] -> [Doc] punctuate p = go   where@@ -293,3 +296,7 @@ instance PP ModName where   ppPrec _   = text . T.unpack . modNameToText +instance PP Assoc where+  ppPrec _ LeftAssoc  = text "left-associative"+  ppPrec _ RightAssoc = text "right-associative"+  ppPrec _ NonAssoc   = text "non-associative"