mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 08:30:27 +03:00
many things
This commit is contained in:
parent
37fb440ea9
commit
e4b262f9d1
71
book/A.kind2
Normal file
71
book/A.kind2
Normal file
@ -0,0 +1,71 @@
|
|||||||
|
//TRY-0
|
||||||
|
//-----
|
||||||
|
|
||||||
|
//A.one : A = ~λP λnew (new Nat.zero)
|
||||||
|
//A.bad : A = ~λP λnew (new (Nat.succ Nat.zero) ?UE)
|
||||||
|
|
||||||
|
//A : * =
|
||||||
|
//$self
|
||||||
|
//∀(P: ∀(x: A) *)
|
||||||
|
//∀(new: ∀(tag: Nat)
|
||||||
|
//let R = λx(*)
|
||||||
|
//let zero = (P A.one)
|
||||||
|
//let succ = λp∀(x:Empty)*
|
||||||
|
//(~tag R succ zero))
|
||||||
|
//(P self)
|
||||||
|
|
||||||
|
//A.elim : ∀(a: A) ∀(P: ∀(x: A) *) ∀(t: (P A.one)) (P a) =
|
||||||
|
//λa λP λt
|
||||||
|
//(~a P λtag(~tag λx(~x λx(*) λp(Empty) (P A.one)) λp(?B) t))
|
||||||
|
|
||||||
|
// TRY-1
|
||||||
|
// -----
|
||||||
|
|
||||||
|
A.one : A = ~λP λnew (new #0)
|
||||||
|
A.bad : A = ~λP λnew (new #1 ?UE)
|
||||||
|
|
||||||
|
A.sel
|
||||||
|
: ∀(P: ∀(x: A) *)
|
||||||
|
∀(k: #U60)
|
||||||
|
*
|
||||||
|
= λP λk #match tag = k {
|
||||||
|
#0: (P A.one)
|
||||||
|
#+: ∀(e: Empty) *
|
||||||
|
}: *
|
||||||
|
|
||||||
|
A : * =
|
||||||
|
$self
|
||||||
|
∀(P: ∀(x: A) *)
|
||||||
|
∀(new: ∀(tag: #U60) (A.sel P tag))
|
||||||
|
(P self)
|
||||||
|
|
||||||
|
A.match : ∀(a: A) ∀(P: ∀(x: A) *) ∀(t: (P A.one)) (P a) =
|
||||||
|
λa λP λt
|
||||||
|
(~a P λtag #match tag = tag {
|
||||||
|
#0: t
|
||||||
|
#+: λx (~x λx(*))
|
||||||
|
}: (A.sel P tag))
|
||||||
|
|
||||||
|
// TRY-2
|
||||||
|
// -----
|
||||||
|
|
||||||
|
//A.one
|
||||||
|
//: A
|
||||||
|
//= ~ λP λnew (new #0 Unit.one)
|
||||||
|
|
||||||
|
//A : * = (Sigma #U60 λtag #match tag = tag {
|
||||||
|
//#0: Unit
|
||||||
|
//#+: Empty
|
||||||
|
//}: *)
|
||||||
|
|
||||||
|
//A.match : ∀(a: A) ∀(P: ∀(x: A) *) ∀(t: (P A.one)) (P a) =
|
||||||
|
//λa λP λt
|
||||||
|
//(~a P λx #match x = x {
|
||||||
|
//#0: λb ?A
|
||||||
|
//#+: λb ?B
|
||||||
|
//}: ∀(b: (#match x = x { #0: Unit #+: Empty }: *))
|
||||||
|
//(P (Sigma.new #U60 λtag(#match tag = tag { #0: Unit #+: Empty }: *) x b)))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
//(P (Sigma.new #U60 Unit b))
|
5
book/Empty.absurd.kind2
Normal file
5
book/Empty.absurd.kind2
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
Empty.absurd
|
||||||
|
: ∀(e: Empty)
|
||||||
|
∀(P: *)
|
||||||
|
P
|
||||||
|
= λe λP (~e λx(P))
|
5
book/Empty.kind2
Normal file
5
book/Empty.kind2
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
Empty
|
||||||
|
: *
|
||||||
|
= $self
|
||||||
|
∀(P: ∀(x: Empty) *)
|
||||||
|
(P self)
|
@ -6,12 +6,13 @@ Kind.Book.to_hvm.go
|
|||||||
let cons = λhead λtail
|
let cons = λhead λtail
|
||||||
let P = λx String.Concatenator
|
let P = λx String.Concatenator
|
||||||
let new = λhead.fst λhead.snd λnil
|
let new = λhead.fst λhead.snd λnil
|
||||||
|
((Kind.Text.show.go "F."
|
||||||
((Kind.Text.show.go head.fst)
|
((Kind.Text.show.go head.fst)
|
||||||
((Kind.Text.show.go " = "
|
((Kind.Text.show.go " = "
|
||||||
((Kind.Term.to_hvm.go head.snd Nat.zero
|
((Kind.Term.to_hvm.go head.snd Nat.zero Bool.true Nat.zero
|
||||||
((Kind.Text.show.go String.newline
|
((Kind.Text.show.go String.newline
|
||||||
((Kind.Book.to_hvm.go tail
|
((Kind.Book.to_hvm.go tail
|
||||||
nil)))))))))
|
nil)))))))))))
|
||||||
(~head P new)
|
(~head P new)
|
||||||
let nil = λnil nil
|
let nil = λnil nil
|
||||||
(~book P cons nil)
|
(~book P cons nil)
|
||||||
|
@ -2,4 +2,4 @@ Kind.Book.to_hvm
|
|||||||
: ∀(book: Kind.Book)
|
: ∀(book: Kind.Book)
|
||||||
String
|
String
|
||||||
= λbook
|
= λbook
|
||||||
(String.Concatenator.build (Kind.Book.to_hvm.go book))
|
(String.Concatenator.build (Kind.Book.to_hvm.go book))
|
||||||
|
9
book/Kind.Book.to_hvm.prelude.kind2
Normal file
9
book/Kind.Book.to_hvm.prelude.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
Kind.Book.to_hvm.prelude
|
||||||
|
: String
|
||||||
|
= `
|
||||||
|
(U60.match 0 z s) = z
|
||||||
|
(U60.match n z s) = (s (- n 1))
|
||||||
|
|
||||||
|
(Str String.nil) = λP λcons λnil nil
|
||||||
|
(Str (String.cons x xs)) = λP λcons λnil (cons x (Str xs))
|
||||||
|
`
|
@ -16,4 +16,4 @@ Kind.Term.parser.mat
|
|||||||
(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.bind Kind.PreTerm Kind.Term.parser λp
|
||||||
(Kind.Term.parser.pure λscp
|
(Kind.Term.parser.pure λscp
|
||||||
(Kind.mat nam (x scp) (z scp) λx(s (Kind.Scope.extend nam x scp)) λx(p (Kind.Scope.extend nam x scp)))))))))))))))))))
|
(Kind.mat nam (x scp) (z scp) λx(s (Kind.Scope.extend (String.concat nam "-1") x scp)) λx(p (Kind.Scope.extend nam x scp)))))))))))))))))))
|
||||||
|
@ -80,7 +80,7 @@ Kind.Term.show.go
|
|||||||
((Kind.Text.show.go " { #0: ")
|
((Kind.Text.show.go " { #0: ")
|
||||||
((Kind.Term.show.go z dep)
|
((Kind.Term.show.go z dep)
|
||||||
((Kind.Text.show.go "; #+: ")
|
((Kind.Text.show.go "; #+: ")
|
||||||
((Kind.Term.show.go (s (Kind.var nam dep)) (Nat.succ dep))
|
((Kind.Term.show.go (s (Kind.var (String.concat nam "-1") dep)) (Nat.succ dep))
|
||||||
((Kind.Text.show.go " }: ")
|
((Kind.Text.show.go " }: ")
|
||||||
((Kind.Term.show.go (p (Kind.var nam dep)) (Nat.succ dep))
|
((Kind.Term.show.go (p (Kind.var nam dep)) (Nat.succ dep))
|
||||||
nil))))))))))
|
nil))))))))))
|
||||||
@ -96,4 +96,4 @@ Kind.Term.show.go
|
|||||||
let var = λnam λidx λnil
|
let var = λnam λidx λnil
|
||||||
((Kind.Text.show.go nam)
|
((Kind.Text.show.go nam)
|
||||||
nil)
|
nil)
|
||||||
(~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var)
|
(~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var)
|
||||||
|
@ -1,73 +1,113 @@
|
|||||||
Kind.Term.to_hvm.go
|
Kind.Term.to_hvm.go
|
||||||
: ∀(term: Kind.Term)
|
: ∀(term: Kind.Term)
|
||||||
∀(dep: Nat)
|
∀(dep: Nat)
|
||||||
|
∀(inc: Bool)
|
||||||
|
∀(tab: Nat)
|
||||||
String.Concatenator
|
String.Concatenator
|
||||||
= λterm λdep
|
= λterm λdep λinc λtab
|
||||||
let P = λx String.Concatenator
|
let P = λx String.Concatenator
|
||||||
let all = λnam λinp λbod
|
let all = λnam λinp λbod λnil
|
||||||
(Kind.Text.show.go "0")
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Text.show.go "0")
|
||||||
|
nil))
|
||||||
let lam = λnam λbod λnil
|
let lam = λnam λbod λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
((Kind.Text.show.go "λ")
|
((Kind.Text.show.go "λ")
|
||||||
((Kind.Text.show.go (U60.name (U60.from_nat dep)))
|
//((Kind.Text.show.go (U60.name (U60.from_nat dep)))
|
||||||
|
((Kind.Text.show.go (String.cons '_' nam))
|
||||||
((Kind.Text.show.go " "
|
((Kind.Text.show.go " "
|
||||||
((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep))
|
((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep) Bool.true tab)
|
||||||
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))))))
|
nil))))))
|
||||||
let set =
|
let app = λfun λarg λnil
|
||||||
(Kind.Text.show.go "0")
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
let u60 =
|
((Kind.Text.show.go "(")
|
||||||
(Kind.Text.show.go "0")
|
((Kind.Term.to_hvm.go fun dep Bool.true tab)
|
||||||
let num = λval
|
((Kind.Text.show.go " ")
|
||||||
(U60.show.go val)
|
((Kind.Term.to_hvm.go arg dep Bool.true tab)
|
||||||
|
((Kind.Text.show.go ")")
|
||||||
|
nil))))))
|
||||||
|
let ann = λval λtyp λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Term.to_hvm.go val dep Bool.true tab)
|
||||||
|
nil))
|
||||||
|
let slf = λnam λbod λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Text.show.go "0")
|
||||||
|
nil))
|
||||||
|
let ins = λval λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Term.to_hvm.go val dep Bool.true tab)
|
||||||
|
nil))
|
||||||
|
let ref = λnam λval λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Text.show.go "(F.")
|
||||||
|
((Kind.Text.show.go nam)
|
||||||
|
((Kind.Text.show.go ")")
|
||||||
|
nil))))
|
||||||
|
let def = λnam λval λbod λnil
|
||||||
|
let tab = ((~inc λx∀(x:Nat)Nat Nat.succ λx(x)) tab)
|
||||||
|
((Kind.Text.show.go String.newline)
|
||||||
|
((Kind.Text.show.go (String.indent tab))
|
||||||
|
((Kind.Text.show.go "let ")
|
||||||
|
//((Kind.Text.show.go (U60.name (U60.from_nat dep)))
|
||||||
|
((Kind.Text.show.go (String.cons '_' nam))
|
||||||
|
((Kind.Text.show.go " = ")
|
||||||
|
((Kind.Term.to_hvm.go val dep Bool.true tab)
|
||||||
|
((Kind.Text.show.go " ")
|
||||||
|
((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep) Bool.false tab)
|
||||||
|
nil))))))))
|
||||||
|
let set = λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Text.show.go "0")
|
||||||
|
nil))
|
||||||
|
let u60 = λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Text.show.go "0")
|
||||||
|
nil))
|
||||||
|
let num = λval λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((U60.show.go val)
|
||||||
|
nil))
|
||||||
let op2 = λopr λfst λsnd λnil
|
let op2 = λopr λfst λsnd λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
((Kind.Text.show.go "(")
|
((Kind.Text.show.go "(")
|
||||||
((Kind.Oper.show.go opr) // TODO: Kind.Oper.to_hvm
|
((Kind.Oper.show.go opr) // TODO: Kind.Oper.to_hvm
|
||||||
((Kind.Text.show.go " ")
|
((Kind.Text.show.go " ")
|
||||||
((Kind.Term.to_hvm.go fst dep)
|
((Kind.Term.to_hvm.go fst dep Bool.true tab)
|
||||||
((Kind.Text.show.go " ")
|
((Kind.Text.show.go " ")
|
||||||
((Kind.Term.to_hvm.go snd dep)
|
((Kind.Term.to_hvm.go snd dep Bool.true tab)
|
||||||
((Kind.Text.show.go ")")
|
((Kind.Text.show.go ")")
|
||||||
nil)))))))
|
nil))))))))
|
||||||
let mat = λnam λx λz λs λp λnil
|
let mat = λnam λx λz λs λp λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
((Kind.Text.show.go "(U60.match ")
|
((Kind.Text.show.go "(U60.match ")
|
||||||
((Kind.Term.to_hvm.go x dep)
|
((Kind.Term.to_hvm.go x dep Bool.true tab)
|
||||||
((Kind.Text.show.go " ")
|
((Kind.Text.show.go " ")
|
||||||
((Kind.Term.to_hvm.go z dep)
|
((Kind.Term.to_hvm.go z dep Bool.true tab)
|
||||||
((Kind.Text.show.go " ")
|
((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.Text.show.go " ")
|
((Kind.Text.show.go (String.cons '_' (String.concat nam "_1")))
|
||||||
((Kind.Term.to_hvm.go (p (Kind.var nam dep)) (Nat.succ dep))
|
//((Kind.Text.show.go (U60.name (U60.from_nat dep)))
|
||||||
|
((Kind.Text.show.go "(")
|
||||||
|
((Kind.Term.to_hvm.go (s (Kind.var (String.concat nam "_1") dep)) (Nat.succ dep) Bool.true tab)
|
||||||
((Kind.Text.show.go ")")
|
((Kind.Text.show.go ")")
|
||||||
nil)))))))))
|
((Kind.Text.show.go ")")
|
||||||
|
nil))))))))))))
|
||||||
let txt = λtxt λnil
|
let txt = λtxt λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
((Kind.Text.show.go "(Str ")
|
||||||
((Kind.Text.show.go String.quote)
|
((Kind.Text.show.go String.quote)
|
||||||
((Kind.Text.show.go txt)
|
((Kind.Text.show.go txt)
|
||||||
((Kind.Text.show.go String.quote)
|
((Kind.Text.show.go String.quote)
|
||||||
nil)))
|
((Kind.Text.show.go ")")
|
||||||
let hol = λnam λctx
|
nil))))))
|
||||||
(Kind.Text.show.go "0")
|
let hol = λnam λctx λnil
|
||||||
let var = λnam λidx
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
(Kind.Text.show.go (U60.name (U60.from_nat idx)))
|
((Kind.Text.show.go "0")
|
||||||
(~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var)
|
nil))
|
||||||
|
let var = λnam λidx λnil
|
||||||
|
((Kind.Term.to_hvm.nl inc tab)
|
||||||
|
//((Kind.Text.show.go (U60.name (U60.from_nat idx)))
|
||||||
|
((Kind.Text.show.go (String.cons '_' nam))
|
||||||
|
nil))
|
||||||
|
(~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var)
|
||||||
|
10
book/Kind.Term.to_hvm.nl.kind2
Normal file
10
book/Kind.Term.to_hvm.nl.kind2
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
Kind.Term.to_hvm.nl
|
||||||
|
: ∀(inc: Bool)
|
||||||
|
∀(tab: Nat)
|
||||||
|
String.Concatenator
|
||||||
|
= λinc λtab
|
||||||
|
let P = λx(String.Concatenator)
|
||||||
|
let true = λnil (nil)
|
||||||
|
let false = λnil ((Kind.Text.show.go String.newline) ((Kind.Text.show.go (String.indent tab)) nil))
|
||||||
|
(~inc P true false)
|
||||||
|
|
@ -4,4 +4,4 @@ Kind.ann
|
|||||||
Kind.Term
|
Kind.Term
|
||||||
= λval λtyp
|
= λval λtyp
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
||||||
(ann val typ)
|
(ann val typ)
|
||||||
|
@ -4,4 +4,4 @@ Kind.app
|
|||||||
Kind.Term
|
Kind.Term
|
||||||
= λfun λarg
|
= λfun λarg
|
||||||
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
||||||
(app fun arg)
|
(app fun arg)
|
||||||
|
@ -22,4 +22,4 @@ Kind.if.def
|
|||||||
let txt = λlit λY λN (N (Kind.txt lit))
|
let txt = λlit λY λN (N (Kind.txt lit))
|
||||||
let hol = λnam λctx λY λN (N (Kind.hol nam ctx))
|
let hol = λnam λctx λY λN (N (Kind.hol nam ctx))
|
||||||
let var = λnam λidx λY λN (N (Kind.var nam idx))
|
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)
|
(~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N)
|
||||||
|
@ -22,4 +22,4 @@ Kind.if.slf
|
|||||||
let txt = λlit λY λN (N (Kind.txt lit))
|
let txt = λlit λY λN (N (Kind.txt lit))
|
||||||
let hol = λnam λctx λY λN (N (Kind.hol nam ctx))
|
let hol = λnam λctx λY λN (N (Kind.hol nam ctx))
|
||||||
let var = λnam λidx λY λN (N (Kind.var nam idx))
|
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)
|
(~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
Kind.set
|
Kind.set
|
||||||
: Kind.Term
|
: Kind.Term
|
||||||
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
||||||
(set)
|
(set)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
Kind.u60
|
Kind.u60
|
||||||
: Kind.Term
|
: Kind.Term
|
||||||
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
= ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
|
||||||
u60
|
u60
|
||||||
|
14
book/List.begin.kind2
Normal file
14
book/List.begin.kind2
Normal file
@ -0,0 +1,14 @@
|
|||||||
|
// Removes the last element
|
||||||
|
List.begin
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(list: (List A))
|
||||||
|
(List A)
|
||||||
|
= λA λlist
|
||||||
|
let P = λx(List A)
|
||||||
|
let cons = λx0 λxs
|
||||||
|
let P = λx(List A)
|
||||||
|
let cons = λx1 λxs (List.cons A x0 (List.begin A (List.cons A x1 xs)))
|
||||||
|
let nil = (List.nil A)
|
||||||
|
(~xs P cons nil)
|
||||||
|
let nil = (List.nil A)
|
||||||
|
(~list P cons nil)
|
71
book/QBool.kind2
Normal file
71
book/QBool.kind2
Normal file
@ -0,0 +1,71 @@
|
|||||||
|
// Ideal:
|
||||||
|
// QBool.true : QBool = ~λP (#0, λx x)
|
||||||
|
// QBool.false : QBool = ~λP (#1, λx x)
|
||||||
|
//
|
||||||
|
// QBool : * =
|
||||||
|
// $self
|
||||||
|
// ∀(P: ∀(x: QBool) *)
|
||||||
|
// Σ(t: #U60)
|
||||||
|
// ∀(x: match t {
|
||||||
|
// 0: (P QBool.true)
|
||||||
|
// 1: (P QBool.false)
|
||||||
|
// +: Empty
|
||||||
|
// })
|
||||||
|
// (P self)
|
||||||
|
//
|
||||||
|
// QBool.match
|
||||||
|
// : ∀(a: QBool)
|
||||||
|
// ∀(P: ∀(x: QBool) *)
|
||||||
|
// ∀(t: (P QBool.true))
|
||||||
|
// ∀(f: (P QBool.false))
|
||||||
|
// (P a)
|
||||||
|
// = λa λP λt λf
|
||||||
|
// let (tag, val) = (~a P)
|
||||||
|
// #match tag = tag {
|
||||||
|
// #0: (val t)
|
||||||
|
// #1: (val f)
|
||||||
|
// #+: (val λe (Empty.absurd e *))
|
||||||
|
// }
|
||||||
|
|
||||||
|
QBool.true : QBool =
|
||||||
|
~λP ~λS λp (p #0 λx x)
|
||||||
|
|
||||||
|
QBool.false : QBool =
|
||||||
|
~λP ~λS λp (p #1 λx x)
|
||||||
|
|
||||||
|
QBool : * =
|
||||||
|
$self
|
||||||
|
∀(P: ∀(x: QBool) *)
|
||||||
|
(Sigma #U60 λt
|
||||||
|
∀(x: #match t = t {
|
||||||
|
#0: (P QBool.true)
|
||||||
|
#+: #match t = t-1 {
|
||||||
|
#0: (P QBool.false)
|
||||||
|
#+: ∀(x: Empty) *
|
||||||
|
}: *
|
||||||
|
}: *)
|
||||||
|
(P self))
|
||||||
|
|
||||||
|
QBool.match
|
||||||
|
: ∀(a: QBool)
|
||||||
|
∀(P: ∀(x: QBool) *)
|
||||||
|
∀(t: (P QBool.true))
|
||||||
|
∀(f: (P QBool.false))
|
||||||
|
(P a)
|
||||||
|
= λa λP λt λf
|
||||||
|
(~(~a P) λx(P a) λtag #match tag = tag {
|
||||||
|
#0: λx (x t)
|
||||||
|
#+: λx ((#match tag-1 = tag-1 {
|
||||||
|
#0: λx (x f)
|
||||||
|
#+: λx (x λe (Empty.absurd e *))
|
||||||
|
}: ∀(x: ∀(x: #match tag-1 = tag-1 {
|
||||||
|
#0: (P QBool.false)
|
||||||
|
#+: ∀(x: Empty) *
|
||||||
|
}: *) (P a)) (P a)) x)
|
||||||
|
}: ∀(x: (∀(x: #match tag = tag {
|
||||||
|
#0: (P QBool.true)
|
||||||
|
#+: #match tag-1 = tag-1 {
|
||||||
|
#0: (P QBool.false)
|
||||||
|
#+: ∀(x: Empty) *
|
||||||
|
}: *
|
||||||
|
}: *) (P a))) (P a))
|
11
book/QUnit.kind2
Normal file
11
book/QUnit.kind2
Normal file
@ -0,0 +1,11 @@
|
|||||||
|
QUnit.one : QUnit =
|
||||||
|
~λP ~λSP λnew (new #0 λone one)
|
||||||
|
|
||||||
|
QUnit : * =
|
||||||
|
$self
|
||||||
|
∀(P: ∀(x: QUnit) *)
|
||||||
|
(Sigma #U60 λtag
|
||||||
|
#match tag = tag {
|
||||||
|
#0: ∀(one: (P QUnit.one)) (P self)
|
||||||
|
#+: Empty
|
||||||
|
}: *)
|
9
book/Sigma.kind2
Normal file
9
book/Sigma.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
Sigma
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(B: ∀(x: A) *)
|
||||||
|
*
|
||||||
|
= λA λB
|
||||||
|
$self
|
||||||
|
∀(P: ∀(x: (Sigma A B)) *)
|
||||||
|
∀(new: ∀(a: A) ∀(b: (B a)) (P (Sigma.new A B a b)))
|
||||||
|
(P self)
|
9
book/Sigma.new.kind2
Normal file
9
book/Sigma.new.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
Sigma.new
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(B: ∀(x: A) *)
|
||||||
|
∀(a: A)
|
||||||
|
∀(b: (B a))
|
||||||
|
(Sigma A B)
|
||||||
|
= λA λB λa λb
|
||||||
|
~λP λnew (new a b)
|
||||||
|
|
5
book/String.begin.kind2
Normal file
5
book/String.begin.kind2
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
String.begin
|
||||||
|
: ∀(str: String)
|
||||||
|
String
|
||||||
|
= λstr
|
||||||
|
(List.begin Char str)
|
8
book/String.indent.kind2
Normal file
8
book/String.indent.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
String.indent
|
||||||
|
: ∀(tab: Nat)
|
||||||
|
String
|
||||||
|
= λtab
|
||||||
|
let P = λx(String)
|
||||||
|
let succ = λtab.pred (String.cons ' ' (String.cons ' ' (String.indent tab.pred)))
|
||||||
|
let zero = String.nil
|
||||||
|
(~tab P succ zero)
|
16
book/String.unpar.kind2
Normal file
16
book/String.unpar.kind2
Normal file
@ -0,0 +1,16 @@
|
|||||||
|
// If first char is '(', remove first and last
|
||||||
|
// FIXME: check if last matches
|
||||||
|
String.unpar
|
||||||
|
: ∀(fst: Char)
|
||||||
|
∀(lst: Char)
|
||||||
|
∀(str: String)
|
||||||
|
String
|
||||||
|
= λfst λlst λstr
|
||||||
|
let P = λx(String)
|
||||||
|
let cons = λhead λtail
|
||||||
|
let P = λx∀(head:Char)∀(tail:String)String
|
||||||
|
let true = λheadλtail(String.begin tail)
|
||||||
|
let false = λheadλtail(String.cons head tail)
|
||||||
|
((~(Char.equal head fst) P true false) head tail)
|
||||||
|
let nil = String.nil
|
||||||
|
(~str P cons nil)
|
11
book/U60.match.kind2
Normal file
11
book/U60.match.kind2
Normal file
@ -0,0 +1,11 @@
|
|||||||
|
U60.match
|
||||||
|
: ∀(x: #U60)
|
||||||
|
∀(P: ∀(x: #U60) *)
|
||||||
|
∀(s: ∀(x: #U60) (P #(+ #1 x)))
|
||||||
|
∀(z: (P #0))
|
||||||
|
(P x)
|
||||||
|
= λx λP λs λz
|
||||||
|
#match self = x {
|
||||||
|
#0: z
|
||||||
|
#+: (s self-1)
|
||||||
|
}: (P self)
|
7
book/Unit.match.kind2
Normal file
7
book/Unit.match.kind2
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
Unit.match
|
||||||
|
: ∀(x: Unit)
|
||||||
|
∀(P: ∀(x: Unit) *)
|
||||||
|
∀(o: (P Unit.one))
|
||||||
|
(P x)
|
||||||
|
= λx λP λo
|
||||||
|
(~x P o)
|
4
book/compile.kind2
Normal file
4
book/compile.kind2
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
compile : String = (Kind.Book.to_hvm (Kind.Book.parse `test9
|
||||||
|
: String
|
||||||
|
= (String.unpar '(' ')' "((foo))")
|
||||||
|
`))
|
@ -1,5 +0,0 @@
|
|||||||
oxi
|
|
||||||
: ∀(b: Bool)
|
|
||||||
(Equal Bool b (Bool.not (Bool.not b)))
|
|
||||||
= λb
|
|
||||||
(~b ?P ?T ?F)
|
|
14
book/test10.kind2
Normal file
14
book/test10.kind2
Normal file
@ -0,0 +1,14 @@
|
|||||||
|
// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
|
||||||
|
_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat)))
|
||||||
|
_exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m (Kind.all "x" P λx(P))) (Kind.app n P)))))
|
||||||
|
|
||||||
|
// C2 : Nat = λs λz (s (s z))
|
||||||
|
_C2 = _Nat
|
||||||
|
_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
|
||||||
|
|
||||||
|
// Checks if `(work 2^4)` is propositionally equal to `true`
|
||||||
|
test10
|
||||||
|
: String
|
||||||
|
= let term = (Kind.app (Kind.app _exp _c2) _c2)
|
||||||
|
(Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)
|
||||||
|
|
@ -1,6 +1,21 @@
|
|||||||
test7.book
|
test7.book
|
||||||
: String
|
: String
|
||||||
= `Test : Kind.Term = (Kind.lam "f" λf(Kind.lam "x" λx(Kind.app f (Kind.app f x))))`
|
= `
|
||||||
|
// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
|
||||||
|
_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat)))
|
||||||
|
_exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m (Kind.all "x" P λx(P))) (Kind.app n P)))))
|
||||||
|
|
||||||
|
// C2 : Nat = λs λz (s (s z))
|
||||||
|
_C2 = _Nat
|
||||||
|
_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
|
||||||
|
|
||||||
|
// Checks if (work 2^4) is propositionally equal to true
|
||||||
|
test10
|
||||||
|
: String
|
||||||
|
= let term = (Kind.app (Kind.app _exp _c2) _c2)
|
||||||
|
(Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)
|
||||||
|
|
||||||
|
`
|
||||||
|
|
||||||
test7
|
test7
|
||||||
: String
|
: String
|
||||||
|
3
book/test9.kind2
Normal file
3
book/test9.kind2
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
test9
|
||||||
|
: String
|
||||||
|
= (String.unpar '(' ')' "((foo))")
|
37
kind2.hvm1
37
kind2.hvm1
@ -123,9 +123,10 @@
|
|||||||
(Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
(Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||||
(Reduce.op2 r opr fst snd) = (Op2 opr fst snd)
|
(Reduce.op2 r opr fst snd) = (Op2 opr fst snd)
|
||||||
|
|
||||||
(Reduce.mat r nam (Num 0) z s p) = (Reduce r z)
|
(Reduce.mat r nam (Num 0) z s p) = (Reduce r z)
|
||||||
(Reduce.mat r nam (Num n) z s p) = (Reduce r (s (Num (- n 1))))
|
(Reduce.mat r nam (Num n) z s p) = (Reduce r (s (Num (- n 1))))
|
||||||
(Reduce.mat r nam val z s p) = (Mat nam val z s p)
|
(Reduce.mat r nam (Op2 ADD (Num 1) k) z s p) = (Reduce r (s k))
|
||||||
|
(Reduce.mat r nam val z s p) = (Mat nam val z s p)
|
||||||
|
|
||||||
(Reduce.txt r (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
|
(Reduce.txt r (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||||
(Reduce.txt r String.nil) = (Reduce 1 Book.String.nil)
|
(Reduce.txt r String.nil) = (Reduce 1 Book.String.nil)
|
||||||
@ -154,25 +155,14 @@
|
|||||||
// --------
|
// --------
|
||||||
|
|
||||||
// Check if two terms are identical. If not...
|
// Check if two terms are identical. If not...
|
||||||
(Equal a b dep) = (Equal.unify.a a λx(x) b dep)
|
(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
||||||
//(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
|
||||||
|
|
||||||
// ...
|
|
||||||
(Equal.unify.a (App a.fun a.arg) as b dep) = (Equal.unify.a a.fun λk(as (App k a.arg)) b dep)
|
|
||||||
(Equal.unify.a (Hol a.nam a.ctx) as b dep) = (Debug dep ["Found: ?" a.nam " = " (Show b dep)] 1)
|
|
||||||
(Equal.unify.a a as b dep) = (Equal.unify.b (as a) b λx(x) dep)
|
|
||||||
|
|
||||||
// ...
|
|
||||||
(Equal.unify.b a (App b.fun b.arg) bs dep) = (Equal.unify.b a b.fun λk(bs (App k b.arg)) dep)
|
|
||||||
(Equal.unify.b a (Hol b.nam b.ctx) bs dep) = (Debug dep ["Found: ?" b.nam " = " (Show a dep)] 1)
|
|
||||||
(Equal.unify.b a b bs dep) = let b = (bs b); (Equal.minor (Identical a b dep) a b dep)
|
|
||||||
|
|
||||||
// Check if they're identical after a minor weak reduction. If not...
|
// Check if they're identical after a minor weak reduction. If not...
|
||||||
(Equal.minor 0 a b dep) = (Equal.major (Identical (Reduce 0 a) (Reduce 0 b) dep) a b dep)
|
(Equal.minor 0 a b dep) = let a = (Reduce 0 a); let b = (Reduce 0 b); (Equal.major (Identical a b dep) a b dep)
|
||||||
(Equal.minor 1 a b dep) = 1
|
(Equal.minor 1 a b dep) = 1
|
||||||
|
|
||||||
// Check if they're identical after a major weak reduction. If not...
|
// Check if they're identical after a major weak reduction. If not...
|
||||||
(Equal.major 0 a b dep) = (Equal.enter (Identical (Reduce 1 a) (Reduce 1 b) dep) a b dep)
|
(Equal.major 0 a b dep) = let a = (Reduce 1 a); let b = (Reduce 1 b); (Equal.enter (Identical a b dep) a b dep)
|
||||||
(Equal.major 1 a b dep) = 1
|
(Equal.major 1 a b dep) = 1
|
||||||
|
|
||||||
// Check if they become identical after reducing fields.
|
// Check if they become identical after reducing fields.
|
||||||
@ -197,12 +187,15 @@
|
|||||||
(Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep)
|
(Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep)
|
||||||
(Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep)
|
(Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep)
|
||||||
(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||||
|
(Comparer rec (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||||
|
(Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||||
(Comparer rec U60 U60 dep) = 1
|
(Comparer rec U60 U60 dep) = 1
|
||||||
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||||
(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst a.snd dep) (rec b.fst b.snd dep))
|
(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst b.fst dep) (rec a.snd b.snd dep))
|
||||||
(Comparer rec (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (Concat a.nam "-1") dep)) (b.s (Var (Concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
(Comparer rec (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (Concat a.nam "-1") dep)) (b.s (Var (Concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||||
(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||||
(Comparer rec a b dep) = 0
|
(Comparer rec a b dep) = 0
|
||||||
|
//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0)
|
||||||
|
|
||||||
// Type-Checking
|
// Type-Checking
|
||||||
// -------------
|
// -------------
|
||||||
@ -322,7 +315,7 @@
|
|||||||
|
|
||||||
(Show (All nam inp bod) dep) = (Join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
(Show (All nam inp bod) dep) = (Join ["∀(" nam ": " (Show inp dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||||
(Show (Lam nam bod) dep) = (Join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
(Show (Lam nam bod) dep) = (Join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||||
(Show (App fun arg) dep) = (Join ["(" (Show.prune (Show fun dep)) " " (Show arg dep) ")"])
|
(Show (App fun arg) dep) = (Join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
|
||||||
(Show (Ann val typ) dep) = (Join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
(Show (Ann val typ) dep) = (Join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
||||||
(Show (Slf nam bod) dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
(Show (Slf nam bod) dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||||
(Show (Ins val) dep) = (Join ["~" (Show val dep)])
|
(Show (Ins val) dep) = (Join ["~" (Show val dep)])
|
||||||
@ -332,7 +325,7 @@
|
|||||||
(Show U60 dep) = "#U60"
|
(Show U60 dep) = "#U60"
|
||||||
(Show (Num val) dep) = (Join ["#" (U60.show val)])
|
(Show (Num val) dep) = (Join ["#" (U60.show val)])
|
||||||
(Show (Op2 opr fst snd) dep) = (Join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
|
(Show (Op2 opr fst snd) dep) = (Join ["#(" (Op2.show opr) " " (Show fst dep) " " (Show snd dep) ")"])
|
||||||
(Show (Mat nam x z s p) dep) = (Join ["match " nam " = " (Show x dep) " { #0 => " (Show z dep) "; #+ => " (Show (s (Var (Concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
|
(Show (Mat nam x z s p) dep) = (Join ["#match " nam " = " (Show x dep) " { #0: " (Show z dep) " #+: " (Show (s (Var (Concat nam "-1") dep)) (+ dep 1)) " }: " (Show (p (Var nam dep)) dep)])
|
||||||
(Show (Txt txt) dep) = (Join [Quote txt Quote])
|
(Show (Txt txt) dep) = (Join [Quote txt Quote])
|
||||||
(Show (Hol nam ctx) dep) = (Join ["?" nam])
|
(Show (Hol nam ctx) dep) = (Join ["?" nam])
|
||||||
(Show (Var nam idx) dep) = (Join [nam])
|
(Show (Var nam idx) dep) = (Join [nam])
|
||||||
@ -344,8 +337,8 @@
|
|||||||
(Show.trim (String.cons ' ' xs)) = xs
|
(Show.trim (String.cons ' ' xs)) = xs
|
||||||
(Show.trim str) = str
|
(Show.trim str) = str
|
||||||
|
|
||||||
(Show.prune (String.cons '(' xs)) = (Show.begin xs)
|
(Show.unwrap (String.cons '(' xs)) = (Show.begin xs)
|
||||||
(Show.prune str) = str
|
(Show.unwrap str) = str
|
||||||
|
|
||||||
(Show.begin (String.cons x (String.cons y String.nil))) = (String.cons x String.nil)
|
(Show.begin (String.cons x (String.cons y String.nil))) = (String.cons x String.nil)
|
||||||
(Show.begin (String.cons x xs)) = (String.cons x (Show.begin xs))
|
(Show.begin (String.cons x xs)) = (String.cons x (Show.begin xs))
|
||||||
|
Loading…
Reference in New Issue
Block a user