nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

New generalised attribute term constructor (untested) 

Refactoring necessary.
This commit is contained in:
Burkhart Wolff 2018-08-20 20:29:04 +02:00
parent 5d7c32479d
commit 627122c3fa
2 changed files with 45 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Isa_DOF.thy
View File

@ -348,7 +348,7 @@ type attributes_info = { def_occurrence : string,
typ : typ
}
fun get_attribute_info_local cid attr ctxt : attributes_info option=
fun get_attribute_info_local (*long*)cid attr ctxt : attributes_info option=
let val hierarchy = get_attributes_local cid ctxt (* search in order *)
fun found (s,L) = case find_first (fn (bind,_,_) => Binding.name_of bind = attr) L of
NONE => NONE
@ -360,8 +360,8 @@ fun get_attribute_info_local cid attr ctxt : attributes_info option=
typ = ty})
end
fun get_attribute_info cid attr thy = get_attribute_info_local cid attr
(Proof_Context.init_global thy)
fun get_attribute_info (*long*)cid attr thy =
get_attribute_info_local cid attr (Proof_Context.init_global thy)
fun get_value_global oid thy = case get_object_global oid thy of

42
test/conceptual/Attributes.thy
View File

@ -55,4 +55,46 @@ DOF_core.get_value_local "dfgdfg" @{context};
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg}) \<close>
(* separate checking and term construction ?*)
ML\<open>val Type(s,t) = @{typ "'a list"}; fold\<close>
ML\<open>
fun calc_update_term thy cid_long (S:(((string * Position.T) * string) * string)list) term =
let val count = Unsynchronized.ref (0 - 1);
fun incr () = Unsynchronized.inc count
val generalize_term = let val n = incr ()
in Term.map_types (AnnoTextelemParser.generalize_typ n) end
fun read_assn (((lhs, pos), opr), rhs) tt =
let val info_opt = DOF_core.get_attribute_info cid_long
(Long_Name.base_name lhs) thy
val (ln,lnt,lnu,lnut) = case info_opt of
NONE => error ("unknown attribute in class: "^cid_long)
| SOME{long_name, typ, ...} => (long_name, typ,
long_name ^"_update",
typ --> dummyT --> dummyT)
val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then ()
else error("illegal notation for attribute of "^cid_long)
val rhs' = Syntax.read_term_global thy rhs |> generalize_term
fun join (ttt as @{typ "int"})
= Const ("Groups.plus_class.plus", ttt --> ttt --> ttt)
|join (ttt as @{typ "string"})
= Const ("List.append", ttt --> ttt --> ttt)
|join (ttt as Type("Set.set",_))
= Const ("Lattices.sup_class.sup", ttt --> ttt --> ttt)
|join (ttt as Type("List.list",_))
= Const ("List.append", ttt --> ttt --> ttt)
|join _ = error("implicit fusion operation not defined on attribute: "^ lhs)
(* could be extended to bool, map, multisets, ... *)
in case opr of
"=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, rhs')
$ tt
| "+=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, join lnt $ (Bound 0) $ rhs')
$ tt
end
in fold read_assn S term end
\<close>
end