diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..496ee2c --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.DS_Store \ No newline at end of file diff --git a/src/.DS_Store b/src/.DS_Store new file mode 100644 index 0000000..5008ddf Binary files /dev/null and b/src/.DS_Store differ diff --git a/src/And.fm b/src/And.fm new file mode 100644 index 0000000..70232de --- /dev/null +++ b/src/And.fm @@ -0,0 +1,14 @@ +// logical conjunction +And(A:Type,B:Type): Type + Pair(A,B) + +// simplification +And.fst(x: And(A,B)) : A + Pair.fst(x) + +And.new(x: A,y:B) : And(A,B) + Pair.new(x,y) + +And.snd(x: And(A,B)) : B + Pair.snd(x) + diff --git a/src/Array.fm b/src/Array.fm new file mode 100644 index 0000000..7673df9 --- /dev/null +++ b/src/Array.fm @@ -0,0 +1,71 @@ +// Array(A, depth) is a container with 2^depth values of type A. +type Array ~ (depth: Nat) { + tip(value: A) ~ (depth: Nat.zero), + tie(lft: Array(A,depth), rgt: Array(A,depth)) ~ (depth: Nat.succ(depth)) +} + +// Creates an array of depth `depth` and initial value `x`. +Array.alloc(depth: Nat, x: A): Array(A, depth) + case depth { + zero: Array.tip(x), + succ: + let half = Array.alloc(depth.pred, x) + Array.tie(half, half) + } : Array(A, depth) + +// Extracts the two subarrays of an array of depth greater than 0. +Array.extract_tie(arr: Array(A,Nat.succ(depth))): Pair(Array(A,depth), Array(A,depth)) + case arr { + tip: Unit.new, + tie: Pair.new<_,_>(arr.lft, arr.rgt) + } : case arr.depth { + zero: Unit, + succ: Pair(Array(A,arr.depth.pred), Array(A,arr.depth.pred)) + } + +// Extracts the unique value of an array of depth 0. +Array.extract_tip(arr: Array(A,0)): A + case arr { + tip: arr.value, + tie: Unit.new + } : case arr.depth { + zero: A, + succ: Unit + } + +// Given array `arr` and little-endian word `idx`, extracts value `arr[idx]`. +// TODO: infinity loop +// Array.get(idx: Word(depth), arr: Array(A,depth)): A +// def P = (depth) Array(A,depth) -> A +// def nil = Array.extract_tip +// def w0 = (rec) (arr) +// // get arr_l _ = Array.extract_tie(arr) +// let arr_l = Array.extract_tie(arr) +// case arr_l{ +// new: arr_l.fst +// } +// def w1 = (rec) (arr) +// // get _ arr_r = Array.extract_tie(arr) +// let arr_r = Array.extract_tie(arr) +// case arr_r{ +// new: rec(arr_r.snd) +// } +// Word.foldl(nil, w0, w1, idx, arr) + +// // Given array `arr`, little-endian word `idx` and function `f`, assigns `arr[idx] = f(arr[idx])`. +// Array.mut(idx: Word(depth), f: A -> A, arr: Array(A,depth)): Array(A,depth) +// def P = (depth) Array(A,depth) -> Array(A,depth) +// def nil = (arr) Array.tip(f(Array.extract_tip(arr))) +// def w0 = (rec) (arr) +// let {arr_l, arr_r} = Array.extract_tie(arr) +// Array.tie(rec(arr_l), arr_r) +// def w1 = (rec) (arr) +// let {arr_l, arr_r} = Array.extract_tie(arr) +// Array.tie(arr_l, rec(arr_r)) +// Word.foldl(nil, w0, w1, idx, arr) + +// // Given array `arr`, little-endian word `idx` and value `val`, assigns `arr[idx] = val`. +// Array.set(idx: Word(depth), val: A, arr: Array(A,depth)) +// : Array(A,depth) +// Array.mut(idx, () val, arr) + diff --git a/src/Bits.fm b/src/Bits.fm index 1a6cb31..c82c3ea 100644 --- a/src/Bits.fm +++ b/src/Bits.fm @@ -114,3 +114,72 @@ Bits.to_nat(b: Bits): Nat i: Nat.succ(Nat.mul(2, Bits.to_nat(b.pred))) } +Bits.from_string(str: String): Bits + case str{ + nil: Bits.e + cons: case U16.eql(str.head, Char.parse("1")){ + true : Bits.i(Bits.from_string(str.tail)) + false: Bits.o(Bits.from_string(str.tail)) + // TODO: what is this from past code? + //| Unit.new + } + } + +Bits.length(xs: Bits): Nat + Bits.length.go(xs, 0) + +Bits.length.go(xs: Bits, n: Nat): Nat + case xs { + e: n, + o : Bits.length.go(xs.pred, Nat.succ(n)), + i : Bits.length.go(xs.pred, Nat.succ(n)) + } + +Bits.slice(len: Nat, bits: Bits): Bits + case len { + zero: Bits.e, + succ: case bits { + e: Bits.e, + o : Bits.o(Bits.slice(len.pred, bits.pred)), + i : Bits.i(Bits.slice(len.pred, bits.pred)) + } + } + +// Converts a bitstring to a string +Bits.to_string(bits: Bits): String + case bits { + e: "", + o : String.concat("0", Bits.to_string(bits.pred)), + i : String.concat("1", Bits.to_string(bits.pred)) + } + +// Converts a bitstring to a U32 value +Bits.to_u32(bits: Bits): U32 + U32.new(Word.from_bits(32, bits)) + +// Multiplies two bitstrings. +Bits.mul(a: Bits, b: Bits): Bits + Bits.mul.go(a, b, Bits.e) + +Bits.mul.go(a: Bits, b: Bits, bits: Bits): Bits + case b { + e: bits, + o : Bits.mul.go(Bits.o(a), b.pred, bits), + i : Bits.mul.go(Bits.o(a), b.pred, Bits.add(a, bits)) + } + +// TODO Divides two bitstrings. +Bits.div(a: Bits, b: Bits): Bits + Bits.div(a, b) + +// TODO Modulus of two Bitstrings. +Bits.mod(a: Bits, b: Bits): Bits + Bits.mod(a, b) + +// TODO +// Subtracts two Bitstrings. +Bits.sub(a: Bits, b: Bits): Bits + Bits.sub(a, b) + + + diff --git a/src/Bool.fm b/src/Bool.fm index f67cc8f..9279325 100644 --- a/src/Bool.fm +++ b/src/Bool.fm @@ -40,3 +40,72 @@ Bool.if(cond: Bool, true_case: A, false_case: A): A true : true_case false: false_case } + +// Boolean negation, fusible +// Bool.notf(a: Bool): Bool +//

(t, f) +// case a { +// true: f, +// false: t, +// } : P(Bool.notf(a.self)) + +// Ensures a Bool is true +Bool.IsTrue(b: Bool): Type + case b { + true: Unit, + false: Empty, + } + +// Ensures a Bool is false. +Bool.IsFalse(b: Bool): Type + case b { + true: Empty, + false: Unit, + } + +// Proof that not(not(b)) == b +Bool.double_negation(b: Bool): Equal(Bool, Bool.not(Bool.not(b)), b) + case b { + true: Equal.refl<_, Bool.true>, + false: Equal.refl<_, Bool.false>, + } : Equal(Bool, Bool.not(Bool.not(b)), b) + +// Proof that false != true +// Bool.false_isnt_true: Not(Equal(Bool, Bool.false, Bool.true)) +// def P = ((b: Bool) +// case b { +// true: Empty, +// false: Unit, +// }) :: Bool -> Type +// (false_is_true) Equal.rewrite<_,_,_,P>(false_is_true, Unit.new) + +// Proof that true != false +// Bool.true_isnt_false: Not(Equal(Bool, Bool.true, Bool.false)) +// def P = ((b : Bool) +// case b { +// true: Unit, +// false: Empty, +// }) :: Bool -> Type +// (true_is_false) Equal.rewrite<_,_,_,P>(true_is_false, Unit.new) + +// Converts to a string +Bool.show(b: Bool): String + case b { + true: "Bool.true", + false: "Bool.false", + } + +// Bool that is provably different from the input +// Bool.test.different_elem: (a: Bool) -> Subset(Bool, (b) Not(Equal(Bool, a, b))) +// (a) +// a<(self) Subset(Bool, (b) Not(Equal(Bool, self, b)))> +// | Subset.new(Bool.false); +// | Subset.new(Bool.true); + + +// Dependent elimination of Bool. +Bool.elim(b: Bool): Type> -> P(Bool.true) -> P(Bool.false) -> P(b) +

(t) (f) b

