Re: [isabelle] Getting a fact with attributes from ML


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 @
   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,

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

On 5/7/19 7:36 PM, Dominique Unruh wrote:


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 <>. The user can specify the names of facts on the qrhl-tool side, and the fact is retrieved via libisabelle from Isabelle.)

Best wishes,

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