[isabelle-dev] Pattern.match -- a minute
Makarius
makarius at sketis.net
Wed Mar 3 12:24:17 CET 2010
On Wed, 3 Mar 2010, Walther Neuper wrote:
> theory Test
> imports Complex_Main
> begin
> ML {*
> val thy = @{theory Complex_Main};
> val parse = Syntax.read_term_global thy;
> val (pa, tm) = (parse "a + b::real", parse "x + 2*z::real");
> val (tye, tme) =
> (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
> Pattern.match thy (pa, tm) (tye, tme);
> *}
> end
>
> ... raises:
> *** Exception- TOPLEVEL_ERROR raised
> *** At command "ML".
>
> Questions:
> (1) How can I get better error messages ?
By using the official Isabelle2009-1 distribution with Poly/ML 5.3.0 you
should get something like this in the very beginning:
*** exception MATCH raised (line 368 of "pattern.ML")
...
You can also say ML "Toplevel.debug := true" to get even more information.
> (2) How do I get rid of the error message ?
By making pa a pattern with schematic variables, not free ones.
Since this is a "global" example for now, you can use Logic.varify
(although that does not work in general local situations, where parts are
fixed and parts are arbitrary).
Makarius
More information about the isabelle-dev
mailing list