diff --git a/Bits.fm b/Bits.fm
index 2eabf00..e3016aa 100644
--- a/Bits.fm
+++ b/Bits.fm
@@ -1,6 +1,6 @@
// Bits.fm
// =======
-//
+//
// Defines a bitstream, or binary sequence.
import Equal
diff --git a/Dec.fm b/Dec.fm
new file mode 100644
index 0000000..cadc9c6
--- /dev/null
+++ b/Dec.fm
@@ -0,0 +1,47 @@
+import Nat
+
+T Dec
+| de
+| d0(pred : Dec)
+| d1(pred : Dec)
+| d2(pred : Dec)
+| d3(pred : Dec)
+| d4(pred : Dec)
+| d5(pred : Dec)
+| d6(pred : Dec)
+| d7(pred : Dec)
+| d8(pred : Dec)
+| d9(pred : Dec)
+
+incDec(x: Dec) : Dec
+ case x
+ | de => d1(de)
+ | d0 => d1(x.pred)
+ | d1 => d2(x.pred)
+ | d2 => d3(x.pred)
+ | d3 => d4(x.pred)
+ | d4 => d5(x.pred)
+ | d5 => d6(x.pred)
+ | d6 => d7(x.pred)
+ | d7 => d8(x.pred)
+ | d8 => d9(x.pred)
+ | d9 => d0(incDec(x.pred))
+
+decToNat(x: Dec) : Nat
+ case x
+ | de => zero
+ | d0 => mul(10n, decToNat(x.pred))
+ | d1 => add(1n, mul(10n, decToNat(x.pred)))
+ | d2 => add(2n, mul(10n, decToNat(x.pred)))
+ | d3 => add(3n, mul(10n, decToNat(x.pred)))
+ | d4 => add(4n, mul(10n, decToNat(x.pred)))
+ | d5 => add(5n, mul(10n, decToNat(x.pred)))
+ | d6 => add(6n, mul(10n, decToNat(x.pred)))
+ | d7 => add(7n, mul(10n, decToNat(x.pred)))
+ | d8 => add(8n, mul(10n, decToNat(x.pred)))
+ | d9 => add(9n, mul(10n, decToNat(x.pred)))
+
+natToDec(x: Nat) : Dec
+ case x
+ | zero => de
+ | succ => incDec(natToDec(x.pred))
diff --git a/Equal.fm b/Equal.fm
index 7853477..367a8e9 100644
--- a/Equal.fm
+++ b/Equal.fm
@@ -5,9 +5,12 @@
// `Equal(A,a,b)` contains the reflexive constructor that
// `a` equals itself, which implies `b` is equal to `a` iff
// `b` reduces to `a`.
-//
+//
// == is sugar for Equal(A, a, b)
+import Pair
+import Sigma
+
// Definition
// ----------
@@ -40,3 +43,11 @@ chain(A; a; b; c; ab: a == b, bc: b == c) : a == c
case bc
| equal => ab
: Equal(A, a, bc.b)
+
+copy_equal(A; a; b; e: a == b) : #{a == b, a == b}
+ case e
+ | equal => #[equal(__), equal(__)]
+ : Pair(Equal(A,a,e.b), Equal(A,a,e.b))
+
+Same(A, x : A) : Type
+ Sigma(A, (y : A) => Equal(A,x,y))
diff --git a/old/Fin.fm b/Fin.fm
similarity index 62%
rename from old/Fin.fm
rename to Fin.fm
index a91503d..5a75bab 100644
--- a/old/Fin.fm
+++ b/Fin.fm
@@ -8,34 +8,34 @@ import Empty
// = Definition =
// ========================================================
-T Fin (lim : -Nat)
-| fzero(~lim : -Nat) : Fin(succ(lim))
-| fsucc(~lim : -Nat, pred : Fin(lim)) : Fin(succ(lim))
+T Fin (lim : Nat)
+| fzero(lim : Nat;) : Fin(succ(lim))
+| fsucc(lim : Nat; pred : Fin(lim)) : Fin(succ(lim))
// ========================================================
// = Operations =
// ========================================================
-fin_inc(~lim : -Nat, fin : Fin(lim)) : Fin(succ(lim))
+fin_inc(lim : Nat; fin : Fin(lim)) : Fin(succ(lim))
case fin
- | fzero => fzero(~succ(fin.lim))
- | fsucc => fsucc(~succ(fin.lim), fin_inc(~fin.lim, fin.pred))
+ | fzero => fzero(succ(fin.lim);)
+ | fsucc => fsucc(succ(fin.lim); fin_inc(fin.lim; fin.pred))
: Fin(succ(fin.lim))
// ========================================================
// = Conversion =
// ========================================================
-fin_to_nat(~lim : -Nat, fin : Fin(lim)) : Nat
+fin_to_nat(lim : Nat; fin : Fin(lim)) : Nat
case fin
| fzero => zero
- | fsucc => succ(fin_to_nat(~fin.lim, fin.pred))
+ | fsucc => succ(fin_to_nat(fin.lim; fin.pred))
: Nat
nat_to_fin(n : Nat) : Fin(succ(n))
case n
- | zero => fzero(~zero)
- | succ => fsucc(~succ(n.pred), nat_to_fin(n.pred))
+ | zero => fzero(zero;)
+ | succ => fsucc(succ(n.pred); nat_to_fin(n.pred))
: Fin(succ(n))
// ========================================================
@@ -44,7 +44,7 @@ nat_to_fin(n : Nat) : Fin(succ(n))
no_fin_zero(fin : Fin(zero)) : Empty
case fin
- + refl(~Nat, ~zero) as e : Equal(Nat, fin.lim, zero)
- | fzero => succ_isnt_zero(~fin.lim, e)
- | fsucc => succ_isnt_zero(~fin.lim, e)
+ + equal(Nat; zero;) as e : Equal(Nat, fin.lim, zero)
+ | fzero => succ_isnt_zero(fin.lim; e)
+ | fsucc => succ_isnt_zero(fin.lim; e)
: Empty
diff --git a/Function.fm b/Function.fm
index 952a6b0..81473d2 100644
--- a/Function.fm
+++ b/Function.fm
@@ -1,6 +1,6 @@
// Function.fm
// ===========
-//
+//
// Wrapper and utilities for the built-in function type.
import Equal
diff --git a/Hex.fm b/Hex.fm
new file mode 100644
index 0000000..ec1e785
--- /dev/null
+++ b/Hex.fm
@@ -0,0 +1,66 @@
+import Nat
+
+T Hex
+| xe
+| x0(pred : Hex)
+| x1(pred : Hex)
+| x2(pred : Hex)
+| x3(pred : Hex)
+| x4(pred : Hex)
+| x5(pred : Hex)
+| x6(pred : Hex)
+| x7(pred : Hex)
+| x8(pred : Hex)
+| x9(pred : Hex)
+| xA(pred : Hex)
+| xB(pred : Hex)
+| xC(pred : Hex)
+| xD(pred : Hex)
+| xE(pred : Hex)
+| xF(pred : Hex)
+
+incHex(x: Hex) : Hex
+ case x
+ | xe => x1(xe)
+ | x0 => x1(x.pred)
+ | x1 => x2(x.pred)
+ | x2 => x3(x.pred)
+ | x3 => x4(x.pred)
+ | x4 => x5(x.pred)
+ | x5 => x6(x.pred)
+ | x6 => x7(x.pred)
+ | x7 => x8(x.pred)
+ | x8 => x9(x.pred)
+ | x9 => xA(x.pred)
+ | xA => xB(x.pred)
+ | xB => xC(x.pred)
+ | xC => xD(x.pred)
+ | xD => xE(x.pred)
+ | xE => xF(x.pred)
+ | xF => x0(incHex(x.pred))
+
+hexToNat(x: Hex) : Nat
+ case x
+ | xe => zero
+ | x0 => mul(10n, hexToNat(x.pred))
+ | x1 => add(1n, mul(10n, hexToNat(x.pred)))
+ | x2 => add(2n, mul(10n, hexToNat(x.pred)))
+ | x3 => add(3n, mul(10n, hexToNat(x.pred)))
+ | x4 => add(4n, mul(10n, hexToNat(x.pred)))
+ | x5 => add(5n, mul(10n, hexToNat(x.pred)))
+ | x6 => add(6n, mul(10n, hexToNat(x.pred)))
+ | x7 => add(7n, mul(10n, hexToNat(x.pred)))
+ | x8 => add(8n, mul(10n, hexToNat(x.pred)))
+ | x9 => add(9n, mul(10n, hexToNat(x.pred)))
+ | xA => add(10n, mul(10n, hexToNat(x.pred)))
+ | xB => add(11n, mul(10n, hexToNat(x.pred)))
+ | xC => add(12n, mul(10n, hexToNat(x.pred)))
+ | xD => add(13n, mul(10n, hexToNat(x.pred)))
+ | xE => add(14n, mul(10n, hexToNat(x.pred)))
+ | xF => add(15n, mul(10n, hexToNat(x.pred)))
+
+natToHex(x: Nat) : Hex
+ case x
+ | zero => xe
+ | succ => incHex(natToHex(x.pred))
+
diff --git a/old/IBin.fm b/IBin.fm
similarity index 75%
rename from old/IBin.fm
rename to IBin.fm
index 114ec39..3e3fa62 100644
--- a/old/IBin.fm
+++ b/IBin.fm
@@ -2,22 +2,17 @@
IBin : Type
${self}
( P : IBin -> Type;
- ileaf : ! P(ileaf),
- inode : ! (k : -IBin; a : P(k), b : P(k)) -> P(inode(k))
- ) -> ! P(self)
+ ileaf : P(ileaf),
+ inode : (k : IBin; a : P(k), b : P(k)) -> P(inode(k))
+ ) -> P(self)
inode(k: IBin) : IBin
new(IBin) (P; ileaf, inode) =>
- dup ileaf = ileaf
- dup inode = inode
- dup endfold = (use(k))((x) => P(x); #ileaf, #inode)
- # inode(k; endfold, endfold)
+ let endfold = (use(k))((x) => P(x); ileaf, inode)
+ inode(k; endfold, endfold)
ileaf : IBin
- new(IBin) (P; ileaf, inode) =>
- dup ileaf = ileaf
- dup inode = inode
- # ileaf
+ new(IBin) (P; ileaf, inode) => ileaf
t0 : IBin; ileaf
t1 : IBin; inode(t0)
diff --git a/IBits.fm b/IBits.fm
new file mode 100644
index 0000000..c43827b
--- /dev/null
+++ b/IBits.fm
@@ -0,0 +1,24 @@
+// Inductive bits
+IBits : Type
+ ${self}
+ ( P : IBits -> Type;
+ ibe : P(ibe),
+ ib0 : (bs : IBits; i : P(bs)) -> P(ib0(bs)),
+ ib1 : (bs : IBits; i : P(bs)) -> P(ib1(bs))
+ ) -> P(self)
+
+// IBits end
+ibe : IBits
+ new(IBits) (P; ibe, ib0, ib1) => ibe
+
+// IBits zero
+ib0(bs: IBits) : IBits
+ new(IBits) (P; ibe, ib0, ib1) =>
+ let ifn = (use(bs))((x) => P(x); ibe, ib0, ib1)
+ ib0(bs; ifn)
+
+// IBits one
+ib1(bs: IBits) : IBits
+ new(IBits) (P; ibe, ib0, ib1) =>
+ let ifn = (use(bs))((x) => P(x); ibe, ib0, ib1)
+ ib1(bs; ifn)
diff --git a/old/INat.fm b/INat.fm
similarity index 83%
rename from old/INat.fm
rename to INat.fm
index b9f9db6..b66862e 100644
--- a/old/INat.fm
+++ b/INat.fm
@@ -13,24 +13,17 @@ import Equal
INat : Type
${self}
( P : INat -> Type;
- izero : ! P(izero),
- isucc : ! (r : -INat; i : P(r)) -> P(isucc(r))
- ) -> ! P(self)
+ izero : P(izero),
+ isucc : (r : INat; i : P(r)) -> P(isucc(r))
+ ) -> P(self)
// INat successor
isucc(r : INat) : INat
- new(INat) (P; izero, isucc) =>
- dup izero = izero
- dup isucc = isucc
- dup irest = (use(r))((x) => P(x); #izero, #isucc)
- # isucc(r; irest)
+ new(INat) (P; izero, isucc) => isucc(r; (use(r))((x) => P(x); izero, isucc))
// INat zero
izero : INat
- new(INat) (P; izero, isucc) =>
- dup izero = izero
- dup isucc = isucc
- # izero
+ new(INat) (P; izero, isucc) => izero
// Operations
@@ -40,24 +33,21 @@ izero : INat
induct(
n: INat,
P: INat -> Type;
- z: !P(izero),
- s: !(n : -INat; i : P(n)) -> P(isucc(n))
-) : !P(n)
+ z: P(izero),
+ s: (n : INat; i : P(n)) -> P(isucc(n))
+) : P(n)
(use(n))((x) => P(x); z, s)
// Simple induction is recursion.
-recurse(n: INat, P: Type; z: ! P, s: ! P -> P) : !P
- dup s = s
- (use(n))((x) => P; z, #(i;) => s)
+recurse(n: INat, P: Type; z: P, s: P -> P) : P
+ (use(n))((x) => P; z, (i;) => s)
// Doubles an INat.
imul2(n: INat) : INat
new(INat) (P; b, s) =>
- dup b = b
- dup s = s
let t = (n) => P(imul2(n))
let s = (n; i) => s(isucc(imul2(n)); s(imul2(n); i))
- (use(n))(t; #b, #s)
+ (use(n))(t; b, s)
//// Adds two INats.
//plus : {a : INat, b : INat} -> INat
diff --git a/Map.fm b/Map.fm
index b29a475..b5818c4 100644
--- a/Map.fm
+++ b/Map.fm
@@ -164,3 +164,5 @@ map_example1 : Pair(Maybe(Bits), Maybe(Bits))
case query(Bits; qry, 10100100b, map) as q0
| pair => case query(Bits; qry, 01100010b, q0.fst) as q1
| pair => pair(__ q0.snd, q1.snd)
+
+
diff --git a/Nat.fm b/Nat.fm
index 5b57aa6..0609dab 100644
--- a/Nat.fm
+++ b/Nat.fm
@@ -32,11 +32,23 @@ pred(n: Nat) : Nat
| succ => n.pred
// Copies a Nat
-copy_nat(n: Nat) : Pair(Nat, Nat)
+copy_nat(n: Nat) : #{Nat, Nat}
case n
- | zero => pair(__ zero, zero)
+ | zero => #[zero, zero]
| succ => case copy_nat(n.pred) as pred
- | pair => pair(__ succ(pred.fst), succ(pred.snd))
+ | pair => #[succ(pred.fst), succ(pred.snd)]
+
+clone_nat(n: Nat) : #{Same(Nat,n),Same(Nat,n)}
+ case n
+ | zero => #[sigma(__ zero, equal(__)),sigma(__ zero, equal(__))]
+ | succ =>
+ get #[n1,n2] = clone_nat(n.pred)
+ get #[n1v,n1e] = n1
+ get #[n2v,n2e] = n2
+ let e1 = apply(_____ n1e)
+ let e2 = apply(_____ n2e)
+ #[sigma(__ succ(n1v), e1), sigma(__ succ(n2v), e2)]
+ : Pair(Same(Nat,n), Same(Nat,n))
// Addition
add(n: Nat, m: Nat) : Nat
@@ -120,6 +132,10 @@ zero_isnt_succ(n: Nat;): zero != succ(n)
apply_succ(n: Nat; m; e: n == m) : succ(n) == succ(m)
apply(_____ e)
+// Proof that `succ(n) == succ(m)` implies `n == m`
+apply_pred(n: Nat; m; e: succ(n) == succ(m)) : n == m
+ apply(____ pred; e)
+
// Tests
// -----
diff --git a/Path.fm b/Path.fm
new file mode 100644
index 0000000..1cf3760
--- /dev/null
+++ b/Path.fm
@@ -0,0 +1,13 @@
+import Nat
+
+T Path (len : Nat)
+| pe : Path(zero)
+| pl(len: Nat, pred: Path(len)) : Path(succ(len))
+| pr(len: Nat, pred: Path(len)) : Path(succ(len))
+
+path_len(len: Nat, path: Path(len)) : Nat
+ case path
+ | pe => zero
+ | pl => succ(path_len(path.len, path.pred))
+ | pr => succ(path_len(path.len, path.pred))
+ : Nat
diff --git a/String.fm b/String.fm
index aacf4f5..e74a554 100644
--- a/String.fm
+++ b/String.fm
@@ -5,6 +5,8 @@
import Bits
import List
+import Dec
+import Hex
// Definition
// ----------
@@ -28,3 +30,45 @@ string.test : Output
let str = "Hello, world!"
let str = reverse(_ str)
print(str)
+
+printBits(x: Bits) : String
+ case x
+ | be => nil(_)
+ | b0 => cons(_ 110000b, printBits(x.pred))
+ | b1 => cons(_ 110001b, printBits(x.pred))
+
+printDec(x: Dec) : String
+ case x
+ | de => nil(_)
+ | d0 => cons(_ 110000b, printDec(x.pred))
+ | d1 => cons(_ 110001b, printDec(x.pred))
+ | d2 => cons(_ 110010b, printDec(x.pred))
+ | d3 => cons(_ 110011b, printDec(x.pred))
+ | d4 => cons(_ 110100b, printDec(x.pred))
+ | d5 => cons(_ 110101b, printDec(x.pred))
+ | d6 => cons(_ 110110b, printDec(x.pred))
+ | d7 => cons(_ 110111b, printDec(x.pred))
+ | d8 => cons(_ 111000b, printDec(x.pred))
+ | d9 => cons(_ 111001b, printDec(x.pred))
+
+printHex(x: Hex) : String
+ case x
+ | xe => nil(_)
+ | x0 => cons(_ 110000b, printDec(x.pred))
+ | x1 => cons(_ 110001b, printDec(x.pred))
+ | x2 => cons(_ 110010b, printDec(x.pred))
+ | x3 => cons(_ 110011b, printDec(x.pred))
+ | x4 => cons(_ 110100b, printDec(x.pred))
+ | x5 => cons(_ 110101b, printDec(x.pred))
+ | x6 => cons(_ 110110b, printDec(x.pred))
+ | x7 => cons(_ 110111b, printDec(x.pred))
+ | x8 => cons(_ 111000b, printDec(x.pred))
+ | x9 => cons(_ 111001b, printDec(x.pred))
+ | xA => cons(_ 100001b, printDec(x.pred))
+ | xB => cons(_ 100010b, printDec(x.pred))
+ | xC => cons(_ 100011b, printDec(x.pred))
+ | xD => cons(_ 100100b, printDec(x.pred))
+ | xE => cons(_ 100101b, printDec(x.pred))
+ | xF => cons(_ 100110b, printDec(x.pred))
+
+
diff --git a/old/Tree.fm b/Tree.fm
similarity index 57%
rename from old/Tree.fm
rename to Tree.fm
index c5b70b9..498aa63 100644
--- a/old/Tree.fm
+++ b/Tree.fm
@@ -7,6 +7,6 @@ import Nat
// = Definition =
// ========================================================
-T Tree (n : -Nat)
-| node(~n : Nat, x : A, a : Tree(A, n), b : Tree(A, n)) : Tree(A, succ(n))
-| leaf : Tree(A, zero)
+T Tree (n : Nat)
+| node(n : Nat, x : A, a : Tree(A, n), b : Tree(A, n)) : Tree(A, succ(n))
+| leaf : Tree(A, zero)
diff --git a/Vector.fm b/Vector.fm
new file mode 100644
index 0000000..5ebcb96
--- /dev/null
+++ b/Vector.fm
@@ -0,0 +1,59 @@
+/* Vector.fm defines a static-length vector type
+ */
+
+import Equal
+import Fin
+import Nat
+import Unit
+
+// ========================================================
+// = Definition =
+// ========================================================
+
+// A vector is a list with a statically known length
+T Vector (len : Nat)
+| vnil : Vector(A, zero)
+| vcons(len : Nat; head : A, tail : Vector(A, len)) : Vector(A, succ(len))
+
+// ========================================================
+// = Operations =
+// ========================================================
+
+// Returns the first element of a non-empty vector
+vhead(A; len : Nat; xs : Vector(A, succ(len))) : A
+ case xs
+ + equal(__) as e : xs.len == succ(len)
+ | vnil => absurd(zero_isnt_succ(_ e), A;)
+ | vcons => xs.head
+
+// Returns all but the first element of a non-empty vector
+vtail(A; len : Nat; xs : Vector(A, succ(len))) : Vector(A, len)
+ case xs
+ + equal(__) as e : xs.len == succ(len)
+ | vnil => absurd(zero_isnt_succ(_ e), Vector(A, zero);)
+ | vcons => xs.tail
+ : Vector(A, pred(xs.len))
+
+// Returns a pair with the head and the tail of a non-empty vector
+vtake(A; len : Nat; xs : Vector(A, succ(len))) : #{A, Vector(A, len)}
+ case xs
+ + equal(__) as e : xs.len == succ(len)
+ | vnil => absurd(zero_isnt_succ(_ e), #{A, Vector(A, zero)};)
+ | vcons => #[xs.head, xs.tail]
+ : #{A, Vector(A, pred(xs.len))}
+
+// Returns the same vector
+vsame(A; len : Nat; xs : Vector(A, len)) : Vector(A, len)
+ case xs
+ | vnil => vnil(_)
+ | vcons => vcons(__ xs.head, vsame(__ xs.tail))
+ : Vector(A, xs.len)
+
+// Allocates a Vec with given length
+valloc(len : Nat) : Vector(Unit, len)
+ case len
+ | zero => vnil(_)
+ | succ => vcons(_ _ unit, valloc(len.pred))
+ : Vector(Unit, len)
+
+// TODO: range, map, concat, zip, etc.
diff --git a/Word.fm b/Word.fm
new file mode 100644
index 0000000..582f195
--- /dev/null
+++ b/Word.fm
@@ -0,0 +1,193 @@
+// Word.fm defines a bitstream with static length
+
+import Nat
+import Equal
+import Bits
+import The
+
+T Word (len : Nat)
+| we : Word(zero)
+| w0(len : Nat, pred : Word(len)) : Word(succ(len))
+| w1(len : Nat, pred : Word(len)) : Word(succ(len))
+
+wordToBits(n : Nat, w : Word(n)) : Bits
+ case w
+ | we => be
+ | w0 => b0(wordToBits(w.len,w.pred))
+ | w1 => b1(wordToBits(w.len,w.pred))
+ : Bits
+
+wordToNat(n : Nat, w : Word(n)) : Nat
+ bits_to_nat(word_to_bits(n,w))
+
+bitsToWord(l : Nat, b : Bits) : Word(l)
+ get #[x, y] = clone_nat(l)
+ get #[n, ne] = x
+ get #[m, me] = y
+ case n
+ + ne : l == n
+ + m : Nat
+ + me : l == m
+ | zero => rewrite(___ mirror(___ ne), (x) => Word(x); we)
+ | succ =>
+ let bs = case b
+ + m : Nat
+ | be => w0(?, bitsToWord(pred(m), be))
+ | b0 => w0(?, bitsToWord(pred(m),b.pred))
+ | b1 => w1(?, bitsToWord(pred(m),b.pred))
+ : Word(succ(pred(m)))
+ get #[ne1,ne2] = copy_equal(Nat;l;succ(n.pred);ne)
+ let mn = apply(_____ chain(____ mirror(___ me),ne1))
+ let bs = rewrite(___ mn,(x) => Word(succ(x));bs)
+ rewrite(___ mirror(___ ne2),Word;bs)
+ : Word(l)
+
+natToWord(l: Nat, n: Nat) : Word(l)
+ bitsToWord(l, nat_to_bits(n))
+
+
+word.not(n: Nat, x: Word(n)) : Word(n)
+ case x
+ + equal(__) as e : x.len == n
+ | we => rewrite(___ e, Word; we)
+ | w0 => rewrite(___ e, Word; w1(x.len,word.not(x.len,x.pred)))
+ | w1 => rewrite(___ e, Word; w0(x.len,word.not(x.len,x.pred)))
+ : Word(n)
+
+
+word.and(n: Nat, x: Word(n), y: Word(n)) : Word(n)
+ case x
+ + y : Word(n)
+ + equal(__) as ex : x.len == n
+ | we => rewrite(___ ex, Word; we)
+ | w0 =>
+ case y
+ + ex : succ(x.len) == n
+ + equal(__) as ey : y.len == n
+ | we => rewrite(___ ey, Word; we)
+ | w0 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let xy = chain(____ ey, mirror(___ x1))
+ let yp = rewrite(___ apply(____ pred; xy), Word; y.pred)
+ rewrite(___ x2,Word; w0(x.len,word.and(x.len,x.pred,yp)))
+ | w1 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let xy = chain(____ ey, mirror(___ x1))
+ let yp = rewrite(___ apply(____ pred; xy), Word; y.pred)
+ rewrite(___ x2,Word; w0(x.len,word.and(x.len,x.pred,yp)))
+ | w1 =>
+ case y
+ + ex : succ(x.len) == n
+ + equal(__) as ey : y.len == n
+ | we => rewrite(___ ey, Word; we)
+ | w0 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let xy = chain(____ ey, mirror(___ x1))
+ let yp = rewrite(___ apply(____ pred; xy), Word; y.pred)
+ rewrite(___ x2,Word; w0(x.len,word.and(x.len,x.pred,yp)))
+ | w1 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let xy = chain(____ ey, mirror(___ x1))
+ let yp = rewrite(___ apply(____ pred; xy), Word; y.pred)
+ rewrite(___ x2,Word; w1(x.len,word.and(x.len,x.pred,yp)))
+ : Word(n)
+
+word.and2(n: Nat, x: Word(n), y: Word(n)) : Word(n)
+ let x = wordToBits(n,x)
+ let y = wordToBits(n,y)
+ bitsToWord(n,and_bits(x,y))
+
+word.inc(n: Nat, x : Word(n)) : #{Word(n), Bool}
+ case x
+ + equal(__) as e : x.len == n
+ | we => #[rewrite(___ e,Word;we), true]
+ | w0 => #[rewrite(___ e,Word; w1(x.len,x.pred)), false]
+ | w1 =>
+ get #[w, b] = word.inc(x.len,x.pred)
+ #[rewrite(___ e,Word; w0(x.len,w)), b]
+ : #{Word(n), Bool}
+
+// n + 1 == l && m + 1 == l => n = m
+pred_chain(n: Nat; m: Nat; l: Nat; nl: succ(n) == l, ml: succ(m) == l) : n == m
+ apply(____ pred; chain(____ nl, mirror(___ ml)))
+
+word.adder(n: Nat, c: Bool, x: Word(n), y: Word(n)) : #{Word(n), Bool}
+ case x
+ + y : Word(n)
+ + equal(__) as ex : x.len == n
+ + c : Bool
+ | we => #[rewrite(___ ex,_ we), c]
+ | w0 =>
+ case y
+ + c : Bool
+ + ex : succ(x.len) == n
+ + equal(__) as ey : Equal(Nat,y.len,n)
+ | we => #[rewrite(___ ey,_ we), c]
+ | w0 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let yp = rewrite(___ pred_chain(___ ey,x1),_ y.pred)
+ get #[w,b] = word.adder(x.len,false,x.pred,yp)
+ let w = case c
+ + w : Word(x.len)
+ | true => w1(?,w)
+ | false => w0(?,w)
+ #[rewrite(___ x2,_ w), b]
+ | w1 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let yp = rewrite(___ pred_chain(___ ey,x1),_ y.pred)
+ get #[c1, c2] = copy_bool(c)
+ get #[w,b] = word.adder(x.len,c1,x.pred,yp)
+ let w = case c2
+ + w : Word(x.len)
+ | true => w0(?, w)
+ | false => w1(?, w)
+ #[rewrite(___ x2,_ w), b]
+ | w1 =>
+ case y
+ + c : Bool
+ + ex : succ(x.len) == n
+ + equal(__) as ey : Equal(Nat,y.len,n)
+ | we => #[rewrite(___ ey,_ we), c]
+ | w0 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let yp = rewrite(___ pred_chain(___ ey,x1),_ y.pred)
+ get #[c1, c2] = copy_bool(c)
+ get #[w,b] = word.adder(x.len,c1,x.pred,yp)
+ let w = case c2
+ + w : Word(x.len)
+ | true => w1(?,w)
+ | false => w0(?,w)
+ #[rewrite(___ x2,_ w), b]
+ | w1 =>
+ get #[x1, x2] = copy_equal(___ ex)
+ let yp = rewrite(___ pred_chain(___ ey,x1),_ y.pred)
+ get #[w,b] = word.adder(x.len,true,x.pred,yp)
+ let w = case c
+ + w : Word(x.len)
+ | true => w0(?, w)
+ | false => w1(?, w)
+ : Word(succ(x.len))
+ #[rewrite(___ x2,_ w), b]
+ : #{Word(n), Bool}
+
+word.add(n: Nat, x: Word(n), y: Word(n)) : Word(n)
+ pair_fst(__ word.adder(n, false, x, y))
+
+----w_7 : Word(4n)
+---- w1(_ w1(_ w1(_ w0(_ we))))
+----
+----word.add_test : The([:Number, Bool],[14,false])
+---- get [x,b] = word.adder(4n, false, w_7, w_7)
+---- let x = bits_to_nat(word_to_bits(4n,x))
+---- the(~[:Number, Bool], [nat_to_number(x), b])
+----
+----word.add_test2 : The([:Number, Bool],[14,true])
+---- get [x,b] = word.adder(4n, false, w_15, w_15)
+---- let x = bits_to_nat(word_to_bits(4n,x))
+---- the(~[:Number, Bool], [nat_to_number(x), b])
+----
+----word.add_test3 : The([:Number, Bool],[0,true])
+---- let w8 = nat_to_word(4n, 8n)
+---- get [x,b] = word.adder(4n, false, w8, w8)
+---- let x = word_to_nat(4n,x)
+---- the(~[:Number, Bool], [nat_to_number(x), b])
diff --git a/old/Array.fm b/old/Array.fm
deleted file mode 100644
index d1473a5..0000000
--- a/old/Array.fm
+++ /dev/null
@@ -1,172 +0,0 @@
-import Nat
-import Path
-import The
-import IBin
-import IBits
-
-Array(A, n : Nat) : Type
- case n
- | zero => A
- | succ => [x : Array(A, n.pred), Array(A, n.pred)]
- : Type
-
-// ::::::::::::
-// :: Getter ::
-// ::::::::::::
-
-// Returns a value and destroys the array
-Getter(A, n : Nat) : Type
- (arr : Array(A, n)) -> A
-
-get.end(~A) : Getter(A, zero)
- (a) => a
-
-get.lft(~A, ~n : -Nat, g : Getter(A, n)) : Getter(A, succ(n))
- (a) => get [x,y] = a; g(x)
-
-get.rgt(~A, ~n : -Nat, g : Getter(A, n)) : Getter(A, succ(n))
- (a) => get [x,y] = a; g(y)
-
-getter#(~A : Type, path : IBits) : !Getter(A, $ibits_to_nat(path))
- let moti = (path) => Getter(A, $ibits_to_nat(path))
- let ibe = get.end(~A)
- let ib0 = (~bs) => get.lft(~A, ~$ibits_to_nat(bs))
- let ib1 = (~bs) => get.rgt(~A, ~$ibits_to_nat(bs))
- use(path)(~moti, #ibe, #ib0, #ib1)
-
-path_to_getter(~A : Type, ~len : -Nat, path : Path(len)) : Getter(A, len)
- case path
- | pe => get.end(~A)
- | pl => get.lft(~A, ~path.len, path_to_getter(~A, ~path.len, path.pred))
- | pr => get.rgt(~A, ~path.len, path_to_getter(~A, ~path.len, path.pred))
- : Getter(A, path.len)
-
-// ::::::::::::
-// :: Mutter ::
-// ::::::::::::
-
-// Applies a function to a value
-Mutter(A, n : Nat) : Type
- (arr : Array(A, n), fun : A -> A) -> Array(A, n)
-
-mut.end(~A) : Mutter(A, zero)
- (a, f) => f(a)
-
-mut.lft(~A, ~n : -Nat, g : Mutter(A, n)) : Mutter(A, succ(n))
- (a, f) => get [x,y] = a; [g(x,f),y]
-
-mut.rgt(~A, ~n : -Nat, g : Mutter(A, n)) : Mutter(A, succ(n))
- (a, f) => get [x,y] = a; [x,g(y,f)]
-
-mutter#(~A : Type, path : IBits) : !Mutter(A, $ibits_to_nat(path))
- let moti = (path) => Mutter(A, $ibits_to_nat(path))
- let ibe = mut.end(~A)
- let ib0 = (~bs) => mut.lft(~A, ~$ibits_to_nat(bs))
- let ib1 = (~bs) => mut.rgt(~A, ~$ibits_to_nat(bs))
- use(path)(~moti, #ibe, #ib0, #ib1)
-
-path_to_mutter(~A, ~len : -Nat, path : Path(len)) : Mutter(A, len)
- case path
- | pe => mut.end(~A)
- | pl => mut.lft(~A, ~path.len, path_to_mutter(~A, ~path.len, path.pred))
- | pr => mut.rgt(~A, ~path.len, path_to_mutter(~A, ~path.len, path.pred))
- : Mutter(A, path.len)
-
-// :::::::::::::
-// :: Querier ::
-// :::::::::::::
-
-// Reads a value, replaces it and returns a function of it and the array
-Querier(A, n : Nat) : Type
- (arr : Array(A, n), query : A -> [:A, A]) -> [: Array(A, n), A]
-
-query.end(~A) : Querier(A, zero)
- (a, q) => q(a)
-
-query.lft(~A, ~n : -Nat, r : Querier(A, n)) : Querier(A, succ(n))
- (a, q) => get [x,y] = a; get [x,k] = r(x,q); [[x,y],k]
-
-query.rgt(~A, ~n : -Nat, r : Querier(A, n)) : Querier(A, succ(n))
- (a, q) => get [x,y] = a; get [y,k] = r(y,q); [[x,y],k]
-
-querier#(~A : Type, path : IBits) : !Querier(A, $ibits_to_nat(path))
- let moti = (path) => Querier(A, $ibits_to_nat(path))
- let ibe = query.end(~A)
- let ib0 = (~bs) => query.lft(~A, ~$ibits_to_nat(bs))
- let ib1 = (~bs) => query.rgt(~A, ~$ibits_to_nat(bs))
- use(path)(~moti, #ibe, #ib0, #ib1)
-
-path_to_querier(~A, ~len : -Nat, path : Path(len)) : Querier(A, len)
- case path
- | pe => query.end(~A)
- | pl => query.lft(~A, ~path.len, path_to_querier(~A, ~path.len, path.pred))
- | pr => query.rgt(~A, ~path.len, path_to_querier(~A, ~path.len, path.pred))
- : Querier(A, path.len)
-
-// :::::::::::::::
-// :: Functions ::
-// :::::::::::::::
-
-// Applies a map/reduce operation over an array
-afold#(t : IBin, ~A : Type, id : !A -> A, fn : ! A -> A -> A)
-: !(Array(A, $ibin_to_nat(t)) -> A)
- dup id = id
- dup fn = fn
- let imoti = (t) => Array(A, $ibin_to_nat(t)) -> A
- let ileaf = (n) => id(n)
- let inode = (~k, a, b, arr) => get [lft, rgt] = arr; fn(a(lft), b(rgt))
- use(t)(~imoti, #ileaf, #inode)
-
-// Creates a range from 0 to 2^depth(t)
-arange#(t : IBin) : !Array(Number, $ibin_to_nat(t))
- let imoti = (t) => (n : Number) -> Array(Number, $ibin_to_nat(t))
- let ileaf = (n) => n
- let inode = (~k, a, b, n) => [
- a(n .*. 2),
- b((n .*. 2) .+. 1)
- ] :: Array(Number, $ibin_to_nat(inode(k)))
- dup start = use(t)(~imoti, #ileaf, #inode)
- # start(0)
-
-// Allocates an array with 2^depth(t) identical elements
-alloc#(t : IBin, ~A : Type, value : !A) : !Array(A, $ibin_to_nat(t))
- dup value = value
- let imoti = (t) => Array(A, $ibin_to_nat(t))
- let ileaf = value
- let inode = (~k, a, b) => [a, b] :: Array(A, $ibin_to_nat(inode(k)))
- use(t)(~imoti, #ileaf, #inode)
-
-// Sums the elements of an array
-asum#(t : IBin) : !Array(Number, $ibin_to_nat(t)) -> Number
- afold#(t, ~Number, #(x) => x, #.+.)
-
-// :::::::::::
-// :: Tests ::
-// :::::::::::
-
-// Summing 256 elements requires 2387 rewrites
-array.ex0
- dup arr = alloc#(t8, ~Number, #1) // creates range from 0 til 256
- dup sum = asum#(t8) // creates summing function
-# sum(arr)
-
-// Query uses ~185 rewrites per new index, ~41 rewrites per reused index
-array.ex1
- dup arr = arange#(t8) // creates range from 0 til 256
- dup qry0 = querier#(~Number, 00000000B) // querier for index 0
- dup qry1 = querier#(~Number, 00000001B) // querier for index 1
- dup qry2 = querier#(~Number, 00000010B) // querier for index 2
- dup qry3 = querier#(~Number, 00000011B) // querier for index 3
- dup qry4 = querier#(~Number, 00000100B) // querier for index 4
- dup qry5 = querier#(~Number, 00000101B) // querier for index 5
-# get [arr, a] = qry0(arr, (x) => [x .+. 10, x]) // a = arr[0]; arr[0] += 10;
- get [arr, b] = qry1(arr, (x) => [x, x .*. 10]) // b = arr[1] * 10;
- get [arr, c] = qry2(arr, (x) => [x, x]) // c = arr[2];
- get [arr, d] = qry3(arr, (x) => [x, x]) // d = arr[3];
- get [arr, e] = qry4(arr, (x) => [x, x]) // e = arr[4];
- get [arr, f] = qry5(arr, (x) => [x, x]) // f = arr[5];
- get [arr, g] = qry0(arr, (x) => [x, x]) // g = arr[0];
- get [arr, h] = qry0(arr, (x) => [x, x]) // h = arr[0];
- get [arr, i] = qry0(arr, (x) => [x, x]) // i = arr[0];
- get [arr, j] = qry0(arr, (x) => [x, x]) // j = arr[0];
- [a, b, c, d, e, f, g, h, i, j]
diff --git a/old/Contract.fm b/old/Contract.fm
deleted file mode 100644
index 0aa8555..0000000
--- a/old/Contract.fm
+++ /dev/null
@@ -1,141 +0,0 @@
-import List
-import Vector
-import Equal
-import Map
-
-// ::::::::::::::::::::::::::
-// :: Smart-Contract Model ::
-// ::::::::::::::::::::::::::
-
-// This is just a very initial draft, there is a lot of work to do!
-
-// An Ethereum address
-Address : Type
- Bits
-
-// A Private Key
-PrivateKey : Type
- Bits
-
-// A amount of Ether, in wei
-Amount : Type
- Bits
-
-// A signature
-Signature : Type
- [: Bits, Bits]
-
-// A signature scheme
-T SignatureScheme
-| signaturescheme(
- sign : (msg : Bits, pvt : PrivateKey) -> Signature,
- addr : (pvt : PrivateKey) -> Address,
- auth : (msg : Bits, sig : Signature) -> Address,
- fact : (msg : Bits, pvt : PrivateKey) ->
- Equal(Address,
- auth(msg, sign(msg, pvt)),
- addr(pvt)))
-
-// An Ethereum transaction
-T Transaction
-| transaction(
- from : Address,
- amount : Amount,
- data : Bits)
-
-// The effects of a transaction
-// TODO: should be an IO type
-T EthIO
-| done(
- cont : EthIO)
-| sstore(
- key : Bits,
- val : Bits,
- nxt : Unit -> EthIO)
-| sload(
- key : Bits,
- nxt : Bits -> EthIO)
-| send(
- adr : Address,
- val : Amount,
- nxt : Unit -> EthIO)
-
-// A contract is an initial state and a transaction function
-T Contract
-| contract(init : Storage, call : EthIO)
-
-get_contract_init(ct : Contract) : Storage
- case ct
- | contract => ct.init
- : Storage
-
-get_contract_call(ct : Contract) : EthIO
- case ct
- | contract => ct.call
- : EthIO
-
-// The contract storage
-Storage : Type
- Map(Bits)
-
-// The contract state is a pair of its balance and state
-State : Type
- [: Amount, Storage]
-
-// Performs an IO procedure under a State context
-perform_eth_io(call : EthIO, st : State) : [:EthIO, State]
- case call
- + st : State
- | done =>
- [call.cont, st]
- | sstore =>
- get [balance, storage] = st
- let storage = mset(~Bits, call.key, call.val, storage)
- perform_eth_io(call.nxt(unit), [balance, storage])
- | sload =>
- get [balance, storage] = st
- get [storage, val] = mqry(~Bits, bits.copy, call.key, storage)
- let val =
- case val
- | none => be
- | some => val.value
- : Bits
- perform_eth_io(call.nxt(val), [balance, storage])
- | send =>
- get [balance, storage] = st
- perform_eth_io(call.nxt(unit), [be, storage])
- : [:EthIO, State]
-
-// Auxiliar function of `compute`
-compute.go(io : EthIO, st : State, txs : List(Transaction)) : State
- case txs
- + st : State
- | nil => st
- | cons =>
- get [io, st] = perform_eth_io(io, st)
- compute.go(io, st, txs.tail)
- : State
-
-// Computes the final state of a contract given a list of transactions
-compute(ct : Contract, txs : List(Transaction)) : State
- case ct
- | contract => compute.go(ct.call, [be, ct.init], txs)
- : State
-
-// :::::::::::::::::::::::::
-// :: Examples & Theorems ::
-// :::::::::::::::::::::::::
-
-// A contract that does nothing
-contract0 : Contract
- contract(
- mleaf(~Bits),
- done(get_contract_call(contract0)))
-
-// A proof that its storage is always empty
-contract0.fact0(txs : List(Transaction))
-: Equal(Storage, snd(compute(contract0,txs)), mleaf(~Bits))
- case txs
- | nil => refl(~Storage, ~mleaf(~Bits))
- | cons => contract0.fact0(txs.tail)
- : Equal(Storage, snd(compute(contract0,txs)), mleaf(~Bits))
diff --git a/old/IBits.fm b/old/IBits.fm
deleted file mode 100644
index a789b8e..0000000
--- a/old/IBits.fm
+++ /dev/null
@@ -1,34 +0,0 @@
-// Inductive bits
-IBits : Type
- ${self}
- ( P : IBits -> Type;
- ibe : ! P(ibe),
- ib0 : ! (bs : -IBits; i : P(bs)) -> P(ib0(bs)),
- ib1 : ! (bs : -IBits; i : P(bs)) -> P(ib1(bs))
- ) -> ! P(self)
-
-// IBits end
-ibe : IBits
- new(IBits) (P; ibe, ib0, ib1) =>
- dup ibe = ibe
- dup ib0 = ib0
- dup ib1 = ib1
- # ibe
-
-// IBits zero
-ib0(bs: IBits) : IBits
- new(IBits) (P; ibe, ib0, ib1) =>
- dup ibe = ibe
- dup ib0 = ib0
- dup ib1 = ib1
- dup ifn = (use(bs))((x) => P(x); #ibe, #ib0, #ib1)
- # ib0(bs; ifn)
-
-// IBits one
-ib1(bs: IBits) : IBits
- new(IBits) (P; ibe, ib0, ib1) =>
- dup ibe = ibe
- dup ib0 = ib0
- dup ib1 = ib1
- dup ifn = (use(bs))((x) => P(x); #ibe, #ib0, #ib1)
- # ib1(bs; ifn)
diff --git a/old/Path.fm b/old/Path.fm
deleted file mode 100644
index bbfd788..0000000
--- a/old/Path.fm
+++ /dev/null
@@ -1,13 +0,0 @@
-import Nat
-
-T Path (len : Nat)
-| pe : Path(zero)
-| pl(~len : -Nat, pred : Path(len)) : Path(succ(len))
-| pr(~len : -Nat, pred : Path(len)) : Path(succ(len))
-
-path_len(~len : -Nat, path : Path(len)) : Nat
- case path
- | pe => zero
- | pl => succ(path_len(~path.len, path.pred))
- | pr => succ(path_len(~path.len, path.pred))
- : Nat
diff --git a/old/U32.fm b/old/U32.fm
deleted file mode 100644
index 43e5676..0000000
--- a/old/U32.fm
+++ /dev/null
@@ -1,88 +0,0 @@
-/* U32.fm is a temporary shim until we disentangle the OP1 operations
- * from the JavaScript number type
- */
-
-import Equal
-
-// ========================================================
-// = Definition =
-// ========================================================
-
-U32 : Type
- Number
-
-u32.max : U32; 4294967295
-u32.min : U32; 0
-
-u32.true : U32; 1
-u32.false : U32; 0
-
-// ========================================================
-// = Operations =
-// ========================================================
-
-u32op(f : (x : Number, y : Number) -> Number) : U32 -> U32 -> U32
- (x, y) => f(x .>>>. 0, y .>>>. 0) .>>>. 0
-
-add(x : U32, y : U32) : U32; u32op(.+., x, y)
-sub(x : U32, y : U32) : U32; u32op(.-., x, y)
-mul(x : U32, y : U32) : U32; u32op(.*., x, y)
-div(x : U32, y : U32) : U32; u32op(./., x, y)
-mod(x : U32, y : U32) : U32; u32op(.%., x, y)
-rsh(x : U32, y : U32) : U32; u32op(.>>>., x, y)
-lsh(x : U32, y : U32) : U32; u32op(.<<., x, y)
-and(x : U32, y : U32) : U32; u32op(.&., x, y)
- or(x : U32, y : U32) : U32; u32op(.|., x, y)
-xor(x : U32, y : U32) : U32; u32op(.^., x, y)
-gth(x : U32, y : U32) : U32; u32op(.>., x, y)
-lth(x : U32, y : U32) : U32; u32op(.<., x, y)
-gte(x : U32, y : U32) : U32; u32op(.<., x, y) .^. 1
-lte(x : U32, y : U32) : U32; u32op(.>., x, y) .^. 1
- eq(x : U32, y : U32) : U32; u32op(.==., x, y)
-neq(x : U32, y : U32) : U32; u32op(.==., x, y) .^. 1
-
-// ========================================================
-// = Type-Level Comparison =
-// ========================================================
-
-u32.is : Equal(U32, %1, %1); refl(~U32, ~%1)
-u32.isnt : Equal(U32, %0, %0); refl(~U32, ~%0)
-
-U32Is(x : U32) : Type; Equal(U32, x, 1)
-
-// ========================================================
-// = Safe Operations =
-// ========================================================
-
-safe.add(a : U32, b : U32, e : U32Is(gte(add(a,b), a))) : U32
- add(a,b)
-
-safe.sub(a : U32, b : U32, e : U32Is(lte(b,a))) : U32
- sub(a,b)
-
-safe.mul(a : U32, b : U32, e : U32Is(eq(div(mul(a,b),a),a))) : U32
- mul(a,b)
-
-safe.div(a : U32, b : U32, e : U32Is(neq(b,0))) : U32
- div(a,b)
-
-safe.mod(a : U32, b : U32, e : U32Is(neq(b,0))) : U32
- mod(a,b)
-
-test_add : U32; safe.add(1,2, u32.is)
-test_sub : U32; safe.sub(2,1, u32.is)
-test_mul : U32; safe.mul(3,3, u32.is)
-test_div : U32; safe.div(3,3, u32.is)
-test_mod : U32; safe.mod(3,3, u32.is)
-
-//test_add_overflow : U32; safe.add(u32.max,u32.max, u32.is)
-//test_sub_underflow : U32; safe.sub(1,2, u32.is)
-//test_mul_overflow : U32; safe.mul(u32.max,u32.max, u32.is)
-//test_div_by_zero : U32; safe.div(3,0, u32.is)
-//test_mod_by_zero : U32; div(3,0, u32.is)
-
-//// this is actually safe, but by construction rather than by proof
-safe.average(a : U32, b : U32) : U32
- let x = add(div(a,2),div(b,2))
- let y = add(mod(a,2),mod(b,2))
- add(x, div(y,2))
diff --git a/old/Vector.fm b/old/Vector.fm
deleted file mode 100644
index 9ac3626..0000000
--- a/old/Vector.fm
+++ /dev/null
@@ -1,60 +0,0 @@
-/* Vector.fm defines a static-length vector type
- */
-
-import Equal
-import Fin
-import Nat
-import Unit
-
-// ========================================================
-// = Definition =
-// ========================================================
-
-// A vector is a list with a statically known length
-T Vector (len : -Nat)
-| vnil : Vector(A, zero)
-| vcons(~len : -Nat, head : A, tail : Vector(A, len)) : Vector(A, succ(len))
-
-// ========================================================
-// = Operations =
-// ========================================================
-
-// Returns the first element of a non-empty vector
-vhead(~A, ~len : -Nat, xs : Vector(A, succ(len))) : A
- case xs
- + refl(~Nat, ~succ(len)) as e : Equal(Nat, xs.len, succ(len))
- | vnil => absurd(zero_isnt_succ(~len, e), ~A)
- | vcons => xs.head
- : A
-
-// Returns all but the first element of a non-empty vector
-vtail(~A, ~len : -Nat, xs : Vector(A, succ(len))) : Vector(A, len)
- case xs
- + refl(~Nat, ~succ(len)) as e : Equal(Nat, xs.len, succ(len))
- | vnil => absurd(zero_isnt_succ(~len, e), ~Vector(A, zero))
- | vcons => xs.tail
- : Vector(A, pred(xs.len))
-
-// Returns a pair with the head and the tail of a non-empty vector
-vtake(~A, ~len : -Nat, xs : Vector(A, succ(len))) : [:A, Vector(A, len)]
- case xs
- + refl(~Nat, ~succ(len)) as e : Equal(Nat, xs.len, succ(len))
- | vnil => absurd(zero_isnt_succ(~len, e), ~[:A, Vector(A, zero)])
- | vcons => [xs.head, xs.tail]
- : [:A, Vector(A, pred(xs.len))]
-
-// Returns the same vector
-vsame(~A, ~len : -Nat, xs : Vector(A, len)) : Vector(A, len)
- case xs
- | vnil => vnil(~A)
- | vcons => vcons(~A, ~xs.len, xs.head, vsame(~A, ~xs.len, xs.tail))
- : Vector(A, xs.len)
-
-// Allocates a Vec with given length
-valloc(len : Nat) : Vector(Unit, len)
- case len
- | zero => vnil(~Unit)
- | succ => vcons(~Unit, ~len.pred, unit, valloc(len.pred))
- : Vector(Unit, len)
-
-// TODO: range, map, concat, zip, etc.
diff --git a/old/Word.fm b/old/Word.fm
deleted file mode 100644
index 3d1e262..0000000
--- a/old/Word.fm
+++ /dev/null
@@ -1,237 +0,0 @@
-// Word.fm defines a bitstream with static length
-
-import Nat
-import Equal
-import Bits
-import The
-
-T Word (len : -Nat)
-| we : Word(zero)
-| w0(~len : -Nat, pred : Word(len)) : Word(succ(len))
-| w1(~len : -Nat, pred : Word(len)) : Word(succ(len))
-
-word_to_bits(n : -Nat, w : Word(n)) : Bits
- case w
- | we => be
- | w0 => b0(word_to_bits(w.len,w.pred))
- | w1 => b1(word_to_bits(w.len,w.pred))
- : Bits
-
-word_to_nat(n : -Nat, w : Word(n)) : Nat
- bits_to_nat(word_to_bits(n,w))
-
-bits_to_word(l : Nat, b : Bits) : Word(l)
- get [x, y] = clone_nat(l)
- get [n, ne] = x
- get [m, me] = y
- case n
- + ne : Equal(Nat,n,l)
- + m : Nat
- + me : Equal(Nat,m,l)
- | zero => rewrite(~Nat,~%zero,~%l,ne, ~(x) => Word(x), we)
- | succ =>
- let bs = case b
- + m : Nat
- | be => w0(~pred(m),bits_to_word(pred(m), be))
- | b0 => w0(~pred(m),bits_to_word(pred(m),b.pred))
- | b1 => w1(~pred(m),bits_to_word(pred(m),b.pred))
- : Word(succ(pred(m)))
- get [ne1,ne2] = same(~Nat,~succ(n.pred),~%l,ne)
- let ln = sym(~Nat,~%succ(n.pred),~%l,ne1)
- let mn = trans(~Nat,~%m,~%l,~%succ(n.pred),me,ln)
- let mn = cong(~Nat,~Nat,~%m,~%succ(n.pred),~pred,mn)
- let P = (x) => Word(succ(x))
- let bs = rewrite(~Nat,~%pred(m),~%n.pred,mn,~P, bs)
- let P = (x) => Word(x)
- let bs = rewrite(~Nat,~%succ(n.pred),~%l,ne2,~P, bs)
- bs
- : Word(l)
-
-nat_to_word(l : Nat, n : Nat) : Word(l)
- bits_to_word(l, nat_to_bits(n))
-
-Word8 : Type; Word(8n)
-
-w_15 : Word(4n)
- w1(~3n,w1(~2n,w1(~1n,w1(~0n,we))))
-
-word.test : The(Number,15)
- let x = bits_to_word(5n,word_to_bits(4n, w_15))
- let x = bits_to_nat(word_to_bits(5n,x))
- the(~Number,nat_to_number(x))
-
-word.not(n : -Nat, x : Word(n)) : Word(n)
- case x
- + refl(~Nat, ~n) as e : Equal(Nat,x.len,n)
- | we => rewrite(~Nat, ~%zero,~%n, e,~(x) => Word(x),we)
- | w0 => let w = w1(~x.len,word.not(x.len,x.pred))
- rewrite(~Nat, ~%succ(x.len),~%n, e,~(x) => Word(x),w)
- | w1 => let w = w0(~x.len,word.not(x.len,x.pred))
- rewrite(~Nat, ~%succ(x.len),~%n, e,~(x) => Word(x),w)
- : Word(n)
-
-word.and(n : -Nat, x : Word(n), y : Word(n)) : Word(n)
- case x
- + y : Word(n)
- + refl(~Nat, ~n) as ex : Equal(Nat,x.len,n)
- | we => rewrite(~Nat,~%zero,~%n,ex,~(x) => Word(x),we)
- | w0 =>
- case y
- + ex : Equal(Nat,succ(x.len),n)
- + refl(~Nat, ~n) as ey : Equal(Nat,y.len,n)
- | we => rewrite(~Nat,~%zero,~%n,ey,~(x) => Word(x),we)
- | w0 =>
- get [x1, x2] = same(~Nat,~%succ(x.len),~%n,ex)
- let xy = trans2(~Nat,~%succ(y.len),~%n,~%succ(x.len),ey,x1)
- let xy = cong_pred(~%y.len, ~%x.len, xy)
- let P = (x) => Word(x)
- let yp = rewrite(~Nat,~%y.len,~%x.len,xy,~P,y.pred)
- let w = w0(~x.len,word.and(x.len,x.pred,yp))
- rewrite(~Nat,~%succ(x.len),~%n,x2,~P,w)
- | w1 =>
- get [x1, x2] = same(~Nat,~%succ(x.len),~%n,ex)
- let xy = trans2(~Nat,~%succ(y.len),~%n,~%succ(x.len),ey,x1)
- let xy = cong_pred(~%y.len, ~%x.len, xy)
- let P = (x) => Word(x)
- let yp = rewrite(~Nat,~%y.len,~%x.len,xy,~P,y.pred)
- let w = w0(~x.len,word.and(x.len,x.pred,yp))
- rewrite(~Nat,~%succ(x.len),~%n,x2,~P,w)
- : Word(n)
- | w1 =>
- case y
- + ex : Equal(Nat,succ(x.len),n)
- + refl(~Nat, ~n) as ey : Equal(Nat,y.len,n)
- | we => rewrite(~Nat,~%zero,~%n,ey,~(x) => Word(x),we)
- | w0 =>
- get [x1, x2] = same(~Nat,~%succ(x.len),~%n,ex)
- let xy = trans2(~Nat,~%succ(y.len),~%n,~%succ(x.len),ey,x1)
- let xy = cong_pred(~%y.len, ~%x.len, xy)
- let P = (x) => Word(x)
- let yp = rewrite(~Nat,~%y.len,~%x.len,xy,~P,y.pred)
- let w = w0(~x.len,word.and(x.len,x.pred,yp))
- rewrite(~Nat,~%succ(x.len),~%n,x2,~P,w)
- | w1 =>
- get [x1, x2] = same(~Nat,~%succ(x.len),~%n,ex)
- let xy = trans2(~Nat,~%succ(y.len),~%n,~%succ(x.len),ey,x1)
- let xy = cong_pred(~%y.len, ~%x.len, xy)
- let P = (x) => Word(x)
- let yp = rewrite(~Nat,~%y.len,~%x.len,xy,~P,y.pred)
- let w = w1(~x.len,word.and(x.len,x.pred,yp))
- rewrite(~Nat,~%succ(x.len),~%n,x2,~P,w)
- : Word(n)
- : Word(n)
-
-word.and2(n : Nat, x : Word(n), y : Word(n)) : Word(n)
- let x = word_to_bits(n,x)
- let y = word_to_bits(n,y)
- bits_to_word(n,bits.and(x,y))
-
-word.inc(n : -Nat, x : Word(n)) : [:Word(n), Bool]
- let P = (x) => Word(x)
- case x
- + refl(~Nat, ~n) as e : Equal(Nat,x.len,n)
- | we => [rewrite(~Nat,~%zero,~%n,e,~P,we), true]
- | w0 =>
- let w = w1(~x.len,x.pred)
- [rewrite(~Nat,~%succ(x.len),~%n,e,~P,w), false]
- | w1 =>
- get [w, b] = word.inc(x.len,x.pred)
- let w = w0(~x.len,w)
- [rewrite(~Nat,~%succ(x.len),~%n,e,~P,w), b]
- : [:Word(n), Bool]
-
-// n + 1 == l && m + 1 == l => n = m
-pred_trans(
- ~n : -Nat,
- ~m : -Nat,
- ~l : -Nat,
- nl : Equal(Nat, %succ(n), l),
- ml : Equal(Nat, %succ(m), l)
-) : Equal(Nat,n,m)
- cong_pred(~n,~m,trans2(~Nat,~%succ(n),~l,~%succ(m),nl,ml))
-
-word.adder(n : -Nat, c : Bool, x : Word(n), y : Word(n)) : [:Word(n), Bool]
- case x
- + y : Word(n)
- + refl(__) as ex : Equal(Nat,x.len,n)
- + c : Bool
- | we => [rewrite(___ ex,_ we), c]
- | w0 =>
- case y
- + c : Bool
- + ex : Equal(Nat,succ(x.len),n)
- + refl(__) as ey : Equal(Nat,y.len,n)
- | we => [rewrite(___ ey,_ we), c]
- | w0 =>
- get [x1, x2] = same(___ ex)
- let yp = rewrite(___ pred_trans(___ ey,x1),_ y.pred)
- get [w,b] = word.adder(x.len,false,x.pred,yp)
- let w = case c
- + w : Word(x.len)
- | true => w1(_ w)
- | false => w0(_ w)
- : Word(succ(x.len))
- [rewrite(___ x2,_ w), b]
- | w1 =>
- get [x1, x2] = same(___ ex)
- let yp = rewrite(___ pred_trans(___ ey,x1),_ y.pred)
- get [c1, c2] = copy_bool(c)
- get [w,b] = word.adder(x.len,c1,x.pred,yp)
- let w = case c2
- + w : Word(x.len)
- | true => w0(_ w)
- | false => w1(_ w)
- : Word(succ(x.len))
- [rewrite(___ x2,_ w), b]
- : [:Word(n), Bool]
- | w1 =>
- case y
- + c : Bool
- + ex : Equal(Nat,succ(x.len),n)
- + refl(__) as ey : Equal(Nat,y.len,n)
- | we => [rewrite(___ ey,_ we), c]
- | w0 =>
- get [x1, x2] = same(___ ex)
- let yp = rewrite(___ pred_trans(___ ey,x1),_ y.pred)
- get [c1, c2] = copy_bool(c)
- get [w,b] = word.adder(x.len,c1,x.pred,yp)
- let w = case c2
- + w : Word(x.len)
- | true => w0(_ w)
- | false => w1(_ w)
- : Word(succ(x.len))
- [rewrite(___ x2,_ w), b]
- | w1 =>
- get [x1, x2] = same(___ ex)
- let yp = rewrite(___ pred_trans(___ ey,x1),_ y.pred)
- get [w,b] = word.adder(x.len,true,x.pred,yp)
- let w = case c
- + w : Word(x.len)
- | true => w1(_ w)
- | false => w0(_ w)
- : Word(succ(x.len))
- [rewrite(___ x2,_ w), b]
- : [:Word(n), Bool]
- : [:Word(n), Bool]
-
-word.add(n : -Nat, x : Word(n), y : Word(n)) : Word(n)
- fst(word.adder(n, false, x, y))
-
-w_7 : Word(4n)
- w1(_ w1(_ w1(_ w0(_ we))))
-
-word.add_test : The([:Number, Bool],[14,false])
- get [x,b] = word.adder(4n, false, w_7, w_7)
- let x = bits_to_nat(word_to_bits(4n,x))
- the(~[:Number, Bool], [nat_to_number(x), b])
-
-word.add_test2 : The([:Number, Bool],[14,true])
- get [x,b] = word.adder(4n, false, w_15, w_15)
- let x = bits_to_nat(word_to_bits(4n,x))
- the(~[:Number, Bool], [nat_to_number(x), b])
-
-word.add_test3 : The([:Number, Bool],[0,true])
- let w8 = nat_to_word(4n, 8n)
- get [x,b] = word.adder(4n, false, w8, w8)
- let x = word_to_nat(4n,x)
- the(~[:Number, Bool], [nat_to_number(x), b])