Add renamer phase and a simala backend for natural4

[fendor]

This PR introduces two new things:

• A Renamer/Name resolver phase for Rules
• A Transpiler which allows transpiling a Rule to a Simala Decl.

The renamer implements lexical scope checking for Hornlike and TypeDecl rules.
It resolves all names, replacing occurrences of each name with its renamed equivalent.
This is supposed to lay the groundwork for a principled transpilation pipeline, avoiding redoing work for each transpiler, such as resolving names, making sure variables are in scope, etc...
In the future, we want to implement a type checker on top of a RnRule. However, that's currently only a dream and there are no attempts of doing any kind of typechecking at the moment.

The simala transpiler solely operates on the renamed rules. This simplifies the implementation a lot, demonstrating how other transpilers may also benefit from the rename phase.
The simala backend can currently only handle Hornlike rules and ignores any kind of TypeDecl rules, as simala is dynamically typed and typechecking should occur in a dedicated rule phase, not ad-hoc in the transpiler.

Both components are somewhat experimental and are expected to have bugs and missing features.

Todos:

• Logging (potentially using colog style logging)
• A proper error type (Don't throw Strings)
• Integration with the main-cli

[ym-han]

Some quick feedback:

Renamer.hs

High level things

• Would be helpful to have a comment or two indicating how to use the Renamer (might be enough to just indicate what the main entrypoints are in the export list and link to the Simala transpiler as an example?)
• Might be helpful to have a quick comment that
  (i) summarizes what the assumptions and guarantees of the Renamer are
  (ii) summarizes why the renaming is sound, if there is an easy way to explain this at a high level --- there may not
• A quick, high level summary of the scoping rules / semantics that have been implemented may also be helpful, though maybe it's obvious enough

Specific things

• RnRelationalPredicate: Might be good to provide examples of the various variants, especially RnRelationalTerm. This isn't high-priority / doesn't have to be done in this PR. (And yes, any unclarity here really has to do with the unclarity in the original RelationalPredicate data structure, and not with what you have done.)
• * @x@: a variable, might be bound ad-hoc -- what does 'bound ad-hoc' mean in this context?

---

In case the above came off as being negative: Again, I think that this PR has been a truly heroic amount of work.

[inariksit]

Looks good to me! Most of my comments are just minor remarks ("a comment rather than a question"). I thought the code was well documented, but of course, true test comes at the point when one starts trying to work with the code, not just passively look at it.

[inariksit]

I guess this could be used for things like number of children (e.g. < 100) or birth year (e.g. > 1900). Even in such cases, the validation would be given as a range rather than an enum. Probably the most practical question is, what kind of error messages we'd like to give if a user claims to be born in 1700: is it a type error, or just a runtime result "you're too old for insurance"?

(There's also the TYPICALLY keyword, but I don't know of its status in any of the various transpilers or previous case studies.)

[inariksit]

Is this meant to be replaced with something else later?

I'm asking, because earlier you wrote that GIVETHs are global, GIVENs are local and DECIDE head term in "IS" clauses is global. Is that the case in WHERE clauses as well? (Or am I mistaken about what renameRules does?)

[fendor]

So, in lexical scoping, we have a hierarchy of scopes. GIVETH and DECIDE are not "global", but their definitions may be used one level up the hierarchy. This generalises nicely, as rules in WHERE can be used by DECIDE and other rules in the WHERE clause, but not outside the rule that defines the WHERE clause.

For a practical example with nested clauses:

GIVEN x
DECIDE f x IS y
WHERE
  y IS g x
  GIVEN d DECIDE g d IS y WHERE y IS SUM(d, d)

• Then the rules y IS g x and GIVEN d DECIDE g d IS y WHERE y IS SUM(d, d) is local to the rule and the function g may be used in both WHERE and DECIDE blocks.
• y IS SUM(d,d) is local to the rule g, and can not be referenced by the top-level WHERE or DECIDE.
• y IS SUM(d,d) name shadows the outer y.

[inariksit]

I see, thanks for the explanation!

[ym-han]

This is another tangential syntax thing, but it's not clear to me that we really should allow users the flexibility to write arbitrary declarations in a WHERE block (as opposed to just things of the form y IS g x. There's probably no easy way to answer this question right now, and it's definitely not high-priority, but I'd be curious to see what you all think.

[inariksit]

The question of what to support has always been a bit vague. If I remember correctly, arbitrary expressions in a single cell became an explicit thing around last spring, with these 4 test cases for (Generic)MathLang.
Simultaneously, we have been saying for many years "we can totally make NaturaL4 stricter and require the user to not just type in whatever". Maybe this could be a natural spot to make some decisions. 😛 @mengwong , any comments/opinions?

[inariksit]

Does this comment mean that you plan to do so eventually (but it wasn't a prio for the first version), or that you are unsure how GIVETHs should be handled?

[fendor]

I suppose both, I want to focus on something that works with documented limitations, so that we can iteratively improve this version.

However, it is also unclear what a GIVETH really is, and how it would work in a function context, for example.

[inariksit]

Is this the excpected result?

[fendor]

Yes! This is intended as documenting the current capabilties of the transpilation.
I struggled to identify all possible meanings of predicates. In this case,

"Loss or Damage" IS ANY ( "caused by rodents"
                                    , "caused by insects"
                                    , "caused by vermin"
                                    , "caused by birds"
                                    )

Is a weird RelationalPredicate in my opinion. ANY feels overloaded. It may mean OR, but IS ANY suddenly means ELEM, and there is actually a RPelem RelationalPredicate which we don't use here.

So, I didn't even try to support this example, but rather we should talk about, which composite operators we want to support, or whether we rather want to use some ELEM operator.

[inariksit]

Good point! I pretty much have forgotten that RPelem existed 😁

[ym-han]

Yeah in general I think we shouldn't be afraid to try to make the syntax more regimented and understandable (not least because there is a non-trivial chance we'll actually have to try to help other people learn and use this!)

[fendor]

I tried to address some of the feedback, moved some code around that makes it hopefully a bit more clear what we are trying to do and added a documentation block that will hopefully evolve to a specification of the scoping rules in naturalL4.

A lot of good questions were raised regarding supported syntax and the type system, which we should write down and discuss.

I also fixed some glaring issues with the Simala Transpiler. However, I expect there are many issues left in the code, which we will hopefully weed out over time.
The renamer seems to be working relatively well, but is likely not tested enough. It would be nice to come up with a test specification that is better than simply printing a renamed rule, as this is really difficult to check, verify and understand.

[ym-han]

Thanks for adding more docs / explanations!