(t, f) + +Bool.and_var: (n: Nat) -> Variadic(n, Bool, Bool) + Variadic.foldr(Bool.and, Bool.true) diff --git a/src/Buffer32.fm b/src/Buffer32.fm new file mode 100644 index 0000000..d7ec036 --- /dev/null +++ b/src/Buffer32.fm @@ -0,0 +1,43 @@ +// A Buffer32 contains 2^depth values of type U32. +// Note: This is compiled to a mutable array. Because of that, buffers must be +// used linearly. This is NOT checked yet, so, right now, buffer compilation is +// unsafe until linearity checks are added! +type Buffer32 { + new(depth: Nat, array: Array(U32, depth)) +} + +Buffer32.alloc(depth: Nat): Buffer32 + Buffer32.new(depth, Array.alloc(depth, U32.zero)) + +// Buffer32.get(idx: U32, buf: Buffer32): U32 +// // TODO: get dep arr = buf +// // TODO: get wrd = idx +// open buf +// let dep = buf.depth +// let arr = buf.array +// open idx +// let wrd = idx.value +// let idx = Word.trim<32>(dep, wrd) +// Array.get(idx, arr) + + +// Converts a hex string into a Buffer32. +// TODO. We need to: +// 1. Compute the length of the string with String.length32 +// 2. Divide by 8 to get the buffer length (add U32 consts on Lang?) +// 3. Use Nat.succ(Word.nat_log2<32>(...)) to compute its depth +// 4. Allocate the buffer with Buffer32.alloc +// 5. Split hex into chunks of 8 chars (32 bits) +// 6. Convert it into a list of U32 using Char.hex_value32 +// 7. Loop with U32.for, using Buffer32.set(i, list[i], buf) +// Use U32 whenever possible +// Buffer32.parse_hex(hex: String): Buffer32 +// Buffer32.parse_hex(hex) + +// Buffer32.set(idx: U32, val: U32, buf: Buffer32): Buffer32 +// get dep arr = buf +// get wrd = idx +// let idx = Word.trim<32>(dep, wrd) +// def arr = Array.set(idx, val, arr) +// Buffer32.new(dep, arr) + diff --git a/src/CList.fm b/src/CList.fm new file mode 100644 index 0000000..082539f --- /dev/null +++ b/src/CList.fm @@ -0,0 +1,210 @@ +//A Circular List +// left is kept in reverse order +// right is kept in order +type CList { + nil, + ring(left: List(A), focus: A, right: List(A)) +} + +type CList.Dir { + Left, + Right +} + +// replaces the focus with the provided element, shifting +// the previous focus to the left +CList.add_left(a: A, cl: CList(A)): CList(A) + case cl { + nil : CList.singleton<_>(a), + ring: CList.ring<_>(List.cons<_>(cl.focus, cl.left), a, cl.right) + } + +// replaces the focus with the provided element, shifting +// the previous focus to the right +CList.add_right(a: A, cl: CList(A)): CList(A) + case cl { + nil : CList.singleton<_>(a), + ring: CList.ring<_>(cl.left, a, List.cons<_>(cl.focus, cl.right)) + } + +CList.balance(cl: CList(A)): CList(A) + CList.from_list<_>(CList.to_list<_>(cl)) + +CList.empty : CList(A) + CList.nil + +CList.filter(p: A -> Bool, cl: CList(A)): CList(A) + case cl { + nil : cl, + ring: + let list = CList.to_list<_>(cl) + let filtered = List.filter<_>(p, list) + CList.from_list<_>(filtered) + } + +CList.focus(cl: CList(A)): Maybe(A) + case cl { + nil : Maybe.none<_>, + ring: Maybe.some<_>(cl.focus) + } + +CList.foldr(b: B, f: A -> B -> B, cl: CList(A)): B + let list = CList.to_list<_>(cl) + List.foldr<_,_>(b, f, list) + +// creates a balanced circular list from a regular list +CList.from_list(as: List(A)): CList(A) + case as { + nil : CList.nil<_>, + cons: + let len = List.length<_>(as) + let mid = Nat.div(len, 2) + open List.split_at<_>(mid, as.tail) as spl + let fst_half = spl.fst + let snd_half = spl.snd + CList.ring<_>(List.reverse<_>(snd_half), as.head, fst_half) + } + +CList.is_empty(cl: CList(A)): Bool + case cl { + nil : Bool.true, + ring: Bool.false + } + +CList.left(cl: CList(A)): Maybe(List(A)) + case cl { + nil : Maybe.none<_>, + ring: Maybe.some<_>(cl.left) + } + +CList.length(cl: CList(A)): Nat + case cl { + nil : 0, + ring: + let left = List.length(cl.left) + let right = List.length(cl.right) + Nat.add(1, Nat.add(left, right)) + } + +CList.map(f: A -> B, cl: CList(A)): CList(B) + case cl { + nil : CList.nil<_>, + ring: + let left = List.map<_,_>(f, cl.left) + let right = List.map<_,_>(f, cl.right) + let focus = f(cl.focus) + CList.ring<_>(left, focus, right) + } + +// removes the focus, replacing it with an element from the left +CList.remove_left(cl: CList(A)): CList(A) + case cl { + nil : cl, + ring: + case cl.left { + nil: case cl.right { + nil : CList.nil<_>, //both right and left are empty + cons: case List.reverse<_>(cl.right) as rev_right { //left is empty, right is not + nil : CList.nil<_>, //unreachable + cons: CList.ring<_>(rev_right.tail, rev_right.head, []) + } + }, + cons: CList.ring<_>(cl.left.tail, cl.left.head, cl.right) + } + } + +// removes the focus, replacing it with an element from the right +CList.remove_right(cl: CList(A)): CList(A) + case cl { + nil : cl, + ring: case cl.right { + nil: case cl.left { + nil : CList.nil<_>, //both right and left are empty + cons: case List.reverse<_>(cl.left) as rev_left { //right is empty, left is not + nil : CList.nil<_>, //unreachable + cons: CList.ring<_>([], rev_left.head, rev_left.tail) + } + }, + cons: CList.ring<_>(cl.left, cl.right.head, cl.right.tail) + } + } + +CList.right(cl: CList(A)): Maybe(List(A)) + case cl { + nil : Maybe.none<_>, + ring: Maybe.some<_>(cl.right) + } + +// single anti-clockwise rotation +CList.rotate_left(cl: CList(A)): CList(A) + case cl { + nil : cl, + ring: case cl.left { + nil: case cl.right { + //we have a singleton, nothing changes + nil: cl, + // left is empty, right is not + cons: case List.reverse<_>(cl.right) as rev_right { + nil : cl, //unreachable + cons: + let new_left = rev_right.tail + let new_focus = rev_right.head + let new_right = [cl.focus] + CList.ring<_>(new_left, new_focus, new_right) + } + }, + // left is not empty + cons: + let new_left = cl.left.tail + let new_focus = cl.left.head + let new_right = List.cons<_>(cl.focus, cl.right) + CList.ring<_>(new_left, new_focus, new_right) + } + } + +CList.rotate_n(dir: CList.Dir, n: Nat, cl: CList(A)): CList(A) + case dir { + Left : Nat.apply<_>(n, CList.rotate_left<_>, cl), + Right: Nat.apply<_>(n, CList.rotate_right<_>, cl) + } + +// single clockwise rotation +CList.rotate_right(cl: CList(A)): CList(A) + case cl { + nil : cl, + ring: + case cl.right { + nil: case cl.left { + //we have a singleton, nothing changes + nil: cl, + //right is empty, left is not + cons: case List.reverse<_>(cl.left) as rev_left { + nil : cl, //unreachable + cons: + let new_left = [cl.focus] + let new_focus = rev_left.head + let new_right = rev_left.tail + CList.ring<_>(new_left, new_focus, new_right) + } + }, + // right is not empty + cons: + let new_left = List.cons<_>(cl.focus, cl.left) + let new_focus = cl.right.head + let new_right = cl.right.tail + CList.ring<_>(new_left, new_focus, new_right) + } + } + +CList.singleton(a: A): CList(A) + CList.ring<_>([], a, []) + +// converts a circular list into a regular one with the head as the focus +CList.to_list(cl: CList(A)): List(A) + case cl { + nil : List.nil<_>, + ring: + let left = List.reverse<_>(cl.left) + let right = List.cons<_>(cl.focus, cl.right) + List.concat<_>(right, left) + } diff --git a/src/Char.fm b/src/Char.fm index 66178b3..a8e68c9 100644 --- a/src/Char.fm +++ b/src/Char.fm @@ -28,3 +28,66 @@ Char.new( Char.eql(a: Char, b: Char): Bool U16.eql(a, b) + +// Char.hex_value(chr: Char): Nat +// U32.to_nat(Char.hex_value32(chr)) + +// Receives a hex char (0-9, a-f, A-F) and returns its value. +Char.hex_value16(chr: Char): U16 + def U16.add10 = ((x0) + def x1 = U16.inc(U16.inc(U16.inc(U16.inc(U16.inc(x0))))) + def x2 = U16.inc(U16.inc(U16.inc(U16.inc(U16.inc(x1))))) + x2) :: U16 -> U16 + if Bool.and(U16.gte(chr,'0'),U16.lte(chr,'9')) then + U16.sub(chr,'0') + else if Bool.and(U16.gte(chr,'a'),U16.lte(chr,'f')) then + U16.add10(U16.sub(chr,'a')) + else if Bool.and(U16.gte(chr,'A'),U16.lte(chr,'F')) then + U16.add10(U16.sub(chr,'A')) + else + U16.zero + +Char.hex_value32(chr: Char): U32 + U16.to_u32(Char.hex_value16(chr)) + + +Char.newline: Char + Char.new( + Bit.o, Bit.o, Bit.o, Bit.o, + Bit.o, Bit.o, Bit.o, Bit.o, + Bit.o, Bit.o, Bit.o, Bit.o, + Bit.i, Bit.o, Bit.i, Bit.o) + +// Parses a character. Example: `Char.parse("x")` +Char.parse(str: String): Char.parse.type(str) + case str { + nil : Unit.new, + cons: str.head + } : Char.parse.type(str) + +Char.parse.type(str: String): Type + case str { + nil : Unit, + cons: Char + } + +// TODO: not recognizing `s` +// Char.to_lower(char: U16): U16 +// case Bool.and(U16.gte(char, 'A'), U16.lte(char, 'Z')) +// U16.add(char, 32s) +// else +// char + +// Char.to_upper(char: U16): U16 +// if Bool.and(U16.gte(char, 'a'), U16.lte(char, 'z')) then +// U16.sub(char, 32s) +// else +// char + +Char.newline: Char + Char.new( + Bit.o, Bit.o, Bit.o, Bit.o, + Bit.o, Bit.o, Bit.o, Bit.o, + Bit.o, Bit.o, Bit.o, Bit.o, + Bit.i, Bit.o, Bit.i, Bit.o) + \ No newline at end of file diff --git a/src/Col32.fm b/src/Col32.fm new file mode 100644 index 0000000..0428408 --- /dev/null +++ b/src/Col32.fm @@ -0,0 +1,125 @@ +Col32: Type + U32 + +// Col32.new(r: U32, g: U32, b: U32, a: U32): Col32 +// let col = 0u +// let col = U32.or(col, r) +// let col = U32.or(col, U32.shl(g, 8u)) +// let col = U32.or(col, U32.shl(b, 16u)) +// let col = U32.or(col, U32.shl(a, 24u)) +// col + +// Col32.black : Col32 +// Col32.new(0u, 0u, 0u, 255u) + +// Col32.blue : Col32 +// Col32.new(0u, 0u, 255u, 255u) + +// Col32.cyan : Col32 +// Col32.new(0u, 255u, 255u, 255u) + +// // Alpha is disconsidered +// // Approximate value due to U32 calculus +// Col32.darken(rgba: Col32, amount: U32): Col32 +// let r = Col32.get_r(rgba) +// let g = Col32.get_g(rgba) +// let b = Col32.get_b(rgba) +// let r_upd = U32.percent(amount, r) +// let g_upd = U32.percent(amount, g) +// let b_upd = U32.percent(amount, b) +// Col32.new(r_upd, g_upd, b_upd, 255u) + +// Col32.get_a(col: Col32): U32 +// U32.and(U32.shr(col, 24u), 255u) + +// Col32.get_b(col: Col32): U32 +// U32.and(U32.shr(col, 16u), 255u) + +// Col32.get_g(col: Col32): U32 +// U32.and(U32.shr(col, 8u), 255u) + +// Col32.get_r(col: Col32): U32 +// U32.and(col, 255u) + +// Col32.gray : Col32 +// Col32.new(128u, 128u, 128u, 255u) + +// Col32.green : Col32 +// Col32.new(0u, 128u, 0u, 255u) + +// // Alpha is disconsidered +// Col32.invert(rgba: Col32): Col32 +// let r = Col32.get_r(rgba) +// let g = Col32.get_g(rgba) +// let b = Col32.get_b(rgba) +// let r_dif = U32.sub(255u, r) +// let g_dif = U32.sub(255u, g) +// let b_dif = U32.sub(255u, b) +// Col32.new(r_dif, g_dif, b_dif, 225u) + +// // Alpha is disconsidered +// // Approximate value due to U32 calculus +// Col32.lighten(rgba: Col32, amount: U32): Col32 +// let r = Col32.get_r(rgba) +// let g = Col32.get_g(rgba) +// let b = Col32.get_b(rgba) +// let r_dif = U32.sub(255u, r) +// let g_dif = U32.sub(255u, g) +// let b_dif = U32.sub(255u, b) +// let r_upd = U32.percent(amount, r_dif) +// let g_upd = U32.percent(amount, g_dif) +// let b_upd = U32.percent(amount, b_dif) +// Col32.new(U32.add(r, r_upd), U32.add(g, g_upd), U32.add(b, b_upd), 255u) + + +// Col32.lime : Col32 +// Col32.new(0u, 255u, 0u, 255u) + +// Col32.magenta : Col32 +// Col32.new(255u, 0u, 255u, 255u) + +// Col32.maroon : Col32 +// Col32.new(128u, 0u, 0u, 255u) + +// Col32.navy : Col32 +// Col32.new(0u, 0u, 128u, 255u) + +// Col32.olive : Col32 +// Col32.new(128u, 128u, 0u, 255u) + +// Col32.purple : Col32 +// Col32.new(128u, 0u, 128u, 255u) + +// Col32.red : Col32 +// Col32.new(255u, 0u, 0u, 255u) + +// // Where "a" is between 0u and 100u +// // Approximate value due to U32 calculus +// Col32.set_alpha(a: U32): U32 +// U32.percent(a, 255u) + +// Col32.show(rgba: Col32): String +// // Get the U32 values +// let r = Col32.get_r(rgba) +// let g = Col32.get_g(rgba) +// let b = Col32.get_b(rgba) +// let a = Col32.get_a(rgba) +// // TODO: add U32.show +// let r_str = Nat.show(U32.to_nat(r)) +// let g_str = Nat.show(U32.to_nat(g)) +// let b_str = Nat.show(U32.to_nat(b)) +// let a_str = Nat.show(U32.to_nat(a)) +// String.flatten(["rgba(", String.intercalate(",", [r_str, g_str, b_str, a_str]), ")"]) + +// Col32.silver : Col32 +// Col32.new(192u, 192u, 192u, 255u) + +// Col32.teal : Col32 +// Col32.new(0u, 128u, 128u, 255u) + +// Col32.white : Col32 +// Col32.new(255u, 255u, 255u, 255u) + +// Col32.yellow : Col32 +// Col32.new(255u, 255u, 0u, 255u) + diff --git a/src/Either.fm b/src/Either.fm index a306f70..65811e7 100644 --- a/src/Either.fm +++ b/src/Either.fm @@ -3,3 +3,42 @@ type Either { right(value: B), } +Either.bind(e: Either(A,B), f: B -> Either(A,C)): Either(A,C) + case e { + left: Either.left<_,_>(e.value), + right: f(e.value), + } + +Either.monad: Monad(Either(A)) + Monad.new(Either.bind, Either.right) + +Either.map(f: B -> C, e: Either(A, B)): Either(A, C) + case e { + left: Either.left(e.value), + right: Either.right(f(e.value)), + } + +Either.functor: Functor(Either(A)) + Functor.new(Either.map) + +Either.functor.verified: VerifiedFunctor(Either(A), Either.functor) + VerifiedFunctor.new>(Either.map.id, Either.map.comp) + +Either.map.id(e: Either(A, B)): Equal(Either(A, B), Either.map(Function.id, e), e) + case e{ + left : _ + right: _ + } : Equal(_, Either.map(Function.id<_>, e), e) + + +Either.map.comp(e: Either(A, B), g: (C -> D), h: (B -> C)) + : Equal(Either(A, D), + Either.map(Function.comp(g, h), e), + Function.comp(Either.map(g), Either.map(h), e)) + case e{ + left : _ + right: _ + } : Equal(_, + Either.map<_,_,_>(Function.comp<_,_,_>(g, h), e), + Function.comp<_,_,_>(Either.map<_,_,_>(g), Either.map<_,_,_>(h))(e)) + diff --git a/src/Equal.fm b/src/Equal.fm index b59104d..b1cb0cf 100644 --- a/src/Equal.fm +++ b/src/Equal.fm @@ -21,3 +21,25 @@ Equal.chain(d: Equal(A,a,b), e: Equal(A,b,c)): Equal( case e { refl: d } : Equal(A, a, e.b) + +Equal.applyd Type, a: A, b: A>(f: (x: A) -> B(x), e: Equal(A, a, b)) + : Equal(B(a), f(a), Equal.rewrite(Equal.mirror(e))(f(b))) + case e{ + refl: Equal.refl + } : Equal(B(a), f(a), Equal.rewrite(Equal.mirror(e),f(e.b))) + +// Erased rewrite +Equal.cast Type, e: Equal(A,a,b)>(x: P(a)): P(b) + case e{ + refl: x + } : P(e.b) + +// If a == x and b == x, then a == b +Equal.left(r: Equal(A, a, x), s: Equal(A, b, x)) +: Equal(A, a, b) + Equal.chain(r, Equal.mirror(s)) + +// If x == a and x == b, then a == b +Equal.right(r: Equal(A, x, a), s: Equal(A, x, b)) +: Equal(A, a, b) + Equal.chain(Equal.mirror(r), s) \ No newline at end of file diff --git a/src/Export.fm b/src/Export.fm new file mode 100644 index 0000000..b8f97bb --- /dev/null +++ b/src/Export.fm @@ -0,0 +1,13 @@ +type Export { + new(T: Type, value: T) +} + +Export.T(ex: Export): Type + open ex + ex.T + +Export.value(ex: Export): Export.T(ex) + case ex{ + new: ex.value + } : case ex{new: ex.T} + diff --git a/src/F64.fm b/src/F64.fm new file mode 100644 index 0000000..45ca61e --- /dev/null +++ b/src/F64.fm @@ -0,0 +1,472 @@ +// An IEEE-754 compliant 64-bit floating point. +type F64 { + new(word: Word(64)) +} + +type F64.Boundary { + new(pts: List(F64.V3)) +} + +type F64.Circle { + new(pos: F64.V3, rad: F64) +} + +type F64.Line { + new(pos: F64.V3, dir: F64.V3) +} + +type F64.Ordering { + LT, + EQ, + GT +} + +type F64.Segment { + new(a: F64.V3, b: F64.V3) +} + +type F64.V3 { + new(x: F64, y: F64, z: F64) +} + +F64.parse_binary(str: String): F64 + F64.new(Word.from_bits(64, String.to_bits(str))) + +F64.0 : F64 + F64.parse_binary("0000000000000000000000000000000000000000000000000000000000000000") + +F64.1 : F64 + F64.parse_binary("0000000000000000000000000000000000000000000000000000111111111100") + +F64.180 : F64 + F64.parse_binary("0000000000000000000000000000000000000000000000010110011000000010") + +F64.2 : F64 + F64.parse_binary("0000000000000000000000000000000000000000000000000000000000000010") + +F64.256 : F64 + F64.parse_binary("0000000000000000000000000000000000000000000000000000111000000010") + +F64.V3.add(a: F64.V3, b: F64.V3): F64.V3 + open a + open b + let c.x = F64.add(a.x, a.x) + let c.y = F64.add(a.y, b.y) + let c.z = F64.add(a.z, b.z) + F64.V3.new(c.x, c.y, c.z) + +F64.V3.circle_boundary_intersects(c: F64.Circle, b: F64.Boundary): F64 + open c + open b + case b.pts { + nil: F64.0, + cons: + let h0 = b.pts.head + let t0 = b.pts.tail + case t0 { + nil: F64.0, + cons: + let h1 = t0.head + let t1 = t0.tail + let p0 = h0 + let p1 = h1 + let sg = F64.Segment.new(p0, p1) + let cd = F64.V3.point_segment_sqrdist(c.pos, sg) + let test = F64.ltn(cd, F64.mul(cd, cd)) + case test { + true: F64.1, + false: + let boun = F64.Boundary.new(List.cons(h1, t1)) + F64.V3.circle_boundary_intersects(c, boun) + } + } + } + +F64.V3.dist(a: F64.V3, b: F64.V3): F64 + F64.sqrt(F64.V3.sqr_dist(a, b)) + +F64.V3.dot(a: F64.V3, b: F64.V3): F64 + open a + open b + let res = F64.0 + let res = F64.add(res, F64.mul(a.x, b.x)) + let res = F64.add(res, F64.mul(a.y, b.y)) + let res = F64.add(res, F64.mul(a.z, b.z)) + res + +F64.V3.eql(a: F64.V3, b: F64.V3): Bool + open a + open b + let same_x = F64.eql(a.x, b.x) + let same_y = F64.eql(a.y, b.y) + let same_z = F64.eql(a.z, b.z) + Bool.and(same_x, Bool.and(same_y, same_z)) + +F64.V3.get_x(v: F64.V3): F64 + open v + v.x + +F64.V3.get_y(v: F64.V3): F64 + open v + v.y + +F64.V3.get_z(v: F64.V3): F64 + open v + v.z + +F64.V3.len(v: F64.V3): F64 + open v + let sqr = F64.0 + let sqr = F64.add(sqr, F64.mul(v.x, v.x)) + let sqr = F64.add(sqr, F64.mul(v.y, v.y)) + let sqr = F64.add(sqr, F64.mul(v.z, v.z)) + let expo = F64.div(F64.1, F64.add(F64.1, F64.1)) + let sqr = F64.pow(sqr, expo) + sqr + +F64.V3.look_at(a: F64.V3, b: F64.V3, c: F64.V3): F64.V3 + open a + open b + open c + let a_eql_b = F64.V3.eql(a, b) + let diff = F64.V3.sub(b, a) + let normdiff = F64.V3.norm(diff) + case a_eql_b { + true : normdiff, + false: c + } + +// Return true if "a" is less than "b" +F64.V3.ltn(a: F64.V3, b: F64.V3): Bool + let len_a = F64.V3.len(a) + let len_b = F64.V3.len(b) + F64.ltn(len_a, len_b) + +F64.V3.map(fn: F64 -> F64, v: F64.V3): F64.V3 + open v + F64.V3.new(fn(v.x), fn(v.y), fn(v.z)) + +F64.V3.map_x(fn: F64 -> F64, v: F64.V3): F64.V3 + open v + F64.V3.new(fn(v.x), v.y, v.z) + +F64.V3.map_y(fn: F64 -> F64, v: F64.V3): F64.V3 + open v + F64.V3.new(v.x, fn(v.y), v.z) + +F64.V3.map_z(fn: F64 -> F64, v: F64.V3): F64.V3 + open v + F64.V3.new(v.x, v.y, fn(v.z)) + +F64.V3.mul(a: F64.V3, b: F64.V3): F64.V3 + open a + open b + let c.x = F64.mul(a.x, a.x) + let c.y = F64.mul(a.y, b.y) + let c.z = F64.mul(a.z, b.z) + F64.V3.new(c.x, c.y, c.z) + +F64.V3.norm(v: F64.V3): F64.V3 + open v + let len = F64.V3.len(v) + let new_x = F64.div(v.x, len) + let new_y = F64.div(v.y, len) + let new_z = F64.div(v.z, len) + F64.V3.new(new_x, new_y, new_z) + +F64.V3.point_segment_dist(p: F64.V3, s: F64.Segment): F64 + F64.sqrt(F64.V3.point_segment_sqrdist(p, s)) + +// Squared distance between a point and a segment +F64.V3.point_segment_sqrdist(p: F64.V3, s: F64.Segment): F64 + open p + open s + open s.a + open s.b + let ab_x_diff_sqrd = F64.pow(F64.sub(s.a.x, s.b.x), F64.2) + let ab_y_diff_sqrd = F64.pow(F64.sub(s.a.y, s.b.y), F64.2) + let pa_x_diff = F64.sub(p.x, s.a.x) + let pa_y_diff = F64.sub(p.y, s.a.y) + let ba_x_diff = F64.sub(s.b.x, s.a.x) + let ba_y_diff = F64.sub(s.b.y, s.a.y) + let l = F64.add(ab_x_diff_sqrd, ab_y_diff_sqrd) + let t = F64.add(F64.mul(pa_x_diff, ba_x_diff), F64.mul(pa_y_diff, ba_y_diff)) + let t = F64.div(t, l) + let t = F64.max(F64.0, F64.min(F64.1, t)) + let d = F64.0 + let t_times_ba_x_diff = F64.mul(t, ba_x_diff) + let t_times_ba_y_diff = F64.mul(t, ba_y_diff) + let k = F64.pow(F64.sub(p.x, F64.add(s.a.x, t_times_ba_x_diff)), F64.2) + let d = F64.add(d, k) + let k = F64.pow(F64.sub(p.y, F64.add(s.a.y, t_times_ba_y_diff)), F64.2) + let d = F64.add(d, k) + d + +F64.V3.polygon_to_segments.cons( + pos: F64.V3, + dir: F64.V3, + pt_b: F64.V3, + segs: (Maybe(F64.V3) -> Maybe(F64.V3) -> List(F64.Segment)), + pt_a: Maybe(F64.V3), + pt_0: Maybe(F64.V3)): + List(F64.Segment) + case pt_a { + none: segs(Maybe.some(pt_b), Maybe.some(pt_b)), + some: + let pt_0 = case pt_0 { + none: Maybe.some(pt_b), + some: pt_0 + } + let p0 = F64.V3.polygon_to_segments.transform(pos, dir, pt_a.value) + let p1 = F64.V3.polygon_to_segments.transform(pos, dir, pt_b) + let sg = F64.Segment.new(p0, p1) + List.cons(sg, segs(Maybe.some(pt_b), pt_0)) + } + +F64.V3.polygon_to_segments( + pos: F64.V3, + dir: F64.V3, + pts: List(F64.V3)): + List(F64.Segment) + List.foldr Maybe(F64.V3) -> List(F64.Segment)>( + F64.V3.polygon_to_segments.nil(pos, dir), + F64.V3.polygon_to_segments.cons(pos, dir), + pts, + Maybe.none, + Maybe.none + ) + +F64.V3.polygon_to_segments.nil( + pos: F64.V3, + dir: F64.V3, + pt_a: Maybe(F64.V3), + pt_0: Maybe(F64.V3)): + List(F64.Segment) + case pt_0 { + none: List.nil, + some: case pt_a { + none: List.nil, + some: + let p0 = F64.V3.polygon_to_segments.transform(pos, dir, pt_a.value) + let p1 = F64.V3.polygon_to_segments.transform(pos, dir, pt_0.value) + let sg = F64.Segment.new(p0, p1) + List.cons(sg, List.nil) + } + } + +F64.V3.polygon_to_segments.transform(pos: F64.V3, dir: F64.V3, pnt: F64.V3): F64.V3 + open pnt + open dir + let a = F64.atan(dir.y, dir.x) + let pnt_x_times_cos_a = F64.mul(pnt.x, F64.cos(a)) + let pnt_y_times_sin_a = F64.mul(pnt.y, F64.sin(a)) + let pnt_x_times_sin_a = F64.mul(pnt.x, F64.sin(a)) + let pnt_y_times_cos_a = F64.mul(pnt.y, F64.cos(a)) + let x = F64.sub(pnt_x_times_cos_a, pnt_y_times_sin_a) + let y = F64.add(pnt_x_times_sin_a, pnt_y_times_cos_a) + F64.V3.add(pos, F64.V3.new(x, y, pnt.z)) + +F64.V3.rot_90(v: F64.V3): F64.V3 + open v + F64.V3.new(v.y, F64.sub(F64.0, v.x), v.z) + +// Rotates a vector on the x-y plane around an arbitrary point +F64.V3.rotate(a: F64, v: F64.V3, p: F64.V3): F64.V3 + open v + open p + let rad = F64.mul(a, F64.div(F64.pi, F64.180)) + let sin = F64.sin(rad) + let cos = F64.cos(rad) + let x_diff = F64.sub(v.x, p.x) + let y_diff = F64.sub(v.y, p.y) + let x_diff_times_cos = F64.mul(x_diff, cos) + let x_diff_times_sin = F64.mul(x_diff, sin) + let y_diff_times_cos = F64.mul(y_diff, cos) + let y_diff_times_sin = F64.mul(y_diff, sin) + let new_x = F64.sub(F64.add(p.x, x_diff_times_cos), y_diff_times_sin) + let new_y = F64.add(F64.add(p.y, x_diff_times_sin), y_diff_times_cos) + F64.V3.new(new_x, new_y, v.z) + +F64.V3.scale(k: F64, v: F64.V3): F64.V3 + open v + let new_x = F64.mul(k, v.x) + let new_y = F64.mul(k, v.y) + let new_z = F64.mul(k, v.z) + F64.V3.new(new_x, new_y, new_z) + +F64.V3.sqr_dist(a: F64.V3, b: F64.V3): F64 + open a + open b + let two = F64.add(F64.1, F64.1) + let x_diff = F64.pow(F64.sub(a.x, b.x), two) + let y_diff = F64.pow(F64.sub(a.y, b.y), two) + let z_diff = F64.pow(F64.sub(a.z, b.z), two) + F64.add(x_diff, F64.add(y_diff, z_diff)) + +F64.V3.sub(a: F64.V3, b: F64.V3): F64.V3 + open a + open b + let c.x = F64.sub(a.x, a.x) + let c.y = F64.sub(a.y, b.y) + let c.z = F64.sub(a.z, b.z) + F64.V3.new(c.x, c.y, c.z) + +// TODO +// Converts a F64.V3 to a Pos32 +F64.V3.to_pos32(pos: F64.V3): Pos32 + F64.V3.to_pos32(pos) + +F64._1 : F64 + F64.parse_binary("0000000000000000000000000000000000000000000000000000111111111101") + +// Arccos function. +F64.acos: F64 -> F64 //prim// + F64.acos + +// TODO Adds two 64-bit floats. +F64.add: F64 -> F64 -> F64 //prim// + F64.add + +// Arcsine function. +F64.asin: F64 -> F64 //prim// + F64.asin + +// Arctan function. +F64.atan: F64 -> F64 -> F64 //prim// + F64.atan + +F64.cmp(x: F64, y: F64): Cmp + open x + open y + Word.cmp<64>(x.word, y.word) + + +F64.compare_numbers(a: F64, b: F64): F64.Ordering + case F64.eql(a, b){ + true : F64.Ordering.EQ + false: case F64.ltn(b, a){ + true : F64.Ordering.GT + false: F64.Ordering.LT + } + } + +// Cosine function. +F64.cos: F64 -> F64 //prim// + F64.cos + +// TODO Divides two 64-bit floats. +F64.div: F64 -> F64 -> F64 //prim// + F64.div + +F64.eql(x: F64, y: F64): Bool + open x + open y + Word.eql<64>(x.word, y.word) + + +F64.ltn(a: F64, b: F64): Bool + open a + open b + Word.ltn<64>(a.word, b.word) + + +// TODO Exponential function. +F64.exp: F64 -> F64 -> F64 //prim// + F64.exp + +F64.floor(x: F64): F64 + let ltn_zero = F64.if<_>(F64.from_bool(F64.ltn(x, F64.0)), F64.1, F64.0) + F64.sub(F64.sub(x, F64.mod(x, F64.1)), ltn_zero) + +F64.from_bool(b: Bool): F64 + case b { + true : F64.1, + false: F64.0 + } + +F64.gte(a: F64, b: F64): Bool + open a + open b + Word.gte<64>(a.word, b.word) + +F64.gtn(a: F64, b: F64): Bool + open a + open b + Word.gtn<64>(a.word, b.word) + +F64.if(x: F64, ct: A, cf: A): A + case F64.eql(x, F64.0) { + true : cf, + false: ct + } + +// Is x inside the a..b range, with `b` exclusive? +F64.is_between(a: F64, b: F64, x: F64): Bool + let a_eql_x = F64.eql(a, x) + let a_ltn_x = F64.ltn(a, x) + let x_ltn_b = F64.ltn(x, b) + Bool.or(a_eql_x, Bool.and(a_ltn_x, x_ltn_b)) + +// TODO: Logarithm function. +F64.log: F64 -> F64 //prim// + F64.log + +F64.lte(a: F64, b: F64): Bool + open a + open b + Word.lte<64>(a.word, b.word) + +// // TODO +F64.max: F64 -> F64 -> F64 //prim// + F64.max + +// TODO +F64.min: F64 -> F64 -> F64 //prim// + F64.min + +// TODO: Modulus of two 64-bit floats. +F64.mod: F64 -> F64 -> F64 //prim// + F64.mod + +// TODO Multiplies two 64-bit floats. +F64.mul: F64 -> F64 -> F64 //prim// + F64.mul + +// TODO +F64.parse: String -> F64 + F64.parse + +F64.pi : F64 + F64.parse_binary("0001100010110100001000100010101011011111100001001001000000000010") + +// TODO Power function +F64.pow: F64 -> F64 -> F64 //prim// + F64.pow + +F64.rotate2d(x: F64, y: F64, a: F64): Pair(F64, F64) + let x2 = F64.sub(F64.mul(x, F64.cos(a)), F64.mul(y, F64.sin(a))) + let y2 = F64.add(F64.mul(x, F64.sin(a)), F64.mul(y, F64.cos(a))) + Pair.new<_,_>(x2, y2) + +// TODO Sine function. +F64.sin: F64 -> F64 //prim// + F64.sin + +// Square root function. +F64.sqrt(n: F64): F64 //prim// + F64.pow(n, F64.div(F64.1, F64.2)) + +// TODO Subtracts two 64-bit floats. +F64.sub: F64 -> F64 -> F64 //prim// + F64.sub + +// TODO Tangent function. +F64.tan: F64 -> F64 //prim// + F64.tan + +// F64.tau: F64 +// 6.28318530718 + +F64.to_u32(a: F64): U32 + F64.to_u32(a) + diff --git a/src/Function.fm b/src/Function.fm new file mode 100644 index 0000000..f724487 --- /dev/null +++ b/src/Function.fm @@ -0,0 +1,42 @@ +// Calls a function in an argument. The most useless function. +Function.call(x: A, f: A -> B): B + f(x) + +// Function composition. +Function.comp(g: B -> C, f: A -> B, x: A): C + g(f(x)) + +// Given a `x`, returns a function that receives an `y` and returns `x`. +Function.const(x: A, y: B): A + x + +// Converts a function that receives a pair into a function of 2 arguments. +Function.curry(f: Pair(A, B) -> C, x: A, y: B): C + f(Pair.new(x, y)) + +// Dependent function composition. +Function.dcompType>(g:(b:B)->C(b), f:A -> B, x:A): C(f(x)) + g(f(x)) + +// Flips the two first arguments of a function. +Function.flip(f: A -> B -> C, y: B, x: A): C + f(x, y) + +// `Function(A, (x) B(x))` is a synonym for `(x: A) -> B(x)` +Function(A: Type, B: A -> Type): Type + (x: A) -> B(x) + +// The identity function returns its argument. +Function.id(x: A): A + x + +// Function application in reverse order. +Function.pipe(x: A, f: A -> B): B + f(x) + +// Converts a function from 2 arguments to a function that receives a pair. +Function.uncurry(f: A -> B -> C, p: Pair(A, B)): C + open p + f(p.fst, p.snd) + + diff --git a/src/Functor.fm b/src/Functor.fm new file mode 100644 index 0000000..dd8265b --- /dev/null +++ b/src/Functor.fm @@ -0,0 +1,11 @@ +Functor.const Type>(f: Functor(F)): -> A -> F(B) -> F(A) + (a) + Functor.map<_>(f)<_,_>(Function.const<_,_>(a)) + +type Functor Type> { + new(map: -> (A -> B) -> F(A) -> F(B)) +} + +Functor.map Type>(f: Functor(F)): -> (A -> B) -> F(A) -> F(B) + open f + f.map diff --git a/src/GMap.fm b/src/GMap.fm new file mode 100644 index 0000000..756aff2 --- /dev/null +++ b/src/GMap.fm @@ -0,0 +1,915 @@ +// A generic map from keys of type `K` to values of type `V` +// which under the hood is a size balanced binary tree +// note that because of this structure, the key type `K` +// *must* be able to implement a function with the signature +// cmp: K -> K -> Cmp +// which is used in many of the map-related operations +// +// Implementation based on +// "Implementing Sets Efficiently in a Functional Language" +// by Stephen Adams and Haskell's `containers` package +// +// left contains elements whose keys are smaller than the +// current node's key, while right contains elements whose keys +// are greater +type GMap { + tip, + bin(size: Nat, key: K, val: V, left: GMap(K,V), right: GMap(K,V)) +} + +// modifies the value associated with a specific key +// by applying a function to it +// in case the key is not in the map, do nothing +// as with other GMap operations, you must provide +// a way to compare the keys +GMap.adjust( + cmp : K -> K -> Cmp, + f : V -> V, + key : K, + map : GMap(K,V) +) : GMap(K,V) + GMap.adjust_with_key( + cmp, + (k, v) f(v), + key, + map + ) + +// modifies the value associated with a specific key +// by applying a function that uses both a key and a +// value to generate a new value +// in case the key is not in the map, do nothing +// as with other GMap operations, you must provide +// a way to compare the keys +GMap.adjust_with_key( + cmp : K -> K -> Cmp, + f : K -> V -> V, + k : K, + map : GMap(K,V) +) : GMap(K,V) + case map { + tip: map, + bin: + case cmp(k, map.key) { + // k < map.key, we check the left subtree + ltn: + let new_left = GMap.adjust_with_key(cmp, f, k, map.left) + GMap.node(map.key, map.val, new_left, map.right), + + // we found the key we were looking for, so just + // apply the function + eql: + let new_val = f(map.key, map.val) + GMap.node(map.key, new_val, map.left, map.right), + + // k > map.key, we check in the right subtree + gtn: + let new_right = GMap.adjust_with_key(cmp, f, k, map.right) + GMap.node(map.key, map.val, map.left, map.right) + } + } + +// In order to to guarantee the efficiency of the search operation +// we *must* preserve the tree balanced, otherwise it could become +// degenerate, looking more like a list, which is much slower +// +// Here we use the size information along with a constant (GMap.w) +// to ensure that one subtree is never more than w times bigger than +// the other subtree +// +// Once a tree is found to be unbalanced, then we build a new tree +// by rotating the former, shifting part of the heavy subtree to +// the lighter subtree. This rotation can be `single` or `double`. +// In the single rotation the entire subtree of the heavy subtree +// is moved to the other side, while in the double only a part is +// moved +// +// A visual representation of these rotations is given below +// +// { a, b, c } are tree keys and a < b < c +// { X, Y, Z } are trees of size Nx, Ny, Nz respectively +// The sums inside the parens represent the size of the tree at that level +// +// SINGLE (LEFT) ROTATION +// a (Nx + Ny + Nz + 2) b (Nx + Ny + Nz + 2) +// / \ => / \ +// X b (Ny + Nz + 1) (Nx + Ny + 1) a Z +// / \ / \ +// Y Z X Y +// +// DOUBLE (LEFT) ROTATION +// a (Nx + Ny + Nz + 3) b (Nx + Ny + Nz + 3) +// / \ / \ +// X c (Ny_1 + Ny_2 + Nz + 2) (Nx + Ny_1 + 1) a c +// / \ => / \ / \ +// (Ny = Ny_1 + Ny_2 + 1) b Z X Y1 Y2 Z +// / \ +// Y1 Y2 + + +GMap.balance(k: K, v: V, l: GMap(K,V), r: GMap(K,V)): GMap(K,V) + let size_l = GMap.size(l) + let size_r = GMap.size(r) + let size_l_plus_size_r = Nat.add(size_l, size_r) + let w_x_size_l = Nat.mul(GMap.w, size_l) + let w_x_size_r = Nat.mul(GMap.w, size_r) + + // size_l_plus_size_r < 2 means that one subtree is empty and the + // other contains only one element, hence the tree cannot be balanced + if Nat.ltn(size_l_plus_size_r, 2) then + GMap.node(k, v, l, r) + // size_r > w * size_l means the right subtree is too heavy + else if Nat.gtn(size_r, w_x_size_l) then + case r { + // this is an impossible case because we already know that + // the right subtree is too heavy + // question: how to deal with it? + tip: GMap.node(k, v, l, r), + bin: + let size_rl = GMap.size(r.left) + let size_rr = GMap.size(r.right) + // size_rl < size_rr means we should perform a single left rotation + if Nat.ltn(size_rl, size_rr) then + let new_key = r.key + let new_val = r.val + let new_left = GMap.node(k, v, l, r.left) + let new_right = r.right + GMap.node(new_key, new_val, new_left, new_right) + // size_rl > size_rr means we should perform a double left rotation + else + // we need to branch on the left subtree of r in order to extract its components + case r.left { + tip: GMap.node(k, v, l, r), // impossible case + bin: + let new_key = r.left.key + let new_val = r.left.val + let new_left = GMap.node(k, v, l, r.left.left) + let new_right = GMap.node(r.key, r.val, r.left.right, r.right) + GMap.node(new_key, new_val, new_left, new_right) + } + } + + // size_l > w * size_r means the left subtree is too heavy + else if Nat.gtn(size_l, w_x_size_r) then + case l { + // this is an impossible case because we already know that + // the left subtree is too heavy + // question: how to deal with it? + tip: GMap.node(k, v, l, r), + bin: + let size_ll = GMap.size(l.left) + let size_lr = GMap.size(l.right) + // size_lr < size_lln means we should perform a single right rotation + if Nat.ltn(size_lr, size_ll) then + let new_key = l.key + let new_val = l.val + let new_left = l.left + let new_right = GMap.node(k, v, l.right, r) + GMap.node(new_key, new_val, new_left, new_right) + // size_lr > size_ll means we should perform a double right rotation + else + // we need to branch on the right subtree of l in order to + // extract its components and move them to the right + case l.right { + tip: GMap.node(k, v, l, r), // impossible case + bin: + let new_key = l.right.key + let new_val = l.right.val + let new_left = GMap.node(l.key, l.val, l.left, l.right.left) + let new_right = GMap.node(k, v, l.right.right, r) + GMap.node(new_key, new_val, new_left, new_right) + } + } + else // neither subtrees are too heavy, no balancing is needed + GMap.node(k, v, l, r) + + +// similar to GMap.concat3, but doesn't use a "glue" key-value pair +// GMap.concat(map_a: GMap(K,V), map_b: GMap(K,V)): GMap(K,V) +// case map_a { +// tip: case map_b { +// tip: GMap.tip, +// bin: map_b +// }, +// bin: case map_b { +// tip: map_a, +// bin: +// let b_is_too_heavy = Nat.ltn(Nat.mul(GMap.w, map_a.size), map_b.size) +// let a_is_too_heavy = Nat.ltn(Nat.mul(GMap.w, map_b.size), map_a.size) + +// if b_is_too_heavy then +// let new_key = map_b.key +// let new_val = map_b.val +// let new_left = GMap.concat(map_a, map_b.left) +// let new_right = map_b.right +// GMap.balance(new_key, new_val, new_left, new_right) + +// else if a_is_too_heavy then +// let new_key = map_a.key +// let new_val = map_a.val +// let new_left = map_a.left +// let new_right = GMap.concat(map_a.right, map_b) +// GMap.balance(new_key, new_val, new_left, new_right) + +// else +// let maybe_min_b = GMap.min(map_b) +// let dummy = Pair.new(map_b.key, map_b.val) +// let min_b = Maybe.extract(maybe_min_b, dummy) // we know map_b isn't empty +// let new_key = Pair.fst(min_b) +// let new_val = Pair.snd(min_b) +// let new_left = map_a +// let new_right = GMap.delete_min(map_b) +// GMap.balance(new_key, new_val, new_left, new_right) +// } +// } + +// Joins two trees with a key that is greater +// than the root key of the left, and less than +// the root key of the right +// A comparison function must be provided +GMap.concat3( + cmp : K -> K -> Cmp, + key : K, + val : V, + left : GMap(K,V), + right: GMap(K,V) +) : GMap(K,V) + + case left { + tip: case right { + tip: GMap.singleton(key, val), // trivial case, both trees are empty + bin: GMap.insert(cmp, key, val, right) // if left is empty, we just insert (key,val) in the right tree + }, + bin: case right { + tip: GMap.insert(cmp, key, val, left), // if right is empety, we just insert (key,val) in the left tree + // if none of the trees are empty, we need to check if we can + // make a balanced tree by using (key,val) as a new node + // if not, we need to find the largest subtree on the side + // "facing" the smaller tree that is small enough to balance + // with the smaller tree + bin: + let right_is_heavier = Nat.ltn(Nat.mul(GMap.w, left.size), right.size) + let left_is_heavier = Nat.ltn(Nat.mul(GMap.w, right.size), left.size) + + if right_is_heavier then + let new_key = right.key + let new_val = right.val + let new_left = GMap.concat3(cmp, key, val, left, right.left) + let new_right = right.right + GMap.balance(new_key, new_val, new_left, new_right) + + else if left_is_heavier then + let new_key = left.key + let new_val = left.val + let new_left = left.left + let new_right = GMap.concat3(cmp, key, val, left.right, right) + GMap.balance(new_key, new_val, new_left, new_right) + + else + GMap.node(key, val, left, right) + } + } + +// // Removes an element from a map, using a user-provided comparison +// // function, balancing the resulting tree in case such element is found +// GMap.delete( +// cmp : K -> K -> Cmp, +// key : K, +// map : GMap(K,V) +// ) : GMap(K,V) + +// case map { +// tip: map, +// bin: case cmp(key, map.key) { +// ltn: GMap.delete(cmp, key, map.left), // if key < map.key, we should look for it in the left subtree +// // when the element is at the root of the current subtree +// // things are a little trickier: we need to get the minimum +// // key of the right subtree and then balance the tree composed +// // of this minimum key we just found, the left subtree and +// // the right subtree without that minimum element +// eql: case map.right { +// tip: case map.left { +// // if both subtrees are empty, we delete +// // the root and return an empty map +// tip: GMap.tip, +// // if the right subtree is empty, and we just +// // deleted the root, we simply return the left +// // subtree, which is not empty +// bin: map.left +// }, +// bin: case map.left { +// // conversely, if left is empty and right is not, we +// // return the right subtree +// tip: map.right, +// // when none of the subtrees are empty, then we need to +// // find the smallest value of the right subtree and delete it +// bin: +// let maybe_min_pair = GMap.min(map.right) +// // a hack, we know it can never be `none` because the right +// // subtree is not empty +// let dummy = Pair.new(key, map.val) +// let min_pair = Maybe.extract(maybe_min_pair, dummy) +// case min_pair { +// new: +// let new_key = min_pair.fst +// let new_val = min_pair.snd +// let new_left = map.left +// let new_right = GMap.delete(cmp, new_key, map.right) +// GMap.balance(new_key, new_val, new_left, new_right) +// } +// } +// }, +// // if key < map.key, we should look for it in the left subtree +// gtn: +// let new_key = map.key +// let new_val = map.val +// let new_left = map.left +// let new_right = GMap.delete(cmp, key, map.right) +// GMap.balance(new_key, new_val, new_left, new_right) +// } +// } + +// Removes the minimum key of the map +// which is always the leftmost one in the tree +GMap.delete_min(map: GMap(K,V)): GMap(K,V) + case map { + tip: map, + bin: case map.left { + tip: map.right, + bin: + let new_left = GMap.delete_min(map.left) + GMap.balance(map.key, map.val, new_left, map.right) + } + } + +// // Suppose we have two Maps: T1 and T2 +// // T1 T2 +// // v u +// // / \ / \ +// // A B C D +// // +// // We can implement efficient Map x Map -> Map operations +// // but applying a "divide and conque" strategy, that means +// // we'll break those sets in smaller parts using `split_ltn` +// // and `split_gtn`, perform the desired operation on those +// // smaller parts, and then combine everything with `concat3` +// // +// // - <> can be union, difference, intersection... +// // - v and u are keys +// // - A, B, C and D are subtrees +// // +// // T1 <> T2 +// // / \ +// // v u C' = split_ltn(T2) +// // / \ / \ D' = split_gtn(T2) +// // A B C D +// // | | +// // | | +// // | | +// // A <> C' B <> D' +// // \ / +// // \ / +// // \ / +// // concat3(A<>C', v, B<>D') +// // +// // Asymetric difference +// GMap.difference( +// cmp : K -> K -> Cmp, +// map_a : GMap(K,V), +// map_b : GMap(K,V) +// ) : GMap(K,V) +// case map_a { +// tip: case map_b { +// tip: GMap.tip, +// bin: map_b +// }, +// bin: case map_b { +// tip: map_a, +// bin: +// // divide & conquer +// let ltn = GMap.split_ltn(cmp, map_b.key, map_a) +// let gtn = GMap.split_gtn(cmp, map_b.key, map_a) +// let left = GMap.difference(cmp, ltn, map_b.left) +// let right = GMap.difference(cmp, gtn, map_b.right) +// GMap.concat(left, right) +// } +// } + +GMap.foldr(f: V -> Z -> Z, z: Z, map : GMap(K,V)): Z + GMap.foldr.go(f, z, map) + +GMap.foldr.go(f: V -> Z -> Z, z: Z, map: GMap(K,V)): Z + case map { + tip: z, + bin: + let right_folded = GMap.foldr.go(f, z, map.right) + let new_z = f(map.val, right_folded) + GMap.foldr.go(f, new_z, map.left) + } + +// like GMap.foldr but with access to both values and keys +GMap.foldr_with_key(f: K -> V -> Z -> Z, z: Z, map: GMap(K,V)): Z + GMap.foldr_with_key.go(f, z, map) + + +GMap.foldr_with_key.go( + f : K -> V -> Z -> Z, + z : Z, + map : GMap(K,V) +) : Z + case map { + tip: z, + bin: + let right_folded = GMap.foldr_with_key.go(f, z, map.right) + let new_z = f(map.key, map.val, right_folded) + GMap.foldr_with_key.go(f, new_z, map.left) + } + +// Creates a map from a list of key-value pairs +GMap.from_list( + cmp : K -> K -> Cmp, + xs : List(Pair(K,V)) +) : GMap(K,V) + GMap.from_list.go(cmp, GMap.tip, xs) + + + GMap.from_list.go( + cmp : K -> K -> Cmp, + acc : GMap(K,V), + xs : List(Pair(K,V)) +) : GMap(K,V) + case xs { + nil : acc, + cons: + let key = Pair.fst(xs.head) + let val = Pair.snd(xs.head) + let new_acc = GMap.insert(cmp, key, val, acc) + GMap.from_list.go(cmp, new_acc, xs.tail) + } + +// Adds a new key-value pair into the map using +// a user-provided comparison function +GMap.insert( + cmp : K -> K -> Cmp, + key : K, + val : V, + map : GMap(K,V) +) : GMap(K,V) + + case map { + tip: GMap.singleton(key, val), + bin: case cmp(key, map.key) { + // if key < map.key, the new value should go into the left subtree + ltn: + let new_key = map.key + let new_val = map.val + let new_left = GMap.insert(cmp, key, val, map.left) + let new_right = map.right + GMap.balance(new_key, new_val, new_left, new_right), + // `val` is already in the map, so how do we proceed? + // if we decide to simply return the map unchanged, we are + // ignoring the case where other fields of `val`, which are not + // used in the comparison function, might have changed + // this comes at some extra cost, of course + eql: GMap.node(key, val, map.left, map.right), + // if key > map.key, the new value should go into the right subtree + gtn: + let new_key = map.key + let new_val = map.val + let new_left = map.left + let new_right = GMap.insert(cmp, key, val, map.right) + GMap.balance(new_key, new_val, new_left, new_right) + } + } + +// // Suppose we have two Maps: T1 and T2 +// // T1 T2 +// // v u +// // / \ / \ +// // A B C D +// // +// // We can implement efficient Map x Map -> Map operations +// // but applying a "divide and conque" strategy, that means +// // we'll break those sets in smaller parts using `split_ltn` +// // and `split_gtn`, perform the desired operation on those +// // smaller parts, and then combine everything with `concat3` +// // +// // - <> can be union, difference, intersection... +// // - v and u are keys +// // - A, B, C and D are subtrees +// // +// // T1 <> T2 +// // / \ +// // v u C' = split_ltn(T2) +// // / \ / \ D' = split_gtn(T2) +// // A B C D +// // | | +// // | | +// // | | +// // A <> C' B <> D' +// // \ / +// // \ / +// // \ / +// // concat3(A<>C', v, B<>D') +// // Right-biased operation, meaning that if +// // both map contains the same key, the value +// // from map_b will be chosen +// // +// GMap.intersection( +// cmp : K -> K -> Cmp, +// map_a : GMap(K,V), +// map_b : GMap(K,V) +// ) : GMap(K,V) + +// case map_a { +// tip: case map_b { +// tip: GMap.tip, +// bin: GMap.tip +// }, +// bin: case map_b { +// tip: GMap.tip, +// bin: +// // divide & conquer +// let ltn = GMap.split_ltn(cmp, map_b.key, map_a) +// let gtn = GMap.split_gtn(cmp, map_b.key, map_a) +// let left = GMap.intersection(cmp, ltn, map_b.left) +// let right = GMap.intersection(cmp, gtn, map_b.right) + +// if GMap.member(cmp, map_b.key, map_a) then +// GMap.concat3(cmp, map_b.key, map_b.val, left, right) +// else +// GMap.concat(left, right) +// } +// } + + +GMap.is_balanced(map: GMap(K,V)): Bool + case map { + tip: Bool.true, + bin: + let size_l = GMap.size<_,_>(map.left) + let size_r = GMap.size<_,_>(map.right) + let max_size_l = Nat.mul(GMap.w, size_r) + let max_size_r = Nat.mul(GMap.w, size_l) + let size_l_plus_r = Nat.add(size_l, size_r) + let sizes_dont_exceed = List.and([ + Nat.lte(size_l, max_size_r), + Nat.lte(size_r, max_size_l) + ]) + let subtrees_sizes_ok = Bool.or(sizes_dont_exceed, Nat.lte(size_l_plus_r, 1)) + let left_is_balanced = GMap.is_balanced<_,_>(map.left) + let right_is_balanced = GMap.is_balanced<_,_>(map.right) + + List.and([subtrees_sizes_ok, left_is_balanced, right_is_balanced]) + } + +// possibly returns the value associated with a key +GMap.lookup(cmp: K -> K -> Cmp, key: K, map: GMap(K,V)): Maybe(V) + case map { + tip: Maybe.none, + bin: case cmp(key, map.key) { + ltn: GMap.lookup(cmp, key, map.left), + eql: Maybe.some(map.val), + gtn: GMap.lookup(cmp, key, map.right) + } + } + +// similar to GMap.lookup, but will return the provided default value +// if the given key is not present in the map +GMap.lookup_with_default( + cmp : K -> K -> Cmp, + key : K, + dft : V, + map : GMap(K,V) +) : V + case GMap.lookup(cmp, key, map) as maybe_val { + none: dft, + some: maybe_val.value + } + +// Applies a function to every value present in the map +GMap.map(f: V -> Z, map: GMap(K,V)): GMap(K,Z) + case map { + tip: GMap.tip, + bin: + let new_val = f(map.val) + let new_left = GMap.map(f, map.left) + let new_right = GMap.map(f, map.right) + GMap.node(map.key, new_val, new_left, new_right) + } + +// checks if a given key is present in the map +GMap.member(cmp: K -> K -> Cmp, key: K, map: GMap(K,V)): Bool + case map { + tip: Bool.false, + bin: case cmp(key, map.key) { + ltn: GMap.member(cmp, key, map.left), + eql: Bool.true, + gtn: GMap.member(cmp, key, map.right) + } + } + +// Possibly returns a pair of the minimum key and value +// of the map +// Since we're working with a balanced tree we only need +// to check the the left subtree, if it's empty, the +// minimum value is the root, because all elements to the +// right are greater than it. If it's not, recurse until +// the leftmost element is found +GMap.min(map: GMap(K,V)): Maybe(Pair(K,V)) + case map { + tip: Maybe.none, + bin: case map.left { + tip: Maybe.some(Pair.new(map.key, map.val)), + bin: GMap.min(map.left) + } + } + +// a smart constructor to ensure that the size of the tree is maintained correctly +// the subtrees passed as arguments must already be balanced +GMap.node(key: K, val: V, left: GMap(K,V), right: GMap(K,V)): GMap(K,V) + let size_left = GMap.size(left) + let size_right = GMap.size(right) + let new_size = List.sum([1, size_left, size_right]) + GMap.bin(new_size, key, val, left, right) + +// checks if a key is not present in a map +GMap.not_member(cmp: K -> K -> Cmp, key: K, map: GMap(K,V)): Bool + Bool.not(GMap.member(cmp, key, map)) + +// checks if a map is empty or not +GMap.null(map: GMap(K,V)): Bool + case map { + tip: Bool.true, + bin: Bool.false + } + +GMap.show( + show_key: K -> String, + show_val: V -> String, + map : GMap(K,V) +): String + let show_pair = Pair.show(show_key, show_val) + let kvs = GMap.to_list(map) + let kvs = List.map(show_pair, kvs) + List.show(String.show, kvs) + +// creates a map from a single pair of key and value +// note that the key type `K` *must* be able to implement +// a function with the signature: +// cmp: K -> K -> Cmp +// which is used in many map-related operations +GMap.singleton(key: K, val: V): GMap(K,V) + GMap.bin(1, key, val, GMap.tip<_,_>, GMap.tip<_,_>) + +// Returns the size of a given map +GMap.size(map: GMap(K,V)): Nat + case map { + tip: 0, + bin: map.size + } + +// Given a comparison function, a map, and a key (cut), this function +// returns a map with keys which are greater than the cut, discarding +// the rest +GMap.split_gtn(cmp: K -> K-> Cmp, cut: K, map: GMap(K,V)): GMap(K,V) + case map { + tip: map, + bin: case cmp(cut, map.key) { + ltn: + let key = map.key + let val = map.val + let left = GMap.split_gtn(cmp, cut, map.left) + let right = map.right + GMap.concat3(cmp, key, val, left, right), + eql: map.right, + gtn: GMap.split_gtn(cmp, cut, map.right) + } + } + +// Given a comparison function, a map, and a key (cut), this function +// returns a map with keys which are less than the cut, discarding +// the rest +GMap.split_ltn(cmp: K -> K-> Cmp, cut: K, map: GMap(K,V)): GMap(K,V) + case map { + tip: map, + bin: case cmp(cut, map.key) { + ltn: GMap.split_ltn(cmp, cut, map.left), + eql: map.left, + gtn: + let key = map.key + let val = map.val + let left = map.left + let right = GMap.split_ltn(cmp, cut, map.right) + GMap.concat3(cmp, key, val, left, right) + } + } + +// transforms a map into a list of key-value pairs +GMap.to_list(map: GMap(K,V)): List(Pair(K,V)) + GMap.foldr_with_key( + (k, v, kvs) List.cons(Pair.new(k,v), kvs), + List.nil, + map + ) + +// Suppose we have two Maps: T1 and T2 +// T1 T2 +// v u +// / \ / \ +// A B C D +// +// We can implement efficient Map x Map -> Map operations +// but applying a "divide and conque" strategy, that means +// we'll break those sets in smaller parts using `split_ltn` +// and `split_gtn`, perform the desired operation on those +// smaller parts, and then combine everything with `concat3` +// +// - <> can be union, difference, intersection... +// - v and u are keys +// - A, B, C and D are subtrees +// +// T1 <> T2 +// / \ +// v u C' = split_ltn(T2) +// / \ / \ D' = split_gtn(T2) +// A B C D +// | | +// | | +// | | +// A <> C' B <> D' +// \ / +// \ / +// \ / +// concat3(A<>C', v, B<>D') +// Right-biased operation, meaning that if +// both map contains the same key, the value +// from map_b will be chosen +// +GMap.union( + cmp : K -> K -> Cmp, + map_a: GMap(K,V), + map_b: GMap(K,V) +) : GMap(K,V) + + case map_a { + tip: case map_b { + tip: GMap.tip, + bin: map_b + }, + bin: case map_b { + tip: map_a, + bin: + let key = map_b.key + let val = map_b.val + let ltn = GMap.split_ltn(cmp, map_b.key, map_a) + let gtn = GMap.split_gtn(cmp, map_b.key, map_a) + let left = GMap.union(cmp, ltn, map_b.left) + let right = GMap.union(cmp, gtn, map_b.right) + GMap.concat3(cmp, key, val, left, right) + } + } + +// used for checking whether a tree is balanced +// it represents the maximum factor by which +// one subtree can outweigh its sibling +// +// this value was empirically chosen +// in Haskell's `containers` package +// and might be changed here later after +// benchmarks are run +GMap.w : Nat + 3 + +GMap.tests.1 : IO(Unit) + let kvs = [ + Pair.new<_,_>(1,"a") + Pair.new<_,_>(2,"b") + Pair.new<_,_>(3,"c") + ] + let map = GMap.from_list<_,_>(Nat.cmp, kvs) + let map = GMap.show<_,_>(Nat.show, String.show, map) + IO.print(map) //["(1,"a")","(2,"b")","(3,"c")"] + +// GMap.tests.2 : The(String, "b") +// def kvs = [ +// Pair.new<_,_>(1,"a") +// Pair.new<_,_>(2,"b") +// Pair.new<_,_>(3,"c") +// ] +// def map = GMap.from_list<_,_>(Nat.cmp, kvs) +// def val_at_key_2 = GMap.lookup_with_default<_,_>(Nat.cmp, 2, "?", map) +// The.value<_>(val_at_key_2) + +// GMap.tests.3 : The(String, "a") +// def empty_map = GMap.tip +// def not_empty = GMap.insert<,>(Nat.cmp, 1, "a", empty_map) +// def the_a = GMap.lookup_with_default<,>(Nat.cmp, 1, "?", not_empty) +// The.value<>(the_a) + +// GMap.tests.4 : The(Maybe(String), Maybe.none<>) +// def kvs = [ +// Pair.new<,>(1,"a") +// Pair.new<,>(2,"b") +// Pair.new<,>(3,"c") +// ] +// def map = GMap.from_list<,>(Nat.cmp, kvs) +// def map = GMap.delete<,>(Nat.cmp, 2, map) +// def res = GMap.lookup<,>(Nat.cmp, 2, map) +// The.value<>(res) + +// GMap.tests.5 : IO(Unit) +// let kvs_a = [ +// Pair.new<,>(1,"a") +// Pair.new<,>(2,"b") +// Pair.new<,>(3,"c") +// ] + +// let kvs_b = [ +// Pair.new<,>(2,"?") +// Pair.new<,>(4,"d") +// Pair.new<,>(5,"e") +// ] + +// let map_a = GMap.from_list<,>(Nat.cmp, kvs_a) +// let map_b = GMap.from_list<,>(Nat.cmp, kvs_b) + +// let res = GMap.union<,>(Nat.cmp, map_a, map_b) +// let res = GMap.show<,>(Nat.show, String.show, res) +// IO.print(res) + +// GMap.tests.6 : IO(Unit) +// let kvs_a = [ +// Pair.new<,>(1,"a") +// Pair.new<,>(2,"b") +// Pair.new<,>(3,"c") +// ] + +// let kvs_b = [ +// Pair.new<,>(2,"?") +// Pair.new<,>(4,"d") +// Pair.new<,>(5,"e") +// ] + +// let map_a = GMap.from_list<,>(Nat.cmp, kvs_a) +// let map_b = GMap.from_list<,>(Nat.cmp, kvs_b) + +// let res = GMap.intersection<,>(Nat.cmp, map_a, map_b) +// let res = GMap.show<,>(Nat.show, String.show, res) +// IO.print(res) + +// GMap.tests.7 : IO(Unit) +// let kvs_a = [ +// Pair.new<,>(1,"a") +// Pair.new<,>(2,"b") +// Pair.new<,>(3,"c") +// ] + +// let kvs_b = [ +// Pair.new<,>(2,"?") +// Pair.new<,>(4,"d") +// Pair.new<,>(5,"e") +// ] + +// let map_a = GMap.from_list<,>(Nat.cmp, kvs_a) +// let map_b = GMap.from_list<,>(Nat.cmp, kvs_b) + +// let res = GMap.difference<,>(Nat.cmp, map_a, map_b) +// let res = GMap.show<,>(Nat.show, String.show, res) +// IO.print(res) + +// GMap.tests.8 : IO(Unit) +// let kvs_a = [ +// Pair.new<,>(1,"a") +// Pair.new<,>(2,"b") +// Pair.new<,>(3,"c") +// ] +// let map_a = GMap.from_list<,>(Nat.cmp, kvs_a) +// let res = GMap.delete_min<,>(map_a) +// let res = GMap.show<,>(Nat.show, String.show, res) +// IO.print(res) + +// GMap.tests.9 : IO(Unit) +// let kvs = [ +// Pair.new<,>(1,"Hello"), +// Pair.new<,>(2,","), +// Pair.new<,>(3," "), +// Pair.new<,>(4,"World"), +// Pair.new<,>(5,"!") +// ] +// let map = GMap.from_list<,>(Nat.cmp, kvs) +// let res = GMap.foldr<,,>(String.concat, String.nil, map) +// IO.print(res) + +// GMap.tests.10: The(Bool, Bool.true) +// def kvs = [ +// Pair.new<,>(1,"Hello"), +// Pair.new<,>(2,","), +// Pair.new<,>(3," "), +// Pair.new<,>(4,"World"), +// Pair.new<,>(5,"!") +// ] +// def map = GMap.from_list<,>(Nat.cmp, kvs) +// def res = GMap.is_balanced<,>(map) +// The.value<>(res) + diff --git a/src/GSet.fm b/src/GSet.fm new file mode 100644 index 0000000..85e2702 --- /dev/null +++ b/src/GSet.fm @@ -0,0 +1,739 @@ +// A generic container for values of a given type +// using sized balanced binary trees +// left contains elements which are smaller than val +// right contains elements which are greater than val +// +// Implementation based on +// "Implementing Sets Efficiently in a Functional Language" +// by Stephen Adams +// +type GSet { + tip, + bin(size: Nat, val: A, left: GSet(A), right: GSet(A)) +} + +// In order to to guarantee the efficiency of the search operation +// we *must* preserve the tree balanced, otherwise it could become +// degenerate, looking more like a list, which is much slower +// +// Here we use the size information along with a constant (GSet.w) +// to ensure that one subtree is never more than w times bigger than +// the other subtree +// +// Once a tree is found to be unbalanced, then we build a new tree +// by rotating the former, shifting part of the heavy subtree to +// the lighter subtree. This rotation can be `single` or `double`. +// In the single rotation the entire subtree of the heavy subtree +// is moved to the other side, while in the double only a part is +// moved +// +// A visual representation of these rotations is given below +// +// { a, b, c } are tree elements (val) and a < b < c +// { X, Y, Z } are trees of size Nx, Ny, Nz respectively +// The sums inside the parens represent the size of the tree at that level +// +// SINGLE (LEFT) ROTATION +// a (Nx + Ny + Nz + 2) b (Nx + Ny + Nz + 2) +// / \ => / \ +// X b (Ny + Nz + 1) (Nx + Ny + 1) a Z +// / \ / \ +// Y Z X Y +// +// DOUBLE (LEFT) ROTATION +// a (Nx + Ny + Nz + 3) b (Nx + Ny + Nz + 3) +// / \ / \ +// X c (Ny_1 + Ny_2 + Nz + 2) (Nx + Ny_1 + 1) a c +// / \ => / \ / \ +// (Ny = Ny_1 + Ny_2 + 1) b Z X Y1 Y2 Z +// / \ +// Y1 Y2 + + +GSet.balance(a: A, l: GSet(A), r: GSet(A)): GSet(A) + let size_l = GSet.size<_>(l) + let size_r = GSet.size<_>(r) + let size_l_plus_size_r = Nat.add(size_l, size_r) + let w_x_size_l = Nat.mul(GSet.w, size_l) + let w_x_size_r = Nat.mul(GSet.w, size_r) + + // size_l_plus_size_r < 2 means that one subtree is empty and the + // other contains only one element, hence the tree cannot be balanced + if Nat.ltn(size_l_plus_size_r, 2) then + GSet.node<_>(a, l, r) + // size_r > w * size_l means the right subtree is too heavy + else if Nat.gtn(size_r, w_x_size_l) then + case r { + // this is an impossible case because we already know that + // the right subtree is too heavy + // question: how to deal with it? + tip: GSet.node<_>(a, l, r), + bin: + let size_rl = GSet.size<_>(r.left) + let size_rr = GSet.size<_>(r.right) + // size_rl < size_rr means we should perform a single left rotation + if Nat.ltn(size_rl, size_rr) then + let new_l = GSet.node<_>(a, l, r.left) + GSet.node<_>(r.val, new_l, r.right) + // size_rl > size_rr means we should perform a double left rotation + else + // we need to branch on the left subtree of r in order to extract its components + case r.left { + tip: GSet.node<_>(a, l, r), // impossible case + bin: + let new_val = r.left.val + let new_left = GSet.node<_>(a, l, r.left.left) + let new_right = GSet.node<_>(r.val, r.left.right, r.right) + GSet.node<_>(new_val, new_left, new_right) + } + } + + // size_l > w * size_r means the left subtree is too heavy + else if Nat.gtn(size_l, w_x_size_r) then + case l { + // this is an impossible case because we already know that + // the left subtree is too heavy + // question: how to deal with it? + tip: GSet.node<_>(a, l, r), + bin: + let size_ll = GSet.size<_>(l.left) + let size_lr = GSet.size<_>(l.right) + // size_lr < size_lln means we should perform a single right rotation + if Nat.ltn(size_lr, size_ll) then + let new_left = l.left + let new_right = GSet.node<_>(a, l.right, r) + GSet.node<_>(l.val, new_left, new_right) + // size_lr > size_ll means we should perform a double right rotation + else + // we need to branch on the right subtree of l in order to + // extract its components and move them to the right + case l.right { + tip: GSet.node<_>(a, l, r), // impossible case + bin: + let new_val = l.right.val + let new_left = GSet.node<_>(l.val, l.left, l.right.left) + let new_right = GSet.node<_>(a, l.right.right, r) + GSet.node<_>(new_val, new_left, new_right) + } + } + else // neither subtrees are too heavy, no balancing is needed + GSet.node<_>(a, l, r) + +// // Similar to GSet.concat3, but doesn't use a "glue element" +// GSet.concat(set_a: GSet(A), set_b: GSet(A)): GSet(A) +// case set_a { +// tip: case set_b { +// tip: GSet.tip<_>, +// bin: set_b +// }, +// bin: case set_b { +// tip: set_a, +// bin: +// let b_is_too_heavy = Nat.ltn(Nat.mul(GSet.w, set_a.size), set_b.size) +// let a_is_too_heavy = Nat.ltn(Nat.mul(GSet.w, set_b.size), set_b.size) + +// if b_is_too_heavy then +// let new_val = set_b.val +// let new_left = GSet.concat<_>(set_a, set_b.left) +// let new_right = set_b.right +// GSet.balance<_>(new_val, new_left, new_right) + +// else if a_is_too_heavy then +// let new_val = set_a.val +// let new_left = set_a.left +// let new_right = GSet.concat<_>(set_a.right, set_b) +// GSet.balance<_>(new_val, new_left, new_right) + +// else +// let min_b = GSet.min<_>(set_b) +// let new_val = Maybe.extract<_>(min_b, set_b.val) //we know b isn't empty +// let new_left = set_a +// let new_right = GSet.delete_min<_>(set_b) +// GSet.balance<_>(new_val, new_left, new_right) +// } +// } + +// Joins two trees with an element that is between +// the values in the left and the ones in the right +// A comparison function must be provided +GSet.concat3( + cmp : A -> A -> Cmp, + val : A, + left : GSet(A), + right: GSet(A) +) : GSet(A) + case left { + tip: case right { + // trivial case, both trees are empty + tip: GSet.singleton<_>(val), + // if the left is empty, we just insert it + // in the right tree + bin: GSet.insert<_>(cmp, val, right) + }, + bin: case right { + // if the right is empty, we just insert it + // in the left tree + tip: GSet.insert<_>(cmp, val, left), + // if none of the trees are empty, we need to check if + // we can make a balanced tree by using `val` as a new node + // if not, we need to find the largest subtree on the side + // "facing" the smaller tree that is small enough to balance + // with the smaller tree + bin: + let right_is_too_heavy = Nat.ltn(Nat.mul(GSet.w, left.size), right.size) + let left_is_too_heavy = Nat.ltn(Nat.mul(GSet.w, right.size), left.size) + + if right_is_too_heavy then + let new_val = right.val + let new_left = GSet.concat3<_>(cmp, val, left, right.left) + let new_right = right.right + GSet.balance<_>(new_val, new_left, new_right) + + else if left_is_too_heavy then + let new_val = left.val + let new_left = left.left + let new_right = GSet.concat3<_>(cmp, val, left.right, right) + GSet.balance<_>(new_val, new_left, new_right) + + else + GSet.node<_>(val, left, right) + } + } + +// // Removes an element from a set, using a user-provided comparison +// // function, balancing the resulting tree in case such element is found +// GSet.delete(cmp: A -> A -> Cmp, a: A, set: GSet(A)): GSet(A) +// case set { +// tip: set, +// bin: case cmp(a, set.val) { +// // if `a` is smaller than the current root +// // we should look for it in the left subtree +// ltn: +// let new_left = GSet.delete<_>(cmp, a, set.left) +// GSet.balance<_>(set.val, new_left, set.right), +// // when the element is at the root of the current subtree +// // things are a little trickier: we need to get the minimum +// // value of the right subtree and then balance the tree composed +// // of this minimum value we just found, the left subtree and +// // the right subtree without that minimum element +// eql: case set.right { +// tip: case set.left { +// // if both subtrees are empty and we deleted the root, we +// // return an empty set +// tip: GSet.tip<_>, +// // if the right subtree is empty, the left is not and +// // we've just deleted the root, all we have left is the +// // left tree +// bin: set.left +// }, +// bin: case set.left { +// // conversely, if left is empty and right is not, we +// // return the right subtree +// tip: set.right, +// // when none of the subtrees are empty, then we need to +// // find the smallest value of the right subtree and delete GSet.min +// bin: +// let min_val = GSet.min<_>(set.right) +// // this is a hack, we know it can never be `none` because the +// // tree is not empty +// let min_val = Maybe.extract<_>(min_val, a) +// let new_right = GSet.delete<_>(cmp, min_val, set.right) +// GSet.balance<_>(min_val, set.left, new_right) +// } +// }, +// // if `a`is greater than the current root +// // we look for it in the right subtree +// gtn: +// let new_right = GSet.delete<_>(cmp, a, set.right) +// GSet.balance<_>(set.val, set.left, new_right) +// } +// } + +// Removes the minimum element of the set, which +// is always the leftmost one in the tree +GSet.delete_min(set: GSet(A)): GSet(A) + case set { + tip: set, + bin: case set.left { + tip: set.right, + bin: + let new_left = GSet.delete_min<_>(set.left) + GSet.balance<_>(set.val, new_left, set.right) + } + } + +// // Suppose we have two Sets: T1 and T2 +// // T1 T2 +// // v u +// // / \ / \ +// // A B C D +// // +// // We can implement efficient Set x Set -> Set operations +// // but applying a "divide and conque" strategy, that means +// // we'll break those sets in smaller parts using `split_ltn` +// // and `split_gtn`, perform the desired operation on those +// // smaller parts, and then combine everything with `concat3` +// // +// // - <> is a binary operation (union, difference, intersection) +// // - v and u are values/elements +// // - A, B, C and D are subtrees +// // +// // T1 <> T2 +// // / \ +// // v u C' = split_ltn(T2) +// // / \ / \ D' = split_gtn(T2) +// // A B C D +// // | \__ __/ | +// // | _\/_ | +// // | / \ | +// // A <> C' B <> D' +// // \ / +// // \ / +// // \ / +// // concat3(A<>C', v, B<>D') +// // +// // Asymetric set difference +// GSet.difference(cmp: A -> A -> Cmp, set_a: GSet(A), set_b: GSet(A)): GSet(A) +// case set_a { +// tip: case set_b { +// tip: GSet.tip<>, +// bin: set_b +// }, +// bin: case set_b { +// tip: set_a, +// bin: +// // divide & conquer +// let ltn = GSet.split_ltn<>(cmp, set_b.val, set_a) +// let gtn = GSet.split_gtn<>(cmp, set_b.val, set_a) +// let left = GSet.difference<>(cmp, ltn, set_b.left) +// let right = GSet.difference<>(cmp, gtn, set_b.right) +// GSet.concat<>(left, right) +// } +// } + +GSet.foldr(f: A -> B -> B, b: B, set: GSet(A)): B + GSet.foldr.go<_,_>(f, b, set) + +GSet.foldr.go(f: A -> B -> B, acc: B, set: GSet(A)): B + case set { + tip: acc, + bin: + let right_folded = GSet.foldr.go<_,_>(f, acc, set.right) + let new_acc = f(set.val, right_folded) + GSet.foldr.go<_,_>(f, new_acc, set.left) + } + +GSet.from_list(cmp: A -> A -> Cmp, xs: List(A)): GSet(A) + List.foldr<_,_>(GSet.tip<_>, GSet.insert<_>(cmp), xs) + +// Adds a new element to a set with a user-provided comparison function +GSet.insert(cmp: A -> A -> Cmp, a: A, set: GSet(A)): GSet(A) + case set { + tip: GSet.singleton<_>(a), + bin: case cmp(a, set.val) { + // if a < set.val, the new value should go into the left subtree + ltn: + let new_left = GSet.insert<_>(cmp, a, set.left) + GSet.balance<_>(set.val, new_left, set.right), + // `a` is already in the set, so how do we proceed? + // if we decide to simply return the set unchanged, we are + // ignoring the case where other fields of `a`, which are not + // used in the comparison function, might have changed + // this comes at some extra cost, of course + eql: GSet.node<_>(a, set.left, set.right), + // if a > set.val, the new value should go into the right subtree + gtn: + let new_right = GSet.insert<_>(cmp, a, set.right) + GSet.balance<_>(set.val, set.left, new_right) + } + } + +// GSet.intersection( +// cmp : A -> A -> Cmp, +// set_a : GSet(A), +// set_b : GSet(A) +// ) : GSet(A) +// case set_a { +// tip: case set_b { +// tip: GSet.tip<>, +// bin: GSet.tip<> +// }, +// bin: case set_b { +// tip: GSet.tip<>, +// bin: +// // divide & conquer +// let ltn = GSet.split_ltn<>(cmp, set_b.val, set_a) +// let gtn = GSet.split_gtn<>(cmp, set_b.val, set_a) +// let new_left = GSet.intersection<>(cmp, ltn, set_b.left) +// let new_right = GSet.intersection<>(cmp, gtn, set_b.right) + +// if GSet.member<>(cmp, set_b.val, set_a) then +// GSet.concat3<>(cmp, set_b.val, new_left, new_right) + +// else +// GSet.concat<>(new_left, new_right) +// } +// } + +GSet.is_balanced(set: GSet(A)): Bool + case set { + tip: Bool.true, + bin: + let size_l = GSet.size<_>(set.left) + let size_r = GSet.size<_>(set.right) + let max_size_l = Nat.mul(GSet.w, size_r) + let max_size_r = Nat.mul(GSet.w, size_l) + let size_l_plus_r = Nat.add(size_l, size_r) + let sizes_dont_exceed = List.and([ + Nat.lte(size_l, max_size_r), + Nat.lte(size_r, max_size_l) + ]) + let subtrees_sizes_ok = Bool.or(sizes_dont_exceed, Nat.lte(size_l_plus_r, 1)) + let left_is_balanced = GSet.is_balanced<_>(set.left) + let right_is_balanced = GSet.is_balanced<_>(set.right) + + List.and([subtrees_sizes_ok, left_is_balanced, right_is_balanced ]) + } + +GSet.is_singleton(set: GSet(A)): Bool + let size = GSet.size<_>(set) + if Nat.eql(size, 1) then Bool.true else Bool.false + +GSet.map(f: A -> B, set: GSet(A)): GSet(B) + case set { + tip: GSet.tip<_>, + bin: + let new_val = f(set.val) + let new_left = GSet.map<_,_>(f, set.left) + let new_right = GSet.map<_,_>(f, set.right) + GSet.node<_>(new_val, new_left, new_right) + } + +GSet.member(cmp: A -> A -> Cmp, a: A, set: GSet(A)): Bool + case set { + tip: Bool.false, + bin: case cmp(a, set.val) { + ltn: GSet.member<_>(cmp, a, set.left), + eql: Bool.true, + gtn: GSet.member<_>(cmp, a, set.right) + } + } + +// Returns the values of a set in ascending order +GSet.members(set: GSet(A)): List(A) + GSet.foldr<_,_>(List.cons<_>, List.nil<_>, set) + +// Possibly returns the minimum value of the set +// Since we're working with a balanced tree we only need +// to check the if the left subtree, if it's empty, the +// minimum value is the root, because all elements to the +// right are greater than it. If it's not, recurse until +// the leftmost element is found +GSet.min(set: GSet(A)): Maybe(A) + case set { + tip: Maybe.none<_>, + bin: case set.left { + tip: Maybe.some<_>(set.val), + bin: GSet.min<_>(set.left) + } + } + +// a smart constructor to ensure that the size +// of the tree is maintained correctly +// the subtrees passed as arguments must already +// be balanced +GSet.node(val: A, left: GSet(A), right: GSet(A)): GSet(A) + let size_left = GSet.size<_>(left) + let size_right = GSet.size<_>(right) + let new_size = List.sum([1, size_left, size_right]) + GSet.bin<_>(new_size, val, left, right) + +GSet.not_member(cmp: A -> A -> Cmp, a: A, set: GSet(A)): Bool + Bool.not(GSet.member<_>(cmp, a, set)) + +GSet.null(set: GSet(A)): Bool + case set { + tip: Bool.true, + bin: Bool.false + } + +GSet.show(to_str: A -> String, set: GSet(A)): String + List.show<_>(to_str, GSet.members<_>(set)) + +GSet.singleton(a: A): GSet(A) + GSet.bin<_>(1, a, GSet.tip<_>, GSet.tip<_>) + +GSet.size(set: GSet(A)): Nat + case set { + tip: 0, + bin: set.size + } + +// Given a comparison function, set, and a value this function +// returns a tree with elements which are greater than the +// cut element, discarding the rest +GSet.split_gtn(cmp: A -> A -> Cmp, cut: A, set: GSet(A)): GSet(A) + case set { + tip: set, + bin: case cmp(cut, set.val) { + ltn: + let left = GSet.split_gtn<_>(cmp, cut, set.left) + GSet.concat3<_>(cmp, set.val, left, set.right), + eql: set.right, + gtn: GSet.split_gtn<_>(cmp, cut, set.right) + } + } + +// Given a comparison function, set, and a value this function +// returns a tree with elements which are less than the cut element +GSet.split_ltn(cmp: A -> A -> Cmp, cut: A, set: GSet(A)): GSet(A) + case set { + tip: set, + bin: case cmp(cut, set.val) { + ltn: GSet.split_ltn<_>(cmp, cut, set.left), + eql: set.left, + gtn: + let right = GSet.split_ltn<_>(cmp, cut, set.right) + GSet.concat3<_>(cmp, set.val, set.left, right) + } + } + +// just a synonym for `members` +GSet.to_list(set: GSet(A)): List(A) + GSet.members<_>(set) + +// Suppose we have two Sets: T1 and T2 +// T1 T2 +// v u +// / \ / \ +// A B C D +// +// We can implement efficient Set x Set -> Set operations +// but applying a "divide and conque" strategy, that means +// we'll break those sets in smaller parts using `split_ltn` +// and `split_gtn`, perform the desired operation on those +// smaller parts, and then combine everything with `concat3` +// +// - <> is a binary operation (union, difference, intersection) +// - v and u are values/elements +// - A, B, C and D are subtrees +// +// T1 <> T2 +// / \ +// v u C' = split_ltn(T2) +// / \ / \ D' = split_gtn(T2) +// A B C D +// | \__ __/ | +// | _\/_ | +// | / \ | +// A <> C' B <> D' +// \ / +// \ / +// \ / +// concat3(A<>C', v, B<>D') +// +GSet.union(cmp: A -> A -> Cmp, set_a: GSet(A), set_b: GSet(A)): GSet(A) + case set_a { + tip: case set_b { + tip: GSet.tip<_>, + bin: set_b + }, + bin: case set_b { + tip: set_a, + bin: + // divide & conquer + let ltn = GSet.split_ltn<_>(cmp, set_b.val, set_a) + let gtn = GSet.split_gtn<_>(cmp, set_b.val, set_a) + let left = GSet.union<_>(cmp, ltn, set_b.left) + let right = GSet.union<_>(cmp, gtn, set_b.right) + GSet.concat3<_>(cmp, set_b.val, left, right) + } + } + +// used for checking whether a tree is balanced +// it represents the maximum factor by which +// one subtree can outweigh its sibling +// +// this value was empirically chosen +// in Haskell's `containers` package +// and might be changed here later after +// benchmarks are run +GSet.w : Nat + 3 + +// Test.the_test: The(ResultType, result_value) +// The.value(computation) + +// if the input is ordered, `from_list` followed by `to_list` +// matches the input +// GSet.tests.1 : The(List(Nat), [1,2,3,4,5]) +// The.value<_>(GSet.to_list<_>(GSet.from_list<_>(Nat.cmp, [1,2,3,4,5]))) + +// if the input is not ordered, `from_list` followed by `to_list` +// orders the input +// GSet.tests.2 : The(List(Nat), [1,2,3,4,5]) +// def xs = [4,3,5,2,1] +// def xs = GSet.from_list<_>(Nat.cmp, xs) +// def xs = GSet.to_list<_>(xs) +// The.value<_>(xs) + +// // `to_list` on a set made from the empty list returns an empty list +// GSet.tests.3 : The(List(Nat), []) +// def xs = [] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def xs = GSet.to_list<>(xs) +// The.value<>(xs) + +// // `null` is true for a set made from the empty list +// GSet.tests.4 : The(Bool, Bool.true) +// def xs = [] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def xs = GSet.null<>(xs) +// The.value<>(xs) + +// // `member` returns `false` for elements not in the set +// GSet.tests.5 : The(Bool, Bool.false) +// def xs = [1,2,3,5] +// def x = 4 +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def r = GSet.member<>(Nat.cmp, x, xs) +// The.value<>(r) + +// // `member`returns `true`for elements in the set +// GSet.tests.6 : The(Bool, Bool.true) +// def xs = [1,2,3,5] +// def x = 3 +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def r = GSet.member<>(Nat.cmp, x, xs) +// The.value<>(r) + +// // `delete` removes the specified element from the set +// GSet.tests.7 : The(List(Nat), [1,3,4,5]) +// def xs = [1,2,3,4,5] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def xs = GSet.delete<>(Nat.cmp, 2, xs) +// def xs = GSet.to_list<>(xs) +// The.value<>(xs) + +// // `delete` does not change the set when the specified +// // element is not present in the set +// GSet.tests.8 : The(List(Nat), [1,2,3,4,5]) +// def xs = [1,2,3,4,5] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def xs = GSet.delete<>(Nat.cmp, 6, xs) +// def xs = GSet.to_list<>(xs) +// The.value<>(xs) + +// // `delete_min` removes the minimum element in the set +// GSet.tests.9 : The(List(Nat), [2,3]) +// def xs = [1,2,3] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def xs = GSet.delete_min<>(xs) +// def xs = GSet.to_list<>(xs) +// The.value<>(xs) + +// // `map` applies the provided function to all elements +// // in the set +// GSet.tests.10 : The(List(Nat), [2,3,4]) +// def xs = [1,2,3] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def xs = GSet.map<,>(Nat.add(1), xs) +// def xs = GSet.to_list<>(xs) +// The.value<>(xs) + +// GSet.tests.11 : The(Nat, 6) +// def xs = [1,2,3] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def r = GSet.foldr<,>(Nat.add, 0, xs) +// The.value<>(r) + +// // `intersection` returns a set whose elements are +// // common in both sets +// GSet.tests.12 : The(List(Nat), [2]) +// def xs = [1,2,3] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def ys = [2,4,5] +// def ys = GSet.from_list<>(Nat.cmp, ys) +// def r = GSet.intersection<>(Nat.cmp, xs, ys) +// def r = GSet.to_list<>(r) +// The.value<>(r) + +// // `union` +// GSet.tests.13 : The(List(Nat), [1,2,3,4,5,6]) +// def xs = [1,2,3] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def ys = [4,5,6] +// def ys = GSet.from_list<>(Nat.cmp, ys) +// def r = GSet.union<>(Nat.cmp, xs, ys) +// def r = GSet.to_list<>(r) +// The.value<>(r) + +// // `union` does not repeat elements +// GSet.tests.14 : The(List(Nat), [1,2,3,4,5]) +// def xs = [1,2,3] +// def xs = GSet.from_list<>(Nat.cmp, xs) +// def ys = [3,4,5] +// def ys = GSet.from_list<>(Nat.cmp, ys) +// def r = GSet.union<>(Nat.cmp, xs, ys) +// def r = GSet.to_list<>(r) +// The.value<>(r) + +// // `difference` returns a set with elements which are +// // present in the first set, but not in the second +// // TODO: check why this test started to fail after updating the syntax +// // GSet.tests.15 : The(List(Nat), [1,2,3]) +// // def xs = GSet.from_list<>(Nat.cmp, [1,2,3,4,5]) +// // def ys = GSet.from_list<>(Nat.cmp, [4,5,6]) +// // def d = GSet.difference<>(Nat.cmp, xs, ys) +// // def d = GSet.to_list<>(d) +// // The.value<>(d) + +// // balance +// GSet.tests.16 : IO(Unit) +// let set = +// GSet.bin<> +// | 7; +// | 1; +// | GSet.tip<>; +// | GSet.bin<> +// | 6; +// | 2; +// | GSet.tip<>; +// | GSet.bin<> +// | 5; +// | 3; +// | GSet.tip<>; +// | GSet.bin<> +// | 4; +// | 4; +// | GSet.tip<>; +// | GSet.bin<> +// | 3; +// | 5; +// | GSet.tip<>; +// | GSet.bin<> +// | 2; +// | 6; +// | GSet.tip<>; +// | GSet.bin<> +// | 1; +// | 7; +// | GSet.tip<>; +// | GSet.tip<>; +// ; +// ; +// ; +// ; +// ; +// ; + +// case set { +// tip: IO.print("it's not empty..."), +// bin: +// let after = GSet.balance<>(set.val, set.left, set.right) +// IO.print(Bool.show(GSet.is_balanced<>(after))) +// } + + + + diff --git a/src/Image3D.fm b/src/Image3D.fm new file mode 100644 index 0000000..4a1796d --- /dev/null +++ b/src/Image3D.fm @@ -0,0 +1,87 @@ +// An Image3D contains `size` 3d pixels (voxels). Each pixel has a 24-bit +// position and a 24-bit color. It is stored on the buffer as follows: +// buffer[0] = voxel0.pos +// buffer[1] = voxel0.col +// buffer[2] = voxel1.pos +// buffer[3] = voxel1.col +// buffer[4] = voxel2.pos +// buffer[5] = voxel2.col +// And so on. Positions and colors are `U32`, interpreted as `Pos32` / `Col32`. +type Image3D { + new(length: U32, capacity: U32, buffer: Buffer32) +} + +// Image3D.alloc_capacity(capacity: U32): Image3D +// let buffer = Buffer32.alloc(U32.needed_depth(U32.mul(2u,capacity))) +// Image3D.new(0u, capacity, buffer) + +// Image3D.clear(img: Image3D): Image3D +// Image3D.set_length(0u, img) + +Image3D.get_capacity(img: Image3D): U32 + open img + img.capacity + +// Image3D.get_col(idx: U32, vox: Image3D): U32 +// open vox +// Buffer32.get(U32.add(U32.mul(idx,2u),1u), vox.buffer) + +Image3D.get_length(img: Image3D): U32 + open img + img.length + +// Image3D.get_pos(idx: U32, vox: Image3D): U32 +// open vox +// Buffer32.get(U32.mul(idx,2u), vox.buffer) + +// Image3D.parse(voxdata: String): Image3D +// let siz = U32.div(U32.length(voxdata), 12u) +// let img = Image3D.alloc_capacity(siz); +// U32.for(img, 0u, siz) +// | (i, img) +// let x = Image3D.parse_byte(U32.add(U32.mul(i, 6u), 0u), voxdata) +// let y = Image3D.parse_byte(U32.add(U32.mul(i, 6u), 1u), voxdata) +// let z = Image3D.parse_byte(U32.add(U32.mul(i, 6u), 2u), voxdata) +// let r = Image3D.parse_byte(U32.add(U32.mul(i, 6u), 3u), voxdata) +// let g = Image3D.parse_byte(U32.add(U32.mul(i, 6u), 4u), voxdata) +// let b = Image3D.parse_byte(U32.add(U32.mul(i, 6u), 5u), voxdata) +// let pos = Pos32.new(x,y,z) +// let col = Col32.new(r,g,b,255u) +// let img = Image3D.push(pos, col, img) +// img; + +// Image3D.parse_byte(idx: U32, voxdata: String): U32 +// let chr = U32.slice(U32.mul(idx,2u), U32.add(U32.mul(idx,2u),2u), voxdata) +// U32.read_base(16u, chr) + +// Image3D.push(pos: U32, col: U32, img: Image3D): Image3D +// open img +// let idx = img.length +// let img = Image3D.set_pos(idx, pos, img) +// let img = Image3D.set_col(idx, col, img) +// let img = Image3D.set_length(U32.add(img.length, 1u), img) +// img + + +// Sets position and color of the idx voxel of an Image3D +// Image3D.set(idx: U32, pos: U32, col: U32, img: Image3D): Image3D +// let img = Image3D.set_pos(idx, pos, img) +// let img = Image3D.set_col(idx, col, img) +// img + +// // Sets the color of the idx voxel of an Image3D +// Image3D.set_col(idx: U32, col: U32, img: Image3D): Image3D +// open img +// let img.buffer = Buffer32.set(U32.add(U32.mul(idx,2u),1u), col, img.buffer) +// Image3D.new(img.length, img.capacity, img.buffer) + +Image3D.set_length(length: U32, img: Image3D): Image3D + open img + Image3D.new(length, img.capacity, img.buffer) + +// // Sets the position of the idx voxel of an Image3D +// Image3D.set_pos(idx: U32, pos: U32, img: Image3D): Image3D +// open img +// let img.buffer = Buffer32.set(U32.mul(idx,2u), pos, img.buffer) +// Image3D.new(img.length, img.capacity, img.buffer) + diff --git a/src/Int.fm b/src/Int.fm new file mode 100644 index 0000000..ba8569f --- /dev/null +++ b/src/Int.fm @@ -0,0 +1,102 @@ +// An integer is a pair of nats quotiented by `(suc x, suc y) ~ (x, y)` +Int: Type + int Type> -> + (new: (x: Nat) -> (y: Nat) -> P(Int.new(x, y))) -> + P(int) + +Int.new(x: Nat, y: Nat): Int +

