30 fun negF absF = repF |
30 fun negF absF = repF |
31 | negF repF = absF |
31 | negF repF = absF |
32 |
32 |
33 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
33 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
34 |
34 |
|
35 fun mk_compose flag (trm1, trm2) = |
|
36 case flag of |
|
37 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
|
38 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
|
39 |
35 fun get_fun_aux lthy s fs = |
40 fun get_fun_aux lthy s fs = |
36 let |
41 let |
37 val thy = ProofContext.theory_of lthy |
42 val thy = ProofContext.theory_of lthy |
38 val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) |
43 val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) |
39 val info = maps_lookup thy s handle NotFound => raise exc |
44 val info = maps_lookup thy s handle NotFound => raise exc |
40 in |
45 in |
41 list_comb (Const (#mapfun info, dummyT), fs) |
46 list_comb (Const (#mapfun info, dummyT), fs) |
42 end |
47 end |
43 |
48 |
44 fun get_const flag lthy _ qty = |
49 fun get_const flag lthy _ qty = |
45 (* FIXME: check here that _ and qty are related *) |
50 (* FIXME: check here that the type-constructors of _ and qty are related *) |
46 let |
51 let |
47 val thy = ProofContext.theory_of lthy |
52 val thy = ProofContext.theory_of lthy |
48 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
53 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
49 in |
54 in |
50 case flag of |
55 case flag of |
66 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
71 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
67 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
72 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
68 in |
73 in |
69 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
74 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
70 end |
75 end |
71 | (Type (s, []), Type (s', [])) => |
76 | (Type (s, _), Type (s', [])) => |
72 if s = s' |
77 if s = s' |
73 then mk_identity qty |
78 then mk_identity qty |
74 else get_const flag lthy rty qty |
79 else get_const flag lthy rty qty |
75 | (Type (s, tys), Type (s', tys')) => |
80 | (Type (s, tys), Type (s', tys')) => |
76 if s = s' |
81 let |
77 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
82 val args = map (get_fun flag lthy) (tys ~~ tys') |
78 else get_const flag lthy rty qty |
83 in |
|
84 if s = s' |
|
85 then get_fun_aux lthy s args |
|
86 else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) |
|
87 end |
79 | (TFree x, TFree x') => |
88 | (TFree x, TFree x') => |
80 if x = x' |
89 if x = x' |
81 then mk_identity qty |
90 then mk_identity qty |
82 else raise (LIFT_MATCH "get_fun (frees)") |
91 else raise (LIFT_MATCH "get_fun (frees)") |
83 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") |
92 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") |