Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

corrected DOF_core.get_attribute_info. 

Restructuring with this respect.
This commit is contained in:
Burkhart Wolff 2018-08-20 13:54:53 +02:00
parent 00a4fd1c6b
commit 5d7c32479d
2 changed files with 35 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
Isa_DOF.thy
View File

@ -317,6 +317,7 @@ fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt)
Symtab.defined t (name2doc_class_name_local ctxt cid)
end
fun get_attributes_local cid ctxt =
if cid = default_cid then []
else let val t = snd(get_data ctxt)
@ -342,15 +343,24 @@ fun get_default_local cid attr ctxt =
fun get_default cid attr thy = get_default_local cid attr (Proof_Context.init_global thy)
fun get_attribute_long_name_local cid attr ctxt =
type attributes_info = { def_occurrence : string,
long_name : string,
typ : typ
}
fun get_attribute_info_local cid attr ctxt : attributes_info option=
let val hierarchy = get_attributes_local cid ctxt (* search in order *)
fun found (_,L) = find_first (fn (bind,_,_) => Binding.name_of bind = attr) L
fun found (s,L) = case find_first (fn (bind,_,_) => Binding.name_of bind = attr) L of
NONE => NONE
| SOME X => SOME(s,X)
in case get_first found hierarchy of
NONE => NONE
| SOME (bind, ty,_) => SOME(cid,(Binding.name_of bind), ty)
| SOME (cid',(bind, ty,_)) => SOME({def_occurrence = cid,
long_name = cid'^"."^(Binding.name_of bind),
typ = ty})
end
fun get_attribute_long_name cid attr thy = get_attribute_long_name_local cid attr
fun get_attribute_info cid attr thy = get_attribute_info_local cid attr
(Proof_Context.init_global thy)
@ -842,10 +852,12 @@ fun calculate_attr_access_check ctxt attr oid = (* template *)
case DOF_core.get_value_local oid (Context.the_proof ctxt) of
SOME term => let val ctxt = Context.the_proof ctxt
val SOME{cid,...} = DOF_core.get_object_local oid ctxt
val (long_cid, attr_b,ty) = case DOF_core.get_attribute_long_name_local cid attr ctxt of
val (* (long_cid, attr_b,ty) = *)
{def_occurrence, long_name, typ=ty} =
case DOF_core.get_attribute_info_local cid attr ctxt of
SOME f => f
| NONE => error ("attribute undefined for ref"^ oid)
val proj_term = Const(long_cid^"."^attr_b,dummyT --> ty)
val proj_term = Const(long_name,dummyT --> ty)
val term = calculate_attr_access ctxt proj_term term
in (ML_Syntax.atomic o ML_Syntax.print_term) term end
| NONE => error "identifier not a docitem reference"
@ -925,11 +937,11 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
val params' = map (Proof_Context.check_tfree ctxt3) params;
fun check_n_filter thy (bind,ty,mf) =
case DOF_core.get_attribute_long_name parent_cid_long (Binding.name_of bind) thy of
case DOF_core.get_attribute_info parent_cid_long (Binding.name_of bind) thy of
NONE => (* no prior declaration *) SOME(bind,ty,mf)
| SOME(class,attr,ty') => if ty = ty'
then (warning("overriding attribute:"^ attr^
" in doc class:" ^ class);
| SOME{def_occurrence, long_name, typ} => if ty = typ
then (warning("overriding attribute:"^long_name^
" in doc class:" ^ def_occurrence);
SOME(bind,ty,mf))
else error("no overloading allowed.")
val gen_antiquotation = OntoLinkParser.docitem_ref_antiquotation

37
test/conceptual/Attributes.thy
View File

@ -2,9 +2,7 @@ theory Attributes
imports "../../ontologies/Conceptual"
begin
ML\<open>open Long_Name;
base_name "Conceptual.A"
\<close>
text*[dfgdfg::B, y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl}}\<close>
text\<open> @{docitem_ref \<open>dfgdfg\<close>} }\<close>
@ -24,24 +22,19 @@ term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
term "C.z ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
ML\<open>
DOF_core.get_attribute_long_name "Conceptual.A" "x" @{theory};
DOF_core.get_attribute_long_name "Conceptual.B" "x" @{theory};
DOF_core.get_attribute_long_name "Conceptual.B" "y" @{theory};
DOF_core.get_attribute_long_name "Conceptual.C" "x" @{theory};
DOF_core.get_attribute_long_name "Conceptual.C" "y" @{theory};
DOF_core.get_attribute_long_name "Conceptual.C" "z" @{theory};
(* this is only partially correct : the attribute longnames should be:
Conceptual.A.x
Conceptual.B.x
Conceptual.B.y
Conceptual.B.x
Conceptual.B.y
Conceptual.C.z
*)
val SOME {def_occurrence = "Conceptual.A", long_name = "Conceptual.A.x", typ = t}
= DOF_core.get_attribute_info "Conceptual.A" "x" @{theory};
DOF_core.get_attribute_info "Conceptual.B" "x" @{theory};
DOF_core.get_attribute_info "Conceptual.B" "y" @{theory};
DOF_core.get_attribute_info "Conceptual.C" "x" @{theory};
val SOME {def_occurrence = "Conceptual.C", long_name = "Conceptual.B.y", typ = t'}
= DOF_core.get_attribute_info "Conceptual.C" "y" @{theory};
(* this is the situation where an attribute is defined in C, but due to inheritance
from B, where it is firstly declared which results in a different long_name. *)
DOF_core.get_attribute_info "Conceptual.C" "z" @{theory};
\<close>
ML\<open>
DOF_core.get_default_local "Conceptual.A" "x" @{context};
@ -60,10 +53,6 @@ DOF_core.get_value_local "xxxy" @{context};
DOF_core.get_value_local "dfgdfg" @{context};
\<close>
ML\<open>
val Type X = @{typ "A"}
\<close>
ML\<open>val t = @{docitem_attr y::dfgdfg} \<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg}) \<close>
end