# HG changeset patch # User krauss # Date 1256304799 -7200 # Node ID 3e9ae903227360358b7d4d70badfbaa2178b01b0 # Parent 6e5b994070c1735e488a7f4c79c8d98ed6f844e4 renamed FundefDatatype -> Function_Fun diff -r 6e5b994070c1 -r 3e9ae9032273 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Fri Oct 23 20:48:14 2009 +0200 +++ b/src/HOL/FunDef.thy Fri Oct 23 15:33:19 2009 +0200 @@ -22,7 +22,7 @@ ("Tools/Function/measure_functions.ML") ("Tools/Function/lexicographic_order.ML") ("Tools/Function/pat_completeness.ML") - ("Tools/Function/fundef_datatype.ML") + ("Tools/Function/fun.ML") ("Tools/Function/induction_scheme.ML") ("Tools/Function/termination.ML") ("Tools/Function/decompose.ML") @@ -115,13 +115,13 @@ use "Tools/Function/auto_term.ML" use "Tools/Function/fundef.ML" use "Tools/Function/pat_completeness.ML" -use "Tools/Function/fundef_datatype.ML" +use "Tools/Function/fun.ML" use "Tools/Function/induction_scheme.ML" setup {* Fundef.setup #> Pat_Completeness.setup - #> FundefDatatype.setup + #> Function_Fun.setup #> InductionScheme.setup *} diff -r 6e5b994070c1 -r 3e9ae9032273 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 23 20:48:14 2009 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 23 15:33:19 2009 +0200 @@ -162,9 +162,9 @@ Tools/Function/descent.ML \ Tools/Function/fundef_common.ML \ Tools/Function/fundef_core.ML \ - Tools/Function/fundef_datatype.ML \ Tools/Function/fundef_lib.ML \ Tools/Function/fundef.ML \ + Tools/Function/fun.ML \ Tools/Function/induction_scheme.ML \ Tools/Function/inductive_wrap.ML \ Tools/Function/lexicographic_order.ML \ diff -r 6e5b994070c1 -r 3e9ae9032273 src/HOL/Tools/Function/fun.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/fun.ML Fri Oct 23 15:33:19 2009 +0200 @@ -0,0 +1,178 @@ +(* Title: HOL/Tools/Function/fun.ML + Author: Alexander Krauss, TU Muenchen + +Sequential mode for function definitions +Command "fun" for fully automated function definitions +*) + +signature FUNCTION_FUN = +sig + val add_fun : FundefCommon.fundef_config -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> + bool -> local_theory -> Proof.context + val add_fun_cmd : FundefCommon.fundef_config -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> + bool -> local_theory -> Proof.context + + val setup : theory -> theory +end + +structure Function_Fun : FUNCTION_FUN = +struct + +open FundefLib +open FundefCommon + + +fun check_pats ctxt geq = + let + fun err str = error (cat_lines ["Malformed definition:", + str ^ " not allowed in sequential mode.", + Syntax.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 Datatype.info_of_constr thy (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 ctxt geq + + 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 _ => Integer.add 1 | _ => I)) args 0 > length qs + then err "Nonlinear patterns" else () + in + () + end + +val by_pat_completeness_auto = + Proof.global_future_terminal_proof + (Method.Basic Pat_Completeness.pat_completeness, + SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) + +fun termination_by method int = + Fundef.termination_proof NONE + #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int + +fun mk_catchall fixes arity_of = + let + fun mk_eqn ((fname, fT), _) = + let + val n = arity_of 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 Logic.all qs + end + in + map mk_eqn fixes + end + +fun add_catchall ctxt fixes spec = + let val fqgars = map (split_def ctxt) spec + val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars + |> AList.lookup (op =) #> the + in + spec @ mk_catchall fixes arity_of + end + +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, []) = (warning (msg t); []) + | check (t, s) = s + in + (map check (origs ~~ tss'); tss) + end + + +fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec = + if sequential then + let + val (bnds, eqss) = split_list spec + + val eqs = map the_single eqss + + val feqs = eqs + |> tap (check_defs ctxt fixes) (* Standard checks *) + |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) + + val compleqs = add_catchall ctxt fixes feqs (* Completion *) + + val spliteqs = warn_if_redundant ctxt feqs + (FundefSplit.split_all_equations ctxt compleqs) + + fun restore_spec thms = + bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms) + + val spliteqs' = flat (Library.take (length bnds, spliteqs)) + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' + + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) + |> map (map snd) + + + val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding + + (* using theorem names for case name currently disabled *) + val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) + (bnds' ~~ spliteqs) + |> flat + in + (flat spliteqs, restore_spec, sort, case_names) + end + else + FundefCommon.empty_preproc check_defs config ctxt fixes spec + +val setup = + Context.theory_map (FundefCommon.set_preproc sequential_preproc) + + +val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), + domintros=false, tailrec=false } + +fun gen_fun add config fixes statements int lthy = + let val group = serial_string () in + lthy + |> LocalTheory.set_group group + |> add fixes statements config + |> by_pat_completeness_auto int + |> LocalTheory.restore + |> LocalTheory.set_group group + |> termination_by (FundefCommon.get_termination_prover lthy) int + end; + +val add_fun = gen_fun Fundef.add_fundef +val add_fun_cmd = gen_fun Fundef.add_fundef_cmd + + + +local structure P = OuterParse and K = OuterKeyword in + +val _ = + OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl + (fundef_parser fun_config + >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements)); + +end + +end diff -r 6e5b994070c1 -r 3e9ae9032273 src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Fri Oct 23 20:48:14 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,178 +0,0 @@ -(* Title: HOL/Tools/Function/fundef_datatype.ML - Author: Alexander Krauss, TU Muenchen - -A package for general recursive function definitions. -A tactic to prove completeness of datatype patterns. -*) - -signature FUNDEF_DATATYPE = -sig - val add_fun : FundefCommon.fundef_config -> - (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> - bool -> local_theory -> Proof.context - val add_fun_cmd : FundefCommon.fundef_config -> - (binding * string option * mixfix) list -> (Attrib.binding * string) list -> - bool -> local_theory -> Proof.context - - val setup : theory -> theory -end - -structure FundefDatatype : FUNDEF_DATATYPE = -struct - -open FundefLib -open FundefCommon - - -fun check_pats ctxt geq = - let - fun err str = error (cat_lines ["Malformed definition:", - str ^ " not allowed in sequential mode.", - Syntax.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 Datatype.info_of_constr thy (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 ctxt geq - - 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 _ => Integer.add 1 | _ => I)) args 0 > length qs - then err "Nonlinear patterns" else () - in - () - end - -val by_pat_completeness_auto = - Proof.global_future_terminal_proof - (Method.Basic Pat_Completeness.pat_completeness, - SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) - -fun termination_by method int = - Fundef.termination_proof NONE - #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int - -fun mk_catchall fixes arity_of = - let - fun mk_eqn ((fname, fT), _) = - let - val n = arity_of 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 Logic.all qs - end - in - map mk_eqn fixes - end - -fun add_catchall ctxt fixes spec = - let val fqgars = map (split_def ctxt) spec - val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars - |> AList.lookup (op =) #> the - in - spec @ mk_catchall fixes arity_of - end - -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, []) = (warning (msg t); []) - | check (t, s) = s - in - (map check (origs ~~ tss'); tss) - end - - -fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec = - if sequential then - let - val (bnds, eqss) = split_list spec - - val eqs = map the_single eqss - - val feqs = eqs - |> tap (check_defs ctxt fixes) (* Standard checks *) - |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) - - val compleqs = add_catchall ctxt fixes feqs (* Completion *) - - val spliteqs = warn_if_redundant ctxt feqs - (FundefSplit.split_all_equations ctxt compleqs) - - fun restore_spec thms = - bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms) - - val spliteqs' = flat (Library.take (length bnds, spliteqs)) - val fnames = map (fst o fst) fixes - val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' - - fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) - |> map (map snd) - - - val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding - - (* using theorem names for case name currently disabled *) - val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) - (bnds' ~~ spliteqs) - |> flat - in - (flat spliteqs, restore_spec, sort, case_names) - end - else - FundefCommon.empty_preproc check_defs config ctxt fixes spec - -val setup = - Context.theory_map (FundefCommon.set_preproc sequential_preproc) - - -val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), - domintros=false, tailrec=false } - -fun gen_fun add config fixes statements int lthy = - let val group = serial_string () in - lthy - |> LocalTheory.set_group group - |> add fixes statements config - |> by_pat_completeness_auto int - |> LocalTheory.restore - |> LocalTheory.set_group group - |> termination_by (FundefCommon.get_termination_prover lthy) int - end; - -val add_fun = gen_fun Fundef.add_fundef -val add_fun_cmd = gen_fun Fundef.add_fundef_cmd - - - -local structure P = OuterParse and K = OuterKeyword in - -val _ = - OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl - (fundef_parser fun_config - >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements)); - -end - -end