support inner syntax cartouches to prevent an error for accent letters in attributes (see hol-testgen/add-ons/Featherweight-OCL/src/compiler_generic/Init.thy )
This commit is contained in:
parent
13db9a9e77
commit
0d96aeb494
79
Isa_DOF.thy
79
Isa_DOF.thy
|
@ -741,12 +741,91 @@ consts ISA_thy :: "string \<Rightarrow> thy" ("@{thy _}")
|
|||
consts ISA_docitem :: "string \<Rightarrow> 'a" ("@{docitem _}")
|
||||
consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a" ("@{docitemattr (_) :: (_)}")
|
||||
|
||||
\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
|
||||
|
||||
ML \<open>
|
||||
(* Author: Frédéric Tuong, Université Paris-Saclay *)
|
||||
(* Title: HOL/ex/Cartouche_Examples.thy
|
||||
Author: Makarius
|
||||
*)
|
||||
local
|
||||
fun mk_char f_char (s, _) accu =
|
||||
fold
|
||||
(fn c => fn (accu, l) =>
|
||||
(f_char c accu,
|
||||
Syntax.const @{const_syntax Cons}
|
||||
$ (Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c)
|
||||
$ l))
|
||||
(rev (map Char.ord (String.explode s)))
|
||||
accu;
|
||||
|
||||
fun mk_string _ accu [] = (accu, Const (@{const_syntax Nil}, @{typ "char list"}))
|
||||
| mk_string f_char accu (s :: ss) = mk_char f_char s (mk_string f_char accu ss);
|
||||
|
||||
in
|
||||
fun string_tr f f_char accu content args =
|
||||
let fun err () = raise TERM ("string_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 $ f (mk_string f_char accu (content (s, pos))) $ p
|
||||
| NONE => err ())
|
||||
| _ => err ())
|
||||
end;
|
||||
end;
|
||||
\<close>
|
||||
|
||||
syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> _" ("_")
|
||||
|
||||
ML\<open>
|
||||
val cartouche_grammar =
|
||||
[ ("char list", snd)
|
||||
, ("String.literal", (fn (_, x) => Syntax.const @{const_syntax STR} $ x))]
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
fun parse_translation_cartouche binding l f_char accu =
|
||||
let val cartouche_type = Attrib.setup_config_string binding (K (fst (hd l)))
|
||||
(* if there is no type specified, by default we set the first element
|
||||
to be the default type of cartouches *) in
|
||||
fn ctxt =>
|
||||
string_tr
|
||||
let val cart_type = Config.get ctxt cartouche_type in
|
||||
case (List.find (fn (s, _) => s = cart_type)
|
||||
l) of
|
||||
NONE => error ("Unregistered return type for the cartouche: \"" ^ cart_type ^ "\"")
|
||||
| SOME (_, f) => f
|
||||
end
|
||||
f_char
|
||||
accu
|
||||
(Symbol_Pos.cartouche_content o Symbol_Pos.explode)
|
||||
end
|
||||
\<close>
|
||||
|
||||
parse_translation \<open>
|
||||
[( @{syntax_const "_cartouche_string"}
|
||||
, parse_translation_cartouche @{binding cartouche_type} cartouche_grammar (K I) ())]
|
||||
\<close>
|
||||
|
||||
|
||||
(* tests *)
|
||||
term "@{typ ''int => int''}"
|
||||
term "@{term ''Bound 0''}"
|
||||
term "@{thm ''refl''}"
|
||||
term "@{docitem ''<doc_ref>''}"
|
||||
ML\<open> @{term "@{docitem ''<doc_ref>''}"}\<close>
|
||||
(**)
|
||||
term "@{typ \<open>int => int\<close>}"
|
||||
term "@{term \<open>Bound 0\<close>}"
|
||||
term "@{thm \<open>refl\<close>}"
|
||||
term "@{docitem \<open><doc_ref>\<close>}"
|
||||
ML\<open> @{term "@{docitem \<open><doc_ref>\<close>}"}\<close>
|
||||
(**)
|
||||
declare [[cartouche_type = "String.literal"]]
|
||||
term "\<open>Université\<close> :: String.literal"
|
||||
declare [[cartouche_type = "char list"]]
|
||||
term "\<open>Université\<close> :: char list"
|
||||
(**)
|
||||
|
||||
|
||||
subsection\<open> Semantics \<close>
|
||||
|
|
Loading…
Reference in New Issue