Skip to content
Juvix imports

module prelude;

import Stdlib.Trait open public;
import Stdlib.Trait.Ord open using {
Ordering;
module Ordering;
Equal;
isEqual;
} public;
import Stdlib.Trait.Eq open using {==} public;
import Stdlib.Debug.Fail open using {failwith};
import Stdlib.Data.Fixity open public;

Juvix Specs PreludeΒΆ

The following are frequent and basic abstractions used in the Anoma specification.

CombinatorsΒΆ

import Stdlib.Function open using {
<<;
>>;
const;
id;
flip;
<|;
|>;
iterate;
>->;
} public;

Useful Type ClassesΒΆ

FunctorΒΆ

import Stdlib.Trait.Functor.Polymorphic as Functor;

ApplicativeΒΆ

import Stdlib.Trait.Applicative as Applicative open using {Applicative} public;

import Stdlib.Trait.Applicative as Applicative open using {Applicative} public;

MonadΒΆ

import Stdlib.Trait.Monad as Monad open using {Monad} public;

import Stdlib.Trait.Monad as Monad open using {Monad} public;

joinΒΆ

Join function for monads

join {M : Type -> Type} {A} {{Monad M}} (mma : M (M A)) : M A := bind mma id;

BifunctorΒΆ

Two-argument functor

trait
type Bifunctor (F : Type -> Type -> Type) :=
mk@{
bimap {A B C D} : (A -> C) -> (B -> D) -> F A B -> F C D;
};

AssociativeProductΒΆ

Product with associators

trait
type AssociativeProduct (F : Type -> Type -> Type) :=
mk@{
assocLeft {A B C} : F A (F B C) -> F (F A B) C;
assocRight {A B C} : F (F A B) C -> F A (F B C);
};

CommutativeProductΒΆ

Product with commuters

trait
type CommutativeProduct (F : Type -> Type -> Type) :=
mk@{
swap {A B} : F A B -> F B A;
};

UnitalProductΒΆ

Product with units

trait
type UnitalProduct U (F : Type -> Type -> Type) :=
mk@{
unitLeft {A} : A -> F U A;
unUnitLeft {A} : F U A -> A;
unitRight {A} : A -> F A U;
unUnitRight {A} : F A U -> A;
};

TraversableΒΆ

import Stdlib.Trait.Traversable as Traversable open using {
Traversable;
sequenceA;
traverse;
} public;

import Stdlib.Trait.Traversable as Traversable open using {
Traversable;
sequenceA;
traverse;
} public;

BoolΒΆ

The type Bool represents boolean values (true or false). Used for logical operations and conditions.

import Stdlib.Data.Bool as Bool open using {
Bool;
true;
false;
&&;
||;
not;
or;
and;
} public;

For example,

verdad : Bool := true;

xorΒΆ

Exlusive or

xor (a b : Bool) : Bool :=
if
| a := not b
| else := b;

nandΒΆ

Not and

nand (a b : Bool) : Bool := not (and a b);

norΒΆ

Not or

nor (a b : Bool) : Bool := not (or a b);

NatΒΆ

The type Nat represents natural numbers (non-negative integers). Used for counting and indexing.

import Stdlib.Data.Nat as Nat open using {
Nat;
zero;
suc;
natToString;
+;
sub;
*;
div;
mod;
==;
<=;
>;
<;
min;
max;
} public;

For example,

ten : Nat := 10;

predΒΆ

Predecessor function for natural numbers.

pred (n : Nat) : Nat :=
case n of
| zero := zero
| suc k := k;

boolToNatΒΆ

Convert boolean to a Bool to a Nat in the standard way of circuits.

boolToNat (b : Bool) : Nat :=
if
| b := 0
| else := 1;

isZeroΒΆ

Check if a natural number is zero.

isZero (n : Nat) : Bool :=
case n of
| zero := true
| suc k := false;

isEven and isOddΒΆ

Parity checking functions

isEven (n : Nat) : Bool := mod n 2 == 0;
isOdd (n : Nat) : Bool := not (isEven n);

foldNatΒΆ

Fold over natural numbers.

terminating
foldNat {B} (z : B) (f : Nat -> B -> B) (n : Nat) : B :=
case n of
| zero := z
| suc k := f k (foldNat z f k);

