remove fv distinct shim

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

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)

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)

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)

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 ->

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 ->

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 ()