8 |
8 |
9 local |
9 local |
10 |
10 |
11 open ThyParse; |
11 open ThyParse; |
12 |
12 |
13 (*ML identifiers for introduction rules.*) |
13 fun mk_bind suffix s = |
14 fun mk_intr_name suffix s = |
|
15 if ThmDatabase.is_ml_identifier s then |
14 if ThmDatabase.is_ml_identifier s then |
16 "op " ^ s ^ suffix (*the "op" cancels any infix status*) |
15 "op " ^ s ^ suffix (*the "op" cancels any infix status*) |
17 else "_"; (*bad name, don't try to bind*) |
16 else "_"; (*bad name, don't try to bind*) |
18 |
17 |
19 |
18 |
20 (*For lists of theorems. Either a string (an ML list expression) or else |
19 (*For lists of theorems. Either a string (an ML list expression) or else |
21 a list of identifiers.*) |
20 a list of identifiers.*) |
22 fun optlist s = |
21 fun optlist s = |
23 optional (s $$-- |
22 optional (s $$-- |
24 (string >> unenclose |
23 (string >> unenclose |
25 || list1 (name>>unenclose) >> mk_list)) |
24 || list1 (name>>unenclose) >> mk_list)) |
26 "[]"; |
25 "[]"; |
27 |
26 |
28 (*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) |
27 (*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) |
29 fun scan_to_id s = |
28 fun scan_to_id s = |
30 s |> Symbol.explode |
29 s |> Symbol.explode |
31 |> Scan.error (Scan.finite Symbol.stopper |
30 |> Scan.error (Scan.finite Symbol.stopper |
32 (Scan.!! (fn _ => "Expected to find an identifier in " ^ s) |
31 (Scan.!! (fn _ => "Expected to find an identifier in " ^ s) |
33 (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
32 (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
34 |> #1; |
33 |> #1; |
35 |
34 |
36 (*(Co)Inductive definitions theory section."*) |
35 |
|
36 (* (Co)Inductive definitions *) |
|
37 |
37 fun inductive_decl coind = |
38 fun inductive_decl coind = |
38 let |
39 let |
39 fun mk_params ((((((recs, sdom_sum), ipairs), |
40 fun mk_params ((((((recs, sdom_sum), ipairs), |
40 monos), con_defs), type_intrs), type_elims) = |
41 monos), con_defs), type_intrs), type_elims) = |
41 let val big_rec_name = space_implode "_" |
42 let val big_rec_name = space_implode "_" |
42 (map (scan_to_id o unenclose) recs) |
43 (map (scan_to_id o unenclose) recs) |
43 and srec_tms = mk_list recs |
44 and srec_tms = mk_list recs |
44 and sintrs = |
45 and sintrs = |
45 mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs) |
46 mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs) |
46 and inames = mk_list (map (mk_intr_name "" o fst) ipairs) |
47 and inames = mk_list (map (mk_bind "" o fst) ipairs) |
47 in |
48 in |
48 ";\n\n\ |
49 ";\n\n\ |
49 \local\n\ |
50 \local\n\ |
50 \val (thy, {defs, intrs, elim, mk_cases, \ |
51 \val (thy, {defs, intrs, elim, mk_cases, \ |
51 \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\ |
52 \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\ |
52 \ " ^ |
53 \ " ^ |
53 (if coind then "Co" else "") ^ |
54 (if coind then "Co" else "") ^ |
54 "Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^ |
55 "Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^ |
55 sintrs ^ " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ |
56 " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ |
56 type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ |
57 \in\n\ |
57 \in\n\ |
58 \structure " ^ big_rec_name ^ " =\n\ |
58 \structure " ^ big_rec_name ^ " =\n\ |
59 \struct\n\ |
59 \struct\n\ |
60 \ val defs = defs\n\ |
60 \ val defs = defs\n\ |
61 \ val bnd_mono = bnd_mono\n\ |
61 \ val bnd_mono = bnd_mono\n\ |
62 \ val dom_subset = dom_subset\n\ |
62 \ val dom_subset = dom_subset\n\ |
63 \ val intrs = intrs\n\ |
63 \ val intrs = intrs\n\ |
64 \ val elim = elim\n\ |
64 \ val elim = elim\n\ |
65 \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ |
65 \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ |
66 \ val mutual_induct = mutual_induct\n\ |
66 \ val mutual_induct = mutual_induct\n\ |
67 \ val mk_cases = mk_cases\n\ |
67 \ val mk_cases = mk_cases\n\ |
68 \ val " ^ inames ^ " = intrs\n\ |
68 \ val " ^ inames ^ " = intrs\n\ |
69 \end;\n\ |
69 \end;\n\ |
70 \val thy = thy;\nend;\n\ |
70 \val thy = thy;\nend;\n\ |
71 \val thy = thy\n" |
71 \val thy = thy\n" |
|
72 end |
72 end |
73 val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string |
73 val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string |
74 val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
74 val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
75 in domains -- ipairs -- optlist "monos" -- optlist "con_defs" |
75 in domains -- ipairs -- optlist "monos" -- optlist "con_defs" |
76 -- optlist "type_intrs" -- optlist "type_elims" |
76 -- optlist "type_intrs" -- optlist "type_elims" |
77 >> mk_params |
77 >> mk_params |
78 end; |
78 end; |
79 |
79 |
80 |
80 |
81 (*Datatype definitions theory section. co is true for codatatypes*) |
81 (* Datatype definitions *) |
|
82 |
82 fun datatype_decl coind = |
83 fun datatype_decl coind = |
83 let |
84 let |
84 (*generate strings*) |
|
85 fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z); |
85 fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z); |
86 val mk_data = mk_list o map mk_const o snd |
86 val mk_data = mk_list o map mk_const o snd |
87 val mk_scons = mk_big_list o map mk_data |
87 val mk_scons = mk_big_list o map mk_data |
88 fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) = |
88 fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) = |
89 let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs |
89 let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs |
90 val big_rec_name = space_implode "_" rec_names |
90 val big_rec_name = space_implode "_" rec_names |
91 and srec_tms = mk_list (map fst rec_pairs) |
91 and srec_tms = mk_list (map fst rec_pairs) |
92 and scons = mk_scons rec_pairs |
92 and scons = mk_scons rec_pairs |
93 val con_names = flat (map (map (unenclose o #1 o #1) o snd) |
93 val con_names = flat (map (map (unenclose o #1 o #1) o snd) |
94 rec_pairs) |
94 rec_pairs) |
95 val inames = mk_list (map (mk_intr_name "_I") con_names) |
95 val inames = mk_list (map (mk_bind "_I") con_names) |
96 in |
96 in |
97 ";\n\n\ |
97 ";\n\n\ |
98 \local\n\ |
98 \local\n\ |
99 \val (thy,\n\ |
99 \val (thy,\n\ |
100 \ {defs, intrs, elim, mk_cases, \ |
100 \ {defs, intrs, elim, mk_cases, \ |
101 \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\ |
101 \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\ |
102 \ {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\ |
102 \ {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\ |
103 \ " ^ |
103 \ " ^ |
104 (if coind then "Co" else "") ^ |
104 (if coind then "Co" else "") ^ |
105 "Data_Package.add_datatype (" ^ sdom ^ ", " ^ srec_tms ^ ", " ^ |
105 "Data_Package.add_datatype_x (" ^ sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^ |
106 scons ^ ", " ^ monos ^ ", " ^ |
106 " (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ |
107 type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ |
107 \in\n\ |
108 \in\n\ |
108 \structure " ^ big_rec_name ^ " =\n\ |
109 \structure " ^ big_rec_name ^ " =\n\ |
109 \struct\n\ |
110 \struct\n\ |
110 \ val defs = defs\n\ |
111 \ val defs = defs\n\ |
111 \ val bnd_mono = bnd_mono\n\ |
112 \ val bnd_mono = bnd_mono\n\ |
112 \ val dom_subset = dom_subset\n\ |
113 \ val dom_subset = dom_subset\n\ |
113 \ val intrs = intrs\n\ |
114 \ val intrs = intrs\n\ |
114 \ val elim = elim\n\ |
115 \ val elim = elim\n\ |
115 \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ |
116 \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ |
116 \ val mutual_induct = mutual_induct\n\ |
117 \ val mutual_induct = mutual_induct\n\ |
117 \ val mk_cases = mk_cases\n\ |
118 \ val mk_cases = mk_cases\n\ |
118 \ val con_defs = con_defs\n\ |
119 \ val con_defs = con_defs\n\ |
119 \ val case_eqns = case_eqns\n\ |
120 \ val case_eqns = case_eqns\n\ |
120 \ val recursor_eqns = recursor_eqns\n\ |
121 \ val recursor_eqns = recursor_eqns\n\ |
121 \ val free_iffs = free_iffs\n\ |
122 \ val free_iffs = free_iffs\n\ |
122 \ val free_SEs = free_SEs\n\ |
123 \ val free_SEs = free_SEs\n\ |
123 \ val mk_free = mk_free\n\ |
124 \ val mk_free = mk_free\n\ |
124 \ val " ^ inames ^ " = intrs;\n\ |
125 \ val " ^ inames ^ " = intrs;\n\ |
125 \end;\n\ |
126 \end;\n\ |
126 \val thy = thy;\nend;\n\ |
127 \val thy = thy;\nend;\n\ |
127 \val thy = thy\n" |
128 \val thy = thy\n" |
|
129 end |
128 end |
130 val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty; |
129 val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty; |
131 val construct = name -- string_list -- opt_mixfix; |
130 val construct = name -- string_list -- opt_mixfix; |
132 in optional ("<=" $$-- string) "\"\"" -- |
131 in optional ("<=" $$-- string) "\"\"" -- |
133 enum1 "and" (name --$$ "=" -- enum1 "|" construct) -- |
132 enum1 "and" (name --$$ "=" -- enum1 "|" construct) -- |
134 optlist "monos" -- optlist "type_intrs" -- optlist "type_elims" |
133 optlist "monos" -- optlist "type_intrs" -- optlist "type_elims" |
135 >> mk_params |
134 >> mk_params |
136 end; |
135 end; |
137 |
136 |
138 |
137 |
|
138 |
139 (** rep_datatype **) |
139 (** rep_datatype **) |
140 |
140 |
141 fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) = |
141 fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) = |
142 "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n " ^ |
142 "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n " ^ |
143 mk_list case_eqns ^ " " ^ mk_list recursor_eqns; |
143 mk_list case_eqns ^ " " ^ mk_list recursor_eqns; |
144 |
144 |
145 val rep_datatype_decl = |
145 val rep_datatype_decl = |
146 (("elim" $$-- ident) -- |
146 (("elim" $$-- ident) -- |
147 ("induct" $$-- ident) -- |
147 ("induct" $$-- ident) -- |
148 ("case_eqns" $$-- list1 ident) -- |
148 ("case_eqns" $$-- list1 ident) -- |
149 optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string; |
149 optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string; |
|
150 |
150 |
151 |
151 |
152 |
152 (** primrec **) |
153 (** primrec **) |
153 |
154 |
154 fun mk_primrec_decl eqns = |
155 fun mk_primrec_decl eqns = |
155 let val names = map fst eqns |
156 let val binds = map (mk_bind "" o fst) eqns in |
156 in |
157 ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^ |
157 ";\nval (thy, " ^ mk_list names ^ |
158 mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\ |
158 ") = PrimrecPackage.add_primrec " ^ |
|
159 mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\ |
|
160 \val thy = thy\n" |
159 \val thy = thy\n" |
161 end; |
160 end; |
162 |
161 |
163 (* either names and axioms or just axioms *) |
162 (* either names and axioms or just axioms *) |
164 val primrec_decl = |
163 val primrec_decl = |
165 ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl; |
164 ((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl; |
166 |
|
167 |
165 |
168 |
166 |
169 |
167 |
170 (** augment thy syntax **) |
168 (** augment thy syntax **) |
171 |
169 |