# HG changeset patch
# User berghofe
# Date 1007995255 -3600
# Node ID 8065020739572fe1209ddad8bb2919a014fc3775
# Parent  68493b92e7a67f5500725c1aa7dac4b2b8177816
- Changed type of invoke_codegen
- Added combinators for sequences

diff -r 68493b92e7a6 -r 806502073957 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Dec 10 15:39:34 2001 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Dec 10 15:40:55 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/HOL/inductive_codegen.ML
+(*  Title:      HOL/inductive_codegen.ML
     ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
@@ -183,15 +183,15 @@
 
     fun compile_prems out_ts' vs names gr [] =
           let
-            val (gr2, out_ps) = foldl_map (fn (gr, t) =>
-              invoke_codegen thy gr dep false t) (gr, out_ts);
+            val (gr2, out_ps) = foldl_map
+              (invoke_codegen thy dep false) (gr, out_ts);
             val (gr3, eq_ps) = foldl_map (fn (gr, (s, t)) =>
               apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
-                (invoke_codegen thy gr dep false t)) (gr2, eqs);
+                (invoke_codegen thy dep false (gr, t))) (gr2, eqs);
             val (nvs, out_ts'') = foldl_map distinct_v
               ((names, map (fn x => (x, [x])) vs), out_ts');
-            val (gr4, out_ps') = foldl_map (fn (gr, t) =>
-              invoke_codegen thy gr dep false t) (gr3, out_ts'');
+            val (gr4, out_ps') = foldl_map
+              (invoke_codegen thy dep false) (gr3, out_ts'');
           in
             (gr4, compile_match (snd nvs) eq_ps out_ps'
               (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
@@ -208,14 +208,14 @@
                Prem (s, us, args) =>
                  let
                    val (in_ts, out_ts') = get_args mode' 1 us;
-                   val (gr1, in_ps) = foldl_map (fn (gr, t) =>
-                     invoke_codegen thy gr dep false t) (gr, in_ts);
-                   val (gr2, arg_ps) = foldl_map (fn (gr, t) =>
-                     invoke_codegen thy gr dep true t) (gr1, args);
+                   val (gr1, in_ps) = foldl_map
+                     (invoke_codegen thy dep false) (gr, in_ts);
+                   val (gr2, arg_ps) = foldl_map
+                     (invoke_codegen thy dep true) (gr1, args);
                    val (nvs, out_ts'') = foldl_map distinct_v
                      ((names, map (fn x => (x, [x])) vs), out_ts);
-                   val (gr3, out_ps) = foldl_map (fn (gr, t) =>
-                     invoke_codegen thy gr dep false t) (gr2, out_ts'')
+                   val (gr3, out_ps) = foldl_map
+                     (invoke_codegen thy dep false) (gr2, out_ts'')
                    val (gr4, rest) = compile_prems out_ts' vs' (fst nvs) gr3 ps';
                  in
                    (gr4, compile_match (snd nvs) [] out_ps
@@ -227,11 +227,11 @@
                  end
              | Sidecond t =>
                  let
-                   val (gr1, side_p) = invoke_codegen thy gr dep true t;
+                   val (gr1, side_p) = invoke_codegen thy dep true (gr, t);
                    val (nvs, out_ts') = foldl_map distinct_v
                      ((names, map (fn x => (x, [x])) vs), out_ts);
-                   val (gr2, out_ps) = foldl_map (fn (gr, t) =>
-                     invoke_codegen thy gr dep false t) (gr1, out_ts')
+                   val (gr2, out_ps) = foldl_map
+                     (invoke_codegen thy dep false) (gr1, out_ts')
                    val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
                  in
                    (gr3, compile_match (snd nvs) [] out_ps
@@ -357,10 +357,10 @@
              else (ts, 1 upto length ts);
            val _ = if mode mem the (assoc (modes, s)) then () else
              error ("No such mode for " ^ s ^ ": " ^ string_of_mode mode);
-           val (gr2, in_ps) = foldl_map (fn (gr, t) =>
-             invoke_codegen thy gr dep false t) (gr1, ts');
-           val (gr3, arg_ps) = foldl_map (fn (gr, t) =>
-             invoke_codegen thy gr dep true t) (gr2, args);
+           val (gr2, in_ps) = foldl_map
+             (invoke_codegen thy dep false) (gr1, ts');
+           val (gr3, arg_ps) = foldl_map
+             (invoke_codegen thy dep true) (gr2, args);
          in
            Some (gr3, Pretty.block (separate (Pretty.brk 1)
              (Pretty.str (modename thy s mode) :: arg_ps @ [mk_tuple in_ps])))
@@ -371,7 +371,7 @@
       (case mk_ind_call thy gr dep t u false of
          None => None
        | Some (gr', call_p) => Some (gr', (if brack then parens else I)
-           (Pretty.block [Pretty.str "nonempty (", call_p, Pretty.str ")"])))
+           (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   | inductive_codegen thy gr dep brack (Free ("query", _) $ (Const ("op :", _) $ t $ u)) =
       mk_ind_call thy gr dep t u true
   | inductive_codegen thy gr dep brack _ = None;
@@ -379,3 +379,21 @@
 val setup = [add_codegen "inductive" inductive_codegen];
 
 end;
+
+
+(**** combinators for code generated from inductive predicates ****)
+
+infix 5 :->;
+infix 3 ++;
+
+fun s :-> f = Seq.flat (Seq.map f s);
+
+fun s1 ++ s2 = Seq.append (s1, s2);
+
+fun ?? b = if b then Seq.single () else Seq.empty;
+
+fun ?! s = is_some (Seq.pull s);    
+
+fun eq_1 x = Seq.single x;
+
+val eq_2 = eq_1;