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

Merge branch 'kind-lang:master' into master

Browse Source
This commit is contained in:
Jordi Saludes 2021-11-18 18:28:16 +01:00 committed by GitHub
commit b43fe75ea8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
66 changed files with 18160 additions and 16160 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
CHANGELOG.md
View File

@ -1,3 +1,19 @@
## Kind 1.0.112
- Replace syntax is like rewrite, but equality is reversed
replace x with e in goal
This replaces the right side of the equality by the left side in the goal
This should be more robust since it doesn't need to use mirror and, thus,
avoids some holes
## Kind 1.0.108
- Allow "for" to be on the left side of a list comprehension
[for x in [0 to 10] where Nat.is_even(x): x * 2]
## Kind 1.0.104
- Implicit arguments are here!

12
base/BBT/max.kind Normal file
View File

@ -0,0 +1,12 @@
BBT.max<K: Type, V: Type>(map: BBT<K, V>): Maybe<Pair<K, V>>
case map {
tip:
none
bin:
case map.right {
tip:
some({map.key, map.val})
bin:
BBT.max!!(map.right)
}
}

31
base/Bits/cmp/identity_by_o.kind Normal file
View File

@ -0,0 +1,31 @@
Bits.cmp.identity_by_o.aux.left(y : Bits) : Bits.cmp.go(Bits.e,y,Cmp.ltn) == Cmp.ltn
case y {
e : refl
o : Bits.cmp.identity_by_o.aux.left(y.pred)
i : refl
}!
Bits.cmp.identity(x : Bits, y : Bits, j : Cmp, j2 : Cmp, H : Bits.cmp.go(x, y, j) == j2)
: Bits.cmp.go(Bits.trim.insert(x), y, j) == j2
case x with H {
o :
case y with H {
i : Bits.cmp.identity(x.pred, y.pred, Cmp.ltn, j2, H)
o : Bits.cmp.identity(x.pred, y.pred, j, j2, H)
e : Bits.cmp.identity(x.pred, Bits.e, j, j2, H)
}!
i : case y with H {
i : Bits.cmp.identity(x.pred, y.pred, j, j2, H)
o : Bits.cmp.identity(x.pred, y.pred, Cmp.gtn, j2, H)
e : H
}!
e : case y with H {
i :
let H = H :: Cmp.ltn == j2
case H {
refl : Bits.cmp.identity_by_o.aux.left(y.pred)
}!
o : H
e : H
}!
}!

65
base/Bits/hex.kind
View File

@ -1,62 +1,65 @@
// This function is fully expanded for max performance
Bits.hex.encode(x: Bits): String
Bits.hex.encode.go("", x)
Bits.hex.encode.go(acc: String, x: Bits): String
case x {
e: ""
e: acc
o: case x.pred as x {
e: "0"
e: acc|"0"
o: case x.pred as x {
e: "0"
e: acc|"0"
o: case x.pred as x {
e: "0"
o: "0" | Bits.hex.encode(x.pred)
i: "8" | Bits.hex.encode(x.pred)
e: acc|"0"
o: Bits.hex.encode.go(acc|"0", x.pred)
i: Bits.hex.encode.go(acc|"8", x.pred)
}
i: case x.pred as x {
e: "4"
o: "4" | Bits.hex.encode(x.pred)
i: "c" | Bits.hex.encode(x.pred)
e: acc|"4"
o: Bits.hex.encode.go(acc|"4", x.pred)
i: Bits.hex.encode.go(acc|"c", x.pred)
}
}
i: case x.pred as x {
e: "2"
e: acc|"2"
o: case x.pred as x {
e: "2"
o: "2" | Bits.hex.encode(x.pred)
i: "a" | Bits.hex.encode(x.pred)
e: acc|"2"
o: Bits.hex.encode.go(acc|"2", x.pred)
i: Bits.hex.encode.go(acc|"a", x.pred)
}
i: case x.pred as x {
e: "6"
o: "6" | Bits.hex.encode(x.pred)
i: "e" | Bits.hex.encode(x.pred)
e: acc|"6"
o: Bits.hex.encode.go(acc|"6", x.pred)
i: Bits.hex.encode.go(acc|"e", x.pred)
}
}
}
i: case x.pred as x {
e: "1"
e: acc|"1"
o: case x.pred as x {
e: "1"
e: acc|"1"
o: case x.pred as x {
e: "1"
o: "1" | Bits.hex.encode(x.pred)
i: "9" | Bits.hex.encode(x.pred)
e: acc|"1"
o: Bits.hex.encode.go(acc|"1", x.pred)
i: Bits.hex.encode.go(acc|"9", x.pred)
}
i: case x.pred as x {
e: "5"
o: "5" | Bits.hex.encode(x.pred)
i: "d" | Bits.hex.encode(x.pred)
e: acc|"5"
o: Bits.hex.encode.go(acc|"5", x.pred)
i: Bits.hex.encode.go(acc|"d", x.pred)
}
}
i: case x.pred as x {
e: "3"
e: acc|"3"
o: case x.pred as x {
e: "3"
o: "3" | Bits.hex.encode(x.pred)
i: "b" | Bits.hex.encode(x.pred)
e: acc|"3"
o: Bits.hex.encode.go(acc|"3", x.pred)
i: Bits.hex.encode.go(acc|"b", x.pred)
}
i: case x.pred as x {
e: "7"
o: "7" | Bits.hex.encode(x.pred)
i: "f" | Bits.hex.encode(x.pred)
e: acc|"7"
o: Bits.hex.encode.go(acc|"7", x.pred)
i: Bits.hex.encode.go(acc|"f", x.pred)
}
}
}

8
base/Bits/to_nat.kind
View File

@ -1,6 +1,6 @@
Bits.to_nat(b: Bits): Nat
case b {
e: 0,
o: Nat.mul(2, Bits.to_nat(b.pred)),
i: Nat.succ(Nat.mul(2, Bits.to_nat(b.pred)))
}
e: Nat.zero
o: Nat.double(Bits.to_nat(b.pred))
i: Nat.succ(Nat.double(Bits.to_nat(b.pred)))
}

22
base/Bits/to_nat/identity.kind Normal file
View File

@ -0,0 +1,22 @@
Bits.to_nat.identity.aux0(x: Bits): Bits.to_nat(Bits.inc(x)) == Nat.succ(Bits.to_nat(x))
case x {
e: refl
o: refl
i: apply(Nat.double, Bits.to_nat.identity.aux0(x.pred))
}!
Bits.to_nat.identity.aux1(x: Nat): Nat.to_bits(Nat.succ(x)) == Bits.inc(Nat.to_bits(x))
case x {
zero: refl
succ: apply(Bits.inc, Bits.to_nat.identity.aux1(x.pred))
}!
Bits.to_nat.identity(n: Nat): Equal<Nat, n, Bits.to_nat(Nat.to_bits(n))>
case n {
zero:
refl
succ:
rewrite X in Nat.succ(n.pred) == Bits.to_nat(X) with Bits.to_nat.identity.aux1(n.pred)
rewrite X in Nat.succ(n.pred) == X with Bits.to_nat.identity.aux0(Nat.to_bits(n.pred))
apply(Nat.succ, Bits.to_nat.identity(n.pred))
}!

3
base/Bits/to_string.kind Normal file
View File

@ -0,0 +1,3 @@
// TODO:
Bits.to_string(bits: Bits): String
Bits.to_string(bits)

9
base/Bits/trim.kind
View File

@ -6,4 +6,11 @@ Bits.trim(new_len: Nat, bits: Bits): Bits
o: Bits.o(Bits.trim(new_len.pred, bits.pred)),
i: Bits.i(Bits.trim(new_len.pred, bits.pred)),
}
}
}
Bits.trim.insert(bits: Bits): Bits
case bits {
e : Bits.o(Bits.e)
o : Bits.o(Bits.trim.insert(bits.pred))
i : Bits.i(Bits.trim.insert(bits.pred))
}

23
base/Bits/trim/identity.kind Normal file
View File

@ -0,0 +1,23 @@
Bits.trim.identity(bits : Bits) : Bits.trim(Bits.length(bits), bits) == bits
case bits {
e : refl
o :
let rec = Bits.trim.identity(bits.pred)
case refl :: Bits.length.go(bits.pred,1) == Bits.length(Bits.o(bits.pred)) {
refl :
let H = Bits.length.succ(bits.pred, 0)
case H {
refl : Equal.apply!!!!(Bits.o, rec)
}!
}!
i :
let rec = Bits.trim.identity(bits.pred)
case refl :: Bits.length.go(bits.pred,1) == Bits.length(Bits.i(bits.pred)) {
refl :
let H = Bits.length.succ(bits.pred, 0)
case H {
refl : Equal.apply!!!!(Bits.i, rec)
}!
}!
}!

6
base/Bool/show.kind
View File

@ -1,5 +1,5 @@
Bool.show(b: Bool): String
case b {
true: "Bool.true",
false: "Bool.false",
}
true: "true",
false: "false",
}

81
base/Bytes.kind Normal file
View File

