HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-07-14 22:50:28 +03:00
Code Issues Packages Projects Releases Wiki Activity

split files and add OBLITERATE

Browse Source
This commit is contained in:
Victor Taelin 2024-02-20 19:23:15 -03:00
parent 9c1a3f16a0
commit 37fb440ea9
148 changed files with 1929 additions and 2072 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
book/Kind.Binder.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Binder
: *
= (Pair String Kind.Term)

5
book/Kind.Binder.new.kind2 Normal file
View File

@ -0,0 +1,5 @@
Kind.Binder.new
: ∀(nam: String) ∀(typ: Kind.Term)
Kind.Binder
= λnam λtyp
(Pair.new String Kind.Term nam typ)

3
book/Kind.Book.String.cons.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Book.String.cons
: Kind.Term
= (Kind.hol "TODO" (List.nil Kind.Term))

3
book/Kind.Book.String.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Book.String
: Kind.Term
= (Kind.hol "TODO" (List.nil Kind.Term))

3
book/Kind.Book.String.nil.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Book.String.nil
: Kind.Term
= (Kind.hol "TODO" (List.nil Kind.Term))

3
book/Kind.Book.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Book
: *
= (String.Map Kind.Term)

8
book/Kind.Book.parse.kind2 Normal file
View File

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

28
book/Kind.Book.parser.kind2 Normal file
View File

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

17
book/Kind.Book.show.go.kind2 Normal file
View File

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

5
book/Kind.Book.show.kind2 Normal file
View File

@ -0,0 +1,5 @@
Kind.Book.show
: ∀(book: Kind.Book)
String
= λbook
(String.Concatenator.build (Kind.Book.show.go book))

17
book/Kind.Book.to_hvm.go.kind2 Normal file
View File

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

5
book/Kind.Book.to_hvm.kind2 Normal file
View File

@ -0,0 +1,5 @@
Kind.Book.to_hvm
: ∀(book: Kind.Book)
String
= λbook
(String.Concatenator.build (Kind.Book.to_hvm.go book))

4
book/Kind.Oper.add.kind2 Normal file
View File

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

4
book/Kind.Oper.and.kind2 Normal file
View File

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

4
book/Kind.Oper.div.kind2 Normal file
View File

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

4
book/Kind.Oper.eq.kind2 Normal file
View File

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

4
book/Kind.Oper.gt.kind2 Normal file
View File

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

4
book/Kind.Oper.gte.kind2 Normal file
View File

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

21
book/Kind.Oper.kind2 Normal file
View File

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

4
book/Kind.Oper.lsh.kind2 Normal file
View File

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

4
book/Kind.Oper.lt.kind2 Normal file
View File

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

4
book/Kind.Oper.lte.kind2 Normal file
View File

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

4
book/Kind.Oper.mod.kind2 Normal file
View File

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

4
book/Kind.Oper.mul.kind2 Normal file
View File

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

4
book/Kind.Oper.ne.kind2 Normal file
View File

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

4
book/Kind.Oper.or.kind2 Normal file
View File

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

28
book/Kind.Oper.parser.kind2 Normal file
View File

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

4
book/Kind.Oper.rsh.kind2 Normal file
View File

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

22
book/Kind.Oper.show.go.kind2 Normal file
View File

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

4
book/Kind.Oper.show.kind2 Normal file
View File

@ -0,0 +1,4 @@
Kind.Oper.show
: ∀(oper: Kind.Oper)
String
= λoper (String.Concatenator.build (Kind.Oper.show.go oper))

4
book/Kind.Oper.sub.kind2 Normal file
View File

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

4
book/Kind.Oper.xor.kind2 Normal file
View File

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

4
book/Kind.PreTerm.kind2 Normal file
View File

@ -0,0 +1,4 @@
Kind.PreTerm
: *
= ∀(ctx: Kind.Scope)
Kind.Term

5
book/Kind.Scope.cons.kind2 Normal file
View File

@ -0,0 +1,5 @@
Kind.Scope.cons
: ∀(head: Kind.Binder)
∀(tail: Kind.Scope)
Kind.Scope
= (List.cons Kind.Binder)

7
book/Kind.Scope.extend.kind2 Normal file
View File

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

11
book/Kind.Scope.find.kind2 Normal file
View File

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

3
book/Kind.Scope.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Scope
: *
= (List Kind.Binder)

3
book/Kind.Scope.nil.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Scope.nil
: Kind.Scope
= (List.nil Kind.Binder)

21
book/Kind.Term.kind2 Normal file
View File

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

8
book/Kind.Term.parse.kind2 Normal file
View File

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

12
book/Kind.Term.parser.all.kind2 Normal file
View File

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

10
book/Kind.Term.parser.ann.kind2 Normal file
View File

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

