From e4b262f9d1ddd3a1d958cc6bb7e9820b0eaeb65e Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Wed, 21 Feb 2024 22:10:51 -0300 Subject: [PATCH] many things --- book/A.kind2 | 71 ++++++++++++++ book/Empty.absurd.kind2 | 5 + book/Empty.kind2 | 5 + book/Kind.Book.to_hvm.go.kind2 | 7 +- book/Kind.Book.to_hvm.kind2 | 2 +- book/Kind.Book.to_hvm.prelude.kind2 | 9 ++ book/Kind.Term.parser.mat.kind2 | 2 +- book/Kind.Term.show.go.kind2 | 4 +- book/Kind.Term.to_hvm.go.kind2 | 138 ++++++++++++++++++---------- book/Kind.Term.to_hvm.nl.kind2 | 10 ++ book/Kind.ann.kind2 | 2 +- book/Kind.app.kind2 | 2 +- book/Kind.if.def.kind2 | 2 +- book/Kind.if.slf.kind2 | 2 +- book/Kind.set.kind2 | 2 +- book/Kind.u60.kind2 | 2 +- book/List.begin.kind2 | 14 +++ book/QBool.kind2 | 71 ++++++++++++++ book/QUnit.kind2 | 11 +++ book/Sigma.kind2 | 9 ++ book/Sigma.new.kind2 | 9 ++ book/String.begin.kind2 | 5 + book/String.indent.kind2 | 8 ++ book/String.unpar.kind2 | 16 ++++ book/U60.match.kind2 | 11 +++ book/Unit.match.kind2 | 7 ++ book/compile.kind2 | 4 + book/oxi.kind2 | 5 - book/test10.kind2 | 14 +++ book/test7.kind2 | 17 +++- book/test9.kind2 | 3 + kind2.hvm1 | 37 +++----- 32 files changed, 416 insertions(+), 90 deletions(-) create mode 100644 book/A.kind2 create mode 100644 book/Empty.absurd.kind2 create mode 100644 book/Empty.kind2 create mode 100644 book/Kind.Book.to_hvm.prelude.kind2 create mode 100644 book/Kind.Term.to_hvm.nl.kind2 create mode 100644 book/List.begin.kind2 create mode 100644 book/QBool.kind2 create mode 100644 book/QUnit.kind2 create mode 100644 book/Sigma.kind2 create mode 100644 book/Sigma.new.kind2 create mode 100644 book/String.begin.kind2 create mode 100644 book/String.indent.kind2 create mode 100644 book/String.unpar.kind2 create mode 100644 book/U60.match.kind2 create mode 100644 book/Unit.match.kind2 create mode 100644 book/compile.kind2 delete mode 100644 book/oxi.kind2 create mode 100644 book/test10.kind2 create mode 100644 book/test9.kind2 diff --git a/book/A.kind2 b/book/A.kind2 new file mode 100644 index 00000000..300a2e42 --- /dev/null +++ b/book/A.kind2 @@ -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)) diff --git a/book/Empty.absurd.kind2 b/book/Empty.absurd.kind2 new file mode 100644 index 00000000..ea39b657 --- /dev/null +++ b/book/Empty.absurd.kind2 @@ -0,0 +1,5 @@ +Empty.absurd +: ∀(e: Empty) + ∀(P: *) + P += λe λP (~e λx(P)) diff --git a/book/Empty.kind2 b/book/Empty.kind2 new file mode 100644 index 00000000..12179db7 --- /dev/null +++ b/book/Empty.kind2 @@ -0,0 +1,5 @@ +Empty +: * += $self + ∀(P: ∀(x: Empty) *) + (P self) diff --git a/book/Kind.Book.to_hvm.go.kind2 b/book/Kind.Book.to_hvm.go.kind2 index 3f81e28c..e2b00e0c 100644 --- a/book/Kind.Book.to_hvm.go.kind2 +++ b/book/Kind.Book.to_hvm.go.kind2 @@ -6,12 +6,13 @@ Kind.Book.to_hvm.go let cons = λhead λtail let P = λx String.Concatenator let new = λhead.fst λhead.snd λnil + ((Kind.Text.show.go "F." ((Kind.Text.show.go head.fst) ((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.Book.to_hvm.go tail - nil))))))))) + nil))))))))))) (~head P new) let nil = λnil nil - (~book P cons nil) \ No newline at end of file + (~book P cons nil) diff --git a/book/Kind.Book.to_hvm.kind2 b/book/Kind.Book.to_hvm.kind2 index f9403a15..d0686f95 100644 --- a/book/Kind.Book.to_hvm.kind2 +++ b/book/Kind.Book.to_hvm.kind2 @@ -2,4 +2,4 @@ Kind.Book.to_hvm : ∀(book: Kind.Book) String = λbook - (String.Concatenator.build (Kind.Book.to_hvm.go book)) \ No newline at end of file + (String.Concatenator.build (Kind.Book.to_hvm.go book)) diff --git a/book/Kind.Book.to_hvm.prelude.kind2 b/book/Kind.Book.to_hvm.prelude.kind2 new file mode 100644 index 00000000..e620254d --- /dev/null +++ b/book/Kind.Book.to_hvm.prelude.kind2 @@ -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)) +` diff --git a/book/Kind.Term.parser.mat.kind2 b/book/Kind.Term.parser.mat.kind2 index 2ab7aa1b..932d38df 100644 --- a/book/Kind.Term.parser.mat.kind2 +++ b/book/Kind.Term.parser.mat.kind2 @@ -16,4 +16,4 @@ Kind.Term.parser.mat (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))))))))))))))))))) \ No newline at end of file + (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))))))))))))))))))) diff --git a/book/Kind.Term.show.go.kind2 b/book/Kind.Term.show.go.kind2 index 32361a00..60040975 100644 --- a/book/Kind.Term.show.go.kind2 +++ b/book/Kind.Term.show.go.kind2 @@ -80,7 +80,7 @@ Kind.Term.show.go ((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.Term.show.go (s (Kind.var (String.concat nam "-1") dep)) (Nat.succ dep)) ((Kind.Text.show.go " }: ") ((Kind.Term.show.go (p (Kind.var nam dep)) (Nat.succ dep)) nil)))))))))) @@ -96,4 +96,4 @@ Kind.Term.show.go 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) \ No newline at end of file + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var) diff --git a/book/Kind.Term.to_hvm.go.kind2 b/book/Kind.Term.to_hvm.go.kind2 index ba27fb45..a59464e2 100644 --- a/book/Kind.Term.to_hvm.go.kind2 +++ b/book/Kind.Term.to_hvm.go.kind2 @@ -1,73 +1,113 @@ Kind.Term.to_hvm.go : ∀(term: Kind.Term) ∀(dep: Nat) + ∀(inc: Bool) + ∀(tab: Nat) String.Concatenator -= λterm λdep += λterm λdep λinc λtab let P = λx String.Concatenator - let all = λnam λinp λbod - (Kind.Text.show.go "0") + let all = λnam λinp λbod λnil + ((Kind.Term.to_hvm.nl inc tab) + ((Kind.Text.show.go "0") + nil)) let lam = λnam λbod λnil + ((Kind.Term.to_hvm.nl inc tab) ((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.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)) + ((Kind.Term.to_hvm.go (bod (Kind.var nam dep)) (Nat.succ dep) Bool.true tab) nil)))))) - let set = - (Kind.Text.show.go "0") - let u60 = - (Kind.Text.show.go "0") - let num = λval - (U60.show.go val) + let app = λfun λarg λnil + ((Kind.Term.to_hvm.nl inc tab) + ((Kind.Text.show.go "(") + ((Kind.Term.to_hvm.go fun dep Bool.true tab) + ((Kind.Text.show.go " ") + ((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 + ((Kind.Term.to_hvm.nl inc tab) ((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.Term.to_hvm.go fst dep Bool.true tab) ((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 ")") - nil))))))) + nil)))))))) let mat = λnam λx λz λs λp λnil + ((Kind.Term.to_hvm.nl inc tab) ((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.Term.to_hvm.go z dep) + ((Kind.Term.to_hvm.go z dep Bool.true tab) ((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 "λ") + ((Kind.Text.show.go (String.cons '_' (String.concat nam "_1"))) + //((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 ")") - nil))))))))) + ((Kind.Text.show.go ")") + 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 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) \ No newline at end of file + ((Kind.Text.show.go ")") + nil)))))) + let hol = λnam λctx λnil + ((Kind.Term.to_hvm.nl inc tab) + ((Kind.Text.show.go "0") + 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) diff --git a/book/Kind.Term.to_hvm.nl.kind2 b/book/Kind.Term.to_hvm.nl.kind2 new file mode 100644 index 00000000..c7b3d0c0 --- /dev/null +++ b/book/Kind.Term.to_hvm.nl.kind2 @@ -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) + diff --git a/book/Kind.ann.kind2 b/book/Kind.ann.kind2 index 61003c96..cd35682b 100644 --- a/book/Kind.ann.kind2 +++ b/book/Kind.ann.kind2 @@ -4,4 +4,4 @@ Kind.ann Kind.Term = λval λtyp ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (ann val typ) \ No newline at end of file + (ann val typ) diff --git a/book/Kind.app.kind2 b/book/Kind.app.kind2 index 733a0adc..5ecc9704 100644 --- a/book/Kind.app.kind2 +++ b/book/Kind.app.kind2 @@ -4,4 +4,4 @@ Kind.app Kind.Term = λfun λarg ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (app fun arg) \ No newline at end of file + (app fun arg) diff --git a/book/Kind.if.def.kind2 b/book/Kind.if.def.kind2 index 8e9735e2..c861f5e6 100644 --- a/book/Kind.if.def.kind2 +++ b/book/Kind.if.def.kind2 @@ -22,4 +22,4 @@ Kind.if.def 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) \ No newline at end of file + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) diff --git a/book/Kind.if.slf.kind2 b/book/Kind.if.slf.kind2 index 534213af..23b77f77 100644 --- a/book/Kind.if.slf.kind2 +++ b/book/Kind.if.slf.kind2 @@ -22,4 +22,4 @@ Kind.if.slf 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) \ No newline at end of file + (~term P all lam app ann slf ins ref def set u60 num op2 mat txt hol var Y N) diff --git a/book/Kind.set.kind2 b/book/Kind.set.kind2 index 3e3d46e4..4742bfb4 100644 --- a/book/Kind.set.kind2 +++ b/book/Kind.set.kind2 @@ -1,4 +1,4 @@ Kind.set : Kind.Term = ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - (set) \ No newline at end of file + (set) diff --git a/book/Kind.u60.kind2 b/book/Kind.u60.kind2 index 7e2db33d..20d74dd8 100644 --- a/book/Kind.u60.kind2 +++ b/book/Kind.u60.kind2 @@ -1,4 +1,4 @@ Kind.u60 : Kind.Term = ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar - u60 \ No newline at end of file + u60 diff --git a/book/List.begin.kind2 b/book/List.begin.kind2 new file mode 100644 index 00000000..28d1240c --- /dev/null +++ b/book/List.begin.kind2 @@ -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) diff --git a/book/QBool.kind2 b/book/QBool.kind2 new file mode 100644 index 00000000..d5f6f224 --- /dev/null +++ b/book/QBool.kind2 @@ -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)) diff --git a/book/QUnit.kind2 b/book/QUnit.kind2 new file mode 100644 index 00000000..53c8da9f --- /dev/null +++ b/book/QUnit.kind2 @@ -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 + }: *) diff --git a/book/Sigma.kind2 b/book/Sigma.kind2 new file mode 100644 index 00000000..0933f413 --- /dev/null +++ b/book/Sigma.kind2 @@ -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) diff --git a/book/Sigma.new.kind2 b/book/Sigma.new.kind2 new file mode 100644 index 00000000..2a98edb8 --- /dev/null +++ b/book/Sigma.new.kind2 @@ -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) + diff --git a/book/String.begin.kind2 b/book/String.begin.kind2 new file mode 100644 index 00000000..32905c77 --- /dev/null +++ b/book/String.begin.kind2 @@ -0,0 +1,5 @@ +String.begin +: ∀(str: String) + String += λstr + (List.begin Char str) diff --git a/book/String.indent.kind2 b/book/String.indent.kind2 new file mode 100644 index 00000000..3bc3f7a9 --- /dev/null +++ b/book/String.indent.kind2 @@ -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) diff --git a/book/String.unpar.kind2 b/book/String.unpar.kind2 new file mode 100644 index 00000000..126fe606 --- /dev/null +++ b/book/String.unpar.kind2 @@ -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) diff --git a/book/U60.match.kind2 b/book/U60.match.kind2 new file mode 100644 index 00000000..b730f6d6 --- /dev/null +++ b/book/U60.match.kind2 @@ -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) diff --git a/book/Unit.match.kind2 b/book/Unit.match.kind2 new file mode 100644 index 00000000..6374c990 --- /dev/null +++ b/book/Unit.match.kind2 @@ -0,0 +1,7 @@ +Unit.match +: ∀(x: Unit) + ∀(P: ∀(x: Unit) *) + ∀(o: (P Unit.one)) + (P x) += λx λP λo + (~x P o) diff --git a/book/compile.kind2 b/book/compile.kind2 new file mode 100644 index 00000000..f2058d9a --- /dev/null +++ b/book/compile.kind2 @@ -0,0 +1,4 @@ +compile : String = (Kind.Book.to_hvm (Kind.Book.parse `test9 +: String += (String.unpar '(' ')' "((foo))") +`)) \ No newline at end of file diff --git a/book/oxi.kind2 b/book/oxi.kind2 deleted file mode 100644 index 19e8e896..00000000 --- a/book/oxi.kind2 +++ /dev/null @@ -1,5 +0,0 @@ -oxi -: ∀(b: Bool) - (Equal Bool b (Bool.not (Bool.not b))) -= λb - (~b ?P ?T ?F) diff --git a/book/test10.kind2 b/book/test10.kind2 new file mode 100644 index 00000000..e3965684 --- /dev/null +++ b/book/test10.kind2 @@ -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) + diff --git a/book/test7.kind2 b/book/test7.kind2 index 70bb132f..25be0cb0 100644 --- a/book/test7.kind2 +++ b/book/test7.kind2 @@ -1,6 +1,21 @@ test7.book : 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 : String diff --git a/book/test9.kind2 b/book/test9.kind2 new file mode 100644 index 00000000..405cd93d --- /dev/null +++ b/book/test9.kind2 @@ -0,0 +1,3 @@ +test9 +: String += (String.unpar '(' ')' "((foo))") diff --git a/kind2.hvm1 b/kind2.hvm1 index 10692c64..05ffb8b3 100644 --- a/kind2.hvm1 +++ b/kind2.hvm1 @@ -123,9 +123,10 @@ (Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> 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 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 (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 (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.nil) = (Reduce 1 Book.String.nil) @@ -154,25 +155,14 @@ // -------- // 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.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) +(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep) // 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 // 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 // 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 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) 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 (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 (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt) (Comparer rec a b dep) = 0 +//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0) // 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 (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 (Slf nam bod) dep) = (Join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))]) (Show (Ins val) dep) = (Join ["~" (Show val dep)]) @@ -332,7 +325,7 @@ (Show U60 dep) = "#U60" (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 (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 (Hol nam ctx) dep) = (Join ["?" nam]) (Show (Var nam idx) dep) = (Join [nam]) @@ -344,8 +337,8 @@ (Show.trim (String.cons ' ' xs)) = xs (Show.trim str) = str -(Show.prune (String.cons '(' xs)) = (Show.begin xs) -(Show.prune str) = str +(Show.unwrap (String.cons '(' xs)) = (Show.begin xs) +(Show.unwrap str) = str (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))