simplified preparation and outer parsing of specification;
authorwenzelm
Thu Mar 12 21:51:02 2009 +0100 (2009-03-12)
changeset 304869cdc7ce0e389
parent 30485 99def5248e7f
child 30487 a14ff49d3083
simplified preparation and outer parsing of specification;
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 21:47:36 2009 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 21:51:02 2009 +0100
     1.3 @@ -359,7 +359,7 @@
     1.4                           >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
     1.5  in
     1.6    fun fundef_parser default_cfg = 
     1.7 -      config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements
     1.8 +      config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
     1.9  end
    1.10  
    1.11  
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 12 21:47:36 2009 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Mar 12 21:51:02 2009 +0100
     2.3 @@ -93,13 +93,12 @@
     2.4      end
     2.5  
     2.6  
     2.7 -fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
     2.8 +fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
     2.9      let
    2.10        val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
    2.11 -      val ((fixes0, spec0), ctxt') = 
    2.12 -        prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
    2.13 +      val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
    2.14        val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    2.15 -      val spec = map (apfst (apfst Binding.name_of)) spec0;
    2.16 +      val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
    2.17        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    2.18  
    2.19        val defname = mk_defname fixes
    2.20 @@ -163,9 +162,8 @@
    2.21    |> LocalTheory.set_group (serial_string ())
    2.22    |> setup_termination_proof term_opt;
    2.23  
    2.24 -val add_fundef = gen_add_fundef true Specification.read_specification "_::type"
    2.25 -val add_fundef_i = 
    2.26 -  gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)
    2.27 +val add_fundef = gen_add_fundef true Specification.read_spec "_::type"
    2.28 +val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
    2.29  
    2.30  
    2.31  (* Datatype hook to declare datatype congs as "fundef_congs" *)
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Mar 12 21:47:36 2009 +0100
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 12 21:51:02 2009 +0100
     3.3 @@ -842,11 +842,10 @@
     3.4  
     3.5  fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
     3.6    let
     3.7 -    val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
     3.8 -      |> Specification.read_specification
     3.9 -          (cnames_syn @ pnames_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs);
    3.10 +    val ((vars, intrs), _) = lthy
    3.11 +      |> ProofContext.set_mode ProofContext.mode_abbrev
    3.12 +      |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
    3.13      val (cs, ps) = chop (length cnames_syn) vars;
    3.14 -    val intrs = map (apsnd the_single) specs;
    3.15      val monos = Attrib.eval_thms lthy raw_monos;
    3.16      val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
    3.17        alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
    3.18 @@ -946,22 +945,12 @@
    3.19  
    3.20  val _ = OuterKeyword.keyword "monos";
    3.21  
    3.22 -(* FIXME eliminate *)
    3.23 -fun flatten_specification specs = specs |> maps
    3.24 -  (fn (a, (concl, [])) => concl |> map
    3.25 -        (fn ((b, atts), [B]) =>
    3.26 -              if Binding.is_empty a then ((b, atts), B)
    3.27 -              else if Binding.is_empty b then ((a, atts), B)
    3.28 -              else error "Illegal nested case names"
    3.29 -          | ((b, _), _) => error "Illegal simultaneous specification")
    3.30 -    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.str_of a)));
    3.31 -
    3.32  fun gen_ind_decl mk_def coind =
    3.33    P.fixes -- P.for_fixes --
    3.34 -  Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
    3.35 +  Scan.optional SpecParse.where_alt_specs [] --
    3.36    Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
    3.37    >> (fn (((preds, params), specs), monos) =>
    3.38 -      (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
    3.39 +      (snd oo gen_add_inductive mk_def true coind preds params specs monos));
    3.40  
    3.41  val ind_decl = gen_ind_decl add_ind_def;
    3.42  
    3.43 @@ -971,7 +960,7 @@
    3.44  val _ =
    3.45    OuterSyntax.local_theory "inductive_cases"
    3.46      "create simplified instances of elimination rules (improper)" K.thy_script
    3.47 -    (P.and_list1 SpecParse.spec >> (fn specs => snd o inductive_cases specs));
    3.48 +    (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
    3.49  
    3.50  end;
    3.51