forked from Isabelle_DOF/Isabelle_DOF
Merge pull request 'referential-equivalence-first-draft' (#4) from nicolas.meric/Isabelle_DOF:referential-equivalence-first-draft into master
Reviewed-on: Isabelle_DOF/Isabelle_DOF#4
This commit is contained in:
commit
1d497db5cf
|
@ -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)
|
||||
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) => [(cid_long,X)]
|
||||
attribute_decl = X, ...})) => [(cid_long,X)]
|
||||
| (SOME ({inherits_from=SOME(_,father),
|
||||
attribute_decl = X, ...}), cid_long) =>
|
||||
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.\<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>
|
||||
|
||||
|
@ -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\<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>
|
||||
|
||||
|
@ -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
|
||||
|
|
|
@ -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