Parse AST translation patterns · Isabelle/ML

Hi all. I am having issues with translations for a custom, non-logic nonterminal. I've boiled down to the following 'surprising' behavior of Syntax_Phases.parse_ast_pattern processing LHS & RHS of translations patterns:

nonterminal foo
syntax
  "_id_as_foo" :: "id ⇒ foo"
  "_id_as_foo_with_syntax" :: "id ⇒ foo" ("FOO'_ID _")
  "_id_as_logic" :: "id ⇒ logic"
  "_foo_to_logic" :: "foo ⇒ logic"

ML‹
  val ctxt = @{context}
  val get_syn_ty = #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
  val foo_ty = get_syn_ty "foo"
  val logic_ty = get_syn_ty "logic"

  (* FAIL: *)
  (* val ast0 = Syntax_Phases.parse_ast_pattern ctxt (foo_ty, "_id_as_foo x") *)
  (* OK (!) *)
  val ast1 = Syntax_Phases.parse_ast_pattern ctxt (logic_ty, "_foo_to_logic (_id_as_foo x)")
  (* FAIL: *)
  (* val ast2 = Syntax_Phases.parse_ast_pattern ctxt (foo_ty, "_id_as_foo_with_syntax x") *)
  (* OK: *)
  val ast3 = Syntax_Phases.parse_ast_pattern ctxt (foo_ty, "FOO_ID x")
  (* FAIL (!) *)
  (* val ast4 = Syntax_Phases.parse_ast_pattern ctxt (logic_ty, "_foo_to_logic (FOO_ID x)") *)
  (* OK: *)
  val ast5 = Syntax_Phases.parse_ast_pattern ctxt (logic_ty, "_id_as_logic x")

Can someone explain what's going on here? Why, for example, would _id_as_foo x fail to parse, while _foo_to_logic (_id_as_foo x) succeeds? Any why does replacing _id_as_foo x by concrete syntax help? I am very puzzled.

Stream: Isabelle/ML

Topic: Parse AST translation patterns

Hanno Becker (Aug 08 2023 at 06:05):