Explicit stride

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. */
@@ -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
 
 
 /**

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 ->

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
@@ -727,6 +734,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

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 }
 

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)

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 ) }
 

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')

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