mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Merge branch 'master' of https://github.com/uwu-tech/Kind
This commit is contained in:
commit
cca573698c
65
base/Bits/hex_tail.kind
Normal file
65
base/Bits/hex_tail.kind
Normal file
@ -0,0 +1,65 @@
|
||||
Bits.hex_tail.encode(x: Bits): String
|
||||
String.reverse(Bits.hex_tail.encode.go(x, ""))
|
||||
|
||||
Bits.hex_tail.encode.go(x: Bits, str: String): String
|
||||
case x {
|
||||
e: str
|
||||
o: case x.pred as x {
|
||||
e: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
o: case x.pred as x {
|
||||
e: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
o: case x.pred as x {
|
||||
e: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
o: Bits.hex_tail.encode.go(x.pred, "0" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "8" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "4" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "4" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "c" | str)
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "2" | str
|
||||
o: case x.pred as x {
|
||||
e: "2" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "2" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "a" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "6" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "6" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "e" | str)
|
||||
}
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "1" | str
|
||||
o: case x.pred as x {
|
||||
e: "1" | str
|
||||
o: case x.pred as x {
|
||||
e: "1" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "1" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "9" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "5" |str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "5" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "d" | str)
|
||||
}
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "3" | str
|
||||
o: case x.pred as x {
|
||||
e: "3" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "3" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "b" | str)
|
||||
}
|
||||
i: case x.pred as x {
|
||||
e: "7" | str
|
||||
o: Bits.hex_tail.encode.go(x.pred, "7" | str)
|
||||
i: Bits.hex_tail.encode.go(x.pred, "f" | str)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
5
base/Either3.kind
Normal file
5
base/Either3.kind
Normal file
@ -0,0 +1,5 @@
|
||||
type Either3 <A: Type, B: Type, C: Type> {
|
||||
fst(value: A)
|
||||
snd(value: B)
|
||||
trd(value: C)
|
||||
}
|
155
base/Nat/AddExp.kind
Normal file
155
base/Nat/AddExp.kind
Normal file
@ -0,0 +1,155 @@
|
||||
type Nat.AddExp {
|
||||
const(value: Nat)
|
||||
var(idx: Nat)
|
||||
add(left: Nat.AddExp, right: Nat.AddExp)
|
||||
}
|
||||
|
||||
Nat.AddExp.from_nat: Nat -> Nat.AddExp
|
||||
Nat.AddExp.const
|
||||
|
||||
Nat.AddExp.dimension(
|
||||
exp: Nat.AddExp
|
||||
): Nat
|
||||
case exp {
|
||||
const:
|
||||
0
|
||||
add:
|
||||
let left_dim = Nat.AddExp.dimension(exp.left)
|
||||
let right_dim = Nat.AddExp.dimension(exp.right)
|
||||
Nat.max(left_dim, right_dim)
|
||||
var:
|
||||
Nat.succ(exp.idx)
|
||||
}
|
||||
|
||||
Nat.AddExp.constant(exp: Nat.AddExp): Type
|
||||
case exp {
|
||||
const:
|
||||
Unit
|
||||
var:
|
||||
Empty
|
||||
add:
|
||||
And<Nat.AddExp.constant(exp.left), Nat.AddExp.constant(exp.right)>
|
||||
}
|
||||
|
||||
Nat.AddExp.dimension.zero(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)
|
||||
): Nat.AddExp.constant(exp)
|
||||
(case exp {
|
||||
const:
|
||||
(Hyp)
|
||||
unit
|
||||
var:
|
||||
(Hyp)
|
||||
let contra = Nat.succ_neq_zero!(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
add:
|
||||
(Hyp)
|
||||
let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
|
||||
let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp,
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
|
||||
left_small
|
||||
))
|
||||
let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
|
||||
max, 0, Hyp
|
||||
(x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
|
||||
right_small
|
||||
))
|
||||
let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
|
||||
let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
|
||||
Pair.new!!(left, right)
|
||||
}: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.AddExp.compute(
|
||||
exp: Nat.AddExp
|
||||
Hyp: Nat.AddExp.constant(exp)
|
||||
): Nat
|
||||
case exp with Hyp {
|
||||
const:
|
||||
exp.value
|
||||
var:
|
||||
Empty.absurd!(Hyp)
|
||||
add:
|
||||
open Hyp
|
||||
Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution(
|
||||
exp: Nat.AddExp
|
||||
): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
|
||||
def dim = Nat.AddExp.dimension(exp)
|
||||
def Hyp = Nat.Order.refl(dim)
|
||||
Nat.AddExp.substitution.aux0(dim, exp, Hyp)
|
||||
|
||||
Nat.AddExp.substitution.aux0(
|
||||
n: Nat
|
||||
exp: Nat.AddExp
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
|
||||
): Variadic(n, Nat, Nat)
|
||||
case n with Hyp {
|
||||
zero:
|
||||
def Hyp = Nat.Order.chain.aux!(Hyp)
|
||||
def Hyp = Nat.AddExp.dimension.zero!(Hyp)
|
||||
Nat.AddExp.compute(exp, Hyp)
|
||||
succ:
|
||||
(value)
|
||||
def new_exp = Nat.AddExp.substitution.aux1(exp, value, n.pred)
|
||||
let Hyp = Nat.AddExp.substitution.aux2(exp, value, n.pred, Hyp)
|
||||
Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
|
||||
}!
|
||||
|
||||
Nat.AddExp.substitution.aux1(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
): Nat.AddExp
|
||||
case exp {
|
||||
const:
|
||||
exp
|
||||
var:
|
||||
case Nat.lte(idx, exp.idx) {
|
||||
true:
|
||||
Nat.AddExp.const(value)
|
||||
false:
|
||||
exp
|
||||
}
|
||||
add:
|
||||
Nat.AddExp.add(
|
||||
Nat.AddExp.substitution.aux1(exp.left, value, idx)
|
||||
Nat.AddExp.substitution.aux1(exp.right, value, idx)
|
||||
)
|
||||
}
|
||||
|
||||
Nat.AddExp.substitution.aux2(
|
||||
exp: Nat.AddExp
|
||||
value: Nat
|
||||
idx: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), Nat.succ(idx)), true)
|
||||
): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
|
||||
Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), idx), true)
|
||||
case exp with Hyp {
|
||||
const:
|
||||
Equal.refl<Bool>(true)
|
||||
var:
|
||||
def cmp = Nat.lte(idx, exp.idx)
|
||||
let cmp_eq = refl :: cmp == cmp
|
||||
case cmp with cmp_eq: ^cmp == cmp {
|
||||
true:
|
||||
Equal.refl<Bool>(true)
|
||||
false:
|
||||
Nat.lte.comm.false(idx, exp.idx, cmp_eq)
|
||||
}! :: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(cmp(() Nat.AddExp, Nat.AddExp.const(value), Nat.AddExp.var(exp.idx))), idx), true)
|
||||
add:
|
||||
let {left_bound, right_bound} = Nat.max.split.left(
|
||||
Nat.AddExp.dimension(exp.left),
|
||||
Nat.AddExp.dimension(exp.right),
|
||||
Nat.succ(idx), Hyp
|
||||
)
|
||||
let ind_left = Nat.AddExp.substitution.aux2(exp.left, value, idx, left_bound)
|
||||
let ind_right = Nat.AddExp.substitution.aux2(exp.right, value, idx, right_bound)
|
||||
Nat.max.combine.left!!!(ind_left, ind_right)
|
||||
}!
|
@ -243,18 +243,41 @@ Nat.Order.mul.right(
|
||||
)
|
||||
qed
|
||||
|
||||
Nat.Order.mul.combine(
|
||||
a: Nat,
|
||||
b: Nat,
|
||||
c: Nat,
|
||||
d: Nat,
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), Bool.true),
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true)
|
||||
): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, d)), Bool.true)
|
||||
let left_lem = Nat.Order.mul.right(a, b, c, Hyp0)
|
||||
let right_lem = Nat.Order.mul.left(c, d, b, Hyp1)
|
||||
let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem)
|
||||
qed
|
||||
//Nat.Order.max.big(
|
||||
// a: Nat
|
||||
// b: Nat
|
||||
//): And<Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true), Equal<Bool>(Nat.lte(b, Nat.max(a, b)), true)>
|
||||
// case a {
|
||||
// zero:
|
||||
// Pair.new!!(Equal.refl<Bool>(true), Nat.Order.refl(b))
|
||||
// succ:
|
||||
// let ind = Nat.Order.max(a.pred, b)
|
||||
// ?succ
|
||||
// }!
|
||||
|
||||
Nat.Order.trichotomy(
|
||||
a: Nat
|
||||
b: Nat
|
||||
): Either3<
|
||||
Equal<Bool>(Nat.lte(a, b), false)
|
||||
Equal<Nat>(a, b)
|
||||
Equal<Bool>(Nat.lte(b, a), false)
|
||||
>
|
||||
def cmp_ab = Nat.lte(a, b)
|
||||
def cmp_ba = Nat.lte(b, a)
|
||||
let lemma_ab = Equal.refl<Bool>(cmp_ab)
|
||||
let lemma_ba = Equal.refl<Bool>(cmp_ba)
|
||||
case cmp_ab with lemma_ab: cmp_ab^ == cmp_ab {
|
||||
false:
|
||||
Either3.fst!!!(Equal.refl<Bool>(false))
|
||||
true:
|
||||
case cmp_ba with lemma_ba: cmp_ba^ == cmp_ba {
|
||||
false:
|
||||
Either3.trd!!!(Equal.refl<Bool>(false))
|
||||
true:
|
||||
Either3.snd!!!(Nat.Order.anti_symm!!(lemma_ab, lemma_ba))
|
||||
}!
|
||||
}!
|
||||
|
||||
//Nat.Order.bernoulli(
|
||||
// a: Nat,
|
||||
|
@ -4,9 +4,9 @@ Nat.Order.mul.combine(
|
||||
c: Nat,
|
||||
d: Nat,
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), Bool.true),
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true),
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true)
|
||||
): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, d)), Bool.true)
|
||||
let left_lem = Nat.Order.mul.right(a, b, c, Hyp0);
|
||||
let right_lem = Nat.Order.mul.left(c, d, b, Hyp1);
|
||||
let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem);
|
||||
let left_lem = Nat.Order.mul.right(a, b, c, Hyp0)
|
||||
let right_lem = Nat.Order.mul.left(c, d, b, Hyp1)
|
||||
let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem)
|
||||
qed
|
||||
|
@ -1,8 +1,10 @@
|
||||
Nat.lte(n: Nat, m: Nat): Bool
|
||||
case n {
|
||||
zero: Bool.true,
|
||||
succ: case m {
|
||||
zero: Bool.false,
|
||||
succ: Nat.lte(n.pred, m.pred),
|
||||
}
|
||||
}
|
||||
zero:
|
||||
true,
|
||||
succ:
|
||||
case m {
|
||||
zero: false,
|
||||
succ: Nat.lte(n.pred, m.pred),
|
||||
}
|
||||
}
|
||||
|
44
base/Nat/lte/comm.kind
Normal file
44
base/Nat/lte/comm.kind
Normal file
@ -0,0 +1,44 @@
|
||||
Nat.lte.comm.false(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), false)
|
||||
): Equal<Bool>(Nat.lte(Nat.succ(b), a), true)
|
||||
(case a {
|
||||
zero:
|
||||
(Hyp)
|
||||
let contra = Bool.true_neq_false(Hyp)
|
||||
Empty.absurd<Equal<Bool>(Nat.lte(Nat.succ(b), 0), true)>(contra)
|
||||
succ:
|
||||
(Hyp)
|
||||
(case b {
|
||||
zero:
|
||||
(Hyp)
|
||||
Equal.refl<Bool>(true)
|
||||
succ:
|
||||
(Hyp)
|
||||
let qed = Nat.lte.comm.false(a.pred, b.pred, Hyp)
|
||||
qed
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), Nat.succ(a.pred)), true))(
|
||||
Hyp
|
||||
)
|
||||
}: (Hyp: Equal<Bool>(Nat.lte(a, b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), a), true))(
|
||||
Hyp
|
||||
)
|
||||
|
||||
Nat.lte.comm.true(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.succ(a), b), true)
|
||||
): Equal<Bool>(Nat.lte(b, a), false)
|
||||
case b with Hyp {
|
||||
zero:
|
||||
let contra = Bool.false_neq_true(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
case a with Hyp {
|
||||
zero:
|
||||
Equal.refl<Bool>(false)
|
||||
succ:
|
||||
Nat.lte.comm.true(a.pred, b.pred, Hyp)
|
||||
}!
|
||||
}!
|
17
base/Nat/lte/succ_left.kind
Normal file
17
base/Nat/lte/succ_left.kind
Normal file
@ -0,0 +1,17 @@
|
||||
Nat.lte.succ_left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.succ(a), b), true)
|
||||
): Equal<Bool>(Nat.lte(a, b), true)
|
||||
case b with Hyp {
|
||||
zero:
|
||||
let contra = Bool.false_neq_true(Hyp)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
case a with Hyp {
|
||||
zero:
|
||||
refl
|
||||
succ:
|
||||
Nat.lte.succ_left(a.pred, b.pred, Hyp)
|
||||
}!
|
||||
}!
|
@ -1,5 +1,7 @@
|
||||
Nat.max(a:Nat, b:Nat): Nat
|
||||
case Nat.gtn(a, b) {
|
||||
true:a
|
||||
false:b
|
||||
}
|
||||
Nat.max(a: Nat, b: Nat): Nat
|
||||
case Nat.lte(a, b) {
|
||||
true:
|
||||
b
|
||||
false:
|
||||
a
|
||||
}
|
||||
|
26
base/Nat/max/big.kind
Normal file
26
base/Nat/max/big.kind
Normal file
@ -0,0 +1,26 @@
|
||||
Nat.max.big(
|
||||
a: Nat
|
||||
b: Nat
|
||||
): And<Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true), Equal<Bool>(Nat.lte(b, Nat.max(a,b)), true)>
|
||||
def cmp_ab = Nat.lte(a, b)
|
||||
let lemma_ab = Equal.refl!(cmp_ab)
|
||||
(case cmp_ab {
|
||||
true:
|
||||
(lemma_ab)
|
||||
Pair.new!!(lemma_ab, Nat.Order.refl(b))
|
||||
false:
|
||||
(lemma_ab)
|
||||
let lemma_ba = Nat.lte.comm.false!!(lemma_ab)
|
||||
let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
|
||||
Pair.new!!(Nat.Order.refl(a), lemma_ba)
|
||||
}: (lemma_ab: Equal<Bool>(Nat.lte(a, b), cmp_ab)) -> And<
|
||||
Equal<Bool>(Nat.lte(a, case cmp_ab { true: b, false: a }), true),
|
||||
Equal<Bool>(Nat.lte(b, case cmp_ab { true: b, false: a }), true)>)(
|
||||
lemma_ab
|
||||
)
|
||||
|
||||
Nat.max.big.left(a: Nat, b: Nat): Equal<Bool>(Nat.lte(a, Nat.max(a, b)), true)
|
||||
Pair.fst!!(Nat.max.big(a, b))
|
||||
|
||||
Nat.max.big.right(a: Nat, b: Nat): Equal<Bool>(Nat.lte(b, Nat.max(a,b)), true)
|
||||
Pair.snd!!(Nat.max.big(a, b))
|
22
base/Nat/max/combine.kind
Normal file
22
base/Nat/max/combine.kind
Normal file
@ -0,0 +1,22 @@
|
||||
Nat.max.combine.right(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(a, b), true)
|
||||
): Equal<Bool>(Nat.lte(a, Nat.max(b, c)), true)
|
||||
Nat.Order.chain!!!(Hyp, Nat.max.big.left(b, c))
|
||||
|
||||
Nat.max.combine.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp0: Equal<Bool>(Nat.lte(a, b), true)
|
||||
Hyp1: Equal<Bool>(Nat.lte(c, b), true)
|
||||
): Equal<Bool>(Nat.lte(Nat.max(a, c), b), true)
|
||||
def cmp_ac = Nat.lte(a, c)
|
||||
case cmp_ac {
|
||||
true:
|
||||
Hyp1
|
||||
false:
|
||||
Hyp0
|
||||
}! :: Equal<Bool>(Nat.lte(cmp_ac(() Nat, c, a), b), true)
|
45
base/Nat/max/comm.kind
Normal file
45
base/Nat/max/comm.kind
Normal file
@ -0,0 +1,45 @@
|
||||
Nat.max.comm(
|
||||
a: Nat
|
||||
b: Nat
|
||||
): Equal<Nat>(Nat.max(a, b), Nat.max(b, a))
|
||||
let lemma = Nat.Order.trichotomy(a, b)
|
||||
case lemma {
|
||||
fst:
|
||||
let lemma_ba = Nat.lte.comm.false!!(lemma.value)
|
||||
let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
|
||||
let qed = Equal.refl<Nat>(a)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
false, Nat.lte(a, b), mirror(lemma.value),
|
||||
(x) Equal<Nat>(x(() Nat, b, a), true(() Nat, a, b))
|
||||
qed
|
||||
)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
true, Nat.lte(b, a), mirror(lemma_ba),
|
||||
(x) Equal<Nat>(Nat.lte(a, b, () Nat, b, a), x(() Nat, a, b))
|
||||
qed
|
||||
)
|
||||
qed
|
||||
snd:
|
||||
let qed = Equal.refl<Nat>(Nat.max(a, a))
|
||||
let qed = Equal.rewrite<Nat>(
|
||||
a, b, lemma.value
|
||||
(x) Equal<Nat>(Nat.max(a, x), Nat.max(x, a))
|
||||
qed
|
||||
)
|
||||
qed
|
||||
trd:
|
||||
let lemma_ab = Nat.lte.comm.false!!(lemma.value)
|
||||
let lemma_ab = Nat.lte.succ_left!!(lemma_ab)
|
||||
let qed = Equal.refl<Nat>(b)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
false, Nat.lte(b, a), mirror(lemma.value),
|
||||
(x) Equal<Nat>(true(() Nat, b, a), x(() Nat, a, b))
|
||||
qed
|
||||
)
|
||||
let qed = Equal.rewrite<Bool>(
|
||||
true, Nat.lte(a, b), mirror(lemma_ab),
|
||||
(x) Equal<Nat>(x(() Nat, b, a), Nat.lte(b, a, () Nat, a, b))
|
||||
qed
|
||||
)
|
||||
qed
|
||||
}
|
8
base/Nat/max/split.kind
Normal file
8
base/Nat/max/split.kind
Normal file
@ -0,0 +1,8 @@
|
||||
Nat.max.split.left(
|
||||
a: Nat
|
||||
b: Nat
|
||||
c: Nat
|
||||
Hyp: Equal<Bool>(Nat.lte(Nat.max(a, b), c), true)
|
||||
): And<Equal<Bool>(Nat.lte(a, c), true), Equal<Bool>(Nat.lte(b, c), true)>
|
||||
let {left_lemma, right_lemma} = Nat.max.big(a, b)
|
||||
{Nat.Order.chain!!!(left_lemma, Hyp), Nat.Order.chain!!!(right_lemma, Hyp)}
|
@ -1,3 +1,16 @@
|
||||
Test: _
|
||||
let b = Litereum.serialize.varlen.go(12)
|
||||
Litereum.deserialize.varlen.go(b)
|
||||
Test<A: Type, B: Type>(
|
||||
f: A -> B,
|
||||
Hyp: (
|
||||
C: Type
|
||||
g: B -> C
|
||||
h: B -> C
|
||||
a: A
|
||||
HHyp: g(f(a)) == h(f(a))
|
||||
b: B
|
||||
) -> g(b) == h(b)
|
||||
target: B
|
||||
): [a: A] f(a) == target
|
||||
let g = ((b) true) :: B -> Bool
|
||||
let h = ((b) Decidable([a: A] f(a) == b)) :: B -> Bool
|
||||
let hmm = Hyp(Type, g, h)
|
||||
?test
|
||||
|
87
base/Tiger/SL.kind
Normal file
87
base/Tiger/SL.kind
Normal file
@ -0,0 +1,87 @@
|
||||
// straight-line programs Type and (very inefficient) interpreter
|
||||
// statement
|
||||
type Tiger.SL.Stm {
|
||||
CompoundStm(fst: Tiger.SL.Stm, snd: Tiger.SL.Stm)
|
||||
AssignStm(id: String, exp: Tiger.SL.Exp)
|
||||
PrintStm(exp_list: List<Tiger.SL.Exp>)
|
||||
}
|
||||
|
||||
// expression
|
||||
type Tiger.SL.Exp {
|
||||
IdExp(id: String)
|
||||
NumExp(num: Int) // #TODO include other numbers?
|
||||
OpExp(op: Tiger.SL.Binop, fst: Tiger.SL.Exp, snd: Tiger.SL.Exp)
|
||||
EseqExp(stm: Tiger.SL.Stm, exp: Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type Tiger.SL.ExpList {
|
||||
PairExpList(head: Tiger.SL.Exp, tail: Tiger.SL.ExpList)
|
||||
LastExpList(head: Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type Tiger.SL.Binop {
|
||||
plus
|
||||
minus
|
||||
times
|
||||
div
|
||||
}
|
||||
|
||||
maxargs(stm: Tiger.SL.Stm): Nat
|
||||
case stm {
|
||||
CompoundStm: Nat.max(maxargs(stm.fst), maxargs(stm.snd))
|
||||
AssignStm: 0
|
||||
PrintStm: List.length!(stm.exp_list)
|
||||
}
|
||||
|
||||
Tiger.SL.interpStm(stm: Tiger.SL.Stm, table: List<Pair<String, Int>>): List<Pair<String, Int>>
|
||||
case stm {
|
||||
CompoundStm:
|
||||
let new_table = Tiger.SL.interpStm(stm.fst, table)
|
||||
Tiger.SL.interpStm(stm.snd, new_table)
|
||||
AssignStm:
|
||||
let {i, new_table} = Tiger.SL.interpExp(stm.exp, table)
|
||||
{stm.id, i} & new_table
|
||||
PrintStm:
|
||||
for exp in stm.exp_list with table:
|
||||
let {i, table} = Tiger.SL.interpExp(exp, table)
|
||||
log(Int.show(i))
|
||||
table
|
||||
table
|
||||
}
|
||||
|
||||
Tiger.SL.lookup(id: String, table: List<Pair<String, Int>>): Int
|
||||
case table {
|
||||
nil:
|
||||
0 :: Int
|
||||
cons:
|
||||
let {table_id, val} = table.head
|
||||
if id =? table_id then
|
||||
val
|
||||
else
|
||||
Tiger.SL.lookup(id, table.tail)
|
||||
}
|
||||
|
||||
Tiger.SL.interpExp(exp: Tiger.SL.Exp, table: List<Pair<String, Int>>): Pair<Int, List<Pair<String, Int>>>
|
||||
case exp {
|
||||
IdExp:
|
||||
{Tiger.SL.lookup(exp.id, table), table}
|
||||
NumExp:
|
||||
{exp.num, table}
|
||||
OpExp:
|
||||
let {fst_val, table} = Tiger.SL.interpExp(exp.fst, table)
|
||||
let {snd_val, table} = Tiger.SL.interpExp(exp.snd, table)
|
||||
case exp.op {
|
||||
plus:
|
||||
{fst_val + snd_val, table}
|
||||
minus:
|
||||
{fst_val - snd_val, table}
|
||||
times:
|
||||
{fst_val * snd_val, table}
|
||||
div:
|
||||
{fst_val / snd_val, table}
|
||||
}
|
||||
EseqExp:
|
||||
let table = Tiger.SL.interpStm(exp.stm, table)
|
||||
Tiger.SL.interpExp(exp.exp, table)
|
||||
}
|
||||
|
@ -1,92 +0,0 @@
|
||||
// i'm studying compilers using "modern compiler implementation in ML" by Andrew Appel
|
||||
// translating to Kind as I go. i'm not too worried about following the book too closely.
|
||||
// for example i'll likely use kind's `Parser` to parse programs instead of Lex and Yacc.
|
||||
// but i'm using ML's naming conventions. it looks ugly but makes lookups easier.
|
||||
|
||||
// position on source code, to produce error messages
|
||||
User.rigille.Tiger.pos: Type
|
||||
Pair<Nat, Nat>
|
||||
|
||||
User.rigille.Tiger.symbol: Type
|
||||
String
|
||||
|
||||
type User.rigille.Tiger.var {
|
||||
SimpleVar(name: User.rigille.Tiger.symbol, pos: User.rigille.Tiger.pos)
|
||||
FieldVar(var: User.rigille.Tiger.var, name: User.rigille.Tiger.symbol, pos: User.rigille.Tiger.pos)
|
||||
SubscriptVar(var: User.rigille.Tiger.var, exp: User.rigille.Tiger.exp, pos: User.rigille.Tiger.pos)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.record_fields {
|
||||
new(
|
||||
name: User.rigille.Tiger.symbol
|
||||
args: List<User.rigille.Tiger.exp>
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
}
|
||||
type User.rigille.Tiger.exp {
|
||||
NilExp
|
||||
VarExp(var: User.rigille.Tiger.var)
|
||||
IntExp(val: Int)
|
||||
StringExp(val: String, pos: User.rigille.Tiger.pos)
|
||||
CallExp(
|
||||
func: User.rigille.Tiger.symbol
|
||||
args: List<User.rigille.Tiger.exp>
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
OpExp(
|
||||
left: User.rigille.Tiger.exp
|
||||
oper: User.rigille.Tiger.oper
|
||||
right: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
RecordExp(
|
||||
fields: List<User.rigille.Tiger.record_fields>
|
||||
typ: User.rigille.Tiger.symbol
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
SeqExp(
|
||||
val: List<User.rigille.Tiger.exp>
|
||||
)
|
||||
AssignExp(
|
||||
var: User.rigille.Tiger.var
|
||||
exp: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
IfExp(
|
||||
test: User.rigille.Tiger.exp
|
||||
then: User.rigille.Tiger.exp
|
||||
else: Maybe<User.rigille.Tiger.exp>
|
||||
)
|
||||
WhileExp(
|
||||
test: User.rigille.Tiger.exp
|
||||
body: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
ForExp(
|
||||
var: User.rigille.Tiger.symbol
|
||||
escape: Bool
|
||||
lo: User.rigille.Tiger.exp
|
||||
hi: User.rigille.Tiger.exp
|
||||
body: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
BreakExp(
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
LetExp(
|
||||
decs: List<User.rigille.Tiger.dec>
|
||||
body: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
ArrayExp(
|
||||
typ: User.rigille.Tiger.symbol
|
||||
size: User.rigille.Tiger.exp
|
||||
pos: User.rigille.Tiger.pos
|
||||
)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.oper {
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.dec {
|
||||
}
|
@ -1,87 +0,0 @@
|
||||
// straight-line programs Type and (very inefficient) interpreter
|
||||
// statement
|
||||
type User.rigille.Tiger.SL.Stm {
|
||||
CompoundStm(fst: User.rigille.Tiger.SL.Stm, snd: User.rigille.Tiger.SL.Stm)
|
||||
AssignStm(id: String, exp: User.rigille.Tiger.SL.Exp)
|
||||
PrintStm(exp_list: List<User.rigille.Tiger.SL.Exp>)
|
||||
}
|
||||
|
||||
// expression
|
||||
type User.rigille.Tiger.SL.Exp {
|
||||
IdExp(id: String)
|
||||
NumExp(num: Int) // #TODO include other numbers?
|
||||
OpExp(op: User.rigille.Tiger.SL.Binop, fst: User.rigille.Tiger.SL.Exp, snd: User.rigille.Tiger.SL.Exp)
|
||||
EseqExp(stm: User.rigille.Tiger.SL.Stm, exp: User.rigille.Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.SL.ExpList {
|
||||
PairExpList(head: User.rigille.Tiger.SL.Exp, tail: User.rigille.Tiger.SL.ExpList)
|
||||
LastExpList(head: User.rigille.Tiger.SL.Exp)
|
||||
}
|
||||
|
||||
type User.rigille.Tiger.SL.Binop {
|
||||
plus
|
||||
minus
|
||||
times
|
||||
div
|
||||
}
|
||||
|
||||
maxargs(stm: User.rigille.Tiger.SL.Stm): Nat
|
||||
case stm {
|
||||
CompoundStm: Nat.max(maxargs(stm.fst), maxargs(stm.snd))
|
||||
AssignStm: 0
|
||||
PrintStm: List.length!(stm.exp_list)
|
||||
}
|
||||
|
||||
User.rigille.Tiger.SL.interpStm(stm: User.rigille.Tiger.SL.Stm, table: List<Pair<String, Int>>): List<Pair<String, Int>>
|
||||
case stm {
|
||||
CompoundStm:
|
||||
let new_table = User.rigille.Tiger.SL.interpStm(stm.fst, table)
|
||||
User.rigille.Tiger.SL.interpStm(stm.snd, new_table)
|
||||
AssignStm:
|
||||
let {i, new_table} = User.rigille.Tiger.SL.interpExp(stm.exp, table)
|
||||
{stm.id, i} & new_table
|
||||
PrintStm:
|
||||
for exp in stm.exp_list with table:
|
||||
let {i, table} = User.rigille.Tiger.SL.interpExp(exp, table)
|
||||
log(Int.show(i))
|
||||
table
|
||||
table
|
||||
}
|
||||
|
||||
User.rigille.Tiger.SL.lookup(id: String, table: List<Pair<String, Int>>): Int
|
||||
case table {
|
||||
nil:
|
||||
0 :: Int
|
||||
cons:
|
||||
let {table_id, val} = table.head
|
||||
if id =? table_id then
|
||||
val
|
||||
else
|
||||
User.rigille.Tiger.SL.lookup(id, table.tail)
|
||||
}
|
||||
|
||||
User.rigille.Tiger.SL.interpExp(exp: User.rigille.Tiger.SL.Exp, table: List<Pair<String, Int>>): Pair<Int, List<Pair<String, Int>>>
|
||||
case exp {
|
||||
IdExp:
|
||||
{User.rigille.Tiger.SL.lookup(exp.id, table), table}
|
||||
NumExp:
|
||||
{exp.num, table}
|
||||
OpExp:
|
||||
let {fst_val, table} = User.rigille.Tiger.SL.interpExp(exp.fst, table)
|
||||
let {snd_val, table} = User.rigille.Tiger.SL.interpExp(exp.snd, table)
|
||||
case exp.op {
|
||||
plus:
|
||||
{fst_val + snd_val, table}
|
||||
minus:
|
||||
{fst_val - snd_val, table}
|
||||
times:
|
||||
{fst_val * snd_val, table}
|
||||
div:
|
||||
{fst_val / snd_val, table}
|
||||
}
|
||||
EseqExp:
|
||||
let table = User.rigille.Tiger.SL.interpStm(exp.stm, table)
|
||||
User.rigille.Tiger.SL.interpExp(exp.exp, table)
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user