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

increasing robustness of generic attribute term constructor 

(adding antiquotations)
This commit is contained in:
Burkhart Wolff 2018-08-21 08:07:07 +02:00
parent 627122c3fa
commit 8e09644e5c
1 changed files with 11 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
test/conceptual/Attributes.thy
View File

@ -65,7 +65,7 @@ fun calc_update_term thy cid_long (S:(((string * Position.T) * string) * string)
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 =
fun read_assn (((lhs, pos), opr), rhs) term =
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
@ -77,24 +77,25 @@ fun calc_update_term thy cid_long (S:(((string * Position.T) * string) * string)
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)
= Const (@{const_name "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)
= Const (@{const_name "append"}, ttt --> ttt --> ttt)
|join (ttt as Type(@{type_name "set"},_))
= Const (@{const_name "sup"}, ttt --> ttt --> ttt)
|join (ttt as Type(@{type_name "list"},_))
= Const (@{const_name "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
$ term
| "+=" => Const(lnu,lnut)
$ Abs ("uu_", lnt, join lnt $ (Bound 0) $ rhs')
$ tt
$ term
| _ => error "corrupted syntax - oops - this should not occur"
end
in fold read_assn S term end
\<close>
ML\<open>\<close>
end