Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project.
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498// Standard library: Core type classes//// Provides:// - Ordering type (lt, eq, gt)// - Ord A — total ordering (uses BEq from prelude)// - Semigroup A — associative combine// - Monoid A — Semigroup with empty// - Default A — default value// - Enum A — enumerable types// - Bounded A — bounded types//// Note: BEq (boolean equality, Sort 1 / Type) is the computational// equality type class from the prelude. Eq (propositional equality,// Sort 0 / Prop) is for proofs and invariants — do NOT use Eq for// runtime comparison.type Ordering { lt, eq, gt}open Ordering {eq, gt, lt}/// Total ordering with three-way comparison.class [BEq A] Ord A { def compare : A -> A -> Ordering}/// Associative binary operation.class Semigroup A { def combine : A -> A -> A}/// Semigroup with an identity element.class [Semigroup A] Monoid A { def empty : A}/// Types with a default value.class Default A { def default : A}/// Enumerable types with successor, predecessor, and conversion to/from Nat.class Enum A { def succ : A -> A def pred : A -> A def to_nat : A -> Nat def from_nat : Nat -> A}/// Types with minimum and maximum bounds.class [Enum A] Bounded A { def min_bound : A def max_bound : A}// ---------- Instances ----------instance BEq Ordering { def beq (a b : Ordering) : Bool := match a { lt => match b { lt => true, eq => false, gt => false }, eq => match b { lt => false, eq => true, gt => false }, gt => match b { lt => false, eq => false, gt => true } }}instance Ord Ordering { def compare (a b : Ordering) : Ordering := match a { lt => match b { lt => eq, eq => lt, gt => lt }, eq => match b { lt => gt, eq => eq, gt => lt }, gt => match b { lt => gt, eq => gt, gt => eq } }}instance Semigroup String { def combine (a b : String) : String := a ++ b}instance Monoid String { def empty : String := ""}instance Default Bool { def default : Bool := false}instance Default I64 { def default : I64 := 0}instance Enum Ordering { def succ (o : Ordering) : Ordering := if BEq.beq o lt then eq else if BEq.beq o eq then gt else lt def pred (o : Ordering) : Ordering := if BEq.beq o lt then gt else if BEq.beq o eq then lt else eq def to_nat (o : Ordering) : Nat := if BEq.beq o lt then Nat.zero else if BEq.beq o eq then Nat.succ Nat.zero else Nat.succ (Nat.succ Nat.zero) def from_nat (n : Nat) : Ordering := if Nat.eq n Nat.zero then lt else if Nat.eq n (Nat.succ Nat.zero) then eq else gt}instance Bounded Ordering { def min_bound : Ordering := lt def max_bound : Ordering := gt}instance Ord I64 { def compare (a b : I64) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord Bool { def compare (a b : Bool) : Ordering := if a == b then eq else if a then gt else lt}instance Ord U8 { def compare (a b : U8) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord I8 { def compare (a b : I8) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord I16 { def compare (a b : I16) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord I32 { def compare (a b : I32) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord U16 { def compare (a b : U16) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord U32 { def compare (a b : U32) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord U64 { def compare (a b : U64) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord F32 { def compare (a b : F32) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}instance Ord F64 { def compare (a b : F64) : Ordering := if a == b then eq else if BOrd.lt a b then lt else gt}def ordering_show (o : Ordering) : String := if BEq.beq o lt then "lt" else if BEq.beq o eq then "eq" else "gt"// ---------- Tests ----------#[test]def test_beq_ordering_lt_lt : Bool := BEq.beq lt lt#[test]def test_beq_ordering_eq_eq : Bool := BEq.beq eq eq#[test]def test_beq_ordering_gt_gt : Bool := BEq.beq gt gt#[test]def test_beq_ordering_lt_eq : Bool := Bool.not (BEq.beq lt eq)#[test]def test_beq_ordering_lt_gt : Bool := Bool.not (BEq.beq lt gt)#[test]def test_beq_ordering_eq_gt : Bool := Bool.not (BEq.beq eq gt)#[test]def test_ord_lt_lt_eq : Bool := match Ord.compare lt eq { lt => true, eq => false, gt => false }#[test]def test_ord_lt_eq_gt : Bool := match Ord.compare eq gt { lt => true, eq => false, gt => false }#[test]def test_ord_lt_lt_gt : Bool := match Ord.compare lt gt { lt => true, eq => false, gt => false }#[test]def test_ord_gt_eq_lt : Bool := match Ord.compare eq lt { lt => false, eq => false, gt => true }#[test]def test_ord_gt_gt_eq : Bool := match Ord.compare gt eq { lt => false, eq => false, gt => true }#[test]def test_ord_eq_eq_eq : Bool := match Ord.compare eq eq { lt => false, eq => true, gt => false }#[test]def test_semigroup_string_concat : Bool := let result : String := Semigroup.combine "hello" "world" in result == "helloworld"#[test]def test_semigroup_string_empty_left : Bool := let result : String := Semigroup.combine "" "world" in result == "world"#[test]def test_semigroup_string_empty_right : Bool := let result : String := Semigroup.combine "hello" "" in result == "hello"#[test]def test_semigroup_string_assoc : Bool := let a : String := "a" in let b : String := "b" in let c : String := "c" in let left : String := Semigroup.combine (Semigroup.combine a b) c in let right : String := Semigroup.combine a (Semigroup.combine b c) in left == right#[test]def test_monoid_empty_string : Bool := let empty_str : String := Monoid.empty in empty_str == ""#[test]def test_default_bool : Bool := Default.default == false#[test]def test_default_i64 : Bool := Default.default == 0i64#[test]def test_default_i64_ne_not_false : Bool := Bool.not (Default.default == 1i64)#[test]def test_enum_succ : Bool := let s1 := Enum.succ lt in let s2 := Enum.succ eq in let s3 := Enum.succ gt in BEq.beq s1 eq && BEq.beq s2 gt && BEq.beq s3 lt#[test]def test_enum_pred : Bool := let p1 := Enum.pred gt in let p2 := Enum.pred lt in let p3 := Enum.pred eq in BEq.beq p1 eq && BEq.beq p2 gt && BEq.beq p3 lt#[test]def test_enum_to_nat : Bool := let n0 := Enum.to_nat lt in let n1 := Enum.to_nat eq in let n2 := Enum.to_nat gt in let zero := Nat.zero in let one := Nat.succ Nat.zero in let two := Nat.succ (Nat.succ Nat.zero) in Nat.eq n0 zero && Nat.eq n1 one && Nat.eq n2 two#[test]def test_enum_from_nat : Bool := // `Enum.from_nat : Nat -> A` has no way to infer `A` from its own // argument (`Nat`, unrelated to `A`) or default to one (`class Enum // A` declares no default, unlike e.g. `FromListLiteral`) — an // explicit annotation is required here so `expected` can pin `A := // Ordering` the same way any other call site would provide it. let f0 : Ordering := Enum.from_nat Nat.zero in let f1 : Ordering := Enum.from_nat (Nat.succ Nat.zero) in BEq.beq f0 lt && BEq.beq f1 eq#[test]def test_bounded_min : Bool := BEq.beq Bounded.min_bound lt#[test]def test_bounded_max : Bool := BEq.beq Bounded.max_bound gt#[test]def test_ord_i64_lt : Bool := match Ord.compare 1i64 5i64 { lt => true, eq => false, gt => false }#[test]def test_ord_i64_eq : Bool := match Ord.compare 42i64 42i64 { lt => false, eq => true, gt => false }#[test]def test_ord_i64_gt : Bool := match Ord.compare 10i64 3i64 { lt => false, eq => false, gt => true }#[test]def test_ord_bool_false_true : Bool := match Ord.compare false true { lt => true, eq => false, gt => false }#[test]def test_ord_bool_true_false : Bool := match Ord.compare true false { lt => false, eq => false, gt => true }#[test]def test_ord_bool_true_true : Bool := match Ord.compare true true { lt => false, eq => true, gt => false }#[test]def test_ord_u8_lt : Bool := match Ord.compare 1u8 5u8 { lt => true, eq => false, gt => false }#[test]def test_ord_u8_eq : Bool := match Ord.compare 42u8 42u8 { lt => false, eq => true, gt => false }#[test]def test_ord_u8_gt : Bool := match Ord.compare 10u8 3u8 { lt => false, eq => false, gt => true }#[test]def test_ordering_show_lt : Bool := ordering_show lt == "lt"#[test]def test_ordering_show_eq : Bool := ordering_show eq == "eq"#[test]def test_ordering_show_gt : Bool := ordering_show gt == "gt"#[test]def test_ord_i8_lt : Bool := BEq.beq (Ord.compare 0i8 5i8) lt#[test]def test_ord_i8_eq : Bool := BEq.beq (Ord.compare 5i8 5i8) eq#[test]def test_ord_i8_gt : Bool := BEq.beq (Ord.compare 5i8 0i8) gt#[test]def test_ord_u16_lt : Bool := BEq.beq (Ord.compare 0u16 5u16) lt#[test]def test_ord_u16_gt : Bool := BEq.beq (Ord.compare 5u16 0u16) gt#[test]def test_ord_f64_lt : Bool := BEq.beq (Ord.compare 0.0f64 5.0f64) lt#[test]def test_ord_f64_gt : Bool := BEq.beq (Ord.compare 5.0f64 0.0f64) gt