- Changed type of invoke_codegen
authorberghofe
Mon Dec 10 15:40:55 2001 +0100 (2001-12-10)
changeset 12453806502073957
parent 12452 68493b92e7a6
child 12454 9b669895f984
- Changed type of invoke_codegen
- Added combinators for sequences
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Dec 10 15:39:34 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Dec 10 15:40:55 2001 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Pure/HOL/inductive_codegen.ML
     1.5 +(*  Title:      HOL/inductive_codegen.ML
     1.6      ID:         $Id$
     1.7      Author:     Stefan Berghofer, TU Muenchen
     1.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9 @@ -183,15 +183,15 @@
    1.10  
    1.11      fun compile_prems out_ts' vs names gr [] =
    1.12            let
    1.13 -            val (gr2, out_ps) = foldl_map (fn (gr, t) =>
    1.14 -              invoke_codegen thy gr dep false t) (gr, out_ts);
    1.15 +            val (gr2, out_ps) = foldl_map
    1.16 +              (invoke_codegen thy dep false) (gr, out_ts);
    1.17              val (gr3, eq_ps) = foldl_map (fn (gr, (s, t)) =>
    1.18                apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
    1.19 -                (invoke_codegen thy gr dep false t)) (gr2, eqs);
    1.20 +                (invoke_codegen thy dep false (gr, t))) (gr2, eqs);
    1.21              val (nvs, out_ts'') = foldl_map distinct_v
    1.22                ((names, map (fn x => (x, [x])) vs), out_ts');
    1.23 -            val (gr4, out_ps') = foldl_map (fn (gr, t) =>
    1.24 -              invoke_codegen thy gr dep false t) (gr3, out_ts'');
    1.25 +            val (gr4, out_ps') = foldl_map
    1.26 +              (invoke_codegen thy dep false) (gr3, out_ts'');
    1.27            in
    1.28              (gr4, compile_match (snd nvs) eq_ps out_ps'
    1.29                (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
    1.30 @@ -208,14 +208,14 @@
    1.31                 Prem (s, us, args) =>
    1.32                   let
    1.33                     val (in_ts, out_ts') = get_args mode' 1 us;
    1.34 -                   val (gr1, in_ps) = foldl_map (fn (gr, t) =>
    1.35 -                     invoke_codegen thy gr dep false t) (gr, in_ts);
    1.36 -                   val (gr2, arg_ps) = foldl_map (fn (gr, t) =>
    1.37 -                     invoke_codegen thy gr dep true t) (gr1, args);
    1.38 +                   val (gr1, in_ps) = foldl_map
    1.39 +                     (invoke_codegen thy dep false) (gr, in_ts);
    1.40 +                   val (gr2, arg_ps) = foldl_map
    1.41 +                     (invoke_codegen thy dep true) (gr1, args);
    1.42                     val (nvs, out_ts'') = foldl_map distinct_v
    1.43                       ((names, map (fn x => (x, [x])) vs), out_ts);
    1.44 -                   val (gr3, out_ps) = foldl_map (fn (gr, t) =>
    1.45 -                     invoke_codegen thy gr dep false t) (gr2, out_ts'')
    1.46 +                   val (gr3, out_ps) = foldl_map
    1.47 +                     (invoke_codegen thy dep false) (gr2, out_ts'')
    1.48                     val (gr4, rest) = compile_prems out_ts' vs' (fst nvs) gr3 ps';
    1.49                   in
    1.50                     (gr4, compile_match (snd nvs) [] out_ps
    1.51 @@ -227,11 +227,11 @@
    1.52                   end
    1.53               | Sidecond t =>
    1.54                   let
    1.55 -                   val (gr1, side_p) = invoke_codegen thy gr dep true t;
    1.56 +                   val (gr1, side_p) = invoke_codegen thy dep true (gr, t);
    1.57                     val (nvs, out_ts') = foldl_map distinct_v
    1.58                       ((names, map (fn x => (x, [x])) vs), out_ts);
    1.59 -                   val (gr2, out_ps) = foldl_map (fn (gr, t) =>
    1.60 -                     invoke_codegen thy gr dep false t) (gr1, out_ts')
    1.61 +                   val (gr2, out_ps) = foldl_map
    1.62 +                     (invoke_codegen thy dep false) (gr1, out_ts')
    1.63                     val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
    1.64                   in
    1.65                     (gr3, compile_match (snd nvs) [] out_ps
    1.66 @@ -357,10 +357,10 @@
    1.67               else (ts, 1 upto length ts);
    1.68             val _ = if mode mem the (assoc (modes, s)) then () else
    1.69               error ("No such mode for " ^ s ^ ": " ^ string_of_mode mode);
    1.70 -           val (gr2, in_ps) = foldl_map (fn (gr, t) =>
    1.71 -             invoke_codegen thy gr dep false t) (gr1, ts');
    1.72 -           val (gr3, arg_ps) = foldl_map (fn (gr, t) =>
    1.73 -             invoke_codegen thy gr dep true t) (gr2, args);
    1.74 +           val (gr2, in_ps) = foldl_map
    1.75 +             (invoke_codegen thy dep false) (gr1, ts');
    1.76 +           val (gr3, arg_ps) = foldl_map
    1.77 +             (invoke_codegen thy dep true) (gr2, args);
    1.78           in
    1.79             Some (gr3, Pretty.block (separate (Pretty.brk 1)
    1.80               (Pretty.str (modename thy s mode) :: arg_ps @ [mk_tuple in_ps])))
    1.81 @@ -371,7 +371,7 @@
    1.82        (case mk_ind_call thy gr dep t u false of
    1.83           None => None
    1.84         | Some (gr', call_p) => Some (gr', (if brack then parens else I)
    1.85 -           (Pretty.block [Pretty.str "nonempty (", call_p, Pretty.str ")"])))
    1.86 +           (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
    1.87    | inductive_codegen thy gr dep brack (Free ("query", _) $ (Const ("op :", _) $ t $ u)) =
    1.88        mk_ind_call thy gr dep t u true
    1.89    | inductive_codegen thy gr dep brack _ = None;
    1.90 @@ -379,3 +379,21 @@
    1.91  val setup = [add_codegen "inductive" inductive_codegen];
    1.92  
    1.93  end;
    1.94 +
    1.95 +
    1.96 +(**** combinators for code generated from inductive predicates ****)
    1.97 +
    1.98 +infix 5 :->;
    1.99 +infix 3 ++;
   1.100 +
   1.101 +fun s :-> f = Seq.flat (Seq.map f s);
   1.102 +
   1.103 +fun s1 ++ s2 = Seq.append (s1, s2);
   1.104 +
   1.105 +fun ?? b = if b then Seq.single () else Seq.empty;
   1.106 +
   1.107 +fun ?! s = is_some (Seq.pull s);    
   1.108 +
   1.109 +fun eq_1 x = Seq.single x;
   1.110 +
   1.111 +val eq_2 = eq_1;