mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Lit.Core: validate on running call branch
This commit is contained in:
parent
09e8b44a91
commit
d92f51959e
@ -195,9 +195,9 @@ Lit.Core.World.check.term(
|
||||
world: Lit.Core.World
|
||||
caller: Maybe<String>
|
||||
): Bool
|
||||
// log("- chk " | Lit.Lang.show.term(term, 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!(context)))) // DEBUG
|
||||
// log("") // DEBUG
|
||||
// log("- chk " | Lit.Lang.show.term(term, 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!(context)))) // DEBUG
|
||||
// log("") // DEBUG
|
||||
let result = case term {
|
||||
var:
|
||||
let var_type = context{term.name} abort false
|
||||
@ -341,19 +341,19 @@ Lit.Core.World.check.owner(
|
||||
// Validation
|
||||
// ----------
|
||||
// Checks if:
|
||||
// - no global binders with the same name
|
||||
// - TODO: no global binders with the same name
|
||||
// - variables are used at most once
|
||||
|
||||
// TODO:
|
||||
// - error list
|
||||
|
||||
Lit.Core.World.validate(
|
||||
Lit.Core.validate.term(
|
||||
term: Lit.Core.Term
|
||||
used: Map<Bool>
|
||||
): Pair<Map<Bool>,Bool>
|
||||
Lit.Core.World.validate.aux({used, true}, term)
|
||||
Lit.Core.validate.term.aux({used, true}, term)
|
||||
|
||||
Lit.Core.World.validate.aux(
|
||||
Lit.Core.validate.term.aux(
|
||||
state: Pair<Map<Bool>, Bool>
|
||||
term: Lit.Core.Term
|
||||
): Pair<Map<Bool>, Bool>
|
||||
@ -378,11 +378,11 @@ Lit.Core.World.validate.aux(
|
||||
|
||||
create:
|
||||
for val in term.vals with state:
|
||||
Lit.Core.World.validate.aux(state, val)
|
||||
Lit.Core.validate.term.aux(state, val)
|
||||
state
|
||||
|
||||
match:
|
||||
let state = Lit.Core.World.validate.aux(state, term.expr)
|
||||
let state = Lit.Core.validate.term.aux(state, term.expr)
|
||||
for cse in term.cses with state:
|
||||
let {fields, _} = cse
|
||||
let field_state = state
|
||||
@ -399,15 +399,15 @@ Lit.Core.World.validate.aux(
|
||||
|
||||
call:
|
||||
for arg in term.args with state:
|
||||
Lit.Core.World.validate.aux(state, arg)
|
||||
Lit.Core.validate.term.aux(state, arg)
|
||||
state
|
||||
|
||||
bind:
|
||||
let {used, valid} = state
|
||||
let used = used{term.name} <- false
|
||||
let state = {used, valid}
|
||||
let state = Lit.Core.World.validate.aux(state, term.main)
|
||||
let state = Lit.Core.World.validate.aux(state, term.cont)
|
||||
let state = Lit.Core.validate.term.aux(state, term.main)
|
||||
let state = Lit.Core.validate.term.aux(state, term.cont)
|
||||
state
|
||||
|
||||
word:
|
||||
@ -416,12 +416,12 @@ Lit.Core.World.validate.aux(
|
||||
compare:
|
||||
let terms = [term.val0, term.val1, term.iflt, term.ifeq, term.ifgt]
|
||||
for i_term in terms with state:
|
||||
Lit.Core.World.validate.aux(state, i_term)
|
||||
Lit.Core.validate.term.aux(state, i_term)
|
||||
state
|
||||
|
||||
operate:
|
||||
let state = Lit.Core.World.validate.aux(state, term.val0)
|
||||
let state = Lit.Core.World.validate.aux(state, term.val1)
|
||||
let state = Lit.Core.validate.term.aux(state, term.val0)
|
||||
let state = Lit.Core.validate.term.aux(state, term.val1)
|
||||
state
|
||||
}
|
||||
|
||||
@ -475,7 +475,9 @@ Lit.Core.World.run.statement(
|
||||
none:
|
||||
let new_world = world{func.name} <- Lit.Core.Entry.bond(func)
|
||||
let ctx = some({})
|
||||
let ctx = for arg in List.zip!!(func.input_names, func.input_types): Maybe {
|
||||
let args = List.zip!!(func.input_names, func.input_types)
|
||||
let ctx = for arg in args:
|
||||
Maybe {
|
||||
let {arg_name, arg_type} = arg
|
||||
get ctx = ctx
|
||||
get typ = Lit.Core.World.get_type(arg_type, world)
|
||||
@ -488,14 +490,20 @@ Lit.Core.World.run.statement(
|
||||
none:
|
||||
log("error: func input type undefined: " | func.name) none
|
||||
some:
|
||||
let otyp = Lit.Core.World.get_type(func.output_type, world) abort log("error: func otyp not found: " | func.name) none
|
||||
if Lit.Core.World.check.term(func.main, otyp, ctx.value, new_world, some(func.name)) then
|
||||
let {ah, ok} = Lit.Core.World.validate(func.main, vld)
|
||||
let otyp = Lit.Core.World.get_type(func.output_type, world)
|
||||
abort log("error: func otyp not found: " | func.name) none
|
||||
let term_ok = Lit.Core.World.check.term(
|
||||
func.main,
|
||||
otyp,
|
||||
ctx.value,
|
||||
new_world,
|
||||
some(func.name),
|
||||
)
|
||||
if term_ok then
|
||||
let {_, ok} = Lit.Core.validate.term(func.main, vld)
|
||||
if ok then
|
||||
//log("here")
|
||||
some(new_world)
|
||||
else
|
||||
//log("there")
|
||||
log("error: func invalid: " | func.name) none
|
||||
else
|
||||
log("error: func ill-typed: " | func.name) none
|
||||
@ -503,15 +511,21 @@ Lit.Core.World.run.statement(
|
||||
} default log("error: func redefinition: " | func.name) none
|
||||
}
|
||||
call:
|
||||
let exec = statement.expr
|
||||
let exec_term = statement.expr
|
||||
// This assumes that the call returns the built-in type Word to avoid
|
||||
// duplicating the typechecking function.
|
||||
let call_type = Lit.Core.Type.word
|
||||
let term_ok = Lit.Core.World.check.term(exec, call_type, {}, world, none)
|
||||
let term_ok =
|
||||
Lit.Core.World.check.term(exec_term, call_type, {}, world, none)
|
||||
if term_ok then
|
||||
let {result, world} = Lit.Core.World.run.term(exec, world, {})
|
||||
let {_, ok} = Lit.Core.validate.term(exec_term, {})
|
||||
if ok then
|
||||
let {result, new_world} =
|
||||
Lit.Core.World.run.term(exec_term, world, {})
|
||||
log("- ext_exec: " | Lit.Lang.show.term(result, world))
|
||||
some(world)
|
||||
some(new_world)
|
||||
else
|
||||
log("error: exec is invalid") none
|
||||
else
|
||||
log("error: exec failed in typecheck") none
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user