mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 17:56:48 +03:00
1459 lines
48 KiB
Plaintext
1459 lines
48 KiB
Plaintext
// Term Type
|
|
// ---------
|
|
|
|
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)))
|
|
∀(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)
|
|
|
|
// Operator Type
|
|
// -------------
|
|
|
|
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))
|
|
(P self)
|
|
|
|
// Other Types
|
|
// -----------
|
|
|
|
Kind.Binder
|
|
: *
|
|
= (Pair String Kind.Term)
|
|
|
|
Kind.Scope
|
|
: *
|
|
= (List Kind.Binder)
|
|
|
|
Kind.PreTerm
|
|
: *
|
|
= ∀(ctx: Kind.Scope)
|
|
Kind.Term
|
|
|
|
// Term Constructors
|
|
// -----------------
|
|
|
|
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 λ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 λ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 λ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 λ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 λ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 λ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 λ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 λtxt λhol λvar
|
|
(def nam val bod)
|
|
|
|
Kind.set
|
|
: Kind.Term
|
|
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λtxt λhol λvar
|
|
(set)
|
|
|
|
Kind.u60
|
|
: Kind.Term
|
|
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λtxt λhol λvar
|
|
u60
|
|
|
|
Kind.num
|
|
: ∀(val: #U60)
|
|
Kind.Term
|
|
= λval
|
|
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λ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 λtxt λhol λvar
|
|
(op2 opr fst snd)
|
|
|
|
Kind.txt
|
|
: ∀(lit: Kind.Text)
|
|
Kind.Term
|
|
= λlit
|
|
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λ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 λ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 λtxt λhol λvar
|
|
(var nam idx)
|
|
|
|
|
|
// Operator Constructors
|
|
// ---------------------
|
|
|
|
Kind.Oper.add
|
|
: Kind.Oper
|
|
= ~λP λadd λmul λsub λdiv
|
|
(add)
|
|
|
|
Kind.Oper.mul
|
|
: Kind.Oper
|
|
= ~λP λadd λmul λsub λdiv
|
|
(mul)
|
|
|
|
Kind.Oper.sub
|
|
: Kind.Oper
|
|
= ~λP λadd λmul λsub λdiv
|
|
(sub)
|
|
|
|
Kind.Oper.div
|
|
: Kind.Oper
|
|
= ~λP λadd λmul λsub λdiv
|
|
(div)
|
|
|
|
// Other Constructors
|
|
// ------------------
|
|
|
|
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)
|
|
|
|
// Other Utils
|
|
// -----------
|
|
|
|
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.set // FIXME: handle unbound reference
|
|
(~found P some none)
|
|
|
|
// Term Selectors
|
|
// --------------
|
|
|
|
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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 txt hol var Y N)
|
|
|
|
|
|
// Primitives
|
|
// ----------
|
|
|
|
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))
|
|
|
|
// Stringifier
|
|
// -----------
|
|
|
|
Kind.Text
|
|
: *
|
|
= String
|
|
|
|
Kind.Text.show.go
|
|
: ∀(text: Kind.Text)
|
|
String.Concatenator
|
|
= String.Concatenator.from_string
|
|
|
|
Kind.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.show.go inp dep)
|
|
((Kind.Text.show.go ") ")
|
|
((Kind.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.show.go (bod (Kind.var nam dep)) (Nat.succ dep))
|
|
nil))))
|
|
let app = λfun λarg λnil
|
|
((Kind.Text.show.go "(")
|
|
((Kind.show.go fun dep)
|
|
((Kind.Text.show.go " ")
|
|
((Kind.show.go arg dep)
|
|
((Kind.Text.show.go ")")
|
|
nil)))))
|
|
let ann = λval λtyp λnil
|
|
((Kind.Text.show.go "{")
|
|
((Kind.show.go val dep)
|
|
((Kind.Text.show.go ": ")
|
|
((Kind.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.show.go (bod (Kind.var nam dep)) (Nat.succ dep))
|
|
nil))))
|
|
let ins = λval λnil
|
|
((Kind.Text.show.go "~")
|
|
((Kind.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.show.go val dep)
|
|
((Kind.Text.show.go "; ")
|
|
((Kind.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.show.go fst dep)
|
|
((Kind.Text.show.go " ")
|
|
((Kind.show.go snd dep)
|
|
((Kind.Text.show.go ")")
|
|
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 txt hol var)
|
|
|
|
Kind.show
|
|
: ∀(term: Kind.Term)
|
|
∀(dep: Nat)
|
|
String
|
|
= λterm λdep (String.Concatenator.build (Kind.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 "/")
|
|
(~oper P add mul sub div)
|
|
|
|
Kind.Oper.show
|
|
: ∀(oper: Kind.Oper)
|
|
String
|
|
= λoper (String.Concatenator.build (Kind.Oper.show.go oper))
|
|
|
|
// Parser
|
|
// ------
|
|
|
|
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)
|
|
|
|
// ∀(x: inp) bod
|
|
Kind.Term.parser.all
|
|
: (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 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)))))))))))
|
|
|
|
// λx bod
|
|
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))))))))
|
|
|
|
// (f x)
|
|
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 Kind.PreTerm Kind.Term.parser λarg
|
|
(Kind.Term.parser.bind Unit (Parser.text ")") λ_
|
|
(Kind.Term.parser.pure λscp
|
|
(Kind.app (fun scp) (arg scp))))))))
|
|
|
|
// {x: T}
|
|
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)))))))))
|
|
|
|
// $x bod
|
|
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))))))))
|
|
|
|
// ~val
|
|
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)))
|
|
|
|
// let x = val; bod
|
|
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))))))))))
|
|
|
|
// #U60
|
|
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)))
|
|
|
|
// #(OP fst snd)
|
|
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)))))))))
|
|
|
|
// #num
|
|
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)))))
|
|
|
|
// 'c'
|
|
Kind.Term.parser.chr
|
|
: (Parser Kind.PreTerm)
|
|
= ?TODO
|
|
//Kind.Term.parser.chr
|
|
//: (Parser Kind.PreTerm)
|
|
//= (Kind.Term.parser.bind Unit (Parser.text "'") λ_
|
|
//(Kind.Term.parser.bind #U60 ?TODO λchr
|
|
//(Kind.Term.parser.bind Unit (Parser.text "'") λ_
|
|
//(Kind.Term.parser.pure λscp
|
|
//(Kind.num chr)))))
|
|
|
|
// "string"
|
|
Kind.Term.parser.str
|
|
: (Parser Kind.PreTerm)
|
|
= ?TODO
|
|
|
|
// ?nam
|
|
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
|
|
|
|
// x
|
|
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)
|
|
= ?TODO
|
|
|
|
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.num
|
|
(TRY Kind.Term.parser.hol
|
|
(TRY Kind.Term.parser.var
|
|
END))))))))))))))
|
|
|
|
// Evaluation
|
|
// ----------
|
|
|
|
Kind.reduce
|
|
: ∀(major: Bool)
|
|
∀(term: Kind.Term)
|
|
Kind.Term
|
|
= λmajor λterm
|
|
let P = λx(Kind.Term)
|
|
let all = Kind.all
|
|
let lam = Kind.lam
|
|
let app = λfun λarg (Kind.reduce.app major (Kind.reduce major fun) arg)
|
|
let slf = Kind.slf
|
|
let ann = λval λtyp (Kind.reduce major val)
|
|
let ins = λval (Kind.reduce major val)
|
|
let ref = λnam λval (Kind.reduce.ref major nam val)
|
|
let def = λnam λval λbod (Kind.reduce major (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 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 txt hol var)
|
|
|
|
Kind.reduce.app
|
|
: ∀(major: Bool)
|
|
∀(fun: Kind.Term)
|
|
∀(arg: Kind.Term)
|
|
Kind.Term
|
|
= λmajor λfun λarg
|
|
let P = ∀(arg: Kind.Term) Kind.Term
|
|
let Y = λnam λbod λarg (Kind.reduce major (bod (Kind.reduce major arg)))
|
|
let N = λfun λarg (Kind.app fun arg)
|
|
(Kind.if.lam fun P Y N arg)
|
|
|
|
Kind.reduce.ref
|
|
: ∀(major: Bool)
|
|
∀(nam: String)
|
|
∀(val: Kind.Term)
|
|
Kind.Term
|
|
= λmajor λnam λval
|
|
let P = λx ∀(nam: String) ∀(val: Kind.Term) Kind.Term
|
|
let true = λnam λval (Kind.reduce major val)
|
|
let false = Kind.ref
|
|
(~major 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))
|
|
(~opr P add mul sub div 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.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)
|
|
|
|
// Normalization
|
|
// -------------
|
|
|
|
Kind.normal
|
|
: ∀(major: Bool)
|
|
∀(term: Kind.Term)
|
|
∀(dep: Nat)
|
|
Kind.Term
|
|
= λmajor λterm λdep
|
|
(Kind.normal.go major (Kind.reduce major term) dep)
|
|
|
|
Kind.normal.go
|
|
: ∀(major: Bool)
|
|
∀(term: Kind.Term)
|
|
∀(dep: Nat)
|
|
Kind.Term
|
|
= λmajor λterm λdep
|
|
let P = λx Kind.Term
|
|
let all = λnam λinp λbod (Kind.all nam (Kind.normal major inp dep) λx (Kind.normal major (bod (Kind.var nam dep)) (Nat.succ dep)))
|
|
let lam = λnam λbod (Kind.lam nam λx (Kind.normal major (bod (Kind.var nam dep)) (Nat.succ dep)))
|
|
let app = λfun λarg (Kind.app (Kind.normal major fun dep) (Kind.normal major arg dep))
|
|
let ann = λval λtyp (Kind.ann (Kind.normal major val dep) (Kind.normal major typ dep))
|
|
let slf = λnam λbod (Kind.slf nam λx (Kind.normal major (bod (Kind.var nam dep)) (Nat.succ dep)))
|
|
let ins = λval (Kind.ins (Kind.normal major val dep))
|
|
let ref = λnam λval (Kind.ref nam (Kind.normal major val dep))
|
|
let def = λnam λval λbod (Kind.def nam (Kind.normal major val dep) λx (Kind.normal major (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 major fst dep) (Kind.normal major snd 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 txt hol var)
|
|
|
|
// Equality
|
|
// --------
|
|
|
|
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 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 txt hol var b dep)
|
|
(Kind.if.hol b R Y N dep a)
|
|
(Kind.if.hol a R Y N b dep)
|
|
|
|
// Type-Checking
|
|
// -------------
|
|
|
|
// Skips Ins, Ann and Let
|
|
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 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 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 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 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 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 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)
|
|
|
|
// Tests
|
|
// -----
|
|
|
|
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.show value Nat.zero)
|
|
let none = "error"
|
|
let chk = (Kind.check test Test Nat.zero)
|
|
(~chk P some none)
|
|
|
|
//Kind = Kind.Term
|
|
//Kind = Kind.all
|
|
//Kind = Kind.lam
|
|
//Kind = Kind.app
|
|
//Kind = Kind.ann
|
|
//Kind = Kind.slf
|
|
//Kind = Kind.ins
|
|
//Kind = Kind.ref
|
|
//Kind = Kind.def
|
|
//Kind = Kind.set
|
|
//Kind = Kind.u60
|
|
//Kind = Kind.num
|
|
//Kind = Kind.op2
|
|
//Kind = Kind.txt
|
|
//Kind = Kind.hol
|
|
//Kind = Kind.var
|
|
//Kind = Kind.if.all
|
|
//Kind = Kind.if.lam
|
|
//Kind = Kind.if.app
|
|
//Kind = Kind.if.ann
|
|
//Kind = Kind.if.slf
|
|
//Kind = Kind.if.ins
|
|
//Kind = Kind.if.ref
|
|
//Kind = Kind.if.def
|
|
//Kind = Kind.if.set
|
|
//Kind = Kind.if.u60
|
|
//Kind = Kind.if.num
|
|
//Kind = Kind.if.op2
|
|
//Kind = Kind.if.txt
|
|
//Kind = Kind.if.hol
|
|
//Kind = Kind.if.var
|
|
//Kind = Kind.Oper
|
|
//Kind = Kind.Oper.add
|
|
//Kind = Kind.Oper.mul
|
|
//Kind = Kind.Oper.sub
|
|
//Kind = Kind.Oper.div
|
|
//Kind = Kind.Text
|
|
//Kind = Kind.Text.show.go
|
|
//Kind = Kind.show.go
|
|
//Kind = Kind.show
|
|
//Kind = Kind.Oper.show.go
|
|
//Kind = Kind.Oper.show
|
|
//Kind = Kind.reduce
|
|
//Kind = Kind.reduce.app
|
|
//Kind = Kind.reduce.ref
|
|
//Kind = Kind.reduce.op2
|
|
//Kind = Kind.reduce.txt
|
|
//Kind = Kind.normal
|
|
//Kind = Kind.normal.go
|
|
//Kind = Kind.equal
|
|
//Kind = Kind.equal.minor
|
|
//Kind = Kind.equal.major
|
|
//Kind = Kind.equal.enter
|
|
//Kind = Kind.identical
|
|
//Kind = Kind.comparer
|
|
//Kind = Kind.skip
|
|
//Kind = Kind.infer
|
|
//Kind = Kind.check
|
|
//Kind = Kind.verify
|
|
//Kind = Kind.report
|