From f3451e442b5b70bd0f27ec194e97d4e7b2e79ecc Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Thu, 22 Feb 2024 17:01:05 -0300 Subject: [PATCH] WIP - breaking; will update after the map merge --- book/HVM.load.kind2 | 7 + book/HVM.log.kind2 | 8 + book/HVM.print.kind2 | 7 + book/HVM.print.many.kind2 | 10 + book/HVM.save.kind2 | 8 + book/Kind.API.file.kind2 | 5 + book/Kind.API.load.kind2 | 6 + book/Kind.API.load.one.kind2 | 6 + book/Kind.Book.get_refs.go.kind2 | 14 + book/Kind.Book.get_refs.kind2 | 5 + book/Kind.Book.parse.kind2 | 2 +- book/Kind.Book.to_hvm.go.kind2 | 12 +- book/Kind.Book.to_hvm.prelude.kind2 | 8 +- book/Kind.Term.get_refs.go.kind2 | 50 + book/Kind.Term.get_refs.kind2 | 6 + book/Kind.Term.kind2 | 2 +- book/Kind.Term.to_hvm.go.kind2 | 2 +- book/Kind.file.kind2 | 2 + book/List.Map.kind2 | 42 - book/Main.kind2 | 10 + book/QBool.kind2 | 9 +- book/QBool2.kind2 | 63 ++ book/String.Map.kind2 | 27 - book/U60.Map.kind2 | 27 - book/_compile.kind2 | 4 + book/test10.kind2 | 3 +- book/test11.kind2 | 3 + book/test7.kind2 | 19 +- bootstrap.hvm1 | 1448 +++++++++++++++++++++++++++ bootstrap.js | 38 + kind2.hvm1 | 31 +- kind2.ts | 30 + 32 files changed, 1776 insertions(+), 138 deletions(-) create mode 100644 book/HVM.load.kind2 create mode 100644 book/HVM.log.kind2 create mode 100644 book/HVM.print.kind2 create mode 100644 book/HVM.print.many.kind2 create mode 100644 book/HVM.save.kind2 create mode 100644 book/Kind.API.file.kind2 create mode 100644 book/Kind.API.load.kind2 create mode 100644 book/Kind.API.load.one.kind2 create mode 100644 book/Kind.Book.get_refs.go.kind2 create mode 100644 book/Kind.Book.get_refs.kind2 create mode 100644 book/Kind.Term.get_refs.go.kind2 create mode 100644 book/Kind.Term.get_refs.kind2 create mode 100644 book/Kind.file.kind2 delete mode 100644 book/List.Map.kind2 create mode 100644 book/QBool2.kind2 delete mode 100644 book/String.Map.kind2 delete mode 100644 book/U60.Map.kind2 create mode 100644 book/_compile.kind2 create mode 100644 book/test11.kind2 create mode 100644 bootstrap.hvm1 create mode 100644 bootstrap.js create mode 100644 kind2.ts diff --git a/book/HVM.load.kind2 b/book/HVM.load.kind2 new file mode 100644 index 00000000..438b1d63 --- /dev/null +++ b/book/HVM.load.kind2 @@ -0,0 +1,7 @@ +HVM.load +: ∀(A: *) + ∀(file: String) + ∀(cont: ∀(x: String) A) + A += λA λfile λcont + (cont String.nil) diff --git a/book/HVM.log.kind2 b/book/HVM.log.kind2 new file mode 100644 index 00000000..dbe9f1e8 --- /dev/null +++ b/book/HVM.log.kind2 @@ -0,0 +1,8 @@ +HVM.log +: ∀(A: *) + ∀(B: *) + ∀(msg: A) + ∀(ret: B) + B += λA λB λmsg λret + ret diff --git a/book/HVM.print.kind2 b/book/HVM.print.kind2 new file mode 100644 index 00000000..87ee2bed --- /dev/null +++ b/book/HVM.print.kind2 @@ -0,0 +1,7 @@ +HVM.print +: ∀(A: *) + ∀(msg: String) + ∀(ret: A) + A += λA λmsg λret + ret diff --git a/book/HVM.print.many.kind2 b/book/HVM.print.many.kind2 new file mode 100644 index 00000000..de94da10 --- /dev/null +++ b/book/HVM.print.many.kind2 @@ -0,0 +1,10 @@ +HVM.print.many +: ∀(A: *) + ∀(msgs: (List String)) + ∀(ret: A) + A += λA λmsgs λret + let P = λx(A) + let cons = λmsg λmsgs (HVM.print A msg (HVM.print.many A msgs ret)) + let nil = ret + (~msgs P cons nil) diff --git a/book/HVM.save.kind2 b/book/HVM.save.kind2 new file mode 100644 index 00000000..a69c0c3d --- /dev/null +++ b/book/HVM.save.kind2 @@ -0,0 +1,8 @@ +HVM.save +: ∀(A: *) + ∀(file: String) + ∀(data: String) + ∀(cont: A) + A += λA λfile λdata λcont + cont diff --git a/book/Kind.API.file.kind2 b/book/Kind.API.file.kind2 new file mode 100644 index 00000000..fd24bfd1 --- /dev/null +++ b/book/Kind.API.file.kind2 @@ -0,0 +1,5 @@ +Kind.API.file +: ∀(name: String) + String += λname + (String.concat name ".kind2") diff --git a/book/Kind.API.load.kind2 b/book/Kind.API.load.kind2 new file mode 100644 index 00000000..21979576 --- /dev/null +++ b/book/Kind.API.load.kind2 @@ -0,0 +1,6 @@ +// TODO +Kind.API.load +: ∀(name: String) + Kind.Book += λname + (Kind.API.load.one name) diff --git a/book/Kind.API.load.one.kind2 b/book/Kind.API.load.one.kind2 new file mode 100644 index 00000000..dafa7c91 --- /dev/null +++ b/book/Kind.API.load.one.kind2 @@ -0,0 +1,6 @@ +Kind.API.load.one +: ∀(name: String) + Kind.Book += λname + (HVM.load Kind.Book (Kind.API.file name) λdata + (Kind.Book.parse data)) diff --git a/book/Kind.Book.get_refs.go.kind2 b/book/Kind.Book.get_refs.go.kind2 new file mode 100644 index 00000000..5fb87437 --- /dev/null +++ b/book/Kind.Book.get_refs.go.kind2 @@ -0,0 +1,14 @@ +Kind.Book.get_refs.go +: ∀(book: Kind.Book) + (List.Concatenator String) += λbook + let P = λx (List.Concatenator String) + let cons = λhead λtail + let P = λx (List.Concatenator String) + let new = λhead.fst λhead.snd λnil + ((Kind.Term.get_refs.go head.snd) + ((Kind.Book.get_refs.go tail) + nil)) + (~head P new) + let nil = λnil nil + (~book P cons nil) diff --git a/book/Kind.Book.get_refs.kind2 b/book/Kind.Book.get_refs.kind2 new file mode 100644 index 00000000..984c4520 --- /dev/null +++ b/book/Kind.Book.get_refs.kind2 @@ -0,0 +1,5 @@ +Kind.Book.get_refs +: ∀(book: Kind.Book) + (List String) += λbook + (List.Concatenator.build String (Kind.Book.get_refs.go book)) diff --git a/book/Kind.Book.parse.kind2 b/book/Kind.Book.parse.kind2 index 65a99147..9a1671fc 100644 --- a/book/Kind.Book.parse.kind2 +++ b/book/Kind.Book.parse.kind2 @@ -5,4 +5,4 @@ Kind.Book.parse let P = λx(Kind.Book) let done = λcode λbook book let fail = λerror (List.nil (Pair String Kind.Term)) - (~(Kind.Book.parser code) P done fail) \ No newline at end of file + (~(Kind.Book.parser code) P done fail) diff --git a/book/Kind.Book.to_hvm.go.kind2 b/book/Kind.Book.to_hvm.go.kind2 index e2b00e0c..282b1b27 100644 --- a/book/Kind.Book.to_hvm.go.kind2 +++ b/book/Kind.Book.to_hvm.go.kind2 @@ -6,13 +6,13 @@ Kind.Book.to_hvm.go let cons = λhead λtail let P = λx String.Concatenator let new = λhead.fst λhead.snd λnil - ((Kind.Text.show.go "F." + ((Kind.Text.show.go "Book.") ((Kind.Text.show.go head.fst) - ((Kind.Text.show.go " = " - ((Kind.Term.to_hvm.go head.snd Nat.zero Bool.true Nat.zero - ((Kind.Text.show.go String.newline - ((Kind.Book.to_hvm.go tail - nil))))))))))) + ((Kind.Text.show.go " = ") + ((Kind.Term.to_hvm.go head.snd Nat.zero Bool.true Nat.zero) + ((Kind.Text.show.go String.newline) + ((Kind.Book.to_hvm.go tail) + nil)))))) (~head P new) let nil = λnil nil (~book P cons nil) diff --git a/book/Kind.Book.to_hvm.prelude.kind2 b/book/Kind.Book.to_hvm.prelude.kind2 index e620254d..45aacf45 100644 --- a/book/Kind.Book.to_hvm.prelude.kind2 +++ b/book/Kind.Book.to_hvm.prelude.kind2 @@ -1,9 +1,11 @@ -Kind.Book.to_hvm.prelude -: String -= ` +Kind.Book.to_hvm.prelude : String = ` (U60.match 0 z s) = z (U60.match n z s) = (s (- n 1)) (Str String.nil) = λP λcons λnil nil (Str (String.cons x xs)) = λP λcons λnil (cons x (Str xs)) + +(Str.view str) = (str 0 λhλt(String.cons h (Str.view t)) String.nil) +(Strs.view strs) = (List.view λx(Str.view x) strs) +(List.view elem list) = (list 0 λhλt(List.cons (elem h) (List.view elem t)) List.nil) ` diff --git a/book/Kind.Term.get_refs.go.kind2 b/book/Kind.Term.get_refs.go.kind2 new file mode 100644 index 00000000..f5e7562b --- /dev/null +++ b/book/Kind.Term.get_refs.go.kind2 @@ -0,0 +1,50 @@ +Kind.Term.get_refs.go +: ∀(term: Kind.Term) + (List.Concatenator String) += λterm + let P = λx(List.Concatenator String) + let all = λnam λinp λbod λnil + ((Kind.Term.get_refs.go inp) + ((Kind.Term.get_refs.go (bod Kind.set)) + nil)) + let lam = λnam λbod λnil + ((Kind.Term.get_refs.go (bod Kind.set)) + nil) + let app = λfun λarg λnil + ((Kind.Term.get_refs.go fun) + ((Kind.Term.get_refs.go arg) + nil)) + let ann = λval λtyp λnil + ((Kind.Term.get_refs.go val) + ((Kind.Term.get_refs.go typ) + nil)) + let slf = λnam λbod λnil + ((Kind.Term.get_refs.go (bod Kind.set)) + nil) + let ins = λval λnil + ((Kind.Term.get_refs.go val) + nil) + let ref = λnam λval λnil + ((List.cons String nam) + nil) + let def = λnam λval λbod λnil + ((Kind.Term.get_refs.go val) + ((Kind.Term.get_refs.go (bod Kind.set)) + nil)) + let set = λnil nil + let u60 = λnil nil + let num = λval λnil nil + let op2 = λopr λfst λsnd λnil + ((Kind.Term.get_refs.go fst) + ((Kind.Term.get_refs.go snd) + nil)) + let mat = λnam λx λz λs λp λnil + ((Kind.Term.get_refs.go x) + ((Kind.Term.get_refs.go z) + ((Kind.Term.get_refs.go (s Kind.set)) + ((Kind.Term.get_refs.go (p Kind.set)) + nil)))) + let txt = λtext λnil nil + let hol = λnam λctx λnil nil + let var = λnam λidx λnil nil + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) diff --git a/book/Kind.Term.get_refs.kind2 b/book/Kind.Term.get_refs.kind2 new file mode 100644 index 00000000..8cbca675 --- /dev/null +++ b/book/Kind.Term.get_refs.kind2 @@ -0,0 +1,6 @@ +// Returns a list with all the references of given term. +Kind.Term.get_refs +: ∀(term: Kind.Term) + (List String) += λterm + (List.Concatenator.build String (Kind.Term.get_refs.go term)) diff --git a/book/Kind.Term.kind2 b/book/Kind.Term.kind2 index b65a7c3b..8885a42a 100644 --- a/book/Kind.Term.kind2 +++ b/book/Kind.Term.kind2 @@ -18,4 +18,4 @@ Kind.Term ∀(txt: ∀(lit: Kind.Text) (P (Kind.txt lit))) ∀(hol: ∀(nam: String) ∀(ctx: (List Kind.Term)) (P (Kind.hol nam ctx))) ∀(var: ∀(nam: String) ∀(idx: Nat) (P (Kind.var nam idx))) - (P self) \ No newline at end of file + (P self) diff --git a/book/Kind.Term.to_hvm.go.kind2 b/book/Kind.Term.to_hvm.go.kind2 index a59464e2..80d4526b 100644 --- a/book/Kind.Term.to_hvm.go.kind2 +++ b/book/Kind.Term.to_hvm.go.kind2 @@ -40,7 +40,7 @@ Kind.Term.to_hvm.go nil)) let ref = λnam λval λnil ((Kind.Term.to_hvm.nl inc tab) - ((Kind.Text.show.go "(F.") + ((Kind.Text.show.go "(Book.") ((Kind.Text.show.go nam) ((Kind.Text.show.go ")") nil)))) diff --git a/book/Kind.file.kind2 b/book/Kind.file.kind2 new file mode 100644 index 00000000..d3907046 --- /dev/null +++ b/book/Kind.file.kind2 @@ -0,0 +1,2 @@ +//Kind.file +//: ∀(name: diff --git a/book/List.Map.kind2 b/book/List.Map.kind2 deleted file mode 100644 index cf03948c..00000000 --- a/book/List.Map.kind2 +++ /dev/null @@ -1,42 +0,0 @@ -List.Map -: ∀(K: *) - ∀(V: *) - * -= λK λV - (List (Pair K V)) - -List.Map.get -: ∀(K: *) - ∀(V: *) - ∀(eql: ∀(a: K) ∀(b: K) Bool) - ∀(key: K) - ∀(map: (List.Map K V)) - (Maybe V) -= λK λV λeql λkey λmap - let P = λx(Maybe V) - let cons = λhead λtail - let P = λx(Maybe V) - let new = λhead.fst λhead.snd - let P = λx(Maybe V) - let true = (Maybe.some V head.snd) - let false = (List.Map.get K V eql key tail) - (~(eql head.fst key) P true false) - (~head P new) - let nil = (Maybe.none V) - (~map P cons nil) - -List.Map.set -: ∀(K: *) - ∀(V: *) - ∀(key: K) - ∀(val: V) - ∀(map: (List.Map K V)) - (List.Map K V) -= λK λV λkey λval λmap - (List.cons (Pair K V) (Pair.new K V key val) map) - -List.Map.new -: ∀(K: *) - ∀(V: *) - (List.Map K V) -= λK λV (List.nil (Pair K V)) diff --git a/book/Main.kind2 b/book/Main.kind2 index 81a8274f..d0b3dcbe 100644 --- a/book/Main.kind2 +++ b/book/Main.kind2 @@ -1,3 +1,13 @@ +Main +: Kind.Book += + let book = (Kind.API.load "Bool.and") + book + //let code = (Kind.Book.to_hvm book) + //let refs = (Kind.Book.get_refs book) + //(HVM.print Unit code + //Unit.one) + //BOOK //: String //= "id = λx x diff --git a/book/QBool.kind2 b/book/QBool.kind2 index d5f6f224..bbe0d8aa 100644 --- a/book/QBool.kind2 +++ b/book/QBool.kind2 @@ -1,4 +1,5 @@ // Ideal: +// // QBool.true : QBool = ~λP (#0, λx x) // QBool.false : QBool = ~λP (#1, λx x) // @@ -9,7 +10,7 @@ // ∀(x: match t { // 0: (P QBool.true) // 1: (P QBool.false) -// +: Empty +// +: ∀(x: Empty) * // }) // (P self) // @@ -55,16 +56,16 @@ QBool.match = λa λP λt λf (~(~a P) λx(P a) λtag #match tag = tag { #0: λx (x t) - #+: λx ((#match tag-1 = tag-1 { + #+: λx ((#match tag_1 = tag-1 { #0: λx (x f) #+: λx (x λe (Empty.absurd e *)) - }: ∀(x: ∀(x: #match tag-1 = tag-1 { + }: ∀(x: ∀(x: #match tag_1 = tag_1 { #0: (P QBool.false) #+: ∀(x: Empty) * }: *) (P a)) (P a)) x) }: ∀(x: (∀(x: #match tag = tag { #0: (P QBool.true) - #+: #match tag-1 = tag-1 { + #+: #match tag_1 = tag-1 { #0: (P QBool.false) #+: ∀(x: Empty) * }: * diff --git a/book/QBool2.kind2 b/book/QBool2.kind2 new file mode 100644 index 00000000..0fd4cb79 --- /dev/null +++ b/book/QBool2.kind2 @@ -0,0 +1,63 @@ +// Ideal: +// +// QBool2.true : QBool2 = ~λP λnew (new #0) +// QBool2.false : QBool2 = ~λP λnew (new #1) +// QBool2.bad : QBool2 = ~λP λnew (new #2 ?impossible) +// +// QBool2 : * = +// $self +// ∀(P: ∀(x: QBool2) *) +// ∀(new: ∀(tag: #U60) #match tag = tag { +// #0: (P QBool2.true) +// #1: (P QBool2.false) +// #+: ∀(e: Empty) * +// }: *) +// (P self) +// +// QBool2.match +// : ∀(a: QBool2) +// ∀(P: ∀(x: QBool2) *) +// ∀(t: (P QBool2.true)) +// ∀(f: (P QBool2.false)) +// (P a) +// = λa λP λt λf +// (~a P λtag #match tag = tag { +// #0: t +// #1: f +// #+: λe (~e λx(*)) +// }) + +QBool2.true : QBool2 = ~λP λnew (new #0) +QBool2.false : QBool2 = ~λP λnew (new #1) +QBool2.bad : QBool2 = ~λP λnew (new #2 ?impossible) + +QBool2 : * = + $self + ∀(P: ∀(x: QBool2) *) + ∀(new: ∀(tag: #U60) #match tag = tag { + #0: (P QBool2.true) + #+: #match tag_1 = tag-1 { + #0: (P QBool2.false) + #+: ∀(e: Empty) * + }: * + }: *) + (P self) + +QBool2.match +: ∀(a: QBool2) + ∀(P: ∀(x: QBool2) *) + ∀(t: (P QBool2.true)) + ∀(f: (P QBool2.false)) + (P a) += λa λP λt λf + (~a P λtag #match tag = tag { + #0: t + #+: #match tag_1 = tag-1 { + #0: f + #+: λe (~e λx(*)) + }: #match tag_1 = tag_1 { #0: (P QBool2.false) #+: ∀(e: Empty) * }: * + }: #match tag = tag { #0: (P QBool2.true) #+: #match tag_1 = tag-1 { #0: (P QBool2.false) #+: ∀(e: Empty) * }: * }: *) + + + + diff --git a/book/String.Map.kind2 b/book/String.Map.kind2 deleted file mode 100644 index b465499e..00000000 --- a/book/String.Map.kind2 +++ /dev/null @@ -1,27 +0,0 @@ -// Temporarily just a list of key/val - -String.Map -: ∀(A: *) * -= (List.Map String) - -String.Map.get -: ∀(A: *) - ∀(key: String) - ∀(map: (String.Map A)) - (Maybe A) -= λA λkey λmap - (List.Map.get String A String.equal key map) - -String.Map.set -: ∀(A: *) - ∀(key: String) - ∀(val: A) - ∀(map: (String.Map A)) - (String.Map A) -= λA λkey λval λmap - (List.Map.set String A key val map) - -String.Map.new -: ∀(V: *) - (String.Map V) -= λV (List.Map.new String V) diff --git a/book/U60.Map.kind2 b/book/U60.Map.kind2 deleted file mode 100644 index ee14a2a3..00000000 --- a/book/U60.Map.kind2 +++ /dev/null @@ -1,27 +0,0 @@ -// Temporarily just a list of key/val - -U60.Map -: ∀(A: *) * -= (List.Map #U60) - -U60.Map.get -: ∀(A: *) - ∀(key: #U60) - ∀(map: (U60.Map A)) - (Maybe A) -= λA λkey λmap - (List.Map.get #U60 A U60.equal key map) - -U60.Map.set -: ∀(A: *) - ∀(key: #U60) - ∀(val: A) - ∀(map: (U60.Map A)) - (U60.Map A) -= λA λkey λval λmap - (List.Map.set #U60 A key val map) - -U60.Map.new -: ∀(V: *) - (U60.Map V) -= λV (List.Map.new #U60 V) diff --git a/book/_compile.kind2 b/book/_compile.kind2 new file mode 100644 index 00000000..32e49e13 --- /dev/null +++ b/book/_compile.kind2 @@ -0,0 +1,4 @@ +_compile : String = (Kind.Book.to_hvm (Kind.Book.parse `test9 +: String += (String.unpar '(' ')' "((foo))") +`)) \ No newline at end of file diff --git a/book/test10.kind2 b/book/test10.kind2 index e3965684..e2c56009 100644 --- a/book/test10.kind2 +++ b/book/test10.kind2 @@ -6,9 +6,8 @@ _exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m _C2 = _Nat _c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z))))) -// Checks if `(work 2^4)` is propositionally equal to `true` +// Checks if (work 2^4) is propositionally equal to true test10 : String = let term = (Kind.app (Kind.app _exp _c2) _c2) (Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero) - diff --git a/book/test11.kind2 b/book/test11.kind2 new file mode 100644 index 00000000..7c227387 --- /dev/null +++ b/book/test11.kind2 @@ -0,0 +1,3 @@ +test11 +: String += #0 diff --git a/book/test7.kind2 b/book/test7.kind2 index 25be0cb0..9c5df7d6 100644 --- a/book/test7.kind2 +++ b/book/test7.kind2 @@ -1,20 +1,11 @@ test7.book : String = ` -// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P)) -_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat))) -_exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m (Kind.all "x" P λx(P))) (Kind.app n P))))) - -// C2 : Nat = λs λz (s (s z)) -_C2 = _Nat -_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z))))) - -// Checks if (work 2^4) is propositionally equal to true -test10 -: String -= let term = (Kind.app (Kind.app _exp _c2) _c2) - (Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero) - +Kind.API.get_refs +: ∀(code: String) + (List String) += λcode + (Kind.Term.get_refs (Kind.Term.parse code)) ` test7 diff --git a/bootstrap.hvm1 b/bootstrap.hvm1 new file mode 100644 index 00000000..f57e3ea4 --- /dev/null +++ b/bootstrap.hvm1 @@ -0,0 +1,1448 @@ +(U60.match 0 z s) = z +(U60.match n z s) = (s (- n 1)) + +(Str String.nil) = λP λcons λnil nil +(Str (String.cons x xs)) = λP λcons λnil (cons x (Str xs)) + +(Str.view str) = (str 0 λhλt(String.cons h (Str.view t)) String.nil) +(Strs.view strs) = (List.view λx(Str.view x) strs) +(List.view elem list) = (list 0 λhλt(List.cons (elem h) (List.view elem t)) List.nil) + +Book.A.one = λ_P λ_new (_new 0) +Book.A.bad = λ_P λ_new ((_new 1) 0) +Book.A.sel = λ_P λ_k (U60.match _k (_P (Book.A.one)) λ_tag_1(0)) +Book.A = 0 +Book.A.match = λ_a λ_P λ_t ((_a _P) λ_tag (U60.match _tag _t λ_tag_1(λ_x (_x λ_x 0)))) + +Book.Bool.and = λ_a + let _P = λ_a 0 + let _true = λ_b _b + let _false = λ_b (Book.Bool.false) + (((_a _P) _true) _false) + +Book.Bool.false = λ_P λ_t λ_f _f + +Book.Bool.if = λ_b λ_P λ_t λ_f (((_b λ_x _P) _t) _f) + +Book.Bool = 0 + +Book.Bool.lemma.notnot = λ_b (((_b λ_x ((((Book.Equal) (Book.Bool)) ((Book.Bool.not) ((Book.Bool.not) _x))) _x)) (((Book.Equal.refl) (Book.Bool)) (Book.Bool.true))) (((Book.Equal.refl) (Book.Bool)) (Book.Bool.false))) + +Book.Bool.match = λ_b λ_P λ_t λ_f (((_b _P) _t) _f) + +Book.Bool.not = λ_x + let _P = λ_x (Book.Bool) + let _true = (Book.Bool.false) + let _false = (Book.Bool.true) + (((_x _P) _true) _false) + +Book.Bool.or = λ_a + let _P = λ_a 0 + let _true = λ_b (Book.Bool.true) + let _false = λ_b _b + (((_a _P) _true) _false) + +Book.Bool.true = λ_P λ_t λ_f _t + +Book.Char.equal = (Book.U60.equal) + +Book.Char.escapes = ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 98) 8)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 102) 12)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 110) 10)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 114) 13)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 116) 9)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 118) 11)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 92) 92)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 34) 34)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 48) 0)) ((((Book.List.cons) (((Book.Pair) (Book.Char)) (Book.Char))) (((((Book.Pair.new) (Book.Char)) (Book.Char)) 39) 39)) ((Book.List.nil) (((Book.Pair) (Book.Char)) (Book.Char))))))))))))) + +Book.Char.is_between = λ_min λ_max λ_chr (((Book.Bool.and) ((Book.U60.to_bool) (>= _chr _min))) ((Book.U60.to_bool) (<= _chr _max))) + +Book.Char.is_blank = λ_a (((Book.Bool.or) (((Book.Char.equal) _a) 10)) (((Book.Char.equal) _a) 32)) + +Book.Char.is_decimal = λ_a ((((Book.Char.is_between) 48) 57) _a) + +Book.Char.is_name = λ_a (((Book.Bool.or) ((((Book.Char.is_between) 97) 122) _a)) (((Book.Bool.or) ((((Book.Char.is_between) 65) 90) _a)) (((Book.Bool.or) ((((Book.Char.is_between) 48) 57) _a)) (((Book.Bool.or) (((Book.Char.equal) 95) _a)) (((Book.Bool.or) (((Book.Char.equal) 46) _a)) (((Book.Bool.or) (((Book.Char.equal) 45) _a)) (Book.Bool.false))))))) + +Book.Char.is_newline = λ_a (((Book.Char.equal) _a) 10) + +Book.Char.is_oper = λ_a (((Book.Bool.or) (((Book.Char.equal) 43) _a)) (((Book.Bool.or) (((Book.Char.equal) 45) _a)) (((Book.Bool.or) (((Book.Char.equal) 42) _a)) (((Book.Bool.or) (((Book.Char.equal) 47) _a)) (((Book.Bool.or) (((Book.Char.equal) 37) _a)) (((Book.Bool.or) (((Book.Char.equal) 60) _a)) (((Book.Bool.or) (((Book.Char.equal) 62) _a)) (((Book.Bool.or) (((Book.Char.equal) 61) _a)) (((Book.Bool.or) (((Book.Char.equal) 38) _a)) (((Book.Bool.or) (((Book.Char.equal) 124) _a)) (((Book.Bool.or) (((Book.Char.equal) 94) _a)) (((Book.Bool.or) (((Book.Char.equal) 33) _a)) (((Book.Bool.or) (((Book.Char.equal) 126) _a)) (Book.Bool.false)))))))))))))) + +Book.Char.is_slash = λ_a (((Book.Char.equal) _a) 47) + +Book.Char = 0 + +Book.Char.slash = 92 + +Book.Empty.absurd = λ_e λ_P (_e λ_x _P) + +Book.Empty = 0 + +Book.Equal.apply = λ_A λ_B λ_f λ_a λ_b λ_e ((_e λ_x ((((Book.Equal) _B) (_f _a)) (_f _x))) λ_P λ_x _x) + +Book.Equal = λ_A λ_a λ_b 0 + +Book.Equal.refl = λ_A λ_a λ_P λ_p _p + +Book.Kind.Binder = (((Book.Pair) (Book.String)) (Book.Kind.Term)) + +Book.Kind.Binder.new = λ_nam λ_typ (((((Book.Pair.new) (Book.String)) (Book.Kind.Term)) _nam) _typ) + +Book.Kind.Book.String.cons = (((Book.Kind.hol) (Str "TODO")) ((Book.List.nil) (Book.Kind.Term))) + +Book.Kind.Book.String = (((Book.Kind.hol) (Str "TODO")) ((Book.List.nil) (Book.Kind.Term))) + +Book.Kind.Book.String.nil = (((Book.Kind.hol) (Str "TODO")) ((Book.List.nil) (Book.Kind.Term))) + +Book.Kind.Book.get_refs.go = λ_book + let _P = λ_x ((Book.List.Concatenator) (Book.String)) + let _cons = λ_head λ_tail + let _P = λ_x ((Book.List.Concatenator) (Book.String)) + let _new = λ_head.fst λ_head.snd λ_nil (((Book.Kind.Term.get_refs.go) _head.snd) (((Book.Kind.Book.get_refs.go) _tail) _nil)) + ((_head _P) _new) + let _nil = λ_nil _nil + (((_book _P) _cons) _nil) + +Book.Kind.Book.get_refs = λ_book (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Book.get_refs.go) _book)) + +Book.Kind.Book = ((Book.String.Map) (Book.Kind.Term)) + +Book.Kind.Book.parse = λ_code + let _P = λ_x (Book.Kind.Book) + let _done = λ_code λ_book _book + let _fail = λ_error ((Book.List.nil) (((Book.Pair) (Book.String)) (Book.Kind.Term))) + (((((Book.Kind.Book.parser) _code) _P) _done) _fail) + +Book.Kind.Book.parser = (((((Book.Parser.bind) (Book.Bool)) (Book.Kind.Book)) (Book.Parser.is_eof)) λ_is_eof + let _P = λ_x ((Book.Parser) (Book.Kind.Book)) + let _true = (((Book.Parser.pure) (Book.Kind.Book)) ((Book.String.Map.new) (Book.Kind.Term))) + let _false = (((((Book.Parser.bind) (Book.String)) (Book.Kind.Book)) (Book.Parser.name)) λ_nam (((((Book.Parser.bind) (Book.Bool)) (Book.Kind.Book)) (((Book.Parser.skip) (Book.Bool)) ((Book.Parser.test) (Str ":")))) λ_ann + let _P = λ_x ((Book.Parser) (Book.Kind.Book)) + let _true = (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Book)) ((Book.Parser.text) (Str ":"))) λ__ (((((Book.Parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Book)) (Book.Kind.Term.parser)) λ_typ (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Book)) ((Book.Parser.text) (Str "="))) λ__ (((((Book.Parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Book)) (Book.Kind.Term.parser)) λ_val (((((Book.Parser.bind) (Book.Kind.Book)) (Book.Kind.Book)) (Book.Kind.Book.parser)) λ_book (((Book.Parser.pure) (Book.Kind.Book)) (((((Book.String.Map.set) (Book.Kind.Term)) _nam) (((Book.Kind.ann) (_val ((Book.List.nil) (Book.Kind.Binder)))) (_typ ((Book.List.nil) (Book.Kind.Binder))))) _book))))))) + let _false = (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Book)) ((Book.Parser.text) (Str "="))) λ__ (((((Book.Parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Book)) (Book.Kind.Term.parser)) λ_val (((((Book.Parser.bind) (Book.Kind.Book)) (Book.Kind.Book)) (Book.Kind.Book.parser)) λ_book (((Book.Parser.pure) (Book.Kind.Book)) (((((Book.String.Map.set) (Book.Kind.Term)) _nam) (_val ((Book.List.nil) (Book.Kind.Binder)))) _book))))) + (((_ann _P) _true) _false))) + (((_is_eof _P) _true) _false)) + +Book.Kind.Book.show.go = λ_book + let _P = λ_x (Book.String.Concatenator) + let _cons = λ_head λ_tail + let _P = λ_x (Book.String.Concatenator) + let _new = λ_head.fst λ_head.snd λ_nil (((Book.Kind.Text.show.go) _head.fst) (((Book.Kind.Text.show.go) (Str " = ")) ((((Book.Kind.Term.show.go) _head.snd) (Book.Nat.zero)) (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Book.show.go) _tail) _nil))))) + ((_head _P) _new) + let _nil = λ_nil _nil + (((_book _P) _cons) _nil) + +Book.Kind.Book.show = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.show.go) _book)) + +Book.Kind.Book.to_hvm.go = λ_book + let _P = λ_x (Book.String.Concatenator) + let _cons = λ_head λ_tail + let _P = λ_x (Book.String.Concatenator) + let _new = λ_head.fst λ_head.snd λ_nil (((Book.Kind.Text.show.go) (Str "Book.")) (((Book.Kind.Text.show.go) _head.fst) (((Book.Kind.Text.show.go) (Str " = ")) ((((((Book.Kind.Term.to_hvm.go) _head.snd) (Book.Nat.zero)) (Book.Bool.true)) (Book.Nat.zero)) (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Book.to_hvm.go) _tail) _nil)))))) + ((_head _P) _new) + let _nil = λ_nil _nil + (((_book _P) _cons) _nil) + +Book.Kind.Book.to_hvm = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.to_hvm.go) _book)) + +Book.Kind.Oper.add = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _add + +Book.Kind.Oper.and = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _and + +Book.Kind.Oper.div = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _div + +Book.Kind.Oper.eq = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _eq + +Book.Kind.Oper.gt = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _gt + +Book.Kind.Oper.gte = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _gte + +Book.Kind.Oper = 0 + +Book.Kind.Oper.lsh = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _lsh + +Book.Kind.Oper.lt = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _lt + +Book.Kind.Oper.lte = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _lte + +Book.Kind.Oper.mod = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _mod + +Book.Kind.Oper.mul = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _mul + +Book.Kind.Oper.ne = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _ne + +Book.Kind.Oper.or = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _or + +Book.Kind.Oper.parser = + let _TRY = ((Book.List.cons) ((Book.Parser.Guard) (Book.Kind.Oper))) + let _END = ((Book.List.nil) ((Book.Parser.Guard) (Book.Kind.Oper))) + let _OP2 = λ_sym λ_oper ((((Book.Parser.Guard.text) (Book.Kind.Oper)) _sym) (((((Book.Parser.bind) (Book.Unit)) (Book.Kind.Oper)) ((Book.Parser.text) _sym)) λ_x (((Book.Parser.pure) (Book.Kind.Oper)) _oper))) + (((Book.Parser.variant) (Book.Kind.Oper)) ((_TRY ((_OP2 (Str "+")) (Book.Kind.Oper.add))) ((_TRY ((_OP2 (Str "*")) (Book.Kind.Oper.mul))) ((_TRY ((_OP2 (Str "-")) (Book.Kind.Oper.sub))) ((_TRY ((_OP2 (Str "/")) (Book.Kind.Oper.div))) ((_TRY ((_OP2 (Str "%")) (Book.Kind.Oper.mod))) ((_TRY ((_OP2 (Str "==")) (Book.Kind.Oper.eq))) ((_TRY ((_OP2 (Str "!=")) (Book.Kind.Oper.ne))) ((_TRY ((_OP2 (Str "<=")) (Book.Kind.Oper.lte))) ((_TRY ((_OP2 (Str ">=")) (Book.Kind.Oper.gte))) ((_TRY ((_OP2 (Str "<<")) (Book.Kind.Oper.lsh))) ((_TRY ((_OP2 (Str ">>")) (Book.Kind.Oper.rsh))) ((_TRY ((_OP2 (Str "<")) (Book.Kind.Oper.lt))) ((_TRY ((_OP2 (Str ">")) (Book.Kind.Oper.gt))) ((_TRY ((_OP2 (Str "&")) (Book.Kind.Oper.and))) ((_TRY ((_OP2 (Str "|")) (Book.Kind.Oper.or))) ((_TRY ((_OP2 (Str "^")) (Book.Kind.Oper.xor))) _END))))))))))))))))) + +Book.Kind.Oper.rsh = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _rsh + +Book.Kind.Oper.show.go = λ_oper + let _P = λ_X (Book.String.Concatenator) + let _add = ((Book.Kind.Text.show.go) (Str "+")) + let _mul = ((Book.Kind.Text.show.go) (Str "*")) + let _sub = ((Book.Kind.Text.show.go) (Str "-")) + let _div = ((Book.Kind.Text.show.go) (Str "/")) + let _mod = ((Book.Kind.Text.show.go) (Str "%")) + let _eq = ((Book.Kind.Text.show.go) (Str "==")) + let _ne = ((Book.Kind.Text.show.go) (Str "!=")) + let _lt = ((Book.Kind.Text.show.go) (Str "<")) + let _gt = ((Book.Kind.Text.show.go) (Str ">")) + let _lte = ((Book.Kind.Text.show.go) (Str "<=")) + let _gte = ((Book.Kind.Text.show.go) (Str ">=")) + let _and = ((Book.Kind.Text.show.go) (Str "&")) + let _or = ((Book.Kind.Text.show.go) (Str "|")) + let _xor = ((Book.Kind.Text.show.go) (Str "^")) + let _lsh = ((Book.Kind.Text.show.go) (Str "<<")) + let _rsh = ((Book.Kind.Text.show.go) (Str ">>")) + (((((((((((((((((_oper _P) _add) _mul) _sub) _div) _mod) _eq) _ne) _lt) _gt) _lte) _gte) _and) _or) _xor) _lsh) _rsh) + +Book.Kind.Oper.show = λ_oper ((Book.String.Concatenator.build) ((Book.Kind.Oper.show.go) _oper)) + +Book.Kind.Oper.sub = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _sub + +Book.Kind.Oper.xor = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _xor + +Book.Kind.PreTerm = 0 + +Book.Kind.Scope.cons = ((Book.List.cons) (Book.Kind.Binder)) + +Book.Kind.Scope.extend = λ_nam λ_typ λ_scp (((Book.Kind.Scope.cons) (((Book.Kind.Binder.new) _nam) _typ)) _scp) + +Book.Kind.Scope.find = λ_name λ_scope + let _cond = λ_bnd ((_bnd λ_x (Book.Bool)) λ_n λ_t (((Book.String.equal) _name) _n)) + let _found = ((((Book.List.find) (Book.Kind.Binder)) _cond) _scope) + let _P = λ_x (Book.Kind.Term) + let _some = λ_bnd ((_bnd λ_x (Book.Kind.Term)) λ_n λ_t _t) + let _none = (((Book.Kind.ref) _name) (Book.Kind.set)) + (((_found _P) _some) _none) + +Book.Kind.Scope = ((Book.List) (Book.Kind.Binder)) + +Book.Kind.Scope.nil = ((Book.List.nil) (Book.Kind.Binder)) + +Book.Kind.Term.get_refs.go = λ_term + let _P = λ_x ((Book.List.Concatenator) (Book.String)) + let _all = λ_nam λ_inp λ_bod λ_nil (((Book.Kind.Term.get_refs.go) _inp) (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil)) + let _lam = λ_nam λ_bod λ_nil (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil) + let _app = λ_fun λ_arg λ_nil (((Book.Kind.Term.get_refs.go) _fun) (((Book.Kind.Term.get_refs.go) _arg) _nil)) + let _ann = λ_val λ_typ λ_nil (((Book.Kind.Term.get_refs.go) _val) (((Book.Kind.Term.get_refs.go) _typ) _nil)) + let _slf = λ_nam λ_bod λ_nil (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil) + let _ins = λ_val λ_nil (((Book.Kind.Term.get_refs.go) _val) _nil) + let _ref = λ_nam λ_val λ_nil ((((Book.List.cons) (Book.String)) _nam) _nil) + let _def = λ_nam λ_val λ_bod λ_nil (((Book.Kind.Term.get_refs.go) _val) (((Book.Kind.Term.get_refs.go) (_bod (Book.Kind.set))) _nil)) + let _set = λ_nil _nil + let _u60 = λ_nil _nil + let _num = λ_val λ_nil _nil + let _op2 = λ_opr λ_fst λ_snd λ_nil (((Book.Kind.Term.get_refs.go) _fst) (((Book.Kind.Term.get_refs.go) _snd) _nil)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_nil (((Book.Kind.Term.get_refs.go) _x) (((Book.Kind.Term.get_refs.go) _z) (((Book.Kind.Term.get_refs.go) (_s (Book.Kind.set))) (((Book.Kind.Term.get_refs.go) (_p (Book.Kind.set))) _nil)))) + let _txt = λ_text λ_nil _nil + let _hol = λ_nam λ_ctx λ_nil _nil + let _var = λ_nam λ_idx λ_nil _nil + (((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) + +Book.Kind.Term.get_refs = λ_term (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Term.get_refs.go) _term)) + +Book.Kind.Term = 0 + +Book.Kind.Term.parse = λ_code + let _P = λ_x (Book.Kind.Term) + let _done = λ_code λ_term (_term ((Book.List.nil) (Book.Kind.Binder))) + let _fail = λ_error (((Book.Kind.hol) (Str "error")) ((Book.List.nil) (Book.Kind.Term))) + (((((Book.Kind.Term.parser) _code) _P) _done) _fail) + +Book.Kind.Term.parser.all = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "∀")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "∀"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "("))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_inp ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ")"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp ((((Book.Kind.all) _nam) (_inp _scp)) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp)))))))))))) + +Book.Kind.Term.parser.ann = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "{")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "{"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_val ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_typ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "}"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.ann) (_val _scp)) (_typ _scp))))))))) + +Book.Kind.Term.parser.app = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "(")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "("))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_fun ((((Book.Kind.Term.parser.bind) ((Book.List) (Book.Kind.PreTerm))) ((((Book.Parser.until) (Book.Kind.PreTerm)) (((Book.Parser.skip) (Book.Bool)) ((Book.Parser.test) (Str ")")))) (Book.Kind.Term.parser))) λ_terms ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ")"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (((((((Book.List.fold) (Book.Kind.PreTerm)) _terms) 0) λ_arg λ_rec λ_fun (_rec (((Book.Kind.app) _fun) (_arg _scp)))) λ_fun _fun) (_fun _scp)))))))) + +Book.Kind.Term.parser.bind = λ_A (((Book.Parser.bind) _A) (Book.Kind.PreTerm)) + +Book.Kind.Term.parser.chr = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "'")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "'"))) λ__ ((((Book.Kind.Term.parser.bind) 0) (Book.Parser.char)) λ_chr ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "'"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.num) _chr)))))) + +Book.Kind.Term.parser.def = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "let ")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "let "))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "="))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_val ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp ((((Book.Kind.def) _nam) (_val _scp)) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp)))))))))) + +Book.Kind.Term.parser.hol = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "?")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "?"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.hol) _nam) ((Book.List.nil) (Book.Kind.Term))))))) + +Book.Kind.Term.parser.ins = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "~")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "~"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_val ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.ins) (_val _scp)))))) + +Book.Kind.Term.parser = + let _TRY = ((Book.List.cons) ((Book.Parser.Guard) (Book.Kind.PreTerm))) + let _END = ((Book.List.nil) ((Book.Parser.Guard) (Book.Kind.PreTerm))) + (((Book.Parser.variant) (Book.Kind.PreTerm)) ((_TRY (Book.Kind.Term.parser.all)) ((_TRY (Book.Kind.Term.parser.lam)) ((_TRY (Book.Kind.Term.parser.app)) ((_TRY (Book.Kind.Term.parser.ann)) ((_TRY (Book.Kind.Term.parser.slf)) ((_TRY (Book.Kind.Term.parser.ins)) ((_TRY (Book.Kind.Term.parser.set)) ((_TRY (Book.Kind.Term.parser.def)) ((_TRY (Book.Kind.Term.parser.u60)) ((_TRY (Book.Kind.Term.parser.op2)) ((_TRY (Book.Kind.Term.parser.mat)) ((_TRY (Book.Kind.Term.parser.chr)) ((_TRY (Book.Kind.Term.parser.str)) ((_TRY (Book.Kind.Term.parser.num)) ((_TRY (Book.Kind.Term.parser.hol)) ((_TRY (Book.Kind.Term.parser.var)) _END))))))))))))))))) + +Book.Kind.Term.parser.lam = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "λ")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "λ"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.lam) _nam) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp)))))))) + +Book.Kind.Term.parser.mat = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#match ")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#match "))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "="))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_x ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "{"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#0"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_z ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#+"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_s ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "}"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ":"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_p ((Book.Kind.Term.parser.pure) λ_scp ((((((Book.Kind.mat) _nam) (_x _scp)) (_z _scp)) λ_x (_s ((((Book.Kind.Scope.extend) (((Book.String.concat) _nam) (Str "-1"))) _x) _scp))) λ_x (_p ((((Book.Kind.Scope.extend) _nam) _x) _scp))))))))))))))))))) + +Book.Kind.Term.parser.num = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#"))) λ__ ((((Book.Kind.Term.parser.bind) 0) (Book.U60.parser.decimal)) λ_num ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.num) _num))))) + +Book.Kind.Term.parser.op2 = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#(")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#("))) λ__ ((((Book.Kind.Term.parser.bind) (Book.Kind.Oper)) (Book.Kind.Oper.parser)) λ_opr ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_fst ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_snd ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str ")"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp ((((Book.Kind.op2) _opr) (_fst _scp)) (_snd _scp))))))))) + +Book.Kind.Term.parser.pure = ((Book.Parser.pure) (Book.Kind.PreTerm)) + +Book.Kind.Term.parser.set = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "*")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "*"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (Book.Kind.set)))) + +Book.Kind.Term.parser.slf = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "$")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "$"))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((((Book.Kind.Term.parser.bind) (Book.Kind.PreTerm)) (Book.Kind.Term.parser)) λ_bod ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.slf) _nam) λ_x (_bod ((((Book.Kind.Scope.extend) _nam) _x) _scp)))))))) + +Book.Kind.Term.parser.str = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Book.String.quote)) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Book.String.quote))) λ__ ((((Book.Kind.Term.parser.bind) (Book.String)) ((((Book.Parser.until) (Book.Char)) ((Book.Parser.test) (Book.String.quote))) (Book.Parser.char))) λ_chars ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Book.String.quote))) λ__ ((Book.Kind.Term.parser.pure) λ_scp ((Book.Kind.txt) _chars)))))) + +Book.Kind.Term.parser.u60 = ((((Book.Parser.Guard.text) (Book.Kind.PreTerm)) (Str "#U60")) ((((Book.Kind.Term.parser.bind) (Book.Unit)) ((Book.Parser.text) (Str "#U60"))) λ__ ((Book.Kind.Term.parser.pure) λ_scp (Book.Kind.u60)))) + +Book.Kind.Term.parser.var = (((Book.Parser.Guard.pass) (Book.Kind.PreTerm)) ((((Book.Kind.Term.parser.bind) (Book.String)) (Book.Parser.name)) λ_nam ((Book.Kind.Term.parser.pure) λ_scp (((Book.Kind.Scope.find) _nam) _scp)))) + +Book.Kind.Term.show.go = λ_term λ_dep + let _P = λ_X (Book.String.Concatenator) + let _all = λ_nam λ_inp λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "∀(")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str ": ")) ((((Book.Kind.Term.show.go) _inp) _dep) (((Book.Kind.Text.show.go) (Str ") ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil)))))) + let _lam = λ_nam λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "λ")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil)))) + let _app = λ_fun λ_arg λ_nil (((Book.Kind.Text.show.go) (Str "(")) ((((Book.Kind.Term.show.go) _fun) _dep) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) _arg) _dep) (((Book.Kind.Text.show.go) (Str ")")) _nil))))) + let _ann = λ_val λ_typ λ_nil (((Book.Kind.Text.show.go) (Str "{")) ((((Book.Kind.Term.show.go) _val) _dep) (((Book.Kind.Text.show.go) (Str " : ")) ((((Book.Kind.Term.show.go) _typ) _dep) (((Book.Kind.Text.show.go) (Str "}")) _nil))))) + let _slf = λ_nam λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "$")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil)))) + let _ins = λ_val λ_nil (((Book.Kind.Text.show.go) (Str "~")) ((((Book.Kind.Term.show.go) _val) _dep) _nil)) + let _ref = λ_nam λ_val λ_nil (((Book.Kind.Text.show.go) _nam) _nil) + let _def = λ_nam λ_val λ_bod λ_nil (((Book.Kind.Text.show.go) (Str "let ")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " = ")) ((((Book.Kind.Term.show.go) _val) _dep) (((Book.Kind.Text.show.go) (Str "; ")) ((((Book.Kind.Term.show.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil)))))) + let _set = λ_nil (((Book.Kind.Text.show.go) (Str "*")) _nil) + let _u60 = λ_nil (((Book.Kind.Text.show.go) (Str "#U60")) _nil) + let _num = λ_val λ_nil (((Book.Kind.Text.show.go) (Str "#")) (((Book.U60.show.go) _val) _nil)) + let _op2 = λ_opr λ_fst λ_snd λ_nil (((Book.Kind.Text.show.go) (Str "#(")) (((Book.Kind.Oper.show.go) _opr) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) _fst) _dep) (((Book.Kind.Text.show.go) (Str " ")) ((((Book.Kind.Term.show.go) _snd) _dep) (((Book.Kind.Text.show.go) (Str ")")) _nil))))))) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_nil (((Book.Kind.Text.show.go) (Str "#match ")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str " = ")) ((((Book.Kind.Term.show.go) _x) _dep) (((Book.Kind.Text.show.go) (Str " { #0: ")) ((((Book.Kind.Term.show.go) _z) _dep) (((Book.Kind.Text.show.go) (Str "; #+: ")) ((((Book.Kind.Term.show.go) (_s (((Book.Kind.var) (((Book.String.concat) _nam) (Str "-1"))) _dep))) ((Book.Nat.succ) _dep)) (((Book.Kind.Text.show.go) (Str " }: ")) ((((Book.Kind.Term.show.go) (_p (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) _nil)))))))))) + let _txt = λ_text λ_nil (((Book.Kind.Text.show.go) (Book.String.quote)) (((Book.Kind.Text.show.go) _text) (((Book.Kind.Text.show.go) (Book.String.quote)) _nil))) + let _hol = λ_nam λ_ctx λ_nil (((Book.Kind.Text.show.go) (Str "?")) (((Book.Kind.Text.show.go) _nam) _nil)) + let _var = λ_nam λ_idx λ_nil (((Book.Kind.Text.show.go) _nam) _nil) + (((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) + +Book.Kind.Term.show = λ_term λ_dep ((Book.String.Concatenator.build) (((Book.Kind.Term.show.go) _term) _dep)) + +Book.Kind.Term.to_hvm.go = λ_term λ_dep λ_inc λ_tab + let _P = λ_x (Book.String.Concatenator) + let _all = λ_nam λ_inp λ_bod λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil)) + let _lam = λ_nam λ_bod λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "λ")) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) _nam)) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) (Book.Bool.true)) _tab) _nil))))) + let _app = λ_fun λ_arg λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(")) ((((((Book.Kind.Term.to_hvm.go) _fun) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _arg) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str ")")) _nil)))))) + let _ann = λ_val λ_typ λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) ((((((Book.Kind.Term.to_hvm.go) _val) _dep) (Book.Bool.true)) _tab) _nil)) + let _slf = λ_nam λ_bod λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil)) + let _ins = λ_val λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) ((((((Book.Kind.Term.to_hvm.go) _val) _dep) (Book.Bool.true)) _tab) _nil)) + let _ref = λ_nam λ_val λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(Book.")) (((Book.Kind.Text.show.go) _nam) (((Book.Kind.Text.show.go) (Str ")")) _nil)))) + let _def = λ_nam λ_val λ_bod λ_nil + let _tab = ((((_inc λ_x 0) (Book.Nat.succ)) λ_x _x) _tab) + (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Text.show.go) ((Book.String.indent) _tab)) (((Book.Kind.Text.show.go) (Str "let ")) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) _nam)) (((Book.Kind.Text.show.go) (Str " = ")) ((((((Book.Kind.Term.to_hvm.go) _val) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep)) (Book.Bool.false)) _tab) _nil)))))))) + let _set = λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil)) + let _u60 = λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil)) + let _num = λ_val λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.U60.show.go) _val) _nil)) + let _op2 = λ_opr λ_fst λ_snd λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(")) (((Book.Kind.Oper.show.go) _opr) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _fst) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _snd) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str ")")) _nil)))))))) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(U60.match ")) ((((((Book.Kind.Term.to_hvm.go) _x) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) ((((((Book.Kind.Term.to_hvm.go) _z) _dep) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str " ")) (((Book.Kind.Text.show.go) (Str "λ")) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) (((Book.String.concat) _nam) (Str "_1")))) (((Book.Kind.Text.show.go) (Str "(")) ((((((Book.Kind.Term.to_hvm.go) (_s (((Book.Kind.var) (((Book.String.concat) _nam) (Str "_1"))) _dep))) ((Book.Nat.succ) _dep)) (Book.Bool.true)) _tab) (((Book.Kind.Text.show.go) (Str ")")) (((Book.Kind.Text.show.go) (Str ")")) _nil)))))))))))) + let _txt = λ_txt λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "(Str ")) (((Book.Kind.Text.show.go) (Book.String.quote)) (((Book.Kind.Text.show.go) _txt) (((Book.Kind.Text.show.go) (Book.String.quote)) (((Book.Kind.Text.show.go) (Str ")")) _nil)))))) + let _hol = λ_nam λ_ctx λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (Str "0")) _nil)) + let _var = λ_nam λ_idx λ_nil ((((Book.Kind.Term.to_hvm.nl) _inc) _tab) (((Book.Kind.Text.show.go) (((Book.String.cons) 95) _nam)) _nil)) + (((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) + +Book.Kind.Term.to_hvm = λ_term λ_dep ((Book.String.Concatenator.build) (((Book.Kind.Term.to_hvm.go) _term) _dep)) + +Book.Kind.Term.to_hvm.nl = λ_inc λ_tab + let _P = λ_x (Book.String.Concatenator) + let _true = λ_nil _nil + let _false = λ_nil (((Book.Kind.Text.show.go) (Book.String.newline)) (((Book.Kind.Text.show.go) ((Book.String.indent) _tab)) _nil)) + (((_inc _P) _true) _false) + +Book.Kind.Text = (Book.String) + +Book.Kind.Text.show.go = (Book.String.Concatenator.from_string) + +Book.Kind.all = λ_nam λ_inp λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((_all _nam) _inp) _bod) + +Book.Kind.ann = λ_val λ_typ λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_ann _val) _typ) + +Book.Kind.app = λ_fun λ_arg λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_app _fun) _arg) + +Book.Kind.check = λ_term λ_type λ_dep + let _bind = (((Book.Maybe.bind) (Book.Kind.Term)) (Book.Kind.Term)) + let _pure = ((Book.Maybe.some) (Book.Kind.Term)) + let _none = ((Book.Maybe.none) (Book.Kind.Term)) + let _P = λ_x 0 + let _all = λ_term.nam λ_term.inp λ_term.bod λ_type λ_dep ((((Book.Kind.verify) ((((Book.Kind.all) _term.nam) _term.inp) _term.bod)) _type) _dep) + let _lam = λ_term.nam λ_term.bod λ_type λ_dep (((((((Book.Kind.if.all) (((Book.Kind.reduce) (Book.Bool.true)) _type)) 0) λ_type.nam λ_type.inp λ_type.bod λ_dep λ_term.bod + let _ann = (((Book.Kind.ann) (((Book.Kind.var) _term.nam) _dep)) _type.inp) + let _term = (_term.bod _ann) + let _type = (_type.bod _ann) + ((((Book.Kind.check) _term) _type) ((Book.Nat.succ) _dep))) λ_type λ_dep λ_term.bod (((Book.Kind.infer) (((Book.Kind.lam) _term.nam) _term.bod)) _dep)) _dep) _term.bod) + let _app = λ_term.fun λ_term.arg λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.app) _term.fun) _term.arg)) _type) _dep) + let _ann = λ_val λ_typ λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.ann) _val) _typ)) _type) _dep) + let _slf = λ_term.nam λ_term.bod λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.slf) _term.nam) _term.bod)) _type) _dep) + let _ins = λ_term.val λ_type λ_dep ((((((Book.Kind.if.slf) (((Book.Kind.reduce) (Book.Bool.true)) _type)) 0) λ_type.nam λ_type.bod λ_term.val ((((Book.Kind.check) _term.val) (_type.bod ((Book.Kind.ins) _term.val))) _dep)) λ_type λ_term.val (((Book.Kind.infer) ((Book.Kind.ins) _term.val)) _dep)) _term.val) + let _ref = λ_term.nam λ_term.val λ_type λ_dep ((((Book.Kind.check) _term.val) _type) _dep) + let _def = λ_term.nam λ_term.val λ_term.bod λ_type λ_dep ((((Book.Kind.check) (_term.bod _term.val)) _type) ((Book.Nat.succ) _dep)) + let _set = λ_type λ_dep ((((Book.Kind.verify) (Book.Kind.set)) _type) _dep) + let _u60 = λ_type λ_dep ((((Book.Kind.verify) (Book.Kind.u60)) _type) _dep) + let _num = λ_term.num λ_type λ_dep ((((Book.Kind.verify) ((Book.Kind.num) _term.num)) _type) _dep) + let _op2 = λ_term.opr λ_term.fst λ_term.snd λ_type λ_dep ((((Book.Kind.verify) ((((Book.Kind.op2) _term.opr) _term.fst) _term.snd)) _type) _dep) + let _mat = λ_term.nam λ_term.x λ_term.z λ_term.s λ_term.p λ_type λ_dep ((((Book.Kind.verify) ((((((Book.Kind.mat) _term.nam) _term.x) _term.z) _term.s) _term.p)) _type) _dep) + let _txt = λ_term.txt λ_type λ_dep ((((Book.Kind.verify) ((Book.Kind.txt) _term.txt)) _type) _dep) + let _hol = λ_term.nam λ_term.ctx λ_type λ_dep (_pure (Book.Kind.set)) + let _var = λ_term.nam λ_term.idx λ_type λ_dep ((((Book.Kind.verify) (((Book.Kind.var) _term.nam) _term.idx)) _type) _dep) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _type) _dep) + +Book.Kind.comparer = λ_rec λ_a λ_b λ_dep + let _VAR = (Book.Kind.var) + let _SUC = (Book.Nat.succ) + let _a = ((Book.Kind.skip) _a) + let _b = ((Book.Kind.skip) _b) + let _R = 0 + let _Y = λ_a.nam λ_a.ctx λ_b λ_dep (Book.Bool.true) + let _N = λ_a λ_b λ_dep + let _R = 0 + let _Y = λ_b.nam λ_b.ctx λ_dep λ_a (Book.Bool.true) + let _N = λ_b λ_dep λ_a + let _P = λ_x 0 + let _all = λ_a.nam λ_a.inp λ_a.bod λ_b λ_dep + let _P = 0 + let _Y = λ_b.nam λ_b.inp λ_b.bod λ_dep (((Book.Bool.and) (((_rec _a.inp) _b.inp) _dep)) (((_rec (_a.bod ((_VAR _a.nam) _dep))) (_b.bod ((_VAR _b.nam) _dep))) (_SUC _dep))) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.all) _b) _P) _Y) _N) _dep) + let _lam = λ_a.nam λ_a.bod λ_b λ_dep + let _P = 0 + let _Y = λ_b.nam λ_b.bod λ_dep (((_rec (_a.bod ((_VAR _a.nam) _dep))) (_b.bod ((_VAR _b.nam) _dep))) (_SUC _dep)) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.lam) _b) _P) _Y) _N) _dep) + let _app = λ_a.fun λ_a.arg λ_b λ_dep + let _P = 0 + let _Y = λ_b.fun λ_b.arg λ_dep (((Book.Bool.and) (((_rec _a.fun) _b.fun) _dep)) (((_rec _a.arg) _b.arg) _dep)) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.app) _b) _P) _Y) _N) _dep) + let _ann = λ_a.val λ_a.typ λ_b λ_dep (Book.Bool.false) + let _slf = λ_a.nam λ_a.bod λ_b λ_dep + let _P = 0 + let _Y = λ_b.nam λ_b.bod λ_dep (((_rec (_a.bod ((_VAR _a.nam) _dep))) (_b.bod ((_VAR _b.nam) _dep))) (_SUC _dep)) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.slf) _b) _P) _Y) _N) _dep) + let _ins = λ_a.val λ_b λ_dep (Book.Bool.false) + let _ref = λ_a.nam λ_a.val λ_b λ_dep + let _P = 0 + let _Y = λ_b.nam λ_b.val λ_dep (((Book.String.equal) _a.nam) _b.nam) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.ref) _b) _P) _Y) _N) _dep) + let _def = λ_a.nam λ_a.val λ_a.bod λ_b λ_dep (Book.Bool.false) + let _set = λ_b λ_dep + let _P = 0 + let _Y = λ_dep (Book.Bool.true) + let _F = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.set) _b) _P) _Y) _F) _dep) + let _u60 = λ_b λ_dep + let _P = 0 + let _Y = λ_dep (Book.Bool.true) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.u60) _b) _P) _Y) _N) _dep) + let _num = λ_a.val λ_b λ_dep + let _P = 0 + let _Y = λ_b.val λ_dep (((Book.U60.equal) _a.val) _b.val) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.num) _b) _P) _Y) _N) _dep) + let _op2 = λ_a.opr λ_a.fst λ_a.snd λ_b λ_dep + let _P = 0 + let _Y = λ_b.opr λ_b.fst λ_b.snd λ_dep (((Book.Bool.and) (((_rec _a.fst) _b.fst) _dep)) (((_rec _a.snd) _b.snd) _dep)) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.op2) _b) _P) _Y) _N) _dep) + let _mat = λ_a.nam λ_a.x λ_a.z λ_a.s λ_a.p λ_b λ_dep + let _P = 0 + let _Y = λ_b.nam λ_b.x λ_b.z λ_b.s λ_b.p λ_dep (((Book.Bool.and) (((_rec _a.x) _b.x) _dep)) (((Book.Bool.and) (((_rec _a.z) _b.z) _dep)) (((Book.Bool.and) (((_rec (_a.s ((_VAR (((Book.String.concat) _a.nam) (Str "-1"))) _dep))) (_b.s ((_VAR (((Book.String.concat) _b.nam) (Str "-1"))) _dep))) (_SUC _dep))) (((_rec (_a.p ((_VAR _a.nam) _dep))) (_b.p ((_VAR _b.nam) _dep))) (_SUC _dep))))) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.mat) _b) _P) _Y) _N) _dep) + let _txt = λ_a.txt λ_b λ_dep + let _P = 0 + let _Y = λ_b.txt λ_dep (((Book.String.equal) _a.txt) _b.txt) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.txt) _b) _P) _Y) _N) _dep) + let _hol = λ_a.nam λ_a.ctx λ_b λ_dep (Book.Bool.false) + let _var = λ_a.nam λ_a.idx λ_b λ_dep + let _P = 0 + let _Y = λ_b.nam λ_b.idx λ_dep (((Book.Nat.equal) _a.idx) _b.idx) + let _N = λ_val λ_dep (Book.Bool.false) + ((((((Book.Kind.if.var) _b) _P) _Y) _N) _dep) + (((((((((((((((((((_a _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _b) _dep) + (((((((Book.Kind.if.hol) _b) _R) _Y) _N) _dep) _a) + (((((((Book.Kind.if.hol) _a) _R) _Y) _N) _b) _dep) + +Book.Kind.def = λ_nam λ_val λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((_def _nam) _val) _bod) + +Book.Kind.equal.enter = λ_e λ_a λ_b λ_dep + let _P = λ_x 0 + let _true = λ_a λ_b λ_dep (Book.Bool.true) + let _false = λ_a λ_b λ_dep (((((Book.Kind.comparer) (Book.Kind.equal)) _a) _b) _dep) + ((((((_e _P) _true) _false) _a) _b) _dep) + +Book.Kind.equal = λ_a λ_b λ_dep (((((Book.Kind.equal.minor) ((((Book.Kind.identical) _a) _b) _dep)) _a) _b) _dep) + +Book.Kind.equal.major = λ_e λ_a λ_b λ_dep + let _P = λ_x 0 + let _true = λ_a λ_b λ_dep (Book.Bool.true) + let _false = λ_a λ_b λ_dep + let _a_wnf = (((Book.Kind.reduce) (Book.Bool.true)) _a) + let _b_wnf = (((Book.Kind.reduce) (Book.Bool.true)) _b) + (((((Book.Kind.equal.enter) ((((Book.Kind.identical) _a_wnf) _b_wnf) _dep)) _a_wnf) _b_wnf) _dep) + ((((((_e _P) _true) _false) _a) _b) _dep) + +Book.Kind.equal.minor = λ_e λ_a λ_b λ_dep + let _P = λ_x 0 + let _true = λ_a λ_b λ_dep (Book.Bool.true) + let _false = λ_a λ_b λ_dep + let _a_wnf = (((Book.Kind.reduce) (Book.Bool.false)) _a) + let _b_wnf = (((Book.Kind.reduce) (Book.Bool.false)) _b) + (((((Book.Kind.equal.major) ((((Book.Kind.identical) _a_wnf) _b_wnf) _dep)) _a_wnf) _b_wnf) _dep) + ((((((_e _P) _true) _false) _a) _b) _dep) + +Book.Kind.hol = λ_nam λ_ctx λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_hol _nam) _ctx) + +Book.Kind.identical = λ_a λ_b λ_dep (((((Book.Kind.comparer) (Book.Kind.identical)) _a) _b) _dep) + +Book.Kind.if.all = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (((_Y _nam) _inp) _bod) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.ann = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N ((_Y _val) _typ) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.app = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N ((_Y _fun) _arg) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.def = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (((_Y _nam) _val) _bod) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.hol = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N ((_Y _nam) _ctx) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.ins = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_Y _val) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.lam = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N ((_Y _nam) _bod) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.mat = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (((((_Y _nam) _x) _z) _s) _p) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.num = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_Y _val) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.op2 = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (((_Y _opr) _fst) _snd) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.ref = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N ((_Y _nam) _val) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.set = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N _Y + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.slf = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N ((_Y _nam) _bod) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.txt = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_Y _lit) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.u60 = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N _Y + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N (_N (((Book.Kind.var) _nam) _idx)) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.if.var = λ_term λ_P λ_Y λ_N + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_Y λ_N (_N ((((Book.Kind.all) _nam) _inp) _bod)) + let _lam = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.lam) _nam) _bod)) + let _app = λ_fun λ_arg λ_Y λ_N (_N (((Book.Kind.app) _fun) _arg)) + let _ann = λ_val λ_typ λ_Y λ_N (_N (((Book.Kind.ann) _val) _typ)) + let _slf = λ_nam λ_bod λ_Y λ_N (_N (((Book.Kind.slf) _nam) _bod)) + let _ins = λ_val λ_Y λ_N (_N ((Book.Kind.ins) _val)) + let _ref = λ_nam λ_val λ_Y λ_N (_N (((Book.Kind.ref) _nam) _val)) + let _def = λ_nam λ_val λ_bod λ_Y λ_N (_N ((((Book.Kind.def) _nam) _val) _bod)) + let _set = λ_Y λ_N (_N (Book.Kind.set)) + let _u60 = λ_Y λ_N (_N (Book.Kind.u60)) + let _num = λ_val λ_Y λ_N (_N ((Book.Kind.num) _val)) + let _op2 = λ_opr λ_fst λ_snd λ_Y λ_N (_N ((((Book.Kind.op2) _opr) _fst) _snd)) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_Y λ_N (_N ((((((Book.Kind.mat) _nam) _x) _z) _s) _p)) + let _txt = λ_lit λ_Y λ_N (_N ((Book.Kind.txt) _lit)) + let _hol = λ_nam λ_ctx λ_Y λ_N (_N (((Book.Kind.hol) _nam) _ctx)) + let _var = λ_nam λ_idx λ_Y λ_N ((_Y _nam) _idx) + (((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _Y) _N) + +Book.Kind.infer = λ_term λ_dep + let _bind = (((Book.Maybe.bind) (Book.Kind.Term)) (Book.Kind.Term)) + let _pure = ((Book.Maybe.some) (Book.Kind.Term)) + let _none = ((Book.Maybe.none) (Book.Kind.Term)) + let _P = λ_x 0 + let _all = λ_nam λ_inp λ_bod λ_dep ((_bind ((((Book.Kind.check) _inp) (Book.Kind.set)) _dep)) λ__ ((_bind ((((Book.Kind.check) (_bod (((Book.Kind.ann) (((Book.Kind.var) _nam) _dep)) _inp))) (Book.Kind.set)) ((Book.Nat.succ) _dep))) λ__ (_pure (Book.Kind.set)))) + let _lam = λ_nam λ_bod λ_dep _none + let _app = λ_fun λ_arg λ_dep ((_bind (((Book.Kind.infer) _fun) _dep)) λ_fun_typ (((((((Book.Kind.if.all) (((Book.Kind.reduce) (Book.Bool.true)) _fun_typ)) 0) λ_fun_typ.nam λ_fun_typ.inp λ_fun_typ.bod λ_fun λ_arg ((_bind ((((Book.Kind.check) _arg) _fun_typ.inp) _dep)) λ__ (_pure (_fun_typ.bod _arg)))) λ_fun_typ λ_fun λ_arg _none) _fun) _arg)) + let _ann = λ_val λ_typ λ_dep (_pure _typ) + let _slf = λ_nam λ_bod λ_dep ((_bind ((((Book.Kind.check) (_bod (((Book.Kind.ann) (((Book.Kind.var) _nam) _dep)) (((Book.Kind.slf) _nam) _bod)))) (Book.Kind.set)) ((Book.Nat.succ) _dep))) λ__ (_pure (Book.Kind.set))) + let _ins = λ_val λ_dep ((_bind (((Book.Kind.infer) _val) _dep)) λ_val_typ ((((((Book.Kind.if.slf) (((Book.Kind.reduce) (Book.Bool.true)) _val_typ)) 0) λ_val_nam λ_val_typ.bod λ_val (_pure (_val_typ.bod ((Book.Kind.ins) _val)))) λ_val_typ λ_val _none) _val)) + let _ref = λ_nam λ_val λ_dep (((Book.Kind.infer) _val) _dep) + let _def = λ_nam λ_val λ_bod λ_dep _none + let _set = λ_dep (_pure (Book.Kind.set)) + let _u60 = λ_dep (_pure (Book.Kind.set)) + let _num = λ_num λ_dep (_pure (Book.Kind.u60)) + let _txt = λ_txt λ_dep (_pure (Book.Kind.Book.String)) + let _op2 = λ_opr λ_fst λ_snd λ_dep ((_bind ((((Book.Kind.check) _fst) (Book.Kind.u60)) _dep)) λ__ ((_bind ((((Book.Kind.check) _snd) (Book.Kind.u60)) _dep)) λ__ (_pure (Book.Kind.u60)))) + let _mat = λ_nam λ_x λ_z λ_s λ_p λ_dep ((_bind ((((Book.Kind.check) _x) (Book.Kind.u60)) _dep)) λ_x_typ ((_bind ((((Book.Kind.check) (_p (((Book.Kind.ann) (((Book.Kind.var) _nam) _dep)) (Book.Kind.u60)))) (Book.Kind.set)) _dep)) λ_p_typ ((_bind ((((Book.Kind.check) _z) (_p ((Book.Kind.num) 0))) _dep)) λ_z_typ ((_bind ((((Book.Kind.check) (_s (((Book.Kind.ann) (((Book.Kind.var) (((Book.String.concat) _nam) (Str "-1"))) _dep)) (Book.Kind.u60)))) (_p ((((Book.Kind.op2) (Book.Kind.Oper.add)) ((Book.Kind.num) 1)) (((Book.Kind.var) (((Book.String.concat) _nam) (Str "-1"))) _dep)))) ((Book.Nat.succ) _dep))) λ_s_typ (_pure (_p _x)))))) + let _hol = λ_nam λ_ctx λ_dep _none + let _var = λ_nam λ_idx λ_dep _none + ((((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) _dep) + +Book.Kind.ins = λ_val λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (_ins _val) + +Book.Kind = + let _a = (((Book.Kind.lam) (Str "f")) λ_f (((Book.Kind.lam) (Str "x")) λ_x (((Book.Kind.app) _f) (((Book.Kind.app) _f) _x)))) + let _b = (((Book.Kind.lam) (Str "f")) λ_f (((Book.Kind.lam) (Str "x")) λ_x (((Book.Kind.app) _f) (((Book.Kind.app) _f) _x)))) + let _Test = ((((Book.Kind.all) (Str "A")) (Book.Kind.set)) λ_A ((((Book.Kind.all) (Str "B")) (Book.Kind.set)) λ_B ((((Book.Kind.all) (Str "a")) _A) λ_a ((((Book.Kind.all) (Str "b")) _B) λ_b _B)))) + let _test = (((Book.Kind.lam) (Str "A")) λ_A (((Book.Kind.lam) (Str "B")) λ_B (((Book.Kind.lam) (Str "a")) λ_a (((Book.Kind.lam) (Str "b")) λ_b _b)))) + let _P = λ_x (Book.String) + let _some = λ_value (((Book.Kind.Term.show) _value) (Book.Nat.zero)) + let _none = (Str "error") + let _chk = ((((Book.Kind.check) _test) _Test) (Book.Nat.zero)) + (((_chk _P) _some) _none) + +Book.Kind.lam = λ_nam λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_lam _nam) _bod) + +Book.Kind.mat = λ_nam λ_x λ_z λ_s λ_p λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((((_mat _nam) _x) _z) _s) _p) + +Book.Kind.normal.go = λ_maj λ_term λ_dep + let _P = λ_x (Book.Kind.Term) + let _all = λ_nam λ_inp λ_bod ((((Book.Kind.all) _nam) ((((Book.Kind.normal) _maj) _inp) _dep)) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) + let _lam = λ_nam λ_bod (((Book.Kind.lam) _nam) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) + let _app = λ_fun λ_arg (((Book.Kind.app) ((((Book.Kind.normal) _maj) _fun) _dep)) ((((Book.Kind.normal) _maj) _arg) _dep)) + let _ann = λ_val λ_typ (((Book.Kind.ann) ((((Book.Kind.normal) _maj) _val) _dep)) ((((Book.Kind.normal) _maj) _typ) _dep)) + let _slf = λ_nam λ_bod (((Book.Kind.slf) _nam) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) + let _ins = λ_val ((Book.Kind.ins) ((((Book.Kind.normal) _maj) _val) _dep)) + let _ref = λ_nam λ_val (((Book.Kind.ref) _nam) ((((Book.Kind.normal) _maj) _val) _dep)) + let _def = λ_nam λ_val λ_bod ((((Book.Kind.def) _nam) ((((Book.Kind.normal) _maj) _val) _dep)) λ_x ((((Book.Kind.normal) _maj) (_bod (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) + let _set = (Book.Kind.set) + let _u60 = (Book.Kind.u60) + let _num = (Book.Kind.num) + let _op2 = λ_opr λ_fst λ_snd ((((Book.Kind.op2) _opr) ((((Book.Kind.normal) _maj) _fst) _dep)) ((((Book.Kind.normal) _maj) _snd) _dep)) + let _mat = λ_nam λ_x λ_z λ_s λ_p ((((((Book.Kind.mat) _nam) ((((Book.Kind.normal) _maj) _x) _dep)) ((((Book.Kind.normal) _maj) _z) _dep)) λ_k ((((Book.Kind.normal) _maj) (_s (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) λ_k ((((Book.Kind.normal) _maj) (_p (((Book.Kind.var) _nam) _dep))) ((Book.Nat.succ) _dep))) + let _txt = λ_txt ((Book.Kind.txt) _txt) + let _hol = λ_nam λ_ctx (((Book.Kind.hol) _nam) _ctx) + let _var = λ_nam λ_idx (((Book.Kind.var) _nam) _idx) + (((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) + +Book.Kind.normal = λ_maj λ_term λ_dep ((((Book.Kind.normal.go) _maj) (((Book.Kind.reduce) _maj) _term)) _dep) + +Book.Kind.num = λ_val λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (_num _val) + +Book.Kind.op2 = λ_opr λ_fst λ_snd λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((_op2 _opr) _fst) _snd) + +Book.Kind.reduce.app = λ_maj λ_fun λ_arg + let _P = 0 + let _Y = λ_nam λ_bod λ_arg (((Book.Kind.reduce) _maj) (_bod (((Book.Kind.reduce) _maj) _arg))) + let _N = λ_fun λ_arg (((Book.Kind.app) _fun) _arg) + ((((((Book.Kind.if.lam) _fun) _P) _Y) _N) _arg) + +Book.Kind.reduce = λ_maj λ_term + let _P = λ_x (Book.Kind.Term) + let _all = (Book.Kind.all) + let _lam = (Book.Kind.lam) + let _app = λ_fun λ_arg ((((Book.Kind.reduce.app) _maj) (((Book.Kind.reduce) _maj) _fun)) _arg) + let _slf = (Book.Kind.slf) + let _ann = λ_val λ_typ (((Book.Kind.reduce) _maj) _val) + let _ins = λ_val (((Book.Kind.reduce) _maj) _val) + let _ref = λ_nam λ_val ((((Book.Kind.reduce.ref) _maj) _nam) _val) + let _def = λ_nam λ_val λ_bod (((Book.Kind.reduce) _maj) (_bod _val)) + let _set = (Book.Kind.set) + let _u60 = (Book.Kind.u60) + let _num = (Book.Kind.num) + let _op2 = λ_opr λ_fst λ_snd ((((Book.Kind.reduce.op2) _opr) _fst) _snd) + let _mat = λ_nam λ_x λ_z λ_s λ_p (((((((Book.Kind.reduce.mat) _maj) _nam) _x) _z) _s) _p) + let _txt = λ_txt ((Book.Kind.reduce.txt) _txt) + let _hol = (Book.Kind.hol) + let _var = (Book.Kind.var) + (((((((((((((((((_term _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) + +Book.Kind.reduce.mat = λ_maj λ_nam λ_x λ_z λ_s λ_p + let _P = 0 + let _Y = λ_x.val (U60.match _x.val λ_z λ_s (((Book.Kind.reduce) _maj) _z) λ_x_1(λ_z λ_s (((Book.Kind.reduce) _maj) (_s ((Book.Kind.num) _x_1))))) + let _N = λ_x λ_z λ_s ((((((Book.Kind.mat) _nam) _x) _z) _s) _p) + (((((((Book.Kind.if.num) _x) _P) _Y) _N) _z) _s) + +Book.Kind.reduce.op2 = λ_opr λ_fst λ_snd + let _P = 0 + let _Y = λ_fst_val λ_snd + let _P = 0 + let _Y = λ_snd_val λ_fst_val + let _P = λ_x 0 + let _add = λ_fst_val λ_snd_val ((Book.Kind.num) (+ _fst_val _snd_val)) + let _mul = λ_fst_val λ_snd_val ((Book.Kind.num) (* _fst_val _snd_val)) + let _sub = λ_fst_val λ_snd_val ((Book.Kind.num) (- _fst_val _snd_val)) + let _div = λ_fst_val λ_snd_val ((Book.Kind.num) (/ _fst_val _snd_val)) + let _eq = λ_fst_val λ_snd_val ((Book.Kind.num) (== _fst_val _snd_val)) + let _ne = λ_fst_val λ_snd_val ((Book.Kind.num) (!= _fst_val _snd_val)) + let _lt = λ_fst_val λ_snd_val ((Book.Kind.num) (< _fst_val _snd_val)) + let _gt = λ_fst_val λ_snd_val ((Book.Kind.num) (> _fst_val _snd_val)) + let _lte = λ_fst_val λ_snd_val ((Book.Kind.num) (<= _fst_val _snd_val)) + let _gte = λ_fst_val λ_snd_val ((Book.Kind.num) (>= _fst_val _snd_val)) + let _and = λ_fst_val λ_snd_val ((Book.Kind.num) (& _fst_val _snd_val)) + let _or = λ_fst_val λ_snd_val ((Book.Kind.num) (| _fst_val _snd_val)) + let _xor = λ_fst_val λ_snd_val ((Book.Kind.num) (^ _fst_val _snd_val)) + let _lsh = λ_fst_val λ_snd_val ((Book.Kind.num) (<< _fst_val _snd_val)) + let _rsh = λ_fst_val λ_snd_val ((Book.Kind.num) (>> _fst_val _snd_val)) + ((((((((((((((((((_opr _P) _add) _mul) _sub) _div) _eq) _ne) _lt) _gt) _lte) _gte) _and) _or) _xor) _lsh) _rsh) _fst_val) _snd_val) + let _N = λ_snd λ_fst_val ((((Book.Kind.op2) _opr) ((Book.Kind.num) _fst_val)) _snd) + ((((((Book.Kind.if.num) _snd) _P) _Y) _N) _fst_val) + let _N = λ_fst λ_snd ((((Book.Kind.op2) _opr) _fst) _snd) + ((((((Book.Kind.if.num) _fst) _P) _Y) _N) _snd) + +Book.Kind.reduce.ref = λ_maj λ_nam λ_val + let _P = λ_x 0 + let _true = λ_nam λ_val (((Book.Kind.reduce) _maj) _val) + let _false = (Book.Kind.ref) + (((((_maj _P) _true) _false) _nam) _val) + +Book.Kind.reduce.txt = λ_txt + let _P = λ_x (Book.Kind.Term) + let _cons = λ_x λ_xs (((Book.Kind.reduce) (Book.Bool.true)) (((Book.Kind.app) (((Book.Kind.app) (Book.Kind.Book.String.cons)) ((Book.Kind.num) _x))) ((Book.Kind.txt) _xs))) + let _nil = (((Book.Kind.reduce) (Book.Bool.true)) (Book.Kind.Book.String.nil)) + (((_txt _P) _cons) _nil) + +Book.Kind.ref = λ_nam λ_val λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_ref _nam) _val) + +Book.Kind.report = λ_e λ_inferred λ_expected λ_value λ_dep + let _pure = ((Book.Maybe.some) (Book.Kind.Term)) + let _none = ((Book.Maybe.none) (Book.Kind.Term)) + let _P = λ_x 0 + let _true = λ_inferred λ_expected λ_value λ_dep (_pure (Book.Kind.set)) + let _false = λ_inferred λ_expected λ_value λ_dep _none + (((((((_e _P) _true) _false) _inferred) _expected) _value) _dep) + +Book.Kind.set = λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var _set + +Book.Kind.skip = λ_x + let _P = λ_x (Book.Kind.Term) + let _all = (Book.Kind.all) + let _lam = (Book.Kind.lam) + let _app = (Book.Kind.app) + let _ann = λ_val λ_typ ((Book.Kind.skip) _val) + let _slf = (Book.Kind.slf) + let _ins = λ_val ((Book.Kind.skip) _val) + let _ref = (Book.Kind.ref) + let _def = λ_nam λ_val λ_bod ((Book.Kind.skip) (_bod _val)) + let _set = (Book.Kind.set) + let _u60 = (Book.Kind.u60) + let _num = (Book.Kind.num) + let _op2 = (Book.Kind.op2) + let _mat = (Book.Kind.mat) + let _txt = (Book.Kind.txt) + let _hol = (Book.Kind.hol) + let _var = (Book.Kind.var) + (((((((((((((((((_x _P) _all) _lam) _app) _ann) _slf) _ins) _ref) _def) _set) _u60) _num) _op2) _mat) _txt) _hol) _var) + +Book.Kind.slf = λ_nam λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_slf _nam) _bod) + +Book.Kind.txt = λ_lit λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (_txt _lit) + +Book.Kind.u60 = λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var _u60 + +Book.Kind.var = λ_nam λ_idx λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_var _nam) _idx) + +Book.Kind.verify = λ_term λ_type λ_dep + let _bind = (((Book.Maybe.bind) (Book.Kind.Term)) (Book.Kind.Term)) + let _pure = ((Book.Maybe.some) (Book.Kind.Term)) + let _none = ((Book.Maybe.none) (Book.Kind.Term)) + ((_bind (((Book.Kind.infer) _term) _dep)) λ_infer ((((((Book.Kind.report) ((((Book.Kind.equal) _infer) _type) _dep)) _infer) _type) _term) _dep)) + +Book.List.Concatenator.build = λ_T λ_x (_x ((Book.List.nil) _T)) + +Book.List.Concatenator.concat = λ_T λ_xs λ_ys λ_nil (_xs (_ys _nil)) + +Book.List.Concatenator.from_list = λ_T λ_xs + let _P = λ_xs ((Book.List.Concatenator) _T) + let _cons = λ_head λ_tail λ_nil ((((Book.List.cons) _T) _head) ((((Book.List.Concatenator.from_list) _T) _tail) _nil)) + let _nil = λ_nil _nil + (((_xs _P) _cons) _nil) + +Book.List.Concatenator.join = λ_T λ_xs + let _P = λ_xs ((Book.List.Concatenator) _T) + let _cons = λ_head λ_tail ((((Book.List.Concatenator.concat) _T) _head) (((Book.List.Concatenator.join) _T) _tail)) + let _nil = ((Book.List.Concatenator.nil) _T) + (((_xs _P) _cons) _nil) + +Book.List.Concatenator = λ_T 0 + +Book.List.Concatenator.nil = λ_T λ_x _x + +Book.List.Folder.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) (((_tail _P) _cons) _nil)) + +Book.List.Folder = λ_T 0 + +Book.List.Folder.nil = λ_T λ_P λ_cons λ_nil _nil + +Book.List.Map = λ_K λ_V ((Book.List) (((Book.Pair) _K) _V)) +Book.List.Map.get = λ_K λ_V λ_eql λ_key λ_map + let _P = λ_x ((Book.Maybe) _V) + let _cons = λ_head λ_tail + let _P = λ_x ((Book.Maybe) _V) + let _new = λ_head.fst λ_head.snd + let _P = λ_x ((Book.Maybe) _V) + let _true = (((Book.Maybe.some) _V) _head.snd) + let _false = ((((((Book.List.Map.get) _K) _V) _eql) _key) _tail) + (((((_eql _head.fst) _key) _P) _true) _false) + ((_head _P) _new) + let _nil = ((Book.Maybe.none) _V) + (((_map _P) _cons) _nil) +Book.List.Map.set = λ_K λ_V λ_key λ_val λ_map ((((Book.List.cons) (((Book.Pair) _K) _V)) (((((Book.Pair.new) _K) _V) _key) _val)) _map) +Book.List.Map.new = λ_K λ_V ((Book.List.nil) (((Book.Pair) _K) _V)) + +Book.List.begin = λ_A λ_list + let _P = λ_x ((Book.List) _A) + let _cons = λ_x0 λ_xs + let _P = λ_x ((Book.List) _A) + let _cons = λ_x1 λ_xs ((((Book.List.cons) _A) _x0) (((Book.List.begin) _A) ((((Book.List.cons) _A) _x1) _xs))) + let _nil = ((Book.List.nil) _A) + (((_xs _P) _cons) _nil) + let _nil = ((Book.List.nil) _A) + (((_list _P) _cons) _nil) + +Book.List.concat = λ_T λ_xs λ_ys + let _P = λ_xs 0 + let _cons = λ_head λ_tail λ_ys ((((Book.List.cons) _T) _head) ((((Book.List.concat) _T) _tail) _ys)) + let _nil = λ_ys _ys + ((((_xs _P) _cons) _nil) _ys) + +Book.List.cons = λ_T λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) + +Book.List.find = λ_A λ_cond λ_list + let _P = λ_x ((Book.Maybe) _A) + let _cons = λ_head λ_tail + let _found = (_cond _head) + let _P = λ_x ((Book.Maybe) _A) + let _true = (((Book.Maybe.some) _A) _head) + let _false = ((((Book.List.find) _A) _cond) _tail) + (((_found _P) _true) _false) + let _nil = ((Book.Maybe.none) _A) + (((_list _P) _cons) _nil) + +Book.List.fold = λ_T λ_list λ_P λ_cons λ_nil + let _fold_P = λ_xs _P + let _fold_cons = λ_head λ_tail ((_cons _head) ((((((Book.List.fold) _T) _tail) _P) _cons) _nil)) + let _fold_nil = _nil + (((_list _fold_P) _fold_cons) _fold_nil) + +Book.List = λ_T 0 + +Book.List.length = λ_A λ_a + let _P = λ_x (Book.Nat) + let _cons = λ_a.head λ_a.tail ((Book.Nat.succ) (((Book.List.length) _A) _a.tail)) + let _nil = (Book.Nat.zero) + (((_a _P) _cons) _nil) + +Book.List.nil = λ_T λ_P λ_cons λ_nil _nil + + +Book.Maybe.bind = λ_A λ_B λ_a λ_b + let _P = λ_x 0 + let _some = λ_a.value λ_b (_b _a.value) + let _none = λ_b ((Book.Maybe.none) _B) + ((((_a _P) _some) _none) _b) + +Book.Maybe = λ_T 0 + +Book.Maybe.monad = ((((Book.Monad.new) (Book.Maybe)) (Book.Maybe.bind)) (Book.Maybe.pure)) + +Book.Maybe.none = λ_T λ_P λ_some λ_none _none + +Book.Maybe.pure = (Book.Maybe.some) + +Book.Maybe.some = λ_T λ_value λ_P λ_some λ_none (_some _value) + +Book.Monad = λ_M 0 +Book.Monad.new = λ_M λ_bind λ_pure λ_P λ_new ((_new _bind) _pure) + +Book.Nat.double = λ_n (((_n λ_x (Book.Nat)) λ_pred ((Book.Nat.succ) ((Book.Nat.succ) ((Book.Nat.double) _pred)))) (Book.Nat.zero)) + +Book.Nat.equal = λ_a λ_b + let _P = λ_x 0 + let _succ = λ_a.pred λ_b + let _P = λ_x 0 + let _succ = λ_b.pred λ_a.pred (((Book.Nat.equal) _a.pred) _b.pred) + let _zero = λ_a.pred (Book.Bool.false) + ((((_b _P) _succ) _zero) _a.pred) + let _zero = λ_b + let _P = λ_x (Book.Bool) + let _succ = λ_b.pred (Book.Bool.false) + let _zero = (Book.Bool.true) + (((_b _P) _succ) _zero) + ((((_a _P) _succ) _zero) _b) + +Book.Nat.half = λ_n (((_n λ_x (Book.Nat)) λ_n (((_n λ_x (Book.Nat)) λ_n ((Book.Nat.succ) ((Book.Nat.half) _n))) (Book.Nat.zero))) (Book.Nat.zero)) + +Book.Nat = 0 + +Book.Nat.lemma.bft = λ_n (((_n λ_x ((((Book.Equal) (Book.Nat)) ((Book.Nat.half) ((Book.Nat.double) _x))) _x)) λ_n (((((((Book.Equal.apply) (Book.Nat)) (Book.Nat)) (Book.Nat.succ)) ((Book.Nat.half) ((Book.Nat.double) _n))) _n) ((Book.Nat.lemma.bft) _n))) λ_P λ_a _a) + +Book.Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n) + +Book.Nat.zero = λ_P λ_succ λ_zero _zero + +Book.Pair.get = λ_A λ_B λ_p λ_P λ_f ((_p λ_x _P) _f) + +Book.Pair = λ_A λ_B 0 + +Book.Pair.new = λ_A λ_B λ_a λ_b λ_P λ_new ((_new _a) _b) + +Book.Parser.Guard.get = λ_A (((Book.Pair.get) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A)) + +Book.Parser.Guard = λ_A (((Book.Pair) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A)) + +Book.Parser.Guard.new = λ_A (((Book.Pair.new) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A)) + +Book.Parser.Guard.pass = λ_A λ_then ((((Book.Parser.Guard.new) _A) (((Book.Parser.pure) (Book.Bool)) (Book.Bool.true))) _then) + +Book.Parser.Guard.text = λ_A λ_text λ_then ((((Book.Parser.Guard.new) _A) (((Book.Parser.skip) (Book.Bool)) ((Book.Parser.test) _text))) _then) + +Book.Parser.Result.done = λ_T λ_code λ_value λ_P λ_done λ_fail ((_done _code) _value) + +Book.Parser.Result.fail = λ_T λ_error λ_P λ_done λ_fail (_fail _error) + +Book.Parser.Result = λ_T 0 + +Book.Parser.bind = λ_A λ_B λ_a λ_b λ_code + let _P = λ_x 0 + let _done = λ_a.code λ_a.value λ_b ((_b _a.value) _a.code) + let _fail = λ_a.error λ_b (((Book.Parser.Result.fail) _B) _a.error) + (((((_a _code) _P) _done) _fail) _b) + +Book.Parser.char = λ_code + let _P = λ_x ((Book.Parser.Result) (Book.Char)) + let _cons = λ_head λ_tail + let _P = λ_x ((Book.Parser.Result) (Book.Char)) + let _true = ((((Book.Parser.Result.done) (Book.Char)) _tail) _head) + let _false = ((((Book.Parser.Result.done) (Book.Char)) _tail) _head) + (((((Book.Char.is_slash) _head) _P) _true) _false) + let _nil = (((Book.Parser.Result.fail) (Book.Char)) (Str "eof")) + (((_code _P) _cons) _nil) + +Book.Parser.decimal = ((Book.Parser.pick_while) (Book.Char.is_decimal)) + +Book.Parser.fail = λ_T λ_error λ_code (((Book.Parser.Result.fail) _T) _error) + +Book.Parser.is_eof = λ_code + let _P = λ_x ((Book.Parser.Result) (Book.Bool)) + let _cons = λ_code.head λ_code.tail ((((Book.Parser.Result.done) (Book.Bool)) (((Book.String.cons) _code.head) _code.tail)) (Book.Bool.false)) + let _nil = ((((Book.Parser.Result.done) (Book.Bool)) (Book.String.nil)) (Book.Bool.true)) + (((((Book.String.skip) _code) _P) _cons) _nil) + +Book.Parser = λ_A 0 + +Book.Parser.map = λ_A λ_B λ_f λ_p λ_code + let _P = λ_x ((Book.Parser.Result) _B) + let _done = λ_code λ_value ((((Book.Parser.Result.done) _B) _code) (_f _value)) + let _fail = λ_error (((Book.Parser.Result.fail) _B) _error) + ((((_p _code) _P) _done) _fail) + +Book.Parser.name = ((Book.Parser.pick_while) (Book.Char.is_name)) + +Book.Parser.oper = ((Book.Parser.pick_while) (Book.Char.is_oper)) + +Book.Parser.pick = λ_code + let _P = λ_x ((Book.Parser.Result) (Book.Char)) + let _cons = λ_head λ_tail ((((Book.Parser.Result.done) (Book.Char)) _tail) _head) + let _nil = (((Book.Parser.Result.fail) (Book.Char)) (Str "empty")) + (((_code _P) _cons) _nil) + +Book.Parser.pick_while.go = λ_cond λ_code + let _P = λ_x ((Book.Parser.Result) (Book.String)) + let _cons = λ_head λ_tail + let _P = λ_x 0 + let _true = λ_head λ_tail + let _P = λ_x ((Book.Parser.Result) (Book.String)) + let _done = λ_code λ_value ((((Book.Parser.Result.done) (Book.String)) _code) (((Book.String.cons) _head) _value)) + let _fail = λ_error (((Book.Parser.Result.fail) (Book.String)) _error) + ((((((Book.Parser.pick_while.go) _cond) _tail) _P) _done) _fail) + let _false = λ_head λ_tail ((((Book.Parser.Result.done) (Book.String)) (((Book.String.cons) _head) _tail)) (Book.String.nil)) + ((((((_cond _head) _P) _true) _false) _head) _tail) + let _nil = ((((Book.Parser.Result.done) (Book.String)) (Book.String.nil)) (Book.String.nil)) + (((_code _P) _cons) _nil) + +Book.Parser.pick_while = λ_cond λ_code (((Book.Parser.pick_while.go) _cond) _code) + +Book.Parser.pure = λ_A λ_value λ_code ((((Book.Parser.Result.done) _A) _code) _value) + +Book.Parser.repeat = λ_n λ_A λ_p + let _P = λ_x ((Book.Parser) ((Book.List) _A)) + let _succ = λ_n.pred (((((Book.Parser.bind) _A) ((Book.List) _A)) _p) λ_head (((((Book.Parser.bind) ((Book.List) _A)) ((Book.List) _A)) ((((Book.Parser.repeat) _n.pred) _A) _p)) λ_tail (((Book.Parser.pure) ((Book.List) _A)) ((((Book.List.cons) _A) _head) _tail)))) + let _zero = (((Book.Parser.pure) ((Book.List) _A)) ((Book.List.nil) _A)) + (((_n _P) _succ) _zero) + +Book.Parser.skip = λ_A λ_parser λ_code (_parser ((Book.String.skip) _code)) + +Book.Parser.take = λ_n ((((Book.Parser.repeat) _n) (Book.Char)) (Book.Parser.pick)) + +Book.Parser.test = λ_test λ_code + let _P = λ_x 0 + let _cons = λ_test.head λ_test.tail λ_code + let _P = λ_x ((Book.Parser.Result) (Book.Bool)) + let _cons = λ_code.head λ_code.tail + let _P = λ_x 0 + let _true = λ_code.head λ_code.tail + let _P = λ_x ((Book.Parser.Result) (Book.Bool)) + let _done = λ_code λ_value ((((Book.Parser.Result.done) (Book.Bool)) (((Book.String.cons) _code.head) _code)) _value) + let _fail = λ_error (((Book.Parser.Result.fail) (Book.Bool)) _error) + ((((((Book.Parser.test) _test.tail) _code.tail) _P) _done) _fail) + let _false = λ_code.head λ_code.tail ((((Book.Parser.Result.done) (Book.Bool)) (((Book.String.cons) _code.head) _code.tail)) (Book.Bool.false)) + ((((((((Book.Char.equal) _test.head) _code.head) _P) _true) _false) _code.head) _code.tail) + let _nil = ((((Book.Parser.Result.done) (Book.Bool)) (Book.String.nil)) (Book.Bool.false)) + (((_code _P) _cons) _nil) + let _nil = λ_code ((((Book.Parser.Result.done) (Book.Bool)) _code) (Book.Bool.true)) + ((((_test _P) _cons) _nil) _code) + +Book.Parser.text = λ_text (((Book.Parser.skip) (Book.Unit)) (((((Book.Parser.bind) (Book.Bool)) (Book.Unit)) ((Book.Parser.test) _text)) λ_success (((((Book.Bool.if) _success) ((Book.Parser) (Book.Unit))) (((((Book.Parser.bind) (Book.String)) (Book.Unit)) ((Book.Parser.take) ((Book.String.length) _text))) λ_x (((Book.Parser.pure) (Book.Unit)) (Book.Unit.one)))) (((Book.Parser.fail) (Book.Unit)) (Str "error"))))) + +Book.Parser.until.go = λ_A λ_until λ_parse λ_terms λ_code + let _P = λ_x ((Book.Parser.Result) ((Book.List.Concatenator) _A)) + let _done = λ_code λ_stop + let _P = λ_x 0 + let _true = λ_code ((((Book.Parser.Result.done) ((Book.List.Concatenator) _A)) _code) _terms) + let _false = λ_code + let _P = λ_x ((Book.Parser.Result) ((Book.List.Concatenator) _A)) + let _done = λ_code λ_value ((((((Book.Parser.until.go) _A) _until) _parse) λ_x (_terms ((((Book.List.cons) _A) _value) _x))) _code) + let _fail = λ_error (((Book.Parser.Result.fail) ((Book.List.Concatenator) _A)) _error) + ((((_parse _code) _P) _done) _fail) + ((((_stop _P) _true) _false) _code) + let _fail = λ_error (((Book.Parser.Result.fail) ((Book.List.Concatenator) _A)) _error) + ((((_until _code) _P) _done) _fail) + +Book.Parser.until = λ_A λ_until λ_parse (((((Book.Parser.map) ((Book.List.Concatenator) _A)) ((Book.List) _A)) ((Book.List.Concatenator.build) _A)) (((((Book.Parser.until.go) _A) _until) _parse) λ_x _x)) + +Book.Parser.variant = λ_A λ_variants + let _P = λ_x ((Book.Parser) _A) + let _cons = λ_variant λ_others ((((((Book.Pair.get) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A)) _variant) ((Book.Parser) _A)) λ_guard λ_parser (((((Book.Parser.bind) (Book.Bool)) _A) _guard) λ_success (((((Book.Bool.if) _success) ((Book.Parser) _A)) _parser) (((Book.Parser.variant) _A) _others)))) + let _nil = (((Book.Parser.fail) _A) (Str "error")) + (((_variants _P) _cons) _nil) + +Book.QBool.true = λ_P λ_S λ_p ((_p 0) λ_x _x) +Book.QBool.false = λ_P λ_S λ_p ((_p 1) λ_x _x) +Book.QBool = 0 +Book.QBool.match = λ_a λ_P λ_t λ_f (((_a _P) λ_x (_P _a)) λ_tag (U60.match _tag λ_x (_x _t) λ_tag_1(λ_x ((U60.match _tag_1 λ_x (_x _f) λ_tag_1_1(λ_x (_x λ_e (((Book.Empty.absurd) _e) 0)))) _x)))) + +Book.QBool2.true = λ_P λ_new (_new 0) +Book.QBool2.false = λ_P λ_new (_new 1) +Book.QBool2.bad = λ_P λ_new ((_new 2) 0) +Book.QBool2 = 0 +Book.QBool2.match = λ_a λ_P λ_t λ_f ((_a _P) λ_tag (U60.match _tag _t λ_tag_1((U60.match _tag_1 _f λ_tag_1_1(λ_e (_e λ_x 0)))))) + +Book.QUnit.one = λ_P λ_SP λ_new ((_new 0) λ_one _one) +Book.QUnit = 0 + +Book.Sigma = λ_A λ_B 0 + +Book.Sigma.new = λ_A λ_B λ_a λ_b λ_P λ_new ((_new _a) _b) + +Book.String.Concatenator.build = ((Book.List.Concatenator.build) (Book.Char)) + +Book.String.Concatenator.concat = ((Book.List.Concatenator.concat) (Book.Char)) + +Book.String.Concatenator.from_string = ((Book.List.Concatenator.from_list) (Book.Char)) + +Book.String.Concatenator.join = ((Book.List.Concatenator.join) (Book.Char)) + +Book.String.Concatenator = ((Book.List.Concatenator) (Book.Char)) + +Book.String.Map = ((Book.List.Map) (Book.String)) +Book.String.Map.get = λ_A λ_key λ_map ((((((Book.List.Map.get) (Book.String)) _A) (Book.String.equal)) _key) _map) +Book.String.Map.set = λ_A λ_key λ_val λ_map ((((((Book.List.Map.set) (Book.String)) _A) _key) _val) _map) +Book.String.Map.new = λ_V (((Book.List.Map.new) (Book.String)) _V) + +Book.String.begin = λ_str (((Book.List.begin) (Book.Char)) _str) + +Book.String.concat = ((Book.List.concat) (Book.Char)) + +Book.String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail) + +Book.String.equal = λ_a λ_b + let _P = λ_x 0 + let _cons = λ_a.head λ_a.tail λ_b + let _P = λ_x 0 + let _cons = λ_b.head λ_b.tail λ_a.head λ_a.tail (((Book.Bool.and) (((Book.U60.equal) _a.head) _b.head)) (((Book.String.equal) _a.tail) _b.tail)) + let _nil = λ_a.head λ_a.tail (Book.Bool.false) + (((((_b _P) _cons) _nil) _a.head) _a.tail) + let _nil = λ_b + let _P = λ_x (Book.Bool) + let _cons = λ_b.head λ_b.tail (Book.Bool.false) + let _nil = (Book.Bool.true) + (((_b _P) _cons) _nil) + ((((_a _P) _cons) _nil) _b) + +Book.String.indent = λ_tab + let _P = λ_x (Book.String) + let _succ = λ_tab.pred (((Book.String.cons) 32) (((Book.String.cons) 32) ((Book.String.indent) _tab.pred))) + let _zero = (Book.String.nil) + (((_tab _P) _succ) _zero) + +Book.String = ((Book.List) (Book.Char)) + +Book.String.length = λ_a (((Book.List.length) (Book.Char)) _a) + +Book.String.newline = (((Book.String.cons) 10) (Book.String.nil)) + +Book.String.nil = λ_P λ_cons λ_nil _nil + +Book.String.quote = (((Book.String.cons) 34) (Book.String.nil)) + +Book.String.skip = λ_str + let _P = λ_x (Book.String) + let _cons = λ_c0 λ_cs + let _P = λ_x 0 + let _true = λ_c0 λ_cs ((Book.String.skip) _cs) + let _false = λ_c0 λ_cs + let _P = λ_x 0 + let _true = λ_c0 λ_cs + let _P = λ_x 0 + let _cons = λ_c1 λ_cs λ_c0 + let _P = λ_x 0 + let _true = λ_c0 λ_c1 λ_cs ((Book.String.skip.comment) _cs) + let _false = λ_c0 λ_c1 λ_cs (((Book.String.cons) _c0) (((Book.String.cons) _c1) _cs)) + ((((((((Book.Char.is_slash) _c1) _P) _true) _false) _c0) _c1) _cs) + let _nil = λ_c0 (((Book.String.cons) _c0) (Book.String.nil)) + ((((_cs _P) _cons) _nil) _c0) + let _false = λ_c0 λ_cs (((Book.String.cons) _c0) _cs) + (((((((Book.Char.is_slash) _c0) _P) _true) _false) _c0) _cs) + (((((((Book.Char.is_blank) _c0) _P) _true) _false) _c0) _cs) + let _nil = (Book.String.nil) + (((_str _P) _cons) _nil) +Book.String.skip.comment = λ_str + let _P = λ_x (Book.String) + let _cons = λ_c0 λ_cs + let _P = λ_x 0 + let _true = λ_c0 λ_cs ((Book.String.skip) _cs) + let _false = λ_c0 λ_cs ((Book.String.skip.comment) _cs) + (((((((Book.Char.is_newline) _c0) _P) _true) _false) _c0) _cs) + let _nil = (Book.String.nil) + (((_str _P) _cons) _nil) + +Book.String.unpar = λ_fst λ_lst λ_str + let _P = λ_x (Book.String) + let _cons = λ_head λ_tail + let _P = λ_x 0 + let _true = λ_head λ_tail ((Book.String.begin) _tail) + let _false = λ_head λ_tail (((Book.String.cons) _head) _tail) + ((((((((Book.Char.equal) _head) _fst) _P) _true) _false) _head) _tail) + let _nil = (Book.String.nil) + (((_str _P) _cons) _nil) + +Book.U60.Map = ((Book.List.Map) 0) +Book.U60.Map.get = λ_A λ_key λ_map ((((((Book.List.Map.get) 0) _A) (Book.U60.equal)) _key) _map) +Book.U60.Map.set = λ_A λ_key λ_val λ_map ((((((Book.List.Map.set) 0) _A) _key) _val) _map) +Book.U60.Map.new = λ_V (((Book.List.Map.new) 0) _V) + +Book.U60.equal = λ_a λ_b (U60.match (== _a _b) (Book.Bool.false) λ_x_1((Book.Bool.true))) + +Book.U60.from_nat = λ_n + let _P = λ_x 0 + let _succ = λ_n.pred (+ 1 ((Book.U60.from_nat) _n.pred)) + let _zero = 0 + (((_n _P) _succ) _zero) + +Book.U60.if = λ_x λ_P λ_t λ_f (U60.match _x _t λ_x_1(_f)) + +Book.U60.match = λ_x λ_P λ_s λ_z (U60.match _x _z λ_self_1((_s _self_1))) + +Book.U60.name.go = λ_n (U60.match _n λ_nil _nil λ_n_1(λ_nil (((Book.String.cons) (+ 97 (% _n_1 26))) (((Book.U60.name.go) (/ _n_1 26)) _nil)))) + +Book.U60.name = λ_n ((Book.String.Concatenator.build) ((Book.U60.name.go) (+ _n 1))) + +Book.U60.parser.decimal = (((((Book.Parser.bind) (Book.String)) 0) (Book.Parser.decimal)) λ_chars (((Book.Parser.pure) 0) (((((((Book.List.fold) (Book.Char)) _chars) 0) λ_h λ_t λ_r (_t (+ (- _h 48) (* _r 10)))) λ_r _r) 0))) + +Book.U60.show.go = λ_n (U60.match (< _n 10) λ_nil (((Book.U60.show.go) (/ _n 10)) (((Book.String.cons) (+ 48 (% _n 10))) _nil)) λ_x_1(λ_nil (((Book.String.cons) (+ 48 _n)) _nil))) + +Book.U60.show = λ_n ((Book.String.Concatenator.build) ((Book.U60.show.go) _n)) + +Book.U60.to_bool = λ_x (U60.match _x (Book.Bool.false) λ_x_1((Book.Bool.true))) + +Book.Unit = 0 + +Book.Unit.match = λ_x λ_P λ_o ((_x _P) _o) + +Book.Unit.one = λ_P λ_one _one + +Book.test0 = λ_A λ_B λ_aa λ_ab λ_ba λ_bb λ_a λ_b (_ba (_ab (_aa (_aa _a)))) + +Book.test1 = λ_x (+ 50 12) + +Book._EXP = ((((Book.Kind.all) (Str "n")) (Book._Nat)) λ_n ((((Book.Kind.all) (Str "m")) (Book._Nat)) λ_m (Book._Nat))) +Book._exp = (((Book.Kind.lam) (Str "n")) λ_n (((Book.Kind.lam) (Str "m")) λ_m (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.app) (((Book.Kind.app) _m) ((((Book.Kind.all) (Str "x")) _P) λ_x _P))) (((Book.Kind.app) _n) _P))))) +Book._C2 = (Book._Nat) +Book._c2 = (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.lam) (Str "s")) λ_s (((Book.Kind.lam) (Str "z")) λ_z (((Book.Kind.app) _s) (((Book.Kind.app) _s) _z))))) +Book.test10 = + let _term = (((Book.Kind.app) (((Book.Kind.app) (Book._exp)) (Book._c2))) (Book._c2)) + (((Book.Kind.Term.show) ((((Book.Kind.normal) (Book.Bool.true)) _term) (Book.Nat.zero))) (Book.Nat.zero)) + +Book.test2 = + let _xs = ((((Book.List.cons) 0) 0) ((((Book.List.cons) 0) 1) ((((Book.List.cons) 0) 2) ((Book.List.nil) 0)))) + let _ys = ((((Book.List.cons) 0) 3) ((((Book.List.cons) 0) 4) ((((Book.List.cons) 0) 5) ((Book.List.nil) 0)))) + ((((Book.List.concat) 0) _xs) _ys) + +Book.test3 = + let _a = 42 + _a + +Book.test4 = ((((Str "abc") λ_x (Book.String)) λ_h λ_t _t) (Book.String.nil)) + +Book.test5 = λ_b (((_b 0) 0) 0) + +Book.test6 = ((Book.Nat.succ) ((Book.Nat.succ) ((Book.Nat.succ) (Book.Nat.zero)))) + +Book.test8 = λ_a ((((Book.U60.if) _a) 0) (Str "test")) + +Book.test9 = ((((Book.String.unpar) 40) 41) (Str "((foo))")) + + +Main = (Str.view ((Book.Kind.Book.to_hvm) ((Book.Kind.Book.parse) (Str "F = λf λx (f (f x))")))) + + + + + + + diff --git a/bootstrap.js b/bootstrap.js new file mode 100644 index 00000000..6865ee87 --- /dev/null +++ b/bootstrap.js @@ -0,0 +1,38 @@ +// Bootstrap by compiling ALL book/ functions to a single HVM1 file. + +const fs = require('fs'); +const { execSync } = require('child_process'); +const path = require('path'); + +const bookDir = './book'; +const outputFilePath = './bootstrap.hvm1'; +let outputs = []; + +fs.readdirSync(bookDir).forEach(file => { + if (path.extname(file) === '.kind2') { + try { + const filePath = path.join(bookDir, file); + const fileContent = fs.readFileSync(filePath, 'utf8'); + const compileString = `_compile : String = (Kind.Book.to_hvm (Kind.Book.parse \`${fileContent}\`))`; + const compileFilePath = path.join(bookDir, '_compile.kind2'); + fs.writeFileSync(compileFilePath, compileString); + console.log("COMPILING", filePath); + const command = `kind2 run _compile`; + const result = execSync(command, { cwd: bookDir }).toString().trim().slice(1,-1); + console.log(result); + outputs.push(result); + } catch (e) { + console.log(e); + } + } +}); + +// Loads prelude +var prelude = fs.readFileSync("./book/Kind.Book.to_hvm.prelude", "utf8"); +const lines = prelude.split("\n"); +lines.shift(); +lines.pop(); +var prelude = lines.join("\n"); + +const finalOutput = prelude + "\n" + outputs.join('\n'); +fs.writeFileSync(outputFilePath, finalOutput); diff --git a/kind2.hvm1 b/kind2.hvm1 index 05ffb8b3..dcc15182 100644 --- a/kind2.hvm1 +++ b/kind2.hvm1 @@ -186,9 +186,9 @@ (Comparer rec (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx) (Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep) (Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep) -(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam) (Comparer rec (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1) (Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1) +(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam) (Comparer rec U60 U60 dep) = 1 (Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val) (Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst b.fst dep) (rec a.snd b.snd dep)) @@ -358,25 +358,37 @@ // Compilation // ----------- +(Str.view str) = (str 0 λheadλtail(String.cons head (Str.view tail)) String.nil) + +(Str.make (String.cons x xs)) = λP λcons λnil (cons x (Str.make xs)) +(Str.make String.nil) = λP λcons λnil nil + +Compile.primitives = [ + (Pair "HVM.log" λA λB λmsg λret (HVM.log msg ret)) + (Pair "HVM.print" λA λmsg λret (HVM.print (Str.view msg) ret)) + (Pair "HVM.save" λA λname λdata λret (HVM.save (Str.view name) (Str.view data) ret)) + (Pair "HVM.load" λA λname λret (HVM.load (Str.view name) λdata (ret (Str.make data)))) +] + (Compile (All nam inp bod)) = 0 (Compile (Lam nam bod)) = λx(Compile (bod (Var "" x))) (Compile (App fun arg)) = ((Compile fun) (Compile arg)) (Compile (Ann val typ)) = (Compile val) (Compile (Slf nam bod)) = 0 (Compile (Ins val)) = (Compile val) -(Compile (Ref nam val)) = (Compile val) +(Compile (Ref nam val)) = (Compile.ref Compile.primitives nam val) (Compile (Let nam val bod)) = (Compile (bod val)) (Compile Set) = 0 (Compile U60) = 0 (Compile (Num val)) = val (Compile (Op2 opr fst snd)) = (Compile.op2 opr (Compile fst) (Compile snd)) (Compile (Mat nam x z s p)) = (Compile.mat (Compile x) (Compile z) λx(Compile (s (Var "" x)))) -(Compile (Txt txt)) = (Compile (Compile.txt txt)) +(Compile (Txt txt)) = (Str.make txt) (Compile (Hol nam ctx)) = 0 (Compile (Var nam val)) = val -(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs)) -(Compile.txt String.nil) = Book.String.nil +//(Compile.txt (String.cons x xs)) = (App (App Book.String.cons (Num x)) (Compile.txt xs)) +//(Compile.txt String.nil) = Book.String.nil (Compile.op2 ADD fst snd) = (+ fst snd) (Compile.op2 SUB fst snd) = (- fst snd) @@ -398,16 +410,15 @@ (Compile.mat 0 z s) = z (Compile.mat n z s) = (s (- n 1)) +(Compile.ref (List.cons (Pair prim_name prim_func) prims) nam val) = (If (Same prim_name nam) prim_func (Compile.ref prims nam val)) +(Compile.ref List.nil nam val) = (Compile val) + // API // --- -(Read str) = (str 0 λheadλtail(String.cons head (Read tail)) String.nil) - (Normalizer (Ref nam val)) = (Normalizer val) (Normalizer (Ann val typ)) = (Normalizer val) -(Normalizer val) = (Read (Compile val)) // compiles to native and reads as string -//(Normalizer val) = ((Compile val)) // compiles to native and show it -//(Normalizer val) = (Normal 1 val 1) // uses the normalizer function +(Normalizer val) = (Compile val) (Checker (Ref nam val)) = (Checker val) (Checker (Ann val typ)) = (Checker.report (Check val typ 0)) diff --git a/kind2.ts b/kind2.ts new file mode 100644 index 00000000..e8f84219 --- /dev/null +++ b/kind2.ts @@ -0,0 +1,30 @@ +import { execSync } from 'child_process'; +import * as fs from 'fs'; + +export function run(expr: string): string { + var command = `hvm1 run -t 1 -c -f bootstrap.hvm1 '${expr}'`; + try { + const output = execSync(command).toString(); + return output; + } catch (error) { + throw error; + } +} + +export function str(result: string): string { + return result.slice(1,-1).trim(); +} + +export function load(name: string): string { + return fs.readFileSync("./book/"+name+".kind2", "utf8"); +} + +export function get_refs(code: string): string { + return run(`(Strs.view ((Book.Kind.Book.get_refs) ((Book.Kind.Book.parse) (Str \`${code}\`))))`).trim(); +} + +export function to_hvm(code: string): string { + return str(run(`(Str.view ((Book.Kind.Book.to_hvm) ((Book.Kind.Book.parse) (Str \`${code}\`))))`).trim()); +} + +console.log(get_refs(`plus2 = λx (Nat.succ (Nat.succ x))`));