@ -0,0 +1,81 @@
// Bytes
// =====
//Byte: Type
//Word<8>
Bytes: Type
List<U8>
Bytes.show(bytes: Bytes): String
List.show!(Bits.show, List.map!!(U8.to_bits, bytes))
Bytes.to_nat.go<size: Nat>(byte: Word<size>): Nat
case byte {
e: Nat.zero
o: Nat.double(Bytes.to_nat.go<byte.size>(byte.pred))
i: Nat.succ(Nat.double(Bytes.to_nat.go<byte.size>(byte.pred)))
}
Bytes.to_nat(bytes: Bytes): Nat
case bytes {
nil:
Nat.zero
cons:
let head = Bytes.to_nat.go<8>(bytes.head@value)
let tail = Bytes.to_nat(bytes.tail)
Nat.add(head, Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(tail)))))))))
}
Bytes.from_nat.go(n: Nat, r: Bytes): Bytes
case n {
zero: r
succ: Bytes.from_nat.go(n.pred, Bytes.inc(r))
}
Bytes.from_nat(n: Nat): Bytes
Bytes.from_nat.go(n, [])
//Bytes.inc.go<size: Nat>(byte: Word<size>): Pair<Word<size>, Bool>
//case byte {
//e: {Word.e, true}
//o: {Word.i!(byte.pred), false}
//i: case Bytes.inc.go!(byte.pred) as result {
//new: {Word.o!(result.fst), result.snd}
//}
//}!
Bytes.inc(bytes: Bytes): Bytes
case bytes {
nil:
[1#8]
cons:
if U8.eql(bytes.head, 255#8) then
List.cons!(0#8, Bytes.inc(bytes.tail))
else
List.cons!(U8.inc(bytes.head), bytes.tail)
}
//case bytes {
//nil: [1#8]
//cons: case Bytes.inc.go!(bytes.head@value) as result {
//new: case result.snd {
//true: List.cons!(U8.new(result.fst), Bytes.inc(bytes.tail))
//false: List.cons!(U8.new(result.fst), bytes.tail)
//}
//}
//}
//Bytes.from_nat.identity(n: Nat): Equal<Nat, Bytes.to_nat(Bytes.from_nat(n)), n>
//Bytes.from_nat.identity(n)
//Aux.1(
//n: Nat
//e0: Nat.ltn(0, n) == true
//e1: Nat.ltn(n, 256) == true
//): Equal<Bytes, Bytes.from_nat(n), [Nat.apply!(n, Word.inc<8>, Word.zero(8))]>
//Aux.1(n, e0, e1)

22
base/Cmp/equal.kind Normal file
View File

@ -0,0 +1,22 @@
Cmp.equal(x : Cmp, y : Cmp) : Bool
case x {
gtn : Cmp.as_gtn(y)
ltn : Cmp.as_ltn(y)
eql : Cmp.as_eql(y)
}
Cmp.equal.absurd(x : Cmp, y : Cmp, H : x == y, H2 : Cmp.equal(x, y) == false) : Empty
case x with H H2 {
gtn :
case H with H2 {
refl : Empty.absurd!(Bool.false_neq_true(mirror(H2)))
}!
ltn :
case H with H2 {
refl : Empty.absurd!(Bool.false_neq_true(mirror(H2)))
}!
eql :
case H with H2 {
refl : Empty.absurd!(Bool.false_neq_true(mirror(H2)))
}!
}!

2
base/Ether/Bits/pad.kind
View File

@ -108,7 +108,7 @@ Ether.Bits.mul_injective(x : Nat, y : Nat, n : Nat, H : Nat.mul(Nat.succ(n), x)
}!
}!
Ether.Bits.succ_pad_nat(x : Bits) :
Ether.Bits.succ_pad_nat(x : Bits) :
Bits.to_nat(Bits.trim(Bits.length(x), x)) == Bits.to_nat(x)
case x {
e : refl

20
base/Ether/RLP/README.md Normal file
View File

@ -0,0 +1,20 @@
# RLP
The purpose of RLP (Recursive Length Prefix) is to encode arbitrarily nested arrays of binary data, and RLP is the main encoding method used to serialize objects in Ethereum. The only purpose of RLP is to encode structure; encoding specific data types (eg. strings, floats) is left up to higher-order protocols;
### Example
The string “dog” = `[ 0x83, ‘d’, ‘o’, ‘g’ ]`
The list [ “cat”, “dog” ] = `[ 0xc8, 0x83, 'c', 'a', 't', 0x83, 'd', 'o', 'g' ]`
The empty string (‘null’) = `[ 0x80 ]`
The empty list = `[ 0xc0 ]`
The integer 0 = `[ 0x80 ]`
The encoded integer 0 (’\x00’) = `[ 0x00 ]`
The encoded integer 15 (’\x0f’) = `[ 0x0f ]`
The encoded integer 1024 (’\x04\x00’) = `[ 0x82, 0x04, 0x00 ]`
The set theoretical representation of three, [ [], [[]], [ [], [[]] ] ] = `[ 0xc7, 0xc0, 0xc1, 0xc0, 0xc3, 0xc0, 0xc1, 0xc0 ]`
The string “Lorem ipsum dolor sit amet, consectetur adipisicing elit” = `[ 0xb8, 0x38, 'L', 'o', 'r', 'e', 'm', ' ', ... , 'e', 'l', 'i', 't' ]`
### Reference
- [Ethereum Wiki](https://eth.wiki/fundamentals/rlp)
- [Ethers.js](https://github.com/ethers-io/ethers.js/tree/master/packages/rlp)

3
base/Ether/RLP/bitify/byte.kind Normal file
View File

@ -0,0 +1,3 @@
// TODO:
Ether.RLP.bitify.byte(b: Byte): Ether.RLP.Tree
Ether.RLP.Tree.tip(Bits.empty)

2
base/Ether/RLP/bitify/empty.kind Normal file
View File

@ -0,0 +1,2 @@
Ether.RLP.bitify.empty: Ether.RLP.Tree
Ether.RLP.Tree.tip(Bits.e)

2
base/Ether/RLP/bitify/nat.kind Normal file
View File

@ -0,0 +1,2 @@
Ether.RLP.bifity.nat(n: Nat): Ether.RLP.Tree
Ether.RLP.Tree.tip(Nat.to_bits(n))

2
base/Ether/RLP/bitify/string.kind Normal file
View File

@ -0,0 +1,2 @@
Ether.RLP.bitify.string(s: String): Ether.RLP.Tree
Ether.RLP.Tree.tip(String.to_bits(s))

10
base/Ether/RLP/decode.kind
View File

@ -21,17 +21,19 @@ Ether.RLP.decode(bits : Bits) : Pair<Ether.RLP.Tree<Bits>, Bits>
Ether.RLP.Constants.bits_192 :
let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
let {head, rest} = Ether.Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head)
let length = Ether.RLP.encode.read.binary(head) * 8
let {prefix, rest} = Ether.Bits.break(length*8, rest)
{Ether.RLP.Tree.tip!(prefix), rest}
Ether.RLP.Constants.bits_248 :
let content_length = (Bits.to_nat(byte_prefix) - 192) * 8
let {xs, rest} = Ether.RLP.decode.decode_list(rest)
let {content, _} = Ether.Bits.break(content_length, rest)
let {xs, rest} = Ether.RLP.decode.decode_list(content)
{Ether.RLP.Tree.list!(xs), rest}
Ether.RLP.Constants.bits_255 :
let content_length = (Bits.to_nat(byte_prefix) - 247) * 8
let {head, rest} = Ether.Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head)
let {xs, rest} = Ether.RLP.decode.decode_list(rest)
let length = Ether.RLP.encode.read.binary(head) * 8
let {content, _} = Ether.Bits.break(length, rest)
let {xs, rest} = Ether.RLP.decode.decode_list(content)
{Ether.RLP.Tree.list!(xs), rest}
} default {Ether.RLP.Tree.tip!(Bits.e), Bits.e}

19
base/Ether/RLP/encode.kind
View File

@ -11,7 +11,10 @@ Ether.RLP.encode(tree : Ether.RLP.Tree<Bits>) : Bits
let bytes = Bits.e
for item in tree.value with bytes :
Bits.concat(bytes, Ether.RLP.encode(item))
let bytes_size = Ether.Bits.get_bytes_size(bytes)
let bytes_size = if Bits.eql(bytes, Bits.e) then
0
else
Ether.Bits.get_bytes_size(bytes)
Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 192), bytes)
}
@ -64,18 +67,20 @@ Ether.RLP.encode.read(bits : Bits) : Pair<String, Bits>
Ether.RLP.Constants.bits_192 :
let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
let {head, rest} = Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head)
let {prefix, rest} = Bits.break(length*8, rest)
let length = Ether.RLP.encode.read.binary(head) * 8
let {prefix, rest} = Bits.break(length, rest)
{String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head))
| String.reverse(Bits.hex.encode(prefix)), rest}
Ether.RLP.Constants.bits_248 :
let content_length = (Bits.to_nat(byte_prefix) - 192) * 8
let {xs, rest} = Ether.RLP.encode.read_list(rest)
let {content, rest} = Ether.Bits.break(content_length, rest)
let {xs, _} = Ether.RLP.encode.read_list(content)
{String.reverse(Bits.hex.encode(byte_prefix)) | xs, rest}
Ether.RLP.Constants.bits_255 :
let content_length = (Bits.to_nat(byte_prefix) - 247) * 8
let {head, rest} = Bits.break(content_length, rest)
let length = Ether.RLP.encode.read.binary(head)
let {xs, rest} = Ether.RLP.encode.read_list(rest)
{String.reverse(Bits.hex.encode(byte_prefix)) | xs, rest}
let length = Ether.RLP.encode.read.binary(head) * 8
let {content, rest} = Ether.Bits.break(length, rest)
let {xs, _} = Ether.RLP.encode.read_list(content)
{String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head)) | xs, rest}
} default {"", Bits.e}

64
base/Ether/RLP/section.kind
View File

@ -19,6 +19,17 @@ Ether.RLP.Tree.to_nat(x : Ether.RLP.Tree<Bits>) : Ether.RLP.Tree<Nat>
}
Nat.complete_diff(x : Nat, y : Nat, H : Nat.lte(x, y) == true) : (x + (y - x)) == y
case x with H {
zero : refl
succ : case y with H {
zero : Empty.absurd!(Bool.false_neq_true(H))
succ :
let rec = Nat.complete_diff(x.pred, y.pred, H)
Equal.apply!!!!(Nat.succ, rec)
}!
}!
Ether.RLP.section.pad_bits8_correctude(value : Bits, H : (Ether.Bits.get_bytes_size(value) =? 1) == true) :
Bits.take(8,Ether.Bits.pad(8,value)) == Ether.Bits.pad(8,value)
let H = Ether.Bits.get_bytes_size.identity_bits_8(value, H)
@ -27,16 +38,57 @@ Ether.RLP.section.pad_bits8_correctude(value : Bits, H : (Ether.Bits.get_bytes_s
refl :
(case Nat.eql(Nat.mod(Bits.length(value),8),0) as H {
true : (_) Bits.take.identity(8, value, H)
false : (H1) ?a-70
} : (Nat.eql(Nat.mod(Bits.length(value),8),0) == H) -> Bits.take(8,H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))) == H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)))(refl)
false : (H1)
let H2 = Nat.Order.trichotomy(Bits.length(value), 8)
let H3 = refl :: Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value) == Bool.false(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))
case H3 {
refl :
case H2 {
fst :
let absurd = Equal.chain(Bool, true, Nat.lte(Bits.length(value),8), false, Equal.mirror(Bool, Nat.lte(Bits.length(value),8), true, H), H2.value)
Empty.absurd!(Bool.false_neq_true(mirror(absurd)))
snd :
let H1 = Equal.rewrite(Nat, Bits.length(value), 8, H2.value, (Y) Nat.eql(Nat.mod(Y,8),0) == Bool.false, H1)
Empty.absurd!(Bool.false_neq_true(mirror(H1)))
trd :
let H2 = Nat.lte.comm.false(8, Bits.length(value), H2.value)
let H2 = Nat.mod.le_mod(Bits.length(value), 8, H2)
let H2 = Equal.mirror(Nat, Nat.mod(Bits.length(value),8), Bits.length(value), H2)
case H2 {
refl :
let H3 = Nat.complete_diff(Bits.length(value), 8, H)
let H3 = Equal.mirror(Nat, Nat.add(Bits.length(value),Nat.sub(8,Bits.length(value))), 8, H3)
let H4 = Equal.mirror(Nat, Bits.length(Bits.trim(8,value)), 8, Bits.trim.preserve_length(8, value))
let H5 = Bits.take.identity(8, Bits.trim(8,value))
let H6 = refl :: Nat.lte(8, 8) == true
let H6 = H6 :: rewrite X in Nat.lte(X, 8) == Bool.true with H4
let qed = Equal.rewrite(Nat, 8, Nat.add(Bits.length(value),Nat.sub(8,Bits.length(value))), H3, (Y) Bits.take(8,Bits.trim(Y,value)) == Bits.trim(Y,value), H5(H6))
qed
// qed :: rewrite X in Bits.take(8,Bits.trim(X,value)) == Bits.trim(X,value) with H3
} : Bits.take(8,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8, H2.b)),value)) == Bits.trim(Nat.add(Bits.length(value),Nat.sub(8, H2.b)),value)
}
}!
} : (Nat.eql(Nat.mod(Bits.length(value),8),0) == H) -> Bits.take(8,H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value))) == H(() Bits,value,Bits.trim(Nat.add(Bits.length(value),Nat.sub(8,Nat.mod(Bits.length(value),8))),value)))(refl)
}!
Ether.RLP.section.tip_case(value : Bits, H : Bits.ltn(value,Ether.RLP.Constants.bits_128) == true) :
Ether.RLP.section.tip_case(value : Bits, H : Bits.ltn(value,Ether.RLP.Constants.bits_128) == true, H2 : (Ether.Bits.get_bytes_size(value) =? 1) == true) :
Ether.RLP.Tree.to_nat(Pair.fst(Ether.RLP.Tree(Bits),Bits,Ether.RLP.decode(Ether.Bits.pad(8,value))))
== Ether.RLP.Tree.to_nat(Ether.RLP.Tree.tip(Bits,value))
let rewr = Ether.Bits.break(8,Ether.Bits.pad(8,value)) == {Ether.Bits.pad(8,value), Bits.drop(8, Ether.Bits.pad(8,value))}
_
// ?a-46
case refl :: Ether.Bits.break(8,Ether.Bits.pad(8,value),() Pair(Ether.RLP.Tree(Bits),Bits),(byte_prefix) (rest) Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),rest),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),128),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),183),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),247),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e))))))) == Ether.RLP.decode(Ether.Bits.pad(8,value)) {
refl :
case refl :: Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),Bits.drop(8,Ether.Bits.pad(8,value))),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),128),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),183),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(Bits.take(8,Ether.Bits.pad(8,value)),Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(Bits.take(8,Ether.Bits.pad(8,value))),247),8),Bits.drop(8,Ether.Bits.pad(8,value)),() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e)))))) == Ether.Bits.break(8,Ether.Bits.pad(8,value),() Pair(Ether.RLP.Tree(Bits),Bits),(byte_prefix) (rest) Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128,() Pair(Ether.RLP.Tree(Bits),Bits),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Ether.Bits.pad(8,value)),rest),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_184,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),128),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_192,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),183),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.Bits.break(Nat.mul(Ether.RLP.encode.read.binary(head),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(prefix) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,prefix),rest))),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_248,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest)),Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_255,() Pair(Ether.RLP.Tree(Bits),Bits),Ether.Bits.break(Nat.mul(Nat.sub(Bits.to_nat(byte_prefix),247),8),rest,() Pair(Ether.RLP.Tree(Bits),Bits),(head) (rest) Ether.RLP.decode.decode_list(rest,() Pair(Ether.RLP.Tree(Bits),Bits),(xs) (rest) Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.list(Bits,xs),rest))),Pair.new(Ether.RLP.Tree(Bits),Bits,Ether.RLP.Tree.tip(Bits,Bits.e),Bits.e))))))) {
refl :
let pad_id = Ether.RLP.section.pad_bits8_correctude(value, H2)
let pad_id = Equal.mirror(Bits, Bits.take(8,Ether.Bits.pad(8,value)), Ether.Bits.pad(8,value), pad_id)
case pad_id {
refl : ?a
}!
}!
}!
// case Bits.ltn(byte_prefix,Ether.RLP.Constants.bits_128) {
// true : ?a
// false : _
// }!
Ether.RLP.section(tree : Ether.RLP.Tree<Bits>) :
Equal(Ether.RLP.Tree<Nat>, Ether.RLP.Tree.to_nat((Pair.fst!!(Ether.RLP.decode(Ether.RLP.encode(tree))))), Ether.RLP.Tree.to_nat(tree))

