diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index cde38d2..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 @@ -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, @@ -666,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)) @@ -799,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\ @@ -985,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 @@ -1014,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 @@ -1056,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) \ @@ -1180,19 +1174,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 +2064,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 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''},