# HG changeset patch
# User bulwahn
# Date 1284536198 -7200
# Node ID c797f3ab2ae1b5a971dad6ca77313a95dbea5748
# Parent  9717ea8d42b313c32dc3cc4879b6f18798c79d82
proposed modes for code_pred now supports modes for mutual predicates

diff -r 9717ea8d42b3 -r c797f3ab2ae1 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 09:36:38 2010 +0200
@@ -139,16 +139,24 @@
         (Term_Graph.strong_conn gr) thy))
   end
 
-fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
+datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list
+  | Single_Pred of (mode * string option) list
+
+fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
   let
     fun chk s = member (op =) raw_options s
+    val proposed_modes = case proposed_modes of
+          Single_Pred proposed_modes => [(const, proposed_modes)]
+        | Multiple_Preds proposed_modes => map
+          (apfst (Code.read_const (ProofContext.theory_of lthy))) proposed_modes
   in
     Options {
       expected_modes = Option.map (pair const) expected_modes,
-      proposed_modes = Option.map (pair const o map fst) proposed_modes,
+      proposed_modes = 
+        map (apsnd (map fst)) proposed_modes,
       proposed_names =
-        the_default [] (Option.map (map_filter
-          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes),
+        maps (fn (predname, ms) => (map_filter
+          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
@@ -174,7 +182,7 @@
      val const = Code.read_const thy raw_const
      val T = Sign.the_const_type thy const
      val t = Const (const, T)
-     val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
+     val options = extract_options lthy (((expected_modes, proposed_modes), raw_options), const)
   in
     if is_inductify options then
       let
@@ -208,9 +216,13 @@
 val mode_and_opt_proposal = parse_mode_expr --
   Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
 
+
 val opt_modes =
   Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
-    Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
+    (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
+        (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
+      || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
+    --| Parse.$$$ ")") (Multiple_Preds [])
 
 val opt_expected_modes =
   Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
diff -r 9717ea8d42b3 -r c797f3ab2ae1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:38 2010 +0200
@@ -99,7 +99,7 @@
   (* Different options for compiler *)
   datatype options = Options of {  
     expected_modes : (string * mode list) option,
-    proposed_modes : (string * mode list) option,
+    proposed_modes : (string * mode list) list,
     proposed_names : ((string * mode) * string) list,
     show_steps : bool,
     show_proof_trace : bool,
@@ -119,7 +119,7 @@
     compilation : compilation
   };
   val expected_modes : options -> (string * mode list) option
-  val proposed_modes : options -> (string * mode list) option
+  val proposed_modes : options -> string -> mode list option
   val proposed_names : options -> string -> mode -> string option
   val show_steps : options -> bool
   val show_proof_trace : options -> bool
@@ -703,7 +703,7 @@
 
 datatype options = Options of {  
   expected_modes : (string * mode list) option,
-  proposed_modes : (string * mode list) option,
+  proposed_modes : (string * mode list) list,
   proposed_names : ((string * mode) * string) list,
   show_steps : bool,
   show_proof_trace : bool,
@@ -724,7 +724,7 @@
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
-fun proposed_modes (Options opt) = #proposed_modes opt
+fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
 fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
   (#proposed_names opt) (name, mode)
 
@@ -752,7 +752,7 @@
 
 val default_options = Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
diff -r 9717ea8d42b3 -r c797f3ab2ae1 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 09:36:38 2010 +0200
@@ -400,8 +400,8 @@
   | NONE => ()
 
 fun check_proposed_modes preds options modes errors =
-  case proposed_modes options of
-    SOME (s, ms) => (case AList.lookup (op =) modes s of
+  map (fn (s, _) => case proposed_modes options s of
+    SOME ms => (case AList.lookup (op =) modes s of
       SOME inferred_ms =>
         let
           val preds_without_modes = map fst (filter (null o snd) modes)
@@ -419,7 +419,7 @@
           else ()
         end
       | NONE => ())
-  | NONE => ()
+  | NONE => ()) preds
 
 (* importing introduction rules *)
 
@@ -2700,8 +2700,8 @@
         all_modes_of_typ T
     val all_modes = 
       map (fn (s, T) =>
-        (s, case (proposed_modes options) of
-            SOME (s', ms) => if s = s' then ms else generate_modes s T
+        (s, case proposed_modes options s of
+            SOME ms => ms
           | NONE => generate_modes s T)) preds
     val params =
       case intrs of
@@ -2719,7 +2719,7 @@
         let
           val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)) 
         in
-          ho_args_of (hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))) args
+          ho_args_of_typ (snd (dest_Const p)) args
         end
     val param_vs = map (fst o dest_Free) params
     fun add_clause intr clauses =
diff -r 9717ea8d42b3 -r c797f3ab2ae1 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 08:58:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 09:36:38 2010 +0200
@@ -56,7 +56,7 @@
 
 val options = Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,