# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 428ddcc16e7b8fe5dedc8560b0403cf664eaa2f2
# Parent  b70fe083694daa7de7081fcbcd2cc273e91e4b83
added optional mode annotations for parameters in the values command

diff -r b70fe083694d -r 428ddcc16e7b src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -198,6 +198,11 @@
 
 val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 
+val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME)
+
+val opt_param_modes = Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
+  P.enum ", " opt_smode --| P.$$$ ")" >> SOME) NONE
+
 val value_options =
   let
     val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
@@ -215,9 +220,9 @@
   OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
 
 val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_print_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
-    >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
-        (Predicate_Compile_Core.values_cmd modes options k t)));
+  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+    >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.no_timing o Toplevel.keep
+        (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
 
 end
 
diff -r b70fe083694d -r 428ddcc16e7b src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -9,7 +9,8 @@
   val setup : theory -> theory
   val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
   val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
-  val values_cmd : string list -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
+  val values_cmd : string list -> Predicate_Compile_Aux.smode option list option
+    -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
   val register_predicate : (string * thm list * thm * int) -> theory -> theory
   val register_intros : string * thm list -> theory -> theory
   val is_registered : theory -> string -> bool
@@ -2480,7 +2481,7 @@
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 (* TODO: *)
-fun analyze_compr thy compfuns (depth_limit, (random, annotated)) t_compr =
+fun analyze_compr thy compfuns param_user_modes (depth_limit, (random, annotated)) t_compr =
   let
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
@@ -2492,8 +2493,15 @@
         else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
     val user_mode' = map (rpair NONE) user_mode
     val all_modes_of = if random then all_generator_modes_of else all_modes_of
-      (*val compile_expr = if random then compile_gen_expr else compile_expr*)
-    val modes = filter (fn Mode (_, is, _) => is = user_mode')
+    fun fits_to is NONE = true
+      | fits_to is (SOME pm) = (is = pm)
+    fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) = fits_to is pm andalso valid (ms @ ms') pms
+      | valid (NONE :: ms') pms = valid ms' pms
+      | valid [] [] = true
+      | valid [] _ = error "Too many mode annotations"
+      | valid (SOME _ :: _) [] = error "Not enough mode annotations"
+    val modes = filter (fn Mode (_, is, ms) => is = user_mode'
+        andalso (the_default true (Option.map (valid ms) param_user_modes)))
       (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
     val m = case modes
      of [] => error ("No mode possible for comprehension "
@@ -2531,10 +2539,10 @@
       in mk_map compfuns T_pred T_compr arrange t_pred end
   in t_eval end;
 
-fun eval thy (options as (depth_limit, (random, annotated))) t_compr =
+fun eval thy param_user_modes (options as (depth_limit, (random, annotated))) t_compr =
   let
     val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns
-    val t = analyze_compr thy compfuns options t_compr;
+    val t = analyze_compr thy compfuns param_user_modes options t_compr;
     val T = dest_predT compfuns (fastype_of t);
     val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
     val eval =
@@ -2546,10 +2554,10 @@
         Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
   in (T, eval) end;
 
-fun values ctxt options k t_compr =
+fun values ctxt param_user_modes options k t_compr =
   let
     val thy = ProofContext.theory_of ctxt;
-    val (T, ts) = eval thy options t_compr;
+    val (T, ts) = eval thy param_user_modes options t_compr;
     val (ts, _) = Predicate.yieldn k ts;
     val setT = HOLogic.mk_setT T;
     val elemsT = HOLogic.mk_set T ts;
@@ -2565,11 +2573,11 @@
   in
   end;
   *)
-fun values_cmd print_modes options k raw_t state =
+fun values_cmd print_modes param_user_modes options k raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
-    val t' = values ctxt options k t;
+    val t' = values ctxt param_user_modes options k t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
     val p = PrintMode.with_modes print_modes (fn () =>
diff -r b70fe083694d -r 428ddcc16e7b src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -472,13 +472,13 @@
 values "{m. succ 0 m}"
 values "{m. succ m 0}"
 
-(* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
+text {* values command needs mode annotation of the parameter succ
+to disambiguate which mode is to be chosen. *} 
 
-(*
-values 20 "{n. tranclp succ 10 n}"
-values "{n. tranclp succ n 10}"
+values [mode: [1]] 20 "{n. tranclp succ 10 n}"
+values [mode: [2]] 10 "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
-*)
+
 
 subsection {* IMP *}