author  wenzelm 
Tue, 29 Sep 2009 22:48:24 +0200  
changeset 32765  3032c0308019 
parent 30364  577edc39b501 
child 32952  aeb1e44fbc19 
permissions  rwrr 
6065  1 
(* Title: ZF/Tools/datatype_package.ML 
6052  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 1994 University of Cambridge 

4 

6065  5 
Datatype/Codatatype Definitions 
6052  6 

7 
The functor will be instantiated for normal sums/products (datatype defs) 

8 
and nonstandard sums/products (codatatype defs) 

9 

10 
Sums are used only for mutual recursion; 

11 
Products are used only to derive "streamlined" induction rules for relations 

12 
*) 

13 

14 
type datatype_result = 

15 
{con_defs : thm list, (*definitions made in thy*) 

16 
case_eqns : thm list, (*equations for case operator*) 

17 
recursor_eqns : thm list, (*equations for the recursor*) 

18 
free_iffs : thm list, (*freeness rewrite rules*) 

19 
free_SEs : thm list, (*freeness destruct rules*) 

6112  20 
mk_free : string > thm}; (*function to make freeness theorems*) 
6052  21 

22 
signature DATATYPE_ARG = 

12183  23 
sig 
6052  24 
val intrs : thm list 
25 
val elims : thm list 

12183  26 
end; 
6052  27 

28 
signature DATATYPE_PACKAGE = 

12131  29 
sig 
6052  30 
(*Insert definitions for the recursive sets, which 
31 
must *already* be declared as constants in parent theory!*) 

12183  32 
val add_datatype_i: term * term list > Ind_Syntax.constructor_spec list list > 
33 
thm list * thm list * thm list > theory > theory * inductive_result * datatype_result 

34 
val add_datatype: string * string list > (string * string list * mixfix) list list > 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26190
diff
changeset

35 
(Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list * 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26190
diff
changeset

36 
(Facts.ref * Attrib.src list) list > theory > theory * inductive_result * datatype_result 
12131  37 
end; 
6052  38 

12131  39 
functor Add_datatype_def_Fun 
12183  40 
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU 
41 
and Ind_Package : INDUCTIVE_PACKAGE 

42 
and Datatype_Arg : DATATYPE_ARG 

43 
val coind : bool): DATATYPE_PACKAGE = 

6052  44 
struct 
45 

12183  46 
(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *) 
6052  47 

26189  48 
(*univ or quniv constitutes the sum domain for mutual recursion; 
49 
it is applied to the datatype parameters and to Consts occurring in the 

50 
definition other than Nat.nat and the datatype sets themselves. 

51 
FIXME: could insert all constant set expressions, e.g. nat>nat.*) 

52 
fun data_domain co (rec_tms, con_ty_lists) = 

53 
let val rec_hds = map head_of rec_tms 

54 
val dummy = assert_all is_Const rec_hds 

