Email Gateway (Aug 22 2022 at 19:48): Email Gateway (Aug 22 2022 at 19:48):From: Dominique Unruh <unruh@ut.ee>
Hi,
I have a string s such as "refl[of x]" and would like to write an ML
function that parses this string and returns the corresponding theorem
(the same theorem that, e.g., the thm command would show, in this case
"x=x").
Note: the string is not known at compile time, so the antiquotation
@{thm refl[of x]} is not what I need. Also, Thm.infer_instantiate is not
what I need because use of "of" is just an example. I want to be able to
use any attribute, e.g., OF, simplified, abs_def, ...
(Proof_Context.get_fact ctxt (Facts.named s) would work if there were no
attributes, but not with attributes.)
I tried the following:
ML ‹
val toks = Token.explode0 (Thy_Header.get_keywords' \<^context>)
"refl[of x]"
val (parsed,leftover) = Scan.catch Parse.thm toks (* [of x] is not
parsed (stays in leftover) *)
val fact = Attrib.eval_thms \<^context> [parsed] (* Gives me
"?t=?t", not "x=x" *)
›
But this does not give me the correct result (see the comments in the ML
source).
What would be the correct approach be?
(Background: I need this for my qrhl-tool
<https://github.com/dominique-unruh/qrhl-tool>. The user can specify the
names of facts on the qrhl-tool side, and the fact is retrieved via
libisabelle from Isabelle.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:48):From: Dominique Unruh <unruh@ut.ee>
Hi,
I have a string s such as "refl[of x]" and would like to write an ML
function that parses this string and returns the corresponding theorem
(the same theorem that, e.g., the thm command would show, in this case
"x=x").
Note: the string is not known at compile time, so the antiquotation
@{thm refl[of x]} is not what I need. Also, Thm.infer_instantiate is not
what I need because use of "of" is just an example. I want to be able to
use any attribute, e.g., OF, simplified, abs_def, ...
(Proof_Context.get_fact ctxt (Facts.named s) would work if there were no
attributes, but not with attributes.)
I tried the following:
ML ‹
val toks = Token.explode0 (Thy_Header.get_keywords' \<^context>)
"refl[of x]"
val (parsed,leftover) = Scan.catch Parse.thm toks (* [of x] is not
parsed (stays in leftover) *)
val fact = Attrib.eval_thms \<^context> [parsed] (* Gives me
"?t=?t", not "x=x" *)
›
But this does not give me the correct result (see the comments in the ML
source).
What would be the correct approach be?
(Background: I need this for my qrhl-tool
<https://github.com/dominique-unruh/qrhl-tool>. The user can specify the
names of facts on the qrhl-tool side, and the fact is retrieved via
libisabelle from Isabelle.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:48):From: Dominique Unruh <unruh@ut.ee>
Hi,
I found a solution by try and error but I would be curious to hear from
an expert whether it is the correct way (it seems somewhat ad-hoc).
ML ‹
val toks = Token.explode0 (Thy_Header.get_keywords' \<^context>)
"refl[of x]" |> filter (not o Token.is_blank) |> (fn t => t @
[Token.eof])
val (parsed,leftover) = Scan.catch Parse.thm toks (* leftover is
[Token.eof] *)
val fact = Attrib.eval_thms \<^context> [parsed] (* Gives "x=x" *)
›
The difference to my failed approach from my previous mail (below) is
that I now filter out all tokens that are spaces after tokenizing
(filter (not o Token.is_blank)).
Additionally, we need to append an EOF (fn t => t @ [Token.eof]) so that
parsing does not fail for strings without attributes (e.g., "refl").
Best wishes,
Dominique.
PS: For completeness, here is the whole thing packaged as an ML
function, with error handling:
fun get_thms ctxt spec = let
val toks = Token.explode0 (Thy_Header.get_keywords' ctxt) spec
|> filter (not o Token.is_blank)
|> (fn t => t @ [Token.eof])
val (parsed,leftover) = Scan.catch Parse.thm toks
val _ = case leftover of [eof] => ()
| _ => error ("Error parsing theorem name \"" ^ spec ^
"\". Leftover tokens: " ^ Pretty.string_of
(Token.pretty_src ctxt leftover))
val fact = Attrib.eval_thms ctxt [parsed]
in fact end
Last updated: Nov 21 2024 at 12:39 UTC