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

Update normalization

This commit is contained in:
Nicolas Méric 2022-07-08 08:13:46 +02:00
parent 4967a3e907
commit a5462195d8
5 changed files with 1076 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

233
src/DOF/Isa_DOF.thy
View File

@ -1055,10 +1055,15 @@ fun elaborate_instance thy _ _ term_option pos =
case term_option of
NONE => error ("Malformed term annotation")
| SOME term => let val instance_name = HOLogic.dest_string term
in case DOF_core.get_value_global instance_name thy of
(*in case DOF_core.get_value_global instance_name thy of
NONE => error ("No class instance: " ^ instance_name)
| SOME(value) =>
DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy
end*)
in case DOF_core.get_object_global instance_name thy of
NONE => error ("No class instance: " ^ instance_name)
| SOME({input_term,...}) =>
DOF_core.transduce_term_global {mk_elaboration=true} (input_term, pos) thy
end
(*
@ -1351,11 +1356,11 @@ fun create_default_object thy class_name =
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
fun init_tag_attr (binding, typ, _) = HOLogic.mk_string (purified_class_name ^ "_"
^ (Binding.name_of binding))
val id = serial ()
fun init_tag_attr (binding, typ, _) = Syntax.read_term_global thy
((LargeInt.toString id) ^ "::int")
(*fun init_tag_attr (binding, typ, _) = HOLogic.mk_string (purified_class_name ^ "_"
^ (Binding.name_of binding))*)
(*val id = serial ()*)
(*fun init_tag_attr (binding, typ, _) = Syntax.read_term_global thy
((LargeInt.toString id) ^ "::int")*)
val class_list' = DOF_core.get_attributes class_name thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
@ -1368,12 +1373,19 @@ fun create_default_object thy class_name =
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list'' = rev (attrs_filter (rev class_list'))
fun add_tag_to_attrs_free tag_attr thy (cid, filtered_attr_list) =
val tag_attr = HOLogic.mk_number @{typ "int"}
(*fun add_tag_to_attrs_free tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (init_tag_attr tag_attr)::(map (attr_to_free) filtered_attr_list)
else (map (attr_to_free) filtered_attr_list)*)
fun add_tag_to_attrs_free' tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (tag_attr (serial ()))::(map (attr_to_free) filtered_attr_list)
else (map (attr_to_free) filtered_attr_list)
val class_list''' = flat (map (add_tag_to_attrs_free DOF_core.tag_attr thy) class_list'')
in list_comb (make_const, (init_tag_attr DOF_core.tag_attr)::class_list''') end
(*val class_list''' = flat (map (add_tag_to_attrs_free DOF_core.tag_attr thy) class_list'')*)
val class_list'''' = flat (map (add_tag_to_attrs_free' tag_attr thy) class_list'')
(*in list_comb (make_const, (init_tag_attr DOF_core.tag_attr)::class_list''') end*)
in list_comb (make_const, (tag_attr (serial()))::class_list'''') end
fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy =
let
@ -1397,7 +1409,43 @@ fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init
fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
(S:(string * Position.T * string * term)list) term =
let val cid_ty = cid_2_cidType cid_long thy
let
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) cid_long
(*val make_const = Syntax.read_term_global thy (Long_Name.qualify cid_long makeN);*)
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
(*fun init_tag_attr (binding, typ, _) = HOLogic.mk_string (purified_class_name ^ "_"
^ (Binding.name_of binding))*)
(*val id = serial ()*)
(*fun init_tag_attr (binding, typ, _) = Syntax.read_term_global thy
((LargeInt.toString id) ^ "::int")*)
val class_list' = DOF_core.get_attributes cid_long thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list'' = rev (attrs_filter (rev class_list'))
val tag_attr = HOLogic.mk_number @{typ "int"}
(*fun add_tag_to_attrs_free tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (init_tag_attr tag_attr)::(map (attr_to_free) filtered_attr_list)
else (map (attr_to_free) filtered_attr_list)*)
fun add_tag_to_attrs_free' tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (tag_attr (serial ()))::(map (attr_to_free) filtered_attr_list)
else (map (attr_to_free) filtered_attr_list)
(*val class_list''' = flat (map (add_tag_to_attrs_free DOF_core.tag_attr thy) class_list'')*)
val class_list'''' = flat (map (add_tag_to_attrs_free' tag_attr thy) class_list'')
(*in list_comb (make_const, (init_tag_attr DOF_core.tag_attr)::class_list''') end*)
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 =
@ -1588,6 +1636,154 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
| SOME (cid,_) => if (DOF_core.is_virtual cid thy)
then SOME (DOF_core.parse_cid_global thy cid)
else NONE
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) cid_long
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
val class_list = DOF_core.get_attributes cid_long thy
val _ = writeln("In create_and_check_docitem class_list: " ^ @{make_string} class_list)
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list' = rev (attrs_filter (rev class_list))
val _ = writeln("In create_and_check_docitem class_list': " ^ @{make_string} class_list')
(* val class_list'' = map (fn (string, attrs) =>
(string , map (fn (binding, typ, term_option) =>
case term_option of
NONE => let
val term = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
in (binding, typ, [term]) end
| SOME (term) => (binding, typ, [term])) attrs))
class_list'*)
val class_list'' = map (fn (string, attrs) =>
(string , map (fn (binding, typ, term_option) =>
let
val term = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
in (binding, typ, [term]) end) attrs))
class_list'
val _ = writeln("In create_and_check_docitem class_list'': " ^ @{make_string} class_list'')
fun normalize_record (Const(update_name, Type(s, [t, u])) $ Abs(_, typ', term') $ term) class_list cid thy =
let
val _ = writeln ("AAAAAAAAAAAAA")
(* I also must check the class to rule out updates of standard record
see testtest3 *)
val update_bname = Long_Name.base_name update_name
val attr_name = String.extract (update_bname, 0, SOME (String.size(update_bname) - String.size(Record.updateN)))
val update_qual = Long_Name.qualifier update_name
val class_typ = Syntax.read_typ_global thy cid
val class_typ' = class_typ --> class_typ
(*val (Const(make_name, typ''), ts)= strip_comb term
val make_bname = Long_Name.base_name make_name
val make_qual = Long_Name.qualifier make_name*)
in
if (String.isSuffix Record.updateN update_bname andalso
(update_qual = cid orelse
(DOF_core.is_subclass_global thy cid update_qual andalso class_typ' = u))
(*andalso make_bname = makeN andalso make_qual = cid*))
then
let
val (Const(make_name, typ''), ts)= strip_comb term
val make_bname = Long_Name.base_name make_name
val make_qual = Long_Name.qualifier make_name
in
if (make_bname = makeN andalso make_qual = cid)
then
let
val _ = writeln ("BBBBBBBBBBBBB")
val _ = writeln ("In normalize_record update class_list: " ^ @{make_string} class_list)
fun update_class_term_list attr_name term attr =
let
val (attr_id, ty, term_list) = attr
in
if (Binding.name_of attr_id = attr_name)
then
let
val term_list' = case term_list of
[] => [term]
| (x::xs) => x::term::xs
in
(attr_id, ty, term_list') end
else attr
end
val class_list' = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (update_class_term_list attr_name term') attr_list) end) class_list
val _ = writeln ("In normalize_record update class_list': " ^ @{make_string} class_list')
fun normalize_attribute [term] = term
| normalize_attribute (x::y::xs) =
case y of
\<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close> $ Bound 0 $ t =>
(*let val (T, i) = HOLogic.dest_number x
val (T',j) = HOLogic.dest_number t*)
let val evaluated_term = Value_Command.value @{context} (\<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close> $ x $ t)
(*in normalize_attribute ((HOLogic.mk_number T (i + j))::xs) end*)
in normalize_attribute (evaluated_term::xs) end
(*| \<^Const>\<open>Lattices.sup_class.sup \<^Type>\<open>set \<^typ>\<open>_\<close>\<close>\<close> $ Bound 0 $ t =>
Value_Command.value*)
| _ => normalize_attribute (y::xs)
val tag_attr = HOLogic.mk_number @{typ "int"}
fun add_tag_to_attrs tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (tag_attr (serial ()))::map (fn (binding, ty, term) => term) filtered_attr_list
else map (fn (binding, ty, term) => term) filtered_attr_list
val class_list'' = map
(fn (string, attrs) =>
(string, map (fn (binding, ty, ts) =>
(binding, ty, normalize_attribute ts)) attrs)) class_list'
val class_list''' = flat (map (add_tag_to_attrs tag_attr thy) class_list'')
(*val make_const = Syntax.read_term_global thy (Long_Name.qualify cid makeN);*)
in list_comb (Const(make_name, typ''), (tag_attr (serial()))::class_list''') end
(*in error ("BBBBBBB") end*)
else
let
fun update_class_term_list attr_name term attr =
let
val (attr_id, ty, term_list) = attr
in
if (Binding.name_of attr_id = attr_name)
then
let
val term_list' = case term_list of
[] => [term]
| (x::xs) => x::term::xs
in
(attr_id, ty, term_list') end
else attr
end
val class_list' = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (update_class_term_list attr_name term') attr_list) end) class_list
val _ = writeln ("In normalize_record update class_list: " ^ @{make_string} class_list)
val _ = writeln ("In normalize_record update class_list': " ^ @{make_string} class_list')
in normalize_record term class_list' cid thy end
end
(*in
normalize_record term class_list' cid thy
(*(Const(update_name,typ) $ abs) :: normalize_record term cid updates thy*)
end*)
else normalize_record term class_list cid thy
end
| normalize_record (t1 $ t2) class_list cid thy =
(normalize_record t1 class_list cid thy) $ (normalize_record t2 class_list cid thy)
| normalize_record t class_list cid thy = t
val value_terms = if (cid_long = DOF_core.default_cid)
then let
val undefined_value = Free ("Undefined_Value", @{typ "unit"})
@ -1598,27 +1794,36 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
without using the burden of ontology classes.
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
*)
else let
else let
val defaults_init = create_default_object thy cid_long
val _ = writeln("In create_and_check_docitem defaults_init: "
^ Syntax.string_of_term (Proof_Context.init_global thy) defaults_init)
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 _ = writeln("In create_and_check_docitem S: "
^ @{make_string} S)
val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false}
thy cid_long S defaults_init;
val _ = writeln("In create_and_check_docitem defaults: "
^ Syntax.string_of_term (Proof_Context.init_global thy) defaults)
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs
val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false}
thy cid_long assns' defaults
val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
thy cid_long assns' defaults
in (input_term, Value_Command.value (Proof_Context.init_global thy) value_term') end
val _ = writeln("In create_and_check_docitem value_term': " ^ @{make_string} value_term')
(*in (input_term, Value_Command.value (Proof_Context.init_global thy) value_term') end*)
in (input_term, normalize_record value_term' class_list'' cid_long thy) end
val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor)
o Context.Theory
in thy |> DOF_core.define_object_global (oid, {pos = pos,
thy_name = Context.theory_name thy,
input_term = fst value_terms,
value = value (Proof_Context.init_global thy)
(snd value_terms),
(*value = value (Proof_Context.init_global thy)
(snd value_terms),*)
value = (snd value_terms),
inline = is_inline,
id = id,
cid = cid_long,

2
src/ontologies/Conceptual/Conceptual.thy
View File

@ -88,7 +88,7 @@ doc_class B =
text\<open>We may even use type-synonyms for class synonyms ...\<close>
type_synonym XX = B
print_doc_items
subsection\<open>Examples of inheritance \<close>
doc_class C = XX +

838
src/tests/High_Level_Syntax_Invariants.thy
View File

@ -11,16 +11,57 @@ text\<open>
To enable the checking of the invariants, the \<open>invariants_checking\<close>
theory attribute must be set:\<close>
declare[[invariants_checking = true]]
text\<open>For example, let's define the following two classes:\<close>
ML\<open>
val update_name = "High_Level_Syntax_Invariants.class_inv1.int1_update"
val term' = Const ("Groups.one_class.one", \<^typ>\<open>int\<close>)
val update_bname = Long_Name.base_name update_name
val attr_name = String.extract (update_bname, 0, SOME (String.size(update_bname) - String.size(Record.updateN)))
fun update_class_term_list attr_name term attr =
let
val (attr_id, ty, term_list) = attr
in
if (Binding.name_of attr_id = attr_name)
then
let
fun update_term_list [] term = [term]
| update_term_list (x::xs) term = x::term::xs
(*| update_term_list (x::y::xs) term = x::(update_term_list xs term)@[y]*)
in
(attr_id, ty, update_term_list term_list term) end
else attr
end
val class_list = [("High_Level_Syntax_Invariants.class_inv1",
[(Binding.name "int1", "int",
[Free ("High_Level_Syntax_Invariants_class_inv2_int1_Attribute_Not_Initialized", \<^typ>\<open>int\<close>),
Const ("Num.numeral_class.numeral", \<^typ>\<open>num \<Rightarrow> int\<close>)
$ (Const ("Num.num.Bit1", \<^typ>\<open>num \<Rightarrow> num\<close>)
$ Const ("Num.num.One", \<^typ>\<open>num\<close>))])]),
("High_Level_Syntax_Invariants.class_inv2",
[(Binding.name "int2", "int",
[Free ("High_Level_Syntax_Invariants_class_inv2_int2_Attribute_Not_Initialized", \<^typ>\<open>int\<close>),
Const ("Groups.one_class.one", \<^typ>\<open>int\<close>)])])]
val class_list' = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (update_class_term_list attr_name term') attr_list) end) class_list
\<close>
doc_class class_inv1 =
int1 :: "int"
int1 :: "int" <= "0"
invariant inv1 :: "int1 \<sigma> \<ge> 3"
doc_class class_inv0 = class_inv1 +
int1 :: "int"
text*[testinv0::class_inv0, int1=4]\<open>lorem ipsum...\<close>
print_doc_items
doc_class class_inv2 = class_inv1 +
int1 :: "int" <= "1"
int2 :: "int"
invariant inv2 :: "int2 \<sigma> < 2"
@ -40,6 +81,8 @@ update_instance*[testinv1::class_inv1, int1:=1]
*)
text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
print_doc_items
value*\<open>int1 @{class-inv2 \<open>testinv2\<close>}\<close>
text\<open>
The value of each attribute defined for the instances is checked against their classes invariants.
@ -146,4 +189,795 @@ declare[[invariants_checking_with_tactics = false]]
declare[[invariants_checking = false]]
text*[testtest0::class_inv1]\<open>lorem ipsum...\<close>
text*[testtest::class_inv1, int1=2]\<open>lorem ipsum...\<close>
text*[testtest1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
update_instance*[testtest::class_inv1, int1+=1]
update_instance*[testtest::class_inv1, int1:=3]
text*[testtest2::class_inv2]\<open>lorem ipsum...\<close>
update_instance*[testtest2::class_inv2, int2+=1]
text*[testtest00::class_inv0]\<open>lorem ipsum...\<close>
ML\<open>
val thy = @{theory}
val cid = "class_inv0"
val t = DOF_core.parse_cid_global thy cid
\<close>
print_doc_classes
print_doc_items
find_consts name:"class_inv1"
find_theorems name:"class_inv1*simps"
find_theorems name:"class_inv1*defs*"
find_theorems name:"class_inv1*ext*"
record point =
xcoord :: int
ycoord :: int
record pointt = point +
xcoord :: int
ycoord :: int
find_consts name:"xcoord"
term\<open>pointt.make\<close>
definition pt1 :: point where "pt1 \<equiv> \<lparr>point.xcoord = 1 , ycoord = 2 \<rparr>"
definition pt2 :: point where "pt2 \<equiv> \<lparr>point.xcoord = 2 , ycoord = 4 \<rparr>"
record cpoint = point +
color :: int
term\<open>\<lparr>xcoord=1, ycoord=3\<rparr>\<close>
term\<open>\<lparr>color = 3, xcoord=1, ycoord=3\<rparr>\<close>
definition cpt1 :: cpoint where "cpt1 \<equiv> \<lparr>point.xcoord=1, ycoord=3, color = 3\<rparr>"
doc_class class_inv4 =
pt_attr :: point <= "pt1"
text*[testtest4::class_inv4, pt_attr="pt2"]\<open>lorem ipsum...\<close>
find_consts name:"point"
find_theorems name:"point*simps"
find_theorems name:"point*defs*"
find_theorems name:"cpoint*ext*"
doc_class class_inv3 =
class_inv1_attr :: "class_inv1 set" <= "{@{class-inv1 \<open>testtest1\<close>}}"
pt :: point
text*[testtest3::class_inv3
, class_inv1_attr="{@{class-inv1 \<open>testtest\<close>}, @{class-inv1 \<open>testtest1\<close>}}"
, pt="\<lparr>point.xcoord = 1 , ycoord = 2 \<rparr>\<lparr>point.xcoord := 2\<rparr>"
]\<open>lorem ipsum...\<close>
doc_class class_inv5 =
a1 :: "class_inv1 set"
b1 :: point
text*[testtest5::class_inv5]\<open>lorem ipsum...\<close>
doc_class class_inv6 = class_inv5 +
a1 :: "class_inv1 set"
b1 :: point
text*[testtest6::class_inv6]\<open>lorem ipsum...\<close>
doc_class class_inv7 = class_inv6 +
a1 :: "class_inv1 set"
b1 :: point
text*[testtest7::class_inv7]\<open>lorem ipsum...\<close>
print_doc_classes
doc_class class_inv8 = class_inv7 +
a1 :: "class_inv1 set"
b1 :: point
c1 :: int
text*[testtest8::class_inv8]\<open>lorem ipsum...\<close>
ML\<open>
val pt1 = @{term "pt1"}
(*val thy = @{theory}*)
val {input_term,...} = the (DOF_core.get_object_global "testtest" @{theory})
(*val {input_term,...} = the (DOF_core.get_object_global "introduction2" @{theory})*)
(*val {input_term,...} = the (DOF_core.get_object_global "testtest3" @{theory})*)
(*val {input_term,...} = the (DOF_core.get_object_global "testtest4" @{theory})*)
val update $ abs $ record = input_term
val make $ tag $ attr = record
\<close>
term\<open>(1::int) + aaaa::int\<close>
term \<open>class_inv1.make\<close>
typ\<open>'a class_inv1_scheme\<close>
find_consts name:"class_inv1"
find_theorems name:"class_inv1"
find_theorems name:"class_inv3"
ML\<open>
val thy = @{theory}
val oid = "testtest1"
val {input_term,value,cid=class_name,...} = the (DOF_core.get_object_global oid thy)
val _ = writeln(Syntax.string_of_term_global thy input_term)
val _ = writeln(Syntax.string_of_term_global thy value)
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
val class_list = DOF_core.get_attributes class_name thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list' = rev (attrs_filter (rev class_list))
val update_name = "High_Level_Syntax_Invariants.class_inv1.int1_update"
val bname = Long_Name.base_name update_name
val attr_name = String.extract (bname, 0, SOME (String.size(bname) - String.size(Record.updateN)))
val term = Const ("Groups.zero_class.zero", @{typ "int"})
val term = Bound 0
fun normalize attr_name term attr =
let
val (attr_id, ty, term_option) = attr
in
if (Binding.name_of attr_id = attr_name)
then
(attr_id, ty, SOME term)
else attr
end
val class_list_test = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (normalize attr_name term) attr_list) end) class_list'
val qual = Long_Name.qualifier update_name
\<close>
ML\<open>
val thy = @{theory}
val oid = "testtest2"
val {input_term,cid=class_name,...} = the (DOF_core.get_object_global oid thy)
val _ = writeln(Syntax.string_of_term_global thy input_term)
val t = DOF_core.is_subclass_global thy "High_Level_Syntax_Invariants.class_inv2" "High_Level_Syntax_Invariants.class_inv1"
\<close>
ML\<open>
val thy = @{theory}
val oid = "testtest2"
val {input_term,cid=class_name,...} = the (DOF_core.get_object_global oid thy)
val _ = writeln(Syntax.string_of_term_global thy input_term)
val (Const(update_name,typ) $ Abs(s, typ', term') $ term) = input_term
val Type(s, [t, u]) = typ
val T = Syntax.read_typ_global thy class_name
val T' = T --> T
val test = u = T'
\<close>
ML\<open>
val thy = @{theory}
val oid = "testtest2"
val oid = "testinv2"
val {input_term,cid=class_name,...} = the (DOF_core.get_object_global oid thy)
val _ = writeln(Syntax.string_of_term_global thy input_term)
val class_list = DOF_core.get_attributes class_name thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list' = rev (attrs_filter (rev class_list))
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name
val class_list'' = map (fn (string, attrs) =>
(string , map (fn (binding, typ, term_option) =>
case term_option of
NONE => let
val term = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
in (binding, typ, [term]) end
| SOME (term) => (binding, typ, [term])) attrs))
class_list'
val (Const(update_name,typ) $ Abs(s, typ', term') $ term) = input_term
val update_bname = Long_Name.base_name update_name
val attr_name = String.extract (update_bname, 0, SOME (String.size(update_bname) - String.size(Record.updateN)))
val update_qual = Long_Name.qualifier update_name
val (Const(make_name, typ''), ts)= strip_comb term
val make_bname = Long_Name.base_name make_name
val make_qual = Long_Name.qualifier make_name
fun update_class_term_list attr_name term attr =
let
val (attr_id, ty, term_list) = attr
in
if (Binding.name_of attr_id = attr_name)
then
(attr_id, ty, term_list @ [term])
else attr
end
val class_list''' = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (update_class_term_list attr_name term') attr_list) end) class_list''
val (Const(update_name,typ) $ Abs(s, typ', term') $ term) = term
val (Const(make_name, typ''), ts)= strip_comb term
val make_bname' = Long_Name.base_name make_name
val make_qual' = Long_Name.qualifier make_name
(*val (Const(make_name, typ''), ts)= strip_comb term
val make_bname = Long_Name.base_name make_name
val make_qual = Long_Name.qualifier make_name
*)
fun normalize_term [term] = term
| normalize_term (x::y::xs) =
case y of
\<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close> $ Bound 0 $ t =>
(*let val (T, i) = HOLogic.dest_number x
val (T',j) = HOLogic.dest_number t*)
let val evaluated_term = Value_Command.value @{context} (\<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close> $ x $ t)
(*in normalize_term ((HOLogic.mk_number T (i + j))::xs) end*)
in normalize_term (evaluated_term::xs) end
(*| \<^Const>\<open>Lattices.sup_class.sup \<^Type>\<open>set \<^typ>\<open>_\<close>\<close>\<close> $ Bound 0 $ t =>
Value_Command.value*)
| _ => normalize_term (y::xs)
val tag_attr = HOLogic.mk_number @{typ "int"}
fun add_tag_to_attrs tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (tag_attr (serial ()))::map (fn (binding, ty, term) => term) filtered_attr_list
else map (fn (binding, ty, term) => term) filtered_attr_list
fun update_class_term_list attr_name term attr =
let
val (attr_id, ty, term_list) = attr
in
if (Binding.name_of attr_id = attr_name)
then
(attr_id, ty, term_list @ [term])
else attr
end
(*val class_list4 = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (update_class_term_list attr_name term') attr_list) end) class_list'''
val _ = writeln ("In normalize_record update class_list': " ^ @{make_string} class_list4)*)
val class_list5 = map
(fn (string, attrs) =>
(string, map (fn (binding, ty, ts) =>
(binding, ty, normalize_term ts)) attrs)) class_list'''
val class_list6 = flat (map (add_tag_to_attrs tag_attr thy) class_list5)
\<close>
print_doc_items
ML\<open>
val thy = @{theory}
val oid = "testtest3"
val oid = "testinv2"
val {input_term,cid=class_name,...} = the (DOF_core.get_object_global oid thy)
val _ = writeln(Syntax.string_of_term_global thy input_term)
(*val a $ b $ c = input_term*)
(*val d $ e $ f = c*)
(*val test_striped = strip_comb f*)
(*val u $ t = f*)
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
val class_list = DOF_core.get_attributes class_name thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list' = rev (attrs_filter (rev class_list))
val class_list'' = map (fn (string, attrs) =>
(string , map (fn (binding, typ, term_option) =>
case term_option of
NONE => let
val term = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
in (binding, typ, [term]) end
| SOME (term) => (binding, typ, [term])) attrs))
class_list'
(*val class_list_test' = map (fn (s, [(b, ty, toption)]) => (s, [(b, ty, [toption])])) class_list'*)
fun normalize_record (Const(update_name, Type(s, [t, u])) $ Abs(_, typ', term') $ term) class_list cid thy =
let
val _ = writeln ("AAAAAAAAAAAAA")
(* I also must check the class to rule out updates of standard record
see testtest3 *)
val update_bname = Long_Name.base_name update_name
val attr_name = String.extract (update_bname, 0, SOME (String.size(update_bname) - String.size(Record.updateN)))
val update_qual = Long_Name.qualifier update_name
val class_typ = Syntax.read_typ_global thy class_name
val class_typ' = class_typ --> class_typ
(*val (Const(make_name, typ''), ts)= strip_comb term
val make_bname = Long_Name.base_name make_name
val make_qual = Long_Name.qualifier make_name*)
in
if (String.isSuffix Record.updateN update_bname andalso
(update_qual = cid orelse
(DOF_core.is_subclass_global thy cid update_qual andalso class_typ' = u))
(*andalso make_bname = makeN andalso make_qual = cid*))
then
let
val (Const(make_name, typ''), ts)= strip_comb term
val make_bname = Long_Name.base_name make_name
val make_qual = Long_Name.qualifier make_name
in
if (make_bname = makeN andalso make_qual = cid)
then
let
fun normalize_attribute [term] = term
| normalize_attribute (x::y::xs) =
case y of
\<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close> $ Bound 0 $ t =>
(*let val (T, i) = HOLogic.dest_number x
val (T',j) = HOLogic.dest_number t*)
let val evaluated_term = Value_Command.value @{context} (\<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close> $ x $ t)
(*in normalize_attribute ((HOLogic.mk_number T (i + j))::xs) end*)
in normalize_attribute (evaluated_term::xs) end
(*| \<^Const>\<open>Lattices.sup_class.sup \<^Type>\<open>set \<^typ>\<open>_\<close>\<close>\<close> $ Bound 0 $ t =>
Value_Command.value*)
| _ => normalize_attribute (y::xs)
val tag_attr = HOLogic.mk_number @{typ "int"}
fun add_tag_to_attrs tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (tag_attr (serial ()))::map (fn (binding, ty, term) => term) filtered_attr_list
else map (fn (binding, ty, term) => term) filtered_attr_list
val class_list'' = map
(fn (string, attrs) =>
(string, map (fn (binding, ty, ts) =>
(binding, ty, normalize_attribute ts)) attrs)) class_list
val class_list''' = flat (map (add_tag_to_attrs tag_attr thy) class_list'')
(*val make_const = Syntax.read_term_global thy (Long_Name.qualify cid makeN);*)
in list_comb (Const(make_name, typ''), (tag_attr (serial()))::class_list''') end
(*in error ("BBBBBBB") end*)
else
let
fun update_class_term_list attr_name term attr =
let
val (attr_id, ty, term_list) = attr
in
if (Binding.name_of attr_id = attr_name)
then
(attr_id, ty, term_list @ [term])
else attr
end
val class_list' = map
(fn class =>
let val (cid, attr_list) = class
in (cid, map (update_class_term_list attr_name term') attr_list) end) class_list
val _ = writeln ("In normalize_record update class_list': " ^ @{make_string} class_list')
in normalize_record term class_list' cid thy end
end
(*in
normalize_record term class_list' cid thy
(*(Const(update_name,typ) $ abs) :: normalize_record term cid updates thy*)
end*)
else normalize_record term class_list cid thy
end
| normalize_record (t1 $ t2) class_list cid thy =
(normalize_record t1 class_list cid thy) $ (normalize_record t2 class_list cid thy)
| normalize_record t class_list cid thy = t
val record = normalize_record input_term class_list'' class_name thy
val _ = writeln(Syntax.string_of_term_global thy record)
(*val class_int'' = normalize_record input_term class_list_test' class_name thy*)
\<close>
term\<open>class_inv1.make 5798756 4\<close>
value\<open>class_inv1.make 5798756 4\<close>
term\<open>class_inv2.make 5813388 1 (High_Level_Syntax_Invariants_class_inv2_int2_Attribute_Not_Initialized + 1)\<close>
value\<open>class_inv2.make 5813388 1 (High_Level_Syntax_Invariants_class_inv2_int2_Attribute_Not_Initialized + 1)\<close>
term*\<open>class_inv3.make
5862176
{@{class-inv1 ''testtest''}, @{class-inv1 ''testtest1''}}
(\<lparr>point.xcoord = 1, ycoord = 2\<rparr>\<lparr>point.xcoord := 2\<rparr>)\<close>
value*\<open>class_inv3.make
5862176
{@{class-inv1 ''testtest''}, @{class-inv1 ''testtest1''}}
(\<lparr>point.xcoord = 1, ycoord = 2\<rparr>\<lparr>point.xcoord := 2\<rparr>)\<close>
value\<open>List.coset [(1::int), 2]\<close>
value\<open>- set [(1::int), 2]\<close>
ML\<open>
val t = \<^const_name>\<open>Lattices.sup\<close>
(*val t = Type(\<^type_name>\<open>set\<close>, _)*)
val tt = \<^Type>\<open>set \<^typ>\<open>'a\<close>\<close>
(*val ttt = tttt as Type(@{type_name "set"},_)*)
\<close>
find_consts name:"Groups.plus_class.plus"
find_consts name:"Nil"
find_theorems name:"ISA_docitem"
find_theorems name:"ISA_thm"
value\<open>Cons (1::int) Nil\<close>
doc_class lattice_test =
attr_lattice :: "int set" <= "{1}"
text*[lattice_test_instance::lattice_test, attr_lattice ="{2}"]\<open>\<close>
update_instance*[lattice_test_instance::lattice_test, attr_lattice +="{3}"]
value\<open>sup (1::int) 2\<close>
value\<open>sup (sup (sup {1::int} {2}) {3}) {4}\<close>
value\<open>sup (sup {1::int} {2}) {3}\<close>
value\<open>sup {1::int} {2}\<close>
value\<open>inf (inf {1::int} {2}) {3}\<close>
value*\<open>attr_lattice @{lattice-test \<open>lattice_test_instance\<close>}\<close>
ML\<open>
val t = \<^term>\<open>(3::int) + 4\<close>
(*val tt = @{value "3 + 4"}*)
\<close>
ML\<open>
val t = HOLogic.mk_number \<^typ>\<open>int\<close> 12
val tt = HOLogic.dest_number t
\<close>
ML\<open>
val t = \<^Const>\<open>Groups.plus_class.plus \<^typ>\<open>int\<close>\<close>
\<close>
ML\<open>
val t = \<^Const>\<open>Isa_DOF.ISA_docitem \<^Type>\<open>nat\<close>\<close>
\<close>
ML\<open>
val t = \<^Const>\<open>Nil \<^typ>\<open>int\<close>\<close>
val tt = \<^Const>\<open>Cons \<^Type>\<open>int\<close>\<close>
\<close>
ML\<open>
fn (A, B) => \<^Const>\<open>conj for A B\<close>
\<close>
ML\<open>
val T1 = \<^typ>\<open>int \<Rightarrow> int \<Rightarrow> int\<close>
val T2 = \<^typ>\<open>int list\<close>
val t = Const (\<^const_name>\<open>Groups.plus\<close>, T1)
(*val tt = \<^const>\<open>Nil\<close> $ \<^typ>\<open>int list\<close>*)
val tt = \<^const>\<open>Isa_DOF.ISA_thm\<close> $ (HOLogic.mk_string "test")
(*val nil = \<^const>\<open>Nil\<close> $ \<^typ>\<open>int =>\<close>*)
val term = \<^term>\<open>Cons\<close>
val nil' = Const ("List.list.Nil", T2);
(*val ts = \<^const>\<open>Cons\<close> $ @{term "1::int"} $ \<^const>\<open>Nil\<close>*)
val t = @{typ "int \<Rightarrow> int"}
(*val tt = \<^const>\<open>Groups.plus_class.plus\<close> $ \<^typ>\<open>int \<Rightarrow> int \<Rightarrow> int\<close>*)
\<close>
ML\<open>
(*val thy = @{theory}*)
(*val t = [@{typ "class_inv1 set"} --> @{typ "class_inv1 set"}, @{typ "class_inv3"}] ---> @{typ "class_inv3"}*)
(*val t = @{typ "(class_inv1 set \<Rightarrow> class_inv1 set) \<Rightarrow> class_inv3 \<Rightarrow> class_inv3"}*)
(*val Type(n, [t]) = @{typ "(class_inv1 set \<Rightarrow> class_inv1 set) \<Rightarrow> class_inv3 \<Rightarrow> class_inv3"}*)
(*val Type(n1,[t1,t2]) = t*)
(*val cid = Long_Name.qualifier n1*)
(*val testesees = DOF_core.is_defined_cid_global cid thy*)
val thy = @{theory}
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val oid = "testtest3"
val {input_term,cid,...} = the (DOF_core.get_object_global "testtest0" @{theory})
(*val (Const(t, u)) $ v = input_term*)
val Const(s, typ) $ abs $ t = input_term
val Const(name, typ) = fst (strip_comb t)
(*val test = Free ("High_Level_Syntax_Invariants_class_inv1_int1_Attribute_Not_Initialized", @{typ int})*)
(*val test' = strip_comb test*)
(*val u $ v $ w = t*)
(*val {input_term,...} = the (DOF_core.get_object_global "introduction2" @{theory})*)
(*val {input_term,cid,...} = the (DOF_core.get_object_global oid @{theory})*)
(*val {input_term,...} = the (DOF_core.get_object_global "testtest4" @{theory})*)
(*val input_term = @{term "1::int"}*)
val _ = writeln(Syntax.string_of_term_global thy input_term)
val elaborated_term = DOF_core.transduce_term_global {mk_elaboration=true} (input_term,\<^here>) thy
val _ = writeln(Syntax.string_of_term_global thy elaborated_term)
fun test_normalize_record (Const(update_name,typ) $ Abs(s, typ', term') $ term) cid updates thy =
let
val _ = writeln ("AAAAAAAAAAAAA")
(* I also must check the class to rule out updates of standard record
see testtest3 *)
val bname = Long_Name.base_name update_name
val qual = Long_Name.qualifier update_name
in
if (String.isSuffix Record.updateN bname andalso qual = cid)
then
let
val _ = writeln(Syntax.string_of_term_global thy term)
val Const(make_name, typ) $ t = term
val bname = Long_Name.base_name make_name
val qual = Long_Name.qualifier make_name
in
(*test_normalize_record term cid (Const(update_name,typ) $ Abs(s, typ', term')::updates) thy*)
if (bname = makeN andalso qual = cid)
then term
else term
end
(*(Const(update_name,typ) $ abs) :: normalize_record' term cid updates thy*)
else
(*test_normalize_record term cid updates thy*)
term
end
| test_normalize_record t cid updates thy = t
(*val (Const(update_name,typ) $ Abs(s, typ', term') $ term) = input_term*)
val updated_term = test_normalize_record input_term "class_inv1" "" thy
(*val a $ b = input_term*)
(*val (Const(nameeee,typeeee) $ termeeee) = input_term*)
(*val (Const(isa_class_nameeee,typeeee) $ abseee $ termeeee) = input_term*)
(*val a' $ b' $ c' = elaborated_term*)
(*val Const(updatee,typee) $ absee $ termee = input_term*)
(*val Const(updateee,typeee) $ abseee $ termeee = termee*)
(*val bnamee = Long_Name.base_name updatee*)
(*val long_cid = Long_Name.qualifier updatee*)
(*val class_list' = DOF_core.get_attributes long_cid thy*)
val class_list' = DOF_core.get_attributes cid thy
val class_list'' = rev (attrs_filter (rev class_list'))
fun normalize_record
(Const(name,typ) $ term) cid updates thy =
if DOF_core.is_class_ISA thy name
then
let val instance_name = HOLogic.dest_string term
val input_term = #input_term (the (DOF_core.get_object_global instance_name thy))
val elaborated_term = DOF_core.transduce_term_global {mk_elaboration=true} (input_term, \<^here>) thy
val bname = Long_Name.base_name name
val qual = Long_Name.qualifier name
val class_name = DOF_core.get_class_name_without_prefix bname
val long_cid = Long_Name.qualify qual class_name
in normalize_record elaborated_term long_cid [] thy end
else Const(name,typ) $ normalize_record term cid updates thy
| normalize_record (Const(update_name,typ) $ Abs(s, typ', term') $ term) cid updates thy = let
val _ = writeln ("AAAAAAAAAAAAA")
(* I also must check the class to rule out updates of standrard record
see testtest3 *)
val bname = Long_Name.base_name update_name
val qual = Long_Name.qualifier update_name
in
if (String.isSuffix Record.updateN bname andalso qual = cid)
then
normalize_record term cid (Const(update_name,typ) $ Abs(s, typ', term')::updates) thy
(*(Const(update_name,typ) $ abs) :: normalize_record term cid updates thy*)
else normalize_record term cid updates thy
end
| normalize_record (Const(name,typ)) cid updates thy =
let
val bname = Long_Name.base_name name
val qual = Long_Name.qualifier name
in if (bname = makeN andalso qual = cid)
then
let
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) cid
val make_const = Syntax.read_term_global thy name
fun attr_to_free (binding, typ, term_option) updates =
case term_option of
NONE => ()
| SOME (term) => ()
(*Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)*)
val class_list' = DOF_core.get_attributes cid thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list'' = rev (attrs_filter (rev class_list'))
fun tag_attr class_name = HOLogic.mk_string (class_name ^ "_tag_attribute")
fun add_tag_to_attrs_free' tag_attr thy (cid, filtered_attr_list) =
let val _ = writeln ("In create_default_object cid: " ^ cid)
val _ = writeln ("In create_default_object filtered_attr_list: " ^ @{make_string} filtered_attr_list)
in
if DOF_core.is_virtual cid thy
then (tag_attr cid)::(map (attr_to_free) filtered_attr_list)
(*then (map (attr_to_free) filtered_attr_list)*)
else (map (attr_to_free) filtered_attr_list)
end
(*fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
*)
in
Const(name,typ) $ normalize_record elaborated_term cid updates thy
end
else Const(name,typ) end
| normalize_record (t $ t') cid updates thy =
normalize_record t cid updates thy $ normalize_record t' cid updates thy
| normalize_record (Abs(s, ty, t)) cid updates thy = Abs (s, ty, normalize_record t cid updates thy)
| normalize_record t cid updates thy = t
fun normalize_record'
(Const(name,typ) $ term) cid updates thy =
if DOF_core.is_class_ISA thy name
then
let val instance_name = HOLogic.dest_string term
val input_term = #input_term (the (DOF_core.get_object_global instance_name thy))
val elaborated_term = DOF_core.transduce_term_global {mk_elaboration=true} (input_term, \<^here>) thy
val bname = Long_Name.base_name name
val qual = Long_Name.qualifier name
val class_name = DOF_core.get_class_name_without_prefix bname
val long_cid = Long_Name.qualify qual class_name
in normalize_record' elaborated_term long_cid [] thy end
else Const(name,typ) $ normalize_record' term cid updates thy
| normalize_record' (Const(update_name,typ) $ Abs(s, typ', term') $ term) cid updates thy = let
val _ = writeln ("AAAAAAAAAAAAA")
(* I also must check the class to rule out updates of standrard record
see testtest3 *)
val bname = Long_Name.base_name update_name
val qual = Long_Name.qualifier update_name
in
if (String.isSuffix Record.updateN bname andalso qual = cid)
then
normalize_record' term cid (Const(update_name,typ) $ Abs(s, typ', term')::updates) thy
(*(Const(update_name,typ) $ abs) :: normalize_record' term cid updates thy*)
else normalize_record' term cid updates thy
end
| normalize_record' (Const(name,typ)) cid updates thy =
let
val bname = Long_Name.base_name name
val qual = Long_Name.qualifier name
in if (bname = makeN andalso qual = cid)
then
let
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) cid
val make_const = Syntax.read_term_global thy name
fun attr_to_free (binding, typ, term_option) updates =
case term_option of
NONE => ()
| SOME (term) => ()
(*Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)*)
val class_list' = DOF_core.get_attributes cid thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list'' = rev (attrs_filter (rev class_list'))
fun tag_attr class_name = HOLogic.mk_string (class_name ^ "_tag_attribute")
fun add_tag_to_attrs_free' tag_attr thy (cid, filtered_attr_list) =
let val _ = writeln ("In create_default_object cid: " ^ cid)
val _ = writeln ("In create_default_object filtered_attr_list: " ^ @{make_string} filtered_attr_list)
in
if DOF_core.is_virtual cid thy
then (tag_attr cid)::(map (attr_to_free) filtered_attr_list)
(*then (map (attr_to_free) filtered_attr_list)*)
else (map (attr_to_free) filtered_attr_list)
end
(*fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
*)
in
Const(name,typ) $ normalize_record' elaborated_term cid updates thy
end
else Const(name,typ) end
| normalize_record' (t $ t') cid updates thy =
normalize_record' t cid updates thy $ normalize_record' t' cid updates thy
| normalize_record' (Abs(s, ty, t)) cid updates thy = Abs (s, ty, normalize_record' t cid updates thy)
| normalize_record' t cid updates thy = t
(*val update_list = normalize_record input_term cid [] thy*)
(*val update_list' = normalize_record elaborated_term*)
(*val temp = map (Syntax.string_of_term @{context}) update_list*)
(*val make_attribute_list = ()*)
(*val Const(make,typ) $ absee $ termee = input_term*)
(*val make_attributes = ()*)
(*val Const(update,typ) $ abs $ record = input_term*)
(*val bname = Long_Name.base_name update;*)
(*if String.isSubstring Record.updateN bname then () else ();*)
(*val class_name = Long_Name.qualifier update*)
(*val {simps,...} = the (Record.get_info thy class_name)*)
(*val attr_update_*)
\<close>
ML\<open>
open SHA1;
val class_name = "High_Level_Syntax_Invariants.class_inv5"
val sha = SHA1.digest class_name
val ttt = rep sha
\<close>
ML\<open>
val testtt = @{typ "int"}
val input_term =
Const ("High_Level_Syntax_Invariants.class_inv1.make", @{typ "int \<Rightarrow> int \<Rightarrow> class_inv1"})
$ Const ("Num.num.One", @{typ "num"})
$ Free ("High_Level_Syntax_Invariants_class_inv1_int1_Attribute_Not_Initialized", @{typ"int"})
val class_name = "High_Level_Syntax_Invariants.class_inv1"
val sha = SHA1.digest class_name
val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
^ (Binding.name_of binding)
^ "_Attribute_Not_Initialized", typ)
val class_list' = DOF_core.get_attributes class_name thy
fun attrs_filter [] = []
| attrs_filter (x::xs) =
let val (cid, ys) = x
fun is_duplicated _ [] = false
| is_duplicated y (x::xs) =
let val (_, ys) = x
in if exists (map_eq_fst_triple Binding.name_of y) ys
then true
else is_duplicated y xs end
in (cid, filter_out (fn y => is_duplicated y xs) ys)::attrs_filter xs end
val class_list'' = rev (attrs_filter (rev class_list'))
val tag_attr = HOLogic.mk_number @{typ "int"}
fun add_tag_to_attrs_free' tag_attr thy (cid, filtered_attr_list) =
if DOF_core.is_virtual cid thy
then (tag_attr (serial ()))::(map (attr_to_free) filtered_attr_list)
else (map (attr_to_free) filtered_attr_list)
val class_list'''' = flat (map (add_tag_to_attrs_free' tag_attr thy) class_list'')
\<close>
ML\<open>
val Type (s, [t]) = @{typ "class_inv7"}
val Type (s', [t']) = t
val Type (s'', [t'']) = t'
\<close>
value\<open> (1::nat) \<le> (2::nat)\<close>
typ\<open>'a High_Level_Syntax_Invariants.class_inv7.class_inv7_ext\<close>
value\<open>High_Level_Syntax_Invariants.class_inv7.make\<close>
typedecl inda
axiomatization Zeroa_Rep :: inda and Suca_Rep :: "inda \<Rightarrow> inda"
\<comment> \<open>The axiom of infinity in 2 parts:\<close>
where Suca_Rep_inject: "Suca_Rep x = Suca_Rep y \<Longrightarrow> x = y"
and Suca_Rep_not_Zero_Rep: "Suca_Rep x \<noteq> Zeroa_Rep"
inductive Nata :: "inda \<Rightarrow> bool"
where
Zero_RepI : "Nata Zeroa_Rep"
| Suc_RepI: "Nata i \<Longrightarrow> Nata (Suca_Rep i)"
typedef nataa = "{n. Nata n}"
morphisms Rep_Nata Abs_Nata
using [[simp_trace=true]]
using Nata.Zero_RepI by auto
ML\<open>
open Term;
\<close>
end

11
src/tests/Instance_Value_Normalization.thy
View File

@ -7,7 +7,7 @@ theory
imports
"Isabelle_DOF-tests.TermAntiquotations"
"Isabelle_DOF.scholarly_paper"
"Isabelle_DOF.CENELEC_50128"
(*"Isabelle_DOF.CENELEC_50128"*)
begin
(*<*)
@ -189,4 +189,13 @@ declare[[invariants_checking = false]]
declare[[invariants_checking_with_tactics = false]]
(*>*)
term \<open>-6::int\<close>
print_doc_items
ML\<open>
val t = HOLogic.mk_number @{typ "int"} (serial ())
\<close>
ML\<open>
(*val thy = @{theory}*)
val {input_term,...} = the (DOF_core.get_object_global "xcv1" @{theory})
\<close>
end

10
src/tests/TermAntiquotations.thy
View File

@ -114,5 +114,15 @@ text\<open>Unfortunately due to different lexical conventions for constant symbo
We need to substitute an hyphen "-" for the underscore "_".\<close>
term*\<open>@{text-element \<open>te\<close>}\<close>
text*[testetst::E]\<open>\<close>
print_doc_items
find_consts name:"trace_update"
ML\<open>
(*val thy = @{theory}*)
val {input_term,...} = the (DOF_core.get_object_global "aaa" @{theory})
val update $ abs $ record = input_term
val make $ tag $ attr = record
\<close>
print_doc_classes
end