12
book/Kind.Term.parser.app.kind2 Normal file
View File

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

6
book/Kind.Term.parser.bind.kind2 Normal file
View File

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

8
book/Kind.Term.parser.chr.kind2 Normal file
View File

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

10
book/Kind.Term.parser.def.kind2 Normal file
View File

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

7
book/Kind.Term.parser.hol.kind2 Normal file
View File

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

7
book/Kind.Term.parser.ins.kind2 Normal file
View File

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

22
book/Kind.Term.parser.kind2 Normal file
View File

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

8
book/Kind.Term.parser.lam.kind2 Normal file
View File

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

19
book/Kind.Term.parser.mat.kind2 Normal file
View File

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

7
book/Kind.Term.parser.num.kind2 Normal file
View File

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

10
book/Kind.Term.parser.op2.kind2 Normal file
View File

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

4
book/Kind.Term.parser.pure.kind2 Normal file
View File

@ -0,0 +1,4 @@
Kind.Term.parser.pure
: ∀(value: Kind.PreTerm)
(Parser Kind.PreTerm)
= (Parser.pure Kind.PreTerm)

6
book/Kind.Term.parser.set.kind2 Normal file
View File

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

8
book/Kind.Term.parser.slf.kind2 Normal file
View File

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

8
book/Kind.Term.parser.str.kind2 Normal file
View File

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

6
book/Kind.Term.parser.u60.kind2 Normal file
View File

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

6
book/Kind.Term.parser.var.kind2 Normal file
View File

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

99
book/Kind.Term.show.go.kind2 Normal file
View File

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

6
book/Kind.Term.show.kind2 Normal file
View File

@ -0,0 +1,6 @@
Kind.Term.show
: ∀(term: Kind.Term)
∀(dep: Nat)
String
= λterm λdep
(String.Concatenator.build (Kind.Term.show.go term dep))

73
book/Kind.Term.to_hvm.go.kind2 Normal file
View File

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

6
book/Kind.Term.to_hvm.kind2 Normal file
View File

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

3
book/Kind.Text.kind2 Normal file
View File

@ -0,0 +1,3 @@
Kind.Text
: *
= String

4
book/Kind.Text.show.go.kind2 Normal file
View File

@ -0,0 +1,4 @@
Kind.Text.show.go
: ∀(text: Kind.Text)
String.Concatenator
= String.Concatenator.from_string

8
book/Kind.all.kind2 Normal file
View File

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

7
book/Kind.ann.kind2 Normal file
View File

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

7
book/Kind.app.kind2 Normal file
View File

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

58
book/Kind.check.kind2 Normal file
View File

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

93
book/Kind.comparer.kind2 Normal file
View File

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

8
book/Kind.def.kind2 Normal file
View File

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

11
book/Kind.equal.enter.kind2 Normal file
View File

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

7
book/Kind.equal.kind2 Normal file
View File

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

14
book/Kind.equal.major.kind2 Normal file
View File

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

14
book/Kind.equal.minor.kind2 Normal file
View File

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

7
book/Kind.hol.kind2 Normal file
View File

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

7
book/Kind.identical.kind2 Normal file
View File

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

25
book/Kind.if.all.kind2 Normal file
View File

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

25
book/Kind.if.ann.kind2 Normal file
View File

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

25
book/Kind.if.app.kind2 Normal file
View File

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

25
book/Kind.if.def.kind2 Normal file
View File

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

25
book/Kind.if.hol.kind2 Normal file
View File

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

25
book/Kind.if.ins.kind2 Normal file
View File

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

25
book/Kind.if.lam.kind2 Normal file
View File

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

25
book/Kind.if.mat.kind2 Normal file
View File

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

25
book/Kind.if.num.kind2 Normal file
View File

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

25
book/Kind.if.op2.kind2 Normal file
View File

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

25
book/Kind.if.ref.kind2 Normal file
View File

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

25
book/Kind.if.set.kind2 Normal file
View File

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

25
book/Kind.if.slf.kind2 Normal file
View File

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

25
book/Kind.if.txt.kind2 Normal file
View File

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

25
book/Kind.if.u60.kind2 Normal file
View File

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

25
book/Kind.if.var.kind2 Normal file
View File

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

64
book/Kind.infer.kind2 Normal file
View File

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

6
book/Kind.ins.kind2 Normal file
View File

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

1738
book/Kind.kind2
View File

File diff suppressed because it is too large Load Diff

7
book/Kind.lam.kind2 Normal file
View File

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

10
book/Kind.mat.kind2 Normal file
View File

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

24
book/Kind.normal.go.kind2 Normal file
View File

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

7
book/Kind.normal.kind2 Normal file
View File

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

Some files were not shown because too many files have changed in this diff Show More