1.1 --- a/src/HOL/FunDef.thy	Sat Jun 02 15:26:32 2007 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Sat Jun 02 15:28:38 2007 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  imports Datatype Accessible_Part
     1.5  uses
     1.6    ("Tools/function_package/sum_tools.ML")
     1.7 +  ("Tools/function_package/fundef_lib.ML")
     1.8    ("Tools/function_package/fundef_common.ML")
     1.9 -  ("Tools/function_package/fundef_lib.ML")
    1.10    ("Tools/function_package/inductive_wrap.ML")
    1.11    ("Tools/function_package/context_tree.ML")
    1.12    ("Tools/function_package/fundef_core.ML")
    1.13 @@ -88,8 +88,8 @@
    1.14  
    1.15  
    1.16  use "Tools/function_package/sum_tools.ML"
    1.17 +use "Tools/function_package/fundef_lib.ML"
    1.18  use "Tools/function_package/fundef_common.ML"
    1.19 -use "Tools/function_package/fundef_lib.ML"
    1.20  use "Tools/function_package/inductive_wrap.ML"
    1.21  use "Tools/function_package/context_tree.ML"
    1.22  use "Tools/function_package/fundef_core.ML"

     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Sat Jun 02 15:26:32 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Sat Jun 02 15:28:38 2007 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4      Author:     Alexander Krauss, TU Muenchen
     2.5  
     2.6  A package for general recursive function definitions. 
     2.7 -Common type definitions and other infrastructure.
     2.8 +Common definitions and other infrastructure.
     2.9  *)
    2.10  
    2.11  structure FundefCommon =
    2.12 @@ -153,12 +153,10 @@
    2.13      #> store_termination_rule termination
    2.14  
    2.15  
    2.16 -
    2.17  (* Configuration management *)
    2.18  datatype fundef_opt 
    2.19    = Sequential
    2.20    | Default of string
    2.21 -  | Preprocessor of string
    2.22    | Target of xstring
    2.23    | DomIntros
    2.24    | Tailrec
    2.25 @@ -168,64 +166,24 @@
    2.26     {
    2.27      sequential: bool,
    2.28      default: string,
    2.29 -    preprocessor: string option,
    2.30      target: xstring option,
    2.31      domintros: bool,
    2.32      tailrec: bool
    2.33     }
    2.34  
    2.35 -
    2.36 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
    2.37 -                                    target=NONE, domintros=false, tailrec=false }
    2.38 -
    2.39 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, 
    2.40 -                                target=NONE, domintros=false, tailrec=false }
    2.41 -
    2.42 -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
    2.43 -    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
    2.44 -  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
    2.45 -    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
    2.46 -  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = 
    2.47 -    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
    2.48 -  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
    2.49 -    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
    2.50 -  | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
    2.51 -    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
    2.52 -  | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
    2.53 -    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } 
    2.54 +fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) = 
    2.55 +    FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec}
    2.56 +  | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) = 
    2.57 +    FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec}
    2.58 +  | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) =
    2.59 +    FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec}
    2.60 +  | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) =
    2.61 +    FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec}
    2.62 +  | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) =
    2.63 +    FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true}
    2.64  
    2.65  fun target_of (FundefConfig {target, ...}) = target
    2.66  
    2.67 -local 
    2.68 -  structure P = OuterParse and K = OuterKeyword 
    2.69 -
    2.70 -  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    2.71 -                       
    2.72 -  val option_parser = (P.$$$ "sequential" >> K Sequential)
    2.73 -                   || ((P.reserved "default" |-- P.term) >> Default)
    2.74 -                   || (P.reserved "domintros" >> K DomIntros)
    2.75 -                   || (P.reserved "tailrec" >> K Tailrec)
    2.76 -                   || ((P.$$$ "in" |-- P.xname) >> Target)
    2.77 -
    2.78 -  fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
    2.79 -                          >> (fn opts => fold apply_opt opts def)
    2.80 -
    2.81 -  fun pipe_list1 s = P.enum1 "|" s
    2.82 -
    2.83 -  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    2.84 -
    2.85 -  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
    2.86 -
    2.87 -  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
    2.88 -                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
    2.89 -
    2.90 -  val statements_ow = pipe_list1 statement_ow
    2.91 -in
    2.92 -  fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
    2.93 -end
    2.94 -
    2.95 -
    2.96 -
    2.97  (* Common operations on equations *)
    2.98  
    2.99  fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
   2.100 @@ -266,6 +224,106 @@
   2.101      end
   2.102  
   2.103  
   2.104 +(* Check for all sorts of errors in the input *)
   2.105 +fun check_defs ctxt fixes eqs =
   2.106 +    let
   2.107 +      val fnames = map (fst o fst) fixes
   2.108 +                                
   2.109 +      fun check geq = 
   2.110 +          let
   2.111 +            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
   2.112 +                                  
   2.113 +            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
   2.114 +                                 
   2.115 +            val _ = fname mem fnames 
   2.116 +                    orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
   2.117 +                                               ^ commas_quote fnames))
   2.118 +                                            
   2.119 +            fun add_bvs t is = add_loose_bnos (t, 0, is)
   2.120 +            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
   2.121 +                        |> map (fst o nth (rev qs))
   2.122 +                      
   2.123 +            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
   2.124 +                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
   2.125 +                                    
   2.126 +            val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs 
   2.127 +                    orelse error (input_error "Recursive Calls not allowed in premises")
   2.128 +          in
   2.129 +            fqgar
   2.130 +          end
   2.131 +
   2.132 +      val _ = mk_arities (map check eqs)
   2.133 +          handle ArgumentCount fname => 
   2.134 +                 error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
   2.135 +    in
   2.136 +      ()
   2.137 +    end
   2.138 +
   2.139 +(* Preprocessors *)
   2.140 +
   2.141 +type fixes = ((string * typ) * mixfix) list
   2.142 +type 'a spec = ((bstring * Attrib.src list) * 'a list) list
   2.143 +type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))
   2.144 +
   2.145 +fun empty_preproc check _ _ ctxt fixes spec =
   2.146 +    let 
   2.147 +      val (nas,tss) = split_list spec
   2.148 +      val _ = check ctxt fixes (flat tss)
   2.149 +    in
   2.150 +      (flat tss, curry op ~~ nas o Library.unflat tss)
   2.151 +    end
   2.152 +
   2.153 +structure Preprocessor = GenericDataFun
   2.154 +(
   2.155 +  type T = preproc
   2.156 +  val empty = empty_preproc check_defs
   2.157 +  val extend = I
   2.158 +  fun merge _ (a, _) = a
   2.159 +);
   2.160 +
   2.161 +val get_preproc = Preprocessor.get o Context.Proof
   2.162 +val set_preproc = Preprocessor.map o K
   2.163 +
   2.164 +
   2.165 +
   2.166 +local 
   2.167 +  structure P = OuterParse and K = OuterKeyword 
   2.168 +
   2.169 +  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
   2.170 +                       
   2.171 +  val option_parser = (P.$$$ "sequential" >> K Sequential)
   2.172 +                   || ((P.reserved "default" |-- P.term) >> Default)
   2.173 +                   || (P.reserved "domintros" >> K DomIntros)
   2.174 +                   || (P.reserved "tailrec" >> K Tailrec)
   2.175 +                   || ((P.$$$ "in" |-- P.xname) >> Target)
   2.176 +
   2.177 +  fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
   2.178 +                              >> (fn opts => fold apply_opt opts default)
   2.179 +
   2.180 +  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
   2.181 +
   2.182 +  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
   2.183 +
   2.184 +  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
   2.185 +                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
   2.186 +
   2.187 +  val statements_ow = P.enum1 "|" statement_ow
   2.188 +
   2.189 +  val flags_statements = statements_ow
   2.190 +                         >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
   2.191 +
   2.192 +  fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
   2.193 +in
   2.194 +  fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
   2.195 +                                  
   2.196 +end
   2.197 +
   2.198 +
   2.199 +
   2.200 +
   2.201 +
   2.202 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
   2.203 +                                    target=NONE, domintros=false, tailrec=false }
   2.204  
   2.205  
   2.206  

     3.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Jun 02 15:26:32 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Sat Jun 02 15:28:38 2007 +0200
     3.3 @@ -14,45 +14,45 @@
     3.4      val setup : theory -> theory
     3.5  end
     3.6  
     3.7 -structure FundefDatatype : FUNDEF_DATATYPE =
     3.8 +structure FundefDatatype (*: FUNDEF_DATATYPE*) =
     3.9  struct
    3.10  
    3.11  open FundefLib
    3.12  open FundefCommon
    3.13  
    3.14 -fun check_constr_pattern thy err (Bound _) = ()
    3.15 -  | check_constr_pattern thy err t =
    3.16 -    let
    3.17 -      val (hd, args) = strip_comb t
    3.18 -    in
    3.19 -      (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of
    3.20 -           SOME _ => ()
    3.21 -         | NONE => err t)
    3.22 -        handle TERM ("dest_Const", _) => err t);
    3.23 -       map (check_constr_pattern thy err) args; 
    3.24 -       ())
    3.25 -    end
    3.26 -
    3.27  
    3.28  fun check_pats ctxt geq =
    3.29      let 
    3.30 -      fun err str = error (cat_lines ["Malformed \"fun\" definition:",
    3.31 -                                      str,
    3.32 +      fun err str = error (cat_lines ["Malformed definition:",
    3.33 +                                      str ^ " not allowed in sequential mode.",
    3.34                                        ProofContext.string_of_term ctxt geq])
    3.35        val thy = ProofContext.theory_of ctxt
    3.36 -
    3.37 +                
    3.38 +      fun check_constr_pattern (Bound _) = ()
    3.39 +        | check_constr_pattern t =
    3.40 +          let
    3.41 +            val (hd, args) = strip_comb t
    3.42 +          in
    3.43 +            (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of
    3.44 +                 SOME _ => ()
    3.45 +               | NONE => err "Non-constructor pattern")
    3.46 +              handle TERM ("dest_Const", _) => err "Non-constructor patterns");
    3.47 +             map check_constr_pattern args; 
    3.48 +             ())
    3.49 +          end
    3.50 +          
    3.51        val (fname, qs, gs, args, rhs) = split_def geq 
    3.52 -
    3.53 -      val _ = if not (null gs) then err "Conditional equations not allowed with \"fun\"" else ()
    3.54 -      val _ = map (check_constr_pattern thy (fn t => err "Not a constructor pattern")) args
    3.55 -
    3.56 +                                       
    3.57 +      val _ = if not (null gs) then err "Conditional equations" else ()
    3.58 +      val _ = map check_constr_pattern args
    3.59 +                  
    3.60                    (* just count occurrences to check linearity *)
    3.61        val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 < length qs
    3.62 -              then err "Nonlinear pattern" else ()
    3.63 +              then err "Nonlinear patterns" else ()
    3.64      in
    3.65        ()
    3.66      end
    3.67 -
    3.68 +    
    3.69  
    3.70  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    3.71  fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
    3.72 @@ -206,27 +206,83 @@
    3.73      FundefPackage.setup_termination_proof NONE
    3.74      #> Proof.global_terminal_proof (Method.Basic (LexicographicOrder.lexicographic_order []), NONE)
    3.75  
    3.76 +fun mk_catchall fixes arities =
    3.77 +    let
    3.78 +      fun mk_eqn ((fname, fT), _) =
    3.79 +          let 
    3.80 +            val n = the (Symtab.lookup arities fname)
    3.81 +            val (argTs, rT) = chop n (binder_types fT)
    3.82 +                                   |> apsnd (fn Ts => Ts ---> body_type fT) 
    3.83 +                              
    3.84 +            val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
    3.85 +          in
    3.86 +            HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    3.87 +                          Const ("HOL.undefined", rT))
    3.88 +              |> HOLogic.mk_Trueprop
    3.89 +              |> fold_rev mk_forall qs
    3.90 +          end
    3.91 +    in
    3.92 +      map mk_eqn fixes
    3.93 +    end
    3.94 +
    3.95 +fun add_catchall fixes spec =
    3.96 +    let 
    3.97 +      val catchalls = mk_catchall fixes (mk_arities (map split_def (map snd spec)))
    3.98 +    in
    3.99 +      spec @ map (pair true) catchalls
   3.100 +    end
   3.101 +
   3.102 +fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
   3.103 +    let
   3.104 +      val enabled = sequential orelse exists I flags
   3.105 +    in 
   3.106 +      if enabled then
   3.107 +        let
   3.108 +          val flags' = if sequential then map (K true) flags else flags
   3.109 +
   3.110 +          val (nas, eqss) = split_list spec
   3.111 +                            
   3.112 +          val eqs = map the_single eqss
   3.113 +                    
   3.114 +          val spliteqs = eqs
   3.115 +                           |> tap (check_defs ctxt fixes) (* Standard checks *)
   3.116 +                           |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
   3.117 +                           |> curry op ~~ flags'
   3.118 +                           |> add_catchall fixes   (* Completion: still disabled *)
   3.119 +                           |> FundefSplit.split_some_equations ctxt
   3.120 +
   3.121 +          fun restore_spec thms =
   3.122 +              nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
   3.123 +        in
   3.124 +          (flat spliteqs, restore_spec)
   3.125 +        end
   3.126 +      else
   3.127 +        FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
   3.128 +    end
   3.129 +
   3.130  val setup =
   3.131 -    Method.add_methods [("pat_completeness", Method.no_args pat_completeness,
   3.132 -      "Completeness prover for datatype patterns")]
   3.133 +    Method.add_methods [("pat_completeness", Method.no_args pat_completeness, 
   3.134 +                         "Completeness prover for datatype patterns")]
   3.135 +    #> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
   3.136  
   3.137  
   3.138 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", 
   3.139 +                                target=NONE, domintros=false, tailrec=false }
   3.140  
   3.141  
   3.142  local structure P = OuterParse and K = OuterKeyword in
   3.143  
   3.144 -fun fun_cmd config fixes statements lthy =
   3.145 +fun fun_cmd config fixes statements flags lthy =
   3.146      lthy
   3.147 -      |> FundefPackage.add_fundef fixes statements config
   3.148 +      |> FundefPackage.add_fundef fixes statements config flags
   3.149        |> by_pat_completeness_simp
   3.150        |> termination_by_lexicographic_order
   3.151  
   3.152 -
   3.153  val funP =
   3.154    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   3.155 -  (fundef_parser FundefCommon.fun_config
   3.156 -     >> (fn ((config, fixes), statements) =>
   3.157 -            (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements))));
   3.158 +  (fundef_parser fun_config
   3.159 +     >> (fn ((config, fixes), (flags, statements)) =>
   3.160 +            (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags))));
   3.161  
   3.162  val _ = OuterSyntax.add_parsers [funP];
   3.163  end

     4.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Jun 02 15:26:32 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Jun 02 15:28:38 2007 +0200
     4.3 @@ -10,12 +10,6 @@
     4.4  
     4.5  structure FundefLib = struct
     4.6  
     4.7 -(* ==> library/string *)
     4.8 -fun plural sg pl [x] = sg
     4.9 -  | plural sg pl _ = pl
    4.10 -
    4.11 -
    4.12 -
    4.13  fun map_option f NONE = NONE 
    4.14    | map_option f (SOME x) = SOME (f x);
    4.15  
    4.16 @@ -25,11 +19,6 @@
    4.17  fun fold_map_option f NONE y = (NONE, y)
    4.18    | fold_map_option f (SOME x) y = apfst SOME (f x y);
    4.19  
    4.20 -
    4.21 -
    4.22 -
    4.23 -
    4.24 -
    4.25  (* ??? *)
    4.26  fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
    4.27  

     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Jun 02 15:26:32 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Jun 02 15:28:38 2007 +0200
     5.3 @@ -10,14 +10,16 @@
     5.4  signature FUNDEF_PACKAGE =
     5.5  sig
     5.6      val add_fundef :  (string * string option * mixfix) list
     5.7 -                      -> ((bstring * Attrib.src list) * (string * bool)) list 
     5.8 +                      -> ((bstring * Attrib.src list) * string) list 
     5.9                        -> FundefCommon.fundef_config
    5.10 +                      -> bool list
    5.11                        -> local_theory
    5.12                        -> Proof.state
    5.13  
    5.14      val add_fundef_i:  (string * typ option * mixfix) list
    5.15 -                       -> ((bstring * Attrib.src list) * (term * bool)) list
    5.16 +                       -> ((bstring * Attrib.src list) * term) list
    5.17                         -> FundefCommon.fundef_config
    5.18 +                       -> bool list
    5.19                         -> local_theory
    5.20                         -> Proof.state
    5.21  
    5.22 @@ -32,7 +34,7 @@
    5.23  end
    5.24  
    5.25  
    5.26 -structure FundefPackage (*: FUNDEF_PACKAGE*) =
    5.27 +structure FundefPackage : FUNDEF_PACKAGE =
    5.28  struct
    5.29  
    5.30  open FundefLib
    5.31 @@ -42,80 +44,12 @@
    5.32  
    5.33  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
    5.34  
    5.35 -
    5.36 -(* Check for all sorts of errors in the input *)
    5.37 -fun check_def ctxt fixes eqs =
    5.38 -    let
    5.39 -      val fnames = map (fst o fst) fixes
    5.40 -                                
    5.41 -      fun check geq = 
    5.42 -          let
    5.43 -            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    5.44 -                                  
    5.45 -            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
    5.46 -                                 
    5.47 -            val _ = fname mem fnames 
    5.48 -                    orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
    5.49 -                                               ^ commas_quote fnames))
    5.50 -                                            
    5.51 -            fun add_bvs t is = add_loose_bnos (t, 0, is)
    5.52 -            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    5.53 -                        |> map (fst o nth (rev qs))
    5.54 -                      
    5.55 -            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    5.56 -                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    5.57 -                                    
    5.58 -            val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
    5.59 -                    error (input_error "Recursive Calls not allowed in premises")
    5.60 -          in
    5.61 -            fqgar
    5.62 -          end
    5.63 -    in
    5.64 -      (mk_arities (map check eqs); ())
    5.65 -      handle ArgumentCount fname => 
    5.66 -             error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    5.67 -    end
    5.68 -
    5.69 -
    5.70 -fun mk_catchall fixes arities =
    5.71 -    let
    5.72 -      fun mk_eqn ((fname, fT), _) =
    5.73 -          let 
    5.74 -            val n = the (Symtab.lookup arities fname)
    5.75 -            val (argTs, rT) = chop n (binder_types fT)
    5.76 -                                   |> apsnd (fn Ts => Ts ---> body_type fT) 
    5.77 -                              
    5.78 -            val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
    5.79 -          in
    5.80 -            HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    5.81 -                          Const ("HOL.undefined", rT))
    5.82 -              |> HOLogic.mk_Trueprop
    5.83 -              |> fold_rev mk_forall qs
    5.84 -          end
    5.85 -    in
    5.86 -      map mk_eqn fixes
    5.87 -    end
    5.88 -
    5.89 -fun add_catchall fixes spec =
    5.90 -    let 
    5.91 -      val catchalls = mk_catchall fixes (mk_arities (map split_def (map (snd o snd) spec)))
    5.92 -    in
    5.93 -      spec @ map (pair ("",[]) o pair true) catchalls
    5.94 -    end
    5.95 -
    5.96 -fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    5.97 -    let val (xs, ys) = split_list ps
    5.98 -    in xs ~~ f ys end
    5.99 -
   5.100 -fun restore_spec_structure reps spec =
   5.101 -    (burrow_snd o burrow o K) reps spec
   5.102 -
   5.103 -fun add_simps fixes spec sort label moreatts simps lthy =
   5.104 +fun add_simps fixes post sort label moreatts simps lthy =
   5.105      let
   5.106        val fnames = map (fst o fst) fixes
   5.107  
   5.108        val (saved_spec_simps, lthy) =
   5.109 -        fold_map note_theorem (restore_spec_structure simps spec) lthy
   5.110 +        fold_map note_theorem (post simps) lthy
   5.111        val saved_simps = flat (map snd saved_spec_simps)
   5.112  
   5.113        val simps_by_f = sort saved_simps
   5.114 @@ -129,13 +63,13 @@
   5.115         fold2 add_for_f fnames simps_by_f lthy)
   5.116      end
   5.117  
   5.118 -fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
   5.119 +fun fundef_afterqed config fixes post defname cont sort_cont [[proof]] lthy =
   5.120      let
   5.121        val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
   5.122            cont (Goal.close_result proof)
   5.123  
   5.124        val qualify = NameSpace.qualified defname
   5.125 -      val addsmps = add_simps fixes spec sort_cont
   5.126 +      val addsmps = add_simps fixes post sort_cont
   5.127  
   5.128        val (((psimps', pinducts'), (_, [termination'])), lthy) =
   5.129            lthy
   5.130 @@ -157,52 +91,36 @@
   5.131      end (* FIXME: Add cases for induct and cases thm *)
   5.132  
   5.133  
   5.134 +fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete when "read_specification" etc. is there *)
   5.135 +    let
   5.136 +      val eqns = map (apsnd single) eqnss
   5.137  
   5.138 -fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
   5.139 -    let
   5.140 -      val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags
   5.141 -      val eqns = map (apsnd (single o fst)) eqnss_flags
   5.142 +      val ((fixes, _), ctxt') = prep fixspec [] lthy             
   5.143 +      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
   5.144  
   5.145 -      val ((fixes, _), ctxt') = prep fixspec [] lthy
   5.146 -
   5.147 -      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
   5.148 -                         |> apsnd the_single
   5.149 -
   5.150 -      val raw_spec = map prep_eqn eqns
   5.151 -                     |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
   5.152 -
   5.153 -      val _ = check_def ctxt' fixes (map snd raw_spec)
   5.154 -
   5.155 -      val spec = raw_spec
   5.156 -                     |> burrow_snd (fn ts => flags ~~ ts)
   5.157 -                     (*|> (if global_flag then add_catchall fixes else I) *) (* Completion: still disabled *)
   5.158 -                     |> burrow_snd (FundefSplit.split_some_equations ctxt')
   5.159 -
   5.160 +      val spec = map prep_eqn eqns
   5.161 +                 |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *)
   5.162      in
   5.163        ((fixes, spec), ctxt')
   5.164      end
   5.165  
   5.166 -fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
   5.167 +fun gen_add_fundef prep fixspec eqnss config flags lthy =
   5.168      let
   5.169 -      val FundefConfig {sequential, ...} = config
   5.170 -
   5.171 -      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
   5.172 +      val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
   5.173 +      val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
   5.174  
   5.175        val defname = mk_defname fixes
   5.176  
   5.177 -      val t_eqns = spec |> map snd |> flat (* flatten external structure *)
   5.178 +      val ((goalstate, cont, sort_cont), lthy) =
   5.179 +          FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
   5.180  
   5.181 -      val ((goalstate, cont, sort_cont), lthy) =
   5.182 -          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns lthy
   5.183 -
   5.184 -      val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
   5.185 +      val afterqed = fundef_afterqed config fixes post defname cont sort_cont
   5.186      in
   5.187        lthy
   5.188          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
   5.189          |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   5.190      end
   5.191  
   5.192 -
   5.193  fun total_termination_afterqed data [[totality]] lthy =
   5.194      let
   5.195        val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data
   5.196 @@ -214,7 +132,6 @@
   5.197        val tsimps = map remove_domain_condition psimps
   5.198        val tinduct = map remove_domain_condition pinducts
   5.199  
   5.200 -        (* FIXME: How to generate code from (possibly) local contexts*)
   5.201        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
   5.202        val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))]
   5.203  
   5.204 @@ -293,8 +210,8 @@
   5.205  val functionP =
   5.206    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   5.207    (fundef_parser default_config
   5.208 -     >> (fn ((config, fixes), statements) =>
   5.209 -            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config)
   5.210 +     >> (fn ((config, fixes), (flags, statements)) =>
   5.211 +            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
   5.212              #> Toplevel.print));
   5.213  
   5.214  val terminationP =

     6.1 --- a/src/HOL/Tools/function_package/mutual.ML	Sat Jun 02 15:26:32 2007 +0200
     6.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Sat Jun 02 15:28:38 2007 +0200
     6.3 @@ -303,7 +303,7 @@
     6.4                                             
     6.5  fun sort_by_function (Mutual {fqgars, ...}) names xs =
     6.6      fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
     6.7 -             (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
     6.8 +             (map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs)      (* the name-thm pairs *)
     6.9               (map (rpair []) names)                (* in the empty buckets labeled with names *)
    6.10               
    6.11               |> map (snd #> map snd)                     (* and remove the labels afterwards *)