mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 08:09:22 +03:00
Litereum massive simplification DONE
This commit is contained in:
parent
a8f88e7080
commit
df6dd3965d
2
base/List/zipped_with.kind
Normal file
2
base/List/zipped_with.kind
Normal file
@ -0,0 +1,2 @@
|
||||
List.zipped_with<A:Type,B:Type>(as: List<A>, bs: List<B>)<C:Type>(f: A -> B -> C): List<C>
|
||||
List.zip_with<A,B,C>(f,as,bs)
|
@ -1,803 +0,0 @@
|
||||
// Litereum: a minimal decentralized computer
|
||||
// ==========================================
|
||||
|
||||
// TODO:
|
||||
// - cost measure Almost there
|
||||
// - Litereum.Term.get_caller ?
|
||||
// - block difficulty (nakamoto consensus)
|
||||
// - Lit.Lang:
|
||||
// - consertar parser para ir ate o final do arquivo !
|
||||
// - paper:
|
||||
// - use railroad diagrams for syntax
|
||||
|
||||
// Types
|
||||
// -----
|
||||
|
||||
// A Litereum term
|
||||
type Litereum.Term {
|
||||
// A variable
|
||||
var(
|
||||
name: String
|
||||
)
|
||||
// Binds a variable
|
||||
let(
|
||||
name: String
|
||||
type: Litereum.Type
|
||||
expr: Litereum.Term
|
||||
body: Litereum.Term
|
||||
)
|
||||
// Creates a value
|
||||
create(
|
||||
data: String
|
||||
ctor: Nat
|
||||
vals: List<Litereum.Term>
|
||||
)
|
||||
// Pattern-matches a value
|
||||
match(
|
||||
name: String
|
||||
expr: Litereum.Term
|
||||
cses: List<Litereum.Term>
|
||||
)
|
||||
// Creates a new 64-bit word
|
||||
word(
|
||||
numb: U64
|
||||
)
|
||||
// Compares two words
|
||||
compare(
|
||||
val0: Litereum.Term
|
||||
val1: Litereum.Term
|
||||
iflt: Litereum.Term
|
||||
ifeq: Litereum.Term
|
||||
ifgt: Litereum.Term
|
||||
)
|
||||
// Binary operation on words
|
||||
operate(
|
||||
oper: Litereum.Operation
|
||||
val0: Litereum.Term
|
||||
val1: Litereum.Term
|
||||
)
|
||||
// Call external function
|
||||
call(
|
||||
bond: String
|
||||
args: List<Litereum.Term>
|
||||
)
|
||||
}
|
||||
|
||||
// A binary operation on words
|
||||
type Litereum.Operation {
|
||||
add sub mul div mod or and xor
|
||||
}
|
||||
|
||||
// A type reference
|
||||
type Litereum.Type {
|
||||
word
|
||||
data(name: String)
|
||||
}
|
||||
|
||||
// A global algebraic datatype (ADT) declaration
|
||||
type Litereum.Data {
|
||||
new(
|
||||
name: String
|
||||
constructors: List<Litereum.Constructor>
|
||||
)
|
||||
}
|
||||
|
||||
// An ADT's constructor
|
||||
type Litereum.Constructor {
|
||||
new(
|
||||
name: String
|
||||
field_names: List<String>
|
||||
field_types: List<Litereum.Type>
|
||||
)
|
||||
}
|
||||
|
||||
// A global smart-contract
|
||||
type Litereum.Bond {
|
||||
new(
|
||||
name: String
|
||||
owners: List<String>
|
||||
main: Litereum.Term
|
||||
input_names: List<String>
|
||||
input_types: List<Litereum.Type>
|
||||
output_type: Litereum.Type
|
||||
)
|
||||
}
|
||||
|
||||
// A global entry
|
||||
type Litereum.Entry {
|
||||
data(value: Litereum.Data)
|
||||
bond(value: Litereum.Bond)
|
||||
}
|
||||
|
||||
// A Litereum transaction
|
||||
type Litereum.Transaction {
|
||||
new_name(name: String)
|
||||
new_data(data: Litereum.Data)
|
||||
new_bond(bond: Litereum.Bond)
|
||||
run_term(term: Litereum.Term)
|
||||
}
|
||||
|
||||
type Litereum.World {
|
||||
new(
|
||||
name_count: Nat
|
||||
name_to_index: Map<Nat>
|
||||
index_to_name: Map<String>
|
||||
entry: Map<Litereum.Entry>
|
||||
)
|
||||
}
|
||||
|
||||
// Utils
|
||||
// -----
|
||||
|
||||
Litereum.World.get_data(world: Litereum.World, name: String): Maybe<Litereum.Data>
|
||||
open world
|
||||
Maybe {
|
||||
get entry = world.entry{name}
|
||||
case entry {
|
||||
type: some(entry.value)
|
||||
} default none
|
||||
}
|
||||
|
||||
Litereum.World.get_bond(world: Litereum.World, name: String): Maybe<Litereum.Bond>
|
||||
open world
|
||||
Maybe {
|
||||
get entry = world.entry{name}
|
||||
case entry {
|
||||
bond: some(entry.value)
|
||||
} default none
|
||||
}
|
||||
|
||||
Litereum.get_constructor_by_name(data: Litereum.Data, name: String): Maybe<Pair<Nat,Litereum.Constructor>>
|
||||
case data {
|
||||
new: List.ifind!((i,f) String.eql(f@name,name), data.constructors)
|
||||
}
|
||||
|
||||
Litereum.extend<A: Type>(
|
||||
map: Map<A>
|
||||
keys: List<String>
|
||||
vals: List<A>
|
||||
): Map<A>
|
||||
case keys vals {
|
||||
cons cons: Litereum.extend<A>(map{keys.head} <- vals.head, keys.tail, vals.tail)
|
||||
} default map
|
||||
|
||||
// Type-Checking
|
||||
// -------------
|
||||
|
||||
Litereum.Type.equal(a: Litereum.Type, b: Litereum.Type): Bool
|
||||
case a b {
|
||||
word word: true
|
||||
data data: String.eql(a.name, b.name)
|
||||
} default false
|
||||
|
||||
Litereum.Type.check(
|
||||
context: Map<Litereum.Type>
|
||||
world: Litereum.World
|
||||
term: Litereum.Term
|
||||
type: Litereum.Type
|
||||
): Bool
|
||||
open context
|
||||
// log("- chk: " | Lit.Lang.show.term(term, context@world) | " : " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
// log("- ctx: " | String.join(", ", List.map!!((a) a@fst|":"|Lit.Lang.show.type.short(a@snd), Map.to_list!(variables)))) // DEBUG
|
||||
// log("") // DEBUG
|
||||
case term {
|
||||
var:
|
||||
let var_type = context{term.name} abort false
|
||||
////log("-- var " | term.name | " " | Lit.Lang.show.type.short(var_type) | " " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
Litereum.Type.equal(var_type, type)
|
||||
let:
|
||||
//log("-- let ") // DEBUG
|
||||
let expr = Litereum.Type.check(context, world, term.expr, term.type)
|
||||
let ctx2 = context{term.name} <- term.type
|
||||
let cont = Litereum.Type.check(ctx2, world, term.body, type)
|
||||
expr && cont
|
||||
create:
|
||||
use data = Litereum.World.get_data(world, term.data) abort false
|
||||
use ctor = data.constructors[term.ctor] abort false
|
||||
let size = Nat.eql(List.length!(term.vals), List.length!(ctor.field_types))
|
||||
let vals = List.zip!!(term.vals, ctor.field_types)
|
||||
let vals = List.all!((x) Litereum.Type.check(context, world, x@fst, x@snd), vals)
|
||||
size && vals
|
||||
match:
|
||||
let type = context{term.name} abort false
|
||||
case type {
|
||||
data:
|
||||
use data = Litereum.World.get_data(world, type.name) abort false
|
||||
let expr = Litereum.Type.check(context, world, term.expr, type)
|
||||
let size = Nat.eql(List.length!(term.cses),List.length!(data.constructors))
|
||||
let cses = List.zipped_with!!(term.cses, data.constructors)!((case_body, case_ctor)
|
||||
let nams = List.map!!(String.concat(type.name|"."), case_ctor@field_names)
|
||||
let typs = case_ctor@field_types
|
||||
let ctx2 = Litereum.extend!(context, nams, typs)
|
||||
Litereum.Type.check(ctx2, world, case_body, type))
|
||||
expr && size && List.and(cses)
|
||||
} default false
|
||||
word: case type {
|
||||
word: true
|
||||
} default false
|
||||
compare:
|
||||
//log("-- compare ") // DEBUG
|
||||
let val0 = Litereum.Type.check(context, world, term.val0, Litereum.Type.word)
|
||||
let val1 = Litereum.Type.check(context, world, term.val0, Litereum.Type.word)
|
||||
let iflt = Litereum.Type.check(context, world, term.iflt, type)
|
||||
let ifeq = Litereum.Type.check(context, world, term.ifeq, type)
|
||||
let ifgt = Litereum.Type.check(context, world, term.ifgt, type)
|
||||
val0 && val1 && iflt && ifeq && ifgt
|
||||
operate:
|
||||
let val0 = Litereum.Type.check(context, world, term.val0, Litereum.Type.word)
|
||||
let val1 = Litereum.Type.check(context, world, term.val1, Litereum.Type.word)
|
||||
val0 && val1
|
||||
call:
|
||||
//log("-- call ") // DEBUG
|
||||
//let ownr = Litereum.World.check.owner(context, term.func)
|
||||
use bond = Litereum.World.get_bond(world, term.bond) abort false
|
||||
let otyp = Litereum.Type.equal(bond.output_type, type)
|
||||
let args = List.zip!!(term.args, bond.input_types)
|
||||
let args = List.all!((x) Litereum.Type.check(context, world, x@fst, x@snd), args)
|
||||
otyp && args
|
||||
} default false
|
||||
|
||||
// Evaluation
|
||||
// ----------
|
||||
|
||||
Litereum.Term.eval(
|
||||
subst: Map<Litereum.Term>
|
||||
world: Litereum.World
|
||||
term: Litereum.Term
|
||||
gas: Nat
|
||||
): Triple<Nat, Litereum.World, Litereum.Term>
|
||||
// log("- run " | Lit.Lang.show.term(term,world)) // DEBUG
|
||||
// log("- var " | String.join(", ", List.map!!((x) x@fst|":"|Lit.Lang.show.term(x@snd,world), Map.to_list!(vars)))) // DEBUG
|
||||
// log("")
|
||||
case term {
|
||||
var:
|
||||
{gas, world, subst{term.name} <> term}
|
||||
create:
|
||||
let {gas, world, vals} = Litereum.Term.eval.many(subst, world, term.vals, gas)
|
||||
{gas, world, Litereum.Term.create(term.data, term.ctor, vals)}
|
||||
match:
|
||||
let {gas, world, expr} = Litereum.Term.eval(subst, world, term.expr, gas)
|
||||
case expr {
|
||||
create:
|
||||
use data = Litereum.World.get_data(world,expr.data) abort {gas, world, term}
|
||||
use ctor = data.constructors[expr.ctor] abort {gas, world, term}
|
||||
let body = term.cses[expr.ctor] abort {gas, world, term}
|
||||
let nams = List.map!!(String.concat(data.name|"."), ctor@field_names)
|
||||
let subst = Litereum.extend!(subst, nams, expr.vals)
|
||||
Litereum.Term.eval(subst, world, body, gas)
|
||||
} default {gas, world, term}
|
||||
word:
|
||||
{gas, world, term}
|
||||
compare:
|
||||
let {gas, world, val0} = Litereum.Term.eval(subst, world, term.val0, gas)
|
||||
let {gas, world, val1} = Litereum.Term.eval(subst, world, term.val1, gas)
|
||||
case val0 val1 {
|
||||
word word: case U64.cmp(val0.numb, val0.numb) {
|
||||
ltn: Litereum.Term.eval(subst, world, term.iflt, gas)
|
||||
eql: Litereum.Term.eval(subst, world, term.ifeq, gas)
|
||||
gtn: Litereum.Term.eval(subst, world, term.ifgt, gas)
|
||||
}
|
||||
} default {gas, world, term}
|
||||
operate:
|
||||
let {gas, world, val0} = Litereum.Term.eval(subst, world, term.val0, gas)
|
||||
let {gas, world, val1} = Litereum.Term.eval(subst, world, term.val1, gas)
|
||||
case val0 val1 {
|
||||
word word: case term.oper {
|
||||
add: {gas, world, Litereum.Term.word(U64.add(val0.numb,val1.numb))}
|
||||
sub: {gas, world, Litereum.Term.word(U64.sub(val0.numb,val1.numb))}
|
||||
mul: {gas, world, Litereum.Term.word(U64.mul(val0.numb,val1.numb))}
|
||||
div: {gas, world, Litereum.Term.word(U64.div(val0.numb,val1.numb))}
|
||||
mod: {gas, world, Litereum.Term.word(U64.mod(val0.numb,val1.numb))}
|
||||
or: {gas, world, Litereum.Term.word(U64.or( val0.numb,val1.numb))}
|
||||
and: {gas, world, Litereum.Term.word(U64.and(val0.numb,val1.numb))}
|
||||
xor: {gas, world, Litereum.Term.word(U64.xor(val0.numb,val1.numb))}
|
||||
}
|
||||
} default {gas, world, term}
|
||||
let:
|
||||
let {gas, world, expr} = Litereum.Term.eval(subst, world, term.expr, gas)
|
||||
let {gas, world, body} = Litereum.Term.eval(subst{term.name} <- expr, world, term.body, gas)
|
||||
{gas, world, body}
|
||||
call:
|
||||
use bond = Litereum.World.get_bond(world, term.bond) abort {gas, world, term}
|
||||
let {gas, world, args} = Litereum.Term.eval.many(subst, world, term.args, gas)
|
||||
let {gas, world, main} = Litereum.Term.eval(Litereum.extend!(subst, bond.input_names, args), world, bond.main, gas)
|
||||
{gas, world, main}
|
||||
} default {gas, world, term}
|
||||
|
||||
Litereum.Term.eval.many(
|
||||
subst: Map<Litereum.Term>
|
||||
world: Litereum.World
|
||||
vals: List<Litereum.Term>
|
||||
gas: Nat
|
||||
): Triple<Nat, Litereum.World, List<Litereum.Term>>
|
||||
case vals {
|
||||
nil:
|
||||
{gas, world, []}
|
||||
cons:
|
||||
let {gas, world, head} = Litereum.Term.eval(subst, world, vals.head, gas)
|
||||
let {gas, world, tail} = Litereum.Term.eval.many(subst, world, vals.tail, gas)
|
||||
{gas, world, head & tail}
|
||||
}
|
||||
|
||||
// Transaction
|
||||
// -----------
|
||||
|
||||
Litereum.Transaction.run(
|
||||
transaction: Litereum.Transaction
|
||||
world: Litereum.World
|
||||
): Maybe<Litereum.World>
|
||||
open world
|
||||
case transaction {
|
||||
new_name:
|
||||
let world = world@name_count <- world.name_count + 1
|
||||
let world = world@name_to_index <- (world.name_to_index{transaction.name} <- world.name_count)
|
||||
let world = world@index_to_name <- (world.index_to_name{Nat.show(world.name_count)} <- transaction.name)
|
||||
let world = world@names <- names
|
||||
some(world)
|
||||
new_data:
|
||||
use data = transaction.data
|
||||
case world.entry{data.name} as got_type {
|
||||
none:
|
||||
some(world@entry <- (world.entry{data.name} <- Litereum.Entry.data(data)))
|
||||
} default
|
||||
log("error: data redefinition: " | data.name)
|
||||
none
|
||||
new_bond:
|
||||
use bond = transaction.bond
|
||||
log("- new_bond: " | bond.name)
|
||||
case world.entry{bond.name} as got {
|
||||
none:
|
||||
let world = world@entry <- (world.entry{bond.name} <- Litereum.Entry.bond(bond))
|
||||
let context = Litereum.extend<Litereum.Type>({}, bond.input_names, bond.input_types)
|
||||
if Litereum.Type.check(context, world, bond.main, bond.output_type) then
|
||||
some(world)
|
||||
else
|
||||
log("error: ill-typed bond: " | bond.name)
|
||||
none
|
||||
} default
|
||||
log("error: bond redefinition: " | bond.name)
|
||||
none
|
||||
run_term:
|
||||
if Litereum.Type.check({}, world, transaction.term, Litereum.Type.word) then
|
||||
let {gas, world, term} = Litereum.Term.eval({}, world, transaction.term, 0)
|
||||
some(world)
|
||||
else
|
||||
log("error: ill-typed run term")
|
||||
none
|
||||
}
|
||||
|
||||
Litereum.Transaction.run.many(
|
||||
transactions: List<Litereum.Transaction>
|
||||
world: Litereum.World
|
||||
): Maybe<Litereum.World>
|
||||
case transactions {
|
||||
nil: some(world)
|
||||
cons: case Litereum.Transaction.run(transactions.head, world) as result {
|
||||
none: none
|
||||
some: Litereum.Transaction.run.many(transactions.tail, result.value)
|
||||
}
|
||||
}
|
||||
|
||||
// Serialization
|
||||
// -------------
|
||||
|
||||
Litereum.serialize.varlen(value: Nat): Bits
|
||||
Litereum.serialize.varlen.go(Nat.add(value,1))
|
||||
|
||||
Litereum.deserialize.varlen(bits: Bits): Pair<Bits,Nat>
|
||||
let {bits,value} = Litereum.deserialize.varlen.go(bits)
|
||||
{bits, Nat.sub(value,1)}
|
||||
|
||||
Litereum.serialize.varlen.go(value: Nat): Bits
|
||||
if Nat.eql(value,1) then
|
||||
Bits.o(Bits.e)
|
||||
else if Nat.eql(Nat.mod(value,2),0)
|
||||
then Bits.i(Bits.o(Litereum.serialize.varlen.go(Nat.div(value,2))))
|
||||
else Bits.i(Bits.i(Litereum.serialize.varlen.go(Nat.div(value,2))))
|
||||
|
||||
Litereum.deserialize.varlen.go(bits: Bits): Pair<Bits,Nat>
|
||||
case bits {
|
||||
e: {Bits.e, 0}
|
||||
o: {bits.pred, 0}
|
||||
i: case bits.pred {
|
||||
e: {bits.pred, 0}
|
||||
o:
|
||||
let {bits,x} = Litereum.deserialize.varlen.go(bits.pred.pred)
|
||||
{bits, Nat.mul(x,2)}
|
||||
i:
|
||||
let {bits,x} = Litereum.deserialize.varlen.go(bits.pred.pred)
|
||||
{bits, Nat.add(Nat.mul(x,2),1)}
|
||||
}
|
||||
}
|
||||
|
||||
Litereum.serialize.fixlen(size: Nat, value: Nat): Bits
|
||||
case size {
|
||||
zero: Bits.e
|
||||
succ: if Nat.eql(Nat.mod(value,2),0)
|
||||
then Bits.o(Litereum.serialize.fixlen(size.pred, Nat.div(value,2)))
|
||||
else Bits.i(Litereum.serialize.fixlen(size.pred, Nat.div(value,2)))
|
||||
}
|
||||
|
||||
Litereum.deserialize.fixlen(size: Nat, bits: Bits): Pair<Bits,Nat>
|
||||
case size {
|
||||
zero: {bits, 0}
|
||||
succ: case bits {
|
||||
e: {Bits.e, 0}
|
||||
o:
|
||||
let {bits,x} = Litereum.deserialize.fixlen(size.pred, bits.pred)
|
||||
{bits, Nat.mul(x,2)}
|
||||
i:
|
||||
let {bits,x} = Litereum.deserialize.fixlen(size.pred, bits.pred)
|
||||
{bits, Nat.add(Nat.mul(x,2),1)}
|
||||
}
|
||||
}
|
||||
|
||||
Litereum.serialize.list<A: Type>(item: A -> Bits, list: List<A>): Bits
|
||||
case list {
|
||||
nil: Bits.o(Bits.e)
|
||||
cons: Bits.i(Bits.concat(item(list.head), Litereum.serialize.list<A>(item, list.tail)))
|
||||
}
|
||||
|
||||
Litereum.deserialize.list<A: Type>(item: Bits -> Pair<Bits,A>, bits: Bits): Pair<Bits,List<A>>
|
||||
case bits {
|
||||
e: {Bits.e, []}
|
||||
o: {bits.pred, []}
|
||||
i:
|
||||
let {bits, head} = item(bits.pred)
|
||||
let {bits, tail} = Litereum.deserialize.list<A>(item, bits)
|
||||
{bits, head & tail}
|
||||
}
|
||||
|
||||
Litereum.serialize.name.new(name: String): Bits
|
||||
case name {
|
||||
nil:
|
||||
Bits.e
|
||||
cons:
|
||||
let numb =
|
||||
if U16.btw('0', name.head, '9') then
|
||||
U16.sub(name.head, '0')
|
||||
else if U16.btw('A', name.head, 'Z') then
|
||||
U16.add(U16.sub(name.head, 'A'), 10#16)
|
||||
else if U16.btw('a', name.head, 'z') then
|
||||
U16.add(U16.sub(name.head, 'a'), 36#16)
|
||||
else if U16.btw('_', name.head, '_') then
|
||||
62#16
|
||||
else
|
||||
63#16
|
||||
let head = Litereum.serialize.fixlen(6, U16.to_nat(numb))
|
||||
let tail = Litereum.serialize.name.new(name.tail)
|
||||
Bits.concat(head, tail)
|
||||
}
|
||||
|
||||
Litereum.deserialize.name.new(bits: Bits): Pair<Bits,String>
|
||||
let {bits, numb} = Litereum.deserialize.fixlen(6, bits)
|
||||
let {bits, tail} = Litereum.deserialize.name.new(bits)
|
||||
let numb = Nat.to_u16(numb)
|
||||
let head =
|
||||
if U16.btw( 0, numb, 9) then
|
||||
U16.add(numb, '0')
|
||||
else if U16.btw(10, numb, 35) then
|
||||
U16.add(U16.sub(numb,10#16), 'A')
|
||||
else if U16.btw(36, numb, 61) then
|
||||
U16.add(U16.sub(numb,36#16), 'a')
|
||||
else if U16.btw(62, numb, 62) then
|
||||
'_'
|
||||
else
|
||||
'.'
|
||||
{bits, String.cons(head,tail)}
|
||||
|
||||
Litereum.serialize.name.old(world: Litereum.World, name: String): Bits
|
||||
open world
|
||||
let value = world.name_to_index{name} abort Bits.e
|
||||
let bits = Litereum.serialize.varlen(value)
|
||||
bits
|
||||
|
||||
Litereum.deserialize.name.old(world: Litereum.World, bits: Bits): Pair<Bits,String>
|
||||
open world
|
||||
let {bits, value} = Litereum.deserialize.varlen(bits)
|
||||
let text = world.index_to_name{Nat.show(value)} abort {bits, ""}
|
||||
{bits, text}
|
||||
|
||||
Litereum.serialize.term(world: Litereum.World, term: Litereum.Term): Bits
|
||||
case term {
|
||||
var:
|
||||
Bits.o(Bits.o(Bits.o(Litereum.serialize.name.old(world,term.name))))
|
||||
let:
|
||||
let name = Litereum.serialize.name.old(world,term.name)
|
||||
let type = Litereum.serialize.type(world,term.type) // TODO
|
||||
let expr = Litereum.serialize.term(world,term.expr)
|
||||
let body = Litereum.serialize.term(world,term.body)
|
||||
Bits.i(Bits.o(Bits.o(Bits.concat(name, Bits.concat(type, Bits.concat(expr, body))))))
|
||||
create:
|
||||
let data = Litereum.serialize.name.old(world,term.data)
|
||||
let ctor = Litereum.serialize.varlen(term.ctor)
|
||||
let vals = Litereum.serialize.list!(Litereum.serialize.term(world), term.vals)
|
||||
Bits.o(Bits.i(Bits.o(Bits.concat(data, Bits.concat(ctor, vals)))))
|
||||
match:
|
||||
let name = Litereum.serialize.name.old(world,term.name)
|
||||
let expr = Litereum.serialize.term(world,term.expr)
|
||||
let cses = Litereum.serialize.list!(Litereum.serialize.term(world), term.cses)
|
||||
Bits.i(Bits.i(Bits.o(Bits.concat(name, Bits.concat(expr, cses)))))
|
||||
word:
|
||||
let numb = Litereum.serialize.fixlen(64, U64.to_nat(term.numb))
|
||||
Bits.o(Bits.o(Bits.i(numb)))
|
||||
compare:
|
||||
let val0 = Litereum.serialize.term(world,term.val0)
|
||||
let val1 = Litereum.serialize.term(world,term.val1)
|
||||
let iflt = Litereum.serialize.term(world,term.iflt)
|
||||
let ifeq = Litereum.serialize.term(world,term.ifeq)
|
||||
let ifgt = Litereum.serialize.term(world,term.ifgt)
|
||||
Bits.i(Bits.o(Bits.i(Bits.concat(val0, Bits.concat(val1, Bits.concat(iflt, Bits.concat(ifeq, ifgt)))))))
|
||||
operate:
|
||||
let oper = Litereum.serialize.fixlen(3, case term.oper { add:0, sub:1, mul:2, div:3, mod:4, or:5, and:6, xor:7 })
|
||||
let val0 = Litereum.serialize.term(world,term.val0)
|
||||
let val1 = Litereum.serialize.term(world,term.val1)
|
||||
Bits.o(Bits.i(Bits.i(Bits.concat(oper, Bits.concat(val0, val1)))))
|
||||
call:
|
||||
let bond = Litereum.serialize.name.old(world,term.bond)
|
||||
let args = Litereum.serialize.list!(Litereum.serialize.term(world), term.args)
|
||||
Bits.i(Bits.i(Bits.i(Bits.concat(bond, args))))
|
||||
} default _
|
||||
|
||||
Litereum.deserialize.term(world: Litereum.World, bits: Bits): Pair<Bits,Litereum.Term>
|
||||
let {bits,ctor} = Litereum.deserialize.fixlen(3, bits)
|
||||
switch Nat.eql(ctor) {
|
||||
0:
|
||||
let {bits,name} = Litereum.deserialize.name.old(world, bits)
|
||||
{bits, Litereum.Term.var(name)}
|
||||
1:
|
||||
let {bits,name} = Litereum.deserialize.name.old(world,bits)
|
||||
let {bits,type} = Litereum.deserialize.type(world,bits)
|
||||
let {bits,expr} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,body} = Litereum.deserialize.term(world,bits)
|
||||
{bits, Litereum.Term.let(name,type,expr,body)}
|
||||
2:
|
||||
let {bits,data} = Litereum.deserialize.name.old(world,bits)
|
||||
let {bits,ctor} = Litereum.deserialize.varlen(bits)
|
||||
let {bits,vals} = Litereum.deserialize.list!(Litereum.deserialize.term(world), bits)
|
||||
{bits, Litereum.Term.create(data, ctor, vals)}
|
||||
3:
|
||||
let {bits,name} = Litereum.deserialize.name.old(world,bits)
|
||||
let {bits,expr} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,cses} = Litereum.deserialize.list!(Litereum.deserialize.term(world), bits)
|
||||
{bits, Litereum.Term.match(name,expr,cses)}
|
||||
4:
|
||||
let {bits,numb} = Litereum.deserialize.fixlen(64,bits)
|
||||
{bits, Litereum.Term.word(Nat.to_u64(numb))}
|
||||
5:
|
||||
let {bits,val0} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,val1} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,iflt} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,ifeq} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,ifgt} = Litereum.deserialize.term(world,bits)
|
||||
{bits, Litereum.Term.compare(val0,val1,iflt,ifeq,ifgt)}
|
||||
6:
|
||||
let {bits,oper} = Litereum.deserialize.fixlen(3, bits)
|
||||
let {bits,val0} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,val1} = Litereum.deserialize.term(world,bits)
|
||||
let oper = switch Nat.eql(oper) {
|
||||
0: Litereum.Operation.add
|
||||
1: Litereum.Operation.sub
|
||||
2: Litereum.Operation.mul
|
||||
3: Litereum.Operation.div
|
||||
4: Litereum.Operation.mod
|
||||
5: Litereum.Operation.or
|
||||
6: Litereum.Operation.and
|
||||
7: Litereum.Operation.xor
|
||||
} default Litereum.Operation.add
|
||||
{bits, Litereum.Term.operate(oper,val0,val1)}
|
||||
7:
|
||||
let {bits,bond} = Litereum.deserialize.name.old(world,bits)
|
||||
let {bits,args} = Litereum.deserialize.list!(Litereum.deserialize.term(world), bits)
|
||||
{bits, Litereum.Term.call(bond,args)}
|
||||
} default {bits, Litereum.Term.word(0)}
|
||||
|
||||
Litereum.serialize.type(world: Litereum.World, typ: Litereum.Type): Bits
|
||||
case typ {
|
||||
word: Bits.o(Bits.e)
|
||||
data: Bits.i(Litereum.serialize.name.old(world,typ.name))
|
||||
}
|
||||
|
||||
Litereum.deserialize.type(world: Litereum.World, bits: Bits): Pair<Bits,Litereum.Type>
|
||||
case bits {
|
||||
o:
|
||||
{bits.pred, Litereum.Type.word}
|
||||
i:
|
||||
let {bits,name} = Litereum.deserialize.name.old(world, bits.pred)
|
||||
{bits, Litereum.Type.data(name)}
|
||||
} default {bits, Litereum.Type.word}
|
||||
|
||||
Litereum.serialize.data(world: Litereum.World, data: Litereum.Data): Bits
|
||||
open data
|
||||
let name = Litereum.serialize.name.old(world, data.name)
|
||||
let ctrs = Litereum.serialize.list!(Litereum.serialize.constructor(world), data.constructors)
|
||||
Bits.concat(name, ctrs)
|
||||
|
||||
Litereum.deserialize.data(world: Litereum.World, bits: Bits): Pair<Bits, Litereum.Data>
|
||||
let {bits,name} = Litereum.deserialize.name.old(world, bits)
|
||||
let {bits,ctrs} = Litereum.deserialize.list!(Litereum.deserialize.constructor(world), bits)
|
||||
{bits, Litereum.Data.new(name,ctrs)}
|
||||
|
||||
Litereum.serialize.constructor(world: Litereum.World, ctor: Litereum.Constructor): Bits
|
||||
open ctor
|
||||
let name = Litereum.serialize.name.old(world,ctor.name)
|
||||
let nams = Litereum.serialize.list!(Litereum.serialize.name.old(world), ctor.field_names)
|
||||
let typs = Litereum.serialize.list!(Litereum.serialize.type(world), ctor.field_types)
|
||||
Bits.concat(name, Bits.concat(nams, typs))
|
||||
|
||||
Litereum.deserialize.constructor(world: Litereum.World, bits: Bits): Pair<Bits,Litereum.Constructor>
|
||||
let {bits,name} = Litereum.deserialize.name.old(world,bits)
|
||||
let {bits,nams} = Litereum.deserialize.list!(Litereum.deserialize.name.old(world), bits)
|
||||
let {bits,typs} = Litereum.deserialize.list!(Litereum.deserialize.type(world), bits)
|
||||
{bits, Litereum.Constructor.new(name, nams, typs)}
|
||||
|
||||
Litereum.serialize.bond(world: Litereum.World, bond: Litereum.Bond): Bits
|
||||
open bond
|
||||
let name = Litereum.serialize.name.old(world, bond.name)
|
||||
let owners = Litereum.serialize.list!(Litereum.serialize.name.old(world), bond.owners)
|
||||
let main = Litereum.serialize.term(world, bond.main)
|
||||
let input_names = Litereum.serialize.list!(Litereum.serialize.name.old(world), bond.input_names)
|
||||
let input_types = Litereum.serialize.list!(Litereum.serialize.type(world), bond.input_types)
|
||||
let output_type = Litereum.serialize.type(world, bond.output_type)
|
||||
Bits.concat(name, Bits.concat(owners, Bits.concat(main, Bits.concat(input_names, Bits.concat(input_types, output_type)))))
|
||||
|
||||
Litereum.deserialize.bond(world: Litereum.World, bits: Bits): Pair<Bits,Litereum.Bond>
|
||||
let {bits,name} = Litereum.deserialize.name.old(world,bits)
|
||||
let {bits,owners} = Litereum.deserialize.list!(Litereum.deserialize.name.old(world), bits)
|
||||
let {bits,main} = Litereum.deserialize.term(world,bits)
|
||||
let {bits,input_names} = Litereum.deserialize.list!(Litereum.deserialize.name.old(world), bits)
|
||||
let {bits,input_types} = Litereum.deserialize.list!(Litereum.deserialize.type(world), bits)
|
||||
let {bits,output_type} = Litereum.deserialize.type(world, bits)
|
||||
{bits, Litereum.Bond.new(name, owners, main, input_names, input_types, output_type)}
|
||||
|
||||
Litereum.serialize.entry(world: Litereum.World, entry: Litereum.Entry): Bits
|
||||
case entry {
|
||||
data: Bits.o(Litereum.serialize.data(world,entry.value))
|
||||
bond: Bits.i(Litereum.serialize.bond(world,entry.value))
|
||||
}
|
||||
|
||||
Litereum.deserialize.entry(world: Litereum.World, bits: Bits): Pair<Bits,Litereum.Entry>
|
||||
case bits {
|
||||
o:
|
||||
let {bits,data} = Litereum.deserialize.data(world,bits.pred)
|
||||
{bits, Litereum.Entry.data(data)}
|
||||
i:
|
||||
let {bits,bond} = Litereum.deserialize.bond(world,bits.pred)
|
||||
{bits, Litereum.Entry.bond(bond)}
|
||||
} default {bits, Litereum.Entry.data(Litereum.Data.new("",[]))}
|
||||
|
||||
Litereum.serialize.transaction(world: Litereum.World, transaction: Litereum.Transaction): Bits
|
||||
case transaction {
|
||||
new_name:
|
||||
let name = Litereum.serialize.name.old(world, transaction.name)
|
||||
Bits.o(Bits.o(name))
|
||||
new_data:
|
||||
let data = Litereum.serialize.data(world, transaction.data)
|
||||
Bits.i(Bits.o(data))
|
||||
new_bond:
|
||||
let bond = Litereum.serialize.bond(world, transaction.bond)
|
||||
Bits.o(Bits.i(bond))
|
||||
run_term:
|
||||
let term = Litereum.serialize.term(world, transaction.term)
|
||||
Bits.i(Bits.i(term))
|
||||
}
|
||||
|
||||
Litereum.deserialize.transaction(world: Litereum.World, bits: Bits): Pair<Bits,Litereum.Transaction>
|
||||
let {bits,ctor} = Litereum.deserialize.fixlen(2, bits)
|
||||
switch Nat.eql(ctor) {
|
||||
0:
|
||||
let {bits,name} = Litereum.deserialize.name.old(world, bits)
|
||||
{bits, Litereum.Transaction.new_name(name)}
|
||||
1:
|
||||
let {bits,data} = Litereum.deserialize.data(world, bits)
|
||||
{bits, Litereum.Transaction.new_data(data)}
|
||||
2:
|
||||
let {bits,bond} = Litereum.deserialize.bond(world, bits)
|
||||
{bits, Litereum.Transaction.new_bond(bond)}
|
||||
3:
|
||||
let {bits,term} = Litereum.deserialize.term(world, bits)
|
||||
{bits, Litereum.Transaction.run_term(term)}
|
||||
} default {bits, Litereum.Transaction.new_name("")}
|
||||
|
||||
////// Tests
|
||||
////// -----
|
||||
|
||||
////// Litereum: _
|
||||
////// let world = {}
|
||||
|
||||
////// let code = ""
|
||||
|
||||
////// let code = code |
|
||||
////// Litereum.Lang.Type
|
||||
////// | Litereum.Lang.Cmp
|
||||
////// | Litereum.Lang.Nat
|
||||
////// | Litereum.Lang.Bits
|
||||
////// | Litereum.Lang.BitsMap
|
||||
////// | Litereum.Lang.Voting
|
||||
////// //| Litereum.Lang.Test
|
||||
|
||||
////// // let code = code |
|
||||
////// // `
|
||||
////// // GiveUnit(): Unit
|
||||
////// // Unit/new
|
||||
////// //
|
||||
////// // TakeUnit(x: Unit): U64
|
||||
////// // 42
|
||||
////// //
|
||||
////// // do {
|
||||
////// // call a1 = GiveUnit()
|
||||
////// // call a2 = GiveUnit()
|
||||
////// // call b = TakeUnit(a1)
|
||||
////// // call c = TakeUnit(a2)
|
||||
////// // (+ b c)
|
||||
////// // }
|
||||
////// // `
|
||||
|
||||
////// let code = code |
|
||||
////// `
|
||||
////// // type Litereum.Costs {
|
||||
////// // new(
|
||||
////// // var: Nat
|
||||
////// // create: Nat
|
||||
////// // match: Nat
|
||||
////// // match_assignment: Nat
|
||||
////// // word: Nat
|
||||
////// // compare: Nat
|
||||
////// // operate: Nat
|
||||
////// // call: Nat
|
||||
////// // bind: Nat
|
||||
////// // )
|
||||
////// // }
|
||||
|
||||
////// candidates(): Candidates
|
||||
////// Candidates/cons{
|
||||
////// count: Nat/zero, tail: Candidates/cons{
|
||||
////// count: Nat/zero, tail: Candidates/cons{
|
||||
////// count: Nat/zero, tail: Candidates/nil }}}
|
||||
|
||||
////// key1(): Bits
|
||||
////// Bits/o{pred: Bits/e}
|
||||
|
||||
////// key2(): Bits
|
||||
////// Bits/i{pred: Bits/e}
|
||||
|
||||
////// do {
|
||||
////// call cand = candidates()
|
||||
////// call joao = key1()
|
||||
////// call maria = key2()
|
||||
|
||||
////// call m = VotingMap.add(VotingMap/new, joao)
|
||||
////// call new_m = VotingMap.add(m, maria)
|
||||
|
||||
////// call new_m = VotingMap.allow_vote(new_m, joao)
|
||||
////// call new_m = VotingMap.allow_vote(new_m, maria)
|
||||
|
||||
////// call result = VotingMap.vote(new_m, joao, Nat/succ{pred: Nat/zero}, cand)
|
||||
////// case result : VoteResult {
|
||||
////// new:
|
||||
////// call new_result = VotingMap.vote(result.map, maria, Nat/zero, result.candidates)
|
||||
////// case new_result : VoteResult {
|
||||
////// new:
|
||||
////// call winner = Candidates.get_winner(new_result.candidates)
|
||||
////// 0
|
||||
////// }
|
||||
////// }
|
||||
////// }
|
||||
////// `
|
||||
|
||||
////// let page = Parser.run!(Litereum.Lang.parser.page(world), code) abort IO.print("parse error")
|
||||
|
||||
////// log("PARSED:") // DEBUG
|
||||
////// log(Litereum.Lang.show.page(page, world)) // DEBUG
|
||||
|
||||
////// case Litereum.World.run.page(page, world) as result {
|
||||
////// none:
|
||||
////// IO.print("FAILURE")
|
||||
////// some:
|
||||
////// IO {
|
||||
////// // log("PAGE:") // DEBUG
|
||||
////// // let new_world = result.value // DEBUG
|
||||
////// // log(Litereum.Lang.show.page(page, new_world)) // DEBUG
|
||||
////// IO.print("SUCCESS")
|
||||
////// }
|
||||
////// }
|
1216
base/Litereum.kind
Normal file
1216
base/Litereum.kind
Normal file
File diff suppressed because it is too large
Load Diff
@ -1,148 +0,0 @@
|
||||
// A simple syntax for Litereum terms
|
||||
|
||||
Literity.show(term: Litereum.Term, world: Litereum.World, vars: List<String>, depth: Nat): String
|
||||
open world
|
||||
case term {
|
||||
var: case vars[term.index] as got {
|
||||
none: "^" | Nat.show(term.index)
|
||||
some: got.value
|
||||
}
|
||||
alloc: Maybe {
|
||||
get type = world.types[term.type]
|
||||
get form = type@forms[term.form]
|
||||
let text = ""
|
||||
let vals = List.zip_with!!!(
|
||||
(field,value)
|
||||
field@name
|
||||
| ":"
|
||||
| Literity.show(value, world, vars, depth),
|
||||
form@fields,
|
||||
term.vals)
|
||||
let vals = if List.is_empty!(vals) then "" else "{" | String.join(",",vals) | "}"
|
||||
return type@name | "#" | form@name | vals
|
||||
} <> "?"
|
||||
match: Maybe {
|
||||
get type = world.types[term.type]
|
||||
let expr = Literity.show(term.expr, world, vars, depth)
|
||||
let name = term.name
|
||||
let vals = List.zip_with!!!(
|
||||
(form,cse)
|
||||
let fields = List.map!!((x) name | "." | x@name, List.reverse!(form@fields))
|
||||
let vars = fields ++ vars
|
||||
let depth = Nat.succ(depth)
|
||||
form@name
|
||||
| ": "
|
||||
| Literity.show(cse, world, vars, depth),
|
||||
type@forms,
|
||||
term.cses)
|
||||
return type@name | "#case " | expr | " as " | name | " { " | String.join(", ",vals) | " }"
|
||||
} <> "?"
|
||||
} default "?"
|
||||
|
||||
Literity.parser.func(world: Litereum.World): Parser<Litereum.Term>
|
||||
Parser {
|
||||
get term = Literity.parser(world, ["input"])
|
||||
return term
|
||||
}
|
||||
|
||||
Literity.parser(world: Litereum.World, vars: List<String>): Parser<Litereum.Term>
|
||||
open world
|
||||
Parser.choice!([
|
||||
Literity.parser.alloc(world, vars)
|
||||
Literity.parser.match(world, vars)
|
||||
Literity.parser.var(world, vars)
|
||||
])
|
||||
|
||||
Literity.parser.alloc(world: Litereum.World, vars: List<String>): Parser<Litereum.Term>
|
||||
Parser {
|
||||
get type_name = Kind.Parser.name
|
||||
case Litereum.World.find_type(type_name, world) as found {
|
||||
none: Parser.fail!("Type not found.")
|
||||
some: Parser {
|
||||
Kind.Parser.text("#")
|
||||
get form_name = Kind.Parser.name
|
||||
let {type_num, type} = found.value
|
||||
case Litereum.Type.find_form(form_name, type) as found {
|
||||
none: Parser.fail!("Form not found.")
|
||||
some: Parser {
|
||||
let {form_num, form} = found.value
|
||||
let fields = form@fields
|
||||
if List.is_empty!(fields) then Parser {
|
||||
return Litereum.Term.alloc(type_num, form_num, [])
|
||||
} else Parser {
|
||||
let fields = List.map!!((x) x@name, fields)
|
||||
Kind.Parser.text("{")
|
||||
get vals = Literity.parser.alloc.vals(fields, world, vars)
|
||||
Kind.Parser.text("}")
|
||||
return Litereum.Term.alloc(type_num, form_num, vals)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Literity.parser.alloc.vals(fields: List<String>, world: Litereum.World, vars: List<String>): Parser<List<Litereum.Term>>
|
||||
case fields {
|
||||
nil: Parser {
|
||||
return []
|
||||
}
|
||||
cons: Parser {
|
||||
Kind.Parser.text(fields.head)
|
||||
Kind.Parser.text(":")
|
||||
get head = Literity.parser(world, vars)
|
||||
Parser.maybe!(Kind.Parser.text(","))
|
||||
get tail = Literity.parser.alloc.vals(fields.tail, world, vars)
|
||||
return head & tail
|
||||
}
|
||||
}
|
||||
|
||||
Literity.parser.match(world: Litereum.World, vars: List<String>): Parser<Litereum.Term>
|
||||
Parser {
|
||||
get type_name = Kind.Parser.name
|
||||
case Litereum.World.find_type(type_name, world) as found {
|
||||
none: Parser.fail!("Type not found.")
|
||||
some: Parser {
|
||||
let {type_num, type} = found.value
|
||||
//let cses = List.map!!((x) x@name, type@forms)
|
||||
Kind.Parser.text("#")
|
||||
Kind.Parser.text("case ")
|
||||
get expr = Literity.parser(world, vars)
|
||||
Kind.Parser.text("as")
|
||||
get name = Kind.Parser.name
|
||||
Kind.Parser.text("{")
|
||||
get cses = Literity.parser.match.cses(type@forms, name, vars, world)
|
||||
Kind.Parser.text("}")
|
||||
return Litereum.Term.match(type_num, name, expr, cses)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Literity.parser.match.cses(cses: List<Litereum.Form>, name: String, vars: List<String>, world: Litereum.World): Parser<List<Litereum.Term>>
|
||||
case cses {
|
||||
nil: Parser {
|
||||
return []
|
||||
}
|
||||
cons: Parser {
|
||||
use form = cses.head
|
||||
Kind.Parser.text(form.name)
|
||||
Kind.Parser.text(":")
|
||||
let fields = List.map!!((x) name | "." | x@name, List.reverse!(form.fields))
|
||||
get head = Literity.parser(world, fields ++ vars)
|
||||
Parser.maybe!(Kind.Parser.text(","))
|
||||
get tail = Literity.parser.match.cses(cses.tail, name, vars, world)
|
||||
return head & tail
|
||||
}
|
||||
}
|
||||
|
||||
Literity.parser.var(world: Litereum.World, vars: List<String>): Parser<Litereum.Term>
|
||||
Parser {
|
||||
get name = Kind.Parser.name
|
||||
case List.find_index!(vars, String.eql(name)) as found {
|
||||
none: Parser.fail!("Unbound variable '" | name | "'.")
|
||||
some: Parser {
|
||||
log("parsed var " | name | " " | Nat.show(found.value) | " " | String.join(",",vars))
|
||||
return Litereum.Term.var(found.value)
|
||||
}
|
||||
}
|
||||
}
|
9
base/Parser/letter.kind
Normal file
9
base/Parser/letter.kind
Normal file
@ -0,0 +1,9 @@
|
||||
Parser.letter(is_letter: Char -> Bool): Parser<Char>
|
||||
(pst)
|
||||
open pst
|
||||
case pst.str {
|
||||
nil: Parser.Reply.fail!(pst.nam, pst.ini, pst.idx, "Unexpected eof."),
|
||||
cons: if is_letter(pst.str.head)
|
||||
then Parser.Reply.value!(Parser.State.new(pst.err, pst.nam, pst.ini, Nat.succ(pst.idx), pst.str.tail), pst.str.head)
|
||||
else Parser.Reply.fail!(pst.nam, pst.ini, pst.idx, "Expected letter."),
|
||||
}
|
@ -1,6 +1,16 @@
|
||||
Test: _
|
||||
let world = Litereum.genesis
|
||||
let code = `
|
||||
eval #50
|
||||
type Bool { true{} false{} }
|
||||
eval +(#10, #20)
|
||||
`
|
||||
let block = Parser.run!(Litereum.parse.block(world), code) abort IO.print("deu ruim")
|
||||
IO {
|
||||
for i from 0 to 32:
|
||||
let serial = Litereum.serialize.word.varlen(Nat.to_u64(i))
|
||||
IO.print(Nat.show(i) | ": " | Bits.show(serial))
|
||||
log("Block: ")
|
||||
for tx in block:
|
||||
IO.print("- " | Litereum.show.transaction(world, tx))
|
||||
log("Evaluation: ")
|
||||
let tmp = Litereum.run.block(world, block)
|
||||
IO.print("Done!")
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user