36 | negF repF = absF |
36 | negF repF = absF |
37 |
37 |
38 fun get_fun flag qenv lthy ty = |
38 fun get_fun flag qenv lthy ty = |
39 let |
39 let |
40 |
40 |
41 fun get_fun_aux s fs_tys = |
41 fun get_fun_aux s fs = |
42 let |
|
43 val (fs, tys) = split_list fs_tys |
|
44 val (otys, ntys) = split_list tys |
|
45 val oty = Type (s, otys) |
|
46 val nty = Type (s, ntys) |
|
47 val ftys = map (op -->) tys |
|
48 in |
|
49 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
42 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
50 SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) |
43 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
51 | NONE => error ("no map association for type " ^ s)) |
44 | NONE => error ("no map association for type " ^ s)) |
52 end |
|
53 |
45 |
54 fun get_fun_fun fs_tys = |
46 fun get_const flag qty = |
55 let |
|
56 val (fs, tys) = split_list fs_tys |
|
57 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
|
58 val oty = nty1 --> oty2 |
|
59 val nty = oty1 --> nty2 |
|
60 val ftys = map (op -->) tys |
|
61 in |
|
62 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
|
63 end |
|
64 |
|
65 fun get_const flag (qty, rty) = |
|
66 let |
47 let |
67 val thy = ProofContext.theory_of lthy |
48 val thy = ProofContext.theory_of lthy |
68 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
49 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
69 in |
50 in |
70 case flag of |
51 case flag of |
71 absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
52 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
72 | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
53 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
73 end |
54 end |
74 |
55 |
75 fun mk_identity ty = Abs ("", ty, Bound 0) |
56 fun mk_identity ty = Abs ("", ty, Bound 0) |
76 |
57 |
77 in |
58 in |
78 if (AList.defined (op=) qenv ty) |
59 if (AList.defined (op=) qenv ty) |
79 then (get_const flag (the (Quotient_Info.lookup_qenv (op=) qenv ty))) |
60 then (get_const flag ty) |
80 else (case ty of |
61 else (case ty of |
81 TFree _ => (mk_identity ty, (ty, ty)) |
62 TFree _ => mk_identity ty |
82 | Type (_, []) => (mk_identity ty, (ty, ty)) |
63 | Type (_, []) => mk_identity ty |
83 | Type ("fun" , [ty1, ty2]) => |
64 | Type ("fun" , [ty1, ty2]) => |
84 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] |
65 let |
|
66 val fs_ty1 = get_fun (negF flag) qenv lthy ty1 |
|
67 val fs_ty2 = get_fun flag qenv lthy ty2 |
|
68 in |
|
69 get_fun_aux "fun" [fs_ty1, fs_ty2] |
|
70 end |
85 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
71 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
86 | _ => raise ERROR ("no type variables")) |
72 | _ => error ("no type variables allowed")) |
87 end |
73 end |
88 |
74 |
89 fun make_def nconst_bname rhs qty mx attr qenv lthy = |
75 fun make_def nconst_bname rhs qty mx attr qenv lthy = |
90 let |
76 let |
91 val (arg_tys, res_ty) = strip_type qty |
77 val (arg_tys, res_ty) = strip_type qty |
92 |
78 |
93 val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys |
79 val rep_fns = map (get_fun repF qenv lthy) arg_tys |
94 val abs_fn = (fst o get_fun absF qenv lthy) res_ty |
80 val abs_fn = (get_fun absF qenv lthy) res_ty |
95 |
81 |
96 fun mk_fun_map t s = |
82 fun mk_fun_map t s = |
97 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
83 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
98 |
84 |
99 val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn |
85 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
100 |> Syntax.check_term lthy |
86 |> Syntax.check_term lthy |
101 in |
87 in |
102 define nconst_bname mx attr (absrep_fn $ rhs) lthy |
88 define nconst_bname mx attr absrep_trm lthy |
103 end |
89 end |
104 |
90 |
105 |
91 |
106 (* returns all subterms where two types differ *) |
92 (* returns all subterms where two types differ *) |
107 fun diff (T, S) Ds = |
93 fun diff (T, S) Ds = |
129 fun sanity_chk lthy qenv = |
115 fun sanity_chk lthy qenv = |
130 let |
116 let |
131 val global_qenv = Quotient_Info.mk_qenv lthy |
117 val global_qenv = Quotient_Info.mk_qenv lthy |
132 val thy = ProofContext.theory_of lthy |
118 val thy = ProofContext.theory_of lthy |
133 |
119 |
134 fun is_inst thy (qty, rty) (qty', rty') = |
120 fun is_inst (qty, rty) (qty', rty') = |
135 if Sign.typ_instance thy (qty, qty') |
121 if Sign.typ_instance thy (qty, qty') |
136 then let |
122 then let |
137 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
123 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
138 in |
124 in |
139 rty = Envir.subst_type inst rty' |
125 rty = Envir.subst_type inst rty' |
140 end |
126 end |
141 else false |
127 else false |
142 |
128 |
143 fun chk_inst (qty, rty) = |
129 fun chk_inst (qty, rty) = |
144 if exists (is_inst thy (qty, rty)) global_qenv |
130 if exists (is_inst (qty, rty)) global_qenv |
145 then true |
131 then true |
146 else error_msg lthy (qty, rty) |
132 else error_msg lthy (qty, rty) |
147 in |
133 in |
148 forall chk_inst qenv |
134 map chk_inst qenv |
149 end |
135 end |
150 |
136 |
151 |
137 |
152 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
138 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
153 let |
139 let |