55 
(fn t => "Datatype set not previously declared as constant: " ^ 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26336
diff
changeset

56 
Syntax.string_of_term_global @{theory IFOL} t); 
26189  57 
val rec_names = (*nat doesn't have to be added*) 
58 
@{const_name nat} :: map (#1 o dest_Const) rec_hds 

59 
val u = if co then @{const QUniv.quniv} else @{const Univ.univ} 

60 
val cs = (fold o fold) (fn (_, _, _, prems) => prems > (fold o fold_aterms) 

61 
(fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t 

62 
 _ => I)) con_ty_lists []; 

63 
in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; 

64 

12183  65 
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy = 
6052  66 
let 
67 
val dummy = (*has essential ancestors?*) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
25985
diff
changeset

68 
Theory.requires thy "Datatype_ZF" "(co)datatype definitions"; 
6052  69 

13150
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset

70 
val rec_hds = map head_of rec_tms; 
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset

71 

0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset

72 
val dummy = assert_all is_Const rec_hds 
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset

73 
(fn t => "Datatype set not previously declared as constant: " ^ 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26336
diff
changeset

74 
Syntax.string_of_term_global thy t); 
13150
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset

75 

0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset

76 
val rec_names = map (#1 o dest_Const) rec_hds 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

77 
val rec_base_names = map Long_Name.base_name rec_names 
6052  78 
val big_rec_base_name = space_implode "_" rec_base_names 
79 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset

80 
val thy_path = thy > Sign.add_path big_rec_base_name 
6052  81 

22578  82 
val big_rec_name = Sign.intern_const thy_path big_rec_base_name; 
6052  83 

22578  84 
val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists); 
6052  85 

12131  86 
val dummy = 
12243  87 
writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name); 
6052  88 

89 
val case_varname = "f"; (*name for case variables*) 

90 

91 
(** Define the constructors **) 

92 

93 
(*The empty tuple is 0*) 

26190  94 
fun mk_tuple [] = @{const "0"} 
7696  95 
 mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; 
6052  96 

32765  97 
fun mk_inject n k u = Balanced_Tree.access 
23419  98 
{left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; 
6052  99 

100 
val npart = length rec_names; (*number of mutually recursive parts*) 

101 

102 

28965  103 
val full_name = Sign.full_bname thy_path; 
6052  104 

12131  105 
(*Make constructor definition; 
6052  106 
kpart is the number of this mutually recursive part*) 
12131  107 
fun mk_con_defs (kpart, con_ty_list) = 
6052  108 
let val ncon = length con_ty_list (*number of constructors*) 
12131  109 
fun mk_def (((id,T,syn), name, args, prems), kcon) = 
110 
(*kcon is index of constructor*) 

24255  111 
PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args), 
12131  112 
mk_inject npart kpart 
113 
(mk_inject ncon kcon (mk_tuple args))) 

6052  114 
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; 
115 

116 

117 
(*** Define the case operator ***) 

118 

119 
(*Combine split terms using case; yields the case operator for one part*) 

12131  120 
fun call_case case_list = 
26190  121 
let fun call_f (free,[]) = Abs("null", @{typ i}, free) 
12131  122 
 call_f (free,args) = 
123 
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) 

26190  124 
@{typ i} 
12131  125 
free 
32765  126 
in Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; 
6052  127 

128 
(** Generating function variables for the case definition 

129 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 

130 

131 
(*The function variable for a single constructor*) 

132 
fun add_case (((_, T, _), name, args, _), (opno, cases)) = 

133 
if Syntax.is_identifier name then 

134 
(opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) 

135 
else 

12131  136 
(opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) 
6052  137 
:: cases); 
138 

139 
(*Treatment of a list of constructors, for one part 

140 
Result adds a list of terms, each a function variable with arguments*) 

141 
fun add_case_list (con_ty_list, (opno, case_lists)) = 

30190  142 
let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list 
6052  143 
in (opno', case_list :: case_lists) end; 
144 

145 
(*Treatment of all parts*) 

30190  146 
val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists; 
6052  147 

148 
(*extract the types of all the variables*) 

26190  149 
val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) > @{typ "i => i"}; 
6052  150 

151 
val case_base_name = big_rec_base_name ^ "_case"; 

152 
val case_name = full_name case_base_name; 

153 

154 
(*The list of all the function variables*) 

