mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 17:56:48 +03:00
85ad65b026
Now, there are two local binders: let x = ... use x = ... The 'let' binder will create a local definition, type-check it, and assign a name to it. When compiled, it will create 'dup' nodes. The 'use' binder is just an alias. It will not bind a new variable, and, when compiled, will create inline copies. Also, for type-checking, it allows creating aliases that are definitionaly equal for the checker.
90 lines
2.6 KiB
Plaintext
90 lines
2.6 KiB
Plaintext
Kind.check
|
|
: ∀(term: Kind.Term) ∀(type: Kind.Term) ∀(dep: Nat)
|
|
(Maybe Kind.Term)
|
|
= λterm λtype λdep
|
|
use bind = (Maybe.bind Kind.Term Kind.Term)
|
|
use pure = (Maybe.some Kind.Term)
|
|
use none = (Maybe.none Kind.Term)
|
|
use P = λx ∀(type: Kind.Term) ∀(dep: Nat) (Maybe Kind.Term)
|
|
use all = λterm.nam λterm.inp λterm.bod λtype λdep
|
|
(Kind.verify
|
|
(Kind.all term.nam term.inp term.bod)
|
|
type
|
|
dep
|
|
)
|
|
use 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
|
|
use ann = (Kind.ann (Kind.var term.nam dep) type.inp)
|
|
use term = (term.bod ann)
|
|
use 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
|
|
)
|
|
use app = λterm.fun λterm.arg λtype λdep
|
|
(Kind.verify (Kind.app term.fun term.arg) type dep)
|
|
use ann = λval λtyp λtype λdep
|
|
(Kind.verify (Kind.ann val typ) type dep)
|
|
use slf = λterm.nam λterm.bod λtype λdep
|
|
(Kind.verify (Kind.slf term.nam term.bod) type dep)
|
|
use 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
|
|
)
|
|
use ref = λterm.nam λterm.val λtype λdep
|
|
(Kind.check term.val type dep)
|
|
use def = λterm.nam λterm.val λterm.bod λtype λdep
|
|
(Kind.check (term.bod term.val) type (Nat.succ dep))
|
|
use set = λtype λdep (Kind.verify Kind.set type dep)
|
|
use u60 = λtype λdep (Kind.verify Kind.u60 type dep)
|
|
use num = λterm.num λtype λdep
|
|
(Kind.verify (Kind.num term.num) type dep)
|
|
use op2 = λterm.opr λterm.fst λterm.snd λtype λdep
|
|
(Kind.verify
|
|
(Kind.op2 term.opr term.fst term.snd)
|
|
type
|
|
dep
|
|
)
|
|
use 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
|
|
)
|
|
use txt = λterm.txt λtype λdep
|
|
(Kind.verify (Kind.txt term.txt) type dep)
|
|
use hol = λterm.nam λterm.ctx λtype λdep (pure Kind.set)
|
|
use 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
|
|
) |