5 (code forked on 5 June 2011) |
5 (code forked on 5 June 2011) |
6 |
6 |
7 Redefinition of config datatype |
7 Redefinition of config datatype |
8 *) |
8 *) |
9 |
9 |
|
10 signature NOMINAL_FUNCTION_DATA = |
|
11 sig |
|
12 |
|
13 type nominal_info = |
|
14 {is_partial : bool, |
|
15 defname : string, |
|
16 (* contains no logical entities: invariant under morphisms: *) |
|
17 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
18 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
19 case_names : string list, |
|
20 fs : term list, |
|
21 R : term, |
|
22 psimps: thm list, |
|
23 pinducts: thm list, |
|
24 simps : thm list option, |
|
25 inducts : thm list option, |
|
26 termination: thm, |
|
27 eqvts: thm list} |
|
28 |
|
29 end |
10 |
30 |
11 |
31 |
12 structure Nominal_Function_Common = |
32 structure Nominal_Function_Common = |
13 struct |
33 struct |
|
34 |
|
35 type nominal_info = |
|
36 {is_partial : bool, |
|
37 defname : string, |
|
38 (* contains no logical entities: invariant under morphisms: *) |
|
39 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
40 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
41 case_names : string list, |
|
42 fs : term list, |
|
43 R : term, |
|
44 psimps: thm list, |
|
45 pinducts: thm list, |
|
46 simps : thm list option, |
|
47 inducts : thm list option, |
|
48 termination: thm, |
|
49 eqvts: thm list} |
|
50 |
|
51 fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, |
|
52 simps, inducts, termination, defname, is_partial, eqvts} : nominal_info) phi = |
|
53 let |
|
54 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
|
55 val name = Binding.name_of o Morphism.binding phi o Binding.name |
|
56 in |
|
57 { add_simps = add_simps, case_names = case_names, |
|
58 fs = map term fs, R = term R, psimps = fact psimps, |
|
59 pinducts = fact pinducts, simps = Option.map fact simps, |
|
60 inducts = Option.map fact inducts, termination = thm termination, |
|
61 defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts } |
|
62 end |
|
63 |
|
64 structure NominalFunctionData = Generic_Data |
|
65 ( |
|
66 type T = (term * nominal_info) Item_Net.T; |
|
67 val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
|
68 val extend = I; |
|
69 fun merge tabs : T = Item_Net.merge tabs; |
|
70 ) |
|
71 |
|
72 val get_function = NominalFunctionData.get o Context.Proof; |
|
73 |
|
74 |
|
75 fun lift_morphism thy f = |
|
76 let |
|
77 val term = Drule.term_rule thy f |
|
78 in |
|
79 Morphism.thm_morphism f $> Morphism.term_morphism term |
|
80 $> Morphism.typ_morphism (Logic.type_map term) |
|
81 end |
|
82 |
|
83 fun import_function_data t ctxt = |
|
84 let |
|
85 val thy = Proof_Context.theory_of ctxt |
|
86 val ct = cterm_of thy t |
|
87 val inst_morph = lift_morphism thy o Thm.instantiate |
|
88 |
|
89 fun match (trm, data) = |
|
90 SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
|
91 handle Pattern.MATCH => NONE |
|
92 in |
|
93 get_first match (Item_Net.retrieve (get_function ctxt) t) |
|
94 end |
|
95 |
|
96 fun import_last_function ctxt = |
|
97 case Item_Net.content (get_function ctxt) of |
|
98 [] => NONE |
|
99 | (t, data) :: _ => |
|
100 let |
|
101 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
|
102 in |
|
103 import_function_data t' ctxt' |
|
104 end |
|
105 |
|
106 val all_function_data = Item_Net.content o get_function |
|
107 |
|
108 fun add_function_data (data : nominal_info as {fs, termination, ...}) = |
|
109 NominalFunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
|
110 #> Function_Common.store_termination_rule termination |
|
111 |
|
112 |
14 |
113 |
15 |
114 |
16 (* Configuration management *) |
115 (* Configuration management *) |
17 datatype nominal_function_opt |
116 datatype nominal_function_opt |
18 = Sequential |
117 = Sequential |