mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Lit.Core.run.term.check_sanity
This commit is contained in:
parent
f62b23fb1c
commit
905fa33192
@ -65,7 +65,7 @@ type Lit.Core.Term {
|
||||
// Binds an new program
|
||||
bind(
|
||||
name: String
|
||||
main: Lit.Core.Term
|
||||
main: Lit.Core.Term // TODO rename to `body`
|
||||
cont: Lit.Core.Term
|
||||
)
|
||||
}
|
||||
@ -632,6 +632,44 @@ Lit.Core.World.run.terms(
|
||||
{head & tail, world}
|
||||
}
|
||||
|
||||
Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool
|
||||
case term {
|
||||
var:
|
||||
log("==> SANITY CHECK FAILED: found term: " | "'" | term.name | "'")
|
||||
false
|
||||
create:
|
||||
let valid = true
|
||||
for val in term.vals with valid:
|
||||
valid && Lit.Core.run.term.check_sanity(val)
|
||||
valid
|
||||
match:
|
||||
let valid = Lit.Core.run.term.check_sanity(term.expr)
|
||||
for cse in term.cses with valid:
|
||||
valid && Lit.Core.run.term.check_sanity(cse@body)
|
||||
valid
|
||||
word:
|
||||
true
|
||||
compare:
|
||||
Lit.Core.run.term.check_sanity(term.val0)
|
||||
&& Lit.Core.run.term.check_sanity(term.val1)
|
||||
&& Lit.Core.run.term.check_sanity(term.iflt)
|
||||
&& Lit.Core.run.term.check_sanity(term.ifeq)
|
||||
&& Lit.Core.run.term.check_sanity(term.ifgt)
|
||||
operate:
|
||||
Lit.Core.run.term.check_sanity(term.val0)
|
||||
&& Lit.Core.run.term.check_sanity(term.val1)
|
||||
call:
|
||||
// TODO I don't know what I'm doing
|
||||
// should this return false (invalid) ?
|
||||
let valid = true
|
||||
for arg in term.args with valid:
|
||||
valid && Lit.Core.run.term.check_sanity(arg)
|
||||
valid && Lit.Core.run.term.check_sanity(term.cont)
|
||||
bind:
|
||||
Lit.Core.run.term.check_sanity(term.main)
|
||||
&& Lit.Core.run.term.check_sanity(term.cont)
|
||||
}
|
||||
|
||||
Lit.Core.World.run.term.call(
|
||||
world: Lit.Core.World
|
||||
vars: Map<Lit.Core.Term>
|
||||
@ -647,16 +685,18 @@ Lit.Core.World.run.term.call(
|
||||
case got.value as entry {
|
||||
bond:
|
||||
use func = entry.value
|
||||
let main_vars = vars
|
||||
let state = {main_vars, world}
|
||||
let state = for arg in List.zip!!(func.input_names, args):
|
||||
let {main_vars, world} = state
|
||||
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, main_vars)
|
||||
let main_vars = main_vars{arg_name} <- arg_term
|
||||
{main_vars, world}
|
||||
let {main_vars, world} = state
|
||||
let {done, world} = Lit.Core.World.run.term(func.main, world, main_vars)
|
||||
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}
|
||||
@ -780,6 +820,7 @@ Lit.Core.World.run.term.bind(
|
||||
} default {Lit.Core.Term.bind(name, main, cont), world}
|
||||
}
|
||||
|
||||
//
|
||||
// Tests
|
||||
// -----
|
||||
|
||||
@ -794,7 +835,7 @@ Lit.Core: _
|
||||
| Lit.Lang.Nat
|
||||
| Lit.Lang.Bits
|
||||
| Lit.Lang.BitsMap
|
||||
// | Lit.Lang.Test
|
||||
| Lit.Lang.Test
|
||||
|
||||
let code = code |
|
||||
`
|
||||
@ -841,17 +882,18 @@ Lit.Core: _
|
||||
// `
|
||||
|
||||
let page = Parser.run!(Lit.Lang.parser.page(world), code) abort IO.print("parse error")
|
||||
log("parsed:")
|
||||
log(Lit.Lang.show.page(page, world))
|
||||
|
||||
// log("PARSED:") // DEBUG
|
||||
// log(Lit.Lang.show.page(page, world)) // DEBUG
|
||||
|
||||
case Lit.Core.World.run.page(page, world) as result {
|
||||
none:
|
||||
IO.print("FAILURE")
|
||||
some:
|
||||
IO {
|
||||
// log("page:")
|
||||
// let new_world = result.value
|
||||
// log(Lit.Lang.show.page(page, new_world))
|
||||
// log("PAGE:") // DEBUG
|
||||
// let new_world = result.value // DEBUG
|
||||
// log(Lit.Lang.show.page(page, new_world)) // DEBUG
|
||||
IO.print("SUCCESS")
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user