Uniform treatment of translation, axiomatization, and skipping

[antalsz]

@sweirich in a comment on commit 4cd6596, about unaxiomatize definition:

How about something a little more general, so that we can have "skip everything except for this" too. What I'm thinking of is:

• default is to translate everything in the module, but we can change that with one of these two edits: axiomatize module skip module

• Even if we change the default, we can override with one of these commands skip definition axiomatize definition translate definition

[antalsz]

@sweirich Well, at a minimum, translate is a much better name than unaxiomatize 🙂 The logic does make sense. The only design question I see is that going from skip module X to skip module X + translate X.y will go from producing no X.v file at all to producing an X.v file containing a y.

[sweirich]

Eventually, we may want a translate module edit too, if we want to move away from Makefile hackery.

[antalsz]

So the design structure is:

• Module → {Translate, Axiomatize, Skip}
• Definition → {Translate, Redefine, Axiomatize, Skip}

Per-definition rules take precedence over the by-module rules.

We leave skip method separate, and continue to have skipping a class have the behavior of skipping its instances. A skipped module is entirely absent unless at least one of its definitions is overridden; skipping every definition in a module will produce an empty module. This is fine; similarly, axiomatizing a module is more aggressive than axiomatizing every definition (failing to translate types/lookup class info is just ignored when the whole module is being axiomatized).

Other related issues:

• Should we teach skip Mod.methodName to have the same effect as skip method Mod.className Mod.methodName?

• Should we add some form of axiomatize type Mod.TypeName? Unfortunately we need to specify the parameter types in that case.

[sweirich]

Sounds good.

WRT related issues

• As skipping a method is more dramatic than skipping a definition, I'd rather keep these edits distinct.
• How about a way to redefine a Definition as an Axiom ?

[antalsz]

We have axiomatize definition working – is that what you mean?

[sweirich]

Does axiomatize definition not work for axiomatize type Mod.TypeName?

[antalsz]

No – mostly because we don't check, although also because we don't have kind signatures that we can fill in.

[sweirich]

The redefine I propose above would require the full type (which could be anything).

If we have data Tree a = Empty | Node a (Tree a) (Tree a)

then I propose that the edit

redefine Axiom Mod.Tree : Type -> Type

would replace the inductive datatype of Tree with the axiom.

[antalsz]

Oh, I see – regardless of whether Mod.Tree was an inductive type or a definition? Seems reasonable!

[antalsz]

OK, e9c47a7 adds support for redefine Axiom, since I wanted that for TrieMap :-)