add bft proof

book/Bool.not.kind2

@@ -1,4 +1,6 @@
 Bool.not
 : ∀(x: Bool) Bool
 = λx
-  (~x λx(Bool) Bool.false Bool.true)
+  (~x λx(Bool)
+    Bool.false
+    Bool.true)

book/Equal.apply.kind2

@@ -0,0 +1,11 @@
+// a == b -> (f a) == (f b)
+Equal.apply
+: ∀(A: *)
+  ∀(B: *)
+  ∀(f: ∀(x: A) B)
+  ∀(a: A)
+  ∀(b: A)
+  ∀(e: (Equal A a b))
+  (Equal B (f a) (f b))
+= λA λB λf λa λb λe
+  (e λx(Equal B (f a) (f x)) λP λx x)

book/Main.kind2

@@ -0,0 +1,3 @@
+Main
+: Nat
+= (Nat.half (Nat.double (Nat.succ (Nat.succ Nat.zero))))

book/Nat.double.kind2

@@ -0,0 +1,7 @@
+Nat.double
+: ∀(n: Nat)
+  Nat
+= λn
+  (~n λx(Nat)
+    λpred (Nat.succ (Nat.succ (Nat.double pred)))
+    Nat.zero)

book/Nat.half.kind2

@@ -0,0 +1,9 @@
+Nat.half
+: ∀(n: Nat)
+  Nat
+= λn
+  (~n λx(Nat)
+    λn (~n λx(Nat)
+      λn (Nat.succ (Nat.half n))
+      Nat.zero)
+    Nat.zero)

book/Nat.kind2

@@ -0,0 +1,7 @@
+Nat
+: *
+= $self
+  ∀(P: ∀(n: Nat) *)
+  ∀(s: ∀(n: Nat) (P (Nat.succ n)))
+  ∀(z: (P Nat.zero))
+  (P self)

book/Nat.lemma.bft.kind2

@@ -0,0 +1,7 @@
+Nat.lemma.bft
+: ∀(n: Nat)
+  (Equal Nat (Nat.half (Nat.double n)) n)
+= λn (~n λx(Equal Nat (Nat.half (Nat.double x)) x)
+  λn(Equal.apply Nat Nat Nat.succ (Nat.half (Nat.double n)) n
+    (Nat.lemma.bft n))
+  λP λa a)

book/Nat.succ.kind2

@@ -0,0 +1,5 @@
+Nat.succ
+: ∀(n: Nat) Nat
+= λn
+  ~λP λs λz
+  (s n)

book/Nat.zero.kind2

@@ -0,0 +1,5 @@
+Nat.zero
+: Nat
+= ~λP λs λz
+  z
+  

kind2.hvm1

@@ -108,8 +108,8 @@
 // Equality
 // --------
 
