Add Moonad lib

.gitignore

@@ -0,0 +1 @@
+.DS_Store

src/And.fm

@@ -0,0 +1,14 @@
+// logical conjunction
+And(A:Type,B:Type): Type
+  Pair(A,B)
+
+// simplification
+And.fst<A: Type,B: Type>(x: And(A,B)) : A
+  Pair.fst<A,B>(x)
+
+And.new<A: Type,B: Type>(x: A,y:B) : And(A,B)
+  Pair.new<A,B>(x,y)
+
+And.snd<A: Type,B: Type>(x: And(A,B)) : B
+  Pair.snd<A,B>(x)
+

src/Array.fm

@@ -0,0 +1,71 @@
+// Array(A, depth) is a container with 2^depth values of type A.
+type Array<A: Type> ~ (depth: Nat) {
+  tip(value: A)                                             ~ (depth: Nat.zero),
+  tie<depth: Nat>(lft: Array(A,depth), rgt: Array(A,depth)) ~ (depth: Nat.succ(depth))
+}
+
+// Creates an array of depth `depth` and initial value `x`.
+Array.alloc<A: Type>(depth: Nat, x: A): Array(A, depth)
+  case depth {
+    zero: Array.tip<A>(x),
+    succ:
+      let half = Array.alloc<A>(depth.pred, x)
+      Array.tie<A, depth.pred>(half, half)
+  } : Array(A, depth)
+
+// Extracts the two subarrays of an array of depth greater than 0.
+Array.extract_tie<A: Type, depth: Nat>(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<A: Type>(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<A:Type, depth:Nat>(idx: Word(depth), arr: Array(A,depth)): A
+//   def P = (depth) Array(A,depth) -> A
+//   def nil = Array.extract_tip<A>
+//   def w0 = <idx.size> (rec) (arr)
+//     // get arr_l _ = Array.extract_tie<A, idx.size>(arr)
+//     let arr_l = Array.extract_tie<A, idx.size>(arr)
+//     case arr_l{
+//       new: arr_l.fst
+//     }
+//   def w1 = <idx.size> (rec) (arr)
+//     // get _ arr_r = Array.extract_tie<A, idx.size>(arr)
+//     let arr_r = Array.extract_tie<A, idx.size>(arr)
+//     case arr_r{
+//       new: rec(arr_r.snd)
+//     }
+//   Word.foldl<P, depth>(nil, w0, w1, idx, arr)
+
+// // Given array `arr`, little-endian word `idx` and function `f`, assigns `arr[idx] = f(arr[idx])`.
+// Array.mut<A:Type, depth:Nat>(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<A>(f(Array.extract_tip<A>(arr)))
+//   def w0 = <idx.size> (rec) (arr)
+//     let {arr_l, arr_r} = Array.extract_tie<A, idx.size>(arr)
+//     Array.tie<A, idx.size>(rec(arr_l), arr_r)
+//   def w1 = <idx.size> (rec) (arr)
+//     let {arr_l, arr_r} = Array.extract_tie<A, idx.size>(arr)
+//     Array.tie<A, idx.size>(arr_l, rec(arr_r))
+//   Word.foldl<P, depth>(nil, w0, w1, idx, arr)
+
+// // Given array `arr`, little-endian word `idx` and value `val`, assigns `arr[idx] = val`.
+// Array.set<A:Type, depth:Nat>(idx: Word(depth), val: A, arr: Array(A,depth))
+// : Array(A,depth)
+//   Array.mut<A,depth>(idx, () val, arr)
+

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

src/Bool.fm

@@ -40,3 +40,72 @@ Bool.if<A: Type>(cond: Bool, true_case: A, false_case: A): A
     true : true_case
     false: false_case
   }
+
+// Boolean negation, fusible
+// Bool.notf(a: Bool): Bool
+//   <P> (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, (b) Not(Equal(Bool, Bool.true, b))>(Bool.false)<Bool.true_isnt_false>;
+//   | Subset.new<Bool, (b) Not(Equal(Bool, Bool.false, b))>(Bool.true)<Bool.false_isnt_true>;
+
+
+// Dependent elimination of Bool.
+Bool.elim(b: Bool): <P: Bool -> Type> -> P(Bool.true) -> P(Bool.false) -> P(b)
+  <P> (t) (f) b<P>(t, f)
+
+Bool.and_var: (n: Nat) -> Variadic(n, Bool, Bool)
+  Variadic.foldr<Bool, Bool>(Bool.and, Bool.true)

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<U32>(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<U32, dep>(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<U32, dep>(idx, val, arr)
+//   Buffer32.new(dep, arr)
+