class-term-antiquotation-implementation #2
|
@ -41,6 +41,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
"define_shortcut*" "define_macro*" :: thy_decl
|
||||
|
||||
and "text*" "text-macro*" :: document_body
|
||||
and "term*" :: diag
|
||||
|
||||
and "print_doc_classes" "print_doc_items"
|
||||
"print_doc_class_template" "check_doc_global" :: diag
|
||||
|
@ -184,7 +185,7 @@ struct
|
|||
in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')}
|
||||
end)
|
||||
|
||||
type ISA_transformer_tab = (theory -> term * typ * Position.T -> term option) Symtab.table
|
||||
type ISA_transformer_tab = (theory -> term * typ * Position.T -> string -> term option) Symtab.table
|
||||
val initial_ISA_tab:ISA_transformer_tab = Symtab.empty
|
||||
|
||||
type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table
|
||||
|
@ -223,7 +224,13 @@ structure Data = Generic_Data
|
|||
docclass_inv_tab = n2}) =
|
||||
{docobj_tab=merge_docobj_tab (d1,d2),
|
||||
docclass_tab = merge_docclass_tab (c1,c2),
|
||||
ISA_transformer_tab = Symtab.merge (fn (_ , _) => false)(e1,e2),
|
||||
(*
|
||||
The following merge is ultra-critical: the transformer tabs were
|
||||
just extended by letting *the first* entry with the same long-name win.
|
||||
Since the range is a (call-back) function, a comparison on its content
|
||||
is impossible and some choice has to be made... Alternative: Symtab.join ?
|
||||
*)
|
||||
ISA_transformer_tab = Symtab.merge (fn (_ , _) => true)(e1,e2),
|
||||
monitor_tab = override(m1,m2),
|
||||
(* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*)
|
||||
docclass_inv_tab = override(n1,n2)
|
||||
|
@ -579,7 +586,26 @@ fun update_value_global oid upd thy =
|
|||
| NONE => error("undefined doc object: "^oid)
|
||||
|
||||
|
||||
val ISA_prefix = "Isa_DOF.ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *)
|
||||
val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *)
|
||||
|
||||
val doc_class_prefix = ISA_prefix ^ "doc_class_"
|
||||
|
||||
fun is_ISA s = String.isPrefix ISA_prefix (Long_Name.base_name s)
|
||||
|
||||
fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_prefix), NONE)
|
||||
|
||||
fun get_doc_class_name_without_ISA_prefix s = String.extract (s, String.size(ISA_prefix), NONE)
|
||||
|
||||
fun is_class_ISA thy s = let val bname = Long_Name.base_name s
|
||||
val qual = Long_Name.qualifier s
|
||||
in
|
||||
if String.isPrefix doc_class_prefix bname then
|
||||
let
|
||||
val class_name =
|
||||
Long_Name.qualify qual (get_class_name_without_prefix bname)
|
||||
in
|
||||
is_defined_cid_global (class_name) thy end
|
||||
else false end
|
||||
|
||||
fun get_isa_global isa thy =
|
||||
case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of
|
||||
|
@ -591,20 +617,24 @@ fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data
|
|||
NONE => error("undefined inner syntax antiquotation: "^isa)
|
||||
|SOME(bbb) => bbb
|
||||
|
||||
fun update_isa_local (isa, trans) ctxt =
|
||||
map_data (upd_ISA_transformers(Symtab.update(ISA_prefix^isa,trans))) ctxt
|
||||
fun update_isa map_data_fun (isa, trans) ctxt =
|
||||
let
|
||||
val bname = Long_Name.base_name isa;
|
||||
val qual = Long_Name.qualifier isa;
|
||||
val long_name = Long_Name.qualify qual (ISA_prefix ^ bname);
|
||||
in map_data_fun (upd_ISA_transformers(Symtab.update(long_name, trans))) ctxt end
|
||||
|
||||
fun update_isa_global (isa, trans) thy =
|
||||
map_data_global (upd_ISA_transformers(Symtab.update(ISA_prefix^isa,trans))) thy
|
||||
fun update_isa_local (isa, trans) ctxt = update_isa map_data (isa, trans) ctxt
|
||||
|
||||
fun update_isa_global (isa, trans) thy = update_isa map_data_global (isa, trans) thy
|
||||
|
||||
fun transduce_term_global (term,pos) thy =
|
||||
(* pre: term should be fully typed in order to allow type-related term-transformations *)
|
||||
let val tab = #ISA_transformer_tab(get_data_global thy)
|
||||
fun T(Const(s,ty) $ t) = if String.isPrefix ISA_prefix s
|
||||
fun T(Const(s,ty) $ t) = if is_ISA s
|
||||
then case Symtab.lookup tab s of
|
||||
NONE => error("undefined inner syntax antiquotation: "^s)
|
||||
| SOME(trans) => (case trans thy (t,ty,pos) of
|
||||
| SOME(trans) => (case trans thy (t,ty,pos) s of
|
||||
NONE => Const(s,ty) $ t
|
||||
(* checking isa, may raise error though. *)
|
||||
| SOME t => Const(s,ty) $ t)
|
||||
|
@ -873,7 +903,7 @@ fun ML_isa_antiq check_file thy (name, _, pos) =
|
|||
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
|
||||
|
||||
|
||||
fun ML_isa_check_generic check thy (term, pos) =
|
||||
fun ML_isa_check_generic check thy (term, pos) _ =
|
||||
let val name = (HOLogic.dest_string term
|
||||
handle TERM(_,[t]) => error ("wrong term format: must be string constant: "
|
||||
^ Syntax.string_of_term_global thy t ))
|
||||
|
@ -881,39 +911,56 @@ fun ML_isa_check_generic check thy (term, pos) =
|
|||
in SOME term end;
|
||||
|
||||
|
||||
fun ML_isa_check_typ thy (term, _, pos) =
|
||||
fun ML_isa_check_typ thy (term, _, pos) s =
|
||||
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
|
||||
in (Syntax.check_typ ctxt o Syntax.parse_typ ctxt) name end
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
|
||||
fun ML_isa_check_term thy (term, _, pos) =
|
||||
fun ML_isa_check_term thy (term, _, pos) s =
|
||||
let fun check thy (name, _) = let val ctxt = (Proof_Context.init_global thy)
|
||||
in (Syntax.check_term ctxt o Syntax.parse_term ctxt) name end
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
|
||||
fun ML_isa_check_thm thy (term, _, pos) =
|
||||
fun ML_isa_check_thm thy (term, _, pos) s =
|
||||
(* this works for long-names only *)
|
||||
let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of
|
||||
NONE => err ("No Theorem:" ^name) pos
|
||||
| SOME X => X
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
|
||||
fun ML_isa_check_file thy (term, _, pos) =
|
||||
fun ML_isa_check_file thy (term, _, pos) s =
|
||||
let fun check thy (name, pos) = check_path (SOME File.check_file)
|
||||
(Proof_Context.init_global thy)
|
||||
(Path.current)
|
||||
(name, pos);
|
||||
in ML_isa_check_generic check thy (term, pos) end;
|
||||
in ML_isa_check_generic check thy (term, pos) s end;
|
||||
|
||||
fun check_instance thy (term, _, pos) s =
|
||||
let
|
||||
val bname = Long_Name.base_name s;
|
||||
val qual = Long_Name.qualifier s;
|
||||
val class_name =
|
||||
Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE));
|
||||
fun check thy (name, _) =
|
||||
let
|
||||
val object_cid = case DOF_core.get_object_global name thy of
|
||||
NONE => err ("No class instance:" ^ name) pos
|
||||
| SOME(object) => #cid object
|
||||
fun check' (class_name, object_cid) =
|
||||
if class_name = object_cid then
|
||||
DOF_core.get_value_global name thy
|
||||
else err (name ^ " is not an instance of " ^ class_name) pos
|
||||
in check' (class_name, object_cid) end;
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
fun ML_isa_id thy (term,pos) = SOME term
|
||||
|
||||
|
||||
fun ML_isa_check_docitem thy (term, req_ty, pos) =
|
||||
let fun check thy (name, _) =
|
||||
fun ML_isa_check_docitem thy (term, req_ty, pos) s =
|
||||
let fun check thy (name, _) s =
|
||||
if DOF_core.is_declared_oid_global name thy
|
||||
then case DOF_core.get_object_global name thy of
|
||||
NONE => warning("oid declared, but not yet defined --- "^
|
||||
|
@ -930,7 +977,35 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) =
|
|||
else ()
|
||||
end
|
||||
else err ("faulty reference to docitem: "^name) pos
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
(*
|
||||
The function declare_ISA_class_accessor_and_check_instance uses a prefix
|
||||
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
|
||||
by add_doc_class_cmd function
|
||||
*)
|
||||
fun declare_ISA_class_accessor_and_check_instance doc_class_name =
|
||||
let
|
||||
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
|
||||
val typestring = "string => " ^ (Binding.name_of doc_class_name)
|
||||
(* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
we can not use "_" for classes names in term antiquotation.
|
||||
We chose to convert "_" to "-".*)
|
||||
val conv_class_name = String.translate (fn #"_" => "-"
|
||||
| x => String.implode [x] )
|
||||
(Binding.name_of doc_class_name)
|
||||
val mixfix_string = "@{" ^ conv_class_name ^ " _}"
|
||||
in
|
||||
Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))]
|
||||
#> (fn thy => let
|
||||
val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name)
|
||||
(*val bname = Long_Name.base_name long_name*)
|
||||
val qual = Long_Name.qualifier long_name
|
||||
val class_name = Long_Name.qualify qual
|
||||
(DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind))
|
||||
in
|
||||
DOF_core.update_isa_global(class_name, check_instance) thy end)
|
||||
end
|
||||
|
||||
(* utilities *)
|
||||
|
||||
|
@ -946,12 +1021,12 @@ end; (* struct *)
|
|||
|
||||
subsection\<open> Isar - Setup\<close>
|
||||
|
||||
setup\<open>DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("term" ,ISA_core.ML_isa_check_term) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("term_repr",fn _ => fn (t,_,_) => SOME t) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("thm" ,ISA_core.ML_isa_check_thm) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("file" ,ISA_core.ML_isa_check_file) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("docitem" ,ISA_core.ML_isa_check_docitem)\<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.typ" ,ISA_core.ML_isa_check_typ) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.term" ,ISA_core.ML_isa_check_term) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.term_repr",fn _ => fn (t,_,_) => fn _ => SOME t) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.thm" ,ISA_core.ML_isa_check_thm) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.file" ,ISA_core.ML_isa_check_file) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.docitem" ,ISA_core.ML_isa_check_docitem)\<close>
|
||||
|
||||
section\<open> Syntax for Annotated Documentation Commands (the '' View'' Part I) \<close>
|
||||
|
||||
|
@ -1386,6 +1461,39 @@ val _ =
|
|||
(attributes -- Parse.opt_target -- Parse.document_source
|
||||
>> (Toplevel.theory o (gen_enriched_document_cmd {inline=true} I I {markdown = true} )));
|
||||
|
||||
(*
|
||||
term* command uses the same code as term command
|
||||
and adds the possibility to check Term Annotation Antiquotations (TA)
|
||||
with the help of DOF_core.transduce_term_global function
|
||||
*)
|
||||
fun string_of_term ctxt s trans =
|
||||
let
|
||||
val t = Syntax.read_term ctxt s;
|
||||
val T = Term.type_of t;
|
||||
val ctxt' = Proof_Context.augment t ctxt;
|
||||
val _ = DOF_core.transduce_term_global (t , Toplevel.pos_of trans)
|
||||
(Proof_Context.theory_of ctxt');
|
||||
in
|
||||
Pretty.string_of
|
||||
(Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
|
||||
end;
|
||||
|
||||
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
|
||||
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
|
||||
|
||||
(*
|
||||
We want to have the current position to pass it to transduce_term_global in
|
||||
string_of_term, so we pass the Toplevel.transition
|
||||
*)
|
||||
fun print_term (string_list, string) trans = print_item
|
||||
(fn state => fn string => string_of_term (Toplevel.context_of state) string trans)
|
||||
(string_list, string) trans;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
||||
(opt_modes -- Parse.term >> print_term);
|
||||
|
||||
(* This is just a stub at present *)
|
||||
val _ =
|
||||
Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro"
|
||||
|
@ -1816,6 +1924,12 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
|||
|> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy)
|
||||
(* defines the ontology-checked text antiquotation to this document class *)
|
||||
|> (fn thy => fold(define_inv (cid thy)) (invariants) thy)
|
||||
(*
|
||||
The function declare_ISA_class_accessor_and_check_instance uses a prefix
|
||||
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
|
||||
by add_doc_class_cmd function
|
||||
*)
|
||||
|> ISA_core.declare_ISA_class_accessor_and_check_instance binding
|
||||
end;
|
||||
|
||||
val parse_invariants = Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)
|
||||
|
|
|
@ -84,5 +84,24 @@ ML\<open> @{docitem_attribute b::xcv4} \<close>
|
|||
ML\<open> @{docitem 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.
|
||||
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>
|
||||
|
||||
text\<open>We can also reference an attribute of the instance.
|
||||
Here we reference the attribute r of the class F which has the type @{typ \<open>thm list\<close>}.\<close>
|
||||
term*\<open>r @{F \<open>xcv4\<close>}\<close>
|
||||
|
||||
text\<open>We declare a new text element. Note that the class name contains an underscore "_".\<close>
|
||||
text*[te::text_element]\<open>Lorem ipsum...\<close>
|
||||
|
||||
text\<open>Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
this term antiquotation has to be denoted like this: @{term\<open>@{text-element \<open>ee\<close>}\<close>}.
|
||||
We need to substitute an hyphen "-" for the underscore "_".\<close>
|
||||
term*\<open>@{text-element \<open>te\<close>}\<close>
|
||||
|
||||
end
|
||||
|
||||
|
|
Loading…
Reference in New Issue