15570  155 
val case_args = List.concat (map (map #1) case_lists); 
6052  156 

12131  157 
val case_const = Const (case_name, case_typ); 
6052  158 
val case_tm = list_comb (case_const, case_args); 
159 

24255  160 
val case_def = PrimitiveDefs.mk_defpair 
32765  161 
(case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists)); 
6052  162 

163 

164 
(** Generating function variables for the recursor definition 

165 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 

166 

167 
(*a recursive call for x is the application rec`x *) 

26190  168 
val rec_call = @{const apply} $ Free ("rec", @{typ i}); 
6052  169 

12131  170 
(*look back down the "case args" (which have been reversed) to 
6052  171 
determine the de Bruijn index*) 
172 
fun make_rec_call ([], _) arg = error 

12131  173 
"Internal error in datatype (variable name mismatch)" 
174 
 make_rec_call (a::args, i) arg = 

175 
if a = arg then rec_call $ Bound i 

176 
else make_rec_call (args, i+1) arg; 

6052  177 

178 
(*creates one case of the "X_case" definition of the recursor*) 

12131  179 
fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) = 
6052  180 
let fun add_abs (Free(a,T), u) = Abs(a,T,u) 
12131  181 
val ncase_args = length case_args 
182 
val bound_args = map Bound ((ncase_args  1) downto 0) 

183 
val rec_args = map (make_rec_call (rev case_args,0)) 

184 
(List.drop(recursor_args, ncase_args)) 

6052  185 
in 
30190  186 
List.foldr add_abs 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

187 
(list_comb (recursor_var, 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

188 
bound_args @ rec_args)) case_args 
6052  189 
end 
190 

191 
(*Find each recursive argument and add a recursive call for it*) 

192 
fun rec_args [] = [] 

24826  193 
 rec_args ((Const(@{const_name mem},_)$arg$X)::prems) = 
6052  194 
(case head_of X of 
12131  195 
Const(a,_) => (*recursive occurrence?*) 
196 
if a mem_string rec_names 

197 
then arg :: rec_args prems 

198 
else rec_args prems 

199 
 _ => rec_args prems) 

200 
 rec_args (_::prems) = rec_args prems; 

6052  201 

202 
(*Add an argument position for each occurrence of a recursive set. 

203 
Strictly speaking, the recursive arguments are the LAST of the function 

204 
variable, but they all have type "i" anyway*) 

26190  205 
fun add_rec_args args' T = (map (fn _ => @{typ i}) args') > T 
6052  206 

207 
(*Plug in the function variable type needed for the recursor 

208 
as well as the new arguments (recursive calls)*) 

209 
fun rec_ty_elem ((id, T, syn), name, args, prems) = 

12131  210 
let val args' = rec_args prems 
211 
in ((id, add_rec_args args' T, syn), 

212 
name, args @ args', prems) 

6052  213 
end; 
214 

12131  215 
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); 
6052  216 

217 
(*Treatment of all parts*) 

30190  218 
val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists; 
6052  219 

220 
(*extract the types of all the variables*) 

26190  221 
val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) > @{typ "i => i"}; 
6052  222 

223 
val recursor_base_name = big_rec_base_name ^ "_rec"; 

224 
val recursor_name = full_name recursor_base_name; 

225 

226 
(*The list of all the function variables*) 

15570  227 
val recursor_args = List.concat (map (map #1) recursor_lists); 
6052  228 

229 
val recursor_tm = 

12131  230 
list_comb (Const (recursor_name, recursor_typ), recursor_args); 
6052  231 

12131  232 
val recursor_cases = map call_recursor 
15570  233 
(List.concat case_lists ~~ List.concat recursor_lists) 
6052  234 

12131  235 
val recursor_def = 
24255  236 
PrimitiveDefs.mk_defpair 
12131  237 
(recursor_tm, 
26189  238 
@{const Univ.Vrecursor} $ 
26190  239 
absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases))); 
6052  240 

241 
(* Build the new theory *) 

242 

12183  243 
val need_recursor = (not coind andalso recursor_typ <> case_typ); 
6052  244 

12131  245 
fun add_recursor thy = 
6052  246 
if need_recursor then 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset

247 
thy > Sign.add_consts_i 
30345  248 
[(Binding.name recursor_base_name, recursor_typ, NoSyn)] 
29579  249 
> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) 
6052  250 
else thy; 
251 

18358  252 
val (con_defs, thy0) = thy_path 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset

253 
> Sign.add_consts_i 
30345  254 
(map (fn (c, T, mx) => (Binding.name c, T, mx)) 
255 
((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists))) 

27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27261
diff
changeset

256 
> PureThy.add_defs false 
29579  257 
(map (Thm.no_attributes o apfst Binding.name) 
12131  258 
(case_def :: 
15570  259 
List.concat (ListPair.map mk_con_defs 
12131  260 
(1 upto npart, con_ty_lists)))) 
18358  261 
> add_recursor 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset

262 
> Sign.parent_path 
6052  263 

28965  264 
val intr_names = map (Binding.name o #2) (List.concat con_ty_lists); 
12131  265 
val (thy1, ind_result) = 
12187  266 
thy0 > Ind_Package.add_inductive_i 
267 
false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms)) 

268 
(monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims); 

6052  269 

270 
(**** Now prove the datatype theorems in this theory ****) 

271 

272 

273 
(*** Prove the case theorems ***) 

274 

12131  275 
(*Each equation has the form 
6052  276 
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) 
12131  277 
fun mk_case_eqn (((_,T,_), name, args, _), case_free) = 
6052  278 
FOLogic.mk_Trueprop 
279 
(FOLogic.mk_eq 

280 
(case_tm $ 

22578  281 
(list_comb (Const (Sign.intern_const thy1 name,T), 
12131  282 
args)), 
283 
list_comb (case_free, args))); 

6052  284 

26189  285 
val case_trans = hd con_defs RS @{thm def_trans} 
286 
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS @{thm trans}; 

6052  287 

17985  288 
fun prove_case_eqn (arg, con_def) = 
20046  289 
Goal.prove_global thy1 [] [] 
17985  290 
(Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg)) 
291 
(*Proves a single case equation. Could use simp_tac, but it's slower!*) 

292 
(fn _ => EVERY 

28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not wellformed tactics due to change of main conclusion;
wenzelm
parents:
28678
diff
changeset

293 
[rewrite_goals_tac [con_def], 
17985  294 
rtac case_trans 1, 
20046  295 
REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]); 
6052  296 

26189  297 
val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]); 
6052  298 

12131  299 
val case_eqns = 
300 
map prove_case_eqn 

15570  301 
(List.concat con_ty_lists ~~ case_args ~~ tl con_defs); 
6052  302 

303 
(*** Prove the recursor theorems ***) 

304 

30345  305 
val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of 
15531  306 
NONE => (writeln " [ No recursion operator ]"; 
12131  307 
[]) 
15531  308 
 SOME recursor_def => 
6052  309 
let 
12131  310 
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *) 
24826  311 
fun subst_rec (Const(@{const_name apply},_) $ Free _ $ arg) = recursor_tm $ arg 
12131  312 
 subst_rec tm = 
313 
let val (head, args) = strip_comb tm 

314 
in list_comb (head, map subst_rec args) end; 

6052  315 

12131  316 
(*Each equation has the form 
317 
REC(coni(args)) = f_coni(args, REC(rec_arg), ...) 

318 
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive 

319 
constructor argument.*) 

320 
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) = 

321 
FOLogic.mk_Trueprop 

322 
(FOLogic.mk_eq 

323 
(recursor_tm $ 

22578  324 
(list_comb (Const (Sign.intern_const thy1 name,T), 
12131  325 
args)), 
18185  326 
subst_rec (Term.betapplys (recursor_case, args)))); 
6052  327 

24893  328 
val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS trans; 
6052  329 

12131  330 
fun prove_recursor_eqn arg = 
20046  331 
Goal.prove_global thy1 [] [] 
17985  332 
(Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg)) 
333 
(*Proves a single recursor equation.*) 

334 
(fn _ => EVERY 

335 
[rtac recursor_trans 1, 

336 
simp_tac (rank_ss addsimps case_eqns) 1, 

20046  337 
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]); 
6052  338 
in 
15570  339 
map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases) 
6052  340 
end 
341 

342 
val constructors = 

343 
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs); 

344 

12187  345 
val free_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs); 
6052  346 

6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset

347 
val {intrs, elim, induct, mutual_induct, ...} = ind_result 
6052  348 

349 
(*Typical theorems have the form ~con1=con2, con1=con2==>False, 

350 
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <> x=y, etc. *) 

351 
fun mk_free s = 

17985  352 
let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*) 
24707  353 
Goal.prove_global thy [] [] (Syntax.read_prop_global thy s) 
17985  354 
(fn _ => EVERY 
355 
[rewrite_goals_tac con_defs, 

20046  356 
fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]) 
17985  357 
end; 
6052  358 

359 
val simps = case_eqns @ recursor_eqns; 

360 

361 
val dt_info = 

12131  362 
{inductive = true, 
363 
constructors = constructors, 

364 
rec_rewrites = recursor_eqns, 

365 
case_rewrites = case_eqns, 

366 
induct = induct, 

367 
mutual_induct = mutual_induct, 

368 
exhaustion = elim}; 

6052  369 

370 
val con_info = 

371 
{big_rec_name = big_rec_name, 

12131  372 
constructors = constructors, 
6052  373 
(*let primrec handle definition by cases*) 
12131  374 
free_iffs = free_iffs, 
375 
rec_rewrites = (case recursor_eqns of 

376 
[] => case_eqns  _ => recursor_eqns)}; 

6052  377 

378 
(*associate with each constructor the datatype name and rewrites*) 

379 
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors 

380 

381 
in 

382 
(*Updating theory components: simprules and datatype info*) 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset

383 
(thy1 > Sign.add_path big_rec_base_name 
18377  384 
> PureThy.add_thmss 
29579  385 
[((Binding.name "simps", simps), [Simplifier.simp_add]), 
386 
((Binding.empty , intrs), [Classical.safe_intro NONE]), 

387 
((Binding.name "con_defs", con_defs), []), 

388 
((Binding.name "case_eqns", case_eqns), []), 

389 
((Binding.name "recursor_eqns", recursor_eqns), []), 

390 
((Binding.name "free_iffs", free_iffs), []), 

391 
((Binding.name "free_elims", free_SEs), [])] > snd 

17412  392 
> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) 
393 
> ConstructorsData.map (fold Symtab.update con_pairs) 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset

394 
> Sign.parent_path, 
6052  395 
ind_result, 
396 
{con_defs = con_defs, 

397 
case_eqns = case_eqns, 

398 
recursor_eqns = recursor_eqns, 

399 
free_iffs = free_iffs, 

400 
free_SEs = free_SEs, 

401 
mk_free = mk_free}) 

402 
end; 

403 

17936  404 
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy = 
12183  405 
let 
24725  406 
val ctxt = ProofContext.init thy; 
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

407 
fun read_is strs = 
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

408 
map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs 
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

409 
> Syntax.check_terms ctxt; 
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

410 

5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

411 
val rec_tms = read_is srec_tms; 
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

412 
val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists; 
12183  413 
val dom_sum = 
26189  414 
if sdom = "" then data_domain coind (rec_tms, con_ty_lists) 
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset

415 
else singleton read_is sdom; 
24725  416 
val monos = Attrib.eval_thms ctxt raw_monos; 
417 
val type_intrs = Attrib.eval_thms ctxt raw_type_intrs; 

418 
val type_elims = Attrib.eval_thms ctxt raw_type_elims; 

419 
in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end; 

420 

12183  421 

422 
(* outer syntax *) 

423 

17057  424 
local structure P = OuterParse and K = OuterKeyword in 
12183  425 

426 
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) = 

427 
#1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims); 

428 

429 
val con_decl = 

430 
P.name  Scan.optional (P.$$$ "("  P.list1 P.term  P.$$$ ")") []  P.opt_mixfix 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12243
diff
changeset

431 
>> P.triple1; 
12183  432 

433 
val datatype_decl = 

25985  434 
(Scan.optional ((P.$$$ "\<subseteq>"  P.$$$ "<=")  P.!!! P.term) "")  
12183  435 
P.and_list1 (P.term  (P.$$$ "="  P.enum1 "" con_decl))  
22101  436 
Scan.optional (P.$$$ "monos"  P.!!! SpecParse.xthms1) []  
437 
Scan.optional (P.$$$ "type_intros"  P.!!! SpecParse.xthms1) []  

438 
Scan.optional (P.$$$ "type_elims"  P.!!! SpecParse.xthms1) [] 

12183  439 
>> (Toplevel.theory o mk_datatype); 
440 

441 
val coind_prefix = if coind then "co" else ""; 

442 

24867  443 
val _ = OuterSyntax.command (coind_prefix ^ "datatype") 
12183  444 
("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl; 
445 

6052  446 
end; 
12183  447 

448 
end; 

15705  449 