Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 18:14:03 -0800 (Thu, 03 Feb 2005)
Revision: 6587
Log message:
Yet another instance of the opname_classes branch, merged once again with the
trunk changes and re-branched.
Known issues:
- The .mli opname declarations are added to the .cmoz in the reverse order.
This, among other things causes Failure ("unknown typeclass:
Mmc_base_judgment!Prop") exception on cd'ing into the /mmc_base_judgment
module.
- The .mli opname declarations are added to the .cmoz even when .cmoz has its
own copy. That results in the "ls" output (and other things, such as .cmoz
and .prla files) being unnecessarily cluttered.
- If the same shape is declared several times (possibly with incompatible
types), does anybody notice?
Potential TODOs and RFEs:
- Proper type checking for display forms.
- Could we may be come up with a way to propagate certain declarations from
.ml into .cmiz (instead of the other way around)? Some declarations needs
to stay in the .ml in order to get properly documented.
- "declare sequent" shortcuts:
- when the type is { Term : Term >- Term } : Term, allow omitting it
- when the type is { Term : Term >- Term } : Foo, allow typing just ": Foo"
- Perv!nil/Perv!cons should have the Dform type.
- When the sequent conclusion is omitted, a we should use something other
than Perv!nil for the conclusion. This new "default conclusion" term
should be a member of a singleton type (in the Term typeclass), and MMC
should be using that in the type of Mmc_core_ast!ty_args
- Base_reflection should use its own cons and nil for bterm lists.
- The new stuff (both the new syntax and the typechecking algorithm) need to
be documented.