mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 17:56:48 +03:00
58 lines
2.5 KiB
Plaintext
58 lines
2.5 KiB
Plaintext
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) |