iterΒΆ

Iteration of a function.

iter {A} (f : A -> A) (n : Nat) (x : A) : A := foldNat x \{_ y := f y} n;

expΒΆ

The exponentiation function.

exp (base : Nat) (exponent : Nat) : Nat :=
iter \{product := base * product} exponent 1;

factorialΒΆ

The factorial function.

factorial : Nat -> Nat := foldNat 1 \{k r := suc k * r};

gcdΒΆ

Greatest common divisor function.

terminating
gcd (a b : Nat) : Nat :=
case b of
| zero := a
| suc _ := gcd b (mod a b);

lcmΒΆ

Least common multiple function.

lcm (a b : Nat) : Nat :=
case b of
| zero := zero
| suc _ :=
case a of
| zero := zero
| suc _ := div (a * b) (gcd a b);

StringΒΆ

The type String represents sequences of characters. Used for text and communication.

import Stdlib.Data.String as String open using {String; ++str} public;

For example,

hello : String := "Hello, World!";

Comparison instance for StringΒΆ

stringCmp (s1 s2 : String) : Ordering :=
if
| s1 == s2 := Ordering.Equal
| else := Ordering.GreaterThan;

instance
StringOrd : Ord String :=
Ord.mk@{
compare := stringCmp;
};

ByteStringΒΆ

ByteString : Type := String;

A basic type for representing binary data.

emptyByteString : ByteString := "";

UnitΒΆ

The type Unit represents a type with a single value. Often used when a function does not return any meaningful value.

import Stdlib.Data.Unit as Unit open using {Unit; unit} public;

For example,

unitValue : Unit := unit;

trivialΒΆ

Unique function to the unit. Universal property of terminal object.

trivial {A} : A -> Unit := const unit;

EmptyΒΆ

The type Empty represents a type with a single value. Often used when a function does not return any meaningful value.

axiom Empty : Type;

explodeΒΆ

Unique function from empty. Universal property of initial object.

axiom explode {A} : Empty -> A;

Pair A BΒΆ

The type Pair A B represents a tuple containing two elements of types A and B. Useful for grouping related values together.

import Stdlib.Data.Pair as Pair;

open Pair using {Pair} public;

open Pair using {,};

import Stdlib.Data.Pair as Pair open using {ordProductI; eqProductI} public;
import Stdlib.Data.Fixity open;

syntax alias mkPair := ,;

For example,

pair : Pair Nat Bool := mkPair 42 true;

fst and sndΒΆ

Projections

fst {A B} : Pair A B -> A
| (mkPair a _) := a;
snd {A B} : Pair A B -> B
| (mkPair _ b) := b;

PairCommutativeProductΒΆ

Swap components

instance
PairCommutativeProduct : CommutativeProduct Pair :=
CommutativeProduct.mk@{
swap := \{p := mkPair (snd p) (fst p)};
};

PairAssociativeProductΒΆ

Pair associations

instance
PairAssociativeProduct : AssociativeProduct Pair :=
AssociativeProduct.mk@{
assocLeft :=
\{p :=
let
pbc := snd p;
in mkPair (mkPair (fst p) (fst pbc)) (snd pbc)};
assocRight :=
\{p :=
let
pab := fst p;
in mkPair (fst pab) (mkPair (snd pab) (snd p))};
};

PairUnitalProductΒΆ

Unit maps for pairs and units

instance
PairUnitalProduct : UnitalProduct Unit Pair :=
UnitalProduct.mk@{
unitLeft := \{a := mkPair unit a};
unUnitLeft := snd;
unitRight := \{a := mkPair a unit};
unUnitRight := \{{A} := fst};
};

PairBifunctorΒΆ

Map functions over pairs

instance
PairBifunctor : Bifunctor Pair :=
Bifunctor.mk@{
bimap := \{f g p := mkPair (f (fst p)) (g (snd p))};
};

forkΒΆ

Universal property of pairs

fork {A B C} (f : C -> A) (g : C -> B) (c : C) : Pair A B := mkPair (f c) (g c);

Result A BΒΆ

The Result A B type represents either a success with a value of ok x with x of type A or an error with value error e with e of type B.

import Stdlib.Data.Result.Base as Result;

