# HG changeset patch
# User wenzelm
# Date 1236891302 -3600
# Node ID a14ff49d30830b7b7349e2b49fc30e172acc912a
# Parent  9cdc7ce0e3891268094611a9e5f357c961c700cd
simplified preparation and outer parsing of specification;
export extern cmd interfaces as well;

diff -r 9cdc7ce0e389 -r a14ff49d3083 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 12 21:51:02 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 12 21:55:02 2009 +0100
@@ -12,6 +12,10 @@
     (binding * typ option * mixfix) list ->
     (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> Proof.state
+  val add_primrec_cmd: string list option -> string option ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> local_theory -> Proof.state
 end;
 
 structure NominalPrimrec : NOMINAL_PRIMREC =
@@ -36,10 +40,10 @@
       (fn Free (v, _) => insert (op =) v | _ => I) body []))
   in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
 
-fun process_eqn lthy is_fixed spec rec_fns = 
+fun process_eqn lthy is_fixed spec rec_fns =
   let
     val eq = unquantify spec;
-    val (lhs, rhs) = 
+    val (lhs, rhs) =
       HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
       handle TERM _ => raise RecError "not a proper equation";
 
@@ -67,7 +71,7 @@
     fun check_vars _ [] = ()
       | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
   in
-    if length middle > 1 then 
+    if length middle > 1 then
       raise RecError "more than one non-variable in pattern"
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
@@ -159,7 +163,7 @@
               val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
                 (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
                   handle RecError s => primrec_eq_err lthy s eq
-            in (fnames'', fnss'', 
+            in (fnames'', fnss'',
                 (list_abs_free (cargs' @ subs, rhs'))::fns)
             end)
 
@@ -172,7 +176,7 @@
             val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) =
               AList.lookup (op =) eqns fname;
             val (fnames', fnss', fns) = fold_rev (trans eqns') constrs
-              ((i, fname)::fnames, fnss, []) 
+              ((i, fname)::fnames, fnss, [])
           in
             (fnames', (i, (fname, ls, rs, fns))::fnss')
           end
@@ -235,15 +239,9 @@
 
 local
 
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
-  let
-    val ((fixes, spec), _) = prep_spec
-      raw_fixes (map (single o apsnd single) raw_spec) ctxt
-  in (fixes, map (apsnd the_single) spec) end;
-
 fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
   let
-    val (fixes', spec) = prepare_spec prep_spec lthy (raw_fixes @ raw_params) raw_spec;
+    val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
     val fixes = List.take (fixes', length raw_fixes);
     val (names_atts, spec') = split_list spec;
     val eqns' = map unquantify spec'
@@ -261,12 +259,12 @@
        then () else primrec_err param_err);
     val tnames = distinct (op =) (map (#1 o snd) eqns);
     val dts = find_dts dt_info tnames tnames;
-    val main_fns = 
+    val main_fns =
       map (fn (tname, {index, ...}) =>
-        (index, 
+        (index,
           (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns))
       dts;
-    val {descr, rec_names, rec_rewrites, ...} = 
+    val {descr, rec_names, rec_rewrites, ...} =
       if null dts then
         primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
       else snd (hd dts);
@@ -388,15 +386,15 @@
 
 in
 
-val add_primrec = gen_primrec false Specification.check_specification (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_specification Syntax.read_term;
+val add_primrec = gen_primrec false Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
 
 end;
 
 
 (* outer syntax *)
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = OuterParse in
 
 val freshness_context = P.reserved "freshness_context";
 val invariant = P.reserved "invariant";
@@ -408,28 +406,16 @@
     (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
 val options =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-    (parser2 --| P.$$$ ")")) (NONE, NONE);
-
-fun pipe_error t = P.!!! (Scan.fail_with (K
-  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
-  ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-val statements = P.enum1 "|" statement;
-
-val primrec_decl = P.opt_target -- options --
-  P.fixes -- P.for_fixes --| P.$$$ "where" -- statements;
+  Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
 
 val _ =
-  OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
-    (primrec_decl >> (fn ((((opt_target, (invs, fctxt)), raw_fixes), raw_params), raw_spec) =>
-      Toplevel.print o Toplevel.local_theory_to_proof opt_target
-        (add_primrec_cmd invs fctxt raw_fixes raw_params raw_spec)));
+  OuterSyntax.local_theory_to_proof "nominal_primrec"
+    "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
+    (options -- P.fixes -- P.for_fixes -- SpecParse.where_alt_specs
+      >> (fn ((((invs, fctxt), fixes), params), specs) =>
+        add_primrec_cmd invs fctxt fixes params specs));
 
 end;
 
-
 end;
 
diff -r 9cdc7ce0e389 -r a14ff49d3083 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Mar 12 21:51:02 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Thu Mar 12 21:55:02 2009 +0100
@@ -9,6 +9,8 @@
 sig
   val add_primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> thm list * local_theory
+  val add_primrec_cmd: (binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> local_theory -> thm list * local_theory
   val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
@@ -213,12 +215,6 @@
 
 local
 
-fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
-  let
-    val ((fixes, spec), _) = prep_spec
-      raw_fixes (map (single o apsnd single) raw_spec) ctxt
-  in (fixes, map (apsnd the_single) spec) end;
-
 fun prove_spec ctxt names rec_rewrites defs eqs =
   let
     val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
@@ -228,7 +224,7 @@
 
 fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
   let
-    val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
+    val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
       orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
     val tnames = distinct (op =) (map (#1 o snd) eqns);
@@ -268,8 +264,8 @@
 
 in
 
-val add_primrec = gen_primrec false Specification.check_specification;
-val add_primrec_cmd = gen_primrec true Specification.read_specification;
+val add_primrec = gen_primrec false Specification.check_spec;
+val add_primrec_cmd = gen_primrec true Specification.read_spec;
 
 end;
 
@@ -300,24 +296,16 @@
 val old_primrec_decl =
   opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
 
-fun pipe_error t = P.!!! (Scan.fail_with (K
-  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
-
-val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
-  ((P.term :-- pipe_error) || Scan.succeed ("",""));
-
-val statements = P.enum1 "|" statement;
-
-val primrec_decl = P.opt_target -- P.fixes --| P.$$$ "where" -- statements;
+val primrec_decl = P.opt_target -- P.fixes -- SpecParse.where_alt_specs;
 
 val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    ((primrec_decl >> (fn ((opt_target, raw_fixes), raw_spec) =>
-      Toplevel.local_theory opt_target (add_primrec_cmd raw_fixes raw_spec #> snd)))
+    ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
+      Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
     || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
       Toplevel.theory (snd o
-        (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec) alt_name
-          (map P.triple_swap eqns)))));
+        (if unchecked then OldPrimrecPackage.add_primrec_unchecked else OldPrimrecPackage.add_primrec)
+          alt_name (map P.triple_swap eqns)))));
 
 end;