From 6ac1445147cdcd9a277512fdc0cdb519b4f713c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 29 Oct 2021 08:26:03 +0200 Subject: [PATCH 1/2] Change the implementation of the tag attribute The philosophy is for the tag attribute to be unique for each class. So this commit updates the implementation of this attribute to match the philosophy. The previous implementation associated a tag attribute with a class but also with each super-class of this class up to the top (default) class "text". Now a class with super-classes has only one tag attribute. --- src/DOF/Isa_DOF.thy | 57 +++++++++++++++++---------------------------- 1 file changed, 22 insertions(+), 35 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index cde38d2..9286c4e 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -535,37 +535,27 @@ fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse Symtab.defined t (parse_cid ctxt cid) end -fun lookup_docobj cid ctxt = -let val t = #docclass_tab(get_data ctxt) - val cid_long = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) -in (Symtab.lookup t cid_long, cid_long) end - -fun get_all_attributes_local tag_attribute cid ctxt = - if cid = default_cid then [] - else case lookup_docobj cid ctxt of - (NONE, _) => error("undefined class id for attributes: "^cid) - | (SOME ({inherits_from=NONE, - attribute_decl = X, ...}), cid_long) => [(cid_long, tag_attribute, X)] - | (SOME ({inherits_from=SOME(_,father), - attribute_decl = X, ...}), cid_long) => - get_all_attributes_local tag_attribute father ctxt - @ [(cid_long, tag_attribute, X)] - -fun get_all_attributes tag_attribute cid thy = - get_all_attributes_local tag_attribute cid (Proof_Context.init_global thy) fun get_attributes_local cid ctxt = if cid = default_cid then [] - else case lookup_docobj cid ctxt of - (NONE, _) => error("undefined class id for attributes: "^cid) - | (SOME ({inherits_from=NONE, - attribute_decl = X, ...}), cid_long) => [(cid_long,X)] - | (SOME ({inherits_from=SOME(_,father), - attribute_decl = X, ...}), cid_long) => + else let val t = #docclass_tab(get_data ctxt) + val cid_long = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) + in case Symtab.lookup t cid_long of + NONE => error("undefined class id for attributes: "^cid) + | (SOME ({inherits_from=NONE, + attribute_decl = X, ...})) => [(cid_long,X)] + | (SOME ({inherits_from=SOME(_,father), + attribute_decl = X, ...})) => get_attributes_local father ctxt @ [(cid_long,X)] + end fun get_attributes cid thy = get_attributes_local cid (Proof_Context.init_global thy) +fun get_all_attributes_local cid ctxt = + (tag_attr, get_attributes_local cid ctxt) + +fun get_all_attributes cid thy = get_all_attributes_local cid (Proof_Context.init_global thy) + type attributes_info = { def_occurrence : string, def_pos : Position.T, long_name : string, @@ -1180,19 +1170,12 @@ fun create_default_object thy class_name = let val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name val make_const = Syntax.read_term_global thy (class_name ^ ".make"); - val typ_list = case make_const of Const (_, ty) => binder_types ty - | _ => error ("Malformed class identifier") fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_" ^ (Binding.name_of binding) ^ "_Attribute_Not_Initialized", typ) - fun all_attr_to_free (_, tag_attr, attr_list) = - (attr_to_free tag_attr, map (attr_to_free) attr_list) - val tag_attr_attr_bname_typ_list_free_list = map (all_attr_to_free) - (DOF_core.get_all_attributes DOF_core.tag_attr class_name thy) - val all_attr_free_list = - flat (map (fn (tag_attr_free, attr_free_list) => tag_attr_free::attr_free_list) - tag_attr_attr_bname_typ_list_free_list) -in list_comb (make_const, all_attr_free_list) end; + fun all_attr_free_list (tag_attr, class_list) = + (attr_to_free tag_attr)::(map (attr_to_free) (flat (map snd class_list))) +in list_comb (make_const, all_attr_free_list (DOF_core.get_all_attributes class_name thy)) end; fun base_default_term cid_long thy = create_default_object thy cid_long; @@ -2077,7 +2060,11 @@ fun add_doc_class_cmd overloaded (raw_params, binding) val _ = map_filter (check_n_filter thy) fields - in thy |> Record.add_record overloaded (params', binding) parent' (DOF_core.tag_attr::fields) + in thy |> (fn thy => case parent' of + NONE => Record.add_record + overloaded (params', binding) parent' (DOF_core.tag_attr::fields) thy + | SOME _ => Record.add_record + overloaded (params', binding) parent' (fields) thy) |> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)]) |> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps reject_Atoms invariants -- 2.39.2 From 08c101c5440eee2a087068581952026e88c39f6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 4 Nov 2021 15:10:02 +0100 Subject: [PATCH 2/2] 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 --- src/DOF/Isa_DOF.thy | 52 ++++++++++++----------- src/tests/Evaluation.thy | 71 +++++++++++++++++++++----------- src/tests/TermAntiquotations.thy | 9 ++++ 3 files changed, 83 insertions(+), 49 deletions(-) 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''}, -- 2.39.2