open Result using {Result; ok; error} public;

Either A BΒΆ

The type Either A B, or sum type of A and B, represents a value of type A or B. It is equivalent to Result A B, however, the meaning of the values is different. There is no such thing as an error or success value in the Either type, instead the values are either left a of type A or right b of type B.

syntax alias Either := Result;

syntax alias left := error;

syntax alias right := ok;

For example,

thisString : Either String Nat := left "Error!";

thisNumber : Either String Nat := right 42;

isLeft and isRightΒΆ

Check components of either.

isLeft {A B} (e : Either A B) : Bool :=
case e of
| left _ := true
| right _ := false;
isRight {A B} (e : Either A B) : Bool :=
case e of
| left _ := false
| right _ := true;

fromLeftΒΆ

Get left element (with default)

fromLeft {A B} (e : Either A B) (d : A) : A :=
case e of
| left x := x
| right _ := d;

fromRightΒΆ

Get right element (with default)

fromRight {A B} (e : Either A B) (d : B) : B :=
case e of
| left _ := d
| right x := x;

EitherCommutativeProductΒΆ

Swap elements

swapEither {A B} (e : Either A B) : Either B A :=
case e of
| left x := right x
| right x := left x;
instance
EitherCommutativeProduct : CommutativeProduct Either :=
CommutativeProduct.mk@{
swap := swapEither;
};

EitherBifunctorΒΆ

Map onto elements of either

eitherBimap {A B C D} (f : A -> C) (g : B -> D) (e : Either A B) : Either C D :=
case e of
| left a := left (f a)
| right b := right (g b);
instance
EitherBifunctor : Bifunctor Either :=
  Bifunctor.mk@{
    bimap := eitherBimap
  };

EitherUnitalProductΒΆ

Unit maps for Either and Empty

unUnitLeftEitherΒΆ

unUnitLeftEither {A} (e : Either Empty A) : A :=
case e of
| left x := explode x
| right x := x;

unUnitRightEitherΒΆ

unUnitRightEither {A} (e : Either A Empty) : A :=
case e of
| left x := x
| right x := explode x;

EitherUnitalProductΒΆ

Unit maps for Either and Empty

instance
EitherUnitalProduct : UnitalProduct Empty Either :=
  UnitalProduct.mk@{
    unitLeft := right;
    unUnitLeft := unUnitLeftEither;
    unitRight := \{{A} := left};
    unUnitRight := unUnitRightEither;
  };

fuseΒΆ

Universal property of coproduct

fuse {A B C} (f : A -> C) (g : B -> C) (e : Either A B) : C :=
case e of
| left x := f x
| right x := g x;

EitherAssociativeProductΒΆ

Association functions for either

assocLeftEitherΒΆ

assocLeftEither {A B C} (e : Either A (Either B C)) : Either (Either A B) C :=
case e of
| left x := left (left x)
| right ebc :=
case ebc of
| left y := left (right y)
| right z := right z;

assocRightEitherΒΆ

assocRightEither {A B C} (e : Either (Either A B) C) : Either A (Either B C) :=
case e of
| left eab :=
case eab of {
| left x := left x
| right y := right (left y)
}
| right z := right (right z);

EitherAssociativeProductΒΆ

instance
EitherAssociativeProduct : AssociativeProduct Either :=
  AssociativeProduct.mk@{
    assocLeft := assocLeftEither;
    assocRight := assocRightEither;
  };

Option AΒΆ

The type Option A represents an optional value of type A. It can be either Some A (containing a value) or None (no value). This type is an alias for Maybe A from the standard library.

import Stdlib.Data.Maybe as Maybe;

open Maybe using {Maybe; just; nothing};
syntax alias Option := Maybe;

syntax alias some := just;

syntax alias none := nothing;

isNoneΒΆ

Check if an optional value is none:

isNone {A} (x : Option A) : Bool :=
case x of
| none := true
| some _ := false;

isSomeΒΆ

Check if an optional value is some:

isSome {A} (x : Option A) : Bool := not (isNone x);

fromOptionΒΆ

Extract the value from an Option term:

fromOption {A} (x : Option A) (default : A) : A :=
case x of
| none := default
| some x := x;

optionΒΆ

Map over option with default