11
base/Ether/RLP/show.kind Normal file
View File

@ -0,0 +1,11 @@
Ether.RLP.to_string(t: List(Ether.RLP.Tree<Bits>)): String
case t {
nil : ""
cons:
"[ " |
case t.head as tree {
tip : Bits.show(tree.value) | ", "
list: Ether.RLP.to_string(t.tail)
}
| " ]"
}

10
base/Ether/RLP/show_list_tree.kind Normal file
View File

@ -0,0 +1,10 @@
Ether.RLP.show_list_tree(l: List<Ether.RLP.Tree<Bits>>): String
Ether.RLP.show_list_tree.aux(l, "")
Ether.RLP.show_list_tree.aux(l: List<Ether.RLP.Tree<Bits>>, aux: String): String
case l {
nil : aux
cons:
let s = aux | Ether.RLP.show_tree(l.head)
Ether.RLP.show_list_tree.aux(l.tail, s)
}

5
base/Ether/RLP/show_tree.kind Normal file
View File

@ -0,0 +1,5 @@
Ether.RLP.show_tree(t: Ether.RLP.Tree<Bits>): String
case t {
tip : "[" | Bits.show(t.value) | "]"
list: Ether.RLP.show_list_tree(t.value)
}

10
base/Ether/RLP/test/all.kind Normal file
View File

@ -0,0 +1,10 @@
RLP.test.all: TestSuite
TestSuite.many("RLP",
[
RLP.test.encode
])
// Show all tests for String
RLP.test.show: _
log(TestSuite.show(RLP.test.all, 0))
0

171
base/Ether/RLP/test/encode.kind Normal file
View File

@ -0,0 +1,171 @@
RLP.test.encode: TestSuite
TestSuite.many("RLP.encode", [
RLP.test.encode.0, RLP.test.encode.1, RLP.test.encode.2,
RLP.test.encode.3, RLP.test.encode.4, RLP.test.encode.5,
RLP.test.encode.6, RLP.test.encode.7, RLP.test.encode.8,
RLP.test.encode.9, RLP.test.encode.10, RLP.test.encode.11
])
// zero
RLP.test.encode.0: TestSuite
let test = "0"
let bin = Ether.RPL.encode.binary(0)
let got = Ether.RLP.encode.read(bin)
let exp = "0x80"
let name = "0"
TestSuite.show.log_string(name, test, exp, got)
// Small int
RLP.test.encode.1: TestSuite
let test = "1"
let bin = Ether.RPL.encode.binary(1)
let got = Ether.RLP.encode.read(bin)
let exp = "0x01"
let name = "1"
TestSuite.show.log_string(name, test, exp, got)
// Small int
RLP.test.encode.2: TestSuite
let test = "16"
let bin = Ether.RPL.encode.binary(16)
let got = Ether.RLP.encode.read(bin)
let exp = "0x10"
let name = "2"
TestSuite.show.log_string(name, test, exp, got)
// Small int
RLP.test.encode.3: TestSuite
let test = "79"
let bin = Ether.RPL.encode.binary(79)
let got = Ether.RLP.encode.read(bin)
let exp = "0x4f"
let name = "3"
TestSuite.show.log_string(name, test, exp, got)
// Medium int
RLP.test.encode.4: TestSuite
let test = "100000"
let bin = Ether.RPL.encode.binary(100000)
let got = Ether.RLP.encode.read(bin)
let exp = "0x830186a0"
let name = "4"
TestSuite.show.log_string(name, test, exp, got)
// Medium int
RLP.test.encode.5: TestSuite
let test = "1000"
let bin = Ether.RPL.encode.binary(1000)
let got = Ether.RLP.encode.read(bin)
let exp = "0x8203e8"
let name = "5"
TestSuite.show.log_string(name, test, exp, got)
// Empty list
RLP.test.encode.6: TestSuite
let test = "[]"
// let bin = Ether.RPL.encode.binary(1000)
let got = Ether.RLP.encode.read([])
let exp = "0xc0"
let name = "6"
TestSuite.show.log_string(name, test, exp, got)
// String list
RLP.test.encode.7: TestSuite
let test = "['dog', 'god', 'cat']"
let got = Ether.RLP.encode(RLP.test.list_string)
let exp = "0xcc83646f6783676f6483636174"
let name = "7"
TestSuite.show.log_string(name, test, exp, got)
// List of list
RLP.test.encode.8: TestSuite
let test = "[[[], []], []]"
let got = Ether.RLP.encode(RLP.test.empty)
let exp = "0xc4c2c0c0c0"
let name = "8"
TestSuite.show.log_string(name, test, exp, got)
// multilist
RLP.test.encode.9: TestSuite
let test = "['zw', [4], 1]"
let got = Ether.RLP.encode(RLP.test.multilist)
let exp = "0xc6827a77c10401"
let name = "9"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.10: TestSuite
let test = "dictionary example"
let got = Ether.RLP.encode(RLP.test.dictionary)
let exp = "0xecca846b6579318476616c31ca846b6579328476616c32ca846b6579338476616c33ca846b6579348476616c34"
let name = "10"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.11: TestSuite
let test = "long list"
let got = Ether.RLP.encode(RLP.test.long_list)
let exp = "0xf840cf84617364668471776572847a786376cf84617364668471776572847a786376cf84617364668471776572847a786376cf84617364668471776572847a786376"
let name = "11"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.12: TestSuite
let test = "long string"
let got = Ether.RLP.encode(Ether.RLP.bitify.string(
"Lorem ipsum dolor sit amet, consectetur adipisicing elit"
))
let exp = "0xb8384c6f72656d20697073756d20646f6c6f722073697420616d65742c20636f6e7365637465747572206164697069736963696e6720656c6974"
let name = "12"
TestSuite.show.log_string(name, test, exp, got)
RLP.test.encode.12: TestSuite
let test = "loooong string"
let got = Ether.RLP.encode(Ether.RLP.bitify.string(
"Lorem ipsum dolor sit amet, consectetur adipiscing elit. Curabitur mauris magna, suscipit sed vehicula non, iaculis faucibus tortor. Proin suscipit ultricies malesuada. Duis tortor elit, dictum quis tristique eu, ultrices at risus. Morbi a est imperdiet mi ullamcorper aliquet suscipit nec lorem. Aenean quis leo mollis, vulputate elit varius, consequat enim. Nulla ultrices turpis justo, et posuere urna consectetur nec. Proin non convallis metus. Donec tempor ipsum in mauris congue sollicitudin. Vestibulum ante ipsum primis in faucibus orci luctus et ultrices posuere cubilia Curae; Suspendisse convallis sem vel massa faucibus, eget lacinia lacus tempor. Nulla quis ultricies purus. Proin auctor rhoncus nibh condimentum mollis. Aliquam consequat enim at metus luctus, a eleifend purus egestas. Curabitur at nibh metus. Nam bibendum, neque at auctor tristique, lorem libero aliquet arcu, non interdum tellus lectus sit amet eros. Cras rhoncus, metus ac ornare cursus, dolor justo ultrices metus, at ullamcorper volutpat"
))
let exp = "0xb904004c6f72656d20697073756d20646f6c6f722073697420616d65742c20636f6e73656374657475722061646970697363696e6720656c69742e20437572616269747572206d6175726973206d61676e612c20737573636970697420736564207665686963756c61206e6f6e2c20696163756c697320666175636962757320746f72746f722e2050726f696e20737573636970697420756c74726963696573206d616c6573756164612e204475697320746f72746f7220656c69742c2064696374756d2071756973207472697374697175652065752c20756c7472696365732061742072697375732e204d6f72626920612065737420696d70657264696574206d6920756c6c616d636f7270657220616c6971756574207375736369706974206e6563206c6f72656d2e2041656e65616e2071756973206c656f206d6f6c6c69732c2076756c70757461746520656c6974207661726975732c20636f6e73657175617420656e696d2e204e756c6c6120756c74726963657320747572706973206a7573746f2c20657420706f73756572652075726e6120636f6e7365637465747572206e65632e2050726f696e206e6f6e20636f6e76616c6c6973206d657475732e20446f6e65632074656d706f7220697073756d20696e206d617572697320636f6e67756520736f6c6c696369747564696e2e20566573746962756c756d20616e746520697073756d207072696d697320696e206661756369627573206f726369206c756374757320657420756c74726963657320706f737565726520637562696c69612043757261653b2053757370656e646973736520636f6e76616c6c69732073656d2076656c206d617373612066617563696275732c2065676574206c6163696e6961206c616375732074656d706f722e204e756c6c61207175697320756c747269636965732070757275732e2050726f696e20617563746f722072686f6e637573206e69626820636f6e64696d656e74756d206d6f6c6c69732e20416c697175616d20636f6e73657175617420656e696d206174206d65747573206c75637475732c206120656c656966656e6420707572757320656765737461732e20437572616269747572206174206e696268206d657475732e204e616d20626962656e64756d2c206e6571756520617420617563746f72207472697374697175652c206c6f72656d206c696265726f20616c697175657420617263752c206e6f6e20696e74657264756d2074656c6c7573206c65637475732073697420616d65742065726f732e20437261732072686f6e6375732c206d65747573206163206f726e617265206375727375732c20646f6c6f72206a7573746f20756c747269636573206d657475732c20617420756c6c616d636f7270657220766f6c7574706174"
let name = "12"
TestSuite.show.log_string(name, test, exp, got)
// -- MOCK --
RLP.test.list_string: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let arr = [bitify_str("dog"), bitify_str("god"), bitify_str("cat")]
Ether.RLP.Tree.list(arr)
// Tree for: ['zw', [4], 1]
RLP.test.multilist: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let tree_num = (num: Nat) Ether.RLP.Tree.list([Ether.RLP.bifity.nat(num)])
Ether.RLP.Tree.list([bitify_str("zw"), tree_num(4), Ether.RLP.bifity.nat(1)])
// [[[], []], []]
RLP.test.empty: Ether.RLP.Tree
Ether.RLP.Tree.list([
Ether.RLP.Tree.list([Ether.RLP.bitify.empty, Ether.RLP.bitify.empty]),
Ether.RLP.bitify.empty
])
// [["key1", "val1"], ["key2", "val2"], ...]
RLP.test.dictionary: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let entry = (key: String, val: String) Ether.RLP.Tree.list([bitify_str(key), bitify_str(val)])
Ether.RLP.Tree.list([
entry("key1", "val1"),
entry("key2", "val2"),
entry("key3", "val3"),
entry("key4", "val4")
])
// [["asdf", "qwer", "zxcv"], ["asdf", "qwer", "zxcv"], ...]
RLP.test.long_list: Ether.RLP.Tree
let bitify_str = (val: String) Ether.RLP.bitify.string(val)
let entry = (key: String, val1: String, val2: String) Ether.RLP.Tree.list([bitify_str(key), bitify_str(val1), bitify_str(val2)])
Ether.RLP.Tree.list([
entry("asdf", "qwer", "zxcv"),
entry("asdf", "qwer", "zxcv"),
entry("asdf", "qwer", "zxcv"),
entry("asdf", "qwer", "zxcv")
])
// Reference: https://github.com/ethereumjs/rlp/blob/master/test/fixture/rlptest.json

