improving mode parsing in the predicate compiler

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Oct 28 12:29:00 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Oct 28 12:29:01 2009 +0100
@@ -156,10 +156,33 @@
 local structure P = OuterParse
 in
 
+(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
+datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
+
+val parse_argmode' =
+  ((Args.$$$ "i" || Args.$$$ "o") >> Argmode) ||
+  (Args.$$$ "(" |-- P.enum1 "," (Args.$$$ "i" || Args.$$$ "o") --| Args.$$$ ")" >> Argmode_Tuple)
+
+fun mk_numeral_mode ss = flat (map_index (fn (i, s) => if s = "i" then [i + 1] else []) ss)
+
+val parse_smode' = P.$$$ "[" |-- P.enum1 "," parse_argmode' --| P.$$$ "]"
+  >> (fn m => flat (map_index
+    (fn (i, Argmode s) => if s = "i" then [(i + 1, NONE)] else []
+      | (i, Argmode_Tuple ss) => [(i + 1, SOME (mk_numeral_mode ss))]) m))
+
+val parse_smode = (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") >> map (rpair NONE)
+
+fun gen_parse_mode smode_parser =
+  (Scan.optional
+    (P.enum "!" ((P.$$$ "X" >> K NONE) || (smode_parser >> SOME)) --| P.$$$ "!") []) -- smode_parser
+
+val parse_mode = gen_parse_mode parse_smode
+
+val parse_mode' = gen_parse_mode parse_smode'
+
 val opt_modes =
   Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
-   P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]")
-  --| P.$$$ ")" >> SOME) NONE
+    P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
 
 val scan_params =
   let

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Oct 28 12:29:00 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Oct 28 12:29:01 2009 +0100
@@ -9,6 +9,9 @@
 structure Predicate_Compile_Aux =
 struct
 
+type smode = (int * int list option) list
+type mode = smode option list * smode
+
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
@@ -136,7 +139,7 @@
 (* Different options for compiler *)
 
 datatype options = Options of {  
-  expected_modes : (string * int list list) option,
+  expected_modes : (string * mode list) option,
   show_steps : bool,
   show_proof_trace : bool,
   show_intermediate_results : bool,

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 12:29:00 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 28 12:29:01 2009 +0100
@@ -421,10 +421,10 @@
   case expected_modes options of
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME modes =>
-        if not (eq_set (op =) (map (map (rpair NONE)) ms, map snd modes)) then
+        if not (eq_set (op =) (ms, modes)) then
           error ("expected modes were not inferred:\n"
-          ^ "inferred modes for " ^ s ^ ": "
-          ^ commas (map ((enclose "[" "]") o string_of_smode o snd) modes))
+          ^ "inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes)
+          ^ "\n expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
         else ()
       | NONE => ())
   | NONE => ()

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Oct 28 12:29:00 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Oct 28 12:29:01 2009 +0100
@@ -1,12 +1,12 @@
 theory Predicate_Compile_ex
-imports Main Predicate_Compile_Alternative_Defs
+imports "../Main" Predicate_Compile_Alternative_Defs
 begin
 
 subsection {* Basic predicates *}
 
 inductive False' :: "bool"
 
-code_pred (mode: []) False' .
+code_pred (mode: X ! []) False' .
 code_pred [depth_limited] False' .
 code_pred [rpred] False' .
 
@@ -26,7 +26,13 @@
 inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
-code_pred (mode: [], [1], [2], [1, 2])EmptyClosure .
+code_pred
+(*  (mode: [] => [], [] => [1], [] => [2], [] => [1, 2],
+         [1] => [], [1] => [1], [1] => [2], [1] => [1, 2],
+         [2] => [], [2] => [1], [2] => [2], [2] => [1, 2],
+         [1, 2] => [], [1, 2] => [1], [1, 2] => [2], [1, 2] => [1, 2])*)
+  EmptyClosure .
+
 thm EmptyClosure.equation
 (* TODO: inductive package is broken!
 inductive False'' :: "bool"
@@ -272,7 +278,7 @@
   "tupled_append ([], xs, xs)"
 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
 
-code_pred tupled_append .
+code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append .
 code_pred [rpred] tupled_append .
 thm tupled_append.equation
 (*
@@ -286,7 +292,7 @@
 | "[| ys = fst (xa, y); x # zs = snd (xa, y);
  tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
 
-code_pred tupled_append' .
+code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append' .
 thm tupled_append'.equation
 
 inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -294,9 +300,7 @@
   "tupled_append'' ([], xs, xs)"
 | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
 
-thm tupled_append''.cases
-
-code_pred [inductify] tupled_append'' .
+code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append'' .
 thm tupled_append''.equation
 
 inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
@@ -304,7 +308,7 @@
   "tupled_append''' ([], xs, xs)"
 | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
 
-code_pred [inductify] tupled_append''' .
+code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append''' .
 thm tupled_append'''.equation
 
 subsection {* map_ofP predicate *}
@@ -325,8 +329,8 @@
   "filter1 P [] []"
 | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
 | "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
-
-code_pred (mode: [1], [1, 2]) filter1 .
+ML {* Scan.optional *}
+code_pred ( mode : [1], [1, 2]) filter1 .
 code_pred [depth_limited] filter1 .
 code_pred [rpred] filter1 .