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