23 Local_Theory.define "" ((name, mx), (attr, rhs)) lthy |
22 Local_Theory.define "" ((name, mx), (attr, rhs)) lthy |
24 in |
23 in |
25 ((rhs, thm), lthy') |
24 ((rhs, thm), lthy') |
26 end |
25 end |
27 |
26 |
28 |
|
29 (* calculates the aggregate abs and rep functions for a given type; |
27 (* calculates the aggregate abs and rep functions for a given type; |
30 repF is for constants' arguments; absF is for constants; |
28 repF is for constants' arguments; absF is for constants; |
31 function types need to be treated specially, since repF and absF |
29 function types need to be treated specially, since repF and absF |
32 change *) |
30 change *) |
33 |
31 |
34 datatype flag = absF | repF |
32 datatype flag = absF | repF |
35 |
33 |
36 fun negF absF = repF |
34 fun negF absF = repF |
37 | negF repF = absF |
35 | negF repF = absF |
38 |
36 |
39 fun get_fun flag qenv lthy ty = |
37 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
38 |
|
39 fun ty_lift_error lthy rty qty = |
40 let |
40 let |
41 |
41 val rty_str = quote (Syntax.string_of_typ lthy rty) |
42 fun get_fun_aux s fs = |
42 val qty_str = quote (Syntax.string_of_typ lthy qty) |
43 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
43 val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."] |
44 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
|
45 | NONE => error ("no map association for type " ^ s)) |
|
46 |
|
47 fun get_const flag qty = |
|
48 let |
|
49 val thy = ProofContext.theory_of lthy |
|
50 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
51 in |
|
52 case flag of |
|
53 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
|
54 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
|
55 end |
|
56 |
|
57 fun mk_identity ty = Abs ("", ty, Bound 0) |
|
58 |
|
59 in |
44 in |
60 if (AList.defined (op=) qenv ty) |
45 raise LIFT_MATCH (space_implode " " msg) |
61 then (get_const flag ty) |
|
62 else (case ty of |
|
63 TFree _ => mk_identity ty |
|
64 | Type (_, []) => mk_identity ty |
|
65 | Type ("fun" , [ty1, ty2]) => |
|
66 let |
|
67 val fs_ty1 = get_fun (negF flag) qenv lthy ty1 |
|
68 val fs_ty2 = get_fun flag qenv lthy ty2 |
|
69 in |
|
70 get_fun_aux "fun" [fs_ty1, fs_ty2] |
|
71 end |
|
72 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
|
73 | _ => error ("no type variables allowed")) |
|
74 end |
46 end |
75 |
47 |
76 (* returns all subterms where two types differ *) |
48 fun get_fun_aux lthy s fs = |
77 fun diff (T, S) Ds = |
49 case (maps_lookup (ProofContext.theory_of lthy) s) of |
78 case (T, S) of |
50 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
79 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds |
51 | NONE => raise LIFT_MATCH ("no map association for type " ^ s) |
80 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds |
|
81 | (Type (a, Ts), Type (b, Us)) => |
|
82 if a = b then diffs (Ts, Us) Ds else (T, S)::Ds |
|
83 | _ => (T, S)::Ds |
|
84 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) |
|
85 | diffs ([], []) Ds = Ds |
|
86 | diffs _ _ = error "Unequal length of type arguments" |
|
87 |
52 |
|
53 fun get_const flag lthy _ qty = |
|
54 (* FIXME: check here that _ and qty are related *) |
|
55 let |
|
56 val thy = ProofContext.theory_of lthy |
|
57 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
58 in |
|
59 case flag of |
|
60 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
|
61 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
|
62 end |
88 |
63 |
89 (* sanity check that the calculated quotient environment |
64 fun get_fun flag lthy (rty, qty) = |
90 matches with the stored quotient environment. *) |
65 case (rty, qty) of |
91 fun sanity_chk qenv lthy = |
66 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
92 let |
67 let |
93 val global_qenv = Quotient_Info.mk_qenv lthy |
68 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
94 val thy = ProofContext.theory_of lthy |
69 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
95 |
70 in |
96 fun error_msg lthy (qty, rty) = |
71 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
97 let |
72 end |
98 val qtystr = quote (Syntax.string_of_typ lthy qty) |
73 | (Type (s, []), Type (s', [])) => |
99 val rtystr = quote (Syntax.string_of_typ lthy rty) |
74 if s = s' |
100 in |
75 then mk_identity qty |
101 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
76 else get_const flag lthy rty qty |
102 end |
77 | (Type (s, tys), Type (s', tys')) => |
103 |
78 if s = s' |
104 fun is_inst (qty, rty) (qty', rty') = |
79 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
105 if Sign.typ_instance thy (qty, qty') |
80 else get_const flag lthy rty qty |
106 then let |
81 | (TFree x, TFree x') => |
107 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
82 if x = x' |
108 in |
83 then mk_identity qty |
109 rty = Envir.subst_type inst rty' |
84 else ty_lift_error lthy rty qty |
110 end |
85 | (TVar _, TVar _) => raise LIFT_MATCH "no type variables allowed" |
111 else false |
86 | _ => ty_lift_error lthy rty qty |
112 |
|
113 fun chk_inst (qty, rty) = |
|
114 if exists (is_inst (qty, rty)) global_qenv |
|
115 then true |
|
116 else error_msg lthy (qty, rty) |
|
117 in |
|
118 map chk_inst qenv |
|
119 end |
|
120 |
87 |
121 fun make_def nconst_bname qty mx attr rhs lthy = |
88 fun make_def nconst_bname qty mx attr rhs lthy = |
122 let |
89 let |
123 val (arg_tys, res_ty) = strip_type qty |
|
124 |
|
125 val rty = fastype_of rhs |
90 val rty = fastype_of rhs |
126 val qenv = distinct (op=) (diff (qty, rty) []) |
91 val (arg_rtys, res_rty) = strip_type rty |
127 |
92 val (arg_qtys, res_qty) = strip_type qty |
128 val _ = sanity_chk qenv lthy |
93 |
129 |
94 val rep_fns = map (get_fun repF lthy) (arg_rtys ~~ arg_qtys) |
130 val rep_fns = map (get_fun repF qenv lthy) arg_tys |
95 val abs_fn = get_fun absF lthy (res_rty, res_qty) |
131 val abs_fn = (get_fun absF qenv lthy) res_ty |
|
132 |
96 |
133 fun mk_fun_map t s = |
97 fun mk_fun_map t s = |
134 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
98 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
135 |
99 |
136 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
100 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
137 |> Syntax.check_term lthy |
101 |> Syntax.check_term lthy |
138 |
102 |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
103 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
140 |
104 |
141 val nconst_str = Binding.name_of nconst_bname |
105 val nconst_str = Binding.name_of nconst_bname |
142 val qcinfo = {qconst = trm, rconst = rhs} |
106 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs} |
143 val lthy'' = Local_Theory.declaration true |
107 val lthy'' = Local_Theory.declaration true |
144 (fn phi => qconsts_update_generic nconst_str |
108 (fn phi => qconsts_update_gen nconst_str (qcinfo phi)) lthy' |
145 (qconsts_transfer phi qcinfo)) lthy' |
|
146 in |
109 in |
147 ((trm, thm), lthy'') |
110 ((trm, thm), lthy'') |
148 end |
111 end |
149 |
112 |
150 (* interface and syntax setup *) |
113 (* interface and syntax setup *) |