option {A B} (o : Option A) (default : B) (f : A -> B) : B :=
case o of
| none := default
| some x := f x;

filterOptionΒΆ

Filter option according to predicate

filterOption {A} (p : A -> Bool) (opt : Option A) : Option A :=
case opt of
| none := none
| some x :=
if
| p x := some x
| else := none;

List AΒΆ

The type List A represents a sequence of elements of type A. Used for collections and ordered data.

import Stdlib.Data.List as List open using {
List;
nil;
::;
isElement;
head;
tail;
length;
take;
drop;
++;
reverse;
any;
all;
zip;
} public;

For example,

numbers : List Nat := 1 :: 2 :: 3 :: nil;

niceNumbers : List Nat := [1; 2; 3];

findIndexΒΆ

Get the first index of an element satisfying a predicate if such an index exists and none, otherwise.

findIndex {A} (predicate : A -> Bool) : List A -> Option Nat
| nil := none
| (x :: xs) :=
if
| predicate x := some zero
| else :=
case findIndex predicate xs of
| none := none
| some i := some (suc i);

lastΒΆ

Get last element of a list

last {A} (lst : List A) (default : A) : A := head default (reverse lst);

mostΒΆ

Get list with last element dropped

most {A} (lst : List A) : List A := tail (reverse lst);

snocΒΆ

Prepend element to a list

snoc {A} (xs : List A) (x : A) : List A := xs ++ [x];

unconsΒΆ

Split one layer of list

uncons {A} : List A -> Option (Pair A (List A))
| nil := none
| (x :: xs) := some (mkPair x xs);

unsnocΒΆ

Split one layer of list from the end

unsnoc {A} : List A -> Option (Pair (List A) A)
| nil := none
| (x :: xs) := some (mkPair (most (x :: xs)) (last xs x));

unfoldΒΆ

Unfold a list, layerwise