(new) + case x { + zero: new(Nat.zero, y), + succ: case y { + zero: new(Nat.succ(x.pred), Nat.zero), + succ: Int.new(Nat.sub(x.pred, y.pred), Nat.sub(y.pred, x.pred))

(new), + } : P(Int.new(Nat.succ(x.pred), y)) + } : P(Int.new(x, y)) + +Int.add(a: Int, b: Int): Int + open a + open b + Int.new(Nat.add(a.x, b.x), Nat.add(a.y, b.y)) + + +Int.0: Int + Int.from_nat(0) + +Int.1: Int + Int.from_nat(1) + +Int.cmp(a: Int, b: Int): Cmp + open a + open b + Nat.cmp(Nat.add(a.x, b.y), Nat.add(b.x, a.y)) + +Int.div_nat(a: Int, n: Nat): Int + open a + Int.new(Nat.div(a.x, n), Nat.div(a.y, n)) + +Int.eql(a: Int, b: Int): Bool + case Int.cmp(a, b) { + ltn: Bool.false, + eql: Bool.true, + gtn: Bool.false, + } + +Int.from_nat(n: Nat): Int + Int.new(n, 0) + +Int.mod_nat(a: Int, n: Nat): Nat + open a + let b = Nat.mod(a.y, n) + let sum = Nat.add(a.x, Nat.sub(n, b)) + Nat.mod(sum, n) + +Int.mul(a: Int, b: Int): Int + open a + open b + Int.new(Nat.add(Nat.mul(a.x, b.x), Nat.mul(a.y, b.y)), Nat.add(Nat.mul(a.x, b.y), Nat.mul(a.y, b.x))) + +Int.neg(a: Int): Int + open a + Int.new(a.y, a.x) + +// Int.parse_decimal(str: String): Int +// case str { +// nil: Int.0, +// cons: U16.eql(str.head, '-')<() Int>( +// Int.new(0, Nat.parse_decimal(str.tail)), +// Int.new(Nat.parse_decimal(String.cons(str.head, str.tail)), 0)), +// } + +// Int.parse_hex(str: String): Int +// case str { +// nil: Int.0, +// cons: case U16.eql(str.head, '-') { +// true: +// let b = Nat.parse_hex(str.tail) +// Int.new(0, b), +// false: +// let a = Nat.parse_hex(String.cons(str.head, str.tail)) +// Int.new(a, 0), +// } +// } + +Int.sub(a: Int, b: Int): Int + Int.add(a, Int.neg(b)) + +// true is negative, false otherwise +Int.to_nat(a: Int): Pair(Bool, Nat) + open a + case a.y { + zero: Pair.new<_,_>(Bool.false, a.x), + succ: Pair.new<_,_>(Bool.true, a.y), + } + + +Int.to_string_base(base: Nat, a: Int): String + open a + case a.y { + zero: Nat.to_string_base(base, a.x), + succ: String.cons('-', Nat.to_string_base(base, a.y)), + } + diff --git a/src/Is.fm b/src/Is.fm new file mode 100644 index 0000000..f3105c1 --- /dev/null +++ b/src/Is.fm @@ -0,0 +1,6 @@ +Is(a : Bool): Type + Equal(Bool,Bool.true,a) + +Is.tis : Is(Bool.true) + Equal.refl<_,_> + diff --git a/src/JSON.fm b/src/JSON.fm new file mode 100644 index 0000000..415af22 --- /dev/null +++ b/src/JSON.fm @@ -0,0 +1,9 @@ +// JavaScript Object Notation. +type JSON { + null, + bool(x: Bool), + number(x: F64), + string(x: String), + array(x: List(JSON)), + object(x: List(Pair(String, JSON))) +} diff --git a/src/List.fm b/src/List.fm index 6f25bfb..b9456b9 100644 --- a/src/List.fm +++ b/src/List.fm @@ -3,12 +3,14 @@ type List { cons(head: A, tail: List(A)), } +// Get the tail of a nonempty list List.tail(xs: List(A)): List(A) - case xs { - nil: List.nil<_>, - cons: xs.tail, + case xs{ + nil : List.nil<_> + cons: xs.tail } +// Returns the first elements of a list, discards the rest. List.take(n: Nat, xs: List(A)): List(A) case xs { nil : List.nil<_>, @@ -18,6 +20,130 @@ List.take(n: Nat, xs: List(A)): List(A) } } +// Return elements while a condition is true +List.take_while(f: A -> Bool, xs: List(A)) : List(A) + case xs{ + nil : List.nil<_> + cons: case f(xs.head){ + true : List.cons<_>(xs.head,List.take_while<_>(f, xs.tail)) + false: List.nil<_> + } + } + +// Appends element to the end of the list. +List.append(as: List(A), a: A): List(A) + case as{ + nil : List.pure<_>(a) + cons: List.cons<_>(as.head,List.append<_>(as.tail, a)) + } + +// A list with only one element. +List.pure(x: A): List(A) + List.cons(x)(List.nil) + +// Removes the first elements of a list. +List.drop(n: Nat, xs: List(A)): List(A) + case n{ + zero: xs + succ: case xs{ + nil: List.nil<_> + cons: List.drop<_>(n.pred,xs.tail) + } + } + +// Remove elements while a condition is true +List.drop_while(f: A -> Bool, xs: List(A)): List(A) + case xs{ + nil : List.nil<_> + cons: case f(xs.head){ + true : List.drop_while<_>(f,xs.tail) + false: xs + } + } + +// Removes an element from the list at given index. +List.delete_at(idx: Nat, list: List(A)): List(A) + case idx{ + zero: List.tail(list) + succ: case list{ + nil : list + cons: List.cons(list.head, List.delete_at(idx.pred, list.tail)) + } + } + +// Updates the element at given position +List.update_at(index: Nat, fn: A -> A, list: List(A)): List(A) + case list{ + nil : List.nil<_> + cons: case index{ + zero: List.cons<_>(fn(list.head), list.tail) + succ: List.cons<_>(list.head, List.update_at(index.pred, fn, list.tail)) + } + } + +// Do all elements satisfy a condition? +List.all(cond: A -> Bool, list: List(A)): Bool + case list{ + nil : Bool.true + cons: case cond(list.head){ + true : List.all<_>(cond, list.tail) + false: Bool.false + } + } + +// Do any element satisfy a condition? +List.any(cond: A -> Bool, list: List(A)): Bool + case list{ + nil : Bool.false + cons: case cond(list.head){ + true : Bool.true + false: List.any<_>(cond, list.tail) + } + } + +// Are all elements true? +List.and(list: List(Bool)): Bool + List.all<_>((x) x, list) + +//Finds the first occurrence that satisfies a condition +List.find(cond: A -> Bool, xs: List(A)): Maybe(A) + case xs{ + nil : Maybe.none<_> + cons: case cond(xs.head){ + true : Maybe.some<_>(xs.head) + false: List.find<_>(cond, xs.tail) + } + } + +// insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]` +List.intersperse(sep: A, xs: List(A)): List(A) + case xs{ + nil : List.nil<_> + cons: case xs.tail{ + nil : List.pure<_>(xs.head) + cons: List.cons<_>(xs.head,List.cons<_>(sep,List.intersperse(sep,xs.tail))) + } + } + +// insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]` +List.intercalate(sep: List(A), xs: List(List(A))): List(A) + List.flatten(List.intersperse(sep,xs)) + +// Shows a list as String +List.show(f: A -> String, xs: List(A)): String + String.flatten(["[",String.intercalate(",", List.map<_,_>(f,xs)),"]"]) + +// Removes all elements that do not satisfy a condition. +List.filter(f: A -> Bool, xs: List(A)): List(A) + case xs{ + nil : List.nil<_> + cons: case f(xs.head){ + true : List.cons<_>(xs.head,List.filter<_>(f, xs.tail)) + false: List.filter<_>(f, xs.tail) + } + } + +// Converts a list to its non-inductive Church encoding. List.fold(list: List(A)): -> P -> (A -> P -> P) -> P

