From b5fe2d908502a897eb9013cc9a534335255ec0ac Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 14 Aug 2019 17:22:55 +0200 Subject: [PATCH] Solution to the assert - Bug : stronger checks in doc_class that reject correctly constructed, but lexically illegal long_names for doc_classes. --- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 2 + .../Isabelle_DOF-Manual/04_RefMan.thy | 14 ++++ .../Isabelle_DOF-Manual.thy | 3 +- src/DOF/Isa_DOF.thy | 71 +++++-------------- .../CENELEC_50128/CENELEC_50128.thy | 6 +- src/ontologies/Conceptual/Conceptual.thy | 16 ++--- src/ontologies/math_paper/math_paper.thy | 8 +-- src/tests/AssnsLemmaThmEtc.thy | 8 +-- src/tests/InnerSyntaxAntiquotations.thy | 3 +- 9 files changed, 58 insertions(+), 73 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index faae7d7..d133c50 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -712,7 +712,9 @@ create dangeling references during the document generation that break the docume Finally, we recommend to use the @{command "check_doc_global"} command at the end of your document to check the global reference structure. + \ + (*<*) end (*>*) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 05624e0..7bd3ef3 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -252,6 +252,15 @@ text\ pecifications~@{cite "wenzel:isabelle-isar:2019"}, and abstract type declarations. \ +text\Note that \isadof works internally with fully qualified names in order to avoid +confusions occurring otherwise, for example, in disjoint class hierarchies. This also extends to +names for \inlineisar|doc_class|es, which must be representable as type-names as well since they +can be used in attribute types. Since theory names are lexically very liberal (\inlineisar|0.thy| +is a legal theory name), this can lead to subtle problems when constructing a class: \inlineisar|foo| +can be a legal name for a type definition, the corresponding type-name \inlineisar|0.foo| is not. +For this reason, additional checks at the definition of a \inlineisar|doc_class| reject problematic +lexical overlaps.\ + subsection*["odl-manual1"::technical]\Defining Document Classes\ text\ @@ -407,6 +416,11 @@ doc_class EC = AC + \ +text*[aaa::assertions]\description with validations I and II\ +assert*[aaa::assertions] "3 < (4::int)" +assert*[aaa::assertions] "0 < (4::int)" + + subsection*["text-elements"::technical]\Annotatable Top-level Text-Elements\ text\ diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy index 6b1896d..b6e5752 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy @@ -8,4 +8,5 @@ text\Resulting trace in doc\_item ''this'': \ ML\@{trace_attribute this}\ end (*>*) - + + diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 9f5b57a..00b74f6 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -254,36 +254,30 @@ fun get_automatas ({automatas, ... } : open_monitor_info) = automatas 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 type_name2doc_class_name thy str = (* Long_Name.qualifier *) str fun typ_to_cid (Type(s,[@{typ "unit"}])) = Long_Name.qualifier s |typ_to_cid (Type(_,[T])) = typ_to_cid T |typ_to_cid _ = error("type is not an ontological type.") -fun name2doc_class_name thy str = - case Syntax.parse_typ (Proof_Context.init_global thy) str of - Type(tyn, _) => type_name2doc_class_name thy tyn - | _ => error "illegal format for doc-class-name." - handle ERROR _ => "" -fun name2doc_class_name_local ctxt str = - (case Syntax.parse_typ ctxt str of - Type(tyn, _) => type_name2doc_class_name ctxt tyn +fun name2doc_class_name_local ctxt cid = + (case Syntax.parse_typ ctxt cid of + Type(tyname, _) => tyname | _ => error "illegal format for doc-class-name.") - handle ERROR _ => "" - + handle ERROR _ => "" (* ignore error *) +fun re_check_class_id thy cid = name2doc_class_name_local (Proof_Context.init_global thy) cid + fun is_defined_cid_global cid thy = let val t = #docclass_tab(get_data_global thy) in cid=default_cid orelse - Symtab.defined t (name2doc_class_name thy cid) + Symtab.defined t (re_check_class_id thy cid) end fun is_defined_cid_global' cid_long thy = 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 = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse Symtab.defined t (name2doc_class_name_local ctxt cid) @@ -364,10 +358,6 @@ fun check_reject_atom cid_long term = (n,_)::_ => error("No schematic variables allowed in monitor regexp:" ^ n) | _ => () (* Missing: Checks on constants such as undefined, ... *) -(* val _ = case term of - Const(_ ,Type(@{type_name "rexp"},[_])) => () - | _ => error("current restriction: only atoms allowed here!") -*) in term end @@ -389,7 +379,9 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms t if not (is_defined_cid_global cid_parent thy) then error("document class undefined : " ^ cid_parent) else () - val cid_long = name2doc_class_name thy cid + val cid_long = re_check_class_id thy cid + val _ = if re_check_class_id thy cid_long <> "" then () + else error"Could not construct type from doc_class (lexical problem?)" val id = serial (); val _ = Position.report pos (docclass_markup true cid id pos); @@ -478,9 +470,10 @@ fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) fun get_attributes_local cid ctxt = if cid = default_cid then [] else let val t = #docclass_tab(get_data ctxt) - val cid_long = name2doc_class_name_local ctxt cid + val cid_long = name2doc_class_name_local ctxt cid (* to assure that the given cid is + really a long_cid *) in case Symtab.lookup t cid_long of - NONE => error("undefined doc class id :"^cid) + NONE => error("undefined doc class id for attributes :"^cid) | SOME ({inherits_from=NONE, attribute_decl = X, ...}) => [(cid_long,X)] | SOME ({inherits_from=SOME(_,father), @@ -1000,7 +993,7 @@ fun base_default_term thy cid_long = Const(@{const_name "undefined"},cid_2_cidTy fun check_classref is_monitor (SOME(cid,pos')) thy = let val _ = if not (DOF_core.is_defined_cid_global cid thy) then error("document class undefined") else () - val cid_long = DOF_core.name2doc_class_name thy cid + val cid_long = DOF_core.re_check_class_id thy cid val {id, name=bind_target,rex,...} = the(DOF_core.get_doc_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!") @@ -1331,7 +1324,7 @@ val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source >> (Toplevel.theory o (enriched_document_command NONE {markdown = true} ))); - + val _ = Outer_Syntax.command @{command_keyword "declare_reference*"} "declare document reference" @@ -1358,9 +1351,8 @@ val _ = fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), prop) = let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) - fun conv_attrs thy = (("property",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") + fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") ::doc_attrs - (* fun conv_attrs thy = (("property",pos),"[@{term ''"^parse_convert thy ^"''}]")::doc_attrs *) fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) fun mks thy = case DOF_core.get_object_global_opt oid thy of SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) @@ -1391,7 +1383,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse let val l = "label = "^ (enclose "{" "}" lab) val cid_long = case cid_opt of NONE => DOF_core.default_cid - | SOME(cid,_) => DOF_core.name2doc_class_name thy cid + | SOME(cid,_) => DOF_core.re_check_class_id thy cid val cid_txt = "type = " ^ (enclose "{" "}" cid_long); fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) @@ -1508,18 +1500,6 @@ end\ section\ Syntax for Ontological Antiquotations (the '' View'' Part II) \ -text\ @{theory Main} @{file "Isa_DOF.thy"}\ - -(* Paradigm theory or paradigm file ? - - val basic_entity = Thy_Output.antiquotation_pretty_source; - ... - basic_entity \<^binding>\theory\ (Scan.lift (Parse.position Args.embedded)) pretty_theory #> - - Thy_Output.antiquotation_raw \<^binding>\file\ - (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #> - -*) ML\ (* 2017: used eg by ::: text\ @{theory Main}\ @@ -1540,22 +1520,9 @@ val basic_entity = Thy_Output.antiquotation_pretty_source (Proof.context -> 'a -> Pretty.T) -> theory -> theory; -(* or ? *) -val docref_scan = (Scan.lift (Parse.position Args.embedded)) - : (string * Position.T) context_parser; -(*val X = Document_Antiquotation.setup \<^binding>\docref\ docref_scan ; *) + \ -text\ @{theory Main}\ - -ML\ - Latex.string : string -> Latex.text ; - Latex.text: string * Position.T -> Latex.text; - Latex.block: Latex.text list -> Latex.text; - Latex.enclose_body: string -> string -> Latex.text list -> Latex.text list; - Latex.enclose_block: string -> string -> Latex.text list -> Latex.text; - Latex.output_text: Latex.text list -> string; -\ ML\ @@ -1800,7 +1767,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) 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.name2doc_class_name thy (Binding.name_of binding) + fun cid thy = DOF_core.re_check_class_id thy (Binding.name_of binding) val (parent, ctxt2) = read_parent raw_parent ctxt1; val parent_cid_long = case parent of NONE => DOF_core.default_cid diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 46cbfe8..cfa0437 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -695,8 +695,8 @@ section\ META : Testing and Validation \ text\Test : @{concept \COTS\}\ ML\ -DOF_core.name2doc_class_name @{theory} "requirement"; -DOF_core.name2doc_class_name @{theory} "SRAC"; +DOF_core.re_check_class_id @{theory} "requirement"; +DOF_core.re_check_class_id @{theory} "SRAC"; DOF_core.is_defined_cid_global "SRAC" @{theory}; DOF_core.is_defined_cid_global "EC" @{theory}; \ @@ -718,7 +718,7 @@ val internal_data_of_SRAC_definition = DOF_core.get_attributes_local "SRAC" @{co \ ML\ -DOF_core.name2doc_class_name @{theory} "requirement"; +DOF_core.re_check_class_id @{theory} "requirement"; 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/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index 4fcbc64..3c202eb 100644 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -31,11 +31,11 @@ doc_class E = D + x :: "string" <= "''qed''" (* overriding default *) doc_class F = - property :: "term list" - r :: "thm list" - u :: "file" - s :: "typ list" - b :: "(A \ C) set" <= "{}" (* This is a relation link, roughly corresponding + properties :: "term list" + r :: "thm list" + u :: "file" + s :: "typ list" + b :: "(A \ C) set" <= "{}" (* This is a relation link, roughly corresponding to an association class. It can be used to track claims to result - relations, for example.*) doc_class G = C + @@ -56,9 +56,9 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl section*[test::A]\Test and Validation\ text\Defining some document elements to be referenced in later on in another theory: \ -text*[sdf]\ f @{thm refl}\ -text*[ sdfg] \ fg @{thm refl}\ -text*[ xxxy ] \ dd @{docitem \sdfg\} @{thm refl}\ +text*[sdf]\ Lorem ipsum @{thm refl}\ +text*[ sdfg] \ Lorem ipsum @{thm refl}\ +text*[ xxxy ] \ Lorem ipsum @{docitem \sdfg\} rate @{thm refl}\ end diff --git a/src/ontologies/math_paper/math_paper.thy b/src/ontologies/math_paper/math_paper.thy index 22a2bce..a46d845 100644 --- a/src/ontologies/math_paper/math_paper.thy +++ b/src/ontologies/math_paper/math_paper.thy @@ -70,20 +70,20 @@ text*[dil_fun :: "definition"]\A dilating function for a run @{term "\This monitor is used to group formal content in a way to classify the relevance. On the presentation level, this gives the possibility to adapt or omit diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy index ef640b1..d71fa26 100644 --- a/src/tests/AssnsLemmaThmEtc.thy +++ b/src/tests/AssnsLemmaThmEtc.thy @@ -16,11 +16,11 @@ print_doc_items section\Definitions, Lemmas, Theorems, Assertions\ -text*[aa::F, property = "[@{term ''True''}]"] +text*[aa::F, properties = "[@{term ''True''}]"] \Our definition of the HOL-Logic has the following properties:\ assert*[aa::F] "True" -(* does not work in batch mode ... +(* does not work in batch mode ... (* sample for accessing a property filled with previous assert's of "aa" *) ML\ ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};\ @@ -30,10 +30,10 @@ assert*[aa::F] " X \ Y \ True" (*example with uni-code *) ML\ ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa}; app writeln (tl (rev it));\ -*) + assert*[aa::F] "\x::bool. X \ Y \ True" (*problem with uni-code *) - +*) ML\ Syntax.read_term_global @{theory} "[@{termrepr ''True @ True''}]"; (* this only works because the isa check is not activated in "term" !!! *) diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/InnerSyntaxAntiquotations.thy index 0cd5fef..fafb4e1 100644 --- a/src/tests/InnerSyntaxAntiquotations.thy +++ b/src/tests/InnerSyntaxAntiquotations.thy @@ -49,7 +49,7 @@ text*[xcv4::F, r="[@{thm ''HOL.refl''}, @{thm ''InnerSyntaxAntiquotations.murks''}]", b="{(@{docitem ''xcv1''},@{docitem ''xcv2''})}", s="[@{typ ''int list''}]", - property = "[@{term ''H --> H''}]" + properties = "[@{term ''H --> H''}]" ]\Lorem ipsum ...\ text*[xcv5::G, g="@{thm ''HOL.sym''}"]\Lorem ipsum ...\ @@ -64,3 +64,4 @@ text\And here is the result on term level:\ ML\ @{docitem_attribute b::xcv4} \ end +