Email Gateway (Aug 19 2022 at 14:30): Email Gateway (Aug 19 2022 at 14:30):From: Moa Johansson <moa.johansson@chalmers.se>
Hi,
I'm defining a new Isar-command (called hipster) which should take a list of constant names as input. However, I seem to run into some problems. The parser I’ve written so far works fine, but requires me to pass the arguments as strings, which is somewhat ugly, like this:
hipster "TreeDemo.mirror" "TreeDemo.tmap"
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"
despite being in the theory “TreeDemo”, where indeed there is a function mirror. Below is the code for my small parser, if anyone has any tips on some other function I can use to reliably parse constants names, please let me know!
Best,
Moa
let
fun call_hipster consts =
Local_Theory.target
(fn ctxt => fst(Hipster_Explore.explore ctxt consts));
in
Outer_Syntax.local_theory @{command_spec "hipster"}
"Theory Exploration with Hipster”
(* This works OK*)
(* (Scan.repeat1 Parse.string >> call_hipster) *)
(* This cause an error - unknown constant *)
(Scan.repeat1 Parse.const >> call_hipster)
end
Email Gateway (Aug 19 2022 at 14:30):From: Makarius <makarius@sketis.net>
Parse.const is the right thing, but only half of it, namely the outer
syntax parser. You also need an inners syntax "read" function.
Peeking at the implementation of the 'notation' command suggests the
following:
Proof_Context.read_const ctxt false dummyT
Makarius
Email Gateway (Aug 19 2022 at 14:31):From: Lars Hupel <hupel@in.tum.de>
Hi,
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
Email Gateway (Aug 19 2022 at 14:31):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 24 2024 at 20:16 UTC