187 FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec} |
188 FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec} |
188 | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) = |
189 | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) = |
189 FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true} |
190 FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true} |
190 |
191 |
191 val default_config = |
192 val default_config = |
192 FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false } |
193 FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), |
|
194 domintros=false, tailrec=false } |
193 |
195 |
194 |
196 |
195 (* Analyzing function equations *) |
197 (* Analyzing function equations *) |
196 |
198 |
197 fun split_def ctxt geq = |
199 fun split_def ctxt geq = |
232 let |
234 let |
233 val fnames = map (fst o fst) fixes |
235 val fnames = map (fst o fst) fixes |
234 |
236 |
235 fun check geq = |
237 fun check geq = |
236 let |
238 let |
237 fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
239 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
238 |
240 |
239 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq |
241 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq |
240 |
242 |
241 val _ = fname mem fnames |
243 val _ = fname mem fnames |
242 orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames |
244 orelse input_error |
243 ^ commas_quote fnames)) |
245 ("Head symbol of left hand side must be " |
|
246 ^ plural "" "one out of " fnames ^ commas_quote fnames) |
244 |
247 |
245 fun add_bvs t is = add_loose_bnos (t, 0, is) |
248 fun add_bvs t is = add_loose_bnos (t, 0, is) |
246 val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |
249 val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |
247 |> map (fst o nth (rev qs)) |
250 |> map (fst o nth (rev qs)) |
248 |
251 |
249 val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs |
252 val _ = null rvs orelse input_error |
250 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) |
253 ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs |
|
254 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
251 |
255 |
252 val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs |
256 val _ = forall (not o Term.exists_subterm |
253 orelse error (input_error "Recursive Calls not allowed in premises") |
257 (fn Free (n, _) => n mem fnames | _ => false)) gs |
|
258 orelse input_error "Recursive Calls not allowed in premises" |
254 |
259 |
255 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
260 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
256 val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
261 val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
257 val _ = null funvars |
262 val _ = null funvars |
258 orelse (warning (cat_lines ["Bound variable" ^ plural " " "s " funvars ^ commas_quote (map fst funvars) ^ |
263 orelse (warning (cat_lines |
259 " occur" ^ plural "s" "" funvars ^ " in function position.", |
264 ["Bound variable" ^ plural " " "s " funvars |
260 "Misspelled constructor???"]); true) |
265 ^ commas_quote (map fst funvars) ^ |
|
266 " occur" ^ plural "s" "" funvars ^ " in function position.", |
|
267 "Misspelled constructor???"]); true) |
261 in |
268 in |
262 fqgar |
269 fqgar |
263 end |
270 end |
264 |
271 |
265 fun check_sorts ((fname, fT), _) = |
272 fun check_sorts ((fname, fT), _) = |
266 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) |
273 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) |
267 orelse error ("Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ".") |
274 orelse error (cat_lines |
|
275 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
|
276 setmp show_sorts true (Syntax.string_of_typ ctxt) fT]) |
268 |
277 |
269 val _ = map check_sorts fixes |
278 val _ = map check_sorts fixes |
270 |
279 |
271 val _ = mk_arities (map check eqs) |
280 val _ = mk_arities (map check eqs) |
272 handle ArgumentCount fname => |
281 handle ArgumentCount fname => |
273 error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") |
282 error ("Function " ^ quote fname ^ |
|
283 " has different numbers of arguments in different equations") |
274 in |
284 in |
275 () |
285 () |
276 end |
286 end |
277 |
287 |
278 (* Preprocessors *) |
288 (* Preprocessors *) |
280 type fixes = ((string * typ) * mixfix) list |
290 type fixes = ((string * typ) * mixfix) list |
281 type 'a spec = ((bstring * Attrib.src list) * 'a list) list |
291 type 'a spec = ((bstring * Attrib.src list) * 'a list) list |
282 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec |
292 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec |
283 -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
293 -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
284 |
294 |
285 val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
295 val fname_of = fst o dest_Free o fst o strip_comb o fst |
|
296 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
286 |
297 |
287 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k |
298 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k |
288 | mk_case_names _ n 0 = [] |
299 | mk_case_names _ n 0 = [] |
289 | mk_case_names _ n 1 = [n] |
300 | mk_case_names _ n 1 = [n] |
290 | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) |
301 | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) |
295 val ts = flat tss |
306 val ts = flat tss |
296 val _ = check ctxt fixes ts |
307 val _ = check ctxt fixes ts |
297 val fnames = map (fst o fst) fixes |
308 val fnames = map (fst o fst) fixes |
298 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
309 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
299 |
310 |
300 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
311 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) |
|
312 (indices ~~ xs) |
301 |> map (map snd) |
313 |> map (map snd) |
302 |
314 |
303 (* using theorem names for case name currently disabled *) |
315 (* using theorem names for case name currently disabled *) |
304 val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat |
316 val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat |
305 in |
317 in |
320 |
332 |
321 |
333 |
322 local |
334 local |
323 structure P = OuterParse and K = OuterKeyword |
335 structure P = OuterParse and K = OuterKeyword |
324 |
336 |
325 val option_parser = (P.reserved "sequential" >> K Sequential) |
337 val option_parser = |
326 || ((P.reserved "default" |-- P.term) >> Default) |
338 P.group "option" ((P.reserved "sequential" >> K Sequential) |
327 || (P.reserved "domintros" >> K DomIntros) |
339 || ((P.reserved "default" |-- P.term) >> Default) |
328 || (P.reserved "tailrec" >> K Tailrec) |
340 || (P.reserved "domintros" >> K DomIntros) |
329 |
341 || (P.reserved "tailrec" >> K Tailrec)) |
330 fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) |
342 |
331 >> (fn opts => fold apply_opt opts default) |
343 fun config_parser default = |
|
344 (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") []) |
|
345 >> (fn opts => fold apply_opt opts default) |
332 |
346 |
333 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" |
347 val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" |
334 |
348 |
335 fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) |
349 fun pipe_error t = |
336 |
350 P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) |
337 val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) |
351 |
338 --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) |
352 val statement_ow = |
|
353 SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) |
|
354 --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) |
339 |
355 |
340 val statements_ow = P.enum1 "|" statement_ow |
356 val statements_ow = P.enum1 "|" statement_ow |
341 |
357 |
342 val flags_statements = statements_ow |
358 val flags_statements = statements_ow |
343 >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow)) |
359 >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow)) |
344 in |
360 in |
345 fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements) |
361 fun fundef_parser default_cfg = |
|
362 config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements |
346 end |
363 end |
347 |
364 |
348 |
365 |
349 end |
366 end |
350 end |
367 end |