diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -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
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -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
diff --git a/cryptol.cabal b/cryptol.cabal
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -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 .
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,
diff --git a/cryptol/Main.hs b/cryptol/Main.hs
--- a/cryptol/Main.hs
+++ b/cryptol/Main.hs
@@ -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."
diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs
--- a/cryptol/REPL/Haskeline.hs
+++ b/cryptol/REPL/Haskeline.hs
@@ -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
diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -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
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@@ -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
diff --git a/src/Cryptol/Eval/Monad.hs b/src/Cryptol/Eval/Monad.hs
--- a/src/Cryptol/Eval/Monad.hs
+++ b/src/Cryptol/Eval/Monad.hs
@@ -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 "<>" <+> 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
diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs
--- a/src/Cryptol/Eval/Reference.lhs
+++ b/src/Cryptol/Eval/Reference.lhs
@@ -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
diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs
--- a/src/Cryptol/Eval/Type.hs
+++ b/src/Cryptol/Eval/Type.hs
@@ -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)
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -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
diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -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)
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -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
diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs
--- a/src/Cryptol/ModuleSystem/Env.hs
+++ b/src/Cryptol/ModuleSystem/Env.hs
@@ -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
diff --git a/src/Cryptol/ModuleSystem/Exports.hs b/src/Cryptol/ModuleSystem/Exports.hs
--- a/src/Cryptol/ModuleSystem/Exports.hs
+++ b/src/Cryptol/ModuleSystem/Exports.hs
@@ -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 {}) = []
diff --git a/src/Cryptol/ModuleSystem/InstantiateModule.hs b/src/Cryptol/ModuleSystem/InstantiateModule.hs
--- a/src/Cryptol/ModuleSystem/InstantiateModule.hs
+++ b/src/Cryptol/ModuleSystem/InstantiateModule.hs
@@ -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)
diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs
--- a/src/Cryptol/ModuleSystem/Interface.hs
+++ b/src/Cryptol/ModuleSystem/Interface.hs
@@ -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)
diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs
--- a/src/Cryptol/ModuleSystem/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Monad.hs
@@ -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
diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs
--- a/src/Cryptol/ModuleSystem/NamingEnv.hs
+++ b/src/Cryptol/ModuleSystem/NamingEnv.hs
@@ -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
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -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 -------------------------------------------------------------------
diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y
--- a/src/Cryptol/Parser.y
+++ b/src/Cryptol/Parser.y
@@ -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" } }
diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs
--- a/src/Cryptol/Parser/AST.hs
+++ b/src/Cryptol/Parser/AST.hs
@@ -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)
diff --git a/src/Cryptol/Parser/Fixity.hs b/src/Cryptol/Parser/Fixity.hs
--- a/src/Cryptol/Parser/Fixity.hs
+++ b/src/Cryptol/Parser/Fixity.hs
@@ -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
diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x
--- a/src/Cryptol/Parser/Lexer.x
+++ b/src/Cryptol/Parser/Lexer.x
@@ -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
diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs
--- a/src/Cryptol/Parser/LexerUtils.hs
+++ b/src/Cryptol/Parser/LexerUtils.hs
@@ -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)
diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs
--- a/src/Cryptol/Parser/Names.hs
+++ b/src/Cryptol/Parser/Names.hs
@@ -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))
diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs
--- a/src/Cryptol/Parser/NoInclude.hs
+++ b/src/Cryptol/Parser/NoInclude.hs
@@ -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]
diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs
--- a/src/Cryptol/Parser/NoPat.hs
+++ b/src/Cryptol/Parser/NoPat.hs
@@ -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 <+>
diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs
--- a/src/Cryptol/Parser/ParserUtils.hs
+++ b/src/Cryptol/Parser/ParserUtils.hs
@@ -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 ->
diff --git a/src/Cryptol/Parser/Selector.hs b/src/Cryptol/Parser/Selector.hs
--- a/src/Cryptol/Parser/Selector.hs
+++ b/src/Cryptol/Parser/Selector.hs
@@ -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
-
-
diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs
--- a/src/Cryptol/Parser/Unlit.hs
+++ b/src/Cryptol/Parser/Unlit.hs
@@ -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
diff --git a/src/Cryptol/Parser/Utils.hs b/src/Cryptol/Parser/Utils.hs
--- a/src/Cryptol/Parser/Utils.hs
+++ b/src/Cryptol/Parser/Utils.hs
@@ -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)
diff --git a/src/Cryptol/Prelude.hs b/src/Cryptol/Prelude.hs
--- a/src/Cryptol/Prelude.hs
+++ b/src/Cryptol/Prelude.hs
@@ -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|]
diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs
--- a/src/Cryptol/Prims/Eval.hs
+++ b/src/Cryptol/Prims/Eval.hs
@@ -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
diff --git a/src/Cryptol/Prims/Syntax.hs b/src/Cryptol/Prims/Syntax.hs
deleted file mode 100644
--- a/src/Cryptol/Prims/Syntax.hs
+++ /dev/null
@@ -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"
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -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.
diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs
--- a/src/Cryptol/REPL/Monad.hs
+++ b/src/Cryptol/REPL/Monad.hs
@@ -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
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -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
diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@@ -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
diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@@ -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
diff --git a/src/Cryptol/Testing/Concrete.hs b/src/Cryptol/Testing/Concrete.hs
--- a/src/Cryptol/Testing/Concrete.hs
+++ b/src/Cryptol/Testing/Concrete.hs
@@ -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 _ _ -> []
diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@@ -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.
diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs
--- a/src/Cryptol/Transform/Specialize.hs
+++ b/src/Cryptol/Transform/Specialize.hs
@@ -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
diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs
--- a/src/Cryptol/TypeCheck/AST.hs
+++ b/src/Cryptol/TypeCheck/AST.hs
@@ -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
diff --git a/src/Cryptol/TypeCheck/CheckModuleInstance.hs b/src/Cryptol/TypeCheck/CheckModuleInstance.hs
--- a/src/Cryptol/TypeCheck/CheckModuleInstance.hs
+++ b/src/Cryptol/TypeCheck/CheckModuleInstance.hs
@@ -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))) [])
diff --git a/src/Cryptol/TypeCheck/Depends.hs b/src/Cryptol/TypeCheck/Depends.hs
--- a/src/Cryptol/TypeCheck/Depends.hs
+++ b/src/Cryptol/TypeCheck/Depends.hs
@@ -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)
diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs
--- a/src/Cryptol/TypeCheck/Error.hs
+++ b/src/Cryptol/TypeCheck/Error.hs
@@ -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.")
diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/src/Cryptol/TypeCheck/Infer.hs
@@ -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 [] =
diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs
--- a/src/Cryptol/TypeCheck/InferTypes.hs
+++ b/src/Cryptol/TypeCheck/InferTypes.hs
@@ -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 =
diff --git a/src/Cryptol/TypeCheck/Instantiate.hs b/src/Cryptol/TypeCheck/Instantiate.hs
--- a/src/Cryptol/TypeCheck/Instantiate.hs
+++ b/src/Cryptol/TypeCheck/Instantiate.hs
@@ -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)
diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs
--- a/src/Cryptol/TypeCheck/Kind.hs
+++ b/src/Cryptol/TypeCheck/Kind.hs
@@ -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.
diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs
--- a/src/Cryptol/TypeCheck/Monad.hs
+++ b/src/Cryptol/TypeCheck/Monad.hs
@@ -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
diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs
--- a/src/Cryptol/TypeCheck/Sanity.hs
+++ b/src/Cryptol/TypeCheck/Sanity.hs
@@ -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
diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/src/Cryptol/TypeCheck/Solve.hs
@@ -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]))
diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs
--- a/src/Cryptol/TypeCheck/Solver/Class.hs
+++ b/src/Cryptol/TypeCheck/Solver/Class.hs
@@ -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 ]
diff --git a/src/Cryptol/TypeCheck/Solver/Selector.hs b/src/Cryptol/TypeCheck/Solver/Selector.hs
--- a/src/Cryptol/TypeCheck/Solver/Selector.hs
+++ b/src/Cryptol/TypeCheck/Solver/Selector.hs
@@ -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
diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs
new file mode 100644
--- /dev/null
+++ b/src/Cryptol/TypeCheck/TCon.hs
@@ -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"
diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
--- a/src/Cryptol/TypeCheck/Type.hs
+++ b/src/Cryptol/TypeCheck/Type.hs
@@ -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
diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs
--- a/src/Cryptol/Utils/PP.hs
+++ b/src/Cryptol/Utils/PP.hs
@@ -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"