nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add docitem_name text and ML antiquotations 

Add the possibility to reference the name of instances
in text and ML code
This commit is contained in:
Nicolas Méric 2023-01-30 07:43:44 +01:00
parent 7c6150affa
commit 7c0d2cee55
2 changed files with 29 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/DOF/Isa_DOF.thy
View File

@ -2565,6 +2565,16 @@ fun get_instance_value_2_ML ctxt (oid:string,pos) =
| NONE => error "not an object id"
in ML_Syntax.print_term value end
fun get_instance_name_2_ML ctxt (oid:string,pos) =
let val ctxt' = Context.the_proof ctxt
val _ = case DOF_core.get_object_local oid ctxt' of
SOME({pos=pos_decl,id,...}) =>
let val markup = docref_markup false oid id pos_decl
val _ = Context_Position.report ctxt' pos markup
in () end
| NONE => error "not an object id"
in "\"" ^ oid ^ "\"" end
fun trace_attr_2_ML ctxt (oid:string,pos) =
let val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string
val toML = (ML_Syntax.atomic o (ML_Syntax.print_list print_string_pair))
@ -2574,6 +2584,15 @@ fun compute_cid_repr ctxt cid pos =
if DOF_core.is_defined_cid_local cid ctxt then Const(cid,dummyT)
else ISA_core.err ("Undefined Class Identifier:"^cid) pos
fun compute_name_repr ctxt oid pos =
let val _ = case DOF_core.get_object_local oid ctxt of
SOME({pos=pos_decl,id,...}) =>
let val markup = docref_markup false oid id pos_decl
val _ = Context_Position.report ctxt pos markup
in () end
| NONE => error "not an object id"
in HOLogic.mk_string oid end
local
fun pretty_attr_access_style ctxt (style, ((attr,pos),(oid,pos'))) =
@ -2582,6 +2601,10 @@ fun pretty_attr_access_style ctxt (style, ((attr,pos),(oid,pos'))) =
fun pretty_trace_style ctxt (style, (oid,pos)) =
Document_Output.pretty_term ctxt (style (ISA_core.compute_attr_access (Context.Proof ctxt)
"trace" oid NONE pos));
fun pretty_name_style ctxt (style, (oid,pos)) =
Document_Output.pretty_term ctxt (style (compute_name_repr ctxt oid pos))
fun pretty_cid_style ctxt (style, (cid,pos)) =
Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos));
@ -2612,10 +2635,13 @@ val _ = Theory.setup
(fn (ctxt,toks) => (parse_attribute_access >> attr_2_ML ctxt) (ctxt, toks)) #>
ML_Antiquotation.inline \<^binding>\<open>trace_attribute\<close>
(fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #>
ML_Antiquotation.inline \<^binding>\<open>docitem_name\<close>
(fn (ctxt,toks) => (parse_oid >> get_instance_name_2_ML ctxt) (ctxt, toks)) #>
basic_entity \<^binding>\<open>trace_attribute\<close> parse_oid' pretty_trace_style #>
basic_entity \<^binding>\<open>doc_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>onto_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>docitem_attribute\<close> parse_attribute_access' pretty_attr_access_style
basic_entity \<^binding>\<open>docitem_attribute\<close> parse_attribute_access' pretty_attr_access_style #>
basic_entity \<^binding>\<open>docitem_name\<close> parse_oid' pretty_name_style
)
end
end

3
src/tests/TermAntiquotations.thy
View File

@ -91,11 +91,12 @@ update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
text\<open>And here is the results of some ML-term antiquotations:\<close>
ML\<open> @{docitem_attribute b::xcv4} \<close>
ML\<open> @{docitem xcv4} \<close>
ML\<open> @{docitem_name xcv4} \<close>
ML\<open> @{trace_attribute aaa} \<close>
text\<open>Now we might need to reference a class instance in a term command and we would like
Isabelle to check that this instance is indeed an instance of this class.
Here, we want to reference the instance @{docitem \<open>xcv4\<close>} previously defined.
Here, we want to reference the instance @{docitem_name "xcv4"} previously defined.
We can use the term* command which extends the classic term command
and does the appropriate checking.\<close>
term*\<open>@{F \<open>xcv4\<close>}\<close>