# HG changeset patch # User krauss # Date 1238416956 -7200 # Node ID 5b7a5a05c7aa4f94885107493807ef4580f8b773 # Parent 15f64e05e7035f23e5f1c3aff8f8962c946b193c remove "otherwise" feature from function package which was never really documented or used diff -r 15f64e05e703 -r 5b7a5a05c7aa src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Mar 30 12:25:52 2009 +1100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Mar 30 14:42:36 2009 +0200 @@ -290,7 +290,7 @@ 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 +type preproc = fundef_config -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) val fname_of = fst o dest_Free o fst o strip_comb o fst @@ -301,7 +301,7 @@ | mk_case_names _ n 1 = [n] | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) -fun empty_preproc check _ _ ctxt fixes spec = +fun empty_preproc check _ ctxt fixes spec = let val (nas,tss) = split_list spec val ts = flat tss @@ -345,22 +345,17 @@ (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 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) + val statement = + SpecParse.opt_thm_name ":" -- P.prop --| 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)) + val statements = P.enum1 "|" statement in fun fundef_parser default_cfg = - config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements + config_parser default_cfg -- P.fixes --| P.where_ -- statements end diff -r 15f64e05e703 -r 5b7a5a05c7aa src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Mar 30 12:25:52 2009 +1100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Mar 30 14:42:36 2009 +0200 @@ -15,10 +15,10 @@ val add_fun : FundefCommon.fundef_config -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> - bool list -> bool -> local_theory -> Proof.context + bool -> local_theory -> Proof.context val add_fun_cmd : FundefCommon.fundef_config -> (binding * string option * mixfix) list -> (Attrib.binding * string) list -> - bool list -> bool -> local_theory -> Proof.context + bool -> local_theory -> Proof.context end structure FundefDatatype : FUNDEF_DATATYPE = @@ -235,32 +235,23 @@ end fun add_catchall ctxt fixes spec = - let - val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec))) - in - spec @ map (pair true) catchalls - end + spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec)) fun warn_if_redundant ctxt origs tss = let fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t) val (tss', _) = chop (length origs) tss - fun check ((_, t), []) = (Output.warning (msg t); []) - | check ((_, t), s) = s + fun check (t, []) = (Output.warning (msg t); []) + | check (t, s) = s in (map check (origs ~~ tss'); tss) end -fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec = - let - val enabled = sequential orelse exists I flags - in - if enabled then +fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec = + if sequential 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 @@ -268,12 +259,11 @@ val feqs = eqs |> tap (check_defs ctxt fixes) (* Standard checks *) |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) - |> curry op ~~ flags' val compleqs = add_catchall ctxt fixes feqs (* Completion *) val spliteqs = warn_if_redundant ctxt feqs - (FundefSplit.split_some_equations ctxt compleqs) + (FundefSplit.split_all_equations ctxt compleqs) fun restore_spec thms = nas ~~ Library.take (length nas, Library.unflat spliteqs thms) @@ -296,8 +286,7 @@ (flat spliteqs, restore_spec, sort, case_names) end else - FundefCommon.empty_preproc check_defs config flags ctxt fixes spec - end + FundefCommon.empty_preproc check_defs config ctxt fixes spec val setup = Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness) @@ -308,11 +297,11 @@ val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false } -fun gen_fun add config fixes statements flags int lthy = +fun gen_fun add config fixes statements int lthy = let val group = serial_string () in lthy |> LocalTheory.set_group group - |> add fixes statements config flags + |> add fixes statements config |> by_pat_completeness_auto int |> LocalTheory.restore |> LocalTheory.set_group group @@ -329,7 +318,7 @@ val _ = OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl (fundef_parser fun_config - >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags)); + >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements)); end diff -r 15f64e05e703 -r 5b7a5a05c7aa src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 30 12:25:52 2009 +1100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Mar 30 14:42:36 2009 +0200 @@ -10,13 +10,11 @@ val add_fundef : (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> FundefCommon.fundef_config - -> bool list -> local_theory -> Proof.state val add_fundef_cmd : (binding * string option * mixfix) list -> (Attrib.binding * string) list -> FundefCommon.fundef_config - -> bool list -> local_theory -> Proof.state @@ -95,13 +93,13 @@ end -fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy = +fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy = let val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy val fixes = map (apfst (apfst Binding.name_of)) fixes0; val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0; - val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec + val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec val defname = mk_defname fixes @@ -209,12 +207,10 @@ local structure P = OuterParse and K = OuterKeyword in -val _ = OuterKeyword.keyword "otherwise"; - val _ = OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal (fundef_parser default_config - >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags)); + >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config)); val _ = OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal