isabelle - 使用 "term parser"解析漩涡花饰的内容

Question

我想在 Isabelle 的漩涡图案中实现一种领域特定语言(带有自己的解析器)。例如，我希望术语 (MY ‹123›, 3) 为子字符串 123 调用我自己的解析器，但将其余部分正常解析为术语。

在 HOL/ex/Cartouche_Examples.thy 之后，我了解了如何为 MY ‹...› 形式的子项安装我自己的解析翻译，以及如何以 string*Position.T 或 Symbol_Pos.T list 的形式获取漩涡花饰的内容。

我还了解如何使用 Isabelle 的解析器组合器编写类型为 term parser 的解析器。

但我找不到如何将解析器应用于字符串(或 Symbol_Pos.T 列表)。

换句话说，我还缺少一个功能

fun parse_cartouche ctx (cartouche:string) (pos:Position.T) : term = ???

将我的 term parser 类型的解析器应用于字符串 cartouche(并正确地向顶层报告解析错误)。

澄清:

• 我想利用 Isabelle 的现有基础架构来跟踪/报告解析位置。例如，如果存在解析错误，我希望代码在 Isabelle/jEdit 中显示为红色，如果在我自己的语言中，我会调用像 Args.parse_term 这样的解析器，我希望 Isabelle/jEdit 颜色变量正确，并通过控制悬停获取类型信息。

• 我不想为 int 等常见事物重新实现自己的解析器，但如果我至少了解了上一个要点，则可以这样做。 (但是，将我的语言的子字符串解析为术语时，我将不得不使用一些现有的解析函数，因为我无法自行重新实现 Isabelle 语法。

---

下面是我到目前为止的完整代码(带有 parse_cartouche 的虚拟实现)。

theory Scratch
imports Main
begin

ML {*
  (* In reality, this would of course be a much more complex parser. *)
  val my_parser : term parser = Parse.nat >> HOLogic.mk_nat

  (* This function should invoke my_parser to parse the content of cartouche.
     Parse errors should be properly reported (i.e., with red highlighting in
    jEdit etc. *)
  fun parse_cartouche ctx (cartouche:string) (pos:Position.T) : term = 
    (warning ("I should parse: " ^ cartouche ^ ". Returning arbitrary term instead"); @{term True})

  (* Modified from Cartouche_Examples.thy *)
  fun cartouche_tr (ctx:Proof.context) args =
      let fun err () = raise TERM ("cartouche_tr", args) in
        (case args of
          [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
            (case Term_Position.decode_position p of
              SOME (pos, _) => c $ (parse_cartouche ctx s pos) $ p
            | NONE => err ())
        | _ => err ())
      end;
*}

syntax "_my_syntax" :: "cartouche_position ⇒ 'a" ("MY_")
parse_translation ‹[(@{syntax_const "_my_syntax"}, cartouche_tr)]›

term "(MY ‹123›, 3)" (* Should parse as (123,3) *)

end

Answer 1

因为这是一个相对罕见的用例，我不确定是否已经出现了“规范”的解决方案。但我至少可以从我自己的代码中给你两个例子，这应该有助于说明一般方法。

ML 代码的评估

source

下面的解析翻译，给定一个函数 eval_term : string -> term，从一个漩涡花饰中提取一些 ML 源，将它评估为一个 term，然后使用它作为解析翻译的结果。

fun term_translation ctxt args =
  let
    fun err () = raise TERM ("Splice.term_translation", args)
    fun input s pos =
      let
        val content = Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))
        val (text, range) = Symbol_Pos.implode_range (Symbol_Pos.range content) content
      in
        Input.source true text range
      end
  in
    case args of
      [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
        (case Term_Position.decode_position p of
          SOME (pos, _) => c $ eval_term (input s pos) ctxt $ p
        | NONE => err ())
    | _ => err ()
end

嵌入 XML

source

这个允许我将 XML 文字嵌入到术语中，然后将其解释为术语。

syntax "_cartouche_xml" :: "cartouche_position \<Rightarrow> 'a"  ("XML _")

parse_translation\<open>
let
  fun translation args =
    let
      fun err () = raise TERM ("Common._cartouche_xml", args)
      fun input s pos = Symbol_Pos.implode (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos)))
      val eval = Codec.the_decode Codec.term o XML.parse
    in
      case args of
        [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
          (case Term_Position.decode_position p of
            SOME (pos, _) => c $ eval (input s pos) $ p
          | NONE => err ())
      | _ => err ()
  end
in
  [(@{syntax_const "_cartouche_xml"}, K translation)]
end
\<close>

---

更新

以下代码应允许您将 Input.source 转换为解析器组合器可消化的内容，包括完整的位置信息:

ML ‹
  val input = ‹term"3 + 4"›;
  (* a bit more complicated than just Input.pos_of because otherwise the position includes the
     outer cartouche brackets, which manifests as an off-by-one-error in the markup *)
  val pos = Input.source_explode input |> Symbol_Pos.range |> Position.range_position;
  val str = Input.source_content input;
  val toks = Token.explode Keyword.empty_keywords pos str;
  val parser = Args.$$$ "term" |-- Args.embedded_inner_syntax;
  parser toks |> fst |> Syntax.read_term @{context}
›