Hello,
Here's another one of my design rants...
Here's another problem we have in Typer: currently error messages will often print types as some horrendous unintelligible expression. This was made worse by my change to make builtins "closed", since now `List` is not shown as `List` any more but as
let List : Type -> Type; List = inductive_ (List t) nil (cons t (List t)) in List
or some less pretty rendition thereof.
I have some idea for how to improve this, e.g. when printing a `lexp`, we should look up some hash-table which will give some candidate var-name, then confirm in the lexp_context that this var's name indeed is equivalent to the lexp we're trying to print.
[ Of course, a hash-table indexed by a `lexp` is a problem in itself, since a given `lexp` can/will be different depending on the context in which it appears (because of debruijn indices being adjusted). But that's a problem we will need to solve somehow anyway. ]
But that's just the beginning of our problems. E.g. Let's say we have a `Tree` module, whose type would be `Set.t`. In reality, `Tree.t` is actually a macro call (i.e. it's equivalent to `__.__ Tree t` which would presumably expand to something like `case Tree | cons (t := x) => x`) which will select the first `t` from the value `Tree`.
So now, how do I go back from the `lexp` that represents this tree type (which will probably look like some `let Tree = ... in Tree` or something even more cumbersome) to `Tree.t`?
It seems this calls for an even more general "reverse lparse" hash-table, which maps all lexps we have elaborated back to their corresponding source code (probably as an sexp since pexp is on the way of the dodo), so that when we try to print a lexp, we look this up in the table to see if this lexp actually existed in the source code and use that source's format.
Hmm... maybe, instead of a hash-table, we should "simply" replace the `location` info (currently file+line+column) with a reference to the corresponding source sexp.
Admittedly, this is not as simple as it sounds: some of the manipulations we do on `lexp` will result in an `lexp` that's not equivalent to any of the `sexps` we got, so either we dynamically try to create a corresponding `sexp`, or this "original sexp" data should be optional.
And it won't solve our `Tree.t` problem, since the tree type returned by (say) `Tree.insert` was not elaborated from `Tree.t` but from the representation used before creating the `Tree` module/object.
A different avenue might be to provide some primitive that the __.__ macro could use to "register" the `Tree.t` sexp in some hash-table, so that if we later see the same type we can know that it can *also* be referred to as `Tree.t` even when this occurrence of the type wasn't originally elaborated from a source code of the form `Tree.t`.
Stefan