(nil, cons) case list { @@ -25,18 +151,42 @@ List.fold(list: List(A)): -> P -> (A -> P -> P) -> P cons: cons(list.head, List.fold(list.tail)

(nil, cons)) } +// Given two lists `xs` and `ys`, applies `f(xs[i],ys[i])` for all `i`. +List.fold_zip(as: List(A), bs: List(B))(fn: A -> B -> C, nil: C, cons: C -> C -> C): C + case as { + nil : nil, + cons: case bs { + nil : nil, + cons: cons(fn(as.head, bs.head), List.fold_zip(as.tail,bs.tail)(fn, nil, cons)) + } + } + +List.foldr(b: B, f: A -> B -> B, xs: List(A)): B + List.fold(xs)(b,f) + +//List.fold1(xs: List(A))(xs)> + //: -> P -> (A -> P -> P) -> P + //

(nil, cons) + //case xs: + //with ne : List.not_empty<_>(xs.self) = ne; + //| Empty.absurd<_>(ne); + //| List.fold<_>(xs)

(nil,cons); + +// Folds over a list, left associative. List.for(xs: List(A))(b: B, f: A -> B -> B): B case xs { nil : b, cons: List.for(xs.tail)(f(xs.head,b),f) } +// Applies a function to all elements of the list. List.map(f: A -> B, as: List(A)): List(B) case as { nil: List.nil<_>, cons: List.cons<_>(f(as.head), List.map<_,_>(f,as.tail)), } +// Reverse the order of the elements of the list. List.reverse(xs: List(A)) : List(A) List.reverse.go<_>(xs,List.nil<_>) @@ -46,18 +196,21 @@ List.reverse.go(xs: List(A), res: List(A)): List(A) cons: List.reverse.go<_>(xs.tail,List.cons<_>(xs.head,res)) } +// Concatenates two lists. List.concat(as: List(A), bs: List(A)): List(A) case as { nil: bs, cons: List.cons<_>(as.head, List.concat<_>(as.tail,bs)) } +// Flattens a list of lists into a single list. List.flatten(xs: List(List(A))): List(A) case xs { nil: List.nil<_>, cons: List.concat<_>(xs.head, List.flatten<_>(xs.tail)) } +// Verify if a list is empty. List.is_empty(list: List(A)): Bool case list { nil: Bool.true, @@ -75,7 +228,7 @@ List.length.go(xs: List(A), n: Nat): Nat cons: List.length.go(xs.tail, Nat.succ(n)) } -// A range of nats +// A range of nats. List.range.nat.go(nat: Nat, list: List(Nat)): List(Nat) case nat { zero: list, @@ -85,6 +238,7 @@ List.range.nat.go(nat: Nat, list: List(Nat)): List(Nat) List.range.nat(nat: Nat): List(Nat) List.range.nat.go(nat, List.nil<_>) +// Compares the equality of two lists. List.eql(eql: A -> A -> Bool, a: List(A), b: List(A)): Bool case a { nil: case b { @@ -97,12 +251,24 @@ List.eql(eql: A -> A -> Bool, a: List(A), b: List(A)): Bool }, } +// Removes the first elements of a list. +List.drop(n: Nat, xs: List(A)): List(A) + case n { + zero: xs + succ: case xs { + nil : List.nil<_> + cons: List.drop<_>(n.pred,xs.tail) + } + } + +// Apply a function f to transform a List(A) into a List(B). List.mapped(as: List(A))(f: A -> B): List(B) case as { nil: List.nil<_>, cons: List.cons<_>(f(as.head),List.mapped(as.tail)(f)) } +// Returns the element at given position. List.at(index: Nat, list: List(A)): Maybe(A) case list { nil: Maybe.none<_>, @@ -112,6 +278,7 @@ List.at(index: Nat, list: List(A)): Maybe(A) } } +// Returns the element at given position, backwards. List.at_last(index: Nat, list: List(A)): Maybe(A) List.at(index, List.reverse<_>(list)) @@ -123,6 +290,17 @@ List.init(list: List(A)): List(A) }, nil: List.nil<_>, } + +List.split_at(n : Nat, xs: List(A)) : Pair(List(A),List(A)) + case xs { + nil : { List.nil<_>, List.nil<_> }, + cons: case n { + zero: { List.nil<_>, xs }, + succ: + open List.split_at<_>(n.pred, xs.tail) as res + { List.cons<_>(xs.head, res.fst), res.snd } + } + } List.zip(as: List(A), bs: List(B)): List(Pair(A,B)) case as { @@ -132,3 +310,371 @@ List.zip(as: List(A), bs: List(B)): List(Pair(A,B)) cons: List.cons<_>(Pair.new<_,_>(as.head, bs.head), List.zip(as.tail, bs.tail)), } } + +// The functor instance for list +// List.functor: Functor(List) +// Functor.new(List.map) + +// // Proof that List.functor conforms to the functor laws +// List.functor.verified: VerifiedFunctor(List, List.functor) +// VerifiedFunctor.new(List.map.id, List.map.comp) + +// May get the head of a list +List.head(xs: List(A)): Maybe(A) + case xs { + nil : Maybe.none<_>, + cons: Maybe.some<_>(xs.head) + } + +// May get the head of a list +List.head_with_default(default: A, xs: List(A)): A + case xs { + nil : default, + cons: xs.head + } + +// Finds the first element that satisfies a condition and its index. +List.ifind(xs: List(A), f: A -> Nat -> Bool): Maybe(Pair(A,Nat)) + List.ifind.go(xs,f,Nat.zero) + +List.ifind.go(xs: List(A), f: A -> Nat -> Bool, i: Nat): Maybe(Pair(A,Nat)) + case xs { + nil : Maybe.none<_>, + cons: case f(xs.head,i) { + true : Maybe.some<_>(Pair.new<_,_>(xs.head)(i)), + false: List.ifind.go<_>(xs.tail,f,Nat.succ(i)) + } + } + +// Folds over a list with an index, right associative +// List.ifoldr.u32(b: B, f: U32 -> A -> B -> B, xs: List(A)): B +// case xs { +// nil : b, +// cons: f(0u, xs.head, List.ifoldr.u32<_,_>(b, (i) f(U32.add(1u, i)), xs.tail)) +// } + +// Folds over a list, left associative +// List.ifor(xs: List(A))(b: B, f: Nat -> A -> B -> B): B +// case xs { +// nil : b, +// cons: List.ifor(xs.tail)(f(0,xs.head,b), (n) f(Nat.succ(n))) +// } + +// Folds over a list, left associative +// List.ifor.u32(xs: List(A))(b: B, f: U32 -> A -> B -> B): B +// case xs { +// nil : b, +// cons: List.ifor.u32(xs.tail)(f(0u,xs.head,b), (n) f(U32.add(n,1u))) +// } + +// Map over a list with the index +List.imap(f: Nat -> A -> B, xs: List(A)): List(B) + case xs { + nil : List.nil<_>, + cons: List.cons<_>(f(0,xs.head),List.imap<_,_>((n) f(Nat.succ(n)),xs.tail)) + } + +// Adds the index of each element in a list +List.indices(xs: List(A)): List(Pair(Nat,A)) + List.imap((i,x) {i,x}, xs) + +// Adds the index of each element in a list +List.indices.u32(xs: List(A)): List(Pair(U32,A)) + List.imap((i,x) {Nat.to_u32(i),x}, xs) + +// Get the all elements of a nonempty list except the last one +// List.init(xs: List(A), not_empty: List.not_empty(xs)) : List(A) +// case xs: +// with ne : List.not_empty(xs.self) = not_empty; +// | Empty.absurd<_>(ne); +// | case xs.tail: +// with e : Equal(_, xs.tail.self,xs.tail) = Equal.to; +// | List.nil<_>; +// | def cne = List.cons_isnt_empty(xs.tail.head,xs.tail.tail) +// def xne = Equal.rewrite<_,_,_,(x) List.not_empty(x)>(e,cne) +// List.cons<_>(xs.head,List.init<_>(xs.tail,xne));; + +// concrete implementation of insertion sort for nats +List.insert_sort_nat(ns: List(Nat)): List(Nat) + List.foldr<_,_>(List.nil<_>, List.insert_sort_nat.aux, ns) + +List.insert_sort_nat.aux(n: Nat, ns: List(Nat)): List(Nat) + open List.span<_>(Nat.lte(n), ns) as spanned + List.concat<_>(spanned.fst, List.cons<_>(n, spanned.snd)) + + +List.span(f: A -> Bool, xs: List(A)): Pair(List(A),List(A)) + case xs { + nil : {List.nil<_>, List.nil<_>}, + cons: case f(xs.head) { + true: + open List.span<_>(f, xs.tail) as spanned + { List.cons<_>(xs.head, spanned.fst), spanned.snd } + false: { List.nil<_>, xs } + } + } + +// Add the total of a list of natural numbers +List.sum(xs: List(Nat)) : Nat + List.sum.go(xs, Nat.zero) + +List.sum.go(xs: List(Nat), n: Nat) : Nat + case xs { + nil : n, + cons: List.sum.go(xs.tail,Nat.add(xs.head,n)) + } + +// concatenate two list builders +List.Builder.concat(a: List.Builder(A), b: List.Builder(A)): List.Builder(A) + (x) a(b(x)) + +// prepend an element +List.Builder.cons(c: A, lb: List.Builder(A)) : List.Builder(A) + (x) List.cons<_>(c,lb(x)) + +// A lazy List constructor, useful for efficient concatenation +List.Builder(A: Type): Type + List(A) -> List(A) + +// construct a new builder (it's just the identity function) +List.Builder.new : List.Builder(A) + (x) x + +// append an element +List.Builder.snoc(c: A, lb: List.Builder(A)) : List.Builder(A) + (x) lb(List.cons<_>(c,x)) + +// The bind function of the list Monad. +List.bind(xs: List(A), f: A -> List(B)): List(B) + List.flatten<_>(List.map<_,_>(f, xs)) + +List.chunk(n: Nat, xs: List(A)): Maybe(List(A)) + case n { + zero: Maybe.some<_>(List.nil<_>), + succ: case xs { + nil : Maybe.none<_>, + cons: Maybe.bind<_,_>(List.chunk<_>(n.pred,xs.tail), + (x) Maybe.some<_>(List.cons<_>(xs.head,x))) + } + } + +List.chunks_of(len: Nat, xs: List(A)): List(List(A)) + List.chunks_of.go<_>(len, xs, len, List.nil<_>) + +List.chunks_of.go( + len : Nat, // length of each chunk + list : List(A), // list to be split + need : Nat, // number of vals to complete chunk + chunk : List(A) // current chunk +) : List(List(A)) + case list { + nil : List.cons<_>(List.reverse<_>(chunk), List.nil<_>), + cons: case need { + zero: + let head = List.reverse<_>(chunk) + let tail = List.chunks_of.go<_>(len, list, len, List.nil<_>) + List.cons<_>(head, tail), + succ: + let chunk = List.cons<_>(list.head, chunk) + List.chunks_of.go<_>(len, list.tail, need.pred, chunk) + } + } + +// Proof that List.cons(f(x)) & List.map(f, xs) commute +List.commute_cons_map(a :A, ls: List(A), f: A -> B) + : Equal(List(B), + List.cons(f(a), List.map(f, ls)), + List.map(f, List.cons(a, ls))) + case ls { + nil : Equal.refl<_,_> + cons: Equal.refl<_,_> + } : Equal(_, List.cons<_>(f(a), List.map<_,_>(f, ls)), List.map<_,_>(f, List.cons<_>(a, ls))) + + +// The monad instance for list +List.monad: Monad(List) + Monad.new(List.bind, List.pure) + +// A theorem that a list made with List.cons is not the empty list +// List.cons_isnt_empty( +// x:A, +// xs: List(A) +// ): List.not_empty(List.cons(x,xs)) +// def y = List.cons(x,xs) + //case y: + //with e : Equal(List(A),y,y.self) = Equal.to; + //| Empty.absurd<>(List.cons_isnt_nil(x,xs,e)); + //| Unit.new; + +// A theorem that List.cons isn't List.nil +// List.cons_isnt_nil(x:A, xs: List(A)) +// : Not(Equal(List(A),List.cons(x,xs), List.nil)) +// def P = ((x) case x { nil: Empty, cons: Unit }) :: List(A) -> Type +// (e) Equal.rewrite(x,xs), List.nil,P>(e, Unit.new) + +// removes an element from the list at given index +// List.delete_at.u32(idx: U32, list: List(A)): List(A) +// if U32.eql(idx, 0u) then +// List.tail(list) +// else +// case list { +// nil : list, +// cons: List.cons(list.head, List.delete_at.u32(U32.sub(idx,1u), list.tail)) +// } + +// Removes an element from the list with a user-supplied equality predicate. +List.delete_by(p: A -> A -> Bool, a: A, as: List(A)): List(A) + case as { + nil : List.nil<_>, + cons: case p(a, as.head) { + true : List.delete_by<_>(p, a, as.tail), + false: List.cons<_>(as.head, List.delete_by<_>(p, a, as.tail)) + } + } + +// checks if an element occurs in the list with a user-supplied equality predicate +List.elem(p: A -> A -> Bool, a: A, as: List(A)): Bool + case as { + nil : Bool.false, + cons: case p(a, as.head) { + true : Bool.true, + false: List.elem(p, a, as.tail) + } + } + +// Finds the last element that satisfies a condition and its index. +List.find_last(xs: List(A), f: A -> Nat -> Bool): Maybe(Pair(A)(Nat)) + List.find_last.go(xs,f,Nat.zero,Maybe.none<_>) + +List.find_last.go( + xs: List(A), + f: A -> Nat -> Bool, + n: Nat, + res: Maybe(Pair(A,Nat)) +): Maybe(Pair(A,Nat)) + case xs { + nil : res, + cons: + let res = case f(xs.head,n) { + true : Maybe.some<_>(Pair.new<_,_>(xs.head,n)), + false: res + } + List.find_last.go<_>(xs.tail,f,Nat.succ(n),res) + } + +// Insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]`. +List.intercalate(sep: List(A), xs: List(List(A))): List(A) + List.flatten(List.intersperse(sep,xs)) + +// A list with only one element. +List.pure(x : A) : List(A) + List.cons(x)(List.nil) + +List.range(n: Nat): List(Nat) + List.range.go(n, List.nil<_>) + +List.range.go(n: Nat, xs: List(Nat)): List(Nat) + case n { + zero: xs, + succ: List.range.go(n.pred, List.cons<_>(n, xs)) + } + +// insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]` +List.intercalate(sep: List(A), xs: List(List(A))): List(A) + List.flatten(List.intersperse(sep,xs)) + +// Insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]`. +List.intersperse(sep: A, xs: List(A)): List(A) + case xs { + nil : List.nil<_>, + cons: case xs.tail { + nil : List.pure<_>(xs.head), + cons: List.cons<_>(xs.head,List.cons<_>(sep,List.intersperse(sep,xs.tail))) + } + } + +// Do any element satisfy a condition? +List.any(cond: A -> Bool, list: List(A)): Bool + case list { + nil: Bool.false, + cons: case cond(list.head) { + true: Bool.true, + false: List.any<_>(cond, list.tail), + } + } + +List.null(xs: List(A)) : Bool + case xs { + nil : Bool.true, + cons: Bool.false + } +// Is any element true? +List.or(list: List(Bool)): Bool + List.any<_>((x) x)(list) + +List.product(xs: List(Nat)) : Nat + List.product.go(xs, Nat.zero) + +List.product.go(xs: List(Nat), n: Nat) : Nat + case xs { + nil : Nat.zero, + cons: List.product.go(xs.tail,Nat.mul(xs.head,n)) + } + +// Turn a builder into a List. +List.run_builder(lb: List.Builder(A)): List(A) + lb(List.nil<_>) + +// List.subsequences(xs: List(A)): List(List(A)) +// List.cons<_>(List.nil<_>,List.subsequences.go<_>(xs)) + +// List.subsequences.go(xs: List(A)): List(List(A)) +// case xs { +// nil : List.nil<_>, +// cons: +// let f = ((ys,r) List.cons<_>(ys,List.cons<_>(List.cons<_>(xs.head,ys),r))) +// :: List(A) -> List(List(A)) -> List(List(A)) +// List.cons<_>( +// List.pure<_>(xs.head), +// List.foldr<_,_>(List.nil<_>,f,List.subsequences.go<_>(xs.tail)) +// ) +// } + +// Convert a list to a builder. +List.to_builder(list: List(A)) : List.Builder(A) + List.to_builder.go<_>(list, List.Builder.new<_>) + +List.to_builder.go(list: List(A), lb: List.Builder(A)) : List.Builder(A) + case list { + nil : lb, + cons: List.to_builder.go<_>(list.tail, List.Builder.snoc<_>(list.head, lb)) + } + +List.uncons(xs: List(A)): Maybe(Pair(A,List(A))) + case xs { + nil : Maybe.none<_>, + cons: Maybe.some<_>(Pair.new<_,_>(xs.head,xs.tail)) + } + + +List.unfoldr(f: A -> Maybe(Pair(A,B)), a: A): List(B) + List.unfoldr.go(f, a, List.nil) + +List.unfoldr.go(f: A -> Maybe(Pair(A,B)), a: A, bs: List(B)): List(B) + case f(a) as res { + none: List.nil, + some: + open res.value as pair + List.unfoldr.go(f, pair.fst, List.cons(pair.snd, bs)) + } + +// Given two lists `xs` and `ys`, applies `f(xs[i],ys[i])` for all `i`. +List.zip_with(f: A -> B -> C, as: List(A), bs: List(B)) + : List(C) + case as { + nil : List.nil<_>, + cons: case bs { + nil : List.nil<_>, + cons: List.cons<_>(f(as.head,bs.head),List.zip_with<_,_,_>(f,as.tail,bs.tail)) + } + } \ No newline at end of file diff --git a/src/Logic.fm b/src/Logic.fm new file mode 100644 index 0000000..8d425e4 --- /dev/null +++ b/src/Logic.fm @@ -0,0 +1,111 @@ +// !(P ∧ Q) => !P ∨ !Q +// Logic.And.forward( +// lem : Logic.ExcludedMiddle, +// not_pq: Not(And(P, Q)) +// ) : Or(Not(P), Not(Q)) +// lem

