[isabelle-dev] Pattern.match -- a minute

[Christian Urban]

Dear Walther,

About your second question: there is a section 
about using the function Pattern.match in the 
Programming Tutorial ([1], Section 3.3). It should  
explain how to do such pattern match examples.
The main contortion below probably comes from the 
parsing of input. Since the antiquotation @{term ...} 
does not allow schematic variables, I written a small
antiquotation @{term_pat ...} that is explained 
section 2.4 and which allows such input terms to
be given directly. All should be conveniently 
referenced.

Hope this helps,
Christian

[1] http://isabelle.in.tum.de/nominal/activities/idp/

Walther Neuper writes:
 > Hi,
 > 
 > re-entering a work done several years ago I now struggle with a simple 
 > detail for an hour -- so apologize the simplistic questions, please:
 > 
 > 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 ?
 > (2) How do I get rid of the error message ?
 > 
 > Thanks a lot,
 > Walther
 > -- 
 > ------------------------------------------------------------------------
 > Walther Neuper                          Mailto: neuper at ist.tugraz.at
 > Institute for Software Technology          Tel: +43-(0)316/873-5728
 > University of Technology                   Fax: +43-(0)316/873-5706
 > Graz, Austria                             Home: www.ist.tugraz.at/neuper
 > ------------------------------------------------------------------------
 > _______________________________________________
 > Isabelle-dev mailing list
 > Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev