author | haftmann |
Tue, 09 Jan 2007 08:31:47 +0100 | |
changeset 22032 | 979671292fbe |
parent 21895 | 6cbc0f69a21c |
child 22049 | a995f9a8f669 |
permissions | -rw-r--r-- |
20387 | 1 |
(* Title: Pure/Tools/codegen_consts.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
20855 | 5 |
Identifying constants by name plus normalized type instantantiation schemes. |
6 |
Type normalization is compatible with overloading discipline and user-defined |
|
22032 | 7 |
ad-hoc overloading. Convenient data structures for constants. |
20387 | 8 |
*) |
9 |
||
10 |
signature CODEGEN_CONSTS = |
|
11 |
sig |
|
12 |
type const = string * typ list (*type instantiations*) |
|
13 |
val const_ord: const * const -> order |
|
14 |
val eq_const: const * const -> bool |
|
15 |
structure Consttab: TABLE |
|
20600 | 16 |
val inst_of_typ: theory -> string * typ -> const |
17 |
val typ_of_inst: theory -> const -> string * typ |
|
18 |
val norm: theory -> const -> const |
|
19 |
val norm_of_typ: theory -> string * typ -> const |
|
20389 | 20 |
val find_def: theory -> const |
20600 | 21 |
-> ((string (*theory name*) * thm) * typ list) option |
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
22 |
val instance_dict: theory -> class * string |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
23 |
-> (string * sort) list * (string * typ) list |
20704 | 24 |
val disc_typ_of_classop: theory -> const -> typ |
25 |
val disc_typ_of_const: theory -> (const -> typ) -> const -> typ |
|
21118 | 26 |
val consts_of: theory -> term -> const list |
20387 | 27 |
val read_const: theory -> string -> const |
28 |
val string_of_const: theory -> const -> string |
|
20600 | 29 |
val raw_string_of_const: const -> string |
20387 | 30 |
val string_of_const_typ: theory -> string * typ -> string |
31 |
end; |
|
32 |
||
33 |
structure CodegenConsts: CODEGEN_CONSTS = |
|
34 |
struct |
|
35 |
||
36 |
||
37 |
(* basic data structures *) |
|
38 |
||
39 |
type const = string * typ list (*type instantiations*); |
|
40 |
val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord); |
|
41 |
val eq_const = is_equal o const_ord; |
|
42 |
||
43 |
structure Consttab = |
|
44 |
TableFun( |
|
45 |
type key = string * typ list; |
|
46 |
val ord = const_ord; |
|
47 |
); |
|
48 |
||
49 |
||
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
50 |
(* type instantiations, overloading, dictionary values *) |
20387 | 51 |
|
20600 | 52 |
fun inst_of_typ thy (c_ty as (c, ty)) = |
20387 | 53 |
(c, Consts.typargs (Sign.consts_of thy) c_ty); |
54 |
||
20600 | 55 |
fun typ_of_inst thy (c_tys as (c, tys)) = |
20387 | 56 |
(c, Consts.instance (Sign.consts_of thy) c_tys); |
57 |
||
20389 | 58 |
fun find_def thy (c, tys) = |
20387 | 59 |
let |
60 |
val specs = Defs.specifications_of (Theory.defs_of thy) c; |
|
20389 | 61 |
val typ_instance = case AxClass.class_of_param thy c |
62 |
of SOME _ => let |
|
63 |
fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2 |
|
64 |
| instance_tycos (_ , TVar _) = true |
|
65 |
| instance_tycos ty_ty = Sign.typ_instance thy ty_ty; |
|
66 |
in instance_tycos end |
|
20600 | 67 |
| NONE => Sign.typ_instance thy; |
68 |
fun get_def (_, { is_def, thyname, name, lhs, rhs }) = |
|
69 |
if is_def andalso forall typ_instance (tys ~~ lhs) then |
|
70 |
case try (Thm.get_axiom_i thy) name |
|
71 |
of SOME thm => SOME ((thyname, thm), lhs) |
|
72 |
| NONE => NONE |
|
73 |
else NONE |
|
20387 | 74 |
in |
20600 | 75 |
get_first get_def specs |
20387 | 76 |
end; |
77 |
||
20389 | 78 |
fun mk_classop_typinst thy (c, tyco) = |
79 |
(c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*))) |
|
80 |
(Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]); |
|
81 |
||
20600 | 82 |
fun norm thy (c, insts) = |
20387 | 83 |
let |
84 |
fun disciplined _ [(Type (tyco, _))] = |
|
20389 | 85 |
mk_classop_typinst thy (c, tyco) |
20387 | 86 |
| disciplined sort _ = |
20389 | 87 |
(c, [TVar (("'a", 0), sort)]); |
20387 | 88 |
fun ad_hoc c tys = |
20389 | 89 |
case find_def thy (c, tys) |
20387 | 90 |
of SOME (_, tys) => (c, tys) |
20600 | 91 |
| NONE => inst_of_typ thy (c, Sign.the_const_type thy c); |
92 |
in case AxClass.class_of_param thy c |
|
93 |
of SOME class => disciplined [class] insts |
|
94 |
| _ => ad_hoc c insts |
|
20387 | 95 |
end; |
96 |
||
20600 | 97 |
fun norm_of_typ thy (c, ty) = |
98 |
norm thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); |
|
99 |
||
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
100 |
fun instance_dict thy (class, tyco) = |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
101 |
let |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
102 |
val (var, cs) = AxClass.params_of_class thy class; |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
103 |
val sort_args = Name.names (Name.declare var Name.context) "'a" |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
104 |
(Sign.arity_sorts thy tyco [class]); |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
105 |
val ty_inst = Type (tyco, map TFree sort_args); |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
106 |
val inst_signs = (map o apsnd o map_type_tfree) (K ty_inst) cs; |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
107 |
in (sort_args, inst_signs) end; |
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
108 |
|
21895 | 109 |
fun disc_typ_of_classop thy (c, [ty]) = |
110 |
let |
|
111 |
val class = (the o AxClass.class_of_param thy) c; |
|
112 |
val cs = case ty |
|
113 |
of TVar _ => snd (AxClass.params_of_class thy class) |
|
114 |
| TFree _ => snd (AxClass.params_of_class thy class) |
|
115 |
| Type (tyco, _) => snd (instance_dict thy (class, tyco)); |
|
116 |
in |
|
117 |
(Logic.varifyT o the o AList.lookup (op =) cs) c |
|
118 |
end; |
|
20387 | 119 |
|
20704 | 120 |
fun disc_typ_of_const thy f (const as (c, [ty])) = |
121 |
if (is_some o AxClass.class_of_param thy) c |
|
122 |
then disc_typ_of_classop thy const |
|
123 |
else f const |
|
124 |
| disc_typ_of_const thy f const = f const; |
|
125 |
||
126 |
fun consts_of thy t = |
|
21118 | 127 |
fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t [] |
20704 | 128 |
|
20387 | 129 |
|
130 |
(* reading constants as terms *) |
|
131 |
||
132 |
fun read_const_typ thy raw_t = |
|
133 |
let |
|
134 |
val t = Sign.read_term thy raw_t |
|
135 |
in case try dest_Const t |
|
20600 | 136 |
of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty |
20389 | 137 |
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) |
20387 | 138 |
end; |
139 |
||
140 |
fun read_const thy = |
|
20600 | 141 |
norm_of_typ thy o read_const_typ thy; |
20387 | 142 |
|
143 |
||
144 |
(* printing constants *) |
|
145 |
||
146 |
fun string_of_const thy (c, tys) = |
|
147 |
space_implode " " (Sign.extern_const thy c |
|
148 |
:: map (enclose "[" "]" o Sign.string_of_typ thy) tys); |
|
149 |
||
20600 | 150 |
fun raw_string_of_const (c, tys) = |
151 |
space_implode " " (c |
|
152 |
:: map (enclose "[" "]" o Display.raw_string_of_typ) tys); |
|
153 |
||
20387 | 154 |
fun string_of_const_typ thy (c, ty) = |
155 |
string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); |
|
156 |
||
157 |
end; |