<() _> +// | (p) lem<() _> +// | (q) Logic.exfalso(not_pq(And.new<_,_>(p,q)), _); +// | (q) Or.rgt<_,_>(q);; +// | (p) Or.lft<_,_>(p); + +// // ¬P ∨ ¬Q -> ¬(P ∧ Q) +// Logic.And.reverse(or_not: Or(Not(A), Not(B))): Not(And(A,B)) +// (and) and<() _> | (a, b) +// or_not<() _> +// | (not_a) not_a(a); +// | (not_b) not_b(b);; + +Logic.ExcludedMiddle: Type + -> Or(P,Not(P)) + +// ¬(P ∨ Q) -> ¬P ∧ ¬Q +Logic.Or.forward(x: Not(Or(A,B))): And(Not(A),Not(B)) + And.new<_,_>((a) x(Or.lft<_, _>(a)), (b) x(Or.rgt<_, _>(b))) + +// ¬P ∧ ¬Q -> ¬(P ∨ Q) +// Logic.Or.reverse(x: And(Not(A), Not(B))): Not(Or(A, B)) +// (or) or<() _> +// | (a) x<() _>((not_a, not_b) not_a(a)); +// | (b) x<() _>((not_a, not_b) not_b(b)); + +// // (P -> Q) ∧ (R -> S) ∧ (P ∨ ¬S) |- (Q ∨ ¬R) +// Logic.bidirectional_dilemma( +// f: P -> Q, +// g: R -> S, +// c: Or(P,Not(S)) +// ) : Or(Q,Not(R)) +// c<() _> +// | (x) Or.lft<_,_>(f(x)); +// | (x) Or.rgt<_,_>((r) x(g(r))); + +Logic.composition(f: P -> Q, g: P -> R, p: P): And(Q,R) + And.new<_,_>(f(p),g(p)) + +// // (P -> Q) ∧ (R -> S) ∧ (P ∨ R) |- (Q ∨ S) +// Logic.constructive_dilemma( +// f: P -> Q, +// g: R -> S, +// c: Or(P,R) +// ) : Or(Q,S) +// c<() _> +// | (x) Or.lft<_,_>(f(x)); +// | (x) Or.rgt<_,_>(g(x)); + +// (P -> Q) -> (¬Q -> ¬P) +Logic.contrapositive(f: P -> Q) : Not(Q) -> Not(P) + (x) (p) x(f(p)) + +// // (P -> Q) ∧ (R -> S) ∧ (¬Q ∨ ¬S) |- (¬P ∨ ¬R) +// Logic.destructive_dilemma( +// f: P -> Q, +// g: R -> S, +// c: Or(Not(Q),Not(S)) +// ) : Or(Not(P),Not(R)) +// c<() _> +// | (x) Or.lft<_,_>((p) x(f(p))); +// | (x) Or.rgt<_,_>((r) x(g(r))); + +// // Modus tollendo ponens: ((P ∨ Q) ∧ ¬P) |- Q +// Logic.disjunctive_syllogism(c: Or(P,Q), not_p: Not(P)) : Q +// c<() Q> +// | (x) Empty.absurd<>(not_p(x)); +// | (x) x; + +Logic.double_negation(p:P): Not(Not(P)) + (notP) notP(p) + +Logic.exfalso(x: Empty,P: Type): P + Empty.absurd<_>(x) + +Logic.hypothetical_syllogism( + f: P -> Q, + g: Q -> R, + x: P +) : R + g(f(x)) + +// (P -> Q) ∧ P |- Q +Logic.modus_ponens(implies: P -> Q, p: P) : Q + implies(p) + +// (P -> Q) ∧ ¬Q |- ¬P +Logic.modus_tollens(implies: P -> Q, not_q: Not(Q)) : Not(P) + (x) not_q(implies(x)) + +// Logic.negation_elimination( +// lem: Logic.ExcludedMiddle, +// not_not_p: Not(Not(P)) +// ): P +// lem

