29 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
29 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
30 |
30 |
31 fun get_fun_aux lthy s fs = |
31 fun get_fun_aux lthy s fs = |
32 case (maps_lookup (ProofContext.theory_of lthy) s) of |
32 case (maps_lookup (ProofContext.theory_of lthy) s) of |
33 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
33 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
34 | NONE => raise |
34 | NONE => raise |
35 (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) |
35 (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) |
36 |
36 |
37 fun get_const flag lthy _ qty = |
37 fun get_const flag lthy _ qty = |
38 (* FIXME: check here that _ and qty are related *) |
38 (* FIXME: check here that _ and qty are related *) |
39 let |
39 let |
40 val thy = ProofContext.theory_of lthy |
40 val thy = ProofContext.theory_of lthy |
41 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
41 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
42 in |
42 in |
43 case flag of |
43 case flag of |
44 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
44 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
45 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
45 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
46 end |
46 end |
47 |
47 |
48 |
48 |
49 (* calculates the aggregate abs and rep functions for a given type; |
49 (* calculates the aggregate abs and rep functions for a given type; |
50 repF is for constants' arguments; absF is for constants; |
50 repF is for constants' arguments; absF is for constants; |
51 function types need to be treated specially, since repF and absF |
51 function types need to be treated specially, since repF and absF |
52 change *) |
52 change *) |
53 |
53 |
54 fun get_fun flag lthy (rty, qty) = |
54 fun get_fun flag lthy (rty, qty) = |
55 if rty = qty then mk_identity qty else |
55 if rty = qty then mk_identity qty else |
56 case (rty, qty) of |
56 case (rty, qty) of |
57 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
57 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
58 let |
58 let |
59 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
59 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
60 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
60 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
61 in |
61 in |
62 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
62 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
63 end |
63 end |
64 | (Type (s, []), Type (s', [])) => |
64 | (Type (s, []), Type (s', [])) => |
65 if s = s' |
65 if s = s' |
66 then mk_identity qty |
66 then mk_identity qty |
67 else get_const flag lthy rty qty |
67 else get_const flag lthy rty qty |
68 | (Type (s, tys), Type (s', tys')) => |
68 | (Type (s, tys), Type (s', tys')) => |
69 if s = s' |
69 if s = s' |
70 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
70 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
71 else get_const flag lthy rty qty |
71 else get_const flag lthy rty qty |
72 | (TFree x, TFree x') => |
72 | (TFree x, TFree x') => |
73 if x = x' |
73 if x = x' |
74 then mk_identity qty |
74 then mk_identity qty |
75 else raise (LIFT_MATCH "get_fun") |
75 else raise (LIFT_MATCH "get_fun") |
76 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
76 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
77 | _ => raise (LIFT_MATCH "get_fun") |
77 | _ => raise (LIFT_MATCH "get_fun") |
78 |
78 |
79 (* interface and syntax setup *) |
79 (* interface and syntax setup *) |