From 8644e292f07c60e916aa35435f94caa7f8cdd44b Mon Sep 17 00:00:00 2001
From: Robert Soeldner <r.soeldner@gmail.com>
Date: Tue, 28 Feb 2023 17:07:00 +0100
Subject: [PATCH 1/2] remove fv distinct shim

---
 docs/en/pact-properties-api.md           | 13 +++++++++++++
 src-tool/Pact/Analyze/Eval/Core.hs       |  7 ++++++-
 src-tool/Pact/Analyze/Feature.hs         | 18 ++++++++++++++++++
 src-tool/Pact/Analyze/PrenexNormalize.hs |  2 ++
 src-tool/Pact/Analyze/Translate.hs       |  5 ++---
 src-tool/Pact/Analyze/Types/Languages.hs | 10 ++++++++++
 tests/AnalyzeSpec.hs                     | 10 ++++++++++
 7 files changed, 61 insertions(+), 4 deletions(-)

diff --git a/docs/en/pact-properties-api.md b/docs/en/pact-properties-api.md
index 70477d202..202763063 100644
--- a/docs/en/pact-properties-api.md
+++ b/docs/en/pact-properties-api.md
@@ -731,6 +731,19 @@ filter a list by keeping the values for which `f` returns `true`
 
 Supported in either invariants or properties.
 
