From b364880bfc86b356aa805eb688f6f93cfa8f09c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 21 Feb 2023 17:38:45 +0100 Subject: [PATCH] Polymorphic classes first draft --- Isabelle_DOF-Example-I/IsaDofApplications.thy | 4 +- Isabelle_DOF-Example-II/paper.thy | 38 +- .../Conceptual/Conceptual.thy | 2 +- Isabelle_DOF-Unit-Tests/Attributes.thy | 2 +- .../Concept_OntoReferencing.thy | 4 +- .../Concept_TermAntiquotations.thy | 12 +- .../Concept_TermEvaluation.thy | 10 +- Isabelle_DOF-Unit-Tests/ROOT | 1 + Isabelle_DOF-Unit-Tests/TestKit.thy | 49 +- .../Test_Polymorphic_Classes.thy | 682 ++++++++++++++++++ .../scholarly_paper/scholarly_paper.thy | 22 +- Isabelle_DOF/thys/Isa_DOF.thy | 678 +++++++++-------- Isabelle_DOF/thys/manual/M_04_RefMan.thy | 2 +- 13 files changed, 1168 insertions(+), 338 deletions(-) create mode 100644 Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index cde82e9..098ebc7 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -184,7 +184,7 @@ scenarios from the point of view of the ontology modeling. In @{text_section (un we discuss the user-interaction generated from the ontological definitions. Finally, we draw conclusions and discuss related work in @{text_section (unchecked) \conclusion\}. \ -section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"] +section*[bgrnd::text_section,main_author="Some(@{author ''bu''}::author)"] \ Background: The Isabelle System \ text*[background::introduction, level="Some 1"]\ While Isabelle is widely perceived as an interactive theorem prover for HOL @@ -246,7 +246,7 @@ can be type-checked before being displayed and can be used for calculations befo typeset. When editing, Isabelle's PIDE offers auto-completion and error-messages while typing the above \<^emph>\semi-formal\ content.\ -section*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]\ \<^isadof> \ +section*[isadof::technical,main_author="Some(@{author ''adb''}::author)"]\ \<^isadof> \ text\ An \<^isadof> document consists of three components: \<^item> the \<^emph>\ontology definition\ which is an Isabelle theory file with definitions diff --git a/Isabelle_DOF-Example-II/paper.thy b/Isabelle_DOF-Example-II/paper.thy index e54b5f2..9d25e96 100644 --- a/Isabelle_DOF-Example-II/paper.thy +++ b/Isabelle_DOF-Example-II/paper.thy @@ -54,7 +54,7 @@ abstract*[abs, keywordlist="[\Shallow Embedding\,\Process-Alg If you consider citing this paper, please refer to @{cite "HOL-CSP-iFM2020"}. \ text\\ -section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\ Introduction \ +section*[introheader::introduction,main_author="Some(@{author ''bu''}::author)"]\ Introduction \ text*[introtext::introduction, level="Some 1"]\ Communicating Sequential Processes (\<^csp>) is a language to specify and verify patterns of interaction of concurrent systems. Together with CCS and LOTOS, it belongs to the family of @@ -126,10 +126,10 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc omitted.\}. \ -section*["pre"::tc,main_author="Some(@{author \bu\}::author)"] +section*["pre"::technical,main_author="Some(@{author \bu\}::author)"] \Preliminaries\ -subsection*[cspsemantics::tc, main_author="Some(@{author ''bu''})"]\Denotational \<^csp> Semantics\ +subsection*[cspsemantics::technical, main_author="Some(@{author ''bu''})"]\Denotational \<^csp> Semantics\ text\ The denotational semantics (following @{cite "roscoe:csp:1998"}) comes in three layers: the \<^emph>\trace model\, the \<^emph>\(stable) failures model\ and the \<^emph>\failure/divergence model\. @@ -189,7 +189,7 @@ of @{cite "IsobeRoggenbach2010"} is restricted to a variant of the failures mode \ -subsection*["isabelleHol"::tc, main_author="Some(@{author ''bu''})"]\Isabelle/HOL\ +subsection*["isabelleHol"::technical, main_author="Some(@{author ''bu''})"]\Isabelle/HOL\ text\ Nowadays, Isabelle/HOL is one of the major interactive theory development environments @{cite "nipkow.ea:isabelle:2002"}. HOL stands for Higher-Order Logic, a logic based on simply-typed \\\-calculus extended by parametric polymorphism and Haskell-like type-classes. @@ -218,10 +218,10 @@ domain theory for a particular type-class \\::pcpo\, \<^ie> fixed-point induction and other (automated) proof infrastructure. Isabelle's type-inference can automatically infer, for example, that if \\::pcpo\, then \(\ \ \)::pcpo\. \ -section*["csphol"::tc,main_author="Some(@{author ''bu''}::author)", level="Some 2"] +section*["csphol"::technical,main_author="Some(@{author ''bu''}::author)", level="Some 2"] \Formalising Denotational \<^csp> Semantics in HOL \ -subsection*["processinv"::tc, main_author="Some(@{author ''bu''})"] +subsection*["processinv"::technical, main_author="Some(@{author ''bu''})"] \Process Invariant and Process Type\ text\ First, we need a slight revision of the concept of \<^emph>\trace\: if \\\ is the type of the atomic events (represented by a type variable), then @@ -272,7 +272,7 @@ but this can be constructed in a straight-forward manner. Suitable definitions f \\\, \\\ and \\\ lifting \fst\ and \snd\ on the new \'\ process\-type allows to derive the above properties for any \P::'\ process\. \ -subsection*["operator"::tc, main_author="Some(@{author ''lina''})"] +subsection*["operator"::technical, main_author="Some(@{author ''lina''})"] \\<^csp> Operators over the Process Type\ text\ Now, the operators of \<^csp> \Skip\, \Stop\, \_\_\, \_\_\, \_\_\,\_\_\_\ etc. for internal choice, external choice, prefix and parallel composition, can @@ -297,7 +297,7 @@ The definitional presentation of the \<^csp> process operators according to @{ci follows always this scheme. This part of the theory comprises around 2000 loc. \ -subsection*["orderings"::tc, main_author="Some(@{author ''bu''})"] +subsection*["orderings"::technical, main_author="Some(@{author ''bu''})"] \Refinement Orderings\ text\ \<^csp> is centered around the idea of process refinement; many critical properties, @@ -327,7 +327,7 @@ states, from which no internal progress is possible. \ -subsection*["fixpoint"::tc, main_author="Some(@{author ''lina''})"] +subsection*["fixpoint"::technical, main_author="Some(@{author ''lina''})"] \Process Ordering and HOLCF\ text\ For any denotational semantics, the fixed point theory giving semantics to systems of recursive equations is considered as keystone. Its prerequisite is a complete partial ordering @@ -394,7 +394,7 @@ Fixed-point inductions are the main proof weapon in verifications, together with and the \<^csp> laws. Denotational arguments can be hidden as they are not needed in practical verifications. \ -subsection*["law"::tc, main_author="Some(@{author ''lina''})"] +subsection*["law"::technical, main_author="Some(@{author ''lina''})"] \\<^csp> Rules: Improved Proofs and New Results\ @@ -436,11 +436,11 @@ cases to be considered as well as their complexity makes pen and paper proofs practically infeasible. \ -section*["newResults"::tc,main_author="Some(@{author ''safouan''}::author)", +section*["newResults"::technical,main_author="Some(@{author ''safouan''}::author)", main_author="Some(@{author ''lina''}::author)", level= "Some 3"] \Theoretical Results on Refinement\ text\\ -subsection*["adm"::tc,main_author="Some(@{author ''safouan''}::author)", +subsection*["adm"::technical,main_author="Some(@{author ''safouan''}::author)", main_author="Some(@{author ''lina''}::author)"] \Decomposition Rules\ text\ @@ -476,7 +476,7 @@ The failure and divergence projections of this operator are also interdependent, sequence operator. Hence, this operator is not monotonic with \\\<^sub>\\, \\\<^sub>\\ and \\\<^sub>\\, but monotonic when their combinations are considered. \ -subsection*["processes"::tc,main_author="Some(@{author ''safouan''}::author)", +subsection*["processes"::technical,main_author="Some(@{author ''safouan''}::author)", main_author="Some(@{author ''lina''}::author)"] \Reference Processes and their Properties\ text\ @@ -597,7 +597,7 @@ then it may still be livelock-free. % This makes sense since livelocks are worse \ -section*["advanced"::tc,main_author="Some(@{author ''safouan''}::author)",level="Some 3"] +section*["advanced"::technical,main_author="Some(@{author ''safouan''}::author)",level="Some 3"] \Advanced Verification Techniques\ text\ @@ -612,7 +612,7 @@ verification. In the latter case, we present an approach to a verification of a architecture, in this case a ring-structure of arbitrary size. \ -subsection*["illustration"::tc,main_author="Some(@{author ''safouan''}::author)", level="Some 3"] +subsection*["illustration"::technical,main_author="Some(@{author ''safouan''}::author)", level="Some 3"] \The General CopyBuffer Example\ text\ We consider the paradigmatic copy buffer example @{cite "Hoare:1985:CSP:3921" and "Roscoe:UCS:2010"} @@ -677,7 +677,7 @@ corollary deadlock_free COPY \ -subsection*["inductions"::tc,main_author="Some(@{author ''safouan''}::author)"] +subsection*["inductions"::technical,main_author="Some(@{author ''safouan''}::author)"] \New Fixed-Point Inductions\ text\ @@ -727,7 +727,7 @@ The astute reader may notice here that if the induction step is weakened (having the base steps require enforcement. \ -subsection*["norm"::tc,main_author="Some(@{author ''safouan''}::author)"] +subsection*["norm"::technical,main_author="Some(@{author ''safouan''}::author)"] \Normalization\ text\ Our framework can reason not only over infinite alphabets, but also over processes parameterized @@ -787,7 +787,7 @@ Summing up, our method consists of four stages: \ -subsection*["dining_philosophers"::tc,main_author="Some(@{author ''safouan''}::author)",level="Some 3"] +subsection*["dining_philosophers"::technical,main_author="Some(@{author ''safouan''}::author)",level="Some 3"] \Generalized Dining Philosophers\ text\ The dining philosophers problem is another paradigmatic example in the \<^csp> literature @@ -879,7 +879,7 @@ for a dozen of philosophers (on a usual machine) due to the exponential combinat Furthermore, our proof is fairly stable against modifications like adding non synchronized events like thinking or sitting down in contrast to model-checking techniques. \ -section*["relatedwork"::tc,main_author="Some(@{author ''lina''}::author)",level="Some 3"] +section*["relatedwork"::technical,main_author="Some(@{author ''lina''}::author)",level="Some 3"] \Related work\ text\ diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index 75bb658..c3ed081 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -131,7 +131,7 @@ type_synonym XX = B section\Examples of inheritance \ -doc_class C = XX + +doc_class C = B + z :: "A option" <= None (* A LINK, i.e. an attribute that has a type referring to a document class. Mathematical relations over document items can be modeled. *) diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index 2dab8f1..14ba9f3 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -160,7 +160,7 @@ ML\ @{docitem_attribute a2::omega}; type_synonym ALFACENTAURI = E -update_instance*[omega::ALFACENTAURI, x+="''inition''"] +update_instance*[omega::E, x+="''inition''"] ML\ val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \ diff --git a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy index 16ab498..6d3ad8c 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy @@ -144,8 +144,8 @@ update_instance*[f::F,r:="[@{thm ''Concept_OntoReferencing.some_proof''}]"] text\ ..., mauris amet, id elit aliquam aptent id, ... @{docitem \a\} \ (*>*) text\Here we add and maintain a link that is actually modeled as m-to-n relation ...\ -update_instance*[f::F,b:="{(@{docitem \a\}::A,@{docitem \c1\}::C), - (@{docitem \a\}, @{docitem \c2\})}"] +update_instance*[f::F,b:="{(@{A \a\}::A,@{C \c1\}::C), + (@{A \a\}, @{C \c2\})}"] section\Closing the Monitor and testing the Results.\ diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermAntiquotations.thy b/Isabelle_DOF-Unit-Tests/Concept_TermAntiquotations.thy index 2f1933f..ebd64c3 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_TermAntiquotations.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_TermAntiquotations.thy @@ -116,20 +116,22 @@ section\Putting everything together\ text\Major sample: test-item of doc-class \F\ with a relational link between class instances, and links to formal Isabelle items like \typ\, \term\ and \thm\. \ +declare[[ML_print_depth = 10000]] text*[xcv4::F, r="[@{thm ''HOL.refl''}, @{thm \Concept_TermAntiquotations.local_sample_lemma\}]", (* long names required *) - b="{(@{docitem ''xcv1''},@{docitem \xcv2\})}", (* notations \...\ vs. ''...'' *) + b="{(@{A ''xcv1''},@{C \xcv2\})}", (* notations \...\ vs. ''...'' *) s="[@{typ \int list\}]", properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*) ]\Lorem ipsum ...\ - +declare[[ML_print_depth = 20]] text*[xcv5::G, g="@{thm \HOL.sym\}"]\Lorem ipsum ...\ text\... and here we add a relation between @{docitem \xcv3\} and @{docitem \xcv2\} into the relation \verb+b+ of @{docitem \xcv5\}. Note that in the link-relation, -a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is legal in -\verb+Isa_DOF+ because of the sub-class relation between those classes: \ -update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"] +a @{typ "C"}-type is required, so if a @{typ "G"}-type is offered, it is considered illegal +in \verb+Isa_DOF+ despite the sub-class relation between those classes: \ +update_instance-assert-error[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"] +\Type unification failed\ text\And here is the results of some ML-term antiquotations:\ ML\ @{docitem_attribute b::xcv4} \ diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy index c23203b..17e8b9d 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy @@ -187,7 +187,7 @@ to update the instance @{docitem \xcv4\}: \ update_instance-assert-error[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"] - \type of attribute: Conceptual.F.b does not fit to term\ + \Type unification failed: Clash of types\ section\\<^theory_text>\assert*\-Annotated assertion-commands\ @@ -225,11 +225,11 @@ 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 after the meta arguments:\ -value* [optional_test_A::A, x=6] [nbe] \filter (\\. A.x \ > 5) @{A_instances}\ +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}\ -assert* [resultProof3::result, evidence = "proof", property="[@{thm \HOL.sym\}]"] [nbe] - \evidence @{result \resultProof3\} = evidence @{result \resultProof2\}\ +assert* [nbe] [resultProof3::result, evidence = "proof", property="[@{thm \HOL.sym\}]"] + \evidence @{result \resultProof3\} = evidence @{result \resultProof2\}\ text\ The evaluation of @{command "assert*"} can be disabled diff --git a/Isabelle_DOF-Unit-Tests/ROOT b/Isabelle_DOF-Unit-Tests/ROOT index 9fb9052..78d731e 100644 --- a/Isabelle_DOF-Unit-Tests/ROOT +++ b/Isabelle_DOF-Unit-Tests/ROOT @@ -16,6 +16,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" + "Cenelec_Test" "OutOfOrderPresntn" "COL_Test" + "Test_Polymorphic_Classes" document_files "root.bib" "figures/A.png" diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index fa8d468..16c1c90 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -23,6 +23,8 @@ keywords "text-" "text-latex" :: document_body and "update_instance-assert-error" :: document_body and "declare_reference-assert-error" :: document_body and "value-assert-error" :: document_body + and "definition-assert-error" :: document_body + and "doc_class-assert-error" :: document_body begin @@ -152,20 +154,55 @@ val _ = val _ = - let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) trans = - (Value_Command.value_cmd {assert=false} args name modes t @{here} trans - handle ERROR msg => (if error_match src msg - then (writeln ("Correct error: "^msg^": reported.");trans) - else error"Wrong error reported")) + let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) trans = + let val pos = Toplevel.pos_of trans + in trans |> Toplevel.theory + (fn thy => Value_Command.value_cmd {assert=false} args name modes t pos thy + handle ERROR msg => (if error_match src msg + then (writeln ("Correct error: "^msg^": reported."); thy) + else error"Wrong error reported")) + end in Outer_Syntax.command \<^command_keyword>\value-assert-error\ "evaluate and print term" (ODL_Meta_Args_Parser.opt_attributes -- (Value_Command.opt_evaluator -- Value_Command.opt_modes -- Parse.term -- Parse.document_source) - >> (Toplevel.theory o pass_trans_to_value_cmd)) + >> (pass_trans_to_value_cmd)) end; +val _ = + let fun definition_cmd' meta_args_opt decl params prems spec src bool ctxt = + Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) ctxt + |> (fn ctxt => Definition_Star_Command.definition_cmd decl params prems spec bool ctxt + handle ERROR msg => if error_match src msg + then (writeln ("Correct error: "^msg^": reported.") + ; pair "Bound 0" @{thm refl} + |> pair (Bound 0) + |> rpair ctxt) + else error"Wrong error reported") + in + Outer_Syntax.local_theory' \<^command_keyword>\definition-assert-error\ "constant definition" + (ODL_Meta_Args_Parser.opt_attributes -- + (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- + Parse_Spec.if_assumes -- Parse.for_fixes -- Parse.document_source) + >> (fn (meta_args_opt, ((((decl, spec), prems), params), src)) => + #2 oo definition_cmd' meta_args_opt decl params prems spec src)) + end; + + +val _ = + let fun add_doc_class_cmd' ((((overloaded, hdr), (parent, attrs)),((rejects,accept_rex),invars)), src) = + (fn thy => OntoParser.add_doc_class_cmd {overloaded = overloaded} hdr parent attrs rejects accept_rex invars thy + handle ERROR msg => (if error_match src msg + then (writeln ("Correct error: "^msg^": reported."); thy) + else error"Wrong error reported")) + in + Outer_Syntax.command \<^command_keyword>\doc_class-assert-error\ + "define document class" + ((OntoParser.parse_doc_class -- Parse.document_source) + >> (Toplevel.theory o add_doc_class_cmd')) + end val _ = Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)" diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy new file mode 100644 index 0000000..6791f38 --- /dev/null +++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy @@ -0,0 +1,682 @@ +theory Test_Polymorphic_Classes + imports Isabelle_DOF.Isa_DOF + TestKit +begin + +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" + +doc_class ('a::one, 'b, 'c) test0 = text_section + + testa :: "'a list" + testb :: "'b list" + testc :: "'c list" + +typ\('a, 'b, 'c) test0\ +typ\('a, 'b, 'c, 'd) test0_scheme\ + +find_consts name:"test0" +find_theorems name:"test0" + + +doc_class 'a test1 = text_section + + test1 :: "'a list" + invariant author_finite_test :: "finite (authored_by \)" + invariant force_level_test :: "(level \) \ None \ the (level \) > 1" + +find_consts name:"test1*inv" +find_theorems name:"test1*inv" + +text*[church::Author, email="\b\"]\\ +text\@{Author "church"}\ +value*\@{Author \church\}\ + +text\\<^value_>\@{Author \church\}\\ + +doc_class ('a, 'b) test2 = "'a test1" + + test2 :: "'b list" +type_synonym ('a, 'b) test2_syn = "('a, 'b) test2" + +find_theorems name:"test2" + +declare [[invariants_checking_with_tactics]] +text*[testtest::"('a, int) test2", level = "Some 2", authored_by = "{@{Author \church\}}", test2 = "[1]"]\\ +value*\test2 @{test2 \testtest\}\ + +text*[testtest2''::"(nat, int) test2", test1 = "[2::nat, 3]", test2 = "[4::int, 5]", level = "Some (2::int)"]\\ +value*\test1 @{test2 \testtest2''\}\ +declare [[invariants_checking_with_tactics = false]] + +ML\ +val t = Syntax.parse_term \<^context> "@{test2 \testtest\}" + +\ +ML\ +val t = \<^term>\test2.make 8142730 Test_Parametric_Classes_2_test2_authored_by_Attribute_Not_Initialized Test_Parametric_Classes_2_test2_level_Attribute_Not_Initialized Test_Parametric_Classes_2_test2_test1_Attribute_Not_Initialized + Test_Parametric_Classes_2_test2_test2_Attribute_Not_Initialized + \authored_by := bot, level := None\ \ +\ + +text\test2 = "[1::'a::one]" should be test2 = "[1::int]" because the type of testtest4 is ('a::one, int) test2:\ +text-assert-error[testtest4::"('a::one, int) test2", level = "Some 2", authored_by = "{@{Author \church\}}", test2 = "[1::'a::one]"]\\ + \Type unification failed\ +text\Indeed this definition fails:\ +definition-assert-error testtest2::"('a::one, int) test2" where "testtest2 \ + test2.make 11953346 + {@{Author \church\}} + (Some 2) + [] + [] + \authored_by := bot + , level := None, level := Some 2 + , authored_by := insert \Author.tag_attribute = 11953164, email = []\ bot + , test2.test2 := [1::('a::one)]\ " +\Type unification failed\ + +text\For now, no more support of type synonyms as parent:\ +doc_class ('a, 'b, 'c) A = +a :: "'a list" +b :: "'b list" +c :: "'c list" +type_synonym ('a, 'b, 'c) A_syn = "('a, 'b, 'c) A" + +doc_class-assert-error ('a, 'b, 'c, 'd) B = "('b, 'c, 'd) A_syn" + +d ::"'a::one list" <= "[1]" +\Undefined onto class: "A_syn"\ + + +declare[[invariants_checking_with_tactics]] + +definition* testauthor0 where "testauthor0 \ \Author.tag_attribute = 5, email = \test_author_email\\" +definition* testauthor :: "Author" where "testauthor \ \Author.tag_attribute = 5, email = \test_author_email\\" +definition* testauthor2 :: "Author" where "testauthor2 \ \Author.tag_attribute = 5, email = \test_author_email\\ \email := \test_author_email_2\ \" +definition* testauthor3 :: "Author" where "testauthor3 \ testauthor \email := \test_author_email_2\ \" + +ML\ +val ctxt = \<^context> +val input0 = Syntax.read_input "@{Author \church\}" +val source = Syntax.read_input "\<^term_>\@{Author \church\}\" +val input = source +val tt = Document_Output.output_document ctxt {markdown = false} input +\ + +doc_class ('a, 'b) elaborate1 = +a :: "'a list" +b :: "'b list" + +doc_class ('a, 'b) elaborate2 = +c :: "('a, 'b) elaborate1 list" + +doc_class ('a, 'b) elaborate3 = +d :: "('a, 'b) elaborate2 list" + +text*[test_elaborate1::"('a::one, 'b) elaborate1", a = "[1]"]\\ + +term*\@{elaborate1 \test_elaborate1\}\ +value* [nbe]\@{elaborate1 \test_elaborate1\}\ + + +text*[test_elaborate2::"('a::one, 'b) elaborate2", c = "[@{elaborate1 \test_elaborate1\}]"]\\ + +text*[test_elaborate3::"('a::one, 'b) elaborate3", d = "[@{elaborate2 \test_elaborate2\}]"]\\ + +term*\(concat o concat) ((map o map) a (map c (elaborate3.d @{elaborate3 \test_elaborate3\})))\ +value*\(concat o concat) ((map o map) a (map c (elaborate3.d @{elaborate3 \test_elaborate3\})))\ + + +text\ +The term antiquotation is considered a ground term. +Then its type here is \<^typ>\'a::one list\ whith \'a\ a fixed-type variable. +So the following definition only works because the parameter of the class is also \'a\.\ +declare[[ML_print_depth = 10000]] +doc_class 'a elaborate4 = +d :: "'a::one list" <= "(concat o concat) ((map o map) a (map c (elaborate3.d @{elaborate3 \test_elaborate3\})))" +declare[[ML_print_depth = 20]] + +declare[[ML_print_depth = 10000]] +text*[test_elaborate4::"'a::one elaborate4"]\\ +declare[[ML_print_depth = 20]] + + +text\Bug: +As the term antiquotation is considered as a ground term, +its type \<^typ>\'a::one list\ conflicts with the type of the attribute \<^typ>\int list\. +To support the instantiataion of the term antiquatation as an \<^typ>\int list\, +the term antiquatation should have the same behavior as a constant definition, +which is not the case for now.\ +declare[[ML_print_depth = 10000]] +doc_class-assert-error elaborate4' = +d :: "int list" <= "(concat o concat) ((map o map) a (map c (elaborate3.d @{elaborate3 \test_elaborate3\})))" +\Type unification failed\ +declare[[ML_print_depth = 20]] + +text\The behavior we want to support: \ + +definition one_list :: "'a::one list" where "one_list \ [1]" + +text\the constant \<^const>\one_list\ can be instantiate as an \<^typ>\int list\:\ +doc_class elaborate4'' = +d :: "int list" <= "one_list" + +declare[[ML_print_depth = 10000]] +text*[test_elaborate4''::"elaborate4''"]\\ +declare[[ML_print_depth = 20]] + + +term*\concat (map a (elaborate2.c @{elaborate2 \test_elaborate2\}))\ +value*\concat (map a (elaborate2.c @{elaborate2 \test_elaborate2\}))\ + +text\ +The term antiquotation is considered a ground term. +Then its type here is \<^typ>\'a::one list\ whith \'a\ a fixed-type variable. +So the following definition only works because the parameter of the class is also \'a\.\ +declare[[ML_print_depth = 10000]] +doc_class 'a elaborate5 = +d :: "'a::one list" <= "concat (map a (elaborate2.c @{elaborate2 \test_elaborate2\}))" +declare[[ML_print_depth = 20]] + +text\Bug: But when defining an instance, as we use a \'b\ variable to specify the type +of the instance (\<^typ>\'b::one elaborate5\, then the unification fails\ +declare[[ML_print_depth = 10000]] +text-assert-error[test_elaborate5::"'b::one elaborate5"]\\ +\Inconsistent sort constraints for type variable "'b"\ +declare[[ML_print_depth = 20]] + +text\Bug: +The term antiquotation is considered a ground term. +Then its type here is \<^typ>\'a::one list\ whith \'a\ a fixed-type variable. +So it is not compatible with the type of the attribute \<^typ>\'a::numeral list\\ +doc_class-assert-error 'a elaborate5' = +d :: "'a::numeral list" <= "concat (map a (elaborate2.c @{elaborate2 \test_elaborate2\}))" +\Sort constraint\ + +text\The behavior we want to support: \ + +text\the constant \<^const>\one_list\ can be instantiate as an \<^typ>\'a::numeral list\:\ +doc_class 'a elaborate5'' = +d :: "'a::numeral list" <= "one_list" + + +text*[test_elaborate1a::"('a::one, int) elaborate1", a = "[1]", b = "[2]"]\\ + +term*\@{elaborate1 \test_elaborate1a\}\ +value* [nbe]\@{elaborate1 \test_elaborate1a\}\ + +text*[test_elaborate2a::"('a::one, int) elaborate2", c = "[@{elaborate1 \test_elaborate1a\}]"]\\ + +text*[test_elaborate3a::"('a::one, int) elaborate3", d = "[@{elaborate2 \test_elaborate2a\}]"]\\ + +text\ +The term antiquotation is considered a ground term. +Then its type here is \<^typ>\'a::one list\ whith \'a\ a fixed-type variable. +So the following definition only works because the parameter of the class is also \'a\.\ +definition* test_elaborate3_embedding ::"'a::one list" + where "test_elaborate3_embedding \ (concat o concat) ((map o map) elaborate1.a (map elaborate2.c (elaborate3.d @{elaborate3 \test_elaborate3a\})))" + +text\Bug: +The term antiquotation is considered a ground term. +Then its type here is \<^typ>\'a::one list\ whith \'a\ a fixed-type variable. +So it is not compatible with the specified type of the definition \<^typ>\int list\:\ +definition-assert-error test_elaborate3_embedding'::"int list" + where "test_elaborate3_embedding' \ (concat o concat) ((map o map) elaborate1.a (map elaborate2.c (elaborate3.d @{elaborate3 \test_elaborate3a\})))" +\Type unification failed\ + +term*\@{elaborate1 \test_elaborate1a\}\ +value* [nbe]\@{elaborate1 \test_elaborate1a\}\ + + +record ('a, 'b) elaborate1' = +a :: "'a list" +b :: "'b list" + +record ('a, 'b) elaborate2' = +c :: "('a, 'b) elaborate1' list" + +record ('a, 'b) elaborate3' = +d :: "('a, 'b) elaborate2' list" + +doc_class 'a one = +a::"'a list" + +text*[test_one::"'a::one one", a = "[1]"]\\ + +value* [nbe] \@{one \test_one\}\ + +term*\a @{one \test_one\}\ + +text\Bug: +The term antiquotation is considered a ground term. +Then its type here is \<^typ>\'a::one list\ whith \'a\ a fixed-type variable. +So it is not compatible with the specified type of the definition \<^typ>\('b::one, 'a::numeral) elaborate1'\ +because the term antiquotation can not be instantiate as a \<^typ>\'b::one list\ +and the \'a\ is checked against the \'a::numeral\ instance type parameter:\ +definition-assert-error test_elaborate1'::"('b::one, 'a::numeral) elaborate1'" + where "test_elaborate1' \ \ elaborate1'.a = a @{one \test_one\}, b = [2] \" +\Sort constraint\ + +text\This is the same behavior as the following:\ +definition-assert-error test_elaborate10::"('b::one, 'a::numeral) elaborate1'" + where "test_elaborate10 \ \ elaborate1'.a = [1::'a::one], b = [2] \" +\Sort constraint\ + +definition-assert-error test_elaborate11::"('b::one, 'c::numeral) elaborate1'" + where "test_elaborate11 \ \ elaborate1'.a = [1::'a::one], b = [2] \" +\Type unification failed\ + +text\So this works:\ +definition* test_elaborate1''::"('a::one, 'b::numeral) elaborate1'" + where "test_elaborate1'' \ \ elaborate1'.a = a @{one \test_one\}, b = [2] \" + +term \elaborate1'.a test_elaborate1''\ +value [nbe] \elaborate1'.a test_elaborate1''\ + +text\But if we embed the term antiquotation in a definition, +the type unification works:\ +definition* onedef where "onedef \ @{one \test_one\}" + +definition test_elaborate1'''::"('b::one, 'a::numeral) elaborate1'" + where "test_elaborate1''' \ \ elaborate1'.a = a onedef, b = [2] \" + +value [nbe] \elaborate1'.a test_elaborate1'''\ + + +definition test_elaborate2'::"(int, 'b::numeral) elaborate2'" + where "test_elaborate2' \ \ c = [test_elaborate1''] \" + +definition test_elaborate3'::"(int, 'b::numeral) elaborate3'" + where "test_elaborate3' \ \ d = [test_elaborate2'] \" + + +doc_class 'a test3' = +test3 :: "int" +test3' :: "'a list" + +text*[testtest30::"'a::one test3'", test3'="[1]"]\\ +text-assert-error[testtest30::"'a test3'", test3'="[1]"]\\ +\Type unification failed: Variable\ + +find_consts name:"test3'.test3" +definition testone :: "'a::one test3'" where "testone \ \tag_attribute = 5, test3 = 3, test3' = [1] \" +definition* testtwo :: "'a::one test3'" where "testtwo \ \tag_attribute = 5, test3 = 1, test3' = [1] \\ test3 := 1\" + +text*[testtest3'::"'a test3'", test3 = "1"]\\ + +declare [[show_sorts = false]] +definition* testtest30 :: "'a test3'" where "testtest30 \ \tag_attribute = 12, test3 = 2, test3' = [] \" +update_instance*[testtest3'::"'a test3'", test3 := "2"] + +ML\ +val t = @{value_ [nbe] \test3 @{test3' \testtest3'\}\} +val tt = HOLogic.dest_number t +\ + +text\@{value_ [] [nbe] \test3 @{test3' \testtest3'\}\}\ + +update_instance*[testtest3'::"'a test3'", test3 += "2"] + +ML\ +val t = @{value_ [nbe] \test3 @{test3' \testtest3'\}\} +val tt = HOLogic.dest_number t +\ + +value\test3 \ tag_attribute = 1, test3 = 2, test3' = [2::int, 3] \\ +value\test3 \ tag_attribute = 1, test3 = 2, test3' = [2::int, 3] \\ +find_consts name:"test3'.test3" + +ML\ +val test_value = @{value_ \@{test3' \testtest3'\}\} + +\ +declare [[show_sorts = false]] +update_instance*[testtest3'::"'a test3'", test3 += "3"] +declare [[show_sorts = false]] +value*\test3 @{test3' \testtest3'\}\ +value\test3 \ tag_attribute = 12, test3 = 5, test3' = AAAAAA\\ + +find_consts name:"test3'.test3" + +text*[testtest3''::"int test3'", test3 = "1"]\\ + +update_instance*[testtest3''::"int test3'", test3' += "[3]"] + +value*\test3' @{test3' \testtest3''\}\ + +update_instance*[testtest3''::"int test3'", test3' := "[3]"] + +value*\test3' @{test3' \testtest3''\}\ + +update_instance*[testtest3''::"int test3'", test3' += "[2,5]"] + +value*\test3' @{test3' \testtest3''\}\ + +definition testeq where "testeq \ \x. x" +find_consts name:"test3'.ma" + +text-assert-error[testtest3''::"int test3'", test3 = "1", test3' = "[3::'a::numeral]"]\\ + \Type unification failed\ + +text-assert-error[testtest3''::"int test3'", test3 = "1", test3' = "[3]"]\\ + \Duplicate instance declaration\ + + +declare[[ML_print_depth = 10000]] +definition-assert-error testest3''' :: "int test3'" + where "testest3''' \ \ tag_attribute = 12, test3 = 1, test3' = [2]\\ test3' := [3::'a::numeral]\" +\Type unification failed\ +declare[[ML_print_depth = 20]] + +value* \test3 @{test3' \testtest3''\}\ +value* \\ tag_attribute = 12, test3 = 1, test3' = [2]\\ test3' := [3::int]\\ +value* \test3 (\ tag_attribute = 12, test3 = 1, test3' = [2]\\ test3' := [3::int]\)\ +term*\@{test3' \testtest3''\}\ + +ML\val t = \<^term_>\test3 @{test3' \testtest3''\}\\ + +value\test3 \ tag_attribute = 12, test3 = 2, test3' = [2::int ,3]\\ + +find_consts name:"test3'.test3" +find_consts name:"Isabelle_DOF_doc_class_test3'" +update_instance*[testtest3''::"int test3'", test3 := "2"] +ML\ +val t = @{value_ [nbe] \test3 @{test3' \testtest3''\}\} +val tt = HOLogic.dest_number t |> snd +\ + +doc_class 'a testa = +a:: "'a set" +b:: "int set" + +text*[testtesta::"'a testa", b = "{2}"]\\ +update_instance*[testtesta::"'a testa", b += "{3}"] + +ML\ +val t = @{value_ [nbe] \b @{testa \testtesta\}\} +val tt = HOLogic.dest_set t |> map (HOLogic.dest_number #> snd) +\ + +update_instance-assert-error[testtesta::"'a::numeral testa", a := "{2::'a::numeral}"] +\incompatible classes:'a Test_Polymorphic_Classes.testa:'a::numeral Test_Polymorphic_Classes.testa\ + +text*[testtesta'::"'a::numeral testa", a = "{2}"]\\ + +update_instance*[testtesta'::"'a::numeral testa", a += "{3}"] + +ML\ +val t = @{value_ [nbe] \a @{testa \testtesta'\}\} +\ + +update_instance-assert-error[testtesta'::"'a::numeral testa", a += "{3::int}"] + \Type unification failed\ + +definition-assert-error testtesta'' :: "'a::numeral testa" + where "testtesta'' \ \tag_attribute = 5, a = {1}, b = {1} \\ a := {1::int}\" +\Type unification failed\ + +update_instance*[testtesta'::"'a::numeral testa", b := "{3::int}"] +ML\ +val t = @{value_ [nbe] \b @{testa \testtesta'\}\} +\ + +value* [nbe] \b @{testa \testtesta'\}\ + +definition testtesta'' :: "'a::numeral testa" + where "testtesta'' \ \tag_attribute = 5, a = {1}, b = {1} \\ b := {2::int}\" + +value [nbe]\b testtesta''\ + +doc_class 'a test3 = +test3 :: "'a list" +type_synonym 'a test3_syn = "'a test3" + +text*[testtest3::"int test3", test3 = "[1]"]\\ +update_instance*[testtest3::"int test3", test3 := "[2]"] +ML\ +val t = \<^term_>\test3 @{test3 \testtest3\}\ +val tt = \<^value_>\test3 @{test3 \testtest3\}\ |> HOLogic.dest_list |> map HOLogic.dest_number +\ + +update_instance*[testtest3::"int test3", test3 += "[3]"] +value*\test3 @{test3 \testtest3\}\ + + +doc_class ('a, 'b) test4 = "'a test3" + + test4 :: "'b list" + +definition-assert-error testtest0'::"('a::one, int) test4" where "testtest0' \ + test4.make 11953346 + [] [1::('a::one)]" +\Type unification failed\ + +definition-assert-error testtest0''::"('a, int) test4" where "testtest0'' \ + test4.make 11953346 + [1] Test_Parametric_Classes_2_test4_test4_Attribute_Not_Initialized" +\Type unification failed\ + +text\Must fail because the equivalent definition +\testtest0'\ below fails +due to the constraint in the where [1::('a::one)] is not an \<^typ>\int list\ +but an \<^typ>\'a::one list\ list \ +text-assert-error[testtest0::"('a::one, int) test4", test4 = "[1::'a::one]"]\\ +\Type unification failed\ +update_instance-assert-error[testtest0::"('a::one, int) test4"] + \Undefined instance: "testtest0"\ + +value-assert-error\@{test4 \testtest0\}\\Undefined instance: "testtest0"\ + +definition testtest0''::"('a, int) test4" where "testtest0'' \ + \ tag_attribute = 11953346, test3 = [], test4 = [1]\\test4 := [2]\" + +definition testtest0'''::"('a, int) test4" where "testtest0''' \ + \ tag_attribute = 11953346, test3 = [], test4 = [1]\\test4 := [2]\" + + +value [nbe] \test3 testtest0''\ + +type_synonym notion = string + +doc_class Introduction = text_section + + authored_by :: "Author set" <= "UNIV" + uses :: "notion set" + invariant author_finite :: "finite (authored_by \)" + and force_level :: "(level \) \ None \ the (level \) > 1" + +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" <= "[]" + invariant has_property :: "evidence \ = proof \ property \ \ []" + +doc_class example = technical + + referring_to :: "(notion + definition) set" <= "{}" + +doc_class conclusion = text_section + + establish :: "(claim \ result) set" + invariant establish_defined :: "\ x. x \ Domain (establish \) + \ (\ y \ Range (establish \). (x, y) \ establish \)" + +text\Next we define some instances (docitems): \ + +declare[[invariants_checking_with_tactics = true]] + +text*[church1::Author, email="\church@lambda.org\"]\\ + +text*[resultProof::result, evidence = "proof", property="[@{thm \HOL.refl\}]"]\\ +text*[resultArgument::result, evidence = "argument"]\\ + +text\The invariants \<^theory_text>\author_finite\ and \<^theory_text>\establish_defined\ can not be checked directly + and need a little help. + We can set the \invariants_checking_with_tactics\ theory attribute to help the checking. + It will enable a basic tactic, using unfold and auto:\ + +declare[[invariants_checking_with_tactics = true]] + +text*[curry::Author, email="\curry@lambda.org\"]\\ +text*[introduction2::Introduction, authored_by = "{@{Author \church\}}", level = "Some 2"]\\ +(* When not commented, should violated the invariant: +update_instance*[introduction2::Introduction + , authored_by := "{@{Author \church\}}" + , level := "Some 1"] +*) + +text*[introduction_test_parsed_elaborate::Introduction, authored_by = "authored_by @{Introduction \introduction2\}", level = "Some 2"]\\ +term*\authored_by @{Introduction \introduction_test_parsed_elaborate\}\ +value*\authored_by @{Introduction \introduction_test_parsed_elaborate\}\ +text*[introduction3::Introduction, authored_by = "{@{Author \church\}}", level = "Some 2"]\\ +text*[introduction4::Introduction, authored_by = "{@{Author \curry\}}", level = "Some 4"]\\ + +text*[resultProof2::result, evidence = "proof", property="[@{thm \HOL.sym\}]"]\\ + +text\Then we can evaluate expressions with instances:\ + +term*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction3\}\ +value*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction3\}\ +value*\authored_by @{Introduction \introduction2\} = authored_by @{Introduction \introduction4\}\ + +value*\@{Introduction \introduction2\}\ + +value*\{@{Author \curry\}} = {@{Author \church\}}\ + +term*\property @{result \resultProof\} = property @{result \resultProof2\}\ +value*\property @{result \resultProof\} = property @{result \resultProof2\}\ + +value*\evidence @{result \resultProof\} = evidence @{result \resultProof2\}\ + +declare[[invariants_checking_with_tactics = false]] + +declare[[invariants_strict_checking = false]] + +doc_class test_A = + level :: "int option" + x :: int + +doc_class test_B = + level :: "int option" + x :: "string" (* attributes live in their own name-space *) + y :: "string list" <= "[]" (* and can have arbitrary type constructors *) + (* LaTeX may have problems with this, though *) + +text\We may even use type-synonyms for class synonyms ...\ +type_synonym test_XX = test_B + +doc_class test_C0 = test_B + + z :: "test_A option" <= None (* A LINK, i.e. an attribute that has a type + referring to a document class. Mathematical + relations over document items can be modeled. *) + g :: "thm" (* a reference to the proxy-type 'thm' allowing + + to denote references to theorems inside attributes *) + + +doc_class test_C = test_B + + z :: "test_A option" <= None (* A LINK, i.e. an attribute that has a type + referring to a document class. Mathematical + relations over document items can be modeled. *) + g :: "thm" (* a reference to the proxy-type 'thm' allowing + + to denote references to theorems inside attributes *) + +datatype enum = X1 | X2 | X3 (* we add an enumeration type ... *) + + +doc_class test_D = test_B + + x :: "string" <= "\def \\" (* overriding default *) + a1 :: enum <= "X2" (* class - definitions may be mixed + with arbitrary HOL-commands, thus + also local definitions of enumerations *) + a2 :: int <= 0 + +doc_class test_E = test_D + + x :: "string" <= "''qed''" (* overriding default *) + +doc_class test_G = test_C + + g :: "thm" <= "@{thm \HOL.refl\}" (* warning overriding attribute expected*) + +doc_class 'a test_F = + properties :: "term list" + r :: "thm list" + u :: "file" + s :: "typ list" + b :: "(test_A \ 'a test_C_scheme) set" <= "{}" (* This is a relation link, roughly corresponding + to an association class. It can be used to track + claims to result - relations, for example.*) + b' :: "(test_A \ 'a test_C_scheme) list" <= "[]" + invariant br :: "r \ \ [] \ card(b \) \ 3" + and br':: "r \ \ [] \ length(b' \) \ 3" + and cr :: "properties \ \ []" + +lemma*[l::test_E] local_sample_lemma : + "@{thm \refl\} = @{thm ''refl''}" by simp + \ \un-evaluated references are similar to + uninterpreted constants. Not much is known + about them, but that doesn't mean that we + can't prove some basics over them...\ + +text*[xcv1::test_A, x=5]\Lorem ipsum ...\ +text*[xcv2::test_C, g="@{thm ''HOL.refl''}"]\Lorem ipsum ...\ +text*[xcv3::test_A, x=7]\Lorem ipsum ...\ + +text\Bug: For now, the implementation is no more compatible with the docitem term-antiquotation:\ +text-assert-error[xcv10::"unit test_F", r="[@{thm ''HOL.refl''}, + @{thm \local_sample_lemma\}]", (* long names required *) + b="{(@{docitem ''xcv1''},@{docitem \xcv2\})}", (* notations \...\ vs. ''...'' *) + s="[@{typ \int list\}]", + properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*) +]\Lorem ipsum ...\\Type unification failed\ + +text*[xcv11::"unit test_F", r="[@{thm ''HOL.refl''}, + @{thm \local_sample_lemma\}]", (* long names required *) + b="{(@{test_A ''xcv1''},@{test_C \xcv2\})}", (* notations \...\ vs. ''...'' *) + s="[@{typ \int list\}]", + properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*) +]\Lorem ipsum ...\ + +value*\b @{test_F \xcv11\}\ + +typ\unit test_F\ + +text*[xcv4::"unit test_F", r="[@{thm ''HOL.refl''}, + @{thm \local_sample_lemma\}]", (* long names required *) + b="{(@{test_A ''xcv1''},@{test_C \xcv2\})}", (* notations \...\ vs. ''...'' *) + s="[@{typ \int list\}]", + properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*) +]\Lorem ipsum ...\ + +value*\b @{test_F \xcv4\}\ + +text*[xcv5::test_G, g="@{thm \HOL.sym\}"]\Lorem ipsum ...\ + +update_instance*[xcv4::"unit test_F", b+="{(@{test_A ''xcv3''},@{test_C ''xcv2''})}"] + +update_instance-assert-error[xcv4::"unit test_F", b+="{(@{test_A ''xcv3''},@{test_G ''xcv5''})}"] + \Type unification failed: Clash of types\ + + + +typ\unit test_G_ext\ +typ\\test_G.tag_attribute :: int\\ +text*[xcv6::"\test_G.tag_attribute :: int\ test_F", b="{(@{test_A ''xcv3''},@{test_G ''xcv5''})}"]\\ + +end \ No newline at end of file diff --git a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy index 732200f..c62d28b 100644 --- a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy +++ b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy @@ -165,11 +165,11 @@ text\The intended use for the \doc_class\es \<^verbatim>\\math_example\ (or \<^verbatim>\math_ex\ for short) are \<^emph>\informal\ descriptions of semi-formal definitions (by inheritance). Math-Examples can be made referentiable triggering explicit, numbered presentations.\ -doc_class math_motivation = tc + +doc_class math_motivation = technical + referentiable :: bool <= False type_synonym math_mtv = math_motivation -doc_class math_explanation = tc + +doc_class math_explanation = technical + referentiable :: bool <= False type_synonym math_exp = math_explanation @@ -207,7 +207,7 @@ datatype math_content_class = text\Instances of the \doc_class\ \<^verbatim>\math_content\ are by definition @{term "semiformal"}; they may be non-referential, but in this case they will not have a @{term "short_name"}.\ -doc_class math_content = tc + +doc_class math_content = technical + referentiable :: bool <= False short_name :: string <= "''''" status :: status <= "semiformal" @@ -516,34 +516,34 @@ subsection\Content in Engineering/Tech Papers \ text\This section is currently experimental and not supported by the documentation generation backend.\ -doc_class engineering_content = tc + +doc_class engineering_content = technical + short_name :: string <= "''''" status :: status type_synonym eng_content = engineering_content -doc_class "experiment" = eng_content + +doc_class "experiment" = engineering_content + tag :: "string" <= "''''" -doc_class "evaluation" = eng_content + +doc_class "evaluation" = engineering_content + tag :: "string" <= "''''" -doc_class "data" = eng_content + +doc_class "data" = engineering_content + tag :: "string" <= "''''" -doc_class tech_definition = eng_content + +doc_class tech_definition = engineering_content + referentiable :: bool <= True tag :: "string" <= "''''" -doc_class tech_code = eng_content + +doc_class tech_code = engineering_content + referentiable :: bool <= True tag :: "string" <= "''''" -doc_class tech_example = eng_content + +doc_class tech_example = engineering_content + referentiable :: bool <= True tag :: "string" <= "''''" -doc_class eng_example = eng_content + +doc_class eng_example = engineering_content + referentiable :: bool <= True tag :: "string" <= "''''" diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 7c4f238..efa7d84 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -93,7 +93,7 @@ structure DOF_core = struct datatype onto_class = Onto_Class of - {params : (string * sort) list, (*currently not used *) + {params : (string * sort) list, name : binding, virtual : {virtual : bool}, inherits_from : (typ list * string) option, (* imports *) @@ -115,33 +115,69 @@ struct val get_onto_classes = Onto_Classes.get o Proof_Context.theory_of + (* Get the Onto_Class object from its short name or long name *) 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 - fun resolve_syn thy name = - name |> Syntax.read_typ_global thy - |> Syntax.string_of_typ_global thy - |> YXML.parse_body |> XML.content_of + fun markup2string s = YXML.content_of s + |> Symbol.explode + |> List.filter (fn c => c <> Symbol.DEL) + |> String.concat - (* takes class synonyms into account *) + fun get_name name = + name |> markup2string + |> Symbol.explode_words |> split_last |> #2 + + (* Get the Onto_Class object. + The function does not use the abstract syntax of an onto_class. + and relies entirely on the associated record created with the onto_class and its type. + The function takes, for the name argument, a string that has the same form as + the input of an ML \<^typ>\\ anti-quotation to get a record type. + To get the type of the record ('a, 'b) A, we'll use \<^typ>\('a, 'b) A\. + So the name argument will be "('a, 'b) A" *) + (* does not take class synonyms into account *) fun get_onto_class_global' name thy = - let val name' = name |> resolve_syn thy + let val name' = name |> get_name in Name_Space.check (Context.Theory thy) (get_onto_classes (Proof_Context.init_global thy)) (name', Position.none) |> #2 end + (* Get the full-qualified name of an onto_class from its short name or long name *) 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 *) + (* Get the full-qualified name of an onto-class. + The function does not use the abstract syntax of an onto_class. + and relies entirely on the associated record created with the onto_class and its type. + The function takes, for the name argument, a string that has the same form as + the input of an ML \<^typ>\\ anti-quotation to get a record type. + To get the type of the record ('a, 'b) A, we'll use \<^typ>\('a, 'b) A\. + So the name argument will be "('a, 'b) A". *) + (* does not take class synonyms into account *) fun get_onto_class_name_global' name thy = - let val name' = name |> resolve_syn thy + let val name' = name |> get_name in Name_Space.check (Context.Theory thy) (get_onto_classes (Proof_Context.init_global thy)) (name', Position.none) |> #1 end + (* Get the full-qualified name of an onto-class, + its string representation with arguments and sorts, and its type + from its short or long name. + To get the type of the record ('a::one, 'b) A, we'll use \<^typ>\('a::one, 'b) A\. + So the name argument will be "('a::one, 'b) A" *) + (* does not takes class synonyms into account *) + fun get_onto_class_cid thy name = + let val cid_typ = name |> Syntax.read_typ_global thy + val (args, name') = name |> Symbol.explode_words |> split_last + val name'' = (name', Position.none) |> Name_Space.check (Context.Theory thy) + (get_onto_classes (Proof_Context.init_global thy)) + |> fst + val args_cid = append args [name''] |> space_implode Symbol.space + in ((name'', args_cid), cid_typ) + end + fun check_onto_class ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_onto_classes ctxt); @@ -198,7 +234,7 @@ struct rejectS , rex, invs) => (params, name, virtual, inherits_from, attribute_decl, rejectS , rex, f invs)) - fun rep_onto_class cid thy = get_onto_class_global' cid thy |> (fn Onto_Class rep => rep) + fun rep_onto_class cid thy = get_onto_class_global cid thy |> (fn Onto_Class rep => rep) fun params_of cid = #params o rep_onto_class cid fun name_of cid = #name o rep_onto_class cid @@ -228,16 +264,18 @@ struct val default_cid = "text" (* the top (default) document class: everything is a text.*) +(* Due to the implementation, is_subclass0 is _NOT_ compatible with DOF classes type synonyms, + so they must be resolved to full class names before use. *) 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) + else get_onto_class_name_global id (Proof_Context.theory_of ctxt) 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'' + (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 @@ -694,9 +732,7 @@ 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 (* takes class synonyms into account *) - val parent' = Option.map (apsnd (fn x => get_onto_class_name_global' x thy)) parent - val rejectS = map (Syntax.read_term_global thy) reject_Atoms; + let 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; val _ = map check_regexps reg_exps @@ -707,7 +743,7 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i |> (fn pos => error("invariant labels must be unique"^ Position.here pos)) else () val invs' = map (apsnd(Syntax.read_term_global thy)) invs - in thy |> add_onto_class binding (make_onto_class (params', binding, virtual, parent', fields + in thy |> add_onto_class binding (make_onto_class (params', binding, virtual, parent, fields , rejectS, reg_exps, invs')) end @@ -739,17 +775,15 @@ fun define_object_global {define = define} ((oid, pos), instance) thy = add_instance binding instance thy end - fun get_attributes_local cid ctxt = if cid = default_cid then [] 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 + case get_onto_class_global cid_long (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)] + | Onto_Class {inherits_from=SOME(_, father), attribute_decl = X, ...} => + get_attributes_local father ctxt @ [(cid_long,X)] end fun get_attributes cid thy = get_attributes_local cid (Proof_Context.init_global thy) @@ -780,8 +814,8 @@ fun get_attribute_info_local (*long*)cid attr ctxt : attributes_info option= typ = ty}) end -fun get_attribute_info (*long*)cid attr thy = - get_attribute_info_local cid attr (Proof_Context.init_global thy) +fun get_attribute_info (*long*)cid attr thy = + get_attribute_info_local cid attr (Proof_Context.init_global thy) fun get_attribute_defaults (* long*)cid thy = let val attrS = flat(map snd (get_attributes cid thy)) @@ -870,6 +904,25 @@ fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy = | T t = t in T term end +(* Elaborate an Isabelle_DOF term-antiquotation from an only parsed-term (not checked) *) +fun parsed_elaborate ctxt pos (Const(s,ty) $ t) = + if is_ISA s + then Syntax.check_term ctxt (Const(s, ty) $ t) + |> (fn t => transduce_term_global {mk_elaboration=true} (t , pos) + (Proof_Context.theory_of ctxt)) + else (Const(s,ty) $ (parsed_elaborate ctxt pos t)) + | parsed_elaborate ctxt pos (t1 $ t2) = parsed_elaborate ctxt pos (t1) $ parsed_elaborate ctxt pos (t2) + | parsed_elaborate ctxt pos (Const(s,ty)) = + if is_ISA s + then Syntax.check_term ctxt (Const(s, ty)) + |> (fn t => transduce_term_global {mk_elaboration=true} (t , pos) + (Proof_Context.theory_of ctxt)) + else Const(s,ty) + | parsed_elaborate ctxt pos (Abs(s,ty,t)) = Abs (s,ty,parsed_elaborate ctxt pos t) + | parsed_elaborate _ _ t = t + +fun elaborate_term' ctxt parsed_term = parsed_elaborate ctxt Position.none parsed_term + fun elaborate_term ctxt term = transduce_term_global {mk_elaboration=true} (term , Position.none) (Proof_Context.theory_of ctxt) @@ -878,6 +931,39 @@ fun check_term ctxt term = transduce_term_global {mk_elaboration=false} (term , Position.none) (Proof_Context.theory_of ctxt) +(* Check an Isabelle_DOF term-antiquotation from an only parsed-term (not checked) *) +fun parsed_check ctxt pos (Const(s,ty) $ t) = + if is_ISA s + then let val _ = Syntax.check_term ctxt (Const(s, ty) $ t) + |> (fn t => transduce_term_global {mk_elaboration=false} (t , pos) + (Proof_Context.theory_of ctxt)) + in (Const(s,ty) $ (parsed_check ctxt pos t)) end + else (Const(s,ty) $ (parsed_check ctxt pos t)) + | parsed_check ctxt pos (t1 $ t2) = parsed_check ctxt pos (t1) $ parsed_check ctxt pos (t2) + | parsed_check ctxt pos (Const(s,ty)) = + if is_ISA s + then let val _ = Syntax.check_term ctxt (Const(s, ty)) + |> (fn t => transduce_term_global {mk_elaboration=false} (t , pos) + (Proof_Context.theory_of ctxt)) + in Const(s,ty) end + else Const(s,ty) + | parsed_check ctxt pos (Abs(s,ty,t)) = Abs (s,ty,parsed_check ctxt pos t) + | parsed_check _ _ t = t + +fun check_term' ctxt parsed_term = parsed_check ctxt Position.none parsed_term + +fun prep_decls prep_var raw_vars ctxt = + let + val (vars, ctxt') = fold_map prep_var raw_vars ctxt; + val (xs, ctxt'') = ctxt' + |> Context_Position.set_visible false + |> Proof_Context.add_fixes vars + ||> Context_Position.restore_visible ctxt'; + val _ = + Context_Position.reports ctxt'' + (map (Binding.pos_of o #1) vars ~~ + map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs); + in ((vars, xs), ctxt'') end; fun print_doc_class_tree ctxt P T = let val classes = Name_Space.dest_table (get_onto_classes ctxt) @@ -1104,12 +1190,13 @@ fun check_instance thy (term, _, pos) s = |> Long_Name.qualify qual fun check thy (name, _) = let - val object_cid = DOF_core.cid_of name thy + 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 else err (name ^ " is not an instance of " ^ class_name) pos - in check' (class_name, object_cid) end; + in check' (class_name, name') end; in ML_isa_check_generic check thy (term, pos) end fun ML_isa_id _ (term,_) = SOME term @@ -1152,12 +1239,11 @@ fun rm_mixfix name mixfix thy = |> Named_Target.theory_map) end -fun elaborate_instance thy _ _ term_option pos = +fun elaborate_instance thy _ _ term_option _ = case term_option of NONE => error ("Malformed term annotation") | SOME term => let val instance_name = HOLogic.dest_string term - val value = DOF_core.value_of instance_name thy - in DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy + in DOF_core.value_of instance_name thy end (* @@ -1165,14 +1251,15 @@ fun elaborate_instance thy _ _ term_option pos = because the class name is already bound to "doc_class Regular_Exp.rexp" constant by add_doc_class_cmd function *) -fun declare_ISA_class_accessor_and_check_instance (doc_class_name, bind_pos) thy = +fun declare_ISA_class_accessor_and_check_instance (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 val bind = bname' |> pair bind_pos |> swap |> Binding.make val bind' = prefix DOF_core.long_doc_class_prefix bname |> pair bind_pos |> swap |> Binding.make - val const_typ = \<^typ>\string\ --> Syntax.read_typ (Proof_Context.init_global thy) doc_class_name + val typ = Type (doc_class_name, map TFree params) + val const_typ = \<^typ>\string\ --> typ fun mixfix_enclose name = name |> enclose "@{" " _}" val mixfix = clean_mixfix bname |> mixfix_enclose val mixfix' = clean_mixfix doc_class_name |> mixfix_enclose @@ -1184,6 +1271,7 @@ fun declare_ISA_class_accessor_and_check_instance (doc_class_name, bind_pos) thy |> Sign.add_consts [(bind', const_typ, Mixfix.mixfix mixfix')] |> DOF_core.add_isa_transformer bind' ((check_instance, elaborate_instance) |> DOF_core.make_isa_transformer) + end fun elaborate_instances_list thy isa_name _ _ _ = @@ -1204,23 +1292,23 @@ fun elaborate_instances_list thy isa_name _ _ _ = in HOLogic.mk_list class_typ values end -fun declare_class_instances_annotation (doc_class_name, bind_pos) thy = +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 class_typ = doc_class_name |> Proof_Context.read_typ (Proof_Context.init_global thy) + 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 class_typ\, Mixfix.mixfix 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 class_typ\, Mixfix.mixfix 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) end @@ -1323,10 +1411,9 @@ ML\ structure ODL_Meta_Args_Parser = struct - -type meta_args_t = (((string * Position.T) * - (string * Position.T) option) - * ((string * Position.T) * string) list) +type meta_args_t = ((string * Position.T) * + (string * Position.T) option) + * ((string * Position.T) * string) list val empty_meta_args = ((("", Position.none), NONE), []) @@ -1373,6 +1460,7 @@ val attributes_upd = (Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," (improper |-- attribute_upd)))) [])) --| Parse.$$$ "]") --| improper + end (* structure ODL_Meta_Args_Parser *) \ @@ -1435,14 +1523,20 @@ fun value_select name ctxt = then default_value ctxt else Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt; -fun value_select' raw_name ctxt = - if raw_name = "" - then (DOF_core.elaborate_term ctxt) #> default_value ctxt - else (DOF_core.elaborate_term ctxt) - #> (let val name = intern_evaluator (Proof_Context.theory_of ctxt) raw_name in - Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt end); +fun value_select' raw_name ctxt raw_t = + let val thy = Proof_Context.theory_of ctxt + val t = Syntax.parse_term ctxt raw_t; + val t' = DOF_core.elaborate_term' ctxt t + val t'' = Syntax.check_term ctxt t' + in + if raw_name = "" + then t'' |> default_value ctxt + else let val name = intern_evaluator thy raw_name + in t'' |> Name_Space.get (Evaluators.get thy) name ctxt + end + end -val value = value_select' "" +val value = value_select "" val value_without_elaboration = value_select "" @@ -1459,13 +1553,12 @@ fun cid_2_cidType cid_long thy = in fold (fn x => fn y => Type(ty_name x,[y])) (fathers cid_long) \<^Type>\unit\ end -fun create_default_object thy class_name = +fun create_default_object thy oid class_name typ = 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) + fun attr_to_s (binding, _, _) = purified_class_name ^ "_" + ^ (Binding.name_of binding) + ^ "_Attribute_Not_Initialized" val class_list = DOF_core.get_attributes class_name thy fun attrs_filter [] = [] | attrs_filter (x::xs) = @@ -1479,44 +1572,51 @@ fun create_default_object thy class_name = 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)) - val tag_attr = HOLogic.mk_number \<^Type>\int\ - fun add_tag_to_attrs_free' tag_attr thy (cid, filtered_attr_list) = + val tag_attr_s = serial () |> string_of_int + fun trans_attr thy trans tag_attr (cid, filtered_attr_list) = if DOF_core.virtual_of cid thy |> #virtual - then (tag_attr (serial ()))::(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' tag_attr thy) class_list') - in list_comb (make_const, (tag_attr (serial()))::class_list'') end + then (tag_attr)::(map (trans) filtered_attr_list) + else (map (trans) filtered_attr_list) + val test_class = class_list' |> map (trans_attr thy (attr_to_s) tag_attr_s) + |> flat + |> cons tag_attr_s + val term = test_class |> cons (Long_Name.qualify class_name makeN) |> space_implode Symbol.space + val ctxt = Proof_Context.init_global thy + val term' = term |> Syntax.parse_term ctxt |> DOF_core.elaborate_term' ctxt + (* rename oid to be compatible with binding naming policy *) + val clean_oid = translate_string (fn ":" => "_" | "-" => "_" | c => c); + val oid' = clean_oid oid + val parsed_prop = Const (\<^const_name>\Pure.eq\, dummyT) $ Free (oid', dummyT) $ term' + val raw_vars = [(Binding.name oid', SOME typ, NoSyn)] + val (_, vars_ctxt) = DOF_core.prep_decls Proof_Context.cert_var raw_vars ctxt + val concl = Syntax.check_prop vars_ctxt parsed_prop + in Logic.dest_equals concl |> snd end -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 {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 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) +fun check_classref {is_monitor=is_monitor} (SOME (cid, pos)) thy = + let + val ctxt = Proof_Context.init_global thy + val name_cid_typ = DOF_core.get_onto_class_cid thy cid + val cid_long = name_cid_typ |> (fst o fst) + val rex = DOF_core.rex_of 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 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 (name_cid_typ, pos) + end + | check_classref _ NONE _ = pair DOF_core.default_cid DOF_core.default_cid + |> rpair \<^typ>\unit\ + |> rpair Position.none - -fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort)); -fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init_global thy) [term]) - - -fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long +fun calc_update_term {mk_elaboration=mk_elaboration} thy (name, typ) (S:(string * Position.T * string * term)list) term = - let val cid_ty = cid_2_cidType cid_long thy + let val cid_long = name + val cid_ty = typ val ctxt = Proof_Context.init_global thy - val generalize_term = Term.map_types (generalize_typ 0) - 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 = let fun get_class_name parent_cid attribute_name pos = @@ -1532,8 +1632,7 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long NONE => ISA_core.err ("Attribute " ^ attribute_name ^ " not defined for class: " ^ cid_long) pos - | SOME (_, parent_name) => - get_class_name parent_name attribute_name pos + | SOME (_, parent_name) => get_class_name parent_name attribute_name pos end val _ = if mk_elaboration then @@ -1544,7 +1643,7 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long 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 + val (ln,lnt,lnu,_) = case info_opt of NONE => error ("unknown attribute >" ^((Long_Name.base_name lhs)) ^"< in class: "^cid_long) @@ -1552,28 +1651,30 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long 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) - handle Type.TYPE_MATCH => (error ("type of attribute: " ^ ln - ^ " does not fit to term: " - ^ toString rhs)); - val tyenv' = (map (fn (s,(t,u)) => ((s,t),u)) (Vartab.dest tyenv)) val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then () else error("illegal notation for attribute of "^cid_long) fun join (ttt as \<^Type>\int\) = \<^Const>\Groups.plus ttt\ - |join (ttt as \<^Type>\set _\) = \<^Const>\Lattices.sup ttt\ - |join \<^Type>\list A\ = \<^Const>\List.append A\ + |join (ttt as \<^Type>\set _\) = \<^Const>\Lattices.sup dummyT\ + |join \<^Type>\list A\ = \<^Const>\List.append dummyT\ |join _ = error("implicit fusion operation not defined for attribute: "^ lhs) (* could be extended to bool, map, multisets, ... *) - val rhs' = instantiate_term tyenv' (generalize_term rhs) - val rhs'' = DOF_core.transduce_term_global {mk_elaboration=mk_elaboration} - (rhs',pos) thy in case opr of - "=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term - | ":=" => Const(lnu,lnut) $ Abs ("uu_", lnt, rhs'') $ term - | "+=" => Const(lnu,lnut) $ Abs ("uu_", lnt, join lnt $ (Bound 0) $ rhs'') $ term + "=" => Const(lnu, dummyT) $ Abs ("uu_", dummyT, rhs) $ term + | ":=" => Const(lnu, dummyT) $ Abs ("uu_", dummyT, rhs) $ term + | "+=" => Const(lnu, dummyT) $ Abs ("uu_u", dummyT, join lnt $ (Bound 0) $ rhs) $ term | _ => error "corrupted syntax - oops - this should not occur" - end - in Sign.certify_term thy (fold read_assn S term) end + end + val t = fold read_assn S term + val t' = if mk_elaboration + then DOF_core.elaborate_term' ctxt t + else DOF_core.check_term' ctxt t + in if t = term + then Sign.certify_term thy t' + else + let + val concl = Syntax.check_term ctxt t'; + in Sign.certify_term thy concl end + end fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking then ISA_core.err txt pos @@ -1584,9 +1685,9 @@ fun msg_intro get n oid cid = ("accepts clause " ^ Int.toString n ^ get (" not enabled for", " rejected") ^ " doc_class: " ^ cid) -fun register_oid_cid_in_open_monitors oid _ cid_pos thy = - let val cid_long= fst cid_pos - val pos' = snd cid_pos +fun register_oid_cid_in_open_monitors oid _ (name, pos') thy = + let + val cid_long= name fun is_enabled (n, monitor_info) = if exists (DOF_core.is_subclass_global thy cid_long) (DOF_core.alphabet_of n thy) @@ -1642,11 +1743,11 @@ fun register_oid_cid_in_open_monitors oid _ cid_pos thy = val trace_attr = if defined then trace_attr_t cid_long oid else [] - fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_instance_global oid thy - in #cid params end + fun mon_cid oid = DOF_core.cid_of oid thy |> DOF_core.get_onto_class_cid thy + |> (fn ((name, _), typ) => (name, typ)) val ctxt = Proof_Context.init_global thy fun def_trans_value oid = - (#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) trace_attr)) + (#1 o (calc_update_term {mk_elaboration=true} thy (mon_cid oid) trace_attr)) #> value ctxt val _ = if null enabled_monitors then () @@ -1671,7 +1772,7 @@ fun register_oid_cid_in_open_monitors oid _ cid_pos thy = fun update_trace mon_oid = if Config.get_global thy DOF_core.object_value_debug then let fun def_trans_input_term oid = - #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) trace_attr) + #1 o (calc_update_term {mk_elaboration=false} thy (mon_cid oid) trace_attr) in DOF_core.map_input_term_value mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid) end else DOF_core.map_value mon_oid (def_trans_value mon_oid) @@ -1686,13 +1787,14 @@ fun register_oid_cid_in_open_monitors oid _ cid_pos thy = fun check_invariants thy (oid, _) = let val docitem_value = DOF_core.value_of oid thy - val cid = DOF_core.cid_of oid thy + val name = DOF_core.cid_of oid thy + |> DOF_core.get_onto_class_cid thy |> (fst o fst) fun get_all_invariants cid thy = - case DOF_core.get_onto_class_global cid thy of - DOF_core.Onto_Class {inherits_from=NONE, invs, ...} => single (cid, invs) - | DOF_core.Onto_Class {inherits_from=SOME(_,father), invs, ...} => - (cid, invs) :: (get_all_invariants father thy) - val cids_invariants = get_all_invariants cid thy + case DOF_core.get_onto_class_global cid thy of + DOF_core.Onto_Class {inherits_from=NONE, invs, ...} => single (cid, invs) + | DOF_core.Onto_Class {inherits_from=SOME(_, father), invs, ...} => + (cid, invs) :: get_all_invariants father thy + val cids_invariants = get_all_invariants name thy val inv_and_apply_list = let fun mk_inv_and_apply cid_invs value thy = let val (cid_long, invs) = cid_invs @@ -1725,7 +1827,7 @@ fun check_invariants thy (oid, _) = val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN) (* Get the make definition (def(1) of the record) *) val thms' = - (Proof_Context.get_thms ctxt (Long_Name.append cid defsN)) @ thms + (Proof_Context.get_thms ctxt (Long_Name.append name defsN)) @ thms val _ = Goal.prove ctxt [] [] prop_term (K ((unfold_tac ctxt thms') THEN (auto_tac ctxt))) |> Thm.close_derivation \<^here> @@ -1766,13 +1868,15 @@ fun check_invariants thy (oid, _) = fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oid pos cid_pos doc_attrs thy = let - val cid_pos' = check_classref is_monitor cid_pos thy + val (((name, args_cid), typ), pos') = check_classref is_monitor cid_pos thy + val cid_pos' = (name, pos') 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.virtual_of cid thy |> #virtual - then SOME (DOF_core.get_onto_class_name_global' cid thy) - else NONE + val default_cid = args_cid = DOF_core.default_cid + val vcid = if default_cid + then NONE + else if DOF_core.virtual_of cid_long thy |> #virtual + then SOME args_cid + else NONE val value_terms = if default_cid then let val undefined_value = Free ("Undefined_Value", \<^Type>\unit\) @@ -1782,19 +1886,19 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi without using the burden of ontology classes. ex: text*[sdf]\ Lorem ipsum @{thm refl}\ *) else let - val defaults_init = create_default_object thy cid_long - fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term); + fun conv_attrs ((lhs, pos), rhs) = (YXML.content_of lhs,pos,"=", Syntax.parse_term (Proof_Context.init_global thy) rhs) + val assns' = map conv_attrs doc_attrs + val defaults_init = create_default_object thy oid cid_long typ + fun conv (na, _(*ty*), parsed_term) =(Binding.name_of na, Binding.pos_of na, "=", parsed_term); val S = map conv (DOF_core.get_attribute_defaults cid_long thy); val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false} - thy cid_long S defaults_init; - fun conv_attrs ((lhs, pos), rhs) = (YXML.content_of lhs,pos,"=", Syntax.read_term_global thy rhs) - val assns' = map conv_attrs doc_attrs + thy (name, typ) S defaults_init; val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true} - thy cid_long assns' defaults + thy (name, typ) assns' defaults in if Config.get_global thy DOF_core.object_value_debug then let val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false} - thy cid_long assns' defaults + thy (name, typ) assns' defaults in (input_term, value_term') end else (\<^term>\()\, value_term') end in thy |> DOF_core.define_object_global @@ -1802,8 +1906,8 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi (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' + is_inline, args_cid, vcid)) + |> register_oid_cid_in_open_monitors oid pos (name, pos') |> (fn thy => if (* declare_reference* without arguments is not checked against invariants *) thy |> DOF_core.defined_of oid |> not @@ -1827,7 +1931,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi end (* structure Docitem_Parser *) -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 = ODL_Meta_Args_Parser.empty_meta_args then (K thy) else Docitem_Parser.create_and_check_docitem @@ -1838,10 +1942,10 @@ fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t pos thy = let val thy' = meta_args_exec meta_args_opt thy val name = intern_evaluator thy' raw_name; - val t = Syntax.read_term_global thy' raw_t; - val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos) - (thy'); - val t' = value_select name (Proof_Context.init_global thy') term'; + val t = Syntax.parse_term (Proof_Context.init_global thy') raw_t; + val term' = DOF_core.parsed_elaborate (Proof_Context.init_global thy') pos t + val term'' = Syntax.check_term (Proof_Context.init_global thy') term' + val t' = value_select name (Proof_Context.init_global thy') term''; val ty' = Term.type_of t'; val ty' = if assert then case ty' of @@ -1866,7 +1970,7 @@ val opt_modes = val opt_evaluator = Scan.optional (\<^keyword>\[\ |-- Parse.name --| \<^keyword>\]\) ""; -fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = +fun pass_trans_to_value_cmd (((name, meta_args_opt), modes), t) trans = let val pos = Toplevel.pos_of trans in trans |> Toplevel.theory (value_cmd {assert=false} meta_args_opt name modes t pos) @@ -1910,7 +2014,7 @@ val (disable_assert_evaluation, disable_assert_evaluation_setup) val _ = Theory.setup disable_assert_evaluation_setup -fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans = +fun pass_trans_to_assert_value_cmd (((name, meta_args_opt), modes), t) trans = let val pos = Toplevel.pos_of trans in trans |> Toplevel.theory @@ -1923,6 +2027,7 @@ in trans end (* setup ontology aware commands *) + val _ = Outer_Syntax.command \<^command_keyword>\term*\ "read and print term" (ODL_Meta_Args_Parser.opt_attributes -- (opt_modes -- Parse.term) @@ -1930,31 +2035,31 @@ val _ = val _ = Outer_Syntax.command \<^command_keyword>\value*\ "evaluate and print term" - (ODL_Meta_Args_Parser.opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) - >> (uncurry pass_trans_to_value_cmd)); - + ((opt_evaluator -- ODL_Meta_Args_Parser.opt_attributes -- opt_modes -- Parse.term) + >> (pass_trans_to_value_cmd)); + val _ = Outer_Syntax.command \<^command_keyword>\assert*\ "evaluate and assert term" - (ODL_Meta_Args_Parser.opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) - >> uncurry pass_trans_to_assert_value_cmd); + ((opt_evaluator -- ODL_Meta_Args_Parser.opt_attributes -- opt_modes -- Parse.term) + >> pass_trans_to_assert_value_cmd); (* setup ontology - aware text and ML antiquotations. Due to lexical restrictions, we can not declare them as value* or term*, although we will refer to them this way in papers. *) -local +local fun pretty_term_style ctxt (style: term -> term, t) = - Document_Output.pretty_term ctxt (style (DOF_core.check_term ctxt t)); + Document_Output.pretty_term ctxt (style (DOF_core.check_term ctxt t)) fun print_term ctxt t = ML_Syntax.print_term (DOF_core.check_term (Context.proof_of ctxt) t) in val _ = Theory.setup (Document_Output.antiquotation_pretty_source_embedded \<^binding>\value_\ - (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) + (Scan.lift opt_evaluator -- Term_Style.parse -- Scan.lift Parse.term) (fn ctxt => fn ((name, style), t) => Document_Output.pretty_term ctxt (style (value_select' name ctxt t))) #> ML_Antiquotation.inline_embedded \<^binding>\value_\ - ((Scan.lift opt_evaluator -- Args.term) + ((Scan.lift (opt_evaluator -- Parse.term)) #> (fn ((name, t),(ctxt, ts)) => (((value_select' name (Context.proof_of ctxt) t) |> (ML_Syntax.atomic o (print_term ctxt))), (ctxt, ts)))) @@ -1980,53 +2085,64 @@ 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 {cid,...} = - 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_instance_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} - cid_pos thy - val cid_long = fst cid_pos' - val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long - then () - else error("incompatible classes:"^cid^":"^cid_long) - - fun conv_attrs (((lhs, pos), opn), rhs) = ((YXML.content_of lhs),pos,opn, - Syntax.read_term_global thy rhs) - val assns' = map conv_attrs doc_attrs - val def_trans_value = - #1 o (Value_Command.Docitem_Parser.calc_update_term {mk_elaboration=true} - thy cid_long assns') - #> Value_Command.value (Proof_Context.init_global thy) - in - thy |> (if Config.get_global thy DOF_core.object_value_debug - then let val def_trans_input_term = - #1 o (Value_Command.Docitem_Parser.calc_update_term - {mk_elaboration=false} thy cid_long assns') - in DOF_core.map_input_term_value oid - def_trans_input_term def_trans_value end - else DOF_core.map_value oid def_trans_value) - |> tap (DOF_core.check_ml_invs cid_long oid {is_monitor=false}) - |> (fn thy => if Config.get_global thy DOF_core.invariants_checking - then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) - else thy) - end + let val cid = let val DOF_core.Instance {cid,...} = + 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_instance_name_global oid thy + |> Name_Space.markup (Name_Space.space_of_table instances) + val _ = Context_Position.report ctxt pos markup; + in cid end + val default_cid = cid = DOF_core.default_cid + val (((name, cid'), typ), pos') = Value_Command.Docitem_Parser.check_classref {is_monitor = false} + cid_pos thy + val cid_pos' = (name, pos') + val cid_long = fst cid_pos' + val _ = if cid' = DOF_core.default_cid orelse cid = cid' + then () + else error("incompatible classes:"^cid^":"^cid') + fun conv_attrs (((lhs, pos), opn), rhs) = ((YXML.content_of lhs),pos,opn, + Syntax.parse_term (Proof_Context.init_global thy) rhs) + val assns' = map conv_attrs doc_attrs + val def_trans_value = + #1 o (Value_Command.Docitem_Parser.calc_update_term {mk_elaboration=true} + thy (name, typ) assns') + #> Value_Command.value (Proof_Context.init_global thy) + in + thy |> (if Config.get_global thy DOF_core.object_value_debug + then let val def_trans_input_term = + #1 o (Value_Command.Docitem_Parser.calc_update_term + {mk_elaboration=false} thy (name, typ) assns') + in DOF_core.map_input_term_value oid + def_trans_input_term def_trans_value end + else DOF_core.map_value oid def_trans_value) + |> tap (DOF_core.check_ml_invs cid_long oid {is_monitor=false}) + (* Bypass checking of high-level invariants when the class default_cid = "text", + the top (default) document class. + We want the class default_cid to stay abstract + and not have the capability to be defined with attribute, invariants, etc. + Hence this bypass handles 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}\ *) + |> (fn thy => if default_cid then thy + else if Config.get_global thy DOF_core.invariants_checking + then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) + else thy) + end (* 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) thy = - let fun o_m_c oid pos cid_pos doc_attrs thy = + +fun open_monitor_command ((((oid, pos), raw_parent_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = + let fun o_m_c oid pos params_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 *) {define=true} - oid pos cid_pos doc_attrs thy + oid pos params_cid_pos doc_attrs thy fun compute_enabled_set cid thy = let val DOF_core.Onto_Class X = DOF_core.get_onto_class_global' cid thy @@ -2034,19 +2150,23 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par val aalph = RegExpInterface.alphabet (#rex X) in (aalph, ralph, map (RegExpInterface.rexp_term2da thy 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 - | SOME (cid, _) => cid - val (accS, rejectS, aS) = compute_enabled_set cid thy - in DOF_core.add_monitor_info (Binding.make (oid, pos)) - (DOF_core.make_monitor_info (accS, rejectS, aS)) thy - end + let val cid = case raw_parent_pos of + NONE => ISA_core.err ("You must specified a monitor class.") pos + | SOME (raw_parent, _) => + DOF_core.markup2string raw_parent + |> DOF_core.get_onto_class_cid thy |> (fst o fst) + val (accS, rejectS, aS) = compute_enabled_set cid thy + in DOF_core.add_monitor_info (Binding.make (oid, pos)) + (DOF_core.make_monitor_info (accS, rejectS, aS)) thy + end in - thy |> o_m_c oid pos cid_pos doc_attrs |> create_monitor_entry oid + thy + |> o_m_c oid pos raw_parent_pos doc_attrs + |> create_monitor_entry oid end; -fun close_monitor_command (args as (((oid, pos), _), +fun close_monitor_command (args as (((oid, pos), cid_pos), _: (((string*Position.T)*string)*string)list)) thy = let fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 in if i >= 1 @@ -2085,9 +2205,14 @@ fun meta_args_2_latex thy sem_attrs transform_attr let val l = DOF_core.get_instance_name_global lab thy |> DOF_core.output_name |> enclose "{" "}" |> prefix "label = " - val cid_long = case cid_opt of - NONE => DOF_core.cid_of lab thy - | SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy + val ((cid_long, _), _) = case cid_opt of + NONE => let val DOF_core.Instance cid = + DOF_core.get_instance_global lab thy + in pair (cid |> #cid) (cid |> #cid) + |> rpair \<^typ>\unit\ end + + | SOME(cid,_) => DOF_core.get_onto_class_cid thy cid + val cid_txt = cid_long |> DOF_core.output_name |> enclose "{" "}" |> prefix "type = " @@ -2123,15 +2248,16 @@ fun meta_args_2_latex thy sem_attrs transform_attr in str_of_term end - fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy)) - + fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy)) val ctxt = Proof_Context.init_global thy val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs)) - attr_list - val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), - ltx_of_term ctxt true t)) - (DOF_core.get_attribute_defaults cid_long thy) - + attr_list + val default_args = + (DOF_core.get_attribute_defaults cid_long thy) + |> map (fn (b,_, parsed_term) => + (toLong (Long_Name.base_name ( Sign.full_name thy b)) + , ltx_of_term ctxt true (Syntax.check_term ctxt parsed_term))) + val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) (map (fn (c,_) => c) actual_args))) default_args val transformed_args = (actual_args@default_args_filtered) @@ -2160,6 +2286,7 @@ fun meta_args_2_latex thy sem_attrs transform_attr Latex.string (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"])) end + (* 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 = @@ -2203,7 +2330,7 @@ fun document_command (name, pos) descr mark cmd sem_attrs transform_attr = (fn (meta_args, text) => Toplevel.theory' (fn _ => cmd meta_args) ((Toplevel.presentation_context - #> document_output_reports name mark sem_attrs transform_attr meta_args text + #> document_output_reports name mark sem_attrs transform_attr meta_args text #> SOME): Toplevel.state -> Latex.text option)) ); fun onto_macro_cmd_output_reports output_cmd (meta_args, text) ctxt = @@ -2235,17 +2362,16 @@ val _ = (ODL_Meta_Args_Parser.attributes_upd >> (Toplevel.theory o close_monitor_command)); - val _ = Outer_Syntax.command \<^command_keyword>\update_instance*\ "update meta-attributes of an instance of a document class" (ODL_Meta_Args_Parser.attributes_upd - >> (Toplevel.theory o update_instance_command)); + >> (Toplevel.theory o update_instance_command)); val _ = document_command \<^command_keyword>\text*\ "formal comment (primary style)" {markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) [] I; - + (* This is just a stub at present *) val _ = @@ -2391,8 +2517,7 @@ fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Ar then (K ctxt) else Context.map_theory (Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = true} - {define = true} 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 @@ -2427,19 +2552,6 @@ fun get_positions ctxt x = | get _ _ = []; in get [] end; -fun prep_decls prep_var raw_vars ctxt = - let - val (vars, ctxt') = fold_map prep_var raw_vars ctxt; - val (xs, ctxt'') = ctxt' - |> Context_Position.set_visible false - |> Proof_Context.add_fixes vars - ||> Context_Position.restore_visible ctxt'; - val _ = - Context_Position.reports ctxt'' - (map (Binding.pos_of o #1) vars ~~ - map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs); - in ((vars, xs), ctxt'') end; - fun dummy_frees ctxt xs tss = let val names = @@ -2450,19 +2562,18 @@ fun dummy_frees ctxt xs tss = fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt = let - val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt; + val ((vars, xs), vars_ctxt) = DOF_core.prep_decls prep_var raw_vars ctxt; val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes; - val props = map (parse_prop params_ctxt) (raw_concl :: raw_prems) |> singleton (dummy_frees params_ctxt (xs @ ys)); - val concl :: prems = Syntax.check_props params_ctxt props; + val props' = props |> map (DOF_core.elaborate_term' ctxt) + val concl :: prems = Syntax.check_props params_ctxt props'; val spec = Logic.list_implies (prems, concl); - val spec' = DOF_core.elaborate_term ctxt spec - val spec_ctxt = Variable.declare_term spec' params_ctxt; + val spec_ctxt = Variable.declare_term spec params_ctxt; fun get_pos x = maps (get_positions spec_ctxt x) props; - in ((vars, xs, get_pos, spec'), spec_ctxt) end; + in ((vars, xs, get_pos, spec), spec_ctxt) end; val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop; @@ -2650,7 +2761,8 @@ val _ = theorem \<^command_keyword>\proposition*\ false "propositio val _ = theorem \<^command_keyword>\schematic_goal*\ true "schematic goal"; in end \ - + + section\ Syntax for Ontological Antiquotations (the '' View'' Part II) \ ML\ @@ -2679,7 +2791,10 @@ fun check_and_mark ctxt cid_decl ({strict_checking = strict}) {inline=inline_req val markup = name' |> Name_Space.markup (Name_Space.space_of_table instances) (* this sends a report for a ref application to the PIDE interface ... *) val _ = Context_Position.report ctxt pos markup; - val _ = if not(DOF_core.is_subclass ctxt cid cid_decl) + val cid' = if cid = DOF_core.default_cid + then cid + else DOF_core.get_onto_class_cid thy cid |> (fst o fst) + val _ = if not(DOF_core.is_subclass ctxt cid' cid_decl) then error("reference ontologically inconsistent: " ^ name ^ " is an instance of " ^ cid ^ " and " ^ cid @@ -2729,7 +2844,6 @@ 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 ctxt' = Context.proof_of ctxt @@ -2905,28 +3019,22 @@ fun read_parent NONE ctxt = (NONE, ctxt) | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); - - fun read_fields raw_fields ctxt = let - val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields); - val terms = map ((Option.map (Syntax.read_term ctxt)) o snd) raw_fields - fun test t1 t2 = Sign.typ_instance (Proof_Context.theory_of ctxt) - (t1, Value_Command.Docitem_Parser.generalize_typ 0 t2) - fun check_default (ty,SOME trm) = - let val ty' = (type_of trm) - in if test ty ty' - then () - else error("type mismatch:"^ - (Syntax.string_of_typ ctxt ty')^":"^ - (Syntax.string_of_typ ctxt ty)) - end - (* BAD STYLE : better would be catching exn. *) - |check_default (_,_) = () - val fields = map2 (fn ((x, _, mx),_) => fn T => (x, T, mx)) raw_fields Ts; - val _ = map check_default (Ts ~~ terms) (* checking types conform to defaults *) - val ctxt' = fold Variable.declare_typ Ts ctxt; - in (fields, terms, ctxt') end; + val fields' = raw_fields |> map (apfst (fn (b, ty, mx) => (b, Syntax.read_typ ctxt ty, mx))) + |> map (apsnd (Option.map (Syntax.parse_term ctxt #> DOF_core.elaborate_term' ctxt))) + fun check_default ctxt ((b, ty, _), SOME trm) = + let val parsed_prop = Const (\<^const_name>\Pure.eq\, dummyT) $ Free (Binding.name_of b, dummyT) $ trm + val raw_vars = [(b, SOME ty, NoSyn)] + val (_, vars_ctxt) = DOF_core.prep_decls Proof_Context.cert_var raw_vars ctxt + (* check typ unification *) + val _ = Syntax.check_prop vars_ctxt parsed_prop + in () end + (* BAD STYLE : better would be catching exn. *) + | check_default _ (_, NONE)= () + val _ = map (check_default ctxt) fields' + val ctxt' = fields' |> map (#2 o fst) |> (fn Ts => fold Variable.declare_typ Ts ctxt); + in (map fst fields', map snd fields', ctxt') end; fun def_cmd (decl, spec, prems, params) lthy = let @@ -2944,10 +3052,8 @@ fun define_cond bind f_sty read_cond (ctxt:local_theory) = val args = (SOME(bind,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) in def_cmd args ctxt end -fun define_inv cid_long (bind, inv) thy = +fun define_inv (params, cid_long) (bind, inv) thy = let val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv - (* Rewrite selectors types to allow invariants on attributes of the superclasses - using the polymorphic type of the class *) fun update_attribute_type thy class_scheme_ty cid_long (Const (s, Type (st,[ty, ty'])) $ t) = let @@ -2957,7 +3063,7 @@ fun define_inv cid_long (bind, inv) thy = 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 - then let val Type(_, tys') = ty + then let val Type(st', tys') = ty in if tys' = [\<^typ>\unit\] then Const (s, Type(st,[ty, ty'])) $ (update_attribute_type thy class_scheme_ty cid_long t) @@ -2976,31 +3082,34 @@ fun define_inv cid_long (bind, inv) thy = then Free (s, class_scheme_ty) else Free (s, ty) | update_attribute_type _ _ _ t = t - val inv_ty = Syntax.read_typ (Proof_Context.init_global thy) - (Name.aT ^ " " ^ cid_long ^ schemeN) + val zeta = (singleton (Name.variant_list (map #1 params)) "'z", \<^sort>\type\) + val typ = Type (cid_long ^ schemeN, map TFree (params @ [zeta])) (* Update the type of each attribute update function to match the type of the 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 (instance_placeholderN, inv_ty)) inv_term' + val inv_term' = update_attribute_type thy typ cid_long inv_term + val eq_inv_ty = typ --> HOLogic.boolT + val abs_term = Term.lambda (Free (instance_placeholderN, typ)) inv_term' in thy |> Named_Target.theory_map (define_cond bind eq_inv_ty abs_term) end fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy = - let + let val bind_pos = Binding.pos_of binding val name = Binding.name_of 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 = (* takes class synonyms into account *) - DOF_core.get_onto_class_name_global' name thy + fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) + (Symbol.explode (YXML.content_of s))) + val name' = + case raw_parent of + NONE => DOF_core.default_cid + | SOME s => markup2string s |> (fn s => DOF_core.get_onto_class_name_global' s thy) + fun cid thy = DOF_core.get_onto_class_name_global name thy val (parent, ctxt2) = read_parent raw_parent ctxt1; - (* takes class synonyms into account *) - val parent' = parent |> Option.map (fn (x, y) => (x, DOF_core.get_onto_class_name_global' y thy)) - val parent_cid_long = if is_some parent' - then parent' |> the |> snd - else DOF_core.default_cid + val parent' = case parent of + NONE => NONE + | SOME (Ts, _) => SOME (Ts, name') val raw_fieldsNdefaults' = filter (fn((bi,_,_),_) => Binding.name_of bi <> traceN) raw_fieldsNdefaults val _ = if length raw_fieldsNdefaults' <> length raw_fieldsNdefaults @@ -3008,22 +3117,21 @@ fun add_doc_class_cmd overloaded (raw_params, binding) else () val raw_fieldsNdefaults'' = if null regexps then raw_fieldsNdefaults' - else trace_attr_ts::raw_fieldsNdefaults' - val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults'' ctxt2; - val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms + else trace_attr_ts::raw_fieldsNdefaults' + val (fields, parsed_terms, ctxt3) = read_fields raw_fieldsNdefaults'' ctxt2; + val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ parsed_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 => 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.") + case DOF_core.get_attribute_info name' (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 fun mk_eq_pair name = (Free (name, doc_class_rexp_T), doc_class_rexp_t name) |> mk_meta_eq @@ -3048,12 +3156,12 @@ fun add_doc_class_cmd overloaded (raw_params, binding) else add [DOF_core.tag_attr] 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) + |> (fn thy => fold(define_inv (params', (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 *) - |> (fn thy => ISA_core.declare_ISA_class_accessor_and_check_instance (cid thy, bind_pos) thy) - |> (fn thy => ISA_core.declare_class_instances_annotation (cid thy, bind_pos) thy) + |> (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 1f78055..292b7fe 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -474,7 +474,7 @@ text\ \<^rail>\ (@@{command "term*"} ('[' meta_args ']')? '\' HOL_term '\' | (@@{command "value*"} - | @@{command "assert*"}) \ ('[' meta_args ']')? ('[' evaluator ']')? '\' HOL_term '\' + | @@{command "assert*"}) \ ('[' evaluator ']')? ('[' meta_args ']')? '\' HOL_term '\' | (@@{command "definition*"}) ('[' meta_args ']')? ('... see ref manual') | (@@{command "lemma*"} | @@{command "theorem*"} | @@{command "corollary*"}