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;