19 |
19 |
20 open Quotient_Info; |
20 open Quotient_Info; |
21 |
21 |
22 exception LIFT_MATCH of string |
22 exception LIFT_MATCH of string |
23 |
23 |
24 (*******************************) |
24 (******************************) |
25 (* Aggregate Rep/Abs Functions *) |
25 (* Aggregate Rep/Abs Function *) |
26 (*******************************) |
26 (******************************) |
27 |
27 |
28 (* The flag repF is for types in negative position, while absF is *) |
28 (* The flag repF is for types in negative position; absF is for types *) |
29 (* for types in positive position. Because of this, function types *) |
29 (* in positive position. Because of this, function types need to be *) |
30 (* need to be treated specially, since there the polarity changes. *) |
30 (* treated specially, since there the polarity changes. *) |
31 |
31 |
32 datatype flag = absF | repF |
32 datatype flag = absF | repF |
33 |
33 |
34 fun negF absF = repF |
34 fun negF absF = repF |
35 | negF repF = absF |
35 | negF repF = absF |
36 |
36 |
37 val mk_id = Const (@{const_name "id"}, dummyT) |
37 val mk_id = Const (@{const_name "id"}, dummyT) |
38 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
38 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
39 |
39 |
|
40 (* makes a Free out of a TVar *) |
40 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
41 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
41 |
42 |
42 fun mk_compose flag (trm1, trm2) = |
43 fun mk_compose flag (trm1, trm2) = |
43 case flag of |
44 case flag of |
44 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
45 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
51 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
52 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
52 in |
53 in |
53 Const (mapfun, dummyT) |
54 Const (mapfun, dummyT) |
54 end |
55 end |
55 |
56 |
|
57 (* produces an aggregate map function for the *) |
|
58 (* rty-part of a quotient definition; abstracts *) |
|
59 (* over all variables listed in vs (these variables *) |
|
60 (* correspond to the type variables in rty *) |
56 fun mk_mapfun ctxt vs ty = |
61 fun mk_mapfun ctxt vs ty = |
57 let |
62 let |
58 val vs' = map (mk_Free) vs |
63 val vs' = map (mk_Free) vs |
59 |
64 |
60 fun mk_mapfun_aux ty = |
65 fun mk_mapfun_aux ty = |
65 | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") |
70 | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") |
66 in |
71 in |
67 fold_rev Term.lambda vs' (mk_mapfun_aux ty) |
72 fold_rev Term.lambda vs' (mk_mapfun_aux ty) |
68 end |
73 end |
69 |
74 |
|
75 (* looks up the (varified) rty and qty for *) |
|
76 (* a quotient definition *) |
70 fun get_rty_qty ctxt s = |
77 fun get_rty_qty ctxt s = |
71 let |
78 let |
72 val thy = ProofContext.theory_of ctxt |
79 val thy = ProofContext.theory_of ctxt |
73 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
80 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
74 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
81 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
75 in |
82 in |
76 (#rtyp qdata, #qtyp qdata) |
83 (#rtyp qdata, #qtyp qdata) |
77 end |
84 end |
78 |
85 |
|
86 (* receives two type-environments and looks *) |
|
87 (* up in both of them the variable v *) |
79 fun double_lookup rtyenv qtyenv v = |
88 fun double_lookup rtyenv qtyenv v = |
80 let |
89 let |
81 val v' = fst (dest_TVar v) |
90 val v' = fst (dest_TVar v) |
82 in |
91 in |
83 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
92 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
84 end |
93 end |
85 |
94 |
|
95 (* produces the rep or abs constants for a qty *) |
86 fun absrep_const flag ctxt qty_str = |
96 fun absrep_const flag ctxt qty_str = |
87 let |
97 let |
88 val thy = ProofContext.theory_of ctxt |
98 val thy = ProofContext.theory_of ctxt |
89 val qty_name = Long_Name.base_name qty_str |
99 val qty_name = Long_Name.base_name qty_str |
90 in |
100 in |
91 case flag of |
101 case flag of |
92 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
102 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
93 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
103 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
94 end |
104 end |
|
105 |
|
106 (* produces the aggregate absrep function *) |
|
107 (* *) |
|
108 (* - In case of function types and TFrees, we recurse, taking in *) |
|
109 (* the first case the polarity change into account. *) |
|
110 (* *) |
|
111 (* - If the type constructors are equal, we recurse for the *) |
|
112 (* arguments and prefix the appropriate map function *) |
|
113 (* *) |
|
114 (* - If the type constructors are unequal, there must be an *) |
|
115 (* instance of quotient types: *) |
|
116 (* - we first look up the corresponding rty_pat and qty_pat *) |
|
117 (* from the quotient definition; the arguments of qty_pat *) |
|
118 (* must be some distinct TVars *) |
|
119 (* - we then match the rty_pat with rty and qty_pat with qty; *) |
|
120 (* if matching fails the types do not match *) |
|
121 (* - the matching produces two environments, we look up the *) |
|
122 (* assignments for the qty_pat variables and recurse on the *) |
|
123 (* assignmetnts *) |
|
124 (* - we prefix the aggregate map function for the rty_pat, *) |
|
125 (* which is an abstraction over all type variables *) |
|
126 (* - finally we compse the result with the appropriate *) |
|
127 (* absrep function *) |
|
128 (* *) |
|
129 (* The composition is necessary for types like *) |
|
130 (* *) |
|
131 (* ('a list) list / ('a foo) foo *) |
|
132 (* *) |
|
133 (* The matching is necessary for types like *) |
|
134 (* *) |
|
135 (* ('a * 'a) list / 'a bar *) |
95 |
136 |
96 fun absrep_fun flag ctxt (rty, qty) = |
137 fun absrep_fun flag ctxt (rty, qty) = |
97 if rty = qty |
138 if rty = qty |
98 then mk_identity qty |
139 then mk_identity qty |
99 else |
140 else |
114 list_comb (get_mapfun ctxt s, args) |
155 list_comb (get_mapfun ctxt s, args) |
115 end |
156 end |
116 else |
157 else |
117 let |
158 let |
118 val thy = ProofContext.theory_of ctxt |
159 val thy = ProofContext.theory_of ctxt |
|
160 val exc = (LIFT_MATCH "absrep_fun (Types do not match.)") |
119 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
161 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
120 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
162 val (rtyenv, qtyenv) = |
121 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
163 (Sign.typ_match thy (rty_pat, rty) Vartab.empty, |
|
164 Sign.typ_match thy (qty_pat, qty) Vartab.empty) |
|
165 handle MATCH_TYPE => raise exc |
122 val args_aux = map (double_lookup rtyenv qtyenv) vs |
166 val args_aux = map (double_lookup rtyenv qtyenv) vs |
123 val args = map (absrep_fun flag ctxt) args_aux |
167 val args = map (absrep_fun flag ctxt) args_aux |
124 val map_fun = mk_mapfun ctxt vs rty_pat |
168 val map_fun = mk_mapfun ctxt vs rty_pat |
125 val result = list_comb (map_fun, args) |
169 val result = list_comb (map_fun, args) |
126 in |
170 in |
129 | (TFree x, TFree x') => |
173 | (TFree x, TFree x') => |
130 if x = x' |
174 if x = x' |
131 then mk_identity qty |
175 then mk_identity qty |
132 else raise (LIFT_MATCH "absrep_fun (frees)") |
176 else raise (LIFT_MATCH "absrep_fun (frees)") |
133 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
177 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
134 | _ => |
178 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
135 let |
|
136 val rty_str = Syntax.string_of_typ ctxt rty |
|
137 val qty_str = Syntax.string_of_typ ctxt qty |
|
138 in |
|
139 raise (LIFT_MATCH ("absrep_fun (default) " ^ rty_str ^ " " ^ qty_str)) |
|
140 end |
|
141 |
179 |
142 fun absrep_fun_chk flag ctxt (rty, qty) = |
180 fun absrep_fun_chk flag ctxt (rty, qty) = |
143 let |
|
144 val rty_str = Syntax.string_of_typ ctxt rty |
|
145 val qty_str = Syntax.string_of_typ ctxt qty |
|
146 val _ = tracing "rty / qty" |
|
147 val _ = tracing rty_str |
|
148 val _ = tracing qty_str |
|
149 in |
|
150 absrep_fun flag ctxt (rty, qty) |
181 absrep_fun flag ctxt (rty, qty) |
151 |> Syntax.check_term ctxt |
182 |> Syntax.check_term ctxt |
152 end |
183 |
153 |
184 |
154 (* Regularizing an rtrm means: |
185 (* Regularizing an rtrm means: |
155 |
186 |
156 - Quantifiers over types that need lifting are replaced |
187 - Quantifiers over types that need lifting are replaced |
157 by bounded quantifiers, for example: |
188 by bounded quantifiers, for example: |