GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-31 20:03:17 +03:00
Code Issues Projects Releases Wiki Activity

Rename primitive demote to the more self-explanatory name number.

Browse Source 
The name "demote" is only meaningful to those who already know what
the Cryptol primitive does. Also, due to recent changes in the error
and warning messages, the name "demote" is showing up much more often
in REPL output. For example:

    Defaulting type argument 'rep' of 'demote' to [2]

    Showing a specific instance of polymorphic result:
      * Using 'Integer' for type argument 'rep' of 'Cryptol::demote'

These messages will hopefully be made less confusing to non-experts
if the name "demote" is replaced with "number".
This commit is contained in:
Brian Huffman 2018-07-27 13:52:57 -07:00
parent 78fa2d58aa
commit f609b36225
33 changed files with 59 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
bench/data/PreludeWithExtras.cry
View File

@ -8,7 +8,7 @@ module Cryptol where
/**
* The value corresponding to a numeric type.
*/
primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
primitive number : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
infixr 10 ||
infixr 20 &&

50
docs/AbstractValuesAndModuleParameters.md
View File

@ -143,7 +143,7 @@ value parameters. To work around this we propose the following restriction:
type arguments*. So, for example `zero` instantiated with `2` may
be used as a module parameter, but `0x10 + 0x20` would not.
Note that literals are a special case of this schema because they
are just sugar for `demote`.
are just sugar for `number`.
With this restriction, the rule is that two module instantiations are the
same if they have the same parameters, where types are compared as usual,
@ -207,51 +207,3 @@ generates a fresh instance of everything, and one has to import the same module
if one wants to get the same types. It is unclear if this kind of named
instantiation is too heavy-weight for modules that have only a couple of
simple parameters...

2
docs/ProgrammingCryptol/prims/Primitives.tex
View File

