From af5c9ea7a38c8bdd088f6eec7a7fa8228ef16539 Mon Sep 17 00:00:00 2001 From: rsoeldner Date: Mon, 26 Feb 2024 15:34:28 +0100 Subject: [PATCH] fixes #1346, parsing of diff-time as property --- src-tool/Pact/Analyze/Parse/Prop.hs | 6 ++++++ tests/AnalyzeSpec.hs | 9 +++++++++ 2 files changed, 15 insertions(+) diff --git a/src-tool/Pact/Analyze/Parse/Prop.hs b/src-tool/Pact/Analyze/Parse/Prop.hs index 81228ccb3..432bfcedd 100644 --- a/src-tool/Pact/Analyze/Parse/Prop.hs +++ b/src-tool/Pact/Analyze/Parse/Prop.hs @@ -458,6 +458,12 @@ inferPreProp preProp = case preProp of _ -> throwErrorIn b $ "expected integer or decimal, found " <> pretty (existentialType b') + PreApp s [a,b] + | s == STemporalDiff -> do + a' <- checkPreProp STime a + b' <- checkPreProp STime b + pure $ Some SDecimal $ CoreProp $ DiffTime a' b' + PreApp op'@(toOp comparisonOpP -> Just op) [a, b] -> do a''@(Some aTy a') <- inferPreProp a b''@(Some bTy b') <- inferPreProp b diff --git a/tests/AnalyzeSpec.hs b/tests/AnalyzeSpec.hs index 8c5deefed..a226f6a41 100644 --- a/tests/AnalyzeSpec.hs +++ b/tests/AnalyzeSpec.hs @@ -2360,6 +2360,15 @@ spec = describe "analyze" $ do (diff-time (time "2021-01-01T00:00:01Z") (time "2021-01-01T00:00:00Z"))) |] in expectVerified code + describe "diff-time implementation as property (#1346)" $ + let code = + [text| + (defun test:decimal (a: time b: time) + @model[(property (> (diff-time a b) 0.0))] + (enforce (> (diff-time a b) 0.0) "a-b > 0") + 1.0) + |] + in expectVerified code describe "regression time representation (int64/integer)" $ let code =