diff --git a/book/Kind.Binder.kind2 b/book/Kind.Binder.kind2 new file mode 100644 index 00000000..42b3400e --- /dev/null +++ b/book/Kind.Binder.kind2 @@ -0,0 +1,3 @@ +Kind.Binder +: * += (Pair String Kind.Term) \ No newline at end of file diff --git a/book/Kind.Binder.new.kind2 b/book/Kind.Binder.new.kind2 new file mode 100644 index 00000000..cea3b955 --- /dev/null +++ b/book/Kind.Binder.new.kind2 @@ -0,0 +1,5 @@ +Kind.Binder.new +: ∀(nam: String) ∀(typ: Kind.Term) + Kind.Binder += λnam λtyp + (Pair.new String Kind.Term nam typ) \ No newline at end of file diff --git a/book/Kind.Book.String.cons.kind2 b/book/Kind.Book.String.cons.kind2 new file mode 100644 index 00000000..6267c687 --- /dev/null +++ b/book/Kind.Book.String.cons.kind2 @@ -0,0 +1,3 @@ +Kind.Book.String.cons +: Kind.Term += (Kind.hol "TODO" (List.nil Kind.Term)) \ No newline at end of file diff --git a/book/Kind.Book.String.kind2 b/book/Kind.Book.String.kind2 new file mode 100644 index 00000000..31793b29 --- /dev/null +++ b/book/Kind.Book.String.kind2 @@ -0,0 +1,3 @@ +Kind.Book.String +: Kind.Term += (Kind.hol "TODO" (List.nil Kind.Term)) \ No newline at end of file diff --git a/book/Kind.Book.String.nil.kind2 b/book/Kind.Book.String.nil.kind2 new file mode 100644 index 00000000..1997b9ae --- /dev/null +++ b/book/Kind.Book.String.nil.kind2 @@ -0,0 +1,3 @@ +Kind.Book.String.nil +: Kind.Term += (Kind.hol "TODO" (List.nil Kind.Term)) \ No newline at end of file diff --git a/book/Kind.Book.kind2 b/book/Kind.Book.kind2 new file mode 100644 index 00000000..eaf01742 --- /dev/null +++ b/book/Kind.Book.kind2 @@ -0,0 +1,3 @@ +Kind.Book +: * += (String.Map Kind.Term) \ No newline at end of file diff --git a/book/Kind.Book.parse.kind2 b/book/Kind.Book.parse.kind2 new file mode 100644 index 00000000..65a99147 --- /dev/null +++ b/book/Kind.Book.parse.kind2 @@ -0,0 +1,8 @@ +Kind.Book.parse +: ∀(code: String) + Kind.Book += λcode + 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 diff --git a/book/Kind.Book.parser.kind2 b/book/Kind.Book.parser.kind2 new file mode 100644 index 00000000..2f92093d --- /dev/null +++ b/book/Kind.Book.parser.kind2 @@ -0,0 +1,28 @@ +Kind.Book.parser +: (Parser Kind.Book) += (Parser.bind Bool Kind.Book Parser.is_eof λis_eof + let P = λx(Parser Kind.Book) + // If EOF, return an empty book + let true = + (Parser.pure Kind.Book (String.Map.new Kind.Term)) + // Otherwise, parse a definition + let false = + (Parser.bind String Kind.Book Parser.name λnam + (Parser.bind Bool Kind.Book (Parser.skip Bool (Parser.test ":")) λann + let P = λx(Parser Kind.Book) + // If annotated, parses the annotation + let true = + (Parser.bind Unit Kind.Book (Parser.text ":") λ_ + (Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λtyp + (Parser.bind Unit Kind.Book (Parser.text "=") λ_ + (Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λval + (Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook + (Parser.pure Kind.Book (String.Map.set Kind.Term nam (Kind.ann (val (List.nil Kind.Binder)) (typ (List.nil Kind.Binder))) book))))))) + // Otherwise, parses just the value + let false = + (Parser.bind Unit Kind.Book (Parser.text "=") λ_ + (Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λval + (Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook + (Parser.pure Kind.Book (String.Map.set Kind.Term nam (val (List.nil Kind.Binder)) book))))) + (~ann P true false))) + (~is_eof P true false)) \ No newline at end of file diff --git a/book/Kind.Book.show.go.kind2 b/book/Kind.Book.show.go.kind2 new file mode 100644 index 00000000..803309ea --- /dev/null +++ b/book/Kind.Book.show.go.kind2 @@ -0,0 +1,17 @@ +Kind.Book.show.go +: ∀(book: Kind.Book) + String.Concatenator += λbook + let P = λx String.Concatenator + let cons = λhead λtail + let P = λx String.Concatenator + let new = λhead.fst λhead.snd λnil + ((Kind.Text.show.go head.fst) + ((Kind.Text.show.go " = " + ((Kind.Term.show.go head.snd Nat.zero + ((Kind.Text.show.go String.newline + ((Kind.Book.show.go tail + nil))))))))) + (~head P new) + let nil = λnil nil + (~book P cons nil) \ No newline at end of file diff --git a/book/Kind.Book.show.kind2 b/book/Kind.Book.show.kind2 new file mode 100644 index 00000000..245398f4 --- /dev/null +++ b/book/Kind.Book.show.kind2 @@ -0,0 +1,5 @@ +Kind.Book.show +: ∀(book: Kind.Book) + String += λbook + (String.Concatenator.build (Kind.Book.show.go book)) \ No newline at end of file diff --git a/book/Kind.Book.to_hvm.go.kind2 b/book/Kind.Book.to_hvm.go.kind2 new file mode 100644 index 00000000..3f81e28c --- /dev/null +++ b/book/Kind.Book.to_hvm.go.kind2 @@ -0,0 +1,17 @@ +Kind.Book.to_hvm.go +: ∀(book: Kind.Book) + String.Concatenator += λbook + let P = λx String.Concatenator + let cons = λhead λtail + let P = λx String.Concatenator + let new = λhead.fst λhead.snd λnil + ((Kind.Text.show.go head.fst) + ((Kind.Text.show.go " = " + ((Kind.Term.to_hvm.go head.snd 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) \ No newline at end of file diff --git a/book/Kind.Book.to_hvm.kind2 b/book/Kind.Book.to_hvm.kind2 new file mode 100644 index 00000000..f9403a15 --- /dev/null +++ b/book/Kind.Book.to_hvm.kind2 @@ -0,0 +1,5 @@ +Kind.Book.to_hvm +: ∀(book: Kind.Book) + String += λbook + (String.Concatenator.build (Kind.Book.to_hvm.go book)) \ No newline at end of file diff --git a/book/Kind.Oper.add.kind2 b/book/Kind.Oper.add.kind2 new file mode 100644 index 00000000..d54f1303 --- /dev/null +++ b/book/Kind.Oper.add.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.add +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (add) \ No newline at end of file diff --git a/book/Kind.Oper.and.kind2 b/book/Kind.Oper.and.kind2 new file mode 100644 index 00000000..f64899b4 --- /dev/null +++ b/book/Kind.Oper.and.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.and +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (and) \ No newline at end of file diff --git a/book/Kind.Oper.div.kind2 b/book/Kind.Oper.div.kind2 new file mode 100644 index 00000000..231606c4 --- /dev/null +++ b/book/Kind.Oper.div.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.div +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (div) \ No newline at end of file diff --git a/book/Kind.Oper.eq.kind2 b/book/Kind.Oper.eq.kind2 new file mode 100644 index 00000000..d6808535 --- /dev/null +++ b/book/Kind.Oper.eq.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.eq +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (eq) \ No newline at end of file diff --git a/book/Kind.Oper.gt.kind2 b/book/Kind.Oper.gt.kind2 new file mode 100644 index 00000000..007f2d3e --- /dev/null +++ b/book/Kind.Oper.gt.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.gt +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (gt) \ No newline at end of file diff --git a/book/Kind.Oper.gte.kind2 b/book/Kind.Oper.gte.kind2 new file mode 100644 index 00000000..530d9cef --- /dev/null +++ b/book/Kind.Oper.gte.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.gte +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (gte) \ No newline at end of file diff --git a/book/Kind.Oper.kind2 b/book/Kind.Oper.kind2 new file mode 100644 index 00000000..79ec34e6 --- /dev/null +++ b/book/Kind.Oper.kind2 @@ -0,0 +1,21 @@ +Kind.Oper +: * += $self + ∀(P: ∀(x: Kind.Oper) *) + ∀(add: (P Kind.Oper.add)) + ∀(mul: (P Kind.Oper.mul)) + ∀(sub: (P Kind.Oper.sub)) + ∀(div: (P Kind.Oper.div)) + ∀(mod: (P Kind.Oper.mod)) + ∀(eq: (P Kind.Oper.eq)) + ∀(ne: (P Kind.Oper.ne)) + ∀(lt: (P Kind.Oper.lt)) + ∀(gt: (P Kind.Oper.gt)) + ∀(lte: (P Kind.Oper.lte)) + ∀(gte: (P Kind.Oper.gte)) + ∀(and: (P Kind.Oper.and)) + ∀(or: (P Kind.Oper.or)) + ∀(xor: (P Kind.Oper.xor)) + ∀(lsh: (P Kind.Oper.lsh)) + ∀(rsh: (P Kind.Oper.rsh)) + (P self) \ No newline at end of file diff --git a/book/Kind.Oper.lsh.kind2 b/book/Kind.Oper.lsh.kind2 new file mode 100644 index 00000000..74bd04b6 --- /dev/null +++ b/book/Kind.Oper.lsh.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.lsh +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (lsh) \ No newline at end of file diff --git a/book/Kind.Oper.lt.kind2 b/book/Kind.Oper.lt.kind2 new file mode 100644 index 00000000..97db10c2 --- /dev/null +++ b/book/Kind.Oper.lt.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.lt +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (lt) \ No newline at end of file diff --git a/book/Kind.Oper.lte.kind2 b/book/Kind.Oper.lte.kind2 new file mode 100644 index 00000000..3bbdd541 --- /dev/null +++ b/book/Kind.Oper.lte.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.lte +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (lte) \ No newline at end of file diff --git a/book/Kind.Oper.mod.kind2 b/book/Kind.Oper.mod.kind2 new file mode 100644 index 00000000..4163b5cc --- /dev/null +++ b/book/Kind.Oper.mod.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.mod +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (mod) \ No newline at end of file diff --git a/book/Kind.Oper.mul.kind2 b/book/Kind.Oper.mul.kind2 new file mode 100644 index 00000000..d41d83c6 --- /dev/null +++ b/book/Kind.Oper.mul.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.mul +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (mul) \ No newline at end of file diff --git a/book/Kind.Oper.ne.kind2 b/book/Kind.Oper.ne.kind2 new file mode 100644 index 00000000..1b143829 --- /dev/null +++ b/book/Kind.Oper.ne.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.ne +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (ne) \ No newline at end of file diff --git a/book/Kind.Oper.or.kind2 b/book/Kind.Oper.or.kind2 new file mode 100644 index 00000000..2b7d15bc --- /dev/null +++ b/book/Kind.Oper.or.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.or +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (or) \ No newline at end of file diff --git a/book/Kind.Oper.parser.kind2 b/book/Kind.Oper.parser.kind2 new file mode 100644 index 00000000..279dd267 --- /dev/null +++ b/book/Kind.Oper.parser.kind2 @@ -0,0 +1,28 @@ +Kind.Oper.parser +: (Parser Kind.Oper) += let TRY = (List.cons (Parser.Guard Kind.Oper)) + let END = (List.nil (Parser.Guard Kind.Oper)) + let OP2 = + { λsym λoper + (Parser.Guard.text Kind.Oper sym + (Parser.bind Unit Kind.Oper (Parser.text sym) λx + (Parser.pure Kind.Oper oper))) + : ∀(sym: String) ∀(oper: Kind.Oper) (Parser.Guard Kind.Oper)} + (Parser.variant Kind.Oper + (TRY (OP2 "+" Kind.Oper.add) + (TRY (OP2 "*" Kind.Oper.mul) + (TRY (OP2 "-" Kind.Oper.sub) + (TRY (OP2 "/" Kind.Oper.div) + (TRY (OP2 "%" Kind.Oper.mod) + (TRY (OP2 "==" Kind.Oper.eq) + (TRY (OP2 "!=" Kind.Oper.ne) + (TRY (OP2 "<=" Kind.Oper.lte) + (TRY (OP2 ">=" Kind.Oper.gte) + (TRY (OP2 "<<" Kind.Oper.lsh) + (TRY (OP2 ">>" Kind.Oper.rsh) + (TRY (OP2 "<" Kind.Oper.lt) + (TRY (OP2 ">" Kind.Oper.gt) + (TRY (OP2 "&" Kind.Oper.and) + (TRY (OP2 "|" Kind.Oper.or) + (TRY (OP2 "^" Kind.Oper.xor) + END))))))))))))))))) \ No newline at end of file diff --git a/book/Kind.Oper.rsh.kind2 b/book/Kind.Oper.rsh.kind2 new file mode 100644 index 00000000..bedf1bc3 --- /dev/null +++ b/book/Kind.Oper.rsh.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.rsh +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (rsh) \ No newline at end of file diff --git a/book/Kind.Oper.show.go.kind2 b/book/Kind.Oper.show.go.kind2 new file mode 100644 index 00000000..5d7f2983 --- /dev/null +++ b/book/Kind.Oper.show.go.kind2 @@ -0,0 +1,22 @@ +Kind.Oper.show.go +: ∀(oper: Kind.Oper) + String.Concatenator += λoper + let P = λX(String.Concatenator) + let add = (Kind.Text.show.go "+") + let mul = (Kind.Text.show.go "*") + let sub = (Kind.Text.show.go "-") + let div = (Kind.Text.show.go "/") + let mod = (Kind.Text.show.go "%") + let eq = (Kind.Text.show.go "==") + let ne = (Kind.Text.show.go "!=") + let lt = (Kind.Text.show.go "<") + let gt = (Kind.Text.show.go ">") + let lte = (Kind.Text.show.go "<=") + let gte = (Kind.Text.show.go ">=") + let and = (Kind.Text.show.go "&") + let or = (Kind.Text.show.go "|") + let xor = (Kind.Text.show.go "^") + let lsh = (Kind.Text.show.go "<<") + let rsh = (Kind.Text.show.go ">>") + (~oper P add mul sub div mod eq ne lt gt lte gte and or xor lsh rsh) \ No newline at end of file diff --git a/book/Kind.Oper.show.kind2 b/book/Kind.Oper.show.kind2 new file mode 100644 index 00000000..8d068a94 --- /dev/null +++ b/book/Kind.Oper.show.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.show +: ∀(oper: Kind.Oper) + String += λoper (String.Concatenator.build (Kind.Oper.show.go oper)) \ No newline at end of file diff --git a/book/Kind.Oper.sub.kind2 b/book/Kind.Oper.sub.kind2 new file mode 100644 index 00000000..f26ac46c --- /dev/null +++ b/book/Kind.Oper.sub.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.sub +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (sub) \ No newline at end of file diff --git a/book/Kind.Oper.xor.kind2 b/book/Kind.Oper.xor.kind2 new file mode 100644 index 00000000..fd28a153 --- /dev/null +++ b/book/Kind.Oper.xor.kind2 @@ -0,0 +1,4 @@ +Kind.Oper.xor +: Kind.Oper += ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh + (xor) \ No newline at end of file diff --git a/book/Kind.PreTerm.kind2 b/book/Kind.PreTerm.kind2 new file mode 100644 index 00000000..804f7a80 --- /dev/null +++ b/book/Kind.PreTerm.kind2 @@ -0,0 +1,4 @@ +Kind.PreTerm +: * += ∀(ctx: Kind.Scope) + Kind.Term \ No newline at end of file diff --git a/book/Kind.Scope.cons.kind2 b/book/Kind.Scope.cons.kind2 new file mode 100644 index 00000000..fc4ba0b6 --- /dev/null +++ b/book/Kind.Scope.cons.kind2 @@ -0,0 +1,5 @@ +Kind.Scope.cons +: ∀(head: Kind.Binder) + ∀(tail: Kind.Scope) + Kind.Scope += (List.cons Kind.Binder) \ No newline at end of file diff --git a/book/Kind.Scope.extend.kind2 b/book/Kind.Scope.extend.kind2 new file mode 100644 index 00000000..d9184bb4 --- /dev/null +++ b/book/Kind.Scope.extend.kind2 @@ -0,0 +1,7 @@ +Kind.Scope.extend +: ∀(nam: String) + ∀(typ: Kind.Term) + ∀(scp: Kind.Scope) + Kind.Scope += λnam λtyp λscp + (Kind.Scope.cons (Kind.Binder.new nam typ) scp) \ No newline at end of file diff --git a/book/Kind.Scope.find.kind2 b/book/Kind.Scope.find.kind2 new file mode 100644 index 00000000..6ee235fe --- /dev/null +++ b/book/Kind.Scope.find.kind2 @@ -0,0 +1,11 @@ +Kind.Scope.find +: ∀(nam: String) + ∀(scp: Kind.Scope) + Kind.Term += λname λscope + let cond = λbnd (~bnd λx(Bool) λnλt(String.equal name n)) + let found = (List.find Kind.Binder cond scope) + let P = λx(Kind.Term) + let some = λbnd (~bnd λx(Kind.Term) λnλt(t)) + let none = (Kind.ref name Kind.set) // FIXME: handle unbound reference + (~found P some none) \ No newline at end of file diff --git a/book/Kind.Scope.kind2 b/book/Kind.Scope.kind2 new file mode 100644 index 00000000..595f3c57 --- /dev/null +++ b/book/Kind.Scope.kind2 @@ -0,0 +1,3 @@ +Kind.Scope +: * += (List Kind.Binder) \ No newline at end of file diff --git a/book/Kind.Scope.nil.kind2 b/book/Kind.Scope.nil.kind2 new file mode 100644 index 00000000..b637e67a --- /dev/null +++ b/book/Kind.Scope.nil.kind2 @@ -0,0 +1,3 @@ +Kind.Scope.nil +: Kind.Scope += (List.nil Kind.Binder) \ No newline at end of file diff --git a/book/Kind.Term.kind2 b/book/Kind.Term.kind2 new file mode 100644 index 00000000..b65a7c3b --- /dev/null +++ b/book/Kind.Term.kind2 @@ -0,0 +1,21 @@ +Kind.Term +: * += $self + ∀(P: ∀(x: Kind.Term) *) + ∀(all: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.all nam inp bod))) + ∀(lam: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.lam nam bod))) + ∀(app: ∀(fun: Kind.Term) ∀(arg: Kind.Term) (P (Kind.app fun arg))) + ∀(ann: ∀(val: Kind.Term) ∀(typ: Kind.Term) (P (Kind.ann val typ))) + ∀(slf: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.slf nam bod))) + ∀(ins: ∀(val: Kind.Term) (P (Kind.ins val))) + ∀(ref: ∀(nam: String) ∀(val: Kind.Term) (P (Kind.ref nam val))) + ∀(def: ∀(nam: String) ∀(val: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.def nam val bod))) + ∀(set: (P Kind.set)) + ∀(u60: (P Kind.u60)) + ∀(num: ∀(val: #U60) (P (Kind.num val))) + ∀(op2: ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term) (P (Kind.op2 opr fst snd))) + ∀(mat: ∀(nam: String) ∀(x: Kind.Term) ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term)Kind.Term) ∀(p: ∀(x: Kind.Term)Kind.Term) (P (Kind.mat nam x z s p))) + ∀(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 diff --git a/book/Kind.Term.parse.kind2 b/book/Kind.Term.parse.kind2 new file mode 100644 index 00000000..bcbf19fd --- /dev/null +++ b/book/Kind.Term.parse.kind2 @@ -0,0 +1,8 @@ +Kind.Term.parse +: ∀(code: String) + Kind.Term += λcode + let P = λx(Kind.Term) + let done = λcode λterm (term (List.nil Kind.Binder)) + let fail = λerror (Kind.hol "error" (List.nil Kind.Term)) + (~(Kind.Term.parser code) P done fail) \ No newline at end of file diff --git a/book/Kind.Term.parser.all.kind2 b/book/Kind.Term.parser.all.kind2 new file mode 100644 index 00000000..55a0de84 --- /dev/null +++ b/book/Kind.Term.parser.all.kind2 @@ -0,0 +1,12 @@ +Kind.Term.parser.all +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "∀" + (Kind.Term.parser.bind Unit (Parser.text "∀") λ_ + (Kind.Term.parser.bind Unit (Parser.text "(") λ_ + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.bind Unit (Parser.text ":") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λinp + (Kind.Term.parser.bind Unit (Parser.text ")") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod + (Kind.Term.parser.pure λscp + (Kind.all nam (inp scp) λx(bod (Kind.Scope.extend nam x scp)))))))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.ann.kind2 b/book/Kind.Term.parser.ann.kind2 new file mode 100644 index 00000000..747d9538 --- /dev/null +++ b/book/Kind.Term.parser.ann.kind2 @@ -0,0 +1,10 @@ +Kind.Term.parser.ann +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "{" + (Kind.Term.parser.bind Unit (Parser.text "{") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λval + (Kind.Term.parser.bind Unit (Parser.text ":") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λtyp + (Kind.Term.parser.bind Unit (Parser.text "}") λ_ + (Kind.Term.parser.pure λscp + (Kind.ann (val scp) (typ scp))))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.app.kind2 b/book/Kind.Term.parser.app.kind2 new file mode 100644 index 00000000..737ae225 --- /dev/null +++ b/book/Kind.Term.parser.app.kind2 @@ -0,0 +1,12 @@ +Kind.Term.parser.app +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "(" + (Kind.Term.parser.bind Unit (Parser.text "(") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λfun + (Kind.Term.parser.bind (List Kind.PreTerm) (Parser.until Kind.PreTerm (Parser.skip Bool (Parser.test ")")) Kind.Term.parser) λterms + (Kind.Term.parser.bind Unit (Parser.text ")") λ_ + (Kind.Term.parser.pure λscp + (((List.fold Kind.PreTerm terms) ∀(fun:Kind.Term)Kind.Term + λargλrecλfun(rec (Kind.app fun (arg scp))) + λfun(fun)) + (fun scp)))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.bind.kind2 b/book/Kind.Term.parser.bind.kind2 new file mode 100644 index 00000000..38fb00ae --- /dev/null +++ b/book/Kind.Term.parser.bind.kind2 @@ -0,0 +1,6 @@ +Kind.Term.parser.bind +: ∀(A: *) + ∀(a: (Parser A)) + ∀(b: ∀(x: A) (Parser Kind.PreTerm)) + (Parser Kind.PreTerm) += λA (Parser.bind A Kind.PreTerm) diff --git a/book/Kind.Term.parser.chr.kind2 b/book/Kind.Term.parser.chr.kind2 new file mode 100644 index 00000000..0d336ad5 --- /dev/null +++ b/book/Kind.Term.parser.chr.kind2 @@ -0,0 +1,8 @@ +Kind.Term.parser.chr +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "'" + (Kind.Term.parser.bind Unit (Parser.text "'") λ_ + (Kind.Term.parser.bind #U60 Parser.char λchr + (Kind.Term.parser.bind Unit (Parser.text "'") λ_ + (Kind.Term.parser.pure λscp + (Kind.num chr)))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.def.kind2 b/book/Kind.Term.parser.def.kind2 new file mode 100644 index 00000000..c4216e4f --- /dev/null +++ b/book/Kind.Term.parser.def.kind2 @@ -0,0 +1,10 @@ +Kind.Term.parser.def +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "let " + (Kind.Term.parser.bind Unit (Parser.text "let ") λ_ + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.bind Unit (Parser.text "=") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λval + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod + (Kind.Term.parser.pure λscp + (Kind.def nam (val scp) λx(bod (Kind.Scope.extend nam x scp)))))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.hol.kind2 b/book/Kind.Term.parser.hol.kind2 new file mode 100644 index 00000000..309b8324 --- /dev/null +++ b/book/Kind.Term.parser.hol.kind2 @@ -0,0 +1,7 @@ +Kind.Term.parser.hol +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "?" + (Kind.Term.parser.bind Unit (Parser.text "?") λ_ + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.pure λscp + (Kind.hol nam (List.nil Kind.Term)))))) // TODO: build context \ No newline at end of file diff --git a/book/Kind.Term.parser.ins.kind2 b/book/Kind.Term.parser.ins.kind2 new file mode 100644 index 00000000..a775eab8 --- /dev/null +++ b/book/Kind.Term.parser.ins.kind2 @@ -0,0 +1,7 @@ +Kind.Term.parser.ins +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "~" + (Kind.Term.parser.bind Unit (Parser.text "~") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λval + (Kind.Term.parser.pure λscp + (Kind.ins (val scp)))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.kind2 b/book/Kind.Term.parser.kind2 new file mode 100644 index 00000000..e17d69b0 --- /dev/null +++ b/book/Kind.Term.parser.kind2 @@ -0,0 +1,22 @@ +Kind.Term.parser +: (Parser Kind.PreTerm) += let TRY = (List.cons (Parser.Guard Kind.PreTerm)) + let END = (List.nil (Parser.Guard Kind.PreTerm)) + (Parser.variant Kind.PreTerm + (TRY Kind.Term.parser.all + (TRY Kind.Term.parser.lam + (TRY Kind.Term.parser.app + (TRY Kind.Term.parser.ann + (TRY Kind.Term.parser.slf + (TRY Kind.Term.parser.ins + (TRY Kind.Term.parser.set + (TRY Kind.Term.parser.def + (TRY Kind.Term.parser.u60 + (TRY Kind.Term.parser.op2 + (TRY Kind.Term.parser.mat + (TRY Kind.Term.parser.chr + (TRY Kind.Term.parser.str + (TRY Kind.Term.parser.num + (TRY Kind.Term.parser.hol + (TRY Kind.Term.parser.var + END))))))))))))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.lam.kind2 b/book/Kind.Term.parser.lam.kind2 new file mode 100644 index 00000000..b06b7386 --- /dev/null +++ b/book/Kind.Term.parser.lam.kind2 @@ -0,0 +1,8 @@ +Kind.Term.parser.lam +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "λ" + (Kind.Term.parser.bind Unit (Parser.text "λ") λ_ + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod + (Kind.Term.parser.pure λscp + (Kind.lam nam λx(bod (Kind.Scope.extend nam x scp)))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.mat.kind2 b/book/Kind.Term.parser.mat.kind2 new file mode 100644 index 00000000..2ab7aa1b --- /dev/null +++ b/book/Kind.Term.parser.mat.kind2 @@ -0,0 +1,19 @@ +Kind.Term.parser.mat +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "#match " + (Kind.Term.parser.bind Unit (Parser.text "#match ") λ_ + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.bind Unit (Parser.text "=") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λx + (Kind.Term.parser.bind Unit (Parser.text "{") λ_ + (Kind.Term.parser.bind Unit (Parser.text "#0") λ_ + (Kind.Term.parser.bind Unit (Parser.text ":") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λz + (Kind.Term.parser.bind Unit (Parser.text "#+") λ_ + (Kind.Term.parser.bind Unit (Parser.text ":") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λs + (Kind.Term.parser.bind Unit (Parser.text "}") λ_ + (Kind.Term.parser.bind Unit (Parser.text ":") λ_ + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λp + (Kind.Term.parser.pure λscp + (Kind.mat nam (x scp) (z scp) λx(s (Kind.Scope.extend nam x scp)) λx(p (Kind.Scope.extend nam x scp))))))))))))))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.num.kind2 b/book/Kind.Term.parser.num.kind2 new file mode 100644 index 00000000..98da131a --- /dev/null +++ b/book/Kind.Term.parser.num.kind2 @@ -0,0 +1,7 @@ +Kind.Term.parser.num +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "#" + (Kind.Term.parser.bind Unit (Parser.text "#") λ_ + (Kind.Term.parser.bind #U60 U60.parser.decimal λnum + (Kind.Term.parser.pure λscp + (Kind.num num))))) diff --git a/book/Kind.Term.parser.op2.kind2 b/book/Kind.Term.parser.op2.kind2 new file mode 100644 index 00000000..d615f5b2 --- /dev/null +++ b/book/Kind.Term.parser.op2.kind2 @@ -0,0 +1,10 @@ +Kind.Term.parser.op2 +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "#(" + (Kind.Term.parser.bind Unit (Parser.text "#(") λ_ + (Kind.Term.parser.bind Kind.Oper Kind.Oper.parser λopr + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λfst + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λsnd + (Kind.Term.parser.bind Unit (Parser.text ")") λ_ + (Kind.Term.parser.pure λscp + (Kind.op2 opr (fst scp) (snd scp))))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.pure.kind2 b/book/Kind.Term.parser.pure.kind2 new file mode 100644 index 00000000..fd208473 --- /dev/null +++ b/book/Kind.Term.parser.pure.kind2 @@ -0,0 +1,4 @@ +Kind.Term.parser.pure +: ∀(value: Kind.PreTerm) + (Parser Kind.PreTerm) += (Parser.pure Kind.PreTerm) \ No newline at end of file diff --git a/book/Kind.Term.parser.set.kind2 b/book/Kind.Term.parser.set.kind2 new file mode 100644 index 00000000..59560b46 --- /dev/null +++ b/book/Kind.Term.parser.set.kind2 @@ -0,0 +1,6 @@ +Kind.Term.parser.set +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "*" + (Kind.Term.parser.bind Unit (Parser.text "*") λ_ + (Kind.Term.parser.pure λscp + Kind.set))) \ No newline at end of file diff --git a/book/Kind.Term.parser.slf.kind2 b/book/Kind.Term.parser.slf.kind2 new file mode 100644 index 00000000..e6e96f5f --- /dev/null +++ b/book/Kind.Term.parser.slf.kind2 @@ -0,0 +1,8 @@ +Kind.Term.parser.slf +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "$" + (Kind.Term.parser.bind Unit (Parser.text "$") λ_ + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod + (Kind.Term.parser.pure λscp + (Kind.slf nam λx(bod (Kind.Scope.extend nam x scp)))))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.str.kind2 b/book/Kind.Term.parser.str.kind2 new file mode 100644 index 00000000..1003bb4e --- /dev/null +++ b/book/Kind.Term.parser.str.kind2 @@ -0,0 +1,8 @@ +Kind.Term.parser.str +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm String.quote + (Kind.Term.parser.bind Unit (Parser.text String.quote) λ_ + (Kind.Term.parser.bind String (Parser.until Char (Parser.test String.quote) Parser.char) λchars + (Kind.Term.parser.bind Unit (Parser.text String.quote) λ_ + (Kind.Term.parser.pure λscp + (Kind.txt chars)))))) \ No newline at end of file diff --git a/book/Kind.Term.parser.u60.kind2 b/book/Kind.Term.parser.u60.kind2 new file mode 100644 index 00000000..41961f55 --- /dev/null +++ b/book/Kind.Term.parser.u60.kind2 @@ -0,0 +1,6 @@ +Kind.Term.parser.u60 +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.text Kind.PreTerm "#U60" + (Kind.Term.parser.bind Unit (Parser.text "#U60") λ_ + (Kind.Term.parser.pure λscp + Kind.u60))) \ No newline at end of file diff --git a/book/Kind.Term.parser.var.kind2 b/book/Kind.Term.parser.var.kind2 new file mode 100644 index 00000000..4765a42b --- /dev/null +++ b/book/Kind.Term.parser.var.kind2 @@ -0,0 +1,6 @@ +Kind.Term.parser.var +: (Parser.Guard Kind.PreTerm) += (Parser.Guard.pass Kind.PreTerm + (Kind.Term.parser.bind String Parser.name λnam + (Kind.Term.parser.pure λscp + (Kind.Scope.find nam scp)))) \ No newline at end of file diff --git a/book/Kind.Term.show.go.kind2 b/book/Kind.Term.show.go.kind2 new file mode 100644 index 00000000..32361a00 --- /dev/null +++ b/book/Kind.Term.show.go.kind2 @@ -0,0 +1,99 @@ +Kind.Term.show.go +: ∀(term: Kind.Term) + ∀(dep: Nat) + String.Concatenator += λterm λdep + let P = λX(String.Concatenator) + let all = λnam λinp λbod λnil + ((Kind.Text.show.go "∀(") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go ": ") + ((Kind.Term.show.go inp dep) + ((Kind.Text.show.go ") ") + ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil)))))) + let lam = λnam λbod λnil + ((Kind.Text.show.go "λ") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go " ") + ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil)))) + let app = λfun λarg λnil + ((Kind.Text.show.go "(") + ((Kind.Term.show.go fun dep) + ((Kind.Text.show.go " ") + ((Kind.Term.show.go arg dep) + ((Kind.Text.show.go ")") + nil))))) + let ann = λval λtyp λnil + ((Kind.Text.show.go "{") + ((Kind.Term.show.go val dep) + ((Kind.Text.show.go " : ") + ((Kind.Term.show.go typ dep) + ((Kind.Text.show.go "}") + nil))))) + let slf = λnam λbod λnil + ((Kind.Text.show.go "$") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go " ") + ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil)))) + let ins = λval λnil + ((Kind.Text.show.go "~") + ((Kind.Term.show.go val dep) + nil)) + let ref = λnam λval λnil + ((Kind.Text.show.go nam) + nil) + let def = λnam λval λbod λnil + ((Kind.Text.show.go "let ") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go " = ") + ((Kind.Term.show.go val dep) + ((Kind.Text.show.go "; ") + ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil)))))) + let set = λnil + ((Kind.Text.show.go "*") + nil) + let u60 = λnil + ((Kind.Text.show.go "#U60") + nil) + let num = λval λnil + ((Kind.Text.show.go "#") + ((U60.show.go val) + nil)) + let op2 = λopr λfst λsnd λnil + ((Kind.Text.show.go "#(") + ((Kind.Oper.show.go opr) + ((Kind.Text.show.go " ") + ((Kind.Term.show.go fst dep) + ((Kind.Text.show.go " ") + ((Kind.Term.show.go snd dep) + ((Kind.Text.show.go ")") + nil))))))) + let mat = λnam λx λz λs λp λnil + ((Kind.Text.show.go "#match ") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go " = ") + ((Kind.Term.show.go x dep) + ((Kind.Text.show.go " { #0: ") + ((Kind.Term.show.go z dep) + ((Kind.Text.show.go "; #+: ") + ((Kind.Term.show.go (s (Kind.var nam dep)) (Nat.succ dep)) + ((Kind.Text.show.go " }: ") + ((Kind.Term.show.go (p (Kind.var nam dep)) (Nat.succ dep)) + nil)))))))))) + let txt = λtext λnil + ((Kind.Text.show.go String.quote) + ((Kind.Text.show.go text) + ((Kind.Text.show.go String.quote) + nil))) + let hol = λnam λctx λnil + ((Kind.Text.show.go "?") + ((Kind.Text.show.go nam) + nil)) + let var = λnam λidx λnil + ((Kind.Text.show.go nam) + nil) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) \ No newline at end of file diff --git a/book/Kind.Term.show.kind2 b/book/Kind.Term.show.kind2 new file mode 100644 index 00000000..76f86a56 --- /dev/null +++ b/book/Kind.Term.show.kind2 @@ -0,0 +1,6 @@ +Kind.Term.show +: ∀(term: Kind.Term) + ∀(dep: Nat) + String += λterm λdep + (String.Concatenator.build (Kind.Term.show.go term dep)) \ No newline at end of file diff --git a/book/Kind.Term.to_hvm.go.kind2 b/book/Kind.Term.to_hvm.go.kind2 new file mode 100644 index 00000000..ba27fb45 --- /dev/null +++ b/book/Kind.Term.to_hvm.go.kind2 @@ -0,0 +1,73 @@ +Kind.Term.to_hvm.go +: ∀(term: Kind.Term) + ∀(dep: Nat) + String.Concatenator += λterm λdep + let P = λx String.Concatenator + let all = λnam λinp λbod + (Kind.Text.show.go "0") + let lam = λnam λbod λnil + ((Kind.Text.show.go "λ") + ((Kind.Text.show.go (U60.name (U60.from_nat dep))) + ((Kind.Text.show.go " " + ((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil))))) + let app = λfun λarg λnil + ((Kind.Text.show.go "(") + ((Kind.Term.to_hvm.go fun dep) + ((Kind.Text.show.go " ") + ((Kind.Term.to_hvm.go arg dep) + ((Kind.Text.show.go ")") + nil))))) + let ann = λval λtyp + (Kind.Term.to_hvm.go val dep) + let slf = λnam λbod + (Kind.Text.show.go "0") + let ins = λval + (Kind.Term.to_hvm.go val dep) + let ref = λnam λval + (Kind.Text.show.go nam) + let def = λnam λval λbod λnil + ((Kind.Text.show.go "let ") + ((Kind.Text.show.go nam) + ((Kind.Text.show.go " = ") + ((Kind.Term.to_hvm.go val dep) + ((Kind.Text.show.go "; ") + ((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep)) + nil)))))) + let set = + (Kind.Text.show.go "0") + let u60 = + (Kind.Text.show.go "0") + let num = λval + (U60.show.go val) + let op2 = λopr λfst λsnd λnil + ((Kind.Text.show.go "(") + ((Kind.Oper.show.go opr) // TODO: Kind.Oper.to_hvm + ((Kind.Text.show.go " ") + ((Kind.Term.to_hvm.go fst dep) + ((Kind.Text.show.go " ") + ((Kind.Term.to_hvm.go snd dep) + ((Kind.Text.show.go ")") + nil))))))) + let mat = λnam λx λz λs λp λnil + ((Kind.Text.show.go "(U60.match ") + ((Kind.Term.to_hvm.go x dep) + ((Kind.Text.show.go " ") + ((Kind.Term.to_hvm.go z dep) + ((Kind.Text.show.go " ") + ((Kind.Term.to_hvm.go (s (Kind.var (String.concat nam "_1") dep)) (Nat.succ dep)) + ((Kind.Text.show.go " ") + ((Kind.Term.to_hvm.go (p (Kind.var nam dep)) (Nat.succ dep)) + ((Kind.Text.show.go ")") + nil))))))))) + let txt = λtxt λnil + ((Kind.Text.show.go String.quote) + ((Kind.Text.show.go txt) + ((Kind.Text.show.go String.quote) + nil))) + let hol = λnam λctx + (Kind.Text.show.go "0") + let var = λnam λidx + (Kind.Text.show.go (U60.name (U60.from_nat idx))) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) \ No newline at end of file diff --git a/book/Kind.Term.to_hvm.kind2 b/book/Kind.Term.to_hvm.kind2 new file mode 100644 index 00000000..582fe1fd --- /dev/null +++ b/book/Kind.Term.to_hvm.kind2 @@ -0,0 +1,6 @@ +Kind.Term.to_hvm +: ∀(term: Kind.Term) + ∀(dep: Nat) + String += λterm λdep + (String.Concatenator.build (Kind.Term.to_hvm.go term dep)) \ No newline at end of file diff --git a/book/Kind.Text.kind2 b/book/Kind.Text.kind2 new file mode 100644 index 00000000..5a5fcb83 --- /dev/null +++ b/book/Kind.Text.kind2 @@ -0,0 +1,3 @@ +Kind.Text +: * += String \ No newline at end of file diff --git a/book/Kind.Text.show.go.kind2 b/book/Kind.Text.show.go.kind2 new file mode 100644 index 00000000..b02251b0 --- /dev/null +++ b/book/Kind.Text.show.go.kind2 @@ -0,0 +1,4 @@ +Kind.Text.show.go +: ∀(text: Kind.Text) + String.Concatenator += String.Concatenator.from_string \ No newline at end of file diff --git a/book/Kind.all.kind2 b/book/Kind.all.kind2 new file mode 100644 index 00000000..89caee76 --- /dev/null +++ b/book/Kind.all.kind2 @@ -0,0 +1,8 @@ +Kind.all +: ∀(nam: String) + ∀(inp: Kind.Term) + ∀(bod: ∀(x: Kind.Term) Kind.Term) + Kind.Term += λnam λinp λbod + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (all nam inp bod) \ No newline at end of file diff --git a/book/Kind.ann.kind2 b/book/Kind.ann.kind2 new file mode 100644 index 00000000..61003c96 --- /dev/null +++ b/book/Kind.ann.kind2 @@ -0,0 +1,7 @@ +Kind.ann +: ∀(val: Kind.Term) + ∀(typ: Kind.Term) + Kind.Term += λval λtyp + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (ann val typ) \ No newline at end of file diff --git a/book/Kind.app.kind2 b/book/Kind.app.kind2 new file mode 100644 index 00000000..733a0adc --- /dev/null +++ b/book/Kind.app.kind2 @@ -0,0 +1,7 @@ +Kind.app +: ∀(fun: Kind.Term) + ∀(arg: Kind.Term) + Kind.Term += λfun λarg + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (app fun arg) \ No newline at end of file diff --git a/book/Kind.check.kind2 b/book/Kind.check.kind2 new file mode 100644 index 00000000..01902496 --- /dev/null +++ b/book/Kind.check.kind2 @@ -0,0 +1,58 @@ +Kind.check +: ∀(term: Kind.Term) + ∀(type: Kind.Term) + ∀(dep: Nat) + (Maybe Kind.Term) += λterm λtype λdep + let bind = (Maybe.bind Kind.Term Kind.Term) + let pure = (Maybe.some Kind.Term) + let none = (Maybe.none Kind.Term) + let P = λx∀(type:Kind.Term)∀(dep:Nat)(Maybe Kind.Term) + let all = λterm.nam λterm.inp λterm.bod λtype λdep + (Kind.verify (Kind.all term.nam term.inp term.bod) type dep) + let lam = λterm.nam λterm.bod λtype λdep + ((Kind.if.all (Kind.reduce Bool.true type) + ∀(dep: Nat)∀(term.bod: ∀(x:Kind.Term)Kind.Term)(Maybe Kind.Term) + λtype.nam λtype.inp λtype.bod λdep λterm.bod + let ann = (Kind.ann (Kind.var term.nam dep) type.inp) + let term = (term.bod ann) + let type = (type.bod ann) + (Kind.check term type (Nat.succ dep)) + λtype λdep λterm.bod + (Kind.infer (Kind.lam term.nam term.bod) dep)) + dep term.bod) + let app = λterm.fun λterm.arg λtype λdep + (Kind.verify (Kind.app term.fun term.arg) type dep) + let ann = λval λtyp λtype λdep + (Kind.verify (Kind.ann val typ) type dep) + let slf = λterm.nam λterm.bod λtype λdep + (Kind.verify (Kind.slf term.nam term.bod) type dep) + let ins = λterm.val λtype λdep + ((Kind.if.slf (Kind.reduce Bool.true type) + ∀(term.val: Kind.Term)(Maybe Kind.Term) + λtype.nam λtype.bod λterm.val + (Kind.check term.val (type.bod (Kind.ins term.val)) dep) + λtype λterm.val + (Kind.infer (Kind.ins term.val) dep)) + term.val) + let ref = λterm.nam λterm.val λtype λdep + (Kind.check term.val type dep) + let def = λterm.nam λterm.val λterm.bod λtype λdep + (Kind.check (term.bod term.val) type (Nat.succ dep)) + let set = λtype λdep + (Kind.verify Kind.set type dep) + let u60 = λtype λdep + (Kind.verify Kind.u60 type dep) + let num = λterm.num λtype λdep + (Kind.verify (Kind.num term.num) type dep) + let op2 = λterm.opr λterm.fst λterm.snd λtype λdep + (Kind.verify (Kind.op2 term.opr term.fst term.snd) type dep) + let mat = λterm.nam λterm.x λterm.z λterm.s λterm.p λtype λdep + (Kind.verify (Kind.mat term.nam term.x term.z term.s term.p) type dep) + let txt = λterm.txt λtype λdep + (Kind.verify (Kind.txt term.txt) type dep) + let hol = λterm.nam λterm.ctx λtype λdep + (pure Kind.set) + let var = λterm.nam λterm.idx λtype λdep + (Kind.verify (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) \ No newline at end of file diff --git a/book/Kind.comparer.kind2 b/book/Kind.comparer.kind2 new file mode 100644 index 00000000..377712bf --- /dev/null +++ b/book/Kind.comparer.kind2 @@ -0,0 +1,93 @@ +Kind.comparer +: ∀(rec: ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool) + ∀(a : Kind.Term) + ∀(b : Kind.Term) + ∀(dep: Nat) + Bool += λrec λa λb λdep + let VAR = Kind.var + let SUC = Nat.succ + // Skips Ins, Ann and Let + let a = (Kind.skip a) + let b = (Kind.skip b) + // Checks if A is hole + let R = ∀(b:Kind.Term) ∀(dep:Nat) Bool + let Y = λa.nam λa.ctx λb λdep Bool.true + let N = λa λb λdep + // Checks if B is hole + let R = ∀(dep:Nat) ∀(a:Kind.Term) Bool + let Y = λb.nam λb.ctx λdep λa Bool.true + let N = λb λdep λa + // Checks if both are equal + let P = λx ∀(b: Kind.Term) ∀(dep: Nat) Bool + let all = λa.nam λa.inp λa.bod λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.nam λb.inp λb.bod λdep (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 Bool.false + (Kind.if.all b P Y N dep) + let lam = λa.nam λa.bod λb λdep + let P = ∀(dep:Nat) Bool + 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 Bool.false + (Kind.if.lam b P Y N dep) + let app = λa.fun λa.arg λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.fun λb.arg λdep (Bool.and (rec a.fun b.fun dep) (rec a.arg b.arg dep)) + let N = λval λdep Bool.false + (Kind.if.app b P Y N dep) + let ann = λa.val λa.typ λb λdep + Bool.false // unreachable + let slf = λa.nam λa.bod λb λdep + let P = ∀(dep:Nat) Bool + 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 Bool.false + (Kind.if.slf b P Y N dep) + let ins = λa.val λb λdep + Bool.false // unreachable + let ref = λa.nam λa.val λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.nam λb.val λdep (String.equal a.nam b.nam) + let N = λval λdep Bool.false + (Kind.if.ref b P Y N dep) + let def = λa.nam λa.val λa.bod λb λdep + Bool.false // unreachable + let set = λb λdep + let P = ∀(dep:Nat) Bool + let Y = λdep Bool.true + let F = λval λdep Bool.false + (Kind.if.set b P Y F dep) + let u60 = λb λdep + let P = ∀(dep:Nat) Bool + let Y = λdep Bool.true + let N = λval λdep Bool.false + (Kind.if.u60 b P Y N dep) + let num = λa.val λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.val λdep (U60.equal a.val b.val) + let N = λval λdep Bool.false + (Kind.if.num b P Y N dep) + let op2 = λa.opr λa.fst λa.snd λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.opr λb.fst λb.snd λdep (Bool.and (rec a.fst b.fst dep) (rec a.snd b.snd dep)) + let N = λval λdep Bool.false + (Kind.if.op2 b P Y N dep) + let mat = λa.nam λa.x λa.z λa.s λa.p λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.nam λb.x λb.z λb.s λb.p λdep (Bool.and (rec a.x b.x dep) (Bool.and (rec a.z b.z dep) (Bool.and (rec (a.s (VAR (String.concat a.nam "-1") dep)) (b.s (VAR (String.concat b.nam "-1") dep)) (SUC dep)) (rec (a.p (VAR a.nam dep)) (b.p (VAR b.nam dep)) (SUC dep))))) + let N = λval λdep Bool.false + (Kind.if.mat b P Y N dep) + let txt = λa.txt λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.txt λdep (String.equal a.txt b.txt) + let N = λval λdep Bool.false + (Kind.if.txt b P Y N dep) + let hol = λa.nam λa.ctx λb λdep + Bool.false // unreachable + let var = λa.nam λa.idx λb λdep + let P = ∀(dep:Nat) Bool + let Y = λb.nam λb.idx λdep (Nat.equal a.idx b.idx) + let N = λval λdep Bool.false + (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) + (Kind.if.hol b R Y N dep a) + (Kind.if.hol a R Y N b dep) diff --git a/book/Kind.def.kind2 b/book/Kind.def.kind2 new file mode 100644 index 00000000..2e6e19de --- /dev/null +++ b/book/Kind.def.kind2 @@ -0,0 +1,8 @@ +Kind.def +: ∀(nam: String) + ∀(val: Kind.Term) + ∀(bod: ∀(x: Kind.Term) Kind.Term) + Kind.Term += λnam λval λbod + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (def nam val bod) \ No newline at end of file diff --git a/book/Kind.equal.enter.kind2 b/book/Kind.equal.enter.kind2 new file mode 100644 index 00000000..7ef9dfd6 --- /dev/null +++ b/book/Kind.equal.enter.kind2 @@ -0,0 +1,11 @@ +Kind.equal.enter +: ∀(e: Bool) + ∀(a: Kind.Term) + ∀(b: Kind.Term) + ∀(dep: Nat) + Bool += λe λa λb λdep + let P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool + let true = λa λb λdep Bool.true + let false = λa λb λdep (Kind.comparer Kind.equal a b dep) + (~e P true false a b dep) \ No newline at end of file diff --git a/book/Kind.equal.kind2 b/book/Kind.equal.kind2 new file mode 100644 index 00000000..9e4ebe9b --- /dev/null +++ b/book/Kind.equal.kind2 @@ -0,0 +1,7 @@ +Kind.equal +: ∀(a: Kind.Term) + ∀(b: Kind.Term) + ∀(dep: Nat) + Bool += λa λb λdep + (Kind.equal.minor (Kind.identical a b dep) a b dep) diff --git a/book/Kind.equal.major.kind2 b/book/Kind.equal.major.kind2 new file mode 100644 index 00000000..0f6dd1a2 --- /dev/null +++ b/book/Kind.equal.major.kind2 @@ -0,0 +1,14 @@ +Kind.equal.major +: ∀(e: Bool) + ∀(a: Kind.Term) + ∀(b: Kind.Term) + ∀(dep: Nat) + Bool += λe λa λb λdep + let P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool + let true = λa λb λdep Bool.true + let false = λa λb λdep + let a_wnf = (Kind.reduce Bool.true a) + let b_wnf = (Kind.reduce Bool.true b) + (Kind.equal.enter (Kind.identical a_wnf b_wnf dep) a_wnf b_wnf dep) + (~e P true false a b dep) \ No newline at end of file diff --git a/book/Kind.equal.minor.kind2 b/book/Kind.equal.minor.kind2 new file mode 100644 index 00000000..a82f7032 --- /dev/null +++ b/book/Kind.equal.minor.kind2 @@ -0,0 +1,14 @@ +Kind.equal.minor +: ∀(e: Bool) + ∀(a: Kind.Term) + ∀(b: Kind.Term) + ∀(dep: Nat) + Bool += λe λa λb λdep + let P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool + let true = λa λb λdep Bool.true + let false = λa λb λdep + let a_wnf = (Kind.reduce Bool.false a) + let b_wnf = (Kind.reduce Bool.false b) + (Kind.equal.major (Kind.identical a_wnf b_wnf dep) a_wnf b_wnf dep) + (~e P true false a b dep) \ No newline at end of file diff --git a/book/Kind.hol.kind2 b/book/Kind.hol.kind2 new file mode 100644 index 00000000..4e100b95 --- /dev/null +++ b/book/Kind.hol.kind2 @@ -0,0 +1,7 @@ +Kind.hol +: ∀(nam: String) + ∀(ctx: (List Kind.Term)) + Kind.Term += λnam λctx + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (hol nam ctx) \ No newline at end of file diff --git a/book/Kind.identical.kind2 b/book/Kind.identical.kind2 new file mode 100644 index 00000000..79a65c81 --- /dev/null +++ b/book/Kind.identical.kind2 @@ -0,0 +1,7 @@ +Kind.identical +: ∀(a: Kind.Term) + ∀(b: Kind.Term) + ∀(dep: Nat) + Bool += λa λb λdep + (Kind.comparer Kind.identical a b dep) \ No newline at end of file diff --git a/book/Kind.if.all.kind2 b/book/Kind.if.all.kind2 new file mode 100644 index 00000000..a53cc4a1 --- /dev/null +++ b/book/Kind.if.all.kind2 @@ -0,0 +1,25 @@ +Kind.if.all +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (Y nam inp bod) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.ann.kind2 b/book/Kind.if.ann.kind2 new file mode 100644 index 00000000..45819f0a --- /dev/null +++ b/book/Kind.if.ann.kind2 @@ -0,0 +1,25 @@ +Kind.if.ann +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(val: Kind.Term) ∀(typ: Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(val: Kind.Term) ∀(typ: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (Y val typ) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.app.kind2 b/book/Kind.if.app.kind2 new file mode 100644 index 00000000..4ba6dac5 --- /dev/null +++ b/book/Kind.if.app.kind2 @@ -0,0 +1,25 @@ +Kind.if.app +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(fun: Kind.Term) ∀(arg: Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(fun: Kind.Term) ∀(arg: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (Y fun arg) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.def.kind2 b/book/Kind.if.def.kind2 new file mode 100644 index 00000000..8e9735e2 --- /dev/null +++ b/book/Kind.if.def.kind2 @@ -0,0 +1,25 @@ +Kind.if.def +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(val: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(val: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (Y nam val bod) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.hol.kind2 b/book/Kind.if.hol.kind2 new file mode 100644 index 00000000..8752552a --- /dev/null +++ b/book/Kind.if.hol.kind2 @@ -0,0 +1,25 @@ +Kind.if.hol +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(ctx: (List Kind.Term)) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(ctx: (List Kind.Term)) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (Y nam ctx) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.ins.kind2 b/book/Kind.if.ins.kind2 new file mode 100644 index 00000000..7284d372 --- /dev/null +++ b/book/Kind.if.ins.kind2 @@ -0,0 +1,25 @@ +Kind.if.ins +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(val: Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(val: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (Y val) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.lam.kind2 b/book/Kind.if.lam.kind2 new file mode 100644 index 00000000..896b2e00 --- /dev/null +++ b/book/Kind.if.lam.kind2 @@ -0,0 +1,25 @@ +Kind.if.lam +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (Y nam bod) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.mat.kind2 b/book/Kind.if.mat.kind2 new file mode 100644 index 00000000..0a0bf374 --- /dev/null +++ b/book/Kind.if.mat.kind2 @@ -0,0 +1,25 @@ +Kind.if.mat +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(x: Kind.Term) ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term) ∀(p: ∀(x: Kind.Term) Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(x: Kind.Term) ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term) ∀(p: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (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 (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.num.kind2 b/book/Kind.if.num.kind2 new file mode 100644 index 00000000..ab43cc4d --- /dev/null +++ b/book/Kind.if.num.kind2 @@ -0,0 +1,25 @@ +Kind.if.num +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(val: #U60) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(val: #U60) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (Y val) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.op2.kind2 b/book/Kind.if.op2.kind2 new file mode 100644 index 00000000..c0f9ec7f --- /dev/null +++ b/book/Kind.if.op2.kind2 @@ -0,0 +1,25 @@ +Kind.if.op2 +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (Y opr fst snd) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.ref.kind2 b/book/Kind.if.ref.kind2 new file mode 100644 index 00000000..8be5d253 --- /dev/null +++ b/book/Kind.if.ref.kind2 @@ -0,0 +1,25 @@ +Kind.if.ref +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(val: Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(val: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (Y nam val) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.set.kind2 b/book/Kind.if.set.kind2 new file mode 100644 index 00000000..bcb71ca6 --- /dev/null +++ b/book/Kind.if.set.kind2 @@ -0,0 +1,25 @@ +Kind.if.set +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (Y) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.slf.kind2 b/book/Kind.if.slf.kind2 new file mode 100644 index 00000000..534213af --- /dev/null +++ b/book/Kind.if.slf.kind2 @@ -0,0 +1,25 @@ +Kind.if.slf +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (Y nam bod) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.txt.kind2 b/book/Kind.if.txt.kind2 new file mode 100644 index 00000000..9a2558cb --- /dev/null +++ b/book/Kind.if.txt.kind2 @@ -0,0 +1,25 @@ +Kind.if.txt +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(lit: Kind.Text) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(lit: Kind.Text) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (Y lit) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.u60.kind2 b/book/Kind.if.u60.kind2 new file mode 100644 index 00000000..17c97680 --- /dev/null +++ b/book/Kind.if.u60.kind2 @@ -0,0 +1,25 @@ +Kind.if.u60 +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (Y) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) + let var = λnam λidx λY λN (N (Kind.var nam idx)) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) \ No newline at end of file diff --git a/book/Kind.if.var.kind2 b/book/Kind.if.var.kind2 new file mode 100644 index 00000000..53c3b9c3 --- /dev/null +++ b/book/Kind.if.var.kind2 @@ -0,0 +1,25 @@ +Kind.if.var +: ∀(term: Kind.Term) + ∀(P: *) + ∀(Y: ∀(nam: String) ∀(idx: Nat) P) + ∀(N: ∀(val: Kind.Term) P) + P += λterm λP λY λN + let P = λx ∀(Y: ∀(nam: String) ∀(idx: Nat) P) ∀(N: ∀(val: Kind.Term) P) P + let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) + let lam = λnam λbod λY λN (N (Kind.lam nam bod)) + let app = λfun λarg λY λN (N (Kind.app fun arg)) + let ann = λval λtyp λY λN (N (Kind.ann val typ)) + let slf = λnam λbod λY λN (N (Kind.slf nam bod)) + let ins = λval λY λN (N (Kind.ins val)) + let ref = λnam λval λY λN (N (Kind.ref nam val)) + let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) + let set = λY λN (N Kind.set) + let u60 = λY λN (N Kind.u60) + let num = λval λY λN (N (Kind.num val)) + let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) + let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) + let txt = λlit λY λN (N (Kind.txt lit)) + let hol = λnam λctx λY λN (N (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) \ No newline at end of file diff --git a/book/Kind.infer.kind2 b/book/Kind.infer.kind2 new file mode 100644 index 00000000..fbdddbdd --- /dev/null +++ b/book/Kind.infer.kind2 @@ -0,0 +1,64 @@ +Kind.infer +: ∀(term: Kind.Term) + ∀(dep: Nat) + (Maybe Kind.Term) += λterm λdep + let bind = (Maybe.bind Kind.Term Kind.Term) + let pure = (Maybe.some Kind.Term) + let none = (Maybe.none Kind.Term) + let P = λx∀(dep:Nat)(Maybe Kind.Term) + let all = λnam λinp λbod λdep + (bind (Kind.check inp Kind.set dep) λ_ + (bind (Kind.check (bod (Kind.ann (Kind.var nam dep) inp)) Kind.set (Nat.succ dep)) λ_ + (pure Kind.set))) + let lam = λnam λbod λdep + none + let app = λfun λarg λdep + (bind (Kind.infer fun dep) λfun_typ + ((Kind.if.all (Kind.reduce Bool.true fun_typ) + ∀(fun: Kind.Term)∀(arg: Kind.Term)(Maybe Kind.Term) + λfun_typ.nam λfun_typ.inp λfun_typ.bod λfun λarg + (bind (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 (Kind.check (bod (Kind.ann (Kind.var nam dep) (Kind.slf nam bod))) Kind.set (Nat.succ dep)) λ_ + (pure Kind.set)) + let ins = λval λdep + (bind (Kind.infer val dep) λval_typ + ((Kind.if.slf (Kind.reduce Bool.true val_typ) + ∀(val: Kind.Term)(Maybe Kind.Term) + λval_nam λval_typ.bod λval (pure (val_typ.bod (Kind.ins val))) + λval_typ λval none) + val)) + let ref = λnam λval λdep + (Kind.infer val dep) + let def = λnam λval λbod λdep + none + let set = λdep + (pure Kind.set) + let u60 = λdep + (pure Kind.set) + let num = λnum λdep + (pure Kind.u60) + let txt = λtxt λdep + (pure Kind.Book.String) + let op2 = λopr λfst λsnd λdep + (bind (Kind.check fst Kind.u60 dep) λ_ + (bind (Kind.check snd Kind.u60 dep) λ_ + (pure Kind.u60))) + let mat = λnam λx λz λs λp λdep + (bind (Kind.check x Kind.u60 dep) λx_typ + (bind (Kind.check (p (Kind.ann (Kind.var nam dep) Kind.u60)) Kind.set dep) λp_typ + (bind (Kind.check z (p (Kind.num #0)) dep) λz_typ + (bind (Kind.check (s (Kind.ann (Kind.var (String.concat nam "-1") dep) Kind.u60)) (p (Kind.op2 Kind.Oper.add (Kind.num #1) (Kind.var (String.concat nam "-1") dep))) (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) \ No newline at end of file diff --git a/book/Kind.ins.kind2 b/book/Kind.ins.kind2 new file mode 100644 index 00000000..60faad25 --- /dev/null +++ b/book/Kind.ins.kind2 @@ -0,0 +1,6 @@ +Kind.ins +: ∀(val: Kind.Term) + Kind.Term += λval + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (ins val) \ No newline at end of file diff --git a/book/Kind.kind2 b/book/Kind.kind2 index 48197c74..8899859a 100644 --- a/book/Kind.kind2 +++ b/book/Kind.kind2 @@ -1,1741 +1,3 @@ -Kind.Term -: * -= $self - ∀(P: ∀(x: Kind.Term) *) - ∀(all: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.all nam inp bod))) - ∀(lam: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.lam nam bod))) - ∀(app: ∀(fun: Kind.Term) ∀(arg: Kind.Term) (P (Kind.app fun arg))) - ∀(ann: ∀(val: Kind.Term) ∀(typ: Kind.Term) (P (Kind.ann val typ))) - ∀(slf: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.slf nam bod))) - ∀(ins: ∀(val: Kind.Term) (P (Kind.ins val))) - ∀(ref: ∀(nam: String) ∀(val: Kind.Term) (P (Kind.ref nam val))) - ∀(def: ∀(nam: String) ∀(val: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.def nam val bod))) - ∀(set: (P Kind.set)) - ∀(u60: (P Kind.u60)) - ∀(num: ∀(val: #U60) (P (Kind.num val))) - ∀(op2: ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term) (P (Kind.op2 opr fst snd))) - ∀(mat: ∀(nam: String) ∀(x: Kind.Term) ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term)Kind.Term) ∀(p: ∀(x: Kind.Term)Kind.Term) (P (Kind.mat nam x z s p))) - ∀(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) - -Kind.Oper -: * -= $self - ∀(P: ∀(x: Kind.Oper) *) - ∀(add: (P Kind.Oper.add)) - ∀(mul: (P Kind.Oper.mul)) - ∀(sub: (P Kind.Oper.sub)) - ∀(div: (P Kind.Oper.div)) - ∀(mod: (P Kind.Oper.mod)) - ∀(eq: (P Kind.Oper.eq)) - ∀(ne: (P Kind.Oper.ne)) - ∀(lt: (P Kind.Oper.lt)) - ∀(gt: (P Kind.Oper.gt)) - ∀(lte: (P Kind.Oper.lte)) - ∀(gte: (P Kind.Oper.gte)) - ∀(and: (P Kind.Oper.and)) - ∀(or: (P Kind.Oper.or)) - ∀(xor: (P Kind.Oper.xor)) - ∀(lsh: (P Kind.Oper.lsh)) - ∀(rsh: (P Kind.Oper.rsh)) - (P self) - -Kind.Binder -: * -= (Pair String Kind.Term) - -Kind.Scope -: * -= (List Kind.Binder) - -Kind.PreTerm -: * -= ∀(ctx: Kind.Scope) - Kind.Term - -Kind.Book -: * -= (String.Map Kind.Term) - -Kind.all -: ∀(nam: String) - ∀(inp: Kind.Term) - ∀(bod: ∀(x: Kind.Term) Kind.Term) - Kind.Term -= λnam λinp λbod - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (all nam inp bod) - -Kind.lam -: ∀(nam: String) - ∀(bod: ∀(x: Kind.Term) Kind.Term) - Kind.Term -= λnam λbod - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (lam nam bod) - -Kind.app -: ∀(fun: Kind.Term) - ∀(arg: Kind.Term) - Kind.Term -= λfun λarg - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (app fun arg) - -Kind.ann -: ∀(val: Kind.Term) - ∀(typ: Kind.Term) - Kind.Term -= λval λtyp - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (ann val typ) - -Kind.slf -: ∀(nam: String) - ∀(bod: ∀(x: Kind.Term) Kind.Term) - Kind.Term -= λnam λbod - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (slf nam bod) - -Kind.ins -: ∀(val: Kind.Term) - Kind.Term -= λval - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (ins val) - -Kind.ref -: ∀(nam: String) - ∀(val: Kind.Term) - Kind.Term -= λnam λval - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (ref nam val) - -Kind.def -: ∀(nam: String) - ∀(val: Kind.Term) - ∀(bod: ∀(x: Kind.Term) Kind.Term) - Kind.Term -= λnam λval λbod - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (def nam val bod) - -Kind.set -: Kind.Term -= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (set) - -Kind.u60 -: Kind.Term -= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - u60 - -Kind.num -: ∀(val: #U60) - Kind.Term -= λval - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (num val) - -Kind.op2 -: ∀(opr: Kind.Oper) - ∀(fst: Kind.Term) - ∀(snd: Kind.Term) - Kind.Term -= λopr λfst λsnd - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (op2 opr fst snd) - -Kind.mat -: ∀(nam: String) - ∀(x: Kind.Term) - ∀(z: Kind.Term) - ∀(s: ∀(x: Kind.Term) Kind.Term) - ∀(p: ∀(x: Kind.Term) Kind.Term) - Kind.Term -= λ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) - -Kind.txt -: ∀(lit: Kind.Text) - Kind.Term -= λlit - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (txt lit) - -Kind.hol -: ∀(nam: String) - ∀(ctx: (List Kind.Term)) - Kind.Term -= λnam λctx - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (hol nam ctx) - -Kind.var -: ∀(nam: String) - ∀(idx: Nat) - Kind.Term -= λnam λidx - ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (var nam idx) - -Kind.Oper.add -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (add) - -Kind.Oper.mul -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (mul) - -Kind.Oper.sub -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (sub) - -Kind.Oper.div -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (div) - -Kind.Oper.mod -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (mod) - -Kind.Oper.eq -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (eq) - -Kind.Oper.ne -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (ne) - -Kind.Oper.lt -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (lt) - -Kind.Oper.gt -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (gt) - -Kind.Oper.lte -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (lte) - -Kind.Oper.gte -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (gte) - -Kind.Oper.and -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (and) - -Kind.Oper.or -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (or) - -Kind.Oper.xor -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (xor) - -Kind.Oper.lsh -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (lsh) - -Kind.Oper.rsh -: Kind.Oper -= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh - (rsh) - -Kind.Binder.new -: ∀(nam: String) ∀(typ: Kind.Term) - Kind.Binder -= λnam λtyp - (Pair.new String Kind.Term nam typ) - -Kind.Scope.nil -: Kind.Scope -= (List.nil Kind.Binder) - -Kind.Scope.cons -: ∀(head: Kind.Binder) - ∀(tail: Kind.Scope) - Kind.Scope -= (List.cons Kind.Binder) - -Kind.Scope.extend -: ∀(nam: String) - ∀(typ: Kind.Term) - ∀(scp: Kind.Scope) - Kind.Scope -= λnam λtyp λscp - (Kind.Scope.cons (Kind.Binder.new nam typ) scp) - -Kind.Scope.find -: ∀(nam: String) - ∀(scp: Kind.Scope) - Kind.Term -= λname λscope - let cond = λbnd (~bnd λx(Bool) λnλt(String.equal name n)) - let found = (List.find Kind.Binder cond scope) - let P = λx(Kind.Term) - let some = λbnd (~bnd λx(Kind.Term) λnλt(t)) - let none = (Kind.ref name Kind.set) // FIXME: handle unbound reference - (~found P some none) - -Kind.if.all -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (Y nam inp bod) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.lam -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (Y nam bod) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.app -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(fun: Kind.Term) ∀(arg: Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(fun: Kind.Term) ∀(arg: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (Y fun arg) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.ann -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(val: Kind.Term) ∀(typ: Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(val: Kind.Term) ∀(typ: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (Y val typ) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.slf -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (Y nam bod) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.ins -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(val: Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(val: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (Y val) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.ref -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(val: Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(val: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (Y nam val) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.def -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(val: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(val: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (Y nam val bod) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.set -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (Y) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.u60 -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (Y) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.num -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(val: #U60) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(val: #U60) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (Y val) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.op2 -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (Y opr fst snd) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.mat -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(x: Kind.Term) ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term) ∀(p: ∀(x: Kind.Term) Kind.Term) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(x: Kind.Term) ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term) ∀(p: ∀(x: Kind.Term) Kind.Term) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (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 (Kind.txt lit)) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.txt -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(lit: Kind.Text) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(lit: Kind.Text) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (Y lit) - let hol = λnam λctx λY λN (N (Kind.hol nam ctx)) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.hol -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(ctx: (List Kind.Term)) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(ctx: (List Kind.Term)) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (Y nam ctx) - let var = λnam λidx λY λN (N (Kind.var nam idx)) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) - -Kind.if.var -: ∀(term: Kind.Term) - ∀(P: *) - ∀(Y: ∀(nam: String) ∀(idx: Nat) P) - ∀(N: ∀(val: Kind.Term) P) - P -= λterm λP λY λN - let P = λx ∀(Y: ∀(nam: String) ∀(idx: Nat) P) ∀(N: ∀(val: Kind.Term) P) P - let all = λnam λinp λbod λY λN (N (Kind.all nam inp bod)) - let lam = λnam λbod λY λN (N (Kind.lam nam bod)) - let app = λfun λarg λY λN (N (Kind.app fun arg)) - let ann = λval λtyp λY λN (N (Kind.ann val typ)) - let slf = λnam λbod λY λN (N (Kind.slf nam bod)) - let ins = λval λY λN (N (Kind.ins val)) - let ref = λnam λval λY λN (N (Kind.ref nam val)) - let def = λnam λval λbod λY λN (N (Kind.def nam val bod)) - let set = λY λN (N Kind.set) - let u60 = λY λN (N Kind.u60) - let num = λval λY λN (N (Kind.num val)) - let op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd)) - let mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p)) - let txt = λlit λY λN (N (Kind.txt lit)) - let hol = λnam λctx λY λN (N (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) - -Kind.Book.String -: Kind.Term -= (Kind.hol "TODO" (List.nil Kind.Term)) - -Kind.Book.String.cons -: Kind.Term -= (Kind.hol "TODO" (List.nil Kind.Term)) - -Kind.Book.String.nil -: Kind.Term -= (Kind.hol "TODO" (List.nil Kind.Term)) - -Kind.Text -: * -= String - -Kind.Text.show.go -: ∀(text: Kind.Text) - String.Concatenator -= String.Concatenator.from_string - -Kind.Term.show.go -: ∀(term: Kind.Term) - ∀(dep: Nat) - String.Concatenator -= λterm λdep - let P = λX(String.Concatenator) - let all = λnam λinp λbod λnil - ((Kind.Text.show.go "∀(") - ((Kind.Text.show.go nam) - ((Kind.Text.show.go ": ") - ((Kind.Term.show.go inp dep) - ((Kind.Text.show.go ") ") - ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) - nil)))))) - let lam = λnam λbod λnil - ((Kind.Text.show.go "λ") - ((Kind.Text.show.go nam) - ((Kind.Text.show.go " ") - ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) - nil)))) - let app = λfun λarg λnil - ((Kind.Text.show.go "(") - ((Kind.Term.show.go fun dep) - ((Kind.Text.show.go " ") - ((Kind.Term.show.go arg dep) - ((Kind.Text.show.go ")") - nil))))) - let ann = λval λtyp λnil - ((Kind.Text.show.go "{") - ((Kind.Term.show.go val dep) - ((Kind.Text.show.go " : ") - ((Kind.Term.show.go typ dep) - ((Kind.Text.show.go "}") - nil))))) - let slf = λnam λbod λnil - ((Kind.Text.show.go "$") - ((Kind.Text.show.go nam) - ((Kind.Text.show.go " ") - ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) - nil)))) - let ins = λval λnil - ((Kind.Text.show.go "~") - ((Kind.Term.show.go val dep) - nil)) - let ref = λnam λval λnil - ((Kind.Text.show.go nam) - nil) - let def = λnam λval λbod λnil - ((Kind.Text.show.go "let ") - ((Kind.Text.show.go nam) - ((Kind.Text.show.go " = ") - ((Kind.Term.show.go val dep) - ((Kind.Text.show.go "; ") - ((Kind.Term.show.go (bod (Kind.var nam dep)) (Nat.succ dep)) - nil)))))) - let set = λnil - ((Kind.Text.show.go "*") - nil) - let u60 = λnil - ((Kind.Text.show.go "#U60") - nil) - let num = λval λnil - ((Kind.Text.show.go "#") - ((U60.show.go val) - nil)) - let op2 = λopr λfst λsnd λnil - ((Kind.Text.show.go "#(") - ((Kind.Oper.show.go opr) - ((Kind.Text.show.go " ") - ((Kind.Term.show.go fst dep) - ((Kind.Text.show.go " ") - ((Kind.Term.show.go snd dep) - ((Kind.Text.show.go ")") - nil))))))) - let mat = λnam λx λz λs λp λnil - ((Kind.Text.show.go "#match ") - ((Kind.Text.show.go nam) - ((Kind.Text.show.go " = ") - ((Kind.Term.show.go x dep) - ((Kind.Text.show.go " { #0: ") - ((Kind.Term.show.go z dep) - ((Kind.Text.show.go "; #+: ") - ((Kind.Term.show.go (s (Kind.var nam dep)) (Nat.succ dep)) - ((Kind.Text.show.go " }: ") - ((Kind.Term.show.go (p (Kind.var nam dep)) (Nat.succ dep)) - nil)))))))))) - let txt = λtext λnil - ((Kind.Text.show.go String.quote) - ((Kind.Text.show.go text) - ((Kind.Text.show.go String.quote) - nil))) - let hol = λnam λctx λnil - ((Kind.Text.show.go "?") - ((Kind.Text.show.go nam) - nil)) - let var = λnam λidx λnil - ((Kind.Text.show.go nam) - nil) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) - -Kind.Term.show -: ∀(term: Kind.Term) - ∀(dep: Nat) - String -= λterm λdep - (String.Concatenator.build (Kind.Term.show.go term dep)) - -Kind.Oper.show.go -: ∀(oper: Kind.Oper) - String.Concatenator -= λoper - let P = λX(String.Concatenator) - let add = (Kind.Text.show.go "+") - let mul = (Kind.Text.show.go "*") - let sub = (Kind.Text.show.go "-") - let div = (Kind.Text.show.go "/") - let mod = (Kind.Text.show.go "%") - let eq = (Kind.Text.show.go "==") - let ne = (Kind.Text.show.go "!=") - let lt = (Kind.Text.show.go "<") - let gt = (Kind.Text.show.go ">") - let lte = (Kind.Text.show.go "<=") - let gte = (Kind.Text.show.go ">=") - let and = (Kind.Text.show.go "&") - let or = (Kind.Text.show.go "|") - let xor = (Kind.Text.show.go "^") - let lsh = (Kind.Text.show.go "<<") - let rsh = (Kind.Text.show.go ">>") - (~oper P add mul sub div mod eq ne lt gt lte gte and or xor lsh rsh) - -Kind.Oper.show -: ∀(oper: Kind.Oper) - String -= λoper (String.Concatenator.build (Kind.Oper.show.go oper)) - -Kind.Book.show.go -: ∀(book: Kind.Book) - String.Concatenator -= λbook - let P = λx String.Concatenator - let cons = λhead λtail - let P = λx String.Concatenator - let new = λhead.fst λhead.snd λnil - ((Kind.Text.show.go head.fst) - ((Kind.Text.show.go " = " - ((Kind.Term.show.go head.snd Nat.zero - ((Kind.Text.show.go String.newline - ((Kind.Book.show.go tail - nil))))))))) - (~head P new) - let nil = λnil nil - (~book P cons nil) - -Kind.Book.show -: ∀(book: Kind.Book) - String -= λbook - (String.Concatenator.build (Kind.Book.show.go book)) - -Kind.Term.parser.bind -: ∀(A: *) - ∀(a: (Parser A)) - ∀(b: ∀(x: A) (Parser Kind.PreTerm)) - (Parser Kind.PreTerm) -= λA (Parser.bind A Kind.PreTerm) - -Kind.Term.parser.pure -: ∀(value: Kind.PreTerm) - (Parser Kind.PreTerm) -= (Parser.pure Kind.PreTerm) - -Kind.Term.parser.all -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "∀" - (Kind.Term.parser.bind Unit (Parser.text "∀") λ_ - (Kind.Term.parser.bind Unit (Parser.text "(") λ_ - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.bind Unit (Parser.text ":") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λinp - (Kind.Term.parser.bind Unit (Parser.text ")") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod - (Kind.Term.parser.pure λscp - (Kind.all nam (inp scp) λx(bod (Kind.Scope.extend nam x scp)))))))))))) - -Kind.Term.parser.lam -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "λ" - (Kind.Term.parser.bind Unit (Parser.text "λ") λ_ - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod - (Kind.Term.parser.pure λscp - (Kind.lam nam λx(bod (Kind.Scope.extend nam x scp)))))))) - -Kind.Term.parser.app -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "(" - (Kind.Term.parser.bind Unit (Parser.text "(") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λfun - (Kind.Term.parser.bind (List Kind.PreTerm) (Parser.until Kind.PreTerm (Parser.skip Bool (Parser.test ")")) Kind.Term.parser) λterms - (Kind.Term.parser.bind Unit (Parser.text ")") λ_ - (Kind.Term.parser.pure λscp - (((List.fold Kind.PreTerm terms) ∀(fun:Kind.Term)Kind.Term - λargλrecλfun(rec (Kind.app fun (arg scp))) - λfun(fun)) - (fun scp)))))))) - -Kind.Term.parser.ann -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "{" - (Kind.Term.parser.bind Unit (Parser.text "{") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λval - (Kind.Term.parser.bind Unit (Parser.text ":") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λtyp - (Kind.Term.parser.bind Unit (Parser.text "}") λ_ - (Kind.Term.parser.pure λscp - (Kind.ann (val scp) (typ scp))))))))) - -Kind.Term.parser.slf -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "$" - (Kind.Term.parser.bind Unit (Parser.text "$") λ_ - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod - (Kind.Term.parser.pure λscp - (Kind.slf nam λx(bod (Kind.Scope.extend nam x scp)))))))) - -Kind.Term.parser.ins -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "~" - (Kind.Term.parser.bind Unit (Parser.text "~") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λval - (Kind.Term.parser.pure λscp - (Kind.ins (val scp)))))) - -Kind.Term.parser.set -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "*" - (Kind.Term.parser.bind Unit (Parser.text "*") λ_ - (Kind.Term.parser.pure λscp - Kind.set))) - -Kind.Term.parser.def -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "let " - (Kind.Term.parser.bind Unit (Parser.text "let ") λ_ - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.bind Unit (Parser.text "=") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λval - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λbod - (Kind.Term.parser.pure λscp - (Kind.def nam (val scp) λx(bod (Kind.Scope.extend nam x scp)))))))))) - -Kind.Term.parser.u60 -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "#U60" - (Kind.Term.parser.bind Unit (Parser.text "#U60") λ_ - (Kind.Term.parser.pure λscp - Kind.u60))) - -Kind.Term.parser.op2 -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "#(" - (Kind.Term.parser.bind Unit (Parser.text "#(") λ_ - (Kind.Term.parser.bind Kind.Oper Kind.Oper.parser λopr - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λfst - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λsnd - (Kind.Term.parser.bind Unit (Parser.text ")") λ_ - (Kind.Term.parser.pure λscp - (Kind.op2 opr (fst scp) (snd scp))))))))) - -Kind.Term.parser.mat -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "#match " - (Kind.Term.parser.bind Unit (Parser.text "#match ") λ_ - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.bind Unit (Parser.text "=") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λx - (Kind.Term.parser.bind Unit (Parser.text "{") λ_ - (Kind.Term.parser.bind Unit (Parser.text "#0") λ_ - (Kind.Term.parser.bind Unit (Parser.text ":") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λz - (Kind.Term.parser.bind Unit (Parser.text "#+") λ_ - (Kind.Term.parser.bind Unit (Parser.text ":") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λs - (Kind.Term.parser.bind Unit (Parser.text "}") λ_ - (Kind.Term.parser.bind Unit (Parser.text ":") λ_ - (Kind.Term.parser.bind Kind.PreTerm Kind.Term.parser λp - (Kind.Term.parser.pure λscp - (Kind.mat nam (x scp) (z scp) λx(s (Kind.Scope.extend nam x scp)) λx(p (Kind.Scope.extend nam x scp))))))))))))))))))) - -Kind.Term.parser.num -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "#" - (Kind.Term.parser.bind Unit (Parser.text "#") λ_ - (Kind.Term.parser.bind #U60 U60.parser.decimal λnum - (Kind.Term.parser.pure λscp - (Kind.num num))))) - -Kind.Term.parser.chr -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "'" - (Kind.Term.parser.bind Unit (Parser.text "'") λ_ - (Kind.Term.parser.bind #U60 Parser.char λchr - (Kind.Term.parser.bind Unit (Parser.text "'") λ_ - (Kind.Term.parser.pure λscp - (Kind.num chr)))))) - -Kind.Term.parser.str -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm String.quote - (Kind.Term.parser.bind Unit (Parser.text String.quote) λ_ - (Kind.Term.parser.bind String (Parser.until Char (Parser.test String.quote) Parser.char) λchars - (Kind.Term.parser.bind Unit (Parser.text String.quote) λ_ - (Kind.Term.parser.pure λscp - (Kind.txt chars)))))) - -Kind.Term.parser.hol -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.text Kind.PreTerm "?" - (Kind.Term.parser.bind Unit (Parser.text "?") λ_ - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.pure λscp - (Kind.hol nam (List.nil Kind.Term)))))) // TODO: build context - -Kind.Term.parser.var -: (Parser.Guard Kind.PreTerm) -= (Parser.Guard.pass Kind.PreTerm - (Kind.Term.parser.bind String Parser.name λnam - (Kind.Term.parser.pure λscp - (Kind.Scope.find nam scp)))) - -Kind.Oper.parser -: (Parser Kind.Oper) -= let TRY = (List.cons (Parser.Guard Kind.Oper)) - let END = (List.nil (Parser.Guard Kind.Oper)) - let OP2 = - { λsym λoper - (Parser.Guard.text Kind.Oper sym - (Parser.bind Unit Kind.Oper (Parser.text sym) λx - (Parser.pure Kind.Oper oper))) - : ∀(sym: String) ∀(oper: Kind.Oper) (Parser.Guard Kind.Oper)} - (Parser.variant Kind.Oper - (TRY (OP2 "+" Kind.Oper.add) - (TRY (OP2 "*" Kind.Oper.mul) - (TRY (OP2 "-" Kind.Oper.sub) - (TRY (OP2 "/" Kind.Oper.div) - (TRY (OP2 "%" Kind.Oper.mod) - (TRY (OP2 "==" Kind.Oper.eq) - (TRY (OP2 "!=" Kind.Oper.ne) - (TRY (OP2 "<=" Kind.Oper.lte) - (TRY (OP2 ">=" Kind.Oper.gte) - (TRY (OP2 "<<" Kind.Oper.lsh) - (TRY (OP2 ">>" Kind.Oper.rsh) - (TRY (OP2 "<" Kind.Oper.lt) - (TRY (OP2 ">" Kind.Oper.gt) - (TRY (OP2 "&" Kind.Oper.and) - (TRY (OP2 "|" Kind.Oper.or) - (TRY (OP2 "^" Kind.Oper.xor) - END))))))))))))))))) - -Kind.Term.parser -: (Parser Kind.PreTerm) -= let TRY = (List.cons (Parser.Guard Kind.PreTerm)) - let END = (List.nil (Parser.Guard Kind.PreTerm)) - (Parser.variant Kind.PreTerm - (TRY Kind.Term.parser.all - (TRY Kind.Term.parser.lam - (TRY Kind.Term.parser.app - (TRY Kind.Term.parser.ann - (TRY Kind.Term.parser.slf - (TRY Kind.Term.parser.ins - (TRY Kind.Term.parser.set - (TRY Kind.Term.parser.def - (TRY Kind.Term.parser.u60 - (TRY Kind.Term.parser.op2 - (TRY Kind.Term.parser.mat - (TRY Kind.Term.parser.chr - (TRY Kind.Term.parser.str - (TRY Kind.Term.parser.num - (TRY Kind.Term.parser.hol - (TRY Kind.Term.parser.var - END))))))))))))))))) - -Kind.Term.parse -: ∀(code: String) - Kind.Term -= λcode - let P = λx(Kind.Term) - let done = λcode λterm (term (List.nil Kind.Binder)) - let fail = λerror (Kind.hol "error" (List.nil Kind.Term)) - (~(Kind.Term.parser code) P done fail) - -Kind.Book.parser -: (Parser Kind.Book) -= (Parser.bind Bool Kind.Book Parser.is_eof λis_eof - let P = λx(Parser Kind.Book) - // If EOF, return an empty book - let true = - (Parser.pure Kind.Book (String.Map.new Kind.Term)) - // Otherwise, parse a definition - let false = - (Parser.bind String Kind.Book Parser.name λnam - (Parser.bind Bool Kind.Book (Parser.skip Bool (Parser.test ":")) λann - let P = λx(Parser Kind.Book) - // If annotated, parses the annotation - let true = - (Parser.bind Unit Kind.Book (Parser.text ":") λ_ - (Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λtyp - (Parser.bind Unit Kind.Book (Parser.text "=") λ_ - (Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λval - (Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook - (Parser.pure Kind.Book (String.Map.set Kind.Term nam (Kind.ann (val (List.nil Kind.Binder)) (typ (List.nil Kind.Binder))) book))))))) - // Otherwise, parses just the value - let false = - (Parser.bind Unit Kind.Book (Parser.text "=") λ_ - (Parser.bind Kind.PreTerm Kind.Book Kind.Term.parser λval - (Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook - (Parser.pure Kind.Book (String.Map.set Kind.Term nam (val (List.nil Kind.Binder)) book))))) - (~ann P true false))) - (~is_eof P true false)) - -Kind.Book.parse -: ∀(code: String) - Kind.Book -= λcode - 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) - -Kind.reduce -: ∀(maj: Bool) - ∀(term: Kind.Term) - Kind.Term -= λmaj λterm - let P = λx(Kind.Term) - let all = Kind.all - let lam = Kind.lam - let app = λfun λarg (Kind.reduce.app maj (Kind.reduce maj fun) arg) - let slf = Kind.slf - let ann = λval λtyp (Kind.reduce maj val) - let ins = λval (Kind.reduce maj val) - let ref = λnam λval (Kind.reduce.ref maj nam val) - let def = λnam λval λbod (Kind.reduce maj (bod val)) - let set = Kind.set - let u60 = Kind.u60 - let num = Kind.num - let op2 = λopr λfst λsnd (Kind.reduce.op2 opr fst snd) - let mat = λnam λx λz λs λp (Kind.reduce.mat maj nam x z s p) - let txt = λtxt (Kind.reduce.txt txt) - let hol = Kind.hol - let var = Kind.var - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) - -Kind.reduce.app -: ∀(maj: Bool) - ∀(fun: Kind.Term) - ∀(arg: Kind.Term) - Kind.Term -= λmaj λfun λarg - let P = ∀(arg: Kind.Term) Kind.Term - let Y = λnam λbod λarg (Kind.reduce maj (bod (Kind.reduce maj arg))) - let N = λfun λarg (Kind.app fun arg) - (Kind.if.lam fun P Y N arg) - -Kind.reduce.ref -: ∀(maj: Bool) - ∀(nam: String) - ∀(val: Kind.Term) - Kind.Term -= λmaj λnam λval - let P = λx ∀(nam: String) ∀(val: Kind.Term) Kind.Term - let true = λnam λval (Kind.reduce maj val) - let false = Kind.ref - (~maj P true false nam val) - -Kind.reduce.op2 -: ∀(opr: Kind.Oper) - ∀(fst: Kind.Term) - ∀(snd: Kind.Term) - Kind.Term -= λopr λfst λsnd - let P = ∀(snd: Kind.Term) Kind.Term - let Y = λfst_val λsnd - let P = ∀(fst_val: #U60) Kind.Term - let Y = λsnd_val λfst_val - let P = λx ∀(fst_val: #U60) ∀(snd_val: #U60) Kind.Term - let add = λfst_val λsnd_val (Kind.num #(+ fst_val snd_val)) - let mul = λfst_val λsnd_val (Kind.num #(* fst_val snd_val)) - let sub = λfst_val λsnd_val (Kind.num #(- fst_val snd_val)) - let div = λfst_val λsnd_val (Kind.num #(/ fst_val snd_val)) - let eq = λfst_val λsnd_val (Kind.num #(== fst_val snd_val)) - let ne = λfst_val λsnd_val (Kind.num #(!= fst_val snd_val)) - let lt = λfst_val λsnd_val (Kind.num #(< fst_val snd_val)) - let gt = λfst_val λsnd_val (Kind.num #(> fst_val snd_val)) - let lte = λfst_val λsnd_val (Kind.num #(<= fst_val snd_val)) - let gte = λfst_val λsnd_val (Kind.num #(>= fst_val snd_val)) - let and = λfst_val λsnd_val (Kind.num #(& fst_val snd_val)) - let or = λfst_val λsnd_val (Kind.num #(| fst_val snd_val)) - let xor = λfst_val λsnd_val (Kind.num #(^ fst_val snd_val)) - let lsh = λfst_val λsnd_val (Kind.num #(<< fst_val snd_val)) - let rsh = λfst_val λsnd_val (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 (Kind.op2 opr (Kind.num fst_val) snd) - (Kind.if.num snd P Y N fst_val) - let N = λfst λsnd (Kind.op2 opr fst snd) - (Kind.if.num fst P Y N snd) - -Kind.reduce.mat -: ∀(maj: Bool) - ∀(nam: String) - ∀(x: Kind.Term) - ∀(z: Kind.Term) - ∀(s: ∀(x:Kind.Term)Kind.Term) - ∀(p: ∀(x:Kind.Term)Kind.Term) - Kind.Term -= λmaj λnam λx λz λs λp - let P = ∀(z: Kind.Term) ∀(s: ∀(x:Kind.Term)Kind.Term) Kind.Term - let Y = λx.val - #match x = x.val { - #0: λz λs (Kind.reduce maj z) - #+: λz λs (Kind.reduce maj (s (Kind.num x-1))) - }: ∀(z: Kind.Term) ∀(s: ∀(x:Kind.Term)Kind.Term) Kind.Term - let N = λx λz λs (Kind.mat nam x z s p) - ((Kind.if.num x P Y N) z s) - -Kind.reduce.txt -: ∀(txt: Kind.Text) - Kind.Term -= λtxt - let P = λx Kind.Term - let cons = λx λxs (Kind.reduce Bool.true (Kind.app (Kind.app Kind.Book.String.cons (Kind.num x)) (Kind.txt xs))) - let nil = (Kind.reduce Bool.true Kind.Book.String.nil) - (~txt P cons nil) - -Kind.normal -: ∀(maj: Bool) - ∀(term: Kind.Term) - ∀(dep: Nat) - Kind.Term -= λmaj λterm λdep - (Kind.normal.go maj (Kind.reduce maj term) dep) - -Kind.normal.go -: ∀(maj: Bool) - ∀(term: Kind.Term) - ∀(dep: Nat) - Kind.Term -= λmaj λterm λdep - let P = λx Kind.Term - let all = λnam λinp λbod (Kind.all nam (Kind.normal maj inp dep) λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) - let lam = λnam λbod (Kind.lam nam λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) - let app = λfun λarg (Kind.app (Kind.normal maj fun dep) (Kind.normal maj arg dep)) - let ann = λval λtyp (Kind.ann (Kind.normal maj val dep) (Kind.normal maj typ dep)) - let slf = λnam λbod (Kind.slf nam λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) - let ins = λval (Kind.ins (Kind.normal maj val dep)) - let ref = λnam λval (Kind.ref nam (Kind.normal maj val dep)) - let def = λnam λval λbod (Kind.def nam (Kind.normal maj val dep) λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) - let set = Kind.set - let u60 = Kind.u60 - let num = Kind.num - let op2 = λopr λfst λsnd (Kind.op2 opr (Kind.normal maj fst dep) (Kind.normal maj snd dep)) - let mat = λnam λx λz λs λp (Kind.mat nam (Kind.normal maj x dep) (Kind.normal maj z dep) λk(Kind.normal maj (s (Kind.var nam dep)) (Nat.succ dep)) λk(Kind.normal maj (p (Kind.var nam dep)) (Nat.succ dep))) - let txt = λtxt (Kind.txt txt) - let hol = λnam λctx (Kind.hol nam ctx) - let var = λnam λidx (Kind.var nam idx) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) - -Kind.equal -: ∀(a: Kind.Term) - ∀(b: Kind.Term) - ∀(dep: Nat) - Bool -= λa λb λdep - (Kind.equal.minor (Kind.identical a b dep) a b dep) - -Kind.equal.minor -: ∀(e: Bool) - ∀(a: Kind.Term) - ∀(b: Kind.Term) - ∀(dep: Nat) - Bool -= λe λa λb λdep - let P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool - let true = λa λb λdep Bool.true - let false = λa λb λdep - let a_wnf = (Kind.reduce Bool.false a) - let b_wnf = (Kind.reduce Bool.false b) - (Kind.equal.major (Kind.identical a_wnf b_wnf dep) a_wnf b_wnf dep) - (~e P true false a b dep) - -Kind.equal.major -: ∀(e: Bool) - ∀(a: Kind.Term) - ∀(b: Kind.Term) - ∀(dep: Nat) - Bool -= λe λa λb λdep - let P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool - let true = λa λb λdep Bool.true - let false = λa λb λdep - let a_wnf = (Kind.reduce Bool.true a) - let b_wnf = (Kind.reduce Bool.true b) - (Kind.equal.enter (Kind.identical a_wnf b_wnf dep) a_wnf b_wnf dep) - (~e P true false a b dep) - -Kind.equal.enter -: ∀(e: Bool) - ∀(a: Kind.Term) - ∀(b: Kind.Term) - ∀(dep: Nat) - Bool -= λe λa λb λdep - let P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool - let true = λa λb λdep Bool.true - let false = λa λb λdep (Kind.comparer Kind.equal a b dep) - (~e P true false a b dep) - -Kind.identical -: ∀(a: Kind.Term) - ∀(b: Kind.Term) - ∀(dep: Nat) - Bool -= λa λb λdep - (Kind.comparer Kind.identical a b dep) - -Kind.comparer -: ∀(rec: ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool) - ∀(a : Kind.Term) - ∀(b : Kind.Term) - ∀(dep: Nat) - Bool -= λrec λa λb λdep - let VAR = Kind.var - let SUC = Nat.succ - // Skips Ins, Ann and Let - let a = (Kind.skip a) - let b = (Kind.skip b) - // Checks if A is hole - let R = ∀(b:Kind.Term) ∀(dep:Nat) Bool - let Y = λa.nam λa.ctx λb λdep Bool.true - let N = λa λb λdep - // Checks if B is hole - let R = ∀(dep:Nat) ∀(a:Kind.Term) Bool - let Y = λb.nam λb.ctx λdep λa Bool.true - let N = λb λdep λa - // Checks if both are equal - let P = λx ∀(b: Kind.Term) ∀(dep: Nat) Bool - let all = λa.nam λa.inp λa.bod λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.nam λb.inp λb.bod λdep (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 Bool.false - (Kind.if.all b P Y N dep) - let lam = λa.nam λa.bod λb λdep - let P = ∀(dep:Nat) Bool - 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 Bool.false - (Kind.if.lam b P Y N dep) - let app = λa.fun λa.arg λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.fun λb.arg λdep (Bool.and (rec a.fun b.fun dep) (rec a.arg b.arg dep)) - let N = λval λdep Bool.false - (Kind.if.app b P Y N dep) - let ann = λa.val λa.typ λb λdep - Bool.false // unreachable - let slf = λa.nam λa.bod λb λdep - let P = ∀(dep:Nat) Bool - 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 Bool.false - (Kind.if.slf b P Y N dep) - let ins = λa.val λb λdep - Bool.false // unreachable - let ref = λa.nam λa.val λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.nam λb.val λdep (String.equal a.nam b.nam) - let N = λval λdep Bool.false - (Kind.if.ref b P Y N dep) - let def = λa.nam λa.val λa.bod λb λdep - Bool.false // unreachable - let set = λb λdep - let P = ∀(dep:Nat) Bool - let Y = λdep Bool.true - let F = λval λdep Bool.false - (Kind.if.set b P Y F dep) - let u60 = λb λdep - let P = ∀(dep:Nat) Bool - let Y = λdep Bool.true - let N = λval λdep Bool.false - (Kind.if.u60 b P Y N dep) - let num = λa.val λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.val λdep (U60.equal a.val b.val) - let N = λval λdep Bool.false - (Kind.if.num b P Y N dep) - let op2 = λa.opr λa.fst λa.snd λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.opr λb.fst λb.snd λdep (Bool.and (rec a.fst b.fst dep) (rec a.snd b.snd dep)) - let N = λval λdep Bool.false - (Kind.if.op2 b P Y N dep) - let mat = λa.nam λa.x λa.z λa.s λa.p λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.nam λb.x λb.z λb.s λb.p λdep (Bool.and (rec a.x b.x dep) (Bool.and (rec a.z b.z dep) (Bool.and (rec (a.s (VAR (String.concat a.nam "-1") dep)) (b.s (VAR (String.concat b.nam "-1") dep)) (SUC dep)) (rec (a.p (VAR a.nam dep)) (b.p (VAR b.nam dep)) (SUC dep))))) - let N = λval λdep Bool.false - (Kind.if.mat b P Y N dep) - let txt = λa.txt λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.txt λdep (String.equal a.txt b.txt) - let N = λval λdep Bool.false - (Kind.if.txt b P Y N dep) - let hol = λa.nam λa.ctx λb λdep - Bool.false // unreachable - let var = λa.nam λa.idx λb λdep - let P = ∀(dep:Nat) Bool - let Y = λb.nam λb.idx λdep (Nat.equal a.idx b.idx) - let N = λval λdep Bool.false - (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) - (Kind.if.hol b R Y N dep a) - (Kind.if.hol a R Y N b dep) - -Kind.skip -: ∀(x: Kind.Term) - Kind.Term -= λx - let P = λx Kind.Term - let all = Kind.all - let lam = Kind.lam - let app = Kind.app - let ann = λval λtyp (Kind.skip val) - let slf = Kind.slf - let ins = λval (Kind.skip val) - let ref = Kind.ref - let def = λnam λval λbod (Kind.skip (bod val)) - let set = Kind.set - let u60 = Kind.u60 - let num = Kind.num - let op2 = Kind.op2 - let mat = Kind.mat - let txt = Kind.txt - let hol = Kind.hol - let var = Kind.var - (~x P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) - -Kind.infer -: ∀(term: Kind.Term) - ∀(dep: Nat) - (Maybe Kind.Term) -= λterm λdep - let bind = (Maybe.bind Kind.Term Kind.Term) - let pure = (Maybe.some Kind.Term) - let none = (Maybe.none Kind.Term) - let P = λx∀(dep:Nat)(Maybe Kind.Term) - let all = λnam λinp λbod λdep - (bind (Kind.check inp Kind.set dep) λ_ - (bind (Kind.check (bod (Kind.ann (Kind.var nam dep) inp)) Kind.set (Nat.succ dep)) λ_ - (pure Kind.set))) - let lam = λnam λbod λdep - none - let app = λfun λarg λdep - (bind (Kind.infer fun dep) λfun_typ - ((Kind.if.all (Kind.reduce Bool.true fun_typ) - ∀(fun: Kind.Term)∀(arg: Kind.Term)(Maybe Kind.Term) - λfun_typ.nam λfun_typ.inp λfun_typ.bod λfun λarg - (bind (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 (Kind.check (bod (Kind.ann (Kind.var nam dep) (Kind.slf nam bod))) Kind.set (Nat.succ dep)) λ_ - (pure Kind.set)) - let ins = λval λdep - (bind (Kind.infer val dep) λval_typ - ((Kind.if.slf (Kind.reduce Bool.true val_typ) - ∀(val: Kind.Term)(Maybe Kind.Term) - λval_nam λval_typ.bod λval (pure (val_typ.bod (Kind.ins val))) - λval_typ λval none) - val)) - let ref = λnam λval λdep - (Kind.infer val dep) - let def = λnam λval λbod λdep - none - let set = λdep - (pure Kind.set) - let u60 = λdep - (pure Kind.set) - let num = λnum λdep - (pure Kind.u60) - let txt = λtxt λdep - (pure Kind.Book.String) - let op2 = λopr λfst λsnd λdep - (bind (Kind.check fst Kind.u60 dep) λ_ - (bind (Kind.check snd Kind.u60 dep) λ_ - (pure Kind.u60))) - let mat = λnam λx λz λs λp λdep - (bind (Kind.check x Kind.u60 dep) λx_typ - (bind (Kind.check (p (Kind.ann (Kind.var nam dep) Kind.u60)) Kind.set dep) λp_typ - (bind (Kind.check z (p (Kind.num #0)) dep) λz_typ - (bind (Kind.check (s (Kind.ann (Kind.var (String.concat nam "-1") dep) Kind.u60)) (p (Kind.op2 Kind.Oper.add (Kind.num #1) (Kind.var (String.concat nam "-1") dep))) (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) - -Kind.check -: ∀(term: Kind.Term) - ∀(type: Kind.Term) - ∀(dep: Nat) - (Maybe Kind.Term) -= λterm λtype λdep - let bind = (Maybe.bind Kind.Term Kind.Term) - let pure = (Maybe.some Kind.Term) - let none = (Maybe.none Kind.Term) - let P = λx∀(type:Kind.Term)∀(dep:Nat)(Maybe Kind.Term) - let all = λterm.nam λterm.inp λterm.bod λtype λdep - (Kind.verify (Kind.all term.nam term.inp term.bod) type dep) - let lam = λterm.nam λterm.bod λtype λdep - ((Kind.if.all (Kind.reduce Bool.true type) - ∀(dep: Nat)∀(term.bod: ∀(x:Kind.Term)Kind.Term)(Maybe Kind.Term) - λtype.nam λtype.inp λtype.bod λdep λterm.bod - let ann = (Kind.ann (Kind.var term.nam dep) type.inp) - let term = (term.bod ann) - let type = (type.bod ann) - (Kind.check term type (Nat.succ dep)) - λtype λdep λterm.bod - (Kind.infer (Kind.lam term.nam term.bod) dep)) - dep term.bod) - let app = λterm.fun λterm.arg λtype λdep - (Kind.verify (Kind.app term.fun term.arg) type dep) - let ann = λval λtyp λtype λdep - (Kind.verify (Kind.ann val typ) type dep) - let slf = λterm.nam λterm.bod λtype λdep - (Kind.verify (Kind.slf term.nam term.bod) type dep) - let ins = λterm.val λtype λdep - ((Kind.if.slf (Kind.reduce Bool.true type) - ∀(term.val: Kind.Term)(Maybe Kind.Term) - λtype.nam λtype.bod λterm.val - (Kind.check term.val (type.bod (Kind.ins term.val)) dep) - λtype λterm.val - (Kind.infer (Kind.ins term.val) dep)) - term.val) - let ref = λterm.nam λterm.val λtype λdep - (Kind.check term.val type dep) - let def = λterm.nam λterm.val λterm.bod λtype λdep - (Kind.check (term.bod term.val) type (Nat.succ dep)) - let set = λtype λdep - (Kind.verify Kind.set type dep) - let u60 = λtype λdep - (Kind.verify Kind.u60 type dep) - let num = λterm.num λtype λdep - (Kind.verify (Kind.num term.num) type dep) - let op2 = λterm.opr λterm.fst λterm.snd λtype λdep - (Kind.verify (Kind.op2 term.opr term.fst term.snd) type dep) - let mat = λterm.nam λterm.x λterm.z λterm.s λterm.p λtype λdep - (Kind.verify (Kind.mat term.nam term.x term.z term.s term.p) type dep) - let txt = λterm.txt λtype λdep - (Kind.verify (Kind.txt term.txt) type dep) - let hol = λterm.nam λterm.ctx λtype λdep - (pure Kind.set) - let var = λterm.nam λterm.idx λtype λdep - (Kind.verify (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) - -Kind.verify -: ∀(term: Kind.Term) - ∀(type: Kind.Term) - ∀(dep: Nat) - (Maybe Kind.Term) -= λterm λtype λdep - let bind = (Maybe.bind Kind.Term Kind.Term) - let pure = (Maybe.some Kind.Term) - let none = (Maybe.none Kind.Term) - (bind (Kind.infer term dep) λinfer - (Kind.report (Kind.equal infer type dep) infer type term dep)) - -Kind.report -: ∀(e: Bool) - ∀(inferred: Kind.Term) - ∀(expected: Kind.Term) - ∀(value: Kind.Term) - ∀(dep: Nat) - (Maybe Kind.Term) -= λe λinferred λexpected λvalue λdep - let pure = (Maybe.some Kind.Term) - let none = (Maybe.none Kind.Term) - let P = λx ∀(inferred: Kind.Term) ∀(expected: Kind.Term) ∀(value: Kind.Term) ∀(dep: Nat) (Maybe Kind.Term) - let true = λinferred λexpected λvalue λdep (pure Kind.set) - let false = λinferred λexpected λvalue λdep none // TODO: HVM.log error - (~e P true false inferred expected value dep) - -Kind.Term.to_hvm.go -: ∀(term: Kind.Term) - ∀(dep: Nat) - String.Concatenator -= λterm λdep - let P = λx String.Concatenator - let all = λnam λinp λbod - (Kind.Text.show.go "0") - let lam = λnam λbod λnil - ((Kind.Text.show.go "λ") - ((Kind.Text.show.go (U60.name (U60.from_nat dep))) - ((Kind.Text.show.go " " - ((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep)) - nil))))) - let app = λfun λarg λnil - ((Kind.Text.show.go "(") - ((Kind.Term.to_hvm.go fun dep) - ((Kind.Text.show.go " ") - ((Kind.Term.to_hvm.go arg dep) - ((Kind.Text.show.go ")") - nil))))) - let ann = λval λtyp - (Kind.Term.to_hvm.go val dep) - let slf = λnam λbod - (Kind.Text.show.go "0") - let ins = λval - (Kind.Term.to_hvm.go val dep) - let ref = λnam λval - (Kind.Text.show.go nam) - let def = λnam λval λbod λnil - ((Kind.Text.show.go "let ") - ((Kind.Text.show.go nam) - ((Kind.Text.show.go " = ") - ((Kind.Term.to_hvm.go val dep) - ((Kind.Text.show.go "; ") - ((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep)) - nil)))))) - let set = - (Kind.Text.show.go "0") - let u60 = - (Kind.Text.show.go "0") - let num = λval - (U60.show.go val) - let op2 = λopr λfst λsnd λnil - ((Kind.Text.show.go "(") - ((Kind.Oper.show.go opr) // TODO: Kind.Oper.to_hvm - ((Kind.Text.show.go " ") - ((Kind.Term.to_hvm.go fst dep) - ((Kind.Text.show.go " ") - ((Kind.Term.to_hvm.go snd dep) - ((Kind.Text.show.go ")") - nil))))))) - let mat = λnam λx λz λs λp λnil - ((Kind.Text.show.go "(U60.match ") - ((Kind.Term.to_hvm.go x dep) - ((Kind.Text.show.go " ") - ((Kind.Term.to_hvm.go z dep) - ((Kind.Text.show.go " ") - ((Kind.Term.to_hvm.go (s (Kind.var (String.concat nam "_1") dep)) (Nat.succ dep)) - ((Kind.Text.show.go " ") - ((Kind.Term.to_hvm.go (p (Kind.var nam dep)) (Nat.succ dep)) - ((Kind.Text.show.go ")") - nil))))))))) - let txt = λtxt λnil - ((Kind.Text.show.go String.quote) - ((Kind.Text.show.go txt) - ((Kind.Text.show.go String.quote) - nil))) - let hol = λnam λctx - (Kind.Text.show.go "0") - let var = λnam λidx - (Kind.Text.show.go (U60.name (U60.from_nat idx))) - (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) - -Kind.Term.to_hvm -: ∀(term: Kind.Term) - ∀(dep: Nat) - String -= λterm λdep - (String.Concatenator.build (Kind.Term.to_hvm.go term dep)) - -Kind.Book.to_hvm.go -: ∀(book: Kind.Book) - String.Concatenator -= λbook - let P = λx String.Concatenator - let cons = λhead λtail - let P = λx String.Concatenator - let new = λhead.fst λhead.snd λnil - ((Kind.Text.show.go head.fst) - ((Kind.Text.show.go " = " - ((Kind.Term.to_hvm.go head.snd 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) - -Kind.Book.to_hvm -: ∀(book: Kind.Book) - String -= λbook - (String.Concatenator.build (Kind.Book.to_hvm.go book)) - Kind : String = let a = (Kind.lam "f" λf(Kind.lam "x" λx(Kind.app f (Kind.app f x)))) diff --git a/book/Kind.lam.kind2 b/book/Kind.lam.kind2 new file mode 100644 index 00000000..b00ac5f9 --- /dev/null +++ b/book/Kind.lam.kind2 @@ -0,0 +1,7 @@ +Kind.lam +: ∀(nam: String) + ∀(bod: ∀(x: Kind.Term) Kind.Term) + Kind.Term += λnam λbod + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (lam nam bod) \ No newline at end of file diff --git a/book/Kind.mat.kind2 b/book/Kind.mat.kind2 new file mode 100644 index 00000000..64842b61 --- /dev/null +++ b/book/Kind.mat.kind2 @@ -0,0 +1,10 @@ +Kind.mat +: ∀(nam: String) + ∀(x: Kind.Term) + ∀(z: Kind.Term) + ∀(s: ∀(x: Kind.Term) Kind.Term) + ∀(p: ∀(x: Kind.Term) Kind.Term) + Kind.Term += λ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) \ No newline at end of file diff --git a/book/Kind.normal.go.kind2 b/book/Kind.normal.go.kind2 new file mode 100644 index 00000000..cc8b55c5 --- /dev/null +++ b/book/Kind.normal.go.kind2 @@ -0,0 +1,24 @@ +Kind.normal.go +: ∀(maj: Bool) + ∀(term: Kind.Term) + ∀(dep: Nat) + Kind.Term += λmaj λterm λdep + let P = λx Kind.Term + let all = λnam λinp λbod (Kind.all nam (Kind.normal maj inp dep) λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) + let lam = λnam λbod (Kind.lam nam λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) + let app = λfun λarg (Kind.app (Kind.normal maj fun dep) (Kind.normal maj arg dep)) + let ann = λval λtyp (Kind.ann (Kind.normal maj val dep) (Kind.normal maj typ dep)) + let slf = λnam λbod (Kind.slf nam λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) + let ins = λval (Kind.ins (Kind.normal maj val dep)) + let ref = λnam λval (Kind.ref nam (Kind.normal maj val dep)) + let def = λnam λval λbod (Kind.def nam (Kind.normal maj val dep) λx (Kind.normal maj (bod (Kind.var nam dep)) (Nat.succ dep))) + let set = Kind.set + let u60 = Kind.u60 + let num = Kind.num + let op2 = λopr λfst λsnd (Kind.op2 opr (Kind.normal maj fst dep) (Kind.normal maj snd dep)) + let mat = λnam λx λz λs λp (Kind.mat nam (Kind.normal maj x dep) (Kind.normal maj z dep) λk(Kind.normal maj (s (Kind.var nam dep)) (Nat.succ dep)) λk(Kind.normal maj (p (Kind.var nam dep)) (Nat.succ dep))) + let txt = λtxt (Kind.txt txt) + let hol = λnam λctx (Kind.hol nam ctx) + let var = λnam λidx (Kind.var nam idx) + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) \ No newline at end of file diff --git a/book/Kind.normal.kind2 b/book/Kind.normal.kind2 new file mode 100644 index 00000000..577ff323 --- /dev/null +++ b/book/Kind.normal.kind2 @@ -0,0 +1,7 @@ +Kind.normal +: ∀(maj: Bool) + ∀(term: Kind.Term) + ∀(dep: Nat) + Kind.Term += λmaj λterm λdep + (Kind.normal.go maj (Kind.reduce maj term) dep) \ No newline at end of file diff --git a/book/Kind.num.kind2 b/book/Kind.num.kind2 new file mode 100644 index 00000000..57ade955 --- /dev/null +++ b/book/Kind.num.kind2 @@ -0,0 +1,6 @@ +Kind.num +: ∀(val: #U60) + Kind.Term += λval + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (num val) \ No newline at end of file diff --git a/book/Kind.op2.kind2 b/book/Kind.op2.kind2 new file mode 100644 index 00000000..d188ce0c --- /dev/null +++ b/book/Kind.op2.kind2 @@ -0,0 +1,8 @@ +Kind.op2 +: ∀(opr: Kind.Oper) + ∀(fst: Kind.Term) + ∀(snd: Kind.Term) + Kind.Term += λopr λfst λsnd + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (op2 opr fst snd) \ No newline at end of file diff --git a/book/Kind.reduce.app.kind2 b/book/Kind.reduce.app.kind2 new file mode 100644 index 00000000..b6e83466 --- /dev/null +++ b/book/Kind.reduce.app.kind2 @@ -0,0 +1,10 @@ +Kind.reduce.app +: ∀(maj: Bool) + ∀(fun: Kind.Term) + ∀(arg: Kind.Term) + Kind.Term += λmaj λfun λarg + let P = ∀(arg: Kind.Term) Kind.Term + let Y = λnam λbod λarg (Kind.reduce maj (bod (Kind.reduce maj arg))) + let N = λfun λarg (Kind.app fun arg) + (Kind.if.lam fun P Y N arg) \ No newline at end of file diff --git a/book/Kind.reduce.kind2 b/book/Kind.reduce.kind2 new file mode 100644 index 00000000..65897075 --- /dev/null +++ b/book/Kind.reduce.kind2 @@ -0,0 +1,23 @@ +Kind.reduce +: ∀(maj: Bool) + ∀(term: Kind.Term) + Kind.Term += λmaj λterm + let P = λx(Kind.Term) + let all = Kind.all + let lam = Kind.lam + let app = λfun λarg (Kind.reduce.app maj (Kind.reduce maj fun) arg) + let slf = Kind.slf + let ann = λval λtyp (Kind.reduce maj val) + let ins = λval (Kind.reduce maj val) + let ref = λnam λval (Kind.reduce.ref maj nam val) + let def = λnam λval λbod (Kind.reduce maj (bod val)) + let set = Kind.set + let u60 = Kind.u60 + let num = Kind.num + let op2 = λopr λfst λsnd (Kind.reduce.op2 opr fst snd) + let mat = λnam λx λz λs λp (Kind.reduce.mat maj nam x z s p) + let txt = λtxt (Kind.reduce.txt txt) + let hol = Kind.hol + let var = Kind.var + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) \ No newline at end of file diff --git a/book/Kind.reduce.mat.kind2 b/book/Kind.reduce.mat.kind2 new file mode 100644 index 00000000..9cd3d124 --- /dev/null +++ b/book/Kind.reduce.mat.kind2 @@ -0,0 +1,17 @@ +Kind.reduce.mat +: ∀(maj: Bool) + ∀(nam: String) + ∀(x: Kind.Term) + ∀(z: Kind.Term) + ∀(s: ∀(x:Kind.Term)Kind.Term) + ∀(p: ∀(x:Kind.Term)Kind.Term) + Kind.Term += λmaj λnam λx λz λs λp + let P = ∀(z: Kind.Term) ∀(s: ∀(x:Kind.Term)Kind.Term) Kind.Term + let Y = λx.val + #match x = x.val { + #0: λz λs (Kind.reduce maj z) + #+: λz λs (Kind.reduce maj (s (Kind.num x-1))) + }: ∀(z: Kind.Term) ∀(s: ∀(x:Kind.Term)Kind.Term) Kind.Term + let N = λx λz λs (Kind.mat nam x z s p) + ((Kind.if.num x P Y N) z s) \ No newline at end of file diff --git a/book/Kind.reduce.op2.kind2 b/book/Kind.reduce.op2.kind2 new file mode 100644 index 00000000..948c666f --- /dev/null +++ b/book/Kind.reduce.op2.kind2 @@ -0,0 +1,31 @@ +Kind.reduce.op2 +: ∀(opr: Kind.Oper) + ∀(fst: Kind.Term) + ∀(snd: Kind.Term) + Kind.Term += λopr λfst λsnd + let P = ∀(snd: Kind.Term) Kind.Term + let Y = λfst_val λsnd + let P = ∀(fst_val: #U60) Kind.Term + let Y = λsnd_val λfst_val + let P = λx ∀(fst_val: #U60) ∀(snd_val: #U60) Kind.Term + let add = λfst_val λsnd_val (Kind.num #(+ fst_val snd_val)) + let mul = λfst_val λsnd_val (Kind.num #(* fst_val snd_val)) + let sub = λfst_val λsnd_val (Kind.num #(- fst_val snd_val)) + let div = λfst_val λsnd_val (Kind.num #(/ fst_val snd_val)) + let eq = λfst_val λsnd_val (Kind.num #(== fst_val snd_val)) + let ne = λfst_val λsnd_val (Kind.num #(!= fst_val snd_val)) + let lt = λfst_val λsnd_val (Kind.num #(< fst_val snd_val)) + let gt = λfst_val λsnd_val (Kind.num #(> fst_val snd_val)) + let lte = λfst_val λsnd_val (Kind.num #(<= fst_val snd_val)) + let gte = λfst_val λsnd_val (Kind.num #(>= fst_val snd_val)) + let and = λfst_val λsnd_val (Kind.num #(& fst_val snd_val)) + let or = λfst_val λsnd_val (Kind.num #(| fst_val snd_val)) + let xor = λfst_val λsnd_val (Kind.num #(^ fst_val snd_val)) + let lsh = λfst_val λsnd_val (Kind.num #(<< fst_val snd_val)) + let rsh = λfst_val λsnd_val (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 (Kind.op2 opr (Kind.num fst_val) snd) + (Kind.if.num snd P Y N fst_val) + let N = λfst λsnd (Kind.op2 opr fst snd) + (Kind.if.num fst P Y N snd) \ No newline at end of file diff --git a/book/Kind.reduce.ref.kind2 b/book/Kind.reduce.ref.kind2 new file mode 100644 index 00000000..57858cfb --- /dev/null +++ b/book/Kind.reduce.ref.kind2 @@ -0,0 +1,10 @@ +Kind.reduce.ref +: ∀(maj: Bool) + ∀(nam: String) + ∀(val: Kind.Term) + Kind.Term += λmaj λnam λval + let P = λx ∀(nam: String) ∀(val: Kind.Term) Kind.Term + let true = λnam λval (Kind.reduce maj val) + let false = Kind.ref + (~maj P true false nam val) \ No newline at end of file diff --git a/book/Kind.reduce.txt.kind2 b/book/Kind.reduce.txt.kind2 new file mode 100644 index 00000000..6363a6aa --- /dev/null +++ b/book/Kind.reduce.txt.kind2 @@ -0,0 +1,8 @@ +Kind.reduce.txt +: ∀(txt: Kind.Text) + Kind.Term += λtxt + let P = λx Kind.Term + let cons = λx λxs (Kind.reduce Bool.true (Kind.app (Kind.app Kind.Book.String.cons (Kind.num x)) (Kind.txt xs))) + let nil = (Kind.reduce Bool.true Kind.Book.String.nil) + (~txt P cons nil) \ No newline at end of file diff --git a/book/Kind.ref.kind2 b/book/Kind.ref.kind2 new file mode 100644 index 00000000..d3e8cfdf --- /dev/null +++ b/book/Kind.ref.kind2 @@ -0,0 +1,7 @@ +Kind.ref +: ∀(nam: String) + ∀(val: Kind.Term) + Kind.Term += λnam λval + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (ref nam val) \ No newline at end of file diff --git a/book/Kind.report.kind2 b/book/Kind.report.kind2 new file mode 100644 index 00000000..d7cde5e7 --- /dev/null +++ b/book/Kind.report.kind2 @@ -0,0 +1,14 @@ +Kind.report +: ∀(e: Bool) + ∀(inferred: Kind.Term) + ∀(expected: Kind.Term) + ∀(value: Kind.Term) + ∀(dep: Nat) + (Maybe Kind.Term) += λe λinferred λexpected λvalue λdep + let pure = (Maybe.some Kind.Term) + let none = (Maybe.none Kind.Term) + let P = λx ∀(inferred: Kind.Term) ∀(expected: Kind.Term) ∀(value: Kind.Term) ∀(dep: Nat) (Maybe Kind.Term) + let true = λinferred λexpected λvalue λdep (pure Kind.set) + let false = λinferred λexpected λvalue λdep none // TODO: HVM.log error + (~e P true false inferred expected value dep) \ No newline at end of file diff --git a/book/Kind.set.kind2 b/book/Kind.set.kind2 new file mode 100644 index 00000000..3e3d46e4 --- /dev/null +++ b/book/Kind.set.kind2 @@ -0,0 +1,4 @@ +Kind.set +: Kind.Term += ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (set) \ No newline at end of file diff --git a/book/Kind.skip.kind2 b/book/Kind.skip.kind2 new file mode 100644 index 00000000..99525baa --- /dev/null +++ b/book/Kind.skip.kind2 @@ -0,0 +1,22 @@ +Kind.skip +: ∀(x: Kind.Term) + Kind.Term += λx + let P = λx Kind.Term + let all = Kind.all + let lam = Kind.lam + let app = Kind.app + let ann = λval λtyp (Kind.skip val) + let slf = Kind.slf + let ins = λval (Kind.skip val) + let ref = Kind.ref + let def = λnam λval λbod (Kind.skip (bod val)) + let set = Kind.set + let u60 = Kind.u60 + let num = Kind.num + let op2 = Kind.op2 + let mat = Kind.mat + let txt = Kind.txt + let hol = Kind.hol + let var = Kind.var + (~x P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) \ No newline at end of file diff --git a/book/Kind.slf.kind2 b/book/Kind.slf.kind2 new file mode 100644 index 00000000..425105ba --- /dev/null +++ b/book/Kind.slf.kind2 @@ -0,0 +1,7 @@ +Kind.slf +: ∀(nam: String) + ∀(bod: ∀(x: Kind.Term) Kind.Term) + Kind.Term += λnam λbod + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (slf nam bod) \ No newline at end of file diff --git a/book/Kind.txt.kind2 b/book/Kind.txt.kind2 new file mode 100644 index 00000000..0d4d17de --- /dev/null +++ b/book/Kind.txt.kind2 @@ -0,0 +1,6 @@ +Kind.txt +: ∀(lit: Kind.Text) + Kind.Term += λlit + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (txt lit) \ No newline at end of file diff --git a/book/Kind.u60.kind2 b/book/Kind.u60.kind2 new file mode 100644 index 00000000..7e2db33d --- /dev/null +++ b/book/Kind.u60.kind2 @@ -0,0 +1,4 @@ +Kind.u60 +: Kind.Term += ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + u60 \ No newline at end of file diff --git a/book/Kind.var.kind2 b/book/Kind.var.kind2 new file mode 100644 index 00000000..d519fe93 --- /dev/null +++ b/book/Kind.var.kind2 @@ -0,0 +1,7 @@ +Kind.var +: ∀(nam: String) + ∀(idx: Nat) + Kind.Term += λnam λidx + ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar + (var nam idx) \ No newline at end of file diff --git a/book/Kind.verify.kind2 b/book/Kind.verify.kind2 new file mode 100644 index 00000000..4991b030 --- /dev/null +++ b/book/Kind.verify.kind2 @@ -0,0 +1,11 @@ +Kind.verify +: ∀(term: Kind.Term) + ∀(type: Kind.Term) + ∀(dep: Nat) + (Maybe Kind.Term) += λterm λtype λdep + let bind = (Maybe.bind Kind.Term Kind.Term) + let pure = (Maybe.some Kind.Term) + let none = (Maybe.none Kind.Term) + (bind (Kind.infer term dep) λinfer + (Kind.report (Kind.equal infer type dep) infer type term dep)) \ No newline at end of file diff --git a/book/Parser.Guard.get.kind2 b/book/Parser.Guard.get.kind2 new file mode 100644 index 00000000..5732b115 --- /dev/null +++ b/book/Parser.Guard.get.kind2 @@ -0,0 +1,7 @@ +Parser.Guard.get +: ∀(A: *) + ∀(p: (Parser.Guard A)) + ∀(P: *) + ∀(f: ∀(a: (Parser Bool)) ∀(b: (Parser A)) P) + P += λA (Pair.get (Parser Bool) (Parser A)) \ No newline at end of file diff --git a/book/Parser.Guard.kind2 b/book/Parser.Guard.kind2 new file mode 100644 index 00000000..1c5a524d --- /dev/null +++ b/book/Parser.Guard.kind2 @@ -0,0 +1,3 @@ +Parser.Guard +: ∀(A: *) * += λA (Pair (Parser Bool) (Parser A)) \ No newline at end of file diff --git a/book/Parser.Guard.new.kind2 b/book/Parser.Guard.new.kind2 new file mode 100644 index 00000000..dfde6735 --- /dev/null +++ b/book/Parser.Guard.new.kind2 @@ -0,0 +1,6 @@ +Parser.Guard.new +: ∀(A: *) + ∀(guard: (Parser Bool)) + ∀(value: (Parser A)) + (Parser.Guard A) += λA (Pair.new (Parser Bool) (Parser A)) \ No newline at end of file diff --git a/book/Parser.Guard.pass.kind2 b/book/Parser.Guard.pass.kind2 new file mode 100644 index 00000000..95a13428 --- /dev/null +++ b/book/Parser.Guard.pass.kind2 @@ -0,0 +1,6 @@ +Parser.Guard.pass +: ∀(A: *) + ∀(then: (Parser A)) + (Parser.Guard A) += λA λthen + (Parser.Guard.new A (Parser.pure Bool Bool.true) then) \ No newline at end of file diff --git a/book/Parser.Guard.text.kind2 b/book/Parser.Guard.text.kind2 new file mode 100644 index 00000000..90359423 --- /dev/null +++ b/book/Parser.Guard.text.kind2 @@ -0,0 +1,7 @@ +Parser.Guard.text +: ∀(A: *) + ∀(text: String) + ∀(then: (Parser A)) + (Parser.Guard A) += λA λtext λthen + (Parser.Guard.new A (Parser.skip Bool (Parser.test text)) then) \ No newline at end of file diff --git a/book/Parser.Result.done.kind2 b/book/Parser.Result.done.kind2 new file mode 100644 index 00000000..fae46bab --- /dev/null +++ b/book/Parser.Result.done.kind2 @@ -0,0 +1,8 @@ +Parser.Result.done +: ∀(T: *) + ∀(code: String) + ∀(value: T) + (Parser.Result T) += λT λcode λvalue + ~λP λdone λfail + (done code value) \ No newline at end of file diff --git a/book/Parser.Result.fail.kind2 b/book/Parser.Result.fail.kind2 new file mode 100644 index 00000000..d87a8ff4 --- /dev/null +++ b/book/Parser.Result.fail.kind2 @@ -0,0 +1,7 @@ +Parser.Result.fail +: ∀(T: *) + ∀(error: String) + (Parser.Result T) += λT λerror + ~λP λdone λfail + (fail error) \ No newline at end of file diff --git a/book/Parser.Result.kind2 b/book/Parser.Result.kind2 new file mode 100644 index 00000000..2344dd3f --- /dev/null +++ b/book/Parser.Result.kind2 @@ -0,0 +1,9 @@ +Parser.Result +: ∀(T: *) + * += λT + $self + ∀(P: ∀(x: (Parser.Result T)) *) + ∀(done: ∀(code: String) ∀(value: T) (P (Parser.Result.done T code value))) + ∀(fail: ∀(error: String) (P (Parser.Result.fail T error))) + (P self) \ No newline at end of file diff --git a/book/Parser.bind.kind2 b/book/Parser.bind.kind2 new file mode 100644 index 00000000..c87b1687 --- /dev/null +++ b/book/Parser.bind.kind2 @@ -0,0 +1,12 @@ +Parser.bind +: ∀(A: *) + ∀(B: *) + ∀(a: (Parser A)) + ∀(b: ∀(x: A) (Parser B)) + (Parser B) += λA λB λa λb + λcode + let P = λx ∀(b: ∀(x: A) (Parser B)) (Parser.Result B) + let done = λa.code λa.value λb (b a.value a.code) + let fail = λa.error λb (Parser.Result.fail B a.error) + (~(a code) P done fail b) diff --git a/book/Parser.char.kind2 b/book/Parser.char.kind2 new file mode 100644 index 00000000..06c68155 --- /dev/null +++ b/book/Parser.char.kind2 @@ -0,0 +1,11 @@ +Parser.char +: (Parser Char) += λcode + let P = λx(Parser.Result Char) + let cons = λhead λtail + let P = λx(Parser.Result Char) + let true = (Parser.Result.done Char tail head) // TODO + let false = (Parser.Result.done Char tail head) + (~(Char.is_slash head) P true false) + let nil = (Parser.Result.fail Char "eof") + (~code P cons nil) \ No newline at end of file diff --git a/book/Parser.decimal.kind2 b/book/Parser.decimal.kind2 new file mode 100644 index 00000000..546af5e7 --- /dev/null +++ b/book/Parser.decimal.kind2 @@ -0,0 +1,3 @@ +Parser.decimal +: (Parser String) += (Parser.pick_while Char.is_decimal) \ No newline at end of file diff --git a/book/Parser.fail.kind2 b/book/Parser.fail.kind2 new file mode 100644 index 00000000..49adff29 --- /dev/null +++ b/book/Parser.fail.kind2 @@ -0,0 +1,6 @@ +Parser.fail +: ∀(A: *) + ∀(error: String) + (Parser A) += λT λerror λcode + (Parser.Result.fail T error) \ No newline at end of file diff --git a/book/Parser.is_eof.kind2 b/book/Parser.is_eof.kind2 new file mode 100644 index 00000000..586eb3d7 --- /dev/null +++ b/book/Parser.is_eof.kind2 @@ -0,0 +1,7 @@ +Parser.is_eof +: (Parser Bool) += λcode + let P = λx(Parser.Result Bool) + let cons = λcode.head λcode.tail (Parser.Result.done Bool (String.cons code.head code.tail) Bool.false) + let nil = (Parser.Result.done Bool String.nil Bool.true) + (~(String.skip code) P cons nil) \ No newline at end of file diff --git a/book/Parser.kind2 b/book/Parser.kind2 index 3325433c..434f05ae 100644 --- a/book/Parser.kind2 +++ b/book/Parser.kind2 @@ -3,310 +3,3 @@ Parser = λA ∀(code: String) (Parser.Result A) - -// TODO: abstract error type -Parser.Result -: ∀(T: *) - * -= λT - $self - ∀(P: ∀(x: (Parser.Result T)) *) - ∀(done: ∀(code: String) ∀(value: T) (P (Parser.Result.done T code value))) - ∀(fail: ∀(error: String) (P (Parser.Result.fail T error))) - (P self) - -Parser.Result.done -: ∀(T: *) - ∀(code: String) - ∀(value: T) - (Parser.Result T) -= λT λcode λvalue - ~λP λdone λfail - (done code value) - -Parser.Result.fail -: ∀(T: *) - ∀(error: String) - (Parser.Result T) -= λT λerror - ~λP λdone λfail - (fail error) - -Parser.Guard -: ∀(A: *) * -= λA (Pair (Parser Bool) (Parser A)) - -Parser.Guard.new -: ∀(A: *) - ∀(guard: (Parser Bool)) - ∀(value: (Parser A)) - (Parser.Guard A) -= λA (Pair.new (Parser Bool) (Parser A)) - -Parser.Guard.get -: ∀(A: *) - ∀(p: (Parser.Guard A)) - ∀(P: *) - ∀(f: ∀(a: (Parser Bool)) ∀(b: (Parser A)) P) - P -= λA (Pair.get (Parser Bool) (Parser A)) - -// Creates a guard that skips the condition. -Parser.Guard.pass -: ∀(A: *) - ∀(then: (Parser A)) - (Parser.Guard A) -= λA λthen - (Parser.Guard.new A (Parser.pure Bool Bool.true) then) - -// Guards a parser with a simple text. -Parser.Guard.text -: ∀(A: *) - ∀(text: String) - ∀(then: (Parser A)) - (Parser.Guard A) -= λA λtext λthen - (Parser.Guard.new A (Parser.skip Bool (Parser.test text)) then) - -Parser.pure -: ∀(A: *) - ∀(value: A) - (Parser A) -= λA λvalue λcode - (Parser.Result.done A code value) - -Parser.bind -: ∀(A: *) - ∀(B: *) - ∀(a: (Parser A)) - ∀(b: ∀(x: A) (Parser B)) - (Parser B) -= λA λB λa λb - λcode - let P = λx ∀(b: ∀(x: A) (Parser B)) (Parser.Result B) - let done = λa.code λa.value λb (b a.value a.code) - let fail = λa.error λb (Parser.Result.fail B a.error) - (~(a code) P done fail b) - -Parser.fail -: ∀(A: *) - ∀(error: String) - (Parser A) -= λT λerror λcode - (Parser.Result.fail T error) - -//Parser.run -//: ∀(A: *) - //∀(parser: (Parser A)) - //∀(code: String) - //∀(default: A) - //A -//= λA λparser λcode λfail - //let P = λx(A) - //let done = λcode λvalue value - //let fail = default - //(~(parser code) P done fail) - -Parser.skip -: ∀(A: *) - ∀(parser: (Parser A)) - (Parser A) -= λA λparser λcode - (parser (String.skip code)) - -// Takes characters while a condition is true. -Parser.pick_while -: ∀(cond: ∀(chr: Char) Bool) - (Parser String) -= λcond λcode (Parser.pick_while.go cond code) - -Parser.pick_while.go -: ∀(cond: ∀(chr: Char) Bool) - (Parser String) -= λcond λcode - let P = λx(Parser.Result String) - let cons = λhead λtail - let P = λx ∀(head: Char) ∀(tail: String) (Parser.Result String) - let true = λhead λtail - let P = λx (Parser.Result String) - let done = λcode λvalue (Parser.Result.done String code (String.cons head value)) - let fail = λerror (Parser.Result.fail String error) - (~(Parser.pick_while.go cond tail) P done fail) - let false = λhead λtail - (Parser.Result.done String (String.cons head tail) String.nil) - (~(cond head) P true false head tail) - let nil = - (Parser.Result.done String String.nil String.nil) - (~code P cons nil) - -// Parses a sequence of name-valid characters. -Parser.name -: (Parser String) -= (Parser.pick_while Char.is_name) - -// Parses a sequence of oper-valid characters. -Parser.oper -: (Parser String) -= (Parser.pick_while Char.is_oper) - -// Parses a sequence of decimal characters. -Parser.decimal -: (Parser String) -= (Parser.pick_while Char.is_decimal) - -// Checks if the next character is EOF. -Parser.is_eof -: (Parser Bool) -= λcode - let P = λx(Parser.Result Bool) - let cons = λcode.head λcode.tail (Parser.Result.done Bool (String.cons code.head code.tail) Bool.false) - let nil = (Parser.Result.done Bool String.nil Bool.true) - (~(String.skip code) P cons nil) - -// Checks if the next characteres match given text. -Parser.test -: ∀(test: String) - (Parser Bool) -= λtest λcode - // Gets the first expected character. - let P = λx ∀(code: String) (Parser.Result Bool) - let cons = λtest.head λtest.tail λcode - // Gets the first detected character. - let P = λx (Parser.Result Bool) - let cons = λcode.head λcode.tail - // Checks if expected == detected. - let P = λx ∀(code.head: Char) ∀(code.tail: String) (Parser.Result Bool) - let true = λcode.head λcode.tail - // If so, parses the next character and reconstructs the original code. - let P = λx(Parser.Result Bool) - let done = λcode λvalue (Parser.Result.done Bool (String.cons code.head code) value) - let fail = λerror (Parser.Result.fail Bool error) - (~(Parser.test test.tail code.tail) P done fail) - let false = λcode.head λcode.tail - // Otherwise, returns false and reconstructs the original code. - (Parser.Result.done Bool (String.cons code.head code.tail) Bool.false) - ((~(Char.equal test.head code.head) P true false) code.head code.tail) - let nil = (Parser.Result.done Bool String.nil Bool.false) - (~code P cons nil) - let nil = λcode (Parser.Result.done Bool code Bool.true) - (~test P cons nil code) - -// Parses an exact text. -// - If successful, consumes text. -// - Otherwise, throws. -Parser.text -: ∀(text: String) - (Parser Unit) -= λtext - (Parser.skip Unit - (Parser.bind Bool Unit (Parser.test text) λsuccess - (Bool.if success (Parser Unit) - // then - (Parser.bind String Unit (Parser.take (String.length text)) λx - (Parser.pure Unit Unit.one)) - // else - (Parser.fail Unit "error")))) - -// Repeats a parser N times. -Parser.repeat -: ∀(n: Nat) - ∀(A: *) - ∀(p: (Parser A)) - (Parser (List A)) -= λn λA λp - let P = λx (Parser (List A)) - let succ = λn.pred - (Parser.bind A (List A) p λhead - (Parser.bind (List A) (List A) (Parser.repeat n.pred A p) λtail - (Parser.pure (List A) (List.cons A head tail)))) - let zero = (Parser.pure (List A) (List.nil A)) - (~n P succ zero) - -// Picks a single character. -Parser.pick -: (Parser Char) -= λcode - let P = λx(Parser.Result Char) - let cons = λhead λtail (Parser.Result.done Char tail head) - let nil = (Parser.Result.fail Char "empty") - (~code P cons nil) - -// Takes a string. -Parser.take -: ∀(n: Nat) - (Parser String) -= λn (Parser.repeat n Char Parser.pick) - -// Attempts to parse one of multiple variants. -// - Each variant is guarded by a (Parser Bool). -// - If the guard succeeds, we parse that variant. -// - Otherwise, we try the next variant. -Parser.variant -: ∀(A: *) - ∀(variants: (List (Parser.Guard A))) - (Parser A) -= λA λvariants - let P = λx(Parser A) - let cons = λvariant λothers - (Pair.get (Parser Bool) (Parser A) variant (Parser A) λguard λparser - (Parser.bind Bool A guard λsuccess - (Bool.if success (Parser A) parser (Parser.variant A others)))) - let nil = (Parser.fail A "error") - (~variants P cons nil) - -// TODO: parse escape sequences. -Parser.char -: (Parser Char) -= λcode - let P = λx(Parser.Result Char) - let cons = λhead λtail - let P = λx(Parser.Result Char) - let true = (Parser.Result.done Char tail head) // TODO - let false = (Parser.Result.done Char tail head) - (~(Char.is_slash head) P true false) - let nil = (Parser.Result.fail Char "eof") - (~code P cons nil) - -// Applies a function to a parsed value. -Parser.map -: ∀(A: *) - ∀(B: *) - ∀(f: ∀(a: A) B) - ∀(p: (Parser A)) - (Parser B) -= λA λB λf λp λcode - let P = λx(Parser.Result B) - let done = λcode λvalue (Parser.Result.done B code (f value)) - let fail = λerror (Parser.Result.fail B error) - (~(p code) P done fail) - -// Parses repeatedly until a terminator parser succeeds. -Parser.until -: ∀(A: *) - ∀(until: (Parser Bool)) - ∀(parse: (Parser A)) - (Parser (List A)) -= λA λuntil λparse - (Parser.map (List.Concatenator A) (List A) (List.Concatenator.build A) - (Parser.until.go A until parse λx(x))) - -Parser.until.go -: ∀(A: *) - ∀(until: (Parser Bool)) - ∀(parse: (Parser A)) - ∀(terms: (List.Concatenator A)) - (Parser (List.Concatenator A)) -= λA λuntil λparse λterms λcode - let P = λx(Parser.Result (List.Concatenator A)) - let done = λcode λstop - let P = λx ∀(code: String) (Parser.Result (List.Concatenator A)) - let true = λcode - (Parser.Result.done (List.Concatenator A) code terms) - let false = λcode - let P = λx (Parser.Result (List.Concatenator A)) - let done = λcode λvalue (Parser.until.go A until parse λx(terms (List.cons A value x)) code) - let fail = λerror (Parser.Result.fail (List.Concatenator A) error) - (~(parse code) P done fail) - ((~stop P true false) code) - let fail = λerror (Parser.Result.fail (List.Concatenator A) error) - (~(until code) P done fail) diff --git a/book/Parser.map.kind2 b/book/Parser.map.kind2 new file mode 100644 index 00000000..f53c2573 --- /dev/null +++ b/book/Parser.map.kind2 @@ -0,0 +1,11 @@ +Parser.map +: ∀(A: *) + ∀(B: *) + ∀(f: ∀(a: A) B) + ∀(p: (Parser A)) + (Parser B) += λA λB λf λp λcode + let P = λx(Parser.Result B) + let done = λcode λvalue (Parser.Result.done B code (f value)) + let fail = λerror (Parser.Result.fail B error) + (~(p code) P done fail) \ No newline at end of file diff --git a/book/Parser.name.kind2 b/book/Parser.name.kind2 new file mode 100644 index 00000000..16f481ef --- /dev/null +++ b/book/Parser.name.kind2 @@ -0,0 +1,3 @@ +Parser.name +: (Parser String) += (Parser.pick_while Char.is_name) \ No newline at end of file diff --git a/book/Parser.oper.kind2 b/book/Parser.oper.kind2 new file mode 100644 index 00000000..7039b3ae --- /dev/null +++ b/book/Parser.oper.kind2 @@ -0,0 +1,3 @@ +Parser.oper +: (Parser String) += (Parser.pick_while Char.is_oper) \ No newline at end of file diff --git a/book/Parser.pick.kind2 b/book/Parser.pick.kind2 new file mode 100644 index 00000000..5b11af8a --- /dev/null +++ b/book/Parser.pick.kind2 @@ -0,0 +1,7 @@ +Parser.pick +: (Parser Char) += λcode + let P = λx(Parser.Result Char) + let cons = λhead λtail (Parser.Result.done Char tail head) + let nil = (Parser.Result.fail Char "empty") + (~code P cons nil) \ No newline at end of file diff --git a/book/Parser.pick_while.go.kind2 b/book/Parser.pick_while.go.kind2 new file mode 100644 index 00000000..c8e0beae --- /dev/null +++ b/book/Parser.pick_while.go.kind2 @@ -0,0 +1,18 @@ +Parser.pick_while.go +: ∀(cond: ∀(chr: Char) Bool) + (Parser String) += λcond λcode + let P = λx(Parser.Result String) + let cons = λhead λtail + let P = λx ∀(head: Char) ∀(tail: String) (Parser.Result String) + let true = λhead λtail + let P = λx (Parser.Result String) + let done = λcode λvalue (Parser.Result.done String code (String.cons head value)) + let fail = λerror (Parser.Result.fail String error) + (~(Parser.pick_while.go cond tail) P done fail) + let false = λhead λtail + (Parser.Result.done String (String.cons head tail) String.nil) + (~(cond head) P true false head tail) + let nil = + (Parser.Result.done String String.nil String.nil) + (~code P cons nil) \ No newline at end of file diff --git a/book/Parser.pick_while.kind2 b/book/Parser.pick_while.kind2 new file mode 100644 index 00000000..8e060728 --- /dev/null +++ b/book/Parser.pick_while.kind2 @@ -0,0 +1,4 @@ +Parser.pick_while +: ∀(cond: ∀(chr: Char) Bool) + (Parser String) += λcond λcode (Parser.pick_while.go cond code) \ No newline at end of file diff --git a/book/Parser.pure.kind2 b/book/Parser.pure.kind2 new file mode 100644 index 00000000..16d7c3ae --- /dev/null +++ b/book/Parser.pure.kind2 @@ -0,0 +1,6 @@ +Parser.pure +: ∀(A: *) + ∀(value: A) + (Parser A) += λA λvalue λcode + (Parser.Result.done A code value) \ No newline at end of file diff --git a/book/Parser.repeat.kind2 b/book/Parser.repeat.kind2 new file mode 100644 index 00000000..67116f49 --- /dev/null +++ b/book/Parser.repeat.kind2 @@ -0,0 +1,13 @@ +Parser.repeat +: ∀(n: Nat) + ∀(A: *) + ∀(p: (Parser A)) + (Parser (List A)) += λn λA λp + let P = λx (Parser (List A)) + let succ = λn.pred + (Parser.bind A (List A) p λhead + (Parser.bind (List A) (List A) (Parser.repeat n.pred A p) λtail + (Parser.pure (List A) (List.cons A head tail)))) + let zero = (Parser.pure (List A) (List.nil A)) + (~n P succ zero) \ No newline at end of file diff --git a/book/Parser.skip.kind2 b/book/Parser.skip.kind2 new file mode 100644 index 00000000..2985ad9b --- /dev/null +++ b/book/Parser.skip.kind2 @@ -0,0 +1,6 @@ +Parser.skip +: ∀(A: *) + ∀(parser: (Parser A)) + (Parser A) += λA λparser λcode + (parser (String.skip code)) \ No newline at end of file diff --git a/book/Parser.take.kind2 b/book/Parser.take.kind2 new file mode 100644 index 00000000..500dca69 --- /dev/null +++ b/book/Parser.take.kind2 @@ -0,0 +1,4 @@ +Parser.take +: ∀(n: Nat) + (Parser String) += λn (Parser.repeat n Char Parser.pick) \ No newline at end of file diff --git a/book/Parser.test.kind2 b/book/Parser.test.kind2 new file mode 100644 index 00000000..89cd0860 --- /dev/null +++ b/book/Parser.test.kind2 @@ -0,0 +1,26 @@ +Parser.test +: ∀(test: String) + (Parser Bool) += λtest λcode + // Gets the first expected character. + let P = λx ∀(code: String) (Parser.Result Bool) + let cons = λtest.head λtest.tail λcode + // Gets the first detected character. + let P = λx (Parser.Result Bool) + let cons = λcode.head λcode.tail + // Checks if expected == detected. + let P = λx ∀(code.head: Char) ∀(code.tail: String) (Parser.Result Bool) + let true = λcode.head λcode.tail + // If so, parses the next character and reconstructs the original code. + let P = λx(Parser.Result Bool) + let done = λcode λvalue (Parser.Result.done Bool (String.cons code.head code) value) + let fail = λerror (Parser.Result.fail Bool error) + (~(Parser.test test.tail code.tail) P done fail) + let false = λcode.head λcode.tail + // Otherwise, returns false and reconstructs the original code. + (Parser.Result.done Bool (String.cons code.head code.tail) Bool.false) + ((~(Char.equal test.head code.head) P true false) code.head code.tail) + let nil = (Parser.Result.done Bool String.nil Bool.false) + (~code P cons nil) + let nil = λcode (Parser.Result.done Bool code Bool.true) + (~test P cons nil code) \ No newline at end of file diff --git a/book/Parser.text.kind2 b/book/Parser.text.kind2 new file mode 100644 index 00000000..17f0240a --- /dev/null +++ b/book/Parser.text.kind2 @@ -0,0 +1,12 @@ +Parser.text +: ∀(text: String) + (Parser Unit) += λtext + (Parser.skip Unit + (Parser.bind Bool Unit (Parser.test text) λsuccess + (Bool.if success (Parser Unit) + // then + (Parser.bind String Unit (Parser.take (String.length text)) λx + (Parser.pure Unit Unit.one)) + // else + (Parser.fail Unit "error")))) \ No newline at end of file diff --git a/book/Parser.until.go.kind2 b/book/Parser.until.go.kind2 new file mode 100644 index 00000000..da937052 --- /dev/null +++ b/book/Parser.until.go.kind2 @@ -0,0 +1,20 @@ +Parser.until.go +: ∀(A: *) + ∀(until: (Parser Bool)) + ∀(parse: (Parser A)) + ∀(terms: (List.Concatenator A)) + (Parser (List.Concatenator A)) += λA λuntil λparse λterms λcode + let P = λx(Parser.Result (List.Concatenator A)) + let done = λcode λstop + let P = λx ∀(code: String) (Parser.Result (List.Concatenator A)) + let true = λcode + (Parser.Result.done (List.Concatenator A) code terms) + let false = λcode + let P = λx (Parser.Result (List.Concatenator A)) + let done = λcode λvalue (Parser.until.go A until parse λx(terms (List.cons A value x)) code) + let fail = λerror (Parser.Result.fail (List.Concatenator A) error) + (~(parse code) P done fail) + ((~stop P true false) code) + let fail = λerror (Parser.Result.fail (List.Concatenator A) error) + (~(until code) P done fail) diff --git a/book/Parser.until.kind2 b/book/Parser.until.kind2 new file mode 100644 index 00000000..8e0480a2 --- /dev/null +++ b/book/Parser.until.kind2 @@ -0,0 +1,8 @@ +Parser.until +: ∀(A: *) + ∀(until: (Parser Bool)) + ∀(parse: (Parser A)) + (Parser (List A)) += λA λuntil λparse + (Parser.map (List.Concatenator A) (List A) (List.Concatenator.build A) + (Parser.until.go A until parse λx(x))) \ No newline at end of file diff --git a/book/Parser.variant.kind2 b/book/Parser.variant.kind2 new file mode 100644 index 00000000..bd723268 --- /dev/null +++ b/book/Parser.variant.kind2 @@ -0,0 +1,12 @@ +Parser.variant +: ∀(A: *) + ∀(variants: (List (Parser.Guard A))) + (Parser A) += λA λvariants + let P = λx(Parser A) + let cons = λvariant λothers + (Pair.get (Parser Bool) (Parser A) variant (Parser A) λguard λparser + (Parser.bind Bool A guard λsuccess + (Bool.if success (Parser A) parser (Parser.variant A others)))) + let nil = (Parser.fail A "error") + (~variants P cons nil) \ No newline at end of file diff --git a/book/_OBLITERATE.kind2 b/book/_OBLITERATE.kind2 new file mode 100644 index 00000000..8d35b3fd --- /dev/null +++ b/book/_OBLITERATE.kind2 @@ -0,0 +1,59 @@ +// Bool : * = ∀(P: *) ∀(s: P) ∀(z: P) P +_BOOL = Kind.set +_Bool = (Kind.all "P" Kind.set λP(Kind.all "t" P λt(Kind.all "f" P λf(P)))) + +// True : Bool = λP λt λf t +_TRUE = _Bool +_True = (Kind.lam "P" λP(Kind.lam "t" λt(Kind.lam "f" λf(t)))) + +// False : Bool = λP λt λf f +_FALSE = _Bool +_False = (Kind.lam "P" λP(Kind.lam "t" λt(Kind.lam "f" λf(f)))) + +// AND : ∀(x: Bool) ∀(y: Bool) Bool = λx λy (x Bool y False) +_AND = (Kind.all "x" _Bool λx(Kind.all "y" _Bool λy(_Bool))) +_and = (Kind.lam "x" λx(Kind.lam "y" λy(Kind.app (Kind.app (Kind.app x _Bool) y) _False))) + +// Nat : * = ∀(P: *) ∀(s: ∀(x: P) P) ∀(z: P) P +_NAT = Kind.set +_Nat = (Kind.all "P" Kind.set λP(Kind.all "s" (Kind.all "x" P λx(P)) λs(Kind.all "z" P λz(P)))) + +// 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))))) + +// C4 : Nat = λs λz (s (s (s (s z)))) +_C4 = _Nat +_c4 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s (Kind.app s (Kind.app s z))))))) + +// Equal : ∀(A: *) ∀(a: A) ∀(b: A) * = λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b) +_EQUAL = (Kind.all "P" Kind.set λA(Kind.all "a" A λa(Kind.all "b" A λb(Kind.set)))) +_Equal = (Kind.lam "A" λA(Kind.lam "a" λa(Kind.lam "b" λb(Kind.all "P" (Kind.all "x" A λx(Kind.set)) λP(Kind.all "p" (Kind.app P a) λp(Kind.app P b)))))) + +// refl : ∀(A: *) ∀(a: A) (Equal A a a) = λA λa λP λp p +_REFL = (Kind.all "A" Kind.set λA(Kind.all "a" A λa(Kind.app (Kind.app (Kind.app _Equal A) a) a))) +_refl = (Kind.lam "A" λA(Kind.lam "a" λa(Kind.lam "P" λP(Kind.lam "p" λp p)))) + +// WORK : ∀(n: Nat) Bool = λn (n ∀(x:Bool)Bool λpλb(Bool.and (p b) (p b)) λx(x) True) +_WORK = (Kind.all "n" _Nat λn(_Bool)) +_work = (Kind.lam "n" λn(Kind.app (Kind.app (Kind.app (Kind.app n (Kind.all "x" _Bool λx(_Bool))) + (Kind.lam "p" λp(Kind.lam "b" λb(Kind.app (Kind.app (Kind.ann _and _AND) (Kind.app p b)) (Kind.app p b))))) + (Kind.lam "x" λx(x))) + _True)) + +// RESULT : Bool = (work c3) +_RESULT = _Bool +_result = (Kind.app (Kind.ann _work _WORK) (Kind.app (Kind.app _exp _c2) _c4)) + +// MAIN : (Equal Bool result True) = λP λrefl refl +_MAIN = (Kind.app (Kind.app (Kind.app _Equal _Bool) _result) _True) +_main = (Kind.lam "P" λP(Kind.lam "refl" λrefl(refl))) + +// Checks if `(work 2^4)` is propositionally equal to `true` +_OBLITERATE +: String += (~(Kind.check _main _MAIN Nat.zero) λx(String) λt("check") "error") diff --git a/book/test7.kind2 b/book/test7.kind2 index d8ce0f1e..70bb132f 100644 --- a/book/test7.kind2 +++ b/book/test7.kind2 @@ -1,31 +1,7 @@ -BOOK +test7.book : String -= ` -Kind -: String -= let a = (Kind.lam "f" λf(Kind.lam "x" λx(Kind.app f (Kind.app f x)))) - let b = (Kind.lam "f" λf(Kind.lam "x" λx(Kind.app f (Kind.app f x)))) - - let Test = - (Kind.all "A" Kind.set λA - (Kind.all "B" Kind.set λB - (Kind.all "a" A λa - (Kind.all "b" B λb - B)))) - let test = - (Kind.lam "A" λA - (Kind.lam "B" λB - (Kind.lam "a" λa - (Kind.lam "b" λb - b)))) - - let P = λx(String) - let some = λvalue (Kind.Term.show value Nat.zero) - let none = "error" - let chk = (Kind.check test Test Nat.zero) - (~chk P some none) -` += `Test : Kind.Term = (Kind.lam "f" λf(Kind.lam "x" λx(Kind.app f (Kind.app f x))))` test7 : String -= (Kind.Book.to_hvm (Kind.Book.parse BOOK)) += (Kind.Book.to_hvm (Kind.Book.parse test7.book))