From 5d2a0c1ff42267d98a8c3d26e1332ebd6bdb471e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 16 Jan 2023 14:45:25 +0100 Subject: [PATCH] Update file hierarchy with Bu proposition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The idea is for the Deep_Interpretation to source the shallow material, and then update the checking and elaboration functions of the term anti-quotations. To achieve this, the mechanism of removing and readding the notations (mixfixes) of the term-antiquotations after the metalogic is sourced is used. Example: With shallow: datatype "typ" = ISA_typ string ("@{typ _}") Generate a datatype whose Constructor ISA_typ has the notation @{typ ...}. You get: find_consts name:"ISA_typ" find_consts name: "ISA_typ" found 1 constant(s): Shallow_Interpretation.typ.ISA_typ :: "char list ⇒ typ" With Deep: no_notation "ISA_typ" ("@{typ _}") consts ISA_typ :: "string ⇒ typ" ("@{typ _}") The notation is removed and then added to the new ISA_typ constant. You get: find_consts name:"ISA_typ" find_consts name: "ISA_typ" found 2 constant(s): Deep_Interpretation.ISA_typ :: "char list ⇒ Core.typ" Shallow_Interpretation.typ.ISA_typ :: "char list ⇒ Shallow_Interpretation.typ" But only the Deep_Interpretation constant has the notation (mixfix). --- src/DOF/DOF_Shallow.thy | 6 +++--- src/DOF/Isa_COL.thy | 2 +- src/ROOT | 4 ---- src/ROOTS | 1 + src/{DOF => deep}/DOF_Deep.thy | 3 +-- .../Deep_Interpretation.thy | 13 ++++++++++++- src/deep/ROOT | 10 ++++++++++ src/{ => deep}/tests/Reification_Test.thy | 2 +- src/ontologies/Conceptual/Conceptual.thy | 2 +- src/ontologies/scholarly_paper/scholarly_paper.thy | 2 +- src/ontologies/small_math/small_math.thy | 2 +- src/tests/ROOT | 1 - 12 files changed, 32 insertions(+), 16 deletions(-) rename src/{DOF => deep}/DOF_Deep.thy (85%) rename src/{DOF/meta_interpretation => deep}/Deep_Interpretation.thy (96%) create mode 100644 src/deep/ROOT rename src/{ => deep}/tests/Reification_Test.thy (99%) diff --git a/src/DOF/DOF_Shallow.thy b/src/DOF/DOF_Shallow.thy index 148f3951..41948413 100644 --- a/src/DOF/DOF_Shallow.thy +++ b/src/DOF/DOF_Shallow.thy @@ -1,6 +1,6 @@ theory DOF_Shallow - imports "Isabelle_DOF.Isa_DOF" - "Isabelle_DOF.Shallow_Interpretation" + imports Isabelle_DOF.Isa_COL + Isabelle_DOF.Shallow_Interpretation begin @@ -18,4 +18,4 @@ term "@{docitem \doc_ref\}" ML\ @{term "@{docitem \doc_ref\}"}\ (**) -end \ No newline at end of file +end diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 039f2e70..d5a54c7a 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -22,7 +22,7 @@ text\ Building a fundamental infrastructure for common document elements s \ theory Isa_COL - imports DOF_Shallow + imports Isa_DOF keywords "title*" "subtitle*" "chapter*" "section*" "subsection*" "subsubsection*" diff --git a/src/ROOT b/src/ROOT index 1c94f424..cbdc8dbb 100644 --- a/src/ROOT +++ b/src/ROOT @@ -2,7 +2,6 @@ session "Isabelle_DOF" = "Functional-Automata" + options [document = pdf, document_output = "output", document_build = dof] sessions "Regular-Sets" - "Metalogic_ProofChecker" directories "DOF" "DOF/meta_interpretation" @@ -15,8 +14,5 @@ session "Isabelle_DOF" = "Functional-Automata" + "ontologies/CC_v3_1_R5" theories "DOF/DOF_Shallow" - "DOF/DOF_Deep" "ontologies/ontologies" export_classpath - - diff --git a/src/ROOTS b/src/ROOTS index 2b29f276..ca704105 100644 --- a/src/ROOTS +++ b/src/ROOTS @@ -1 +1,2 @@ tests +deep \ No newline at end of file diff --git a/src/DOF/DOF_Deep.thy b/src/deep/DOF_Deep.thy similarity index 85% rename from src/DOF/DOF_Deep.thy rename to src/deep/DOF_Deep.thy index 1e3f88d1..b4be2a8d 100644 --- a/src/DOF/DOF_Deep.thy +++ b/src/deep/DOF_Deep.thy @@ -1,6 +1,5 @@ theory DOF_Deep - imports "Isabelle_DOF.Isa_DOF" - "Isabelle_DOF.Deep_Interpretation" + imports Deep_Interpretation begin diff --git a/src/DOF/meta_interpretation/Deep_Interpretation.thy b/src/deep/Deep_Interpretation.thy similarity index 96% rename from src/DOF/meta_interpretation/Deep_Interpretation.thy rename to src/deep/Deep_Interpretation.thy index 77ebbba5..2ac95225 100644 --- a/src/DOF/meta_interpretation/Deep_Interpretation.thy +++ b/src/deep/Deep_Interpretation.thy @@ -1,5 +1,5 @@ theory Deep_Interpretation - imports Isabelle_DOF.DOF_Core + imports Isabelle_DOF.DOF_Shallow Metalogic_ProofChecker.ProofTerm begin @@ -8,6 +8,17 @@ subsection\ Syntax \ \ \and others in the future : file, http, thy, ...\ +(* Delete shallow interpretation notations (mixfixes) of the term anti-quotations, + so we can use them for the deep interpretation *) +no_notation "ISA_typ" ("@{typ _}") +no_notation "ISA_term" ("@{term _}") +no_notation "ISA_thm" ("@{thm _}") +no_notation "ISA_file" ("@{file _}") +no_notation "ISA_thy" ("@{thy _}") +no_notation "ISA_docitem" ("@{docitem _}") +no_notation "ISA_docitem_attr" ("@{docitemattr (_) :: (_)}") +no_notation "ISA_trace_attribute" ("@{trace-attribute _}") + consts ISA_typ :: "string \ typ" ("@{typ _}") consts ISA_term :: "string \ term" ("@{term _}") consts ISA_term_repr :: "string \ term" ("@{termrepr _}") diff --git a/src/deep/ROOT b/src/deep/ROOT new file mode 100644 index 00000000..67418175 --- /dev/null +++ b/src/deep/ROOT @@ -0,0 +1,10 @@ +session "Isabelle_DOF-Deep" = Isabelle_DOF + + options [document = pdf, document_output = "output", document_build = dof] + sessions + "Metalogic_ProofChecker" + directories + "tests" + theories + "DOF_Deep" + "tests/Reification_Test" + export_classpath \ No newline at end of file diff --git a/src/tests/Reification_Test.thy b/src/deep/tests/Reification_Test.thy similarity index 99% rename from src/tests/Reification_Test.thy rename to src/deep/tests/Reification_Test.thy index 5eadc7b7..64c5fd76 100644 --- a/src/tests/Reification_Test.thy +++ b/src/deep/tests/Reification_Test.thy @@ -1,5 +1,5 @@ theory Reification_Test - imports "Isabelle_DOF.DOF_Deep" + imports "../DOF_Deep" begin diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index a263e38f..f04a6679 100644 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -17,7 +17,7 @@ theory Conceptual imports "Isabelle_DOF.DOF_Shallow" - "Isabelle_DOF.Isa_COL" + begin diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 6002e088..df537c92 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -14,7 +14,7 @@ section\An example ontology for scientific, MINT-oriented papers.\ theory scholarly_paper - imports "Isabelle_DOF.Isa_COL" + imports "Isabelle_DOF.DOF_Shallow" keywords "author*" "abstract*" "Definition*" "Lemma*" "Theorem*" :: document_body begin diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index d82f730e..40b761b2 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -14,7 +14,7 @@ section\An example ontology for a math paper\ theory small_math - imports "Isabelle_DOF.Isa_COL" + imports "Isabelle_DOF.DOF_Shallow" begin doc_class title = diff --git a/src/tests/ROOT b/src/tests/ROOT index 00aa768a..39f6ee73 100644 --- a/src/tests/ROOT +++ b/src/tests/ROOT @@ -9,6 +9,5 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" + "Evaluation" "High_Level_Syntax_Invariants" "Ontology_Matching_Example" - "Reification_Test" theories [condition = ISABELLE_DOF_HOME] "Isabelle2022"