Re: [isabelle] Isar parser for constant names

On Mon, 19 May 2014, Lars Hupel wrote:

here's what I do for my Isar command:

fun const_raw (..., raw_const) thy =
    val ctxt = Proof_Context.init_global thy
    val (name, _) = Syntax.parse_term ctxt raw_const
     | >  Type.strip_constraints
     | >  dest_Const

    (* ... *)
    (* ... *)

val _ =
    @{command_spec "declassify"}
    "redefines a constant after applying the dictionary construction"
    ((* ... *) -- Parse.const >> (Toplevel.theory o const_raw))

This works with proper markup in Isabelle/jEdit. I'm not sure whether this is the canonical solution, but so far I never got any "unknown constant" exceptions.

It is better than working with raw uninterpreted strings. Going through the full term language is conceptually simple, and often adequate as approximation.

The business of reading just consts, not terms that are mean to be consts, is more delicate. For the next release I have brushed up the canonical functions for that: it will also do the right thing for name space completion. For Isabelle2013-2 the given ProofContext.read_const should do the job.

Note that above the Proof_Context.init_global only makes sense in a global theory context, which seems to be the case here, but that is a special case.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.