Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-05 19:55:00 -0800 (Sat, 05 Feb 2005)
Revision: 6606
Log message:
Disallow type constraints rules and rewrites. For type inference,
type rewrites become equalities.
declare rewrite TyElem{TyExp} <--> Exp
This means, in addition to the rewrite, that TyElem{TyExp} = Exp.
So, if we are unifying t1 and t2, it is legal to unify t1 with TyElem{TyExp},
and Exp with t2.
> 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.
These are fixed. Only the declarations that don't exist in the .ml are copied.
> - If the same shape is declared several times (possibly with incompatible
> types), does anybody notice?
This is now checked in Filter_cache_fun.
> Potential TODOs and RFEs:
> - Proper type checking for display forms.
Implemented.
> - 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.
What about copying the documentation from the .mli (preserving the order)?
> - "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"
Implemented.
> - 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.
Implemented.
> - The new stuff (both the new syntax and the typechecking algorithm) need to
> be documented.
I need to do this.