add diff-time to FV

docs/en/pact-properties-api.md

@@ -944,6 +944,20 @@ Add seconds to a time
 
 Supported in either invariants or properties.
 
+### diff-time {#FTemporalDiff}
+
+```lisp
+(diff-time a b)
+```
+
+* takes `a`: `time`
+* takes `b`: `time`
+* produces `decimal`
+
+Time difference in seconds
+
+Supported in properties only.
+
 ## Quantification operators {#Quantification}
 
 ### forall {#FUniversalQuantification}

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

@@ -103,6 +103,16 @@ evalDecAddTime timeT secsT = do
   else throwErrorNoLoc $ PossibleRoundoff
     "A time being added is not concrete, so we can't guarantee that roundoff won't happen when it's converted to an integer."
 
+evalDiffTime
+  :: Analyzer m
+  => TermOf m 'TyTime
+  -> TermOf m 'TyTime
+  -> m (S Decimal)
+evalDiffTime a b = do
+  a' <- eval a
+  b' <- eval b
+  pure $  (fromInteger' (fromIntegralS a' - fromIntegralS b')) / 1000000
+
 evalComparisonOp
   :: forall m a.
      Analyzer m
@@ -211,6 +221,7 @@ evalCore (StrDrop n s)                     = evalStrDrop n s
 evalCore (Numerical a)                     = evalNumerical a
 evalCore (IntAddTime time secs)            = evalIntAddTime time secs
 evalCore (DecAddTime time secs)            = evalDecAddTime time secs
+evalCore (DiffTime a b)                    = evalDiffTime a b
 evalCore (Comparison ty op x y)            = evalComparisonOp ty op x y
 evalCore (Logical op props)                = evalLogicalOp op props
 evalCore (ObjAt schema colNameT objT)

src-tool/Pact/Analyze/Feature.hs

@@ -135,6 +135,7 @@ data Feature
   | FListHash
   -- Temporal operators
   | FTemporalAddition
+  | FTemporalDiff
   -- Quantification forms
   | FUniversalQuantification
   | FExistentialQuantification
@@ -1320,7 +1321,16 @@ doc FTemporalAddition = Doc
         ]
         (TyCon time)
   ]
-
+doc FTemporalDiff = Doc
+  "diff-time"
+  CTemporal
+  PropOnly
+  "Time difference in seconds"
+  [Usage
+    "(diff-time a b)"
+    Map.empty
+    $ Fun Nothing [("a", TyCon time), ("b", TyCon time)] (TyCon dec)
+  ]
 --
 -- Property-specific features
 --
@@ -1885,6 +1895,7 @@ PAT(SNumericalHash, FNumericalHash)
 PAT(SBoolHash, FBoolHash)
 PAT(SListHash, FListHash)
 PAT(STemporalAddition, FTemporalAddition)
+PAT(STemporalDiff, FTemporalDiff)
 PAT(SUniversalQuantification, FUniversalQuantification)
 PAT(SExistentialQuantification, FExistentialQuantification)
 PAT(SColumnOf, FColumnOf)

src-tool/Pact/Analyze/Patterns.hs

@@ -192,6 +192,9 @@ pattern AST_Hash val <- App _node (NativeFunc "hash") [val]
 pattern AST_AddTime :: forall a. AST a -> AST a -> AST a
 pattern AST_AddTime time seconds <- App _ (NativeFunc STemporalAddition) [time, seconds]
 
+pattern AST_DiffTime :: forall a. AST a -> AST a -> AST a
+pattern AST_DiffTime a b <- App _ (NativeFunc STemporalDiff) [a, b]
+
 pattern AST_Days :: forall a. AST a -> AST a
 pattern AST_Days days <- App _ (NativeFunc "days") [days]
 

src-tool/Pact/Analyze/PrenexNormalize.hs

@@ -112,6 +112,7 @@ singFloat ty p = case p of
   -- time
   CoreProp (IntAddTime time int) -> PIntAddTime <$> float time <*> float int
   CoreProp (DecAddTime time dec) -> PDecAddTime <$> float time <*> float dec
+  CoreProp (DiffTime a b) -> CoreProp ... DiffTime <$> float a <*> float b
 
   -- bool
   -- - quantification

src-tool/Pact/Analyze/Translate.hs

