151 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = |
151 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = |
152 FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) |
152 FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) |
153 #> store_termination_rule termination |
153 #> store_termination_rule termination |
154 |
154 |
155 |
155 |
156 |
|
157 (* Configuration management *) |
156 (* Configuration management *) |
158 datatype fundef_opt |
157 datatype fundef_opt |
159 = Sequential |
158 = Sequential |
160 | Default of string |
159 | Default of string |
161 | Preprocessor of string |
|
162 | Target of xstring |
160 | Target of xstring |
163 | DomIntros |
161 | DomIntros |
164 | Tailrec |
162 | Tailrec |
165 |
163 |
166 datatype fundef_config |
164 datatype fundef_config |
167 = FundefConfig of |
165 = FundefConfig of |
168 { |
166 { |
169 sequential: bool, |
167 sequential: bool, |
170 default: string, |
168 default: string, |
171 preprocessor: string option, |
|
172 target: xstring option, |
169 target: xstring option, |
173 domintros: bool, |
170 domintros: bool, |
174 tailrec: bool |
171 tailrec: bool |
175 } |
172 } |
176 |
173 |
177 |
174 fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) = |
178 val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, |
175 FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec} |
179 target=NONE, domintros=false, tailrec=false } |
176 | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) = |
180 |
177 FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec} |
181 val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, |
178 | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) = |
182 target=NONE, domintros=false, tailrec=false } |
179 FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec} |
183 |
180 | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) = |
184 fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = |
181 FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec} |
185 FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } |
182 | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) = |
186 | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = |
183 FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true} |
187 FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } |
|
188 | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = |
|
189 FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec } |
|
190 | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = |
|
191 FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec } |
|
192 | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = |
|
193 FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec } |
|
194 | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = |
|
195 FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } |
|
196 |
184 |
197 fun target_of (FundefConfig {target, ...}) = target |
185 fun target_of (FundefConfig {target, ...}) = target |
198 |
|
199 local |
|
200 structure P = OuterParse and K = OuterKeyword |
|
201 |
|
202 val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false |
|
203 |
|
204 val option_parser = (P.$$$ "sequential" >> K Sequential) |
|
205 || ((P.reserved "default" |-- P.term) >> Default) |
|
206 || (P.reserved "domintros" >> K DomIntros) |
|
207 || (P.reserved "tailrec" >> K Tailrec) |
|
208 || ((P.$$$ "in" |-- P.xname) >> Target) |
|
209 |
|
210 fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) |
|
211 >> (fn opts => fold apply_opt opts def) |
|
212 |
|
213 fun pipe_list1 s = P.enum1 "|" s |
|
214 |
|
215 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" |
|
216 |
|
217 fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) |
|
218 |
|
219 val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) |
|
220 --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) |
|
221 |
|
222 val statements_ow = pipe_list1 statement_ow |
|
223 in |
|
224 fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow |
|
225 end |
|
226 |
|
227 |
|
228 |
186 |
229 (* Common operations on equations *) |
187 (* Common operations on equations *) |
230 |
188 |
231 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) |
189 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) |
232 | open_all_all t = ([], t) |
190 | open_all_all t = ([], t) |
264 in |
222 in |
265 fold f fqgars Symtab.empty |
223 fold f fqgars Symtab.empty |
266 end |
224 end |
267 |
225 |
268 |
226 |
|
227 (* Check for all sorts of errors in the input *) |
|
228 fun check_defs ctxt fixes eqs = |
|
229 let |
|
230 val fnames = map (fst o fst) fixes |
|
231 |
|
232 fun check geq = |
|
233 let |
|
234 fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] |
|
235 |
|
236 val fqgar as (fname, qs, gs, args, rhs) = split_def geq |
|
237 |
|
238 val _ = fname mem fnames |
|
239 orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames |
|
240 ^ commas_quote fnames)) |
|
241 |
|
242 fun add_bvs t is = add_loose_bnos (t, 0, is) |
|
243 val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |
|
244 |> map (fst o nth (rev qs)) |
|
245 |
|
246 val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs |
|
247 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) |
|
248 |
|
249 val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs |
|
250 orelse error (input_error "Recursive Calls not allowed in premises") |
|
251 in |
|
252 fqgar |
|
253 end |
|
254 |
|
255 val _ = mk_arities (map check eqs) |
|
256 handle ArgumentCount fname => |
|
257 error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") |
|
258 in |
|
259 () |
|
260 end |
|
261 |
|
262 (* Preprocessors *) |
|
263 |
|
264 type fixes = ((string * typ) * mixfix) list |
|
265 type 'a spec = ((bstring * Attrib.src list) * 'a list) list |
|
266 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec)) |
|
267 |
|
268 fun empty_preproc check _ _ ctxt fixes spec = |
|
269 let |
|
270 val (nas,tss) = split_list spec |
|
271 val _ = check ctxt fixes (flat tss) |
|
272 in |
|
273 (flat tss, curry op ~~ nas o Library.unflat tss) |
|
274 end |
|
275 |
|
276 structure Preprocessor = GenericDataFun |
|
277 ( |
|
278 type T = preproc |
|
279 val empty = empty_preproc check_defs |
|
280 val extend = I |
|
281 fun merge _ (a, _) = a |
|
282 ); |
|
283 |
|
284 val get_preproc = Preprocessor.get o Context.Proof |
|
285 val set_preproc = Preprocessor.map o K |
|
286 |
|
287 |
|
288 |
|
289 local |
|
290 structure P = OuterParse and K = OuterKeyword |
|
291 |
|
292 val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false |
|
293 |
|
294 val option_parser = (P.$$$ "sequential" >> K Sequential) |
|
295 || ((P.reserved "default" |-- P.term) >> Default) |
|
296 || (P.reserved "domintros" >> K DomIntros) |
|
297 || (P.reserved "tailrec" >> K Tailrec) |
|
298 || ((P.$$$ "in" |-- P.xname) >> Target) |
|
299 |
|
300 fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) |
|
301 >> (fn opts => fold apply_opt opts default) |
|
302 |
|
303 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" |
|
304 |
|
305 fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) |
|
306 |
|
307 val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) |
|
308 --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) |
|
309 |
|
310 val statements_ow = P.enum1 "|" statement_ow |
|
311 |
|
312 val flags_statements = statements_ow |
|
313 >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow)) |
|
314 |
|
315 fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements) |
|
316 in |
|
317 fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements) |
|
318 |
|
319 end |
|
320 |
|
321 |
|
322 |
|
323 |
|
324 |
|
325 val default_config = FundefConfig { sequential=false, default="%x. arbitrary", |
|
326 target=NONE, domintros=false, tailrec=false } |
269 |
327 |
270 |
328 |
271 |
329 |
272 end |
330 end |
273 |
331 |