+### distinct {#FDistinct}
+
+```lisp
+(distinct xs)
+```
+
+* takes `xs`: [_a_]
+* produces [_a_]
+
+returns a list of distinct values
+
+Supported in either invariants or properties.
+
 ### fold {#FFold}
 
 ```lisp
diff --git a/src-tool/Pact/Analyze/Eval/Core.hs b/src-tool/Pact/Analyze/Eval/Core.hs
index fa1002880..67b754575 100644
--- a/src-tool/Pact/Analyze/Eval/Core.hs
+++ b/src-tool/Pact/Analyze/Eval/Core.hs
@@ -242,6 +242,11 @@ evalCore (LiteralList ty xs) = withSymVal ty $ withSing ty $ do
   vals <- traverse (fmap _sSbv . eval) xs
   pure $ sansProv $ SBVL.implode vals
 
+evalCore (ListDistinct ty list) = withSymVal ty $ withSing ty $ withEq ty $ do
+  S _ list' <- eval list
+  pure $ sansProv (SBVL.reverse (bfoldr listBound (\a b -> ite (SBVL.elem a b) b (a SBVL..: b)) SBVL.nil list'))
+
+ 
 evalCore (ListDrop ty n list) = withSymVal ty $ withSing ty $ do
   S _ n'    <- eval n
   S _ list' <- eval list
@@ -296,7 +301,7 @@ evalCore (ListFilter tya (Open vid _ f) as)
         (\sbva svblst -> do
           S _ x' <- withVar vid (mkAVal' sbva) (eval f)
           pure $ ite x' (sbva .: svblst) svblst)
-        (literal [])
+        SBVL.nil
   sansProv <$> bfilterM as'
 
 evalCore (ListFold tya tyb (Open vid1 _ (Open vid2 _ f)) a bs)
diff --git a/src-tool/Pact/Analyze/Feature.hs b/src-tool/Pact/Analyze/Feature.hs
index de3f514b1..70a2d5178 100644
--- a/src-tool/Pact/Analyze/Feature.hs
+++ b/src-tool/Pact/Analyze/Feature.hs
@@ -117,6 +117,7 @@ data Feature
   | FMakeList
   | FMap
   | FFilter
+  | FDistinct
   | FFold
   -- String operators
   | FStringLength
@@ -1069,6 +1070,22 @@ doc FFilter = Doc
         ]
       (TyList' a)
   ]
+
+doc FDistinct = Doc
+  "distinct"
+  CList
+  InvAndProp
+  "returns a list of distinct values"
+  [ let a = TyVar $ TypeVar "a"
+    in Usage
+      "(distinct xs)"
+      Map.empty
+      $ Fun
+        Nothing
+        [ ("xs", TyList' a)
+        ]
+      (TyList' a)
+  ]
 doc FFold = Doc
   "fold"
   CList
@@ -1722,6 +1739,7 @@ PAT(SContains, FContains)
 PAT(SReverse, FReverse)
 PAT(SSort, FSort)
 PAT(SListDrop, FListDrop)
+PAT(SDistinct, FDistinct)
 PAT(SListTake, FListTake)
 PAT(SMakeList, FMakeList)
 PAT(SMap, FMap)
diff --git a/src-tool/Pact/Analyze/PrenexNormalize.hs b/src-tool/Pact/Analyze/PrenexNormalize.hs
index 7d42fdfe6..59e1f2661 100644
--- a/src-tool/Pact/Analyze/PrenexNormalize.hs
+++ b/src-tool/Pact/Analyze/PrenexNormalize.hs
@@ -153,6 +153,8 @@ singFloat ty p = case p of
     -> CoreProp . ListReverse ty' <$> singFloat (SList ty') lst
   CoreProp (ListSort ty' lst)
     -> CoreProp . ListSort ty' <$> singFloat (SList ty') lst
+  CoreProp (ListDistinct ty' lst)
+    -> CoreProp . ListDistinct ty' <$> singFloat (SList ty') lst
   CoreProp (ListDrop ty' a b)
     -> CoreProp <$> (ListDrop ty' <$> float a <*> singFloat (SList ty') b)
   CoreProp (ListTake ty' a b)
diff --git a/src-tool/Pact/Analyze/Translate.hs b/src-tool/Pact/Analyze/Translate.hs
index b845b8621..6ba804857 100644
--- a/src-tool/Pact/Analyze/Translate.hs
+++ b/src-tool/Pact/Analyze/Translate.hs
@@ -1708,9 +1708,8 @@ translateNode astNode = withAstContext astNode $ case astNode of
     -- elide translation of event capability
     shimNative astNode node fn []
 
-  AST_NFun node fn@"distinct" [xs] -> translateNode xs >>= \xs' -> case xs' of
-    Some (SList _) _ ->
-      shimNative' node fn [] "original list" xs'
+  AST_NFun _ "distinct" [xs] -> translateNode xs >>= \xs' -> case xs' of
+    Some ty@(SList elemTy) l -> pure $ Some ty $ CoreTerm $ ListDistinct elemTy l
     _ -> unexpectedNode astNode
 
   AST_NFun node fn@"enumerate" args ->
diff --git a/src-tool/Pact/Analyze/Types/Languages.hs b/src-tool/Pact/Analyze/Types/Languages.hs
index 383c3d19d..9fe9b78b3 100644
--- a/src-tool/Pact/Analyze/Types/Languages.hs
+++ b/src-tool/Pact/Analyze/Types/Languages.hs
@@ -261,6 +261,8 @@ data Core (t :: Ty -> K.Type) (a :: Ty) where
   ListEqNeq    :: SingTy a -> EqNeq -> t ('TyList a) -> t ('TyList a) -> Core t 'TyBool
   ListAt       :: SingTy a -> t 'TyInteger -> t ('TyList a) -> Core t a
   ListContains :: SingTy a -> t a      -> t ('TyList a) -> Core t 'TyBool
+  
+  ListDistinct :: SingTy a -> t ('TyList a) -> Core t ('TyList a)
 
   ListLength   :: SingTy a -> t ('TyList a) -> Core t 'TyInteger
 
@@ -843,6 +845,11 @@ showsPrecCore ty p core = showParen (p > 10) $ case core of
     . showsPrec 11 ty'
     . showChar ' '
     . singShowsTmList ty' 11 a
+  ListDistinct ty' a ->
+      showString "ListDistinct "
+      . showsPrec 11 ty'
+      . showChar ' '
+      . singShowsTmList ty' 11 a
   ListDrop ty' i l ->
       showString "ListDrop "
     . showsPrec 11 ty'
@@ -980,6 +987,7 @@ prettyCore ty = \case
   ListLength ty' x         -> parensSep [pretty SListLength, singPrettyTmList ty' x]
   ListReverse ty' lst      -> parensSep [pretty SReverse, singPrettyTmList ty' lst]
   ListSort ty' lst         -> parensSep [pretty SSort, singPrettyTmList ty' lst]
+  ListDistinct ty' lst     -> parensSep [pretty SDistinct, singPrettyTmList ty' lst]
   ListDrop ty' n lst       -> parensSep [pretty SListDrop, prettyTm n, singPrettyTmList ty' lst]
   ListTake ty' n lst       -> parensSep [pretty SListTake, prettyTm n, singPrettyTmList ty' lst]
   ListConcat ty' x y       -> parensSep [pretty SConcatenation, singPrettyTmList ty' x, singPrettyTmList ty' y]
@@ -1862,6 +1870,8 @@ propToInvariant (CoreProp core) = CoreInvariant <$> case core of
     ListReverse ty <$> f tm
   ListSort ty tm ->
     ListSort ty <$> f tm
+  ListDistinct ty tm ->
+    ListDistinct ty <$> f tm
   ListConcat ty tm1 tm2 ->
     ListConcat ty <$> f tm1 <*> f tm2
   ListDrop ty tm1 tm2 ->
diff --git a/tests/AnalyzeSpec.hs b/tests/AnalyzeSpec.hs
index 6e1ae89ce..895b7a471 100644
--- a/tests/AnalyzeSpec.hs
+++ b/tests/AnalyzeSpec.hs
@@ -3859,6 +3859,16 @@ spec = describe "analyze" $ do
             (min a (min b c)))
           |]
 
+  describe "list distinct" $ do
+    let code9 model = [text|
+          (defun test:[integer] (a:integer b:integer)
+            @model $model
+            (enforce (not (= a b)) "")
+            (distinct [a b a]))
+          |]
+    expectVerified  $ code9 "[(property (= result [a b]))]"
+    expectFalsified $ code9 "[(property (= result [a b a]))]"
+
   describe "identity" $ do
     expectVerified [text|
           (defun test:integer ()

From 97ef3e15252d9f6461a0bb0b984a6d81751c641e Mon Sep 17 00:00:00 2001
From: Robert Soeldner <r.soeldner@gmail.com>
Date: Wed, 1 Mar 2023 20:47:24 +0100
Subject: [PATCH 2/2] add distinct prop parsing

---
 src-tool/Pact/Analyze/Parse/Prop.hs | 8 ++++++++
 tests/AnalyzeSpec.hs                | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/src-tool/Pact/Analyze/Parse/Prop.hs b/src-tool/Pact/Analyze/Parse/Prop.hs
index fffda2d01..36827e918 100644
--- a/src-tool/Pact/Analyze/Parse/Prop.hs
+++ b/src-tool/Pact/Analyze/Parse/Prop.hs
@@ -402,6 +402,14 @@ inferPreProp preProp = case preProp of
         -> pure $ Some SInteger $ CoreProp $ ListLength ty lst
       _ -> throwErrorIn preProp "expected string or list argument to length"
 
+  PreApp s [a]
+    | s == SDistinct -> do
+        arg <- inferPreProp a
+        case arg of
+          Some (SList ty) ls -> pure $ Some (SList ty) $ CoreProp $ ListDistinct ty ls
+          _otherwise -> throwErrorIn preProp "expected list argument"
+
+
   PreApp s [a, b] | s == SModulus -> do
     it <- PNumerical ... ModOp <$> checkPreProp SInteger a <*> checkPreProp SInteger b
     pure $ Some SInteger it
diff --git a/tests/AnalyzeSpec.hs b/tests/AnalyzeSpec.hs
index 895b7a471..c44926c11 100644
--- a/tests/AnalyzeSpec.hs
+++ b/tests/AnalyzeSpec.hs
@@ -3869,6 +3869,14 @@ spec = describe "analyze" $ do
     expectVerified  $ code9 "[(property (= result [a b]))]"
     expectFalsified $ code9 "[(property (= result [a b a]))]"
 
+  describe "list distinct property" $ do
+    let code model = [text|
+          (defun test:[integer] (a:integer b:integer)
+            @model $model
+            (distinct [a b a]))
+          |]
+    expectVerified  $ code "[(property (= result (distinct [a b a])))]"
+
   describe "identity" $ do
     expectVerified [text|
           (defun test:integer ()