6a6259bf29
ci/woodpecker/push/build Pipeline was successful
Details
Use metalogic to generate meta term anti-quotations The idea is for the Very_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 reading the notations (mixfixes) of the term-antiquotations, after the metalogic is sourced, is used. Example: With shallow: datatype "typ" = Isabelle_DOF_typ string ("@{typ _}") Generate a datatype whose Constructor Isabelle_DOF_typ has the notation @{typ ...}. You get: find_consts name:"Isabelle_DOF_typ" find_consts name: "Isabelle_DOF_typ" found 1 constant(s): Shallow_Interpretation.typ.Isabelle_DOF_typ :: "char list ⇒ typ" With Deep: no_notation "Isabelle_DOF_typ" ("@{typ _}") consts Isabelle_DOF_typ :: "string ⇒ typ" ("@{typ _}") The notation is removed and then added to the new Isabelle_DOF_typ constant. You get: find_consts name:"Isabelle_DOF_typ" find_consts name: "Isabelle_DOF_typ" found 2 constant(s): Deep_Interpretation.Isabelle_DOF_typ :: "char list ⇒ Core.typ" Shallow_Interpretation.typ.Isabelle_DOF_typ :: "char list ⇒ Shallow_Interpretation.typ" But only the Deep_Interpretation constant has the notation (mixfix). Then new interpretation of term anti-quotations is available for the user. |
||
---|---|---|
.. | ||
ROOT | ||
Reification_Test.thy | ||
Very_Deep_DOF.thy | ||
Very_Deep_Interpretation.thy |