/*
Checks for recursion in proofs.
When proofs call themselves directly or indirectly,
this can lead to unsoundness.
This script checks the HOOO module,
such that no proofs call themselves.
*/
fn main() {
~ data := unwrap(load(meta: "assets/rec-syntax.txt", file: "src/hooo.rs"))
~ start_fns := sift i {if is_start(data[i], "fn") {clone(i)} else {continue}}
~ end_fns := sift i {if is_end(data[i], "fn") {clone(i)} else {continue}}
~ start_methods := sift i {if is_start(data[i], "method") {clone(i)} else {continue}}
~ end_methods := sift i {if is_end(data[i], "method") {clone(i)} else {continue}}
~ start_calls := sift i {if is_start(data[i], "call") {clone(i)} else {continue}}
~ end_calls := sift i {if is_end(data[i], "call") {clone(i)} else {continue}}
~ start_lets := sift i {if is_start(data[i], "let") {clone(i)} else {continue}}
~ end_lets := sift i {if is_end(data[i], "let") {clone(i)} else {continue}}
~ names := sift i {if is_str(data[i], "name") {clone(i)} else {continue}}
~ depths := depths()
~ call_depths := call_depths()
~ let_depths := let_depths()
~ range_fns := sift i len(start_fns) {range(i)}
~ range_methods := sift i len(start_methods) {range_method(i)}
~ range_calls := sift i len(start_calls) {range_call(i)}
~ range_lets := sift i len(start_lets) {range_let(i)}
analysis := []
allow := sift i {
if depths[i] != 0 {continue}
name_ind := name_of(start_fns[i])
clone([i, data[unwrap(name_ind)][4]])
}
for i {
list := []
if is_fn_method(i) {}
else if depths[i] == 0 {
name_ind := name_of(start_fns[i])
if name_ind != none() {
name := data[unwrap(name_ind)][4]
calls := calls(i)
lets := lets(i)
'outer: for j {
k := calls[j]
for l {if is(call: k, let: lets[l]) {continue 'outer}}
name_ind := name_of(start_calls[k])
if name_ind != none() {
name := data[unwrap(name_ind)][4]
found := any i {name == allow[i][1]}
if found {
why := why(found)
push(mut list, why[0])
}
}
}
}
}
push(mut analysis, list)
}
todo := sift i len(start_fns) {
if len(analysis[i]) == 0 {continue}
clone(i)
}
old_len := 0
'outer: loop {
if len(todo) == old_len {break}
old_len = len(todo)
for i {
if all j {
k := analysis[todo[i]][j]
(!any m {todo[m] == allow[k][0]})
} {
if len(todo) >= 2 {
swap(mut todo, i, len(todo) - 1)
}
_ := pop(mut todo)
continue 'outer
}
}
}
for i {
j := todo[i]
name_ind := name_of(start_fns[j])
if name_ind != none() {
name := data[unwrap(name_ind)][4]
println(name)
for k {
allow := allow[analysis[j][k]]
found := any m {todo[m] == allow[0]}
if found {
why := why(found)
i := why[0]
name_ind := name_of(start_fns[todo[i]])
println(link {" "data[unwrap(name_ind)][4]})
}
}
}
}
}
is__call_let(i, j) ~ start_calls, start_lets, data = {
call_name_ind := name_of(start_calls[i])
let_name_ind := name_of(start_lets[j])
if (call_name_ind == none()) || (let_name_ind == none()) {return false}
data[unwrap(call_name_ind)][4] == data[unwrap(let_name_ind)][4]
}
lets(i) ~ range_fns, range_lets = {
rfn := range_fns[i]
sift j {
r := range_lets[j]
if (r[0] >= rfn[0]) && (r[1] <= rfn[1]) {clone(j)} else {continue}
}
}
calls(i) ~ range_fns, range_calls = {
rfn := range_fns[i]
sift j {
r := range_calls[j]
if (r[0] >= rfn[0]) && (r[1] <= rfn[1]) {clone(j)} else {continue}
}
}
sub_fns(i) ~ range_fns = {
range := range_fns[i]
sift j {
if j == i {continue}
r := range_fns[j]
if (r[0] >= range[0]) && (r[1] <= range[1]) {clone(j)} else {continue}
}
}
is_fn_method(i) ~ range_fns, range_methods = {
range_fn := range_fns[i]
any j {
r := range_methods[j]
(r[0] <= range_fn[0]) && (r[1] >= range_fn[1])
}
}
is_str(data, tag) = (data[2] == "str") && (data[3] == tag)
is_start(data, tag) = (data[2] == "start") && (data[3] == tag)
is_end(data, tag) = (data[2] == "end") && (data[3] == tag)
name_of(i) ~ data = {
j := i + 1
depth := 0
loop {
if (depth == 0) && is_str(data[j], "name") {return some(j)}
else if data[j][2] == "start" {depth += 1}
else if data[j][2] == "end" {
if depth == 0 {break}
depth -= 1
}
j += 1
}
none()
}
range_of(start, end, depths, i) ~ data = {
j := i
depth := depths[i]
loop {
j += 1
if j >= len(depths) {break}
if (depths[j] <= depth) {break}
}
clone([start[i], if j == len(start) {len(data)} else {end[j-1]}])
}
range(i) ~ start_fns, end_fns, depths = range_of(start_fns, end_fns, depths, i)
range_call(i) ~ start_calls, end_calls, call_depths = range_of(start_calls, end_calls, call_depths, i)
range_let(i) ~ start_lets, end_lets, let_depths = range_of(start_lets, end_lets, let_depths, i)
range_method(i) ~ start_methods, end_methods = {
clone([start_methods[i], end_methods[i]])
}
depths_of(start, end) = {
depth := 0
i := 0
j := 0
depths := []
loop {
if (i >= len(start)) {break}
if start[i] < end[j] {
push(mut depths, depth)
depth += 1
i += 1
} else {
j += 1
depth -= 1
}
}
clone(depths)
}
depths() ~ start_fns, end_fns = depths_of(start_fns, end_fns)
call_depths() ~ start_calls, end_calls = depths_of(start_calls, end_calls)
let_depths() ~ start_lets, end_lets = depths_of(start_lets, end_lets)