equal
deleted
inserted
replaced
38 | negF repF = absF |
38 | negF repF = absF |
39 |
39 |
40 val mk_id = Const (@{const_name "id"}, dummyT) |
40 val mk_id = Const (@{const_name "id"}, dummyT) |
41 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
41 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
42 |
42 |
43 (* makes a Free out of a TVar *) |
|
44 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
|
45 |
|
46 fun mk_compose flag (trm1, trm2) = |
43 fun mk_compose flag (trm1, trm2) = |
47 case flag of |
44 case flag of |
48 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
45 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
49 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
46 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
50 |
47 |
55 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
52 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
56 in |
53 in |
57 Const (mapfun, dummyT) |
54 Const (mapfun, dummyT) |
58 end |
55 end |
59 |
56 |
|
57 (* makes a Free out of a TVar *) |
|
58 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
|
59 |
60 (* produces an aggregate map function for the *) |
60 (* produces an aggregate map function for the *) |
61 (* rty-part of a quotient definition; abstracts *) |
61 (* rty-part of a quotient definition; abstracts *) |
62 (* over all variables listed in vs (these variables *) |
62 (* over all variables listed in vs (these variables *) |
63 (* correspond to the type variables in rty) *) |
63 (* correspond to the type variables in rty) *) |
|
64 (* *) |
|
65 (* for example for: ?'a list *) |
|
66 (* it produces: %a. map a *) |
|
67 (* |
64 fun mk_mapfun ctxt vs ty = |
68 fun mk_mapfun ctxt vs ty = |
65 let |
69 let |
66 val vs' = map (mk_Free) vs |
70 val vs' = map (mk_Free) vs |
67 |
71 |
68 fun mk_mapfun_aux ty = |
72 fun mk_mapfun_aux ty = |
94 val v' = fst (dest_TVar v) |
98 val v' = fst (dest_TVar v) |
95 in |
99 in |
96 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
100 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
97 end |
101 end |
98 |
102 |
99 (* produces the rep or abs constants for a qty *) |
103 (* produces the rep or abs constant for a qty *) |
100 fun absrep_const flag ctxt qty_str = |
104 fun absrep_const flag ctxt qty_str = |
101 let |
105 let |
102 val thy = ProofContext.theory_of ctxt |
106 val thy = ProofContext.theory_of ctxt |
103 val qty_name = Long_Name.base_name qty_str |
107 val qty_name = Long_Name.base_name qty_str |
104 in |
108 in |
173 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
177 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
174 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
178 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
175 handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty |
179 handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty |
176 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
180 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
177 handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty |
181 handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty |
178 val args_aux = map (double_lookup rtyenv qtyenv) vs |
182 val args_aux = map (double_lookup rtyenv qtyenv) vs |
179 val args = map (absrep_fun flag ctxt) args_aux |
183 val args = map (absrep_fun flag ctxt) args_aux |
180 val map_fun = mk_mapfun ctxt vs rty_pat |
184 val map_fun = mk_mapfun ctxt vs rty_pat |
181 val result = list_comb (map_fun, args) |
185 val result = list_comb (map_fun, args) |
182 in |
186 in |
183 mk_compose flag (absrep_const flag ctxt s', result) |
187 mk_compose flag (absrep_const flag ctxt s', result) |