author | huffman |
Sat, 13 Mar 2010 15:18:25 -0800 | |
changeset 35774 | 218e9766a848 |
parent 35659 | a78bc1930a7a |
child 35775 | 9b7e2e17be69 |
permissions | -rw-r--r-- |
32126 | 1 |
(* Title: HOLCF/Tools/Domain/domain_extender.ML |
23152 | 2 |
Author: David von Oheimb |
3 |
||
4 |
Theory extender for domain command, including theory syntax. |
|
5 |
*) |
|
6 |
||
7 |
signature DOMAIN_EXTENDER = |
|
8 |
sig |
|
33796 | 9 |
val add_domain_cmd: |
35774 | 10 |
binding -> |
33796 | 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: |
|
35774 | 16 |
binding -> |
33796 | 17 |
((string * string option) list * binding * mixfix * |
18 |
(binding * (bool * binding option * typ) list * mixfix) list) list |
|
19 |
-> theory -> theory |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
20 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
21 |
val add_new_domain_cmd: |
35774 | 22 |
binding -> |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
23 |
((string * string option) list * binding * mixfix * |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
24 |
(binding * (bool * binding option * string) list * mixfix) list) list |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
25 |
-> theory -> theory |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
26 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
27 |
val add_new_domain: |
35774 | 28 |
binding -> |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
29 |
((string * string option) list * binding * mixfix * |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
30 |
(binding * (bool * binding option * typ) list * mixfix) list) list |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
31 |
-> theory -> theory |
23152 | 32 |
end; |
33 |
||
31023 | 34 |
structure Domain_Extender :> DOMAIN_EXTENDER = |
23152 | 35 |
struct |
36 |
||
37 |
open Domain_Library; |
|
38 |
||
39 |
(* ----- general testing and preprocessing of constructor list -------------- *) |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
40 |
fun check_and_sort_domain |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
41 |
(definitional : bool) |
33796 | 42 |
(dtnvs : (string * typ list) list) |
43 |
(cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
44 |
(thy : theory) |
31288 | 45 |
: ((string * typ list) * |
46 |
(binding * (bool * binding option * typ) list * mixfix) list) list = |
|
33796 | 47 |
let |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
48 |
val defaultS = Sign.defaultS thy; |
33796 | 49 |
|
50 |
val test_dupl_typs = |
|
51 |
case duplicates (op =) (map fst dtnvs) of |
|
52 |
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups); |
|
53 |
||
54 |
val all_cons = map (Binding.name_of o first) (flat cons''); |
|
55 |
val test_dupl_cons = |
|
56 |
case duplicates (op =) all_cons of |
|
57 |
[] => false | dups => error ("Duplicate constructors: " |
|
58 |
^ commas_quote dups); |
|
59 |
val all_sels = |
|
60 |
(map Binding.name_of o map_filter second o maps second) (flat cons''); |
|
61 |
val test_dupl_sels = |
|
62 |
case duplicates (op =) all_sels of |
|
63 |
[] => false | dups => error("Duplicate selectors: "^commas_quote dups); |
|
64 |
||
65 |
fun test_dupl_tvars s = |
|
66 |
case duplicates (op =) (map(fst o dest_TFree)s) of |
|
67 |
[] => false | dups => error("Duplicate type arguments: " |
|
68 |
^commas_quote dups); |
|
69 |
val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs); |
|
70 |
||
71 |
(* test for free type variables, illegal sort constraints on rhs, |
|
72 |
non-pcpo-types and invalid use of recursive type; |
|
73 |
replace sorts in type variables on rhs *) |
|
74 |
fun analyse_equation ((dname,typevars),cons') = |
|
75 |
let |
|
76 |
val tvars = map dest_TFree typevars; |
|
77 |
val distinct_typevars = map TFree tvars; |
|
78 |
fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
|
79 |
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
|
80 |
| rm_sorts (TVar(s,_)) = TVar(s,[]) |
|
81 |
and remove_sorts l = map rm_sorts l; |
|
35525 | 82 |
val indirect_ok = |
83 |
[@{type_name "*"}, @{type_name cfun}, @{type_name ssum}, |
|
84 |
@{type_name sprod}, @{type_name u}]; |
|
33796 | 85 |
fun analyse indirect (TFree(v,s)) = |
86 |
(case AList.lookup (op =) tvars v of |
|
87 |
NONE => error ("Free type variable " ^ quote v ^ " on rhs.") |
|
88 |
| SOME sort => if eq_set (op =) (s, defaultS) orelse |
|
89 |
eq_set (op =) (s, sort) |
|
90 |
then TFree(v,sort) |
|
91 |
else error ("Inconsistent sort constraint" ^ |
|
92 |
" for type variable " ^ quote v)) |
|
93 |
| analyse indirect (t as Type(s,typl)) = |
|
94 |
(case AList.lookup (op =) dtnvs s of |
|
95 |
NONE => |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
96 |
if definitional orelse s mem indirect_ok |
33796 | 97 |
then Type(s,map (analyse false) typl) |
98 |
else Type(s,map (analyse true) typl) |
|
99 |
| SOME typevars => |
|
100 |
if indirect |
|
101 |
then error ("Indirect recursion of type " ^ |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
102 |
quote (string_of_typ thy t)) |
33796 | 103 |
else if dname <> s orelse |
104 |
(** BUG OR FEATURE?: |
|
105 |
mutual recursion may use different arguments **) |
|
106 |
remove_sorts typevars = remove_sorts typl |
|
107 |
then Type(s,map (analyse true) typl) |
|
108 |
else error ("Direct recursion of type " ^ |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
109 |
quote (string_of_typ thy t) ^ |
33796 | 110 |
" with different arguments")) |
111 |
| analyse indirect (TVar _) = Imposs "extender:analyse"; |
|
112 |
fun check_pcpo lazy T = |
|
113 |
let val ok = if lazy then cpo_type else pcpo_type |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
114 |
in if ok thy T then T |
33796 | 115 |
else error ("Constructor argument type is not of sort pcpo: " ^ |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
116 |
string_of_typ thy T) |
33796 | 117 |
end; |
118 |
fun analyse_arg (lazy, sel, T) = |
|
119 |
(lazy, sel, check_pcpo lazy (analyse false T)); |
|
120 |
fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); |
|
121 |
in ((dname,distinct_typevars), map analyse_con cons') end; |
|
122 |
in ListPair.map analyse_equation (dtnvs,cons'') |
|
123 |
end; (* let *) |
|
23152 | 124 |
|
125 |
(* ----- calls for building new thy and thms -------------------------------- *) |
|
126 |
||
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
127 |
fun gen_add_domain |
33796 | 128 |
(prep_typ : theory -> 'a -> typ) |
35774 | 129 |
(comp_dbind : binding) |
33796 | 130 |
(eqs''' : ((string * string option) list * binding * mixfix * |
131 |
(binding * (bool * binding option * 'a) list * mixfix) list) list) |
|
35516 | 132 |
(thy : theory) = |
33796 | 133 |
let |
35520 | 134 |
val dtnvs : (binding * typ list * mixfix) list = |
135 |
let |
|
136 |
fun readS (SOME s) = Syntax.read_sort_global thy s |
|
137 |
| readS NONE = Sign.defaultS thy; |
|
138 |
fun readTFree (a, s) = TFree (a, readS s); |
|
139 |
in |
|
140 |
map (fn (vs,dname:binding,mx,_) => |
|
141 |
(dname, map readTFree vs, mx)) eqs''' |
|
142 |
end; |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
143 |
|
35520 | 144 |
(* declare new types *) |
35516 | 145 |
val thy = |
35520 | 146 |
let |
147 |
fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); |
|
148 |
fun thy_arity (dname,tvars,mx) = |
|
149 |
(Sign.full_name thy dname, map (snd o dest_TFree) tvars, pcpoS); |
|
150 |
in |
|
151 |
thy |
|
152 |
|> Sign.add_types (map thy_type dtnvs) |
|
153 |
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs |
|
154 |
end; |
|
155 |
||
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
156 |
val dbinds : binding list = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
157 |
map (fn (_,dbind,_,_) => dbind) eqs'''; |
35520 | 158 |
val cons''' : |
159 |
(binding * (bool * binding option * 'a) list * mixfix) list list = |
|
160 |
map (fn (_,_,_,cons) => cons) eqs'''; |
|
161 |
val cons'' : |
|
162 |
(binding * (bool * binding option * typ) list * mixfix) list list = |
|
163 |
map (map (upd_second (map (upd_third (prep_typ thy))))) cons'''; |
|
164 |
val dtnvs' : (string * typ list) list = |
|
35516 | 165 |
map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs; |
33796 | 166 |
val eqs' : ((string * typ list) * |
167 |
(binding * (bool * binding option * typ) list * mixfix) list) list = |
|
35520 | 168 |
check_and_sort_domain false dtnvs' cons'' thy; |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
169 |
(* val thy = Domain_Syntax.add_syntax eqs' thy; *) |
35520 | 170 |
val dts : typ list = map (Type o fst) eqs'; |
171 |
val new_dts : (string * string list) list = |
|
172 |
map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; |
|
173 |
fun one_con (con,args,mx) : cons = |
|
35129 | 174 |
(Binding.name_of con, (* FIXME preverse binding (!?) *) |
33796 | 175 |
ListPair.map (fn ((lazy,sel,tp),vn) => |
35519 | 176 |
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn)) |
35520 | 177 |
(args, Datatype_Prop.make_tnames (map third args))); |
33796 | 178 |
val eqs : eq list = |
179 |
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; |
|
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
180 |
|
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
181 |
fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
182 |
fun mk_con_typ (bind, args, mx) = |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
183 |
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
184 |
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
185 |
val repTs : typ list = map mk_eq_typ eqs'; |
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
186 |
val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs); |
35659 | 187 |
val ((iso_infos, take_info), thy) = |
35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
188 |
Domain_Axioms.add_axioms dom_eqns thy; |
35529
089e438b925b
simplify add_axioms function; remove obsolete domain_syntax.ML
huffman
parents:
35525
diff
changeset
|
189 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
190 |
val ((rewss, take_rews), theorems_thy) = |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
191 |
thy |
35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
192 |
|> fold_map (fn ((eq, (x,cs)), info) => |
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
193 |
Domain_Theorems.theorems (eq, eqs) (Type x, cs) info) |
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
194 |
(eqs ~~ eqs' ~~ iso_infos) |
35774 | 195 |
||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
196 |
in |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
197 |
theorems_thy |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
198 |
|> PureThy.add_thmss |
35774 | 199 |
[((Binding.qualified true "rews" comp_dbind, |
200 |
flat rewss @ take_rews), [])] |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
201 |
|> snd |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
202 |
end; |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
203 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
204 |
fun gen_add_new_domain |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
205 |
(prep_typ : theory -> 'a -> typ) |
35774 | 206 |
(comp_dbind : binding) |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
207 |
(eqs''' : ((string * string option) list * binding * mixfix * |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
208 |
(binding * (bool * binding option * 'a) list * mixfix) list) list) |
35516 | 209 |
(thy : theory) = |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
210 |
let |
35520 | 211 |
val dtnvs : (binding * typ list * mixfix) list = |
212 |
let |
|
213 |
fun readS (SOME s) = Syntax.read_sort_global thy s |
|
214 |
| readS NONE = Sign.defaultS thy; |
|
215 |
fun readTFree (a, s) = TFree (a, readS s); |
|
216 |
in |
|
217 |
map (fn (vs,dname:binding,mx,_) => |
|
218 |
(dname, map readTFree vs, mx)) eqs''' |
|
219 |
end; |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
220 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
221 |
fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
222 |
fun thy_arity (dname,tvars,mx) = |
35516 | 223 |
(Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep}); |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
224 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
225 |
(* this theory is used just for parsing and error checking *) |
35516 | 226 |
val tmp_thy = thy |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
227 |
|> Theory.copy |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
228 |
|> Sign.add_types (map thy_type dtnvs) |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
229 |
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
230 |
|
35520 | 231 |
val cons''' : |
232 |
(binding * (bool * binding option * 'a) list * mixfix) list list = |
|
233 |
map (fn (_,_,_,cons) => cons) eqs'''; |
|
234 |
val cons'' : |
|
235 |
(binding * (bool * binding option * typ) list * mixfix) list list = |
|
236 |
map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons'''; |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
237 |
val dtnvs' : (string * typ list) list = |
35520 | 238 |
map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
239 |
val eqs' : ((string * typ list) * |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
240 |
(binding * (bool * binding option * typ) list * mixfix) list) list = |
35520 | 241 |
check_and_sort_domain true dtnvs' cons'' tmp_thy; |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
242 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
243 |
fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T; |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
244 |
fun mk_con_typ (bind, args, mx) = |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
245 |
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args); |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
246 |
fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons); |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
247 |
|
35659 | 248 |
val ((iso_infos, take_info), thy) = thy |> |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
249 |
Domain_Isomorphism.domain_isomorphism |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
250 |
(map (fn ((vs, dname, mx, _), eq) => |
34149
a0efb4754cb7
add 'morphisms' option to domain_isomorphism command
huffman
parents:
33971
diff
changeset
|
251 |
(map fst vs, dname, mx, mk_eq_typ eq, NONE)) |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
252 |
(eqs''' ~~ eqs')) |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
253 |
|
35520 | 254 |
val dts : typ list = map (Type o fst) eqs'; |
255 |
val new_dts : (string * string list) list = |
|
256 |
map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; |
|
257 |
fun one_con (con,args,mx) : cons = |
|
35129 | 258 |
(Binding.name_of con, (* FIXME preverse binding (!?) *) |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
259 |
ListPair.map (fn ((lazy,sel,tp),vn) => |
35519 | 260 |
mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn)) |
35443
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
35288
diff
changeset
|
261 |
(args, Datatype_Prop.make_tnames (map third args)) |
35520 | 262 |
); |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
263 |
val eqs : eq list = |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
264 |
map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; |
33796 | 265 |
val ((rewss, take_rews), theorems_thy) = |
266 |
thy |
|
35558
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
267 |
|> fold_map (fn ((eq, (x,cs)), info) => |
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
268 |
Domain_Theorems.theorems (eq, eqs) (Type x, cs) info) |
bb088a6fafbc
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
huffman
parents:
35529
diff
changeset
|
269 |
(eqs ~~ eqs' ~~ iso_infos) |
35774 | 270 |
||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info; |
33796 | 271 |
in |
272 |
theorems_thy |
|
273 |
|> PureThy.add_thmss |
|
35774 | 274 |
[((Binding.qualified true "rews" comp_dbind, |
275 |
flat rewss @ take_rews), [])] |
|
33796 | 276 |
|> snd |
277 |
end; |
|
23152 | 278 |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
279 |
val add_domain = gen_add_domain Sign.certify_typ; |
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
280 |
val add_domain_cmd = gen_add_domain Syntax.read_typ_global; |
23152 | 281 |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
282 |
val add_new_domain = gen_add_new_domain Sign.certify_typ; |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
283 |
val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global; |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
284 |
|
23152 | 285 |
|
286 |
(** outer syntax **) |
|
287 |
||
288 |
local structure P = OuterParse and K = OuterKeyword in |
|
289 |
||
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
24926
diff
changeset
|
290 |
val _ = OuterKeyword.keyword "lazy"; |
24867 | 291 |
|
30919
dcf8a7a66bd1
make domain package ML interface more consistent with datatype package; use binding instead of bstring
huffman
parents:
30916
diff
changeset
|
292 |
val dest_decl : (bool * binding option * string) parser = |
33796 | 293 |
P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- |
294 |
(P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 |
|
295 |
|| P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" |
|
296 |
>> (fn t => (true,NONE,t)) |
|
297 |
|| P.typ >> (fn t => (false,NONE,t)); |
|
23152 | 298 |
|
299 |
val cons_decl = |
|
33796 | 300 |
P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
301 |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
302 |
val type_var' : (string * string option) parser = |
33796 | 303 |
(P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); |
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
304 |
|
31161
a27d4254ff4c
fix domain package parsing of lhs sort constraints
huffman
parents:
31023
diff
changeset
|
305 |
val type_args' : (string * string option) list parser = |
33796 | 306 |
type_var' >> single |
307 |
|| P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") |
|
308 |
|| Scan.succeed []; |
|
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
309 |
|
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
310 |
val domain_decl = |
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
35288
diff
changeset
|
311 |
(type_args' -- P.binding -- P.opt_mixfix) -- |
33796 | 312 |
(P.$$$ "=" |-- P.enum1 "|" cons_decl); |
23152 | 313 |
|
30916
a3d2128cac92
allow infix declarations for type constructors defined with domain package
huffman
parents:
30915
diff
changeset
|
314 |
val domains_decl = |
35774 | 315 |
Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") -- |
33796 | 316 |
P.and_list1 domain_decl; |
23152 | 317 |
|
33796 | 318 |
fun mk_domain |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
319 |
(definitional : bool) |
35774 | 320 |
(opt_name : binding option, |
33796 | 321 |
doms : ((((string * string option) list * binding) * mixfix) * |
322 |
((binding * (bool * binding option * string) list) * mixfix) list) list ) = |
|
323 |
let |
|
324 |
val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; |
|
325 |
val specs : ((string * string option) list * binding * mixfix * |
|
326 |
(binding * (bool * binding option * string) list * mixfix) list) list = |
|
327 |
map (fn (((vs, t), mx), cons) => |
|
328 |
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; |
|
35774 | 329 |
val comp_dbind = |
330 |
case opt_name of NONE => Binding.name (space_implode "_" names) |
|
331 |
| SOME s => s; |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
332 |
in |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
333 |
if definitional |
35774 | 334 |
then add_new_domain_cmd comp_dbind specs |
335 |
else add_domain_cmd comp_dbind specs |
|
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
336 |
end; |
23152 | 337 |
|
24867 | 338 |
val _ = |
33796 | 339 |
OuterSyntax.command "domain" "define recursive domains (HOLCF)" |
33798
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
340 |
K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false)); |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
341 |
|
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
342 |
val _ = |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
343 |
OuterSyntax.command "new_domain" "define recursive domains (HOLCF)" |
46cbbcbd4e68
clean up indentation; add 'definitional' option flag
huffman
parents:
33796
diff
changeset
|
344 |
K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true)); |
23152 | 345 |
|
24867 | 346 |
end; |
23152 | 347 |
|
348 |
end; |