-(Equal a b dep) = (Compare a b dep)
-//(Equal a b dep) = (Debug ["Equal: " (Show a dep) NewLine "    == " (Show b dep)] (Compare a b dep))
+(Equal a b dep) = (If (Compare a b dep) 1 (Compare (Reduce 1 a) (Reduce 1 b) dep))
+//(Equal a b dep) = (Debug ["Equal: " (Show a dep) NewLine "    == " (Show b dep)] (If (Compare a b dep) 1 (Compare (Reduce 1 a) (Reduce 1 b) dep)))
 
 (Compare (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Equal a.inp b.inp dep) (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
 (Compare (Lam a.nam a.bod)       (Lam b.nam b.bod)       dep) = (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
@@ -127,17 +127,11 @@
 (Compare a                       (Ann b.val b.typ)       dep) = (Equal a b.val dep)
 (Compare (Hol a.nam a.ctx)       b                       dep) = (Debug ["Found: ?" a.nam " = " (Show b dep)] 1)
 (Compare a                       (Hol b.nam b.ctx)       dep) = (Debug ["Found: ?" b.nam " = " (Show a dep)] 1)
-(Compare (App a.fun a.arg)       b                       dep) = (Compare.app.l (Reduce 1 (App a.fun a.arg)) b dep)
-(Compare a                       (App b.fun b.arg)       dep) = (Compare.app.r a (Reduce 1 (App b.fun b.arg)) dep)
+//(Compare (App a.fun a.arg)       b                       dep) = (Compare.app.l (Reduce 1 (App a.fun a.arg)) b dep)
+//(Compare a                       (App b.fun b.arg)       dep) = (Compare.app.r a (Reduce 1 (App b.fun b.arg)) dep)
 //(Compare (Lam a.nam a.bod)       b                       dep) = (Compare (Lam a.nam a.bod) (Lam a.nam λx(App b x)) dep)
 //(Compare a                       (Lam b.nam b.bod)       dep) = (Compare (Lam b.nam λx(App a x)) (Lam b.nam b.bod) dep)
-(Compare a                       b                       dep) = (Debug ["OhNo0: " (Show a dep) " != " (Show b dep)] 0)
-
-(Compare.app.l (App a.fun a.arg) b dep) = (Debug ["OhNo1: " (Show (App a.fun a.arg) dep) " != " (Show b dep)] 0)
-(Compare.app.l a                 b dep) = (Equal a b dep)
-
-(Compare.app.r a (App b.fun b.arg) dep) = (Debug ["OhNo2: " (Show a dep) " != " (Show (App b.fun b.arg) dep)] 0)
-(Compare.app.r a b                 dep) = (Equal a b dep)
+(Compare a                       b                       dep) = 0
 
 // Logger
 // -------
@@ -188,15 +182,19 @@
   (Debug ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
 
 //(Check term type dep) = (Debug ["Check: " (Show term dep) " :: " (Show (Reduce 1 type) dep)] (Check.match term (Reduce 1 type) dep))
-(Check term type dep) = (Check.match term (Reduce 1 type) dep)
+(Check term type dep) = (Check.match term type dep)
 
-(Check.match (Lam term.nam term.bod) (All type.nam type.inp type.bod) dep) =
-  let ann  = (Ann (Var term.nam dep) type.inp)
-  let term = (term.bod ann)
-  let type = (type.bod ann)
-  (Check term type (+ dep 1))
-(Check.match (Ins term.val) (Slf type.nam type.bod) dep) =
-  (Check term.val (type.bod (Ins term.val)) dep)
+(Check.match (Lam term.nam term.bod) type dep) =
+  (IfAll (Reduce 1 type) λtype.nam λtype.inp λtype.bod
+    let ann  = (Ann (Var term.nam dep) type.inp)
+    let term = (term.bod ann)
+    let type = (type.bod ann)
+    (Check term type (+ dep 1))
+  (Infer (Lam term.nam term.bod) dep))
+(Check.match (Ins term.val) type dep) =
+  (IfSlf type λtype.nam λtype.bod
+    (Check term.val (type.bod (Ins term.val)) dep)
+    (Infer (Ins term.val) dep))
 (Check.match (Ref term.nam term.val) type dep) =
   (Check term.val type dep)
 (Check.match (Hol term.nam term.ctx) type dep) =
@@ -206,7 +204,7 @@
   (Bind (Infer val dep) λinfer
   (If (Equal term.type infer dep)
     (Pure 0)
-    (Debug ["Error: " (Show (Normal 0 term.type dep) dep) " != " (Show (Normal 0 infer dep) dep)] None)))
+    (Debug ["Error: " (Show (Normal 0 infer dep) dep) NewLine "    != " (Show (Normal 0 term.type dep) dep)] None)))
 
 // Syntax
 // ------
@@ -240,9 +238,11 @@
 // API
 // ---
 
+(Normalizer term) = (HVM.print (Show (Normal 1 term 0) 0) OK)
+
 (Checker (Ref nam val)) = (Checker val)
 (Checker (Ann val typ)) = (Checker.report (Check val typ 0))
-(Checker val)           = (HVM.print "Untyped." 1)
+(Checker val)           = (HVM.print "Untyped." OK)
 
-(Checker.report (Some x)) = (HVM.print "Check!" 1)
-(Checker.report None)     = (HVM.print "Error." 0)
+(Checker.report (Some x)) = (HVM.print "Check!" OK)
+(Checker.report None)     = (HVM.print "Error." ERR)

main.ts

@@ -1,8 +1,6 @@
 #!/usr/bin/env ts-node
 
-// NOTE FOR GPT: the file below has been refactored in order to add a "nam"
-// field to the All, Lam, Slf and Var constructors. not all functions were
-// updated. your task is to update these functions when asked.
+// TODO: move the parser to HVM
 
 // ICC: Parser, Stringifier and CLI
 // ================================