# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID 422cac7d6e31be0f0cb14e855c772acabd97b1e0
# Parent  88c9c3460fe71a56a710e4829dcdd51c87f50574
added option to execute depth-limited computations for the values command in the predicate compiler

diff -r 88c9c3460fe7 -r 422cac7d6e31 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -37,7 +37,7 @@
   val print_all_modes: theory -> unit
   val do_proofs: bool Unsynchronized.ref
   val mk_casesrule : Proof.context -> int -> thm list -> term
-  val analyze_compr: theory -> term -> term
+  val analyze_compr: theory -> int option -> term -> term
   val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
   val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val code_pred_intros_attrib : attribute
@@ -1278,14 +1278,14 @@
     fold_rev lambda vs (f (list_comb (t, vs)))
   end;
 
-fun compile_param depth thy compfuns (NONE, t) = t
-  | compile_param depth thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
+fun compile_param depth_limited thy compfuns (NONE, t) = t
+  | compile_param depth_limited thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
    let
      val (f, args) = strip_comb (Envir.eta_contract t)
      val (params, args') = chop (length ms) args
-     val params' = map (compile_param depth thy compfuns) (ms ~~ params)
-     val mk_fun_of = case depth of NONE => mk_fun_of | SOME _ => mk_depth_limited_fun_of
-     val funT_of = case depth of NONE => funT_of | SOME _ => depth_limited_funT_of
+     val params' = map (compile_param depth_limited thy compfuns) (ms ~~ params)
+     val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of
+     val funT_of = if depth_limited then depth_limited_funT_of else funT_of
      val f' =
        case f of
          Const (name, T) => mk_fun_of compfuns thy (name, T) (iss, is')
@@ -1295,18 +1295,18 @@
      list_comb (f', params' @ args')
    end
 
-fun compile_expr depth thy ((Mode (mode, is, ms)), t) =
+fun compile_expr depth_limited thy ((Mode (mode, is, ms)), t) =
   case strip_comb t of
     (Const (name, T), params) =>
        let
-         val params' = map (compile_param depth thy PredicateCompFuns.compfuns) (ms ~~ params)
-         val mk_fun_of = case depth of NONE => mk_fun_of | SOME _ => mk_depth_limited_fun_of
+         val params' = map (compile_param depth_limited thy PredicateCompFuns.compfuns) (ms ~~ params)
+         val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of
        in
          list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params')
        end
   | (Free (name, T), args) =>
        let 
-         val funT_of = case depth of NONE => funT_of | SOME _ => depth_limited_funT_of 
+         val funT_of = if depth_limited then depth_limited_funT_of else funT_of
        in
          list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args)
        end;
@@ -1431,7 +1431,7 @@
                      NONE => in_ts
                    | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
                    val u = lift_pred compfuns
-                     (list_comb (compile_expr depth thy (mode, t), args))
+                     (list_comb (compile_expr (is_some depth) thy (mode, t), args))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1439,12 +1439,11 @@
              | Negprem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us
-                   val depth' = Option.map (apfst HOLogic.mk_not) depth
-                   val args = case depth' of
+                   val args = case depth of
                      NONE => in_ts
-                   | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
+                   | SOME (polarity, depth_t) => in_ts @ [HOLogic.mk_not polarity, depth_t]
                    val u = lift_pred compfuns (mk_not PredicateCompFuns.compfuns
-                     (list_comb (compile_expr depth' thy (mode, t), args)))
+                   (list_comb (compile_expr (is_some depth) thy (mode, t), args)))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1461,7 +1460,7 @@
                    val args = case depth of
                      NONE => in_ts
                      | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
-                   val u = compile_gen_expr depth thy compfuns (mode, t) args
+                   val u = compile_gen_expr (is_some depth) thy compfuns (mode, t) args
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -2438,7 +2437,7 @@
 val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
-fun analyze_compr thy t_compr =
+fun analyze_compr thy depth_limit 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);
@@ -2458,7 +2457,10 @@
       | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
                 ^ Syntax.string_of_term_global thy t_compr); m);
     val (inargs, outargs) = split_smode user_mode' args;
-    val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
+    val inargs' = case depth_limit of NONE => inargs
+      | SOME d => inargs @ [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d]
+    val t_pred = list_comb (compile_expr (is_some depth_limit) thy
+      (m, list_comb (pred, params)), inargs');
     val t_eval = if null outargs then t_pred else
       let
         val outargs_bounds = map (fn Bound i => i) outargs;
@@ -2474,17 +2476,17 @@
       in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end
   in t_eval end;
 
-fun eval thy t_compr =
+fun eval thy depth_limit t_compr =
   let
-    val t = analyze_compr thy t_compr;
+    val t = analyze_compr thy depth_limit t_compr;
     val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
     val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
   in (T, Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []) end;
 
-fun values ctxt k t_compr =
+fun values ctxt depth_limit k t_compr =
   let
     val thy = ProofContext.theory_of ctxt;
-    val (T, t) = eval thy t_compr;
+    val (T, t) = eval thy depth_limit t_compr;
     val setT = HOLogic.mk_setT T;
     val (ts, _) = Predicate.yieldn k t;
     val elemsT = HOLogic.mk_set T ts;
@@ -2499,11 +2501,11 @@
   in
   end;
   *)
-fun values_cmd modes k raw_t state =
+fun values_cmd modes depth_limit k raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
-    val t' = values ctxt k t;
+    val t' = values ctxt depth_limit k t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
     val p = PrintMode.with_modes modes (fn () =>
@@ -2515,10 +2517,15 @@
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 
+val _ = List.app OuterKeyword.keyword ["depth_limit"]
+
+val opt_depth_limit =
+  Scan.optional (P.$$$ "[" |-- P.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat --| P.$$$ "]" >> SOME) NONE
+
 val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_modes -- Scan.optional P.nat ~1 -- P.term
-    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
-        (values_cmd modes k t)));
+  (opt_modes -- opt_depth_limit -- Scan.optional P.nat ~1 -- P.term
+    >> (fn (((modes, depth_limit), k), t) => Toplevel.no_timing o Toplevel.keep
+        (values_cmd modes depth_limit k t)));
 
 end;