Yes, I noticed. I think I solved most of the issues in my next commit. I have an issue with attributes. It seems the context is not allowed to change when adding attributes. (Test "Implicit Arguments").
Don't know what you mean by "context is not allowed to change". Maybe it's related to my comment:
(* FIXME: We need to have something in lexp to represent this * add-attribute operation! *)
Nevertheless, the test about attributes is working. I am still investigating on the issue.
One thing that occurred to me is that maybe this attribute business is not needed. More specifically, instead of
greater-than = new-attribute (Int -> Bool); [...] attribute w greater-than (lambda (y : Int) -> True);"
being special declarations, we should just macro-expand them to
attribute_greater-than_table : lexp-table (Int -> Bool); attribute_greater-than_table = lexp-table-empty; [...] attribute_greater-than_table = lexp-table-add attribute_greater-than_table w (lambda (y : Int) -> True)
For that we need to implement the `lexp-table` data type, which would be an associative table indexed by lexps. And the main difference would be that the lookup would be done based on the *value* of `w` rather than based on the identity of the variable itself (and similarly, the `greater-than` would be treated as a *string* rather than referring to a particular variable).
Another thing I've been thinking about has to do with naming conventions:
- we need a special name-space for builtin thingies. E.g. when we print a "Sort (...)" usually it can be printed as "Type" or "Type1" but these vars may be hidden. We currently print them as "<Type>" or some such, but it's not an "official" syntax. I think we need an official syntax (one that works when reading a program) that stands for "builtin". It could be "##..." or "<...>" (i.e. a special naming convention) or "(## ...)" or the "(built-in ...)" we currently use. The important thing is that it should also be usable to represent the Sort(...) and SortLevel(...) lexps. And it should be sufficiently concise to be tolerable in printed output. I'm leaning towards "##" so we'd write "##Type ##0", "##Type (##S ##0)", "##+", "##TypeLevel", ... OTOH, since I plan on using "." for module-field names, we could use a ".." prefix and write things like "..Type ..0".
- For explicitly written metavariables (i.e. wholes that will be filled via type-inference), I was thinking of using the "?" prefix. So you could write:
foo : ?; bar : ?; foo = ...; bar = ...;
to declare that foo and bar are mutually-exclusive without specifying their type. And those metavars would be automatically generalized (as usual in Hindley-Milner type inference), so you could write:
identity : ?a -> ?a;
instead of
identity : (a : Type) ≡> a -> a; or identity : (a : ?) ≡> a -> a;
But admittedly, for such type declarations we could also accept
identity : a -> a;
if "a" is not in the context (yet).
Stefan