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