wenzelm@43022
|
1 |
(* Title: HOL/HOLCF/Tools/Domain/domain.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 |
|
huffman@40221
|
8 |
signature DOMAIN =
|
wenzelm@23152
|
9 |
sig
|
huffman@33790
|
10 |
val add_domain_cmd:
|
huffman@33790
|
11 |
((string * string option) list * binding * mixfix *
|
huffman@33790
|
12 |
(binding * (bool * binding option * string) list * mixfix) list) list
|
huffman@33790
|
13 |
-> theory -> theory
|
huffman@33790
|
14 |
|
huffman@33790
|
15 |
val add_domain:
|
huffman@40456
|
16 |
((string * sort) list * binding * mixfix *
|
huffman@33790
|
17 |
(binding * (bool * binding option * typ) list * mixfix) list) list
|
huffman@33790
|
18 |
-> theory -> theory
|
huffman@33792
|
19 |
|
huffman@33792
|
20 |
val add_new_domain_cmd:
|
huffman@33792
|
21 |
((string * string option) list * binding * mixfix *
|
huffman@33792
|
22 |
(binding * (bool * binding option * string) list * mixfix) list) list
|
huffman@33792
|
23 |
-> theory -> theory
|
huffman@33792
|
24 |
|
huffman@33792
|
25 |
val add_new_domain:
|
huffman@40456
|
26 |
((string * sort) list * binding * mixfix *
|
huffman@33792
|
27 |
(binding * (bool * binding option * typ) list * mixfix) list) list
|
huffman@33792
|
28 |
-> theory -> theory
|
huffman@41080
|
29 |
end
|
wenzelm@23152
|
30 |
|
huffman@41544
|
31 |
structure Domain : DOMAIN =
|
wenzelm@23152
|
32 |
struct
|
wenzelm@23152
|
33 |
|
huffman@41080
|
34 |
open HOLCF_Library
|
huffman@40207
|
35 |
|
huffman@41080
|
36 |
fun first (x,_,_) = x
|
huffman@41080
|
37 |
fun second (_,x,_) = x
|
huffman@40207
|
38 |
|
wenzelm@23152
|
39 |
(* ----- calls for building new thy and thms -------------------------------- *)
|
wenzelm@23152
|
40 |
|
huffman@36118
|
41 |
type info =
|
huffman@41080
|
42 |
Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info
|
huffman@36118
|
43 |
|
huffman@40720
|
44 |
fun add_arity ((b, sorts, mx), sort) thy : theory =
|
huffman@40720
|
45 |
thy
|
wenzelm@43246
|
46 |
|> Sign.add_types_global [(b, length sorts, mx)]
|
huffman@41080
|
47 |
|> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
|
huffman@40720
|
48 |
|
huffman@30919
|
49 |
fun gen_add_domain
|
huffman@40456
|
50 |
(prep_sort : theory -> 'a -> sort)
|
huffman@40456
|
51 |
(prep_typ : theory -> (string * sort) list -> 'b -> typ)
|
huffman@36118
|
52 |
(add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
|
huffman@40146
|
53 |
(arg_sort : bool -> sort)
|
huffman@40456
|
54 |
(raw_specs : ((string * 'a) list * binding * mixfix *
|
huffman@40456
|
55 |
(binding * (bool * binding option * 'b) list * mixfix) list) list)
|
huffman@35502
|
56 |
(thy : theory) =
|
huffman@33792
|
57 |
let
|
huffman@35506
|
58 |
val dtnvs : (binding * typ list * mixfix) list =
|
huffman@35506
|
59 |
let
|
huffman@41080
|
60 |
fun prep_tvar (a, s) = TFree (a, prep_sort thy s)
|
huffman@35506
|
61 |
in
|
huffman@40225
|
62 |
map (fn (vs, dbind, mx, _) =>
|
huffman@40456
|
63 |
(dbind, map prep_tvar vs, mx)) raw_specs
|
huffman@41080
|
64 |
end
|
huffman@33792
|
65 |
|
huffman@40223
|
66 |
fun thy_arity (dbind, tvars, mx) =
|
huffman@41080
|
67 |
((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false)
|
huffman@33792
|
68 |
|
huffman@33792
|
69 |
(* this theory is used just for parsing and error checking *)
|
huffman@35502
|
70 |
val tmp_thy = thy
|
huffman@33792
|
71 |
|> Theory.copy
|
huffman@41080
|
72 |
|> fold (add_arity o thy_arity) dtnvs
|
huffman@33792
|
73 |
|
huffman@35776
|
74 |
val dbinds : binding list =
|
huffman@41080
|
75 |
map (fn (_,dbind,_,_) => dbind) raw_specs
|
huffman@40225
|
76 |
val raw_rhss :
|
huffman@40456
|
77 |
(binding * (bool * binding option * 'b) list * mixfix) list list =
|
huffman@41080
|
78 |
map (fn (_,_,_,cons) => cons) raw_specs
|
huffman@33792
|
79 |
val dtnvs' : (string * typ list) list =
|
huffman@44951
|
80 |
map (fn (dbind, vs, _) => (Sign.full_name thy dbind, vs)) dtnvs
|
huffman@40225
|
81 |
|
huffman@41080
|
82 |
val all_cons = map (Binding.name_of o first) (flat raw_rhss)
|
huffman@44951
|
83 |
val _ =
|
huffman@40225
|
84 |
case duplicates (op =) all_cons of
|
huffman@40225
|
85 |
[] => false | dups => error ("Duplicate constructors: "
|
huffman@41080
|
86 |
^ commas_quote dups)
|
huffman@40225
|
87 |
val all_sels =
|
huffman@41080
|
88 |
(map Binding.name_of o map_filter second o maps second) (flat raw_rhss)
|
huffman@44951
|
89 |
val _ =
|
huffman@40225
|
90 |
case duplicates (op =) all_sels of
|
huffman@41080
|
91 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups)
|
huffman@40225
|
92 |
|
huffman@40225
|
93 |
fun test_dupl_tvars s =
|
huffman@40225
|
94 |
case duplicates (op =) (map(fst o dest_TFree)s) of
|
huffman@40225
|
95 |
[] => false | dups => error("Duplicate type arguments: "
|
huffman@41080
|
96 |
^commas_quote dups)
|
huffman@44951
|
97 |
val _ = exists test_dupl_tvars (map snd dtnvs')
|
huffman@40225
|
98 |
|
huffman@40225
|
99 |
val sorts : (string * sort) list =
|
huffman@41080
|
100 |
let val all_sorts = map (map dest_TFree o snd) dtnvs'
|
huffman@40225
|
101 |
in
|
huffman@40225
|
102 |
case distinct (eq_set (op =)) all_sorts of
|
huffman@40225
|
103 |
[sorts] => sorts
|
huffman@40225
|
104 |
| _ => error "Mutually recursive domains must have same type parameters"
|
huffman@41080
|
105 |
end
|
huffman@40225
|
106 |
|
huffman@40225
|
107 |
(* a lazy argument may have an unpointed type *)
|
huffman@40225
|
108 |
(* unless the argument has a selector function *)
|
huffman@40225
|
109 |
fun check_pcpo (lazy, sel, T) =
|
huffman@40225
|
110 |
let val sort = arg_sort (lazy andalso is_none sel) in
|
huffman@40225
|
111 |
if Sign.of_sort tmp_thy (T, sort) then ()
|
huffman@40225
|
112 |
else error ("Constructor argument type is not of sort " ^
|
huffman@40225
|
113 |
Syntax.string_of_sort_global tmp_thy sort ^ ": " ^
|
huffman@40225
|
114 |
Syntax.string_of_typ_global tmp_thy T)
|
huffman@41080
|
115 |
end
|
huffman@40225
|
116 |
|
huffman@40225
|
117 |
(* test for free type variables, illegal sort constraints on rhs,
|
huffman@41080
|
118 |
non-pcpo-types and invalid use of recursive type
|
huffman@40225
|
119 |
replace sorts in type variables on rhs *)
|
huffman@41080
|
120 |
val rec_tab = Domain_Take_Proofs.get_rec_tab thy
|
huffman@44951
|
121 |
fun check_rec _ (T as TFree (v,_)) =
|
huffman@40225
|
122 |
if AList.defined (op =) sorts v then T
|
huffman@40225
|
123 |
else error ("Free type variable " ^ quote v ^ " on rhs.")
|
huffman@44876
|
124 |
| check_rec no_rec (T as Type (s, Ts)) =
|
huffman@40225
|
125 |
(case AList.lookup (op =) dtnvs' s of
|
huffman@40225
|
126 |
NONE =>
|
huffman@44876
|
127 |
let val no_rec' =
|
huffman@44876
|
128 |
if no_rec = NONE then
|
huffman@44876
|
129 |
if Symtab.defined rec_tab s then NONE else SOME s
|
huffman@44876
|
130 |
else no_rec
|
huffman@44876
|
131 |
in Type (s, map (check_rec no_rec') Ts) end
|
huffman@40225
|
132 |
| SOME typevars =>
|
huffman@40225
|
133 |
if typevars <> Ts
|
huffman@40225
|
134 |
then error ("Recursion of type " ^
|
huffman@40225
|
135 |
quote (Syntax.string_of_typ_global tmp_thy T) ^
|
huffman@40225
|
136 |
" with different arguments")
|
huffman@44876
|
137 |
else (case no_rec of
|
huffman@44876
|
138 |
NONE => T
|
huffman@44876
|
139 |
| SOME c =>
|
huffman@44876
|
140 |
error ("Illegal indirect recursion of type " ^
|
huffman@44876
|
141 |
quote (Syntax.string_of_typ_global tmp_thy T) ^
|
huffman@44876
|
142 |
" under type constructor " ^ quote c)))
|
huffman@44951
|
143 |
| check_rec _ (TVar _) = error "extender:check_rec"
|
huffman@40225
|
144 |
|
huffman@40225
|
145 |
fun prep_arg (lazy, sel, raw_T) =
|
huffman@40225
|
146 |
let
|
huffman@41080
|
147 |
val T = prep_typ tmp_thy sorts raw_T
|
huffman@44876
|
148 |
val _ = check_rec NONE T
|
huffman@41080
|
149 |
val _ = check_pcpo (lazy, sel, T)
|
huffman@41080
|
150 |
in (lazy, sel, T) end
|
huffman@41080
|
151 |
fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
|
huffman@41080
|
152 |
fun prep_rhs cons = map prep_con cons
|
huffman@40225
|
153 |
val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
|
huffman@41080
|
154 |
map prep_rhs raw_rhss
|
huffman@33792
|
155 |
|
huffman@44951
|
156 |
fun mk_arg_typ (lazy, _, T) = if lazy then mk_upT T else T
|
huffman@44951
|
157 |
fun mk_con_typ (_, args, _) =
|
huffman@41080
|
158 |
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args)
|
huffman@41080
|
159 |
fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons)
|
huffman@40223
|
160 |
|
huffman@41080
|
161 |
val absTs : typ list = map Type dtnvs'
|
huffman@41080
|
162 |
val repTs : typ list = map mk_rhs_typ rhss
|
huffman@33792
|
163 |
|
huffman@36118
|
164 |
val iso_spec : (binding * mixfix * (typ * typ)) list =
|
huffman@36118
|
165 |
map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
|
huffman@41080
|
166 |
(dtnvs ~~ (absTs ~~ repTs))
|
huffman@36118
|
167 |
|
huffman@41080
|
168 |
val ((iso_infos, take_info), thy) = add_isos iso_spec thy
|
huffman@36118
|
169 |
|
huffman@40197
|
170 |
val (constr_infos, thy) =
|
huffman@33790
|
171 |
thy
|
huffman@40223
|
172 |
|> fold_map (fn ((dbind, cons), info) =>
|
huffman@40223
|
173 |
Domain_Constructors.add_domain_constructors dbind cons info)
|
huffman@41080
|
174 |
(dbinds ~~ rhss ~~ iso_infos)
|
huffman@40197
|
175 |
|
huffman@44951
|
176 |
val (_, thy) =
|
huffman@40343
|
177 |
Domain_Induction.comp_theorems
|
huffman@41080
|
178 |
dbinds take_info constr_infos thy
|
huffman@33790
|
179 |
in
|
huffman@40207
|
180 |
thy
|
huffman@41080
|
181 |
end
|
wenzelm@23152
|
182 |
|
huffman@36118
|
183 |
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
|
huffman@36118
|
184 |
let
|
huffman@36118
|
185 |
fun prep (dbind, mx, (lhsT, rhsT)) =
|
huffman@44951
|
186 |
let val (_, vs) = dest_Type lhsT
|
huffman@41080
|
187 |
in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
|
huffman@36118
|
188 |
in
|
huffman@36118
|
189 |
Domain_Isomorphism.domain_isomorphism (map prep spec)
|
huffman@41080
|
190 |
end
|
wenzelm@23152
|
191 |
|
huffman@41080
|
192 |
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}
|
huffman@41080
|
193 |
fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"}
|
huffman@40146
|
194 |
|
huffman@40456
|
195 |
fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
|
huffman@41080
|
196 |
| read_sort thy NONE = Sign.defaultS thy
|
huffman@40456
|
197 |
|
huffman@40225
|
198 |
(* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *)
|
huffman@40225
|
199 |
fun read_typ thy sorts str =
|
huffman@40225
|
200 |
let
|
wenzelm@43232
|
201 |
val ctxt = Proof_Context.init_global thy
|
huffman@41080
|
202 |
|> fold (Variable.declare_typ o TFree) sorts
|
huffman@41080
|
203 |
in Syntax.read_typ ctxt str end
|
huffman@40225
|
204 |
|
huffman@40225
|
205 |
fun cert_typ sign sorts raw_T =
|
huffman@40225
|
206 |
let
|
huffman@40225
|
207 |
val T = Type.no_tvars (Sign.certify_typ sign raw_T)
|
huffman@41080
|
208 |
handle TYPE (msg, _, _) => error msg
|
huffman@41080
|
209 |
val sorts' = Term.add_tfreesT T sorts
|
huffman@40225
|
210 |
val _ =
|
huffman@40225
|
211 |
case duplicates (op =) (map fst sorts') of
|
huffman@40225
|
212 |
[] => ()
|
huffman@40225
|
213 |
| dups => error ("Inconsistent sort constraints for " ^ commas dups)
|
huffman@41080
|
214 |
in T end
|
huffman@40225
|
215 |
|
huffman@36118
|
216 |
val add_domain =
|
huffman@41080
|
217 |
gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg
|
huffman@36118
|
218 |
|
huffman@36118
|
219 |
val add_new_domain =
|
huffman@41080
|
220 |
gen_add_domain (K I) cert_typ define_isos rep_arg
|
huffman@36118
|
221 |
|
huffman@36118
|
222 |
val add_domain_cmd =
|
huffman@41080
|
223 |
gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg
|
huffman@36118
|
224 |
|
huffman@36118
|
225 |
val add_new_domain_cmd =
|
huffman@41080
|
226 |
gen_add_domain read_sort read_typ define_isos rep_arg
|
huffman@33792
|
227 |
|
wenzelm@23152
|
228 |
|
wenzelm@23152
|
229 |
(** outer syntax **)
|
wenzelm@23152
|
230 |
|
huffman@30919
|
231 |
val dest_decl : (bool * binding option * string) parser =
|
wenzelm@47823
|
232 |
@{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false --
|
wenzelm@47823
|
233 |
(Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ) --| @{keyword ")"} >> Parse.triple1
|
wenzelm@47823
|
234 |
|| @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"}
|
wenzelm@47823
|
235 |
>> (fn t => (true, NONE, t))
|
wenzelm@47823
|
236 |
|| Parse.typ >> (fn t => (false, NONE, t))
|
wenzelm@23152
|
237 |
|
wenzelm@23152
|
238 |
val cons_decl =
|
huffman@41080
|
239 |
Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix
|
wenzelm@23152
|
240 |
|
huffman@30916
|
241 |
val domain_decl =
|
wenzelm@36970
|
242 |
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
|
wenzelm@47823
|
243 |
(@{keyword "="} |-- Parse.enum1 "|" cons_decl)
|
huffman@30916
|
244 |
|
wenzelm@23152
|
245 |
val domains_decl =
|
wenzelm@47823
|
246 |
Scan.optional (@{keyword "("} |-- (@{keyword "unsafe"} >> K true) --| @{keyword ")"}) false --
|
huffman@41080
|
247 |
Parse.and_list1 domain_decl
|
huffman@30916
|
248 |
|
huffman@33790
|
249 |
fun mk_domain
|
huffman@40567
|
250 |
(unsafe : bool,
|
huffman@40567
|
251 |
doms : ((((string * string option) list * binding) * mixfix) *
|
huffman@33790
|
252 |
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
|
huffman@33790
|
253 |
let
|
huffman@33790
|
254 |
val specs : ((string * string option) list * binding * mixfix *
|
huffman@33790
|
255 |
(binding * (bool * binding option * string) list * mixfix) list) list =
|
huffman@33790
|
256 |
map (fn (((vs, t), mx), cons) =>
|
huffman@41080
|
257 |
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms
|
huffman@33792
|
258 |
in
|
huffman@40567
|
259 |
if unsafe
|
huffman@40567
|
260 |
then add_domain_cmd specs
|
huffman@40567
|
261 |
else add_new_domain_cmd specs
|
huffman@41080
|
262 |
end
|
wenzelm@23152
|
263 |
|
wenzelm@24867
|
264 |
val _ =
|
wenzelm@36970
|
265 |
Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
|
huffman@41080
|
266 |
Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain))
|
wenzelm@23152
|
267 |
|
huffman@41080
|
268 |
end
|