simplified preparation and outer parsing of specification;
authorwenzelm
Thu Mar 12 21:55:02 2009 +0100 (2009-03-12)
changeset 30487a14ff49d3083
parent 30486 9cdc7ce0e389
child 30490 d09b7f0c2c14
simplified preparation and outer parsing of specification;
export extern cmd interfaces as well;
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 12 21:51:02 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 12 21:55:02 2009 +0100
     1.3 @@ -12,6 +12,10 @@
     1.4      (binding * typ option * mixfix) list ->
     1.5      (binding * typ option * mixfix) list ->
     1.6      (Attrib.binding * term) list -> local_theory -> Proof.state
     1.7 +  val add_primrec_cmd: string list option -> string option ->
     1.8 +    (binding * string option * mixfix) list ->
     1.9 +    (binding * string option * mixfix) list ->
    1.10 +    (Attrib.binding * string) list -> local_theory -> Proof.state
    1.11  end;
    1.12  
    1.13  structure NominalPrimrec : NOMINAL_PRIMREC =
    1.14 @@ -36,10 +40,10 @@
    1.15        (fn Free (v, _) => insert (op =) v | _ => I) body []))
    1.16    in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
    1.17  
    1.18 -fun process_eqn lthy is_fixed spec rec_fns = 
    1.19 +fun process_eqn lthy is_fixed spec rec_fns =
    1.20    let
    1.21      val eq = unquantify spec;
    1.22 -    val (lhs, rhs) = 
    1.23 +    val (lhs, rhs) =
    1.24        HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
    1.25        handle TERM _ => raise RecError "not a proper equation";
    1.26  
    1.27 @@ -67,7 +71,7 @@
    1.28      fun check_vars _ [] = ()
    1.29        | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
    1.30    in
    1.31 -    if length middle > 1 then 
    1.32 +    if length middle > 1 then
    1.33        raise RecError "more than one non-variable in pattern"
    1.34      else
    1.35       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    1.36 @@ -159,7 +163,7 @@
    1.37                val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    1.38                  (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    1.39                    handle RecError s => primrec_eq_err lthy s eq
    1.40 -            in (fnames'', fnss'', 
    1.41 +            in (fnames'', fnss'',
    1.42                  (list_abs_free (cargs' @ subs, rhs'))::fns)
    1.43              end)
    1.44  
    1.45 @@ -172,7 +176,7 @@
    1.46              val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) =
    1.47                AList.lookup (op =) eqns fname;
    1.48              val (fnames', fnss', fns) = fold_rev (trans eqns') constrs
    1.49 -              ((i, fname)::fnames, fnss, []) 
    1.50 +              ((i, fname)::fnames, fnss, [])
    1.51            in
    1.52              (fnames', (i, (fname, ls, rs, fns))::fnss')
    1.53            end
    1.54 @@ -235,15 +239,9 @@
    1.55  
    1.56  local
    1.57  
    1.58 -fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
    1.59 -  let
    1.60 -    val ((fixes, spec), _) = prep_spec
    1.61 -      raw_fixes (map (single o apsnd single) raw_spec) ctxt
    1.62 -  in (fixes, map (apsnd the_single) spec) end;
    1.63 -
    1.64  fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
    1.65    let
    1.66 -    val (fixes', spec) = prepare_spec prep_spec lthy (raw_fixes @ raw_params) raw_spec;
    1.67 +    val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
    1.68      val fixes = List.take (fixes', length raw_fixes);
    1.69      val (names_atts, spec') = split_list spec;
    1.70      val eqns' = map unquantify spec'
    1.71 @@ -261,12 +259,12 @@
    1.72         then () else primrec_err param_err);
    1.73      val tnames = distinct (op =) (map (#1 o snd) eqns);
    1.74      val dts = find_dts dt_info tnames tnames;
    1.75 -    val main_fns = 
    1.76 +    val main_fns =
    1.77        map (fn (tname, {index, ...}) =>
    1.78 -        (index, 
    1.79 +        (index,
    1.80            (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns))
    1.81        dts;
    1.82 -    val {descr, rec_names, rec_rewrites, ...} = 
    1.83 +    val {descr, rec_names, rec_rewrites, ...} =
    1.84        if null dts then
    1.85          primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
    1.86        else snd (hd dts);
    1.87 @@ -388,15 +386,15 @@
    1.88  
    1.89  in
    1.90  
    1.91 -val add_primrec = gen_primrec false Specification.check_specification (K I);
    1.92 -val add_primrec_cmd = gen_primrec true Specification.read_specification Syntax.read_term;
    1.93 +val add_primrec = gen_primrec false Specification.check_spec (K I);
    1.94 +val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
    1.95  
    1.96  end;
    1.97  
    1.98  
    1.99  (* outer syntax *)
   1.100  
   1.101 -local structure P = OuterParse and K = OuterKeyword in
   1.102 +local structure P = OuterParse in
   1.103  
   1.104  val freshness_context = P.reserved "freshness_context";
   1.105  val invariant = P.reserved "invariant";
   1.106 @@ -408,28 +406,16 @@
   1.107      (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
   1.108    (parser1 >> pair NONE);
   1.109  val options =
   1.110 -  Scan.optional (P.$$$ "(" |-- P.!!!
   1.111 -    (parser2 --| P.$$$ ")")) (NONE, NONE);
   1.112 -
   1.113 -fun pipe_error t = P.!!! (Scan.fail_with (K
   1.114 -  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
   1.115 -
   1.116 -val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
   1.117 -  ((P.term :-- pipe_error) || Scan.succeed ("",""));
   1.118 -
   1.119 -val statements = P.enum1 "|" statement;
   1.120 -
   1.121 -val primrec_decl = P.opt_target -- options --
   1.122 -  P.fixes -- P.for_fixes --| P.$$$ "where" -- statements;
   1.123 +  Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
   1.124  
   1.125  val _ =
   1.126 -  OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
   1.127 -    (primrec_decl >> (fn ((((opt_target, (invs, fctxt)), raw_fixes), raw_params), raw_spec) =>
   1.128 -      Toplevel.print o Toplevel.local_theory_to_proof opt_target
   1.129 -        (add_primrec_cmd invs fctxt raw_fixes raw_params raw_spec)));
   1.130 +  OuterSyntax.local_theory_to_proof "nominal_primrec"
   1.131 +    "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
   1.132 +    (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
   1.133 +      >> (fn ((((invs, fctxt), fixes), params), specs) =>
   1.134 +        add_primrec_cmd invs fctxt fixes params specs));
   1.135  
   1.136  end;
   1.137  
   1.138 -
   1.139  end;
   1.140  
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Mar 12 21:51:02 2009 +0100
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Mar 12 21:55:02 2009 +0100
     2.3 @@ -9,6 +9,8 @@
     2.4  sig
     2.5    val add_primrec: (binding * typ option * mixfix) list ->
     2.6      (Attrib.binding * term) list -> local_theory -> thm list * local_theory
     2.7 +  val add_primrec_cmd: (binding * string option * mixfix) list ->
     2.8 +    (Attrib.binding * string) list -> local_theory -> thm list * local_theory
     2.9    val add_primrec_global: (binding * typ option * mixfix) list ->
    2.10      (Attrib.binding * term) list -> theory -> thm list * theory
    2.11    val add_primrec_overloaded: (string * (string * typ) * bool) list ->
    2.12 @@ -213,12 +215,6 @@
    2.13  
    2.14  local
    2.15  
    2.16 -fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
    2.17 -  let
    2.18 -    val ((fixes, spec), _) = prep_spec
    2.19 -      raw_fixes (map (single o apsnd single) raw_spec) ctxt
    2.20 -  in (fixes, map (apsnd the_single) spec) end;
    2.21 -
    2.22  fun prove_spec ctxt names rec_rewrites defs eqs =
    2.23    let
    2.24      val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
    2.25 @@ -228,7 +224,7 @@
    2.26  
    2.27  fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
    2.28    let
    2.29 -    val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
    2.30 +    val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
    2.31      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
    2.32        orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
    2.33      val tnames = distinct (op =) (map (#1 o snd) eqns);
    2.34 @@ -268,8 +264,8 @@
    2.35  
    2.36  in
    2.37  
    2.38 -val add_primrec = gen_primrec false Specification.check_specification;
    2.39 -val add_primrec_cmd = gen_primrec true Specification.read_specification;
    2.40 +val add_primrec = gen_primrec false Specification.check_spec;
    2.41 +val add_primrec_cmd = gen_primrec true Specification.read_spec;
    2.42  
    2.43  end;
    2.44  
    2.45 @@ -300,24 +296,16 @@
    2.46  val old_primrec_decl =
    2.47    opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
    2.48  
    2.49 -fun pipe_error t = P.!!! (Scan.fail_with (K
    2.50 -  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
    2.51 -
    2.52 -val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
    2.53 -  ((P.term :-- pipe_error) || Scan.succeed ("",""));
    2.54 -
    2.55 -val statements = P.enum1 "|" statement;
    2.56 -
    2.57 -val primrec_decl = P.opt_target -- P.fixes --| P.$$$ "where" -- statements;
    2.58 +val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
    2.59  
    2.60  val _ =
    2.61    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
    2.62 -    ((primrec_decl >> (fn ((opt_target, raw_fixes), raw_spec) =>
    2.63 -      Toplevel.local_theory opt_target (add_primrec_cmd raw_fixes raw_spec #> snd)))
    2.64 +    ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
    2.65 +      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
    2.66      || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
    2.67        Toplevel.theory (snd o
    2.68 -        (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec) alt_name
    2.69 -          (map P.triple_swap eqns)))));
    2.70 +        (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec)
    2.71 +          alt_name (map P.triple_swap eqns)))));
    2.72  
    2.73  end;
    2.74