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 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
38 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
39 |
|
40 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
38 |
41 |
39 fun mk_compose flag (trm1, trm2) = |
42 fun mk_compose flag (trm1, trm2) = |
40 case flag of |
43 case flag of |
41 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
44 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
42 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
45 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
43 |
46 |
44 fun get_map ctxt ty_str = |
47 fun get_mapfun ctxt s = |
45 let |
48 let |
46 val thy = ProofContext.theory_of ctxt |
49 val thy = ProofContext.theory_of ctxt |
47 val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."]) |
50 val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.") |
48 val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc |
51 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
49 in |
52 in |
50 Const (mapfun, dummyT) |
53 Const (mapfun, dummyT) |
51 end |
54 end |
52 |
55 |
53 fun get_absrep_const flag ctxt _ qty = |
56 fun mk_mapfun ctxt vs ty = |
54 (* FIXME: check here that the type-constructors of _ and qty are related *) |
57 let |
|
58 val vs' = map (mk_Free) vs |
|
59 |
|
60 fun mk_mapfun_aux ty = |
|
61 case ty of |
|
62 TVar _ => mk_Free ty |
|
63 | Type (_, []) => mk_id |
|
64 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
|
65 | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") |
|
66 in |
|
67 fold_rev Term.lambda vs' (mk_mapfun_aux ty) |
|
68 end |
|
69 |
|
70 fun get_rty_qty ctxt s = |
55 let |
71 let |
56 val thy = ProofContext.theory_of ctxt |
72 val thy = ProofContext.theory_of ctxt |
57 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
73 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
|
74 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
|
75 in |
|
76 (#rtyp qdata, #qtyp qdata) |
|
77 end |
|
78 |
|
79 fun double_lookup rtyenv qtyenv v = |
|
80 let |
|
81 val v' = fst (dest_TVar v) |
|
82 in |
|
83 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
|
84 end |
|
85 |
|
86 fun absrep_const flag ctxt qty_str = |
|
87 let |
|
88 val thy = ProofContext.theory_of ctxt |
|
89 val qty_name = Long_Name.base_name qty_str |
58 in |
90 in |
59 case flag of |
91 case flag of |
60 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
92 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
61 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
93 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
62 end |
94 end |
63 |
95 |
64 fun absrep_fun flag ctxt (rty, qty) = |
96 fun absrep_fun flag ctxt (rty, qty) = |
65 if rty = qty then mk_identity qty else |
97 if rty = qty |
66 case (rty, qty) of |
98 then mk_identity qty |
67 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
99 else |
68 let |
100 case (rty, qty) of |
69 val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
101 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
70 val arg2 = absrep_fun flag ctxt (ty2, ty2') |
102 let |
71 in |
103 val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
72 list_comb (get_map ctxt "fun", [arg1, arg2]) |
104 val arg2 = absrep_fun flag ctxt (ty2, ty2') |
73 end |
105 in |
74 | (Type (s, _), Type (s', [])) => |
106 list_comb (get_mapfun ctxt "fun", [arg1, arg2]) |
75 if s = s' |
107 end |
76 then mk_identity qty |
108 | (Type (s, tys), Type (s', tys')) => |
77 else get_absrep_const flag ctxt rty qty |
|
78 | (Type (s, tys), Type (s', tys')) => |
|
79 let |
|
80 val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
|
81 val result = list_comb (get_map ctxt s, args) |
|
82 in |
|
83 if s = s' |
109 if s = s' |
84 then result |
110 then |
85 else mk_compose flag (get_absrep_const flag ctxt rty qty, result) |
111 let |
86 end |
112 val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
87 | (TFree x, TFree x') => |
113 in |
88 if x = x' |
114 list_comb (get_mapfun ctxt s, args) |
89 then mk_identity qty |
115 end |
90 else raise (LIFT_MATCH "absrep_fun (frees)") |
116 else |
91 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
117 let |
92 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
118 val thy = ProofContext.theory_of ctxt |
|
119 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 |
|
121 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
|
122 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
123 val args = map (absrep_fun flag ctxt) args_aux |
|
124 val map_fun = mk_mapfun ctxt vs rty_pat |
|
125 val result = list_comb (map_fun, args) |
|
126 in |
|
127 mk_compose flag (absrep_const flag ctxt s', result) |
|
128 end |
|
129 | (TFree x, TFree x') => |
|
130 if x = x' |
|
131 then mk_identity qty |
|
132 else raise (LIFT_MATCH "absrep_fun (frees)") |
|
133 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
|
134 | _ => |
|
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 |
93 |
141 |
94 fun absrep_fun_chk flag ctxt (rty, qty) = |
142 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 |
95 absrep_fun flag ctxt (rty, qty) |
150 absrep_fun flag ctxt (rty, qty) |
96 |> Syntax.check_term ctxt |
151 |> Syntax.check_term ctxt |
97 |
152 end |
98 |
153 |
99 (* Regularizing an rtrm means: |
154 (* Regularizing an rtrm means: |
100 |
155 |
101 - Quantifiers over types that need lifting are replaced |
156 - Quantifiers over types that need lifting are replaced |
102 by bounded quantifiers, for example: |
157 by bounded quantifiers, for example: |