/*

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)