Implement built-ins referential equivalence
- Add a first implementation of a referential equivalence for the built-ins term annotations (TA) - Some built-ins remain as unspecified constants: - the docitem TA offers a way to check the reference of class instances without checking the instances type. It must be avoided for certification - the termrepr TA is left as an unspecified constant for now. A major refactoring of code should be done to enable referential equivalence for termrepr, by changing the dependency between the Isa_DOF theory and the Assert theory. The assert_cmd function in Assert should use the value* command functions, which make the elaboration of the term referenced by the TA before passing it to the evaluator - Update the Evaluation test theory to test the referential equivalence and expose some of current implementation limitations - Add a warning about the docitem TA in the TermAntiquotations theory
This commit is contained in:
parent
6ac1445147
commit
08c101c544
|
@ -194,7 +194,7 @@ struct
|
|||
end)
|
||||
type ISA_transformers = {check :
|
||||
(theory -> term * typ * Position.T -> string -> term option),
|
||||
elaborate : (theory -> term -> term)
|
||||
elaborate : (theory -> string -> typ -> term -> term)
|
||||
}
|
||||
|
||||
type ISA_transformer_tab = ISA_transformers Symtab.table
|
||||
|
@ -656,7 +656,7 @@ fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
|
|||
(* checking isa, may raise error though. *)
|
||||
| SOME t =>
|
||||
if mk_elaboration
|
||||
then elaborate thy t
|
||||
then elaborate thy s ty t
|
||||
else Const(s,ty) $ t)
|
||||
(* transforming isa *)
|
||||
else (Const(s,ty) $ (T t))
|
||||
|
@ -789,22 +789,17 @@ versions might extend this feature substantially.\<close>
|
|||
subsection\<open> Syntax \<close>
|
||||
|
||||
typedecl "doc_class"
|
||||
typedecl "typ"
|
||||
typedecl "term"
|
||||
typedecl "thm"
|
||||
typedecl "file"
|
||||
typedecl "thy"
|
||||
|
||||
\<comment> \<open>and others in the future : file, http, thy, ...\<close>
|
||||
|
||||
consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
||||
consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
|
||||
datatype "typ" = ISA_typ string ("@{typ _}")
|
||||
datatype "term" = ISA_term string ("@{term _}")
|
||||
consts ISA_term_repr :: "string \<Rightarrow> term" ("@{termrepr _}")
|
||||
consts ISA_thm :: "string \<Rightarrow> thm" ("@{thm _}")
|
||||
consts ISA_file :: "string \<Rightarrow> file" ("@{file _}")
|
||||
consts ISA_thy :: "string \<Rightarrow> thy" ("@{thy _}")
|
||||
datatype "thm" = ISA_thm string ("@{thm _}")
|
||||
datatype "file" = ISA_file string ("@{file _}")
|
||||
datatype "thy" = ISA_thy string ("@{thy _}")
|
||||
consts ISA_docitem :: "string \<Rightarrow> 'a" ("@{docitem _}")
|
||||
consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a" ("@{docitemattr (_) :: (_)}")
|
||||
datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}")
|
||||
|
||||
\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
|
||||
|
||||
|
@ -975,11 +970,6 @@ fun check_instance thy (term, _, pos) s =
|
|||
in check' (class_name, object_cid) end;
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
fun elaborate_instance thy term = let val instance_name = HOLogic.dest_string term
|
||||
in case DOF_core.get_value_global instance_name thy of
|
||||
NONE => error ("No class instance: " ^ instance_name)
|
||||
| SOME(value) => value
|
||||
end
|
||||
|
||||
fun ML_isa_id thy (term,pos) = SOME term
|
||||
|
||||
|
@ -1004,6 +994,14 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) s =
|
|||
else err ("faulty reference to docitem: "^name) pos
|
||||
in ML_isa_check_generic check thy (term, pos) s end
|
||||
|
||||
fun ML_isa_elaborate_generic (thy:theory) isa_name ty term = Const (isa_name, ty) $ term
|
||||
|
||||
fun elaborate_instance thy _ _ term = let val instance_name = HOLogic.dest_string term
|
||||
in case DOF_core.get_value_global instance_name thy of
|
||||
NONE => error ("No class instance: " ^ instance_name)
|
||||
| SOME(value) => value
|
||||
end
|
||||
|
||||
(*
|
||||
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
|
||||
|
@ -1046,12 +1044,18 @@ end; (* struct *)
|
|||
|
||||
subsection\<open> Isar - Setup\<close>
|
||||
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.typ" ,{check=ISA_core.ML_isa_check_typ, elaborate=(fn _ => fn term => term)}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.term" ,{check=ISA_core.ML_isa_check_term, elaborate=(fn _ => fn term => term)}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.term_repr",{check=(fn _ => fn (t,_,_) => fn _ => SOME t), elaborate=(fn _ => fn term => term)}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.thm" ,{check=ISA_core.ML_isa_check_thm, elaborate=(fn _ => fn term => term)}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.file" ,{check=ISA_core.ML_isa_check_file, elaborate=(fn _ => fn term => term)}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.docitem" ,{check=ISA_core.ML_isa_check_docitem, elaborate=(fn _ => fn term => term)})\<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.typ.typ",
|
||||
{check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.term.term",
|
||||
{check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.term_repr",
|
||||
{check=(fn _ => fn (t,_,_) => fn _ => SOME t), elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.thm.thm",
|
||||
{check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.file.file",
|
||||
{check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("Isa_DOF.docitem",
|
||||
{check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \<close>
|
||||
|
||||
section\<open> Syntax for Annotated Documentation Commands (the '' View'' Part I) \<close>
|
||||
|
||||
|
|
|
@ -12,10 +12,19 @@ text\<open>The value* command uses the same code as the value command
|
|||
and adds the possibility to evaluate Term Annotation Antiquotations (TA).
|
||||
For that an elaboration of the term referenced by a TA must be done before
|
||||
passing it to the evaluator.
|
||||
The current implementation is really basic:
|
||||
\<^item> For the built-ins, the term referenced by the TA is returned
|
||||
as it is;
|
||||
\<^item> For an instance class, the value of the instance is returned.
|
||||
The current implementation is based on referential equality, syntactically, and
|
||||
with the help of HOL, on referential equivalence, semantically:
|
||||
Some built-ins remain as unspecified constants:
|
||||
\<^item> the docitem TA offers a way to check the reference of class instances
|
||||
without checking the instances type.
|
||||
It must be avoided for certification
|
||||
\<^item> the termrepr TA is left as unspecified constant for now.
|
||||
A major refactoring of code should be done to enable
|
||||
referential equivalence for termrepr, by changing the dependency
|
||||
between the Isa_DOF theory and the Assert theory.
|
||||
The assert_cmd function in Assert should use the value* command
|
||||
functions, which make the elaboration of the term
|
||||
referenced by the TA before passing it to the evaluator
|
||||
The emphasis of this presentation is to present the evaluation possibilities and limitations
|
||||
of the current implementation.
|
||||
\<close>
|
||||
|
@ -56,11 +65,6 @@ value*\<open>@{A \<open>xcv1\<close>}\<close>
|
|||
text\<open>We can also get the value of an attribute of the instance:\<close>
|
||||
value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
|
||||
|
||||
ML\<open>
|
||||
val {docobj_tab={tab = x, ...},docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context};
|
||||
Symtab.dest ISA_transformer_tab;
|
||||
\<close>
|
||||
|
||||
text\<open>If the attribute of the instance is not initialized, we get an undefined value,
|
||||
whose type is the type of the attribute:\<close>
|
||||
term*\<open>level @{C \<open>xcv2\<close>}\<close>
|
||||
|
@ -71,29 +75,46 @@ term*\<open>C.g @{C \<open>xcv2\<close>}\<close>
|
|||
value*\<open>C.g @{C \<open>xcv2\<close>}\<close>
|
||||
|
||||
text\<open>Some terms can be validated, i.e. the term will be checked,
|
||||
and the existence of every object referenced by a TA will be checked,
|
||||
but can not be evaluated, i.e. the elaboration of the TA to be evaluated will fail.
|
||||
and the existence of every object referenced by a TA will be checked,
|
||||
and can be evaluated by using referential equivalence.
|
||||
The existence of the instance @{docitem \<open>xcv4\<close>} can be validated,
|
||||
and the fact that it is an instance of the class @{doc_class F} } will be checked:\<close>
|
||||
term*\<open>@{F \<open>xcv4\<close>}\<close>
|
||||
|
||||
text\<open>But the evaluation will fail with the current implementation.
|
||||
text\<open>We can also evaluate the instance @{docitem \<open>xcv4\<close>}.
|
||||
The attribute \<open>b\<close> of the instance @{docitem \<open>xcv4\<close>} is of type @{typ "(A \<times> C) set"}
|
||||
and then the elements of the set must have equivalence properties,
|
||||
i.e. definitions for the equality.
|
||||
But the current definition does not define equality for TA.
|
||||
So the attribute \<open>g\<close> of the class @{doc_class C}, which is a @{typ "thm"},
|
||||
does not have a definition for the equality and the evaluation of the set fails:
|
||||
but the instance @{docitem \<open>xcv4\<close>} initializes the attribute by using the \<open>docitem\<close> TA.
|
||||
Then the instance can be evaluate but only the references of the classes of the set
|
||||
used in the \<open>b\<close> attribute will be checked, and the type of these classes will not:
|
||||
\<close>
|
||||
value* \<open>@{F \<open>xcv4\<close>}\<close>
|
||||
|
||||
text\<open>If we want the classes to be checked,
|
||||
we can use the TA which will also check the type of the instances.
|
||||
The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:
|
||||
\<close>
|
||||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
|
||||
|
||||
text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
|
||||
value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
|
||||
value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
|
||||
|
||||
ML\<open>
|
||||
@{thm "refl"}
|
||||
\<close>
|
||||
|
||||
text\<open>There are still some limitations.
|
||||
The terms passed as arguments to the TA are not simplified and their evaluation fails:
|
||||
\<close>
|
||||
(* Error:
|
||||
value* \<open>@{F \<open>xcv4\<close>}\<close>*)
|
||||
value*\<open>@{thm (''HOL.re'' @ ''fl'')}\<close>
|
||||
value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.re'' @ ''fl'')}\<close>*)
|
||||
|
||||
text\<open>Because we do not keep necessarily the same type for the TA and the term referenced
|
||||
by the TA, evaluation may fail due to type mismatch.
|
||||
Here, we have a list of @{typ "thm"}, but after the elaboration,
|
||||
the theorem become an HOL string with type @{typ "char list"} and then
|
||||
does not match the list type\<close>
|
||||
text\<open>The type checking is unaware that a class is subclass of another one.
|
||||
The @{doc_class "G"} is a subclass of the class @{doc_class "C"}, but one can not use it
|
||||
to update the instance @{docitem \<open>xcv4\<close>}:
|
||||
\<close>
|
||||
(* Error:
|
||||
value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>*)
|
||||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
|
||||
|
||||
end
|
|
@ -62,6 +62,15 @@ text\<open>Example for a meta-attribute of ODL-type @{typ "typ"} with an appropr
|
|||
theorem @{thm "refl"}}\<close>
|
||||
text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
text\<open>A warning about the usage of the \<open>docitem\<close> TA:
|
||||
The \<open>docitem\<close> TA offers a way to check the reference of class instances
|
||||
without checking the instances type.
|
||||
So one will be able to reference \<open>docitem\<close>s (class instances) and have them checked,
|
||||
without the burden of the type checking required otherwise.
|
||||
But it may give rise to unwanted behaviors, due to its polymorphic type.
|
||||
It must not be used for certification.
|
||||
\<close>
|
||||
|
||||
text\<open>Major sample: test-item of doc-class \<open>F\<close> with a relational link between class instances,
|
||||
and links to formal Isabelle items like \<open>typ\<close>, \<open>term\<close> and \<open>thm\<close>. \<close>
|
||||
text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
||||
|
|
Loading…
Reference in New Issue