Reducing Redundant Choicepoints

[eignnx]

https://github.com/eignnx/rellog/blob/e8e1f45a896d6b50256d657b470e175798870238/syntax-ideas.md?plain=1#L481-L547

Probably relies on #6 to do automatic subsumption checking on the different clauses.

See also Rust's exhaustiveness checking algorithm:

• https://rustc-dev-guide.rust-lang.org/pat-exhaustive-checking.html
• https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/pattern/usefulness/index.html

[eignnx]

I think for now, rather than rely on static analysis via #6 let's do a runtime check for head unifiability.

Example

> [foo X]
    - [is_num X]
> [foo Y]
    - [is_txt Y]

~We'll just check that there's only one index_match result, so in this example, an error would be thrown.~

We need a system with guards that would include the [is_num] test.

See:

https://www.swi-prolog.org/pldoc/man?section=ssu

[eignnx]

Cut needs to be a minor part of the language only used when implementing other things.

Maybe we just allow guards in rel sets i.e.

[Term][type int]; [is_num Term]
    - ...

[Term][type int] when [is_num Term]
    - ...

[Term][type int] <= [is_num Term]
    - ...

This would allow me to not add cut, just do smarter argument indexing. Basically we'd also look at guards when doing (or right after doing) argument indexing.

That preserves purity (I think?) Cause there's no cuts but we can still avoid unnecessary backtracking.

Maybe it would even allow indexing/solving in parallel.

[eignnx]

Erlang has guards on it's fn def clauses but you can only have certain functions in them. Why this restriction?

I guess cause in order to solve a rel you have to solve another rel?