equal
deleted
inserted
replaced
21 val ((rhs, (_ , thm)), lthy') = |
21 val ((rhs, (_ , thm)), lthy') = |
22 LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy |
22 LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy |
23 in |
23 in |
24 ((rhs, thm), lthy') |
24 ((rhs, thm), lthy') |
25 end |
25 end |
26 |
|
27 fun lookup_qenv qenv qty = |
|
28 (case (AList.lookup (op=) qenv qty) of |
|
29 SOME rty => SOME (qty, rty) |
|
30 | NONE => NONE) |
|
31 |
26 |
32 |
27 |
33 (* calculates the aggregate abs and rep functions for a given type; |
28 (* calculates the aggregate abs and rep functions for a given type; |
34 repF is for constants' arguments; absF is for constants; |
29 repF is for constants' arguments; absF is for constants; |
35 function types need to be treated specially, since repF and absF |
30 function types need to be treated specially, since repF and absF |
79 |
74 |
80 fun mk_identity ty = Abs ("", ty, Bound 0) |
75 fun mk_identity ty = Abs ("", ty, Bound 0) |
81 |
76 |
82 in |
77 in |
83 if (AList.defined (op=) qenv ty) |
78 if (AList.defined (op=) qenv ty) |
84 then (get_const flag (the (lookup_qenv qenv ty))) |
79 then (get_const flag (the (Quotient_Info.lookup_qenv (op=) qenv ty))) |
85 else (case ty of |
80 else (case ty of |
86 TFree _ => (mk_identity ty, (ty, ty)) |
81 TFree _ => (mk_identity ty, (ty, ty)) |
87 | Type (_, []) => (mk_identity ty, (ty, ty)) |
82 | Type (_, []) => (mk_identity ty, (ty, ty)) |
88 | Type ("fun" , [ty1, ty2]) => |
83 | Type ("fun" , [ty1, ty2]) => |
89 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] |
84 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] |