@ -115,7 +115,7 @@ primsPlaceHolder=1;
% (%$) : {a} (Arith a) => a -> a -> a
% (/$) : {a} (Arith a) => a -> a -> a
% demote : {val, rep} (Literal val rep) => rep
% number : {val, rep} (Literal val rep) => rep
% elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
% fromThen :
% {first, next, bits, len} (fin first, fin next, fin bits,

2
lib/Cryptol.cry
View File

@ -8,7 +8,7 @@ module Cryptol where
/**
* The value corresponding to a numeric type.
*/
primitive demote : {val, rep} Literal val rep => rep
primitive number : {val, rep} Literal val rep => rep
infixr 5 ==>
infixr 10 \/

2
src/Cryptol/Eval/Monad.hs
View File

@ -189,7 +189,7 @@ evalPanic cxt = panic ("[Eval] " ++ cxt)
-- | Data type describing errors that can occur during evaluation.
data EvalError
= InvalidIndex Integer -- ^ Out-of-bounds index
| TypeCannotBeDemoted Type -- ^ Non-numeric type passed to demote function
| TypeCannotBeDemoted Type -- ^ Non-numeric type passed to @number@ function
| DivideByZero -- ^ Division or modulus by 0
| NegativeExponent -- ^ Exponentiation by negative integer
| LogNegative -- ^ Logarithm of a negative integer

4
src/Cryptol/Eval/Reference.lhs
View File

@ -501,7 +501,7 @@ Cryptol primitives fall into several groups:
* Logic: `&&`, `||`, `^`, `complement`, `zero`, `True`, `False`
* Arithmetic: `+`, `-`, `*`, `/`, `%`, `^^`, `lg2`, `negate`, `demote`
* Arithmetic: `+`, `-`, `*`, `/`, `%`, `^^`, `lg2`, `negate`, `number`
* Comparison: `<`, `>`, `<=`, `>=`, `==`, `!=`
@ -540,7 +540,7 @@ Cryptol primitives fall into several groups:
> , ("^^" , binary (arithBinary expWrap))
> , ("lg2" , unary (arithUnary lg2Wrap))
> , ("negate" , unary (arithUnary (\x -> Right (- x))))
> , ("demote" , vFinPoly $ \val ->
> , ("number" , vFinPoly $ \val ->
> VPoly $ \a ->
> arithNullary (Right val) a)
> , ("toInteger" , vFinPoly $ \_bits ->

6
src/Cryptol/Eval/Value.hs
View File

@ -805,9 +805,9 @@ toExpr prims t0 v0 = findOne (go t0 v0)
(TCon (TC TCBit) [], VBit True ) -> return (prim "True")
(TCon (TC TCBit) [], VBit False) -> return (prim "False")
(TCon (TC TCInteger) [], VInteger i) ->
return $ ETApp (ETApp (prim "demote") (tNum i)) ty
return $ ETApp (ETApp (prim "number") (tNum i)) ty
(TCon (TC TCIntMod) [_n], VInteger i) ->
return $ ETApp (ETApp (prim "demote") (tNum i)) ty
return $ ETApp (ETApp (prim "number") (tNum i)) ty
(TCon (TC TCSeq) [a,b], VSeq 0 _) -> do
guard (a == tZero)
return $ EList [] b
@ -818,7 +818,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do
BV w v <- lift (asWordVal =<< wval)
guard (a == tNum w)
return $ ETApp (ETApp (prim "demote") (tNum v)) ty
return $ ETApp (ETApp (prim "number") (tNum v)) ty
(_, VStream _) -> fail "cannot construct infinite expressions"
(_, VFun _) -> fail "cannot convert function values to expressions"
(_, VPoly _) -> fail "cannot convert polymorphic values to expressions"

10
src/Cryptol/Prims/Eval.hs
View File

@ -131,8 +131,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
carryV)
, ("scarry" , {-# SCC "Prelude::scarry" #-}
scarryV)
, ("demote" , {-# SCC "Prelude::demote" #-}
ecDemoteV)
, ("number" , {-# SCC "Prelude::number" #-}
ecNumberV)
, ("#" , {-# SCC "Prelude::(#)" #-}
nlam $ \ front ->
@ -228,11 +228,11 @@ mkLit ty =
| w >= Arch.maxBigIntWidth -> wordTooWide w
| otherwise -> word w
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
[ "Invalid type for demote" ]
[ "Invalid type for number" ]
-- | Make a numeric constant.
ecDemoteV :: BitWord b w i => GenValue b w i
ecDemoteV = nlam $ \valT ->
ecNumberV :: BitWord b w i => GenValue b w i
ecNumberV = nlam $ \valT ->
tlam $ \ty ->
case valT of
Nat v -> mkLit ty v

6
src/Cryptol/Symbolic/Prims.hs
View File

@ -38,7 +38,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
fromThenV, fromToV, fromThenToV,
transposeV, indexPrim,
ecToIntegerV, ecFromIntegerV,
ecDemoteV, updatePrim, randomV, liftWord,
ecNumberV, updatePrim, randomV, liftWord,
cmpValue, lg2)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Decl(..))
@ -79,8 +79,8 @@ primTable :: Map.Map Ident Value
primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
[ ("True" , VBit SBV.svTrue)
, ("False" , VBit SBV.svFalse)
, ("demote" , ecDemoteV) -- Converts a numeric type into its corresponding value.
-- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
, ("number" , ecNumberV) -- Converts a numeric type into its corresponding value.
-- { val, rep } (Literal val rep) => rep
, ("+" , binary (arithBinary (liftBinArith SBV.svPlus) (liftBin SBV.svPlus)
(const (liftBin SBV.svPlus)))) -- {a} (Arith a) => a -> a -> a
, ("-" , binary (arithBinary (liftBinArith SBV.svMinus) (liftBin SBV.svMinus)

2
src/Cryptol/TypeCheck/AST.hs
View File

@ -190,7 +190,7 @@ eString :: PrimMap -> String -> Expr
eString prims str = EList (map (eChar prims) str) tChar
eChar :: PrimMap -> Char -> Expr
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "demote")) (tNum v)) (tWord (tNum w))
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "number")) (tNum v)) (tWord (tNum w))
where v = fromEnum c
w = 8 :: Int

8
src/Cryptol/TypeCheck/Infer.hs
View File

@ -91,16 +91,16 @@ mkPrim' str =
desugarLiteral :: Bool -> P.Literal -> InferM (P.Expr Name)
desugarLiteral fixDec lit =
do l <- curRange
demotePrim <- mkPrim "demote"
numberPrim <- mkPrim "number"
let named (x,y) = P.NamedInst
P.Named { name = Located l (packIdent x), value = y }
demote fs = P.EAppT demotePrim (map named fs)
number fs = P.EAppT numberPrim (map named fs)
tBits n = P.TSeq (P.TNum n) P.TBit
return $ case lit of
P.ECNum num info ->
demote $ [ ("val", P.TNum num) ] ++ case info of
number $ [ ("val", P.TNum num) ] ++ case info of
P.BinLit n -> [ ("rep", tBits (1 * toInteger n)) ]
P.OctLit n -> [ ("rep", tBits (3 * toInteger n)) ]
P.HexLit n -> [ ("rep", tBits (4 * toInteger n)) ]
@ -355,7 +355,7 @@ checkE expr tGoal =
P.ETypeVal t ->
do l <- curRange
prim <- mkPrim "demote"
prim <- mkPrim "number"
checkE (P.EAppT prim
[P.NamedInst
P.Named { name = Located l (packIdent "val")

4
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -267,13 +267,13 @@ ppUse :: Expr -> Doc
ppUse expr =
case expr of
EVar (asPrim -> Just prim)
| identText prim == "demote" -> text "literal or demoted expression"
| identText prim == "number" -> text "literal or demoted expression"
| identText prim == "infFrom" -> text "infinite enumeration"
| identText prim == "infFromThen" -> text "infinite enumeration (with step)"
| identText prim == "fromThen" -> text "finite enumeration"
| identText prim == "fromTo" -> text "finite enumeration"
| identText prim == "fromThenTo" -> text "finite enumeration"
_ -> text "expression" <+> pp expr
_ -> text "expression" <+> pp expr
instance PP (WithNames Goal) where
ppPrec _ (WithNames g names) =

2
src/Cryptol/TypeCheck/Monad.hs
View File

@ -80,7 +80,7 @@ data InferInput = InferInput
, inpPrimNames :: !PrimMap
-- ^ This is used when the type-checker needs to refer to a predefined
-- identifier (e.g., @demote@).
-- identifier (e.g., @number@).
, inpSupply :: !Supply -- ^ The supply for fresh name generation
} deriving Show

2
src/Cryptol/TypeCheck/Parseable.hs
View File

@ -93,7 +93,7 @@ instance (ShowParseable a) => ShowParseable [a] where
text "]"
instance (ShowParseable a) => ShowParseable (Maybe a) where
showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow demote
showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow number
showParseable (Just x) = showParseable x
instance (ShowParseable a) => ShowParseable (Located a) where

2
tests/issues/Karatsuba.cry
View File

@ -2,7 +2,7 @@ module Karatsuba where
kmult : {limb,n} (fin n, fin limb, limb >= 6, n>=1) => [n] -> [n] -> [2*n]
kmult x y =
if `n <= (demote`{limb, [max (width limb) (width n)]}) then
if `n <= (`limb : [max (width limb) (width n)]) then
(zero#x)*(zero#y)
else
take (splitmult`{limb} (make_atleast`{limb} x) (make_atleast`{limb} y))

2
tests/issues/issue226.icry.stdout
View File

@ -56,7 +56,6 @@ Symbols
carry : {n} (fin n) => [n] -> [n] -> Bit
complement : {a} (Logic a) => a -> a
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
demote : {val, rep} (Literal val rep) => rep
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
error : {a, len} (fin len) => [len][8] -> a
@ -93,6 +92,7 @@ Symbols
max : {a} (Cmp a) => a -> a -> a
min : {a} (Cmp a) => a -> a -> a
negate : {a} (Arith a) => a -> a
number : {val, rep} (Literal val rep) => rep
or : {n} (fin n) => [n] -> Bit
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]

2
tests/issues/issue290.icry.stdout
View File

@ -2,7 +2,7 @@ Loading module Cryptol
Loading module issue290
Loading module issue290bar
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
* Using 'Integer' for type argument 'rep' of 'Cryptol::number'
2
0x1
0x1

2
tests/issues/issue323.icry.stdout
View File

@ -2,7 +2,7 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./issue323.cry:2:54--2:55:
Defaulting type argument 'rep' of 'demote' to [0]
Defaulting type argument 'rep' of 'number' to [0]
[error] at ./issue323.cry:2:1--3:51:
Failed to validate user-specified signature.

4
tests/mono-binds/test03.icry.stdout
View File

@ -10,7 +10,7 @@ test03::test = \{a} (fin a, a >= width a) ->
where
/* Not recursive */
test03::foo : {b} (Literal a b) => b
test03::foo = \{b} (Literal a b) -> Cryptol::demote a b <>
test03::foo = \{b} (Literal a b) -> Cryptol::number a b <>
@ -25,7 +25,7 @@ test03::test = \{a} (fin a, a >= width a) ->
where
/* Not recursive */
test03::foo : [a]
test03::foo = Cryptol::demote a [a] <>
test03::foo = Cryptol::number a [a] <>

2
tests/mono-binds/test04.icry.stdout
View File

@ -6,7 +6,7 @@ import Cryptol
/* Not recursive */
test04::test : {a, b} (Literal 10 b) => a -> ((a, ()), (a, b))
test04::test = \{a, b} (Literal 10 b) (a : a) ->
(test04::f () (), test04::f b (Cryptol::demote 10 b <>))
(test04::f () (), test04::f b (Cryptol::number 10 b <>))
where
/* Not recursive */
test04::f : {c} c -> (a, c)

12
tests/mono-binds/test05.icry.stdout
View File

@ -11,16 +11,16 @@ module test05
import Cryptol
/* Not recursive */
test05::foo : [10]
test05::foo = Cryptol::demote 10 [10] <>
test05::foo = Cryptol::number 10 [10] <>
/* Not recursive */
test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
Cryptol::demote 10 b <>
Cryptol::number 10 b <>
where
/* Not recursive */
test05::foo : [10]
test05::foo = Cryptol::demote 10 [10] <>
test05::foo = Cryptol::number 10 [10] <>
/* Not recursive */
test05::f : {m} (fin m) => [n + m]a
@ -54,16 +54,16 @@ module test05
import Cryptol
/* Not recursive */
test05::foo : [10]
test05::foo = Cryptol::demote 10 [10] <>
test05::foo = Cryptol::number 10 [10] <>
/* Not recursive */
test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
Cryptol::demote 10 b <>
Cryptol::number 10 b <>
where
/* Not recursive */
test05::foo : [10]
test05::foo = Cryptol::demote 10 [10] <>
test05::foo = Cryptol::number 10 [10] <>
/* Not recursive */
test05::f : [n]a

4
tests/parser/unary-2.icry.stdout
View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./unary-2.cry:3:22--3:23:
Defaulting type argument 'rep' of 'demote' to [2]
Defaulting type argument 'rep' of 'number' to [2]
[warning] at ./unary-2.cry:2:22--2:23:
Defaulting type argument 'rep' of 'demote' to [2]
Defaulting type argument 'rep' of 'number' to [2]
True
True

2
tests/regression/AES.icry.stdout
View File

@ -10,7 +10,7 @@ Loading module AES
[warning] at ./AES.cry:147:53--147:63:
Defaulting type argument 'ix' of '(@)' to 4
[warning] at ./AES.cry:127:32--127:33:
Defaulting type argument 'rep' of 'demote' to [3]
Defaulting type argument 'rep' of 'number' to [3]
True
True
True

2
tests/regression/check02.icry.stdout
View File

@ -2,7 +2,7 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check02.cry:3:24--3:25:
Defaulting type argument 'rep' of 'demote' to [1]
Defaulting type argument 'rep' of 'number' to [1]
[warning] at <interactive>:1:1--1:18:
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:

2
tests/regression/check04.icry.stdout
View File

@ -4,7 +4,7 @@ Loading module Main
[warning] at ./check04.cry:4:10--4:45:
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check04.cry:4:43--4:44:
Defaulting type argument 'rep' of 'demote' to [2]
Defaulting type argument 'rep' of 'number' to [2]
[warning] at <interactive>:1:1--1:21:
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:

2
tests/regression/check05.icry.stdout
View File

@ -4,7 +4,7 @@ Loading module Main
[warning] at ./check05.cry:4:10--4:45:
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check05.cry:4:43--4:44:
Defaulting type argument 'rep' of 'demote' to [2]
Defaulting type argument 'rep' of 'number' to [2]
[warning] at <interactive>:1:1--1:21:
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:

2
tests/regression/check06.icry.stdout
View File

@ -4,7 +4,7 @@ Loading module Main
[warning] at ./check06.cry:5:10--5:70:
Defaulting type argument 'ix' of '(@@)' to 2
[warning] at ./check06.cry:5:66--5:67:
Defaulting type argument 'rep' of 'demote' to [2]
Defaulting type argument 'rep' of 'number' to [2]
[warning] at <interactive>:1:1--1:24:
Defaulting type argument 'ix' of '(@@)' to 4
Showing a specific instance of polymorphic result:

4
tests/regression/check14.icry.stdout
View File

@ -2,8 +2,8 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check14.cry:5:73--5:74:
Defaulting type argument 'rep' of 'demote' to [3]
Defaulting type argument 'rep' of 'number' to [3]
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
* Using 'Integer' for type argument 'rep' of 'Cryptol::number'
[[3, 2, 1, 0], [7, 6, 5, 4]]
True

2
tests/regression/check20.icry.stdout
View File

@ -2,5 +2,5 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
[warning] at ./check20.cry:3:31--3:33:
Defaulting type argument 'rep' of 'demote' to [4]
Defaulting type argument 'rep' of 'number' to [4]
True

4
tests/regression/check25.icry.stdout
View File

@ -5,7 +5,7 @@ Loading module check25
This binding for tz shadows the existing binding from
(at ./check25.cry:3:1--3:3, tz)
[warning] at ./check25.cry:8:17--8:19:
Defaulting type argument 'rep' of 'demote' to [4]
Defaulting type argument 'rep' of 'number' to [4]
[warning] at ./check25.cry:6:14--6:16:
Defaulting type argument 'rep' of 'demote' to [5]
Defaulting type argument 'rep' of 'number' to [5]
True

4
tests/regression/check26.icry.stdout
View File

@ -10,11 +10,11 @@ Loading module Main
[warning] at ./check26.cry:8:31--8:34:
Defaulting 2nd type argument of 'Main::xys' to [3]
[warning] at ./check26.cry:5:41--5:43:
Defaulting type argument 'rep' of 'demote' to [5]
Defaulting type argument 'rep' of 'number' to [5]
[warning] at ./check26.cry:5:35--5:37:
Defaulting 1st type argument of 'Main::xy' to [4]
[warning] at ./check26.cry:5:23--5:25:
Defaulting type argument 'rep' of 'demote' to [4]
Defaulting type argument 'rep' of 'number' to [4]
[warning] at ./check26.cry:5:17--5:19:
Defaulting 2nd type argument of 'Main::xy' to [5]
[warning] at ./check26.cry:4:43--4:45:

8
tests/regression/layout01.icry.stdout
View File

@ -1,13 +1,13 @@
Loading module Cryptol
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
* Using 'Integer' for type argument 'rep' of 'Cryptol::number'
1
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
* Using 'Integer' for type argument 'rep' of 'Cryptol::number'
[1, 2]
Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
* Using 'Integer' for type argument 'rep' of 'Cryptol::demote'
* Using 'Integer' for type argument 'rep' of 'Cryptol::number'
* Using 'Integer' for type argument 'rep' of 'Cryptol::number'
{x = 1, y = 2}
[warning] at <interactive>:1:1--1:22:
Defaulting the type of '<interactive>::y' to [2]

2
tests/regression/r02.icry.stdout
View File

@ -3,5 +3,5 @@ Showing a specific instance of polymorphic result:
* Using 'Integer' for type argument 'a' of 'Cryptol::fromThenTo'
[11, 11, 11, 11, 11, 11, 11, 11, 11, 11]
[warning] at <interactive>:1:65--1:67:
Defaulting type argument 'rep' of 'demote' to [4]
Defaulting type argument 'rep' of 'number' to [4]
True