haftmann@32104
|
1 |
(* Title: HOLCF/Tools/Domain/domain_extender.ML
|
wenzelm@23152
|
2 |
Author: David von Oheimb
|
huffman@35794
|
3 |
Author: Brian Huffman
|
wenzelm@23152
|
4 |
|
wenzelm@23152
|
5 |
Theory extender for domain command, including theory syntax.
|
wenzelm@23152
|
6 |
*)
|
wenzelm@23152
|
7 |
|
wenzelm@23152
|
8 |
signature DOMAIN_EXTENDER =
|
wenzelm@23152
|
9 |
sig
|
huffman@33790
|
10 |
val add_domain_cmd:
|
huffman@35774
|
11 |
binding ->
|
huffman@33790
|
12 |
((string * string option) list * binding * mixfix *
|
huffman@33790
|
13 |
(binding * (bool * binding option * string) list * mixfix) list) list
|
huffman@33790
|
14 |
-> theory -> theory
|
huffman@33790
|
15 |
|
huffman@33790
|
16 |
val add_domain:
|
huffman@35774
|
17 |
binding ->
|
huffman@33790
|
18 |
((string * string option) list * binding * mixfix *
|
huffman@33790
|
19 |
(binding * (bool * binding option * typ) list * mixfix) list) list
|
huffman@33790
|
20 |
-> theory -> theory
|
huffman@33792
|
21 |
|
huffman@33792
|
22 |
val add_new_domain_cmd:
|
huffman@35774
|
23 |
binding ->
|
huffman@33792
|
24 |
((string * string option) list * binding * mixfix *
|
huffman@33792
|
25 |
(binding * (bool * binding option * string) list * mixfix) list) list
|
huffman@33792
|
26 |
-> theory -> theory
|
huffman@33792
|
27 |
|
huffman@33792
|
28 |
val add_new_domain:
|
huffman@35774
|
29 |
binding ->
|
huffman@33792
|
30 |
((string * string option) list * binding * mixfix *
|
huffman@33792
|
31 |
(binding * (bool * binding option * typ) list * mixfix) list) list
|
huffman@33792
|
32 |
-> theory -> theory
|
wenzelm@23152
|
33 |
end;
|
wenzelm@23152
|
34 |
|
huffman@31023
|
35 |
structure Domain_Extender :> DOMAIN_EXTENDER =
|
wenzelm@23152
|
36 |
struct
|
wenzelm@23152
|
37 |
|
huffman@40207
|
38 |
open HOLCF_Library;
|
huffman@40207
|
39 |
|
huffman@40207
|
40 |
fun first (x,_,_) = x;
|
huffman@40207
|
41 |
fun second (_,x,_) = x;
|
huffman@40207
|
42 |
fun third (_,_,x) = x;
|
huffman@40207
|
43 |
|
huffman@40207
|
44 |
fun upd_first f (x,y,z) = (f x, y, z);
|
huffman@40207
|
45 |
fun upd_second f (x,y,z) = ( x, f y, z);
|
huffman@40207
|
46 |
fun upd_third f (x,y,z) = ( x, y, f z);
|
wenzelm@23152
|
47 |
|
wenzelm@23152
|
48 |
(* ----- general testing and preprocessing of constructor list -------------- *)
|
huffman@30919
|
49 |
fun check_and_sort_domain
|
huffman@40146
|
50 |
(arg_sort : bool -> sort)
|
huffman@33790
|
51 |
(dtnvs : (string * typ list) list)
|
huffman@33790
|
52 |
(cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
|
huffman@33792
|
53 |
(thy : theory)
|
huffman@31288
|
54 |
: ((string * typ list) *
|
huffman@31288
|
55 |
(binding * (bool * binding option * typ) list * mixfix) list) list =
|
huffman@33790
|
56 |
let
|
huffman@33792
|
57 |
val defaultS = Sign.defaultS thy;
|
huffman@33790
|
58 |
|
huffman@33790
|
59 |
val test_dupl_typs =
|
huffman@33790
|
60 |
case duplicates (op =) (map fst dtnvs) of
|
huffman@33790
|
61 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups);
|
huffman@33790
|
62 |
|
huffman@33790
|
63 |
val all_cons = map (Binding.name_of o first) (flat cons'');
|
huffman@33790
|
64 |
val test_dupl_cons =
|
huffman@33790
|
65 |
case duplicates (op =) all_cons of
|
huffman@33790
|
66 |
[] => false | dups => error ("Duplicate constructors: "
|
huffman@33790
|
67 |
^ commas_quote dups);
|
huffman@33790
|
68 |
val all_sels =
|
huffman@33790
|
69 |
(map Binding.name_of o map_filter second o maps second) (flat cons'');
|
huffman@33790
|
70 |
val test_dupl_sels =
|
huffman@33790
|
71 |
case duplicates (op =) all_sels of
|
huffman@33790
|
72 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups);
|
huffman@33790
|
73 |
|
huffman@33790
|
74 |
fun test_dupl_tvars s =
|
huffman@33790
|
75 |
case duplicates (op =) (map(fst o dest_TFree)s) of
|
huffman@33790
|
76 |
[] => false | dups => error("Duplicate type arguments: "
|
huffman@33790
|
77 |
^commas_quote dups);
|
huffman@33790
|
78 |
val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs);
|
huffman@33790
|
79 |
|
huffman@33790
|
80 |
(* test for free type variables, illegal sort constraints on rhs,
|
huffman@33790
|
81 |
non-pcpo-types and invalid use of recursive type;
|
huffman@33790
|
82 |
replace sorts in type variables on rhs *)
|
huffman@33790
|
83 |
fun analyse_equation ((dname,typevars),cons') =
|
huffman@33790
|
84 |
let
|
huffman@33790
|
85 |
val tvars = map dest_TFree typevars;
|
huffman@33790
|
86 |
val distinct_typevars = map TFree tvars;
|
huffman@33790
|
87 |
fun rm_sorts (TFree(s,_)) = TFree(s,[])
|
huffman@33790
|
88 |
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
|
huffman@33790
|
89 |
| rm_sorts (TVar(s,_)) = TVar(s,[])
|
huffman@33790
|
90 |
and remove_sorts l = map rm_sorts l;
|
huffman@33790
|
91 |
fun analyse indirect (TFree(v,s)) =
|
huffman@33790
|
92 |
(case AList.lookup (op =) tvars v of
|
huffman@33790
|
93 |
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
|
huffman@33790
|
94 |
| SOME sort => if eq_set (op =) (s, defaultS) orelse
|
huffman@33790
|
95 |
eq_set (op =) (s, sort)
|
huffman@33790
|
96 |
then TFree(v,sort)
|
huffman@33790
|
97 |
else error ("Inconsistent sort constraint" ^
|
huffman@33790
|
98 |
" for type variable " ^ quote v))
|
huffman@33790
|
99 |
| analyse indirect (t as Type(s,typl)) =
|
huffman@33790
|
100 |
(case AList.lookup (op =) dtnvs s of
|
huffman@36119
|
101 |
NONE => Type (s, map (analyse false) typl)
|
huffman@33790
|
102 |
| SOME typevars =>
|
huffman@33790
|
103 |
if indirect
|
huffman@33790
|
104 |
then error ("Indirect recursion of type " ^
|
huffman@40207
|
105 |
quote (Syntax.string_of_typ_global thy t))
|
huffman@33790
|
106 |
else if dname <> s orelse
|
huffman@33790
|
107 |
(** BUG OR FEATURE?:
|
huffman@33790
|
108 |
mutual recursion may use different arguments **)
|
huffman@33790
|
109 |
remove_sorts typevars = remove_sorts typl
|
huffman@33790
|
110 |
then Type(s,map (analyse true) typl)
|
huffman@33790
|
111 |
else error ("Direct recursion of type " ^
|
huffman@40207
|
112 |
quote (Syntax.string_of_typ_global thy t) ^
|
huffman@33790
|
113 |
" with different arguments"))
|
huffman@40207
|
114 |
| analyse indirect (TVar _) = error "extender:analyse";
|
huffman@33790
|
115 |
fun check_pcpo lazy T =
|
huffman@40146
|
116 |
let val sort = arg_sort lazy in
|
huffman@40146
|
117 |
if Sign.of_sort thy (T, sort) then T
|
huffman@40146
|
118 |
else error ("Constructor argument type is not of sort " ^
|
huffman@40146
|
119 |
Syntax.string_of_sort_global thy sort ^ ": " ^
|
huffman@40207
|
120 |
Syntax.string_of_typ_global thy T)
|
huffman@33790
|
121 |
end;
|
huffman@33790
|
122 |
fun analyse_arg (lazy, sel, T) =
|
huffman@33790
|
123 |
(lazy, sel, check_pcpo lazy (analyse false T));
|
huffman@33790
|
124 |
fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
|
huffman@33790
|
125 |
in ((dname,distinct_typevars), map analyse_con cons') end;
|
huffman@33790
|
126 |
in ListPair.map analyse_equation (dtnvs,cons'')
|
huffman@33790
|
127 |
end; (* let *)
|
wenzelm@23152
|
128 |
|
wenzelm@23152
|
129 |
(* ----- calls for building new thy and thms -------------------------------- *)
|
wenzelm@23152
|
130 |
|
huffman@36118
|
131 |
type info =
|
huffman@36118
|
132 |
Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
|
huffman@36118
|
133 |
|
huffman@30919
|
134 |
fun gen_add_domain
|
huffman@33790
|
135 |
(prep_typ : theory -> 'a -> typ)
|
huffman@36118
|
136 |
(add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
|
huffman@40146
|
137 |
(arg_sort : bool -> sort)
|
huffman@35774
|
138 |
(comp_dbind : binding)
|
huffman@33792
|
139 |
(eqs''' : ((string * string option) list * binding * mixfix *
|
huffman@33792
|
140 |
(binding * (bool * binding option * 'a) list * mixfix) list) list)
|
huffman@35502
|
141 |
(thy : theory) =
|
huffman@33792
|
142 |
let
|
huffman@35506
|
143 |
val dtnvs : (binding * typ list * mixfix) list =
|
huffman@35506
|
144 |
let
|
huffman@35506
|
145 |
fun readS (SOME s) = Syntax.read_sort_global thy s
|
huffman@35506
|
146 |
| readS NONE = Sign.defaultS thy;
|
huffman@35506
|
147 |
fun readTFree (a, s) = TFree (a, readS s);
|
huffman@35506
|
148 |
in
|
huffman@35506
|
149 |
map (fn (vs,dname:binding,mx,_) =>
|
huffman@35506
|
150 |
(dname, map readTFree vs, mx)) eqs'''
|
huffman@35506
|
151 |
end;
|
huffman@33792
|
152 |
|
huffman@33792
|
153 |
fun thy_type (dname,tvars,mx) = (dname, length tvars, mx);
|
huffman@33792
|
154 |
fun thy_arity (dname,tvars,mx) =
|
huffman@40155
|
155 |
(Sign.full_name thy dname, map (snd o dest_TFree) tvars, arg_sort false);
|
huffman@33792
|
156 |
|
huffman@33792
|
157 |
(* this theory is used just for parsing and error checking *)
|
huffman@35502
|
158 |
val tmp_thy = thy
|
huffman@33792
|
159 |
|> Theory.copy
|
huffman@33792
|
160 |
|> Sign.add_types (map thy_type dtnvs)
|
huffman@33792
|
161 |
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
|
huffman@33792
|
162 |
|
huffman@35776
|
163 |
val dbinds : binding list =
|
huffman@35776
|
164 |
map (fn (_,dbind,_,_) => dbind) eqs''';
|
huffman@35506
|
165 |
val cons''' :
|
huffman@35506
|
166 |
(binding * (bool * binding option * 'a) list * mixfix) list list =
|
huffman@35506
|
167 |
map (fn (_,_,_,cons) => cons) eqs''';
|
huffman@35506
|
168 |
val cons'' :
|
huffman@35506
|
169 |
(binding * (bool * binding option * typ) list * mixfix) list list =
|
huffman@35506
|
170 |
map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
|
huffman@33792
|
171 |
val dtnvs' : (string * typ list) list =
|
huffman@35506
|
172 |
map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
|
huffman@33792
|
173 |
val eqs' : ((string * typ list) *
|
huffman@33792
|
174 |
(binding * (bool * binding option * typ) list * mixfix) list) list =
|
huffman@40146
|
175 |
check_and_sort_domain arg_sort dtnvs' cons'' tmp_thy;
|
huffman@36118
|
176 |
val dts : typ list = map (Type o fst) eqs';
|
huffman@33792
|
177 |
|
huffman@40207
|
178 |
fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T;
|
huffman@33792
|
179 |
fun mk_con_typ (bind, args, mx) =
|
huffman@33792
|
180 |
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
|
huffman@33792
|
181 |
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
|
huffman@36118
|
182 |
val repTs : typ list = map mk_eq_typ eqs';
|
huffman@33792
|
183 |
|
huffman@36118
|
184 |
val iso_spec : (binding * mixfix * (typ * typ)) list =
|
huffman@36118
|
185 |
map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
|
huffman@36118
|
186 |
(dtnvs ~~ (dts ~~ repTs));
|
huffman@36118
|
187 |
|
huffman@36118
|
188 |
val ((iso_infos, take_info), thy) = add_isos iso_spec thy;
|
huffman@36118
|
189 |
|
huffman@40197
|
190 |
val (constr_infos, thy) =
|
huffman@33790
|
191 |
thy
|
huffman@40197
|
192 |
|> fold_map (fn ((dbind, (_,cs)), info) =>
|
huffman@40197
|
193 |
Domain_Constructors.add_domain_constructors dbind cs info)
|
huffman@40197
|
194 |
(dbinds ~~ eqs' ~~ iso_infos);
|
huffman@40197
|
195 |
|
huffman@40207
|
196 |
val (take_rews, thy) =
|
huffman@40207
|
197 |
Domain_Theorems.comp_theorems comp_dbind
|
huffman@40207
|
198 |
dbinds take_info constr_infos thy;
|
huffman@33790
|
199 |
in
|
huffman@40207
|
200 |
thy
|
huffman@33790
|
201 |
end;
|
wenzelm@23152
|
202 |
|
huffman@36118
|
203 |
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
|
huffman@36118
|
204 |
let
|
huffman@36118
|
205 |
fun prep (dbind, mx, (lhsT, rhsT)) =
|
huffman@36118
|
206 |
let val (dname, vs) = dest_Type lhsT;
|
huffman@36118
|
207 |
in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end;
|
huffman@36118
|
208 |
in
|
huffman@36118
|
209 |
Domain_Isomorphism.domain_isomorphism (map prep spec)
|
huffman@36118
|
210 |
end;
|
wenzelm@23152
|
211 |
|
huffman@40146
|
212 |
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
|
huffman@40167
|
213 |
fun rep_arg lazy = @{sort bifinite};
|
huffman@40146
|
214 |
|
huffman@36118
|
215 |
val add_domain =
|
huffman@40146
|
216 |
gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg;
|
huffman@36118
|
217 |
|
huffman@36118
|
218 |
val add_new_domain =
|
huffman@40146
|
219 |
gen_add_domain Sign.certify_typ define_isos rep_arg;
|
huffman@36118
|
220 |
|
huffman@36118
|
221 |
val add_domain_cmd =
|
huffman@40146
|
222 |
gen_add_domain Syntax.read_typ_global Domain_Axioms.add_axioms pcpo_arg;
|
huffman@36118
|
223 |
|
huffman@36118
|
224 |
val add_new_domain_cmd =
|
huffman@40146
|
225 |
gen_add_domain Syntax.read_typ_global define_isos rep_arg;
|
huffman@33792
|
226 |
|
wenzelm@23152
|
227 |
|
wenzelm@23152
|
228 |
(** outer syntax **)
|
wenzelm@23152
|
229 |
|
wenzelm@36970
|
230 |
val _ = Keyword.keyword "lazy";
|
wenzelm@24867
|
231 |
|
huffman@30919
|
232 |
val dest_decl : (bool * binding option * string) parser =
|
wenzelm@36970
|
233 |
Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
|
wenzelm@36970
|
234 |
(Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1
|
wenzelm@36970
|
235 |
|| Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
|
huffman@33790
|
236 |
>> (fn t => (true,NONE,t))
|
wenzelm@36970
|
237 |
|| Parse.typ >> (fn t => (false,NONE,t));
|
wenzelm@23152
|
238 |
|
wenzelm@23152
|
239 |
val cons_decl =
|
wenzelm@36970
|
240 |
Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
|
wenzelm@23152
|
241 |
|
huffman@30916
|
242 |
val domain_decl =
|
wenzelm@36970
|
243 |
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
|
wenzelm@36970
|
244 |
(Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
|
huffman@30916
|
245 |
|
wenzelm@23152
|
246 |
val domains_decl =
|
wenzelm@36970
|
247 |
Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
|
wenzelm@36970
|
248 |
Parse.and_list1 domain_decl;
|
huffman@30916
|
249 |
|
huffman@33790
|
250 |
fun mk_domain
|
huffman@33792
|
251 |
(definitional : bool)
|
huffman@35774
|
252 |
(opt_name : binding option,
|
huffman@33790
|
253 |
doms : ((((string * string option) list * binding) * mixfix) *
|
huffman@33790
|
254 |
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
|
huffman@33790
|
255 |
let
|
huffman@33790
|
256 |
val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
|
huffman@33790
|
257 |
val specs : ((string * string option) list * binding * mixfix *
|
huffman@33790
|
258 |
(binding * (bool * binding option * string) list * mixfix) list) list =
|
huffman@33790
|
259 |
map (fn (((vs, t), mx), cons) =>
|
huffman@33790
|
260 |
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
|
huffman@35774
|
261 |
val comp_dbind =
|
huffman@35774
|
262 |
case opt_name of NONE => Binding.name (space_implode "_" names)
|
huffman@35774
|
263 |
| SOME s => s;
|
huffman@33792
|
264 |
in
|
huffman@33792
|
265 |
if definitional
|
huffman@35774
|
266 |
then add_new_domain_cmd comp_dbind specs
|
huffman@35774
|
267 |
else add_domain_cmd comp_dbind specs
|
huffman@33792
|
268 |
end;
|
wenzelm@23152
|
269 |
|
wenzelm@24867
|
270 |
val _ =
|
wenzelm@36970
|
271 |
Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
|
wenzelm@36970
|
272 |
Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
|
huffman@33792
|
273 |
|
huffman@33792
|
274 |
val _ =
|
wenzelm@36970
|
275 |
Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
|
wenzelm@36970
|
276 |
Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
|
wenzelm@23152
|
277 |
|
wenzelm@24867
|
278 |
end;
|