20387
|
1 |
(* Title: Pure/Tools/codegen_consts.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Distinction of ad-hoc overloaded constants. Convenient data structures
|
|
6 |
for constants.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature CODEGEN_CONSTS =
|
|
10 |
sig
|
|
11 |
type const = string * typ list (*type instantiations*)
|
|
12 |
val const_ord: const * const -> order
|
|
13 |
val eq_const: const * const -> bool
|
|
14 |
structure Consttab: TABLE
|
|
15 |
val typinst_of_typ: theory -> string * typ -> const
|
|
16 |
val typ_of_typinst: theory -> const -> string * typ
|
20389
|
17 |
val find_def: theory -> const
|
|
18 |
-> ((string (*theory name*) * string (*definition name*)) * typ list) option
|
|
19 |
val sortinsts: theory -> typ * typ -> (typ * sort) list
|
20387
|
20 |
val norminst_of_typ: theory -> string * typ -> const
|
|
21 |
val class_of_classop: theory -> const -> class option
|
|
22 |
val insts_of_classop: theory -> const -> const list
|
20389
|
23 |
val typ_of_classop: theory -> const -> typ
|
20387
|
24 |
val read_const: theory -> string -> const
|
|
25 |
val read_const_typ: theory -> string -> string * typ
|
|
26 |
val string_of_const: theory -> const -> string
|
|
27 |
val string_of_const_typ: theory -> string * typ -> string
|
|
28 |
end;
|
|
29 |
|
|
30 |
structure CodegenConsts: CODEGEN_CONSTS =
|
|
31 |
struct
|
|
32 |
|
|
33 |
|
|
34 |
(* basic data structures *)
|
|
35 |
|
|
36 |
type const = string * typ list (*type instantiations*);
|
|
37 |
val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord);
|
|
38 |
val eq_const = is_equal o const_ord;
|
|
39 |
|
|
40 |
structure Consttab =
|
|
41 |
TableFun(
|
|
42 |
type key = string * typ list;
|
|
43 |
val ord = const_ord;
|
|
44 |
);
|
|
45 |
|
|
46 |
|
|
47 |
(* type instantiations and overloading *)
|
|
48 |
|
|
49 |
fun typinst_of_typ thy (c_ty as (c, ty)) =
|
|
50 |
(c, Consts.typargs (Sign.consts_of thy) c_ty);
|
|
51 |
|
|
52 |
fun typ_of_typinst thy (c_tys as (c, tys)) =
|
|
53 |
(c, Consts.instance (Sign.consts_of thy) c_tys);
|
|
54 |
|
20389
|
55 |
fun find_def thy (c, tys) =
|
20387
|
56 |
let
|
|
57 |
val specs = Defs.specifications_of (Theory.defs_of thy) c;
|
20389
|
58 |
val typ_instance = case AxClass.class_of_param thy c
|
|
59 |
of SOME _ => let
|
|
60 |
fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
|
|
61 |
| instance_tycos (_ , TVar _) = true
|
|
62 |
| instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
|
|
63 |
in instance_tycos end
|
|
64 |
| NONE => Sign.typ_instance thy
|
20387
|
65 |
in
|
20389
|
66 |
get_first (fn (_, { is_def, thyname, name, lhs, ... }) => if is_def
|
|
67 |
andalso forall typ_instance (tys ~~ lhs)
|
|
68 |
then SOME ((thyname, name), lhs) else NONE) specs
|
20387
|
69 |
end;
|
|
70 |
|
20389
|
71 |
fun sortinsts thy (ty, ty_decl) =
|
|
72 |
Vartab.empty
|
|
73 |
|> Sign.typ_match thy (ty_decl, ty)
|
|
74 |
|> Vartab.dest
|
|
75 |
|> map (fn (_, (sort, ty)) => (ty, sort));
|
|
76 |
|
|
77 |
fun mk_classop_typinst thy (c, tyco) =
|
|
78 |
(c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
|
|
79 |
(Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
|
|
80 |
|
20387
|
81 |
fun norminst_of_typ thy (c, ty) =
|
|
82 |
let
|
|
83 |
fun disciplined _ [(Type (tyco, _))] =
|
20389
|
84 |
mk_classop_typinst thy (c, tyco)
|
20387
|
85 |
| disciplined sort _ =
|
20389
|
86 |
(c, [TVar (("'a", 0), sort)]);
|
20387
|
87 |
fun ad_hoc c tys =
|
20389
|
88 |
case find_def thy (c, tys)
|
20387
|
89 |
of SOME (_, tys) => (c, tys)
|
|
90 |
| NONE => typinst_of_typ thy (c, Sign.the_const_type thy c);
|
|
91 |
val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty);
|
20389
|
92 |
in if c = "op =" then disciplined (Sign.defaultS thy) tyinsts
|
20387
|
93 |
(*the distinction on op = will finally disappear!*)
|
|
94 |
else case AxClass.class_of_param thy c
|
20389
|
95 |
of SOME class => disciplined [class] tyinsts
|
20387
|
96 |
| _ => ad_hoc c tyinsts
|
|
97 |
end;
|
|
98 |
|
20389
|
99 |
fun class_of_classop thy (c, [TVar _]) =
|
|
100 |
AxClass.class_of_param thy c
|
|
101 |
| class_of_classop thy (c, [TFree _]) =
|
|
102 |
AxClass.class_of_param thy c
|
|
103 |
| class_of_classop thy (c, _) = NONE;
|
20387
|
104 |
|
|
105 |
fun insts_of_classop thy (c_tys as (c, tys)) =
|
20428
|
106 |
(*get rid of this finally*)
|
20387
|
107 |
case AxClass.class_of_param thy c
|
|
108 |
of NONE => [c_tys]
|
20389
|
109 |
| SOME class => let
|
|
110 |
val cs = maps (AxClass.params_of thy)
|
|
111 |
(Sorts.all_super_classes (Sign.classes_of thy) class)
|
|
112 |
fun add_tyco (tyco, classes) =
|
|
113 |
if member (op = o apsnd fst) classes class
|
|
114 |
then cons tyco else I;
|
|
115 |
val tycos =
|
|
116 |
Symtab.fold add_tyco
|
|
117 |
((#arities o Sorts.rep_algebra o Sign.classes_of) thy) [];
|
|
118 |
in maps (fn c => map (fn tyco => mk_classop_typinst thy (c, tyco)) tycos) cs end;
|
|
119 |
|
|
120 |
fun typ_of_classop thy (c, [TVar _]) =
|
|
121 |
let
|
|
122 |
val class = (the o AxClass.class_of_param thy) c;
|
|
123 |
val (v, cs) = ClassPackage.the_consts_sign thy class
|
|
124 |
in
|
|
125 |
(Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
|
|
126 |
((the o AList.lookup (op =) cs) c)
|
|
127 |
end
|
|
128 |
| typ_of_classop thy (c, [TFree _]) =
|
|
129 |
let
|
|
130 |
val class = (the o AxClass.class_of_param thy) c;
|
|
131 |
val (v, cs) = ClassPackage.the_consts_sign thy class
|
|
132 |
in
|
|
133 |
(Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
|
|
134 |
((the o AList.lookup (op =) cs) c)
|
|
135 |
end
|
|
136 |
| typ_of_classop thy (c, [Type (tyco, _)]) =
|
|
137 |
let
|
|
138 |
val class = (the o AxClass.class_of_param thy) c;
|
|
139 |
val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco);
|
|
140 |
in
|
|
141 |
Logic.varifyT ((the o AList.lookup (op =) cs) c)
|
|
142 |
end;
|
20387
|
143 |
|
|
144 |
|
|
145 |
(* reading constants as terms *)
|
|
146 |
|
|
147 |
fun read_const_typ thy raw_t =
|
|
148 |
let
|
|
149 |
val t = Sign.read_term thy raw_t
|
|
150 |
in case try dest_Const t
|
|
151 |
of SOME c_ty => c_ty
|
20389
|
152 |
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
|
20387
|
153 |
end;
|
|
154 |
|
|
155 |
fun read_const thy =
|
|
156 |
typinst_of_typ thy o read_const_typ thy;
|
|
157 |
|
|
158 |
|
|
159 |
(* printing constants *)
|
|
160 |
|
|
161 |
fun string_of_const thy (c, tys) =
|
|
162 |
space_implode " " (Sign.extern_const thy c
|
|
163 |
:: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
|
|
164 |
|
|
165 |
fun string_of_const_typ thy (c, ty) =
|
|
166 |
string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
|
|
167 |
|
|
168 |
end;
|