Exclusive enumeration

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -790,7 +790,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:806:14--806:20
+  (Cryptol::@) called at Cryptol:822:14--822:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9

lib/Cryptol.cry

@@ -167,6 +167,13 @@ type constraint i < j = j >= i + 1
 /** 'Literal n a' asserts that type 'a' contains the number 'n'. */
 primitive type Literal : # -> * -> Prop
 
+/**
+ * 'LiteralLessThan n a' asserts that the type 'a' contains all the
+ * natural numbers strictly below 'n'.  Note that we may have 'n = inf',
+ * in which case the type 'a' must be unbounded.
+ */
+primitive type LiteralLessThan : # -> * -> Prop
+
 /**
  * The value corresponding to a numeric type.
  */
@@ -194,6 +201,15 @@ primitive fromTo : {first, last, a} (fin last, last >= first,
                                     Literal first a, Literal last a) =>
                                     [1 + (last - first)]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.
+ */
+primitive fromToLessThan :
+  {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => [bound - first]a
+
+
 /**
  * A finite arithmetic sequence starting with 'first' and 'next',
  * stopping when the values reach or would skip over 'last'.
@@ -879,8 +895,8 @@ updatesEnd xs0 idxs vals = xss!0
  * Declarations of the form 'x @ i = e' are syntactic sugar for
  * 'x = generate (\i -> e)'.
  */
-generate : {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n-1) ix) => (ix -> a) -> [n]a
-generate f = [ f i | i <- [0 .. n-1] ]
+generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
+generate f = [ f i | i <- [0 .. <n] ]
 
 
 // GF_2^n polynomial computations -------------------------------------------

src/Cryptol/Eval/Generic.hs

@@ -1581,6 +1581,21 @@ 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 ]@
@@ -2285,9 +2300,14 @@ genericPrimTable sym getEOpts =
     -- Finite enumerations
   , ("fromTo"     , {-# SCC "Prelude::fromTo" #-}
                     fromToV sym)
+
   , ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}
                     fromThenToV sym)
 
+  , ("fromToLessThan"
+                  , {-# SCC "Prelude::fromToLessThan" #-}
+                    fromToLessThanV sym)
+
     -- Sequence manipulations
   , ("#"          , {-# SCC "Prelude::(#)" #-}
                     PFinPoly \front ->

src/Cryptol/ModuleSystem/Renamer.hs

@@ -724,6 +724,10 @@ instance Rename Expr where
                                <*> traverse rename n
                                <*> rename e
                                <*> traverse rename t
+    EFromToLessThan s e t ->
+                       EFromToLessThan <$> rename s
+                                       <*> 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'

src/Cryptol/Parser.y

@@ -93,7 +93,9 @@ import Paths_cryptol
   '<-'        { Located $$ (Token (Sym ArrL    ) _)}
   '..'        { Located $$ (Token (Sym DotDot  ) _)}
   '...'       { Located $$ (Token (Sym DotDotDot) _)}
+  '..<'       { Located $$ (Token (Sym DotDotLt) _)}
   '|'         { Located $$ (Token (Sym Bar     ) _)}
+  '<'         { Located $$ (Token (Sym Lt      ) _)}
 
   '('         { Located $$ (Token (Sym ParenL  ) _)}
   ')'         { Located $$ (Token (Sym ParenR  ) _)}
@@ -404,6 +406,7 @@ pat_op                           :: { LPName }
   | '-'                             { Located $1 $ mkUnqual $ mkInfix "-" }
   | '~'                             { Located $1 $ mkUnqual $ mkInfix "~" }
   | '^^'                            { Located $1 $ mkUnqual $ mkInfix "^^" }
+  | '<'                             { Located $1 $ mkUnqual $ mkInfix "<" }
 
 
 other_op                         :: { LPName }
@@ -570,6 +573,9 @@ list_expr                      :: { Expr PName }
   | expr          '..' expr       {% eFromTo $2 $1 Nothing   $3 }
   | expr ',' expr '..' expr       {% eFromTo $4 $1 (Just $3) $5 }
 
+  | expr '..' '<' expr            {% eFromToLessThan $2 $1 $4   }
+  | expr '..<'    expr            {% eFromToLessThan $2 $1 $3   }
+
   | expr '...'                    { EInfFrom $1 Nothing         }
   | expr ',' expr '...'           { EInfFrom $1 (Just $3)       }
 

src/Cryptol/Parser/AST.hs

@@ -314,6 +314,9 @@ 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] @
+              | EFromToLessThan (Type n) (Type n) (Maybe (Type n))
+                                                -- ^ @ [ 1 .. < 10 : t ] @
+
               | EInfFrom (Expr n) (Maybe (Expr n))-- ^ @ [1, 3 ...] @
               | EComp (Expr n) [[Match n]]      -- ^ @ [ 1 | x <- xs ] @
               | EApp (Expr n) (Expr n)          -- ^ @ f x @
@@ -748,6 +751,9 @@ 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
+      EFromToLessThan e1 e2 t1 -> brackets (strt <+> text ".. <" <+> end)
+        where strt = maybe (pp e1) (\t -> pp e1 <+> colon <+> pp t) t1
+              end  = pp e2
       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))
@@ -995,6 +1001,7 @@ 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)
+      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)
       EApp  x y       -> EApp     (noPos x) (noPos y)

src/Cryptol/Parser/Lexer.x

@@ -142,6 +142,7 @@ $white+                   { emit $ White Space }
 "`"                       { emit $ Sym BackTick }
 ".."                      { emit $ Sym DotDot }
 "..."                     { emit $ Sym DotDotDot }
+"..<"                     { emit $ Sym DotDotLt  }
 "|"                       { emit $ Sym Bar }
 "("                       { emit $ Sym ParenL }
 ")"                       { emit $ Sym ParenR }
@@ -161,6 +162,9 @@ $white+                   { emit $ White Space }
 "*"                       { emit  (Op   Mul  ) }
 "^^"                      { emit  (Op   Exp  ) }
 
+-- < can appear in the enumeration syntax `[ x .. < y ]
+"<"                       { emit $ Sym Lt }
+
 -- hash is used as a kind, and as a pattern
 "#"                       { emit  (Op   Hash ) }
 

src/Cryptol/Parser/LexerUtils.hs

@@ -524,12 +524,14 @@ data TokenSym = Bar
               | Dot
               | DotDot
               | DotDotDot
+              | DotDotLt
               | Colon
               | BackTick
               | ParenL   | ParenR
               | BracketL | BracketR
               | CurlyL   | CurlyR
               | TriL     | TriR
+              | Lt
               | Underscore
                 deriving (Eq, Show, Generic, NFData)
 

src/Cryptol/Parser/Names.hs

@@ -84,6 +84,7 @@ namesE expr =
                      in Set.unions (e : map namesUF fs)
     EList es      -> Set.unions (map namesE es)
     EFromTo{}     -> 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)
                      in Set.union (boundLNames (concat dss) (namesE e))
@@ -203,6 +204,8 @@ tnamesE expr =
                        `Set.union` maybe Set.empty tnamesT b
                        `Set.union` tnamesT c
                        `Set.union` 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')
     EComp e mss     -> Set.union (tnamesE e) (Set.unions (map tnamesM (concat mss)))
     EApp e1 e2      -> Set.union (tnamesE e1) (tnamesE e2)

src/Cryptol/Parser/NoPat.hs

@@ -154,6 +154,7 @@ noPatE expr =
     EUpd mb fs    -> EUpd    <$> traverse noPatE mb <*> traverse noPatUF fs
     EList es      -> EList   <$> mapM noPatE es
     EFromTo {}    -> return expr
+    EFromToLessThan{} -> return expr
     EInfFrom e e' -> EInfFrom <$> noPatE e <*> traverse noPatE e'
     EComp e mss   -> EComp  <$> noPatE e <*> mapM noPatArm mss
     EApp e1 e2    -> EApp   <$> noPatE e1 <*> noPatE e2

src/Cryptol/Parser/ParserUtils.hs

@@ -371,10 +371,11 @@ eFromTo r e1 e2 e3 =
     (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
+
+asETyped :: Expr n -> Maybe (Expr n, Type n)
+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)
@@ -384,6 +385,24 @@ eFromToType r e1 e2 e3 t =
           <*> exprToNumT r e3
           <*> pure t
 
+eFromToLessThan ::
+  Range -> Expr PName -> Expr PName -> ParseM (Expr PName)
+eFromToLessThan r e1 e2 =
+  case asETyped e2 of
+    Just _  -> errorMessage r ["The exclusive upper bound of an enumeration may not have a type annotation."]
+    Nothing ->
+      case asETyped e1 of
+        Nothing      -> eFromToLessThanType r e1  e2 Nothing
+        Just (e1',t) -> eFromToLessThanType r e1' e2 (Just t)
+
+eFromToLessThanType ::
+  Range -> Expr PName -> Expr PName -> Maybe (Type PName) -> ParseM (Expr PName)
+eFromToLessThanType r e1 e2 t =
+  EFromToLessThan
+    <$> exprToNumT r e1
+    <*> exprToNumT r e2
+    <*> pure t
+
 exprToNumT :: Range -> Expr PName -> ParseM (Type PName)
 exprToNumT r expr =
   case translateExprToNumT expr of

src/Cryptol/TypeCheck/Default.hs

@@ -3,7 +3,7 @@ module Cryptol.TypeCheck.Default where
 import qualified Data.Set as Set
 import           Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Maybe(mapMaybe)
+import Data.Maybe(mapMaybe, isJust)
 import Data.List((\\),nub)
 import Control.Monad(guard,mzero)
 
@@ -35,14 +35,16 @@ defaultLiterals as gs = let (binds,warns) = unzip (mapMaybe tryDefVar as)
   allProps = saturatedPropSet gSet
   has p a  = Set.member (p (TVar a)) allProps
 
+  isLiteralGoal a = isJust (Map.lookup a (literalGoals gSet)) ||
+                    isJust (Map.lookup a (literalLessThanGoals gSet))
   tryDefVar a =
     -- If there is an `FLiteral` constraint we use that for defaulting.
     case Map.lookup a (flitDefaultCandidates gSet) of
       Just m -> m
 
       -- Otherwise we try to use a `Literal`
-      Nothing ->
-        do _gt <- Map.lookup a (literalGoals gSet)
+      Nothing
+        | isLiteralGoal a -> do
            defT <- if has pLogic a then mzero
                    else if has pField a && not (has pIntegral a)
                           then pure tRational
@@ -56,6 +58,7 @@ defaultLiterals as gs = let (binds,warns) = unzip (mapMaybe tryDefVar as)
            -- to depend on
            return ((a,defT),w)
 
+        | otherwise -> mzero
 
 flitDefaultCandidates :: Goals -> Map TVar (Maybe ((TVar,Type),Warning))
 flitDefaultCandidates gs =

src/Cryptol/TypeCheck/Error.hs

@@ -537,6 +537,10 @@ explainUnsolvable names gs =
             let doc2 = tys !! 1
             in custom (doc1 <+> "is not a valid literal of type" <+> doc2)
 
+          PLiteralLessThan ->
+            let doc2 = tys !! 1
+            in custom ("Type" <+> doc2 <+> "does not contain all literals below" <+> (doc1 <> "."))
+
           PFLiteral ->
             case ts of
               ~[m,n,_r,_a] ->

src/Cryptol/TypeCheck/Infer.hs

@@ -183,6 +183,7 @@ appTys expr ts tGoal =
     P.ESel      {} -> mono
     P.EList     {} -> mono
     P.EFromTo   {} -> mono
+    P.EFromToLessThan {} -> mono
     P.EInfFrom  {} -> mono
     P.EComp     {} -> mono
     P.EApp      {} -> mono
@@ -294,6 +295,20 @@ checkE expr tGoal =
          es' <- mapM checkElem es
          return (EList es' a)
 
+    P.EFromToLessThan t1 t2 mety ->
+      do l <- curRange
+         let fs0 =
+               case mety of
+                 Just ety -> [("a", ety)]
+                 Nothing  -> []
+         let fs = [("first", t1), ("bound", t2)] ++ fs0
+         prim <- mkPrim "fromToLessThan"
+         let e' = P.EAppT prim
+                  [ P.NamedInst P.Named { name = Located l (packIdent x), value = y }
+                  | (x,y) <- fs
+                  ]
+         checkE e' tGoal
+
     P.EFromTo t1 mbt2 t3 mety ->
       do l <- curRange
          let fs0 =

src/Cryptol/TypeCheck/InferTypes.hs

@@ -67,6 +67,10 @@ data Goals = Goals
 
   , literalGoals :: Map TVar LitGoal
     -- ^ An entry @(a,t)@ corresponds to @Literal t a@.
+
+  , literalLessThanGoals :: Map TVar LitGoal
+    -- ^ An entry @(a,t)@ corresponds to @LiteralLessThan t a@.
+
   } deriving (Show)
 
 -- | This abuses the type 'Goal' a bit. The 'goal' field contains
@@ -85,15 +89,35 @@ goalToLitGoal g =
      return (a, g { goal = tn })
 
 
+litLessThanGoalToGoal :: (TVar,LitGoal) -> Goal
+litLessThanGoalToGoal (a,g) = g { goal = pLiteralLessThan (goal g) (TVar a) }
+
+goalToLitLessThanGoal :: Goal -> Maybe (TVar,LitGoal)
+goalToLitLessThanGoal g =
+  do (tn,a) <- matchMaybe $ do (tn,b) <- aLiteralLessThan (goal g)
+                               a      <- aTVar b
+                               return (tn,a)
+     return (a, g { goal = tn })
+
 
 emptyGoals :: Goals
-emptyGoals  = Goals { goalSet = Set.empty, saturatedPropSet = Set.empty, literalGoals = Map.empty }
+emptyGoals  =
+  Goals
+  { goalSet = Set.empty
+  , saturatedPropSet = Set.empty
+  , literalGoals = Map.empty
+  , literalLessThanGoals = Map.empty
+  }
 
 nullGoals :: Goals -> Bool
-nullGoals gs = Set.null (goalSet gs) && Map.null (literalGoals gs)
+nullGoals gs =
+  Set.null (goalSet gs) &&
+  Map.null (literalGoals gs) &&
+  Map.null (literalLessThanGoals gs)
 
 fromGoals :: Goals -> [Goal]
 fromGoals gs = map litGoalToGoal (Map.toList (literalGoals gs)) ++
+               map litLessThanGoalToGoal (Map.toList (literalLessThanGoals gs)) ++
                Set.toList (goalSet gs)
 
 goalsFromList :: [Goal] -> Goals
@@ -109,6 +133,11 @@ insertGoal g gls
            , saturatedPropSet = Set.insert (pFin (TVar a)) (saturatedPropSet gls)
            }
 
+  | Just (a,newG) <- goalToLitLessThanGoal g =
+       let jn g1 g2 = g1 { goal = tMax (goal g1) (goal g2) } in
+       gls { literalLessThanGoals = Map.insertWith jn a newG (literalLessThanGoals gls)
+           }
+
   -- If the goal is already implied by some other goal, skip it
   | Set.member (goal g) (saturatedPropSet gls) = gls