15
base/Ether/tests.kind
View File

@ -1,13 +1,8 @@
round_n(n : Nat, m : Nat) : Nat
case Nat.lte(m, 8) {
true : 8 - m
false : round_n(n, m-8)
}
Ether.tests : Nat
let m = 32
let n = 8
m + (n - (if Nat.eql(Nat.mod(m, n), 0) then m else Nat.mod(m, n)))
Ether.tests : _
let test = Ether.RLP.Tree.list!([Ether.RLP.Tree.tip!(Nat.to_bits(222222))])
//let list = [test, test, test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test,test]
// let tree = Ether.RLP.Tree.list(Bits, [Ether.RLP.Tree.list!(list)])
Ether.RLP.encode.read(Ether.RLP.encode(test))
//let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")

11
base/Example/json.kind Normal file
View File

@ -0,0 +1,11 @@
Example.json: IO<Unit>
IO {
let result = Maybe {
get name = JSON.parse(`"Roberta"`)
get json = JSON.parse(`{"name": "Robert", "age": 42, "items": ["sword", "shield","book"]}`)
get json = JSON.set(json, "name", name)
return JSON.stringify(json)
} <> ""
IO.print(result)
}

14
base/JSON.kind
View File

@ -1,8 +1,8 @@
type JSON {
null,
bool(x: Bool),
number(x: F64),
string(x: String),
array(x: List<JSON>),
object(x: List<Pair<String, JSON>>)
}
null
bool(value: Bool)
number(value: F64)
string(value: String)
array(value: List<JSON>)
object(value: Map<JSON>)
}

41
base/Kind/Parser/comprehension.kind
View File

@ -19,8 +19,8 @@ Kind.Parser.comprehension: Parser<Kind.Term>
let filter_fun = Kind.Term.ref("List.filter")
let filter_fun = Kind.Term.app(filter_fun, Kind.Term.hol(Bits.e))
let lamb_filter = Kind.Term.lam(elem, (i) and)
let filter_fun = Kind.Term.app(filter_fun, lamb_filter)
let lam_filter = Kind.Term.lam(elem, (i) and)
let filter_fun = Kind.Term.app(filter_fun, lam_filter)
let filter_fun = Kind.Term.app(filter_fun, list)
let term = Kind.Term.ref("List.map")
@ -33,6 +33,41 @@ Kind.Parser.comprehension: Parser<Kind.Term>
return term
}
Kind.Parser.comprehension.mapped: Parser<Kind.Term>
Parser {
Kind.Parser.text("[")
Kind.Parser.text("for")
get elem = Kind.Parser.name1
Kind.Parser.text("in")
get list = Kind.Parser.term
get cond = Parser.maybe!(Parser {
Kind.Parser.text("where")
get cond = Kind.Parser.term
return cond
})
Kind.Parser.text(":")
get loop = Kind.Parser.term
Kind.Parser.text("]")
let term = Kind.Term.ref("List.map")
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let lamb = Kind.Term.lam(elem, (i) loop)
let term = Kind.Term.app(term, lamb)
let term = Kind.Term.app(term, case cond {
none:
list
some:
let filt = Kind.Term.ref("List.filter")
let filt = Kind.Term.app(filt, Kind.Term.hol(Bits.e))
let filt = Kind.Term.app(filt, Kind.Term.lam(elem, (i) cond.value))
let filt = Kind.Term.app(filt, list)
filt
})
return term
}
// transform list of Kind.Term in a Kind.Term representing a list
Kind.Parser.comprehension.and_all(a: List<Kind.Term>): Kind.Term
case a {
@ -105,4 +140,4 @@ Kind.Parser.comprehension_range.go(typename: Maybe<String>): Parser(Kind.Term)
return list(typename.value)
}
}
})
})

97
base/Kind/Parser/do.kind
View File