terminating
unfold {A B} (step : B -> Option (Pair A B)) (seed : B) : List A :=
case step seed of
| none := nil
| some (x, seed') := x :: unfold step seed';

unzipΒΆ

Unzip a list of pairs into two lists

terminating
unzip {A B} (xs : List (Pair A B)) : Pair (List A) (List B) :=
case xs of
| nil := mkPair nil nil
| p :: ps :=
let
unzipped := unzip ps;
in mkPair (fst p :: fst unzipped) (snd p :: snd unzipped);

partitionEitherΒΆ

Partition a list

partitionEither {A B} (es : List (Either A B)) : Pair (List A) (List B) :=
foldr
\{e acc :=
case e of
| left a := mkPair (a :: fst acc) (snd acc)
| right b := mkPair (fst acc) (b :: snd acc)}
(mkPair nil nil)
es;

partitionEitherWithΒΆ

partitionEitherWith
{A B C} (f : C -> Either A B) (es : List C) : Pair (List A) (List B) :=
partitionEither (map f es);

catOptionsΒΆ

Collapse list of options

catOptions {A} : List (Option A) -> List A :=
foldr
\{opt acc :=
case opt of
| none := acc
| some x := x :: acc}
nil;

maximumByΒΆ

Get the maximal element of a list.

maximumBy {A B} {{Ord B}} (f : A -> B) (lst : List A) : Option A :=
let
maxHelper :=
\{curr acc :=
case acc of
| none := some curr
| some maxVal :=
if
| f curr > f maxVal := some curr
| else := some maxVal};
in foldr maxHelper none lst;

minimumByΒΆ

Get the minimal element of a list.

minimalBy {A B} {{Ord B}} (f : A -> B) (lst : List A) : Option A :=
let
minHelper :=
\{curr acc :=
case acc of
| none := some curr
| some minVal :=
if
| f curr < f minVal := some curr
| else := some minVal};
in foldr minHelper none lst;

chunksOfΒΆ

Splits a list into chunks of size n. The last chunk may be smaller than n if the length of the list is not divisible by n.

Example:

  • chunksOf 2 [1;2;3;4;5] = [[1;2]; [3;4]; [5]]
terminating
chunksOf {A} : (chunkSize : Nat) -> (list : List A) -> List (List A)
| zero _ := nil
| _ nil := nil
| n xs := take n xs :: chunksOf n (drop n xs);

slidingΒΆ

Returns all contiguous sublists of size n. If n is larger than the list length, returns empty list. If n is zero, returns empty list.

Example: - sliding 2 [1;2;3;4] = [[1;2]; [2;3]; [3;4]]

sliding {A} : (windowSize : Nat) -> (list : List A) -> List (List A)
| zero _ := nil
| n xs :=
let
len : Nat := length xs;
terminating
go : List A -> List (List A)
| nil := nil
| ys :=
if
| length ys < n := nil
| else := take n ys :: go (tail ys);
in if
| n > len := nil
| else := go xs;

spanΒΆ

Takes a predicate and a list, and returns a tuple where:

  • First element is the longest prefix of the list that satisfies the predicate
  • Second element is the remainder of the list
span {A} (p : A -> Bool) : List A -> Pair (List A) (List A)
| nil := mkPair nil nil
| (x :: xs) :=
if
| p x :=
let
(ys1, ys2) := span p xs;
in mkPair (x :: ys1) ys2
| else := mkPair nil (x :: xs);

groupBy and groupΒΆ

Groups consecutive elements in a list that satisfy a given equality predicate.

Example:

  • groupBy (==) [1;1;2;2;2;3;1;1] = [[1;1];[2;2;2];[3];[1;1]]
terminating
groupBy {A} (eq : A -> A -> Bool) : List A -> List (List A)
| nil := nil
| (x :: xs) := case span (eq x) xs of ys1, ys2 := (x :: ys1) :: groupBy eq ys2;
group {A} {{Eq A}} : List A -> List (List A) := groupBy (==);

nubByΒΆ

Returns a list with duplicates removed according to the given equivalence function, keeping the first occurrence of each element. Unlike regular ;nub;, this function allows specifying a custom equality predicate.

Examples:

  • nubBy ({x y := mod x 3 == mod y 3}) [1;2;3;4;5;6] = [1;2;3]
  • nub [1;1;2;2;3;3] = [1;2;3]
nubBy {A} (eq : A -> A -> Bool) : List A -> List A :=
let
elemBy (x : A) : List A -> Bool
| nil := false
| (y :: ys) := eq x y || elemBy x ys;
go : List A -> List A -> List A
| acc nil := reverse acc
| acc (x :: xs) :=
if
| elemBy x acc := go acc xs
| else := go (x :: acc) xs;
in go nil;

nubΒΆ

nub {A} {{Eq A}} : List A -> List A := nubBy (==);

powerlistsΒΆ

Generate all possible sublists of a list. Each element can either be included or not.

powerlists {A} : List A -> List (List A)
| nil := nil :: nil
| (x :: xs) :=
let
rest : List (List A) := powerlists xs;
withX : List (List A) := map ((::) x) rest;
in rest ++ withX;

Set AΒΆ

The type Set A represents a collection of unique elements of type A. Used for sets of values.

import Stdlib.Data.Set as Set open using {
Set;
module Set;
difference;
union;
insert;
eqSetI;
ordSetI;
isSubset;
} public;

For example,

uniqueNumbers : Set Nat := Set.fromList [1; 2; 2; 2; 3];

setMapΒΆ

setMap {A B} {{Ord B}} (f : A -> B) (set : Set A) : Set B :=
Set.fromList (map f (Set.toList set));

setJoinΒΆ

Collapse a set of sets into a set

setJoin {A} {{Ord A}} (sets : Set (Set A)) : Set A :=
for (acc := Set.empty) (innerSet in sets) {
Set.union acc innerSet
};

disjointUnionΒΆ

--- Computes the disjoint union of two ;Set;s.
disjointUnion {T} {{Ord T}} (s1 s2 : Set T) : Result (Set T) (Set T) :=
case Set.intersection s1 s2 of
| Set.empty := ok (Set.union s1 s2)
| s := error s;

symmetricDifferenceΒΆ

Caclulate the symmetric difference of two sets.

symmetricDifference {A} {{Ord A}} (s1 s2 : Set A) : Set A :=
let
in1not2 := difference s1 s2;
in2not1 := difference s2 s1;
in union in1not2 in2not1;

cartesianProductΒΆ

Generate the set of all cartesian products of a set.

cartesianProduct
{A B} {{Ord A}} {{Ord B}} (s1 : Set A) (s2 : Set B) : Set (Pair A B) :=
let
pairsForElement (a : A) : Set (Pair A B) :=
for (acc := Set.empty) (b in s2) {
insert (mkPair a b) acc
};
pairSets : Set (Set (Pair A B)) :=
for (acc := Set.empty) (a in s1) {
insert (pairsForElement a) acc
};
in setJoin pairSets;

powersetΒΆ

Generate the powerset (set of all subsets) of a set.

powerset {A} {{Ord A}} (s : Set A) : Set (Set A) :=
let
elements := Set.toList s;
subLists := powerlists elements;
in Set.fromList (map Set.fromList subLists);

isProperSubsetΒΆ

Checks if all elements of set1 are in set2, and that the two sets are not the same.

isProperSubset {A} {{Eq A}} {{Ord A}} (set1 set2 : Set A) : Bool :=
isSubset set1 set2 && not (set1 == set2);

Map K VΒΆ

The type Map K V represents a collection of key-value pairs, sometimes called a dictionary, where keys are of type K and values are of type V.

import Stdlib.Data.Map as Map public;

open Map using {Map} public;

For example,

codeToken : Map Nat String := Map.fromList [1, "BTC"; 2, "ETH"; 3, "ANM"];

updateLookupWithKeyΒΆ

Updates a value at a specific key using the update function and returns both the old value (if the key existed) and the updated map.

updateLookupWithKey
{Key Value}
{{Ord Key}}
(updateFn : Key -> Value -> Option Value)
(k : Key)
(map : Map Key Value)
: Pair (Option Value) (Map Key Value) :=
let
oldValue : Option Value := Map.lookup k map;
newMap : Map Key Value :=
case oldValue of
| none := map
| some v :=
case updateFn k v of
| none := Map.delete k map
| some newV := Map.insert k newV map;
in oldValue, newMap;

mapKeysΒΆ

Maps all keys in the Map to new keys using the provided function. If the mapping function is not injective (maps different keys to the same key), later entries in the map will overwrite earlier ones with the same new key.

mapKeys
{Key1 Key2 Value}
{{Ord Key2}}
(fun : Key1 -> Key2)
(map : Map Key1 Value)
: Map Key2 Value :=
Map.fromList
(for (acc := nil) (k, v in Map.toList map) {
(fun k, v) :: acc
});

restrictKeysΒΆ

Restrict a map to only contain keys from the given set.

restrictKeys
{Key Value}
{{Ord Key}}
(map : Map Key Value)
(validKeys : Set.Set Key)
: Map Key Value :=
for (acc := Map.empty) (k, v in map) {
if
| Set.isMember k validKeys := Map.insert k v acc
| else := acc
};

withoutKeysΒΆ

Remove all entries from a map whose keys appear in the given set.

withoutKeys
{Key Value}
{{Ord Key}}
(map : Map Key Value)
(invalidKeys : Set.Set Key)
: Map Key Value :=
for (acc := Map.empty) (k, v in map) {
if
| Set.isMember k invalidKeys := acc
| else := Map.insert k v acc
};

mapPartitionΒΆ

Split a map according to a predicate on values. Returns a pair of maps, (matching, non-matching).

mapPartition
{Key Value}
{{Ord Key}}
(predicate : Value -> Bool)
(map : Map Key Value)
: Pair (Map Key Value) (Map Key Value) :=
for (matching, nonMatching := Map.empty, Map.empty) (k, v in map) {
if
| predicate v := Map.insert k v matching, nonMatching
| else := matching, Map.insert k v nonMatching
};

partitionWithKeyΒΆ

Split a map according to a predicate that can examine both key and value. Returns a pair of maps, (matching, non-matching).

partitionWithKey
{Key Value}
{{Ord Key}}
(predicate : Key -> Value -> Bool)
(map : Map Key Value)
: Pair (Map Key Value) (Map Key Value) :=
for (matching, nonMatching := Map.empty, Map.empty) (k, v in map) {
if
| predicate k v := Map.insert k v matching, nonMatching
| else := matching, Map.insert k v nonMatching
};

mapOptionΒΆ

Apply a partial function to all values in the map, keeping only the entries where the function returns 'some'.

mapOption
{Key Value1 Value2}
{{Ord Key}}
(f : Value1 -> Option Value2)
(map : Map Key Value1)
: Map Key Value2 :=
for (acc := Map.empty) (k, v in map) {
case f v of
| none := acc
| some v' := Map.insert k v' acc
};

mapOptionWithKeyΒΆ

Same as mapOption but allows the function to examine the key as well.

mapOptionWithKey
{Key Value1 Value2}
{{Ord Key}}
(f : Key -> Value1 -> Option Value2)
(map : Map Key Value1)
: Map Key Value2 :=
for (acc := Map.empty) (k, v in map) {
case f k v of
| none := acc
| some v' := Map.insert k v' acc
};

mapEitherΒΆ

Apply a function that returns Either to all values in the map.

mapEither
{Key Value Error Result}
{{Ord Key}}
(f : Value -> Either Error Result)
(map : Map Key Value)
: Pair (Map Key Error) (Map Key Result) :=
for (lefts, rights := Map.empty, Map.empty) (k, v in map) {
case f v of
| error e := Map.insert k e lefts, rights
| ok r := lefts, Map.insert k r rights
};

mapEitherWithKeyΒΆ

Same as mapEither but allows the function to examine the key as well.

mapEitherWithKey
{Key Value Error Result}
{{Ord Key}}
(f : Key -> Value -> Either Error Result)
(map : Map Key Value)
: Pair (Map Key Error) (Map Key Result) :=
for (lefts, rights := Map.empty, Map.empty) (k, v in map) {
case f k v of
| error e := Map.insert k e lefts, rights
| ok r := lefts, Map.insert k r rights
};

Undefined valuesΒΆ

The term undef is a placeholder for unspecified values.

undefΒΆ

axiom undef {A} : A;

TODOΒΆ

axiom TODO {A} : A;

OMap K VΒΆ

A simple map implementation represented as a function from keys to optional values. Note: Unlike Stdlib.Data.Map, this implementation does not require an Ord instance for the key type K. However, operations like insert, delete, and fromList require an Eq instance instead of an Ord instance.

Meant for usage with String which does not have a working Ord instance but does have a working Eq instance.

module OMap;
type OMap K V :=
mk@{
omap : K -> Option V;
};

empty
{K V} : OMap K V := OMap.mk \{_ := none};

lookup
{K V} (k : K) (m : OMap K V) : Option V := OMap.omap m k;

insert
{K V} {{Eq K}} (k : K) (v : V) (m : OMap K V) : OMap K V :=
OMap.mk@{
omap :=
\{k' :=
if
| k == k' := some v
| else := OMap.omap m k'};
};

delete
{K V} {{Eq K}} (k : K) (m : OMap K V) : OMap K V :=
OMap.mk@{
omap :=
\{k' :=
if
| k == k' := none
| else := OMap.omap m k'};
};

fromList
{K V} {{Eq K}} (pairs : List (Pair K V)) : OMap K V :=
foldl \{m (k, v) := insert k v m} empty pairs;

map
{K V1 V2} (f : V1 -> V2) (m : OMap K V1) : OMap K V2 :=
OMap.mk@{
omap := \{k := Functor.map f (OMap.omap m k)};
};

mapOption
{K V1 V2} (f : V1 -> Option V2) (m : OMap K V1) : OMap K V2 :=
OMap.mk@{
omap :=
\{k :=
case OMap.omap m k of
| none := none
| some v1 := f v1};
};

mapOptionWithKey

{K V1 V2} (f : K -> V1 -> Option V2) (m : OMap K V1) : OMap K V2 :=
OMap.mk@{
omap :=
\{k :=
case OMap.omap m k of
| none := none
| some v1 := f k v1};
};

foldWithKeys

{K V Acc}
(f : K -> V -> Acc -> Acc)
(init : Acc)
(keys : List K)
(m : OMap K V)
: Acc :=
foldl
\{acc k :=
case OMap.omap m k of
| none := acc
| some v := f k v acc}
init
keys;

singleton
{K V} {{Eq K}} (k : K) (v : V) : OMap K V :=
OMap.mk@{
omap :=
\{k' :=
if
| k == k' := some v
| else := none};
};
end;