author | nipkow |
Sun, 05 Jan 2003 21:03:14 +0100 | |
changeset 13771 | 6cd59cc885a1 |
parent 12183 | c10cea75dd56 |
child 14598 | 7009f59711e3 |
permissions | -rw-r--r-- |
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
1 |
(* Title: ZF/thy_syntax.ML |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
2 |
ID: $Id$ |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
5 |
|
12050 | 6 |
Additional sections for *old-style* theory files in ZF. |
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
7 |
*) |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
8 |
|
3622 | 9 |
local |
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
10 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
11 |
open ThyParse; |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
12 |
|
12183 | 13 |
fun mk_bind suffix s = |
6093 | 14 |
if ThmDatabase.is_ml_identifier s then |
12183 | 15 |
"op " ^ s ^ suffix (*the "op" cancels any infix status*) |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
16 |
else "_"; (*bad name, don't try to bind*) |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
17 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
18 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
19 |
(*For lists of theorems. Either a string (an ML list expression) or else |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
20 |
a list of identifiers.*) |
12183 | 21 |
fun optlist s = |
22 |
optional (s $$-- |
|
23 |
(string >> unenclose |
|
24 |
|| list1 (name>>unenclose) >> mk_list)) |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
25 |
"[]"; |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
26 |
|
8813
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
27 |
(*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
28 |
fun scan_to_id s = |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
29 |
s |> Symbol.explode |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
30 |
|> Scan.error (Scan.finite Symbol.stopper |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
31 |
(Scan.!! (fn _ => "Expected to find an identifier in " ^ s) |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
32 |
(Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8127
diff
changeset
|
33 |
|> #1; |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
34 |
|
12183 | 35 |
|
36 |
(* (Co)Inductive definitions *) |
|
37 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
38 |
fun inductive_decl coind = |
12183 | 39 |
let |
40 |
fun mk_params ((((((recs, sdom_sum), ipairs), |
|
1461 | 41 |
monos), con_defs), type_intrs), type_elims) = |
12183 | 42 |
let val big_rec_name = space_implode "_" |
6642 | 43 |
(map (scan_to_id o unenclose) recs) |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
44 |
and srec_tms = mk_list recs |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
12050
diff
changeset
|
45 |
and sintrs = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
12050
diff
changeset
|
46 |
mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs) |
12183 | 47 |
and inames = mk_list (map (mk_bind "" o fst) ipairs) |
1428 | 48 |
in |
12183 | 49 |
";\n\n\ |
50 |
\local\n\ |
|
51 |
\val (thy, {defs, intrs, elim, mk_cases, \ |
|
52 |
\bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\ |
|
53 |
\ " ^ |
|
54 |
(if coind then "Co" else "") ^ |
|
55 |
"Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^ |
|
56 |
" (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ |
|
57 |
\in\n\ |
|
58 |
\structure " ^ big_rec_name ^ " =\n\ |
|
59 |
\struct\n\ |
|
60 |
\ val defs = defs\n\ |
|
61 |
\ val bnd_mono = bnd_mono\n\ |
|
62 |
\ val dom_subset = dom_subset\n\ |
|
63 |
\ val intrs = intrs\n\ |
|
64 |
\ val elim = elim\n\ |
|
65 |
\ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ |
|
66 |
\ val mutual_induct = mutual_induct\n\ |
|
67 |
\ val mk_cases = mk_cases\n\ |
|
68 |
\ val " ^ inames ^ " = intrs\n\ |
|
69 |
\end;\n\ |
|
70 |
\val thy = thy;\nend;\n\ |
|
71 |
\val thy = thy\n" |
|
1428 | 72 |
end |
73 |
val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string |
|
74 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
75 |
in domains -- ipairs -- optlist "monos" -- optlist "con_defs" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
76 |
-- optlist "type_intrs" -- optlist "type_elims" |
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
77 |
>> mk_params |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
78 |
end; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
79 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
80 |
|
12183 | 81 |
(* Datatype definitions *) |
82 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
83 |
fun datatype_decl coind = |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
84 |
let |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
85 |
fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z); |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
86 |
val mk_data = mk_list o map mk_const o snd |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
87 |
val mk_scons = mk_big_list o map mk_data |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
88 |
fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) = |
6642 | 89 |
let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs |
12183 | 90 |
val big_rec_name = space_implode "_" rec_names |
91 |
and srec_tms = mk_list (map fst rec_pairs) |
|
92 |
and scons = mk_scons rec_pairs |
|
93 |
val con_names = flat (map (map (unenclose o #1 o #1) o snd) |
|
94 |
rec_pairs) |
|
95 |
val inames = mk_list (map (mk_bind "_I") con_names) |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
96 |
in |
12183 | 97 |
";\n\n\ |
98 |
\local\n\ |
|
99 |
\val (thy,\n\ |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
100 |
\ {defs, intrs, elim, mk_cases, \ |
12183 | 101 |
\bnd_mono, dom_subset, induct, mutual_induct, ...},\n\ |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
102 |
\ {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\ |
12183 | 103 |
\ " ^ |
104 |
(if coind then "Co" else "") ^ |
|
105 |
"Data_Package.add_datatype_x (" ^ sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^ |
|
106 |
" (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ |
|
107 |
\in\n\ |
|
108 |
\structure " ^ big_rec_name ^ " =\n\ |
|
109 |
\struct\n\ |
|
110 |
\ val defs = defs\n\ |
|
111 |
\ val bnd_mono = bnd_mono\n\ |
|
112 |
\ val dom_subset = dom_subset\n\ |
|
113 |
\ val intrs = intrs\n\ |
|
114 |
\ val elim = elim\n\ |
|
115 |
\ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ |
|
116 |
\ val mutual_induct = mutual_induct\n\ |
|
117 |
\ val mk_cases = mk_cases\n\ |
|
118 |
\ val con_defs = con_defs\n\ |
|
119 |
\ val case_eqns = case_eqns\n\ |
|
120 |
\ val recursor_eqns = recursor_eqns\n\ |
|
121 |
\ val free_iffs = free_iffs\n\ |
|
122 |
\ val free_SEs = free_SEs\n\ |
|
123 |
\ val mk_free = mk_free\n\ |
|
124 |
\ val " ^ inames ^ " = intrs;\n\ |
|
125 |
\end;\n\ |
|
126 |
\val thy = thy;\nend;\n\ |
|
127 |
\val thy = thy\n" |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
128 |
end |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
129 |
val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty; |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
130 |
val construct = name -- string_list -- opt_mixfix; |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
131 |
in optional ("<=" $$-- string) "\"\"" -- |
8127
68c6159440f1
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents:
6642
diff
changeset
|
132 |
enum1 "and" (name --$$ "=" -- enum1 "|" construct) -- |
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
133 |
optlist "monos" -- optlist "type_intrs" -- optlist "type_elims" |
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
134 |
>> mk_params |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
135 |
end; |
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
136 |
|
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
137 |
|
12183 | 138 |
|
6070 | 139 |
(** rep_datatype **) |
140 |
||
141 |
fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) = |
|
142 |
"|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n " ^ |
|
143 |
mk_list case_eqns ^ " " ^ mk_list recursor_eqns; |
|
144 |
||
145 |
val rep_datatype_decl = |
|
12183 | 146 |
(("elim" $$-- ident) -- |
6070 | 147 |
("induct" $$-- ident) -- |
12183 | 148 |
("case_eqns" $$-- list1 ident) -- |
6112 | 149 |
optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string; |
6070 | 150 |
|
151 |
||
12183 | 152 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
153 |
(** primrec **) |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
154 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
155 |
fun mk_primrec_decl eqns = |
12183 | 156 |
let val binds = map (mk_bind "" o fst) eqns in |
157 |
";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^ |
|
158 |
mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\ |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
159 |
\val thy = thy\n" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
160 |
end; |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
161 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
162 |
(* either names and axioms or just axioms *) |
12183 | 163 |
val primrec_decl = |
164 |
((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl; |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
165 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3925
diff
changeset
|
166 |
|
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
167 |
|
3622 | 168 |
(** augment thy syntax **) |
169 |
||
170 |
in |
|
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
171 |
|
3622 | 172 |
val _ = ThySyn.add_syntax |
173 |
["inductive", "coinductive", "datatype", "codatatype", "and", "|", |
|
6070 | 174 |
"<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims", |
175 |
(*rep_datatype*) |
|
176 |
"elim", "induct", "case_eqns", "recursor_eqns"] |
|
177 |
[section "inductive" "" (inductive_decl false), |
|
178 |
section "coinductive" "" (inductive_decl true), |
|
179 |
section "datatype" "" (datatype_decl false), |
|
180 |
section "codatatype" "" (datatype_decl true), |
|
181 |
section "rep_datatype" "" rep_datatype_decl, |
|
182 |
section "primrec" "" primrec_decl]; |
|
3622 | 183 |
|
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset
|
184 |
end; |