Jcb/rewrite

Bits.fm

@@ -1,6 +1,6 @@
 // Bits.fm
 // =======
-// 
+//
 // Defines a bitstream, or binary sequence.
 
 import Equal

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

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

old/Fin.fm → 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

Function.fm

@@ -1,6 +1,6 @@
 // Function.fm
 // ===========
-// 
+//
 // Wrapper and utilities for the built-in function type.
 
 import Equal

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

old/IBin.fm → 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)

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)

old/INat.fm → 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

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

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
 // -----
 

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