@ -1,16 +1,35 @@
Kind.Parser.do: Parser(Kind.Term)
Kind.Parser.block("do", Parser {
Parser.maybe!(Kind.Parser.text("do "))
get name = Kind.Parser.name1
get name = Kind.Parser.name1
get params = Parser.until!(Kind.Parser.text_now(" {"),
Parser.choice!([
Kind.Parser.items_now!("(", Kind.Parser.term, ")")
Kind.Parser.items_now!("<", Kind.Parser.term, ">")
Parser {
Kind.Parser.text_now("!")
return [Kind.Term.hol(Bits.e)]
}
])
)
let params = List.flatten!(params)
let type = Kind.Term.ref(name)
let monad = Kind.Term.ref(String.concat(name, ".monad"))
let result = {type, monad}
for param in params with result:
open result
let n_type = Kind.Term.app(result.fst, param)
let n_monad = Kind.Term.app(result.snd, param)
{n_type, n_monad}
let {type, monad} = result
if String.is_upper(String.slice(0,1,name)) then Parser {
Parser.text(" {")
get term = Kind.Parser.do.statements(name)
get term = Kind.Parser.do.statements(name, type, monad)
Kind.Parser.text("}")
return term
} else Parser.fail!("Not a do-block.")
})
Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
Kind.Parser.do.statements(monad_name: Kind.Name, type: Kind.Term, monad: Kind.Term): Parser(Kind.Term)
Parser.choice!([
// Binding call: @ask x = expr rest@
Kind.Parser.block("do-get", Parser {
@ -22,9 +41,9 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
Kind.Parser.text("=")
get expr = Kind.Parser.term
Parser.maybe!(Kind.Parser.text(";"))
get body = Kind.Parser.do.statements(monad_name)
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), Kind.Term.ref(monad_name))
let term = Kind.Term.app(term, Kind.Term.ref(String.concat(monad_name, ".monad")))
get body = Kind.Parser.do.statements(monad_name, type, monad)
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), type)
let term = Kind.Term.app(term, monad)
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, expr)
@ -36,8 +55,8 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
Kind.Parser.text("return ")
get expr = Kind.Parser.term
Parser.maybe!(Kind.Parser.text(";"))
let term = Kind.Term.app(Kind.Term.ref("Monad.pure"), Kind.Term.ref(monad_name))
let term = Kind.Term.app(term, Kind.Term.ref(String.concat(monad_name, ".monad")))
let term = Kind.Term.app(Kind.Term.ref("Monad.pure"), type)
let term = Kind.Term.app(term, monad)
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, expr)
return term
@ -52,15 +71,15 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
get upto = Kind.Parser.term
Kind.Parser.text(":")
get loop = Kind.Parser.term
get body = Parser.maybe!(Kind.Parser.do.statements(monad_name))
get body = Parser.maybe!(Kind.Parser.do.statements(monad_name, type, monad))
let expr = Kind.Term.ref("Nat.for.io")
let expr = Kind.Term.app(expr, from)
let expr = Kind.Term.app(expr, upto)
let expr = Kind.Term.app(expr, Kind.Term.lam(name, (x) loop))
case body {
some: Parser {
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), Kind.Term.ref(monad_name))
let term = Kind.Term.app(term, Kind.Term.ref(String.concat(monad_name, ".monad")))
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), type)
let term = Kind.Term.app(term, monad)
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, expr)
@ -80,15 +99,15 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
get list = Kind.Parser.term
Kind.Parser.text(":")
get loop = Kind.Parser.term
get body = Parser.maybe!(Kind.Parser.do.statements(monad_name))
get body = Parser.maybe!(Kind.Parser.do.statements(monad_name, type, monad))
let expr = Kind.Term.ref("List.for.io")
let expr = Kind.Term.app(expr, Kind.Term.hol(Bits.e))
let expr = Kind.Term.app(expr, list)
let expr = Kind.Term.app(expr, Kind.Term.lam(name, (x) loop))
case body {
some: Parser {
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), Kind.Term.ref(monad_name))
let term = Kind.Term.app(term, Kind.Term.ref(String.concat(monad_name, ".monad")))
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), type)
let term = Kind.Term.app(term, monad)
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, expr)
@ -101,34 +120,34 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
}
})
// Binders
Kind.Parser.letforrange.u32((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letforrange.u32.with((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letforrange.nat((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letforrange.nat.with((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letforin((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letforin.with((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letwhile((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letwhile.with((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.getforin((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.getforin.with((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.let.abort((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.let((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.getwhile((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.getwhile.with((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.get((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.def((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.lens.let((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.use.abort((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.use((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.log((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.open((x) Kind.Parser.do.statements(monad_name))
Kind.Parser.letforrange.u32((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letforrange.u32.with((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letforrange.nat((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letforrange.nat.with((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letforin((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letforin.with((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letwhile((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.letwhile.with((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.getforin((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.getforin.with((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.let.abort((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.let((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.getwhile((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.getwhile.with((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.get((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.def((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.lens.let((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.use.abort((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.use((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.log((x) Kind.Parser.do.statements(monad_name, type, monad))
Kind.Parser.open((x) Kind.Parser.do.statements(monad_name, type, monad))
// Non-binding call: @expr rest@
Kind.Parser.block("do-statement", Parser {
get expr = Kind.Parser.term
Parser.maybe!(Kind.Parser.text(";"))
get body = Kind.Parser.do.statements(monad_name)
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), Kind.Term.ref(monad_name))
let term = Kind.Term.app(term, Kind.Term.ref(String.concat(monad_name, ".monad")))
get body = Kind.Parser.do.statements(monad_name, type, monad)
let term = Kind.Term.app(Kind.Term.ref("Monad.bind"), type)
let term = Kind.Term.app(term, monad)
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, expr)

34
base/Kind/Parser/lens.kind
View File

@ -29,15 +29,17 @@ Kind.Parser.lens(term: Kind.Term): Parser<Kind.Term>
Parser {
get dirs = Parser.many1!(Kind.Parser.lens.path)
Parser.choice!([
Parser {
Kind.Parser.text("<-")
get xval = Kind.Parser.term
return Kind.Parser.lens.mutter(term, () xval, dirs)
}
// mut
Parser {
Kind.Parser.text("<~")
get xfun = Kind.Parser.term
return Kind.Parser.lens.mutter(term, (x) Kind.Term.app(xfun, x), dirs)
return Kind.Parser.lens.mutter(term, (x) Kind.Term.app(xfun, x), dirs, false)
}
// set
Parser {
Kind.Parser.text("<-")
get xval = Kind.Parser.term
return Kind.Parser.lens.mutter(term, () xval, dirs, true)
}
Parser {
return Kind.Parser.lens.getter(term, dirs)
@ -50,33 +52,37 @@ Kind.Parser.lens.let(body: Unit -> Parser(Kind.Term)): Parser<Kind.Term>
Kind.Parser.text("let ")
get name = Kind.Parser.name1
get dirs = Parser.many1!(Kind.Parser.lens.path)
get symb = Parser.option([Kind.Parser.text("<-"), Kind.Parser.text("<~")])
get symb = Parser.option([Kind.Parser.text("<~"), Kind.Parser.text("<-")])
get expr = Kind.Parser.term
Parser.maybe!(Kind.Parser.text(";"))
get body = body(unit)
let expr = Kind.Parser.lens.mutter(Kind.Term.ref(name), case symb { zero: () expr, succ: (x) Kind.Term.app(expr,x) }, dirs)
let expr = case symb {
zero: Kind.Parser.lens.mutter(Kind.Term.ref(name), (x) Kind.Term.app(expr,x), dirs, false)
succ: Kind.Parser.lens.mutter(Kind.Term.ref(name), (x) expr, dirs, true)
}
return Kind.Term.let(name, expr, (x) body)
}
Kind.Parser.lens.mutter(expr: Kind.Term, func: Kind.Term -> Kind.Term, dirs: List<Kind.Parser.lens.dir>): Kind.Term
Kind.Parser.lens.mutter(expr: Kind.Term, func: Kind.Term -> Kind.Term, dirs: List<Kind.Parser.lens.dir>, is_set: Bool): Kind.Term
case dirs {
nil: func(expr)
cons: case dirs.head {
record:
//foo@x <- 7
Kind.Term.mut(expr, dirs.head.key, Kind.Term.lam("x", (x) Kind.Parser.lens.mutter(x, func, dirs.tail)))
Kind.Term.mut(expr, dirs.head.key, Kind.Term.lam("x", (x) Kind.Parser.lens.mutter(x, func, dirs.tail, is_set)))
list:
let term = Kind.Term.ref("List.mut")
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, dirs.head.key)
let term = Kind.Term.app(term, Kind.Term.lam("x", (x) Kind.Parser.lens.mutter(x, func, dirs.tail)))
let term = Kind.Term.app(term, Kind.Term.lam("x", (x) Kind.Parser.lens.mutter(x, func, dirs.tail, is_set)))
let term = Kind.Term.app(term, expr)
term
map:
let term = Kind.Term.ref("Map.mut")
let sets = List.is_empty!(dirs.tail) && is_set
let term = Kind.Term.ref(if sets then "Map.set" else "Map.mut")
let term = Kind.Term.app(term, Kind.Term.hol(Bits.e))
let term = Kind.Term.app(term, dirs.head.key)
let term = Kind.Term.app(term, Kind.Term.lam("x", (x) Kind.Parser.lens.mutter(x, func, dirs.tail)))
let argf = if sets then func(Kind.Term.ref("?")) else Kind.Term.lam("x", (x) Kind.Parser.lens.mutter(x, func, dirs.tail, is_set))
let term = Kind.Term.app(term, argf)
let term = Kind.Term.app(term, expr)
term
}

1
base/Kind/Parser/term.kind
View File

@ -47,6 +47,7 @@ Kind.Parser.term: Parser(Kind.Term)
Kind.Parser.chain
Kind.Parser.mirror
Kind.Parser.comprehension
Kind.Parser.comprehension.mapped
Kind.Parser.comprehension_range
Kind.Parser.list
Kind.Parser.map

2
base/Kind/version.kind
View File

@ -1,2 +1,2 @@
Kind.version: String
"1.0.105"
"1.0.113"

71
base/Parser/JSON.kind Normal file
View File

@ -0,0 +1,71 @@
Parser.JSON: Parser<JSON>
Parser.choice!([
Parser.JSON.string
Parser.JSON.array
Parser.JSON.object
Parser.JSON.null
Parser.JSON.bool
Parser.JSON.number
])
Parser.JSON.null: Parser<JSON>
Parser {
Parser.spaces_text("null")
return JSON.null
}
Parser.JSON.bool: Parser<JSON>
Parser.choice!([
Parser {
Parser.spaces_text("true")
return JSON.bool(true)
}
Parser {
Parser.spaces_text("false")
return JSON.bool(false)
}
])
Parser.JSON.number: Parser<JSON>
Parser {
Parser.spaces
get val = Parser.f64
return JSON.number(val)
}
Parser.JSON.string: Parser<JSON>
Parser {
Parser.spaces
get str = Parser.string
return JSON.string(str)
}
Parser.JSON.array: Parser<JSON>
Parser {
get vals = Parser.wrap!(
Parser.spaces_text("[")
Parser {
get val = Parser.JSON
Parser.maybe!(Parser.spaces_text(","))
return val
}
Parser.spaces_text("]"))
return JSON.array(vals)
}
Parser.JSON.object: Parser<JSON>
Parser {
get key_vals = Parser.wrap!(
Parser.spaces_text("{")
Parser {
Parser.spaces
get key = Parser.string
Parser.spaces_text(":")
get val = Parser.JSON
Parser.maybe!(Parser.spaces_text(","))
return {key, val}
}
Parser.spaces_text("}"))
return JSON.object(Map.from_list!(key_vals))
}

18
base/Parser/char.kind Normal file
View File

@ -0,0 +1,18 @@
Parser.char: Parser<Char>
Parser {
Parser.text("'")
get chrx = Parser.char.single
Parser.text("'")
return chrx
}
Parser.char.single: Parser<Char>
Parser.choice!([
Parser.choice!(List.mapped!(Parser.escapes)!((esc) case esc {
new: Parser {
Parser.text(esc.fst)
return esc.snd
}
}))
Parser.one
])

16
base/Parser/escapes.kind Normal file
View File

@ -0,0 +1,16 @@
Parser.escapes: List<Pair<String, Char>>
[
{"\\b" , '\b'},
{"\\f" , '\f'},
{"\\n" , '\n'},
{"\\r" , '\r'},
{"\\t" , '\t'},
{"\\v" , '\v'},
{String.cons(Parser.escapes.backslash, String.cons(Parser.escapes.backslash, String.nil)), Parser.escapes.backslash},
{"\\\"", '"'},
{"\\0" , '\0'},
{"\\'" , '\''},
]
Parser.escapes.backslash: Char
Nat.to_u16(92)

15
base/Parser/f64.kind Normal file
View File

@ -0,0 +1,15 @@
Parser.f64: Parser<F64>
Parser {
get num = Parser.num
open num
let val = Nat.to_f64(num.numb)
let val = case num.sign {
none: val
some: if num.sign.value then val * 1.0 else val * -1.0
}
let val = case num.frac {
none: val
some: log("TODO") val
}
return val
}

22
base/Parser/string.kind Normal file
View File

@ -0,0 +1,22 @@
Parser.string.go(delim: Char, str: String): Parser<String>
(pst)
open pst
case pst.str {
nil:
Parser.Reply.fail<String>(pst.nam, pst.ini, pst.idx, "Non-terminating string.")
cons:
if U16.eql(pst.str.head, delim) then
let pst = Parser.State.new(pst.err, pst.nam, pst.ini, Nat.succ(pst.idx), pst.str.tail)
Parser.Reply.value<String>(pst, String.reverse(str))
else case Parser.char.single(pst) as parsed {
error: Parser.Reply.error<String>(parsed.err)
value: Parser.string.go(delim, String.cons(parsed.val,str), parsed.pst)
}
}
Parser.string: Parser<String>
Parser {
Parser.text(String.cons('"', String.nil))
get strx = Parser.string.go('"', "")
return strx
}

122
base/RLP.kind Normal file
View File

@ -0,0 +1,122 @@
// The RLP format
//
// Serialization and deserialization for the BytesTree type, under the following grammar:
// | First byte | Meaning |
// | ---------- | -------------------------------------------------------------------------- |
// | 0 to 127 | HEX(leaf) |
// | 128 to 183 | HEX(length_of_leaf + 128) + HEX(leaf) |
// | 184 to 191 | HEX(length_of_length_of_leaf + 128 + 56) + HEX(length_of_leaf) + HEX(leaf) |
// | 192 to 247 | HEX(length_of_node + 192) + HEX(node) |
// | 248 to 255 | HEX(length_of_length_of_node + 192 + 56) + HEX(length_of_node) + HEX(node) |
//
// The first byte of RLP.encode.length
// buffer length (len) | RLP.encode.length(add,len)[0]
// ------------------- | -----------------------------
// 56 ~ 256**1-1 | 185
// 256**1 ~ 256**2-1 | 186
// 256**2 ~ 256**3-1 | 187
// 256**3 ~ 256**4-1 | 188
// 256**4 ~ 256**5-1 | 189
// 256**5 ~ 256**6-1 | 190
// 256**6 ~ 256**7-1 | 191
// Type
// ----
type RLP {
data(value: List<U8>)
node(child: List<RLP>)
}
// Length
// ------
RLP.decoder.byte(bytes: Bytes): Pair<Bytes, U8>
case bytes {
nil: {[], 0#8}
cons: {bytes.tail, bytes.head}
}
RLP.encode.length(add: Nat, length: Nat): Bytes
if Nat.ltn(length, 56) then
Bytes.from_nat(Nat.add(add,length))
else
let a = Bytes.from_nat(Nat.add(56, Nat.add(add, RLP.needed_bytes(length))))
let b = Bytes.from_nat(length)
List.concat!(a, b)
RLP.decoder.length(add: Nat, bytes: Bytes): Pair<Bytes, Nat>
case bytes {
nil:
{[], 0}
cons:
let fst = Nat.sub(Bytes.to_nat([bytes.head]), add)
if Nat.ltn(fst, 56) then
{bytes.tail, fst}
else
let {bytes, length} = RLP.decoder.repeat!(RLP.decoder.byte, Nat.sub(fst,56), bytes.tail)
{bytes, Bytes.to_nat(length)}
}
RLP.decode.length(add: Nat, bytes: Bytes): Nat
case RLP.decoder.length(add, bytes) as got {
new: got.snd
}
// Repeat
// ------
RLP.encode.repeat<A: Type>(encode: A -> Bytes, values: List<A>): Bytes
case values {
nil: []
cons: List.concat!(encode(values.head), RLP.encode.repeat<A>(encode, values.tail))
}
RLP.decoder.repeat<A: Type>(decoder: Bytes -> Pair<Bytes,A>, count: Nat, bytes: Bytes): Pair<Bytes, List<A>>
case count {
zero:
{bytes, []}
succ:
let {bytes, head} = decoder(bytes)
let {bytes, tail} = RLP.decoder.repeat<A>(decoder, count.pred, bytes)
{bytes, head & tail}
}
RLP.encode.many(trees: List<RLP>): Bytes
RLP.encode.repeat<RLP>(RLP.encode, trees)
// RLP
// ---
RLP.encode(tree: RLP): Bytes
case tree {
data:
if Bool.and(Nat.eql(List.length!(tree.value),1), U8.ltn(List.head_with_default!(0#8,tree.value), 128#8)) then
tree.value
else
List.concat!(RLP.encode.length(128, List.length!(tree.value)), tree.value)
node:
List.concat!(RLP.encode.length(192, List.length!(tree.child)), RLP.encode.many(tree.child))
}
RLP.decoder(bytes: Bytes): Pair<Bytes, RLP>
case bytes {
nil:
{[], RLP.data([])}
cons:
if U8.ltn(bytes.head, 128#8) then
{List.tail!(bytes), RLP.data([List.head_with_default!(0#8,bytes)])}
else if U8.ltn(bytes.head, 192#8) then
let {bytes, count} = RLP.decoder.length(128, bytes)
let {bytes, value} = RLP.decoder.repeat!(RLP.decoder.byte, count, bytes)
{bytes, RLP.data(value)}
else
let {bytes, count} = RLP.decoder.length(192, bytes)
let {bytes, child} = RLP.decoder.repeat!(RLP.decoder, count, bytes)
{bytes, RLP.node(child)}
}
RLP.decode(bytes: Bytes): RLP
case RLP.decoder(bytes) as got {
new: got.snd
}

184
base/RLP/aux.kind Normal file
View File

@ -0,0 +1,184 @@
// These sub-theorems were not proven yet!
// Most of them are simple, and should be finished over the next days
// TODO: include `a <= 192`
RLP.aux.0(
add: Nat
len: Nat
pf0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
): Nat.ltn(0,Nat.add(add,len)) == Bool.true
RLP.aux.0(add, len, pf0)
// TODO: include `a <= 192`
RLP.aux.1(
a: Nat
n: Nat
e: Equal<Bool, Nat.ltn(n,56), true>
): Equal<Bool, Nat.ltn(Nat.add(a,n), 256), true>
RLP.aux.1(a, n, e)
RLP.aux.2(
n: Nat
e0: Equal<Bool, Nat.ltn(0, n), true>
e1: Equal<Bool, Nat.ltn(n, 256), true>
): Equal<Bytes, Bytes.from_nat(n), [Nat.apply<U8>(n, U8.inc, U8.zero)]>
RLP.aux.2(n, e0, e1)
// TODO: include `a <= 192`
RLP.aux.3(
a: Nat
n: Nat
e: Equal<Bool, Nat.ltn(n,56), true>
): Equal<Bool, Nat.ltn(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(a,n),U8.inc,U8.zero),List.nil(U8))),a),56), true>
RLP.aux.3(a, n, e)
// TODO: include `a <= 192`
RLP.aux.4(
a: Nat
n: Nat
e: Equal<Bool, Nat.ltn(n,56), true>
): Equal<Nat, Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(a,n),U8.inc,U8.zero),List.nil(U8))),a), n>
RLP.aux.4(a, n, e)
// TODO: include `a <= 192`
// TODO: include `n < RLP.max_len` (otherwise this is actually false)
RLP.aux.5(
a: Nat
n: Nat
): Equal<Bool, Nat.ltn(Nat.add(56, Nat.add(a, RLP.needed_bytes(n))), 256), true>
RLP.aux.5(a, n)
// TODO: include `a <= 192`
RLP.aux.6(
a: Nat
n: Nat
): Equal<Bool, Nat.ltn(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(a,RLP.needed_bytes(n))),U8.inc,U8.zero),List.nil(U8))),a),56), false>
RLP.aux.6(a, n)
// TODO: include `a <= 192`
RLP.aux.7(
a: Nat
n: Nat
): Equal<Nat, Nat.sub(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(a,RLP.needed_bytes(n))),U8.inc,U8.zero),List.nil(U8))),a),56), List.length(U8,Bytes.from_nat(n))>
RLP.aux.7(a, n)
RLP.aux.8(
xs: Bytes
ys: Bytes
): Equal<Pair<Bytes,Bytes>, RLP.decoder.repeat<U8>(RLP.decoder.byte,List.length(U8,xs),List.concat<U8>(xs,ys)), Pair.new!!(ys, xs)>
RLP.aux.8(xs,ys)
RLP.aux.9(
n: Nat
): Equal<Nat, Bytes.to_nat(Bytes.from_nat(n)), n>
RLP.aux.9(n)
RLP.aux.10(
a: Bool
b: Bool
e: Equal<Bool, Bool.and(a,b), true>
): Equal<Bool, a, true>
RLP.aux.10(a, b, e)
RLP.aux.11(
a: Bool
b: Bool
e: Equal<Bool, Bool.and(a,b), true>
): Equal<Bool, b, true>
RLP.aux.11(a, b, e)
RLP.aux.12(
xs: List<U8>
e1: Equal<Bool, Nat.eql(List.length(U8,xs),1), Bool.true>
): Equal<List<U8>, xs, List.cons<U8>(List.head_with_default<U8>(Nat.to_u8(0),xs), List.nil<U8>)>
RLP.aux.12(xs, e1)
RLP.aux.13(
xs: Bytes
ys: Bytes
e0: Nat.eql(List.length(U8,xs),1) == Bool.true
): Equal<Bytes, List.tail(U8,List.concat(U8,xs,ys)), ys>
RLP.aux.13(xs, ys, e0)
RLP.aux.14(
xs: Bytes
ys: Bytes
e0: Nat.eql(List.length(U8,xs),1) == Bool.true
): Equal<Bytes, List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,xs,ys)),List.nil(U8)), xs>
RLP.aux.14(xs, ys, e0)
RLP.aux.15(
x: U8
xs: Bytes
ys: Bytes
zs: Bytes
): Equal<Bytes, List.cons(U8,x,List.concat(U8,List.concat(U8,xs,ys),zs)), List.concat(U8,List.cons(U8,x,xs),List.concat(U8,ys,zs))>
RLP.aux.15(x, xs, ys, zs)
RLP.aux.15.sym(
x: U8
xs: Bytes
ys: Bytes
zs: Bytes
): Equal<Bytes, List.concat(U8,List.cons(U8,x,xs),List.concat(U8,ys,zs)), List.cons(U8,x,List.concat(U8,List.concat(U8,xs,ys),zs))>
mirror(RLP.aux.15(x, xs, ys, zs))
RLP.aux.16(
xs: Bytes
): Equal<Bytes, List.concat<U8>(xs, List.nil<U8>), xs>
case xs {
nil: refl
cons:
let a = RLP.aux.16(xs.tail)
let b = apply(List.cons<U8>(xs.head), a)
b
}!
RLP.aux.17(
len: Nat
): Not<Equal<Bytes, RLP.encode.length(128, len), List.nil(U8)>>
RLP.aux.17(len)
RLP.aux.18(
len: Nat
): Not<Equal<Bytes, RLP.encode.length(192, len), List.nil(U8)>>
RLP.aux.18(len)
RLP.aux.19(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(128,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 128#8), false>
RLP.aux.19(len, head, tail, prof)
RLP.aux.20(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(128,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 192#8), true>
RLP.aux.20(len, head, tail, prof)
RLP.aux.21(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(192,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 128#8), false>
RLP.aux.21(len, head, tail, prof)
RLP.aux.22(
len: Nat
head: U8
tail: Bytes
prof: Equal<Bytes, RLP.encode.length(192,len), List.cons(U8,head,tail)>
): Equal<Bool, U8.ltn(head, 192#8), false>
RLP.aux.22(len, head, tail, prof)
RLP.aux.23<A: Type>(
xs: List<A>
ys: List<A>
zs: List<A>
): Equal<List<A>, List.concat<A>(List.concat<A>(xs,ys),zs), List.concat<A>(xs,List.concat<A>(ys,zs))>
RLP.aux.23<A>(xs, ys, zs)

72
base/RLP/encode_identity.kind Normal file
View File

@ -0,0 +1,72 @@
RLP.encode_identity(rlp: RLP): RLP.decode(RLP.encode(rlp)) == rlp
let pf = RLP.encode_identity.go(rlp, [])
let e0 = RLP.aux.16(RLP.encode(rlp))
let e1 = pf :: rewrite X in RLP.decoder(X) == Pair.new(Bytes,RLP,List.nil(U8),rlp) with e0
replace X with mirror(e1) in X((got) RLP,(got.fst) (got.snd) got.snd) == rlp
refl
RLP.encode_identity.go(rlp: RLP, bts: Bytes): Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat<U8>(RLP.encode(rlp),bts)), Pair.new<Bytes,RLP>(bts,rlp)>
let ref_0 = RLP.encode_length_identity.go
let ref_1 = RLP.encode_repeat_identity.go
case rlp {
data:
let e0 = Equal.refl<Bool, Bool.and(Nat.eql(List.length(U8,rlp.value),1),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(128)))>
case Bool.and(Nat.eql(List.length(U8,rlp.value),1),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(128))) as X
with e0 : Equal<Bool, Bool.and(Nat.eql(List.length(U8,rlp.value),1),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(128))), X> {
true:
let e1 = RLP.aux.10(_, _, e0)
let e2 = RLP.aux.11(_, _, e0)
let e3 = RLP.aux.12(rlp.value, e1)
replace X with mirror(e3) in List.concat(U8,X,bts,(bytes) Pair(Bytes,RLP),Pair.new(Bytes,RLP,List.nil(U8),RLP.data(List.nil(U8))),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.concat(U8,rlp.value,bts)),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,rlp.value,bts)),List.nil(U8)))),U8.ltn(bytes.head,Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
replace X with mirror(e2) in X(() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.concat(U8,rlp.value,bts)),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,rlp.value,bts)),List.nil(U8)))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.concat(U8,rlp.value,bts),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e4 = RLP.aux.13(rlp.value, bts, e1)
replace X with mirror(e4) in Pair.new(List(U8),RLP,X,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.concat(U8,rlp.value,bts)),List.nil(U8)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e5 = RLP.aux.14(rlp.value, bts, e1)
replace X with mirror(e5) in Pair.new(List(U8),RLP,bts,RLP.data(X)) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
refl
false:
let e1 = Equal.refl<Bytes, RLP.encode.length(128,List.length(U8,rlp.value))>
case RLP.encode.length(128,List.length(U8,rlp.value)) as X
with e1 : Equal<Bytes, RLP.encode.length(128,List.length(U8,rlp.value)), X> {
nil:
let e2 = RLP.aux.17(List.length(U8,rlp.value))
let e3 = e2(e1)
Empty.absurd!(e3)
cons:
let e2 = RLP.aux.19(List.length(U8,rlp.value), X.head, X.tail, e1)
replace X with mirror(e2) in X(() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts))),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts))),List.nil(U8)))),U8.ltn(X.head,Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e3 = RLP.aux.20(List.length(U8,rlp.value), X.head, X.tail, e1)
replace X with mirror(e3) in X(() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,rlp.value),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e4 = RLP.aux.15.sym(X.head, X.tail, rlp.value, bts)
replace X with e4 in RLP.decoder.length(128,X,() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
replace X with e1 in RLP.decoder.length(128,List.concat(U8,X,List.concat(U8,rlp.value,bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e5 = RLP.encode_length_identity.go(128, List.length<U8>(rlp.value), List.concat(U8,rlp.value,bts), Either.left!!(refl))
replace X with mirror(e5) in X(() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
let e6 = RLP.aux.8(rlp.value, bts)
replace X with mirror(e6) in X(() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value))) == Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))
refl
}: Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat(U8,List.concat(U8,X,rlp.value),bts)), Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))>
} : Equal<Pair<Bytes,RLP>, RLP.decoder(List.concat(U8,X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value)),bts)), Pair.new(Bytes,RLP,bts,RLP.data(rlp.value))>
node:
let e0 = refl
case RLP.encode.length(192,List.length(RLP,rlp.child)) as X
with e0 : Equal<Bytes, RLP.encode.length(192,List.length(RLP,rlp.child)), X> {
nil:
let e1 = RLP.aux.18(List.length(RLP,rlp.child))
let e2 = e1(e0)
Empty.absurd!(e2)
cons:
let e1 = RLP.aux.21(List.length(RLP,rlp.child), X.head, X.tail, e0)
replace X with mirror(e1) in X(() Pair(Bytes,RLP),Pair.new(List(U8),RLP,List.tail(U8,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts))),RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts))),List.nil(U8)))),U8.ltn(X.head,Nat.to_u8(192),() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e2 = RLP.aux.22(List.length(RLP,rlp.child), X.head, X.tail, e0)
replace X with mirror(e2) in X(() Pair(Bytes,RLP),RLP.decoder.length(128,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(U8,RLP.decoder.byte,count,bytes,() Pair(Bytes,RLP),(bytes) (value) Pair.new(Bytes,RLP,bytes,RLP.data(value)))),RLP.decoder.length(192,List.cons(U8,X.head,List.concat(U8,List.concat(U8,X.tail,RLP.encode.many(rlp.child)),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e3 = RLP.aux.15.sym(X.head, X.tail, RLP.encode.many(rlp.child), bts)
replace X with e3 in RLP.decoder.length(192,X,() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
replace X with e0 in RLP.decoder.length(192,List.concat(U8,X,List.concat(U8,RLP.encode.many(rlp.child),bts)),() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e4 = RLP.encode_length_identity.go(192, List.length(RLP,rlp.child), List.concat(U8,RLP.encode.many(rlp.child),bts), Either.right!!(refl))
replace X with mirror(e4) in X(() Pair(Bytes,RLP),(bytes) (count) RLP.decoder.repeat(RLP,RLP.decoder,count,bytes,() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child)))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
let e5 = RLP.encode_repeat_identity.go<RLP>(RLP.encode, RLP.decoder, RLP.encode_identity.go, rlp.child, bts)
replace X with mirror(e5) in X(() Pair(Bytes,RLP),(bytes) (child) Pair.new(Bytes,RLP,bytes,RLP.node(child))) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
refl
} : RLP.decoder(List.concat(U8,List.concat(U8,X,RLP.encode.many(rlp.child)),bts)) == Pair.new(Bytes,RLP,bts,RLP.node(rlp.child))
}!

32
base/RLP/encode_length_identity.kind Normal file
View File

@ -0,0 +1,32 @@
RLP.encode_length_identity.go(
add: Nat
len: Nat
bts: Bytes
pf0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
): Equal<Pair<Bytes,Nat>, RLP.decoder.length(add,List.concat<U8>(RLP.encode.length(add,len),bts)), Pair.new<Bytes,Nat>(bts,len)>
let e0 = refl
case Nat.ltn(len,56) as X with e0 : Equal<Bool, Nat.ltn(len,56), X> {
true:
let e1 = RLP.aux.0(add, len, pf0)
let e2 = RLP.aux.1(add, len, e0)
let e3 = RLP.aux.2(Nat.add(add,len), e1, e2)
replace X with mirror(e3) in RLP.decoder.length(add,List.concat(U8,X,bts)) == Pair.new(Bytes,Nat,bts,len)
let e4 = RLP.aux.3(add, len, e0)
replace X with mirror(e4) in X(() Pair(Bytes,Nat),Pair.new(List(U8),Nat,List.concat(U8,List.nil(U8),bts),Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(add,len),U8.inc,U8.zero),List.nil(U8))),add)),RLP.decoder.repeat(U8,RLP.decoder.byte,Nat.sub(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(add,len),U8.inc,U8.zero),List.nil(U8))),add),56),List.concat(U8,List.nil(U8),bts),() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length)))) == Pair.new(Bytes,Nat,bts,len)
let e5 = RLP.aux.4(add, len, e0)
replace X with mirror(e5) in Pair.new(List(U8),Nat,bts,X) == Pair.new(Bytes,Nat,bts,len)
refl
false:
let e1 = RLP.aux.5(add, len)
let e2 = RLP.aux.2(Nat.add(56,Nat.add(add,RLP.needed_bytes(len))), refl, e1)
replace X with mirror(e2) in RLP.decoder.length(add,List.concat(U8,List.concat(U8,X,Bytes.from_nat(len)),bts)) == Pair.new(Bytes,Nat,bts,len)
let e3 = RLP.aux.6(add, len)
replace X with mirror(e3) in X(() Pair(Bytes,Nat),Pair.new(List(U8),Nat,List.concat(U8,List.concat(U8,List.nil(U8),Bytes.from_nat(len)),bts),Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(add,RLP.needed_bytes(len))),U8.inc,U8.zero),List.nil(U8))),add)),RLP.decoder.repeat(U8,RLP.decoder.byte,Nat.sub(Nat.sub(Bytes.to_nat(List.cons(U8,Nat.apply(U8,Nat.add(56,Nat.add(add,RLP.needed_bytes(len))),U8.inc,U8.zero),List.nil(U8))),add),56),List.concat(U8,List.concat(U8,List.nil(U8),Bytes.from_nat(len)),bts),() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length)))) == Pair.new(Bytes,Nat,bts,len)
let e4 = RLP.aux.7(add, len)
replace X with mirror(e4) in RLP.decoder.repeat(U8,RLP.decoder.byte,X,List.concat(U8,List.concat(U8,List.nil(U8),Bytes.from_nat(len)),bts),() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length))) == Pair.new(Bytes,Nat,bts,len)
let e5 = RLP.aux.8(Bytes.from_nat(len), bts)
replace X with mirror(e5) in X(() Pair(Bytes,Nat),(bytes) (length) Pair.new(Bytes,Nat,bytes,Bytes.to_nat(length))) == Pair.new(Bytes,Nat,bts,len)
let e6 = RLP.aux.9(len)
replace X with mirror(e6) in Pair.new(Bytes,Nat,bts,X) == Pair.new(Bytes,Nat,bts,len)
refl
}: RLP.decoder.length(add,List.concat(U8,X(() Bytes,Bytes.from_nat(Nat.add(add,len)),List.concat(U8,Bytes.from_nat(Nat.add(56,Nat.add(add,RLP.needed_bytes(len)))),Bytes.from_nat(len))),bts)) == Pair.new(Bytes,Nat,bts,len)

21
base/RLP/encode_repeat_identity.kind Normal file
View File

@ -0,0 +1,21 @@
RLP.encode_repeat_identity.go<A: Type>(
encode: A -> Bytes
decoder: Bytes -> Pair<Bytes,A>
identity: (val: A, bts: Bytes) -> Equal<Pair<Bytes,A>, decoder(List.concat<U8>(encode(val),bts)), Pair.new<Bytes,A>(bts,val)>
values: List<A>
rest: Bytes
) : def encoded = List.concat<U8>(RLP.encode.repeat<A>(encode, values), rest)
def decoded = RLP.decoder.repeat<A>(decoder, List.length!(values), encoded)
Equal<Pair<Bytes, List<A>>, decoded, Pair.new<Bytes, List<A>>(rest, values)>
case values {
nil:
refl
cons:
let e0 = RLP.aux.23<U8>(encode(values.head), RLP.encode.repeat(A,encode,values.tail), rest)
replace X with mirror(e0) in decoder(X)(() Pair(Bytes,List(A)),(bytes) (head) RLP.decoder.repeat(A,decoder,List.length(A,values.tail),bytes,() Pair(Bytes,List(A)),(bytes) (tail) Pair.new(Bytes,List(A),bytes,List.cons(A,head,tail)))) == Pair.new(Bytes,List(A),rest,List.cons(A,values.head,values.tail))
let e1 = identity(values.head, List.concat<U8>(RLP.encode.repeat(A,encode,values.tail),rest))
replace X with mirror(e1) in X(() Pair(Bytes,List(A)),(bytes) (head) RLP.decoder.repeat(A,decoder,List.length(A,values.tail),bytes,() Pair(Bytes,List(A)),(bytes) (tail) Pair.new(Bytes,List(A),bytes,List.cons(A,head,tail)))) == Pair.new(Bytes,List(A),rest,List.cons(A,values.head,values.tail))
let e2 = RLP.encode_repeat_identity.go<A>(encode, decoder, identity, values.tail, rest)
replace X with mirror(e2) in X(() Pair(Bytes,List(A)),(bytes) (tail) Pair.new(Bytes,List(A),bytes,List.cons(A,values.head,tail))) == Pair.new(Bytes,List(A),rest,List.cons(A,values.head,values.tail))
refl
}!

5
base/RLP/needed_bytes.kind Normal file
View File

@ -0,0 +1,5 @@
RLP.needed_bytes(length: Nat): Nat
case length {
zero: 0
succ: Nat.succ(RLP.needed_bytes(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(Nat.half(length))))))))))
}

2
base/Refinement.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement<A: Type>: Type
(a: A) -> Type

2
base/Refinement/all.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.all<A: Type>: Refinement<A>
(a: A) Unit

2
base/Refinement/complement.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.complement<T: Type>(A: Refinement<T>): Refinement<T>
(a: T) Not(A(a))

2
base/Refinement/difference.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.difference<T: Type>(A: Refinement<T>, B: Refinement<T>): Refinement<T>
Refinement.intersection<T>(A, Refinement.complement<T>(B))

2
base/Refinement/empty.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.empty<A: Type>: Refinement<A>
(a: A) Empty

2
base/Refinement/intersection.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.intersection<T: Type>(A: Refinement<T>, B: Refinement<T>): Refinement<T>
(a: T) And(A(a), B(a))

2
base/Refinement/member.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.member<T: Type>(x: T, A: Refinement<T>): Type
A(x)

2
base/Refinement/symmetric_difference.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.symmetric_difference<T: Type>(A: Refinement<T>, B: Refinement<T>): Refinement<T>
Refinement.union<T>(Refinement.difference<T>(A, B), Refinement.difference<T>(B, A))

2
base/Refinement/union.kind Normal file
View File

@ -0,0 +1,2 @@
Refinement.union<T: Type>(A: Refinement<T>, B: Refinement<T>): Refinement<T>
(a: T) Or(A(a), B(a))

10
base/String/hash_code.kind Normal file
View File

@ -0,0 +1,10 @@
// From https://stackoverflow.com/a/8831937/1031791
String.hash_code(str: String): U32
String.hash_code.go(str, 0)
String.hash_code.go(str: String, hash: U32): U32
case str {
nil: hash
cons: String.hash_code.go(str.tail, (U32.shl(hash, 5) - hash) + U16.to_u32(str.head))
}

40
base/Test.kind
View File

@ -1,26 +1,18 @@
type Object {
new(
name: String
data: Map<List<F64>>
)
}
Test: _
Either<String> {
get a = bar([[2]])
get b = foo(a)
return b
}
Test: Maybe<F64>
let obj = Object.new("sample", {
"a": [1.0, 2.0, 3.0, 4.0, 5.0, 6.0]
"b": [7.0, 7.0, 7.0, 7.0, 7.0, 7.0]
})
let obj@data{"a"}[0] <~ F64.mul(2.0)
obj@data{"a"}[0]
// ------------------------------------
id<A: $Type>(x: A): A
x
explicit: Nat
id<$Nat>(7)
implicit: Nat
id(7)
bar(ll: List<List<Nat>>): Either<String, List<Nat>>
case ll {
nil: Either.left!!("no lists")
cons: Either.right!!(ll.head)
}
foo(l: List<Nat>): Either<String, Nat>
case l {
nil: Either.left!!("empty list")
cons: Either.right!!(l.head)
}

5
base/U32/murmur2.kind Normal file
View File

@ -0,0 +1,5 @@
U32.murmur2(h: U32): U32
let h = U32.xor(h, U32.shr(h, 13))
let h = U32.mul(h, 0x5bd1e995)
let h = U32.xor(h, U32.shr(h, 15))
h

7
base/U32/murmur3.kind Normal file
View File

@ -0,0 +1,7 @@
U32.murmur3(h: U32): U32
let h = U32.xor(h, U32.shr(h, 16))
let h = U32.mul(h, 0x85ebca6b)
let h = U32.xor(h, U32.shr(h, 13))
let h = U32.mul(h, 0xc2b2ae35)
let h = U32.xor(h, U32.shr(h, 16))
h

6
base/User/rigille/List/Monotone/exists.kind
View File

@ -29,7 +29,7 @@ User.rigille.List.Monotone.exists<A: Type>(after: A -> A -> Type, O: User.rigill
def ret = ext.fst & tail_call.fst
// prove return value is a permutation
let ret_perm = (lem_left = User.rigille.List.Perm.refl<A>(xs.head & xs.tail)
let ret_perm = (let lem_left = User.rigille.List.Perm.refl<A>(xs.head & xs.tail)
// Perm(min_split.fst ++ [ext.fst] ++ min_split.snd.fst, xs.head & xs.tail)
let lem_right = lem_left :: rewrite X in Perm(X, _) with min_split.snd.snd
// Perm([ext.fst] ++ min_split.fst, min_split.fst ++ [ext.fst])
@ -54,10 +54,10 @@ User.rigille.List.Monotone.exists<A: Type>(after: A -> A -> Type, O: User.rigill
let ret_monotone = case tail_call.fst
with tail_call.snd.snd
ret_perm {
nil: qed = unit :: User.rigille.List.Monotone<A, after, O>(ext.fst & [])
nil: let qed = unit :: User.rigille.List.Monotone<A, after, O>(ext.fst & [])
qed
cons: in_tail_call = right(left(refl)) :: User.rigille.List.In<A>(ext.fst & tail_call.fst.head & tail_call.fst.tail, tail_call.fst.head)
cons: let in_tail_call = right(left(refl)) :: User.rigille.List.In<A>(ext.fst & tail_call.fst.head & tail_call.fst.tail, tail_call.fst.head)
let in_param = User.rigille.List.Perm.In<A>(_, _, _,
in_tail_call, User.rigille.List.Perm.symm<A>(_, _, ret_perm))
let qed = ext.snd.snd(_, in_param)

4
base/User/rigille/List/Perm/cat_comm.kind
View File

@ -4,11 +4,11 @@ User.rigille.List.Perm.cat_comm<A: Type>(
): User.rigille.List.Perm<A>(ys ++ xs, xs ++ ys)
def Perm = User.rigille.List.Perm<A>
case xs {
nil: lem = User.rigille.List.Perm.refl<A>(ys)
nil: let lem = User.rigille.List.Perm.refl<A>(ys)
let calc = User.rigille.List.cat_l_nil!(ys)
let qed = lem :: rewrite X in (Perm(X, ys)) with calc
qed
cons: ind = User.rigille.List.Perm.cat_comm<A>(xs.tail, ys)
cons: let ind = User.rigille.List.Perm.cat_comm<A>(xs.tail, ys)
let lem_right = User.rigille.List.Perm.skip<A>(xs.head, _, _, ind)
let lem_left = User.rigille.List.Perm.front_to_back<A>(xs.head, ys)
let lem_left = User.rigille.List.Perm.push_tail<A>(_, _, xs.tail, lem_left)

18
bin/js/package-lock.json generated
View File

@ -1,24 +1,24 @@
{
"name": "kind-lang",
"version": "1.0.97",
"version": "1.0.110",
"lockfileVersion": 2,
"requires": true,
"packages": {
"": {
"name": "kind-lang",
"version": "1.0.97",
"version": "1.0.110",
"license": "MIT",
"dependencies": {
"formcore-js": "^0.1.92"
"formcore-js": "^0.1.95"
},
"bin": {
"kind": "src/main.js"
}
},
"node_modules/formcore-js": {
"version": "0.1.92",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.92.tgz",
"integrity": "sha512-BKhzJXSpVC5IQbQm0KYLqVnIlyKvEKRppx9DcAG8+fjejmnUdg3WAYZYGZiKLr3Iwr1WgBB04PJQaYMtfjJN1Q==",
"version": "0.1.95",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
"integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw==",
"bin": {
"fmc": "main.js"
}
@ -26,9 +26,9 @@
},
"dependencies": {
"formcore-js": {
"version": "0.1.92",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.92.tgz",
"integrity": "sha512-BKhzJXSpVC5IQbQm0KYLqVnIlyKvEKRppx9DcAG8+fjejmnUdg3WAYZYGZiKLr3Iwr1WgBB04PJQaYMtfjJN1Q=="
"version": "0.1.95",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
"integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw=="
}
}
}

4
bin/js/package.json
View File

@ -1,6 +1,6 @@
{
"name": "kind-lang",
"version": "1.0.105",
"version": "1.0.113",
"description": "Kind-Lang in JavaScript",
"main": "src/kind.js",
"scripts": {
@ -20,6 +20,6 @@
},
"homepage": "https://github.com/uwu-tech/kind#readme",
"dependencies": {
"formcore-js": "^0.1.92"
"formcore-js": "^0.1.95"
}
}

32591
bin/js/src/kind.js
View File

File diff suppressed because it is too large Load Diff

14
bin/package-lock.json generated
View File

@ -9,13 +9,13 @@
"version": "0.1.0",
"license": "MIT",
"dependencies": {
"formcore-js": "^0.1.92"
"formcore-js": "^0.1.95"
}
},
"node_modules/formcore-js": {
"version": "0.1.92",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.92.tgz",
"integrity": "sha512-BKhzJXSpVC5IQbQm0KYLqVnIlyKvEKRppx9DcAG8+fjejmnUdg3WAYZYGZiKLr3Iwr1WgBB04PJQaYMtfjJN1Q==",
"version": "0.1.95",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
"integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw==",
"bin": {
"fmc": "main.js"
}
@ -23,9 +23,9 @@
},
"dependencies": {
"formcore-js": {
"version": "0.1.92",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.92.tgz",
"integrity": "sha512-BKhzJXSpVC5IQbQm0KYLqVnIlyKvEKRppx9DcAG8+fjejmnUdg3WAYZYGZiKLr3Iwr1WgBB04PJQaYMtfjJN1Q=="
"version": "0.1.95",
"resolved": "https://registry.npmjs.org/formcore-js/-/formcore-js-0.1.95.tgz",
"integrity": "sha512-6HqawzYO+X/bPGcXuMS8jyhuN2m+J4v9vnqp12QFRCZbGRCaNW5soAc4Md8KO9e5FwK1bRXGVvKHEDgOPDI6Xw=="
}
}
}

2
bin/package.json
View File

@ -9,6 +9,6 @@
"author": "",
"license": "MIT",
"dependencies": {
"formcore-js": "^0.1.92"
"formcore-js": "^0.1.95"
}
}

179
blog/4-funcional-alquimista.md Normal file
View File

@ -0,0 +1,179 @@
Funcional Alquimista
====================
O Haskell e outras linguagens funcionais usam tipos algébricos, declarados com a sintaxe "data":
```
data Bool = True | False
data Jokenpo = Rock | Paper | Scissor
data Pair x = MakePair x x
data Maybe x = Nothing | Just x
data Nat = Zero | Succ Nat
data List x = Nil | Cons x (List x)
data Tree x = Empty | Branch x (List (Tree x))
```
Se você não entende o que está acontecendo acima, o resto não vai fazer sentido (e tudo bem); nesse caso, recomendo ler algum tutorial de Haskell caso ainda tenha interesse nesse post. Se as linhas acima fazem sentido para você, continue lendo, pois lhe contarei a história de um alquimista funcional que foi longe demais.
Era uma linda tarde de sol, quando um alquimista funcional, como outro qualquer, se perguntou a pergunta que todos fazemos um dia: "se tipos funcionais são chamados algébricos... por que não escrevemos eles como equações algébricas?" Sem saber que essa pergunta lhe levaria a um caminho sem volta que tangeria a porta da verdade, o pobre alquimista pegou um giz e, em seu já desgastado quadro negro, escreveu a seguinte equação:
```
Bool = 1 + 1
```
Em sua cabeça, isso fez sentido, porque Bool é um tipo soma, que pode ter dois valores: True e False. Na linha abaixo, ele escreveu:
```
Jokenpo = 1 + 1 + 1
```
Isso também fez sentido, porque existem 3 movimentos no Jokenpo: Rock, Paper, Scissor. Até aí, tudo parecia uma brincadeira inocente. Mas foi na próxima linha que as coisas começaram a ficar... interessantes. Se tipos soma são representados por uma adição, então tipos produto só podem ser representados com...
```
Pair x = x * x
```
Uma multiplicação! Mas isso realmente funciona? Vamos verificar: de acordo com essa equação, o tipo `Pair Jokenpo Jokenpo` deveria ter um total de `(1 + 1 + 1) * (1 + 1 + 1) = 3 * 3 = 9`, elementos. Vamos contar:
```
(Rock, Rock)
(Rock, Paper)
(Rock, Scissor)
(Paper, Rock)
(Paper, Paper)
(Paper, Scissor)
(Scissor, Rock)
(Scissor, Paper)
(Scissor, Scissor)
```
NANI!? Não pode ser. Será? Na linha abaixo, ele escreveu:
```
Maybe x = 1 + x
```
De acordo com essa equação, o tipo `Maybe Bool` deveria ter `1 + 2 = 3` elementos. Vamos contar:
```
Nothing
Just True
Just False
```
Caramba. Mas o que acontece com tipos infinitos?
```
Nat = 1 + Nat
```
Nesse caso, temos um loop:
```
Nat = 1 + 1 + Nat
Nat = 1 + 1 + 1 + Nat
Nat = 1 + 1 + 1 + 1 + ... Nat
```
O que reflete o fato que existem infinitos números naturais. Logo mais, ele descobriu que o mesmo vale para listas e árvores:
```
List x = 1 + x * List x
```
Pra visualizar essa equação, vamos primeiro contar a quantidade de elementos do tipo `List Bool`, para cada tamanho de lista:
List Bool de tamanho 0 tem 1 elemento:
```
[]
```
List Bool de tamanho 1 tem 2 elementos:
```
[True]
[False]
```
List Bool de tamanho 2 tem 4 elementos:
```
[True,True]
[True,False]
[False,True]
[False,False]
```
List Bool de tamanho 3 tem 8 elementos:
```
[True,True,True]
[True,True,False]
[True,False,True]
[True,False,False]
[False,True,True]
[False,True,False]
[False,False,True]
[False,False,False]
```
Ou seja, ao todo, List Bool tem um total de:
```
1 + 2 + 4 + 8 + 16 + ...
```
Elementos. Será que isso condiz com a equação acima? Vamos tentar aplicá-la:
```
List Bool = 1 + 2 * List Bool
List Bool = 1 + 2 * (1 + 2 * List Bool)
List Bool = 1 + 2 + 4 * List Bool
List Bool = 1 + 2 + 4 * (1 + 2 * List Bool)
List Bool = 1 + 2 + 4 + 8 * List Bool
List Bool = 1 + 2 + 4 + 8 * (1 + 2 * List Bool)
List Bool = 1 + 2 + 4 + 8 + 16 * List Bool
List Bool = ...
```
Uau! Nesse momento, o alquimista estava ciente de que havia encontrado algo realmente interessante. Ele estava à beira da porta da verdade, mas ainda havia tempo para voltar: virar de costas, fingir que aquela brincadeira nunca havia acontecido e levar uma vida normal e pacata. Mas o alquimia tinha sede por verdade, e não temia a inquisição. Então, com sangue nos olhos e as mãos tremendo, ele escreveu mais uma linha. Esta linha, eu lhes transcrevo na forma original:
```
d/dx Pair x = ?
```
Nesse momento, a porta da verdade se abriu.
```
d/dx Pair x =
d/dx (x * x) =
d/dx (x²) =
2x
```
Essa linha lhe disse que a derivada do tipo par, representado por "x * x", é o tipo representado por "x + x", ou seja:
```
data DeltaPair x = Fst x | Snd x
```
Mas qual seria a relação desse tipo, com o tipo par? O alquimista, perplexo, pensou por muito tempo, até formular a seguinte teoria: se a derivada de uma função algébrica é uma função capaz de focar em um ponto infinitesimal da função original, então, a derivada de um tipo algébrico deveria ser um tipo capaz de focar em um ponto do tipo original. Isso fez sentido. Afinal, se temos o par `(5, 7)`, então, podemos focar em dois elementos: o da esquerda, `(*, 7)`, ou o da direita, `(5, *)`. Esses dois pontos de foco podem ser representados pelo tipo DeltaPair, como `Fst 7` ou `Snd 5`, respectivamente. Para confirmar essa teoria, o alquimista tentou aplicar o mesmo ao tipo das listas, o que lhe demandou certa ingenuidade algébrica:
```
List x = 1 + x * List x
List x - x * List x = 1
List x * (1 - x) = 1
List x = 1 / (1 - x)
d/dx List x = d/dx 1 / (1 - x)
d/dx List x = 1 / (1 - x)²
d/dx List x = 1 / (1 - x) * 1 / (1 - x)
d/dx List x = List x * List x
data DeltaList x = Split (DeltaList x) (DeltaList x)
```
Isso nos indica que a derivada do tipo lista é nada mais do que duas listas. E isso também faz sentido, pois, para focar em um ponto de uma lista, precisamos de duas listas: uma com os elementos à esquerda do foco, e outra com os elementos à direita. Por exemplo, se criamos uma lista de 5 elementos, podemos focar no elemento do meio como: `[1, 2, *, 4, 5]`, o que pode ser representado pelo tipo `DeltaList` como `Split [1, 2] [4, 5]`.
Infelizmente, a verdade sobre a interligação entre tipos e equações algébricas foi poderosa demais até para o nosso bravo alquimista, que logo perdeu a sanidade e sumiu do mapa. Seu paradeiro, até hoje, é desconhecido, mas reza a lenda que ele ainda está entre nós, vagando por algum vilarejo pacato, comendo bananas radioativas e tentando derivar o tipo das monadas.