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.
