[isabelle-dev] use term patterns, was: 'produce term patterns'
Walther Neuper
neuper at ist.tugraz.at
Thu Sep 30 16:25:36 CEST 2010
Thanks to the help of several developers our database (of types of
equations etc) can be parsed again !
Now we are going to use this database, and again we have problems with
different behavior of Isabelle2009-2:
Given
val t = @{term "a + b * x = (0 ::real)"};
val pat = parse_patt thy "?l = (?r ::real)";
val precond = @{term "l is_polynomial"};
we match
val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
in order to get an environment for instantiating the precondition
val preinst = Envir.subst_term inst precond;
to "(a + b * x) is_polynomial"; but we have still 'preinst = precond'.
Studying pattern.ML and envir.ML did not help.
Any help is appreciated !
Walther
PS:
(1) The environment '[(l, a+b*x), (r, 0)]' looks like ready to use:
val inst =
(Empty,
Branch3
(Empty,
(("l", 0),
("RealDef.real",
Const ("Groups.plus_class.plus",
"RealDef.real => RealDef.real => RealDef.real") $
Free ("a", "RealDef.real") $
(Const ("Groups.times_class.times",
"RealDef.real => RealDef.real => RealDef.real") $
Free ("b", "RealDef.real") $ Free ("x", "RealDef.real")))),
Empty,
(("r", 0),
("RealDef.real", Const ("Groups.zero_class.zero", "RealDef.real"))),
Empty))
: Type.tyenv * Envir.tenv
(2) val precond = parse_patt thy "?l is_polynomial"; produces
*** exception TYPE raised (line 109 of "envir.ML"):
*** Variable "?l" has two distinct types
*** real
*** ?'a1 => ?'b1
What is going on here ?
On 09/03/2010 02:19 PM, Walther Neuper wrote:
> Makarius,
>
> thanks for the warning ...
>
> On 09/03/2010 01:31 PM, Makarius wrote:
>> On Fri, 3 Sep 2010, Walther Neuper wrote:
>> [...]
>>> That is exactly what we need, ...
>>>
>>> ML {* print_depth 99;
>>> val ctxt = ProofContext.init_global @{theory};
>>> ProofContext.read_term_pattern ctxt "matches (?a + ?b * bdv^2 =
>>> (0::real)) equ";
>>> *}
>>
>> BTW, the "global" in ProofContext.init_global indicates that this is a
>> somewhat unusual operation to be used only as last resort, when no
>> proper local context is available. Here you have one, which is the
>> context of the 'ML' command.
>>
> ... but we are still struggling to bring the old code alive in the
> Isabelle2009 world. If the code runs again, then we shall take advantage
> of all the wonderful services of present Isabelle and then with pleasure
> follow your recommendations ...
>
>> So you really should use proper @{context} here, not the raw
>> background @{theory}. Of course, these antiquotations only work for
>> individual tests -- the context is that of the compile-time of the ML
>> command. In production code you need to abstract over the "ctxt",
>> passing through the value that you get from the surrounding system
>> infrastructure (i.e. concrete syntax wrappers of proof methods etc.).
>>
>> Makarius
> Walther
More information about the isabelle-dev
mailing list