Re: [isabelle] Isar parser for constant names



Hi,

It would be nice to be able to use similar syntax to generate_code,
i.e. have the theory names deduced automatically, so I though I’d make
use of the function Parse.const. However, although this function
parses the constant name to a string, it appears it is not the same
one as passing the function names explicitly as a string, which I
would expect.
Checking what Parse.const does with print statements makes me no
wiser, here it looks OK.

Hipster uses the code generator, and this is where the problem
manifests itself, when I use Parse.const instead of Parse.string:

exception TYPE raised (line 97 of "consts.ML"): Unknown constant:
"TreeDemo.mirror"

here's what I do for my Isar command:

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

    (* ... *)
  in
    (* ... *)
  end

val _ =
  Outer_Syntax.command
    @{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.

Cheers
Lars




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