FV remove enumerate shim (#1155)

Author: rsoeldner

src-tool/Pact/Analyze/Eval/Core.hs

@@ -163,6 +163,27 @@ evalCore (Compose tya tyb _ a (Open vida _nma tmb) (Open vidb _nmb tmc)) = do
   b' <- withVar vida (mkAVal a') $ withSing tyb $ eval tmb
   withVar vidb (mkAVal b') $ eval tmc
 evalCore (StrConcat p1 p2)                 = (.++) <$> eval p1 <*> eval p2
+
+evalCore (Enumerate from to step)          =  do
+  S _ from' <- eval from
+  S _ to'   <- eval to
+  S _ step' <- eval step
+  let
+    go :: (forall v. OrdSymbolic v => v -> v -> SBV Bool) -> SBV Integer -> SBV Integer -> SBV Integer -> SBV [Integer]
+    go cmp b e s = ite (b `cmp` e) (b SBVL..: go cmp (b + s) e s) SBVL.nil
+    
+  let algPos = ite (from' .== to') (SBVL.singleton from')
+              (ite (step' .== 0) (SBVL.singleton from' )
+               (ite (from' + step' .> to') (SBVL.singleton from') (go (.<=) from' to' step')))
+               
+      algNeg =  ite (step' .== 0) (SBVL.singleton from' )
+                (ite (from' + step' .< to') (SBVL.singleton from') (go (.>=) from' to' step'))
+
+
+  markFailure $ (from' .< to' .&& step' .< 0) .|| (from' .> to' .&& step' .> 0)
+
+  pure $ sansProv (ite (from' .<= to') algPos algNeg)
+
 evalCore (StrLength p)
   = over s2Sbv SBVS.length . coerceS @Str @String <$> eval p
 evalCore (StrToInt s)                      = evalStrToInt s

src-tool/Pact/Analyze/Feature.hs

@@ -110,6 +110,7 @@ data Feature
   | FListProjection
   | FListLength
   | FContains
+  | FEnumerate
   | FReverse
   | FSort
   | FListDrop
@@ -952,6 +953,22 @@ doc FContains = Doc
         ]
       (TyCon bool)
   ]
+doc FEnumerate = Doc
+  "enumerate"
+  CList
+  InvAndProp
+  "Returns a sequence of numbers as a list"
+  [ Usage
+      "(drop n xs)"
+      Map.empty
+      $ Fun
+        Nothing
+        [ ("from", TyCon int)
+        , ("to"  , TyCon int)
+        , ("step", TyCon int)
+        ]
+      (TyList' (TyCon int))
+  ]
 
 doc FReverse = Doc
   "reverse"
@@ -1736,6 +1753,7 @@ PAT(SOrQ, FOrQ)
 PAT(SObjectProjection, FObjectProjection)
 PAT(SListLength, FListLength)
 PAT(SContains, FContains)
+PAT(SEnumerate, FEnumerate)
 PAT(SReverse, FReverse)
 PAT(SSort, FSort)
 PAT(SListDrop, FListDrop)

src-tool/Pact/Analyze/Parse/Prop.hs

@@ -393,6 +393,18 @@ inferPreProp preProp = case preProp of
   -- applications:
   --
   -- Function types are inferred; arguments are checked.
+
+  PreApp s args
+    | s == SEnumerate -> do
+        args' <- for args $ \arg -> inferPreProp arg >>= \case
+          Some SInteger i -> pure i
+          _otherwise -> throwErrorIn preProp "expected integer arguments"
+
+        case args' of
+          [from, to] -> pure $ Some (SList SInteger) $ CoreProp $ Enumerate from to (Lit' 1)
+          [from, to, step] -> pure $ Some (SList SInteger) $ CoreProp $ Enumerate from to step
+          _otherwise -> throwErrorIn preProp "expected 2 or 3 integer arguments"
+
   PreApp s [arg] | s == SStringLength -> do
     arg' <- inferPreProp arg
     case arg' of

src-tool/Pact/Analyze/PrenexNormalize.hs

@@ -126,6 +126,8 @@ singFloat ty p = case p of
     CoreProp <$> (ListEqNeq ty' op <$> singFloat (SList ty') a <*> singFloat (SList ty') b)
   CoreProp (StrContains needle haystack) -> CoreProp <$>
     (StrContains <$> float needle <*> float haystack)
+  CoreProp (Enumerate from to step) -> CoreProp <$>
+    (Enumerate <$> float from <*> float to <*> float step) 
   CoreProp (ListContains ty' needle haystack) ->
     CoreProp <$> (ListContains ty' <$> singFloat ty' needle <*> singFloat (SList ty') haystack)
 

src-tool/Pact/Analyze/Translate.hs

@@ -1714,8 +1714,14 @@ translateNode astNode = withAstContext astNode $ case astNode of
     Some ty@(SList elemTy) l -> pure $ Some ty $ CoreTerm $ ListDistinct elemTy l
     _ -> unexpectedNode astNode
 
-  AST_NFun node fn@"enumerate" args ->
-    shimNative' node fn args "[0]" (Some (SList SInteger) (Lit' [0]))
+  AST_NFun _node _fn@"enumerate" args -> do
+    args' <- for args $ \arg -> translateNode arg >>= \case
+      Some SInteger i' -> pure i'
+      _otherwise -> unexpectedNode astNode
+    case args' of
+      [from, to']       -> pure $ Some (SList SInteger) $ CoreTerm $ Enumerate from to' (Lit' 1)
+      [from, to', step] -> pure $ Some (SList SInteger) $ CoreTerm $ Enumerate from to' step
+      _otherwise -> unexpectedNode astNode
 
   AST_NFun node fn@"format" [a, b] -> translateNode a >>= \a' -> case a' of
     -- uncaught case is dynamic list, sub format string

src-tool/Pact/Analyze/Types/Languages.hs

@@ -206,6 +206,8 @@ data Core (t :: Ty -> K.Type) (a :: Ty) where
   StrToIntBase :: t 'TyInteger -> t 'TyStr -> Core t 'TyInteger
   StrContains  :: t 'TyStr     -> t 'TyStr -> Core t 'TyBool
 
+  Enumerate :: t 'TyInteger -> t 'TyInteger -> t 'TyInteger -> Core t ('TyList 'TyInteger)
+
   -- numeric ops
   Numerical    :: Numerical t a -> Core t a
 
@@ -721,6 +723,7 @@ showsPrecCore ty p core = showParen (p > 10) $ case core of
   StrToInt a       -> showString "StrToInt "     . showsTm 11 a
   StrToIntBase a b -> showString "StrToIntBase " . showsTm 11 a . showChar ' ' . showsTm 11 b
   StrContains  a b -> showString "StrContains "  . showsTm 11 a . showChar ' ' . showsTm 11 b
+  Enumerate a b c  -> showString "Enumerate "    . showsTm 11 a . showChar ' ' . showsTm 11 b . showChar ' ' . showsTm 11 c
   Numerical a      -> showString "Numerical "    . showsNumerical ty 11 a
   IntAddTime a b   -> showString "IntAddTime "   . showsTm 11 a . showChar ' ' . showsTm 11 b
   DecAddTime a b   -> showString "DecAddTime "   . showsTm 11 a . showChar ' ' . showsTm 11 b
@@ -964,6 +967,7 @@ prettyCore ty = \case
   StrToIntBase b s         -> parensSep [pretty SStringToInteger, prettyTm b, prettyTm s]
   StrContains needle haystack
     -> parensSep [pretty SContains, prettyTm needle, prettyTm haystack]
+  Enumerate x y z          -> parensSep [pretty SEnumerate, prettyTm x, prettyTm y, prettyTm z]
   Numerical tm             -> prettyNumerical ty tm
   IntAddTime x y           -> parensSep [pretty STemporalAddition, prettyTm x, prettyTm y]
   DecAddTime x y           -> parensSep [pretty STemporalAddition, prettyTm x, prettyTm y]
@@ -1830,6 +1834,8 @@ propToInvariant (CoreProp core) = CoreInvariant <$> case core of
     StrToIntBase <$> f tm1 <*> f tm2
   StrContains tm1 tm2 ->
     StrContains <$> f tm1 <*> f tm2
+  Enumerate tm1 tm2 tm3 ->
+    Enumerate <$> f tm1 <*> f tm2 <*> f tm3
   Numerical num ->
     Numerical <$> numF num
   IntAddTime tm1 tm2 ->

tests/AnalyzeSpec.hs

@@ -3672,6 +3672,82 @@ spec = describe "analyze" $ do
     -- we expect this to give an error
     expectVerified code
 
+  describe "enumeration positive" $ do
+      let code model =
+            [text|
+                 (defun test:[integer] ()
+                   @model $model
+                   (enumerate 0 10 1))
+            |]
+      expectVerified $ code "[(property (= result (enumerate 0 10)))]"
+      expectVerified $ code "[(property (= result (enumerate 0 10 1)))]"
+
+  describe "enumeration positive (FROM = TO)" $ do
+      let code model =
+            [text|
+                 (defun test:[integer] ()
+                   @model $model
+                   (enumerate 10 10))
+            |]
+      expectVerified $ code "[(property (= result [10]))]"
+
+  describe "enumeration positive (INC = 0)" $ do
+      let code model =
+            [text|
+                 (defun test:[integer] ()
+                   @model $model
+                   (enumerate 10 10 0))
+            |]
+      expectVerified $ code "[(property (= result [10]))]"
+
+  describe "enumeration positive (FROM + INC > TO)" $ do
+      let code model =
+            [text|
+                 (defun test:[integer] ()
+                   @model $model
+                   (enumerate 10 15 10))
+            |]
+      expectVerified $ code "[(property (= result [10]))]"
+
+ 
+  describe "enumeration negative" $ do
+      let code model =
+            [text|
+                 (defun test:[integer] ()
+                   @model $model
+                   (enumerate 10 1 -1))
+            |]
+      expectVerified $ code "[(property (= result (enumerate 10 1 -1)))]"
+      expectVerified $ code "[(property (= result [10 9 8 7 6 5 4 3 2 1]))]"
+
+  describe "enumeration negative should fail" $ do
+      let code =
+            [text|
+                 (defun test:[integer] ()
+                 @model [(property (= result (enumerate 10 1 1))]
+                   (enumerate 10 1 1))
+            |]
+      expectFalsified code 
+  describe "enumeration positive should fail" $ do
+      let code =
+            [text|
+                 (defun test:[integer] ()
+                 @model [(property (= result (enumerate 1 10 -1))]
+                   (enumerate 1 10 -1))
+            |]
+      expectFalsified code 
+
+  describe "enumeration positiv with step" $ do
+      let code model =
+            [text|
+                 (defun test:[integer] ()
+                   @model $model
+                   (enumerate 0 10 2))
+            |]
+      expectVerified  $ code "[(property (= result [0 2 4 6 8 10]))]"
+      expectFalsified $ code "[(property (= result []))]"
+
+
   describe "string drop" $ do
     let code1 model = [text|
           (defun test:string ()