diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 9286c4e..dcaa259 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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.\ subsection\ Syntax \ typedecl "doc_class" -typedecl "typ" -typedecl "term" -typedecl "thm" -typedecl "file" -typedecl "thy" \ \and others in the future : file, http, thy, ...\ -consts ISA_typ :: "string \ typ" ("@{typ _}") -consts ISA_term :: "string \ term" ("@{term _}") +datatype "typ" = ISA_typ string ("@{typ _}") +datatype "term" = ISA_term string ("@{term _}") consts ISA_term_repr :: "string \ term" ("@{termrepr _}") -consts ISA_thm :: "string \ thm" ("@{thm _}") -consts ISA_file :: "string \ file" ("@{file _}") -consts ISA_thy :: "string \ thy" ("@{thy _}") +datatype "thm" = ISA_thm string ("@{thm _}") +datatype "file" = ISA_file string ("@{file _}") +datatype "thy" = ISA_thy string ("@{thy _}") consts ISA_docitem :: "string \ 'a" ("@{docitem _}") -consts ISA_docitem_attr :: "string \ string \ 'a" ("@{docitemattr (_) :: (_)}") +datatype "docitem_attr" = ISA_docitem_attr string string ("@{docitemattr (_) :: (_)}") \ \Dynamic setup of inner syntax cartouche\ @@ -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\ Isar - Setup\ -setup\DOF_core.update_isa_global("Isa_DOF.typ" ,{check=ISA_core.ML_isa_check_typ, elaborate=(fn _ => fn term => term)}) \ -setup\DOF_core.update_isa_global("Isa_DOF.term" ,{check=ISA_core.ML_isa_check_term, elaborate=(fn _ => fn term => term)}) \ -setup\DOF_core.update_isa_global("Isa_DOF.term_repr",{check=(fn _ => fn (t,_,_) => fn _ => SOME t), elaborate=(fn _ => fn term => term)}) \ -setup\DOF_core.update_isa_global("Isa_DOF.thm" ,{check=ISA_core.ML_isa_check_thm, elaborate=(fn _ => fn term => term)}) \ -setup\DOF_core.update_isa_global("Isa_DOF.file" ,{check=ISA_core.ML_isa_check_file, elaborate=(fn _ => fn term => term)}) \ -setup\DOF_core.update_isa_global("Isa_DOF.docitem" ,{check=ISA_core.ML_isa_check_docitem, elaborate=(fn _ => fn term => term)})\ +setup\DOF_core.update_isa_global("Isa_DOF.typ.typ", + {check=ISA_core.ML_isa_check_typ, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Isa_DOF.term.term", + {check=ISA_core.ML_isa_check_term, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Isa_DOF.term_repr", + {check=(fn _ => fn (t,_,_) => fn _ => SOME t), elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Isa_DOF.thm.thm", + {check=ISA_core.ML_isa_check_thm, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Isa_DOF.file.file", + {check=ISA_core.ML_isa_check_file, elaborate=ISA_core.ML_isa_elaborate_generic}) \ +setup\DOF_core.update_isa_global("Isa_DOF.docitem", + {check=ISA_core.ML_isa_check_docitem, elaborate=ISA_core.ML_isa_elaborate_generic}) \ section\ Syntax for Annotated Documentation Commands (the '' View'' Part I) \ diff --git a/src/tests/Evaluation.thy b/src/tests/Evaluation.thy index 089f315..5c314ad 100644 --- a/src/tests/Evaluation.thy +++ b/src/tests/Evaluation.thy @@ -12,10 +12,19 @@ text\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. \ @@ -56,11 +65,6 @@ value*\@{A \xcv1\}\ text\We can also get the value of an attribute of the instance:\ value*\A.x @{A \xcv1\}\ -ML\ -val {docobj_tab={tab = x, ...},docclass_tab, ISA_transformer_tab,...} = DOF_core.get_data @{context}; - Symtab.dest ISA_transformer_tab; -\ - text\If the attribute of the instance is not initialized, we get an undefined value, whose type is the type of the attribute:\ term*\level @{C \xcv2\}\ @@ -71,29 +75,46 @@ term*\C.g @{C \xcv2\}\ value*\C.g @{C \xcv2\}\ text\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 \xcv4\} can be validated, and the fact that it is an instance of the class @{doc_class F} } will be checked:\ term*\@{F \xcv4\}\ -text\But the evaluation will fail with the current implementation. +text\We can also evaluate the instance @{docitem \xcv4\}. The attribute \b\ of the instance @{docitem \xcv4\} is of type @{typ "(A \ 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 \g\ 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 \xcv4\} initializes the attribute by using the \docitem\ TA. +Then the instance can be evaluate but only the references of the classes of the set +used in the \b\ attribute will be checked, and the type of these classes will not: +\ +value* \@{F \xcv4\}\ + +text\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 \xcv3\} is of type @{typ "A"} and the instance @{C \xcv2\} is of type @{typ "C"}: +\ +update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"] + +text\Using a TA in terms is possible, and the term is evaluated:\ +value*\[@{thm \HOL.refl\}, @{thm \HOL.refl\}]\ +value*\@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\ + +ML\ +@{thm "refl"} +\ + +text\There are still some limitations. +The terms passed as arguments to the TA are not simplified and their evaluation fails: \ (* Error: -value* \@{F \xcv4\}\*) +value*\@{thm (''HOL.re'' @ ''fl'')}\ +value*\@{thm ''HOL.refl''} = @{thm (''HOL.re'' @ ''fl'')}\*) -text\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\ +text\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 \xcv4\}: +\ (* Error: -value*\[@{thm \HOL.refl\}, @{thm \HOL.refl\}]\*) +update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*) -end \ No newline at end of file +end diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy index 35a0265..9e8dd06 100755 --- a/src/tests/TermAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -62,6 +62,15 @@ text\Example for a meta-attribute of ODL-type @{typ "typ"} with an appropr theorem @{thm "refl"}}\ text*[xcv2::C, g="@{thm ''HOL.refl''}"]\Lorem ipsum ...\ +text\A warning about the usage of the \docitem\ TA: +The \docitem\ TA offers a way to check the reference of class instances +without checking the instances type. +So one will be able to reference \docitem\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. +\ + 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\. \ text*[xcv4::F, r="[@{thm ''HOL.refl''},