First reasonably well-tested version with
- access of attributes for objects created over multiple inheritance - taking updates into account
This commit is contained in:
parent
25bcc030b4
commit
cedac17646
33
Isa_DOF.thy
33
Isa_DOF.thy
|
|
@ -490,12 +490,19 @@ val SPY2 = Unsynchronized.ref ([]:Symbol_Pos.T list);
|
|||
val SPY3 = Unsynchronized.ref ("");
|
||||
|
||||
|
||||
fun cid_2_cidType cid_long =
|
||||
fun cid_2_cidType cid_long thy =
|
||||
if cid_long = DOF_core.default_cid then @{typ "unit"}
|
||||
else let val ty_name = cid_long^"."^ Long_Name.base_name cid_long^"_ext"
|
||||
in Type(ty_name, [@{typ "unit"}]) end
|
||||
else let val t = snd(DOF_core.get_data_global thy)
|
||||
fun ty_name cid = cid^"."^ Long_Name.base_name cid^"_ext"
|
||||
fun fathers cid_long = case Symtab.lookup t cid_long of
|
||||
NONE => error("undefined doc class id :"^cid_long)
|
||||
| SOME ({inherits_from=NONE, ...}) => [cid_long]
|
||||
| SOME ({inherits_from=SOME(_,father), ...}) =>
|
||||
cid_long :: (fathers father)
|
||||
in fold (fn x => fn y => Type(ty_name x,[y])) (fathers cid_long) @{typ "unit"}
|
||||
end
|
||||
|
||||
fun base_default_term cid_long = Const(@{const_name "undefined"},cid_2_cidType cid_long)
|
||||
fun base_default_term thy cid_long = Const(@{const_name "undefined"},cid_2_cidType thy cid_long)
|
||||
|
||||
fun check_classref (SOME(cid,pos')) thy =
|
||||
let val _ = if not (DOF_core.is_defined_cid_global cid thy)
|
||||
|
|
@ -518,7 +525,7 @@ val SPY6 = Unsynchronized.ref("")
|
|||
val SPY7 = Unsynchronized.ref([]:(string * Position.T * string * term) list)
|
||||
|
||||
fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) term =
|
||||
let val cid_ty = cid_2_cidType cid_long
|
||||
let val cid_ty = cid_2_cidType cid_long thy
|
||||
val generalize_term = Term.map_types (generalize_typ 0)
|
||||
fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t
|
||||
fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t)
|
||||
|
|
@ -591,7 +598,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta
|
|||
(* val _ = (SPY:=assns)
|
||||
val _ = (SPY2 := Input.source_explode toks) *)
|
||||
*)
|
||||
val defaults_init = base_default_term cid_long
|
||||
val defaults_init = base_default_term cid_long thy
|
||||
fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term);
|
||||
val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
|
||||
val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init;
|
||||
|
|
@ -898,16 +905,16 @@ end (* struct *)
|
|||
*}
|
||||
|
||||
ML{*
|
||||
structure AttributeAcces =
|
||||
struct
|
||||
|
||||
fun calculate_attr_access ctxt proj_term term =
|
||||
(* term assumed to be ground type, (f term) not necessarily *)
|
||||
let val _ = writeln("XXX "^(Syntax.string_of_term ctxt (proj_term $ term)))
|
||||
val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term]
|
||||
let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term]
|
||||
val ty = type_of (subterm')
|
||||
val _ = writeln("YYY "^(Syntax.string_of_term ctxt subterm'))
|
||||
val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT)
|
||||
$ subterm'
|
||||
$ Free("_XXXXXXX", ty))
|
||||
val _ = writeln("ZZZ "^(Syntax.string_of_term ctxt term'))
|
||||
val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term')));
|
||||
val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm)
|
||||
in lhs end
|
||||
|
|
@ -926,9 +933,7 @@ fun calculate_attr_access_check ctxt attr oid = (* template *)
|
|||
in (ML_Syntax.atomic o ML_Syntax.print_term) term end
|
||||
| NONE => error "identifier not a docitem reference"
|
||||
|
||||
*}
|
||||
|
||||
ML{*
|
||||
|
||||
val _ = Theory.setup
|
||||
(ML_Antiquotation.inline @{binding docitem_attr}
|
||||
(fn (ctxt,toks) =>
|
||||
|
|
@ -939,6 +944,8 @@ val _ = Theory.setup
|
|||
)
|
||||
(ctxt, toks))
|
||||
)
|
||||
|
||||
end
|
||||
*}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -24,6 +24,9 @@ doc_class D = B +
|
|||
also local definitions of enumerations *)
|
||||
a2 :: int <= 0
|
||||
|
||||
doc_class E = D +
|
||||
x :: "string" <= "''qed''" (* overriding default *)
|
||||
|
||||
doc_class F =
|
||||
r :: "thm list"
|
||||
b :: "(A \<times> C) set" <= "{}"
|
||||
|
|
|
|||
|
|
@ -16,8 +16,15 @@ Symtab.dest y;
|
|||
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
|
||||
|
||||
typ "C"
|
||||
typ "D"
|
||||
ML\<open>val Type("Conceptual.B.B_ext",[Type("Conceptual.C.C_ext",t)]) = @{typ "C"};
|
||||
val @{typ "D"} = ODL_Command_Parser.cid_2_cidType "Conceptual.D" @{theory};
|
||||
val @{typ "E"}= ODL_Command_Parser.cid_2_cidType "Conceptual.E" @{theory};
|
||||
\<close>
|
||||
|
||||
text*[dfgdfg2::C, z = "None"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
|
||||
|
||||
text*[omega::E, x = "''g''"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
|
||||
|
||||
text\<open> @{docitem_ref \<open>dfgdfg\<close>} \<close>
|
||||
|
||||
|
|
@ -25,7 +32,7 @@ text\<open> @{docitem_ref \<open>dfgdfg\<close>} \<close>
|
|||
|
||||
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
|
||||
term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
|
||||
term "C.z ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
|
||||
term "C.z ((undefined::C)\<lparr>B.y := [''sdf''], z:= Some undefined\<rparr>)"
|
||||
|
||||
ML\<open>
|
||||
val SOME {def_occurrence = "Conceptual.A", long_name = "Conceptual.A.x", typ = t, def_pos}
|
||||
|
|
@ -41,19 +48,22 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory};
|
|||
\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
ML\<open>
|
||||
DOF_core.get_value_local "sdf" @{context};
|
||||
DOF_core.get_value_local "sdfg" @{context};
|
||||
DOF_core.get_value_local "xxxy" @{context};
|
||||
DOF_core.get_value_local "dfgdfg" @{context};
|
||||
DOF_core.get_value_local "omega" @{context};
|
||||
\<close>
|
||||
|
||||
text\<open>Not too trivial test: default y -> [].
|
||||
text\<open>A not too trivial test: default y -> [].
|
||||
At creation : x -> "f", y -> "sdf".
|
||||
The latter wins at access time.\<close>
|
||||
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg}) \<close>
|
||||
The latter wins at access time.
|
||||
Then @{term "t"}: creation of a multi inheritance object omega,
|
||||
triple updates, the last one wins.\<close>
|
||||
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg});
|
||||
val t = HOLogic.dest_string (@{docitem_attr x::omega});
|
||||
\<close>
|
||||
|
||||
(* separate checking and term construction ?*)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue