From 70245005d8e07fd8b5edc894840c9456073046c2 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 29 Jun 2021 12:08:28 -0700 Subject: [PATCH 01/16] Add new syntactic forms for enumerations with explicit stride values. This doesn't yet pipe the new constructs through the typechecker. --- src/Cryptol/ModuleSystem/Renamer.hs | 12 ++++++++++ src/Cryptol/Parser.y | 15 ++++++++++-- src/Cryptol/Parser/AST.hs | 17 +++++++++++++ src/Cryptol/Parser/Lexer.x | 6 +++++ src/Cryptol/Parser/Names.hs | 4 ++++ src/Cryptol/Parser/NoPat.hs | 2 ++ src/Cryptol/Parser/ParserUtils.hs | 37 +++++++++++++++++++++++++++++ src/Cryptol/Parser/Token.hs | 5 +++- src/Cryptol/TypeCheck/Infer.hs | 8 +++++++ 9 files changed, 103 insertions(+), 3 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index a05c97ba4..3d85f6387 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -727,6 +727,18 @@ instance Rename Expr where <*> traverse rename n <*> rename e <*> traverse rename t + EFromToBy isStrict s e b t -> + EFromToBy isStrict + <$> rename s + <*> rename e + <*> rename b + <*> traverse rename t + EFromToDownBy isStrict s e b t -> + EFromToDownBy isStrict + <$> rename s + <*> rename e + <*> rename b + <*> traverse rename t EFromToLessThan s e t -> EFromToLessThan <$> rename s <*> rename e diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index a9fb04d1b..95fab2841 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -85,6 +85,8 @@ import Paths_cryptol 'then' { Located $$ (Token (KW KW_then ) _)} 'else' { Located $$ (Token (KW KW_else ) _)} 'x' { Located $$ (Token (KW KW_x) _)} + 'down' { Located $$ (Token (KW KW_down) _)} + 'by' { Located $$ (Token (KW KW_by) _)} 'primitive' { Located $$ (Token (KW KW_primitive) _)} 'constraint'{ Located $$ (Token (KW KW_constraint) _)} @@ -96,8 +98,10 @@ import Paths_cryptol '..' { Located $$ (Token (Sym DotDot ) _)} '...' { Located $$ (Token (Sym DotDotDot) _)} '..<' { Located $$ (Token (Sym DotDotLt) _)} + '..>' { Located $$ (Token (Sym DotDotGt) _)} '|' { Located $$ (Token (Sym Bar ) _)} '<' { Located $$ (Token (Sym Lt ) _)} + '>' { Located $$ (Token (Sym Gt ) _)} '(' { Located $$ (Token (Sym ParenL ) _)} ')' { Located $$ (Token (Sym ParenR ) _)} @@ -418,7 +422,7 @@ pat_op :: { LPName } | '~' { Located $1 $ mkUnqual $ mkInfix "~" } | '^^' { Located $1 $ mkUnqual $ mkInfix "^^" } | '<' { Located $1 $ mkUnqual $ mkInfix "<" } - + | '>' { Located $1 $ mkUnqual $ mkInfix ">" } other_op :: { LPName } : OP { let Token (Op (Other [] str)) _ = thing $1 @@ -587,6 +591,14 @@ list_expr :: { Expr PName } | expr '..' '<' expr {% eFromToLessThan $2 $1 $4 } | expr '..<' expr {% eFromToLessThan $2 $1 $3 } + | expr '..' expr 'by' expr {% eFromToBy $2 $1 $3 $5 False } + | expr '..' '<' expr 'by' expr {% eFromToBy $2 $1 $4 $6 True } + | expr '..<' expr 'by' expr {% eFromToBy $2 $1 $3 $5 True } + + | expr '..' expr 'down' 'by' expr {% eFromToDownBy $2 $1 $3 $6 False } + | expr '..' '>' expr 'down' 'by' expr {% eFromToDownBy $2 $1 $4 $7 True } + | expr '..>' expr 'down' 'by' expr {% eFromToDownBy $2 $1 $3 $6 True } + | expr '...' { EInfFrom $1 Nothing } | expr ',' expr '...' { EInfFrom $1 (Just $3) } @@ -732,7 +744,6 @@ ident :: { Located Ident } | 'as' { Located { srcRange = $1, thing = mkIdent "as" } } | 'hiding' { Located { srcRange = $1, thing = mkIdent "hiding" } } - name :: { LPName } : ident { fmap mkUnqual $1 } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 7c7e1fbd8..8d72b1216 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -351,6 +351,11 @@ data Expr n = EVar n -- ^ @ x @ | EList [Expr n] -- ^ @ [1,2,3] @ | EFromTo (Type n) (Maybe (Type n)) (Type n) (Maybe (Type n)) -- ^ @ [1, 5 .. 117 : t] @ + | EFromToBy Bool (Type n) (Type n) (Type n) (Maybe (Type n)) + -- ^ @ [1 .. 10 by 2 : t ] @ + + | EFromToDownBy Bool (Type n) (Type n) (Type n) (Maybe (Type n)) + -- ^ @ [10 .. 1 down by 2 : t ] @ | EFromToLessThan (Type n) (Type n) (Maybe (Type n)) -- ^ @ [ 1 .. < 10 : t ] @ @@ -817,6 +822,14 @@ instance (Show name, PPName name) => PP (Expr name) where 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 + EFromToBy isStrict e1 e2 e3 t1 -> brackets (pp e1 <+> dots <+> pp e2 <+> text "by" <+> end) + where end = maybe (pp e3) (\t -> pp e3 <+> colon <+> pp t) t1 + dots | isStrict = text ".. <" + | otherwise = text ".." + EFromToDownBy isStrict e1 e2 e3 t1 -> brackets (pp e1 <+> dots <+> pp e2 <+> text "down by" <+> end) + where end = maybe (pp e3) (\t -> pp e3 <+> colon <+> pp t) t1 + dots | isStrict = text ".. >" + | otherwise = text ".." EFromToLessThan e1 e2 t1 -> brackets (strt <+> text ".. <" <+> end) where strt = maybe (pp e1) (\t -> pp e1 <+> colon <+> pp t) t1 end = pp e2 @@ -1074,6 +1087,10 @@ instance NoPos (Expr name) where 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) + EFromToBy isStrict x y z t + -> EFromToBy isStrict (noPos x) (noPos y) (noPos z) (noPos t) + EFromToDownBy isStrict x y z t + -> EFromToDownBy isStrict (noPos x) (noPos y) (noPos z) (noPos t) EFromToLessThan x y t -> EFromToLessThan (noPos x) (noPos y) (noPos t) EInfFrom x y -> EInfFrom (noPos x) (noPos y) EComp x y -> EComp (noPos x) (noPos y) diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index 74063ce0a..0f76c62ae 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -116,6 +116,8 @@ $white+ { emit $ White Space } "as" { emit $ KW KW_as } "hiding" { emit $ KW KW_hiding } "newtype" { emit $ KW KW_newtype } +"down" { emit $ KW KW_down } +"by" { emit $ KW KW_by } "infixl" { emit $ KW KW_infixl } "infixr" { emit $ KW KW_infixr } @@ -147,6 +149,7 @@ $white+ { emit $ White Space } ".." { emit $ Sym DotDot } "..." { emit $ Sym DotDotDot } "..<" { emit $ Sym DotDotLt } +"..>" { emit $ Sym DotDotGt } "|" { emit $ Sym Bar } "(" { emit $ Sym ParenL } ")" { emit $ Sym ParenR } @@ -169,6 +172,9 @@ $white+ { emit $ White Space } -- < can appear in the enumeration syntax `[ x .. < y ] "<" { emit $ Sym Lt } +-- > can appear in the enumeration syntax `[ x .. > y down by n ] +">" { emit $ Sym Gt } + -- hash is used as a kind, and as a pattern "#" { emit (Op Hash ) } diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index d4ffb46be..06027391b 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -82,6 +82,8 @@ namesE expr = in Set.unions (e : map namesUF fs) EList es -> Set.unions (map namesE es) EFromTo{} -> Set.empty + EFromToBy{} -> Set.empty + EFromToDownBy{} -> Set.empty EFromToLessThan{} -> Set.empty EInfFrom e e' -> Set.union (namesE e) (maybe Set.empty namesE e') EComp e arms -> let (dss,uss) = unzip (map namesArm arms) @@ -203,6 +205,8 @@ tnamesE expr = `Set.union` maybe Set.empty tnamesT b `Set.union` tnamesT c `Set.union` maybe Set.empty tnamesT t + EFromToBy _ a b c t -> Set.unions [ tnamesT a, tnamesT b, tnamesT c, maybe Set.empty tnamesT t ] + EFromToDownBy _ a b c t -> Set.unions [ tnamesT a, tnamesT b, tnamesT c, maybe Set.empty tnamesT t ] EFromToLessThan a b t -> tnamesT a `Set.union` tnamesT b `Set.union` maybe Set.empty tnamesT t EInfFrom e e' -> Set.union (tnamesE e) (maybe Set.empty tnamesE e') diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 835a4fa4e..c4f475e6e 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -159,6 +159,8 @@ noPatE expr = EUpd mb fs -> EUpd <$> traverse noPatE mb <*> traverse noPatUF fs EList es -> EList <$> mapM noPatE es EFromTo {} -> return expr + EFromToBy {} -> return expr + EFromToDownBy {} -> return expr EFromToLessThan{} -> return expr EInfFrom e e' -> EInfFrom <$> noPatE e <*> traverse noPatE e' EComp e mss -> EComp <$> noPatE e <*> mapM noPatArm mss diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index f64313187..8d299c203 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -378,6 +378,43 @@ eFromTo r e1 e2 e3 = (Nothing, Nothing, Nothing) -> eFromToType r e1 e2 e3 Nothing _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."] +eFromToBy :: Range -> Expr PName -> Expr PName -> Expr PName -> Bool -> ParseM (Expr PName) +eFromToBy r e1 e2 e3 isStrictBound = + case (asETyped e1, asETyped e2, asETyped e3) of + (Just (e1', t), Nothing, Nothing) -> eFromToByTyped r e1' e2 e3 (Just t) isStrictBound + (Nothing, Just (e2', t), Nothing) -> eFromToByTyped r e1 e2' e3 (Just t) isStrictBound + (Nothing, Nothing, Just (e3', t)) -> eFromToByTyped r e1 e2 e3' (Just t) isStrictBound + (Nothing, Nothing, Nothing) -> eFromToByTyped r e1 e2 e3 Nothing isStrictBound + _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."] + +eFromToByTyped :: Range -> Expr PName -> Expr PName -> Expr PName -> Maybe (Type PName) -> Bool -> ParseM (Expr PName) +eFromToByTyped r e1 e2 e3 t isStrictBound = + EFromToBy isStrictBound + <$> exprToNumT r e1 + <*> exprToNumT r e2 + <*> exprToNumT r e3 + <*> pure t + +eFromToDownBy :: + Range -> Expr PName -> Expr PName -> Expr PName -> Bool -> ParseM (Expr PName) +eFromToDownBy r e1 e2 e3 isStrictBound = + case (asETyped e1, asETyped e2, asETyped e3) of + (Just (e1', t), Nothing, Nothing) -> eFromToDownByTyped r e1' e2 e3 (Just t) isStrictBound + (Nothing, Just (e2', t), Nothing) -> eFromToDownByTyped r e1 e2' e3 (Just t) isStrictBound + (Nothing, Nothing, Just (e3', t)) -> eFromToDownByTyped r e1 e2 e3' (Just t) isStrictBound + (Nothing, Nothing, Nothing) -> eFromToDownByTyped r e1 e2 e3 Nothing isStrictBound + _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."] + +eFromToDownByTyped :: + Range -> Expr PName -> Expr PName -> Expr PName -> Maybe (Type PName) -> Bool -> ParseM (Expr PName) +eFromToDownByTyped r e1 e2 e3 t isStrictBound = + EFromToDownBy isStrictBound + <$> exprToNumT r e1 + <*> exprToNumT r e2 + <*> exprToNumT r e3 + <*> pure t + + asETyped :: Expr n -> Maybe (Expr n, Type n) asETyped (ELocated e _) = asETyped e asETyped (ETyped e t) = Just (e, t) diff --git a/src/Cryptol/Parser/Token.hs b/src/Cryptol/Parser/Token.hs index 280f8157d..c1ec16903 100644 --- a/src/Cryptol/Parser/Token.hs +++ b/src/Cryptol/Parser/Token.hs @@ -51,6 +51,8 @@ data TokenKW = KW_else | KW_parameter | KW_constraint | KW_Prop + | KW_by + | KW_down deriving (Eq, Show, Generic, NFData) -- | The named operators are a special case for parsing types, and 'Other' is @@ -71,13 +73,14 @@ data TokenSym = Bar | DotDot | DotDotDot | DotDotLt + | DotDotGt | Colon | BackTick | ParenL | ParenR | BracketL | BracketR | CurlyL | CurlyR | TriL | TriR - | Lt + | Lt | Gt | Underscore deriving (Eq, Show, Generic, NFData) diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 95e201c6a..e72a9537d 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -164,6 +164,8 @@ appTys expr ts tGoal = P.ESel {} -> mono P.EList {} -> mono P.EFromTo {} -> mono + P.EFromToBy {} -> mono + P.EFromToDownBy {} -> mono P.EFromToLessThan {} -> mono P.EInfFrom {} -> mono P.EComp {} -> mono @@ -276,6 +278,12 @@ checkE expr tGoal = es' <- mapM checkElem es return (EList es' a) + P.EFromToBy _isStrict _t1 _t2 _t3 _mety -> + error "TODO! implement typechecking for EFromToBy" + + P.EFromToDownBy _isStrict _t1 _t2 _t3 _mety -> + error "TODO! implement typechecking for EFromToDownBy" + P.EFromToLessThan t1 t2 mety -> do l <- curRange let fs0 = From 6fe2970b52fbce46112a7a505eb6c0e2c22854e4 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 29 Jun 2021 14:26:51 -0700 Subject: [PATCH 02/16] Add new primtives for the explicit stride enumerations. Hook them up through the typechecker. However, we still need implementations. --- lib/Cryptol.cry | 59 ++++++++++++++++++++++++++++++---- src/Cryptol/TypeCheck/Infer.hs | 56 +++++++++++++++++++++++++++++--- 2 files changed, 104 insertions(+), 11 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index a2b3c27c9..2af66dc74 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -195,19 +195,66 @@ length _ = `n /** * A finite sequence counting up from 'first' to 'last'. * - * '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'. + * '[x .. y]' is syntactic sugar for 'fromTo`{first=x,last=y}'. */ -primitive fromTo : {first, last, a} (fin last, last >= first, - Literal first a, Literal last a) => - [1 + (last - first)]a +primitive fromTo : {first, last, a} + (fin last, last >= first, Literal last a) => + [1 + (last - first)]a + +/** + * A finite sequence counting up from 'first' to 'last' by 'stride' + * + * '[x .. y by n]` is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'. + */ +primitive fromToBy : {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first)/stride]a /** * A possibly infinite sequence counting up from 'first' up to (but not including) 'bound'. * - * Note that if 'first' = 'bound' then the sequence will be empty. + * '[ x ..< y ]' is syntacic sugar for 'fromToLessThan`{first=x,bound=y}'. + * + * Note that if 'first' = 'bound' then the sequence will be empty. If 'bound = inf' + * then the sequence will be infinite, and will eventually wrap around for bounded types. */ primitive fromToLessThan : - {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => [bound - first]a + {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + +/** + * A finite sequence counting from 'first' up to (but not including) 'bound' + * by 'stride'. Note that if 'first = bound' then the sequence will + * be empty. If 'bound = inf' then the sequence will be infinite, and will + * eventually wrap around for bounded types. + * + * '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=a,bound=b,stride=n}'. + */ +primitive fromToByLessThan : {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) => + [(bound - first)/^stride]a + +/** + * A finite sequence counting from 'first' down to 'last' by 'stride'. + * + * '[x .. y down by n]` is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'. + */ +primitive fromToDownBy : {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last)/stride]a + +/** + * A finite sequence counting from 'first' down to (but not including) + * 'bound' by 'stride'. + * + * '[x ..> y down by n]` is syntactic sugar for + * 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'. + * + * Note that if 'first = bound' the sequence will be empty. + */ +primitive fromToDownByGreaterThan : {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound)/^stride]a /** diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index e72a9537d..50abcc486 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -278,11 +278,57 @@ checkE expr tGoal = es' <- mapM checkElem es return (EList es' a) - P.EFromToBy _isStrict _t1 _t2 _t3 _mety -> - error "TODO! implement typechecking for EFromToBy" - - P.EFromToDownBy _isStrict _t1 _t2 _t3 _mety -> - error "TODO! implement typechecking for EFromToDownBy" + P.EFromToBy isStrict t1 t2 t3 mety + | isStrict -> + do l <- curRange + let fs = [("first",t1),("bound",t2),("stride",t3)] ++ + case mety of + Just ety -> [("a",ety)] + Nothing -> [] + prim <- mkPrim "fromToByLessThan" + let e' = P.EAppT prim + [ P.NamedInst P.Named{ name = Located l (packIdent x), value = y } + | (x,y) <- fs + ] + checkE e' tGoal + | otherwise -> + do l <- curRange + let fs = [("first",t1),("last",t2),("stride",t3)] ++ + case mety of + Just ety -> [("a",ety)] + Nothing -> [] + prim <- mkPrim "fromToBy" + let e' = P.EAppT prim + [ P.NamedInst P.Named{ name = Located l (packIdent x), value = y } + | (x,y) <- fs + ] + checkE e' tGoal + + P.EFromToDownBy isStrict t1 t2 t3 mety + | isStrict -> + do l <- curRange + let fs = [("first",t1),("bound",t2),("stride",t3)] ++ + case mety of + Just ety -> [("a",ety)] + Nothing -> [] + prim <- mkPrim "fromToDownByGreaterThan" + let e' = P.EAppT prim + [ P.NamedInst P.Named{ name = Located l (packIdent x), value = y } + | (x,y) <- fs + ] + checkE e' tGoal + | otherwise -> + do l <- curRange + let fs = [("first",t1),("last",t2),("stride",t3)] ++ + case mety of + Just ety -> [("a",ety)] + Nothing -> [] + prim <- mkPrim "fromToDownBy" + let e' = P.EAppT prim + [ P.NamedInst P.Named{ name = Located l (packIdent x), value = y } + | (x,y) <- fs + ] + checkE e' tGoal P.EFromToLessThan t1 t2 mety -> do l <- curRange From 14a660167c49942e08f64d29dc4ec4819a0e11c8 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 29 Jun 2021 16:24:40 -0700 Subject: [PATCH 03/16] Add implementations for the new enumeration primitives. --- src/Cryptol/Eval/Generic.hs | 100 ++++++++++++++++++++++++++++++------ 1 file changed, 83 insertions(+), 17 deletions(-) diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 834a5c9ab..005bc8754 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -1437,7 +1437,6 @@ updatePrim sym updateWord updateSeq = (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val) {-# INLINE fromToV #-} - -- @[ 0 .. 10 ]@ fromToV :: Backend sym => sym -> Prim sym fromToV sym = @@ -1452,23 +1451,7 @@ fromToV sym = in VSeq len $ indexSeqMap $ \i -> f (first' + i) _ -> evalPanic "fromToV" ["invalid arguments"] -{-# INLINE fromToLessThanV #-} - --- @[ 0 .. <10 ]@ -fromToLessThanV :: Backend sym => sym -> Prim sym -fromToLessThanV sym = - PFinPoly \first -> - PNumPoly \bound -> - PTyPoly \ty -> - PVal - let !f = mkLit sym ty - ss = indexSeqMap $ \i -> f (first + i) - in case bound of - Inf -> VStream ss - Nat bound' -> VSeq (bound' - first) ss - {-# INLINE fromThenToV #-} - -- @[ 0, 1 .. 10 ]@ fromThenToV :: Backend sym => sym -> Prim sym fromThenToV sym = @@ -1485,6 +1468,75 @@ fromThenToV sym = in VSeq len' $ indexSeqMap $ \i -> f (first' + i*diff) _ -> evalPanic "fromThenToV" ["invalid arguments"] +{-# INLINE fromToLessThanV #-} +-- @[ 0 .. <10 ]@ +fromToLessThanV :: Backend sym => sym -> Prim sym +fromToLessThanV sym = + PFinPoly \first -> + PNumPoly \bound -> + PTyPoly \ty -> + PVal + let !f = mkLit sym ty + ss = indexSeqMap $ \i -> f (first + i) + in case bound of + Inf -> VStream ss + Nat bound' -> VSeq (bound' - first) ss + +{-# INLINE fromToByV #-} +-- @[ 0 .. 10 by 2 ]@ +fromToByV :: Backend sym => sym -> Prim sym +fromToByV sym = + PFinPoly \first -> + PFinPoly \lst -> + PFinPoly \stride -> + PTyPoly \ty -> + PVal + let !f = mkLit sym ty + ss = indexSeqMap $ \i -> f (first + i*stride) + in VSeq (1 + ((lst - first) `div` stride)) ss + +{-# INLINE fromToByLessThanV #-} +-- @[ 0 .. <10 by 2 ]@ +fromToByLessThanV :: Backend sym => sym -> Prim sym +fromToByLessThanV sym = + PFinPoly \first -> + PNumPoly \bound -> + PFinPoly \stride -> + PTyPoly \ty -> + PVal + let !f = mkLit sym ty + ss = indexSeqMap $ \i -> f (first + i*stride) + in case bound of + Inf -> VStream ss + Nat bound' -> VSeq ((bound' - first + stride - 1) `div` stride) ss + + +{-# INLINE fromToDownByV #-} +-- @[ 10 .. 0 down by 2 ]@ +fromToDownByV :: Backend sym => sym -> Prim sym +fromToDownByV sym = + PFinPoly \first -> + PFinPoly \lst -> + PFinPoly \stride -> + PTyPoly \ty -> + PVal + let !f = mkLit sym ty + ss = indexSeqMap $ \i -> f (first - i*stride) + in VSeq (1 + ((first - lst) `div` stride)) ss + +{-# INLINE fromToDownByGreaterThanV #-} +-- @[ 10 .. >0 down by 2 ]@ +fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym +fromToDownByGreaterThanV sym = + PFinPoly \first -> + PFinPoly \bound -> + PFinPoly \stride -> + PTyPoly \ty -> + PVal + let !f = mkLit sym ty + ss = indexSeqMap $ \i -> f (first - i*stride) + in VSeq ((first - bound + stride - 1) `div` stride) ss + {-# INLINE infFromV #-} infFromV :: Backend sym => sym -> Prim sym infFromV sym = @@ -2015,6 +2067,20 @@ genericPrimTable sym getEOpts = , {-# SCC "Prelude::fromToLessThan" #-} fromToLessThanV sym) + , ("fromToBy" , {-# SCC "Prelude::fromToBy" #-} + fromToByV sym) + + , ("fromToByLessThan", + {-# SCC "Prelude::fromToByLessThan" #-} + fromToByLessThanV sym) + + , ("fromToDownBy", {-# SCC "Prelude::fromToDownBy" #-} + fromToDownByV sym) + + , ("fromToDownByGreaterThan" + , {-# SCC "Prelude::fromToDownByGreaterThan" #-} + fromToDownByGreaterThanV sym) + -- Sequence manipulations , ("#" , {-# SCC "Prelude::(#)" #-} PFinPoly \front -> From 94a4c77fdb821fcf5084a139fe4bb49f5cbcfc3b Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 08:32:39 -0700 Subject: [PATCH 04/16] Relax the finiteness restriction on the first argument of `/^` and `%^`. We define `inf /^ n = inf` and `inf %^ n` for finite, positive `n`. --- lib/Cryptol.cry | 4 ++-- src/Cryptol/TypeCheck/SimpType.hs | 2 -- src/Cryptol/TypeCheck/Solver/InfNat.hs | 19 +++++++++---------- 3 files changed, 11 insertions(+), 14 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 2af66dc74..3188df268 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -131,13 +131,13 @@ primitive type max : # -> # -> # /** Divide numeric types, rounding up. */ primitive type { m : #, n : # } - (fin m, fin n, n >= 1) => + (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) => + (fin n, n >= 1) => m %^ n : # /** The length of an enumeration. */ diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs index 964550914..0d42e2009 100644 --- a/src/Cryptol/TypeCheck/SimpType.hs +++ b/src/Cryptol/TypeCheck/SimpType.hs @@ -182,7 +182,6 @@ tMod x y tCeilDiv :: Type -> Type -> Type tCeilDiv x y | Just t <- tOp TCCeilDiv (op2 nCeilDiv) [x,y] = t - | tIsInf x = bad | tIsInf y = bad | Just 0 <- tIsNum y = bad | otherwise = tf2 TCCeilDiv x y @@ -191,7 +190,6 @@ tCeilDiv x y tCeilMod :: Type -> Type -> Type tCeilMod x y | Just t <- tOp TCCeilMod (op2 nCeilMod) [x,y] = t - | tIsInf x = bad | tIsInf y = bad | Just 0 <- tIsNum x = bad | otherwise = tf2 TCCeilMod x y diff --git a/src/Cryptol/TypeCheck/Solver/InfNat.hs b/src/Cryptol/TypeCheck/Solver/InfNat.hs index 893ab1dd7..9072fbd4f 100644 --- a/src/Cryptol/TypeCheck/Solver/InfNat.hs +++ b/src/Cryptol/TypeCheck/Solver/InfNat.hs @@ -122,23 +122,22 @@ nMod (Nat x) (Nat y) = Just (Nat (mod x y)) nMod (Nat x) Inf = Just (Nat x) -- inf * 0 + x = 0 + x -- | @nCeilDiv msgLen blockSize@ computes the least @n@ such that --- @msgLen <= blockSize * n@. It is undefined when @blockSize = 0@. --- It is also undefined when either input is infinite; perhaps this --- could be relaxed later. +-- @msgLen <= blockSize * n@. It is undefined when @blockSize = 0@, +-- or when @blockSize = inf@. @inf@ divided by any positive +-- finite value is @inf@. nCeilDiv :: Nat' -> Nat' -> Maybe Nat' +nCeilDiv _ Inf = Nothing nCeilDiv _ (Nat 0) = Nothing -nCeilDiv Inf _ = Nothing -nCeilDiv (Nat _) Inf = Nothing +nCeilDiv Inf (Nat _) = Just Inf nCeilDiv (Nat x) (Nat y) = Just (Nat (- div (- x) y)) -- | @nCeilMod msgLen blockSize@ computes the least @k@ such that --- @blockSize@ divides @msgLen + k@. It is undefined when @blockSize = 0@. --- It is also undefined when either input is infinite; perhaps this --- could be relaxed later. +-- @blockSize@ divides @msgLen + k@. It is undefined when @blockSize = 0@ +-- or @blockSize = inf@. @inf@ modulus any positive finite value is @0@. nCeilMod :: Nat' -> Nat' -> Maybe Nat' +nCeilMod _ Inf = Nothing nCeilMod _ (Nat 0) = Nothing -nCeilMod Inf _ = Nothing -nCeilMod (Nat _) Inf = Nothing +nCeilMod Inf (Nat _) = Just (Nat 0) nCeilMod (Nat x) (Nat y) = Just (Nat (mod (- x) y)) -- | Rounds up. From 33afaccb4bf71e01e4d6ac437ed84e1f32055375 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 09:10:26 -0700 Subject: [PATCH 05/16] Fix incorrect "unused name" warnings from `primitive type` declarations. --- src/Cryptol/ModuleSystem/Renamer.hs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 3d85f6387..0b13eeb77 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -465,6 +465,13 @@ instance Rename PrimType where depsOf (NamedThing (thing x)) do let (as,ps) = primTCts pt (_,cts) <- renameQual as ps $ \as' ps' -> pure (as',ps') + + -- Record an additional use for each parameter since we checked + -- earlier that all the parameters are used exactly once in the + -- body of the signature. This prevents incorret warnings + -- about unused names. + mapM_ (recordUse . tpName) (fst cts) + pure pt { primTCts = cts, primTName = x } instance Rename ParameterType where From d1f945b20ef3524cfd7bb89bdd7227ea96ca89b3 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 09:25:43 -0700 Subject: [PATCH 06/16] Add regression test for enumerations with explicit strides --- tests/regression/explicit-strides.icry | 12 ++++++++ tests/regression/explicit-strides.icry.stdout | 30 +++++++++++++++++++ 2 files changed, 42 insertions(+) create mode 100644 tests/regression/explicit-strides.icry create mode 100644 tests/regression/explicit-strides.icry.stdout diff --git a/tests/regression/explicit-strides.icry b/tests/regression/explicit-strides.icry new file mode 100644 index 000000000..758dac51c --- /dev/null +++ b/tests/regression/explicit-strides.icry @@ -0,0 +1,12 @@ +[ 0:Integer .. 10 by 2] +[ 0 .. <10:Integer by 2] + +[ 0 .. 9 by 2] : [_]Integer +[ 0 .. <9 by 2:Integer] + +[ 10:Integer .. 0 down by 2 ] +[ 10 .. >0 down by 2 ] + +[ 2^^16-1 .. >50000 down by 100 ] : [_][16] + +[ 200 .. 100:Integer down by 9 ] diff --git a/tests/regression/explicit-strides.icry.stdout b/tests/regression/explicit-strides.icry.stdout new file mode 100644 index 000000000..2d5416b61 --- /dev/null +++ b/tests/regression/explicit-strides.icry.stdout @@ -0,0 +1,30 @@ +Loading module Cryptol +[0, 2, 4, 6, 8, 10] +[0, 2, 4, 6, 8] +[0, 2, 4, 6, 8] +[0, 2, 4, 6, 8] +[10, 8, 6, 4, 2, 0] +Showing a specific instance of polymorphic result: + * Using 'Integer' for type argument 'a' of 'Cryptol::fromToDownByGreaterThan' +[10, 8, 6, 4, 2] +[0xffff, 0xff9b, 0xff37, 0xfed3, 0xfe6f, 0xfe0b, 0xfda7, 0xfd43, + 0xfcdf, 0xfc7b, 0xfc17, 0xfbb3, 0xfb4f, 0xfaeb, 0xfa87, 0xfa23, + 0xf9bf, 0xf95b, 0xf8f7, 0xf893, 0xf82f, 0xf7cb, 0xf767, 0xf703, + 0xf69f, 0xf63b, 0xf5d7, 0xf573, 0xf50f, 0xf4ab, 0xf447, 0xf3e3, + 0xf37f, 0xf31b, 0xf2b7, 0xf253, 0xf1ef, 0xf18b, 0xf127, 0xf0c3, + 0xf05f, 0xeffb, 0xef97, 0xef33, 0xeecf, 0xee6b, 0xee07, 0xeda3, + 0xed3f, 0xecdb, 0xec77, 0xec13, 0xebaf, 0xeb4b, 0xeae7, 0xea83, + 0xea1f, 0xe9bb, 0xe957, 0xe8f3, 0xe88f, 0xe82b, 0xe7c7, 0xe763, + 0xe6ff, 0xe69b, 0xe637, 0xe5d3, 0xe56f, 0xe50b, 0xe4a7, 0xe443, + 0xe3df, 0xe37b, 0xe317, 0xe2b3, 0xe24f, 0xe1eb, 0xe187, 0xe123, + 0xe0bf, 0xe05b, 0xdff7, 0xdf93, 0xdf2f, 0xdecb, 0xde67, 0xde03, + 0xdd9f, 0xdd3b, 0xdcd7, 0xdc73, 0xdc0f, 0xdbab, 0xdb47, 0xdae3, + 0xda7f, 0xda1b, 0xd9b7, 0xd953, 0xd8ef, 0xd88b, 0xd827, 0xd7c3, + 0xd75f, 0xd6fb, 0xd697, 0xd633, 0xd5cf, 0xd56b, 0xd507, 0xd4a3, + 0xd43f, 0xd3db, 0xd377, 0xd313, 0xd2af, 0xd24b, 0xd1e7, 0xd183, + 0xd11f, 0xd0bb, 0xd057, 0xcff3, 0xcf8f, 0xcf2b, 0xcec7, 0xce63, + 0xcdff, 0xcd9b, 0xcd37, 0xccd3, 0xcc6f, 0xcc0b, 0xcba7, 0xcb43, + 0xcadf, 0xca7b, 0xca17, 0xc9b3, 0xc94f, 0xc8eb, 0xc887, 0xc823, + 0xc7bf, 0xc75b, 0xc6f7, 0xc693, 0xc62f, 0xc5cb, 0xc567, 0xc503, + 0xc49f, 0xc43b, 0xc3d7, 0xc373] +[200, 191, 182, 173, 164, 155, 146, 137, 128, 119, 110, 101] From 0778fd8ff2334b8e9577716167e32d602497ac53 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 10:05:39 -0700 Subject: [PATCH 07/16] Update "ProgrammingCryptol" Minor output changes in the exercises are required. --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index bdd280b2c..b0d9c0cbf 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -790,7 +790,7 @@ \subsection{Appending and indexing} [] invalid sequence index: 12 -- Backtrace -- - (Cryptol::@) called at Cryptol:820:14--820:20 + (Cryptol::@) called at Cryptol:867:14--867:20 (Cryptol::@@) called at :9:1--9:28 [9, 8, 7, 6, 5, 4, 3, 2, 1, 0] 9 @@ -1795,7 +1795,7 @@ \section{Characters and strings} command to see the type Cryptol infers for this expression explicitly: \begin{replPrompt} Cryptol> :t [1:[_] .. 10] - [1 .. 10 : [_]] : {n} (n >= 4, n >= 1, fin n) => [10][n] + [1 .. 10 : [_]] : {n} (n >= 4, fin n) => [10][n] \end{replPrompt} Cryptol tells us that the sequence has precisely $10$ elements, and each element is at least $4$ bits wide. From 3debc2bb4794fd385418ad681d8c894ffd9e625d Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 10:06:21 -0700 Subject: [PATCH 08/16] Add a `check-docs` command to the `cry` script --- cry | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/cry b/cry index 5566a0951..34301f165 100755 --- a/cry +++ b/cry @@ -23,6 +23,7 @@ Available commands: rpc-test Run RPC server tests rpc-docs Check that the RPC documentation is up-to-date exe-path Print the location of the local executable + check-docs Check the exercises embedded in the documentation EOM } @@ -97,6 +98,10 @@ case $COMMAND in $DIR/cryptol-remote-api/check_docs.sh ;; + check-docs) + cabal v2-build exe:check-exercises + find ./docs/ProgrammingCryptol -name '*.tex' -print0 | xargs -0 -n1 cabal v2-exec check-exercises + ;; help) show_usage && exit 0 ;; From 5a8a00fc81490d2445a0885fafa94ac46ee8fd23 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 10:19:39 -0700 Subject: [PATCH 09/16] Minor test suite updates --- tests/issues/T146.icry.stdout | 8 ++++---- tests/issues/issue1024.icry.stdout | 12 ++++++------ tests/issues/issue103.icry.stdout | 2 +- tests/issues/issue226.icry.stdout | 19 +++++++++++++++++-- tests/issues/issue290v2.icry.stdout | 4 ++-- tests/issues/issue582.icry.stdout | 24 ++---------------------- tests/issues/issue723.icry.stdout | 4 ++-- tests/modsys/T16.icry.stdout | 2 +- tests/regression/safety.icry.stdout | 2 +- tests/regression/tc-errors.icry.stdout | 8 ++++---- 10 files changed, 40 insertions(+), 45 deletions(-) diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 1ac3940f3..6f88b3458 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -4,15 +4,15 @@ Loading module Main [error] at T146.cry:1:18--6:10: The type ?a is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`812 + It cannot depend on quantified variables: fv`828 When checking type of field 'v0' where ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 - fv`812 is signature variable 'fv' at T146.cry:11:10--11:12 + fv`828 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: The type ?b is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`812 + It cannot depend on quantified variables: fv`828 When checking signature variable 'fv' where ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 - fv`812 is signature variable 'fv' at T146.cry:11:10--11:12 + fv`828 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/issue1024.icry.stdout b/tests/issues/issue1024.icry.stdout index 8e21eec48..24986410e 100644 --- a/tests/issues/issue1024.icry.stdout +++ b/tests/issues/issue1024.icry.stdout @@ -8,20 +8,20 @@ Loading module Main [warning] at issue1024a.cry:4:34--4:39 Unused name: g [error] at issue1024a.cry:1:6--1:11: - Illegal kind assigned to type variable: f`809 + Illegal kind assigned to type variable: f`825 Unexpected: # -> * where - f`809 is signature variable 'f' at issue1024a.cry:1:12--1:24 + f`825 is signature variable 'f' at issue1024a.cry:1:12--1:24 [error] at issue1024a.cry:2:6--2:13: - Illegal kind assigned to type variable: f`810 + Illegal kind assigned to type variable: f`826 Unexpected: Prop where - f`810 is signature variable 'f' at issue1024a.cry:2:14--2:24 + f`826 is signature variable 'f' at issue1024a.cry:2:14--2:24 [error] at issue1024a.cry:4:13--4:49: - Illegal kind assigned to type variable: f`812 + Illegal kind assigned to type variable: f`828 Unexpected: # -> * where - f`812 is signature variable 'f' at issue1024a.cry:4:22--4:32 + f`828 is signature variable 'f' at issue1024a.cry:4:22--4:32 Loading module Cryptol Loading module Main 0xffff diff --git a/tests/issues/issue103.icry.stdout b/tests/issues/issue103.icry.stdout index e003e8023..a1ddb96e0 100644 --- a/tests/issues/issue103.icry.stdout +++ b/tests/issues/issue103.icry.stdout @@ -2,7 +2,7 @@ Loading module Cryptol Run-time error: undefined -- Backtrace -- -Cryptol::error called at Cryptol:990:13--990:18 +Cryptol::error called at Cryptol:1037:13--1037:18 Cryptol::undefined called at issue103.icry:1:9--1:18 Using exhaustive testing. Testing... ERROR for the following inputs: diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index e49259c79..1602e1739 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -138,9 +138,24 @@ Symbols lengthFromThenTo first next last == len) => [len]a fromTo : - {first, last, a} (fin last, last >= first, Literal first a, - Literal last a) => + {first, last, a} (fin last, last >= first, Literal last a) => [1 + (last - first)]a + fromToBy : + {first, last, stride, a} (fin last, fin stride, stride >= 1, + last >= first, Literal last a) => + [1 + (last - first) / stride]a + fromToByLessThan : + {first, bound, stride, a} (fin first, fin stride, stride >= 1, + bound >= first, LiteralLessThan bound a) => + [(bound - first) /^ stride]a + fromToDownBy : + {first, last, stride, a} (fin first, fin stride, stride >= 1, + first >= last, Literal first a) => + [1 + (first - last) / stride]a + fromToDownByGreaterThan : + {first, bound, stride, a} (fin first, fin stride, stride >= 1, + first >= bound, Literal first a) => + [(first - bound) /^ stride]a fromToLessThan : {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 6f22bf306..1c4211fe1 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`809 == 1 + • n`825 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at issue290v2.cry:2:8--2:11 where - n`809 is signature variable 'n' at issue290v2.cry:1:11--1:12 + n`825 is signature variable 'n' at issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue582.icry.stdout b/tests/issues/issue582.icry.stdout index 72056447d..07de82fc5 100644 --- a/tests/issues/issue582.icry.stdout +++ b/tests/issues/issue582.icry.stdout @@ -6,13 +6,7 @@ Loading module Cryptol arising from use of partial type function (/^) at issue582.icry:1:1--1:18 - -[error] at issue582.icry:2:1--2:18: - • Unsolvable constraint: - fin inf - arising from - use of partial type function (/^) - at issue582.icry:2:1--2:18 +[False, False, False, False, False, ...] [error] at issue582.icry:3:1--3:16: • Unsolvable constraint: @@ -27,13 +21,7 @@ Loading module Cryptol arising from use of partial type function (%^) at issue582.icry:4:1--4:18 - -[error] at issue582.icry:5:1--5:18: - • Unsolvable constraint: - fin inf - arising from - use of partial type function (%^) - at issue582.icry:5:1--5:18 +0x0 [error] at issue582.icry:6:1--6:16: • Unsolvable constraint: @@ -54,10 +42,6 @@ Loading module Main arising from use of partial type function (/^) at issue582.cry:1:7--1:21 - • fin i - arising from - use of partial type function (/^) - at issue582.cry:1:7--1:21 • j >= 1 arising from use of partial type function (/^) @@ -72,10 +56,6 @@ Loading module Main arising from use of partial type function (%^) at issue582.cry:4:7--4:21 - • fin i - arising from - use of partial type function (%^) - at issue582.cry:4:7--4:21 • j >= 1 arising from use of partial type function (%^) diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index f954bf1dd..c383045b8 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -10,9 +10,9 @@ Loading module Main assuming • fin k the following constraints hold: - • k == n`809 + • k == n`825 arising from matching types at issue723.cry:7:17--7:19 where - n`809 is signature variable 'n' at issue723.cry:1:6--1:7 + n`825 is signature variable 'n' at issue723.cry:1:6--1:7 diff --git a/tests/modsys/T16.icry.stdout b/tests/modsys/T16.icry.stdout index 953033fd5..30dffed60 100644 --- a/tests/modsys/T16.icry.stdout +++ b/tests/modsys/T16.icry.stdout @@ -5,5 +5,5 @@ Loading module T16::B [error] at ./T16/B.cry:5:5--5:11 Multiple definitions for symbol: update - (at Cryptol:844:11--844:17, update) + (at Cryptol:891:11--891:17, update) (at ./T16/A.cry:3:1--3:7, T16::A::update) diff --git a/tests/regression/safety.icry.stdout b/tests/regression/safety.icry.stdout index 796324d60..66f56cee3 100644 --- a/tests/regression/safety.icry.stdout +++ b/tests/regression/safety.icry.stdout @@ -3,7 +3,7 @@ Counterexample (\x -> assert x "asdf" "asdf") False ~> ERROR Run-time error: asdf -- Backtrace -- -Cryptol::error called at Cryptol:998:41--998:46 +Cryptol::error called at Cryptol:1045:41--1045:46 Cryptol::assert called at safety.icry:3:14--3:20 ::it called at safety.icry:3:7--3:37 Counterexample diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout index c66ca8122..5bdd30908 100644 --- a/tests/regression/tc-errors.icry.stdout +++ b/tests/regression/tc-errors.icry.stdout @@ -83,19 +83,19 @@ Loading module Main [error] at tc-errors-5.cry:2:5--2:7: Inferred type is not sufficiently polymorphic. - Quantified variable: a`809 + Quantified variable: a`825 cannot match type: [0]?a When checking the type of 'Main::f' where ?a is type of sequence member at tc-errors-5.cry:2:5--2:7 - a`809 is signature variable 'a' at tc-errors-5.cry:1:6--1:7 + a`825 is signature variable 'a' at tc-errors-5.cry:1:6--1:7 Loading module Cryptol Loading module Main [error] at tc-errors-6.cry:4:7--4:8: The type ?a is not sufficiently polymorphic. - It cannot depend on quantified variables: b`813 + It cannot depend on quantified variables: b`829 When checking the type of 'g' where ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4 - b`813 is signature variable 'b' at tc-errors-6.cry:3:8--3:9 + b`829 is signature variable 'b' at tc-errors-6.cry:3:8--3:9 From 52587711a311d9dd0a70fd42f17d4449a0565a35 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 10:21:50 -0700 Subject: [PATCH 10/16] rename some identifiers in the test for `issue138` We need to avoid the new `down` keyword. --- tests/issues/issue138.cry | 8 ++++---- tests/issues/issue138.icry | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/issues/issue138.cry b/tests/issues/issue138.cry index b28d8398c..24a1a8c35 100644 --- a/tests/issues/issue138.cry +++ b/tests/issues/issue138.cry @@ -1,8 +1,8 @@ -down: [16][4] -down = [ 1+d | d <- tail down ] # [0] +dwn: [16][4] +dwn = [ 1+d | d <- tail dwn ] # [0] -down': [16][4] -down' = [ 1+(down' @ i) | i <- [1 .. 15] ] # [0] +dwn': [16][4] +dwn' = [ 1+(dwn' @ i) | i <- [1 .. 15] ] # [0] take_some: {n,k,t} (n>=k) => [n]t -> [k]t take_some xs = takes where takes = [ x | x <- xs | _ <- takes ] diff --git a/tests/issues/issue138.icry b/tests/issues/issue138.icry index 517399f00..71dbac5cc 100644 --- a/tests/issues/issue138.icry +++ b/tests/issues/issue138.icry @@ -1,4 +1,4 @@ :l issue138.cry -down -down' +dwn +dwn' take_some`{4,3} "abcd" From acb3ca9faef4b1cd6627c08d9b2e26b82e89c6bc Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 10:50:40 -0700 Subject: [PATCH 11/16] Update the `fin` prover with changes to the division operators. --- src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs index 4826bdcb0..0355dbc86 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs @@ -56,7 +56,7 @@ cryIsFinType ctxt ty = i2 = typeInterval varInfo t2 - (TCDiv, [t1,_]) -> SolvedIf [ pFin t1 ] + (TCDiv, [_,_]) -> SolvedIf [] (TCMod, [_,_]) -> SolvedIf [] -- fin (x ^ y) @@ -85,7 +85,7 @@ cryIsFinType ctxt ty = (TCMax, [t1,t2]) -> SolvedIf [ pFin t1, pFin t2 ] (TCWidth, [t1]) -> SolvedIf [ pFin t1 ] - (TCCeilDiv, [_,_]) -> SolvedIf [] + (TCCeilDiv, [t1,_]) -> SolvedIf [ pFin t1 ] (TCCeilMod, [_,_]) -> SolvedIf [] (TCLenFromThenTo,[_,_,_]) -> SolvedIf [] From b3c4317784dd75566d51bef6c1aa5a0c0da440ae Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 13:18:12 -0700 Subject: [PATCH 12/16] Update solver definitions related to `/^` and `%^`. --- lib/CryptolTC.z3 | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3 index 7d8736943..f48923f1d 100644 --- a/lib/CryptolTC.z3 +++ b/lib/CryptolTC.z3 @@ -293,15 +293,19 @@ ) (define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat - (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr - (ite (= (value y) 0) cryErr (cryNat (- (div (- (value x)) (value y))))) - ) + (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr + (ite (= (value y) 0) cryErr + (ite (not (isFin x)) cryInf + (cryNat (- (div (- (value x)) (value y)))) + ))) ) (define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat - (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr - (ite (= (value y) 0) cryErr (cryNat (mod (- (value x)) (value y)))) - ) + (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr + (ite (= (value y) 0) cryErr + (ite (not (isFin x)) (cryNat 0) + (cryNat (mod (- (value x)) (value y))) + ))) ) (define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat From 3ea59c7a69c3a9e5f10b281565088fec8e932865 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 16:01:08 -0700 Subject: [PATCH 13/16] Fix windows test output --- tests/modsys/T16.icry.stdout.mingw32 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/modsys/T16.icry.stdout.mingw32 b/tests/modsys/T16.icry.stdout.mingw32 index 1ed7c0bcc..b203ef673 100644 --- a/tests/modsys/T16.icry.stdout.mingw32 +++ b/tests/modsys/T16.icry.stdout.mingw32 @@ -5,5 +5,5 @@ Loading module T16::B [error] at .\T16\B.cry:5:5--5:11 Multiple definitions for symbol: update - (at Cryptol:844:11--844:17, update) + (at Cryptol:891:11--891:17, update) (at .\T16\A.cry:3:1--3:7, T16::A::update) From 362649bb74ccf323eefe69a1532923effc421861 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 16:23:15 -0700 Subject: [PATCH 14/16] Documentation tweaks and spellcheck in the prelude --- lib/Cryptol.cry | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 3188df268..f6c2e2102 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -32,7 +32,7 @@ primitive type Integer : * /** * 'Z n' is the type of integers, modulo 'n'. * - * The values of 'Z n' may be thought of as equivalance + * The values of 'Z n' may be thought of as equivalence * classes of integers according to the equivalence * 'x ~ y' iff 'n' divides 'x - y'. 'Z n' naturally * forms a ring, but does not support integral division @@ -41,9 +41,9 @@ primitive type Integer : * * However, you may use the 'fromZ' operation * to project values in 'Z n' into the integers if such operations * are required. This will compute the reduced representative - * of the equivalance class. In other words, 'fromZ' computes + * of the equivalence class. In other words, 'fromZ' computes * the (unique) integer value 'i' where '0 <= i < n' and - * 'i' is in the given equivalance class. + * 'i' is in the given equivalence class. * * If the modulus 'n' is prime, 'Z n' also * supports computing inverses and forms a field. @@ -201,19 +201,10 @@ primitive fromTo : {first, last, a} (fin last, last >= first, Literal last a) => [1 + (last - first)]a -/** - * A finite sequence counting up from 'first' to 'last' by 'stride' - * - * '[x .. y by n]` is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'. - */ -primitive fromToBy : {first, last, stride, a} - (fin last, fin stride, stride >= 1, last >= first, Literal last a) => - [1 + (last - first)/stride]a - /** * A possibly infinite sequence counting up from 'first' up to (but not including) 'bound'. * - * '[ x ..< y ]' is syntacic sugar for 'fromToLessThan`{first=x,bound=y}'. + * '[ x ..< y ]' is syntactic sugar for 'fromToLessThan`{first=x,bound=y}'. * * Note that if 'first' = 'bound' then the sequence will be empty. If 'bound = inf' * then the sequence will be infinite, and will eventually wrap around for bounded types. @@ -222,6 +213,17 @@ primitive fromToLessThan : {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => [bound - first]a +/** + * A finite sequence counting up from 'first' to 'last' by 'stride'. + * Note that 'last' will only be an element of the enumeration if + * 'stride' divides 'last - first' evenly. + * + * '[x .. y by n]` is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'. + */ +primitive fromToBy : {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first)/stride]a + /** * A finite sequence counting from 'first' up to (but not including) 'bound' * by 'stride'. Note that if 'first = bound' then the sequence will @@ -236,6 +238,8 @@ primitive fromToByLessThan : {first, bound, stride, a} /** * A finite sequence counting from 'first' down to 'last' by 'stride'. + * Note that 'last' will only be an element of the enumeration if + * 'stride' divides 'first - last' evenly. * * '[x .. y down by n]` is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'. */ @@ -256,7 +260,6 @@ primitive fromToDownByGreaterThan : {first, bound, stride, a} (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => [(first - bound)/^stride]a - /** * A finite arithmetic sequence starting with 'first' and 'next', * stopping when the values reach or would skip over 'last'. @@ -434,7 +437,7 @@ primitive infFromThen : {a} (Integral a) => a -> a -> [inf]a /** * Value types that correspond to a field; that is, - * a ring also posessing multiplicative inverses for + * a ring also possessing multiplicative inverses for * non-zero elements. * * Floating-point values are only approximately a field, @@ -990,7 +993,7 @@ primitive pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] /** * Parallel map. The given function is applied to each element in the - * given finite seqeuence, and the results are computed in parallel. + * given finite sequence, and the results are computed in parallel. * The values in the resulting sequence are reduced to normal form, * as is done with the deepseq operation. * From a3534f99b752a93ca16a14d2a46aa372998e6146 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 16:34:17 -0700 Subject: [PATCH 15/16] Update tests again --- tests/issues/issue103.icry.stdout | 2 +- tests/modsys/T16.icry.stdout | 2 +- tests/modsys/T16.icry.stdout.mingw32 | 2 +- tests/regression/safety.icry.stdout | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/issues/issue103.icry.stdout b/tests/issues/issue103.icry.stdout index a1ddb96e0..1e5c34c41 100644 --- a/tests/issues/issue103.icry.stdout +++ b/tests/issues/issue103.icry.stdout @@ -2,7 +2,7 @@ Loading module Cryptol Run-time error: undefined -- Backtrace -- -Cryptol::error called at Cryptol:1037:13--1037:18 +Cryptol::error called at Cryptol:1040:13--1040:18 Cryptol::undefined called at issue103.icry:1:9--1:18 Using exhaustive testing. Testing... ERROR for the following inputs: diff --git a/tests/modsys/T16.icry.stdout b/tests/modsys/T16.icry.stdout index 30dffed60..545eec073 100644 --- a/tests/modsys/T16.icry.stdout +++ b/tests/modsys/T16.icry.stdout @@ -5,5 +5,5 @@ Loading module T16::B [error] at ./T16/B.cry:5:5--5:11 Multiple definitions for symbol: update - (at Cryptol:891:11--891:17, update) + (at Cryptol:894:11--894:17, update) (at ./T16/A.cry:3:1--3:7, T16::A::update) diff --git a/tests/modsys/T16.icry.stdout.mingw32 b/tests/modsys/T16.icry.stdout.mingw32 index b203ef673..baaee3222 100644 --- a/tests/modsys/T16.icry.stdout.mingw32 +++ b/tests/modsys/T16.icry.stdout.mingw32 @@ -5,5 +5,5 @@ Loading module T16::B [error] at .\T16\B.cry:5:5--5:11 Multiple definitions for symbol: update - (at Cryptol:891:11--891:17, update) + (at Cryptol:894:11--894:17, update) (at .\T16\A.cry:3:1--3:7, T16::A::update) diff --git a/tests/regression/safety.icry.stdout b/tests/regression/safety.icry.stdout index 66f56cee3..58fc9cb35 100644 --- a/tests/regression/safety.icry.stdout +++ b/tests/regression/safety.icry.stdout @@ -3,7 +3,7 @@ Counterexample (\x -> assert x "asdf" "asdf") False ~> ERROR Run-time error: asdf -- Backtrace -- -Cryptol::error called at Cryptol:1045:41--1045:46 +Cryptol::error called at Cryptol:1048:41--1048:46 Cryptol::assert called at safety.icry:3:14--3:20 ::it called at safety.icry:3:7--3:37 Counterexample From 4d5d66ff272756336ce106db40635995596527bd Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 30 Jun 2021 16:51:54 -0700 Subject: [PATCH 16/16] update docs again --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index b0d9c0cbf..63af10205 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -790,7 +790,7 @@ \subsection{Appending and indexing} [] invalid sequence index: 12 -- Backtrace -- - (Cryptol::@) called at Cryptol:867:14--867:20 + (Cryptol::@) called at Cryptol:870:14--870:20 (Cryptol::@@) called at :9:1--9:28 [9, 8, 7, 6, 5, 4, 3, 2, 1, 0] 9