40586
|
1 |
(* Title: HOL/Tools/functorial_mappers.ML
|
40582
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
|
|
4 |
Functorial mappers on types.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature FUNCTORIAL_MAPPERS =
|
|
8 |
sig
|
|
9 |
val find_atomic: theory -> typ -> (typ * (bool * bool)) list
|
|
10 |
val construct_mapper: theory -> (string * bool -> term)
|
|
11 |
-> bool -> typ -> typ -> term
|
|
12 |
val register: string -> string -> (sort * (bool * bool)) list -> thm -> thm
|
|
13 |
-> theory -> theory
|
40584
|
14 |
val type_mapper: term -> theory -> Proof.state
|
40582
|
15 |
type entry
|
|
16 |
val entries: theory -> entry Symtab.table
|
|
17 |
end;
|
|
18 |
|
|
19 |
structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
|
|
20 |
struct
|
|
21 |
|
|
22 |
(** functorial mappers and their properties **)
|
|
23 |
|
|
24 |
(* bookkeeping *)
|
|
25 |
|
|
26 |
type entry = { mapper: string, variances: (sort * (bool * bool)) list,
|
|
27 |
concatenate: thm, identity: thm };
|
|
28 |
|
|
29 |
structure Data = Theory_Data(
|
|
30 |
type T = entry Symtab.table
|
|
31 |
val empty = Symtab.empty
|
|
32 |
val merge = Symtab.merge (K true)
|
|
33 |
val extend = I
|
|
34 |
);
|
|
35 |
|
|
36 |
val entries = Data.get;
|
|
37 |
|
|
38 |
|
|
39 |
(* type analysis *)
|
|
40 |
|
|
41 |
fun find_atomic thy T =
|
|
42 |
let
|
|
43 |
val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
|
|
44 |
fun add_variance is_contra T =
|
|
45 |
AList.map_default (op =) (T, (false, false))
|
|
46 |
((if is_contra then apsnd else apfst) (K true));
|
|
47 |
fun analyze' is_contra (_, (co, contra)) T =
|
|
48 |
(if co then analyze is_contra T else I)
|
|
49 |
#> (if contra then analyze (not is_contra) T else I)
|
|
50 |
and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
|
|
51 |
of NONE => add_variance is_contra T
|
|
52 |
| SOME variances => fold2 (analyze' is_contra) variances Ts)
|
|
53 |
| analyze is_contra T = add_variance is_contra T;
|
|
54 |
in analyze false T [] end;
|
|
55 |
|
|
56 |
fun construct_mapper thy atomic =
|
|
57 |
let
|
|
58 |
val lookup = the o Symtab.lookup (Data.get thy);
|
|
59 |
fun constructs is_contra (_, (co, contra)) T T' =
|
|
60 |
(if co then [construct is_contra T T'] else [])
|
|
61 |
@ (if contra then [construct (not is_contra) T T'] else [])
|
|
62 |
and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
|
|
63 |
let
|
|
64 |
val { mapper, variances, ... } = lookup tyco;
|
|
65 |
val args = maps (fn (arg_pattern, (T, T')) =>
|
|
66 |
constructs is_contra arg_pattern T T')
|
|
67 |
(variances ~~ (Ts ~~ Ts'));
|
|
68 |
val (U, U') = if is_contra then (T', T) else (T, T');
|
|
69 |
in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
|
|
70 |
| construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
|
|
71 |
in construct end;
|
|
72 |
|
|
73 |
|
|
74 |
(* mapper properties *)
|
|
75 |
|
|
76 |
fun make_concatenate_prop variances (tyco, mapper) =
|
|
77 |
let
|
|
78 |
fun invents n k nctxt =
|
|
79 |
let
|
|
80 |
val names = Name.invents nctxt n k;
|
|
81 |
in (names, fold Name.declare names nctxt) end;
|
|
82 |
val (((vs1, vs2), vs3), _) = Name.context
|
|
83 |
|> invents Name.aT (length variances)
|
|
84 |
||>> invents Name.aT (length variances)
|
|
85 |
||>> invents Name.aT (length variances);
|
|
86 |
fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
|
|
87 |
vs variances;
|
|
88 |
val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
|
|
89 |
fun mk_argT ((T, T'), (_, (co, contra))) =
|
|
90 |
(if co then [(T --> T')] else [])
|
|
91 |
@ (if contra then [(T' --> T)] else []);
|
|
92 |
val contras = maps (fn (_, (co, contra)) =>
|
|
93 |
(if co then [false] else []) @ (if contra then [true] else [])) variances;
|
|
94 |
val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
|
|
95 |
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
|
|
96 |
val ((names21, names32), nctxt) = Name.context
|
|
97 |
|> invents "f" (length Ts21)
|
|
98 |
||>> invents "f" (length Ts32);
|
|
99 |
val T1 = Type (tyco, Ts1);
|
|
100 |
val T2 = Type (tyco, Ts2);
|
|
101 |
val T3 = Type (tyco, Ts3);
|
|
102 |
val x = Free (the_single (Name.invents nctxt "a" 1), T3);
|
|
103 |
val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
|
|
104 |
val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
|
|
105 |
if not is_contra then
|
|
106 |
Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
|
|
107 |
else
|
|
108 |
Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
|
|
109 |
) contras (args21 ~~ args32)
|
|
110 |
fun mk_mapper T T' args = list_comb (Const (mapper,
|
|
111 |
map fastype_of args ---> T --> T'), args);
|
|
112 |
val lhs = mk_mapper T2 T1 (map Free args21) $
|
|
113 |
(mk_mapper T3 T2 (map Free args32) $ x);
|
|
114 |
val rhs = mk_mapper T3 T1 args31 $ x;
|
|
115 |
in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
|
|
116 |
|
|
117 |
fun make_identity_prop variances (tyco, mapper) =
|
|
118 |
let
|
|
119 |
val vs = Name.invents Name.context Name.aT (length variances);
|
|
120 |
val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
|
|
121 |
fun bool_num b = if b then 1 else 0;
|
|
122 |
fun mk_argT (T, (_, (co, contra))) =
|
|
123 |
replicate (bool_num co + bool_num contra) (T --> T)
|
|
124 |
val Ts' = maps mk_argT (Ts ~~ variances)
|
|
125 |
val T = Type (tyco, Ts);
|
|
126 |
val x = Free ("a", T);
|
|
127 |
val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
|
|
128 |
map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
|
|
129 |
in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
|
|
130 |
|
|
131 |
|
40587
|
132 |
(* registering mappers *)
|
40582
|
133 |
|
|
134 |
fun register tyco mapper variances raw_concatenate raw_identity thy =
|
|
135 |
let
|
|
136 |
val (_, concatenate_prop) = make_concatenate_prop variances (tyco, mapper);
|
|
137 |
val (_, identity_prop) = make_identity_prop variances (tyco, mapper);
|
|
138 |
val concatenate = Goal.prove_global thy
|
|
139 |
(Term.add_free_names concatenate_prop []) [] concatenate_prop
|
|
140 |
(K (ALLGOALS (ProofContext.fact_tac [raw_concatenate])));
|
|
141 |
val identity = Goal.prove_global thy
|
|
142 |
(Term.add_free_names identity_prop []) [] identity_prop
|
|
143 |
(K (ALLGOALS (ProofContext.fact_tac [raw_identity])));
|
|
144 |
in
|
|
145 |
thy
|
|
146 |
|> Data.map (Symtab.update (tyco, { mapper = mapper,
|
|
147 |
variances = variances,
|
|
148 |
concatenate = concatenate, identity = identity }))
|
|
149 |
end;
|
|
150 |
|
40587
|
151 |
fun split_mapper_typ "fun" T =
|
|
152 |
let
|
|
153 |
val (Ts', T') = strip_type T;
|
|
154 |
val (Ts'', T'') = split_last Ts';
|
|
155 |
val (Ts''', T''') = split_last Ts'';
|
|
156 |
in (Ts''', T''', T'' --> T') end
|
|
157 |
| split_mapper_typ tyco T =
|
|
158 |
let
|
|
159 |
val (Ts', T') = strip_type T;
|
|
160 |
val (Ts'', T'') = split_last Ts';
|
|
161 |
in (Ts'', T'', T') end;
|
|
162 |
|
|
163 |
fun analyze_variances thy tyco T =
|
|
164 |
let
|
|
165 |
fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
|
|
166 |
val (Ts, T1, T2) = split_mapper_typ tyco T
|
|
167 |
handle List.Empty => bad_typ ();
|
|
168 |
val _ = pairself
|
|
169 |
((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
|
|
170 |
val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
|
|
171 |
handle TYPE _ => bad_typ ();
|
|
172 |
val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
|
|
173 |
then bad_typ () else ();
|
|
174 |
in [] end;
|
|
175 |
|
40583
|
176 |
fun gen_type_mapper prep_term raw_t thy =
|
|
177 |
let
|
40587
|
178 |
val (mapper, T) = case prep_term thy raw_t
|
|
179 |
of Const cT => cT
|
|
180 |
| t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
|
|
181 |
val _ = Type.no_tvars T;
|
|
182 |
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
|
|
183 |
| add_tycos _ = I;
|
|
184 |
val tycos = add_tycos T [];
|
|
185 |
val tyco = if tycos = ["fun"] then "fun"
|
|
186 |
else case remove (op =) "fun" tycos
|
|
187 |
of [tyco] => tyco
|
|
188 |
| _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
|
|
189 |
val variances = analyze_variances thy tyco T;
|
|
190 |
val (_, concatenate_prop) = make_concatenate_prop variances (tyco, mapper);
|
|
191 |
val (_, identity_prop) = make_identity_prop variances (tyco, mapper);
|
|
192 |
fun after_qed [[concatenate], [identity]] lthy =
|
|
193 |
lthy
|
|
194 |
|> (Local_Theory.background_theory o Data.map)
|
|
195 |
(Symtab.update (tyco, { mapper = mapper, variances = variances,
|
|
196 |
concatenate = concatenate, identity = identity }));
|
40583
|
197 |
in
|
|
198 |
thy
|
|
199 |
|> Named_Target.theory_init
|
40587
|
200 |
|> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
|
40583
|
201 |
end
|
|
202 |
|
|
203 |
val type_mapper = gen_type_mapper Sign.cert_term;
|
|
204 |
val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
|
|
205 |
|
|
206 |
val _ =
|
|
207 |
Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
|
|
208 |
(Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
|
|
209 |
|
40582
|
210 |
end;
|