equal
deleted
inserted
replaced
21 val ((rhs, (_ , thm)), lthy') = |
21 val ((rhs, (_ , thm)), lthy') = |
22 Local_Theory.define "" ((name, mx), (attr, rhs)) lthy |
22 Local_Theory.define "" ((name, mx), (attr, rhs)) lthy |
23 in |
23 in |
24 ((rhs, thm), lthy') |
24 ((rhs, thm), lthy') |
25 end |
25 end |
26 |
|
27 (* calculates the aggregate abs and rep functions for a given type; |
|
28 repF is for constants' arguments; absF is for constants; |
|
29 function types need to be treated specially, since repF and absF |
|
30 change *) |
|
31 |
26 |
32 datatype flag = absF | repF |
27 datatype flag = absF | repF |
33 |
28 |
34 fun negF absF = repF |
29 fun negF absF = repF |
35 | negF repF = absF |
30 | negF repF = absF |
70 case flag of |
65 case flag of |
71 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
66 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
72 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
67 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
73 end |
68 end |
74 |
69 |
|
70 |
|
71 (* calculates the aggregate abs and rep functions for a given type; |
|
72 repF is for constants' arguments; absF is for constants; |
|
73 function types need to be treated specially, since repF and absF |
|
74 change *) |
|
75 |
75 fun get_fun flag lthy (rty, qty) = |
76 fun get_fun flag lthy (rty, qty) = |
76 case (rty, qty) of |
77 case (rty, qty) of |
77 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
78 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
78 let |
79 let |
79 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
80 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
94 then mk_identity qty |
95 then mk_identity qty |
95 else ty_lift_error1 lthy rty qty |
96 else ty_lift_error1 lthy rty qty |
96 | (TVar _, TVar _) => ty_lift_error2 lthy rty qty |
97 | (TVar _, TVar _) => ty_lift_error2 lthy rty qty |
97 | _ => ty_lift_error1 lthy rty qty |
98 | _ => ty_lift_error1 lthy rty qty |
98 |
99 |
99 fun make_def nconst_bname qty mx attr rhs lthy = |
100 fun make_def qconst_bname qty mx attr rhs lthy = |
100 let |
101 let |
101 val rty = fastype_of rhs |
102 val rty = fastype_of rhs |
102 val (arg_rtys, res_rty) = strip_type rty |
103 val (arg_rtys, res_rty) = strip_type rty |
103 val (arg_qtys, res_qty) = strip_type qty |
104 val (arg_qtys, res_qty) = strip_type qty |
104 |
105 |
109 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
110 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
110 |
111 |
111 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
112 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
112 |> Syntax.check_term lthy |
113 |> Syntax.check_term lthy |
113 |
114 |
114 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
115 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
115 |
116 |
116 val nconst_str = Binding.name_of nconst_bname |
117 val qconst_str = Binding.name_of qconst_bname |
117 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs} |
118 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs} |
118 val lthy'' = Local_Theory.declaration true |
119 val lthy'' = Local_Theory.declaration true |
119 (fn phi => qconsts_update_gen nconst_str (qcinfo phi)) lthy' |
120 (fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy' |
120 in |
121 in |
121 ((trm, thm), lthy'') |
122 ((trm, thm), lthy'') |
122 end |
123 end |
123 |
124 |
124 (* interface and syntax setup *) |
125 (* interface and syntax setup *) |