Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-05-23 14:55:17 -0700 (Sun, 23 May 1999)
Revision: 2669
Log message:
This is a major modification to how parameters are handled.
1. All level parmeters are now meta. That is, univ[@i:l] is
exactly the same as univ[i:l]. The rewriter handles
lavel expressions, so matching with levels like
univ[3 | i':l | j:l] should work correctly.
The syntax still requires the @ for meta-parameter of
other types. For instance, token["hello world":t] is
a normal token, and token[@"hello world":t] is a
token with a meta-parameter.
2. There are no more parameter expressions. For instance,
the term natural_number[@i + @j] is not valid anymore.
To replace them, the module theories/base/base_meta.ml
defines ML rewrites that implement the same functionality.
For example,
meta_sum{number[12]; number[5]} --> number[17]
3. There is no term natural_number[@i:n] any more. This was
always a bad name, since it has always been possible for the
parameter to be negative.
4. The Itt_equal.cumulativity rule is no longer defined as a
side-condition. It now uses Base_meta.meta_lt to define
inclusion on level expression. Cumulativity expansion
should be performed automatically by the dT tactic.
So:
sequent ['ext] { ... >- univ[@i:l] = univ[@i:l] in univ[@j:l] }
BY dT 0
should always either succeed or fail, without producing
subgoals.
I haven't fully tested the side-conditions. As usual, let me know
if you see anything strange. Next, I'm looking at the
rewriter free variable soundness problem.