Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 13:38:00 -0700 (Thu, 31 Jul 2003)
Revision: 4797
Log message:
*** WARNING ***
*** This check-in breaks .prlb compatibility ***
*** Export any unsaved proofs to .prla ***
*** before running "cvs update" ***
This is a major change in the way meta-variables work. This commit is supposed
to finally bring the implementation of the rewriter into full argeement with
the on-paper semantics of the sequent schema language and make our implementation
fully valid.
This commit makes sequent contexts binding occurrences and makes all meta-variables
(bot SO variables and sequent contexts) explicitly list all the contexts that can
introduce variables that can occur freely in whatever the meta-variable can match.
For example, f<||>[] can only match closed terms, f<|H|>[] can only match terms whose
only free variables (more specifically - free first-order and context variables) are
those introduced by H.
To avoid having to specify contexts explicitly all the time, the following conventions
are observed:
- in a term (on I/O), the maximal possible contexts are presumed. E.g.
sequent{ <H>; x: A; <J['x]> >- C['x] } is now a shortcut for
sequent{ <H<||>>; x: A<|H|>; <J<|H|>['x]> >- C<|J;H|>['x] }
- in a rule (input only), the terms are scanned top-to-bottom (e.g. conclusion,
then assumptions from last to first, then rule arguments, then whatever terms
are mentioned in resource annotations) and the first time each meta-variable occurs,
its contexts are remembered and copied over all other places where it is used without
contexts being explicitly specified.
For example,
sequent { <H>; <J> >- A } --> sequent { <H>; A; <J> >- C }
will get parsed as ... A <|H|> ... A<|H|> ...
but
sequent { <H>; A; <J> >- C } sequent { <H>; <J> >- A }
will get parsed as ... A <|J;H|> ... A<|J;H|> ...
(as will cause the rule to be rejected by the rewriter since the first sequent
now has a free occurrence of H).
- in a top-loop variables in terms are expanded according to the rule being proven.
for example, if a rule has a s-o variable "v<|H;J|>" in it, then when inside such
a rule, <<'v>> will get parsed as << 'v<|H;J|> >> (and it will get parsed as
a f-o variable v in other rules, where v is not used as a s-o variable). Note
that << lambda{v.'v} >> will still get parsed as << lambda{v.'v} >> (e.g. with v
being a f-o variable), not as << lambda{v. 'v<|H;J|> } >>!
This commit also creates a distinction between 0-arity second-order variables and
free first-order variables. For now (to keep some of the old code happy), the
first-oder variables are considered a special case of second-order variables, but
this will (hopefully) soon go away.
Currently, the free variable computations in TermSubsts return the union of all 3
kinds of variables in a term - free context variables, free f-o variables and all
s-o variables. This is not necessarily the best choice from the semantic standpoint,
but it make the implementation easier. Note that an attempt to substitute something
for a context variable or s-o variable, will produce and Invalid_argument exception.
In the term_std and dest_term'ed representation, v<|contexts|>[terms] is represented
as var[v:v]{[contexts]; terms} where [contexts] is an xlist term with f-o variables
as its leafs.
This commit also refreshes half of the .prla (and simplifies a few proofs). This was
necessary to make sure proofs still expand cleanly.