@@ -1433,6 +1433,12 @@ translateNode astNode = withAstContext astNode $ case astNode of
     tsStaticCapsInScope %= Set.insert capName
     return app
 
+  AST_DiffTime a b -> translateNode a >>= \case
+    Some STime a' -> translateNode b >>= \case
+      Some STime b' -> pure $ Some SDecimal $ CoreTerm $ DiffTime a' b'
+      _ -> unexpectedNode astNode
+    _ -> unexpectedNode astNode
+
   AST_AddTime time seconds
     | seconds ^. aNode . aTy == TyPrim Pact.TyInteger ||
       seconds ^. aNode . aTy == TyPrim Pact.TyDecimal -> translateNode time >>= \case

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

@@ -223,6 +223,8 @@ data Core (t :: Ty -> K.Type) (a :: Ty) where
   IntAddTime :: t 'TyTime -> t 'TyInteger -> Core t 'TyTime
   -- | Adds a 'Decimal' expression to a 'Time' expression
   DecAddTime :: t 'TyTime -> t 'TyDecimal -> Core t 'TyTime
+  -- | Diff two times
+  DiffTime :: t 'TyTime -> t 'TyTime -> Core t 'TyDecimal
 
   -- comparison. Note that while it's cumbersome to define five different
   -- monomorphized comparisons, the alternative is implementing Eq by hand
@@ -767,6 +769,7 @@ showsPrecCore ty p core = showParen (p > 10) $ case core of
   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
+  DiffTime a b     -> showString "DiffTime "     . showsTm 11 a . showChar ' ' . showsTm 11 b
   Comparison ty' op a b ->
       showString "Comparison "
     . showsPrec 11 ty'
@@ -1015,7 +1018,7 @@ prettyCore ty = \case
   StrToIntBase b s         -> parensSep [pretty SStringToInteger, prettyTm b, prettyTm s]
   StrContains needle haystack
     -> parensSep [pretty SContains, prettyTm needle, prettyTm haystack]
-    
+
   StrHash x                -> parensSep [pretty SStringHash, prettyTm x]
   IntHash x                -> parensSep [pretty SNumericalHash, prettyTm x]
   BoolHash x               -> parensSep [pretty SBoolHash, prettyTm x]
@@ -1026,6 +1029,7 @@ prettyCore ty = \case
   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]
+  DiffTime a b             -> parensSep [pretty STemporalDiff, prettyTm a, prettyTm b]
   Comparison ty' op x y    -> parensSep [pretty op, singPrettyTm ty' x, singPrettyTm ty' y]
   GuardEqNeq op x y        -> parensSep [pretty op, prettyTm x, prettyTm y]
   ObjectEqNeq ty1 ty2 op x y
@@ -1915,6 +1919,8 @@ propToInvariant (CoreProp core) = CoreInvariant <$> case core of
     IntAddTime <$> f tm1 <*> f tm2
   DecAddTime tm1 tm2 ->
     DecAddTime <$> f tm1 <*> f tm2
+  DiffTime tm1 tm2 ->
+    DiffTime <$> f tm1 <*> f tm2
   Comparison ty op tm1 tm2 ->
     Comparison ty op <$> f tm1 <*> f tm2
   GuardEqNeq op tm1 tm2 ->

tests/AnalyzeSpec.hs

@@ -2333,6 +2333,24 @@ spec = describe "analyze" $ do
               ))
           |]
     in expectPass code $ Valid $ sNot Abort'
+
+  describe "diff-time implementation (#1291)" $
+    let code =
+          [text|
+            (defun test:decimal ()
+              @model[(property (= result -60.0))]
+              (diff-time (time "2021-01-01T00:00:00Z") (time "2021-01-01T00:01:00Z")))
+
+            (defun test1:decimal ()
+              @model[(property (= result -61.0))]
+              (diff-time (time "2021-01-01T00:00:00Z") (time "2021-01-01T00:01:01Z")))
+
+            (defun test2:decimal ()
+              @model[(property (= result 1.0))]
+              (diff-time (time "2021-01-01T00:00:01Z") (time "2021-01-01T00:00:00Z")))
+          |]
+    in expectVerified code
+
   describe "regression time representation (int64/integer)" $
     let code =
           [text|