<() _> +// | (x) x; +// | (x) Logic.exfalso(not_not_p(x),P); + +// // ¬(P ∧ ¬P) +// Logic.noncontradiction: Not(And(P,Not(P))) +// (contra) contra<() _> +// | (p) (not_p) not_p(p); + +Logic.transposition(f: P -> Q, not_q: Not(Q)): Not(P) + (p) not_q(f(p)) + diff --git a/src/Map.fm b/src/Map.fm index 6fa3a30..3385e87 100644 --- a/src/Map.fm +++ b/src/Map.fm @@ -109,3 +109,201 @@ Map.values.go(xs: Map(A), list: List(A)): List(A) list2 } +Map.disj(a: Map(A), b: Map(A)): Bool + case a { + new: Bool.true, + tie: case b { + new: Bool.true, + tie: + let v = case a.val { + none: Bool.true, + some: case b.val { + none: Bool.true, + some: Bool.false + } + } + Bool.and(v, Bool.and(Map.disj<_>(a.lft, b.lft), Map.disj<_>(a.rgt, b.rgt))) + } + } + +// Returns the element stored at a given key and a copy of the map. +// Map.lookup(bits: Bits, val: A, map: Map(A)): Pair(A, Map(A)) +// case bits { +// e: case map { +// new: +// let map = Map.tie(Maybe.some(val), Map.new, Map.new) +// Pair.new(val, map), +// tie: +// let value = Maybe.extract(map.val, val) +// let map = Map.tie(Maybe.some(value), map.lft, map.rgt) +// Pair.new(value, map), +// }, +// o: case map { +// new: +// // get p.fst p.snd = Map.lookup(bits.pred, val, Map.new) +// let p = Map.lookup(bits.pred, val, Map.new) +// case p{ +// new: Pair.new(p.fst, Map.tie(Maybe.none, p.snd, Map.new)) +// } +// tie: +// // get p.fst p.snd = Map.lookup(bits.pred, val, map.lft) +// let p = Map.lookup(bits.pred, val, map.lft) +// case p{ +// new: Pair.new(p.fst, Map.tie(map.val, p.snd, map.rgt)) +// } +// }, +// i: case map { +// new: +// // get p.fst p.snd = Map.lookup(bits.pred, val, Map.new) +// let p = Map.lookup(bits.pred, val, Map.new) +// case p{ +// new: Pair.new(p.fst, Map.tie(Maybe.none, Map.new, p.snd)) +// } +// tie: +// // get p.fst p.snd = Map.lookup(bits.pred, val, map.rgt) +// let p = Map.lookup(bits.pred, val, map.rgt) +// case p { +// new: Pair.new(p.fst, Map.tie(map.val, map.lft, p.snd)) +// } +// } +// } + +Map.map(fn: A -> B, map: Map(A)): Map(B) + case map { + new: Map.new<_>, + tie: + let val = case map.val { + none: Maybe.none<_>, + some: Maybe.some<_>(fn(map.val.value)) + } + let lft = Map.map(fn, map.lft) + let rgt = Map.map(fn, map.rgt) + Map.tie<_>(val, lft, rgt) + } + +// general merge function +Map.merge( + a_not_b : Bits -> A -> Maybe(C), + b_not_a : Bits -> B -> Maybe(C), + a_and_b : Bits -> A -> B -> Maybe(C), + a: Map(A), + b: Map(B) +) : Map(C) + Map.merge.go<_,_,_>(a_not_b,b_not_a,a_and_b,Bits.e,a,b) + +Map.merge.go( + f: Bits -> A -> Maybe(C), + g: Bits -> B -> Maybe(C), + h: Bits -> A -> B -> Maybe(C), + key: Bits, + a: Map(A), + b: Map(B) +) : Map(C) + case a { + new: case b { + new: Map.new<_>, + tie: + let val = case b.val as bv { + none: Maybe.none<_>, + some: g(key,bv.value) + } + Map.tie<_>(val, + Map.merge.go<_,_,_>(f, g, h, Bits.o(key), Map.new<_>,b.lft), + Map.merge.go<_,_,_>(f, g, h, Bits.i(key), Map.new<_>,b.rgt)) + }, + tie: case b { + new: + let val = case a.val as av { + none: Maybe.none<_>, + some: f(key, av.value) + } + Map.tie<_>(val, + Map.merge.go<_,_,_>(f,g,h,Bits.o(key),a.lft,Map.new<_>), + Map.merge.go<_,_,_>(f,g,h,Bits.i(key),a.rgt,Map.new<_>)), + tie: + let val = case a.val as av { + none: case b.val as bv { + none: Maybe.none<_>, + some: g(key, bv.value) + }, + some: case b.val as bv { + none: f(key, av.value), + some: h(key, av.value, bv.value) + } + } + Map.tie<_>(val, + Map.merge.go<_,_,_>(f, g, h, Bits.o(key), a.lft, b.lft), + Map.merge.go<_,_,_>(f, g, h, Bits.i(key), a.rgt, b.rgt)) + } + } + +// Modifies the element at a given key, returns it and a copy of the map. +// This used to be important on linear back-ends, but it isn't linear anymore. +// TODO: use `with` to make this function linear again. +Map.query(cpy: A -> Pair(A, A), bits: Bits, map: Map(A)): Pair(Map(A), Maybe(A)) + case bits { + e: case map { + new: + let map = Map.new<_> + let val = Maybe.none<_> + Pair.new<_,_>(map, val), + tie: case map.val { + none: + let map = Map.tie<_>(Maybe.none<_>, map.lft, map.rgt) + let val = Maybe.none<_> + Pair.new<_,_>(map, val), + some: case cpy(map.val.value) as p { + new: + let map = Map.tie<_>(Maybe.some<_>(p.fst), map.lft, map.rgt) + let val = Maybe.some<_>(p.snd) + Pair.new<_,_>(map, val) + } + } + }, + o: case map { + new: + let map = Map.new<_> + let val = Maybe.none<_> + Pair.new<_,_>(map, val), + tie: case Map.query<_>(cpy, bits.pred, map.lft) as p { + new: + let map = Map.tie<_>(map.val, p.fst, map.rgt) + let val = p.snd + Pair.new<_,_>(map, val) + } + }, + i: case map { + new: + let map = Map.new<_> + let val = Maybe.none<_> + Pair.new<_,_>(map, val), + tie: case Map.query<_>(cpy, bits.pred, map.rgt) as p { + new: + let map = Map.tie<_>(map.val, map.lft, p.fst) + let val = p.snd + Pair.new<_,_>(map, val) + } + } + } + + +Map.Row(A : Type,key: Bits, x: A, xs: Map(A)) : Type + case Map.get(key,xs) as v { + none: Empty, + some: Equal(A,x,v.value) + } + +// combines two maps, preferring the left-hand map in case of duplicates entries +Map.union(a: Map(A), b: Map(A)): Map(A) + case a { + new: b, + tie: case b { + new: a, + tie: case a.val { + none: Map.tie<_>(b.val, Map.union<_>(a.lft,b.lft), Map.union<_>(a.rgt,b.rgt)), + some: Map.tie<_>(a.val, Map.union<_>(a.lft,b.lft), Map.union<_>(a.rgt,b.rgt)) + } + } + } + + diff --git a/src/Maybe.fm b/src/Maybe.fm index 00b384c..2140720 100644 --- a/src/Maybe.fm +++ b/src/Maybe.fm @@ -45,3 +45,61 @@ Maybe.or(a: Maybe(A), b: Maybe(A)): Maybe(A) some: Maybe.some<_>(a.value), } +Maybe.map(f: A -> B, m: Maybe(A)): Maybe(B) + case m { + none: Maybe.none, + some: Maybe.some(f(m.value)), + } + +Maybe.map.comp(ma: Maybe(A), g: (B -> C), h: (A -> B)) + : Equal(Maybe(C), + Maybe.map(Function.comp(g, h), ma), + Function.comp(Maybe.map(g), Maybe.map(h))(ma)) + case ma{ + none: _ + some: _ + } : Equal(_, + Maybe.map<_,_>(Function.comp<_,_,_>(g, h), ma), + Function.comp<_,_,_>(Maybe.map<_,_>(g), Maybe.map<_,_>(h))(ma)) + +Maybe.map.id(ma: Maybe(A)): Equal(Maybe(A), Maybe.map(Function.id, ma), ma) + case ma{ + none: _ + some: _ + } : Equal(_, Maybe.map<_,_>(Function.id<_>, ma), ma) + +// The functor instance for maybe +Maybe.functor: Functor(Maybe) + Functor.new(Maybe.map) + +// Proof that Maybe.functor conforms to the functor laws +Maybe.functor.verified: VerifiedFunctor(Maybe, Maybe.functor) + VerifiedFunctor.new(Maybe.map.id, Maybe.map.comp) + +// Maybe.is_some(x: A): Maybe.IsSome(A,Maybe.some(x)) +// def y = Maybe.some(x) +// case y{ +// with e : Equal(Maybe(A),y,y.self) = Equal.to +// none: Empty.absurd<>(Maybe.some_isnt_none(x,e)) +// some: y.value +// } + +Maybe.IsSome(A: Type,x: Maybe(A)): Type + case x{ + none: Empty + some: A + } + +Maybe.join(m: Maybe(Maybe(A))): Maybe(A) + case m{ + none: Maybe.none + some: m.value + } + +// Maybe.some_isnt_none(x: A) : Not(Equal(Maybe(A),Maybe.some(x),Maybe.none)) +// def P = ((x) case x { none: Empty, some: Unit) :: Maybe(A) -> Type +// (e) Equal.rewrite(x), Maybe.none,P>(e, Unit.new) + + + + diff --git a/src/Module.fm b/src/Module.fm new file mode 100644 index 0000000..1e388f8 --- /dev/null +++ b/src/Module.fm @@ -0,0 +1,41 @@ +Module: Type + Map(Export) + +Module.new: Module + Map.new + +Module.Row(field: String, T: Type, m: Module) : Type + let got = Map.get(String.to_bits(field),m) + case got { + none: Empty + some: Equal(Type,T,Export.T(got.value)) + } + +Module.from(defs: List(Pair(String, Export))): Module + Map.from_list<_,_>(String.to_bits,defs) + +Module.get(key: String, mod: Module): Module.type(key, mod) + case Map.get(String.to_bits(key), mod) as got { + none: Unit.new + some: Export.value(got.value) + } : case got { + none: Unit + some: Export.T(got.value) + } + +Module.set(key: String, val: Export, mod: Module): Module + Map.set(String.to_bits(key), val, mod) + +// Module.to_list(m : Module) : List(Pair(Bits,Type)) +// def f = ((p) let {x, y} = p Pair.new(x,Export.T(y))) +// :: Pair(Bits,Export) -> Pair(Bits,Type) +// List.map<_,_>(f, Map.to_list<_>(m)) + +Module.type(key: String, mod: Module): Type + let got = Map.get(String.to_bits(key), mod) + case got { + none: Unit + some: Export.T(got.value) + } + + diff --git a/src/Monad.fm b/src/Monad.fm index 65ecc3b..cb65d39 100644 --- a/src/Monad.fm +++ b/src/Monad.fm @@ -6,12 +6,10 @@ type Monad Type> { } Monad.pure Type>(m: Monad(M)): -> A -> M(A) - case m { - new: m.pure - } + open m + m.pure Monad.bind Type>(m: Monad(M)): -> M(A) -> (A -> M(B)) -> M(B) - case m { - new: m.bind - } + open m + m.bind diff --git a/src/Nat.fm b/src/Nat.fm index 14d371b..705a8ab 100644 --- a/src/Nat.fm +++ b/src/Nat.fm @@ -25,11 +25,10 @@ Nat.to_base(base: Nat, nat: Nat): List(Nat) Nat.to_base.go(base, nat, List.nil) Nat.to_base.go(base: Nat, nat: Nat, res: List(Nat)): List(Nat) - case Nat.div_mod(nat, base) as div_mod { - new: case div_mod.fst { - zero: List.cons<_>(div_mod.snd, res), - succ: Nat.to_base.go(base, div_mod.fst, List.cons<_>(div_mod.snd, res)) - } + open Nat.div_mod(nat, base) as div_mod + case div_mod.fst { + zero: List.cons<_>(div_mod.snd, res), + succ: Nat.to_base.go(base, div_mod.fst, List.cons<_>(div_mod.snd, res)) } Nat.from_base(base: Nat, ds: List(Nat)) : Nat @@ -137,7 +136,7 @@ Nat.ltn(n: Nat, m: Nat): Bool Nat.is_even(n: Nat): Bool case n { - zero: true + zero: Bool.true succ: Bool.not(Nat.is_even(n.pred)) } @@ -151,14 +150,163 @@ Nat.show_digit(base: Nat, n: Nat) : Char ,'G','H','I','J','K','L','M','N','O','P','Q','R','S','T','U','V' ,'W','X','Y','Z','a','b','c','d','e','f','g','h','i','j','k','l' ,'m','n','o','p','q','r','s','t','u','v','w','x','y','z','+','/']; - if Bool.and(Nat.gtn(base,0),Nat.lte(base,64)) then - case List.at<_>(m,base64) as c { + if Bool.and(Nat.gtn(base,0),Nat.lte(base,64)) then + let c = List.at<_>(m,base64) + case c { none: '#', some: c.value, } else '#' +//Nat.to_u8(n: Nat): U8 + //Nat.apply(n, U8.inc, U8.0) + // TODO: optimize (this is swapped on the JS compiler though) Nat.to_u16(n: Nat): U16 Nat.apply(n, U16.inc, U16.zero) +Nat.to_u32(n: Nat): U32 + Nat.apply(n, U32.inc, U32.zero) + +//Nat.to_u64(n: Nat): U64 + //Nat.apply(n, U64.inc, U64.0) + +//Nat.to_u256(n: Nat): U256 + //Nat.apply(n,U256.inc, U256.0) + +Nat.bitwise_and(a: Nat, b: Nat): Nat + case Bool.or(Nat.eql(a, 0), Nat.eql(a, 0)){ + true : 0 + false: + let bit = Bool.if(Bool.or(Nat.eql(Nat.mod(a, 2), 0), Nat.eql(Nat.mod(b, 2), 0)), 0, 1) + let a = Nat.div(a, 2) + let b = Nat.div(b, 2) + Nat.add(bit, Nat.mul(2, Nat.bitwise_and(a, b))) + } + +// Nat.zero_not_succ(a: Nat): Not(0 == Nat.succ(a)) +// (eq) +// def P = (x) +// case x{ +// zero: Unit +// succ: Empty +// } +// Equal.rewrite(eq, Unit.new) + +// Nat.equal(a: Nat, b: Nat): Either(a == b, Not(a == b)) +// case a { +// zero: case b { +// zero: Either.left<_,_>(Equal.refl), +// succ: Either.right<_,_>(Nat.zero_not_succ(b.pred)) +// } : Either(0 == b, Not(0 == b)), +// succ: case b { +// zero: Either.right<_,_>(Nat.succ_not_zero(a.pred)), +// succ: case Nat.equal(a.pred, b.pred) as rec { +// left : Either.left<_,_>(Equal.apply(rec.value)), +// right: Either.right<_,_>((eq) rec.value(Nat.succ_inj(a.pred, b.pred, eq))) +// } : Either(Nat.succ(a.pred) == Nat.succ(b.pred), Not(Nat.succ(a.pred) == Nat.succ(b.pred))) +// } : Either(Nat.succ(a.pred) == b, Not(Nat.succ(a.pred) == b)) +// } : Either(a == b, Not(a == b)) + +Nat.for(state: S, from: Nat, til: Nat, func: Nat -> S -> S): S + if Nat.eql(from, til) then + state + else + Nat.for(func(from, state), Nat.succ(from), til, func) + +Nat.half(n: Nat): Nat + case n { + zero: Nat.zero, + succ: case n.pred { + zero: Nat.zero, + succ: Nat.succ(Nat.half(n.pred.pred)) + } + } + +Nat.induction(n: Nat): Type> -> (z: P(Nat.zero)) -> (s: ((m:Nat) -> P(m) -> P(Nat.succ(m)))) -> P(n) +

(z) (s) n

