author | wenzelm |
Sun, 20 Nov 2011 21:07:06 +0100 | |
changeset 45606 | b1e1508643b1 |
parent 44080 | 53d95b52954c |
child 46947 | b8c7eb0c2f89 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/Domain/domain.ML |
23152 | 2 |
Author: David von Oheimb |
35794 | 3 |
Author: Brian Huffman |
23152 | 4 |
|
5 |
Theory extender for domain command, including theory syntax. |
|
6 |
*) |
|
7 |
||
40040
3adb92ee2f22
rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
huffman
parents:
40026
diff
changeset
|
8 |
signature DOMAIN = |
23152 | 9 |
sig |
33796 | 10 |
val add_domain_cmd: |
11 |
((string * string option) list * binding * mixfix * |
|
12 |
(binding * (bool * binding option * string) list * mixfix) list) list |
|
13 |
-> theory -> theory |
|
14 |
||
15 |
val add_domain: |
|
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
16 |
((string * sort) list * binding * mixfix * |
33796 | 17 |
(binding * (bool * binding option * typ) list * mixfix) list) list |
18 |
-> theory -> theory |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
19 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
20 |
val add_new_domain_cmd: |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
21 |
((string * string option) list * binding * mixfix * |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
22 |
(binding * (bool * binding option * string) list * mixfix) list) list |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
23 |
-> theory -> theory |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
24 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
25 |
val add_new_domain: |
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
26 |
((string * sort) list * binding * mixfix * |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
27 |
(binding * (bool * binding option * typ) list * mixfix) list) list |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
28 |
-> theory -> theory |
40832 | 29 |
end |
23152 | 30 |
|
41296
6aaf80ea9715
switch to transparent ascription, to avoid warning messages
huffman
parents:
40832
diff
changeset
|
31 |
structure Domain : DOMAIN = |
23152 | 32 |
struct |
33 |
||
40832 | 34 |
open HOLCF_Library |
40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40019
diff
changeset
|
35 |
|
40832 | 36 |
fun first (x,_,_) = x |
37 |
fun second (_,x,_) = x |
|
40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40019
diff
changeset
|
38 |
|
23152 | 39 |
(* ----- calls for building new thy and thms -------------------------------- *) |
40 |
||
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
41 |
type info = |
40832 | 42 |
Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
43 |
|
40485 | 44 |
fun add_arity ((b, sorts, mx), sort) thy : theory = |
45 |
thy |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
46 |
|> Sign.add_types_global [(b, length sorts, mx)] |
40832 | 47 |
|> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort) |
40485 | 48 |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
49 |
fun gen_add_domain |
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
50 |
(prep_sort : theory -> 'a -> sort) |
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
51 |
(prep_typ : theory -> (string * sort) list -> 'b -> typ) |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
52 |
(add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory) |
39965
da88519e6a0b
new_domain emits proper error message when a constructor argument type does not have sort 'rep'
huffman
parents:
39557
diff
changeset
|
53 |
(arg_sort : bool -> sort) |
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
54 |
(raw_specs : ((string * 'a) list * binding * mixfix * |
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
55 |
(binding * (bool * binding option * 'b) list * mixfix) list) list) |
35516 | 56 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
57 |
let |
35520 | 58 |
val dtnvs : (binding * typ list * mixfix) list = |
59 |
let |
|
40832 | 60 |
fun prep_tvar (a, s) = TFree (a, prep_sort thy s) |
35520 | 61 |
in |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
62 |
map (fn (vs, dbind, mx, _) => |
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
63 |
(dbind, map prep_tvar vs, mx)) raw_specs |
40832 | 64 |
end |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
65 |
|
40042
87c72a02eaf2
simplify check_and_sort_domain; more meaningful variable names
huffman
parents:
40040
diff
changeset
|
66 |
fun thy_arity (dbind, tvars, mx) = |
40832 | 67 |
((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false) |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
68 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
69 |
(* this theory is used just for parsing and error checking *) |
35516 | 70 |
val tmp_thy = thy |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
71 |
|> Theory.copy |
40832 | 72 |
|> fold (add_arity o thy_arity) dtnvs |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
73 |
|
35776
b0bc15d8ad3b
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
huffman
parents:
35775
diff
changeset
|
74 |
val dbinds : binding list = |
40832 | 75 |
map (fn (_,dbind,_,_) => dbind) raw_specs |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
76 |
val raw_rhss : |
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
77 |
(binding * (bool * binding option * 'b) list * mixfix) list list = |
40832 | 78 |
map (fn (_,_,_,cons) => cons) raw_specs |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
79 |
val dtnvs' : (string * typ list) list = |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
80 |
map (fn (dbind, vs, _) => (Sign.full_name thy dbind, vs)) dtnvs |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
81 |
|
40832 | 82 |
val all_cons = map (Binding.name_of o first) (flat raw_rhss) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
83 |
val _ = |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
84 |
case duplicates (op =) all_cons of |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
85 |
[] => false | dups => error ("Duplicate constructors: " |
40832 | 86 |
^ commas_quote dups) |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
87 |
val all_sels = |
40832 | 88 |
(map Binding.name_of o map_filter second o maps second) (flat raw_rhss) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
89 |
val _ = |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
90 |
case duplicates (op =) all_sels of |
40832 | 91 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups) |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
92 |
|
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
93 |
fun test_dupl_tvars s = |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
94 |
case duplicates (op =) (map(fst o dest_TFree)s) of |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
95 |
[] => false | dups => error("Duplicate type arguments: " |
40832 | 96 |
^commas_quote dups) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
97 |
val _ = exists test_dupl_tvars (map snd dtnvs') |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
98 |
|
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
99 |
val sorts : (string * sort) list = |
40832 | 100 |
let val all_sorts = map (map dest_TFree o snd) dtnvs' |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
101 |
in |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
102 |
case distinct (eq_set (op =)) all_sorts of |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
103 |
[sorts] => sorts |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
104 |
| _ => error "Mutually recursive domains must have same type parameters" |
40832 | 105 |
end |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
106 |
|
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
107 |
(* a lazy argument may have an unpointed type *) |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
108 |
(* unless the argument has a selector function *) |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
109 |
fun check_pcpo (lazy, sel, T) = |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
110 |
let val sort = arg_sort (lazy andalso is_none sel) in |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
111 |
if Sign.of_sort tmp_thy (T, sort) then () |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
112 |
else error ("Constructor argument type is not of sort " ^ |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
113 |
Syntax.string_of_sort_global tmp_thy sort ^ ": " ^ |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
114 |
Syntax.string_of_typ_global tmp_thy T) |
40832 | 115 |
end |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
116 |
|
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
117 |
(* test for free type variables, illegal sort constraints on rhs, |
40832 | 118 |
non-pcpo-types and invalid use of recursive type |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
119 |
replace sorts in type variables on rhs *) |
40832 | 120 |
val rec_tab = Domain_Take_Proofs.get_rec_tab thy |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
121 |
fun check_rec _ (T as TFree (v,_)) = |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
122 |
if AList.defined (op =) sorts v then T |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
123 |
else error ("Free type variable " ^ quote v ^ " on rhs.") |
44005
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
124 |
| check_rec no_rec (T as Type (s, Ts)) = |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
125 |
(case AList.lookup (op =) dtnvs' s of |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
126 |
NONE => |
44005
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
127 |
let val no_rec' = |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
128 |
if no_rec = NONE then |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
129 |
if Symtab.defined rec_tab s then NONE else SOME s |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
130 |
else no_rec |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
131 |
in Type (s, map (check_rec no_rec') Ts) end |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
132 |
| SOME typevars => |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
133 |
if typevars <> Ts |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
134 |
then error ("Recursion of type " ^ |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
135 |
quote (Syntax.string_of_typ_global tmp_thy T) ^ |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
136 |
" with different arguments") |
44005
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
137 |
else (case no_rec of |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
138 |
NONE => T |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
139 |
| SOME c => |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
140 |
error ("Illegal indirect recursion of type " ^ |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
141 |
quote (Syntax.string_of_typ_global tmp_thy T) ^ |
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
142 |
" under type constructor " ^ quote c))) |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
143 |
| check_rec _ (TVar _) = error "extender:check_rec" |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
144 |
|
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
145 |
fun prep_arg (lazy, sel, raw_T) = |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
146 |
let |
40832 | 147 |
val T = prep_typ tmp_thy sorts raw_T |
44005
421f8bc19ce4
domain package: more informative error message for illegal indirect recursion
huffman
parents:
42375
diff
changeset
|
148 |
val _ = check_rec NONE T |
40832 | 149 |
val _ = check_pcpo (lazy, sel, T) |
150 |
in (lazy, sel, T) end |
|
151 |
fun prep_con (b, args, mx) = (b, map prep_arg args, mx) |
|
152 |
fun prep_rhs cons = map prep_con cons |
|
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
153 |
val rhss : (binding * (bool * binding option * typ) list * mixfix) list list = |
40832 | 154 |
map prep_rhs raw_rhss |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
155 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
156 |
fun mk_arg_typ (lazy, _, T) = if lazy then mk_upT T else T |
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
157 |
fun mk_con_typ (_, args, _) = |
40832 | 158 |
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args) |
159 |
fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons) |
|
40042
87c72a02eaf2
simplify check_and_sort_domain; more meaningful variable names
huffman
parents:
40040
diff
changeset
|
160 |
|
40832 | 161 |
val absTs : typ list = map Type dtnvs' |
162 |
val repTs : typ list = map mk_rhs_typ rhss |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
163 |
|
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
164 |
val iso_spec : (binding * mixfix * (typ * typ)) list = |
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
165 |
map (fn ((dbind, _, mx), eq) => (dbind, mx, eq)) |
40832 | 166 |
(dtnvs ~~ (absTs ~~ repTs)) |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
167 |
|
40832 | 168 |
val ((iso_infos, take_info), thy) = add_isos iso_spec thy |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
169 |
|
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
39986
diff
changeset
|
170 |
val (constr_infos, thy) = |
33796 | 171 |
thy |
40042
87c72a02eaf2
simplify check_and_sort_domain; more meaningful variable names
huffman
parents:
40040
diff
changeset
|
172 |
|> fold_map (fn ((dbind, cons), info) => |
87c72a02eaf2
simplify check_and_sort_domain; more meaningful variable names
huffman
parents:
40040
diff
changeset
|
173 |
Domain_Constructors.add_domain_constructors dbind cons info) |
40832 | 174 |
(dbinds ~~ rhss ~~ iso_infos) |
40016
2eff1cbc1ccb
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
huffman
parents:
39986
diff
changeset
|
175 |
|
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
176 |
val (_, thy) = |
40097
429cd74f795f
remove legacy comp_dbind option from domain package
huffman
parents:
40044
diff
changeset
|
177 |
Domain_Induction.comp_theorems |
40832 | 178 |
dbinds take_info constr_infos thy |
33796 | 179 |
in |
40026
8f8f18a88685
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
huffman
parents:
40019
diff
changeset
|
180 |
thy |
40832 | 181 |
end |
23152 | 182 |
|
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
183 |
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) = |
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
184 |
let |
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
185 |
fun prep (dbind, mx, (lhsT, rhsT)) = |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
44005
diff
changeset
|
186 |
let val (_, vs) = dest_Type lhsT |
40832 | 187 |
in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
188 |
in |
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
189 |
Domain_Isomorphism.domain_isomorphism (map prep spec) |
40832 | 190 |
end |
23152 | 191 |
|
40832 | 192 |
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo} |
193 |
fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"} |
|
39965
da88519e6a0b
new_domain emits proper error message when a constructor argument type does not have sort 'rep'
huffman
parents:
39557
diff
changeset
|
194 |
|
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
195 |
fun read_sort thy (SOME s) = Syntax.read_sort_global thy s |
40832 | 196 |
| read_sort thy NONE = Sign.defaultS thy |
40215
d8fd7ae0254f
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
huffman
parents:
40097
diff
changeset
|
197 |
|
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
198 |
(* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *) |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
199 |
fun read_typ thy sorts str = |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
200 |
let |
42361 | 201 |
val ctxt = Proof_Context.init_global thy |
40832 | 202 |
|> fold (Variable.declare_typ o TFree) sorts |
203 |
in Syntax.read_typ ctxt str end |
|
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
204 |
|
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
205 |
fun cert_typ sign sorts raw_T = |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
206 |
let |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
207 |
val T = Type.no_tvars (Sign.certify_typ sign raw_T) |
40832 | 208 |
handle TYPE (msg, _, _) => error msg |
209 |
val sorts' = Term.add_tfreesT T sorts |
|
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
210 |
val _ = |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
211 |
case duplicates (op =) (map fst sorts') of |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
212 |
[] => () |
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
213 |
| dups => error ("Inconsistent sort constraints for " ^ commas dups) |
40832 | 214 |
in T end |
40044
89381a2f8864
combine check_and_sort_domain with main function; rewrite much of the error-checking code
huffman
parents:
40043
diff
changeset
|
215 |
|
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
216 |
val add_domain = |
40832 | 217 |
gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
218 |
|
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
219 |
val add_new_domain = |
40832 | 220 |
gen_add_domain (K I) cert_typ define_isos rep_arg |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
221 |
|
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
222 |
val add_domain_cmd = |
40832 | 223 |
gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg |
36118
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
224 |
|
413d6d1f0f6e
share more code between definitional and axiomatic domain packages
huffman
parents:
36117
diff
changeset
|
225 |
val add_new_domain_cmd = |
40832 | 226 |
gen_add_domain read_sort read_typ define_isos rep_arg |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
227 |
|
23152 | 228 |
|
229 |
(** outer syntax **) |
|
230 |
||
40832 | 231 |
val _ = Keyword.keyword "lazy" |
232 |
val _ = Keyword.keyword "unsafe" |
|
24867 | 233 |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
234 |
val dest_decl : (bool * binding option * string) parser = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36119
diff
changeset
|
235 |
Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36119
diff
changeset
|
236 |
(Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1 |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36119
diff
changeset
|
237 |
|| Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")" |
33796 | 238 |
>> (fn t => (true,NONE,t)) |
40832 | 239 |
|| Parse.typ >> (fn t => (false,NONE,t)) |
23152 | 240 |
|
241 |
val cons_decl = |
|
40832 | 242 |
Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
243 |
|
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
244 |
val domain_decl = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36119
diff
changeset
|
245 |
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) -- |
40832 | 246 |
(Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl) |
23152 | 247 |
|
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
248 |
val domains_decl = |
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40215
diff
changeset
|
249 |
Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false -- |
40832 | 250 |
Parse.and_list1 domain_decl |
23152 | 251 |
|
33796 | 252 |
fun mk_domain |
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40215
diff
changeset
|
253 |
(unsafe : bool, |
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40215
diff
changeset
|
254 |
doms : ((((string * string option) list * binding) * mixfix) * |
33796 | 255 |
((binding * (bool * binding option * string) list) * mixfix) list) list ) = |
256 |
let |
|
257 |
val specs : ((string * string option) list * binding * mixfix * |
|
258 |
(binding * (bool * binding option * string) list * mixfix) list) list = |
|
259 |
map (fn (((vs, t), mx), cons) => |
|
40832 | 260 |
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
261 |
in |
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40215
diff
changeset
|
262 |
if unsafe |
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40215
diff
changeset
|
263 |
then add_domain_cmd specs |
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40215
diff
changeset
|
264 |
else add_new_domain_cmd specs |
40832 | 265 |
end |
23152 | 266 |
|
24867 | 267 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36119
diff
changeset
|
268 |
Outer_Syntax.command "domain" "define recursive domains (HOLCF)" |
40832 | 269 |
Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain)) |
23152 | 270 |
|
40832 | 271 |
end |