Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2002-05-11 11:28:23 -0700 (Sat, 11 May 2002)
Revision: 3624
Log message:
Added "input forms" that are the input analogy to display forms.
An iform is declared exactly like a rewrite. An example:
declare junk{'t}
declare magic[v:s]{'t}
iform bind : junk{magic[x:s]{'t}} <--> lambda{x. 't}
# test_rewrite bind << junk{magic[y:s]{.'y +@ 1}} >>;;
- lambda{y.y +@ 1} : term
The difference is this: iforms use the rewriter in Relaxed mode,
where capture is allowed. The rewrites have no logical meaning;
the refiner will not allow you to use one in a proof. However,
they are otherwise normal conversions, and you can add them
to resources etc.
Also, I added a function
val Top_conversionals.create_iform : string -> term -> term -> conv
This will allow us to create rewrites on the fly. I added example
code to mp_mc_compile to illustrate, but I don't know how to
test it.
Adam, you should probably change all rewrites in Mp_mc_fir_phobos to
iforms. Don't use magic (remove that sample code I added). The rewrites
should work as they are written now.