made function syntax strict, requiring | to separate equations; cleanup
authorkrauss
Thu Mar 22 13:36:57 2007 +0100 (2007-03-22)
changeset 2249862cdd4b3e96b
parent 22497 1fe951654cee
child 22499 68c8a8390e16
made function syntax strict, requiring | to separate equations; cleanup
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 22 13:36:56 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 22 13:36:57 2007 +0100
     1.3 @@ -9,27 +9,23 @@
     1.4  structure FundefCommon =
     1.5  struct
     1.6  
     1.7 -(* Theory Dependencies *)
     1.8 -val acc_const_name = "Accessible_Part.acc"
     1.9 -
    1.10 +(* Profiling *)
    1.11  val profile = ref false;
    1.12  
    1.13  fun PROFILE msg = if !profile then timeap_msg msg else I
    1.14  
    1.15 +
    1.16 +val acc_const_name = "Accessible_Part.acc"
    1.17  fun mk_acc domT R =
    1.18      Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
    1.19  
    1.20 -(* FIXME, unused *)
    1.21  val function_name = suffix "C"
    1.22  val graph_name = suffix "_graph"
    1.23  val rel_name = suffix "_rel"
    1.24  val dom_name = suffix "_dom"
    1.25  
    1.26 -val dest_rel_name = unsuffix "_rel"
    1.27 -
    1.28  type depgraph = int IntGraph.T
    1.29  
    1.30 -
    1.31  datatype ctx_tree 
    1.32    = Leaf of term
    1.33    | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
    1.34 @@ -160,30 +156,38 @@
    1.35    | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
    1.36      FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } 
    1.37  
    1.38 +fun target_of (FundefConfig {target, ...}) = target
    1.39  
    1.40 -local structure P = OuterParse and K = OuterKeyword in
    1.41 -
    1.42 -val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    1.43 +local 
    1.44 +  structure P = OuterParse and K = OuterKeyword 
    1.45  
    1.46 -val option_parser = (P.$$$ "sequential" >> K Sequential)
    1.47 -               || ((P.reserved "default" |-- P.term) >> Default)
    1.48 -               || (P.reserved "domintros" >> K DomIntros)
    1.49 -               || (P.reserved "tailrec" >> K Tailrec)
    1.50 -               || ((P.$$$ "in" |-- P.xname) >> Target)
    1.51 +  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    1.52 +                       
    1.53 +  val option_parser = (P.$$$ "sequential" >> K Sequential)
    1.54 +                   || ((P.reserved "default" |-- P.term) >> Default)
    1.55 +                   || (P.reserved "domintros" >> K DomIntros)
    1.56 +                   || (P.reserved "tailrec" >> K Tailrec)
    1.57 +                   || ((P.$$$ "in" |-- P.xname) >> Target)
    1.58  
    1.59 -fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
    1.60 +  fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
    1.61                            >> (fn opts => fold apply_opt opts def)
    1.62  
    1.63 +  fun pipe_list1 s = P.enum1 "|" s
    1.64 +
    1.65 +  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    1.66 +
    1.67 +  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
    1.68 +
    1.69 +  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
    1.70 +                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
    1.71 +
    1.72 +  val statements_ow = pipe_list1 statement_ow
    1.73 +in
    1.74 +  fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
    1.75  end
    1.76  
    1.77 -
    1.78 -
    1.79 -
    1.80 -
    1.81  end
    1.82  
    1.83 -
    1.84 -
    1.85  (* Common Abbreviations *)
    1.86  
    1.87  structure FundefAbbrev =
    1.88 @@ -191,32 +195,13 @@
    1.89  
    1.90  fun implies_elim_swp x y = implies_elim y x
    1.91  
    1.92 -(* Some HOL things frequently used *)
    1.93 +(* HOL abbreviations *)
    1.94  val boolT = HOLogic.boolT
    1.95  val mk_prod = HOLogic.mk_prod
    1.96 -val mk_mem = HOLogic.mk_mem
    1.97  val mk_eq = HOLogic.mk_eq
    1.98  val eq_const = HOLogic.eq_const
    1.99  val Trueprop = HOLogic.mk_Trueprop
   1.100 -
   1.101  val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
   1.102 -fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))
   1.103 -
   1.104 -fun mk_subset T A B = 
   1.105 -    let val sT = HOLogic.mk_setT T
   1.106 -    in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end
   1.107 -
   1.108 -
   1.109 -(* with explicit types: Needed with loose bounds *)
   1.110 -fun mk_relmemT xT yT (x,y) R = 
   1.111 -    let 
   1.112 -  val pT = HOLogic.mk_prodT (xT, yT)
   1.113 -  val RT = HOLogic.mk_setT pT
   1.114 -    in
   1.115 -  Const ("op :", [pT, RT] ---> boolT)
   1.116 -        $ (HOLogic.pair_const xT yT $ x $ y)
   1.117 -        $ R
   1.118 -    end
   1.119  
   1.120  fun free_to_var (Free (v,T)) = Var ((v,0),T)
   1.121    | free_to_var _ = raise Match
     2.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Mar 22 13:36:56 2007 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Mar 22 13:36:57 2007 +0100
     2.3 @@ -181,25 +181,18 @@
     2.4  
     2.5  local structure P = OuterParse and K = OuterKeyword in
     2.6  
     2.7 -
     2.8 -fun or_list1 s = P.enum1 "|" s
     2.9 -val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    2.10 -val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
    2.11 -val statements_ow = or_list1 statement_ow
    2.12 -
    2.13 -
    2.14 -fun fun_cmd fixes statements lthy =
    2.15 +fun fun_cmd config fixes statements lthy =
    2.16      lthy
    2.17 -      |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
    2.18 +      |> FundefPackage.add_fundef fixes statements config
    2.19        ||> by_pat_completeness_simp
    2.20        |-> termination_by_lexicographic_order
    2.21  
    2.22  
    2.23  val funP =
    2.24    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
    2.25 -  ((P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    2.26 -     >> (fn ((target, fixes), statements) =>
    2.27 -            (Toplevel.local_theory target (fun_cmd fixes statements))));
    2.28 +  (fundef_parser FundefCommon.fun_config
    2.29 +     >> (fn ((config, fixes), statements) =>
    2.30 +            (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements))));
    2.31  
    2.32  val _ = OuterSyntax.add_parsers [funP];
    2.33  end
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 22 13:36:56 2007 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 22 13:36:57 2007 +0100
     3.3 @@ -10,13 +10,13 @@
     3.4  signature FUNDEF_PACKAGE =
     3.5  sig
     3.6      val add_fundef :  (string * string option * mixfix) list
     3.7 -                      -> ((bstring * Attrib.src list) * (string * bool) list) list list
     3.8 +                      -> ((bstring * Attrib.src list) * (string * bool)) list 
     3.9                        -> FundefCommon.fundef_config
    3.10                        -> local_theory
    3.11                        -> string * Proof.state
    3.12  
    3.13      val add_fundef_i:  (string * typ option * mixfix) list
    3.14 -                       -> ((bstring * Attrib.src list) * (term * bool) list) list list
    3.15 +                       -> ((bstring * Attrib.src list) * (term * bool)) list
    3.16                         -> FundefCommon.fundef_config
    3.17                         -> local_theory
    3.18                         -> string * Proof.state
    3.19 @@ -47,15 +47,15 @@
    3.20      in xs ~~ f ys end
    3.21  
    3.22  fun restore_spec_structure reps spec =
    3.23 -    (burrow o burrow_snd o burrow o K) reps spec
    3.24 +    (burrow_snd o burrow o K) reps spec
    3.25  
    3.26  fun add_simps fixes spec sort label moreatts simps lthy =
    3.27      let
    3.28        val fnames = map (fst o fst) fixes
    3.29  
    3.30        val (saved_spec_simps, lthy) =
    3.31 -        fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy
    3.32 -      val saved_simps = flat (map snd (flat saved_spec_simps))
    3.33 +        fold_map note_theorem (restore_spec_structure simps spec) lthy
    3.34 +      val saved_simps = flat (map snd saved_spec_simps)
    3.35  
    3.36        val simps_by_f = sort saved_simps
    3.37  
    3.38 @@ -99,21 +99,21 @@
    3.39  
    3.40  fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
    3.41      let
    3.42 -      val eqnss = map (map (apsnd (map fst))) eqnss_flags
    3.43 -      val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags
    3.44 +      val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags
    3.45 +      val eqns = map (apsnd (single o fst)) eqnss_flags
    3.46  
    3.47        val ((fixes, _), ctxt') = prep fixspec [] lthy
    3.48 -      val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
    3.49 -                     |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
    3.50 -                     |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
    3.51 -                     |> (burrow o burrow_snd o burrow)
    3.52 -                          (FundefSplit.split_some_equations lthy)
    3.53 -                     |> map (map (apsnd flat))
    3.54 +
    3.55 +      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
    3.56 +                         |> apsnd the_single
    3.57 +
    3.58 +      val spec = map prep_eqn eqns
    3.59 +                     |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *)
    3.60 +                     |> burrow_snd (fn ts => FundefSplit.split_some_equations ctxt' (flags ~~ ts))
    3.61      in
    3.62        ((fixes, spec), ctxt')
    3.63      end
    3.64  
    3.65 -
    3.66  fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
    3.67      let
    3.68        val FundefConfig {sequential, default, tailrec, ...} = config
    3.69 @@ -122,8 +122,7 @@
    3.70  
    3.71        val defname = mk_defname fixes
    3.72  
    3.73 -      val t_eqns = spec
    3.74 -                     |> flat |> map snd |> flat (* flatten external structure *)
    3.75 +      val t_eqns = spec |> map snd |> flat (* flatten external structure *)
    3.76  
    3.77        val ((goalstate, cont, sort_cont), lthy) =
    3.78            FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy
    3.79 @@ -225,26 +224,13 @@
    3.80  
    3.81  local structure P = OuterParse and K = OuterKeyword in
    3.82  
    3.83 -
    3.84 -
    3.85 -fun or_list1 s = P.enum1 "|" s
    3.86 -
    3.87 -val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    3.88 -
    3.89 -val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
    3.90 -val statement_ow = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
    3.91 -val statements_ow = or_list1 statement_ow
    3.92 -
    3.93 -
    3.94  val functionP =
    3.95    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    3.96 -  ((config_parser default_config -- P.opt_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    3.97 -     >> (fn (((config, target), fixes), statements) =>
    3.98 -            Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
    3.99 +  (fundef_parser default_config
   3.100 +     >> (fn ((config, fixes), statements) =>
   3.101 +            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd)
   3.102              #> Toplevel.print));
   3.103  
   3.104 -
   3.105 -
   3.106  val terminationP =
   3.107    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   3.108    (P.opt_target -- Scan.option P.name
   3.109 @@ -252,7 +238,6 @@
   3.110             Toplevel.print o
   3.111             Toplevel.local_theory_to_proof target (setup_termination_proof name)));
   3.112  
   3.113 -
   3.114  val _ = OuterSyntax.add_parsers [functionP];
   3.115  val _ = OuterSyntax.add_parsers [terminationP];
   3.116  val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];