mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
change types and add lots of holes
This commit is contained in:
Rígille S. B. Menezes
parent
7ad0b149f3
commit
0eca11c51a
@ -384,6 +384,15 @@ Lit.Core.World.check.owner(
|
||||
// Execution
|
||||
// ---------
|
||||
|
||||
//Pair<Lit.Core.Term, Lit.Core.World>
|
||||
type Lit.Core.run.Context {
|
||||
new(
|
||||
term: Lit.Core.Term
|
||||
world: Lit.Core.World
|
||||
gas: Nat
|
||||
)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.page(
|
||||
page: Lit.Core.Page
|
||||
world: Lit.Core.World
|
||||
@ -400,7 +409,6 @@ Lit.Core.World.run.page(
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
Lit.Core.World.run.statement(
|
||||
statement: Lit.Core.Statement
|
||||
world: Lit.Core.World
|
||||
@ -475,10 +483,10 @@ Lit.Core.World.run.statement(
|
||||
let context = Lit.Core.Check.Context.from_world(world)
|
||||
let term_ok = Lit.Core.World.check.term(context, exec_term, call_type)
|
||||
if term_ok then
|
||||
let {result, new_world} =
|
||||
Lit.Core.World.run.term(exec_term, world, {})
|
||||
log("- ext_exec: " | Lit.Lang.show.term(result, world))
|
||||
some(new_world)
|
||||
use ctx =
|
||||
Lit.Core.World.run.term(exec_term, world, {}, _) // TODO
|
||||
log("- ext_exec: " | Lit.Lang.show.term(ctx.term, world))
|
||||
some(ctx.world)
|
||||
else
|
||||
log("error: exec failed in typecheck") none
|
||||
}
|
||||
@ -489,7 +497,8 @@ Lit.Core.World.run.term(
|
||||
term: Lit.Core.Term
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
gas: Nat
|
||||
): Lit.Core.run.Context
|
||||
// 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("")
|
||||
@ -501,7 +510,7 @@ Lit.Core.World.run.term(
|
||||
match:
|
||||
Lit.Core.World.run.term.match(world, vars, term.name, term.type, term.expr, term.cses)
|
||||
word:
|
||||
{term, world}
|
||||
{term, world, gas}
|
||||
compare:
|
||||
Lit.Core.World.run.term.compare(world, vars, term.val0, term.val1, term.iflt, term.ifeq, term.ifgt)
|
||||
operate:
|
||||
@ -516,14 +525,194 @@ Lit.Core.World.run.terms(
|
||||
terms: List<Lit.Core.Term>
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
): Pair<List<Lit.Core.Term>, Lit.Core.World>
|
||||
gas: Nat
|
||||
): Triple<List<Lit.Core.Term>, Lit.Core.World, Nat>
|
||||
case terms {
|
||||
nil:
|
||||
{[], world}
|
||||
{[], world, gas}
|
||||
cons:
|
||||
let {head, world} = Lit.Core.World.run.term(terms.head, world, vars)
|
||||
let {tail, world} = Lit.Core.World.run.terms(terms.tail, world, vars)
|
||||
{head & tail, world}
|
||||
//let {head, world} = Lit.Core.World.run.term(terms.head, world, vars, _) // TODO
|
||||
use ctx = Lit.Core.World.run.term(terms.head, world, vars, gas) // TODO
|
||||
use tail = Lit.Core.World.run.terms(terms.tail, ctx.world, vars, ctx.gas)
|
||||
{ctx.term & tail.fst, tail.snd, tail.trd}
|
||||
}
|
||||
Lit.Core.World.run.term.call(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
func: String
|
||||
args: List<Lit.Core.Term>
|
||||
cont: Lit.Core.Term
|
||||
): Lit.Core.run.Context
|
||||
case world{func} as got {
|
||||
none:
|
||||
//{Lit.Core.Term.call(name, func, args, cont), world}
|
||||
_ // TODO
|
||||
some:
|
||||
case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let inner_vars = vars
|
||||
let state = {inner_vars, world}
|
||||
for arg in List.zip!!(func.input_names, args) with state:
|
||||
let {inner_vars, world} = state
|
||||
let {arg_name, arg_term} = arg
|
||||
use ctx = Lit.Core.World.run.term(arg_term, world, inner_vars, _)
|
||||
let _ = Lit.Core.run.term.check_sanity(ctx.term) // DEBUG-ish
|
||||
let inner_vars = inner_vars{arg_name} <- ctx.term
|
||||
{inner_vars, ctx.world}
|
||||
let {inner_vars, world} = state
|
||||
//let {done, world} = Lit.Core.World.run.term(func.main, world, inner_vars, _)
|
||||
use ctx = Lit.Core.World.run.term(func.main, world, inner_vars, _)
|
||||
let _ = Lit.Core.run.term.check_sanity(ctx.term) // DEBUG-ish
|
||||
let vars = vars{name} <- ctx.term
|
||||
Lit.Core.World.run.term(cont, ctx.world, vars, _) // TODO
|
||||
} default
|
||||
//{Lit.Core.Term.call(name, func, args, cont), world}
|
||||
_ // TODO
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.compare(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
val0: Lit.Core.Term
|
||||
val1: Lit.Core.Term
|
||||
iflt: Lit.Core.Term
|
||||
ifeq: Lit.Core.Term
|
||||
ifgt: Lit.Core.Term
|
||||
): Lit.Core.run.Context
|
||||
//let {val0, world} = Lit.Core.World.run.term(val0, world, vars, _) // TODO
|
||||
use ctx0 = Lit.Core.World.run.term(val0, world, vars, _) // TODO
|
||||
//let {val1, world} = Lit.Core.World.run.term(val1, ctx.world, vars, _) // TODO
|
||||
use ctx1 = Lit.Core.World.run.term(val1, ctx0.world, vars, _) // TODO
|
||||
case ctx0.term ctx1.term {
|
||||
word word:
|
||||
case U64.cmp(ctx0.term.numb, ctx1.term.numb) {
|
||||
ltn:
|
||||
Lit.Core.World.run.term(iflt, world, vars, _) // TODO
|
||||
eql:
|
||||
Lit.Core.World.run.term(ifeq, world, vars, _) // TODO
|
||||
gtn:
|
||||
Lit.Core.World.run.term(ifgt, world, vars, _) // TODO
|
||||
}
|
||||
} default
|
||||
//log("error: operands didn't reduce to words") {Lit.Core.Term.compare(val0, val1, iflt, ifeq, ifgt), world}
|
||||
_ // TODO
|
||||
|
||||
|
||||
Lit.Core.World.run.term.match(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
type: String
|
||||
expr: Lit.Core.Term
|
||||
cses: List<Lit.Core.Term.Case>
|
||||
): Lit.Core.run.Context
|
||||
//let {expr, world} = Lit.Core.World.run.term(expr, world, vars, _) // TODO
|
||||
use ctx = Lit.Core.World.run.term(expr, world, vars, _) // TODO
|
||||
case ctx.term {
|
||||
create: case cses[ctx.term.ctor] as selected_case {
|
||||
some:
|
||||
let {case_fields, case_body} = selected_case.value
|
||||
let vars = for subst in List.zip!!(case_fields, ctx.term.vals):
|
||||
let {field, value} = subst
|
||||
vars{field} <- value
|
||||
Lit.Core.World.run.term(case_body, ctx.world, vars, _) // TODO
|
||||
} default
|
||||
//{Lit.Core.Term.match(name, type, ctx.term, cses), world}
|
||||
_ // TODO
|
||||
} default
|
||||
//{Lit.Core.Term.match(name, type, ctx.term, cses), world}
|
||||
_ // TODO
|
||||
|
||||
Lit.Core.World.run.term.create(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
type: String
|
||||
ctor: Nat
|
||||
vals: List<Lit.Core.Term>
|
||||
): Lit.Core.run.Context
|
||||
let {vals, world} = Lit.Core.World.run.terms(vals, world, vars, _) //TODO
|
||||
//{Lit.Core.Term.create(type, ctor, vals), world}
|
||||
_ // TODO
|
||||
|
||||
Lit.Core.World.run.term.var(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
): Lit.Core.run.Context
|
||||
case vars{name} as got {
|
||||
none:
|
||||
//{Lit.Core.Term.var(name), world}
|
||||
_ // TODO
|
||||
some:
|
||||
Lit.Core.World.run.term(got.value, world, vars, _) // TODO
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.operate(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
oper: Lit.Core.Operation
|
||||
val0: Lit.Core.Term
|
||||
val1: Lit.Core.Term
|
||||
): Lit.Core.run.Context
|
||||
let {val0, world} = Lit.Core.World.run.term(val0, world, vars, _) // TODO
|
||||
let {val1, world} = Lit.Core.World.run.term(val1, world, vars, _) // TODO
|
||||
case val0 val1 {
|
||||
word word:
|
||||
case oper {
|
||||
add:
|
||||
//{Lit.Core.Term.word(val0.numb + val1.numb), world}
|
||||
_ // TODO
|
||||
sub:
|
||||
//{Lit.Core.Term.word(val0.numb - val1.numb), world}
|
||||
_ // TODO
|
||||
mul:
|
||||
//{Lit.Core.Term.word(val0.numb * val1.numb), world}
|
||||
_ // TODO
|
||||
div:
|
||||
//{Lit.Core.Term.word(val0.numb / val1.numb), world}
|
||||
_ // TODO
|
||||
mod:
|
||||
//{Lit.Core.Term.word(val0.numb % val1.numb), world}
|
||||
_ // TODO
|
||||
or:
|
||||
//{Lit.Core.Term.word(val0.numb || val1.numb), world}
|
||||
_ // TODO
|
||||
and:
|
||||
//{Lit.Core.Term.word(val0.numb && val1.numb), world}
|
||||
_ // TODO
|
||||
xor:
|
||||
//{Lit.Core.Term.word(U64.xor(val0.numb, val1.numb)), world}
|
||||
_ // TODO
|
||||
}
|
||||
} default
|
||||
//log("error: operand didn't reduce to word")
|
||||
//{Lit.Core.Term.operate(oper, val0, val1), world}
|
||||
_ // TODO
|
||||
|
||||
Lit.Core.World.run.term.bind(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
main: Lit.Core.Term
|
||||
cont: Lit.Core.Term
|
||||
): Lit.Core.run.Context
|
||||
case world{name} as got {
|
||||
none:
|
||||
//{Lit.Core.Term.bind(name, main, cont), world}
|
||||
_ // TODO
|
||||
some:
|
||||
case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
//let {main, world} = Lit.Core.World.run.term(main, world, vars, _) // TODO
|
||||
use ctx = Lit.Core.World.run.term(main, world, vars, _) // TODO
|
||||
let world = ctx.world{name} <- Lit.Core.Entry.bond(func@main <- ctx.term)
|
||||
Lit.Core.World.run.term(cont, world, vars, _) // TODO
|
||||
} default
|
||||
//{Lit.Core.Term.bind(name, main, cont), world}
|
||||
_ // TODO
|
||||
}
|
||||
|
||||
Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool
|
||||
@ -564,155 +753,6 @@ Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool
|
||||
&& Lit.Core.run.term.check_sanity(term.cont)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.call(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
func: String
|
||||
args: List<Lit.Core.Term>
|
||||
cont: Lit.Core.Term
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
case world{func} as got {
|
||||
none:
|
||||
{Lit.Core.Term.call(name, func, args, cont), world}
|
||||
some:
|
||||
case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let inner_vars = vars
|
||||
let state = {inner_vars, world}
|
||||
for arg in List.zip!!(func.input_names, args) with state:
|
||||
let {inner_vars, world} = state
|
||||
let {arg_name, arg_term} = arg
|
||||
let {arg_term, world} = Lit.Core.World.run.term(arg_term, world, inner_vars)
|
||||
let _ = Lit.Core.run.term.check_sanity(arg_term) // DEBUG-ish
|
||||
let inner_vars = inner_vars{arg_name} <- arg_term
|
||||
{inner_vars, world}
|
||||
let {inner_vars, world} = state
|
||||
let {done, world} = Lit.Core.World.run.term(func.main, world, inner_vars)
|
||||
let _ = Lit.Core.run.term.check_sanity(done) // DEBUG-ish
|
||||
let vars = vars{name} <- done
|
||||
Lit.Core.World.run.term(cont, world, vars)
|
||||
} default {Lit.Core.Term.call(name, func, args, cont), world}
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.compare(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
val0: Lit.Core.Term
|
||||
val1: Lit.Core.Term
|
||||
iflt: Lit.Core.Term
|
||||
ifeq: Lit.Core.Term
|
||||
ifgt: Lit.Core.Term
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
let {val0, world} = Lit.Core.World.run.term(val0, world, vars)
|
||||
let {val1, world} = Lit.Core.World.run.term(val1, world, vars)
|
||||
case val0 val1 {
|
||||
word word:
|
||||
case U64.cmp(val0.numb, val1.numb) {
|
||||
ltn:
|
||||
Lit.Core.World.run.term(iflt, world, vars)
|
||||
eql:
|
||||
Lit.Core.World.run.term(ifeq, world, vars)
|
||||
gtn:
|
||||
Lit.Core.World.run.term(ifgt, world, vars)
|
||||
}
|
||||
} default log("error: operands didn't reduce to words") {Lit.Core.Term.compare(val0, val1, iflt, ifeq, ifgt), world}
|
||||
|
||||
|
||||
Lit.Core.World.run.term.match(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
type: String
|
||||
expr: Lit.Core.Term
|
||||
cses: List<Lit.Core.Term.Case>
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
let {expr, world} = Lit.Core.World.run.term(expr, world, vars)
|
||||
case expr {
|
||||
create: case cses[expr.ctor] as selected_case {
|
||||
some:
|
||||
let {case_fields, case_body} = selected_case.value
|
||||
let vars = for subst in List.zip!!(case_fields, expr.vals):
|
||||
let {field, value} = subst
|
||||
vars{field} <- value
|
||||
Lit.Core.World.run.term(case_body, world, vars)
|
||||
} default {Lit.Core.Term.match(name, type, expr, cses), world}
|
||||
} default {Lit.Core.Term.match(name, type, expr, cses), world}
|
||||
|
||||
Lit.Core.World.run.term.create(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
type: String
|
||||
ctor: Nat
|
||||
vals: List<Lit.Core.Term>
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
let {vals, world} = Lit.Core.World.run.terms(vals, world, vars)
|
||||
{Lit.Core.Term.create(type, ctor, vals), world}
|
||||
|
||||
Lit.Core.World.run.term.var(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
case vars{name} as got {
|
||||
none:
|
||||
{Lit.Core.Term.var(name), world}
|
||||
some:
|
||||
Lit.Core.World.run.term(got.value, world, vars)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.operate(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
oper: Lit.Core.Operation
|
||||
val0: Lit.Core.Term
|
||||
val1: Lit.Core.Term
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
let {val0, world} = Lit.Core.World.run.term(val0, world, vars)
|
||||
let {val1, world} = Lit.Core.World.run.term(val1, world, vars)
|
||||
case val0 val1 {
|
||||
word word:
|
||||
case oper {
|
||||
add:
|
||||
{Lit.Core.Term.word(val0.numb + val1.numb), world}
|
||||
sub:
|
||||
{Lit.Core.Term.word(val0.numb - val1.numb), world}
|
||||
mul:
|
||||
{Lit.Core.Term.word(val0.numb * val1.numb), world}
|
||||
div:
|
||||
{Lit.Core.Term.word(val0.numb / val1.numb), world}
|
||||
mod:
|
||||
{Lit.Core.Term.word(val0.numb % val1.numb), world}
|
||||
or:
|
||||
{Lit.Core.Term.word(val0.numb || val1.numb), world}
|
||||
and:
|
||||
{Lit.Core.Term.word(val0.numb && val1.numb), world}
|
||||
xor:
|
||||
{Lit.Core.Term.word(U64.xor(val0.numb, val1.numb)), world}
|
||||
}
|
||||
} default log("error: operand didn't reduce to word")
|
||||
{Lit.Core.Term.operate(oper, val0, val1), world}
|
||||
|
||||
Lit.Core.World.run.term.bind(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
name: String
|
||||
main: Lit.Core.Term
|
||||
cont: Lit.Core.Term
|
||||
): Pair<Lit.Core.Term, Lit.Core.World>
|
||||
case world{name} as got {
|
||||
none:
|
||||
{Lit.Core.Term.bind(name, main, cont), world}
|
||||
some:
|
||||
case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let {main, world} = Lit.Core.World.run.term(main, world, vars)
|
||||
let world = world{name} <- Lit.Core.Entry.bond(func@main <- main)
|
||||
Lit.Core.World.run.term(cont, world, vars)
|
||||
} default {Lit.Core.Term.bind(name, main, cont), world}
|
||||
}
|
||||
|
||||
//
|
||||
// Tests
|
||||
|
||||
Loading…
Reference in New Issue
Block a user