don’t require uppercase operator names
Closed this issue · 8 comments
This is really annoying... the reason we do it is that otherwise there is an ambiguity between variables and nullary operators. the solution is to parse terms in some less structured formaf, extended sexprs. then we turn these into abts during RedML elaboration, so that we can correctly choose whether something is an operator head or a variable based on the resolver environment.
This is a better design anyway.it will also solve many problems with sort inference.
We can also get rid of the stupid sigils for metavariables 😄
And we can also start using upper case letters as variables in the object language, which will help us get rid of a ton of annoying contortions
Another thing too is that this will greatly decrease the size of the parser, making it easier to move away from MLYacc in the future, perhaps switching to Karl's tool.
To be able to parse things like tactics under this scheme, I guess I need to design a parsetree type for tactics that wraps these "RedExpr" nodes. (For now: later, if we switch tactics to an immortal notation, we can get rid of this.)
I think we should also solve the syntax of inductive types along with this. For example, (. S1' type) should just be S1'.
Do you have any concrete plan how this should be implemented?
In addition to operators, inductive types themselves and variables, I also want to use the same syntax for specifications for inductive types and normal terms.
@favonia I had a plan for it, but then I realized that it was way harder than I initially thought. I don't want to regurgitate my original plan (because it may not be the best one), but let me just say that we need a representation of RedPRL ASTs which doesn't distinguish between things like variables, metavariables and operators names, which can then be elaborated to the real thing. We should abandon the ast structure from the ABT library.