simplified interfaces, some restructuring
authorkrauss
Fri Jun 01 15:57:45 2007 +0200 (2007-06-01)
changeset 231894574ab8f3b21
parent 23188 595a0e24bd8e
child 23190 d45c4d6c5f15
simplified interfaces, some restructuring
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Jun 01 15:20:53 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Jun 01 15:57:45 2007 +0200
     1.3 @@ -224,6 +224,51 @@
     1.4    fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
     1.5  end
     1.6  
     1.7 +
     1.8 +
     1.9 +(* Common operations on equations *)
    1.10 +
    1.11 +fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
    1.12 +  | open_all_all t = ([], t)
    1.13 +
    1.14 +exception MalformedEquation of term
    1.15 +
    1.16 +fun split_def geq =
    1.17 +    let
    1.18 +      val (qs, imp) = open_all_all geq
    1.19 +
    1.20 +      val gs = Logic.strip_imp_prems imp
    1.21 +      val eq = Logic.strip_imp_concl imp
    1.22 +
    1.23 +      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    1.24 +          handle TERM _ => raise MalformedEquation geq
    1.25 +
    1.26 +      val (head, args) = strip_comb f_args
    1.27 +
    1.28 +      val fname = fst (dest_Free head)
    1.29 +          handle TERM _ => raise MalformedEquation geq
    1.30 +    in
    1.31 +      (fname, qs, gs, args, rhs)
    1.32 +    end
    1.33 +
    1.34 +exception ArgumentCount of string
    1.35 +
    1.36 +fun mk_arities fqgars =
    1.37 +    let fun f (fname, _, _, args, _) arities =
    1.38 +            let val k = length args
    1.39 +            in
    1.40 +              case Symtab.lookup arities fname of
    1.41 +                NONE => Symtab.update (fname, k) arities
    1.42 +              | SOME i => (if i = k then arities else raise ArgumentCount fname)
    1.43 +            end
    1.44 +    in
    1.45 +      fold f fqgars Symtab.empty
    1.46 +    end
    1.47 +
    1.48 +
    1.49 +
    1.50 +
    1.51 +
    1.52  end
    1.53  
    1.54  (* Common Abbreviations *)
     2.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Jun 01 15:20:53 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Jun 01 15:57:45 2007 +0200
     2.3 @@ -10,9 +10,8 @@
     2.4  sig
     2.5      val prepare_fundef : FundefCommon.fundef_config
     2.6                           -> string (* defname *)
     2.7 -                         -> (string * typ * mixfix) (* defined symbol *)
     2.8 +                         -> ((string * typ) * mixfix) list (* defined symbol *)
     2.9                           -> ((string * typ) list * term list * term * term) list (* specification *)
    2.10 -                         -> string (* default_value, not parsed yet *)
    2.11                           -> local_theory
    2.12  
    2.13                           -> (term   (* f *)
    2.14 @@ -858,9 +857,9 @@
    2.15      end
    2.16  
    2.17  
    2.18 -fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
    2.19 +fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
    2.20      let
    2.21 -      val FundefConfig {domintros, tailrec, ...} = config 
    2.22 +      val FundefConfig {domintros, tailrec, default=default_str, ...} = config 
    2.23                                                           
    2.24        val fvar = Free (fname, fT)
    2.25        val domT = domain_type fT
     3.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jun 01 15:20:53 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Jun 01 15:57:45 2007 +0200
     3.3 @@ -20,6 +20,40 @@
     3.4  open FundefLib
     3.5  open FundefCommon
     3.6  
     3.7 +fun check_constr_pattern thy err (Bound _) = ()
     3.8 +  | check_constr_pattern thy err t =
     3.9 +    let
    3.10 +      val (hd, args) = strip_comb t
    3.11 +    in
    3.12 +      (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of
    3.13 +           SOME _ => ()
    3.14 +         | NONE => err t)
    3.15 +        handle TERM ("dest_Const", _) => err t);
    3.16 +       map (check_constr_pattern thy err) args; 
    3.17 +       ())
    3.18 +    end
    3.19 +
    3.20 +
    3.21 +fun check_pats ctxt geq =
    3.22 +    let 
    3.23 +      fun err str = error (cat_lines ["Malformed \"fun\" definition:",
    3.24 +                                      str,
    3.25 +                                      ProofContext.string_of_term ctxt geq])
    3.26 +      val thy = ProofContext.theory_of ctxt
    3.27 +
    3.28 +      val (fname, qs, gs, args, rhs) = split_def geq 
    3.29 +
    3.30 +      val _ = if not (null gs) then err "Conditional equations not allowed with \"fun\"" else ()
    3.31 +      val _ = map (check_constr_pattern thy (fn t => err "Not a constructor pattern")) args
    3.32 +
    3.33 +                  (* just count occurrences to check linearity *)
    3.34 +      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 < length qs
    3.35 +              then err "Nonlinear pattern" else ()
    3.36 +    in
    3.37 +      ()
    3.38 +    end
    3.39 +
    3.40 +
    3.41  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    3.42  fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
    3.43  
     4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Jun 01 15:20:53 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Jun 01 15:57:45 2007 +0200
     4.3 @@ -32,7 +32,7 @@
     4.4  end
     4.5  
     4.6  
     4.7 -structure FundefPackage : FUNDEF_PACKAGE =
     4.8 +structure FundefPackage (*: FUNDEF_PACKAGE*) =
     4.9  struct
    4.10  
    4.11  open FundefLib
    4.12 @@ -42,6 +42,67 @@
    4.13  
    4.14  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
    4.15  
    4.16 +
    4.17 +(* Check for all sorts of errors in the input *)
    4.18 +fun check_def ctxt fixes eqs =
    4.19 +    let
    4.20 +      val fnames = map (fst o fst) fixes
    4.21 +                                
    4.22 +      fun check geq = 
    4.23 +          let
    4.24 +            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    4.25 +                                  
    4.26 +            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
    4.27 +                                 
    4.28 +            val _ = fname mem fnames 
    4.29 +                    orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
    4.30 +                                               ^ commas_quote fnames))
    4.31 +                                            
    4.32 +            fun add_bvs t is = add_loose_bnos (t, 0, is)
    4.33 +            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    4.34 +                        |> map (fst o nth (rev qs))
    4.35 +                      
    4.36 +            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    4.37 +                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    4.38 +                                    
    4.39 +            val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
    4.40 +                    error (input_error "Recursive Calls not allowed in premises")
    4.41 +          in
    4.42 +            fqgar
    4.43 +          end
    4.44 +    in
    4.45 +      (mk_arities (map check eqs); ())
    4.46 +      handle ArgumentCount fname => 
    4.47 +             error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    4.48 +    end
    4.49 +
    4.50 +
    4.51 +fun mk_catchall fixes arities =
    4.52 +    let
    4.53 +      fun mk_eqn ((fname, fT), _) =
    4.54 +          let 
    4.55 +            val n = the (Symtab.lookup arities fname)
    4.56 +            val (argTs, rT) = chop n (binder_types fT)
    4.57 +                                   |> apsnd (fn Ts => Ts ---> body_type fT) 
    4.58 +                              
    4.59 +            val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
    4.60 +          in
    4.61 +            HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    4.62 +                          Const ("HOL.undefined", rT))
    4.63 +              |> HOLogic.mk_Trueprop
    4.64 +              |> fold_rev mk_forall qs
    4.65 +          end
    4.66 +    in
    4.67 +      map mk_eqn fixes
    4.68 +    end
    4.69 +
    4.70 +fun add_catchall fixes spec =
    4.71 +    let 
    4.72 +      val catchalls = mk_catchall fixes (mk_arities (map split_def (map (snd o snd) spec)))
    4.73 +    in
    4.74 +      spec @ map (pair ("",[]) o pair true) catchalls
    4.75 +    end
    4.76 +
    4.77  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    4.78      let val (xs, ys) = split_list ps
    4.79      in xs ~~ f ys end
    4.80 @@ -107,16 +168,23 @@
    4.81        fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
    4.82                           |> apsnd the_single
    4.83  
    4.84 -      val spec = map prep_eqn eqns
    4.85 +      val raw_spec = map prep_eqn eqns
    4.86                       |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
    4.87 -                     |> burrow_snd (fn ts => FundefSplit.split_some_equations ctxt' (flags ~~ ts))
    4.88 +
    4.89 +      val _ = check_def ctxt' fixes (map snd raw_spec)
    4.90 +
    4.91 +      val spec = raw_spec
    4.92 +                     |> burrow_snd (fn ts => flags ~~ ts)
    4.93 +                     (*|> (if global_flag then add_catchall fixes else I) *) (* Completion: still disabled *)
    4.94 +                     |> burrow_snd (FundefSplit.split_some_equations ctxt')
    4.95 +
    4.96      in
    4.97        ((fixes, spec), ctxt')
    4.98      end
    4.99  
   4.100  fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
   4.101      let
   4.102 -      val FundefConfig {sequential, default, tailrec, ...} = config
   4.103 +      val FundefConfig {sequential, ...} = config
   4.104  
   4.105        val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
   4.106  
   4.107 @@ -125,7 +193,7 @@
   4.108        val t_eqns = spec |> map snd |> flat (* flatten external structure *)
   4.109  
   4.110        val ((goalstate, cont, sort_cont), lthy) =
   4.111 -          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
   4.112 +          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns lthy
   4.113  
   4.114        val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
   4.115      in
     5.1 --- a/src/HOL/Tools/function_package/mutual.ML	Fri Jun 01 15:20:53 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Fri Jun 01 15:57:45 2007 +0200
     5.3 @@ -13,7 +13,6 @@
     5.4                                -> string (* defname *)
     5.5                                -> ((string * typ) * mixfix) list
     5.6                                -> term list
     5.7 -                              -> string (* default, unparsed term *)
     5.8                                -> local_theory
     5.9                                -> ((thm (* goalstate *)
    5.10                                     * (thm -> FundefCommon.fundef_result) (* proof continuation *)
    5.11 @@ -72,50 +71,6 @@
    5.12      if n < 5 then fst (chop n ["P","Q","R","S"])
    5.13      else map (fn i => "P" ^ string_of_int i) (1 upto n)
    5.14  
    5.15 -
    5.16 -fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
    5.17 -  | open_all_all t = ([], t)
    5.18 -
    5.19 -(* Builds a curried clause description in abstracted form *)
    5.20 -fun split_def ctxt fnames geq arities =
    5.21 -    let
    5.22 -      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    5.23 -                            
    5.24 -      val (qs, imp) = open_all_all geq
    5.25 -
    5.26 -      val gs = Logic.strip_imp_prems imp
    5.27 -      val eq = Logic.strip_imp_concl imp
    5.28 -
    5.29 -      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    5.30 -      val (head, args) = strip_comb f_args
    5.31 -
    5.32 -      val invalid_head_msg = "Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames
    5.33 -      val fname = fst (dest_Free head)
    5.34 -          handle TERM _ => error (input_error invalid_head_msg)
    5.35 -
    5.36 -      val _ = fname mem fnames orelse error (input_error invalid_head_msg)
    5.37 -
    5.38 -      fun add_bvs t is = add_loose_bnos (t, 0, is)
    5.39 -      val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    5.40 -                  |> map (fst o nth (rev qs))
    5.41 -                
    5.42 -      val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    5.43 -                                              ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    5.44 -
    5.45 -      val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
    5.46 -                     error (input_error "Recursive Calls not allowed in premises")
    5.47 -
    5.48 -      val k = length args
    5.49 -
    5.50 -      val arities' = case Symtab.lookup arities fname of
    5.51 -                       NONE => Symtab.update (fname, k) arities
    5.52 -                     | SOME i => (i = k orelse
    5.53 -                                  error (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations"));
    5.54 -                                  arities)
    5.55 -    in
    5.56 -      ((fname, qs, gs, args, rhs), arities')
    5.57 -    end
    5.58 -    
    5.59  fun get_part fname =
    5.60      the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
    5.61                       
    5.62 @@ -133,7 +88,8 @@
    5.63  fun analyze_eqs ctxt defname fs eqs =
    5.64      let
    5.65          val fnames = map fst fs
    5.66 -        val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty
    5.67 +        val fqgars = map split_def eqs
    5.68 +        val arities = mk_arities fqgars
    5.69  
    5.70          fun curried_types (fname, fT) =
    5.71              let
    5.72 @@ -325,15 +281,17 @@
    5.73        fun mk_mpsimp fqgar sum_psimp =
    5.74            in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
    5.75            
    5.76 +      val rew_ss = HOL_basic_ss addsimps all_f_defs
    5.77        val mpsimps = map2 mk_mpsimp fqgars psimps
    5.78        val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
    5.79        val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
    5.80 -      val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
    5.81 +      val mtermination = full_simplify rew_ss termination
    5.82 +      val mdomintros = map_option (map (full_simplify rew_ss)) domintros
    5.83      in
    5.84        FundefResult { fs=fs, G=G, R=R,
    5.85                       psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
    5.86                       cases=cases, termination=mtermination,
    5.87 -                     domintros=domintros,
    5.88 +                     domintros=mdomintros,
    5.89                       trsimps=mtrsimps}
    5.90      end
    5.91        
    5.92 @@ -351,13 +309,13 @@
    5.93               |> map (snd #> map snd)                     (* and remove the labels afterwards *)
    5.94  
    5.95  
    5.96 -fun prepare_fundef_mutual config defname fixes eqss default lthy =
    5.97 +fun prepare_fundef_mutual config defname fixes eqss lthy =
    5.98      let
    5.99        val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
   5.100        val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
   5.101            
   5.102        val ((fsum, goalstate, cont), lthy') =
   5.103 -          FundefCore.prepare_fundef config defname (n, T, NoSyn) qglrs default lthy
   5.104 +          FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy
   5.105            
   5.106        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
   5.107