HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-08-17 00:20:32 +03:00
Code Issues Packages Projects Releases Wiki Activity

U60 to U48, use let to make match expr, WIPs

Browse Source
This commit is contained in:
Victor Taelin 2024-07-05 10:06:49 -03:00
parent 24510cedbe
commit d409b9d5b7
68 changed files with 252 additions and 761 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.gitignore vendored
View File

@ -18,3 +18,7 @@ guide.txt
-e
# Hidden files
.*
# .bak files
*.bak
# all tmp/ directories
tmp/

2
README.md
View File

@ -40,7 +40,7 @@ complex, hardcoded datatype system. It compiles to
```javascript
// The Fibonacci function
fib (n: U60) : U60 =
fib (n: U48) : U48 =
switch n {
0: 0
1: 1

2
book/Char/_.kind2
View File

@ -1,3 +1,3 @@
Char
: *
= U60
= U48

2
book/Char/equal.kind2
View File

@ -1,2 +1,2 @@
equal (a: Char) (b: Char) : Bool =
(U60/equal a b)
(U48/equal a b)

4
book/Char/is_between.kind2
View File

@ -1,4 +1,4 @@
is_between (min: Char) (max: Char) (chr: Char) : Bool =
(Bool/and
(U60/to_bool (>= chr min))
(U60/to_bool (<= chr max)))
(U48/to_bool (>= chr min))
(U48/to_bool (<= chr max)))

2
book/Kind/Term.kind2
View File

@ -37,7 +37,7 @@ Kind.Term
)
∀(set: (P Kind.set))
∀(u60: (P Kind.u60))
∀(num: ∀(val: U60) (P (Kind.num val)))
∀(num: ∀(val: U48) (P (Kind.num val)))
∀(op2:
∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term)
(P (Kind.op2 opr fst snd))

2
book/Kind/Term/parser/chr.kind2
View File

@ -8,7 +8,7 @@ Kind.Term.parser.chr
(Parser.text "'")
λ_
(Kind.Term.parser.bind
U60
U48
Parser.char
λchr
(Kind.Term.parser.bind

4
book/Kind/Term/parser/num.kind2
View File

@ -8,8 +8,8 @@ Kind.Term.parser.num
(Parser.text "")
λ_
(Kind.Term.parser.bind
U60
U60.parser.decimal
U48
U48.parser.decimal
λnum (Kind.Term.parser.pure λscp (Kind.num num))
)
)

4
book/Kind/Term/parser/u60.kind2
View File

@ -2,10 +2,10 @@ Kind.Term.parser.u60
: (Parser.Guard Kind.PreTerm)
= (Parser.Guard.text
Kind.PreTerm
"U60"
"U48"
(Kind.Term.parser.bind
Unit
(Parser.text "U60")
(Parser.text "U48")
λ_ (Kind.Term.parser.pure λscp Kind.u60)
)
)

4
book/Kind/Term/show/go.kind2
View File

@ -104,8 +104,8 @@ Kind.Term.show.go
)
)
use set = λnil (Kind.Text.show.go "*" nil)
use u60 = λnil (Kind.Text.show.go "U60" nil)
use num = λval λnil (Kind.Text.show.go "" (U60.show.go val nil))
use u60 = λnil (Kind.Text.show.go "U48" nil)
use num = λval λnil (Kind.Text.show.go "" (U48.show.go val nil))
use op2 = λopr λfst λsnd λnil
(Kind.Text.show.go
"("

2
book/Kind/comparer.kind2
View File

@ -77,7 +77,7 @@ Kind.comparer
(Kind.if.u60 b P Y N dep)
use num = λa.val λb λdep
use P = ∀(dep: Nat) Bool
use Y = λb.val λdep (U60.equal a.val b.val)
use Y = λb.val λdep (U48.equal a.val b.val)
use N = λval λdep Bool.false
(Kind.if.num b P Y N dep)
use op2 = λa.opr λa.fst λa.snd λb λdep

4
book/Kind/if/num.kind2
View File

@ -1,12 +1,12 @@
Kind.if.num
: ∀(term: Kind.Term)
∀(P: *)
∀(Y: ∀(val: U60) P)
∀(Y: ∀(val: U48) P)
∀(N: ∀(val: Kind.Term) P)
P
= λterm λP λY λN
use P = λx
∀(Y: ∀(val: U60) P) ∀(N: ∀(val: Kind.Term) P) P
∀(Y: ∀(val: U48) P) ∀(N: ∀(val: Kind.Term) P) P
use all = λnam λinp λbod λY λN (N (Kind.all nam inp bod))
use lam = λnam λbod λY λN (N (Kind.lam nam bod))
use app = λfun λarg λY λN (N (Kind.app fun arg))

2
book/Kind/num.kind2
View File

@ -1,5 +1,5 @@
Kind.num
: ∀(val: U60) Kind.Term
: ∀(val: U48) Kind.Term
= λval
~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
(num val)

4
book/Kind/reduce/op2.kind2
View File

@ -4,9 +4,9 @@ Kind.reduce.op2
= λopr λfst λsnd
use P = ∀(snd: Kind.Term) Kind.Term
use Y = λfst_val λsnd
use P = ∀(fst_val: U60) Kind.Term
use P = ∀(fst_val: U48) Kind.Term
use Y = λsnd_val λfst_val
use P = λx ∀(fst_val: U60) ∀(snd_val: U60) Kind.Term
use P = λx ∀(fst_val: U48) ∀(snd_val: U48) Kind.Term
use add = λfst_val λsnd_val (Kind.num (+ fst_val snd_val))
use mul = λfst_val λsnd_val (Kind.num (* fst_val snd_val))
use sub = λfst_val λsnd_val (Kind.num (- fst_val snd_val))

2
book/List/sum.kind2
View File

@ -1,4 +1,4 @@
sum (xs: (List U60)): U60 =
sum (xs: (List U48)): U48 =
match xs {
++: (+ xs.head (sum xs.tail))
[]: 0

8
book/Nat/is_zero.kind2
View File

@ -32,7 +32,7 @@ def to_map(t):
case Arr/Node:
return merge(to_map(t.a), to_map(t.b))
# ToArr : U60 -> Map -> Arr
# ToArr : U48 -> Map -> Arr
def to_arr(x, m):
match m:
case Map_/Free:
@ -58,7 +58,7 @@ def merge(a, b):
case Map_/Both:
return Map_/Both{ a: merge(a.a, b.a), b: merge(a.b, b.b) }
# Radix : U60 -> Map
# Radix : U48 -> Map
def radix(n):
r = Map_/Used
r = swap(n & 1, r, Map_/Free)
@ -105,7 +105,7 @@ def reverse(t):
case Arr/Node:
return Arr/Node{ a: reverse(t.b), b: reverse(t.a) }
# Sum : Arr -> U60
# Sum : Arr -> U48
def sum(t):
match t:
case Arr/Null:
@ -115,7 +115,7 @@ def sum(t):
case Arr/Node:
return sum(t.a) + sum(t.b)
# Gen : U60 -> Arr
# Gen : U48 -> Arr
def gen(n):
return gen_go(n, 0)

2
book/QBool/_.kind2
View File

@ -3,7 +3,7 @@ QBool
= $(self: QBool)
∀(P: ∀(x: QBool) *)
(Sigma
U60
U48
λt
∀(x:
switch t = t {

2
book/QBool2/_.kind2
View File

@ -3,7 +3,7 @@ QBool2
= $(self: QBool2)
∀(P: ∀(x: QBool2) *)
∀(new:
∀(tag: U60)
∀(tag: U48)
switch tag = tag {
0: (P QBool2.true)
_: switch tag_1 = tag-1 {

2
book/QUnit/_.kind2
View File

@ -3,7 +3,7 @@ QUnit
= $(self: QUnit)
∀(P: ∀(x: QUnit) *)
(Sigma
U60
U48
λtag
switch tag = tag {
0: ∀(one: (P QUnit.one)) (P self)

2
book/String/cmp.kind2
View File

@ -9,7 +9,7 @@ String/cmp
use ltn = Cmp/ltn
use eql = (cmp a.tail b.tail)
use gtn = Cmp/gtn
(~(U60/cmp a.head b.head) P ltn eql gtn)
(~(U48/cmp a.head b.head) P ltn eql gtn)
use nil = λa.head λa.tail Cmp/gtn
(~b P cons nil a.head a.tail)
use nil = λb

2
book/String/equal.kind2
View File

@ -4,7 +4,7 @@ String/equal (a: String) (b: String) : Bool =
use P = λx ∀(a.head: Char) ∀(a.tail: String) Bool
use cons = λb.head λb.tail λa.head λa.tail
(Bool/and
(U60/equal a.head b.head)
(U48/equal a.head b.head)
(String/equal a.tail b.tail)
)
use nil = λa.head λa.tail Bool/false

2
book/Tree/gen.kind2
View File

@ -1,6 +1,6 @@
use Tree/{node,leaf}
gen (n: U60) (x: U60) : (Tree U60) =
gen (n: U48) (x: U48) : (Tree U48) =
switch n {
0: leaf
_: (node x (gen n-1 (+ (* x 2) 1)) (gen n-1 (+ (* x 2) 2)))

2
book/Tree/sum.kind2
View File

@ -7,7 +7,7 @@ use Tree/{node,leaf}
// / \ / \ (4) (9)
// (1) (2) (3) (4)
sum (x: (Tree U60)) : U60 =
sum (x: (Tree U48)) : U48 =
fold x {
node: (+ x.val (+ x.lft x.rgt))
leaf: 0

2
book/U60/Map.kind2
View File

@ -1,2 +1,2 @@
Map (V: *) : * =
(BBT U60 V)
(BBT U48 V)

5
book/U60/abs_diff.kind2
View File

@ -1,7 +1,8 @@
use Bool/{true,false}
abs_diff (a: U60) (b: U60) : U60 =
match Bool/true {
abs_diff (a: U48) (b: U48) : U48 =
let x = (U48/to_bool (< a b))
match x {
true: (- b a)
false: (- a b)
}

6
book/U60/cmp.kind2
View File

@ -1,4 +1,4 @@
cmp (a: U60) (b: U60) : Cmp =
(U60/if (== a b)
(U60/if (< a b) Cmp/gtn Cmp/ltn)
cmp (a: U48) (b: U48) : Cmp =
(U48/if (== a b)
(U48/if (< a b) Cmp/gtn Cmp/ltn)
Cmp/eql)

2
book/U60/equal.kind2
View File

@ -1,6 +1,6 @@
use Bool/{true,false}
equal (a: U60) (b: U60) : Bool =
equal (a: U48) (b: U48) : Bool =
switch x = (== a b) {
0: false
_: true

2
book/U60/fib.kind2
View File

@ -1,4 +1,4 @@
fib (n: U60) : U60 =
fib (n: U48) : U48 =
switch n {
0: 0
1: 1

2
book/U60/from_nat.kind2
View File

@ -1,6 +1,6 @@
use Nat/{succ,zero}
from_nat (n: Nat) : U60 =
from_nat (n: Nat) : U48 =
match n {
succ: (+ 1 (from_nat n.pred))
zero: 0

2
book/U60/if.kind2
View File

@ -1,4 +1,4 @@
if <P> (x: U60) (t: P) (f: P) : P =
if <P> (x: U48) (t: P) (f: P) : P =
switch x {
0: t
_: f

2
book/U60/match.kind2
View File

@ -1,4 +1,4 @@
U60.match (x: U60) (P: U60 -> *) (s: U60 -> (P (+ 1 x))) (z: (P 0)) : (P x) =
U48.match (x: U48) (P: U48 -> *) (s: U48 -> (P (+ 1 x))) (z: (P 0)) : (P x) =
switch x {
0: z
_: (s x-1)

2
book/U60/max.kind2
View File

@ -1,4 +1,4 @@
max (a: U60) (b: U60) : U60 =
max (a: U48) (b: U48) : U48 =
switch x = (< a b) {
0: a
_: b

2
book/U60/min.kind2
View File

@ -1,4 +1,4 @@
min (a: U60) (b: U60) : U60 =
min (a: U48) (b: U48) : U48 =
switch x = (< a b) {
0: b
_: a

4
book/U60/name.kind2
View File

@ -1,2 +1,2 @@
U60/name (n: U60) : String =
(String/Chunk/build (U60/name/go (+ n 1)))
U48/name (n: U48) : String =
(String/Chunk/build (U48/name/go (+ n 1)))

6
book/U60/name/go.kind2
View File

@ -1,11 +1,11 @@
U60.name.go
: ∀(n: U60) String.Chunk
U48.name.go
: ∀(n: U48) String.Chunk
= λn
switch n = n {
0: λnil nil
_: λnil
(String/cons
(+ 97 (% n-1 26))
(U60.name.go (/ n-1 26) nil)
(U48.name.go (/ n-1 26) nil)
)
}: String.Chunk

10
book/U60/parser/decimal.kind2
View File

@ -1,16 +1,16 @@
U60.parser.decimal
: (Parser U60)
U48.parser.decimal
: (Parser U48)
= (Parser.bind
String
U60
U48
Parser.decimal
λchars
(Parser.pure
U60
U48
(List.fold
Char
chars
∀(r: U60) U60
∀(r: U48) U48
λh λt λr (t (+ (- h 48) (* r 10)))
λr r
0

4
book/U60/show.kind2
View File

@ -1,2 +1,2 @@
U60/show (n: U60) : String =
(String/Chunk/build (U60/show/go n))
U48/show (n: U48) : String =
(String/Chunk/build (U48/show/go n))

2
book/U60/show/go.kind2
View File

@ -1,4 +1,4 @@
go (n: U60) : String/Chunk =
go (n: U48) : String/Chunk =
switch x = (< n 10) {
0: λnil (go (/ n 10) (String/cons (+ 48 (% n 10)) nil))
_: λnil (String/cons (+ 48 n) nil)

2
book/U60/sum.kind2
View File

@ -1,4 +1,4 @@
sum (n: U60) : U60 =
sum (n: U48) : U48 =
switch n {
0: 0
_: (+ n (sum n-1))

2
book/U60/to_bool.kind2
View File

@ -1,6 +1,6 @@
use Bool/{true,false}
to_bool (x: U60) : Bool =
to_bool (x: U48) : Bool =
switch x {
0: false
_: true

59
book/tmp/_OBLITERATE.kind2
View File

@ -1,59 +0,0 @@
// Bool : * = ∀(P: *) ∀(s: P) ∀(z: P) P
T_BOOL = Kind.set
T_Bool = (Kind.all "P" Kind.set λP(Kind.all "t" P λt(Kind.all "f" P λf(P))))
// True : Bool = λP λt λf t
T_TRUE = T_Bool
T_True = (Kind.lam "P" λP(Kind.lam "t" λt(Kind.lam "f" λf(t))))
// False : Bool = λP λt λf f
T_FALSE = T_Bool
T_False = (Kind.lam "P" λP(Kind.lam "t" λt(Kind.lam "f" λf(f))))
// AND : ∀(x: Bool) ∀(y: Bool) Bool = λx λy (x Bool y False)
T_AND = (Kind.all "x" T_Bool λx(Kind.all "y" T_Bool λy(T_Bool)))
T_and = (Kind.lam "x" λx(Kind.lam "y" λy(Kind.app (Kind.app (Kind.app x T_Bool) y) T_False)))
// Nat : * = ∀(P: *) ∀(s: ∀(x: P) P) ∀(z: P) P
T_NAT = Kind.set
T_Nat = (Kind.all "P" Kind.set λP(Kind.all "s" (Kind.all "x" P λx(P)) λs(Kind.all "z" P λz(P))))
// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
T_EXP = (Kind.all "n" T_Nat λn(Kind.all "m" T_Nat λm(T_Nat)))
T_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))
T_C2 = T_Nat
T_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
// C4 : Nat = λs λz (s (s (s (s z))))
T_C4 = T_Nat
T_c4 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s (Kind.app s (Kind.app s z)))))))
// Equal : ∀(A: *) ∀(a: A) ∀(b: A) * = λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b)
T_EQUAL = (Kind.all "P" Kind.set λA(Kind.all "a" A λa(Kind.all "b" A λb(Kind.set))))
T_Equal = (Kind.lam "A" λA(Kind.lam "a" λa(Kind.lam "b" λb(Kind.all "P" (Kind.all "x" A λx(Kind.set)) λP(Kind.all "p" (Kind.app P a) λp(Kind.app P b))))))
// refl : ∀(A: *) ∀(a: A) (Equal A a a) = λA λa λP λp p
T_REFL = (Kind.all "A" Kind.set λA(Kind.all "a" A λa(Kind.app (Kind.app (Kind.app T_Equal A) a) a)))
T_refl = (Kind.lam "A" λA(Kind.lam "a" λa(Kind.lam "P" λP(Kind.lam "p" λp p))))
// WORK : ∀(n: Nat) Bool = λn (n ∀(x:Bool)Bool λpλb(Bool.and (p b) (p b)) λx(x) True)
T_WORK = (Kind.all "n" T_Nat λn(T_Bool))
T_work = (Kind.lam "n" λn(Kind.app (Kind.app (Kind.app (Kind.app n (Kind.all "x" T_Bool λx(T_Bool)))
(Kind.lam "p" λp(Kind.lam "b" λb(Kind.app (Kind.app (Kind.ann T_and T_AND) (Kind.app p b)) (Kind.app p b)))))
(Kind.lam "x" λx(x)))
T_True))
// RESULT : Bool = (work c3)
T_RESULT = T_Bool
T_result = (Kind.app (Kind.ann T_work T_WORK) (Kind.app (Kind.app T_exp T_c2) T_c4))
// MAIN : (Equal Bool result True) = λP λrefl refl
T_MAIN = (Kind.app (Kind.app (Kind.app T_Equal T_Bool) T_result) T_True)
T_main = (Kind.lam "P" λP(Kind.lam "refl" λrefl(refl)))
// Checks if `(work 2^4)` is propositionally equal to `true`
_OBLITERATE
: String
= (~(Kind.check T_main T_MAIN Nat.zero) λx(String) λt("check") "error")

70
book/tmp/_err.txt
View File

@ -1,70 +0,0 @@
QBool.switch
: ∀(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
switch tag = tag {
0: λx (x t)
+: λx
(switch tag_1 = tag-1 {
0: λx (x f)
+: λx (x λe (Empty.absurd e *))
}: ∀(x:
∀(x:
switch tag_1 = tag_1 {
0: (P QBool.false)
+: ∀(x: Empty) *
}: *
)
(P a)
)
(P a)
x
)
}: ∀(x:
∀(x:
switch tag = tag {
0: (P QBool.true)
+: switch tag_1 = tag-1 {
0: (P QBool.false)
+: ∀(x: Empty) *
}: *
}: *
)
(P a)
)
(P a)
)
QBool2.switch
: ∀(a: QBool2)
∀(P: ∀(x: QBool2) *)
∀(t: (P QBool2.true))
∀(f: (P QBool2.false))
(P a)
= λa λP λt λf
(~a
P
λtag
switch tag = tag {
0: t
+: switch tag_1 = tag-1 {
0: f
+: λe (~e λx *)
}: switch tag_1 = tag_1 {
0: (P QBool2.false)
+: ∀(e: Empty) *
}: *
}: switch tag = tag {
0: (P QBool2.true)
+: switch tag_1 = tag-1 {
0: (P QBool2.false)
+: ∀(e: Empty) *
}: *
}: *
)

BIN
book/tmp/_main
View File

Binary file not shown.

33
book/tmp/_main.hvm2
View File

@ -1,33 +0,0 @@
//WARNING: unsolved metas_
//WARNING: unsolved metas_
_Char = 0
_List = λ_T 0
_List_cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
_List_nil = λ_P λ_cons λ_nil _nil
_Nat = 0
_Nat_succ = λ_n λ_P λ_succ λ_zero (_succ _n)
_Nat_zero = λ_P λ_succ λ_zero _zero
_String = (_List _Char)
_String_cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
_String_nil = λ_P λ_cons λ_nil _nil
_Tree = λ_A 0
_Tree_fold = λ_bm λ_nd λ_lf
let _bm_P = 0
let _bm_node = λ_bm_val λ_bm_lft λ_bm_rgt λ_nd λ_lf (((_nd _bm_val) (((_Tree_fold _bm_lft) _nd) _lf)) (((_Tree_fold _bm_rgt) _nd) _lf))
let _bm_leaf = λ_nd λ_lf _lf
(((((_bm _bm_P) _bm_node) _bm_leaf) _nd) _lf)
_Tree_gen = λ_n λ_x match _n = _n {
0: _Tree_leaf
1+: let _n-1 = _n-1
(((_Tree_node _x) ((_Tree_gen _n-1) (+ (* _x 2) 1))) ((_Tree_gen _n-1) (+ (* _x 2) 2)))
}
_Tree_leaf = λ_P λ_node λ_leaf _leaf
_Tree_node = λ_val λ_lft λ_rgt λ_P λ_node λ_leaf (((_node _val) _lft) _rgt)
_Tree_sum = λ_x
let _x_P = 0
let _x_node = λ_x_val λ_x_lft λ_x_rgt (+ _x_val (+ _x_lft _x_rgt))
let _x_leaf = 0
(((_Tree_fold _x) _x_node) _x_leaf)
__main = (_Tree_sum ((_Tree_gen 22) 0))
main = __main

37
book/tmp/_main.hvmc
View File

@ -1,37 +0,0 @@
@_chr = #0
@_ls = (* #0)
@_ls_cn = (a (b (* ((a (b c)) (* c)))))
@_ls_nl = (* @_ls_nl_0)
@_ls_nl_0 = (* (a a))
@_N = #0
@_N_s = (a (* ((a b) (* b))))
@_N_z = (* @_N_z_0)
@_N_z_0 = (* (a a))
@_str = a
& @_ls ~ (@_chr a)
@_str_cn = (a (b (* ((a (b c)) (* c)))))
@_str_nl = (* @_str_nl_0)
@_str_nl_0 = (* (a a))
@_T = (* #0)
@_T_f = ((#0 (@_T_f_0 (@_T_f_1 (a (b c))))) (a (b c)))
@_T_f_0 = (a (b (c ({7 (a (d (e f))) {7 g h}} ({9 i j} f)))))
& @_T_f ~ (c (h (j e)))
& @_T_f ~ (b (g (i d)))
@_T_f_1 = (* (a a))
@_T_gn = (?<(@_T_gn_0 @_T_gn_1) (a b)> (a b))
@_T_gn_0 = (* @_T_lf)
@_T_gn_1 = ({5 a b} ({3 c {3 <* #2 <+ #1 d>> <* #2 <+ #2 e>>}} f))
& @_T_nd ~ (c (g (h f)))
& @_T_gn ~ (b (e h))
& @_T_gn ~ (a (d g))
@_T_lf = (* @_T_lf_0)
@_T_lf_0 = (* (a a))
@_T_nd = (a (b (c (* ((a (b (c d))) (* d))))))
@_T_sum = (a b)
& @_T_f ~ (a (@_T_sum_0 (#0 b)))
@_T_sum_0 = (<+ a b> (<+ c a> (c b)))
@__main = a
& @_T_sum ~ (b a)
& @_T_gn ~ (#22 (#0 b))
@main = @__main

36
book/tmp/_main.js
View File

@ -1,36 +0,0 @@
let _Char = 0;
let _List = (_T) => 0;
let _List_cons = (_head) => (_tail) => (_P) => (_cons) => (_nil) => ((_cons(_head))(_tail));
let _List_nil = (_P) => (_cons) => (_nil) => _nil;
let _Nat = 0;
let _Nat_succ = (_n) => (_P) => (_succ) => (_zero) => (_succ(_n));
let _Nat_zero = (_P) => (_succ) => (_zero) => _zero;
let _String = (_List(_Char));
let _String_cons = (_head) => (_tail) => (_P) => (_cons) => (_nil) => ((_cons(_head))(_tail));
let _String_nil = (_P) => (_cons) => (_nil) => _nil;
let _Tree = (_A) => 0;
let _Tree_fold = (_bm) => (_nd) => (_lf) => {
let _bm_P = 0;
let _bm_node = (_bm_val) => (_bm_lft) => (_bm_rgt) => (_nd) => (_lf) => (((_nd(_bm_val))(((_Tree_fold(_bm_lft))(_nd))(_lf)))(((_Tree_fold(_bm_rgt))(_nd))(_lf)));
let _bm_leaf = (_nd) => (_lf) => _lf;
return (((((_bm(_bm_P))(_bm_node))(_bm_leaf))(_nd))(_lf));
};
let _Tree_gen = (_n) => (_x) => {
if (_n === 0) {
return _Tree_leaf;
} else {
let _n_1 = _n - 1;
return (((_Tree_node(_x))((_Tree_gen(_n_1))(((_x * 2) + 1))))((_Tree_gen(_n_1))(((_x * 2) + 2))));
}
};
let _Tree_leaf = (_P) => (_node) => (_leaf) => _leaf;
let _Tree_node = (_val) => (_lft) => (_rgt) => (_P) => (_node) => (_leaf) => (((_node(_val))(_lft))(_rgt));
let _Tree_sum = (_x) => {
let _x_P = 0;
let _x_node = (_x_val) => (_x_lft) => (_x_rgt) => (_x_val + (_x_lft + _x_rgt));
let _x_leaf = 0;
return (((_Tree_fold(_x))(_x_node))(_x_leaf));
};
let __main = (_Tree_sum((_Tree_gen(22))(0)));
console.log(__main)

241
book/tmp/_main.kind2
View File

@ -1,241 +0,0 @@
//// Sums a binary tree in parallel, using fold
//// __(1)__
//// / \ __(1)__
//// (1) (2) => / \ => (14)
//// / \ / \ (4) (9)
//// (1) (2) (3) (4)
//use Tree/{node,leaf}
//data Tree A
//| node (val: A) (lft: (Tree A)) (rgt: (Tree A))
//| leaf
//sum (x: (Tree U60)) : U60 =
//fold x {
//node: (+ x.val (+ x.lft x.rgt))
//leaf: 0
//}
//gen (n: U60) (x: U60) : (Tree U60) =
//switch n {
//0: leaf
//_: (node x (gen n-1 (+ (* x 2) 1)) (gen n-1 (+ (* x 2) 2)))
//}
//main = (sum (gen 16 0))
use Tree/{node,leaf,gen,sum}
_main: U60 =
(sum (gen 16 0))
//use Nat.{succ,zero}
//_main: (List U60) =
//(List.map _ _ (List.cons _ 1 (List.cons _ 2 (List.cons _ 3 (List.nil _)))) λx(+ x 1))
//_main : (Maybe U60) =
//(Maybe.bind _ _ (Maybe.some _ 1) λx
//(Maybe.bind _ _ (Maybe.some _ 2) λy
//(Maybe.some _ (+ x y))))
//main : (Maybe U60) = {
//x = !bar
//y = 80
//for i in [1,2,!(foo y)]:
//for j in [10,20,30]:
//x += i
//if x > j:
//return x
//return x + y
//}
//fold xs:
//cons:
//xs.head + xs.tail
//nil:
//0
//for x in xs:
//_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
//switch a {
//succ: switch b {
//succ: e
//zero: e
//}
//zero: switch b {
//succ: e
//zero: ?D
//}
//}
//λa λb λe
//use a.P = _
//use a.succ = λa.pred λb λe ?A
//use a.zero = λb λe ?B
//({ (~a a.P a.succ a.zero)
//: ∀(b: Nat) ∀(e: (Equal A a b)) _}
//b e)
//({(~a
//_
//λa.pred λe2 ?A
//λe2 ?B
//): ∀(e2: (Equal A a b)) _} e)
//_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
//switch a {
//succ: switch b {
//succ: ?A
//zero: ?B
//}
//zero: switch b {
//succ: ?C
//zero: ?D
//}
//}
//λa (~a _
//λap λb (~b _
//λbp λe ?SS
//λe ?SZ
//)
//λb (~b _
//λbp λe ?ZS
//λe ?ZZ
//)
//)
//switch x {
//}
//_main
//: ∀(A0: *) ∀(X: *) ∀(R: *)
//use F = ∀(x: X) ∀(a0: A0) R
//use G = ∀(a0: A0) ∀(x: X) R
//∀(f: F) G
//= λA0 λX λR λf
//λa0 λx
//(f x a0)
//_main
//: ∀(A0: *) ∀(A1: *) ∀(X: *) ∀(R: *)
//use F = ∀(x: X) ∀(a0: A0) R
//use G = ∀(a0: A0) ∀(a1: A1) ∀(x: X) R
//∀(f: F) G
//= λA0 λA1 λX λR λf
//λa0 λa1 λx
//(f x a0 a1)
//_main : ∀(a: Nat) ∀(b: Nat) ∀(e: (Equal A a b)) (Equal A a b) =
//λa (~a _
//λap λb (~b _
//λbp λe ?A
//λe ?B)
//λb (~b _
//λbp λe ?C
//λe ?D)
//)
//_main : ∀(a: A) ∀(b: A) ∀(e: (Equal A a b)) (Equal A a b) =
//λa (~a _
//λat λb (~b _
//λbt λe ?SS
//λbt λe ?SZ
//)
//λat λb (~b _
//λbt λe ?ZS
//λbt λe ?ZZ
//)
//)
//_main : ∀(a: A) ∀(b: A) ∀(e: (Equal A a b)) (Equal A a b) =
//λa (~a _
//λat λb (at (~b
//λbt λap (bt λbp (REC ap bp))
//_
//))
//λat λb ?b
//)
//_main : ∀(a: (List Nat)) ∀(b: (List Nat)) ∀(e: (Equal (List Nat) a b)) (Equal (List Nat) a b) =
//λa
//(~a _
//λa.head λa.tail λb (~b _
//λb.head λb.tail λe ?A
//λe ?B)
//λb λe ?C
//)
//_main : ∀(a: (List Nat)) ∀(b: (List Nat)) ∀(e: (Equal (List Nat) a b)) (Equal (List Nat) a b) =
//λa
//(~a _
//λa.fields λb (a.fields (~b _
//λb.head λb.tail λa.head λa.tail λe ?A
//λe ?B))
//λb λe ?C
//)
//switch a {
//cons: switch b {
//cons: ... a.tail ...
//nil: ... a.tail ...
//}
//nil: switch b {
//cons:
//nil:
//}
//}
//_main
//: use list =
//(List.cons _ Nat.zero
//(List.cons _ 1
//(List.cons _ (Nat.succ (Nat.succ Nat.zero))
//(List.nil _))))
//(The (List Nat) list)
//= ?A
//C0
//All { nam: "len", inp: Var { nam: "Nat" }, bod:
//All { nam: "head", inp: Var { nam: "A" }, bod:
//All { nam: "tail", inp: App { fun: App { fun: Var { nam: "Vector" }, arg: Var { nam: "A" } }, arg: Var { nam: "len" } }, bod:
//App { fun: App { fun: Var { nam: "P" }, arg: App { fun: Var { nam: "Nat.succ" }, arg: Var { nam: "len" } } }, arg: App { fun: App { fun: App { fun: App { fun: Var { nam: "Vector.cons" }, arg: Var { nam: "A" } }, arg: Var { nam: "len" } }, arg: Var { nam: "head" } }, arg: Var { nam: "tail" } } } } } }
//ADT {
//name: "Vector",
//pars: ["A"],
//idxs: [("len", Var { nam: "Nat" })],
//ctrs: [
//Constructor {
//name: "cons",
//flds: [("len", Var { nam: "Nat" }), ("head", Var { nam: "A" }), ("tail", App { fun: App { fun: Var { nam: "Vector" }, arg: Var { nam: "A" } }, arg: Var { nam: "len" } })],
//idxs: [App { fun: Var { nam: "Nat.succ" }, arg: Var { nam: "len" } }, App { fun: App { fun: App { fun: App { fun: Var { nam: "Vector.cons" }, arg: Var { nam: "A" } }, arg: Var { nam: "len" } }, arg: Var { nam: "head" } }, arg: Var { nam: "tail" } }]
//},
//Constructor {
//name: "nil",
//flds: [],
//idxs: [
//Var { nam: "Nat.zero" },
//App { fun: Var { nam: "Vector.nil" }, arg: Var { nam: "A" } }
//]
//}
//]
//}

12
book/tmp/test0.kind2
View File

@ -1,12 +0,0 @@
test0
: ∀(A: *)
∀(B: *)
∀(aa: ∀(x: A) A)
∀(ab: ∀(x: A) B)
∀(ba: ∀(x: B) A)
∀(bb: ∀(x: B) B)
∀(a: A)
∀(b: B)
A
= λA λB λaa λab λba λbb λa λb
(ba (ab (aa (aa a))))

3
book/tmp/test1.kind2
View File

@ -1,3 +0,0 @@
test1
: ∀(x: U60) U60
= λx (+ 50 12)

13
book/tmp/test10.kind2
View File

@ -1,13 +0,0 @@
// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
T_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat)))
T_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))
T_C2 = _Nat
T_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
= use term = (Kind.app (Kind.app T_exp T_c2) T_c2)
(Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)

3
book/tmp/test11.kind2
View File

@ -1,3 +0,0 @@
test11
: String
= 0

13
book/tmp/test2.kind2
View File

@ -1,13 +0,0 @@
test2
: (List U60)
= use xs = (List.cons
U60
0
(List.cons U60 1 (List.cons U60 2 (List.nil U60)))
)
use ys = (List.cons
U60
3
(List.cons U60 4 (List.cons U60 5 (List.nil U60)))
)
(List.concat U60 xs ys)

4
book/tmp/test3.kind2
View File

@ -1,4 +0,0 @@
test3
: U60
= use a = {42:U60}
a

3
book/tmp/test4.kind2
View File

@ -1,3 +0,0 @@
test4
: String
= (~"abc" λx String λh λt t String/nil)

3
book/tmp/test5.kind2
View File

@ -1,3 +0,0 @@
test5
: ∀(x: Bool) (Equal Bool (Bool.not (Bool.not x)) x)
= λb (~b ?A ?T ?F)

3
book/tmp/test6.kind2
View File

@ -1,3 +0,0 @@
test6
: Nat
= (Nat.succ (Nat.succ (Nat.succ Nat.zero)))

8
book/tmp/test7.kind2
View File

@ -1,8 +0,0 @@
test7
: (IO Unit)
= (IO.run
Unit
(IO.print.do
(Kind.Book.to_hvm (Kind.Book.parse test7.book))
)
)

7
book/tmp/test8.kind2
View File

@ -1,7 +0,0 @@
test8
: ∀(b: Bool) (~b λx(*) U60 U60)
= λb (~b _h ?A ?B)
//test8
//: U60
//= (U60.test 0)

3
book/tmp/test9.kind2
View File

@ -1,3 +0,0 @@
test9
: String
= (String.unpar 40 41 "((foo))")

8
book/tmp/testBBT.kind2
View File

@ -1,8 +0,0 @@
testBBT
: String
= "
File commented for backward compatibility.
To run the tests, uncomment the code on:
testBBT.kind2
U60.Map
"

2
src/book/parse.rs
View File

@ -158,7 +158,7 @@ impl Term {
}
// NOTE: match-passthrough removed due to problems. For example:
// U60.if (x: U60) (P: *) (t: P) (f: P) : P = switch x { 0: t _: f }
// U48.if (x: U48) (P: *) (t: P) (f: P) : P = switch x { 0: t _: f }
// This wouldn't check, because 'P' is moved inside, becoming a different 'P'.
// I think automatic behaviors like this are dangerous and should be avoided.

163
src/kindc.hs
View File

@ -2,7 +2,7 @@
-- ==========
--
-- This is a Haskell implementation of Kind2's proof kernel. It is based on the
-- Calculus of Constructions, extended with Self-Types and U60 operations. This
-- Calculus of Constructions, extended with Self-Types and U48 operations. This
-- allows us to express arbitrary inductive types and proofs with a simple core.
import Control.Monad (forM_)
@ -52,16 +52,16 @@ data Term
-- Type : Type
| Set
-- U60 Type
| U60
-- U48 Type
| U48
-- U60 Value
-- U48 Value
| Num Int
-- U60 Binary Operation
-- U48 Binary Operation
| Op2 Oper Term Term
-- U60 Elimination
-- U48 Elimination
| Swi String Term Term (Term -> Term) (Term -> Term)
-- Inspection Hole
@ -185,7 +185,7 @@ bind term = go term [] where
go (Let nam val bod) ctx = Let nam (go val ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go (Use nam val bod) ctx = Use nam (go val ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go Set ctx = Set
go U60 ctx = U60
go U48 ctx = U48
go (Num val) ctx = Num val
go (Op2 opr fst snd) ctx = Op2 opr (go fst ctx) (go snd ctx)
go (Swi nam x z s p) ctx = Swi nam (go x ctx) (go z ctx) (\k -> go (s (Var (nam ++ "-1") 0)) ((nam ++ "-1", k) : ctx)) (\k -> go (p (Var nam 0)) ((nam, k) : ctx))
@ -292,7 +292,7 @@ normal book fill lv term dep = normalGo book fill lv (reduce book fill lv term)
normalGo book fill lv (Use nam val bod) dep = Use nam (normal book fill lv val dep) (\x -> normal book fill lv (bod (Var nam dep)) (dep + 1))
normalGo book fill lv (Hol nam ctx) dep = Hol nam ctx
normalGo book fill lv Set dep = Set
normalGo book fill lv U60 dep = U60
normalGo book fill lv U48 dep = U48
normalGo book fill lv (Num val) dep = Num val
normalGo book fill lv (Op2 opr fst snd) dep = Op2 opr (normal book fill lv fst dep) (normal book fill lv snd dep)
normalGo book fill lv (Swi nam x z s p) dep = Swi nam (normal book fill lv x dep) (normal book fill lv z dep) (\k -> normal book fill lv (s (Var (nam ++ "-1") dep)) dep) (\k -> normal book fill lv (p (Var nam dep)) dep)
@ -315,7 +315,7 @@ normal book fill lv term dep = normalGo book fill lv (reduce book fill lv term)
equal :: Term -> Term -> Int -> Env Bool
equal a b dep = do
-- trace ("= " ++ termStr a dep ++ "\n? " ++ termStr b dep) $ do
-- trace ("== " ++ termStr a dep ++ "\n.. " ++ termStr b dep) $ do
book <- envGetBook
fill <- envGetFill
let a' = reduce book fill 2 a
@ -335,7 +335,10 @@ tryIdentical a b dep = do
else envRewind state >> envPure False
similar :: Term -> Term -> Int -> Env Bool
similar a b dep = go a b dep where
similar a b dep =
-- trace ("~~ " ++ termStr a dep ++ "\n.. " ++ termStr b dep) $ do
go a b dep
where
go (All aNam aInp aBod) (All bNam bInp bBod) dep = do
eInp <- equal aInp bInp dep
eBod <- equal (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
@ -401,7 +404,7 @@ identical a b dep = go a b dep where
return True
go a (Hol bNam bCtx) dep =
return True
go U60 U60 dep =
go U48 U48 dep =
return True
go (Num aVal) (Num bVal) dep =
return (aVal == bVal)
@ -455,17 +458,19 @@ unify uid spn b dep = do
let unsolved = not (IM.member uid fill) -- is this hole not already solved?
let solvable = unifyValid fill spn [] -- does the spine satisfies conditions?
let no_loops = not $ unifyIsRec book fill uid b dep -- is the solution not recursive?
-- If all is ok, generate the solution and return true
if unsolved && solvable && no_loops then do
let solution = unifySolve book fill uid spn b
envFill uid solution
return True
-- Otherwise, return true iff both are identical metavars
else case b of
(Met bUid bSpn) -> return $ uid == bUid
other -> return False
-- trace ("unify: " ++ show uid ++ " " ++ termStr b dep ++ " | " ++ show unsolved ++ " " ++ show solvable ++ " " ++ show no_loops) $ do
do
-- If all is ok, generate the solution and return true
if unsolved && solvable && no_loops then do
let solution = unifySolve book fill uid spn b
envFill uid solution
return True
-- Otherwise, return true iff both are identical metavars
else case b of
(Met bUid bSpn) -> return $ uid == bUid
other -> return False
-- Checks if an problem is solveable by pattern unification.
-- Checks if a problem is solveable by pattern unification.
unifyValid :: Fill -> [Term] -> [Int] -> Bool
unifyValid fill [] vars = True
unifyValid fill (x : spn) vars = case reduce M.empty fill 0 x of
@ -512,7 +517,7 @@ unifySubst lvl neo (Use nam val bod) = Use nam (unifySubst lvl neo val) (\x -> u
unifySubst lvl neo (Met uid spn) = Met uid (map (unifySubst lvl neo) spn)
unifySubst lvl neo (Hol nam ctx) = Hol nam (map (unifySubst lvl neo) ctx)
unifySubst lvl neo Set = Set
unifySubst lvl neo U60 = U60
unifySubst lvl neo U48 = U48
unifySubst lvl neo (Num n) = Num n
unifySubst lvl neo (Op2 opr fst snd) = Op2 opr (unifySubst lvl neo fst) (unifySubst lvl neo snd)
unifySubst lvl neo (Swi nam x z s p) = Swi nam (unifySubst lvl neo x) (unifySubst lvl neo z) (\k -> unifySubst lvl neo (s k)) (\k -> unifySubst lvl neo (p k))
@ -612,16 +617,16 @@ inferGo Set dep = do
return Set
-- ...
-- --------- U60-type
-- U60 : Set
inferGo U60 dep = do
-- --------- U48-type
-- U48 : Set
inferGo U48 dep = do
return Set
-- ...
-- ----------- U60-value
-- <num> : U60
-- ----------- U48-value
-- <num> : U48
inferGo (Num num) dep = do
return U60
return U48
-- ...
-- -------------- String-literal
@ -635,26 +640,26 @@ inferGo (Txt txt) dep = do
inferGo (Nat val) dep = do
return (Ref "Nat")
-- fst : U60
-- snd : U60
-- ----------------- U60-operator
-- (+ fst snd) : U60
-- fst : U48
-- snd : U48
-- ----------------- U48-operator
-- (+ fst snd) : U48
inferGo (Op2 opr fst snd) dep = do
envSusp (Check 0 fst U60 dep)
envSusp (Check 0 snd U60 dep)
return U60
envSusp (Check 0 fst U48 dep)
envSusp (Check 0 snd U48 dep)
return U48
-- x : U60
-- p : U60 -> Set
-- x : U48
-- p : U48 -> Set
-- z : (p 0)
-- s : (n: U60) -> (p (+ 1 n))
-- ------------------------------------- U60-elim
-- s : (n: U48) -> (p (+ 1 n))
-- ------------------------------------- U48-elim
-- (switch x { 0: z ; _: s }: p) : (p x)
inferGo (Swi nam x z s p) dep = do
envSusp (Check 0 x U60 dep)
envSusp (Check 0 (p (Ann False (Var nam dep) U60)) Set dep)
envSusp (Check 0 x U48 dep)
envSusp (Check 0 (p (Ann False (Var nam dep) U48)) Set dep)
envSusp (Check 0 z (p (Num 0)) dep)
envSusp (Check 0 (s (Ann False (Var (nam ++ "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (nam ++ "-1") dep))) (dep + 1))
envSusp (Check 0 (s (Ann False (Var (nam ++ "-1") dep) U48)) (p (Op2 ADD (Num 1) (Var (nam ++ "-1") dep))) (dep + 1))
return (p x)
-- val : typ
@ -847,7 +852,7 @@ termStr (Use nam val bod) dep =
bod' = termStr (bod (Var nam dep)) (dep + 1)
in concat ["use " , nam' , " = " , val' , "; " , bod']
termStr Set dep = "*"
termStr U60 dep = "U60"
termStr U48 dep = "U48"
termStr (Num val) dep =
let val' = show val
in concat [val']
@ -928,51 +933,48 @@ doParseTerm input = case P.parse parseTerm "" input of
Right term -> bind term
parseTerm :: P.Parsec String () Term
parseTerm = P.choice
[ parseAll
, parseLam
, parseOp2
, parseApp
, parseAnn
, parseSlf
, parseIns
, parseUse
, parseLet
, parseSet
, parseNum
, parseSwi
, parseTxt
, parseNat
, parseHol
, parseMet
, parseSrc
, parseRef
]
parseTerm = do
P.spaces
P.choice
[ parseAll
, parseLam
, parseOp2
, parseApp
, parseAnn
, parseSlf
, parseIns
, parseUse
, parseLet
, parseSet
, parseNum
, parseSwi
, parseTxt
, parseNat
, parseHol
, parseMet
, parseSrc
, parseRef
]
parseAll = do
P.string "∀"
P.spaces
P.char '('
nam <- parseName
P.char ':'
P.spaces
inp <- parseTerm
P.char ')'
P.spaces
bod <- parseTerm
return $ All nam inp (\x -> bod)
parseLam = do
P.string "λ"
nam <- parseName
P.spaces
bod <- parseTerm
return $ Lam nam (\x -> bod)
parseApp = do
P.char '('
fun <- parseTerm
P.spaces
arg <- parseTerm
P.char ')'
return $ App fun arg
@ -980,10 +982,11 @@ parseApp = do
parseAnn = do
P.char '{'
val <- parseTerm
P.spaces
P.char ':'
chk <- P.option False (P.char ':' >> return True)
P.spaces
typ <- parseTerm
P.spaces
P.char '}'
return $ Ann chk val typ
@ -991,10 +994,8 @@ parseSlf = do
P.string "$("
nam <- parseName
P.char ':'
P.spaces
typ <- parseTerm
P.char ')'
P.spaces
bod <- parseTerm
return $ Slf nam typ (\x -> bod)
@ -1006,32 +1007,26 @@ parseIns = do
parseRef = do
name <- parseName
return $ case name of
"U60" -> U60
"U48" -> U48
_ -> Ref name
parseUse = do
P.try (P.string "use ")
P.spaces
nam <- parseName
P.spaces
P.char '='
P.spaces
val <- parseTerm
P.char ';'
P.spaces
bod <- parseTerm
return $ Use nam val (\x -> bod)
parseLet = do
P.try (P.string "let ")
P.spaces
nam <- parseName
P.spaces
P.char '='
P.spaces
val <- parseTerm
P.char ';'
P.spaces
bod <- parseTerm
return $ Let nam val (\x -> bod)
@ -1044,35 +1039,28 @@ parseOp2 = do
P.string "("
opr <- parseOper
return opr
P.spaces
fst <- parseTerm
P.spaces
snd <- parseTerm
P.char ')'
return $ Op2 opr fst snd
parseSwi = do
P.try (P.string "switch ")
P.spaces
nam <- parseName
P.spaces
P.char '='
P.spaces
x <- parseTerm
P.spaces
P.char '{'
P.spaces
P.string "0:"
P.spaces
z <- parseTerm
P.spaces
P.string "_:"
P.spaces
s <- parseTerm
P.spaces
P.char '}'
P.char ':'
P.spaces
p <- parseTerm
return $ Swi nam x z (\k -> s) (\k -> p)
@ -1105,12 +1093,12 @@ parseMet = do
parseSrc = do
P.char '!'
src <- read <$> P.many1 P.digit
P.spaces
val <- parseTerm
return $ Src src val
parseName :: P.Parsec String () String
parseName = do
P.spaces
head <- P.letter
tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_' <|> P.char '-')
return (head : tail)
@ -1141,17 +1129,14 @@ parseBook = do
parseDef :: P.Parsec String () (String, Term)
parseDef = do
P.spaces
name <- parseName
P.spaces
(typ, hasType) <- P.option (undefined, False) $ do
P.char ':'
P.spaces
typ <- parseTerm
P.spaces
return (typ, True)
P.char '='
P.spaces
value <- parseTerm
P.char ';'
P.spaces

2
src/main.rs
View File

@ -43,7 +43,7 @@ fn check(name: &str) {
println!("{}", info.pretty(&book));
}
if stderr.is_empty() && infos.is_empty() {
println!("check!");
println!("Checked.");
}
eprintln!("{stderr}");
}

54
src/sugar/mod.rs
View File

@ -36,7 +36,7 @@ pub struct Match {
pub adt: String, // datatype
pub fold: bool, // is this a fold?
pub name: String, // scrutinee name
pub expr: Term, // structinee expression
pub expr: Option<Term>, // structinee expression
pub with: Vec<(String,Term)>, // terms to move in
pub cses: Vec<(String,Term)>, // matched cases
pub moti: Option<Term>, // motive
@ -174,14 +174,14 @@ pub struct Match {
// For a full example, the expression:
//
// match x = (f arg) with (a: A) (b: B) {
// Vector.cons: (U60.add x.head (sum x.tail))
// Vector.cons: (U48.add x.head (sum x.tail))
// Vector.nil: #0
// }: #U60
// }: #U48
//
// Is converted to:
//
// use x.P = λx.len λx ∀(a: A) ∀(b: B) #U60
// use x.cons = λx.head λx.tail λa λb ((U60.add x.head) (sum x.tail))
// use x.P = λx.len λx ∀(a: A) ∀(b: B) #U48
// use x.cons = λx.head λx.tail λa λb ((U48.add x.head) (sum x.tail))
// use x.nil = λx.len λa λb #0
// (({(((~(f arg) x.P) x.cons) x.nil): ∀(a: A) ∀(b: B) _} a) b)
@ -961,7 +961,7 @@ impl Term {
term = Term::App {
era: false,
fun: Box::new(term),
arg: Box::new(mat.expr.clone()),
arg: Box::new(Term::Var { nam: mat.name.clone() }),
};
// 6. Annotates with the moved var foralls
@ -1007,6 +1007,15 @@ impl Term {
bod: Box::new(term)
};
// 10. Create the local 'let' for the expr
if let Some(expr) = &mat.expr {
term = Term::Let {
nam: mat.name.clone(),
val: Box::new(expr.clone()),
bod: Box::new(term),
};
}
// Debug: Prints the generated term
//println!("{}", term.format().flatten(Some(800)));
@ -1023,8 +1032,30 @@ impl Match {
Show::glue(" ", vec![
Show::text(if self.fold { "fold" } else { "match" }),
Show::text(&self.name),
Show::text("="),
self.expr.format_go(),
if let Some(expr) = &self.expr {
Show::glue(" ", vec![
Show::text("="),
expr.format_go(),
])
} else {
Show::text("")
},
if !self.with.is_empty() {
Show::glue(" ", vec![
Show::text("with"),
Show::pile(" ", self.with.iter().map(|(name, typ)| {
Show::call("", vec![
Show::text("("),
Show::text(name),
Show::text(":"),
typ.format_go(),
Show::text(")"),
])
}).collect()),
])
} else {
Show::text("")
},
]),
Show::glue(" ", vec![
Show::text("{"),
@ -1059,9 +1090,9 @@ impl<'i> KindParser<'i> {
self.skip_trivia();
let expr = if self.peek_one() == Some('=') {
self.consume("=")?;
self.parse_term(fid, uses)?
Some(self.parse_term(fid, uses)?)
} else {
Term::Var { nam: name.clone() }
None
};
// Parses the with clause: 'with (a: A) (b: B) ...'
let mut with = Vec::new();
@ -1136,6 +1167,9 @@ impl<'i> KindParser<'i> {
} else {
None
};
return Ok(Match { adt, fold, name, expr, with, cses, moti });
}

4
src/term/compile.rs
View File

@ -80,7 +80,7 @@ impl Term {
Term::Set => {
format!("0")
},
Term::U60 => {
Term::U48 => {
format!("0")
},
Term::Num { val } => {
@ -161,7 +161,7 @@ impl Term {
format!("~{}", val.to_kindc(env.clone(), met))
},
Term::Set => "*".to_string(),
Term::U60 => "U60".to_string(),
Term::U48 => "U48".to_string(),
Term::Num { val } => val.to_string(),
Term::Op2 { opr, fst, snd } => {
format!("({} {} {})", opr.to_kindc(), fst.to_kindc(env.clone(), met), snd.to_kindc(env.clone(), met))

18
src/term/mod.rs
View File

@ -33,7 +33,7 @@ pub struct Src {
// SLF | $(<name>: <term>) <term>
// INS | ~<term>
// SET | *
// U60 | U60
// U48 | U48
// NUM | <uint>
// OP2 | (<oper> <term> <term>)
// SWI | switch <name> = <term> { 0: <term>; +: <term> }: <term>
@ -52,7 +52,7 @@ pub enum Term {
Slf { nam: String, typ: Box<Term>, bod: Box<Term> },
Ins { val: Box<Term> },
Set,
U60,
U48,
Num { val: u64 },
Op2 { opr: Oper, fst: Box<Term>, snd: Box<Term> },
Swi { nam: String, x: Box<Term>, z: Box<Term>, s: Box<Term>, p: Box<Term> },
@ -62,11 +62,11 @@ pub enum Term {
Hol { nam: String },
Met {},
Src { src: Src, val: Box<Term> },
// Syntax Sugars that are NOT compiled
Mch { mch: Box<Match> },
// Syntax Sugars that are compiled
Nat { nat: u64 },
Txt { txt: String },
// Syntax Sugars that are NOT compiled
Mch { mch: Box<Match> },
}
impl Src {
@ -130,7 +130,7 @@ impl Term {
val.get_free_vars(env.clone(), free_vars);
},
Term::Set => {},
Term::U60 => {},
Term::U48 => {},
Term::Num { val: _ } => {},
Term::Op2 { opr: _, fst, snd } => {
fst.get_free_vars(env.clone(), free_vars);
@ -215,8 +215,8 @@ impl Term {
Term::Set => {
Term::Set
},
Term::U60 => {
Term::U60
Term::U48 => {
Term::U48
},
Term::Num { val } => {
Term::Num { val: *val }
@ -328,7 +328,7 @@ impl Term {
val.desugar();
},
Term::Set => {},
Term::U60 => {},
Term::U48 => {},
Term::Num { .. } => {},
Term::Nat { .. } => {},
Term::Txt { .. } => {},
@ -364,7 +364,7 @@ impl Term {
val.expand_implicits(env.clone(), implicit_count);
},
Term::Set => {},
Term::U60 => {},
Term::U48 => {},
Term::Num { val: _ } => {},
Term::Op2 { opr: _, fst, snd } => {
fst.expand_implicits(env.clone(), implicit_count);

4
src/term/parse.rs
View File

@ -452,8 +452,8 @@ impl<'i> KindParser<'i> {
let nam = uses.get(&old).unwrap_or(&old).to_string();
let end = *self.index() as u64;
let src = Src::new(fid, ini, end);
let val = if nam == "U60" {
Box::new(Term::U60)
let val = if nam == "U48" {
Box::new(Term::U48)
} else {
Box::new(Term::Var { nam })
};

84
src/term/show.rs
View File

@ -1,3 +1,5 @@
//./../sugar/mod.rs//
use crate::{*};
impl Oper {
@ -142,8 +144,8 @@ impl Term {
Term::Set => {
Show::text("*")
},
Term::U60 => {
Show::text("U60")
Term::U48 => {
Show::text("U48")
},
Term::Num { val } => {
Show::text(&format!("{}", val))
@ -229,33 +231,57 @@ impl Term {
Term::Nat { nat } => {
Show::text(&format!("{}", nat))
},
Term::Mch { mch } => {
Show::call(" ", vec![
Show::glue(" ", vec![
Show::text("match"),
Show::text(&mch.name),
Show::text("= "),
mch.expr.format_go(),
Show::text("{"),
]),
Show::pile("; ", mch.cses.iter().map(|(nam, bod)| {
Show::glue("", vec![
Show::text(nam),
Show::text(": "),
bod.format_go(),
])
}).collect()),
Show::glue("", vec![
Show::text("}"),
]),
mch.moti.as_ref().map_or(
Show::text(""),
|bod| Show::glue("", vec![
Show::text(": "),
bod.format_go(),
])
),
])
Term::Mch { mch: _ } => {
// FIXME: isn't this unreachable?
unreachable!()
//Show::call(" ", vec![
//Show::glue(" ", vec![
//Show::text("match"),
//Show::text(&mch.name),
//if let Some(expr) = &mch.expr {
//Show::glue(" ", vec![
//Show::text("="),
//expr.format_go(),
//])
//} else {
//Show::text("")
//},
//if !mch.with.is_empty() {
//Show::glue(" ", vec![
//Show::text("with"),
//Show::pile(" ", mch.with.iter().map(|(name, typ)| {
//Show::call("", vec![
//Show::text("("),
//Show::text(name),
//Show::text(":"),
//typ.format_go(),
//Show::text(")"),
//])
//}).collect()),
//])
//} else {
//Show::text("")
//},
//Show::text("{"),
//]),
//Show::pile("; ", mch.cses.iter().map(|(nam, bod)| {
//Show::glue("", vec![
//Show::text(nam),
//Show::text(": "),
//bod.format_go(),
//])
//}).collect()),
//Show::glue("", vec![
//Show::text("}"),
//]),
//mch.moti.as_ref().map_or(
//Show::text(""),
//|bod| Show::glue("", vec![
//Show::text(": "),
//bod.format_go(),
//])
//),
//])
},
}
}