mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
more refactoring on Lit.Core.World.validate
This commit is contained in:
parent
370f84e0db
commit
ebae487c12
@ -318,6 +318,9 @@ Lit.Core.World.check.owner(
|
||||
// - no global binders with the same name
|
||||
// - variables are used at most once
|
||||
|
||||
// TODO:
|
||||
// - error list
|
||||
|
||||
Lit.Core.World.validate(
|
||||
term: Lit.Core.Term
|
||||
used: Map<Bool>
|
||||
@ -348,60 +351,52 @@ Lit.Core.World.validate.aux(
|
||||
}
|
||||
|
||||
create:
|
||||
let state = for val in term.vals:
|
||||
let {used, res0} = state
|
||||
let {used, res1} = Lit.Core.World.validate(val, used)
|
||||
{used, res0 && res1}
|
||||
for val in term.vals with state:
|
||||
Lit.Core.World.validate.aux(state, val)
|
||||
state
|
||||
|
||||
match:
|
||||
let state = Lit.Core.World.validate.aux(state, term.expr)
|
||||
let {used, valid} = state
|
||||
let valid = for cse in term.cses:
|
||||
let {fields, body} = cse
|
||||
for cse in term.cses with state:
|
||||
let {fields, _} = cse
|
||||
let field_state = state
|
||||
let field_state = for field in fields:
|
||||
let {used, res} = field_state
|
||||
for field in fields with field_state:
|
||||
let {used, valid} = field_state
|
||||
case used{field} {
|
||||
some:
|
||||
{used, false} // same name used more than once
|
||||
none:
|
||||
{used{field} <- false, res}
|
||||
{used{field} <- false, valid}
|
||||
}
|
||||
field_state@snd
|
||||
{state@fst, valid}
|
||||
state
|
||||
state
|
||||
|
||||
call:
|
||||
let state = for arg in term.args:
|
||||
let {used, res0} = state
|
||||
let {used, res1} = Lit.Core.World.validate(arg, used)
|
||||
{used, res0 && res1}
|
||||
for arg in term.args with state:
|
||||
Lit.Core.World.validate.aux(state, arg)
|
||||
state
|
||||
|
||||
bind:
|
||||
let {used, valid} = state
|
||||
let used = used{term.name} <- false
|
||||
let {used, res0} = Lit.Core.World.validate(term.main, used)
|
||||
let {used, res1} = Lit.Core.World.validate(term.cont, used)
|
||||
{used, valid && res0 && res1}
|
||||
let state = {used, valid}
|
||||
let state = Lit.Core.World.validate.aux(state, term.main)
|
||||
let state = Lit.Core.World.validate.aux(state, term.cont)
|
||||
state
|
||||
|
||||
word:
|
||||
state
|
||||
|
||||
compare:
|
||||
let {used, valid} = state
|
||||
let {used, val0} = Lit.Core.World.validate(term.val0, used)
|
||||
let {used, val1} = Lit.Core.World.validate(term.val1, used)
|
||||
let {used, iflt} = Lit.Core.World.validate(term.iflt, used)
|
||||
let {used, ifeq} = Lit.Core.World.validate(term.ifeq, used)
|
||||
let {used, ifgt} = Lit.Core.World.validate(term.ifgt, used)
|
||||
{used, valid && val0 && val1 && iflt && ifeq && ifgt}
|
||||
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)
|
||||
state
|
||||
|
||||
operate:
|
||||
let {used, valid} = state
|
||||
let {used, val0} = Lit.Core.World.validate(term.val0, used)
|
||||
let {used, val1} = Lit.Core.World.validate(term.val1, used)
|
||||
{used, val0 && val1}
|
||||
let state = Lit.Core.World.validate.aux(state, term.val0)
|
||||
let state = Lit.Core.World.validate.aux(state, term.val1)
|
||||
state
|
||||
}
|
||||
|
||||
// Execution
|
||||
|
Loading…
Reference in New Issue
Block a user