"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
more cleanup.
--- a/src/HOL/FunDef.thy Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/FunDef.thy Sat Jun 02 15:28:38 2007 +0200
@@ -9,8 +9,8 @@
imports Datatype Accessible_Part
uses
("Tools/function_package/sum_tools.ML")
+ ("Tools/function_package/fundef_lib.ML")
("Tools/function_package/fundef_common.ML")
- ("Tools/function_package/fundef_lib.ML")
("Tools/function_package/inductive_wrap.ML")
("Tools/function_package/context_tree.ML")
("Tools/function_package/fundef_core.ML")
@@ -88,8 +88,8 @@
use "Tools/function_package/sum_tools.ML"
+use "Tools/function_package/fundef_lib.ML"
use "Tools/function_package/fundef_common.ML"
-use "Tools/function_package/fundef_lib.ML"
use "Tools/function_package/inductive_wrap.ML"
use "Tools/function_package/context_tree.ML"
use "Tools/function_package/fundef_core.ML"
--- a/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 15:28:38 2007 +0200
@@ -3,7 +3,7 @@
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
-Common type definitions and other infrastructure.
+Common definitions and other infrastructure.
*)
structure FundefCommon =
@@ -153,12 +153,10 @@
#> store_termination_rule termination
-
(* Configuration management *)
datatype fundef_opt
= Sequential
| Default of string
- | Preprocessor of string
| Target of xstring
| DomIntros
| Tailrec
@@ -168,64 +166,24 @@
{
sequential: bool,
default: string,
- preprocessor: string option,
target: xstring option,
domintros: bool,
tailrec: bool
}
-
-val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
- target=NONE, domintros=false, tailrec=false }
-
-val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE,
- target=NONE, domintros=false, tailrec=false }
-
-fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
- FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
- | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
- FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
- | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
- FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
- | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
- FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
- | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
- FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
- | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
- FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true }
+fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) =
+ FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec}
+ | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) =
+ FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec}
+ | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) =
+ FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec}
+ | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) =
+ FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec}
+ | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) =
+ FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true}
fun target_of (FundefConfig {target, ...}) = target
-local
- structure P = OuterParse and K = OuterKeyword
-
- val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
-
- val option_parser = (P.$$$ "sequential" >> K Sequential)
- || ((P.reserved "default" |-- P.term) >> Default)
- || (P.reserved "domintros" >> K DomIntros)
- || (P.reserved "tailrec" >> K Tailrec)
- || ((P.$$$ "in" |-- P.xname) >> Target)
-
- fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
- >> (fn opts => fold apply_opt opts def)
-
- fun pipe_list1 s = P.enum1 "|" s
-
- val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-
- fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
-
- val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
- --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
-
- val statements_ow = pipe_list1 statement_ow
-in
- fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
-end
-
-
-
(* Common operations on equations *)
fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
@@ -266,6 +224,106 @@
end
+(* Check for all sorts of errors in the input *)
+fun check_defs ctxt fixes eqs =
+ let
+ val fnames = map (fst o fst) fixes
+
+ fun check geq =
+ let
+ fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
+
+ val fqgar as (fname, qs, gs, args, rhs) = split_def geq
+
+ val _ = fname mem fnames
+ orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames
+ ^ commas_quote fnames))
+
+ fun add_bvs t is = add_loose_bnos (t, 0, is)
+ val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
+ |> map (fst o nth (rev qs))
+
+ val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
+ ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
+
+ val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs
+ orelse error (input_error "Recursive Calls not allowed in premises")
+ in
+ fqgar
+ end
+
+ val _ = mk_arities (map check eqs)
+ handle ArgumentCount fname =>
+ error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
+ in
+ ()
+ end
+
+(* Preprocessors *)
+
+type fixes = ((string * typ) * mixfix) list
+type 'a spec = ((bstring * Attrib.src list) * 'a list) list
+type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))
+
+fun empty_preproc check _ _ ctxt fixes spec =
+ let
+ val (nas,tss) = split_list spec
+ val _ = check ctxt fixes (flat tss)
+ in
+ (flat tss, curry op ~~ nas o Library.unflat tss)
+ end
+
+structure Preprocessor = GenericDataFun
+(
+ type T = preproc
+ val empty = empty_preproc check_defs
+ val extend = I
+ fun merge _ (a, _) = a
+);
+
+val get_preproc = Preprocessor.get o Context.Proof
+val set_preproc = Preprocessor.map o K
+
+
+
+local
+ structure P = OuterParse and K = OuterKeyword
+
+ val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
+
+ val option_parser = (P.$$$ "sequential" >> K Sequential)
+ || ((P.reserved "default" |-- P.term) >> Default)
+ || (P.reserved "domintros" >> K DomIntros)
+ || (P.reserved "tailrec" >> K Tailrec)
+ || ((P.$$$ "in" |-- P.xname) >> Target)
+
+ fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
+ >> (fn opts => fold apply_opt opts default)
+
+ val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
+
+ fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
+
+ val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
+ --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
+
+ val statements_ow = P.enum1 "|" statement_ow
+
+ val flags_statements = statements_ow
+ >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
+
+ fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
+in
+ fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
+
+end
+
+
+
+
+
+val default_config = FundefConfig { sequential=false, default="%x. arbitrary",
+ target=NONE, domintros=false, tailrec=false }
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Sat Jun 02 15:28:38 2007 +0200
@@ -14,45 +14,45 @@
val setup : theory -> theory
end
-structure FundefDatatype : FUNDEF_DATATYPE =
+structure FundefDatatype (*: FUNDEF_DATATYPE*) =
struct
open FundefLib
open FundefCommon
-fun check_constr_pattern thy err (Bound _) = ()
- | check_constr_pattern thy err t =
- let
- val (hd, args) = strip_comb t
- in
- (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of
- SOME _ => ()
- | NONE => err t)
- handle TERM ("dest_Const", _) => err t);
- map (check_constr_pattern thy err) args;
- ())
- end
-
fun check_pats ctxt geq =
let
- fun err str = error (cat_lines ["Malformed \"fun\" definition:",
- str,
+ fun err str = error (cat_lines ["Malformed definition:",
+ str ^ " not allowed in sequential mode.",
ProofContext.string_of_term ctxt geq])
val thy = ProofContext.theory_of ctxt
-
+
+ fun check_constr_pattern (Bound _) = ()
+ | check_constr_pattern t =
+ let
+ val (hd, args) = strip_comb t
+ in
+ (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of
+ SOME _ => ()
+ | NONE => err "Non-constructor pattern")
+ handle TERM ("dest_Const", _) => err "Non-constructor patterns");
+ map check_constr_pattern args;
+ ())
+ end
+
val (fname, qs, gs, args, rhs) = split_def geq
-
- val _ = if not (null gs) then err "Conditional equations not allowed with \"fun\"" else ()
- val _ = map (check_constr_pattern thy (fn t => err "Not a constructor pattern")) args
-
+
+ val _ = if not (null gs) then err "Conditional equations" else ()
+ val _ = map check_constr_pattern args
+
(* just count occurrences to check linearity *)
val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 < length qs
- then err "Nonlinear pattern" else ()
+ then err "Nonlinear patterns" else ()
in
()
end
-
+
fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
@@ -206,27 +206,83 @@
FundefPackage.setup_termination_proof NONE
#> Proof.global_terminal_proof (Method.Basic (LexicographicOrder.lexicographic_order []), NONE)
+fun mk_catchall fixes arities =
+ let
+ fun mk_eqn ((fname, fT), _) =
+ let
+ val n = the (Symtab.lookup arities fname)
+ val (argTs, rT) = chop n (binder_types fT)
+ |> apsnd (fn Ts => Ts ---> body_type fT)
+
+ val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
+ in
+ HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
+ Const ("HOL.undefined", rT))
+ |> HOLogic.mk_Trueprop
+ |> fold_rev mk_forall qs
+ end
+ in
+ map mk_eqn fixes
+ end
+
+fun add_catchall fixes spec =
+ let
+ val catchalls = mk_catchall fixes (mk_arities (map split_def (map snd spec)))
+ in
+ spec @ map (pair true) catchalls
+ end
+
+fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
+ let
+ val enabled = sequential orelse exists I flags
+ in
+ if enabled then
+ let
+ val flags' = if sequential then map (K true) flags else flags
+
+ val (nas, eqss) = split_list spec
+
+ val eqs = map the_single eqss
+
+ val spliteqs = eqs
+ |> tap (check_defs ctxt fixes) (* Standard checks *)
+ |> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
+ |> curry op ~~ flags'
+ |> add_catchall fixes (* Completion: still disabled *)
+ |> FundefSplit.split_some_equations ctxt
+
+ fun restore_spec thms =
+ nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
+ in
+ (flat spliteqs, restore_spec)
+ end
+ else
+ FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
+ end
+
val setup =
- Method.add_methods [("pat_completeness", Method.no_args pat_completeness,
- "Completeness prover for datatype patterns")]
+ Method.add_methods [("pat_completeness", Method.no_args pat_completeness,
+ "Completeness prover for datatype patterns")]
+ #> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
+val fun_config = FundefConfig { sequential=true, default="%x. arbitrary",
+ target=NONE, domintros=false, tailrec=false }
local structure P = OuterParse and K = OuterKeyword in
-fun fun_cmd config fixes statements lthy =
+fun fun_cmd config fixes statements flags lthy =
lthy
- |> FundefPackage.add_fundef fixes statements config
+ |> FundefPackage.add_fundef fixes statements config flags
|> by_pat_completeness_simp
|> termination_by_lexicographic_order
-
val funP =
OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
- (fundef_parser FundefCommon.fun_config
- >> (fn ((config, fixes), statements) =>
- (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements))));
+ (fundef_parser fun_config
+ >> (fn ((config, fixes), (flags, statements)) =>
+ (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
val _ = OuterSyntax.add_parsers [funP];
end
--- a/src/HOL/Tools/function_package/fundef_lib.ML Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Sat Jun 02 15:28:38 2007 +0200
@@ -10,12 +10,6 @@
structure FundefLib = struct
-(* ==> library/string *)
-fun plural sg pl [x] = sg
- | plural sg pl _ = pl
-
-
-
fun map_option f NONE = NONE
| map_option f (SOME x) = SOME (f x);
@@ -25,11 +19,6 @@
fun fold_map_option f NONE y = (NONE, y)
| fold_map_option f (SOME x) y = apfst SOME (f x y);
-
-
-
-
-
(* ??? *)
fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
--- a/src/HOL/Tools/function_package/fundef_package.ML Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sat Jun 02 15:28:38 2007 +0200
@@ -10,14 +10,16 @@
signature FUNDEF_PACKAGE =
sig
val add_fundef : (string * string option * mixfix) list
- -> ((bstring * Attrib.src list) * (string * bool)) list
+ -> ((bstring * Attrib.src list) * string) list
-> FundefCommon.fundef_config
+ -> bool list
-> local_theory
-> Proof.state
val add_fundef_i: (string * typ option * mixfix) list
- -> ((bstring * Attrib.src list) * (term * bool)) list
+ -> ((bstring * Attrib.src list) * term) list
-> FundefCommon.fundef_config
+ -> bool list
-> local_theory
-> Proof.state
@@ -32,7 +34,7 @@
end
-structure FundefPackage (*: FUNDEF_PACKAGE*) =
+structure FundefPackage : FUNDEF_PACKAGE =
struct
open FundefLib
@@ -42,80 +44,12 @@
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-
-(* Check for all sorts of errors in the input *)
-fun check_def ctxt fixes eqs =
- let
- val fnames = map (fst o fst) fixes
-
- fun check geq =
- let
- fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
-
- val fqgar as (fname, qs, gs, args, rhs) = split_def geq
-
- val _ = fname mem fnames
- orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames
- ^ commas_quote fnames))
-
- fun add_bvs t is = add_loose_bnos (t, 0, is)
- val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
- |> map (fst o nth (rev qs))
-
- val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
- ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
-
- val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
- error (input_error "Recursive Calls not allowed in premises")
- in
- fqgar
- end
- in
- (mk_arities (map check eqs); ())
- handle ArgumentCount fname =>
- error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
- end
-
-
-fun mk_catchall fixes arities =
- let
- fun mk_eqn ((fname, fT), _) =
- let
- val n = the (Symtab.lookup arities fname)
- val (argTs, rT) = chop n (binder_types fT)
- |> apsnd (fn Ts => Ts ---> body_type fT)
-
- val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
- in
- HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
- Const ("HOL.undefined", rT))
- |> HOLogic.mk_Trueprop
- |> fold_rev mk_forall qs
- end
- in
- map mk_eqn fixes
- end
-
-fun add_catchall fixes spec =
- let
- val catchalls = mk_catchall fixes (mk_arities (map split_def (map (snd o snd) spec)))
- in
- spec @ map (pair ("",[]) o pair true) catchalls
- end
-
-fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
- let val (xs, ys) = split_list ps
- in xs ~~ f ys end
-
-fun restore_spec_structure reps spec =
- (burrow_snd o burrow o K) reps spec
-
-fun add_simps fixes spec sort label moreatts simps lthy =
+fun add_simps fixes post sort label moreatts simps lthy =
let
val fnames = map (fst o fst) fixes
val (saved_spec_simps, lthy) =
- fold_map note_theorem (restore_spec_structure simps spec) lthy
+ fold_map note_theorem (post simps) lthy
val saved_simps = flat (map snd saved_spec_simps)
val simps_by_f = sort saved_simps
@@ -129,13 +63,13 @@
fold2 add_for_f fnames simps_by_f lthy)
end
-fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
+fun fundef_afterqed config fixes post defname cont sort_cont [[proof]] lthy =
let
val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} =
cont (Goal.close_result proof)
val qualify = NameSpace.qualified defname
- val addsmps = add_simps fixes spec sort_cont
+ val addsmps = add_simps fixes post sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
@@ -157,52 +91,36 @@
end (* FIXME: Add cases for induct and cases thm *)
-
-fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
+fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete when "read_specification" etc. is there *)
let
- val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags
- val eqns = map (apsnd (single o fst)) eqnss_flags
-
- val ((fixes, _), ctxt') = prep fixspec [] lthy
-
- fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
- |> apsnd the_single
+ val eqns = map (apsnd single) eqnss
- val raw_spec = map prep_eqn eqns
- |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
-
- val _ = check_def ctxt' fixes (map snd raw_spec)
+ val ((fixes, _), ctxt') = prep fixspec [] lthy
+ fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
- val spec = raw_spec
- |> burrow_snd (fn ts => flags ~~ ts)
- (*|> (if global_flag then add_catchall fixes else I) *) (* Completion: still disabled *)
- |> burrow_snd (FundefSplit.split_some_equations ctxt')
-
+ val spec = map prep_eqn eqns
+ |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *)
in
((fixes, spec), ctxt')
end
-fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
+fun gen_add_fundef prep fixspec eqnss config flags lthy =
let
- val FundefConfig {sequential, ...} = config
-
- val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
+ val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
+ val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
- val t_eqns = spec |> map snd |> flat (* flatten external structure *)
+ val ((goalstate, cont, sort_cont), lthy) =
+ FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
- val ((goalstate, cont, sort_cont), lthy) =
- FundefMutual.prepare_fundef_mutual config defname fixes t_eqns lthy
-
- val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
+ val afterqed = fundef_afterqed config fixes post defname cont sort_cont
in
lthy
|> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
|> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
end
-
fun total_termination_afterqed data [[totality]] lthy =
let
val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data
@@ -214,7 +132,6 @@
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
- (* FIXME: How to generate code from (possibly) local contexts*)
val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))]
@@ -293,8 +210,8 @@
val functionP =
OuterSyntax.command "function" "define general recursive functions" K.thy_goal
(fundef_parser default_config
- >> (fn ((config, fixes), statements) =>
- Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config)
+ >> (fn ((config, fixes), (flags, statements)) =>
+ Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
#> Toplevel.print));
val terminationP =
--- a/src/HOL/Tools/function_package/mutual.ML Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Sat Jun 02 15:28:38 2007 +0200
@@ -303,7 +303,7 @@
fun sort_by_function (Mutual {fqgars, ...}) names xs =
fold_rev (store_grouped (eq_str o apfst fst)) (* fill *)
- (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *)
+ (map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs) (* the name-thm pairs *)
(map (rpair []) names) (* in the empty buckets labeled with names *)
|> map (snd #> map snd) (* and remove the labels afterwards *)