Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-07-04 19:34:48 -0700 (Sun, 04 Jul 1999)
Revision: 2778
Log message:
Added Itt_sort for Alexey's demo. Reading the .prla file is _really_ slow
so I added the .prlb file as well. We known that normalization is exponential:
do we have to add a number to every term, or can we be smarter?
In Base_dtactic I added two options:
IntroArgsOption of (tactic_arg -> term -> term list) * term option
ElimArgsOption of (tactic_arg -> term -> term list) * term option
The function computes the term arguments for the rule, and the term option
specifies the subterm to pass. Example:
interactive applyMember {| intro_resource [IntroArgsOption (infer_type_args, << 'f >>)] |} 'H ('A -> 'B) :
[wf] sequent [squash] { 'H >- member{.'A -> 'B; 'f} } -->
...
sequent ['ext] { 'H >- member{'T; .'f 'a} }
This would use the type inference function "infer_type_args" to infer the type for 'f
and use it as the term argument ('A -> 'B). Of course, the refiner will complain if
the infered type is not a simple function type.
This is only used in Itt_sort right now, and it is experimental. We want
an option like this because type inference is such a common requirement.
But this specification is too ad-hoc, and I will think about it further
(suggestions welcome).