src/HOL/Tools/function_package/fundef_package.ML
changeset 23203 a5026e73cfcf
parent 23189 4574ab8f3b21
child 23473 997bca36d4fe
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Jun 02 15:26:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Jun 02 15:28:38 2007 +0200
     1.3 @@ -10,14 +10,16 @@
     1.4  signature FUNDEF_PACKAGE =
     1.5  sig
     1.6      val add_fundef :  (string * string option * mixfix) list
     1.7 -                      -> ((bstring * Attrib.src list) * (string * bool)) list 
     1.8 +                      -> ((bstring * Attrib.src list) * string) list 
     1.9                        -> FundefCommon.fundef_config
    1.10 +                      -> bool list
    1.11                        -> local_theory
    1.12                        -> Proof.state
    1.13  
    1.14      val add_fundef_i:  (string * typ option * mixfix) list
    1.15 -                       -> ((bstring * Attrib.src list) * (term * bool)) list
    1.16 +                       -> ((bstring * Attrib.src list) * term) list
    1.17                         -> FundefCommon.fundef_config
    1.18 +                       -> bool list
    1.19                         -> local_theory
    1.20                         -> Proof.state
    1.21  
    1.22 @@ -32,7 +34,7 @@
    1.23  end
    1.24  
    1.25  
    1.26 -structure FundefPackage (*: FUNDEF_PACKAGE*) =
    1.27 +structure FundefPackage : FUNDEF_PACKAGE =
    1.28  struct
    1.29  
    1.30  open FundefLib
    1.31 @@ -42,80 +44,12 @@
    1.32  
    1.33  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
    1.34  
    1.35 -
    1.36 -(* Check for all sorts of errors in the input *)
    1.37 -fun check_def ctxt fixes eqs =
    1.38 -    let
    1.39 -      val fnames = map (fst o fst) fixes
    1.40 -                                
    1.41 -      fun check geq = 
    1.42 -          let
    1.43 -            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
    1.44 -                                  
    1.45 -            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
    1.46 -                                 
    1.47 -            val _ = fname mem fnames 
    1.48 -                    orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
    1.49 -                                               ^ commas_quote fnames))
    1.50 -                                            
    1.51 -            fun add_bvs t is = add_loose_bnos (t, 0, is)
    1.52 -            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    1.53 -                        |> map (fst o nth (rev qs))
    1.54 -                      
    1.55 -            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    1.56 -                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    1.57 -                                    
    1.58 -            val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse
    1.59 -                    error (input_error "Recursive Calls not allowed in premises")
    1.60 -          in
    1.61 -            fqgar
    1.62 -          end
    1.63 -    in
    1.64 -      (mk_arities (map check eqs); ())
    1.65 -      handle ArgumentCount fname => 
    1.66 -             error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    1.67 -    end
    1.68 -
    1.69 -
    1.70 -fun mk_catchall fixes arities =
    1.71 -    let
    1.72 -      fun mk_eqn ((fname, fT), _) =
    1.73 -          let 
    1.74 -            val n = the (Symtab.lookup arities fname)
    1.75 -            val (argTs, rT) = chop n (binder_types fT)
    1.76 -                                   |> apsnd (fn Ts => Ts ---> body_type fT) 
    1.77 -                              
    1.78 -            val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
    1.79 -          in
    1.80 -            HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    1.81 -                          Const ("HOL.undefined", rT))
    1.82 -              |> HOLogic.mk_Trueprop
    1.83 -              |> fold_rev mk_forall qs
    1.84 -          end
    1.85 -    in
    1.86 -      map mk_eqn fixes
    1.87 -    end
    1.88 -
    1.89 -fun add_catchall fixes spec =
    1.90 -    let 
    1.91 -      val catchalls = mk_catchall fixes (mk_arities (map split_def (map (snd o snd) spec)))
    1.92 -    in
    1.93 -      spec @ map (pair ("",[]) o pair true) catchalls
    1.94 -    end
    1.95 -
    1.96 -fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.97 -    let val (xs, ys) = split_list ps
    1.98 -    in xs ~~ f ys end
    1.99 -
   1.100 -fun restore_spec_structure reps spec =
   1.101 -    (burrow_snd o burrow o K) reps spec
   1.102 -
   1.103 -fun add_simps fixes spec sort label moreatts simps lthy =
   1.104 +fun add_simps fixes post sort label moreatts simps lthy =
   1.105      let
   1.106        val fnames = map (fst o fst) fixes
   1.107  
   1.108        val (saved_spec_simps, lthy) =
   1.109 -        fold_map note_theorem (restore_spec_structure simps spec) lthy
   1.110 +        fold_map note_theorem (post simps) lthy
   1.111        val saved_simps = flat (map snd saved_spec_simps)
   1.112  
   1.113        val simps_by_f = sort saved_simps
   1.114 @@ -129,13 +63,13 @@
   1.115         fold2 add_for_f fnames simps_by_f lthy)
   1.116      end
   1.117  
   1.118 -fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
   1.119 +fun fundef_afterqed config fixes post defname cont sort_cont [[proof]] lthy =
   1.120      let
   1.121        val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
   1.122            cont (Goal.close_result proof)
   1.123  
   1.124        val qualify = NameSpace.qualified defname
   1.125 -      val addsmps = add_simps fixes spec sort_cont
   1.126 +      val addsmps = add_simps fixes post sort_cont
   1.127  
   1.128        val (((psimps', pinducts'), (_, [termination'])), lthy) =
   1.129            lthy
   1.130 @@ -157,52 +91,36 @@
   1.131      end (* FIXME: Add cases for induct and cases thm *)
   1.132  
   1.133  
   1.134 -
   1.135 -fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
   1.136 +fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete when "read_specification" etc. is there *)
   1.137      let
   1.138 -      val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags
   1.139 -      val eqns = map (apsnd (single o fst)) eqnss_flags
   1.140 -
   1.141 -      val ((fixes, _), ctxt') = prep fixspec [] lthy
   1.142 -
   1.143 -      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
   1.144 -                         |> apsnd the_single
   1.145 +      val eqns = map (apsnd single) eqnss
   1.146  
   1.147 -      val raw_spec = map prep_eqn eqns
   1.148 -                     |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
   1.149 -
   1.150 -      val _ = check_def ctxt' fixes (map snd raw_spec)
   1.151 +      val ((fixes, _), ctxt') = prep fixspec [] lthy             
   1.152 +      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
   1.153  
   1.154 -      val spec = raw_spec
   1.155 -                     |> burrow_snd (fn ts => flags ~~ ts)
   1.156 -                     (*|> (if global_flag then add_catchall fixes else I) *) (* Completion: still disabled *)
   1.157 -                     |> burrow_snd (FundefSplit.split_some_equations ctxt')
   1.158 -
   1.159 +      val spec = map prep_eqn eqns
   1.160 +                 |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *)
   1.161      in
   1.162        ((fixes, spec), ctxt')
   1.163      end
   1.164  
   1.165 -fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
   1.166 +fun gen_add_fundef prep fixspec eqnss config flags lthy =
   1.167      let
   1.168 -      val FundefConfig {sequential, ...} = config
   1.169 -
   1.170 -      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
   1.171 +      val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
   1.172 +      val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
   1.173  
   1.174        val defname = mk_defname fixes
   1.175  
   1.176 -      val t_eqns = spec |> map snd |> flat (* flatten external structure *)
   1.177 +      val ((goalstate, cont, sort_cont), lthy) =
   1.178 +          FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
   1.179  
   1.180 -      val ((goalstate, cont, sort_cont), lthy) =
   1.181 -          FundefMutual.prepare_fundef_mutual config defname fixes t_eqns lthy
   1.182 -
   1.183 -      val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
   1.184 +      val afterqed = fundef_afterqed config fixes post defname cont sort_cont
   1.185      in
   1.186        lthy
   1.187          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
   1.188          |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   1.189      end
   1.190  
   1.191 -
   1.192  fun total_termination_afterqed data [[totality]] lthy =
   1.193      let
   1.194        val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data
   1.195 @@ -214,7 +132,6 @@
   1.196        val tsimps = map remove_domain_condition psimps
   1.197        val tinduct = map remove_domain_condition pinducts
   1.198  
   1.199 -        (* FIXME: How to generate code from (possibly) local contexts*)
   1.200        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
   1.201        val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))]
   1.202  
   1.203 @@ -293,8 +210,8 @@
   1.204  val functionP =
   1.205    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.206    (fundef_parser default_config
   1.207 -     >> (fn ((config, fixes), statements) =>
   1.208 -            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config)
   1.209 +     >> (fn ((config, fixes), (flags, statements)) =>
   1.210 +            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags)
   1.211              #> Toplevel.print));
   1.212  
   1.213  val terminationP =