diff --git a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy index 51ff20a..0361e9b 100644 --- a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy +++ b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy @@ -17,7 +17,7 @@ no_notation "Isabelle_DOF_file" ("@{file _}") no_notation "Isabelle_DOF_thy" ("@{thy _}") no_notation "Isabelle_DOF_docitem" ("@{docitem _}") no_notation "Isabelle_DOF_docitem_attr" ("@{docitemattr (_) :: (_)}") -no_notation "Isabelle_DOF_trace_attribute" ("@{trace-attribute _}") +no_notation "Isabelle_DOF_trace_attribute" ("@{trace'_-attribute _}") consts Isabelle_DOF_typ :: "string \ typ" ("@{typ _}") consts Isabelle_DOF_term :: "string \ term" ("@{term _}") @@ -27,7 +27,7 @@ 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 _}") +consts Isabelle_DOF_trace_attribute :: "string \ (string * string) list" ("@{trace'_-attribute _}") subsection\ Semantics \ diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index 14ba9f3..092ec22 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -214,12 +214,12 @@ no_notation Plus (infixr "||" 55) no_notation Times (infixr "~~" 60) no_notation Atom ("\_\" 65) -value* \ DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \aaa\}) \ +value* \ DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace_attribute \aaa\}) \ definition word_test :: "'a list \ 'a rexp \ bool" (infix "is-in" 60) where " w is-in rexp \ DA.accepts (na2da (rexp2na rexp)) (w)" -value* \ (map fst @{trace-attribute \aaa\}) is-in example_expression \ +value* \ (map fst @{trace_attribute \aaa\}) is-in example_expression \ (*<*) diff --git a/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy b/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy index 878c465..7393db5 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy @@ -213,9 +213,9 @@ value*\@{scholarly_paper.author \church'\}\ value*\@{author \church\}\ value*\@{Concept_High_Level_Invariants.author \church\}\ -value*\@{scholarly_paper.author_instances}\ -value*\@{author_instances}\ -value*\@{Concept_High_Level_Invariants.author_instances}\ +value*\@{instances_of \scholarly_paper.author\}\ +value*\@{instances_of \author\}\ +value*\@{instances_of \Concept_High_Level_Invariants.author\}\ text*[introduction3::introduction, authored_by = "{@{author \church\}}", level = "Some 2"]\\ text*[introduction4::introduction, authored_by = "{@{author \curry\}}", level = "Some 4"]\\ diff --git a/Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy b/Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy index ceb9fb6..fcea1ea 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy @@ -104,8 +104,8 @@ ML\ val (oid, DOF_core.Instance {value, ...}) = Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none) \ -term*\map fst @{trace-attribute \test_monitor_M\}\ -value*\map fst @{trace-attribute \test_monitor_M\}\ +term*\map fst @{trace_attribute \test_monitor_M\}\ +value*\map fst @{trace_attribute \test_monitor_M\}\ ML\@{assert} ([("Conceptual.A", "test"), ("Conceptual.F", "sdfg")] = @{trace_attribute aaa}) \ diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy index 17e8b9d..d821672 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy @@ -136,6 +136,9 @@ ML\@{thm "refl"}\ section\Request on instances\ +text\The instances directly attached to the default super class \text\: \ +value*\@{instances_of \text\}\ + text\We define a new class Z:\ doc_class Z = z::"int" @@ -146,28 +149,27 @@ text*[test2Z::Z, z=4]\lorem ipsum...\ text*[test3Z::Z, z=3]\lorem ipsum...\ text\We want to get all the instances of the @{doc_class Z}:\ -value*\@{Z_instances}\ +value*\@{instances_of \Z\}\ text\Now we want to get the instances of the @{doc_class Z} whose attribute z > 2:\ -value*\filter (\\. Z.z \ > 2) @{Z_instances}\ +value*\filter (\\. Z.z \ > 2) @{instances_of \Z\}\ text\We can check that we have the list of instances we wanted:\ -value*\filter (\\. Z.z \ > 2) @{Z_instances} = [@{Z \test3Z\}, @{Z \test2Z\}] - \ filter (\\. Z.z \ > 2) @{Z_instances} = [@{Z \test2Z\}, @{Z \test3Z\}]\ +assert*\filter (\\. Z.z \ > 2) @{instances_of \Z\} = [@{Z \test3Z\}, @{Z \test2Z\}] + \ filter (\\. Z.z \ > 2) @{instances_of \Z\} = [@{Z \test2Z\}, @{Z \test3Z\}]\ text\Now, we want to get all the instances of the @{doc_class A}\ -value*\@{A_instances}\ +value*\@{instances_of \A\}\ -(*<*) -text\Warning: If you make a request on attributes that are undefined in some instances, -you will get a result which includes these unresolved cases. + +text\Warning: Requests on attributes that are undefined in some instances +include all the instances. In the following example, we request the instances of the @{doc_class A}. -But we have defined an instance @{docitem \sdf\} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"} -whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\x\. -So in the request result we get an unresolved case because the evaluator can not get -the value of the \<^emph>\x\ attribute of the instance @{docitem \sdf\}:\ -value*\filter (\\. A.x \ > 5) @{A_instances}\ -(*>*) +But we have defined instances @{A \axx\} and @{A \axx\} previously +and these docitem instances do not initialize their \<^const>\A.x\ attribute. +So the request can not be evaluated:\ +value*\filter (\\. A.x \ > 5) @{instances_of \A\}\ + section\Limitations\ text\There are still some limitations. @@ -226,7 +228,7 @@ text\... and here we reference @{A \assertionA\}.\ assert*\evidence @{result \resultProof\} = evidence @{result \resultProof2\}\ text\The optional evaluator of \value*\ and \assert*\ must be specified before the meta arguments:\ -value* [nbe] [optional_test_A::A, x=6] \filter (\\. A.x \ > 5) @{A_instances}\ +value* [nbe] [optional_test_A::A, x=6] \filter (\\. A.x \ > 5) @{instances_of \A\}\ assert* [nbe] [resultProof3::result, evidence = "proof", property="[@{thm \HOL.sym\}]"] \evidence @{result \resultProof3\} = evidence @{result \resultProof2\}\ diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy index f6f255a..0d5aa30 100644 --- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy +++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy @@ -3,6 +3,11 @@ theory Test_Polymorphic_Classes TestKit begin +text\The name \text\ is reserved by the implementation and refers to the default super class:\ +doc_class-assert-error "text" = +a::int +\text: This name is reserved by the implementation\ + doc_class title = short_title :: "string option" <= "None" diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index ba42a64..6f02e90 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -1050,7 +1050,8 @@ 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 _}") +consts Isabelle_DOF_trace_attribute :: "string \ (string * string) list" ("@{trace'_attribute _}") +consts Isabelle_DOF_instances_of :: "string \ 'a list" ("@{instances'_of _}") \ \Dynamic setup of inner syntax cartouche\ @@ -1192,12 +1193,27 @@ fun check_instance thy (term, _, pos) s = val name' = DOF_core.cid_of name thy |> DOF_core.get_onto_class_cid thy |> (fst o fst) fun check' (class_name, object_cid) = - if class_name = object_cid then - DOF_core.value_of name thy + if class_name = object_cid + then () else err (name ^ " is not an instance of " ^ class_name) pos in check' (class_name, name') end; in ML_isa_check_generic check thy (term, pos) end +fun check_instance_of thy (term, _, pos) _ = + let + fun check thy (name, _) = + if equal name DOF_core.default_cid + then () + else + let + val class_typ = name |> DOF_core.get_onto_class_cid thy |> snd + fun check' (class_name, typ) = + if equal (class_name |> Syntax.read_typ_global thy) typ + then () + else err (name ^ " is not a class name") pos + in check' (name, class_typ) end; + in ML_isa_check_generic check thy (term, pos) end + fun ML_isa_id _ (term,_) = SOME term @@ -1273,44 +1289,44 @@ fun declare_ISA_class_accessor_and_check_instance (params, doc_class_name, bind_ end -fun elaborate_instances_list thy isa_name _ _ _ = +fun elaborate_instances_of thy _ _ term_option _ = let - val base_name = Long_Name.base_name isa_name - val qualifier = Long_Name.qualifier isa_name - val isa_name' = (case try (unprefix DOF_core.doc_class_prefix) base_name of - NONE => unprefix DOF_core.long_doc_class_prefix base_name - | SOME name => name) - |> unsuffix instances_of_suffixN - |> Long_Name.qualify qualifier - val class_typ = isa_name' |> Proof_Context.read_typ (Proof_Context.init_global thy) - val long_class_name = DOF_core.get_onto_class_name_global isa_name' thy - val values = thy |> Proof_Context.init_global |> DOF_core.get_instances - |> Name_Space.dest_table - |> filter (fn (name, _) => equal (DOF_core.cid_of name thy) long_class_name) - |> map (fn (oid, _) => DOF_core.value_of oid thy) - in HOLogic.mk_list class_typ values end - - -fun declare_class_instances_annotation (params, doc_class_name, bind_pos) thy = - let - val bname = Long_Name.base_name doc_class_name - val bname' = prefix DOF_core.doc_class_prefix bname |> suffix instances_of_suffixN - val bind = bname' |> pair bind_pos |> swap |> Binding.make - val bind' = prefix DOF_core.long_doc_class_prefix bname - |> suffix instances_of_suffixN |> pair bind_pos |> swap |> Binding.make - val typ = Type (doc_class_name, map TFree params) - fun mixfix_enclose name = name |> enclose "@{" "}" - val mixfix = clean_mixfix (bname ^ instances_of_suffixN) |> mixfix_enclose - val mixfix' = clean_mixfix (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose - in - thy |> rm_mixfix bname' mixfix - |> Sign.add_consts [(bind, \<^Type>\list typ\, Mixfix.mixfix mixfix)] - |> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list) - |> DOF_core.make_isa_transformer) - |> Sign.add_consts [(bind', \<^Type>\list typ\, Mixfix.mixfix mixfix')] - |> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list) - |> DOF_core.make_isa_transformer) - end + val class_name = case term_option of + NONE => error ("Malformed term annotation") + | SOME term => HOLogic.dest_string term + fun mk_list class_typ f = + let + val values = thy |> Proof_Context.init_global |> DOF_core.get_instances + |> Name_Space.dest_table + |> map fst + |> tap (fn is => writeln ("In elaborate_instances_list instances: " ^ \<^make_string> is)) + |> f + |> tap (fn is => writeln ("In elaborate_instances_list instances after filter: " ^ \<^make_string> is)) + |> map (fn oid => DOF_core.value_of oid thy) + in HOLogic.mk_list class_typ values end + in if equal class_name DOF_core.default_cid + then + (* When the class name is default_cid = "text", + return the instances attached to this default class. + We want the class default_cid to stay abstract + and not have the capability to be defined with attribute, invariants, etc. + Hence this can handle docitem without a class associated, + for example when you just want a document element to be referentiable + without using the burden of ontology classes. + ex: text*[sdf]\ Lorem ipsum @{thm refl}\ *) + (filter (fn name => DOF_core.cid_of name thy |> equal DOF_core.default_cid)) + |> mk_list \<^typ>\unit\ + else + let + val class_typ = class_name |> Syntax.read_typ_global thy + in + (filter_out (fn name => DOF_core.cid_of name thy |> equal DOF_core.default_cid) + #> filter (fn name => DOF_core.cid_of name thy + |> Syntax.read_typ_global thy + |> equal class_typ)) + |> mk_list class_typ + end + end fun symbex_attr_access0 ctxt proj_term term = let @@ -1393,7 +1409,9 @@ end) ([(\<^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)] + ISA_core.ML_isa_check_trace_attribute, ISA_core.ML_isa_elaborate_trace_attribute) + , (\<^const_name>\Isabelle_DOF_instances_of\, + ISA_core.check_instance_of, ISA_core.elaborate_instances_of)] |> fold (fn (n, check, elaborate) => fn thy => let val ns = Sign.consts_of thy |> Consts.space_of val name = n @@ -1877,7 +1895,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi else NONE val value_terms = if default_cid then let - val undefined_value = Free ("Undefined_Value", \<^Type>\unit\) + val undefined_value = Free (oid ^ "_Undefined_Value", \<^Type>\unit\) in (undefined_value, undefined_value) end (* Handle initialization of docitem without a class associated, for example when you just want a document element to be referentiable @@ -3097,7 +3115,13 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy = let val bind_pos = Binding.pos_of binding - val name = Binding.name_of binding + val name = + let val name = Binding.name_of binding + in case name |> Option.filter (not o equal DOF_core.default_cid) of + NONE => bind_pos |> ISA_core.err (name + ^ ": This name is reserved by the implementation") + | SOME name => name + end 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; @@ -3163,7 +3187,6 @@ fun add_doc_class_cmd overloaded (raw_params, binding) because the class name is already bound to "doc_class Regular_Exp.rexp" constant by add_doc_class_cmd function *) |> (fn thy => ISA_core.declare_ISA_class_accessor_and_check_instance (params', cid thy, bind_pos) thy) - |> (fn thy => ISA_core.declare_class_instances_annotation (params', cid thy, bind_pos) thy) end; diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy index 27d3313..583601c 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -1019,6 +1019,38 @@ schemata: section*["sec_advanced"::technical]\Advanced ODL Concepts\ +(*<*) +doc_class title = + short_title :: "string option" <= "None" +doc_class author = + email :: "string" <= "''''" +datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 +doc_class abstract = + keywordlist :: "string list" <= "[]" + safety_level :: "classification" <= "SIL3" +doc_class text_section = + authored_by :: "author set" <= "{}" + level :: "int option" <= "None" +type_synonym notion = string +doc_class introduction = text_section + + authored_by :: "author set" <= "UNIV" + uses :: "notion set" +doc_class claim = introduction + + based_on :: "notion list" +doc_class technical = text_section + + formal_results :: "thm list" +doc_class "definition" = technical + + is_formal :: "bool" + property :: "term list" <= "[]" +datatype kind = expert_opinion | argument | "proof" +doc_class result = technical + + evidence :: kind + property :: "thm list" <= "[]" +doc_class example = technical + + referring_to :: "(notion + definition) set" <= "{}" +doc_class "conclusion" = text_section + + establish :: "(claim \ result) set" +(*>*) subsection*["sec_example"::technical]\Example\ text\We assume in this section the following local ontology: @@ -1301,6 +1333,12 @@ text\ (See @{technical "sec_low_level_inv"} for an example). \ +(*<*) +value*\map (result.property) @{instances_of \result\}\ +value*\map (text_section.authored_by) @{instances_of \introduction\}\ +value*\filter (\\. result.evidence \ = proof) @{instances_of \result\}\ +value*\filter (\\. the (text_section.level \) > 1) @{instances_of \introduction\}\ +(*>*) subsection*["sec_queries_on_instances"::technical]\Queries On Instances\ @@ -1315,19 +1353,18 @@ text\ or to get the list of the authors of the instances of \introduction\, it suffices to treat this meta-data as usual: @{theory_text [display,indent=5, margin=70] \ -value*\map (result.property) @{result_instances}\ -value*\map (text_section.authored_by) @{introduction_instances}\ +value*\map (result.property) @{instances_of \result\}\ +value*\map (text_section.authored_by) @{instances_of \introduction\}\ \} In order to get the list of the instances of the class \myresult\ whose \evidence\ is a \proof\, one can use the command: @{theory_text [display,indent=5, margin=70] \ -value*\filter (\\. result.evidence \ = proof) @{result_instances}\ +value*\filter (\\. result.evidence \ = proof) @{instances_of \result\}\ \} The list of the instances of the class \introduction\ whose \level\ > 1, can be filtered by: @{theory_text [display,indent=5, margin=70] \ -value*\filter (\\. the (text_section.level \) > 1) - @{introduction_instances}\ +value*\filter (\\. the (text_section.level \) > 1) @{instances_of \introduction\}\ \} \