29 fun negF absF = repF |
29 fun negF absF = repF |
30 | negF repF = absF |
30 | negF repF = absF |
31 |
31 |
32 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
32 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
33 |
33 |
34 fun ty_strs lthy (ty1, ty2) = |
|
35 (quote (Syntax.string_of_typ lthy ty1), |
|
36 quote (Syntax.string_of_typ lthy ty2)) |
|
37 |
|
38 fun ty_lift_error1 lthy rty qty = |
|
39 let |
|
40 val (rty_str, qty_str) = ty_strs lthy (rty, qty) |
|
41 val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."] |
|
42 in |
|
43 error (space_implode " " msg) |
|
44 end |
|
45 |
|
46 fun ty_lift_error2 lthy rty qty = |
|
47 let |
|
48 val (rty_str, qty_str) = ty_strs lthy (rty, qty) |
|
49 val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."] |
|
50 in |
|
51 error (space_implode " " msg) |
|
52 end |
|
53 |
|
54 fun get_fun_aux lthy s fs = |
34 fun get_fun_aux lthy s fs = |
55 case (maps_lookup (ProofContext.theory_of lthy) s) of |
35 case (maps_lookup (ProofContext.theory_of lthy) s) of |
56 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
36 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
57 | NONE => error (space_implode " " ["No map function for type", quote s, "."]) |
37 | NONE => raise |
|
38 (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) |
58 |
39 |
59 fun get_const flag lthy _ qty = |
40 fun get_const flag lthy _ qty = |
60 (* FIXME: check here that _ and qty are related *) |
41 (* FIXME: check here that _ and qty are related *) |
61 let |
42 let |
62 val thy = ProofContext.theory_of lthy |
43 val thy = ProofContext.theory_of lthy |
91 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
72 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
92 else get_const flag lthy rty qty |
73 else get_const flag lthy rty qty |
93 | (TFree x, TFree x') => |
74 | (TFree x, TFree x') => |
94 if x = x' |
75 if x = x' |
95 then mk_identity qty |
76 then mk_identity qty |
96 else ty_lift_error1 lthy rty qty |
77 else raise (LIFT_MATCH "get_fun") |
97 | (TVar _, TVar _) => ty_lift_error2 lthy rty qty |
78 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
98 | _ => ty_lift_error1 lthy rty qty |
79 | _ => raise (LIFT_MATCH "get_fun") |
99 |
80 |
100 fun make_def qconst_bname qty mx attr rhs lthy = |
81 fun make_def qconst_bname qty mx attr rhs lthy = |
101 let |
82 let |
102 val rty = fastype_of rhs |
83 val rty = fastype_of rhs |
103 val (arg_rtys, res_rty) = strip_type rty |
84 val (arg_rtys, res_rty) = strip_type rty |