35 datatype flag = absF | repF |
35 datatype flag = absF | repF |
36 |
36 |
37 fun negF absF = repF |
37 fun negF absF = repF |
38 | negF repF = absF |
38 | negF repF = absF |
39 |
39 |
40 val mk_id = Const (@{const_name "id"}, dummyT) |
|
41 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
40 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
42 |
41 |
43 fun mk_compose flag (trm1, trm2) = |
42 fun mk_compose flag (trm1, trm2) = |
44 case flag of |
43 case flag of |
45 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
44 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
60 (* produces an aggregate map function for the *) |
59 (* produces an aggregate map function for the *) |
61 (* rty-part of a quotient definition; abstracts *) |
60 (* rty-part of a quotient definition; abstracts *) |
62 (* over all variables listed in vs (these variables *) |
61 (* over all variables listed in vs (these variables *) |
63 (* correspond to the type variables in rty) *) |
62 (* correspond to the type variables in rty) *) |
64 (* *) |
63 (* *) |
65 (* for example for: ?'a list *) |
64 (* for example for: (?'a list * ?'b) *) |
66 (* it produces: %a. map a *) |
65 (* it produces: %a b. prod_map (map a) b *) |
67 fun mk_mapfun ctxt vs ty = |
66 fun mk_mapfun ctxt vs rty = |
68 let |
67 let |
69 val vs' = map (mk_Free) vs |
68 val vs' = map (mk_Free) vs |
70 |
69 |
71 fun mk_mapfun_aux ty = |
70 fun mk_mapfun_aux rty = |
72 case ty of |
71 case rty of |
73 TVar _ => mk_Free ty |
72 TVar _ => mk_Free rty |
74 | Type (_, []) => mk_id |
73 | Type (_, []) => mk_identity rty |
75 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
74 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
76 | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") |
75 | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") |
77 in |
76 in |
78 fold_rev Term.lambda vs' (mk_mapfun_aux ty) |
77 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
79 end |
78 end |
80 |
79 |
81 (* looks up the (varified) rty and qty for *) |
80 (* looks up the (varified) rty and qty for *) |
82 (* a quotient definition *) |
81 (* a quotient definition *) |
83 fun get_rty_qty ctxt s = |
82 fun get_rty_qty ctxt s = |
118 raise LIFT_MATCH (space_implode " " |
117 raise LIFT_MATCH (space_implode " " |
119 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
118 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
120 end |
119 end |
121 |
120 |
122 (* produces an aggregate absrep function *) |
121 (* produces an aggregate absrep function *) |
|
122 (* *) |
|
123 (* - In case of equal types we just return the identity *) |
123 (* *) |
124 (* *) |
124 (* - In case of function types and TFrees, we recurse, taking in *) |
125 (* - In case of function types and TFrees, we recurse, taking in *) |
125 (* the first case the polarity change into account. *) |
126 (* the first case the polarity change into account. *) |
126 (* *) |
127 (* *) |
127 (* - If the type constructors are equal, we recurse for the *) |
128 (* - If the type constructors are equal, we recurse for the *) |
150 (* *) |
151 (* *) |
151 (* ('a * 'a) list / 'a bar *) |
152 (* ('a * 'a) list / 'a bar *) |
152 |
153 |
153 fun absrep_fun flag ctxt (rty, qty) = |
154 fun absrep_fun flag ctxt (rty, qty) = |
154 if rty = qty |
155 if rty = qty |
155 then mk_identity qty |
156 then mk_identity rty |
156 else |
157 else |
157 case (rty, qty) of |
158 case (rty, qty) of |
158 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
159 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
159 let |
160 let |
160 val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
161 val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
185 in |
186 in |
186 mk_compose flag (absrep_const flag ctxt s', result) |
187 mk_compose flag (absrep_const flag ctxt s', result) |
187 end |
188 end |
188 | (TFree x, TFree x') => |
189 | (TFree x, TFree x') => |
189 if x = x' |
190 if x = x' |
190 then mk_identity qty |
191 then mk_identity rty |
191 else raise (LIFT_MATCH "absrep_fun (frees)") |
192 else raise (LIFT_MATCH "absrep_fun (frees)") |
192 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
193 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
193 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
194 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
194 |
195 |
195 fun absrep_fun_chk flag ctxt (rty, qty) = |
196 fun absrep_fun_chk flag ctxt (rty, qty) = |