1 signature QUOTIENT_TERM = |
1 signature QUOTIENT_TERM = |
2 sig |
2 sig |
3 val regularize_trm: Proof.context -> term -> term -> term |
3 exception LIFT_MATCH of string |
4 val inj_repabs_trm: Proof.context -> (term * term) -> term |
4 |
|
5 datatype flag = absF | repF |
|
6 val get_fun: flag -> Proof.context -> typ * typ -> term |
|
7 |
|
8 val regularize_trm: Proof.context -> term -> term -> term |
|
9 val inj_repabs_trm: Proof.context -> (term * term) -> term |
5 end; |
10 end; |
6 |
11 |
7 structure Quotient_Term: QUOTIENT_TERM = |
12 structure Quotient_Term: QUOTIENT_TERM = |
8 struct |
13 struct |
9 |
14 |
10 open Quotient_Info; |
15 open Quotient_Info; |
11 open Quotient_Type; |
16 |
12 open Quotient_Def; |
17 exception LIFT_MATCH of string |
|
18 |
|
19 (* Calculates the aggregate abs and rep functions for a given type; *) |
|
20 (* repF is for constants' arguments; absF is for constants; *) |
|
21 (* function types need to be treated specially, since repF and absF *) |
|
22 (* change *) |
|
23 |
|
24 datatype flag = absF | repF |
|
25 |
|
26 fun negF absF = repF |
|
27 | negF repF = absF |
|
28 |
|
29 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
30 |
|
31 fun mk_compose flag (trm1, trm2) = |
|
32 case flag of |
|
33 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
|
34 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
|
35 |
|
36 fun get_fun_aux lthy s fs = |
|
37 let |
|
38 val thy = ProofContext.theory_of lthy |
|
39 val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) |
|
40 val info = maps_lookup thy s handle NotFound => raise exc |
|
41 in |
|
42 list_comb (Const (#mapfun info, dummyT), fs) |
|
43 end |
|
44 |
|
45 fun get_const flag lthy _ qty = |
|
46 (* FIXME: check here that the type-constructors of _ and qty are related *) |
|
47 let |
|
48 val thy = ProofContext.theory_of lthy |
|
49 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
50 in |
|
51 case flag of |
|
52 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
|
53 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
|
54 end |
|
55 |
|
56 fun get_fun flag lthy (rty, qty) = |
|
57 if rty = qty then mk_identity qty else |
|
58 case (rty, qty) of |
|
59 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
|
60 let |
|
61 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
|
62 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
|
63 in |
|
64 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
|
65 end |
|
66 | (Type (s, _), Type (s', [])) => |
|
67 if s = s' |
|
68 then mk_identity qty |
|
69 else get_const flag lthy rty qty |
|
70 | (Type (s, tys), Type (s', tys')) => |
|
71 let |
|
72 val args = map (get_fun flag lthy) (tys ~~ tys') |
|
73 in |
|
74 if s = s' |
|
75 then get_fun_aux lthy s args |
|
76 else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) |
|
77 end |
|
78 | (TFree x, TFree x') => |
|
79 if x = x' |
|
80 then mk_identity qty |
|
81 else raise (LIFT_MATCH "get_fun (frees)") |
|
82 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") |
|
83 | _ => raise (LIFT_MATCH "get_fun (default)") |
|
84 |
13 |
85 |
14 (* |
86 (* |
15 Regularizing an rtrm means: |
87 Regularizing an rtrm means: |
16 |
88 |
17 - Quantifiers over types that need lifting are replaced |
89 - Quantifiers over types that need lifting are replaced |
216 |
288 |
217 Vars case cannot occur. |
289 Vars case cannot occur. |
218 *) |
290 *) |
219 |
291 |
220 fun mk_repabs lthy (T, T') trm = |
292 fun mk_repabs lthy (T, T') trm = |
221 Quotient_Def.get_fun repF lthy (T, T') |
293 get_fun repF lthy (T, T') $ (get_fun absF lthy (T, T') $ trm) |
222 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
|
223 |
294 |
224 |
295 |
225 (* bound variables need to be treated properly, *) |
296 (* bound variables need to be treated properly, *) |
226 (* as the type of subterms needs to be calculated *) |
297 (* as the type of subterms needs to be calculated *) |
227 |
298 |