src/HOL/Tools/function_package/fundef_package.ML
changeset 23189 4574ab8f3b21
parent 22846 fb79144af9a3
child 23203 a5026e73cfcf
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Jun 01 15:20:53 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Jun 01 15:57:45 2007 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -structure FundefPackage : FUNDEF_PACKAGE =
     1.8 +structure FundefPackage (*: FUNDEF_PACKAGE*) =
     1.9  struct
    1.10  
    1.11  open FundefLib
    1.12 @@ -42,6 +42,67 @@
    1.13  
    1.14  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
    1.15  
    1.16 +
    1.17 +(* Check for all sorts of errors in the input *)
    1.18 +fun check_def ctxt fixes eqs =
    1.19 +    let
    1.20 +      val fnames = map (fst o fst) fixes
    1.21 +                                
    1.22 +      fun check geq = 
    1.23 +          let
    1.24 +            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    1.25 +                                  
    1.26 +            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
    1.27 +                                 
    1.28 +            val _ = fname mem fnames 
    1.29 +                    orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
    1.30 +                                               ^ commas_quote fnames))
    1.31 +                                            
    1.32 +            fun add_bvs t is = add_loose_bnos (t, 0, is)
    1.33 +            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    1.34 +                        |> map (fst o nth (rev qs))
    1.35 +                      
    1.36 +            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    1.37 +                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    1.38 +                                    
    1.39 +            val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
    1.40 +                    error (input_error "Recursive Calls not allowed in premises")
    1.41 +          in
    1.42 +            fqgar
    1.43 +          end
    1.44 +    in
    1.45 +      (mk_arities (map check eqs); ())
    1.46 +      handle ArgumentCount fname => 
    1.47 +             error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    1.48 +    end
    1.49 +
    1.50 +
    1.51 +fun mk_catchall fixes arities =
    1.52 +    let
    1.53 +      fun mk_eqn ((fname, fT), _) =
    1.54 +          let 
    1.55 +            val n = the (Symtab.lookup arities fname)
    1.56 +            val (argTs, rT) = chop n (binder_types fT)
    1.57 +                                   |> apsnd (fn Ts => Ts ---> body_type fT) 
    1.58 +                              
    1.59 +            val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
    1.60 +          in
    1.61 +            HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    1.62 +                          Const ("HOL.undefined", rT))
    1.63 +              |> HOLogic.mk_Trueprop
    1.64 +              |> fold_rev mk_forall qs
    1.65 +          end
    1.66 +    in
    1.67 +      map mk_eqn fixes
    1.68 +    end
    1.69 +
    1.70 +fun add_catchall fixes spec =
    1.71 +    let 
    1.72 +      val catchalls = mk_catchall fixes (mk_arities (map split_def (map (snd o snd) spec)))
    1.73 +    in
    1.74 +      spec @ map (pair ("",[]) o pair true) catchalls
    1.75 +    end
    1.76 +
    1.77  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.78      let val (xs, ys) = split_list ps
    1.79      in xs ~~ f ys end
    1.80 @@ -107,16 +168,23 @@
    1.81        fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
    1.82                           |> apsnd the_single
    1.83  
    1.84 -      val spec = map prep_eqn eqns
    1.85 +      val raw_spec = map prep_eqn eqns
    1.86                       |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
    1.87 -                     |> burrow_snd (fn ts => FundefSplit.split_some_equations ctxt' (flags ~~ ts))
    1.88 +
    1.89 +      val _ = check_def ctxt' fixes (map snd raw_spec)
    1.90 +
    1.91 +      val spec = raw_spec
    1.92 +                     |> burrow_snd (fn ts => flags ~~ ts)
    1.93 +                     (*|> (if global_flag then add_catchall fixes else I) *) (* Completion: still disabled *)
    1.94 +                     |> burrow_snd (FundefSplit.split_some_equations ctxt')
    1.95 +
    1.96      in
    1.97        ((fixes, spec), ctxt')
    1.98      end
    1.99  
   1.100  fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
   1.101      let
   1.102 -      val FundefConfig {sequential, default, tailrec, ...} = config
   1.103 +      val FundefConfig {sequential, ...} = config
   1.104  
   1.105        val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
   1.106  
   1.107 @@ -125,7 +193,7 @@
   1.108        val t_eqns = spec |> map snd |> flat (* flatten external structure *)
   1.109  
   1.110        val ((goalstate, cont, sort_cont), lthy) =
   1.111 -          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
   1.112 +          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns lthy
   1.113  
   1.114        val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
   1.115      in