From d2a6106be5eaa7198eeb817a3de158981c1e7548 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 17 Nov 2021 12:55:37 +0100 Subject: [PATCH] Fix the record generation in class implementation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Fix the generation of the record associated with a class and used for the logic. The old implementation generated a new attribute for each attribute defined by a subclass, even the ones that were overriding ones of the superclass. The new implementation generates the attributes of the subclass which are not overriding ones. Warning: It implies that overridden attributes in a subclass are not new attributes added to the theory context. So the base name of an attribute will refer to the attribute of the last declared class where it is defined. If ones wants to refer to atttributes, one should use long names, even in the invariants of a subclass definition which overrides the attribute used in the invariant. For example, in ~~/src/ontologies/scholarly_paper/scholarly_paper.thy: doc_class technical = text_section + definition_list :: "string list" <= "[]" status :: status <= "description" formal_results :: "thm list" invariant L1 :: "λσ::technical. the (level σ) > 0" type_synonym tc = technical (* technical content *) doc_class example = text_section + referentiable :: bool <= True status :: status <= "description" short_name :: string <= "''''" doc_class math_content = tc + referentiable :: bool <= True short_name :: string <= "''''" status :: status <= "semiformal" mcc :: "math_content_class" <= "thm" invariant s1 :: "λ σ::math_content. ¬referentiable σ ⟶ short_name σ = ''''" invariant s2 :: "λ σ::math_content. technical.status σ = semiformal" The class math_content overrride the attribute status of the class technical, by using the type synonym tc, but the base name of this attribute refers to the attribute of the class example where it is last defined and not just overridden. So in the invariant s2 of the class math_content, we must use the long name of the attribute, i.e. the base name "status" with its qualifier which refers to the superclass where it is defined, the class technical. Type synonyms as qualifiers are not yet supported. - Qualify classes that only override attributes of their superclass as vitual classes by adding a virtual attribute. This attribute is used to discriminate virtual classes and generate an adequate make function to initialize their associated record. The implementation uses an hidden attribute (the tag_attribute) to force the virtual class to be concrete or the logic by having a full new record definition associated with it. For example: doc_class W = a::"int" <= "1" doc_class X = W + a::"int" <= "2" The class X is tagged as a virtual class and the record make functions of the classes W and X are: W.make W_tag_attribute W_a X.make X_tag_attribute X_a X_tag_attribute So a record definition is added to the theory context for each class, even though a virtual class only overrides attributes of its superclass. This behavior allows us to support definitions of new default values for attributes in the subclass, as shown in the example. - Factorize make name components - Use Record name components instead of strings to refer to Record components - Fix typos --- src/DOF/Isa_DOF.thy | 180 +++++++++++------- .../scholarly_paper/scholarly_paper.thy | 2 +- 2 files changed, 116 insertions(+), 66 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index dcaa259..7ae3bc7 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -59,7 +59,12 @@ section\Primitive Markup Generators\ ML\ val docrefN = "docref"; -val docclassN = "doc_class"; +val docclassN = "doc_class"; + + +(** name components **) + +val makeN = "make"; (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = @@ -121,6 +126,7 @@ fun map_optional _ s NONE = s fun map_fst f (x,y) = (f x,y) fun map_snd f (x,y) = (x,f y) +fun map_eq_fst_triple f (x,_,_) (y,_,_) = equal (f x) (f y) \ @@ -131,9 +137,10 @@ ML\ structure DOF_core = struct - + type virtual = {virtual : bool} type docclass_struct = {params : (string * sort) list, (*currently not used *) - name : binding, + 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 *) @@ -177,7 +184,8 @@ struct value : term, inline : bool, id : serial, - cid : string} + cid : string, + vcid : string option} type docobj_tab ={tab : (docobj option) Symtab.table, maxano : int @@ -302,7 +310,7 @@ fun typ_to_cid (Type(s,[@{typ "unit"}])) = Long_Name.qualifier s fun parse_cid ctxt cid = -(* parses a type lexically/syntactically, checks abscence of type vars *) +(* 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.") @@ -313,7 +321,7 @@ 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 + 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 @@ -372,6 +380,13 @@ fun is_defined_oid_local oid thy = let val {tab,...} = #docobj_tab(get_data th |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 + in case Symtab.lookup tab long_name of + NONE => error("Undefined class id: " ^ cid) + | 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} @@ -426,8 +441,8 @@ fun check_reject_atom cid_long term = in term end -fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms invs thy = -(* This operation is executed in a context where the record has amready been defined, but +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 ... *) @@ -437,9 +452,7 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i 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 @@ -461,7 +474,8 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i else () val invs' = map (map_snd(Syntax.read_term_global thy)) invs val info = {params=params', - name = binding, + name = binding, + virtual = virtual, thy_name = nn, id = id, (* for pide --- really fresh or better reconstruct from prior record definition ? For the moment: own @@ -551,11 +565,13 @@ fun get_attributes_local cid ctxt = fun get_attributes cid thy = get_attributes_local cid (Proof_Context.init_global thy) + fun get_all_attributes_local cid ctxt = (tag_attr, get_attributes_local cid ctxt) fun get_all_attributes cid thy = get_all_attributes_local cid (Proof_Context.init_global thy) + type attributes_info = { def_occurrence : string, def_pos : Position.T, long_name : string, @@ -595,10 +611,10 @@ fun get_value_local oid ctxt = case get_object_local oid ctxt of (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) fun update_value_global oid upd thy = case get_object_global oid thy of - SOME{pos,thy_name,value,inline,id,cid} => + SOME{pos,thy_name,value,inline,id,cid,vcid} => let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, value=upd value,id=id, - inline=inline,cid=cid}) + 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) @@ -677,12 +693,14 @@ fun print_doc_items b ctxt = val _ = writeln "====================================="; fun dfg true = "true" |dfg false= "false" - fun print_item (n, SOME({cid,id,pos,thy_name,inline,value})) = - (writeln ("docitem: "^n); - writeln (" type: "^cid); - writeln (" origine: "^thy_name); - writeln (" inline: "^dfg inline); - writeln (" value: "^(Syntax.string_of_term ctxt value)) + fun print_item (n, SOME({cid,vcid,id,pos,thy_name,inline,value})) = + (writeln ("docitem: "^n); + writeln (" type: "^cid); + case vcid of NONE => () | SOME (s) => + writeln (" virtual type: "^ s); + writeln (" origine: "^thy_name); + writeln (" inline: "^dfg inline); + writeln (" value: "^(Syntax.string_of_term ctxt value)) ) | print_item (n, NONE) = (writeln ("forward reference for docitem: "^n)); @@ -709,14 +727,16 @@ fun print_doc_classes b ctxt = 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_class (n, {attribute_decl, id, inherits_from, name, params, thy_name, rejectS, rex,invs}) = + fun print_virtual {virtual} = Bool.toString virtual + fun print_class (n, {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^" + "); - writeln (" name: "^(Binding.print name)); - writeln (" origin: "^thy_name); - writeln (" attrs: "^commas (map print_attr attribute_decl)); - writeln (" invs: "^commas (map print_inv invs)) + 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)) ); in map print_class (Symtab.dest docclass_tab); writeln "=====================================\n\n\n" @@ -1022,7 +1042,6 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name = Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))] #> (fn thy => let val long_name = DOF_core.read_cid_global thy (Binding.name_of doc_class_name) - (*val bname = Long_Name.base_name long_name*) val qual = Long_Name.qualifier long_name val class_name = Long_Name.qualify qual (DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind)) @@ -1157,7 +1176,7 @@ val attributes_upd = fun cid_2_cidType cid_long thy = if cid_long = DOF_core.default_cid then @{typ "unit"} else let val t = #docclass_tab(DOF_core.get_data_global thy) - fun ty_name cid = cid^"."^ Long_Name.base_name cid^"_ext" + 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 @@ -1171,15 +1190,30 @@ fun cid_2_cidType cid_long thy = end fun create_default_object thy class_name = -let - val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name - val make_const = Syntax.read_term_global thy (class_name ^ ".make"); - fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_" - ^ (Binding.name_of binding) - ^ "_Attribute_Not_Initialized", typ) - fun all_attr_free_list (tag_attr, class_list) = - (attr_to_free tag_attr)::(map (attr_to_free) (flat (map snd class_list))) -in list_comb (make_const, all_attr_free_list (DOF_core.get_all_attributes class_name thy)) end; + let + val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name + val make_const = Syntax.read_term_global thy (Long_Name.qualify class_name makeN); + fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_" + ^ (Binding.name_of binding) + ^ "_Attribute_Not_Initialized", typ) + val class_list' = DOF_core.get_attributes class_name thy + fun attrs_filter [] = [] + | attrs_filter (x::xs) = + let val (cid, ys) = x + fun is_duplicated _ [] = false + | is_duplicated y (x::xs) = + let val (_, ys) = x + in if exists (map_eq_fst_triple Binding.name_of y) ys + then true + else is_duplicated y xs end + in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end + val class_list'' = rev (attrs_filter (rev class_list')) + fun add_tag_to_attrs_free tag_attr thy (cid, filtered_attr_list) = + if DOF_core.is_virtual cid thy + then (attr_to_free tag_attr)::(map (attr_to_free) filtered_attr_list) + else (map (attr_to_free) filtered_attr_list) + val class_list''' = flat (map (add_tag_to_attrs_free DOF_core.tag_attr thy) class_list'') + in list_comb (make_const, (attr_to_free DOF_core.tag_attr)::class_list''') end fun base_default_term cid_long thy = create_default_object thy cid_long; @@ -1215,7 +1249,7 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) ^((Long_Name.base_name lhs)) ^"< in class: "^cid_long) | SOME{long_name, typ, ...} => (long_name, typ, - long_name ^"_update", + long_name ^ Record.updateN, (typ --> typ) --> cid_ty --> cid_ty) val tyenv = Sign.typ_match thy ((generalize_typ 0)(type_of rhs), lnt) (Vartab.empty) @@ -1310,6 +1344,10 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do (* 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 cid_long = check_classref is_monitor cid_pos thy + 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) + else NONE val value_term = if (cid_long = DOF_core.default_cid) then (Free ("Undefined_Value", @{typ "unit"})) (* @@ -1334,7 +1372,8 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do value = value_term, inline = is_inline, id = id, - cid = cid_long}) + cid = cid_long, + vcid = vcid}) |> register_oid_cid_in_open_monitors oid pos cid_long |> (fn thy => (check_inv thy; thy)) end @@ -2020,7 +2059,7 @@ fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u; fun define_cond binding f_sty cond_suffix read_cond (ctxt:local_theory) = let val bdg = Binding.suffix_name cond_suffix binding val eq = mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond ctxt) - val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) + val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) in def_cmd args true ctxt end fun define_inv cid_long ((lbl, pos), inv) thy = @@ -2029,7 +2068,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy = val inv_ty = (Syntax.read_typ_global thy cid_long) --> HOLogic.boolT in thy |> Named_Target.theory_map (define_cond bdg inv_ty "_inv" inv_term) end -fun add_doc_class_cmd overloaded (raw_params, binding) +fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy = let val ctxt = Proof_Context.init_global thy; @@ -2038,8 +2077,9 @@ fun add_doc_class_cmd overloaded (raw_params, binding) fun cid thy = DOF_core.parse_cid_global thy (Binding.name_of binding) 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 *) + (* takes class synonyms into account *) val parent' = map_option (map_snd (K (DOF_core.read_cid_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 val _ = if length raw_fieldsNdefaults' <> length raw_fieldsNdefaults @@ -2049,39 +2089,49 @@ fun add_doc_class_cmd overloaded (raw_params, binding) then raw_fieldsNdefaults' else trace_attr::raw_fieldsNdefaults' val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults'' ctxt2; - val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms val params' = map (Proof_Context.check_tfree ctxt3) params; fun check_n_filter thy (bind,ty,mf) = - case DOF_core.get_attribute_info parent_cid_long (Binding.name_of bind) thy of - NONE => (* no prior declaration *) SOME(bind,ty,mf) - | SOME{def_occurrence,long_name,typ,...} => if ty = typ - then (warning("overriding attribute:"^long_name^ - " in doc class:" ^ def_occurrence); - SOME(bind,ty,mf)) - else error("no overloading allowed.") - val _ = map_filter (check_n_filter thy) fields - - - in thy |> (fn thy => case parent' of - NONE => Record.add_record - overloaded (params', binding) parent' (DOF_core.tag_attr::fields) thy - | SOME _ => Record.add_record - overloaded (params', binding) parent' (fields) thy) - |> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)]) - |> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps - reject_Atoms invariants + case DOF_core.get_attribute_info parent'_cid_long (Binding.name_of bind) thy of + NONE => SOME(bind,ty,mf) + | SOME{def_occurrence,long_name,typ,...} + => if ty = typ + then (warning("overriding attribute:" + ^ long_name + ^ " in doc class:" + ^ def_occurrence); + 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.*) + in thy |> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)]) + |> (fn thy => + 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 + | SOME _ => + if (not o null) 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 + 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) + |> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy) (* defines the ontology-checked text antiquotation to this document class *) |> (fn thy => fold(define_inv (cid thy)) (invariants) thy) - (* - The function declare_ISA_class_accessor_and_check_instance uses a prefix - because the class name is already bound to "doc_class Regular_Exp.rexp" constant - by add_doc_class_cmd function - *) - |> ISA_core.declare_ISA_class_accessor_and_check_instance binding + (* The function declare_ISA_class_accessor_and_check_instance uses a prefix + because the class name is already bound to "doc_class Regular_Exp.rexp" constant + by add_doc_class_cmd function *) + |> ISA_core.declare_ISA_class_accessor_and_check_instance binding end; diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index daa7d55..749f381 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -187,7 +187,7 @@ doc_class math_content = tc + status :: status <= "semiformal" mcc :: "math_content_class" <= "thm" invariant s1 :: "\ \::math_content. \referentiable \ \ short_name \ = ''''" - invariant s2 :: "\ \::math_content. status \ = semiformal" + invariant s2 :: "\ \::math_content. technical.status \ = semiformal" type_synonym math_tc = math_content text\The class \<^typ>\math_content\ is perhaps more adequaltely described as "math-alike content".