Simplification of the modules and terms

GuillaumeGen commented 2 years ago

This makes a lot of things:

It completely suppress CTree,
It cleans all the useless imports,
It makes a lot of names more explicit,
It suppress a lot of type indirection to make it easier to unroll definition of most of the types, especially the Term and Type ones.

Furthermore, it mainly focused on the part of the code defining our version of System F. Here are a lot of thoughts I collected on those modules while doing it.

Pirouette.Term.Syntax.Subst

[ ] Does it really make sense to have a module defining term independent substitution?
[x] The representation is quite exotic, an example would be welcome.
[ ] The composition operation is in the reverse order. Is this intended?
[x] As far as I know, composition is associative, so (.) is not especially right-associative. (I would even say the contrary, and expect (h . g . f) x to be (h . g) (f x). But it might be a strict-language user view of the thing.)

Pirouette.Term.Syntax.SystemF

[x] Why not long names for "Bound" "Free" and "Meta"?
[x] A comment on the fact that meta-variables are holes with an arbitrary type. It is a mechanism to make heterogeneous terms.
[x] In AnnType, the variable ty should be tyVar.
[x] No idea of what tyFlatten does. Plus it is unused.
[x] Do we really need to introduce a Type type here, which is only used to define another Type type in Base?
[x] Pointfree functions often hurts readability.
[x] Does it really make sense to mix tyApp and tyAfterTermApp?
[x] Class HasApp is very hard to read, because term is a type family, and I have no idea of what the type AppArg represents.
[x] The comment before AnnTerm is outdated.
[x] termAnnFold gathers also the type variables. Any reason to do/not do it?
[x] Any reason not to implement termTriMap as runIdentity . termTriMapM?
[x] preserveLams do not preserve the Abs, so it does not always go down to the first application.
[x] Shouldn't Arg be named TermArg?
[x] Term should be suppressed here.
[x] pattern Free and Term (if not suppressed) should not be defined here.
[x] No idea of what termFlatten does. Plus it is unused.
[x] I (re-)discovered line 252 that the type variables do not count when computing the de-Bruijn indices. This should be documented (and justified).
[x] Shouldn't expandVar use transform rather than rewrite, so that it inlines every occurrence, but do not do it recursively.
[x] Naming variables would help in appN of AnnTerm.
[x] It should be documented that appN of an "heterogeneous list" with both term and type arguments does not work.
[x] Comment of mapNameScoped is not a proper English sentence.
[x] Function permute is very weird and unused.
[x] app should not be pointfree.

Pirouette.Term.Syntax.Pretty.Class

[x] Line 25: "enclosing".

Pirouette.Term.Syntax.Base

[x] A small comment about the distinction between Constants and BuiltinTerms.
[x] What about renaming TyFree into TypeFromSignature.
[x] I would name LanguageDef as LanguageBuiltins.
[x] Idem about FreeName.
[x] What does the Bottom stands for? ANSWER: The error term presents in PlutusIR.
[x] Any reason to keep Base polymorphic in name?
[ ] Base contains declaration/definition related functions. Should we rename it?

Pirouette.Term.Syntax.Pretty

Pirouette.Term.Syntax

[x] Not being name polymorphic in Base would suppress the indirection of Prt....
[x] Expand Set and Map name. Probably also Raw.
[x] Typo line 154, "indices" without 'i'.
[ ] A lot of clever things about unique naming. Better names should be found, and probably to put in a separate module.

GuillaumeGen commented 2 years ago

This PR also completely removes the currently not working translation to TLA+ and fixes the CI accordingly.

VictorCMiraldo commented 2 years ago

@GuillaumeGen, we might want to split your PR in two: one that does the renaming and ormolu across the board; then another that executes commit https://github.com/tweag/pirouette/pull/55/commits/b1118a140be8f6d16994ff18bd1ab97335140961, this way its very easy for us to rescue things we need from the old TLA+ translation.

tweag / pirouette