Add Encoded

Anoma.juvix

@@ -7,5 +7,4 @@ import Anoma.Delta as Delta public;
 import Anoma.Delta open using {Delta} public;
 import Anoma.Random open public;
 import Anoma.Utils as Utils public;
-
-import Anoma.Builtin.System open using {anomaEncode; anomaDecode} public;
+import Anoma.Encode open public;

Anoma/Builtin/System.juvix

@@ -13,7 +13,7 @@ end;
 
 --- Encodes a value into a natural number.
 builtin anoma-encode
-axiom anomaEncode
+axiom builtinAnomaEncode
   : {Value : Type}
     -- | The value to encode.
     -> Value
@@ -22,7 +22,7 @@ axiom anomaEncode
 
 --- Decodes a value from a natural number.
 builtin anoma-decode
-axiom anomaDecode
+axiom builtinAnomaDecode
   : {Value : Type}
     -- | The natural number to decode.
     -> Nat

Anoma/Encode.juvix

@@ -0,0 +1,20 @@
+module Anoma.Encode;
+
+import Stdlib.Prelude open;
+import Anoma.Builtin.System open;
+
+module Encode;
+  module Internal;
+    type Encoded A := mkEncoded Nat;
+  end;
+
+  open Internal using {Encoded} public;
+
+  decode {A} : (encoded : Encoded A) -> A
+    | (Internal.mkEncoded n) := builtinAnomaDecode n;
+
+  encode {A} (obj : A) : Encoded A :=
+    Internal.mkEncoded (builtinAnomaEncode obj);
+end;
+
+open Encode using {Encoded; decode; encode} public;

Anoma/Resource/Types.juvix

@@ -12,7 +12,7 @@ open B using {Kind} public;
 instance
 KindEq : Eq Kind :=
   mkEq@{
-    eq (a b : Kind) : Bool := anomaEncode a == anomaEncode b;
+    eq (a b : Kind) : Bool := builtinAnomaEncode a == builtinAnomaEncode b;
   };
 
 --- A fixed-size data type encoding the public commitment to the private nullifier key.

Applib/Data/AnomaMap.juvix

@@ -2,9 +2,8 @@ module Applib.Data.AnomaMap;
 
 import Stdlib.Prelude open;
 import Stdlib.Data.Map as Map open using {Map};
-import Anoma.Builtin.System open using {anomaEncode; anomaDecode};
-
--- TODO add size
+import Anoma.Builtin.System open using {builtinAnomaEncode; builtinAnomaDecode};
+import Anoma.Encode open;
 
 module Private;
   type AnomaMap := mkAnoma (Map Nat Nat);
@@ -14,10 +13,17 @@ open Private using {AnomaMap} public;
 
 empty : AnomaMap := Private.mkAnoma Map.empty;
 
-lookup {Key Value : Type} : Key -> AnomaMap -> Maybe Value
+size : AnomaMap -> Nat
+  | (Private.mkAnoma m) := Map.size m;
+
+lookup {Key Value : Type} : Key -> AnomaMap -> Maybe (Encoded Value)
   | key (Private.mkAnoma a) :=
-    Map.lookup (anomaEncode key) a |> map anomaDecode;
+    Map.lookup (builtinAnomaEncode key) a |> map Encode.Internal.mkEncoded;
+
+lookupDecode {Key Value : Type} (k : Key) (m : AnomaMap) : Maybe Value :=
+  map decode (lookup k m);
 
 insert {Key Value : Type} : Key -> Value -> AnomaMap -> AnomaMap
   | k v (Private.mkAnoma a) :=
-    Private.mkAnoma (Map.insert (anomaEncode k) (anomaEncode v) a);
+    Private.mkAnoma
+      (Map.insert (builtinAnomaEncode k) (builtinAnomaEncode v) a);