diff --git a/Anoma/Base.juvix b/Anoma/Base.juvix index 4b09628..e9621ac 100644 --- a/Anoma/Base.juvix +++ b/Anoma/Base.juvix @@ -26,6 +26,8 @@ import Stdlib.Prelude open; --- A module containing types that are currently unknown or require furhter discussion. -- SPEC_QUESTION / INST_QUESTION: What should these types be? +import Anoma.Base.Set as Set open using {Set} public; + module Unknown; -- This is currently equal to the function type in RM instantiation. axiom ResourceLogicFieldType : Type; @@ -78,10 +80,6 @@ module Opaque; --- The zero value of `Opaque.Delta`. -- This is not in the specification but is used to initialize delta fields. axiom zeroDelta : Delta; - - -- TODO: Other Set functions will be required. - -- See https://github.com/anoma/nspec/issues/197 - axiom Set : Type -> Type; end; -- Add opaque types to the scope for convenience. diff --git a/Anoma/Base/Set.juvix b/Anoma/Base/Set.juvix new file mode 100644 index 0000000..1c91231 --- /dev/null +++ b/Anoma/Base/Set.juvix @@ -0,0 +1,147 @@ +{-- This module contains the Set API to be used when interacting with Anoma. + +It is recommended that you import this module as follows: + +import Anoma.Base.Set as Set open using {Set} + +or + +import Anoma.Base.Set as AnomaSet open using {Set as AnomaSet} + +if you use this module and the standard library set from Stdlib.Data.Set in the +same module. --} +module Anoma.Base.Set; + +import Stdlib.Prelude open hiding {foldl; all; any; isMember; for}; +import Stdlib.Data.Set as StdlibSet open using {Set as StdlibSet}; + +--- A module containing the builtin Anoma Set API. +module Internal; + + axiom Set : Type -> Type; + + axiom lookup : {A : Type} -> (elem : A) -> (set : Set A) -> Maybe A; + + axiom isMember : {A : Type} -> (elem : A) -> (set : Set A) -> Bool; + + axiom insert : {A : Type} -> (elem : A) -> (set : Set A) -> Set A; + + axiom toList : {A : Type} -> (set : Set A) -> List A; + + axiom fromList : {A : Type} -> (list : List A) -> Set A; + + axiom size : {A : Type} -> (set : Set A) -> Nat; + + axiom delete : {A : Type} -> (elem : A) -> (set : Set A) -> Set A; + + axiom map : {A B : Type} -> (fun : A -> B) -> (set : Set A) -> Set B; + + --- Implemented using `++rep:in` https://developers.urbit.org/reference/hoon/stdlib/2h#repin + -- NB: The initial accumulator should be the second default argument of the function. + axiom foldl : {A B : Type} -> (fun : B -> A -> B) -> (acc : B) -> Set A -> B; + + axiom union : {A : Type} -> (set1 set2 : Set A) -> Set A; + + axiom intersection : {A : Type} -> (set1 set2 : Set A) -> Set A; + + axiom difference : {A : Type} -> (set1 set2 : Set A) -> Set A; + + axiom all : {A : Type} -> (predicate : A -> Bool) -> (set : Set A) -> Bool; + + axiom any : {A : Type} -> (predicate : A -> Bool) -> (set : Set A) -> Bool; +end; + +open Internal using {Set} public; + +{-# inline: true #-} +singleton {A} (elem : A) : Set A := Internal.fromList {A} [elem]; + +{-# inline: true #-} +empty {A} : Set A := Internal.fromList {A} []; + +{-# inline: true #-} +lookup {A} (elem : A) (set : Set A) : Maybe A := Internal.lookup {A} elem set; + +{-# inline: true #-} +isMember {A} (elem : A) (set : Set A) : Bool := Internal.isMember {A} elem set; + +{-# inline: true #-} +insert {A} (elem : A) (set : Set A) : Set A := Internal.insert {A} elem set; + +{-# inline: true #-} +toList {A} (set : Set A) : List A := Internal.toList {A} set; + +{-# inline: true #-} +fromList {A} (list : List A) : Set A := Internal.fromList {A} list; + +fromStdlibSet {A} (set : StdlibSet A) : Set A := + set |> StdlibSet.toList |> fromList; + +toStdlibSet {A} {{Ord A}} (set : Set A) : StdlibSet A := + set |> toList |> StdlibSet.fromList; + +{-# inline: true #-} +size {A} (set : Set A) : Nat := Internal.size {A} set; + +{-# inline: true #-} +delete {A} (elem : A) (set : Set A) : Set A := Internal.delete elem set; + +{-# inline: true #-} +union {A} (set1 set2 : Set A) : Set A := Internal.union {A} set1 set2; + +{-# inline: true #-} +intersection {A} (set1 set2 : Set A) : Set A := Internal.intersection set1 set2; + +{-# inline: true #-} +difference {A} (set1 set2 : Set A) : Set A := Internal.difference set1 set2; + +{-# inline: true #-} +isEmpty {A} (set : Set A) : Bool := size set == 0; + +syntax iterator map {init := 0; range := 1}; +{-# inline: true #-} +map {A B} (fun : A -> B) (set : Set A) : Set B := Internal.map {A} {B} fun set; + +{-# inline: true #-} +foldl {A B} (fun : B -> A -> B) (acc : B) (set : Set A) : B := + Internal.foldl {A} {B} fun acc set; + +-- The hoon stdlib does not define foldr so we cannot implement Foldable. +syntax iterator for {init := 1; range := 1}; +{-# inline: true #-} +for : {A B : Type} -> (B -> A -> B) -> B -> Set A -> B := foldl; + +syntax iterator all {init := 0; range := 1}; +{-# inline: true #-} +all {A} (predicate : A -> Bool) (set : Set A) : Bool := + Internal.all {A} predicate set; + +syntax iterator any {init := 0; range := 1}; +{-# inline: true #-} +any {A} (predicate : A -> Bool) (set : Set A) : Bool := + Internal.any {A} predicate set; + +isSubset {A} (set1 set2 : Set A) : Bool := + all (x in set1) { + isMember x set2 + }; + +syntax iterator filter {init := 0; range := 1}; +{-# specialize: [1] #-} +filter {A} (predicate : A -> Bool) (set : Set A) : Set A := + for (acc := empty) (x in set) { + if + | predicate x := insert x acc + | else := acc + }; + +{-# specialize: [1] #-} +disjointUnion {A} (set1 set2 : Set A) : Result A (Set A) := + for (acc := ok set2) (x in set1) { + case acc of + | error _ := acc + | ok set := + if + | isMember x set2 := error x + | else := ok (insert x set) + };