forked from Isabelle_DOF/Isabelle_DOF
Remove docobj table, instances were moved to a name space
This commit is contained in:
Nicolas Méric
parent
e5a301a3bd
commit
90a6b5aeb2
|
|
@ -222,6 +222,10 @@ struct
|
|||
fun update_instance name instance thy =
|
||||
thy |> Instances.map
|
||||
(Name_Space.define (Context.Theory thy) false (name, instance) #> #2);
|
||||
|
||||
fun update_instance_entry name new_instance thy =
|
||||
thy |> Instances.map
|
||||
(Name_Space.map_table_entry name (fn _ => new_instance));
|
||||
|
||||
fun print_instances verbose ctxt =
|
||||
Pretty.big_list "Isabelle.DOF Instances:"
|
||||
|
|
@ -236,29 +240,6 @@ struct
|
|||
fun the_instance instances i =
|
||||
the_entry_key instances i
|
||||
|
||||
|
||||
type docobj = {pos : Position.T,
|
||||
thy_name : string,
|
||||
input_term : term,
|
||||
value : term,
|
||||
inline : bool,
|
||||
id : serial,
|
||||
cid : string,
|
||||
vcid : string option}
|
||||
|
||||
type docobj_tab ={tab : (docobj option) Symtab.table,
|
||||
maxano : int
|
||||
}
|
||||
|
||||
val initial_docobj_tab:docobj_tab = {tab = Symtab.empty, maxano = 0}
|
||||
|
||||
fun merge_docobj_tab ({tab=otab,maxano=m}, {tab=otab',maxano=m'}) =
|
||||
(let fun X(NONE,NONE) = false
|
||||
|X(SOME _, NONE) = false
|
||||
|X(NONE, SOME _) = false
|
||||
|X(SOME b, SOME b') = true (* b = b' *)
|
||||
in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')}
|
||||
end)
|
||||
type ISA_transformers = {check :
|
||||
(theory -> term * typ * Position.T -> string -> term option),
|
||||
elaborate : (theory -> string -> typ -> term option -> Position.T -> term)
|
||||
|
|
@ -352,31 +333,28 @@ fun the_monitor_instance monitor_instances i =
|
|||
(* registrating data of the Isa_DOF component *)
|
||||
structure Data = Generic_Data
|
||||
(
|
||||
type T = {docobj_tab : docobj_tab,
|
||||
docclass_tab : docclass_tab,
|
||||
type T = {docclass_tab : docclass_tab,
|
||||
ISA_transformer_tab : ISA_transformer_tab,
|
||||
monitor_tab : monitor_tab,
|
||||
docclass_inv_tab : docclass_inv_tab,
|
||||
docclass_eager_inv_tab : docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab : docclass_lazy_inv_tab}
|
||||
val empty = {docobj_tab = initial_docobj_tab,
|
||||
docclass_tab = initial_docclass_tab,
|
||||
val empty = {docclass_tab = initial_docclass_tab,
|
||||
ISA_transformer_tab = initial_ISA_tab,
|
||||
monitor_tab = initial_monitor_tab,
|
||||
docclass_inv_tab = initial_docclass_inv_tab,
|
||||
docclass_eager_inv_tab = initial_docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab
|
||||
}
|
||||
fun merge( {docobj_tab=d1,docclass_tab = c1,
|
||||
fun merge( {docclass_tab = c1,
|
||||
ISA_transformer_tab = e1, monitor_tab=m1,
|
||||
docclass_inv_tab = n1,
|
||||
docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1},
|
||||
{docobj_tab=d2,docclass_tab = c2,
|
||||
{docclass_tab = c2,
|
||||
ISA_transformer_tab = e2, monitor_tab=m2,
|
||||
docclass_inv_tab = n2,
|
||||
docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) =
|
||||
{docobj_tab=merge_docobj_tab (d1,d2),
|
||||
docclass_tab = merge_docclass_tab (c1,c2),
|
||||
{docclass_tab = merge_docclass_tab (c1,c2),
|
||||
(*
|
||||
The following merge is ultra-critical: the transformer tabs were
|
||||
just extended by letting *the first* entry with the same long-name win.
|
||||
|
|
@ -402,59 +380,50 @@ val get_data_global = Data.get o Context.Theory;
|
|||
val map_data_global = Context.theory_map o map_data;
|
||||
|
||||
|
||||
fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab,docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab = f docobj_tab, docclass_tab=docclass_tab,
|
||||
ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab,
|
||||
docclass_eager_inv_tab=docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab=docclass_lazy_inv_tab};
|
||||
|
||||
fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z,
|
||||
fun upd_docclass_tab f {docclass_tab = y,ISA_transformer_tab = z,
|
||||
monitor_tab, docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab,
|
||||
{docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab,
|
||||
docclass_eager_inv_tab=docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab=docclass_lazy_inv_tab};
|
||||
fun upd_ISA_transformers f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z,
|
||||
fun upd_ISA_transformers f {docclass_tab = y,ISA_transformer_tab = z,
|
||||
monitor_tab, docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab,
|
||||
{docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab,
|
||||
docclass_eager_inv_tab=docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab=docclass_lazy_inv_tab};
|
||||
fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
fun upd_monitor_tabs f {docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
{docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = f monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab,
|
||||
docclass_eager_inv_tab=docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab=docclass_lazy_inv_tab};
|
||||
fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
fun upd_docclass_inv_tab f {docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
{docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab,
|
||||
docclass_inv_tab = f docclass_inv_tab,
|
||||
docclass_eager_inv_tab=docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab=docclass_lazy_inv_tab};
|
||||
|
||||
fun upd_docclass_eager_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
fun upd_docclass_eager_inv_tab f {docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
{docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab,
|
||||
docclass_eager_inv_tab=f docclass_eager_inv_tab,
|
||||
docclass_lazy_inv_tab=docclass_lazy_inv_tab};
|
||||
|
||||
fun upd_docclass_lazy_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
||||
fun upd_docclass_lazy_inv_tab f {docclass_tab,ISA_transformer_tab,
|
||||
monitor_tab, docclass_inv_tab,
|
||||
docclass_eager_inv_tab, docclass_lazy_inv_tab} =
|
||||
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
|
||||
{docclass_tab = docclass_tab,
|
||||
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab,
|
||||
docclass_inv_tab=docclass_inv_tab,
|
||||
docclass_eager_inv_tab=docclass_eager_inv_tab,
|
||||
|
|
@ -547,12 +516,12 @@ fun is_declared_oid_global' oid thy =
|
|||
val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy)
|
||||
(get_instances (Proof_Context.init_global thy)) (oid, [Position.none])
|
||||
handle ERROR _ => (("undefined_instance", []), none_instance)
|
||||
|
||||
val _ = writeln ("In define_object_global instance: " ^ \<^make_string> instance)
|
||||
in if oid = undefined_instance andalso instance = none_instance
|
||||
then false
|
||||
else if Long_Name.qualifier oid = Context.theory_name thy
|
||||
else true (*if Long_Name.qualifier oid = Context.theory_name thy
|
||||
then true
|
||||
else false
|
||||
else false*)
|
||||
end
|
||||
|
||||
(*fun is_declared_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy)
|
||||
|
|
@ -729,25 +698,17 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i
|
|||
in map_data_global(upd_docclass_tab(Symtab.update(cid_long,info)))(thy)
|
||||
end
|
||||
|
||||
|
||||
fun define_object_global (oid, bbb) thy =
|
||||
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
|
||||
the space where it is ... *)
|
||||
in if is_defined_oid_global' oid thy
|
||||
then error("multiple definition of document reference")
|
||||
else map_data_global (upd_docobj_tab(fn {tab=t,maxano=x} =>
|
||||
{tab=Symtab.update(oid,SOME bbb) t,
|
||||
maxano=x}))
|
||||
(thy)
|
||||
end
|
||||
|
||||
fun define_object_global' ((oid, pos), bbb) thy =
|
||||
fun define_object_global ((oid, pos), bbb) thy =
|
||||
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
|
||||
the space where it is ... *)
|
||||
|
||||
in if is_declared_oid_global' oid thy
|
||||
then if is_defined_oid_global' oid thy
|
||||
then error("multiple definition of document reference")
|
||||
else update_instance (Binding.make (oid, pos)) (Instance (SOME bbb)) thy
|
||||
(*else update_instance (Binding.make (oid, pos)) (Instance (SOME bbb)) thy*)
|
||||
else let val ((oid', rs), instance) = Name_Space.check_reports (Context.Theory thy)
|
||||
(get_instances (Proof_Context.init_global thy)) (oid, [Position.none])
|
||||
in update_instance_entry oid' (Instance (SOME bbb)) thy end
|
||||
else add_instance (Binding.make (oid, pos)) (Instance (SOME bbb)) thy
|
||||
end
|
||||
|
||||
|
|
@ -1052,15 +1013,10 @@ fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt)
|
|||
in writeln (String.concatWith "," (Symtab.keys tab)) end
|
||||
|
||||
|
||||
fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt)
|
||||
in writeln (String.concatWith "," (Symtab.keys tab)) end
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
fun print_doc_class_tree ctxt P T =
|
||||
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
|
||||
let val {docclass_tab, ...} = get_data ctxt;
|
||||
val class_tab:(string * docclass_struct)list = (Symtab.dest docclass_tab)
|
||||
fun is_class_son X (n, dc:docclass_struct) = (X = #inherits_from dc)
|
||||
fun tree lev ([]:(string * docclass_struct)list) = ""
|
||||
|
|
@ -1390,8 +1346,6 @@ fun elaborate_instances_list thy isa_name _ _ _ =
|
|||
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
|
||||
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
(base_name')
|
||||
val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
|
||||
(*val table_list = Symtab.dest tab*)
|
||||
val table_list = Name_Space.dest_table (DOF_core.get_instances (Proof_Context.init_global thy))
|
||||
fun get_instances_name_list _ [] = []
|
||||
| get_instances_name_list class_name (x::xs) =
|
||||
|
|
@ -2058,7 +2012,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} obinding cid_pos d
|
|||
id = id,
|
||||
cid = cid_long,
|
||||
vcid = vcid})*)
|
||||
|> DOF_core.define_object_global' ((oid, pos), {pos = pos,
|
||||
|> DOF_core.define_object_global ((oid, pos), {pos = pos,
|
||||
thy_name = Context.theory_name thy,
|
||||
input_term = fst value_terms,
|
||||
value = value (Proof_Context.init_global thy)
|
||||
|
|
@ -2526,7 +2480,7 @@ end (* structure Monitor_Command_Parser *)
|
|||
|
||||
ML\<open>
|
||||
fun print_doc_classes b ctxt =
|
||||
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = DOF_core.get_data ctxt;
|
||||
let val {docclass_tab, ...} = DOF_core.get_data ctxt;
|
||||
val _ = writeln "=====================================";
|
||||
fun print_attr (n, ty, NONE) = (Binding.print n)
|
||||
| print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")")
|
||||
|
|
@ -2567,12 +2521,12 @@ val _ =
|
|||
"print document class latex template"
|
||||
(Parse.string >> (fn b => Toplevel.keep (print_docclass_template b o Toplevel.context_of)));
|
||||
|
||||
fun print_doc_items b ctxt =
|
||||
let val {docobj_tab={tab = x, ...},...}= DOF_core.get_data ctxt;
|
||||
fun print_doc_items b ctxt =
|
||||
let val x = DOF_core.get_instances ctxt
|
||||
val _ = writeln "=====================================";
|
||||
fun dfg true = "true"
|
||||
|dfg false= "false"
|
||||
fun print_item (n, SOME({cid,vcid,id,pos,thy_name,inline, input_term, value})) =
|
||||
fun print_item (n, DOF_core.Instance (SOME({cid,vcid,id,pos,thy_name,inline, input_term, value}))) =
|
||||
(writeln ("docitem: "^n);
|
||||
writeln (" type: "^cid);
|
||||
case vcid of NONE => () | SOME (s) =>
|
||||
|
|
@ -2584,9 +2538,9 @@ fun print_doc_items b ctxt =
|
|||
else ());
|
||||
writeln (" value: "^ (Syntax.string_of_term ctxt value))
|
||||
)
|
||||
| print_item (n, NONE) =
|
||||
| print_item (n, DOF_core.Instance NONE) =
|
||||
(writeln ("forward reference for docitem: "^n));
|
||||
in map print_item (Symtab.dest x);
|
||||
in map print_item (Name_Space.dest_table x);
|
||||
writeln "=====================================\n\n\n" end;
|
||||
|
||||
val _ =
|
||||
|
|
@ -2594,8 +2548,9 @@ val _ =
|
|||
(Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of)));
|
||||
|
||||
fun check_doc_global (strict_checking : bool) ctxt =
|
||||
let val {docobj_tab={tab = x, ...}, monitor_tab, ...} = DOF_core.get_data ctxt;
|
||||
val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x)
|
||||
let val {monitor_tab, ...} = DOF_core.get_data ctxt;
|
||||
val x = DOF_core.get_instances ctxt
|
||||
val S = map_filter (fn (s, DOF_core.Instance NONE) => SOME s | _ => NONE) (Name_Space.dest_table x)
|
||||
val T = map fst (Symtab.dest monitor_tab)
|
||||
in if null S
|
||||
then if null T then ()
|
||||
|
|
@ -2621,7 +2576,7 @@ struct
|
|||
|
||||
fun meta_args_exec (meta_args as ((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy =
|
||||
thy |> (if meta_args = Value_Command.empty_meta_args
|
||||
then (K thy)
|
||||
then (K thy)
|
||||
else Context.map_theory (Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline = false}
|
||||
binding (I cid_pos) (I doc_attrs))
|
||||
|
|
|
|||
|
|
@ -1272,8 +1272,9 @@ ML
|
|||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.test_requirement"; \<close>
|
||||
|
||||
ML
|
||||
\<open> val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
|
||||
Symtab.dest ref_tab;
|
||||
\<open> val ref_tab = DOF_core.get_instances \<^context>
|
||||
val {docclass_tab=class_tab,...} = DOF_core.get_data @{context};
|
||||
Name_Space.dest_table ref_tab;
|
||||
Symtab.dest class_tab; \<close>
|
||||
|
||||
ML
|
||||
|
|
|
|||
|
|
@ -25,14 +25,15 @@ print_doc_items
|
|||
|
||||
(* this corresponds to low-level accesses : *)
|
||||
ML\<open>
|
||||
val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...}
|
||||
val docitem_tab = DOF_core.get_instances \<^context>
|
||||
val {docclass_tab, ISA_transformer_tab, monitor_tab,...}
|
||||
= DOF_core.get_data @{context};
|
||||
Symtab.dest docitem_tab;
|
||||
Name_Space.dest_table docitem_tab;
|
||||
Symtab.dest docclass_tab;
|
||||
\<close>
|
||||
ML\<open>
|
||||
val (oid, DOF_core.Instance (SOME {value, ...})) =
|
||||
Name_Space.check (Context.Proof ctxt) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
|
||||
Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
|
||||
\<close>
|
||||
|
||||
find_theorems (60) name:"Conceptual.M."
|
||||
|
|
|
|||
|
|
@ -41,8 +41,9 @@ ODL on a paradigmatical example.
|
|||
|
||||
|
||||
text\<open>Voila the content of the Isabelle_DOF environment so far:\<close>
|
||||
ML\<open>
|
||||
val {docobj_tab={tab = x, ...},docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context};
|
||||
ML\<open>
|
||||
val x = DOF_core.get_instances \<^context>
|
||||
val {docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context};
|
||||
Symtab.dest ISA_transformer_tab;
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue