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
|
|
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
|
20704
|
22 |
val disc_typ_of_classop: theory -> const -> typ
|
|
23 |
val disc_typ_of_const: theory -> (const -> typ) -> const -> typ
|
|
24 |
val consts_of: theory -> term -> const list * (string * typ) list
|
20387
|
25 |
val read_const: theory -> string -> const
|
|
26 |
val string_of_const: theory -> const -> string
|
20600
|
27 |
val raw_string_of_const: const -> string
|
20387
|
28 |
val string_of_const_typ: theory -> string * typ -> string
|
|
29 |
end;
|
|
30 |
|
|
31 |
structure CodegenConsts: CODEGEN_CONSTS =
|
|
32 |
struct
|
|
33 |
|
|
34 |
|
|
35 |
(* basic data structures *)
|
|
36 |
|
|
37 |
type const = string * typ list (*type instantiations*);
|
|
38 |
val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord);
|
|
39 |
val eq_const = is_equal o const_ord;
|
|
40 |
|
|
41 |
structure Consttab =
|
|
42 |
TableFun(
|
|
43 |
type key = string * typ list;
|
|
44 |
val ord = const_ord;
|
|
45 |
);
|
|
46 |
|
|
47 |
|
|
48 |
(* type instantiations and overloading *)
|
|
49 |
|
20600
|
50 |
fun inst_of_typ thy (c_ty as (c, ty)) =
|
20387
|
51 |
(c, Consts.typargs (Sign.consts_of thy) c_ty);
|
|
52 |
|
20600
|
53 |
fun typ_of_inst thy (c_tys as (c, tys)) =
|
20387
|
54 |
(c, Consts.instance (Sign.consts_of thy) c_tys);
|
|
55 |
|
20389
|
56 |
fun find_def thy (c, tys) =
|
20387
|
57 |
let
|
|
58 |
val specs = Defs.specifications_of (Theory.defs_of thy) c;
|
20389
|
59 |
val typ_instance = case AxClass.class_of_param thy c
|
|
60 |
of SOME _ => let
|
|
61 |
fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
|
|
62 |
| instance_tycos (_ , TVar _) = true
|
|
63 |
| instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
|
|
64 |
in instance_tycos end
|
20600
|
65 |
| NONE => Sign.typ_instance thy;
|
|
66 |
fun get_def (_, { is_def, thyname, name, lhs, rhs }) =
|
|
67 |
if is_def andalso forall typ_instance (tys ~~ lhs) then
|
|
68 |
case try (Thm.get_axiom_i thy) name
|
|
69 |
of SOME thm => SOME ((thyname, thm), lhs)
|
|
70 |
| NONE => NONE
|
|
71 |
else NONE
|
20387
|
72 |
in
|
20600
|
73 |
get_first get_def specs
|
20387
|
74 |
end;
|
|
75 |
|
20389
|
76 |
fun mk_classop_typinst thy (c, tyco) =
|
|
77 |
(c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
|
|
78 |
(Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
|
|
79 |
|
20600
|
80 |
fun norm thy (c, insts) =
|
20387
|
81 |
let
|
|
82 |
fun disciplined _ [(Type (tyco, _))] =
|
20389
|
83 |
mk_classop_typinst thy (c, tyco)
|
20387
|
84 |
| disciplined sort _ =
|
20389
|
85 |
(c, [TVar (("'a", 0), sort)]);
|
20387
|
86 |
fun ad_hoc c tys =
|
20389
|
87 |
case find_def thy (c, tys)
|
20387
|
88 |
of SOME (_, tys) => (c, tys)
|
20600
|
89 |
| NONE => inst_of_typ thy (c, Sign.the_const_type thy c);
|
|
90 |
in case AxClass.class_of_param thy c
|
|
91 |
of SOME class => disciplined [class] insts
|
|
92 |
| _ => ad_hoc c insts
|
20387
|
93 |
end;
|
|
94 |
|
20600
|
95 |
fun norm_of_typ thy (c, ty) =
|
|
96 |
norm thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
|
|
97 |
|
20704
|
98 |
fun disc_typ_of_classop thy (c, [TVar _]) =
|
|
99 |
let
|
|
100 |
val class = (the o AxClass.class_of_param thy) c;
|
|
101 |
val (v, cs) = ClassPackage.the_consts_sign thy class
|
|
102 |
in
|
|
103 |
(Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
|
|
104 |
((the o AList.lookup (op =) cs) c)
|
|
105 |
end
|
|
106 |
| disc_typ_of_classop thy (c, [TFree _]) =
|
20389
|
107 |
let
|
|
108 |
val class = (the o AxClass.class_of_param thy) c;
|
|
109 |
val (v, cs) = ClassPackage.the_consts_sign thy class
|
|
110 |
in
|
|
111 |
(Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
|
|
112 |
((the o AList.lookup (op =) cs) c)
|
|
113 |
end
|
20704
|
114 |
| disc_typ_of_classop thy (c, [Type (tyco, _)]) =
|
20389
|
115 |
let
|
|
116 |
val class = (the o AxClass.class_of_param thy) c;
|
|
117 |
val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco);
|
|
118 |
in
|
|
119 |
Logic.varifyT ((the o AList.lookup (op =) cs) c)
|
|
120 |
end;
|
20387
|
121 |
|
20704
|
122 |
fun disc_typ_of_const thy f (const as (c, [ty])) =
|
|
123 |
if (is_some o AxClass.class_of_param thy) c
|
|
124 |
then disc_typ_of_classop thy const
|
|
125 |
else f const
|
|
126 |
| disc_typ_of_const thy f const = f const;
|
|
127 |
|
|
128 |
fun consts_of thy t =
|
|
129 |
fold_aterms (fn Const c => cons (norm_of_typ thy c, c) | _ => I) t []
|
|
130 |
|> split_list;
|
|
131 |
|
20387
|
132 |
|
|
133 |
(* reading constants as terms *)
|
|
134 |
|
|
135 |
fun read_const_typ thy raw_t =
|
|
136 |
let
|
|
137 |
val t = Sign.read_term thy raw_t
|
|
138 |
in case try dest_Const t
|
20600
|
139 |
of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty
|
20389
|
140 |
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
|
20387
|
141 |
end;
|
|
142 |
|
|
143 |
fun read_const thy =
|
20600
|
144 |
norm_of_typ thy o read_const_typ thy;
|
20387
|
145 |
|
|
146 |
|
|
147 |
(* printing constants *)
|
|
148 |
|
|
149 |
fun string_of_const thy (c, tys) =
|
|
150 |
space_implode " " (Sign.extern_const thy c
|
|
151 |
:: map (enclose "[" "]" o Sign.string_of_typ thy) tys);
|
|
152 |
|
20600
|
153 |
fun raw_string_of_const (c, tys) =
|
|
154 |
space_implode " " (c
|
|
155 |
:: map (enclose "[" "]" o Display.raw_string_of_typ) tys);
|
|
156 |
|
20387
|
157 |
fun string_of_const_typ thy (c, ty) =
|
|
158 |
string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty));
|
|
159 |
|
|
160 |
end;
|