From 7c0d2cee55e3a3d45262a09a3518192bf710775b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 30 Jan 2023 07:43:44 +0100 Subject: [PATCH 01/18] Add docitem_name text and ML antiquotations Add the possibility to reference the name of instances in text and ML code --- src/DOF/Isa_DOF.thy | 28 +++++++++++++++++++++++++++- src/tests/TermAntiquotations.thy | 3 ++- 2 files changed, 29 insertions(+), 2 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 42da6d2..146e05c 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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>\trace_attribute\ (fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #> + ML_Antiquotation.inline \<^binding>\docitem_name\ + (fn (ctxt,toks) => (parse_oid >> get_instance_name_2_ML ctxt) (ctxt, toks)) #> basic_entity \<^binding>\trace_attribute\ parse_oid' pretty_trace_style #> basic_entity \<^binding>\doc_class\ parse_cid' pretty_cid_style #> basic_entity \<^binding>\onto_class\ parse_cid' pretty_cid_style #> - basic_entity \<^binding>\docitem_attribute\ parse_attribute_access' pretty_attr_access_style + basic_entity \<^binding>\docitem_attribute\ parse_attribute_access' pretty_attr_access_style #> + basic_entity \<^binding>\docitem_name\ parse_oid' pretty_name_style ) end end diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy index 2a0a01f..78069a2 100644 --- a/src/tests/TermAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -91,11 +91,12 @@ update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"] text\And here is the results of some ML-term antiquotations:\ ML\ @{docitem_attribute b::xcv4} \ ML\ @{docitem xcv4} \ +ML\ @{docitem_name xcv4} \ ML\ @{trace_attribute aaa} \ text\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 \xcv4\} 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.\ term*\@{F \xcv4\}\ From 5b3086bbe55b045978c5f8291e341ce31d200c76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 6 Feb 2023 17:09:02 +0100 Subject: [PATCH 02/18] Use a name space for docitems (instances) - Use a name space table to store docitem (instance) objects - Remove docobj table, as instances were moved to the name space table - It offers the possibility to define scoped versions of docitems declaration for text* (and others docitems definition command like value*) and declare_reference*. --- .../Isabelle_DOF-Manual/02_Background.thy | 2 +- src/DOF/Isa_DOF.thy | 699 ++++++++---------- .../CENELEC_50128/CENELEC_50128.thy | 35 +- src/tests/Attributes.thy | 19 +- src/tests/TermAntiquotations.thy | 5 +- 5 files changed, 362 insertions(+), 398 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index d9115a3..408fa3b 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -65,7 +65,7 @@ text\ \ (*<*) -declare_reference*["fig:dependency"::text_section] +declare_reference*["fig:dependency"::figure] (*>*) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 146e05c..891f429 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -72,6 +72,7 @@ val invariant_suffixN = "_inv" val invariantN = "\" val makeN = "make" val schemeN = "_scheme" +val instanceN = "instance" (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = @@ -138,8 +139,8 @@ fun map_eq_fst_triple f (x,_,_) (y,_,_) = equal (f x) (f y) section\ A HomeGrown Document Type Management (the ''Model'') \ -ML\ -structure DOF_core = +ML\ +structure DOF_core = struct type virtual = {virtual : bool} @@ -184,28 +185,70 @@ struct (s <> default_cid andalso father_is_sub s) end - 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} + datatype instance = Instance of + {defined: bool, + pos: Position.T, + thy_name: string, + input_term: term, + value: term, + inline: bool, + id: serial, + cid: string, + vcid: string option} + + val empty_instance = Instance {defined = false, + pos = Position.none, + thy_name = "", + input_term = \<^term>\()\, + value = \<^term>\()\, + inline = false, + id = 0, + cid = "", + vcid = NONE} + + fun make_instance (defined, pos, thy_name, input_term, value, inline, id, cid, vcid) = + Instance {defined = defined, pos = pos, thy_name = thy_name, + input_term = input_term, value = value, inline = inline, + id = id, cid = cid, vcid = vcid} + + structure Instances = Theory_Data + ( + type T = instance Name_Space.table; + val empty : T = Name_Space.empty_table instanceN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_instances = Instances.get o Proof_Context.theory_of + + fun check_instance ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_instances ctxt); + + fun add_instance name instance thy = + thy |> Instances.map + (Name_Space.define (Context.Theory thy) true (name, instance) #> #2); + + 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:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_instances ctxt))) + |> Pretty.writeln; + + fun the_entry_key T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown instance: " ^ quote i, [], [])); + + fun the_instance instances i = + the_entry_key instances i - 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) @@ -238,31 +281,28 @@ struct (* 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. @@ -288,58 +328,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, @@ -421,27 +453,6 @@ fun is_defined_cid_local' cid_long ctxt = let val t = #docclass_tab(get_data ctxt) in cid_long=default_cid orelse Symtab.defined t cid_long end - -fun is_declared_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) - in Symtab.defined tab oid end - -fun is_declared_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy) - in Symtab.defined tab oid end - -fun is_defined_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) - in case Symtab.lookup tab oid of - NONE => false - |SOME(NONE) => false - |SOME _ => true - end - -fun is_defined_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data thy) - in case Symtab.lookup tab oid of - NONE => false - |SOME(NONE) => false - |SOME _ => true - end - fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) (* takes class synonyms into account *) val long_name = read_cid_global thy cid @@ -450,20 +461,8 @@ fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) | SOME ({virtual=virtual, ...}) => #virtual virtual end -fun declare_object_global oid thy = - let fun decl {tab=t,maxano=x} = {tab=Symtab.update_new(oid,NONE)t, maxano=x} - in (map_data_global (upd_docobj_tab(decl)) (thy) - handle Symtab.DUP _ => error("multiple declaration of document reference")) - end -fun declare_object_local oid ctxt = - let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, maxano=maxano} - in (map_data(upd_docobj_tab decl)(ctxt) - handle Symtab.DUP _ => error("multiple declaration of document reference")) - end - - -fun update_class_invariant cid_long f thy = +fun update_class_invariant cid_long f thy = let val _ = if is_defined_cid_global' cid_long thy then () else error("undefined class id : " ^cid_long) in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, @@ -585,49 +584,32 @@ 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 {define = define} ((oid, pos), bbb) thy = + let + val binding = if Long_Name.is_qualified oid + then Binding.make (Long_Name.base_name oid, pos) + else Binding.make (oid, pos) + val undefined_instance = "undefined_instance" + val ((oid', rs), instance) = Name_Space.check_reports (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, [pos]) + handle ERROR _ => ((undefined_instance, []), empty_instance) + val {pos, thy_name, input_term, value, inline, id, cid, vcid, ...} = bbb + val instance' = make_instance (define, pos, thy_name, input_term, value, inline, id, cid, vcid) + in if oid' = undefined_instance andalso instance = empty_instance + then add_instance binding instance' thy + else if define + then let val Instance {defined, ...} = instance + in if defined + then add_instance binding instance' thy + else update_instance_entry oid' instance' thy end + else add_instance binding (Instance bbb) 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_local (oid, bbb) ctxt = - map_data (upd_docobj_tab(fn{tab,maxano}=>{tab=Symtab.update(oid,SOME bbb)tab,maxano=maxano})) ctxt - - -(* declares an anonyme label of a given type and generates a unique reference ... *) -fun declare_anoobject_global thy cid = - let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) - val _ = writeln("Anonymous reference declared: " ^ str) - in {tab=Symtab.update(str,NONE)tab,maxano= maxano+1} end - in map_data_global (upd_docobj_tab declare) (thy) - end - -fun declare_anoobject_local ctxt cid = - let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) - val _ = writeln("Anonymous reference declared: " ^str) - in {tab=Symtab.update(str,NONE)tab, maxano=maxano+1} end - in map_data (upd_docobj_tab declare) (ctxt) - end - - -fun get_object_global_opt oid thy = Symtab.lookup (#tab(#docobj_tab(get_data_global thy))) oid - -fun get_object_global oid thy = case get_object_global_opt oid thy of - NONE => error("undefined reference: "^oid) - |SOME(bbb) => bbb - -fun get_object_local_opt oid ctxt = Symtab.lookup (#tab(#docobj_tab(get_data ctxt))) oid - -fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of - NONE => error("undefined reference: "^oid) - |SOME(bbb) => bbb +fun get_object_global (oid, pos) thy = + let + val ((oid', rs), instance) = Name_Space.check_reports (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, [pos]) + in instance end fun get_doc_class_global cid thy = if cid = default_cid then error("default class access") (* TODO *) @@ -696,37 +678,38 @@ fun get_attribute_defaults (* long*)cid thy = |trans (na,ty,SOME def) =SOME(na,ty, def) in map_filter trans attrS end -fun get_value_global oid thy = case get_object_global oid thy of - SOME{value=term,...} => SOME term - | NONE => NONE +fun get_value_global (oid, pos) thy = let val Instance v = get_object_global (oid, pos) thy + in v |> #value end -fun get_value_local oid ctxt = case get_object_local oid ctxt of - SOME{value=term,...} => SOME term - | NONE => NONE +fun get_value_local (oid, pos) ctxt = + let val Instance v = get_object_global (oid, pos) (Proof_Context.theory_of ctxt) + in v |> #value end (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) -fun update_value_global oid upd_value thy = - case get_object_global oid thy of - SOME{pos,thy_name, input_term, value,inline,id,cid,vcid} => - let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, - input_term= input_term, - value=upd_value value,id=id, - inline=inline,cid=cid, vcid=vcid}) - in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end - | NONE => error("undefined doc object: "^oid) -fun update_input_term_global oid upd_input_term thy = - case get_object_global oid thy of - SOME{pos,thy_name, input_term, value,inline,id,cid,vcid} => - let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, - input_term=upd_input_term input_term, - value= value,id=id, - inline=inline,cid=cid, vcid=vcid}) - in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end - | NONE => error("undefined doc object: "^oid) +fun update_value_global name pos upd_value thy = + let + val binding = Binding.make (name, pos) + val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (name, [pos]) + val Instance {defined, pos, thy_name, input_term, value, inline, id, cid, vcid} = instance + val instance' = make_instance (defined, pos, thy_name, input_term, + upd_value value, inline, id, cid, vcid) + in update_instance binding (instance') thy end + +fun update_input_term_global name pos upd_input_term thy = + let + val binding = Binding.make (name, pos) + val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (name, [pos]) + val Instance {defined, pos, thy_name, input_term, value, inline, id, cid, vcid} = instance + val instance' = make_instance (defined, pos, thy_name, upd_input_term input_term, + value, inline, id, cid, vcid) + in update_instance binding (instance') thy end + +fun update_value_input_term_global name pos upd_input_term upd_value thy = + update_value_global name pos upd_value thy |> update_input_term_global name pos upd_input_term -fun update_value_input_term_global oid upd_input_term upd_value thy = - update_value_global oid upd_value thy |> update_input_term_global oid upd_input_term val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) @@ -811,15 +794,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) = "" @@ -1052,47 +1030,42 @@ fun check_instance thy (term, _, pos) s = 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 + val object_cid = let val DOF_core.Instance cid = DOF_core.get_object_global (name, pos) thy + in cid |> #cid end fun check' (class_name, object_cid) = if class_name = object_cid then - DOF_core.get_value_global name thy + DOF_core.get_value_global (name, pos) 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) 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, _) 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 --- "^ - " type-check incomplete") - | SOME {pos=pos_decl,cid,id,...} => - let val ctxt = (Proof_Context.init_global thy) - val req_class = case req_ty of + let val DOF_core.Instance {pos=pos_decl,cid,id,...} = + DOF_core.get_object_global (name, pos) thy + val ctxt = (Proof_Context.init_global thy) + val req_class = case req_ty of \<^Type>\fun _ T\ => DOF_core.typ_to_cid T | _ => error("can not infer type for: "^ name) - in if cid <> DOF_core.default_cid + in if cid <> DOF_core.default_cid andalso not(DOF_core.is_subclass ctxt cid req_class) - then error("reference ontologically inconsistent: " + then error("reference ontologically inconsistent: " ^cid^" vs. "^req_class^ Position.here pos_decl) - else () - end - else err ("faulty reference to docitem: "^name) pos + else () + end in ML_isa_check_generic check thy (term, pos) end fun ML_isa_check_trace_attribute thy (term, _, pos) s = let - fun check thy (name, _) = - case DOF_core.get_object_global name thy of - NONE => err ("No class instance: " ^ name) pos - | SOME(_) => () - in ML_isa_check_generic check thy (term, pos) end + val oid = (HOLogic.dest_string term + handle TERM(_,[t]) => error ("wrong term format: must be string constant: " + ^ Syntax.string_of_term_global thy t )) + val _ = DOF_core.get_object_global (oid, pos) thy + in SOME term end + fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ = case term_option of @@ -1103,10 +1076,8 @@ fun elaborate_instance thy _ _ term_option pos = case term_option of NONE => error ("Malformed term annotation") | SOME term => let val instance_name = HOLogic.dest_string term - in case DOF_core.get_value_global instance_name thy of - NONE => error ("No class instance: " ^ instance_name) - | SOME(value) => - DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy + val value = DOF_core.get_value_global (instance_name, pos) thy + in DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy end (* @@ -1138,7 +1109,7 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name = end) end -fun elaborate_instances_list thy isa_name _ _ _ = +fun elaborate_instances_list thy isa_name _ _ pos = let val base_name = Long_Name.base_name isa_name fun get_isa_name_without_intances_suffix s = @@ -1147,23 +1118,15 @@ 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 - fun get_instances_name_list _ [] = [] - | get_instances_name_list class_name (x::xs) = - let - val (_, docobj_option) = x - in - case docobj_option of - NONE => get_instances_name_list class_name xs - | SOME {cid=cid, value=value, ...} => - if cid = class_name - then value::get_instances_name_list class_name xs - else get_instances_name_list class_name xs - end val long_class_name = DOF_core.read_cid_global thy base_name' - val values_list = get_instances_name_list long_class_name table_list - in HOLogic.mk_list class_typ values_list end + val values = thy |> Proof_Context.init_global |> DOF_core.get_instances + |> Name_Space.dest_table + |> filter (fn (_, instance) => + let val DOF_core.Instance cid = instance + in (cid |> #cid) = long_class_name end) + |> map (fn (oid, _) => DOF_core.get_value_global (oid, pos) thy) + in HOLogic.mk_list class_typ values end + fun declare_class_instances_annotation thy doc_class_name = let @@ -1195,35 +1158,35 @@ let in Value_Command.value ctxt (subterm') end fun compute_attr_access ctxt attr oid pos_option pos' = (* template *) - case DOF_core.get_value_global oid (Context.theory_of ctxt) of - SOME term => let val ctxt = (Proof_Context.init_global (Context.theory_of ctxt)) - val SOME{cid,pos=pos_decl,id,...} = DOF_core.get_object_local oid ctxt - val docitem_markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report ctxt pos' docitem_markup; - val (* (long_cid, attr_b,ty) = *) - {long_name, typ=ty, def_pos, ...} = - case DOF_core.get_attribute_info_local cid attr ctxt of - SOME f => f - | NONE => error("attribute undefined for reference: " - ^ oid - ^ Position.here - (the pos_option handle Option.Option => - error("Attribute " - ^ attr - ^ " undefined for reference: " - ^ oid ^ Position.here pos'))) - val proj_term = Const(long_name,dummyT --> ty) - val _ = case pos_option of - NONE => () - | SOME pos => - let - val class_name = Long_Name.qualifier long_name - val SOME{id,...} = DOF_core.get_doc_class_local class_name ctxt - val class_markup = docclass_markup false class_name id def_pos - in Context_Position.report ctxt pos class_markup end - in symbex_attr_access0 ctxt proj_term term end - (*in Value_Command.value ctxt term end*) - | NONE => error("identifier not a docitem reference" ^ Position.here pos') + let + val value = DOF_core.get_value_global (oid, pos') (Context.theory_of ctxt) + val ctxt' = Context.proof_of ctxt + val DOF_core.Instance {cid,pos=pos_decl,id,...} = + DOF_core.get_object_global (oid, pos') (Context.theory_of ctxt) + val docitem_markup = docref_markup false oid id pos_decl; + val _ = Context_Position.report ctxt' pos' docitem_markup; + val (* (long_cid, attr_b,ty) = *) + {long_name, typ=ty, def_pos, ...} = + case DOF_core.get_attribute_info_local cid attr ctxt' of + SOME f => f + | NONE => error("attribute undefined for reference: " + ^ oid + ^ Position.here + (the pos_option handle Option.Option => + error("Attribute " + ^ attr + ^ " undefined for reference: " + ^ oid ^ Position.here pos'))) + val proj_term = Const(long_name,dummyT --> ty) + val _ = case pos_option of + NONE => () + | SOME pos => + let + val class_name = Long_Name.qualifier long_name + val SOME{id,...} = DOF_core.get_doc_class_local class_name ctxt' + val class_markup = docclass_markup false class_name id def_pos + in Context_Position.report ctxt' pos class_markup end + in symbex_attr_access0 ctxt' proj_term value end fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos = case term_option of @@ -1336,7 +1299,7 @@ val attribute_upd : (((string * Position.T) * string) * string) parser = : (((string * Position.T) * string) * string) parser; val reference = - Parse.position Parse.name + Parse.position Parse.name --| improper -- Scan.option (Parse.$$$ "::" -- improper @@ -1344,7 +1307,6 @@ val reference = ) --| improper; - val attributes = ((Parse.$$$ "[" -- improper @@ -1521,7 +1483,7 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long else case inherits_from of NONE => - ISA_core.err ("Attribute not defined for class: " ^ cid_long) pos + ISA_core.err ("Attribute " ^ attribute_name ^ " not defined for class: " ^ cid_long) pos | SOME (_, parent_name) => get_class_name parent_name attribute_name pos end @@ -1562,7 +1524,7 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long | ":=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term | "+=" => Const(lnu,lnut) $ Abs ("uu_", lnt, join lnt $ (Bound 0) $ rhs'') $ term | _ => error "corrupted syntax - oops - this should not occur" - end + end in Sign.certify_term thy (fold read_assn S term) end fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking @@ -1637,7 +1599,8 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = Syntax.read_term_global thy rhs) val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] val assns' = map conv_attrs trace_attr - fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy)) + fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_object_global (oid, pos) thy + in #cid params end fun def_trans_input_term oid = #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') fun def_trans_value oid = @@ -1656,9 +1619,9 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = automatas=aS}) tab end fun update_trace mon_oid = if Config.get_global thy DOF_core.object_value_debug - then DOF_core.update_value_input_term_global mon_oid + then DOF_core.update_value_input_term_global mon_oid pos (def_trans_input_term mon_oid) (def_trans_value mon_oid) - else DOF_core.update_value_global mon_oid (def_trans_value mon_oid) + else DOF_core.update_value_global mon_oid pos (def_trans_value mon_oid) val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) in thy |> (* update traces of all enabled monitors *) fold (update_trace) (enabled_monitors) @@ -1668,10 +1631,11 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = DOF_core.map_data_global(update_automatons) end -fun check_invariants thy oid = +fun check_invariants thy (oid, pos) = let - val docitem_value = the (DOF_core.get_value_global oid thy) - val cid = #cid (the (DOF_core.get_object_global oid thy)) + val docitem_value = DOF_core.get_value_global (oid, pos) thy + val DOF_core.Instance params = DOF_core.get_object_global (oid, pos) thy + val cid = #cid params fun get_all_invariants cid thy = case DOF_core.get_doc_class_global cid thy of NONE => error("undefined class id for invariants: " ^ cid) @@ -1740,7 +1704,8 @@ fun check_invariants thy oid = val _ = map check_invariants' inv_and_apply_list in thy end -fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy = + +fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oid pos cid_pos doc_attrs thy = let val id = serial (); val _ = Position.report pos (docref_markup true oid id pos); @@ -1779,8 +1744,8 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do else (\<^term>\()\, value_term') end val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) o Context.Theory - - in thy |> DOF_core.define_object_global (oid, {pos = pos, + in thy |> DOF_core.define_object_global {define = define} ((oid, pos), {defined = false, + pos = pos, thy_name = Context.theory_name thy, input_term = fst value_terms, value = value (Proof_Context.init_global thy) @@ -1805,18 +1770,18 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do ex: text*[sdf]\ Lorem ipsum @{thm refl}\ *) |> (fn thy => if default_cid then thy else if Config.get_global thy DOF_core.invariants_checking - then check_invariants thy oid else thy) + then check_invariants thy (oid, pos) else thy) end end (* structure Docitem_Parser *) val empty_meta_args = ((("", Position.none), NONE), []) -fun meta_args_exec (meta_args as (((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = +fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = thy |> (if meta_args = empty_meta_args then (K thy) else Docitem_Parser.create_and_check_docitem - {is_monitor = false} {is_inline = false} + {is_monitor = false} {is_inline = false} {define = true} oid pos (I cid_pos) (I doc_attrs)) fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t pos thy = @@ -1851,21 +1816,16 @@ val opt_modes = val opt_evaluator = Scan.optional (\<^keyword>\[\ |-- Parse.name --| \<^keyword>\]\) ""; -(* - We want to have the current position to pass it to transduce_term_global in - value_cmd, so we pass the Toplevel.transition -*) - -fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) = -let val pos = Position.none +fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = +let val pos = Toplevel.pos_of trans in - Toplevel.theory (value_cmd {assert=false} meta_args_opt name modes t pos) + trans |> Toplevel.theory (value_cmd {assert=false} meta_args_opt name modes t pos) end -fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) = -let val pos = Position.none +fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans = +let val pos = Toplevel.pos_of trans in - Toplevel.theory (value_cmd {assert=true} meta_args_opt name modes t pos) + trans |> Toplevel.theory (value_cmd {assert=true} meta_args_opt name modes t pos) end \ \c.f. \<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ @@ -1965,16 +1925,15 @@ end; (* structure Value_Command *) structure Monitor_Command_Parser = struct -fun update_instance_command (((oid:string,pos),cid_pos), +fun update_instance_command (((oid, pos), cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) thy : theory = - let val cid = case DOF_core.get_object_global oid thy of - SOME{pos=pos_decl,cid,id,...} => - let val markup = docref_markup false oid id pos_decl; - val ctxt = Proof_Context.init_global thy; - val _ = Context_Position.report ctxt pos markup; - in cid end - | NONE => error("undefined doc_class.") + let val cid = let val DOF_core.Instance {pos=pos_decl,cid,id,...} = + DOF_core.get_object_global (oid, pos) thy + val markup = docref_markup false oid id pos_decl; + val ctxt = Proof_Context.init_global thy; + val _ = Context_Position.report ctxt pos markup; + in cid end val cid_pos' = Value_Command.Docitem_Parser.check_classref {is_monitor = false} cid_pos thy val cid_long = fst cid_pos' @@ -1997,13 +1956,13 @@ fun update_instance_command (((oid:string,pos),cid_pos), thy) in thy |> (if Config.get_global thy DOF_core.object_value_debug - then DOF_core.update_value_input_term_global oid + then DOF_core.update_value_input_term_global oid pos def_trans_input_term def_trans_value - else DOF_core.update_value_global oid + else DOF_core.update_value_global oid pos def_trans_value) |> check_inv |> (fn thy => if Config.get_global thy DOF_core.invariants_checking - then Value_Command.Docitem_Parser.check_invariants thy oid + then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) else thy) end @@ -2011,11 +1970,12 @@ fun update_instance_command (((oid:string,pos),cid_pos), (* General criticism : attributes like "level" were treated here in the kernel instead of dragging them out into the COL -- bu *) -fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = +fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = let fun o_m_c oid pos cid_pos doc_attrs thy = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor=true} (* this is a monitor *) - {is_inline=false} (* monitors are always inline *) + {is_inline=false} (* monitors are always inline *) + {define=true} oid pos cid_pos doc_attrs thy fun compute_enabled_set cid thy = let @@ -2027,7 +1987,7 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Pars in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end | NONE => error("Internal error: class id undefined. ") end - fun create_monitor_entry thy = + fun create_monitor_entry oid thy = let val cid = case cid_pos of NONE => ISA_core.err ("You must specified a monitor class.") pos | SOME (cid, _) => cid @@ -2036,11 +1996,11 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Pars in DOF_core.map_data_global(DOF_core.upd_monitor_tabs(Symtab.update(oid, info )))(thy) end in - o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry + o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry oid end; -fun close_monitor_command (args as (((oid:string,pos),cid_pos), +fun close_monitor_command (args as (((oid, pos), cid_pos), doc_attrs: (((string*Position.T)*string)*string)list)) thy = let val {monitor_tab,...} = DOF_core.get_data_global thy fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 @@ -2056,7 +2016,7 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), SOME {automatas,...} => check_if_final automatas | NONE => error ("Not belonging to a monitor class: "^oid) val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid)) - val {cid=cid_long, id, ...} = the(DOF_core.get_object_global oid thy) + val DOF_core.Instance {cid=cid_long, id, ...} = DOF_core.get_object_global (oid, pos) thy val markup = docref_markup false oid id pos; val _ = Context_Position.report (Proof_Context.init_global thy) pos markup; val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true} @@ -2067,21 +2027,22 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), |> update_instance_command args |> (fn thy => (check_inv thy; thy)) |> (fn thy => if Config.get_global thy DOF_core.invariants_checking - then Value_Command.Docitem_Parser.check_invariants thy oid + then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) else thy) |> delete_monitor_entry end -fun meta_args_2_latex thy ((((lab, _), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = +fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = (* for the moment naive, i.e. without textual normalization of attribute names and adapted term printing *) let val l = "label = "^ (enclose "{" "}" lab) (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) val cid_long = case cid_opt of - NONE => (case DOF_core.get_object_global lab thy of - NONE => DOF_core.default_cid - | SOME X => #cid X) + NONE => let val DOF_core.Instance cid = + DOF_core.get_object_global (lab, pos) thy + in cid |> #cid end + | SOME(cid,_) => DOF_core.parse_cid_global thy cid (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) val cid_txt = "type = " ^ (enclose "{" "}" cid_long); @@ -2139,9 +2100,9 @@ fun meta_args_2_latex thy ((((lab, _), cid_opt), attr_list) : ODL_Meta_Args_Pars (* level-attribute information management *) fun gen_enriched_document_cmd {inline} cid_transform attr_transform - ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory = + ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = inline} - oid pos (cid_transform cid_pos) (attr_transform doc_attrs); + {define = true} oid pos (cid_transform cid_pos) (attr_transform doc_attrs); (* markup reports and document output *) @@ -2214,8 +2175,10 @@ val _ = val _ = Outer_Syntax.command \<^command_keyword>\declare_reference*\ "declare document reference" - (ODL_Meta_Args_Parser.attributes >> (fn (((oid,pos),cid),doc_attrs) => - (Toplevel.theory (DOF_core.declare_object_global oid)))); + (ODL_Meta_Args_Parser.attributes >> (fn (((oid, pos),cid_pos),doc_attrs) => + (Toplevel.theory (Value_Command.Docitem_Parser.create_and_check_docitem + {is_monitor = false} {is_inline=true} + {define = false} oid pos (cid_pos) (doc_attrs))))); end (* structure Monitor_Command_Parser *) \ @@ -2224,7 +2187,7 @@ end (* structure Monitor_Command_Parser *) ML\ 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^")") @@ -2265,13 +2228,18 @@ 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})) = - (writeln ("docitem: "^n); + fun print_item (n, DOF_core.Instance {defined,cid,vcid,id,pos, + thy_name,inline, input_term, value}) = + ((if defined then + writeln ("docitem: "^n) + else + writeln ("forward reference for docitem: "^n)); + writeln (" defined: "^dfg defined); writeln (" type: "^cid); case vcid of NONE => () | SOME (s) => writeln (" virtual type: "^ s); @@ -2282,9 +2250,7 @@ fun print_doc_items b ctxt = else ()); writeln (" value: "^ (Syntax.string_of_term ctxt value)) ) - | print_item (n, 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 _ = @@ -2292,16 +2258,18 @@ 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) - val T = map fst (Symtab.dest monitor_tab) - in if null S - then if null T then () - else error("Global consistency error - there are open monitors: " - ^ String.concatWith "," T) - else error("Global consistency error - Unresolved forward references: " - ^ String.concatWith "," S) - end + let val {monitor_tab, ...} = DOF_core.get_data ctxt; + val S = ctxt |> DOF_core.get_instances |> Name_Space.dest_table + |> filter (fn (_, DOF_core.Instance {defined,...}) => (not defined)) + |> map #1 + val T = map fst (Symtab.dest monitor_tab) + in if null S + then if null T then () + else error("Global consistency error - there are open monitors: " + ^ String.concatWith "," T) + else error("Global consistency error - Unresolved forward references: " + ^ String.concatWith "," S) + end val _ = Outer_Syntax.command \<^command_keyword>\check_doc_global\ "check global document consistency" @@ -2317,12 +2285,12 @@ ML\ structure ML_star_Command = struct -fun meta_args_exec (meta_args as (((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = +fun meta_args_exec (meta_args as (((oid, pos),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} - oid pos (I cid_pos) (I doc_attrs)) + {define = true} oid pos (I cid_pos) (I doc_attrs)) ) val attributes_opt = Scan.option ODL_Meta_Args_Parser.attributes @@ -2344,15 +2312,15 @@ ML\ structure ODL_LTX_Converter = struct -fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = +fun meta_args_2_string thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = (* for the moment naive, i.e. without textual normalization of attribute names and adapted term printing *) let val l = "label = "^ (enclose "{" "}" lab) (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) val cid_long = case cid_opt of - NONE => (case DOF_core.get_object_global lab thy of - NONE => DOF_core.default_cid - | SOME X => #cid X) + NONE => let val DOF_core.Instance cid = + DOF_core.get_object_global (lab, pos) thy + in cid |> #cid end | SOME(cid,_) => DOF_core.parse_cid_global thy cid (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) val cid_txt = "type = " ^ (enclose "{" "}" cid_long); @@ -2425,26 +2393,19 @@ val basic_entity = Document_Output.antiquotation_pretty_source fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = let val thy = Proof_Context.theory_of ctxt; - in - if DOF_core.is_defined_oid_global name thy - then let val {pos=pos_decl,id,cid,inline,...} = the(DOF_core.get_object_global name thy) - val _ = if not inline_req - then if inline then () else error("referred text-element is macro! (try option display)") - else if not inline then () else error("referred text-element is no macro!") - val markup = docref_markup false name id pos_decl; - val _ = Context_Position.report ctxt pos markup; - (* this sends a report for a ref application to the PIDE interface ... *) - val _ = if not(DOF_core.is_subclass ctxt cid cid_decl) - then error("reference ontologically inconsistent: "^cid - ^" must be subclass of "^cid_decl^ Position.here pos_decl) - else () + val DOF_core.Instance {pos=pos_decl,id,cid,inline,...} = + DOF_core.get_object_global (name, pos) thy + val _ = if not inline_req + then if inline then () else error("referred text-element is macro! (try option display)") + else if not inline then () else error("referred text-element is no macro!") + val markup = docref_markup false name id pos_decl; + val _ = Context_Position.report ctxt pos markup; + (* this sends a report for a ref application to the PIDE interface ... *) + val _ = if not(DOF_core.is_subclass ctxt cid cid_decl) + then error("reference ontologically inconsistent: "^cid + ^" must be subclass of "^cid_decl^ Position.here pos_decl) + else () in () end - else if DOF_core.is_declared_oid_global name thy - then (if #strict_checking str - then warning("declared but undefined document reference: "^name) - else ()) - else error("undefined document reference: "^name) - end val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} -> {inline:bool} -> @@ -2482,26 +2443,24 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src end -fun docitem_antiquotation bind cid = - Document_Output.antiquotation_raw bind docitem_antiquotation_parser - (pretty_docitem_antiquotation_generic cid); +fun docitem_antiquotation bind cid = + Document_Output.antiquotation_raw bind docitem_antiquotation_parser + (pretty_docitem_antiquotation_generic cid) fun check_and_mark_term ctxt oid = - let val thy = Context.theory_of ctxt; - in if DOF_core.is_defined_oid_global oid thy - then let val {pos=pos_decl,id,cid,value,...} = the(DOF_core.get_object_global oid thy) - val markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report_generic ctxt pos_decl markup; - (* this sends a report for a ref application to the PIDE interface ... *) - val _ = if cid = DOF_core.default_cid - then error("anonymous "^ DOF_core.default_cid ^ " class has no value" ) - else () - in value end - else error("undefined document reference:"^oid) - end - - + let + val thy = Context.theory_of ctxt; + val DOF_core.Instance {pos=pos_decl,id,cid,value,...} = + DOF_core.get_object_global (oid, Position.none) thy + val markup = docref_markup false oid id pos_decl; + val _ = Context_Position.report_generic ctxt pos_decl markup; + (* this sends a report for a ref application to the PIDE interface ... *) + val _ = if cid = DOF_core.default_cid + then error("anonymous "^ DOF_core.default_cid ^ " class has no value" ) + else () + in value end + fun ML_antiquotation_docitem_value (ctxt, toks) = (Scan.lift (Args.cartouche_input) >> (fn inp => (ML_Syntax.atomic o ML_Syntax.print_term) @@ -2557,22 +2516,20 @@ fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o M fun get_instance_value_2_ML ctxt (oid:string,pos) = let val ctxt' = Context.the_proof ctxt - val value = case DOF_core.get_object_local oid ctxt' of - SOME({pos=pos_decl,id,value,...}) => - let val markup = docref_markup false oid id pos_decl - val _ = Context_Position.report ctxt' pos markup - in value end - | NONE => error "not an object id" + val value = let val DOF_core.Instance {pos=pos_decl,id,value,...} = + DOF_core.get_object_global (oid, pos) (Context.theory_of ctxt) + val markup = docref_markup false oid id pos_decl + val _ = Context_Position.report ctxt' pos markup + in value end 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" + val _ = let val DOF_core.Instance {pos=pos_decl,id,...} = + DOF_core.get_object_global (oid, pos) (Context.theory_of ctxt) + val markup = docref_markup false oid id pos_decl + val _ = Context_Position.report ctxt' pos markup + in () end in "\"" ^ oid ^ "\"" end fun trace_attr_2_ML ctxt (oid:string,pos) = @@ -2585,12 +2542,11 @@ fun compute_cid_repr ctxt cid pos = 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" + let val _ = let val DOF_core.Instance {pos=pos_decl,id,...} = + DOF_core.get_object_global (oid, pos) (Proof_Context.theory_of ctxt) + val markup = docref_markup false oid id pos_decl + val _ = Context_Position.report ctxt pos markup + in () end in HOLogic.mk_string oid end local @@ -2624,7 +2580,7 @@ val parse_cid = (context_position_parser Args.typ_abbrev) val parse_cid' = Term_Style.parse -- parse_cid fun pretty_cid_style ctxt (style,(pos,cid)) = - (*reconversion to term in order to haave access to term print options like: short_names etc...) *) + (*reconversion to term in order to have access to term print options like: names_short etc...) *) Document_Output.pretty_term ctxt ((compute_cid_repr ctxt cid pos)); in @@ -2784,7 +2740,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) NONE) else error("no overloading allowed.") val record_fields = map_filter (check_n_filter thy) fields - (* adding const symbol representing doc-class for Monitor-RegExps.*) + (* adding const symbol representing doc-class for Monitor-RegExps.*) val constant_typ = \<^typ>\doc_class rexp\ val constant_term = \<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ @@ -2792,24 +2748,23 @@ fun add_doc_class_cmd overloaded (raw_params, binding) val eq = mk_meta_eq(Free(Binding.name_of binding, constant_typ), constant_term) val args = (SOME(binding,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) in thy |> Named_Target.theory_map (def_cmd args) - |> (fn thy => - case parent' of - NONE => (Record.add_record + |> ( case parent' of + NONE => Record.add_record overloaded (params', binding) parent' (DOF_core.tag_attr::record_fields) #> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps - reject_Atoms invariants {virtual=false}) thy + reject_Atoms invariants {virtual=false} | SOME _ => if (not o null) record_fields - then (Record.add_record overloaded (params', binding) parent' (record_fields) + then Record.add_record overloaded (params', binding) parent' (record_fields) #> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps - reject_Atoms invariants {virtual=false}) thy - else (Record.add_record + reject_Atoms invariants {virtual=false} + else Record.add_record overloaded (params', binding) parent' ([DOF_core.tag_attr]) #> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps - reject_Atoms invariants {virtual=true}) thy) + reject_Atoms invariants {virtual=true} ) |> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy) (* defines the ontology-checked text antiquotation to this document class *) diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index c5d96bd..a3c27a5 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -157,10 +157,10 @@ which have the required safety integrity level.\ Definition*[entity] \person, group or organisation who fulfils a role as defined in this European Standard.\ -declare_reference*[fault] +declare_reference*[fault::cenelec_term] Definition*[error] \defect, mistake or inaccuracy which could result in failure or in a deviation -from the intended performance or behaviour (cf. @{cenelec_term (unchecked) \fault\})).\ +from the intended performance or behaviour (cf. @{cenelec_term (unchecked) \fault\}).\ Definition*[fault] \defect, mistake or inaccuracy which could result in failure or in a deviation @@ -1009,14 +1009,16 @@ ML\ fun check_sil oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) - val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt')) + val DOF_core.Instance {value = monitor_record_value, ...} = + DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) val Const _ $ _ $ monitor_sil $ _ = monitor_record_value val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here> fun check_sil'' [] = true | check_sil'' (x::xs) = let val (_, doc_oid) = x - val doc_record_value = #value (the (DOF_core.get_object_local doc_oid ctxt')) + val DOF_core.Instance {value = doc_record_value, ...} = + DOF_core.get_object_global (doc_oid, Position.none) (Context.theory_of ctxt) val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext in @@ -1038,8 +1040,10 @@ ML\ fun check_sil_slow oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) - val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt')) - val monitor_cid = #cid (the (DOF_core.get_object_local oid ctxt')) + val DOF_core.Instance {value = monitor_record_value, ...} = + DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) + val DOF_core.Instance {cid = monitor_cid, ...} = + DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) val monitor_sil_typ = (Syntax.read_typ ctxt' monitor_cid) --> @{typ "sil"} val monitor_sil = Value_Command.value ctxt' (Const("CENELEC_50128.monitor_SIL.sil", monitor_sil_typ) $ monitor_record_value) @@ -1048,7 +1052,8 @@ fun check_sil_slow oid _ ctxt = | check_sil' (x::xs) = let val (doc_cid, doc_oid) = x - val doc_record_value = #value (the (DOF_core.get_object_local doc_oid ctxt')) + val DOF_core.Instance {value = doc_record_value, ...} = + DOF_core.get_object_global (doc_oid, Position.none) (Context.theory_of ctxt) val doc_sil_typ = (Syntax.read_typ ctxt' doc_cid) --> @{typ "sil"} val doc_sil = Value_Command.value ctxt' (Const ("CENELEC_50128.cenelec_document.sil", doc_sil_typ) $ doc_record_value) @@ -1082,7 +1087,8 @@ fun check_required_documents oid _ ctxt = else let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) - val monitor_record_value = #value (the (DOF_core.get_object_local oid ctxt')) + val DOF_core.Instance {value = monitor_record_value, ...} = + DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) val Const _ $ _ $ monitor_sil $ _ = monitor_record_value in error ("A " ^ cid ^ " cenelec document is required with " ^ Syntax.string_of_term ctxt' monitor_sil) @@ -1101,11 +1107,11 @@ text*[MonitorPatternMatchingTest::monitor_SIL0]\\ text*[CenelecClassPatternMatchingTest::SQAP, sil = "SIL0"]\\ ML\ val thy = @{theory} -val monitor_record_value = - #value (the (DOF_core.get_object_global "MonitorPatternMatchingTest" thy)) +val DOF_core.Instance {value = monitor_record_value, ...} = + DOF_core.get_object_global ("MonitorPatternMatchingTest", Position.none) thy val Const _ $ _ $ monitor_sil $ _ = monitor_record_value -val doc_record_value = #value (the (DOF_core.get_object_global - "CenelecClassPatternMatchingTest" thy)) +val DOF_core.Instance {value = doc_record_value, ...} = + DOF_core.get_object_global ("CenelecClassPatternMatchingTest", Position.none) thy val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext \ @@ -1266,8 +1272,9 @@ ML DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.test_requirement"; \ ML -\ val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context}; - Symtab.dest ref_tab; +\ 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; \ ML diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 73266b1..63b0fe8 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -25,14 +25,15 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ -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; \ ML\ -#value(the(the(Symtab.lookup docitem_tab "aaa"))) - +val (oid, DOF_core.Instance {value, ...}) = + Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none) \ find_theorems (60) name:"Conceptual.M." @@ -124,11 +125,11 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory}; ML\ -DOF_core.get_value_local "sdf" @{context}; -DOF_core.get_value_local "sdfg" @{context}; -DOF_core.get_value_local "xxxy" @{context}; -DOF_core.get_value_local "dfgdfg" @{context}; -DOF_core.get_value_local "omega" @{context}; +DOF_core.get_value_local ("sdf", Position.none) @{context}; +DOF_core.get_value_local ("sdfg", Position.none) @{context}; +DOF_core.get_value_local ("xxxy", Position.none) @{context}; +DOF_core.get_value_local ("dfgdfg", Position.none) @{context}; +DOF_core.get_value_local ("omega", Position.none) @{context}; \ text\A not too trivial test: default y -> []. diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy index 78069a2..72252e4 100644 --- a/src/tests/TermAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -41,8 +41,9 @@ ODL on a paradigmatical example. text\Voila the content of the Isabelle_DOF environment so far:\ -ML\ -val {docobj_tab={tab = x, ...},docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context}; +ML\ +val x = DOF_core.get_instances \<^context> +val {docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context}; Symtab.dest ISA_transformer_tab; \ From c440f9628fd9bd2b4161cc353a7518173bf5a883 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 9 Feb 2023 16:40:05 +0100 Subject: [PATCH 03/18] Fix typo --- src/DOF/Isa_DOF.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 891f429..5915e11 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -246,8 +246,8 @@ struct SOME entry => entry | NONE => raise TYPE ("Unknown instance: " ^ quote i, [], [])); - fun the_instance instances i = - the_entry_key instances i + fun the_instance instance i = + the_entry_key instance i type ISA_transformers = {check : (theory -> term * typ * Position.T -> string -> term option), From 9b51844fadaf2734cb1047b9c1c7e4c94b018945 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 9 Feb 2023 16:41:32 +0100 Subject: [PATCH 04/18] Use a name space for monitors infos - Use a name space table to store monitor infos objects - Remove monitor_tab table, as monitor infos were moved to the name space table - It offers the possibility to define scoped versions of monitors --- src/DOF/Isa_DOF.thy | 180 +++++++++++------- .../CENELEC_50128/CENELEC_50128.thy | 4 +- src/tests/Attributes.thy | 22 +-- src/tests/OutOfOrderPresntn.thy | 9 +- 4 files changed, 121 insertions(+), 94 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 5915e11..511af36 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -73,6 +73,7 @@ val invariantN = "\" val makeN = "make" val schemeN = "_scheme" val instanceN = "instance" +val monitor_infoN = "monitor_info" (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = @@ -241,14 +242,11 @@ struct (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_instances ctxt))) |> Pretty.writeln; - fun the_entry_key T i = + fun the_instance T i = (case Name_Space.lookup_key T i of SOME entry => entry | NONE => raise TYPE ("Unknown instance: " ^ quote i, [], [])); - fun the_instance instance i = - the_entry_key instance i - type ISA_transformers = {check : (theory -> term * typ * Position.T -> string -> term option), elaborate : (theory -> string -> typ -> term option -> Position.T -> term) @@ -268,13 +266,52 @@ struct (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table val initial_docclass_lazy_inv_tab : docclass_lazy_inv_tab = Symtab.empty - type open_monitor_info = {accepted_cids : string list, - rejected_cids : string list, - automatas : RegExpInterface.automaton list - } - type monitor_tab = open_monitor_info Symtab.table - val initial_monitor_tab:monitor_tab = Symtab.empty + datatype monitor_info = Monitor_Info of + {accepted_cids : string list, + rejected_cids : string list, + automatas : RegExpInterface.automaton list} + + + fun make_monitor_info (accepted_cids, rejected_cids, automatas) = + Monitor_Info {accepted_cids = accepted_cids, + rejected_cids = rejected_cids, + automatas = automatas} + + structure Monitor_Info = Theory_Data + ( + type T = monitor_info Name_Space.table; + val empty : T = Name_Space.empty_table monitor_infoN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_monitor_infos = Monitor_Info.get o Proof_Context.theory_of + + fun check_monitor_info ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_monitor_infos ctxt); + + fun add_monitor_info name monitor_info thy = + thy |> Monitor_Info.map + (Name_Space.define (Context.Theory thy) true (name, monitor_info) #> #2); + + fun update_monitor_info name monitor_info thy = + thy |> Monitor_Info.map + (Name_Space.define (Context.Theory thy) false (name, monitor_info) #> #2); + + fun update_monitor_info_entry name new_monitor_info thy = + thy |> Monitor_Info.map + (Name_Space.map_table_entry name (fn _ => new_monitor_info)); + + fun print_monitors_infos verbose ctxt = + Pretty.big_list "Isabelle.DOF Monitor_Infos:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_monitor_infos ctxt))) + |> Pretty.writeln; + + fun the_monitor_info T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown monitor_info: " ^ quote i, [], [])); + fun override(t1,t2) = fold(Symtab.update)(Symtab.dest t2)(t1) @@ -283,23 +320,21 @@ structure Data = Generic_Data ( 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 = {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( {docclass_tab = c1, - ISA_transformer_tab = e1, monitor_tab=m1, + ISA_transformer_tab = e1, docclass_inv_tab = n1, docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1}, {docclass_tab = c2, - ISA_transformer_tab = e2, monitor_tab=m2, + ISA_transformer_tab = e2, docclass_inv_tab = n2, docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) = {docclass_tab = merge_docclass_tab (c1,c2), @@ -310,8 +345,6 @@ structure Data = Generic_Data 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), (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) docclass_eager_inv_tab = override(en1,en2), @@ -329,58 +362,50 @@ val map_data_global = Context.theory_map o map_data; fun upd_docclass_tab f {docclass_tab = y,ISA_transformer_tab = z, - monitor_tab, docclass_inv_tab, + docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab, + {docclass_tab = f y,ISA_transformer_tab = z, 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 {docclass_tab = y,ISA_transformer_tab = z, - monitor_tab, docclass_inv_tab, + docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab, + {docclass_tab = y,ISA_transformer_tab = f z, 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 {docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_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 {docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, + docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = {docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, + ISA_transformer_tab = ISA_transformer_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 {docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, + docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = {docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, + ISA_transformer_tab = ISA_transformer_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 {docclass_tab,ISA_transformer_tab, - monitor_tab, docclass_inv_tab, + docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = {docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, + ISA_transformer_tab = ISA_transformer_tab, docclass_inv_tab=docclass_inv_tab, docclass_eager_inv_tab=docclass_eager_inv_tab, docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; -fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids -fun get_rejected_cids ({rejected_cids, ... } : open_monitor_info) = rejected_cids +fun get_accepted_cids (Monitor_Info {accepted_cids, ... }) = accepted_cids +fun get_rejected_cids (Monitor_Info {rejected_cids, ... }) = rejected_cids fun get_alphabet monitor_info = (get_accepted_cids monitor_info) @ (get_rejected_cids monitor_info) -fun get_automatas ({automatas, ... } : open_monitor_info) = automatas +fun get_automatas (Monitor_Info {automatas, ... }) = automatas (* doc-class-name management: We still use the record-package for internally @@ -611,6 +636,18 @@ fun get_object_global (oid, pos) thy = (get_instances (Proof_Context.init_global thy)) (oid, [pos]) in instance end +fun get_monitor_info_global (oid, pos) thy = + let + val ((oid', rs), monitor_info) = Name_Space.check_reports (Context.Theory thy) + (get_monitor_infos (Proof_Context.init_global thy)) (oid, [pos]) + in monitor_info end + +fun get_monitor_info_name_global (oid, pos) thy = + let + val ((oid', rs), monitor_info) = Name_Space.check_reports (Context.Theory thy) + (get_monitor_infos (Proof_Context.init_global thy)) (oid, [pos]) + in oid' end + fun get_doc_class_global cid thy = if cid = default_cid then error("default class access") (* TODO *) else let val t = #docclass_tab(get_data_global thy) @@ -689,7 +726,9 @@ fun get_value_local (oid, pos) ctxt = fun update_value_global name pos upd_value thy = let - val binding = Binding.make (name, pos) + val binding = if Long_Name.is_qualified name + then Binding.make (Long_Name.base_name name, pos) + else Binding.make (name, pos) val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy) (get_instances (Proof_Context.init_global thy)) (name, [pos]) val Instance {defined, pos, thy_name, input_term, value, inline, id, cid, vcid} = instance @@ -699,7 +738,9 @@ fun update_value_global name pos upd_value thy = fun update_input_term_global name pos upd_input_term thy = let - val binding = Binding.make (name, pos) + val binding = if Long_Name.is_qualified name + then Binding.make (Long_Name.base_name name, pos) + else Binding.make (name, pos) val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy) (get_instances (Proof_Context.init_global thy)) (name, [pos]) val Instance {defined, pos, thy_name, input_term, value, inline, id, cid, vcid} = instance @@ -1532,24 +1573,22 @@ fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking else ISA_core.warn txt pos fun register_oid_cid_in_open_monitors oid pos cid_pos thy = - let val {monitor_tab,...} = DOF_core.get_data_global thy - val cid_long= fst cid_pos + let val cid_long= fst cid_pos val pos' = snd cid_pos - fun is_enabled (n, info) = + fun is_enabled (n, monitor_info) = if exists (DOF_core.is_subclass_global thy cid_long) - (DOF_core.get_alphabet info) - then SOME n + (DOF_core.get_alphabet monitor_info) + then SOME (n, monitor_info) else if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking orelse Config.get_global thy DOF_core.free_class_in_monitor_checking - then SOME n + then SOME (n, monitor_info) else NONE (* filtering those monitors with automata, whose alphabet contains the cid of this oid. The enabled ones were selected and moved to their successor state along the super-class id. The evaluation is in parallel, simulating a product semantics without expanding the subclass relationship. *) - fun is_enabled_for_cid moid = - let val {accepted_cids, automatas, rejected_cids, ...} = - the(Symtab.lookup monitor_tab moid) + fun is_enabled_for_cid (moid , monitor_info) = + let val DOF_core.Monitor_Info {accepted_cids, automatas, rejected_cids, ...} = monitor_info val indexS= 1 upto (length automatas) val indexed_autoS = automatas ~~ indexS fun check_for_cid (A,n) = @@ -1593,8 +1632,9 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = ^ " of monitor " ^ moid ^ " rejected doc_class: " ^ cid_long) pos';A)) end - in (moid,map check_for_cid indexed_autoS) end - val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab) + in (moid,map check_for_cid indexed_autoS, monitor_info) end + val enabled_monitors = List.mapPartial is_enabled + (Name_Space.dest_table (DOF_core.get_monitor_infos (Proof_Context.init_global thy))) fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, Syntax.read_term_global thy rhs) val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] @@ -1607,28 +1647,27 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = (#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')) #> value (Proof_Context.init_global thy) val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." - val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; + val _ = app (fn (n, _) => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; (* check that any transition is possible : *) fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false} - fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors - val delta_autoS = map is_enabled_for_cid enabled_monitors; - fun update_info (n, aS) (tab: DOF_core.monitor_tab) = - let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n) - in Symtab.update(n, {accepted_cids=accepted_cids, - rejected_cids=rejected_cids, - automatas=aS}) tab end + fun class_inv_checks ctxt = map (fn (x, _) => inst_class_inv x ctxt) enabled_monitors + val delta_autoS = map is_enabled_for_cid enabled_monitors; + fun update_info (n, aS, monitor_info) = + let val DOF_core.Monitor_Info {accepted_cids,rejected_cids,...} = monitor_info + in Name_Space.map_table_entry n (fn _ => DOF_core.make_monitor_info + (accepted_cids, rejected_cids, aS)) + end fun update_trace mon_oid = if Config.get_global thy DOF_core.object_value_debug then DOF_core.update_value_input_term_global mon_oid pos (def_trans_input_term mon_oid) (def_trans_value mon_oid) else DOF_core.update_value_global mon_oid pos (def_trans_value mon_oid) - val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) in thy |> (* update traces of all enabled monitors *) - fold (update_trace) (enabled_monitors) + fold update_trace (map #1 enabled_monitors) |> (* check class invariants of enabled monitors *) (fn thy => (class_inv_checks (Context.Theory thy); thy)) |> (* update the automata of enabled monitors *) - DOF_core.map_data_global(update_automatons) + DOF_core.Monitor_Info.map (fold update_info delta_autoS) end fun check_invariants thy (oid, pos) = @@ -1993,7 +2032,7 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par | SOME (cid, _) => cid val (accS, rejectS, aS) = compute_enabled_set cid thy val info = {accepted_cids = accS, rejected_cids = rejectS, automatas = aS } - in DOF_core.map_data_global(DOF_core.upd_monitor_tabs(Symtab.update(oid, info )))(thy) + in DOF_core.add_monitor_info (Binding.make (oid, pos)) (DOF_core.Monitor_Info info) thy end in o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry oid @@ -2002,8 +2041,7 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par fun close_monitor_command (args as (((oid, pos), cid_pos), doc_attrs: (((string*Position.T)*string)*string)list)) thy = - let val {monitor_tab,...} = DOF_core.get_data_global thy - fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 + let fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 in if i >= 1 then Value_Command.Docitem_Parser.msg thy @@ -2012,10 +2050,11 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), ^ " not in final state.") pos else () end - val _ = case Symtab.lookup monitor_tab oid of - SOME {automatas,...} => check_if_final automatas - | NONE => error ("Not belonging to a monitor class: "^oid) - val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid)) + val _ = let val DOF_core.Monitor_Info {automatas,...} = + DOF_core.get_monitor_info_global (oid, pos) thy + in check_if_final automatas end + val oid' = DOF_core.get_monitor_info_name_global (oid, pos) thy + val delete_monitor_entry = DOF_core.Monitor_Info.map (Name_Space.del_table oid') val DOF_core.Instance {cid=cid_long, id, ...} = DOF_core.get_object_global (oid, pos) thy val markup = docref_markup false oid id pos; val _ = Context_Position.report (Proof_Context.init_global thy) pos markup; @@ -2258,11 +2297,10 @@ 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 {monitor_tab, ...} = DOF_core.get_data ctxt; - val S = ctxt |> DOF_core.get_instances |> Name_Space.dest_table + let val S = ctxt |> DOF_core.get_instances |> Name_Space.dest_table |> filter (fn (_, DOF_core.Instance {defined,...}) => (not defined)) |> map #1 - val T = map fst (Symtab.dest monitor_tab) + val T = map fst (Name_Space.dest_table (DOF_core.get_monitor_infos ctxt)) in if null S then if null T then () else error("Global consistency error - there are open monitors: " diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index a3c27a5..1bbf2ef 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1077,8 +1077,8 @@ ML\ fun check_required_documents oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) - val {monitor_tab,...} = DOF_core.get_data ctxt' - val {accepted_cids, ...} = the (Symtab.lookup monitor_tab oid) + val DOF_core.Monitor_Info {accepted_cids, ...} = + DOF_core.get_monitor_info_global (oid, Position.none) (Context.theory_of ctxt) val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here> fun check_required_documents' [] = true | check_required_documents' (cid::cids) = diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 63b0fe8..31c43be 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -26,7 +26,7 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ val docitem_tab = DOF_core.get_instances \<^context> -val {docclass_tab, ISA_transformer_tab, monitor_tab,...} +val {docclass_tab, ISA_transformer_tab, ...} = DOF_core.get_data @{context}; Name_Space.dest_table docitem_tab; Symtab.dest docclass_tab; @@ -183,10 +183,7 @@ val t = DOF_core.get_doc_class_global long_cid thy \ open_monitor*[figs1::figure_group, caption="''Sample ''"] -ML\ -val thy = \<^theory> -val {monitor_tab,...} = DOF_core.get_data_global thy -\ +ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ text*[testFreeA::A]\\ figure*[fig_A::figure, spawn_columns=False, relative_width="90", @@ -199,20 +196,14 @@ figure*[fig_B::figure, \ The B train \ldots \ open_monitor*[figs2::figure_group, caption="''Sample ''"] -ML\ -val thy = \<^theory> -val {monitor_tab,...} = DOF_core.get_data_global thy -\ +ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ figure*[fig_C::figure, spawn_columns=False, relative_width="90", src="''figures/A.png''"] \ The C train \ldots \ open_monitor*[figs3::figure_group, caption="''Sample ''"] -ML\ -val thy = \<^theory> -val {monitor_tab,...} = DOF_core.get_data_global thy -\ +ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ figure*[fig_D::figure, spawn_columns=False,relative_width="90", @@ -222,10 +213,7 @@ close_monitor*[figs3] open_monitor*[figs4::figure_group, caption="''Sample ''"] -ML\ -val thy = \<^theory> -val {monitor_tab,...} = DOF_core.get_data_global thy -\ +ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ text*[testRejected1::figure_group, caption="''figures/A.png''"] \ The A train \ldots \ diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index a275abe..073090f 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -28,10 +28,11 @@ print_doc_classes print_doc_items (* this corresponds to low-level accesses : *) -ML\ -val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} +ML\ +val docitem_tab = DOF_core.get_instances \<^context> +val {docclass_tab, ISA_transformer_tab, ...} = DOF_core.get_data @{context}; -Symtab.dest docitem_tab; +Name_Space.dest_table docitem_tab; Symtab.dest docclass_tab; app; \ @@ -80,7 +81,7 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark (* ... generating the level-attribute syntax *) in ( Value_Command.Docitem_Parser.create_and_check_docitem - {is_monitor = false} {is_inline = false} + {is_monitor = false} {is_inline = false} {define = true} oid pos (cid_transform cid_pos) (attr_transform doc_attrs) #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) end; From 821eefb2309f24efd801d1525c6d4cc0cacaf4d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 10 Feb 2023 15:23:23 +0100 Subject: [PATCH 05/18] Fix some markups --- src/DOF/Isa_DOF.thy | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 511af36..bea02f5 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -632,8 +632,10 @@ fun define_object_global {define = define} ((oid, pos), bbb) thy = fun get_object_global (oid, pos) thy = let + val ctxt = Proof_Context.init_global thy val ((oid', rs), instance) = Name_Space.check_reports (Context.Theory thy) - (get_instances (Proof_Context.init_global thy)) (oid, [pos]) + (get_instances ctxt) (oid, [pos]) + (*val _ = Context_Position.reports ctxt rs;*) in instance end fun get_monitor_info_global (oid, pos) thy = @@ -1968,7 +1970,7 @@ fun update_instance_command (((oid, pos), cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) thy : theory = let val cid = let val DOF_core.Instance {pos=pos_decl,cid,id,...} = - DOF_core.get_object_global (oid, pos) thy + DOF_core.get_object_global (oid, Position.none) thy val markup = docref_markup false oid id pos_decl; val ctxt = Proof_Context.init_global thy; val _ = Context_Position.report ctxt pos markup; @@ -2055,8 +2057,9 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), in check_if_final automatas end val oid' = DOF_core.get_monitor_info_name_global (oid, pos) thy val delete_monitor_entry = DOF_core.Monitor_Info.map (Name_Space.del_table oid') - val DOF_core.Instance {cid=cid_long, id, ...} = DOF_core.get_object_global (oid, pos) thy - val markup = docref_markup false oid id pos; + val DOF_core.Instance {cid=cid_long, id, pos=pos_decl, ...} = + DOF_core.get_object_global (oid, pos) thy + val markup = docref_markup false oid id pos_decl; val _ = Context_Position.report (Proof_Context.init_global thy) pos markup; val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true} o Context.Theory From 2398fc579adadf1ea6acabfd6acd606a10971a04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Sat, 11 Feb 2023 22:48:11 +0100 Subject: [PATCH 06/18] Use name space markup for instances entries reporting - Name spaces offer the possibility to make reporting by embedding entries position. Use this possibility for instances (docitems) reporting - Position and theory entries in an Instance record are now useless, as this information is given by the name space. Remove them --- src/DOF/Isa_DOF.thy | 237 +++++++++--------- .../CENELEC_50128/CENELEC_50128.thy | 18 +- src/tests/Attributes.thy | 10 +- 3 files changed, 135 insertions(+), 130 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index bea02f5..76c5816 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -189,8 +189,6 @@ struct datatype instance = Instance of {defined: bool, - pos: Position.T, - thy_name: string, input_term: term, value: term, inline: bool, @@ -199,8 +197,6 @@ struct vcid: string option} val empty_instance = Instance {defined = false, - pos = Position.none, - thy_name = "", input_term = \<^term>\()\, value = \<^term>\()\, inline = false, @@ -208,9 +204,8 @@ struct cid = "", vcid = NONE} - fun make_instance (defined, pos, thy_name, input_term, value, inline, id, cid, vcid) = - Instance {defined = defined, pos = pos, thy_name = thy_name, - input_term = input_term, value = value, inline = inline, + fun make_instance (defined, input_term, value, inline, id, cid, vcid) = + Instance {defined = defined, input_term = input_term, value = value, inline = inline, id = id, cid = cid, vcid = vcid} structure Instances = Theory_Data @@ -615,11 +610,11 @@ fun define_object_global {define = define} ((oid, pos), bbb) thy = then Binding.make (Long_Name.base_name oid, pos) else Binding.make (oid, pos) val undefined_instance = "undefined_instance" - val ((oid', rs), instance) = Name_Space.check_reports (Context.Theory thy) - (get_instances (Proof_Context.init_global thy)) (oid, [pos]) - handle ERROR _ => ((undefined_instance, []), empty_instance) - val {pos, thy_name, input_term, value, inline, id, cid, vcid, ...} = bbb - val instance' = make_instance (define, pos, thy_name, input_term, value, inline, id, cid, vcid) + val (oid', instance) = Name_Space.check (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, Position.none) + handle ERROR _ => (undefined_instance, empty_instance) + val {input_term, value, inline, id, cid, vcid, ...} = bbb + val instance' = make_instance (define, input_term, value, inline, id, cid, vcid) in if oid' = undefined_instance andalso instance = empty_instance then add_instance binding instance' thy else if define @@ -630,25 +625,21 @@ fun define_object_global {define = define} ((oid, pos), bbb) thy = else add_instance binding (Instance bbb) thy end -fun get_object_global (oid, pos) thy = - let - val ctxt = Proof_Context.init_global thy - val ((oid', rs), instance) = Name_Space.check_reports (Context.Theory thy) - (get_instances ctxt) (oid, [pos]) - (*val _ = Context_Position.reports ctxt rs;*) - in instance end +fun get_object_global oid thy = + Name_Space.check (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, Position.none) |> #2 -fun get_monitor_info_global (oid, pos) thy = - let - val ((oid', rs), monitor_info) = Name_Space.check_reports (Context.Theory thy) - (get_monitor_infos (Proof_Context.init_global thy)) (oid, [pos]) - in monitor_info end +fun get_object_name_global oid thy = + Name_Space.check (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, Position.none) |> #1 -fun get_monitor_info_name_global (oid, pos) thy = - let - val ((oid', rs), monitor_info) = Name_Space.check_reports (Context.Theory thy) - (get_monitor_infos (Proof_Context.init_global thy)) (oid, [pos]) - in oid' end +fun get_monitor_info_global oid thy = + Name_Space.check (Context.Theory thy) + (get_monitor_infos (Proof_Context.init_global thy)) (oid, Position.none) |> #2 + +fun get_monitor_info_name_global oid thy = + Name_Space.check (Context.Theory thy) + (get_monitor_infos (Proof_Context.init_global thy)) (oid, Position.none) |> #1 fun get_doc_class_global cid thy = if cid = default_cid then error("default class access") (* TODO *) @@ -717,11 +708,11 @@ fun get_attribute_defaults (* long*)cid thy = |trans (na,ty,SOME def) =SOME(na,ty, def) in map_filter trans attrS end -fun get_value_global (oid, pos) thy = let val Instance v = get_object_global (oid, pos) thy +fun get_value_global oid thy = let val Instance v = get_object_global oid thy in v |> #value end -fun get_value_local (oid, pos) ctxt = - let val Instance v = get_object_global (oid, pos) (Proof_Context.theory_of ctxt) +fun get_value_local oid ctxt = + let val Instance v = get_object_global oid (Proof_Context.theory_of ctxt) in v |> #value end (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) @@ -731,11 +722,8 @@ fun update_value_global name pos upd_value thy = val binding = if Long_Name.is_qualified name then Binding.make (Long_Name.base_name name, pos) else Binding.make (name, pos) - val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy) - (get_instances (Proof_Context.init_global thy)) (name, [pos]) - val Instance {defined, pos, thy_name, input_term, value, inline, id, cid, vcid} = instance - val instance' = make_instance (defined, pos, thy_name, input_term, - upd_value value, inline, id, cid, vcid) + val Instance {defined, input_term, value, inline, id, cid, vcid} = get_object_global name thy + val instance' = make_instance (defined, input_term, upd_value value, inline, id, cid, vcid) in update_instance binding (instance') thy end fun update_input_term_global name pos upd_input_term thy = @@ -743,10 +731,8 @@ fun update_input_term_global name pos upd_input_term thy = val binding = if Long_Name.is_qualified name then Binding.make (Long_Name.base_name name, pos) else Binding.make (name, pos) - val ((oid, rs), instance) = Name_Space.check_reports (Context.Theory thy) - (get_instances (Proof_Context.init_global thy)) (name, [pos]) - val Instance {defined, pos, thy_name, input_term, value, inline, id, cid, vcid} = instance - val instance' = make_instance (defined, pos, thy_name, upd_input_term input_term, + val Instance {defined, input_term, value, inline, id, cid, vcid} = get_object_global name thy + val instance' = make_instance (defined, upd_input_term input_term, value, inline, id, cid, vcid) in update_instance binding (instance') thy end @@ -1073,11 +1059,11 @@ fun check_instance thy (term, _, pos) s = Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE)); fun check thy (name, _) = let - val object_cid = let val DOF_core.Instance cid = DOF_core.get_object_global (name, pos) thy + val object_cid = let val DOF_core.Instance cid = DOF_core.get_object_global name thy in cid |> #cid end fun check' (class_name, object_cid) = if class_name = object_cid then - DOF_core.get_value_global (name, pos) thy + 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) end @@ -1087,18 +1073,21 @@ fun ML_isa_id thy (term,pos) = SOME term fun ML_isa_check_docitem thy (term, req_ty, pos) _ = let fun check thy (name, _) s = - let val DOF_core.Instance {pos=pos_decl,cid,id,...} = - DOF_core.get_object_global (name, pos) thy - val ctxt = (Proof_Context.init_global thy) - val req_class = case req_ty of - \<^Type>\fun _ T\ => DOF_core.typ_to_cid T - | _ => error("can not infer type for: "^ name) - in if cid <> DOF_core.default_cid - andalso not(DOF_core.is_subclass ctxt cid req_class) - then error("reference ontologically inconsistent: " - ^cid^" vs. "^req_class^ Position.here pos_decl) - else () - end + let val DOF_core.Instance {cid,...} = + DOF_core.get_object_global name thy + val ns = DOF_core.get_instances (Proof_Context.init_global thy) + |> Name_Space.space_of_table + val {pos=pos', ...} = Name_Space.the_entry ns name + val ctxt = (Proof_Context.init_global thy) + val req_class = case req_ty of + \<^Type>\fun _ T\ => DOF_core.typ_to_cid T + | _ => error("can not infer type for: "^ name) + in if cid <> DOF_core.default_cid + andalso not(DOF_core.is_subclass ctxt cid req_class) + then error("reference ontologically inconsistent: " + ^cid^" vs. "^req_class^ Position.here pos') + else () + end in ML_isa_check_generic check thy (term, pos) end fun ML_isa_check_trace_attribute thy (term, _, pos) s = @@ -1106,7 +1095,7 @@ fun ML_isa_check_trace_attribute thy (term, _, pos) s = val oid = (HOLogic.dest_string term handle TERM(_,[t]) => error ("wrong term format: must be string constant: " ^ Syntax.string_of_term_global thy t )) - val _ = DOF_core.get_object_global (oid, pos) thy + val _ = DOF_core.get_object_global oid thy in SOME term end @@ -1119,7 +1108,7 @@ fun elaborate_instance thy _ _ term_option pos = case term_option of NONE => error ("Malformed term annotation") | SOME term => let val instance_name = HOLogic.dest_string term - val value = DOF_core.get_value_global (instance_name, pos) thy + val value = DOF_core.get_value_global instance_name thy in DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy end @@ -1167,7 +1156,7 @@ fun elaborate_instances_list thy isa_name _ _ pos = |> filter (fn (_, instance) => let val DOF_core.Instance cid = instance in (cid |> #cid) = long_class_name end) - |> map (fn (oid, _) => DOF_core.get_value_global (oid, pos) thy) + |> map (fn (oid, _) => DOF_core.get_value_global oid thy) in HOLogic.mk_list class_typ values end @@ -1202,12 +1191,15 @@ in Value_Command.value ctxt (subterm') end fun compute_attr_access ctxt attr oid pos_option pos' = (* template *) let - val value = DOF_core.get_value_global (oid, pos') (Context.theory_of ctxt) + val value = DOF_core.get_value_global oid (Context.theory_of ctxt) val ctxt' = Context.proof_of ctxt - val DOF_core.Instance {cid,pos=pos_decl,id,...} = - DOF_core.get_object_global (oid, pos') (Context.theory_of ctxt) - val docitem_markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report ctxt' pos' docitem_markup; + val thy = Context.theory_of ctxt + val DOF_core.Instance {cid,...} = + DOF_core.get_object_global oid thy + val instances = DOF_core.get_instances ctxt' + val markup = DOF_core.get_object_name_global oid thy + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt' pos' markup; val (* (long_cid, attr_b,ty) = *) {long_name, typ=ty, def_pos, ...} = case DOF_core.get_attribute_info_local cid attr ctxt' of @@ -1637,11 +1629,18 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = in (moid,map check_for_cid indexed_autoS, monitor_info) end val enabled_monitors = List.mapPartial is_enabled (Name_Space.dest_table (DOF_core.get_monitor_infos (Proof_Context.init_global thy))) + val enabled_monitors_pos = + enabled_monitors + |> map (fn (s, mi) => + let val ns = DOF_core.get_instances (Proof_Context.init_global thy) + |> Name_Space.space_of_table + val {pos, ...} = Name_Space.the_entry ns s + in (s, pos) end) fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, Syntax.read_term_global thy rhs) val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] val assns' = map conv_attrs trace_attr - fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_object_global (oid, pos) thy + fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_object_global oid thy in #cid params end fun def_trans_input_term oid = #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') @@ -1659,13 +1658,13 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = in Name_Space.map_table_entry n (fn _ => DOF_core.make_monitor_info (accepted_cids, rejected_cids, aS)) end - fun update_trace mon_oid = + fun update_trace (mon_oid, pos) = if Config.get_global thy DOF_core.object_value_debug then DOF_core.update_value_input_term_global mon_oid pos (def_trans_input_term mon_oid) (def_trans_value mon_oid) else DOF_core.update_value_global mon_oid pos (def_trans_value mon_oid) in thy |> (* update traces of all enabled monitors *) - fold update_trace (map #1 enabled_monitors) + fold update_trace enabled_monitors_pos |> (* check class invariants of enabled monitors *) (fn thy => (class_inv_checks (Context.Theory thy); thy)) |> (* update the automata of enabled monitors *) @@ -1674,8 +1673,8 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = fun check_invariants thy (oid, pos) = let - val docitem_value = DOF_core.get_value_global (oid, pos) thy - val DOF_core.Instance params = DOF_core.get_object_global (oid, pos) thy + val docitem_value = DOF_core.get_value_global oid thy + val DOF_core.Instance params = DOF_core.get_object_global oid thy val cid = #cid params fun get_all_invariants cid thy = case DOF_core.get_doc_class_global cid thy of @@ -1748,10 +1747,7 @@ fun check_invariants thy (oid, pos) = fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oid pos cid_pos doc_attrs thy = let - val id = serial (); - val _ = Position.report pos (docref_markup true oid id pos); - (* creates a markup label for this position and reports it to the PIDE framework; - this label is used as jump-target for point-and-click feature. *) + val id = serial (); val cid_pos' = check_classref is_monitor cid_pos thy val cid_long = fst cid_pos' val default_cid = cid_long = DOF_core.default_cid @@ -1786,8 +1782,6 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) o Context.Theory in thy |> DOF_core.define_object_global {define = define} ((oid, pos), {defined = false, - pos = pos, - thy_name = Context.theory_name thy, input_term = fst value_terms, value = value (Proof_Context.init_global thy) (snd value_terms), @@ -1969,10 +1963,12 @@ struct fun update_instance_command (((oid, pos), cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) thy : theory = - let val cid = let val DOF_core.Instance {pos=pos_decl,cid,id,...} = - DOF_core.get_object_global (oid, Position.none) thy - val markup = docref_markup false oid id pos_decl; - val ctxt = Proof_Context.init_global thy; + let val cid = let val DOF_core.Instance {cid,...} = + DOF_core.get_object_global oid thy + val ctxt = Proof_Context.init_global thy + val instances = DOF_core.get_instances ctxt + val markup = DOF_core.get_object_name_global oid thy + |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; in cid end val cid_pos' = Value_Command.Docitem_Parser.check_classref {is_monitor = false} @@ -1995,11 +1991,15 @@ fun update_instance_command (((oid, pos), cid_pos), fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} o Context.Theory ) thy ; thy) + val ns = DOF_core.get_instances (Proof_Context.init_global thy) + |> Name_Space.space_of_table + val {pos = pos', ...} = + Name_Space.the_entry ns (DOF_core.get_object_name_global oid thy) in thy |> (if Config.get_global thy DOF_core.object_value_debug - then DOF_core.update_value_input_term_global oid pos + then DOF_core.update_value_input_term_global oid pos' def_trans_input_term def_trans_value - else DOF_core.update_value_global oid pos + else DOF_core.update_value_global oid pos' def_trans_value) |> check_inv |> (fn thy => if Config.get_global thy DOF_core.invariants_checking @@ -2053,14 +2053,16 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), else () end val _ = let val DOF_core.Monitor_Info {automatas,...} = - DOF_core.get_monitor_info_global (oid, pos) thy + DOF_core.get_monitor_info_global oid thy in check_if_final automatas end - val oid' = DOF_core.get_monitor_info_name_global (oid, pos) thy + val oid' = DOF_core.get_monitor_info_name_global oid thy val delete_monitor_entry = DOF_core.Monitor_Info.map (Name_Space.del_table oid') - val DOF_core.Instance {cid=cid_long, id, pos=pos_decl, ...} = - DOF_core.get_object_global (oid, pos) thy - val markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report (Proof_Context.init_global thy) pos markup; + val DOF_core.Instance {cid=cid_long,...} = DOF_core.get_object_global oid thy + val ctxt = Proof_Context.init_global thy + val instances = DOF_core.get_instances ctxt + val markup = DOF_core.get_object_name_global oid thy + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt pos markup; val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true} o Context.Theory val check_lazy_inv = (DOF_core.get_class_lazy_invariant cid_long thy oid) {is_monitor=true} @@ -2082,7 +2084,7 @@ fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Pa (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) val cid_long = case cid_opt of NONE => let val DOF_core.Instance cid = - DOF_core.get_object_global (lab, pos) thy + DOF_core.get_object_global lab thy in cid |> #cid end | SOME(cid,_) => DOF_core.parse_cid_global thy cid @@ -2275,8 +2277,7 @@ fun print_doc_items b ctxt = val _ = writeln "====================================="; fun dfg true = "true" |dfg false= "false" - fun print_item (n, DOF_core.Instance {defined,cid,vcid,id,pos, - thy_name,inline, input_term, value}) = + fun print_item (n, DOF_core.Instance {defined,cid,vcid,id, inline, input_term, value}) = ((if defined then writeln ("docitem: "^n) else @@ -2285,7 +2286,6 @@ fun print_doc_items b ctxt = writeln (" type: "^cid); case vcid of NONE => () | SOME (s) => writeln (" virtual type: "^ s); - writeln (" origin: "^thy_name); writeln (" inline: "^dfg inline); (if Config.get ctxt DOF_core.object_value_debug then writeln (" input_term: "^ (Syntax.string_of_term ctxt input_term)) @@ -2360,7 +2360,7 @@ fun meta_args_2_string thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_P (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) val cid_long = case cid_opt of NONE => let val DOF_core.Instance cid = - DOF_core.get_object_global (lab, pos) thy + DOF_core.get_object_global lab thy in cid |> #cid end | SOME(cid,_) => DOF_core.parse_cid_global thy cid (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) @@ -2434,19 +2434,22 @@ val basic_entity = Document_Output.antiquotation_pretty_source fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = let val thy = Proof_Context.theory_of ctxt; - val DOF_core.Instance {pos=pos_decl,id,cid,inline,...} = - DOF_core.get_object_global (name, pos) thy + val DOF_core.Instance {cid,inline,...} = DOF_core.get_object_global name thy val _ = if not inline_req then if inline then () else error("referred text-element is macro! (try option display)") else if not inline then () else error("referred text-element is no macro!") - val markup = docref_markup false name id pos_decl; + val instances = DOF_core.get_instances ctxt + val name' = DOF_core.get_object_name_global name thy + val markup = name' |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; + val ns = instances |> Name_Space.space_of_table + val {pos=pos', ...} = Name_Space.the_entry ns name' (* this sends a report for a ref application to the PIDE interface ... *) val _ = if not(DOF_core.is_subclass ctxt cid cid_decl) then error("reference ontologically inconsistent: "^cid - ^" must be subclass of "^cid_decl^ Position.here pos_decl) + ^" must be subclass of "^cid_decl^ Position.here pos') else () - in () end + in () end val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} -> {inline:bool} -> @@ -2492,10 +2495,15 @@ fun docitem_antiquotation bind cid = fun check_and_mark_term ctxt oid = let val thy = Context.theory_of ctxt; - val DOF_core.Instance {pos=pos_decl,id,cid,value,...} = - DOF_core.get_object_global (oid, Position.none) thy - val markup = docref_markup false oid id pos_decl; - val _ = Context_Position.report_generic ctxt pos_decl markup; + val ctxt' = Context.proof_of ctxt + val DOF_core.Instance {cid,value,...} = + DOF_core.get_object_global oid thy + val instances = DOF_core.get_instances ctxt' + val ns = instances |> Name_Space.space_of_table + val {pos, ...} = Name_Space.the_entry ns oid + val markup = DOF_core.get_object_name_global oid thy + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt' pos markup; (* this sends a report for a ref application to the PIDE interface ... *) val _ = if cid = DOF_core.default_cid then error("anonymous "^ DOF_core.default_cid ^ " class has no value" ) @@ -2557,20 +2565,19 @@ fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o M fun get_instance_value_2_ML ctxt (oid:string,pos) = let val ctxt' = Context.the_proof ctxt - val value = let val DOF_core.Instance {pos=pos_decl,id,value,...} = - DOF_core.get_object_global (oid, pos) (Context.theory_of ctxt) - val markup = docref_markup false oid id pos_decl - val _ = Context_Position.report ctxt' pos markup - in value end + val value = DOF_core.get_value_local oid ctxt' + val instances = DOF_core.get_instances ctxt' + val markup = DOF_core.get_object_name_global oid (Proof_Context.theory_of ctxt') + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt' pos markup; 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 _ = let val DOF_core.Instance {pos=pos_decl,id,...} = - DOF_core.get_object_global (oid, pos) (Context.theory_of ctxt) - val markup = docref_markup false oid id pos_decl - val _ = Context_Position.report ctxt' pos markup - in () end + val instances = DOF_core.get_instances ctxt' + val markup = DOF_core.get_object_name_global oid (Proof_Context.theory_of ctxt') + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt' pos markup; in "\"" ^ oid ^ "\"" end fun trace_attr_2_ML ctxt (oid:string,pos) = @@ -2583,11 +2590,10 @@ fun compute_cid_repr ctxt cid pos = else ISA_core.err ("Undefined Class Identifier:"^cid) pos fun compute_name_repr ctxt oid pos = - let val _ = let val DOF_core.Instance {pos=pos_decl,id,...} = - DOF_core.get_object_global (oid, pos) (Proof_Context.theory_of ctxt) - val markup = docref_markup false oid id pos_decl - val _ = Context_Position.report ctxt pos markup - in () end + let val instances = DOF_core.get_instances ctxt + val markup = DOF_core.get_object_name_global oid (Proof_Context.theory_of ctxt) + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt pos markup; in HOLogic.mk_string oid end local @@ -2806,7 +2812,6 @@ fun add_doc_class_cmd overloaded (raw_params, binding) #> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps reject_Atoms invariants {virtual=true} ) - |> (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) diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 1bbf2ef..14edeaf 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1010,7 +1010,7 @@ fun check_sil oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_object_global oid (Context.theory_of ctxt) val Const _ $ _ $ monitor_sil $ _ = monitor_record_value val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here> fun check_sil'' [] = true @@ -1018,7 +1018,7 @@ fun check_sil oid _ ctxt = let val (_, doc_oid) = x val DOF_core.Instance {value = doc_record_value, ...} = - DOF_core.get_object_global (doc_oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_object_global doc_oid (Context.theory_of ctxt) val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext in @@ -1041,9 +1041,9 @@ fun check_sil_slow oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_object_global oid (Context.theory_of ctxt) val DOF_core.Instance {cid = monitor_cid, ...} = - DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_object_global oid (Context.theory_of ctxt) val monitor_sil_typ = (Syntax.read_typ ctxt' monitor_cid) --> @{typ "sil"} val monitor_sil = Value_Command.value ctxt' (Const("CENELEC_50128.monitor_SIL.sil", monitor_sil_typ) $ monitor_record_value) @@ -1053,7 +1053,7 @@ fun check_sil_slow oid _ ctxt = let val (doc_cid, doc_oid) = x val DOF_core.Instance {value = doc_record_value, ...} = - DOF_core.get_object_global (doc_oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_object_global doc_oid (Context.theory_of ctxt) val doc_sil_typ = (Syntax.read_typ ctxt' doc_cid) --> @{typ "sil"} val doc_sil = Value_Command.value ctxt' (Const ("CENELEC_50128.cenelec_document.sil", doc_sil_typ) $ doc_record_value) @@ -1078,7 +1078,7 @@ fun check_required_documents oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Monitor_Info {accepted_cids, ...} = - DOF_core.get_monitor_info_global (oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_monitor_info_global oid (Context.theory_of ctxt) val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here> fun check_required_documents' [] = true | check_required_documents' (cid::cids) = @@ -1088,7 +1088,7 @@ fun check_required_documents oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global (oid, Position.none) (Context.theory_of ctxt) + DOF_core.get_object_global oid (Context.theory_of ctxt) val Const _ $ _ $ monitor_sil $ _ = monitor_record_value in error ("A " ^ cid ^ " cenelec document is required with " ^ Syntax.string_of_term ctxt' monitor_sil) @@ -1108,10 +1108,10 @@ text*[CenelecClassPatternMatchingTest::SQAP, sil = "SIL0"]\\ ML\ val thy = @{theory} val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global ("MonitorPatternMatchingTest", Position.none) thy + DOF_core.get_object_global "MonitorPatternMatchingTest" thy val Const _ $ _ $ monitor_sil $ _ = monitor_record_value val DOF_core.Instance {value = doc_record_value, ...} = - DOF_core.get_object_global ("CenelecClassPatternMatchingTest", Position.none) thy + DOF_core.get_object_global "CenelecClassPatternMatchingTest" thy val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext \ diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 31c43be..691c64f 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -125,11 +125,11 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory}; ML\ -DOF_core.get_value_local ("sdf", Position.none) @{context}; -DOF_core.get_value_local ("sdfg", Position.none) @{context}; -DOF_core.get_value_local ("xxxy", Position.none) @{context}; -DOF_core.get_value_local ("dfgdfg", Position.none) @{context}; -DOF_core.get_value_local ("omega", Position.none) @{context}; +DOF_core.get_value_local "sdf" @{context}; +DOF_core.get_value_local "sdfg" @{context}; +DOF_core.get_value_local "xxxy" @{context}; +DOF_core.get_value_local "dfgdfg" @{context}; +DOF_core.get_value_local "omega" @{context}; \ text\A not too trivial test: default y -> []. From 4a77347e40fc336b188fb806189f65eb41ee43c2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Sun, 12 Feb 2023 11:16:07 +0100 Subject: [PATCH 07/18] Simplify reporting of monitors --- src/DOF/Isa_DOF.thy | 49 +++++++++++++++++++-------------------------- 1 file changed, 21 insertions(+), 28 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 76c5816..e048668 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -717,27 +717,32 @@ fun get_value_local oid ctxt = (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) -fun update_value_global name pos upd_value thy = +fun binding_from_instance_pos name thy = let - val binding = if Long_Name.is_qualified name - then Binding.make (Long_Name.base_name name, pos) - else Binding.make (name, pos) + val ns = get_instances (Proof_Context.init_global thy) + |> Name_Space.space_of_table + val {pos, ...} = Name_Space.the_entry ns (get_object_name_global name thy) + in if Long_Name.is_qualified name + then Binding.make (Long_Name.base_name name, pos) + else Binding.make (name, pos)end + +fun update_value_global name upd_value thy = + let + val binding = binding_from_instance_pos name thy val Instance {defined, input_term, value, inline, id, cid, vcid} = get_object_global name thy val instance' = make_instance (defined, input_term, upd_value value, inline, id, cid, vcid) in update_instance binding (instance') thy end -fun update_input_term_global name pos upd_input_term thy = +fun update_input_term_global name upd_input_term thy = let - val binding = if Long_Name.is_qualified name - then Binding.make (Long_Name.base_name name, pos) - else Binding.make (name, pos) + val binding = binding_from_instance_pos name thy val Instance {defined, input_term, value, inline, id, cid, vcid} = get_object_global name thy val instance' = make_instance (defined, upd_input_term input_term, value, inline, id, cid, vcid) in update_instance binding (instance') thy end -fun update_value_input_term_global name pos upd_input_term upd_value thy = - update_value_global name pos upd_value thy |> update_input_term_global name pos upd_input_term +fun update_value_input_term_global name upd_input_term upd_value thy = + update_value_global name upd_value thy |> update_input_term_global name upd_input_term val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) @@ -1629,13 +1634,6 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = in (moid,map check_for_cid indexed_autoS, monitor_info) end val enabled_monitors = List.mapPartial is_enabled (Name_Space.dest_table (DOF_core.get_monitor_infos (Proof_Context.init_global thy))) - val enabled_monitors_pos = - enabled_monitors - |> map (fn (s, mi) => - let val ns = DOF_core.get_instances (Proof_Context.init_global thy) - |> Name_Space.space_of_table - val {pos, ...} = Name_Space.the_entry ns s - in (s, pos) end) fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, Syntax.read_term_global thy rhs) val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] @@ -1658,13 +1656,13 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = in Name_Space.map_table_entry n (fn _ => DOF_core.make_monitor_info (accepted_cids, rejected_cids, aS)) end - fun update_trace (mon_oid, pos) = + fun update_trace mon_oid = if Config.get_global thy DOF_core.object_value_debug - then DOF_core.update_value_input_term_global mon_oid pos + then DOF_core.update_value_input_term_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid) - else DOF_core.update_value_global mon_oid pos (def_trans_value mon_oid) + else DOF_core.update_value_global mon_oid (def_trans_value mon_oid) in thy |> (* update traces of all enabled monitors *) - fold update_trace enabled_monitors_pos + fold update_trace (map #1 enabled_monitors) |> (* check class invariants of enabled monitors *) (fn thy => (class_inv_checks (Context.Theory thy); thy)) |> (* update the automata of enabled monitors *) @@ -1991,16 +1989,11 @@ fun update_instance_command (((oid, pos), cid_pos), fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} o Context.Theory ) thy ; thy) - val ns = DOF_core.get_instances (Proof_Context.init_global thy) - |> Name_Space.space_of_table - val {pos = pos', ...} = - Name_Space.the_entry ns (DOF_core.get_object_name_global oid thy) in thy |> (if Config.get_global thy DOF_core.object_value_debug - then DOF_core.update_value_input_term_global oid pos' + then DOF_core.update_value_input_term_global oid def_trans_input_term def_trans_value - else DOF_core.update_value_global oid pos' - def_trans_value) + else DOF_core.update_value_global oid def_trans_value) |> check_inv |> (fn thy => if Config.get_global thy DOF_core.invariants_checking then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) From 7c16d02979c0c49878ce6047ced5062cd42a8033 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Sun, 12 Feb 2023 15:56:06 +0100 Subject: [PATCH 08/18] Use a name space for Isabelle_DOF transformers - Use a name space table to store Isabelle_DOF transformers objects - Remove ISA_transformer_tab table and accesses --- src/DOF/Isa_DOF.thy | 246 ++++++++++++++++--------------- src/tests/Attributes.thy | 4 +- src/tests/TermAntiquotations.thy | 5 +- 3 files changed, 131 insertions(+), 124 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index e048668..93a0c1a 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -74,6 +74,7 @@ val makeN = "make" val schemeN = "_scheme" val instanceN = "instance" val monitor_infoN = "monitor_info" +val isa_transformerN = "isa_transformer" (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = @@ -242,13 +243,48 @@ struct SOME entry => entry | NONE => raise TYPE ("Unknown instance: " ^ quote i, [], [])); - type ISA_transformers = {check : - (theory -> term * typ * Position.T -> string -> term option), - elaborate : (theory -> string -> typ -> term option -> Position.T -> term) - } - type ISA_transformer_tab = ISA_transformers Symtab.table - val initial_ISA_tab:ISA_transformer_tab = Symtab.empty + datatype isa_transformer = ISA_Transformer of + {check : (theory -> term * typ * Position.T -> string -> term option), + elaborate : (theory -> string -> typ -> term option -> Position.T -> term)} + + fun make_isa_transformer (check, elaborate) = + ISA_Transformer {check = check, elaborate = elaborate} + + structure ISA_Transformers = Theory_Data + ( + type T = isa_transformer Name_Space.table; + val empty : T = Name_Space.empty_table isa_transformerN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_isa_transformers = ISA_Transformers.get o Proof_Context.theory_of + + fun check_isa_transformer ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_isa_transformers ctxt); + + fun add_isa_transformer name isa_transformer thy = + thy |> ISA_Transformers.map + (Name_Space.define (Context.Theory thy) true (name, isa_transformer) #> #2); + + fun update_isa_transformer name isa_transformer thy = + thy |> ISA_Transformers.map + (Name_Space.define (Context.Theory thy) false (name, isa_transformer) #> #2); + + fun update_isa_transformer_entry name new_isa_transformer thy = + thy |> ISA_Transformers.map + (Name_Space.map_table_entry name (fn _ => new_isa_transformer)); + + fun print_isa_transformers verbose ctxt = + Pretty.big_list "Isabelle.DOF ISA_Transformers:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_isa_transformers ctxt))) + |> Pretty.writeln; + + fun the_isa_transformer T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown isa_transformer: " ^ quote i, [], [])); + type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty @@ -314,32 +350,21 @@ struct structure Data = Generic_Data ( type T = {docclass_tab : docclass_tab, - ISA_transformer_tab : ISA_transformer_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 = {docclass_tab = initial_docclass_tab, - ISA_transformer_tab = initial_ISA_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( {docclass_tab = c1, - ISA_transformer_tab = e1, docclass_inv_tab = n1, docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1}, {docclass_tab = c2, - ISA_transformer_tab = e2, docclass_inv_tab = n2, docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) = {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. - 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), docclass_inv_tab = override(n1,n2), (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) docclass_eager_inv_tab = override(en1,en2), @@ -356,43 +381,33 @@ val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; -fun upd_docclass_tab f {docclass_tab = y,ISA_transformer_tab = z, +fun upd_docclass_tab f {docclass_tab = y, docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = f y,ISA_transformer_tab = z, + {docclass_tab = f y, 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 {docclass_tab = y,ISA_transformer_tab = z, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = y,ISA_transformer_tab = f z, - 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 {docclass_tab,ISA_transformer_tab, +fun upd_docclass_inv_tab f {docclass_tab, docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = {docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_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 {docclass_tab,ISA_transformer_tab, +fun upd_docclass_eager_inv_tab f {docclass_tab, docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = {docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_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 {docclass_tab,ISA_transformer_tab, +fun upd_docclass_lazy_inv_tab f {docclass_tab, docclass_inv_tab, docclass_eager_inv_tab, docclass_lazy_inv_tab} = {docclass_tab = docclass_tab, - ISA_transformer_tab = ISA_transformer_tab, docclass_inv_tab=docclass_inv_tab, docclass_eager_inv_tab=docclass_eager_inv_tab, docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; @@ -745,7 +760,7 @@ fun update_value_input_term_global name upd_input_term upd_value thy = update_value_global name upd_value thy |> update_input_term_global name upd_input_term -val ISA_prefix = "ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) +val ISA_prefix = "Isabelle_DOF_" val doc_class_prefix = ISA_prefix ^ "doc_class_" @@ -766,54 +781,38 @@ fun is_class_ISA thy s = let val bname = Long_Name.base_name s 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 - NONE => error("undefined inner syntax antiquotation: "^isa) - | SOME(bbb) => bbb - - -fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data ctxt)) (ISA_prefix^isa) of - NONE => error("undefined inner syntax antiquotation: "^isa) - |SOME(bbb) => bbb - -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_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 {mk_elaboration=mk_elaboration} (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 is_ISA s - then case Symtab.lookup tab s of - NONE => error("undefined inner syntax antiquotation: "^s) - | SOME({check=check, elaborate=elaborate}) => - case check thy (t,ty,pos) s of - NONE => Const(s,ty) $ t - (* checking isa, may raise error though. *) - | SOME t => if mk_elaboration - then elaborate thy s ty (SOME t) pos - else Const(s,ty) $ t - (* transforming isa *) - else (Const(s,ty) $ (T t)) - |T(t1 $ t2) = T(t1) $ T(t2) - |T(Const(s,ty)) = if is_ISA s - then case Symtab.lookup tab s of - NONE => error("undefined inner syntax antiquotation: "^s) - | SOME({elaborate=elaborate, ...}) => - if mk_elaboration - then elaborate thy s ty NONE pos - else Const(s, ty) - (* transforming isa *) - else Const(s, ty) - |T(Abs(s,ty,t)) = Abs(s,ty,T t) - |T t = t + let val ctxt = Proof_Context.init_global thy + val tab = get_isa_transformers ctxt + fun T(Const(s,ty) $ t) = + if is_ISA s + then let val name = check_isa_transformer ctxt (s, Position.none) + val (_, ISA_Transformer {check, elaborate}) = the_isa_transformer tab name + in case check thy (t,ty,pos) s of + NONE => Const(s,ty) $ t + (* checking isa, may raise error though. *) + | SOME t => if mk_elaboration + then elaborate thy s ty (SOME t) pos + else Const(s,ty) $ t + (* transforming isa *) + end + else (Const(s,ty) $ (T t)) + | T(t1 $ t2) = T(t1) $ T(t2) + | T(Const(s,ty)) = + if is_ISA s + then + let val name = check_isa_transformer ctxt (s, Position.none) + val (_, ISA_Transformer {elaborate, ...}) = the_isa_transformer tab name + in if mk_elaboration + then elaborate thy s ty NONE pos + else Const(s, ty) + (* transforming isa *) + end + else Const(s, ty) + | T(Abs(s,ty,t)) = Abs(s,ty,T t) + | T t = t in T term end fun elaborate_term ctxt term = transduce_term_global {mk_elaboration=true} @@ -893,15 +892,15 @@ datatype "doc_class" = mk string \ \and others in the future : file, http, thy, ...\ -datatype "typ" = ISA_typ string ("@{typ _}") -datatype "term" = ISA_term string ("@{term _}") -consts ISA_term_repr :: "string \ term" ("@{termrepr _}") -datatype "thm" = ISA_thm string ("@{thm _}") -datatype "file" = ISA_file string ("@{file _}") -datatype "thy" = ISA_thy string ("@{thy _}") -consts ISA_docitem :: "string \ 'a" ("@{docitem _}") -datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}") -consts ISA_trace_attribute :: "string \ (string * string) list" ("@{trace-attribute _}") +datatype "typ" = Isabelle_DOF_typ string ("@{typ _}") +datatype "term" = Isabelle_DOF_term string ("@{term _}") +consts Isabelle_DOF_term_repr :: "string \ term" ("@{termrepr _}") +datatype "thm" = Isabelle_DOF_thm string ("@{thm _}") +datatype "file" = Isabelle_DOF_file string ("@{file _}") +datatype "thy" = Isabelle_DOF_thy string ("@{thy _}") +consts Isabelle_DOF_docitem :: "string \ 'a" ("@{docitem _}") +datatype "docitem_attr" = Isabelle_DOF_docitem_attr string string ("@{docitemattr (_) :: (_)}") +consts Isabelle_DOF_trace_attribute :: "string \ (string * string) list" ("@{trace-attribute _}") \ \Dynamic setup of inner syntax cartouche\ @@ -1135,15 +1134,8 @@ fun declare_ISA_class_accessor_and_check_instance 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 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=check_instance, elaborate=elaborate_instance}) thy - end) + #> DOF_core.add_isa_transformer bind (DOF_core.make_isa_transformer + (check_instance, elaborate_instance)) end fun elaborate_instances_list thy isa_name _ _ pos = @@ -1179,14 +1171,8 @@ fun declare_class_instances_annotation thy doc_class_name = val mixfix_string = "@{" ^ conv_class_name' ^ "}" in Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))] - #> (fn thy => let - val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) - val qual = Long_Name.qualifier long_name - val transformer_name = Long_Name.qualify qual - (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind')) - in - DOF_core.update_isa_global (transformer_name, - {check=check_identity, elaborate= elaborate_instances_list}) thy end) + #> DOF_core.add_isa_transformer bind' (DOF_core.make_isa_transformer + (check_identity, elaborate_instances_list)) end fun symbex_attr_access0 ctxt proj_term term = @@ -1245,8 +1231,8 @@ case term_option of (* utilities *) fun property_list_dest ctxt X = - map (fn \<^Const_>\ISA_term for s\ => HOLogic.dest_string s - |\<^Const_>\ISA_term_repr for s\ => holstring_to_bstring ctxt (HOLogic.dest_string s)) + map (fn \<^Const_>\Isabelle_DOF_term for s\ => HOLogic.dest_string s + |\<^Const_>\Isabelle_DOF_term_repr for s\ => holstring_to_bstring ctxt (HOLogic.dest_string s)) (HOLogic.dest_list X) end; (* struct *) @@ -1255,21 +1241,41 @@ end; (* struct *) subsection\ Isar - Setup\ +(* Isa_transformers declaration for Isabelle_DOF term anti-quotations (typ, term, thm, etc.). + They must be declared in the same theory file as the one of the declaration + of Isabelle_DOF term anti-quotations !!! *) +setup\ +[(\<^type_name>\typ\, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_generic) + , (\<^type_name>\term\, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_generic) + , (\<^type_name>\thm\, ISA_core.ML_isa_check_thm, ISA_core.ML_isa_elaborate_generic) + , (\<^type_name>\file\, ISA_core.ML_isa_check_file, ISA_core.ML_isa_elaborate_generic)] +|> fold (fn (n, check, elaborate) => fn thy => +let val ns = Sign.tsig_of thy |> Type.type_space + val name = n + val {pos, ...} = Name_Space.the_entry ns name + val bname = Long_Name.base_name name + val binding = Binding.make (bname, pos) + val binding' = (Binding.prefix_name DOF_core.ISA_prefix binding) + |> Binding.prefix false bname +in DOF_core.add_isa_transformer binding' ((check, elaborate) |> DOF_core.make_isa_transformer) thy +end) +#> +([(\<^const_name>\Isabelle_DOF_term_repr\, + ISA_core.check_identity, ISA_core.ML_isa_elaborate_generic) + ,(\<^const_name>\Isabelle_DOF_docitem\, + ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic) + ,(\<^const_name>\Isabelle_DOF_trace_attribute\, + ISA_core.ML_isa_check_trace_attribute, ISA_core.ML_isa_elaborate_trace_attribute)] +|> fold (fn (n, check, elaborate) => fn thy => +let val ns = Sign.consts_of thy |> Consts.space_of + val name = n + val {pos, ...} = Name_Space.the_entry ns name + val bname = Long_Name.base_name name + val binding = Binding.make (bname, pos) +in DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy +end)) +\ -setup\DOF_core.update_isa_global("Isa_DOF.typ.typ", - {check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.term.term", - {check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.term_repr", - {check=ISA_core.check_identity, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.thm.thm", - {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.file.file", - {check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.docitem", - {check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \ -setup\DOF_core.update_isa_global("Isa_DOF.trace_attribute", - {check=ISA_core.ML_isa_check_trace_attribute, elaborate=ISA_core.ML_isa_elaborate_trace_attribute}) \ section\ Syntax for Annotated Documentation Commands (the '' View'' Part I) \ diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 691c64f..90240e2 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -26,8 +26,8 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ val docitem_tab = DOF_core.get_instances \<^context> -val {docclass_tab, ISA_transformer_tab, ...} - = DOF_core.get_data @{context}; +val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> +val {docclass_tab, ...} = DOF_core.get_data @{context}; Name_Space.dest_table docitem_tab; Symtab.dest docclass_tab; \ diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy index 72252e4..e0b15c8 100644 --- a/src/tests/TermAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -43,8 +43,9 @@ ODL on a paradigmatical example. text\Voila the content of the Isabelle_DOF environment so far:\ ML\ val x = DOF_core.get_instances \<^context> -val {docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context}; - Symtab.dest ISA_transformer_tab; +val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> +val {docclass_tab,...} = DOF_core.get_data @{context}; +Name_Space.dest_table isa_transformer_tab; \ text\Some sample lemma:\ From e01ec9fc21ca8dac01be7701801ed65ccf092d95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Sun, 12 Feb 2023 17:57:35 +0100 Subject: [PATCH 09/18] Use a name space for ML invariants - Use a name space table to store ML inariants objects - Remove docclass_inv_tab, docclass_eager_inv_tab, and docclass_lazy_inv_tab tables and accesses --- .../Isabelle_DOF-Manual/04_RefMan.thy | 4 +- src/DOF/Isa_DOF.thy | 309 ++++++++++-------- .../CENELEC_50128/CENELEC_50128.thy | 27 +- .../scholarly_paper/scholarly_paper.thy | 18 +- src/ontologies/small_math/small_math.thy | 22 +- .../Concept_Example_Low_Level_Invariant.thy | 40 ++- 6 files changed, 261 insertions(+), 159 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 189a457..26819e7 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1218,8 +1218,8 @@ text\ Low-level invariants checking can be set up to be triggered when opening a monitor, when closing a monitor, or both - by using the \<^ML>\DOF_core.update_class_eager_invariant\, - \<^ML>\DOF_core.update_class_lazy_invariant\, or \<^ML>\DOF_core.update_class_invariant\ commands + by using the \<^ML>\DOF_core.add_opening_ml_invariant\, + \<^ML>\DOF_core.add_closing_ml_invariant\, or \<^ML>\DOF_core.add_ml_invariant\ commands respectively, to add the invariants to the theory context (See \<^technical>\sec:low_level_inv\ for an example). \ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 93a0c1a..1939072 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -69,12 +69,13 @@ val def_suffixN = "_" ^ defN val defsN = defN ^ "s" val instances_of_suffixN = "_instances" val invariant_suffixN = "_inv" -val invariantN = "\" +val instance_placeholderN = "\" val makeN = "make" val schemeN = "_scheme" val instanceN = "instance" val monitor_infoN = "monitor_info" val isa_transformerN = "isa_transformer" +val ml_invariantN = "ml_invariant" (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = @@ -286,16 +287,134 @@ struct | NONE => raise TYPE ("Unknown isa_transformer: " ^ quote i, [], [])); - type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty + type ml_invariant = string -> {is_monitor:bool} -> Context.generic -> bool - type docclass_eager_inv_tab = - (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_eager_inv_tab : docclass_eager_inv_tab = Symtab.empty + structure ML_Invariants = Theory_Data + ( + type T = ml_invariant Name_Space.table; + val empty : T = Name_Space.empty_table ml_invariantN; + fun merge data : T = Name_Space.merge_tables data; + ); - type docclass_lazy_inv_tab = - (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_lazy_inv_tab : docclass_lazy_inv_tab = Symtab.empty + val get_ml_invariants = ML_Invariants.get o Proof_Context.theory_of + + fun get_ml_invariant_global cid thy = + Name_Space.check (Context.Theory thy) + (get_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #2 + + fun get_ml_invariant_name_global cid thy = + Name_Space.check (Context.Theory thy) + (get_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #1 + + fun check_ml_invariant ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_ml_invariants ctxt); + + fun add_ml_invariant name ml_invariant thy = + thy |> ML_Invariants.map + (Name_Space.define (Context.Theory thy) true (name, ml_invariant) #> #2); + + fun update_ml_invariant name ml_invariant thy = + thy |> ML_Invariants.map + (Name_Space.define (Context.Theory thy) false (name, ml_invariant) #> #2); + + fun update_ml_invariant_entry name new_ml_invariant thy = + thy |> ML_Invariants.map + (Name_Space.map_table_entry name (fn _ => new_ml_invariant)); + + fun print_ml_invariants verbose ctxt = + Pretty.big_list "Isabelle.DOF ML_Invariants:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_ml_invariants ctxt))) + |> Pretty.writeln; + + fun the_ml_invariant T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown ml_invariant: " ^ quote i, [], [])); + + + structure Opening_ML_Invariants = Theory_Data + ( + type T = ml_invariant Name_Space.table; + val empty : T = Name_Space.empty_table ml_invariantN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_opening_ml_invariants = Opening_ML_Invariants.get o Proof_Context.theory_of + + fun get_opening_ml_invariant_global cid thy = + Name_Space.check (Context.Theory thy) + (get_opening_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #2 + + fun get_opening_ml_invariant_name_global cid thy = + Name_Space.check (Context.Theory thy) + (get_opening_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #1 + + fun check_opening_ml_invariant ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_opening_ml_invariants ctxt); + + fun add_opening_ml_invariant name opening_ml_invariant thy = + thy |> Opening_ML_Invariants.map + (Name_Space.define (Context.Theory thy) true (name, opening_ml_invariant) #> #2); + + fun update_opening_ml_invariant name opening_ml_invariant thy = + thy |> Opening_ML_Invariants.map + (Name_Space.define (Context.Theory thy) false (name, opening_ml_invariant) #> #2); + + fun update_opening_ml_invariant_entry name new_opening_ml_invariant thy = + thy |> Opening_ML_Invariants.map + (Name_Space.map_table_entry name (fn _ => new_opening_ml_invariant)); + + fun print_opening_ml_invariants verbose ctxt = + Pretty.big_list "Isabelle.DOF Opening_ML_Invariants:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_opening_ml_invariants ctxt))) + |> Pretty.writeln; + + fun the_opening_ml_invariant T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown opening_ml_invariant: " ^ quote i, [], [])); + + structure Closing_ML_Invariants = Theory_Data + ( + type T = ml_invariant Name_Space.table; + val empty : T = Name_Space.empty_table ml_invariantN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_closing_ml_invariants = Closing_ML_Invariants.get o Proof_Context.theory_of + + fun get_closing_ml_invariant_global cid thy = + Name_Space.check (Context.Theory thy) + (get_closing_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #2 + + fun get_closing_ml_invariant_name_global cid thy = + Name_Space.check (Context.Theory thy) + (get_closing_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #1 + + fun check_closing_ml_invariant ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_closing_ml_invariants ctxt); + + fun add_closing_ml_invariant name closing_ml_invariant thy = + thy |> Closing_ML_Invariants.map + (Name_Space.define (Context.Theory thy) true (name, closing_ml_invariant) #> #2); + + fun update_closing_ml_invariant name closing_ml_invariant thy = + thy |> Closing_ML_Invariants.map + (Name_Space.define (Context.Theory thy) false (name, closing_ml_invariant) #> #2); + + fun update_closing_ml_invariant_entry name new_closing_ml_invariant thy = + thy |> Closing_ML_Invariants.map + (Name_Space.map_table_entry name (fn _ => new_closing_ml_invariant)); + + fun print_closing_ml_invariants verbose ctxt = + Pretty.big_list "Isabelle.DOF Closing_ML_Invariants:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_closing_ml_invariants ctxt))) + |> Pretty.writeln; + + fun the_closing_ml_invariant T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown closing_ml_invariant: " ^ quote i, [], [])); datatype monitor_info = Monitor_Info of @@ -349,29 +468,11 @@ struct (* registrating data of the Isa_DOF component *) structure Data = Generic_Data ( - type T = {docclass_tab : docclass_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 = {docclass_tab = initial_docclass_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( {docclass_tab = c1, - docclass_inv_tab = n1, - docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1}, - {docclass_tab = c2, - docclass_inv_tab = n2, - docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) = - {docclass_tab = merge_docclass_tab (c1,c2), - docclass_inv_tab = override(n1,n2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_eager_inv_tab = override(en1,en2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_lazy_inv_tab = override(ln1,ln2) - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - } + type T = {docclass_tab : docclass_tab} + val empty = {docclass_tab = initial_docclass_tab} + fun merge( {docclass_tab = c1}, + {docclass_tab = c2}) = + {docclass_tab = merge_docclass_tab (c1,c2) } ); @@ -381,36 +482,8 @@ val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; -fun upd_docclass_tab f {docclass_tab = y, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = f y, - 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 {docclass_tab, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = docclass_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 {docclass_tab, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = docclass_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 {docclass_tab, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = docclass_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; +fun upd_docclass_tab f {docclass_tab = y} = + {docclass_tab = f y}; fun get_accepted_cids (Monitor_Info {accepted_cids, ... }) = accepted_cids fun get_rejected_cids (Monitor_Info {rejected_cids, ... }) = rejected_cids @@ -497,57 +570,6 @@ fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) end -fun update_class_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt )))))) - thy - end - -fun update_class_eager_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_eager_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Eager Invariant check of: " ^cid_long); f ctxt )))))) - thy - end - -fun update_class_lazy_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_lazy_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Lazy Invariant check of: " ^cid_long); f ctxt )))))) - thy - end - -fun get_class_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -fun get_class_eager_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_eager_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_eager_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -fun get_class_lazy_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_lazy_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_lazy_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - val SPY = Unsynchronized.ref(Bound 0) fun check_regexps term = @@ -1646,15 +1668,20 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = val assns' = map conv_attrs trace_attr fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_object_global oid thy in #cid params end + val ctxt = Proof_Context.init_global thy fun def_trans_input_term oid = #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') fun def_trans_value oid = (#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')) - #> value (Proof_Context.init_global thy) + #> value ctxt val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." val _ = app (fn (n, _) => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; (* check that any transition is possible : *) - fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false} + fun inst_class_inv x = let val invs = DOF_core.get_ml_invariants ctxt + val check_option = Name_Space.lookup invs (cid_of x) + in case check_option of + NONE => (K true) + | SOME check => (check x {is_monitor=false}) end fun class_inv_checks ctxt = map (fn (x, _) => inst_class_inv x ctxt) enabled_monitors val delta_autoS = map is_enabled_for_cid enabled_monitors; fun update_info (n, aS, monitor_info) = @@ -1783,8 +1810,12 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi thy cid_long assns' defaults in (input_term, value_term') end else (\<^term>\()\, value_term') end - val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) - o Context.Theory + val check_inv = Context.Theory + #> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid is_monitor) end) in thy |> DOF_core.define_object_global {define = define} ((oid, pos), {defined = false, input_term = fst value_terms, value = value (Proof_Context.init_global thy) @@ -1795,9 +1826,13 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi vcid = vcid}) |> register_oid_cid_in_open_monitors oid pos cid_pos' |> (fn thy => if #is_monitor(is_monitor) - then (((DOF_core.get_class_eager_invariant cid_long thy oid) is_monitor - o Context.Theory) thy; thy) - else thy) + then ((Context.Theory + #> (let val invs = DOF_core.get_opening_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid is_monitor) end)) thy; thy) + else thy) |> (fn thy => (check_inv thy; thy)) (* Bypass checking of high-level invariants when the class default_cid = "text", the top (default) document class. @@ -1992,9 +2027,13 @@ fun update_instance_command (((oid, pos), cid_pos), #1 o (Value_Command.Docitem_Parser.calc_update_term {mk_elaboration=true} thy cid_long assns') #> Value_Command.value (Proof_Context.init_global thy) - fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} - o Context.Theory ) thy ; - thy) + fun check_inv thy = + ((Context.Theory + #> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid {is_monitor=false}) end) ) thy ; thy) in thy |> (if Config.get_global thy DOF_core.object_value_debug then DOF_core.update_value_input_term_global oid @@ -2062,11 +2101,21 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), val markup = DOF_core.get_object_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; - val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true} - o Context.Theory - val check_lazy_inv = (DOF_core.get_class_lazy_invariant cid_long thy oid) {is_monitor=true} - o Context.Theory - in thy |> (fn thy => (check_lazy_inv thy; thy)) + val check_inv = + Context.Theory + #> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid {is_monitor=true}) end) + val check_closing_inv = + Context.Theory + #> (let val invs = DOF_core.get_closing_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid {is_monitor=true}) end) + in thy |> (fn thy => (check_closing_inv thy; thy)) |> update_instance_command args |> (fn thy => (check_inv thy; thy)) |> (fn thy => if Config.get_global thy DOF_core.invariants_checking @@ -2737,7 +2786,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy = $ (update_attribute_type thy class_scheme_ty cid_long t') | update_attribute_type thy class_scheme_ty cid_long (Abs(s, ty, t)) = Abs(s, ty, update_attribute_type thy class_scheme_ty cid_long t) - | update_attribute_type _ class_scheme_ty _ (Free(s, ty)) = if s = invariantN + | update_attribute_type _ class_scheme_ty _ (Free(s, ty)) = if s = instance_placeholderN then Free (s, class_scheme_ty) else Free (s, ty) | update_attribute_type _ _ _ t = t @@ -2747,7 +2796,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy = current class. *) val inv_term' = update_attribute_type thy inv_ty cid_long inv_term val eq_inv_ty = inv_ty --> HOLogic.boolT - val abs_term = Term.lambda (Free (invariantN, inv_ty)) inv_term' + val abs_term = Term.lambda (Free (instance_placeholderN, inv_ty)) inv_term' in thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end fun add_doc_class_cmd overloaded (raw_params, binding) diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 14edeaf..80c50a1 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1030,7 +1030,14 @@ fun check_sil oid _ ctxt = in check_sil'' traces end \ -setup\DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil\ +setup\ +(fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end + in DOF_core.add_ml_invariant binding check_sil thy end) +\ text\ A more generic example of check_sil which can be generalized: @@ -1066,7 +1073,14 @@ fun check_sil_slow oid _ ctxt = in check_sil' traces end \ -(*setup\DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil_slow\*) +(*setup\ +(fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end + in DOF_core.add_ml_invariant binding check_sil_slow thy end) +\*) (* As traces of monitor instances (docitems) are updated each time an instance is declared (with text*, section*, etc.), invariants checking functions which check the full list of traces @@ -1096,7 +1110,14 @@ fun check_required_documents oid _ ctxt = in check_required_documents' accepted_cids end \ -setup\DOF_core.update_class_lazy_invariant "CENELEC_50128.monitor_SIL0" check_required_documents\ +setup\ +(fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end + in DOF_core.add_closing_ml_invariant binding check_required_documents thy end) +\ (* Test pattern matching for the records of the current CENELEC implementation classes, and used by checking functions. diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 05a034a..5a36452 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -489,15 +489,17 @@ end end \ - -setup\ let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical", +setup\ +(fn thy => +let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical", "scholarly_paper.example", "scholarly_paper.conclusion"]; - fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check - ctxt cidS moni_oid NONE; - true) - in DOF_core.update_class_invariant "scholarly_paper.article" body end\ - -ML\ \ + fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check ctxt cidS moni_oid NONE; true) + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "article" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding body thy end) +\ section\Miscelleous\ diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index fc7cc4f..5a1020f 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -64,7 +64,9 @@ doc_class result = technical + -ML\fun check_invariant_invariant oid {is_monitor:bool} ctxt = +ML\ +fn thy => +let fun check_invariant_invariant oid {is_monitor:bool} ctxt = let val kind_term = ISA_core.compute_attr_access ctxt "kind" oid NONE @{here} val property_termS = ISA_core.compute_attr_access ctxt "property" oid NONE @{here} val tS = HOLogic.dest_list property_termS @@ -73,9 +75,14 @@ ML\fun check_invariant_invariant oid {is_monitor:bool} ctxt = else error("class class invariant violation") | _ => false end + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "result" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding check_invariant_invariant thy end \ -setup\DOF_core.update_class_invariant "small_math.result" check_invariant_invariant\ +(*setup\DOF_core.add_ml_invariant "small_math.result" check_invariant_invariant\*) doc_class example = technical + @@ -164,10 +171,17 @@ end end \ -setup\ let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"]; +setup\ +fn thy => +let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"]; fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check ctxt cidS moni_oid NONE; true) - in DOF_core.update_class_invariant "small_math.article" body end\ + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "article" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding body thy end +\ end diff --git a/src/tests/Concept_Example_Low_Level_Invariant.thy b/src/tests/Concept_Example_Low_Level_Invariant.thy index de11e0a..910b52f 100644 --- a/src/tests/Concept_Example_Low_Level_Invariant.thy +++ b/src/tests/Concept_Example_Low_Level_Invariant.thy @@ -34,24 +34,35 @@ The implementor of an ontology must know what he does ... \ text\Setting a sample invariant, which simply produces some side-effect:\ -setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => - fn {is_monitor = b} => - fn ctxt => - (writeln ("sample echo : "^oid); true))\ +setup\ +fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "A" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding (fn oid => + fn {is_monitor = b} => + fn ctxt => + (writeln ("sample echo : "^oid); true)) thy end +\ subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ -ML\fun check_A_invariant oid {is_monitor:bool} ctxt = +ML\ +fn thy => +let fun check_A_invariant oid {is_monitor:bool} ctxt = let val term = ISA_core.compute_attr_access ctxt "x" oid NONE @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term - in if x_value > 5 then error("class A invariant violation") else true end + in if x_value > 5 then error("class A invariant violation") else true end + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "A" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding check_A_invariant thy end \ -setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ - - subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ @@ -79,7 +90,9 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\fun check_M_invariant oid {is_monitor} ctxt = +ML\ +fn thy => +let fun check_M_invariant oid {is_monitor} ctxt = let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = @@ -93,10 +106,13 @@ ML\fun check_M_invariant oid {is_monitor} ctxt = val n = length (filter is_C cid_list) val m = length (filter is_D cid_list) in if m > n then error("class M invariant violation") else true end + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "M" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding check_M_invariant thy end \ -setup\DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\ - section\Example: Monitor Class Invariant\ From 1e09598d81293f5ecd52a173121433bad68c04e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 14 Feb 2023 07:08:43 +0100 Subject: [PATCH 10/18] Fix typo --- src/tests/Cenelec_Test.thy | 92 +++++++++++++++++++------------------- 1 file changed, 46 insertions(+), 46 deletions(-) diff --git a/src/tests/Cenelec_Test.thy b/src/tests/Cenelec_Test.thy index 4b1473a..0b86419 100644 --- a/src/tests/Cenelec_Test.thy +++ b/src/tests/Cenelec_Test.thy @@ -13,52 +13,52 @@ print_doc_classes open_monitor*[SIL0Test::monitor_SIL0] -text*[sqap_intance::SQAP, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\\ -text*[sqavr_intance::SQAVR, sil= "SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[scmp_intance::SCMP, sil="SIL0", written_by="Some CM", fst_check="Some VER", snd_check="Some VAL"]\\ -text*[svp_intance::SVP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[svap_intance::SVAP, sil="SIL0", written_by="Some VAL", fst_check="Some VER", snd_check="None"]\\ -text*[swrs_intance::SWRS, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\\ -text*[oswts_intance::OSWTS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swrvr_intance::SWRVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swas_intance::SWAS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swds_intance::SWDS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swis_intance::SWIS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swits_intance::SWITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swhits_intance::SWHITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swadvr_intance::SWADVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swcds_intance::SWCDS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swcts_intance::SWCTS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swcdvr_intance::SWCDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swscd_intance::SWSCD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swctr_intance::SWCTR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swscvr_intance::SWSCVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[switr_intance::SWITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swhaitr_intance::SWHAITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swivr_intance::SWIVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[oswtr_intance::OSWTR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swvalr_intance::SWVALR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[tvalr_intance::TVALR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swvrn_intance::SWVRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[ars_intance::ARS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[app_intance::APP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[ats_intance::ATS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[aad_intance::AAD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[apvr_intance::APVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[atr_intance::ATR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[socoada_intance::SOCOADA, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[adavr_intance::ADAVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swrdp_intance::SWRDP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swdm_intance::SWDM, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swdrn_intance::SWDRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swdr_intance::SWDR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swdvr_intance::SWDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swmp_intance::SWMP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swcr_intance::SWCR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swmr_intance::SWMR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swmvr_intance::SWMVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swap_intance::SWAP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ -text*[swar_intance::SWAR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[sqap_instance::SQAP, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\\ +text*[sqavr_instance::SQAVR, sil= "SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[scmp_instance::SCMP, sil="SIL0", written_by="Some CM", fst_check="Some VER", snd_check="Some VAL"]\\ +text*[svp_instance::SVP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[svap_instance::SVAP, sil="SIL0", written_by="Some VAL", fst_check="Some VER", snd_check="None"]\\ +text*[swrs_instance::SWRS, sil="SIL0", written_by="Some RQM", fst_check="Some VER", snd_check="Some VAL"]\\ +text*[oswts_instance::OSWTS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swrvr_instance::SWRVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swas_instance::SWAS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swds_instance::SWDS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swis_instance::SWIS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swits_instance::SWITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swhits_instance::SWHITS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swadvr_instance::SWADVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcds_instance::SWCDS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcts_instance::SWCTS, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcdvr_instance::SWCDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swscd_instance::SWSCD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swctr_instance::SWCTR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swscvr_instance::SWSCVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[switr_instance::SWITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swhaitr_instance::SWHAITR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swivr_instance::SWIVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[oswtr_instance::OSWTR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swvalr_instance::SWVALR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[tvalr_instance::TVALR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swvrn_instance::SWVRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[ars_instance::ARS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[app_instance::APP, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[ats_instance::ATS, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[aad_instance::AAD, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[apvr_instance::APVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[atr_instance::ATR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[socoada_instance::SOCOADA, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[adavr_instance::ADAVR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swrdp_instance::SWRDP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdm_instance::SWDM, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdrn_instance::SWDRN, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdr_instance::SWDR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swdvr_instance::SWDVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swmp_instance::SWMP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swcr_instance::SWCR, sil="SIL0", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swmr_instance::SWMR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swmvr_instance::SWMVR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swap_instance::SWAP, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ +text*[swar_instance::SWAR, sil="SIL0", nlvl="R", written_by="Some VER", fst_check="None", snd_check="Some VAL"]\\ close_monitor*[SIL0Test] From 93509ab17dc4771918f48a4a0cbc45e89ce1bb6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 14 Feb 2023 07:09:27 +0100 Subject: [PATCH 11/18] Update file to match the new name space implementation --- src/tests/OutOfOrderPresntn.thy | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index 073090f..b21131c 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -30,9 +30,11 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ val docitem_tab = DOF_core.get_instances \<^context> -val {docclass_tab, ISA_transformer_tab, ...} +val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> +val {docclass_tab, ...} = DOF_core.get_data @{context}; Name_Space.dest_table docitem_tab; +Name_Space.dest_table isa_transformer_tab; Symtab.dest docclass_tab; app; \ From 55690bba33f5313e4f250438218a39baea517c1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 14 Feb 2023 07:39:06 +0100 Subject: [PATCH 12/18] Homogenize instance getters names --- src/DOF/Isa_DOF.thy | 82 +++++++++---------- .../CENELEC_50128/CENELEC_50128.thy | 16 ++-- 2 files changed, 49 insertions(+), 49 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 1939072..6e54f8a 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -219,6 +219,14 @@ struct val get_instances = Instances.get o Proof_Context.theory_of + fun get_instance_global oid thy = + Name_Space.check (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, Position.none) |> #2 + + fun get_instance_name_global oid thy = + Name_Space.check (Context.Theory thy) + (get_instances (Proof_Context.init_global thy)) (oid, Position.none) |> #1 + fun check_instance ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_instances ctxt); @@ -437,6 +445,14 @@ struct val get_monitor_infos = Monitor_Info.get o Proof_Context.theory_of + fun get_monitor_info_global oid thy = + Name_Space.check (Context.Theory thy) + (get_monitor_infos (Proof_Context.init_global thy)) (oid, Position.none) |> #2 + + fun get_monitor_info_name_global oid thy = + Name_Space.check (Context.Theory thy) + (get_monitor_infos (Proof_Context.init_global thy)) (oid, Position.none) |> #1 + fun check_monitor_info ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_monitor_infos ctxt); @@ -662,22 +678,6 @@ fun define_object_global {define = define} ((oid, pos), bbb) thy = else add_instance binding (Instance bbb) thy end -fun get_object_global oid thy = - Name_Space.check (Context.Theory thy) - (get_instances (Proof_Context.init_global thy)) (oid, Position.none) |> #2 - -fun get_object_name_global oid thy = - Name_Space.check (Context.Theory thy) - (get_instances (Proof_Context.init_global thy)) (oid, Position.none) |> #1 - -fun get_monitor_info_global oid thy = - Name_Space.check (Context.Theory thy) - (get_monitor_infos (Proof_Context.init_global thy)) (oid, Position.none) |> #2 - -fun get_monitor_info_name_global oid thy = - Name_Space.check (Context.Theory thy) - (get_monitor_infos (Proof_Context.init_global thy)) (oid, Position.none) |> #1 - fun get_doc_class_global cid thy = if cid = default_cid then error("default class access") (* TODO *) else let val t = #docclass_tab(get_data_global thy) @@ -745,11 +745,11 @@ fun get_attribute_defaults (* long*)cid thy = |trans (na,ty,SOME def) =SOME(na,ty, def) in map_filter trans attrS end -fun get_value_global oid thy = let val Instance v = get_object_global oid thy +fun get_value_global oid thy = let val Instance v = get_instance_global oid thy in v |> #value end fun get_value_local oid ctxt = - let val Instance v = get_object_global oid (Proof_Context.theory_of ctxt) + let val Instance v = get_instance_global oid (Proof_Context.theory_of ctxt) in v |> #value end (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) @@ -758,7 +758,7 @@ fun binding_from_instance_pos name thy = let val ns = get_instances (Proof_Context.init_global thy) |> Name_Space.space_of_table - val {pos, ...} = Name_Space.the_entry ns (get_object_name_global name thy) + val {pos, ...} = Name_Space.the_entry ns (get_instance_name_global name thy) in if Long_Name.is_qualified name then Binding.make (Long_Name.base_name name, pos) else Binding.make (name, pos)end @@ -766,14 +766,14 @@ fun binding_from_instance_pos name thy = fun update_value_global name upd_value thy = let val binding = binding_from_instance_pos name thy - val Instance {defined, input_term, value, inline, id, cid, vcid} = get_object_global name thy + val Instance {defined, input_term, value, inline, id, cid, vcid} = get_instance_global name thy val instance' = make_instance (defined, input_term, upd_value value, inline, id, cid, vcid) in update_instance binding (instance') thy end fun update_input_term_global name upd_input_term thy = let val binding = binding_from_instance_pos name thy - val Instance {defined, input_term, value, inline, id, cid, vcid} = get_object_global name thy + val Instance {defined, input_term, value, inline, id, cid, vcid} = get_instance_global name thy val instance' = make_instance (defined, upd_input_term input_term, value, inline, id, cid, vcid) in update_instance binding (instance') thy end @@ -1085,7 +1085,7 @@ fun check_instance thy (term, _, pos) s = Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE)); fun check thy (name, _) = let - val object_cid = let val DOF_core.Instance cid = DOF_core.get_object_global name thy + val object_cid = let val DOF_core.Instance cid = DOF_core.get_instance_global name thy in cid |> #cid end fun check' (class_name, object_cid) = if class_name = object_cid then @@ -1100,7 +1100,7 @@ fun ML_isa_id thy (term,pos) = SOME term fun ML_isa_check_docitem thy (term, req_ty, pos) _ = let fun check thy (name, _) s = let val DOF_core.Instance {cid,...} = - DOF_core.get_object_global name thy + DOF_core.get_instance_global name thy val ns = DOF_core.get_instances (Proof_Context.init_global thy) |> Name_Space.space_of_table val {pos=pos', ...} = Name_Space.the_entry ns name @@ -1121,7 +1121,7 @@ fun ML_isa_check_trace_attribute thy (term, _, pos) s = val oid = (HOLogic.dest_string term handle TERM(_,[t]) => error ("wrong term format: must be string constant: " ^ Syntax.string_of_term_global thy t )) - val _ = DOF_core.get_object_global oid thy + val _ = DOF_core.get_instance_global oid thy in SOME term end @@ -1208,9 +1208,9 @@ fun compute_attr_access ctxt attr oid pos_option pos' = (* template *) val ctxt' = Context.proof_of ctxt val thy = Context.theory_of ctxt val DOF_core.Instance {cid,...} = - DOF_core.get_object_global oid thy + DOF_core.get_instance_global oid thy val instances = DOF_core.get_instances ctxt' - val markup = DOF_core.get_object_name_global oid thy + val markup = DOF_core.get_instance_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt' pos' markup; val (* (long_cid, attr_b,ty) = *) @@ -1666,7 +1666,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = Syntax.read_term_global thy rhs) val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] val assns' = map conv_attrs trace_attr - fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_object_global oid thy + fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_instance_global oid thy in #cid params end val ctxt = Proof_Context.init_global thy fun def_trans_input_term oid = @@ -1705,7 +1705,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = fun check_invariants thy (oid, pos) = let val docitem_value = DOF_core.get_value_global oid thy - val DOF_core.Instance params = DOF_core.get_object_global oid thy + val DOF_core.Instance params = DOF_core.get_instance_global oid thy val cid = #cid params fun get_all_invariants cid thy = case DOF_core.get_doc_class_global cid thy of @@ -2003,10 +2003,10 @@ fun update_instance_command (((oid, pos), cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) thy : theory = let val cid = let val DOF_core.Instance {cid,...} = - DOF_core.get_object_global oid thy + DOF_core.get_instance_global oid thy val ctxt = Proof_Context.init_global thy val instances = DOF_core.get_instances ctxt - val markup = DOF_core.get_object_name_global oid thy + val markup = DOF_core.get_instance_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; in cid end @@ -2095,10 +2095,10 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), in check_if_final automatas end val oid' = DOF_core.get_monitor_info_name_global oid thy val delete_monitor_entry = DOF_core.Monitor_Info.map (Name_Space.del_table oid') - val DOF_core.Instance {cid=cid_long,...} = DOF_core.get_object_global oid thy + val DOF_core.Instance {cid=cid_long,...} = DOF_core.get_instance_global oid thy val ctxt = Proof_Context.init_global thy val instances = DOF_core.get_instances ctxt - val markup = DOF_core.get_object_name_global oid thy + val markup = DOF_core.get_instance_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; val check_inv = @@ -2132,7 +2132,7 @@ fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Pa (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) val cid_long = case cid_opt of NONE => let val DOF_core.Instance cid = - DOF_core.get_object_global lab thy + DOF_core.get_instance_global lab thy in cid |> #cid end | SOME(cid,_) => DOF_core.parse_cid_global thy cid @@ -2408,7 +2408,7 @@ fun meta_args_2_string thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_P (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) val cid_long = case cid_opt of NONE => let val DOF_core.Instance cid = - DOF_core.get_object_global lab thy + DOF_core.get_instance_global lab thy in cid |> #cid end | SOME(cid,_) => DOF_core.parse_cid_global thy cid (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) @@ -2482,12 +2482,12 @@ val basic_entity = Document_Output.antiquotation_pretty_source fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = let val thy = Proof_Context.theory_of ctxt; - val DOF_core.Instance {cid,inline,...} = DOF_core.get_object_global name thy + val DOF_core.Instance {cid,inline,...} = DOF_core.get_instance_global name thy val _ = if not inline_req then if inline then () else error("referred text-element is macro! (try option display)") else if not inline then () else error("referred text-element is no macro!") val instances = DOF_core.get_instances ctxt - val name' = DOF_core.get_object_name_global name thy + val name' = DOF_core.get_instance_name_global name thy val markup = name' |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; val ns = instances |> Name_Space.space_of_table @@ -2545,11 +2545,11 @@ fun check_and_mark_term ctxt oid = val thy = Context.theory_of ctxt; val ctxt' = Context.proof_of ctxt val DOF_core.Instance {cid,value,...} = - DOF_core.get_object_global oid thy + DOF_core.get_instance_global oid thy val instances = DOF_core.get_instances ctxt' val ns = instances |> Name_Space.space_of_table val {pos, ...} = Name_Space.the_entry ns oid - val markup = DOF_core.get_object_name_global oid thy + val markup = DOF_core.get_instance_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt' pos markup; (* this sends a report for a ref application to the PIDE interface ... *) @@ -2615,7 +2615,7 @@ fun get_instance_value_2_ML ctxt (oid:string,pos) = let val ctxt' = Context.the_proof ctxt val value = DOF_core.get_value_local oid ctxt' val instances = DOF_core.get_instances ctxt' - val markup = DOF_core.get_object_name_global oid (Proof_Context.theory_of ctxt') + val markup = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt') |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt' pos markup; in ML_Syntax.print_term value end @@ -2623,7 +2623,7 @@ fun get_instance_value_2_ML ctxt (oid:string,pos) = fun get_instance_name_2_ML ctxt (oid:string,pos) = let val ctxt' = Context.the_proof ctxt val instances = DOF_core.get_instances ctxt' - val markup = DOF_core.get_object_name_global oid (Proof_Context.theory_of ctxt') + val markup = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt') |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt' pos markup; in "\"" ^ oid ^ "\"" end @@ -2639,7 +2639,7 @@ fun compute_cid_repr ctxt cid pos = fun compute_name_repr ctxt oid pos = let val instances = DOF_core.get_instances ctxt - val markup = DOF_core.get_object_name_global oid (Proof_Context.theory_of ctxt) + val markup = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt) |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; in HOLogic.mk_string oid end diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 80c50a1..2c39493 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1010,7 +1010,7 @@ fun check_sil oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global oid (Context.theory_of ctxt) + DOF_core.get_instance_global oid (Context.theory_of ctxt) val Const _ $ _ $ monitor_sil $ _ = monitor_record_value val traces = AttributeAccess.compute_trace_ML ctxt oid NONE \<^here> fun check_sil'' [] = true @@ -1018,7 +1018,7 @@ fun check_sil oid _ ctxt = let val (_, doc_oid) = x val DOF_core.Instance {value = doc_record_value, ...} = - DOF_core.get_object_global doc_oid (Context.theory_of ctxt) + DOF_core.get_instance_global doc_oid (Context.theory_of ctxt) val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext in @@ -1048,9 +1048,9 @@ fun check_sil_slow oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global oid (Context.theory_of ctxt) + DOF_core.get_instance_global oid (Context.theory_of ctxt) val DOF_core.Instance {cid = monitor_cid, ...} = - DOF_core.get_object_global oid (Context.theory_of ctxt) + DOF_core.get_instance_global oid (Context.theory_of ctxt) val monitor_sil_typ = (Syntax.read_typ ctxt' monitor_cid) --> @{typ "sil"} val monitor_sil = Value_Command.value ctxt' (Const("CENELEC_50128.monitor_SIL.sil", monitor_sil_typ) $ monitor_record_value) @@ -1060,7 +1060,7 @@ fun check_sil_slow oid _ ctxt = let val (doc_cid, doc_oid) = x val DOF_core.Instance {value = doc_record_value, ...} = - DOF_core.get_object_global doc_oid (Context.theory_of ctxt) + DOF_core.get_instance_global doc_oid (Context.theory_of ctxt) val doc_sil_typ = (Syntax.read_typ ctxt' doc_cid) --> @{typ "sil"} val doc_sil = Value_Command.value ctxt' (Const ("CENELEC_50128.cenelec_document.sil", doc_sil_typ) $ doc_record_value) @@ -1102,7 +1102,7 @@ fun check_required_documents oid _ ctxt = let val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global oid (Context.theory_of ctxt) + DOF_core.get_instance_global oid (Context.theory_of ctxt) val Const _ $ _ $ monitor_sil $ _ = monitor_record_value in error ("A " ^ cid ^ " cenelec document is required with " ^ Syntax.string_of_term ctxt' monitor_sil) @@ -1129,10 +1129,10 @@ text*[CenelecClassPatternMatchingTest::SQAP, sil = "SIL0"]\\ ML\ val thy = @{theory} val DOF_core.Instance {value = monitor_record_value, ...} = - DOF_core.get_object_global "MonitorPatternMatchingTest" thy + DOF_core.get_instance_global "MonitorPatternMatchingTest" thy val Const _ $ _ $ monitor_sil $ _ = monitor_record_value val DOF_core.Instance {value = doc_record_value, ...} = - DOF_core.get_object_global "CenelecClassPatternMatchingTest" thy + DOF_core.get_instance_global "CenelecClassPatternMatchingTest" thy val Const _ $ _ $ _ $ _ $ _ $ cenelec_document_ext = doc_record_value val Const _ $ _ $ _ $ doc_sil $ _ $ _ $ _ $ _ $ _ $ _ = cenelec_document_ext \ From 234ff18ec00faff317c9cb13629830e6be12dae5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 14 Feb 2023 17:57:53 +0100 Subject: [PATCH 13/18] Use a name space for Onto Classes - Use a name space table to store ontological class objects - Remove docclass_tab table and accesses --- .../Isabelle_DOF-Manual/04_RefMan.thy | 3 +- .../Isabelle_DOF-Manual/05_Implementation.thy | 56 +-- src/DOF/Isa_COL.thy | 9 +- src/DOF/Isa_DOF.thy | 406 ++++++++---------- .../CENELEC_50128/CENELEC_50128.thy | 34 +- .../scholarly_paper/scholarly_paper.thy | 4 +- src/ontologies/small_math/small_math.thy | 9 +- src/tests/Attributes.thy | 9 +- .../Concept_Example_Low_Level_Invariant.thy | 19 +- src/tests/OutOfOrderPresntn.thy | 10 +- src/tests/TermAntiquotations.thy | 2 +- 11 files changed, 241 insertions(+), 320 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 26819e7..42997d7 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -350,8 +350,7 @@ is currently only available in the SML API's of the kernel. | macro_command \ \<^item> \<^isadof> \change_status_command\ : - \<^rail>\ (@@{command "update_instance*"} '[' upd_meta_args ']') - | (@@{command "declare_reference*"} (obj_id ('::' class_id)))\ + \<^rail>\ (@@{command "update_instance*"} '[' upd_meta_args ']')\ \<^item> \<^isadof> \inspection_command\ : \<^rail>\ @@{command "print_doc_classes"} | @@{command "print_doc_items"} diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy index 3f8a603..049ed1e 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy @@ -46,40 +46,42 @@ text\ A plugin in Isabelle starts with defining the local data and registering it in the framework. As mentioned before, contexts are structures with independent cells/compartments having three primitives \<^boxed_sml>\init\, \<^boxed_sml>\extend\ and \<^boxed_sml>\merge\. Technically this is done by - instantiating a functor \<^boxed_sml>\Generic_Data\, and the following fairly typical code-fragment + instantiating a functor \<^boxed_sml>\Theory_Data\, and the following fairly typical code-fragment is drawn from \<^isadof>: @{boxed_sml [display] -\structure Data = Generic_Data -( type T = docobj_tab * docclass_tab * ... - val empty = (initial_docobj_tab, initial_docclass_tab, ...) - fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...), - merge_docclass_tab(c1,c2,...)) -);\} - where the table \<^boxed_sml>\docobj_tab\ manages document class instances - and \<^boxed_sml>\docclass_tab\ the environment for class definitions - (inducing the inheritance relation). Other tables capture, \eg, - the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where +\structure Onto_Classes = Theory_Data + ( + type T = onto_class Name_Space.table; + val empty : T = Name_Space.empty_table onto_classN; + fun merge data : T = Name_Space.merge_tables data; + );\} + where the table \<^boxed_sml>\Name_Space.table\ manages + the environment for class definitions (\<^boxed_sml>\onto_class\), inducing the inheritance relation, + using a \<^boxed_sml>\Name_Space\ table. Other tables capture, \eg, + the class instances, class invariants, inner-syntax antiquotations. + Operations follow the MVC-pattern, where Isabelle/Isar provides the controller part. A typical model operation has the type: @{boxed_sml [display] -\val opn :: -> Context.generic -> Context.generic\} - representing a transformation on system contexts. For example, the operation of declaring a local - reference in the context is presented as follows: +\val opn :: -> theory -> theory\} + representing a transformation on system contexts. For example, the operation of defining a class + in the context is presented as follows: @{boxed_sml [display] -\fun declare_object_local oid ctxt = -let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, - maxano=maxano} -in (Data.map(apfst decl)(ctxt) - handle Symtab.DUP _ => - error("multiple declaration of document reference")) -end\} - where \<^boxed_sml>\Data.map\ is the update function resulting from the instantiation of the - functor \<^boxed_sml>\Generic_Data\. This code fragment uses operations from a library structure - \<^boxed_sml>\Symtab\ that were used to update the appropriate table for document objects in - the plugin-local state. Possible exceptions to the update operation were mapped to a system-global - error reporting function. +\fun add_onto_class name onto_class thy = + thy |> Onto_Classes.map + (Name_Space.define (Context.Theory thy) true (name, onto_class) #> #2); +\} + This code fragment uses operations from the library structure \<^boxed_sml>\Name_Space\ + that were used to update the appropriate table for document objects in + the plugin-local state. + A name space manages a collection of long names, together with a mapping + between partially qualified external names and fully qualified internal names + (in both directions). + It can also keep track of the declarations and updates position of objects, + and then allows a simple markup-generation. + Possible exceptions to the update operation are automatically triggered. Finally, the view-aspects were handled by an API for parsing-combinators. The library structure \<^boxed_sml>\Scan\ provides the operators: @@ -120,7 +122,7 @@ val attributes =(Parse.$$$ "[" |-- (reference new \emph{command}: @{boxed_theory_text [display]\ -declare_reference [lal::requirement, alpha="main", beta=42] +declare_reference* [lal::requirement, alpha="main", beta=42] \} The construction also generates implicitly some markup information; for example, when hovering diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index e649ec3..3c75163 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -30,7 +30,7 @@ theory Isa_COL "figure*" "side_by_side_figure*" :: document_body begin - + section\Basic Text and Text-Structuring Elements\ text\ The attribute @{term "level"} in the subsequent enables doc-notation support section* etc. @@ -92,8 +92,8 @@ local fun transform_cid thy NONE X = X |transform_cid thy (SOME ncid) NONE = (SOME(ncid,@{here})) |transform_cid thy (SOME cid) (SOME (sub_cid,pos)) = - let val cid_long = DOF_core.read_cid_global thy cid - val sub_cid_long = DOF_core.read_cid_global thy sub_cid + let val cid_long = DOF_core.get_onto_class_name_global' cid thy + val sub_cid_long = DOF_core.get_onto_class_name_global' sub_cid thy in if DOF_core.is_subclass_global thy sub_cid_long cid_long then (SOME (sub_cid,pos)) else (* (SOME (sub_cid,pos)) *) @@ -146,7 +146,8 @@ datatype placement = pl_h | (*here*) pl_ht | (*here -> top*) pl_hb (*here -> bottom*) -ML\(Symtab.defined (#docclass_tab(DOF_core.get_data_global @{theory}))) "side_by_side_figure"\ +ML\ "side_by_side_figure" |> Name_Space.declared (DOF_core.get_onto_classes \<^context> + |> Name_Space.space_of_table)\ print_doc_classes diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 6e54f8a..01faac9 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -61,6 +61,7 @@ ML\ val docrefN = "docref"; val docclassN = "doc_class"; +val onto_classN = "onto_class"; (** name components **) @@ -146,23 +147,84 @@ ML\ structure DOF_core = struct - type virtual = {virtual : bool} - type docclass_struct = {params : (string * sort) list, (*currently not used *) - name : binding, - virtual : virtual, - thy_name : string, id : serial, (* for pide *) - inherits_from : (typ list * string) option, (* imports *) - attribute_decl : (binding*typ*term option)list, (* class local *) - rejectS : term list, - rex : term list, - invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) + datatype onto_class = Onto_Class of + {params : (string * sort) list, (*currently not used *) + name : binding, + virtual : {virtual : bool}, + thy_name : string, id : serial, (* for pide *) + inherits_from : (typ list * string) option, (* imports *) + attribute_decl : (binding*typ*term option)list, (* class local *) + rejectS : term list, + rex : term list, + invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) - type docclass_tab = docclass_struct Symtab.table + fun make_onto_class (params, name, virtual, thy_name, id, inherits_from, attribute_decl + , rejectS, rex, invs) = + Onto_Class {params = params, name = name, virtual = virtual, thy_name = thy_name, id = id + , inherits_from = inherits_from, attribute_decl = attribute_decl, rejectS = rejectS + , rex = rex, invs = invs} - val initial_docclass_tab = Symtab.empty:docclass_tab + structure Onto_Classes = Theory_Data + ( + type T = onto_class Name_Space.table; + val empty : T = Name_Space.empty_table onto_classN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_onto_classes = Onto_Classes.get o Proof_Context.theory_of + + fun get_onto_class_global name thy = + Name_Space.check (Context.Theory thy) + (get_onto_classes (Proof_Context.init_global thy)) (name, Position.none) |> #2 + + (* takes class synonyms into account *) + fun get_onto_class_global' name thy = + let val name' = name |> Syntax.read_typ_global thy + |> Syntax.string_of_typ_global thy + |> YXML.parse_body |> XML.content_of + in Name_Space.check (Context.Theory thy) + (get_onto_classes (Proof_Context.init_global thy)) (name', Position.none) |> #2 + end + + fun get_onto_class_name_global name thy = + Name_Space.check (Context.Theory thy) + (get_onto_classes (Proof_Context.init_global thy)) (name, Position.none) |> #1 + + (* takes class synonyms into account *) + fun get_onto_class_name_global' name thy = + let val name' = name |> Syntax.read_typ_global thy + |> Syntax.string_of_typ_global thy + |> YXML.parse_body |> XML.content_of + in Name_Space.check (Context.Theory thy) + (get_onto_classes (Proof_Context.init_global thy)) (name', Position.none) |> #1 + end + + fun check_onto_class ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_onto_classes ctxt); + + fun add_onto_class name onto_class thy = + thy |> Onto_Classes.map + (Name_Space.define (Context.Theory thy) true (name, onto_class) #> #2); + + fun update_onto_class name onto_class thy = + thy |> Onto_Classes.map + (Name_Space.define (Context.Theory thy) false (name, onto_class) #> #2); + + fun update_onto_class_entry name new_onto_class thy = + thy |> Onto_Classes.map + (Name_Space.map_table_entry name (fn _ => new_onto_class)); + + fun print_onto_classes verbose ctxt = + Pretty.big_list "Isabelle.DOF Onto_Classes:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_onto_classes ctxt))) + |> Pretty.writeln; + + fun the_onto_class T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown onto_class: " ^ quote i, [], [])); - fun merge_docclass_tab (otab,otab') = Symtab.merge (op =) (otab,otab') val tag_attr = (\<^binding>\tag_attribute\, \<^Type>\int\, Mixfix.NoSyn) (* Attribute hidden to the user and used internally by isabelle_DOF. @@ -172,21 +234,22 @@ struct val default_cid = "text" (* the top (default) document class: everything is a text.*) - fun is_subclass0 (tab:docclass_tab) s t = - let val _ = case Symtab.lookup tab t of - NONE => if t <> default_cid - then error ("document superclass not defined: "^t) - else default_cid - | SOME _ => "" - fun father_is_sub s = case Symtab.lookup tab s of - NONE => error ("document subclass not defined: "^s) - | SOME ({inherits_from=NONE, ...}) => s = t - | SOME ({inherits_from=SOME (_,s'), ...}) => - s' = t orelse father_is_sub s' - in s = t orelse - (t = default_cid andalso Symtab.defined tab s ) orelse - (s <> default_cid andalso father_is_sub s) - end + fun is_subclass0 s t ctxt = + let fun get id = if id = default_cid + then default_cid + else check_onto_class ctxt (id, Position.none) + val s' = get s + val t' = get t + fun father_is_sub s = case get_onto_class_global s (Proof_Context.theory_of ctxt) of + (Onto_Class {inherits_from=NONE, ...}) => s' = t' + | (Onto_Class {inherits_from=SOME (_,s''), ...}) => + s'' = t' orelse father_is_sub s'' + val s'_defined = s' |> Name_Space.declared (get_onto_classes ctxt + |> Name_Space.space_of_table) + in s' = t' orelse + (t' = default_cid andalso s'_defined) orelse + (s' <> default_cid andalso father_is_sub s') + end datatype instance = Instance of @@ -479,28 +542,6 @@ struct | NONE => raise TYPE ("Unknown monitor_info: " ^ quote i, [], [])); - fun override(t1,t2) = fold(Symtab.update)(Symtab.dest t2)(t1) - -(* registrating data of the Isa_DOF component *) -structure Data = Generic_Data -( - type T = {docclass_tab : docclass_tab} - val empty = {docclass_tab = initial_docclass_tab} - fun merge( {docclass_tab = c1}, - {docclass_tab = c2}) = - {docclass_tab = merge_docclass_tab (c1,c2) } -); - - -val get_data = Data.get o Context.Proof; -val map_data = Data.map; -val get_data_global = Data.get o Context.Theory; -val map_data_global = Context.theory_map o map_data; - - -fun upd_docclass_tab f {docclass_tab = y} = - {docclass_tab = f y}; - fun get_accepted_cids (Monitor_Info {accepted_cids, ... }) = accepted_cids fun get_rejected_cids (Monitor_Info {rejected_cids, ... }) = rejected_cids fun get_alphabet monitor_info = (get_accepted_cids monitor_info) @ (get_rejected_cids monitor_info) @@ -518,8 +559,9 @@ fun get_automatas (Monitor_Info {automatas, ... }) = automatas However, we use Syntax.read_typ in order to allow type-synonyms which requires an appropriate adaption in read_cid.*) -fun is_subclass (ctxt) s t = is_subclass0(#docclass_tab(get_data ctxt)) s t -fun is_subclass_global thy s t = is_subclass0(#docclass_tab(get_data_global thy)) s t +fun is_subclass (ctxt) s t = is_subclass0 s t ctxt +fun is_subclass_global thy s t = let val ctxt = Proof_Context.init_global thy + in is_subclass0 s t ctxt end fun typ_to_cid (Type(s,[\<^Type>\unit\])) = Long_Name.qualifier s @@ -527,63 +569,13 @@ fun typ_to_cid (Type(s,[\<^Type>\unit\])) = Long_Name.qualifier s |typ_to_cid _ = error("type is not an ontological type.") -fun parse_cid ctxt cid = -(* parses a type lexically/syntactically, checks absence of type vars *) - (case Syntax.parse_typ ctxt cid of - Type(tyname, []) => tyname - | _ => error "illegal type-format for doc-class-name.") - handle ERROR _ => "" (* ignore error *) +fun get_onto_class_name_super_class_global _ "text" = default_cid + | get_onto_class_name_super_class_global thy cid = get_onto_class_name_global' cid thy -fun read_cid ctxt "text" = default_cid (* text = default_cid *) - | read_cid ctxt cid = -(* parses a type syntactically, type-identification, checking as class id *) - (case Syntax.read_typ ctxt cid of - ty as Type(tyname, _) => let val res = typ_to_cid ty - val t = #docclass_tab(get_data ctxt) - in if Symtab.defined t res - then res - else error("type identifier not a class id:"^res) - end - | _ => error "illegal type-format for doc-class-name.") - handle ERROR _ => error("type identifier not a class id:"^cid) - -fun parse_cid_global thy cid = parse_cid (Proof_Context.init_global thy) cid -fun read_cid_global thy cid = read_cid (Proof_Context.init_global thy) cid - - -fun is_defined_cid_global cid thy = -(* works with short and long names *) - let val t = #docclass_tab(get_data_global thy) - in cid=default_cid orelse - Symtab.defined t (parse_cid_global thy cid) - end - -fun is_defined_cid_global' cid_long thy = -(* works with long names only *) - let val t = #docclass_tab(get_data_global thy) - in cid_long=default_cid orelse Symtab.defined t cid_long end - - -fun is_defined_cid_local cid ctxt = -(* works with short and long names *) - let val t = #docclass_tab(get_data ctxt) - in cid=default_cid orelse - Symtab.defined t (parse_cid ctxt cid) - end - -fun is_defined_cid_local' cid_long ctxt = -(* works with long names only *) - let val t = #docclass_tab(get_data ctxt) - in cid_long=default_cid orelse Symtab.defined t cid_long end - -fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) - (* takes class synonyms into account *) - val long_name = read_cid_global thy cid - in case Symtab.lookup tab long_name of - NONE => error("Undefined class id: " ^ cid) - | SOME ({virtual=virtual, ...}) => #virtual virtual - end +fun is_virtual cid thy = + let val Onto_Class {virtual, ...} = get_onto_class_global' cid thy + in virtual |> #virtual end val SPY = Unsynchronized.ref(Bound 0) @@ -598,7 +590,7 @@ fun check_regexps term = (* Missing: Checks on constants such as undefined, ... *) in term end -fun check_reject_atom cid_long term = +fun check_reject_atom term = let val _ = case fold_aterms Term.add_free_names term [] of n::_ => error("No free variables allowed in monitor regexp:" ^ n) | _ => () @@ -616,23 +608,15 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i the space where it is ... *) val cid = (Binding.name_of binding) val pos = (Binding.pos_of binding) - - val _ = if is_defined_cid_global cid thy + (*val _ = if is_defined_cid_global cid thy then error("redefinition of document class:"^cid ) - else () - val parent' = map_option (map_snd (read_cid_global thy)) parent - (* weird construction. Necessary since parse produces at rare cases - string representations that do no longer have the lexis of a type name. *) - val cid_long = parse_cid_global thy cid - val cid_long' = parse_cid_global thy cid_long - val _ = if cid_long' <> "" then () - else error("Could not construct type from doc_class (lexical problem?)") - + else ()*) + (* takes class synonyms into account *) + val parent' = map_option (map_snd (fn x => get_onto_class_name_global' x thy)) parent val id = serial (); val _ = Position.report pos (docclass_markup true cid id pos); - val rejectS = map (Syntax.read_term_global thy) reject_Atoms; - val _ = map (check_reject_atom cid_long) rejectS; + val _ = map (check_reject_atom) rejectS; val reg_exps = map (Syntax.read_term_global thy) rexp; val _ = map check_regexps reg_exps val _ = if not(null rejectS) andalso (null reg_exps) @@ -641,20 +625,8 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs)))) else () val invs' = map (map_snd(Syntax.read_term_global thy)) invs - val info = {params=params', - name = binding, - virtual = virtual, - thy_name = nn, - id = id, (* for pide --- really fresh or better reconstruct - from prior record definition ? For the moment: own - generation of serials ... *) - inherits_from = parent', - attribute_decl = fields , - rejectS = rejectS, - rex = reg_exps, - invs = invs'} - - in map_data_global(upd_docclass_tab(Symtab.update(cid_long,info)))(thy) + in thy |> add_onto_class binding (make_onto_class (params', binding, virtual, nn, id, parent' + , fields, rejectS, reg_exps, invs')) end fun define_object_global {define = define} ((oid, pos), bbb) thy = @@ -678,33 +650,16 @@ fun define_object_global {define = define} ((oid, pos), bbb) thy = else add_instance binding (Instance bbb) thy end -fun get_doc_class_global cid thy = - if cid = default_cid then error("default class access") (* TODO *) - else let val t = #docclass_tab(get_data_global thy) - in (Symtab.lookup t cid) end - - -fun get_doc_class_local cid ctxt = - if cid = default_cid then error("default class access") (* TODO *) - else let val t = #docclass_tab(get_data ctxt) - in (Symtab.lookup t cid) end - - -fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) - in cid=default_cid orelse - Symtab.defined t (parse_cid ctxt cid) - end fun get_attributes_local cid ctxt = if cid = default_cid then [] - else let val t = #docclass_tab(get_data ctxt) - val cid_long = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) - in case Symtab.lookup t cid_long of - NONE => error("undefined class id for attributes: "^cid) - | (SOME ({inherits_from=NONE, - attribute_decl = X, ...})) => [(cid_long,X)] - | (SOME ({inherits_from=SOME(_,father), - attribute_decl = X, ...})) => + else let val cid_long = get_onto_class_name_global cid (Proof_Context.theory_of ctxt) + in + case get_onto_class_global cid (Proof_Context.theory_of ctxt) of + Onto_Class {inherits_from=NONE, + attribute_decl = X, ...} => [(cid_long,X)] + | Onto_Class {inherits_from=SOME(_,father), + attribute_decl = X, ...} => get_attributes_local father ctxt @ [(cid_long,X)] end @@ -754,15 +709,21 @@ fun get_value_local oid ctxt = (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) -fun binding_from_instance_pos name thy = +fun binding_from_pos get_objects get_objects_name name thy = let - val ns = get_instances (Proof_Context.init_global thy) + val ns = get_objects (Proof_Context.init_global thy) |> Name_Space.space_of_table - val {pos, ...} = Name_Space.the_entry ns (get_instance_name_global name thy) + val {pos, ...} = Name_Space.the_entry ns (get_objects_name name thy) in if Long_Name.is_qualified name then Binding.make (Long_Name.base_name name, pos) else Binding.make (name, pos)end +fun binding_from_onto_class_pos name thy = + binding_from_pos get_onto_classes get_onto_class_name_global name thy + +fun binding_from_instance_pos name thy = + binding_from_pos get_instances get_instance_name_global name thy + fun update_value_global name upd_value thy = let val binding = binding_from_instance_pos name thy @@ -792,17 +753,6 @@ fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_p 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 transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy = (* pre: term should be fully typed in order to allow type-related term-transformations *) @@ -845,23 +795,19 @@ fun check_term ctxt term = transduce_term_global {mk_elaboration=false} (term , Position.none) (Proof_Context.theory_of ctxt) -fun writeln_classrefs ctxt = let val tab = #docclass_tab(get_data ctxt) - in writeln (String.concatWith "," (Symtab.keys tab)) end - - - fun print_doc_class_tree ctxt P T = - 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) = "" - |tree lev ((n,R)::S) = (if P(lev,n) + let val classes = Name_Space.dest_table (get_onto_classes ctxt) + fun is_class_son X (_, onto_class) = + let val Onto_Class inherits_from = onto_class + in (inherits_from |> #inherits_from) = X end + fun tree _ [] = "" + |tree lev ((n,_)::S) = (if P(lev,n) then "."^Int.toString lev^" "^(T n)^"{...}.\n" - ^ (tree(lev + 1)(filter(is_class_son(SOME([],n)))class_tab)) + ^ (tree(lev + 1)(filter(is_class_son(SOME([],n))) classes)) else "."^Int.toString lev^" ... \n") ^ (tree lev S) - val roots = filter(is_class_son NONE) class_tab + val roots = filter(is_class_son NONE) classes in ".0 .\n" ^ tree 1 roots end val (object_value_debug, object_value_debug_setup) @@ -1169,7 +1115,7 @@ fun elaborate_instances_list thy isa_name _ _ pos = 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 long_class_name = DOF_core.read_cid_global thy base_name' + val long_class_name = DOF_core.get_onto_class_name_global base_name' thy val values = thy |> Proof_Context.init_global |> DOF_core.get_instances |> Name_Space.dest_table |> filter (fn (_, instance) => @@ -1231,7 +1177,7 @@ fun compute_attr_access ctxt attr oid pos_option pos' = (* template *) | SOME pos => let val class_name = Long_Name.qualifier long_name - val SOME{id,...} = DOF_core.get_doc_class_local class_name ctxt' + val DOF_core.Onto_Class {id,...} = DOF_core.get_onto_class_global class_name thy val class_markup = docclass_markup false class_name id def_pos in Context_Position.report ctxt' pos class_markup end in symbex_attr_access0 ctxt' proj_term value end @@ -1245,7 +1191,7 @@ case term_option of val traces = compute_attr_access (Context.Theory thy) "trace" oid NONE pos fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = - let val s' = DOF_core.read_cid (Proof_Context.init_global thy) (HOLogic.dest_string s) + let val s' = DOF_core.get_onto_class_name_global (HOLogic.dest_string s) thy in \<^Const>\Pair \<^typ>\string\ \<^typ>\string\\ $ HOLogic.mk_string s' $ S end val traces' = map conv (HOLogic.dest_list traces) in HOLogic.mk_list \<^Type>\prod \<^typ>\string\ \<^typ>\string\\ traces' end @@ -1470,16 +1416,11 @@ struct fun cid_2_cidType cid_long thy = if cid_long = DOF_core.default_cid then \<^Type>\unit\ - else let val t = #docclass_tab(DOF_core.get_data_global thy) - fun ty_name cid = cid^"."^ Long_Name.base_name cid ^ Record.extN - fun fathers cid_long = case Symtab.lookup t cid_long of - NONE => let val ctxt = Proof_Context.init_global thy - val tty = Syntax.parse_typ (Proof_Context.init_global thy) cid_long - in error("undefined doc class id :"^cid_long) - end - | SOME ({inherits_from=NONE, ...}) => [cid_long] - | SOME ({inherits_from=SOME(_,father), ...}) => - cid_long :: (fathers father) + else let fun ty_name cid = cid^"."^ Long_Name.base_name cid ^ Record.extN + fun fathers cid_long = case DOF_core.get_onto_class_global cid_long thy of + DOF_core.Onto_Class {inherits_from=NONE, ...} => [cid_long] + | DOF_core.Onto_Class {inherits_from=SOME(_,father), ...} => + cid_long :: (fathers father) in fold (fn x => fn y => Type(ty_name x,[y])) (fathers cid_long) \<^Type>\unit\ end @@ -1513,9 +1454,9 @@ fun create_default_object thy class_name = fun check_classref {is_monitor=is_monitor} (SOME(cid,pos)) thy = let - val cid_long = DOF_core.read_cid_global thy cid - - val {id, name=bind_target,rex,...} = the(DOF_core.get_doc_class_global cid_long thy) + val cid_long = DOF_core.get_onto_class_name_global' cid thy + val DOF_core.Onto_Class {id, name=bind_target,rex,...} = + DOF_core.get_onto_class_global cid_long thy val _ = if is_monitor andalso (null rex orelse cid_long= DOF_core.default_cid ) then error("should be monitor class!") else () @@ -1542,8 +1483,8 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long let fun get_class_name parent_cid attribute_name pos = let - val {attribute_decl, inherits_from, ...} = - the (DOF_core.get_doc_class_global parent_cid thy) + val DOF_core.Onto_Class {attribute_decl, inherits_from, ...} = + DOF_core.get_onto_class_global parent_cid thy in if exists (fn (binding, _, _) => Binding.name_of binding = attribute_name) attribute_decl @@ -1558,7 +1499,8 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long val _ = if mk_elaboration then let val attr_defined_cid = get_class_name cid_long lhs pos - val {id, name, ...} = the (DOF_core.get_doc_class_global attr_defined_cid thy) + val DOF_core.Onto_Class {id, name, ...} = + DOF_core.get_onto_class_global attr_defined_cid thy val markup = docclass_markup false cid_long id (Binding.pos_of name); val ctxt = Context.Theory thy in Context_Position.report_generic ctxt pos markup end @@ -1708,10 +1650,10 @@ fun check_invariants thy (oid, pos) = val DOF_core.Instance params = DOF_core.get_instance_global oid thy val cid = #cid params fun get_all_invariants cid thy = - case DOF_core.get_doc_class_global cid thy of - NONE => error("undefined class id for invariants: " ^ cid) - | SOME ({inherits_from=NONE, invs, ...}) => invs - | SOME ({inherits_from=SOME(_,father), invs, ...}) => (invs) @ (get_all_invariants father thy) + case DOF_core.get_onto_class_global cid thy of + DOF_core.Onto_Class {inherits_from=NONE, invs, ...} => invs + | DOF_core.Onto_Class {inherits_from=SOME(_,father), invs, ...} => + (invs) @ (get_all_invariants father thy) val invariants = get_all_invariants cid thy val inv_and_apply_list = let fun mk_inv_and_apply inv value thy = @@ -1778,13 +1720,13 @@ fun check_invariants thy (oid, pos) = fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oid pos cid_pos doc_attrs thy = let - val id = serial (); + val id = serial (); val cid_pos' = check_classref is_monitor cid_pos thy val cid_long = fst cid_pos' val default_cid = cid_long = DOF_core.default_cid val vcid = case cid_pos of NONE => NONE | SOME (cid,_) => if (DOF_core.is_virtual cid thy) - then SOME (DOF_core.parse_cid_global thy cid) + then SOME (DOF_core.get_onto_class_name_global' cid thy) else NONE val value_terms = if default_cid then let @@ -2058,14 +2000,10 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par oid pos cid_pos doc_attrs thy fun compute_enabled_set cid thy = let - val long_cid = DOF_core.read_cid (Proof_Context.init_global thy) cid - in - case DOF_core.get_doc_class_global long_cid thy of - SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X) - val aalph = RegExpInterface.alphabet (#rex X) - in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end - | NONE => error("Internal error: class id undefined. ") - end + val DOF_core.Onto_Class X = DOF_core.get_onto_class_global' cid thy + val ralph = RegExpInterface.alphabet (#rejectS X) + val aalph = RegExpInterface.alphabet (#rex X) + in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end fun create_monitor_entry oid thy = let val cid = case cid_pos of NONE => ISA_core.err ("You must specified a monitor class.") pos @@ -2135,7 +2073,7 @@ fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Pa DOF_core.get_instance_global lab thy in cid |> #cid end - | SOME(cid,_) => DOF_core.parse_cid_global thy cid + | SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) val cid_txt = "type = " ^ (enclose "{" "}" cid_long); @@ -2279,13 +2217,14 @@ end (* structure Monitor_Command_Parser *) ML\ fun print_doc_classes b ctxt = - let val {docclass_tab, ...} = DOF_core.get_data ctxt; + let val classes = Name_Space.dest_table (DOF_core.get_onto_classes 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^")") fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm) fun print_virtual {virtual} = Bool.toString virtual - fun print_class (n, {attribute_decl, id, inherits_from, name, virtual, params, thy_name, rejectS, rex,invs}) = + fun print_class (n, DOF_core.Onto_Class {attribute_decl, id, inherits_from, name, virtual + , params, thy_name, rejectS, rex,invs}) = (case inherits_from of NONE => writeln ("docclass: "^n) | SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + "); @@ -2295,7 +2234,7 @@ fun print_doc_classes b ctxt = writeln (" attrs: "^commas (map print_attr attribute_decl)); writeln (" invs: "^commas (map print_inv invs)) ); - in map print_class (Symtab.dest docclass_tab); + in map print_class classes; writeln "=====================================\n\n\n" end; @@ -2304,7 +2243,8 @@ val _ = (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_classes b o Toplevel.context_of))); fun print_docclass_template cid ctxt = - let val cid_long = DOF_core.read_cid ctxt cid (* assure that given cid is really a long_cid *) + let (* takes class synonyms into account *) + val cid_long = DOF_core.get_onto_class_name_global' cid (Proof_Context.theory_of ctxt) val brute_hierarchy = (DOF_core.get_attributes_local cid_long ctxt) val flatten_hrchy = flat o (map(fn(lname, attrS) => map (fn (s,_,_)=>(lname,(Binding.name_of s))) attrS)) @@ -2410,7 +2350,7 @@ fun meta_args_2_string thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_P NONE => let val DOF_core.Instance cid = DOF_core.get_instance_global lab thy in cid |> #cid end - | SOME(cid,_) => DOF_core.parse_cid_global thy cid + | SOME(cid,_) => DOF_core.get_onto_class_name_global cid thy (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) val cid_txt = "type = " ^ (enclose "{" "}" cid_long); @@ -2586,7 +2526,7 @@ fun compute_trace_ML ctxt oid pos_opt pos' = let val term = ISA_core.compute_attr_access ctxt "trace" oid pos_opt pos' fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = - let val s' = DOF_core.read_cid (Context.proof_of ctxt) (HOLogic.dest_string s) + let val s' = DOF_core.get_onto_class_name_global (HOLogic.dest_string s) (Context.theory_of ctxt) in (s', HOLogic.dest_string S) end in map conv (HOLogic.dest_list term) end @@ -2634,8 +2574,8 @@ fun trace_attr_2_ML ctxt (oid:string,pos) = in toML (compute_trace_ML ctxt oid NONE pos) end 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 + let val _ = DOF_core.get_onto_class_name_global cid (Proof_Context.theory_of ctxt) + in Const(cid,dummyT) end fun compute_name_repr ctxt oid pos = let val instances = DOF_core.get_instances ctxt @@ -2767,7 +2707,8 @@ fun define_inv cid_long ((lbl, pos), inv) thy = (Const (s, Type (st,[ty, ty'])) $ t) = let val cid = Long_Name.qualifier s - in case DOF_core.get_doc_class_global cid thy of + in case Name_Space.lookup + (DOF_core.get_onto_classes (Proof_Context.init_global thy)) cid of NONE => Const (s, Type(st,[ty, ty'])) $ (update_attribute_type thy class_scheme_ty cid_long t) | SOME _ => if DOF_core.is_subclass_global thy cid_long cid @@ -2801,15 +2742,18 @@ fun define_inv cid_long ((lbl, pos), inv) thy = fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy = - let + let val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; - fun cid thy = DOF_core.parse_cid_global thy (Binding.name_of binding) + fun cid thy = (* takes class synonyms into account *) + DOF_core.get_onto_class_name_global' (Binding.name_of binding) thy val (parent, ctxt2) = read_parent raw_parent ctxt1; val parent_cid_long = map_optional snd DOF_core.default_cid parent; (* takes class synonyms into account *) - val parent' = map_option (map_snd (K (DOF_core.read_cid_global thy parent_cid_long))) parent + val parent' = map_option + (map_snd (K (DOF_core.get_onto_class_name_super_class_global thy parent_cid_long))) + parent val parent'_cid_long = map_optional snd DOF_core.default_cid parent'; val raw_fieldsNdefaults' = filter (fn((bi,_,_),_) => Binding.name_of bi <> "trace") raw_fieldsNdefaults diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 2c39493..57322d2 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1033,10 +1033,8 @@ fun check_sil oid _ ctxt = setup\ (fn thy => let val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end - in DOF_core.add_ml_invariant binding check_sil thy end) + val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy +in DOF_core.add_ml_invariant binding check_sil thy end) \ text\ @@ -1076,10 +1074,8 @@ fun check_sil_slow oid _ ctxt = (*setup\ (fn thy => let val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end - in DOF_core.add_ml_invariant binding check_sil_slow thy end) + val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy +in DOF_core.add_ml_invariant binding check_sil_slow thy end) \*) (* As traces of monitor instances (docitems) are updated each time an instance is declared @@ -1111,12 +1107,10 @@ fun check_required_documents oid _ ctxt = \ setup\ -(fn thy => +fn thy => let val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end - in DOF_core.add_closing_ml_invariant binding check_required_documents thy end) + val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy +in DOF_core.add_closing_ml_invariant binding check_required_documents thy end \ (* Test pattern matching for the records of the current CENELEC implementation classes, @@ -1281,10 +1275,10 @@ section\ META : Testing and Validation \ text\Test : @{semi_formal_content \COTS\}\ ML -\ DOF_core.read_cid_global @{theory} "requirement"; - DOF_core.read_cid_global @{theory} "SRAC"; - DOF_core.is_defined_cid_global "SRAC" @{theory}; - DOF_core.is_defined_cid_global "EC" @{theory}; \ +\ DOF_core.get_onto_class_name_global "requirement" @{theory}; + DOF_core.get_onto_class_name_global "SRAC" @{theory}; + DOF_core.get_onto_class_global "SRAC" @{theory}; + DOF_core.get_onto_class_global "EC" @{theory}; \ ML \ DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.EC"; @@ -1294,15 +1288,15 @@ ML ML \ val ref_tab = DOF_core.get_instances \<^context> - val {docclass_tab=class_tab,...} = DOF_core.get_data @{context}; + val docclass_tab = DOF_core.get_onto_classes @{context}; Name_Space.dest_table ref_tab; - Symtab.dest class_tab; \ + Name_Space.dest_table docclass_tab; \ ML \ val internal_data_of_SRAC_definition = DOF_core.get_attributes_local "SRAC" @{context} \ ML -\ DOF_core.read_cid_global @{theory} "requirement"; +\ DOF_core.get_onto_class_name_global "requirement" @{theory}; Syntax.parse_typ @{context} "requirement"; val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT; Syntax.read_typ @{context} "hypothesis" handle _ => dummyT; diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 5a36452..2d7170f 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -495,9 +495,7 @@ let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical", "scholarly_paper.example", "scholarly_paper.conclusion"]; fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check ctxt cidS moni_oid NONE; true) val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "article" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end + val binding = DOF_core.binding_from_onto_class_pos "article" thy in DOF_core.add_ml_invariant binding body thy end) \ diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index 5a1020f..62e8367 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -75,10 +75,7 @@ let fun check_invariant_invariant oid {is_monitor:bool} ctxt = else error("class class invariant violation") | _ => false end - val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "result" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end + val binding = DOF_core.binding_from_onto_class_pos "result" thy in DOF_core.add_ml_invariant binding check_invariant_invariant thy end \ @@ -177,9 +174,7 @@ let val cidS = ["small_math.introduction","small_math.technical", "small_math.co fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check ctxt cidS moni_oid NONE; true) val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "article" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end + val binding = DOF_core.binding_from_onto_class_pos "article" thy in DOF_core.add_ml_invariant binding body thy end \ diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 90240e2..ea41c08 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -27,9 +27,9 @@ print_doc_items ML\ val docitem_tab = DOF_core.get_instances \<^context> val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> -val {docclass_tab, ...} = DOF_core.get_data @{context}; +val docclass_tab = DOF_core.get_onto_classes @{context}; Name_Space.dest_table docitem_tab; -Symtab.dest docclass_tab; +Name_Space.dest_table docclass_tab; \ ML\ val (oid, DOF_core.Instance {value, ...}) = @@ -176,11 +176,6 @@ section\Simulation of a Monitor\ declare[[free_class_in_monitor_checking]] -ML\ -val thy = \<^theory> -val long_cid = "Isa_COL.figure_group" -val t = DOF_core.get_doc_class_global long_cid thy -\ open_monitor*[figs1::figure_group, caption="''Sample ''"] ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ diff --git a/src/tests/Concept_Example_Low_Level_Invariant.thy b/src/tests/Concept_Example_Low_Level_Invariant.thy index 910b52f..c32c993 100644 --- a/src/tests/Concept_Example_Low_Level_Invariant.thy +++ b/src/tests/Concept_Example_Low_Level_Invariant.thy @@ -37,9 +37,7 @@ text\Setting a sample invariant, which simply produces some side-effect:\< setup\ fn thy => let val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "A" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end + val binding = DOF_core.binding_from_onto_class_pos "A" thy in DOF_core.add_ml_invariant binding (fn oid => fn {is_monitor = b} => fn ctxt => @@ -56,10 +54,7 @@ let fun check_A_invariant oid {is_monitor:bool} ctxt = let val term = ISA_core.compute_attr_access ctxt "x" oid NONE @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term in if x_value > 5 then error("class A invariant violation") else true end - val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "A" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end + val binding = DOF_core.binding_from_onto_class_pos "A" thy in DOF_core.add_ml_invariant binding check_A_invariant thy end \ @@ -96,7 +91,7 @@ let fun check_M_invariant oid {is_monitor} ctxt = let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = - let val s' = DOF_core.read_cid (Context.proof_of ctxt) (HOLogic.dest_string s) + let val s' = DOF_core.get_onto_class_name_global' (HOLogic.dest_string s) thy in (s', HOLogic.dest_string S) end val string_pair_list = map conv (HOLogic.dest_list term) val cid_list = map fst string_pair_list @@ -106,10 +101,7 @@ let fun check_M_invariant oid {is_monitor} ctxt = val n = length (filter is_C cid_list) val m = length (filter is_D cid_list) in if m > n then error("class M invariant violation") else true end - val ctxt = Proof_Context.init_global thy - val binding = let val cid = DOF_core.read_cid ctxt "M" - in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) - |> #name end + val binding = DOF_core.binding_from_onto_class_pos "M" thy in DOF_core.add_ml_invariant binding check_M_invariant thy end \ @@ -138,7 +130,8 @@ ML\val ctxt = @{context} fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) fun conv' (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = - let val s' = DOF_core.read_cid ctxt (HOLogic.dest_string s) + let val s' = DOF_core.get_onto_class_name_global' (HOLogic.dest_string s) + (Proof_Context.theory_of ctxt) in (s', HOLogic.dest_string S) end val string_pair_list = map conv' (HOLogic.dest_list term) \ diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index b21131c..6efef90 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -29,13 +29,13 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ -val docitem_tab = DOF_core.get_instances \<^context> -val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> -val {docclass_tab, ...} - = DOF_core.get_data @{context}; +val docitem_tab = DOF_core.get_instances \<^context>; +val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>; +val docclass_tab = DOF_core.get_onto_classes \<^context>; + Name_Space.dest_table docitem_tab; Name_Space.dest_table isa_transformer_tab; -Symtab.dest docclass_tab; +Name_Space.dest_table docclass_tab; app; \ diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy index e0b15c8..50b943b 100644 --- a/src/tests/TermAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -44,7 +44,7 @@ text\Voila the content of the Isabelle_DOF environment so far:\ ML\ val x = DOF_core.get_instances \<^context> val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> -val {docclass_tab,...} = DOF_core.get_data @{context}; +val docclass_tab = DOF_core.get_onto_classes \<^context>; Name_Space.dest_table isa_transformer_tab; \ From 1459b8cfc34bd44603476360e5d5ade66b36e311 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 16 Feb 2023 10:07:56 +0100 Subject: [PATCH 14/18] Use name space markup for onto_class entries reporting --- src/DOF/Isa_DOF.thy | 41 +++++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 01faac9..dad0dff 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -606,15 +606,13 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i its conversion into a class is not yet done. *) let val nn = Context.theory_name thy (* in case that we need the thy-name to identify the space where it is ... *) - val cid = (Binding.name_of binding) - val pos = (Binding.pos_of binding) - (*val _ = if is_defined_cid_global cid thy + (*val cid = (Binding.name_of binding) + val _ = if is_defined_cid_global cid thy then error("redefinition of document class:"^cid ) else ()*) (* takes class synonyms into account *) val parent' = map_option (map_snd (fn x => get_onto_class_name_global' x thy)) parent val id = serial (); - val _ = Position.report pos (docclass_markup true cid id pos); val rejectS = map (Syntax.read_term_global thy) reject_Atoms; val _ = map (check_reject_atom) rejectS; val reg_exps = map (Syntax.read_term_global thy) rexp; @@ -1160,7 +1158,7 @@ fun compute_attr_access ctxt attr oid pos_option pos' = (* template *) |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt' pos' markup; val (* (long_cid, attr_b,ty) = *) - {long_name, typ=ty, def_pos, ...} = + {long_name, typ=ty, ...} = case DOF_core.get_attribute_info_local cid attr ctxt' of SOME f => f | NONE => error("attribute undefined for reference: " @@ -1177,9 +1175,10 @@ fun compute_attr_access ctxt attr oid pos_option pos' = (* template *) | SOME pos => let val class_name = Long_Name.qualifier long_name - val DOF_core.Onto_Class {id,...} = DOF_core.get_onto_class_global class_name thy - val class_markup = docclass_markup false class_name id def_pos - in Context_Position.report ctxt' pos class_markup end + val onto_classes = DOF_core.get_onto_classes ctxt' + val markup = DOF_core.get_onto_class_name_global class_name thy + |> Name_Space.markup (Name_Space.space_of_table onto_classes) + in Context_Position.report ctxt' pos markup end in symbex_attr_access0 ctxt' proj_term value end fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos = @@ -1455,14 +1454,15 @@ fun create_default_object thy class_name = fun check_classref {is_monitor=is_monitor} (SOME(cid,pos)) thy = let val cid_long = DOF_core.get_onto_class_name_global' cid thy - val DOF_core.Onto_Class {id, name=bind_target,rex,...} = - DOF_core.get_onto_class_global cid_long thy + val DOF_core.Onto_Class {rex, ...} = DOF_core.get_onto_class_global cid_long thy val _ = if is_monitor andalso (null rex orelse cid_long= DOF_core.default_cid ) then error("should be monitor class!") else () - val markup = docclass_markup false cid id (Binding.pos_of bind_target); - val ctxt = Context.Theory thy - val _ = Context_Position.report_generic ctxt pos markup; + val ctxt = Proof_Context.init_global thy + val onto_classes = DOF_core.get_onto_classes ctxt + val markup = DOF_core.get_onto_class_name_global cid_long thy + |> Name_Space.markup (Name_Space.space_of_table onto_classes) + val _ = Context_Position.report ctxt pos markup; in (cid_long, pos) end | check_classref _ NONE _ = (DOF_core.default_cid, Position.none) @@ -1475,8 +1475,9 @@ fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long (S:(string * Position.T * string * term)list) term = let val cid_ty = cid_2_cidType cid_long thy + val ctxt = Proof_Context.init_global thy val generalize_term = Term.map_types (generalize_typ 0) - fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t + fun toString t = Syntax.string_of_term ctxt t fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S)) (t) fun read_assn (lhs, pos:Position.T, opr, rhs) term = @@ -1492,18 +1493,18 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long else case inherits_from of NONE => - ISA_core.err ("Attribute " ^ attribute_name ^ " not defined for class: " ^ cid_long) pos + ISA_core.err ("Attribute " ^ attribute_name + ^ " not defined for class: " ^ cid_long) pos | SOME (_, parent_name) => get_class_name parent_name attribute_name pos end val _ = if mk_elaboration then let val attr_defined_cid = get_class_name cid_long lhs pos - val DOF_core.Onto_Class {id, name, ...} = - DOF_core.get_onto_class_global attr_defined_cid thy - val markup = docclass_markup false cid_long id (Binding.pos_of name); - val ctxt = Context.Theory thy - in Context_Position.report_generic ctxt pos markup end + val onto_classes = DOF_core.get_onto_classes ctxt + val markup = DOF_core.get_onto_class_name_global attr_defined_cid thy + |> Name_Space.markup (Name_Space.space_of_table onto_classes) + in Context_Position.report ctxt pos markup end else () val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy val (ln,lnt,lnu,lnut) = case info_opt of From 9de18b148a47f7d23229cff562c96b2d0bf2ca1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 16 Feb 2023 10:41:04 +0100 Subject: [PATCH 15/18] Remove some instance and onto_class datatypes entries Id in instance datatype entry and name, id and thy_name in onto_class datatype entry are now useless, as this information is given by the name space. Remove them --- src/DOF/Isa_DOF.thy | 49 +++++++++++++++++---------------------------- 1 file changed, 18 insertions(+), 31 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index dad0dff..31823cd 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -150,20 +150,16 @@ struct datatype onto_class = Onto_Class of {params : (string * sort) list, (*currently not used *) - name : binding, virtual : {virtual : bool}, - thy_name : string, id : serial, (* for pide *) inherits_from : (typ list * string) option, (* imports *) attribute_decl : (binding*typ*term option)list, (* class local *) rejectS : term list, rex : term list, invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) - fun make_onto_class (params, name, virtual, thy_name, id, inherits_from, attribute_decl - , rejectS, rex, invs) = - Onto_Class {params = params, name = name, virtual = virtual, thy_name = thy_name, id = id - , inherits_from = inherits_from, attribute_decl = attribute_decl, rejectS = rejectS - , rex = rex, invs = invs} + fun make_onto_class (params, virtual, inherits_from, attribute_decl , rejectS, rex, invs) = + Onto_Class {params = params, virtual = virtual, inherits_from = inherits_from + , attribute_decl = attribute_decl, rejectS = rejectS , rex = rex, invs = invs} structure Onto_Classes = Theory_Data ( @@ -257,7 +253,6 @@ struct input_term: term, value: term, inline: bool, - id: serial, cid: string, vcid: string option} @@ -265,13 +260,12 @@ struct input_term = \<^term>\()\, value = \<^term>\()\, inline = false, - id = 0, cid = "", vcid = NONE} - fun make_instance (defined, input_term, value, inline, id, cid, vcid) = - Instance {defined = defined, input_term = input_term, value = value, inline = inline, - id = id, cid = cid, vcid = vcid} + fun make_instance (defined, input_term, value, inline, cid, vcid) = + Instance {defined = defined, input_term = input_term, value = value, inline = inline + , cid = cid, vcid = vcid} structure Instances = Theory_Data ( @@ -604,15 +598,12 @@ fun check_reject_atom term = fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms invs virtual thy = (* This operation is executed in a context where the record has already been defined, but its conversion into a class is not yet done. *) - let val nn = Context.theory_name thy (* in case that we need the thy-name to identify - the space where it is ... *) - (*val cid = (Binding.name_of binding) + let (*val cid = (Binding.name_of binding) val _ = if is_defined_cid_global cid thy then error("redefinition of document class:"^cid ) else ()*) (* takes class synonyms into account *) val parent' = map_option (map_snd (fn x => get_onto_class_name_global' x thy)) parent - val id = serial (); val rejectS = map (Syntax.read_term_global thy) reject_Atoms; val _ = map (check_reject_atom) rejectS; val reg_exps = map (Syntax.read_term_global thy) rexp; @@ -623,8 +614,8 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs)))) else () val invs' = map (map_snd(Syntax.read_term_global thy)) invs - in thy |> add_onto_class binding (make_onto_class (params', binding, virtual, nn, id, parent' - , fields, rejectS, reg_exps, invs')) + in thy |> add_onto_class binding (make_onto_class (params', virtual, parent', fields + , rejectS, reg_exps, invs')) end fun define_object_global {define = define} ((oid, pos), bbb) thy = @@ -636,8 +627,8 @@ fun define_object_global {define = define} ((oid, pos), bbb) thy = val (oid', instance) = Name_Space.check (Context.Theory thy) (get_instances (Proof_Context.init_global thy)) (oid, Position.none) handle ERROR _ => (undefined_instance, empty_instance) - val {input_term, value, inline, id, cid, vcid, ...} = bbb - val instance' = make_instance (define, input_term, value, inline, id, cid, vcid) + val {input_term, value, inline, cid, vcid, ...} = bbb + val instance' = make_instance (define, input_term, value, inline, cid, vcid) in if oid' = undefined_instance andalso instance = empty_instance then add_instance binding instance' thy else if define @@ -725,16 +716,16 @@ fun binding_from_instance_pos name thy = fun update_value_global name upd_value thy = let val binding = binding_from_instance_pos name thy - val Instance {defined, input_term, value, inline, id, cid, vcid} = get_instance_global name thy - val instance' = make_instance (defined, input_term, upd_value value, inline, id, cid, vcid) + val Instance {defined, input_term, value, inline, cid, vcid} = get_instance_global name thy + val instance' = make_instance (defined, input_term, upd_value value, inline, cid, vcid) in update_instance binding (instance') thy end fun update_input_term_global name upd_input_term thy = let val binding = binding_from_instance_pos name thy - val Instance {defined, input_term, value, inline, id, cid, vcid} = get_instance_global name thy + val Instance {defined, input_term, value, inline, cid, vcid} = get_instance_global name thy val instance' = make_instance (defined, upd_input_term input_term, - value, inline, id, cid, vcid) + value, inline, cid, vcid) in update_instance binding (instance') thy end fun update_value_input_term_global name upd_input_term upd_value thy = @@ -1721,7 +1712,6 @@ fun check_invariants thy (oid, pos) = fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oid pos cid_pos doc_attrs thy = let - val id = serial (); val cid_pos' = check_classref is_monitor cid_pos thy val cid_long = fst cid_pos' val default_cid = cid_long = DOF_core.default_cid @@ -1764,7 +1754,6 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi value = value (Proof_Context.init_global thy) (snd value_terms), inline = is_inline, - id = id, cid = cid_long, vcid = vcid}) |> register_oid_cid_in_open_monitors oid pos cid_pos' @@ -2224,14 +2213,12 @@ fun print_doc_classes b ctxt = | print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")") fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm) fun print_virtual {virtual} = Bool.toString virtual - fun print_class (n, DOF_core.Onto_Class {attribute_decl, id, inherits_from, name, virtual - , params, thy_name, rejectS, rex,invs}) = + fun print_class (n, DOF_core.Onto_Class {attribute_decl, inherits_from, virtual + , params, rejectS, rex, invs}) = (case inherits_from of NONE => writeln ("docclass: "^n) | SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + "); - writeln (" name: "^(Binding.print name)); writeln (" virtual: "^(print_virtual virtual)); - writeln (" origin: "^thy_name); writeln (" attrs: "^commas (map print_attr attribute_decl)); writeln (" invs: "^commas (map print_inv invs)) ); @@ -2266,7 +2253,7 @@ fun print_doc_items b ctxt = val _ = writeln "====================================="; fun dfg true = "true" |dfg false= "false" - fun print_item (n, DOF_core.Instance {defined,cid,vcid,id, inline, input_term, value}) = + fun print_item (n, DOF_core.Instance {defined,cid,vcid, inline, input_term, value}) = ((if defined then writeln ("docitem: "^n) else From bdfea3ddb138933be1380c0054264d1def889068 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 17 Feb 2023 09:08:34 +0100 Subject: [PATCH 16/18] Some cleanup --- src/DOF/Isa_DOF.thy | 97 ++++++++++++++++++++------------------------- 1 file changed, 42 insertions(+), 55 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 31823cd..2884f36 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -200,16 +200,13 @@ struct #1 o Name_Space.check (Context.Proof ctxt) (get_onto_classes ctxt); fun add_onto_class name onto_class thy = - thy |> Onto_Classes.map - (Name_Space.define (Context.Theory thy) true (name, onto_class) #> #2); + thy |> Onto_Classes.map (Name_Space.define (Context.Theory thy) true (name, onto_class) #> #2); fun update_onto_class name onto_class thy = - thy |> Onto_Classes.map - (Name_Space.define (Context.Theory thy) false (name, onto_class) #> #2); + thy |> Onto_Classes.map (Name_Space.define (Context.Theory thy) false (name, onto_class) #> #2); - fun update_onto_class_entry name new_onto_class thy = - thy |> Onto_Classes.map - (Name_Space.map_table_entry name (fn _ => new_onto_class)); + fun update_onto_class_entry name new_onto_class = + Onto_Classes.map (Name_Space.map_table_entry name (K new_onto_class)); fun print_onto_classes verbose ctxt = Pretty.big_list "Isabelle.DOF Onto_Classes:" @@ -288,16 +285,13 @@ struct #1 o Name_Space.check (Context.Proof ctxt) (get_instances ctxt); fun add_instance name instance thy = - thy |> Instances.map - (Name_Space.define (Context.Theory thy) true (name, instance) #> #2); + thy |> Instances.map (Name_Space.define (Context.Theory thy) true (name, instance) #> #2); fun update_instance name instance thy = - thy |> Instances.map - (Name_Space.define (Context.Theory thy) false (name, instance) #> #2); + 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 update_instance_entry name new_instance = + Instances.map (Name_Space.map_table_entry name (K new_instance)); fun print_instances verbose ctxt = Pretty.big_list "Isabelle.DOF Instances:" @@ -338,8 +332,7 @@ struct (Name_Space.define (Context.Theory thy) false (name, isa_transformer) #> #2); fun update_isa_transformer_entry name new_isa_transformer thy = - thy |> ISA_Transformers.map - (Name_Space.map_table_entry name (fn _ => new_isa_transformer)); + ISA_Transformers.map (Name_Space.map_table_entry name (K new_isa_transformer)); fun print_isa_transformers verbose ctxt = Pretty.big_list "Isabelle.DOF ISA_Transformers:" @@ -382,9 +375,8 @@ struct thy |> ML_Invariants.map (Name_Space.define (Context.Theory thy) false (name, ml_invariant) #> #2); - fun update_ml_invariant_entry name new_ml_invariant thy = - thy |> ML_Invariants.map - (Name_Space.map_table_entry name (fn _ => new_ml_invariant)); + fun update_ml_invariant_entry name new_ml_invariant = + ML_Invariants.map (Name_Space.map_table_entry name (K new_ml_invariant)); fun print_ml_invariants verbose ctxt = Pretty.big_list "Isabelle.DOF ML_Invariants:" @@ -425,9 +417,8 @@ struct thy |> Opening_ML_Invariants.map (Name_Space.define (Context.Theory thy) false (name, opening_ml_invariant) #> #2); - fun update_opening_ml_invariant_entry name new_opening_ml_invariant thy = - thy |> Opening_ML_Invariants.map - (Name_Space.map_table_entry name (fn _ => new_opening_ml_invariant)); + fun update_opening_ml_invariant_entry name new_opening_ml_invariant = + Opening_ML_Invariants.map (Name_Space.map_table_entry name (K new_opening_ml_invariant)); fun print_opening_ml_invariants verbose ctxt = Pretty.big_list "Isabelle.DOF Opening_ML_Invariants:" @@ -467,9 +458,8 @@ struct thy |> Closing_ML_Invariants.map (Name_Space.define (Context.Theory thy) false (name, closing_ml_invariant) #> #2); - fun update_closing_ml_invariant_entry name new_closing_ml_invariant thy = - thy |> Closing_ML_Invariants.map - (Name_Space.map_table_entry name (fn _ => new_closing_ml_invariant)); + fun update_closing_ml_invariant_entry name new_closing_ml_invariant = + Closing_ML_Invariants.map (Name_Space.map_table_entry name (K new_closing_ml_invariant)); fun print_closing_ml_invariants verbose ctxt = Pretty.big_list "Isabelle.DOF Closing_ML_Invariants:" @@ -521,9 +511,8 @@ struct thy |> Monitor_Info.map (Name_Space.define (Context.Theory thy) false (name, monitor_info) #> #2); - fun update_monitor_info_entry name new_monitor_info thy = - thy |> Monitor_Info.map - (Name_Space.map_table_entry name (fn _ => new_monitor_info)); + fun update_monitor_info_entry name new_monitor_info = + Monitor_Info.map (Name_Space.map_table_entry name (K new_monitor_info)); fun print_monitors_infos verbose ctxt = Pretty.big_list "Isabelle.DOF Monitor_Infos:" @@ -618,25 +607,25 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i , rejectS, reg_exps, invs')) end -fun define_object_global {define = define} ((oid, pos), bbb) thy = +fun define_object_global {define = define} ((oid, pos), instance) thy = let val binding = if Long_Name.is_qualified oid then Binding.make (Long_Name.base_name oid, pos) else Binding.make (oid, pos) val undefined_instance = "undefined_instance" - val (oid', instance) = Name_Space.check (Context.Theory thy) + val (oid', instance') = Name_Space.check (Context.Theory thy) (get_instances (Proof_Context.init_global thy)) (oid, Position.none) handle ERROR _ => (undefined_instance, empty_instance) - val {input_term, value, inline, cid, vcid, ...} = bbb - val instance' = make_instance (define, input_term, value, inline, cid, vcid) - in if oid' = undefined_instance andalso instance = empty_instance - then add_instance binding instance' thy + val Instance {input_term, value, inline, cid, vcid, ...} = instance + val instance'' = make_instance (define, input_term, value, inline, cid, vcid) + in if oid' = undefined_instance andalso instance' = empty_instance + then add_instance binding instance'' thy else if define - then let val Instance {defined, ...} = instance + then let val Instance {defined, ...} = instance' in if defined - then add_instance binding instance' thy - else update_instance_entry oid' instance' thy end - else add_instance binding (Instance bbb) thy + then add_instance binding instance'' thy + else update_instance_entry oid' instance'' thy end + else add_instance binding instance thy end @@ -718,15 +707,14 @@ fun update_value_global name upd_value thy = val binding = binding_from_instance_pos name thy val Instance {defined, input_term, value, inline, cid, vcid} = get_instance_global name thy val instance' = make_instance (defined, input_term, upd_value value, inline, cid, vcid) - in update_instance binding (instance') thy end + in update_instance binding instance' thy end fun update_input_term_global name upd_input_term thy = let val binding = binding_from_instance_pos name thy val Instance {defined, input_term, value, inline, cid, vcid} = get_instance_global name thy - val instance' = make_instance (defined, upd_input_term input_term, - value, inline, cid, vcid) - in update_instance binding (instance') thy end + val instance' = make_instance (defined, upd_input_term input_term, value, inline, cid, vcid) + in update_instance binding instance' thy end fun update_value_input_term_global name upd_input_term upd_value thy = update_value_global name upd_value thy |> update_input_term_global name upd_input_term @@ -1091,8 +1079,8 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name = val mixfix_string = "@{" ^ conv_class_name ^ " _}" in Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))] - #> DOF_core.add_isa_transformer bind (DOF_core.make_isa_transformer - (check_instance, elaborate_instance)) + #> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance) + |> DOF_core.make_isa_transformer) end fun elaborate_instances_list thy isa_name _ _ pos = @@ -1128,8 +1116,8 @@ fun declare_class_instances_annotation thy doc_class_name = val mixfix_string = "@{" ^ conv_class_name' ^ "}" in Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))] - #> DOF_core.add_isa_transformer bind' (DOF_core.make_isa_transformer - (check_identity, elaborate_instances_list)) + #> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list) + |> DOF_core.make_isa_transformer) end fun symbex_attr_access0 ctxt proj_term term = @@ -1620,8 +1608,8 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = val delta_autoS = map is_enabled_for_cid enabled_monitors; fun update_info (n, aS, monitor_info) = let val DOF_core.Monitor_Info {accepted_cids,rejected_cids,...} = monitor_info - in Name_Space.map_table_entry n (fn _ => DOF_core.make_monitor_info - (accepted_cids, rejected_cids, aS)) + in Name_Space.map_table_entry n (K ((accepted_cids, rejected_cids, aS) + |> DOF_core.make_monitor_info)) end fun update_trace mon_oid = if Config.get_global thy DOF_core.object_value_debug @@ -1749,13 +1737,12 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi in case check_option of NONE => (K true) | SOME check => (check oid is_monitor) end) - in thy |> DOF_core.define_object_global {define = define} ((oid, pos), {defined = false, - input_term = fst value_terms, - value = value (Proof_Context.init_global thy) - (snd value_terms), - inline = is_inline, - cid = cid_long, - vcid = vcid}) + in thy |> DOF_core.define_object_global + {define = define} ((oid, pos), DOF_core.make_instance + (false, fst value_terms, + (snd value_terms) + |> value (Proof_Context.init_global thy), + is_inline, cid_long, vcid)) |> register_oid_cid_in_open_monitors oid pos cid_pos' |> (fn thy => if #is_monitor(is_monitor) then ((Context.Theory From 6115f0de4a64ca44c7105d0c2fa1061bb702e3d8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 17 Feb 2023 11:35:51 +0100 Subject: [PATCH 17/18] Some cleanup --- src/DOF/Isa_DOF.thy | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 2884f36..e70c96c 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -174,11 +174,14 @@ struct Name_Space.check (Context.Theory thy) (get_onto_classes (Proof_Context.init_global thy)) (name, Position.none) |> #2 + fun resolve_syn thy name = + name |> Syntax.read_typ_global thy + |> Syntax.string_of_typ_global thy + |> YXML.parse_body |> XML.content_of + (* takes class synonyms into account *) fun get_onto_class_global' name thy = - let val name' = name |> Syntax.read_typ_global thy - |> Syntax.string_of_typ_global thy - |> YXML.parse_body |> XML.content_of + let val name' = name |> resolve_syn thy in Name_Space.check (Context.Theory thy) (get_onto_classes (Proof_Context.init_global thy)) (name', Position.none) |> #2 end @@ -189,9 +192,7 @@ struct (* takes class synonyms into account *) fun get_onto_class_name_global' name thy = - let val name' = name |> Syntax.read_typ_global thy - |> Syntax.string_of_typ_global thy - |> YXML.parse_body |> XML.content_of + let val name' = name |> resolve_syn thy in Name_Space.check (Context.Theory thy) (get_onto_classes (Proof_Context.init_global thy)) (name', Position.none) |> #1 end @@ -687,11 +688,11 @@ fun get_value_local oid ctxt = (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) -fun binding_from_pos get_objects get_objects_name name thy = +fun binding_from_pos get_objects get_object_name name thy = let val ns = get_objects (Proof_Context.init_global thy) |> Name_Space.space_of_table - val {pos, ...} = Name_Space.the_entry ns (get_objects_name name thy) + val {pos, ...} = Name_Space.the_entry ns (get_object_name name thy) in if Long_Name.is_qualified name then Binding.make (Long_Name.base_name name, pos) else Binding.make (name, pos)end @@ -1105,7 +1106,7 @@ fun elaborate_instances_list thy isa_name _ _ pos = fun declare_class_instances_annotation thy doc_class_name = let val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name - val bind' = Binding.suffix_name instances_of_suffixN bind + |> Binding.suffix_name instances_of_suffixN val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy) ((Binding.name_of doc_class_name) ^ " List.list") (* Unfortunately due to different lexical conventions for constant symbols and mixfix symbols @@ -1115,8 +1116,8 @@ fun declare_class_instances_annotation thy doc_class_name = ((Binding.name_of doc_class_name) ^ instances_of_suffixN) val mixfix_string = "@{" ^ conv_class_name' ^ "}" in - Sign.add_consts [(bind', class_list_typ, Mixfix.mixfix(mixfix_string))] - #> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list) + Sign.add_consts [(bind, class_list_typ, Mixfix.mixfix(mixfix_string))] + #> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list) |> DOF_core.make_isa_transformer) end @@ -1201,9 +1202,9 @@ let val ns = Sign.tsig_of thy |> Type.type_space val {pos, ...} = Name_Space.the_entry ns name val bname = Long_Name.base_name name val binding = Binding.make (bname, pos) - val binding' = (Binding.prefix_name DOF_core.ISA_prefix binding) - |> Binding.prefix false bname -in DOF_core.add_isa_transformer binding' ((check, elaborate) |> DOF_core.make_isa_transformer) thy + |> Binding.prefix_name DOF_core.ISA_prefix + |> Binding.prefix false bname +in DOF_core.add_isa_transformer binding ((check, elaborate) |> DOF_core.make_isa_transformer) thy end) #> ([(\<^const_name>\Isabelle_DOF_term_repr\, From 848ce311e2b5b347fa2cb0ea46a214b3ba516e69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 17 Feb 2023 12:56:45 +0100 Subject: [PATCH 18/18] Re-add name field to onto_class To keep the abstract syntax information of the onto_class name, re-add it to the field of the onto_class structure --- src/DOF/Isa_DOF.thy | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index e70c96c..69c5744 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -150,6 +150,7 @@ struct datatype onto_class = Onto_Class of {params : (string * sort) list, (*currently not used *) + name : binding, virtual : {virtual : bool}, inherits_from : (typ list * string) option, (* imports *) attribute_decl : (binding*typ*term option)list, (* class local *) @@ -157,8 +158,8 @@ struct rex : term list, invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) - fun make_onto_class (params, virtual, inherits_from, attribute_decl , rejectS, rex, invs) = - Onto_Class {params = params, virtual = virtual, inherits_from = inherits_from + fun make_onto_class (params, name, virtual, inherits_from, attribute_decl , rejectS, rex, invs) = + Onto_Class {params = params, name = name, virtual = virtual, inherits_from = inherits_from , attribute_decl = attribute_decl, rejectS = rejectS , rex = rex, invs = invs} structure Onto_Classes = Theory_Data @@ -604,7 +605,7 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs)))) else () val invs' = map (map_snd(Syntax.read_term_global thy)) invs - in thy |> add_onto_class binding (make_onto_class (params', virtual, parent', fields + in thy |> add_onto_class binding (make_onto_class (params', binding, virtual, parent', fields , rejectS, reg_exps, invs')) end @@ -2201,11 +2202,12 @@ fun print_doc_classes b ctxt = | print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")") fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm) fun print_virtual {virtual} = Bool.toString virtual - fun print_class (n, DOF_core.Onto_Class {attribute_decl, inherits_from, virtual + fun print_class (n, DOF_core.Onto_Class {attribute_decl, name, inherits_from, virtual , params, rejectS, rex, invs}) = (case inherits_from of NONE => writeln ("docclass: "^n) | SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + "); + writeln (" name: "^(Binding.print name)); writeln (" virtual: "^(print_virtual virtual)); writeln (" attrs: "^commas (map print_attr attribute_decl)); writeln (" invs: "^commas (map print_inv invs))