(z, (pred) s(pred, Nat.induction(pred)

(z, s))) + +Nat.min(a: Nat, b: Nat): Nat + case a { + zero: 0, + succ: case b { + zero: 0, + succ: Nat.succ(Nat.min(a.pred, b.pred)) + } + } + +Nat.odd(n: Nat): Bool + Nat.eql(Nat.mod(n, 2), 1) + +Nat.square(a: Nat): Nat + Nat.mul(a, a) + +Nat.succ_inj(a: Nat, b: Nat, eq: Nat.succ(a) == Nat.succ(b)): a == b + Equal.apply(eq) + +Nat.sum(n: Nat): Nat + Nat.sum.go(n, Nat.zero) + +Nat.sum.go(n: Nat , r: Nat): Nat //loop// + case n { + zero: r, + succ: Nat.sum.go(n.pred, Nat.add(n, r)) + } + +// TODO +Nat.to_f64(s: Bool, a: Nat, b: Nat): F64 + Nat.to_f64(s, a, b) + +Nat.to_string_unary(n: Nat): String + case n { + zero: String.nil, + succ: String.cons('1', Nat.to_string_unary(n.pred)) + } + +Nat.to_string(n: Nat): String + case n { + zero: String.cons(Char.parse("z"), String.nil), + succ: String.cons(Char.parse("s"), Nat.to_string(n.pred)) + } + +// Nat.succ_isnt_zero: Not(Equal(Nat, Nat.succ(n), Nat.zero)) +// def P = (n : Nat) +// case n { +// zero: Empty +// succ: Unit +// } +// def p_succ = +// Unit.new +// (succ_is_zero) +// Equal.rewrite<_,_,_,P>(succ_is_zero, p_succ) + +// Nat.succ_not_zero(a: Nat): Not(Nat.succ(a) == 0) +// (eq) +// def P = (x) case x { zero: Empty, succ: Unit } +// Equal.rewrite(eq, Unit.new) + +//TODO: error on misformatted Nat +// Nat.parse_decimal(str: String): Nat +// Nat.parse_decimal.go(str, Nat.zero) + +// Nat.parse_decimal.go(str: String, res: Nat): Nat +// case str { +// nil : res, +// cons: +// let dig = Nat.sub(U16.to_nat(str.head), 48) +// let res = Nat.add(dig, Nat.mul(10, res)) +// Nat.parse_decimal.go(str.tail, res) +// } + +// Nat.parse_hex(str: String): Nat +// Nat.parse_hex.go(str, Nat.zero) + +// Nat.parse_hex.go(str: String, res: Nat): Nat +// case str { +// nil : res, +// cons: +// let dig = Char.hex_value(str.head) +// let res = Nat.add(dig, Nat.mul(16, res)) +// Nat.parse_hex.go(str.tail, res) +// } + diff --git a/src/Newtype.fm b/src/Newtype.fm new file mode 100644 index 0000000..0eda3d5 --- /dev/null +++ b/src/Newtype.fm @@ -0,0 +1,9 @@ +type Newtype ~ (tag: String) { + new(val: A) ~ (tag: tag) +} + +Newtype.elim(x: Newtype(A, tag)): A + open x + x.val + + diff --git a/src/NonEmpty.fm b/src/NonEmpty.fm new file mode 100644 index 0000000..49345cc --- /dev/null +++ b/src/NonEmpty.fm @@ -0,0 +1,10 @@ +type NonEmpty { + end(value: A), + cons(head: A, tail: NonEmpty(A)) +} + +NonEmpty.to_list(xs: NonEmpty(A)): List(A) + case xs { + end : List.cons(xs.value)(List.nil), + cons: List.cons(xs.head)(NonEmpty.to_list(xs.tail)) + } diff --git a/src/Not.fm b/src/Not.fm new file mode 100644 index 0000000..c6afceb --- /dev/null +++ b/src/Not.fm @@ -0,0 +1,4 @@ +// logical negation +Not(P: Type): Type + P -> Empty + diff --git a/src/Or.fm b/src/Or.fm new file mode 100644 index 0000000..62c86bf --- /dev/null +++ b/src/Or.fm @@ -0,0 +1,10 @@ +// logical disjunction +Or(A:Type,B:Type): Type + Either(A,B) + +Or.lft(x: A): Or(A,B) + Either.left<_,_>(x) + +Or.rgt(x: B): Or(A,B) + Either.right<_,_>(x) + diff --git a/src/Pair.fm b/src/Pair.fm index 1c4a271..438da48 100644 --- a/src/Pair.fm +++ b/src/Pair.fm @@ -12,3 +12,42 @@ Pair.snd(pair: Pair(A, B)): B new: pair.snd } +Pair.map(f: B -> C, p: Pair(A, B)): Pair(A, C) + case p { + new: Pair.new(p.fst, f(p.snd)) + } + +Pair.show( + show_a: A -> String, + show_b: B -> String, + pair: Pair(A,B) +) : String + case pair{ + new: let str = String.concat("(", show_a(pair.fst)) + let str = String.concat(str, ",") + let str = String.concat(str, show_b(pair.snd)) + let str = String.concat(str, ")") + str + } + +Pair.functor: Functor(Pair(A)) + Functor.new(Pair.map) + +Pair.functor.verified: VerifiedFunctor(Pair(A), Pair.functor) + VerifiedFunctor.new>(Pair.map.id, Pair.map.comp) + +Pair.map.id(p: Pair(A, B)): Equal(Pair(A, B), Pair.map(Function.id, p), p) + case p{ + new: _ + } : Equal(_, Pair.map(Function.id<_>, p), p) + +Pair.map.comp(e: Pair(A, B), g: (C -> D), h: (B -> C)) + : Equal(Pair(A, D), + Pair.map(Function.comp(g, h), e), + Function.comp(Pair.map(g), Pair.map(h), e)) + case e{ + new: _ + } : Equal(_, + Pair.map<_,_,_>(Function.comp<_,_,_>(g, h), e), + Function.comp<_,_,_>(Pair.map<_,_,_>(g), Pair.map<_,_,_>(h))(e)) + diff --git a/src/Parser.fm b/src/Parser.fm index 3fcb07d..734a308 100644 --- a/src/Parser.fm +++ b/src/Parser.fm @@ -122,8 +122,8 @@ Parser.until1(cond: Parser(Unit), parser: Parser(V)): Parser(List(V)) // Parses an optional Parser.maybe(parse: Parser(V)): Parser(Maybe(V)) (idx,code) case parse(idx,code) as reply { - error: Parser.Reply.value(idx, code, Maybe.none), - value: Parser.Reply.value(reply.idx, reply.code, Maybe.some(reply.val)), + error: Parser.Reply.value(idx, code, Maybe.none) + value: Parser.Reply.value(reply.idx, reply.code, Maybe.some(reply.val)) } Parser.ErrorAt.combine( @@ -134,11 +134,9 @@ Parser.ErrorAt.combine( none: b, some: case b { none: a, - some: case a.value { - new: case b.value { - new: if Nat.gtn(a.value.idx, b.value.idx) then a else b - } - } + some: open a.value + open b.value + if Nat.gtn(a.value.idx, b.value.idx) then a else b } } @@ -147,10 +145,9 @@ Parser.first_of.go(pars: List(Parser(A)), err: Maybe(Parser.ErrorAt)): (idx,code) case pars { nil: case err { - none: Parser.Reply.error<_>(idx, code, "No parse."), - some: case err.value { - new: Parser.Reply.error<_>(err.value.idx, err.value.code, err.value.err), - } + none: Parser.Reply.error<_>(idx, code, "No parse.") + some: open err.value + Parser.Reply.error<_>(err.value.idx, err.value.code, err.value.err) }, cons: let parsed = pars.head(idx, code); diff --git a/src/Pos32.fm b/src/Pos32.fm new file mode 100644 index 0000000..93b05f3 --- /dev/null +++ b/src/Pos32.fm @@ -0,0 +1,85 @@ +// A position represented using a U32, such that: +// x = pos & 0x7FF // 0 .. 4096 +// y = (pos >>> 12) & 0x7FF // 0 .. 4096 +// z = (pos >>> 24) // 0 .. 256 +// The `x` and `y` values are 12-bit, and `z` is 8-bit. +Pos32: Type + U32 + +// // Adds two positions +// Pos32.add(a: Pos32, b: Pos32): Pos32 +// let a_x = Pos32.get_x(a) +// let a_y = Pos32.get_y(a) +// let a_z = Pos32.get_z(a) +// let b_x = Pos32.get_x(b) +// let b_y = Pos32.get_y(b) +// let b_z = Pos32.get_z(b) +// let c_x = U32.add(a_x, b_x) +// let c_y = U32.add(a_y, b_y) +// let c_z = U32.add(a_z, b_z) +// Pos32.new(c_x, c_y, c_z) + +// // The dot product of two positions +// // Returns (ax * bx + ay * by + az * bz) +// Pos32.dot(a: Pos32, b: Pos32): U32 +// let x = U32.mul(Pos32.get_x(a), Pos32.get_x(b)) +// let y = U32.mul(Pos32.get_y(a), Pos32.get_y(b)) +// let z = U32.mul(Pos32.get_z(a), Pos32.get_z(b)) +// U32.add(U32.add(x, y), z) + +// Pos32.get_x(pos: Pos32): U32 +// U32.and(pos, 2047u) + +// Pos32.get_y(pos: Pos32): U32 +// U32.and(U32.shr(pos, 12u), 2047u) + +// Pos32.get_z(pos: Pos32): U32 +// U32.shr(pos, 24u) + +// Pos32.new(x: U32, y: U32, z: U32): Pos32 +// let pos = 0u +// let pos = U32.or(pos, x) +// let pos = U32.or(pos, U32.shl(y, 12u)) +// let pos = U32.or(pos, U32.shl(z, 24u)) +// pos + +// // Multiplies all positions by a scaling factor +// Pos32.scale(a: Pos32, s: U32): Pos32 +// let x = U32.mul(Pos32.get_x(a), s) +// let y = U32.mul(Pos32.get_y(a), s) +// let z = U32.mul(Pos32.get_z(a), s) +// Pos32.new(x, y, z) + +// Pos32.set_x(pos: Pos32, x: U32): U32 +// Pos32.new(x, Pos32.get_y(pos), Pos32.get_z(pos)) + +// Pos32.set_y(pos: Pos32, y: U32): U32 +// Pos32.new(Pos32.get_x(pos), y, Pos32.get_z(pos)) + +// Pos32.set_z(pos: Pos32, z: U32): U32 +// Pos32.new(Pos32.get_x(pos), Pos32.get_y(pos), z) + +// // Subtracts two positions +// Pos32.sub(a: Pos32, b: Pos32): Pos32 +// let a_x = Pos32.get_x(a) +// let a_y = Pos32.get_y(a) +// let a_z = Pos32.get_z(a) +// let b_x = Pos32.get_x(b) +// let b_y = Pos32.get_y(b) +// let b_z = Pos32.get_z(b) +// let c_x = U32.sub(a_x, b_x) +// let c_y = U32.sub(a_y, b_y) +// let c_z = U32.sub(a_z, b_z) +// Pos32.new(c_x, c_y, c_z) + +// Pos32.to_string(pos: Pos32): String +// let x = U32.to_string(Pos32.get_x(pos)) +// let y = U32.to_string(Pos32.get_y(pos)) +// let z = U32.to_string(Pos32.get_z(pos)) +// String.flatten(["[",x,",",y,",",z,"]"]) + +// // TODO +// // Converts a Pos32 to a F64.V3 +// Pos32.to_v3(pos: Pos32): F64.V3 +// Pos32.to_v3(pos) + diff --git a/src/Queue.fm b/src/Queue.fm new file mode 100644 index 0000000..48b2b67 --- /dev/null +++ b/src/Queue.fm @@ -0,0 +1,143 @@ +// Queue implements a First-In-First-Out (FIFO) policy +// Invariants: +// - size_front >= size_rear +// - size_front == 0 implies size_rear == 0 +type Queue { + new(front: List(A), size_front: Nat, rear: List(A), size_rear: Nat) +} + +// f : front +// sf : size_front +// r : rear +// sr : size_rear +// Here we maintain the invariant: +// sf <= max_diff * sr + 1 /\ sr <= max_diff * sf + 1 +Queue.balance(f: List(A), sf: Nat, r: List(A), sr: Nat): Queue(A) + let max_sf = Nat.add(1, Nat.mul(Queue.max_diff, sf)) + let max_sr = Nat.add(1, Nat.mul(Queue.max_diff, sr)) + let size1 = Nat.div(Nat.add(sf, sr), 2) + let size2 = Nat.sub(Nat.add(sf, sr), 1) + case Nat.gtn(sf, max_sf) { + // if the front is way too long + true: + let new_f = List.take(size1, f) + let tail = List.reverse(List.drop(size1, f)) + let new_r = List.concat(r, tail) + Queue.new(new_f, size1, new_r, size2), + // if the rear is way too long + false: case Nat.gtn(sr, max_sr) { + true: + let tail = List.reverse(List.drop(size1, r)) + let new_f = List.concat(f, tail) + let new_r = List.take(size1, r) + Queue.new(new_f, size2, new_r, size1), + // queue is balanced + false: Queue.new(f, sf, r, sr) + } + } + +// insert at the front +Queue.cons(a: A, q: Queue(A)): Queue(A) + open q + let new_f = List.cons(a, q.front) + let new_sf = Nat.add(q.size_front, 1) + Queue.balance(new_f, new_sf, q.rear, q.size_rear) + +Queue.empty: Queue(A) + Queue.new(List.nil, 0, List.nil, 0) + +Queue.foldr(b: B, f: A -> B -> B, q: Queue(A)): B + open q + let as_list = List.concat(q.front, List.reverse(q.rear)) + List.foldr(b, f, as_list) + + +Queue.from_list(as: List(A)): Queue(A) + let len = List.length(as) + Queue.balance(as, len, List.nil, 0) + +// We don't bother to check the rear because +// if size_front == 0, size_rear == 0 +Queue.head(q: Queue(A)): Maybe(A) + open q + case q.front { + nil : Maybe.none, + cons: Maybe.some(q.front.head) + } + + +// removes last element +Queue.init(q: Queue(A)): Maybe(Queue(A)) + open q + case q.rear { + nil: case q.front { + nil : Maybe.none, + cons: + let new_f = List.drop(1, q.front) + let new_sf = Nat.sub(q.size_front, 1) + let new_q = Queue.balance(new_f, new_sf, List.nil, 0) + Maybe.some(new_q) + }, + cons: + let new_r = List.drop(1, q.rear) + let new_sr = Nat.sub(q.size_rear, 1) + let new_q = Queue.balance(q.front, q.size_front, new_r, new_sr) + Maybe.some(new_q) + } + + +Queue.last(q: Queue(A)): Maybe(A) + open q + case q.rear { + nil: case q.front { + nil : Maybe.none, + cons: case List.reverse(q.front) as reversed { + nil : Maybe.none, + cons: Maybe.some(reversed.head) + }, + }, + cons: Maybe.some(q.rear.head) + } + +Queue.length(q: Queue(A)): Nat + open q + Nat.add(q.size_front, q.size_rear) + +Queue.map(f: A -> B, q: Queue(A)): Queue(B) + open q + let new_f = List.map<_,_>(f, q.front) + let new_r = List.map<_,_>(f, q.rear) + Queue.new<_>(new_f, q.size_front, new_r, q.size_rear) + +// this constant represents how many times longer +// one half of the queue is allowed to be relative to the other +Queue.max_diff : Nat + 2 + +Queue.null(q: Queue(A)): Bool + open q + let front_is_empty = Nat.eql(q.size_front, 0) + let rear_is_empty = Nat.eql(q.size_rear, 0) + Bool.and(front_is_empty, rear_is_empty) + +// Insert at the back +Queue.snoc(a: A, q: Queue(A)): Queue(A) + open q + let new_rear = List.cons(a, q.rear) + Queue.balance(q.front, q.size_front, new_rear, Nat.add(q.size_rear, 1)) + +Queue.tail(q: Queue(A)): Maybe(Queue(A)) + open q + case q.front { + nil : Maybe.none, + cons: + let new_front = List.drop(1, q.front) + let new_q = Queue.balance(new_front, Nat.sub(q.size_front, 1), q.rear, q.size_rear) + Maybe.some(new_q) + } + +Queue.to_list(q: Queue(A)): List(A) + open q + List.concat(q.front, List.reverse(q.rear)) + + diff --git a/src/Show.fm b/src/Show.fm new file mode 100644 index 0000000..4c8cb4d --- /dev/null +++ b/src/Show.fm @@ -0,0 +1,3 @@ +type Show ~ (str: String) { + msg(str: String) ~ (str: str) +} diff --git a/src/Sigma.fm b/src/Sigma.fm index b0c2bfd..2c86c14 100644 --- a/src/Sigma.fm +++ b/src/Sigma.fm @@ -3,9 +3,8 @@ type Sigma (A: Type) (B: A -> Type) { } Sigma.fst Type>(sig: Sigma(A, B)): A - case sig { - new: sig.fst - } + open sig + sig.fst Sigma.snd Type>(sig: Sigma(A, B)): B(Sigma.fst(sig)) case sig { diff --git a/src/String.fm b/src/String.fm index 917dcc1..117716f 100644 --- a/src/String.fm +++ b/src/String.fm @@ -24,6 +24,17 @@ String.length.go(xs: String, n: Nat): Nat cons: String.length.go(xs.tail, Nat.succ(n)) } +// Computes the length of the string as a U32. +String.length32(xs: String): U32 + String.length32.go(xs, U32.zero) + +String.length32.go(xs: String, n: U32): U32 + case xs{ + nil : n + cons: String.length32.go(xs.tail, U32.inc(n)) + } + + String.concat(as: String, bs: String): String case as { nil: bs, @@ -92,6 +103,10 @@ String.append(as: String, a: Char): String nil : String.pure(a) cons: String.cons(as.head,String.append(as.tail, a)) } + +// A string with only one character. +String.pure(x : Char) : String + String.cons(x, String.nil) // Check if "xs" starts with "match" String.starts_with(xs: String, match: String): Bool @@ -248,8 +263,178 @@ String.split(xs: String, match: String): List(String) } } +String.split_at(n : Nat, xs: String) : Pair(String,String) + Pair.new<_,_>(String.take(n,xs),String.drop(n,xs)) + // String.to_bits(str: String): Bits // case str{ -// nil : Bits.nil +// nil : Bits.e // cons: Bits.concat(U16.to_bits(str.head))(String.to_bits(str.tail)) // } + +// insert separators between characters, i.e. `[A,B,C] ~> [A,sep,B,sep,C]` +String.intercalate(sep: String, xs: List(String)): String + String.flatten(List.intersperse<_>(sep,xs)) + +// insert separators between characters, i.e. `[A,B,C] ~> [A,sep,B,sep,C]` +String.intersperse(sep: Char, xs: String): String + case xs{ + nil : String.nil + cons: case xs.tail{ + nil : String.pure(xs.head) + cons: String.cons(xs.head,String.cons(sep,String.intersperse(sep,xs.tail))) + } + } + +// Converts a String to Bits +String.to_bits(str: String): Bits + case str { + nil : Bits.e, + cons: case U16.eql(str.head, '1') { + true : Bits.i(String.to_bits(str.tail)), + false: Bits.o(String.to_bits(str.tail)), + } + } + +// Print a string +String.show(xs: String): String + String.flatten(["\"",xs,"\""]) + +// Get the all characters of a nonempty string except the last one +// String.init(xs: String, not_empty: String.not_empty(xs)) : String +// case xs{ +// with ne : String.not_empty(xs.self) = not_empty; +// nil : Empty.absurd<>(ne); +// cons: case xs.tail{ +// with e : Equal(_, xs.tail.self,xs.tail) = Equal.to; +// nil : String.nil +// cons: def cne = String.cons_isnt_empty(xs.tail.head,xs.tail.tail) +// def xne = Equal.rewrite<_,_,_,(x) String.not_empty(x)>(e,cne) +// String.cons(xs.head,String.init(xs.tail,xne)) +// } +// } + +// Folds over a string, right associative +String.fold(xs: String) : -> P -> (Char -> P -> P) -> P +

(nil, cons) + case xs{ + nil : nil + cons: cons(xs.head, String.fold(xs.tail)

(nil, cons)) + } + +// Map over a string with the index +String.imap(f: Nat -> Char -> Char, xs: String): String + case xs{ + nil : String.nil + cons: String.cons(f(0,xs.head),String.imap((n) f(Nat.succ(n)),xs.tail)) + } + +// Get the last character of a nonempty string +// String.last(xs: String, not_empty: String.not_empty(xs)) : Char +// case xs{ +// with ne : String.not_empty(xs.self) = not_empty; +// nil : Empty.absurd<>(ne); +// cons: case xs.tail{ +// with e : Equal(_, xs.tail.self,xs.tail) = Equal.to; +// nil : xs.head +// cons: def cne = String.cons_isnt_empty(xs.tail.head,xs.tail.tail) +// def xne = Equal.rewrite<_,_,_,(x) String.not_empty(x)>(e,cne) +// String.last(xs.tail,xne) +// } +// } + +// A lazy String constructor, useful for efficient concatenation +String.Builder: Type + String -> String + +// concatenate two string builders +String.Builder.concat(a: String.Builder, b: String.Builder): String.Builder + (x) a(b(x)) + +// turn a builder into a String +String.run_builder(lb: String.Builder): String + lb(String.nil) + +String.span(f: Char -> Bool, xs: String): Pair(String,String) + case xs{ + nil : Pair.new<_,_>(String.nil,String.nil) + cons: case f(xs.head){ + true : + open String.span(f,xs.tail) as span + let y = span.fst + let z = span.snd + Pair.new<_,_>(String.cons(xs.head,y),z) + false: Pair.new<_,_>(String.nil,xs) + } + } + +// Get the tail of a nonempty string +// String.tail(xs: String, not_empty: String.not_empty(xs)) : String +// case xs{ +// with ne : String.not_empty(xs.self) = not_empty; +// nil : Empty.absurd<>(ne) +// cons: xs.tail +// } + +// String.take_n.aux(n: Nat, str: String, res: String): Maybe(Pair(String, String)) +// case res{ +// nil : case n{ +// zero: Maybe.some<_>(Pair.new<_,_>(str, String.nil)) +// succ: Maybe.none +// } +// cons: case n{ +// zero: Maybe.some<_>(Pair.new(str, res)) +// cons: String.take_n.aux(n.pred, String.cons(res.head, str), res.tail) +// } +// } +//String.take_n.aux(n: Nat, str: String, res: String): Maybe(Pair(String, String)) + //case res: + //| case n: + //| Maybe.some<>(Pair.new<,>(str, String.nil)); + //| Maybe.none;; + //| case n: + //| Maybe.some<>(Pair.new(str, res)); + //| String.take_n.aux(n.pred, String.cons(res.head, str), res.tail);; + +// Get the tail of a nonempty string +// String.tail(xs: String, not_empty: String.not_empty(xs)) : String +// case xs{ +// with ne : String.not_empty(xs) = not_empty +// nil : Empty.absurd<_>(ne) +// cons: xs.tail +// } + +String.to_bits(str: String): Bits + case str{ + nil : Bits.e + cons: Bits.concat(U16.to_bits(str.head), String.to_bits(str.tail)) + } + +// convert a string to a builder +String.to_builder(string: String) : String.Builder + String.to_builder.go(string, String.Builder.new) + +String.to_builder.go(string: String, lb: String.Builder) : String.Builder + case string{ + nil : lb + cons: String.to_builder.go(string.tail, String.Builder.snoc(string.head, lb)) + } + +// A lazy String constructor, useful for efficient concatenation +String.Builder: Type + String -> String + +// construct a new builder (it's just the identity function) +String.Builder.new : String.Builder + (x) x + +// append a character +String.Builder.snoc(c: Char, lb: String.Builder) : String.Builder + (x) lb(String.cons(c,x)) + +String.to_list(str: String): List(Char) + case str{ + nil : List.nil<_> + cons: List.cons<_>(str.head, String.to_list(str.tail)) + } + diff --git a/src/Subset.fm b/src/Subset.fm new file mode 100644 index 0000000..4328fd8 --- /dev/null +++ b/src/Subset.fm @@ -0,0 +1,3 @@ +type Subset Type> { + new(a: A) +} diff --git a/src/Text.fm b/src/Text.fm new file mode 100644 index 0000000..22f858c --- /dev/null +++ b/src/Text.fm @@ -0,0 +1,3 @@ +Text: Type + String + diff --git a/src/The.fm b/src/The.fm new file mode 100644 index 0000000..d51ca94 --- /dev/null +++ b/src/The.fm @@ -0,0 +1,3 @@ +type The ~ (x: A) { + value(x: A) ~ (x: x) +} diff --git a/src/U16.fm b/src/U16.fm index b2de8c3..70cd8af 100644 --- a/src/U16.fm +++ b/src/U16.fm @@ -3,9 +3,8 @@ type U16 { } U16.to_word(a: U16): Word(16) - case a { - new: a.value - } + open a + a.value // 0 U16.zero: U16 @@ -13,65 +12,50 @@ U16.zero: U16 // ++a U16.inc(a: U16): U16 - case a { - new: U16.new(Word.inc<_>(a.value)) - } + open a + U16.new(Word.inc<_>(a.value)) // a + b U16.add(a: U16, b: U16): U16 - case a { - new: case b { - new: U16.new(Word.add<_>(a.value, b.value)) - } - } + open a + open b + U16.new(Word.add<_>(a.value, b.value)) // a - b U16.sub(a: U16, b: U16): U16 - case a { - new: case b { - new: U16.new(Word.sub<_>(a.value, b.value)) - } - } + open a + open b + U16.new(Word.sub<_>(a.value, b.value)) // a == b U16.eql(a: U16, b: U16): Bool - case a { - new: case b { - new: Word.eql<_>(a.value, b.value) - } - } + open a + open b + Word.eql<_>(a.value, b.value) // a >= b U16.gte(a: U16, b: U16): Bool - case a { - new: case b { - new: Word.gte<_>(a.value, b.value) - } - } + open a + open b + Word.gte<_>(a.value, b.value) // a > b U16.gtn(a: U16, b: U16): Bool - case a { - new: case b { - new: Word.gtn<_>(a.value, b.value) - } - } + open a + open b + Word.gtn<_>(a.value, b.value) // a <= b U16.lte(a: U16, b: U16): Bool - case a { - new: case b { - new: Word.lte<_>(a.value, b.value) - } - } + open a + open b + Word.lte<_>(a.value, b.value) // a < b U16.ltn(a: U16, b: U16): Bool - case a { - new: case b { - new: Word.ltn<_>(a.value, b.value) - } - } + open a + open b + Word.ltn<_>(a.value, b.value) // a <= b <= c U16.btw(a: U16, b: U16, c: U16): Bool @@ -79,13 +63,76 @@ U16.btw(a: U16, b: U16, c: U16): Bool // Stringifies to hex U16.show_hex(a: U16): String - case a { - new: Nat.to_string_base(16, Bits.to_nat(Word.to_bits<16>(a.value))) - } + open a + Nat.to_string_base(16, Bits.to_nat(Word.to_bits<16>(a.value))) +U16.to_u32(a: U16): U32 + open a + U32.new(Word.trim<16>(32, a.value)) + +U16.pow(a: U16, b: U16): U16 + open a + open b + U16.new(Word.pow<_>(a.value, b.value)) + +U16.shl(n: U16, a: U16): U16 + U16.shl(n, a) + +U16.shr(n: U16, a: U16): U16 + U16.shl(n, a) + +U16.to_bits(a: U16): Bits + open a + Word.to_bits<_>(a.value) + +// U16.to_nat(a: U16): Nat +// case a{ +// new: Word.to_nat<_>(a.value) +// } + +// TODO: optimize +// U16.to_string(n: U16): String +// Nat.to_string_base(10, U16.to_nat(n)) + +U16.xor(a: U16, b: U16): U16 + open a + open b + U16.new(Word.xor<_>(a.value, b.value)) + +U16.mod(a: U16, b: U16): U16 + open a + open b + U16.new(Word.mod<_>(a.value, b.value)) + +U16.and(a: U16, b: U16): U16 + open a + open b + U16.new(Word.and<_>(a.value, b.value)) + +U16.concat(a: U16, b: U16): U32 + open a + open b + U32.new(Word.concat<_,_>(a.value, b.value)) + +U16.div(a: U16, b: U16): U16 + open a + open b + U16.new(Word.div<_>(a.value, b.value)) + +U16.mul(a: U16, b: U16): U16 + open a + open b + U16.new(Word.mul<_>(a.value, b.value)) + +U16.or(a: U16, b: U16): U16 + open a + open b + U16.new(Word.or<_>(a.value, b.value)) + +// U16.parse_hex(str: String): U16 +// U16.new(Word.from_bits(16, Bits.parse_hex(str))) U16.to_bits(a: U16): Bits - case a { - new: Word.to_bits<16>(a.value) - } + open a + Word.to_bits<16>(a.value) diff --git a/src/U256.fm b/src/U256.fm new file mode 100644 index 0000000..3fbe763 --- /dev/null +++ b/src/U256.fm @@ -0,0 +1,51 @@ +type U256 { + new(value: Word(256)) +} + +U256.0: U256 + U256.new(Word.zero(256)) + +// U256.add(a: U256, b: U256): U256 +// open a +// open b +// U256.new(Word.add<_>(a_val, b_val)) + +// U256.div(a: U256, b: U256): U256 +// open a +// open b +// U256.new(Word.div<_>(a_val, b_val)) + +// U256.eql(a: U256, b: U256): Bool +// open a +// open b +// Word.eql<_>(a_val, b_val) + +// U256.gte(a: U256, b: U256): Bool +// open a +// open b +// Word.gte<_>(a_val, b_val) + +// U256.inc(a: U256): U256 +// open a +// U256.new(Word.inc<_>(a_val)) + +// U256.lte(a: U256, b: U256): Bool +// open a +// open b +// Word.lte<_>(a_val, b_val) + +// U256.mod(a: U256, b: U256): U256 +// open a +// open b +// U256.new(Word.mod<_>(a_val, b_val)) + +// U256.mul(a: U256, b: U256): U256 +// open a +// open b +// U256.new(Word.mul<_>(a_val, b_val)) + +// U256.sub(a: U256, b: U256): U256 +// open a +// open b +// U256.new(Word.sub<_>(a_val, b_val)) + diff --git a/src/U32.fm b/src/U32.fm index 7f496b3..c25fd60 100644 --- a/src/U32.fm +++ b/src/U32.fm @@ -7,41 +7,31 @@ U32.zero: U32 U32.new(Word.zero(32)) U32.add(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.add<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.add<_>(a.value, b.value)) U32.and(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.and<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.and<_>(a.value, b.value)) -U32.concat(a: U32, b: U32): U64 - case a { - new: case b { - new: U64.new(Word.concat<_,_>(a.value, b.value)) - } - } +// U32.concat(a: U32, b: U32): U64 +// open a +// open b +// U64.new(Word.concat<_,_>(a.value, b.value)) // a / b U32.div(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.div<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.div<_>(a.value, b.value)) // a == b U32.eql(a: U32, b: U32): Bool - case a { - new: case b { - new: Word.eql<_>(a.value, b.value) - } - } + open a + open b + Word.eql<_>(a.value, b.value) U32.for(state: S, from: U32, til: U32, func: U32 -> S -> S): S case U32.eql(from, til){ @@ -51,59 +41,46 @@ U32.for(state: S, from: U32, til: U32, func: U32 -> S -> S): S // a >= b U32.gte(a: U32, b: U32): Bool - case a { - new: case b { - new: Word.gte<_>(a.value, b.value) - } - } + open a + open b + Word.gte<_>(a.value, b.value) // a > b U32.gtn(a: U32, b: U32): Bool - case a { - new: case b { - new: Word.gtn<_>(a.value, b.value) - } - } + open a + open b + Word.gtn<_>(a.value, b.value) U32.inc(a: U32): U32 - case a{ - new: U32.new(Word.inc<_>(a.value)) - } + open a + U32.new(Word.inc<_>(a.value)) U32.length(str: String): U32 U32.length(str) // a <= b U32.lte(a: U32, b: U32): Bool - case a { - new: case b { - new: Word.lte<_>(a.value, b.value) - } - } + open a + open b + Word.lte<_>(a.value, b.value) // a < b U32.ltn(a: U32, b: U32): Bool - case a { - new: case b { - new: Word.ltn<_>(a.value, b.value) - } - } + open a + open b + Word.ltn<_>(a.value, b.value) // a % b U32.mod(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.mod<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.mod<_>(a.value, b.value)) // a * b U32.mul(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.mul<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.mul<_>(a.value, b.value)) // U32.needed_depth(size: U32): Nat // U32.needed_depth.go(U32.sub(size, 1u)) @@ -115,11 +92,9 @@ U32.mul(a: U32, b: U32): U32 // } U32.or(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.or<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.or<_>(a.value, b.value)) // U32.parse_hex(str: String): U32 // U32.new(Word.from_bits(32, Bits.parse_hex(str))) @@ -128,11 +103,9 @@ U32.or(a: U32, b: U32): U32 // U32.div(U32.mul(p, t), 100u) U32.pow(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.pow<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.pow<_>(a.value, b.value)) // U32.read_base(base: U32, str: String): U32 // U32.read_base(base, str) @@ -150,33 +123,27 @@ U32.slice(i: U32, j: U32, str: String): String U32.slice(i, j, str) U32.sub(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.sub<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.sub<_>(a.value, b.value)) U32.to_bits(a: U32): Bits - case a { - new: Word.to_bits<_>(a.value) - } + open a + Word.to_bits<_>(a.value) -// U32.to_f64(a: U32): F64 -// U32.to_f64(a) +U32.to_f64(a: U32): F64 + U32.to_f64(a) // U32.to_nat(a: U32): Nat -// case a{ -// new: Word.to_nat<_>(a.value) -// } +// open a +// Word.to_nat<_>(a.value) // TODO: optimize // U32.to_string(n: U32): String // Nat.to_string_base(10, U32.to_nat(n)) U32.xor(a: U32, b: U32): U32 - case a { - new: case b { - new: U32.new(Word.xor<_>(a.value, b.value)) - } - } + open a + open b + U32.new(Word.xor<_>(a.value, b.value)) diff --git a/src/U64.fm b/src/U64.fm index d5612e7..aa75539 100644 --- a/src/U64.fm +++ b/src/U64.fm @@ -1,3 +1,109 @@ type U64 { new(a: Word(64)) } + +U64.0: U64 + U64.new(Word.zero(64)) + +U64.add(a: U64, b: U64): U64 + open a + open b + U64.new(Word.add<_>(a_val, b_val)) + +U64.and(a: U64, b: U64): U64 + open a + open b + U64.new(Word.and<_>(a_val, b_val)) + +U64.div(a: U64, b: U64): U64 + open a + open b + U64.new(Word.div<_>(a_val, b_val)) + +// a == b +U64.eql(a: U64, b: U64): Bool + open a + open b + Word.eql<_>(a_val, b_val) + +// a >= b +U64.gte(a: U64, b: U64): Bool + open a + open b + Word.gte<_>(a_val, b_val) + +// a > b +U64.gtn(a: U64, b: U64): Bool + open a + open b + Word.gtn<_>(a_val, b_val) + +U64.inc(a: U64): U64 + open a + U64.new(Word.inc<_>(a_val)) + +// a <= b +U64.lte(a: U64, b: U64): Bool + open a + open b + Word.lte<_>(a_val, b_val) + +// a < b +U64.ltn(a: U64, b: U64): Bool + open a + open b + Word.ltn<_>(a_val, b_val) + +// U64.mix.const0: U64 +// U64.parse_hex("ff51afd7ed558ccd") + +// U64.mix.const1: U64 +// U64.parse_hex("c4ceb9fe1a85ec53") + +U64.mod(a: U64, b: U64): U64 + open a + open b + U64.new(Word.mod<_>(a_val, b_val)) + +U64.mul(a: U64, b: U64): U64 + open a + open b + U64.new(Word.mul<_>(a_val, b_val)) + +U64.or(a: U64, b: U64): U64 + open a + open b + U64.new(Word.or<_>(a_val, b_val)) + +U64.parse_hex(str: String): U64 + U64.new(Word.from_bits(64, Bits.parse_hex(str))) + +U64.pow(a: U64, b: U64): U64 + open a + open b + U64.new(Word.pow<_>(a_val, b_val)) + +U64.shl(n: U32, a: U64): U64 + U64.shl(n, a) + +U64.shr(n: U64, a: U64): U64 + U64.shr(n, a) + +U64.sub(a: U64, b: U64): U64 + open a + open b + U64.new(Word.sub<_>(a_val, b_val)) + +U64.to_bits(a: U64): Bits + open a + Word.to_bits<_>(a_val) + +// U64.to_nat(a: U64): Nat +// open a +// Word.to_nat<_>(a_val) + +U64.xor(a: U64, b: U64): U64 + open a + open b + U64.new(Word.xor<_>(a_val, b_val)) + diff --git a/src/U8.fm b/src/U8.fm new file mode 100644 index 0000000..5d56a54 --- /dev/null +++ b/src/U8.fm @@ -0,0 +1,112 @@ +type U8 { + new(value: Word(8)) +} + +U8.0: U8 + U8.new(Word.zero(8)) + +U8.add(a: U8, b: U8): U8 + open a + open b + U8.new(Word.add<_>(a.value, b.value)) + +U8.and(a: U8, b: U8): U8 + open a + open b + U8.new(Word.and<_>(a.value, b.value)) + +U8.concat(a: U8, b: U8): U16 + open a + open b + U16.new(Word.concat<_,_>(a.value, b.value)) + +U8.div(a: U8, b: U8): U8 + open a + open b + U8.new(Word.div<_>(a.value, b.value)) + +// a == b +U8.eql(a: U8, b: U8): Bool + open a + open b + Word.eql<_>(a.value, b.value) + +// U8.from_nat(n: Nat): U8 +// // TODO +// U8.parse_hex(Nat.to_string_base(16, n)) + +// a >= b +U8.gte(a: U8, b: U8): Bool + open a + open b + Word.gte<_>(a.value, b.value) + +// a > b +U8.gtn(a: U8, b: U8): Bool + open a + open b + Word.gtn<_>(a.value, b.value) + +U8.inc(a: U8): U8 + open a + U8.new(Word.inc<_>(a.value)) + +// a <= b +U8.lte(a: U8, b: U8): Bool + open a + open b + Word.lte<_>(a.value, b.value) + +// a < b +U8.ltn(a: U8, b: U8): Bool + open a + open b + Word.ltn<_>(a.value, b.value) + +U8.mod(a: U8, b: U8): U8 + open a + open b + U8.new(Word.mod<_>(a.value, b.value)) + +U8.mul(a: U8, b: U8): U8 + open a + open b + U8.new(Word.mul<_>(a.value, b.value)) + +U8.or(a: U8, b: U8): U8 + open a + open b + U8.new(Word.or<_>(a.value, b.value)) + +// U8.parse_hex(str: String): U8 +// U8.new(Word.from_bits(8, Bits.parse_hex(str))) + +U8.pow(a: U8, b: U8): U8 + open a + open b + U8.new(Word.pow<_>(a.value, b.value)) + +U8.shl(n: U32, a: U8): U8 + U8.shl(n, a) + +U8.shr(n: U8, a: U8): U8 + U8.shr(n, a) + +U8.sub(a: U8, b: U8): U8 + open a + open b + U8.new(Word.sub<_>(a.value, b.value)) + +U8.to_bits(a: U8): Bits + open a + Word.to_bits<_>(a.value) + +// U8.to_nat(a: U8): Nat +// open a +// Word.to_nat<_>(a.value) + +U8.xor(a: U8, b: U8): U8 + open a + open b + U8.new(Word.xor<_>(a.value, b.value)) + diff --git a/src/UFind.fm b/src/UFind.fm new file mode 100644 index 0000000..8e66b0d --- /dev/null +++ b/src/UFind.fm @@ -0,0 +1,38 @@ +// UFind.equivalent (uf: UFind, path1: Bits, path2: Bits): Bool +// // get uf root1 rank1 = UFind.find(uf, path1) +// // get uf root2 rank2 = UFind.find(uf, path2) +// Bits.eql(root1, root2) + +// UFind.find(uf: UFind, path: Bits): -> (UFind -> Bits -> Nat -> B) -> B +// (k) +// get node uf = Map.lookup(path, UNode.root(Nat.zero), uf) +// case node: +// | k(uf, path, node.rank); +// | get uf root rank = UFind.find(uf, node.parent) +// let uf = Map.set(path, UNode.link(root), uf) +// k(uf, root, rank); + +UFind: Type + Map(UNode) + +UFind.new : UFind + Map.new + +UFind.new_node(uf: UFind, path: Bits): UFind + Map.set(path, UNode.root(Nat.zero), uf) + +// UFind.union(uf: UFind, path1: Bits, path2: Bits): UFind +// get uf root_path1 rank1 = UFind.find(uf, path1) +// get uf root_path2 rank2 = UFind.find(uf, path2) +// case Bits.eql(root_path1, root_path2): +// | uf; +// | case Nat.cmp(rank1, rank2): +// | let uf = Map.set<>(root_path1, UNode.link(root_path2), uf) +// uf; +// | let uf = Map.set<>(root_path1, UNode.link(root_path2), uf) +// let uf = Map.set<>(root_path2, UNode.root(Nat.succ(rank2)), uf) +// uf; +// | let uf = Map.set<>(root_path1, UNode.root(rank2), uf) +// let uf = Map.set<>(root_path2, UNode.link(root_path1), uf) +// uf;; + diff --git a/src/UNode.fm b/src/UNode.fm new file mode 100644 index 0000000..6329af0 --- /dev/null +++ b/src/UNode.fm @@ -0,0 +1,5 @@ +type UNode{ + root(rank: Nat), + link(parent: Bits) +} + diff --git a/src/Unit.fm b/src/Unit.fm index 300ec83..4cfe620 100644 --- a/src/Unit.fm +++ b/src/Unit.fm @@ -2,3 +2,5 @@ type Unit { new } +Unit.show(u: Unit): String + "Unit.new" diff --git a/src/Variadic.fm b/src/Variadic.fm new file mode 100644 index 0000000..24440db --- /dev/null +++ b/src/Variadic.fm @@ -0,0 +1,21 @@ +Variadic(n: Nat, A: Type, B: Type): Type + case n { + zero: B, + succ: A -> Variadic(n.pred, A, B) + } + +Variadic.foldl(acc: B -> A -> B, b: B, n: Nat): Variadic(n, A, B) + case n { + zero: b, + succ: (a) Variadic.foldl(acc, acc(b, a), n.pred) + } : Variadic(n, A, B) + +Variadic.foldr(acc: A -> B -> B, b: B, n: Nat): Variadic(n, A, B) + Variadic.foldr.go(acc, b, (r) r, n) + +Variadic.foldr.go(acc: A -> B -> B, b: B, k: B -> B, n: Nat): Variadic(n, A, B) + case n { + zero: k(b), + succ: (a) Variadic.foldr.go(acc, b, (r) k(acc(a, r)), n.pred) + } : Variadic(n, A, B) + diff --git a/src/Vector.fm b/src/Vector.fm index de0fe28..8d7d8b9 100644 --- a/src/Vector.fm +++ b/src/Vector.fm @@ -14,3 +14,67 @@ Vector.tail(vector: Vector(A, Nat.succ(size))): Vector(A, si nil: Unit.new ext: vector.tail }: case vector.size { zero: Unit, succ: Vector(A, Nat.pred(vector.size)) } + +Vector.concat(as: Vector(A, n), bs: Vector(A, m)): Vector(A, Nat.add(n, m)) + case as { + nil: bs, + ext: Vector.ext(as.head, Vector.concat(as.tail, bs)) + } : Vector(A, Nat.add(as.size, m)) + +Vector.extract(xs: Vector(A, Nat.succ(n))): Pair(A, Vector(A, n)) + case xs { + nil: Unit.new, + ext: Pair.new(xs.head, xs.tail) + } : Bool.if(Nat.eql(0, xs.size), Unit, Pair(A, Vector(A, Nat.pred(xs.size)))) + +Vector.fill(n: Nat, a: A): Vector(A, n) + case n { + zero: Vector.nil, + succ: Vector.ext(a, Vector.fill(n.pred, a)) + } : Vector(A, n) + +Vector.indl Type, m: Nat> +(nil : P(Nat.zero)) +(ext : -> (a: A) -> (tail: P(size)) -> P(Nat.succ(size))) +(vector : Vector(A, m)) +: P(m) + case vector { + nil: nil, + ext: + def P = (n) P(Nat.succ(n)) + def nil = ext(vector.head, nil) + def ext = ext + Vector.indl(nil, ext, vector.tail) + } : P(vector.size) + +Vector.reverse(xs: Vector(A, size)): Vector(A, size) + Vector.indl(Vector.nil, Vector.ext, xs) + +// Vector.size_0_is_nil(vec: Vector(Nat, Nat.zero)): Equal(_, vec, Vector.nil) +// case vec with e : Equal(Nat, vec.size, Nat.zero) = Equal.to { +// nil: +// def P0 = ((x) Vector(Nat, Nat.zero)) :: Nat -> Type +// def x0 = Equal.rewrite<_,_,_, P0>(e, Vector.nil) +// Equal.to, +// ext: +// Empty.absurd<_>(Nat.succ_isnt_zero(e)) +// } +// : def P0 = ((x) Vector(Nat, x)) :: Nat -> Type +// def P1 = ((x) Vector(Nat, Nat.zero)) :: Nat -> Type +// let x0 = Equal.rewrite<_, vec.size, Nat.zero, P0>(e, vec) +// let x1 = Equal.rewrite<_, vec.size, Nat.zero, P1>(e, Vector.nil) +// Equal(_, x0, x1) + +// Vector.split_at(xs: Vector(A, n)): (m: Nat) -> Pair(Vector(A, Nat.min(n, m)), Vector(A, Nat.sub(n, m))) +// case xs { +// nil: (m) Pair.new(Vector.nil, Vector.nil), +// ext: (m) +// case m { +// zero: Pair.new<_,_>(Vector.nil, Vector.ext(xs.head, xs.tail)), +// succ: +// get x y = Vector.split_at(xs.tail, m.pred) +// let x = Vector.ext(xs.head, x) +// Pair.new<_,_>(x, y) +// } : Pair(Vector(A, Nat.min(Nat.succ(xs.size), m)), Vector(A, Nat.sub(Nat.succ(xs.size), m))) +// } : (m: Nat) -> Pair(Vector(A, Nat.min(xs.size, m)), Vector(A, Nat.sub(xs.size, m))) + diff --git a/src/VerifiedFunctor.fm b/src/VerifiedFunctor.fm new file mode 100644 index 0000000..d474d04 --- /dev/null +++ b/src/VerifiedFunctor.fm @@ -0,0 +1,15 @@ +// VerifiedFunctor is a Functor +// with map satisfying the functor laws +// map id == id +// map (f . g) == map f . map g +type VerifiedFunctor Type, f: Functor(F)>{ + new( + id: -> + (fa: F(A)) -> Equal(F(A), Functor.map(f)(Function.id, fa), Function.id(fa)), + comp: -> + (fa: F(A)) -> (g: B -> C) -> (h: A -> B) -> + Equal(F(C), + Functor.map(f)(Function.comp(g, h), fa), + Function.comp(Functor.map(f)(g), Functor.map(f)(h))(fa)) + ) +} diff --git a/src/Word.fm b/src/Word.fm index ae3126b..10b614e 100644 --- a/src/Word.fm +++ b/src/Word.fm @@ -21,12 +21,55 @@ Word.from_bits(size: Nat, bits: Bits): Word(size) } : Word(Nat.succ(size.pred)) } : Word(size) +Word.from_nat(size: Nat, n: Nat): Word(size) + Nat.apply(n, Word.inc, Word.zero(size)) + +// // Converts a Word to a Nat +// Word.to_nat(word: Word(size)): Nat +// Word.fold<()Nat,size>(0, <_> Nat.mul(2), <_> (x) Nat.succ(Nat.mul(2, x)), word) + Word.zero(size: Nat): Word(size) case size { zero: Word.e, succ: Word.o(Word.zero(size.pred)) } : Word(size) +Word.nat_log2(word: Word(size)): Nat + Word.nat_log2.go(word, 0, 0) + +Word.nat_log2.go(word: Word(size), c: Nat, n: Nat): Nat + case word { + e: n + o : Word.nat_log2.go(word.pred, Nat.succ(c), n) + i : Word.nat_log2.go(word.pred, Nat.succ(c), c) + } + +Word.neg.aux(word: Word(size), inc: Bool): Word(size) + case word { + e: Word.e, + o : case inc { + true : Word.o(Word.neg.aux(word.pred, Bool.true)), + false: Word.i(Word.neg.aux(word.pred, Bool.false)) + } + i : case inc { + true : Word.i(Word.neg.aux(word.pred, Bool.false)), + false: Word.o(Word.neg.aux(word.pred, Bool.false)) + } + } : Word(word.size) + +Word.neg(word: Word(size)): Word(size) + case word { + e: Word.e, + o : Word.o(Word.neg.aux(word.pred, Bool.true)), + i : Word.i(Word.neg.aux(word.pred, Bool.false)) + } : Word(word.size) + +Word.reverse(word: Word(size)): Word(size) + def nil = Word.e + def w0 = (rev) Word.o(rev) + def w1 = (rev) Word.i(rev) + Word.foldl(nil, w0, w1, word) + Word.cmp.go(a: Word(size), b: Word(size), c: Cmp): Cmp case a with b : Word(a.size) = b { e: c, @@ -161,6 +204,21 @@ Word.inc(word: Word(size)): Word(size) i: Word.o(Word.inc(word.pred)) } : Word(word.size) +Word.pred(word: Word(Nat.succ(size))): Word(size) + case word { + e: Word.e, + o : word.pred, + i : word.pred + } : Word(Nat.pred(word.size)) + +Word.drop(n: Nat, word: Word(Nat.add(n, size))): Word(size) + case n with word: Word(Nat.add(n, size)) = word { + zero: word, + succ: + let word.pred = Word.pred(word) + Word.drop(n.pred, word.pred) + } : Word(size) + // a + b Word.add(a: Word(size), b: Word(size)): Word(size) Word.adder(a)(b)(Bool.false) @@ -224,3 +282,15 @@ Word.pow(a: Word(size), b: Word(size)): Word(size) // TODO bitwise XOR between two words Word.xor(a: Word(size), b: Word(size)): Word(size) Word.xor(a, b) + +// Converts a Word to a Nat +// Word.to_nat(word: Word(size)): Nat +// Word.fold<()Nat,size>(0, <_> Nat.mul(2), <_> (x) Nat.succ(Nat.mul(2, x)), word) + +// TODO Bitwise-shifts a word left +Word.shift_left: -> Nat -> Word(size) -> Word(size) + Word.shift_left + +// TODO Bitwise-shifts a word right +Word.shift_right: -> Nat -> Word(size) -> Word(size) + Word.shift_right \ No newline at end of file