established canonical argument order in SML code generators
authorhaftmann
Thu Oct 09 08:47:27 2008 +0200 (2008-10-09)
changeset 285371e84256d1a8a
parent 28536 8dccb6035d0f
child 28538 3147236326ea
established canonical argument order in SML code generators
src/HOL/Code_Setup.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/typedef_codegen.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Oct 09 08:47:26 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Oct 09 08:47:27 2008 +0200
     1.3 @@ -169,20 +169,20 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 -fun eq_codegen thy defs gr dep thyname b t =
     1.8 +fun eq_codegen thy defs dep thyname b t gr =
     1.9      (case strip_comb t of
    1.10         (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.11       | (Const ("op =", _), [t, u]) =>
    1.12            let
    1.13 -            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.14 -            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    1.15 -            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    1.16 +            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    1.17 +            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    1.18 +            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
    1.19            in
    1.20 -            SOME (gr''', Codegen.parens
    1.21 -              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
    1.22 +            SOME (Codegen.parens
    1.23 +              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    1.24            end
    1.25       | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.26 -         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.27 +         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.28       | _ => NONE);
    1.29  
    1.30  in
     2.1 --- a/src/HOL/Int.thy	Thu Oct 09 08:47:26 2008 +0200
     2.2 +++ b/src/HOL/Int.thy	Thu Oct 09 08:47:27 2008 +0200
     2.3 @@ -1969,11 +1969,11 @@
     2.4  fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
     2.5    | strip_number_of t = t;
     2.6  
     2.7 -fun numeral_codegen thy defs gr dep module b t =
     2.8 +fun numeral_codegen thy defs dep module b t gr =
     2.9    let val i = HOLogic.dest_numeral (strip_number_of t)
    2.10    in
    2.11 -    SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
    2.12 -      Codegen.str (string_of_int i))
    2.13 +    SOME (Codegen.str (string_of_int i),
    2.14 +      snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
    2.15    end handle TERM _ => NONE;
    2.16  
    2.17  in
     3.1 --- a/src/HOL/List.thy	Thu Oct 09 08:47:26 2008 +0200
     3.2 +++ b/src/HOL/List.thy	Thu Oct 09 08:47:27 2008 +0200
     3.3 @@ -3631,21 +3631,21 @@
     3.4  setup {*
     3.5  let
     3.6  
     3.7 -fun list_codegen thy defs gr dep thyname b t =
     3.8 +fun list_codegen thy defs dep thyname b t gr =
     3.9    let
    3.10      val ts = HOLogic.dest_list t;
    3.11 -    val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
    3.12 -      (gr, fastype_of t);
    3.13 -    val (gr'', ps) = foldl_map
    3.14 -      (Codegen.invoke_codegen thy defs dep thyname false) (gr', ts)
    3.15 -  in SOME (gr'', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
    3.16 -
    3.17 -fun char_codegen thy defs gr dep thyname b t =
    3.18 +    val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
    3.19 +      (fastype_of t) gr;
    3.20 +    val (ps, gr'') = fold_map
    3.21 +      (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
    3.22 +  in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
    3.23 +
    3.24 +fun char_codegen thy defs dep thyname b t gr =
    3.25    let
    3.26      val i = HOLogic.dest_char t;
    3.27 -    val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
    3.28 -      (gr, fastype_of t)
    3.29 -  in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i)))
    3.30 +    val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
    3.31 +      (fastype_of t) gr;
    3.32 +  in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
    3.33    end handle TERM _ => NONE;
    3.34  
    3.35  in
     4.1 --- a/src/HOL/Product_Type.thy	Thu Oct 09 08:47:26 2008 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Thu Oct 09 08:47:27 2008 +0200
     4.3 @@ -979,7 +979,7 @@
     4.4        | _ => ([], u))
     4.5    | strip_abs_split i t = ([], t);
     4.6  
     4.7 -fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of
     4.8 +fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of
     4.9      (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
    4.10      let
    4.11        fun dest_let (l as Const ("Let", _) $ t $ u) =
    4.12 @@ -987,44 +987,44 @@
    4.13               ([p], u') => apfst (cons (p, t)) (dest_let u')
    4.14             | _ => ([], l))
    4.15          | dest_let t = ([], t);
    4.16 -      fun mk_code (gr, (l, r)) =
    4.17 +      fun mk_code (l, r) gr =
    4.18          let
    4.19 -          val (gr1, pl) = Codegen.invoke_codegen thy defs dep thyname false (gr, l);
    4.20 -          val (gr2, pr) = Codegen.invoke_codegen thy defs dep thyname false (gr1, r);
    4.21 -        in (gr2, (pl, pr)) end
    4.22 +          val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
    4.23 +          val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
    4.24 +        in ((pl, pr), gr2) end
    4.25      in case dest_let (t1 $ t2 $ t3) of
    4.26          ([], _) => NONE
    4.27        | (ps, u) =>
    4.28            let
    4.29 -            val (gr1, qs) = foldl_map mk_code (gr, ps);
    4.30 -            val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
    4.31 -            val (gr3, pargs) = foldl_map
    4.32 -              (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
    4.33 +            val (qs, gr1) = fold_map mk_code ps gr;
    4.34 +            val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    4.35 +            val (pargs, gr3) = fold_map
    4.36 +              (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    4.37            in
    4.38 -            SOME (gr3, Codegen.mk_app brack
    4.39 +            SOME (Codegen.mk_app brack
    4.40                (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
    4.41                    (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    4.42                      [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
    4.43                         Pretty.brk 1, pr]]) qs))),
    4.44                  Pretty.brk 1, Codegen.str "in ", pu,
    4.45 -                Pretty.brk 1, Codegen.str "end"])) pargs)
    4.46 +                Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
    4.47            end
    4.48      end
    4.49    | _ => NONE);
    4.50  
    4.51 -fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of
    4.52 +fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
    4.53      (t1 as Const ("split", _), t2 :: ts) =>
    4.54        (case strip_abs_split 1 (t1 $ t2) of
    4.55           ([p], u) =>
    4.56             let
    4.57 -             val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
    4.58 -             val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
    4.59 -             val (gr3, pargs) = foldl_map
    4.60 -               (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
    4.61 +             val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
    4.62 +             val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    4.63 +             val (pargs, gr3) = fold_map
    4.64 +               (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    4.65             in
    4.66 -             SOME (gr2, Codegen.mk_app brack
    4.67 +             SOME (Codegen.mk_app brack
    4.68                 (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
    4.69 -                 Pretty.brk 1, pu, Codegen.str ")"]) pargs)
    4.70 +                 Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
    4.71             end
    4.72         | _ => NONE)
    4.73    | _ => NONE);
     5.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 09 08:47:26 2008 +0200
     5.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 09 08:47:27 2008 +0200
     5.3 @@ -38,7 +38,7 @@
     5.4          (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
     5.5    in case xs of [] => NONE | x :: _ => SOME x end;
     5.6  
     5.7 -fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) sorts =
     5.8 +fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
     5.9    let
    5.10      val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    5.11      val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
    5.12 @@ -48,21 +48,20 @@
    5.13      val node_id = tname ^ " (type)";
    5.14      val module' = if_library (thyname_of_type thy tname) module;
    5.15  
    5.16 -    fun mk_dtdef gr prfx [] = (gr, [])
    5.17 -      | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
    5.18 +    fun mk_dtdef prfx [] gr = ([], gr)
    5.19 +      | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
    5.20            let
    5.21              val tvs = map DatatypeAux.dest_DtTFree dts;
    5.22              val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    5.23 -            val (gr', (_, type_id)) = mk_type_id module' tname gr;
    5.24 -            val (gr'', ps) =
    5.25 -              foldl_map (fn (gr, (cname, cargs)) =>
    5.26 -                foldl_map (invoke_tycodegen thy defs node_id module' false)
    5.27 -                  (gr, cargs) |>>>
    5.28 -                mk_const_id module' cname) (gr', cs');
    5.29 -            val (gr''', rest) = mk_dtdef gr'' "and " xs
    5.30 +            val ((_, type_id), gr') = mk_type_id module' tname gr;
    5.31 +            val (ps, gr'') = gr' |>
    5.32 +              fold_map (fn (cname, cargs) =>
    5.33 +                fold_map (invoke_tycodegen thy defs node_id module' false)
    5.34 +                  cargs ##>>
    5.35 +                mk_const_id module' cname) cs';
    5.36 +            val (rest, gr''') = mk_dtdef "and " xs gr''
    5.37            in
    5.38 -            (gr''',
    5.39 -             Pretty.block (str prfx ::
    5.40 +            (Pretty.block (str prfx ::
    5.41                 (if null tvs then [] else
    5.42                    [mk_tuple (map str tvs), str " "]) @
    5.43                 [str (type_id ^ " ="), Pretty.brk 1] @
    5.44 @@ -72,7 +71,7 @@
    5.45                      (if null ps' then [] else
    5.46                       List.concat ([str " of", Pretty.brk 1] ::
    5.47                         separate [str " *", Pretty.brk 1]
    5.48 -                         (map single ps'))))]) ps))) :: rest)
    5.49 +                         (map single ps'))))]) ps))) :: rest, gr''')
    5.50            end;
    5.51  
    5.52      fun mk_constr_term cname Ts T ps =
    5.53 @@ -92,9 +91,9 @@
    5.54                  str ("x" ^ string_of_int i)) (1 upto length Ts)
    5.55                in ("  | ", Pretty.blk (4,
    5.56                  [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    5.57 -                 if null Ts then str (snd (get_const_id cname gr))
    5.58 +                 if null Ts then str (snd (get_const_id gr cname))
    5.59                   else parens (Pretty.block
    5.60 -                   [str (snd (get_const_id cname gr)),
    5.61 +                   [str (snd (get_const_id gr cname)),
    5.62                      Pretty.brk 1, mk_tuple args]),
    5.63                   str " =", Pretty.brk 1] @
    5.64                   mk_constr_term cname Ts T
    5.65 @@ -129,7 +128,7 @@
    5.66                    (DatatypeProp.indexify_names (replicate (length dts) "x"));
    5.67                  val ts = map str
    5.68                    (DatatypeProp.indexify_names (replicate (length dts) "t"));
    5.69 -                val (_, id) = get_const_id cname gr
    5.70 +                val (_, id) = get_const_id gr cname
    5.71                in
    5.72                  mk_let
    5.73                    (map2 (fn p => fn q => mk_tuple [p, q]) xs ts ~~ gs)
    5.74 @@ -152,7 +151,7 @@
    5.75              val gs = maps (fn s =>
    5.76                let val s' = strip_tname s
    5.77                in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
    5.78 -            val gen_name = "gen_" ^ snd (get_type_id tname gr)
    5.79 +            val gen_name = "gen_" ^ snd (get_type_id gr tname)
    5.80  
    5.81            in
    5.82              Pretty.blk (4, separate (Pretty.brk 1) 
    5.83 @@ -186,12 +185,12 @@
    5.84            end
    5.85  
    5.86    in
    5.87 -    ((add_edge_acyclic (node_id, dep) gr
    5.88 +    (module', (add_edge_acyclic (node_id, dep) gr
    5.89          handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
    5.90           let
    5.91             val gr1 = add_edge (node_id, dep)
    5.92               (new_node (node_id, (NONE, "", "")) gr);
    5.93 -           val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
    5.94 +           val (dtdef, gr2) = mk_dtdef "datatype " descr' gr1 ;
    5.95           in
    5.96             map_node node_id (K (NONE, module',
    5.97               string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
    5.98 @@ -204,17 +203,16 @@
    5.99                  string_of (Pretty.blk (0, separate Pretty.fbrk
   5.100                    (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   5.101                else ""))) gr2
   5.102 -         end,
   5.103 -     module')
   5.104 +         end)
   5.105    end;
   5.106  
   5.107  
   5.108  (**** case expressions ****)
   5.109  
   5.110 -fun pretty_case thy defs gr dep module brack constrs (c as Const (_, T)) ts =
   5.111 +fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
   5.112    let val i = length constrs
   5.113    in if length ts <= i then
   5.114 -       invoke_codegen thy defs dep module brack (gr, eta_expand c ts (i+1))
   5.115 +       invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
   5.116      else
   5.117        let
   5.118          val ts1 = Library.take (i, ts);
   5.119 @@ -223,62 +221,62 @@
   5.120            (map (fst o fst o dest_Var) (foldr add_term_vars [] ts1)) ts1;
   5.121          val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
   5.122  
   5.123 -        fun pcase gr [] [] [] = ([], gr)
   5.124 -          | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
   5.125 +        fun pcase [] [] [] gr = ([], gr)
   5.126 +          | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
   5.127                let
   5.128                  val j = length cargs;
   5.129                  val xs = Name.variant_list names (replicate j "x");
   5.130                  val Us' = Library.take (j, fst (strip_type U));
   5.131                  val frees = map Free (xs ~~ Us');
   5.132 -                val (gr0, cp) = invoke_codegen thy defs dep module false
   5.133 -                  (gr, list_comb (Const (cname, Us' ---> dT), frees));
   5.134 +                val (cp, gr0) = invoke_codegen thy defs dep module false
   5.135 +                  (list_comb (Const (cname, Us' ---> dT), frees)) gr;
   5.136                  val t' = Envir.beta_norm (list_comb (t, frees));
   5.137 -                val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t');
   5.138 -                val (ps, gr2) = pcase gr1 cs ts Us;
   5.139 +                val (p, gr1) = invoke_codegen thy defs dep module false t' gr0;
   5.140 +                val (ps, gr2) = pcase cs ts Us gr1;
   5.141                in
   5.142                  ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
   5.143                end;
   5.144  
   5.145 -        val (ps1, gr1) = pcase gr constrs ts1 Ts;
   5.146 +        val (ps1, gr1) = pcase constrs ts1 Ts gr ;
   5.147          val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
   5.148 -        val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t);
   5.149 -        val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2)
   5.150 -      in (gr3, (if not (null ts2) andalso brack then parens else I)
   5.151 +        val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
   5.152 +        val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
   5.153 +      in ((if not (null ts2) andalso brack then parens else I)
   5.154          (Pretty.block (separate (Pretty.brk 1)
   5.155            (Pretty.block ([str "(case ", p, str " of",
   5.156 -             Pretty.brk 1] @ ps @ [str ")"]) :: ps2))))
   5.157 +             Pretty.brk 1] @ ps @ [str ")"]) :: ps2))), gr3)
   5.158        end
   5.159    end;
   5.160  
   5.161  
   5.162  (**** constructors ****)
   5.163  
   5.164 -fun pretty_constr thy defs gr dep module brack args (c as Const (s, T)) ts =
   5.165 +fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
   5.166    let val i = length args
   5.167    in if i > 1 andalso length ts < i then
   5.168 -      invoke_codegen thy defs dep module brack (gr, eta_expand c ts i)
   5.169 +      invoke_codegen thy defs dep module brack (eta_expand c ts i) gr
   5.170       else
   5.171         let
   5.172 -         val id = mk_qual_id module (get_const_id s gr);
   5.173 -         val (gr', ps) = foldl_map
   5.174 -           (invoke_codegen thy defs dep module (i = 1)) (gr, ts);
   5.175 +         val id = mk_qual_id module (get_const_id gr s);
   5.176 +         val (ps, gr') = fold_map
   5.177 +           (invoke_codegen thy defs dep module (i = 1)) ts gr;
   5.178         in (case args of
   5.179 -          _ :: _ :: _ => (gr', (if brack then parens else I)
   5.180 -            (Pretty.block [str id, Pretty.brk 1, mk_tuple ps]))
   5.181 -        | _ => (gr', mk_app brack (str id) ps))
   5.182 +          _ :: _ :: _ => (if brack then parens else I)
   5.183 +            (Pretty.block [str id, Pretty.brk 1, mk_tuple ps])
   5.184 +        | _ => (mk_app brack (str id) ps), gr')
   5.185         end
   5.186    end;
   5.187  
   5.188  
   5.189  (**** code generators for terms and types ****)
   5.190  
   5.191 -fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of
   5.192 +fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
   5.193     (c as Const (s, T), ts) =>
   5.194       (case DatatypePackage.datatype_of_case thy s of
   5.195          SOME {index, descr, ...} =>
   5.196            if is_some (get_assoc_code thy (s, T)) then NONE else
   5.197 -          SOME (pretty_case thy defs gr dep module brack
   5.198 -            (#3 (the (AList.lookup op = descr index))) c ts)
   5.199 +          SOME (pretty_case thy defs dep module brack
   5.200 +            (#3 (the (AList.lookup op = descr index))) c ts gr )
   5.201        | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
   5.202          (SOME {index, descr, ...}, (_, U as Type _)) =>
   5.203            if is_some (get_assoc_code thy (s, T)) then NONE else
   5.204 @@ -286,26 +284,24 @@
   5.205              (#3 (the (AList.lookup op = descr index))) s
   5.206            in
   5.207              SOME (pretty_constr thy defs
   5.208 -              (fst (invoke_tycodegen thy defs dep module false (gr, U)))
   5.209 -              dep module brack args c ts)
   5.210 +              dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
   5.211            end
   5.212        | _ => NONE)
   5.213   | _ => NONE);
   5.214  
   5.215 -fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   5.216 +fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   5.217        (case DatatypePackage.get_datatype thy s of
   5.218           NONE => NONE
   5.219         | SOME {descr, sorts, ...} =>
   5.220             if is_some (get_assoc_type thy s) then NONE else
   5.221             let
   5.222 -             val (gr', ps) = foldl_map
   5.223 -               (invoke_tycodegen thy defs dep module false) (gr, Ts);
   5.224 -             val (gr'', module') = add_dt_defs thy defs dep module gr' descr sorts;
   5.225 -             val (gr''', tyid) = mk_type_id module' s gr''
   5.226 -           in SOME (gr''',
   5.227 -             Pretty.block ((if null Ts then [] else
   5.228 +             val (ps, gr') = fold_map
   5.229 +               (invoke_tycodegen thy defs dep module false) Ts gr;
   5.230 +             val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
   5.231 +             val (tyid, gr''') = mk_type_id module' s gr''
   5.232 +           in SOME (Pretty.block ((if null Ts then [] else
   5.233                 [mk_tuple ps, str " "]) @
   5.234 -               [str (mk_qual_id module tyid)]))
   5.235 +               [str (mk_qual_id module tyid)]), gr''')
   5.236             end)
   5.237    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   5.238  
     6.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 09 08:47:26 2008 +0200
     6.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 09 08:47:27 2008 +0200
     6.3 @@ -302,11 +302,11 @@
     6.4    end;
     6.5  
     6.6  fun modename module s (iss, is) gr =
     6.7 -  let val (gr', id) = if s = "op =" then (gr, ("", "equal"))
     6.8 +  let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
     6.9      else mk_const_id module s gr
    6.10 -  in (gr', space_implode "__"
    6.11 +  in (space_implode "__"
    6.12      (mk_qual_id module id ::
    6.13 -      map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])))
    6.14 +      map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])), gr')
    6.15    end;
    6.16  
    6.17  fun mk_funcomp brack s k p = (if brack then parens else I)
    6.18 @@ -314,34 +314,34 @@
    6.19      separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @
    6.20      (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]);
    6.21  
    6.22 -fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) =
    6.23 -      apsnd single (invoke_codegen thy defs dep module brack (gr, t))
    6.24 -  | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
    6.25 -      (gr, [str name])
    6.26 -  | compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) =
    6.27 +fun compile_expr thy defs dep module brack modes (NONE, t) gr =
    6.28 +      apfst single (invoke_codegen thy defs dep module brack t gr)
    6.29 +  | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
    6.30 +      ([str name], gr)
    6.31 +  | compile_expr thy defs dep module brack modes (SOME (Mode (mode, _, ms)), t) gr =
    6.32        (case strip_comb t of
    6.33           (Const (name, _), args) =>
    6.34 -           if name = "op =" orelse AList.defined op = modes name then
    6.35 +           if name = @{const_name "op ="} orelse AList.defined op = modes name then
    6.36               let
    6.37                 val (args1, args2) = chop (length ms) args;
    6.38 -               val (gr', (ps, mode_id)) = foldl_map
    6.39 -                   (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
    6.40 -                 modename module name mode;
    6.41 -               val (gr'', ps') = (case mode of
    6.42 -                   ([], []) => (gr', [str "()"])
    6.43 -                 | _ => foldl_map
    6.44 -                     (invoke_codegen thy defs dep module true) (gr', args2))
    6.45 -             in (gr', (if brack andalso not (null ps andalso null ps') then
    6.46 +               val ((ps, mode_id), gr') = gr |> fold_map
    6.47 +                   (compile_expr thy defs dep module true modes) (ms ~~ args1)
    6.48 +                   ||>> modename module name mode;
    6.49 +               val (ps', gr'') = (case mode of
    6.50 +                   ([], []) => ([str "()"], gr')
    6.51 +                 | _ => fold_map
    6.52 +                     (invoke_codegen thy defs dep module true) args2 gr')
    6.53 +             in ((if brack andalso not (null ps andalso null ps') then
    6.54                 single o parens o Pretty.block else I)
    6.55                   (List.concat (separate [Pretty.brk 1]
    6.56 -                   ([str mode_id] :: ps @ map single ps'))))
    6.57 +                   ([str mode_id] :: ps @ map single ps'))), gr')
    6.58               end
    6.59 -           else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    6.60 -             (invoke_codegen thy defs dep module true (gr, t))
    6.61 -       | _ => apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    6.62 -           (invoke_codegen thy defs dep module true (gr, t)));
    6.63 +           else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    6.64 +             (invoke_codegen thy defs dep module true t gr)
    6.65 +       | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    6.66 +           (invoke_codegen thy defs dep module true t gr));
    6.67  
    6.68 -fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) inp =
    6.69 +fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
    6.70    let
    6.71      val modes' = modes @ List.mapPartial
    6.72        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
    6.73 @@ -352,32 +352,32 @@
    6.74          let val s = Name.variant names "x";
    6.75          in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
    6.76  
    6.77 -    fun compile_eq (gr, (s, t)) =
    6.78 -      apsnd (Pretty.block o cons (str (s ^ " = ")) o single)
    6.79 -        (invoke_codegen thy defs dep module false (gr, t));
    6.80 +    fun compile_eq (s, t) gr =
    6.81 +      apfst (Pretty.block o cons (str (s ^ " = ")) o single)
    6.82 +        (invoke_codegen thy defs dep module false t gr);
    6.83  
    6.84      val (in_ts, out_ts) = get_args is 1 ts;
    6.85      val ((all_vs', eqs), in_ts') =
    6.86        foldl_map check_constrt ((all_vs, []), in_ts);
    6.87  
    6.88 -    fun compile_prems out_ts' vs names gr [] =
    6.89 +    fun compile_prems out_ts' vs names [] gr =
    6.90            let
    6.91 -            val (gr2, out_ps) = foldl_map
    6.92 -              (invoke_codegen thy defs dep module false) (gr, out_ts);
    6.93 -            val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
    6.94 +            val (out_ps, gr2) = fold_map
    6.95 +              (invoke_codegen thy defs dep module false) out_ts gr;
    6.96 +            val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
    6.97              val ((names', eqs'), out_ts'') =
    6.98                foldl_map check_constrt ((names, []), out_ts');
    6.99              val (nvs, out_ts''') = foldl_map distinct_v
   6.100                ((names', map (fn x => (x, [x])) vs), out_ts'');
   6.101 -            val (gr4, out_ps') = foldl_map
   6.102 -              (invoke_codegen thy defs dep module false) (gr3, out_ts''');
   6.103 -            val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
   6.104 +            val (out_ps', gr4) = fold_map
   6.105 +              (invoke_codegen thy defs dep module false) (out_ts''') gr3;
   6.106 +            val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
   6.107            in
   6.108 -            (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
   6.109 +            (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
   6.110                (Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
   6.111 -              (exists (not o is_exhaustive) out_ts'''))
   6.112 +              (exists (not o is_exhaustive) out_ts'''), gr5)
   6.113            end
   6.114 -      | compile_prems out_ts vs names gr ps =
   6.115 +      | compile_prems out_ts vs names ps gr =
   6.116            let
   6.117              val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
   6.118              val SOME (p, mode as SOME (Mode (_, js, _))) =
   6.119 @@ -387,77 +387,77 @@
   6.120                foldl_map check_constrt ((names, []), out_ts);
   6.121              val (nvs, out_ts'') = foldl_map distinct_v
   6.122                ((names', map (fn x => (x, [x])) vs), out_ts');
   6.123 -            val (gr0, out_ps) = foldl_map
   6.124 -              (invoke_codegen thy defs dep module false) (gr, out_ts'');
   6.125 -            val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
   6.126 +            val (out_ps, gr0) = fold_map
   6.127 +              (invoke_codegen thy defs dep module false) out_ts'' gr;
   6.128 +            val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
   6.129            in
   6.130              (case p of
   6.131                 Prem (us, t, is_set) =>
   6.132                   let
   6.133                     val (in_ts, out_ts''') = get_args js 1 us;
   6.134 -                   val (gr2, in_ps) = foldl_map
   6.135 -                     (invoke_codegen thy defs dep module true) (gr1, in_ts);
   6.136 -                   val (gr3, ps) =
   6.137 +                   val (in_ps, gr2) = fold_map
   6.138 +                     (invoke_codegen thy defs dep module true) in_ts gr1;
   6.139 +                   val (ps, gr3) =
   6.140                       if not is_set then
   6.141 -                       apsnd (fn ps => ps @
   6.142 +                       apfst (fn ps => ps @
   6.143                             (if null in_ps then [] else [Pretty.brk 1]) @
   6.144                             separate (Pretty.brk 1) in_ps)
   6.145                           (compile_expr thy defs dep module false modes
   6.146 -                           (gr2, (mode, t)))
   6.147 +                           (mode, t) gr2)
   6.148                       else
   6.149 -                       apsnd (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
   6.150 -                           (invoke_codegen thy defs dep module true (gr2, t));
   6.151 -                   val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   6.152 +                       apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
   6.153 +                           (invoke_codegen thy defs dep module true t gr2);
   6.154 +                   val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
   6.155                   in
   6.156 -                   (gr4, compile_match (snd nvs) eq_ps out_ps
   6.157 +                   (compile_match (snd nvs) eq_ps out_ps
   6.158                        (Pretty.block (ps @
   6.159                           [str " :->", Pretty.brk 1, rest]))
   6.160 -                      (exists (not o is_exhaustive) out_ts''))
   6.161 +                      (exists (not o is_exhaustive) out_ts''), gr4)
   6.162                   end
   6.163               | Sidecond t =>
   6.164                   let
   6.165 -                   val (gr2, side_p) = invoke_codegen thy defs dep module true (gr1, t);
   6.166 -                   val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
   6.167 +                   val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1;
   6.168 +                   val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
   6.169                   in
   6.170 -                   (gr3, compile_match (snd nvs) eq_ps out_ps
   6.171 +                   (compile_match (snd nvs) eq_ps out_ps
   6.172                        (Pretty.block [str "?? ", side_p,
   6.173                          str " :->", Pretty.brk 1, rest])
   6.174 -                      (exists (not o is_exhaustive) out_ts''))
   6.175 +                      (exists (not o is_exhaustive) out_ts''), gr3)
   6.176                   end)
   6.177            end;
   6.178  
   6.179 -    val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
   6.180 +    val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ;
   6.181    in
   6.182 -    (gr', Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
   6.183 -       str " :->", Pretty.brk 1, prem_p])
   6.184 +    (Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
   6.185 +       str " :->", Pretty.brk 1, prem_p], gr')
   6.186    end;
   6.187  
   6.188 -fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
   6.189 +fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr =
   6.190    let
   6.191      val xs = map str (Name.variant_list arg_vs
   6.192        (map (fn i => "x" ^ string_of_int i) (snd mode)));
   6.193 -    val (gr', (cl_ps, mode_id)) =
   6.194 -      foldl_map (fn (gr, cl) => compile_clause thy defs
   6.195 -        gr dep module all_vs arg_vs modes mode cl (mk_tuple xs)) (gr, cls) |>>>
   6.196 +    val ((cl_ps, mode_id), gr') = gr |>
   6.197 +      fold_map (fn cl => compile_clause thy defs
   6.198 +        dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>>
   6.199        modename module s mode
   6.200    in
   6.201 -    ((gr', "and "), Pretty.block
   6.202 +    (Pretty.block
   6.203        ([Pretty.block (separate (Pretty.brk 1)
   6.204           (str (prfx ^ mode_id) ::
   6.205             map str arg_vs @
   6.206             (case mode of ([], []) => [str "()"] | _ => xs)) @
   6.207           [str " ="]),
   6.208          Pretty.brk 1] @
   6.209 -       List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))))
   6.210 +       List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
   6.211    end;
   6.212  
   6.213 -fun compile_preds thy defs gr dep module all_vs arg_vs modes preds =
   6.214 -  let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
   6.215 -    foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
   6.216 -      dep module prfx' all_vs arg_vs modes s cls mode)
   6.217 -        ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
   6.218 +fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
   6.219 +  let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
   6.220 +    fold_map (fn mode => fn (gr', prfx') => compile_pred thy defs
   6.221 +      dep module prfx' all_vs arg_vs modes s cls mode gr')
   6.222 +        (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
   6.223    in
   6.224 -    (gr', space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n")
   6.225 +    (space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n", gr')
   6.226    end;
   6.227  
   6.228  (**** processing of introduction rules ****)
   6.229 @@ -543,8 +543,8 @@
   6.230          (infer_modes thy extra_modes arities arg_vs clauses);
   6.231        val _ = print_arities arities;
   6.232        val _ = print_modes modes;
   6.233 -      val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs)
   6.234 -        arg_vs (modes @ extra_modes) clauses;
   6.235 +      val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs)
   6.236 +        arg_vs (modes @ extra_modes) clauses gr';
   6.237      in
   6.238        (map_node (hd names)
   6.239          (K (SOME (Modes (modes, arities)), module, s)) gr'')
   6.240 @@ -556,7 +556,7 @@
   6.241         ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   6.242     | mode => mode);
   6.243  
   6.244 -fun mk_ind_call thy defs gr dep module is_query s T ts names thyname k intrs =
   6.245 +fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr =
   6.246    let
   6.247      val (ts1, ts2) = chop k ts;
   6.248      val u = list_comb (Const (s, T), ts1);
   6.249 @@ -574,13 +574,11 @@
   6.250          fst (Library.foldl mk_mode ((([], []), 1), ts2))
   6.251        else (ts2, 1 upto length (binder_types T) - k);
   6.252      val mode = find_mode gr1 dep s u modes is;
   6.253 -    val (gr2, in_ps) = foldl_map
   6.254 -      (invoke_codegen thy defs dep module true) (gr1, ts');
   6.255 -    val (gr3, ps) =
   6.256 -      compile_expr thy defs dep module false modes (gr2, (mode, u))
   6.257 +    val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1;
   6.258 +    val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
   6.259    in
   6.260 -    (gr3, Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
   6.261 -       separate (Pretty.brk 1) in_ps))
   6.262 +    (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
   6.263 +       separate (Pretty.brk 1) in_ps), gr3)
   6.264    end;
   6.265  
   6.266  fun clause_of_eqn eqn =
   6.267 @@ -602,8 +600,8 @@
   6.268        val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
   6.269          (HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
   6.270        val mode = 1 upto arity;
   6.271 -      val (gr', (fun_id, mode_id)) = gr |>
   6.272 -        mk_const_id module' name |>>>
   6.273 +      val ((fun_id, mode_id), gr') = gr |>
   6.274 +        mk_const_id module' name ||>>
   6.275          modename module' pname ([], mode);
   6.276        val vars = map (fn i => str ("x" ^ string_of_int i)) mode;
   6.277        val s = string_of (Pretty.block
   6.278 @@ -617,9 +615,9 @@
   6.279        val (modes, _) = lookup_modes gr'' dep;
   6.280        val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop
   6.281          (Logic.strip_imp_concl (hd clauses)))) modes mode
   6.282 -    in (gr'', mk_qual_id module fun_id) end
   6.283 +    in (mk_qual_id module fun_id, gr'') end
   6.284    | SOME _ =>
   6.285 -      (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
   6.286 +      (mk_qual_id module (get_const_id gr name), add_edge (name, dep) gr);
   6.287  
   6.288  (* convert n-tuple to nested pairs *)
   6.289  
   6.290 @@ -644,7 +642,7 @@
   6.291      else p
   6.292    end;
   6.293  
   6.294 -fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
   6.295 +fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
   6.296      (Const ("Collect", _), [u]) =>
   6.297        let val (r, Ts, fs) = HOLogic.strip_split u
   6.298        in case strip_comb r of
   6.299 @@ -661,11 +659,11 @@
   6.300                    if null (duplicates op = ots) andalso
   6.301                      no_loose ts1 andalso no_loose its
   6.302                    then
   6.303 -                    let val (gr', call_p) = mk_ind_call thy defs gr dep module true
   6.304 -                      s T (ts1 @ ts2') names thyname k intrs
   6.305 -                    in SOME (gr', (if brack then parens else I) (Pretty.block
   6.306 +                    let val (call_p, gr') = mk_ind_call thy defs dep module true
   6.307 +                      s T (ts1 @ ts2') names thyname k intrs gr 
   6.308 +                    in SOME ((if brack then parens else I) (Pretty.block
   6.309                        [str "DSeq.list_of", Pretty.brk 1, str "(",
   6.310 -                       conv_ntuple fs ots call_p, str ")"]))
   6.311 +                       conv_ntuple fs ots call_p, str ")"]), gr')
   6.312                      end
   6.313                    else NONE
   6.314                  end
   6.315 @@ -676,21 +674,21 @@
   6.316        NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
   6.317          (SOME (names, thyname, k, intrs), NONE) =>
   6.318            if length ts < k then NONE else SOME
   6.319 -            (let val (gr', call_p) = mk_ind_call thy defs gr dep module false
   6.320 -               s T (map Term.no_dummy_patterns ts) names thyname k intrs
   6.321 -             in (gr', mk_funcomp brack "?!"
   6.322 -               (length (binder_types T) - length ts) (parens call_p))
   6.323 -             end handle TERM _ => mk_ind_call thy defs gr dep module true
   6.324 -               s T ts names thyname k intrs)
   6.325 +            (let val (call_p, gr') = mk_ind_call thy defs dep module false
   6.326 +               s T (map Term.no_dummy_patterns ts) names thyname k intrs gr
   6.327 +             in (mk_funcomp brack "?!"
   6.328 +               (length (binder_types T) - length ts) (parens call_p), gr')
   6.329 +             end handle TERM _ => mk_ind_call thy defs dep module true
   6.330 +               s T ts names thyname k intrs gr )
   6.331        | _ => NONE)
   6.332      | SOME eqns =>
   6.333          let
   6.334            val (_, thyname) :: _ = eqns;
   6.335 -          val (gr', id) = mk_fun thy defs s (preprocess thy (map fst (rev eqns)))
   6.336 +          val (id, gr') = mk_fun thy defs s (preprocess thy (map fst (rev eqns)))
   6.337              dep module (if_library thyname module) gr;
   6.338 -          val (gr'', ps) = foldl_map
   6.339 -            (invoke_codegen thy defs dep module true) (gr', ts);
   6.340 -        in SOME (gr'', mk_app brack (str id) ps)
   6.341 +          val (ps, gr'') = fold_map
   6.342 +            (invoke_codegen thy defs dep module true) ts gr';
   6.343 +        in SOME (mk_app brack (str id) ps, gr'')
   6.344          end)
   6.345    | _ => NONE);
   6.346  
     7.1 --- a/src/HOL/Tools/typedef_codegen.ML	Thu Oct 09 08:47:26 2008 +0200
     7.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Thu Oct 09 08:47:27 2008 +0200
     7.3 @@ -13,17 +13,17 @@
     7.4  structure TypedefCodegen: TYPEDEF_CODEGEN =
     7.5  struct
     7.6  
     7.7 -fun typedef_codegen thy defs gr dep module brack t =
     7.8 +fun typedef_codegen thy defs dep module brack t gr =
     7.9    let
    7.10      fun get_name (Type (tname, _)) = tname
    7.11        | get_name _ = "";
    7.12      fun mk_fun s T ts =
    7.13        let
    7.14 -        val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
    7.15 -        val (gr'', ps) =
    7.16 -          foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    7.17 -        val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    7.18 -      in SOME (gr'', Codegen.mk_app brack (Codegen.str id) ps) end;
    7.19 +        val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
    7.20 +        val (ps, gr'') =
    7.21 +          fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
    7.22 +        val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
    7.23 +      in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
    7.24      fun lookup f T =
    7.25        (case TypedefPackage.get_info thy (get_name T) of
    7.26          NONE => ""
    7.27 @@ -45,7 +45,7 @@
    7.28    | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
    7.29    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    7.30  
    7.31 -fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    7.32 +fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    7.33        (case TypedefPackage.get_info thy s of
    7.34           NONE => NONE
    7.35         | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
    7.36 @@ -54,20 +54,20 @@
    7.37               val module' = Codegen.if_library
    7.38                 (Codegen.thyname_of_type thy tname) module;
    7.39               val node_id = tname ^ " (type)";
    7.40 -             val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    7.41 +             val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
    7.42                   (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    7.43 -                   (gr, Ts) |>>>
    7.44 -               Codegen.mk_const_id module' Abs_name |>>>
    7.45 -               Codegen.mk_const_id module' Rep_name |>>>
    7.46 +                   Ts ||>>
    7.47 +               Codegen.mk_const_id module' Abs_name ||>>
    7.48 +               Codegen.mk_const_id module' Rep_name ||>>
    7.49                 Codegen.mk_type_id module' s;
    7.50               val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    7.51 -           in SOME (case try (Codegen.get_node gr') node_id of
    7.52 +           in SOME (tyexpr, case try (Codegen.get_node gr') node_id of
    7.53                 NONE =>
    7.54                 let
    7.55 -                 val (gr'', p :: ps) = foldl_map
    7.56 +                 val (p :: ps, gr'') = fold_map
    7.57                     (Codegen.invoke_tycodegen thy defs node_id module' false)
    7.58 -                   (Codegen.add_edge (node_id, dep)
    7.59 -                      (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
    7.60 +                   (oldT :: Us) (Codegen.add_edge (node_id, dep)
    7.61 +                      (Codegen.new_node (node_id, (NONE, "", "")) gr'));
    7.62                   val s =
    7.63                     Codegen.string_of (Pretty.block [Codegen.str "datatype ",
    7.64                       mk_tyexpr ps (snd ty_id),
    7.65 @@ -96,9 +96,9 @@
    7.66                            Codegen.str "i);"]]) ^ "\n\n"
    7.67                      else "")
    7.68                 in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
    7.69 -             | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
    7.70 +             | SOME _ => Codegen.add_edge (node_id, dep) gr')
    7.71             end)
    7.72 -  | typedef_tycodegen thy defs gr dep module brack _ = NONE;
    7.73 +  | typedef_tycodegen thy defs dep module brack _ gr = NONE;
    7.74  
    7.75  val setup =
    7.76    Codegen.add_codegen "typedef" typedef_codegen
     8.1 --- a/src/Pure/codegen.ML	Thu Oct 09 08:47:26 2008 +0200
     8.2 +++ b/src/Pure/codegen.ML	Thu Oct 09 08:47:27 2008 +0200
     8.3 @@ -48,15 +48,15 @@
     8.4      (typ mixfix list * (string * string) list) option
     8.5    val codegen_error: codegr -> string -> string -> 'a
     8.6    val invoke_codegen: theory -> deftab -> string -> string -> bool ->
     8.7 -    codegr * term -> codegr * Pretty.T
     8.8 +    term -> codegr -> Pretty.T * codegr
     8.9    val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    8.10 -    codegr * typ -> codegr * Pretty.T
    8.11 +    typ -> codegr -> Pretty.T * codegr
    8.12    val mk_id: string -> string
    8.13    val mk_qual_id: string -> string * string -> string
    8.14 -  val mk_const_id: string -> string -> codegr -> codegr * (string * string)
    8.15 -  val get_const_id: string -> codegr -> string * string
    8.16 -  val mk_type_id: string -> string -> codegr -> codegr * (string * string)
    8.17 -  val get_type_id: string -> codegr -> string * string
    8.18 +  val mk_const_id: string -> string -> codegr -> (string * string) * codegr
    8.19 +  val get_const_id: codegr -> string -> string * string
    8.20 +  val mk_type_id: string -> string -> codegr -> (string * string) * codegr
    8.21 +  val get_type_id: codegr -> string -> string * string
    8.22    val thyname_of_type: theory -> string -> string
    8.23    val thyname_of_const: theory -> string -> string
    8.24    val rename_terms: term list -> term list
    8.25 @@ -175,12 +175,12 @@
    8.26  type 'a codegen =
    8.27    theory ->    (* theory in which generate_code was called *)
    8.28    deftab ->    (* definition table (for efficiency) *)
    8.29 -  codegr ->    (* code dependency graph *)
    8.30    string ->    (* node name of caller (for recording dependencies) *)
    8.31    string ->    (* module name of caller (for modular code generation) *)
    8.32    bool ->      (* whether to parenthesize generated expression *)
    8.33    'a ->        (* item to generate code from *)
    8.34 -  (codegr * Pretty.T) option;
    8.35 +  codegr ->    (* code dependency graph *)
    8.36 +  (Pretty.T * codegr) option;
    8.37  
    8.38  (* parameters for random testing *)
    8.39  
    8.40 @@ -452,9 +452,9 @@
    8.41      val ((module, s), tab1') = mk_long_id tab1 module cname
    8.42      val s' = mk_id s;
    8.43      val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
    8.44 -  in ((gr, (tab1', tab2)), (module, s'')) end;
    8.45 +  in (((module, s'')), (gr, (tab1', tab2))) end;
    8.46  
    8.47 -fun get_const_id cname (gr, (tab1, tab2)) =
    8.48 +fun get_const_id (gr, (tab1, tab2)) cname =
    8.49    case Symtab.lookup (fst tab1) cname of
    8.50      NONE => error ("get_const_id: no such constant: " ^ quote cname)
    8.51    | SOME (module, s) =>
    8.52 @@ -468,9 +468,9 @@
    8.53      val ((module, s), tab2') = mk_long_id tab2 module tyname
    8.54      val s' = mk_id s;
    8.55      val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
    8.56 -  in ((gr, (tab1, tab2')), (module, s'')) end;
    8.57 +  in ((module, s''), (gr, (tab1, tab2'))) end;
    8.58  
    8.59 -fun get_type_id tyname (gr, (tab1, tab2)) =
    8.60 +fun get_type_id (gr, (tab1, tab2)) tyname =
    8.61    case Symtab.lookup (fst tab2) tyname of
    8.62      NONE => error ("get_type_id: no such type: " ^ quote tyname)
    8.63    | SOME (module, s) =>
    8.64 @@ -479,7 +479,7 @@
    8.65          val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
    8.66        in (module, s'') end;
    8.67  
    8.68 -fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab);
    8.69 +fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname);
    8.70  
    8.71  fun get_node (gr, x) k = Graph.get_node gr k;
    8.72  fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
    8.73 @@ -569,14 +569,14 @@
    8.74  fun codegen_error (gr, _) dep s =
    8.75    error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
    8.76  
    8.77 -fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
    8.78 -   (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
    8.79 +fun invoke_codegen thy defs dep module brack t gr = (case get_first
    8.80 +   (fn (_, f) => f thy defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
    8.81        NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
    8.82          Syntax.string_of_term_global thy t)
    8.83      | SOME x => x);
    8.84  
    8.85 -fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
    8.86 -   (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
    8.87 +fun invoke_tycodegen thy defs dep module brack T gr = (case get_first
    8.88 +   (fn (_, f) => f thy defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
    8.89        NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
    8.90          Syntax.string_of_typ_global thy T)
    8.91      | SOME x => x);
    8.92 @@ -643,39 +643,39 @@
    8.93  
    8.94  fun if_library x y = if member (op =) (!mode) "library" then x else y;
    8.95  
    8.96 -fun default_codegen thy defs gr dep module brack t =
    8.97 +fun default_codegen thy defs dep module brack t gr =
    8.98    let
    8.99      val (u, ts) = strip_comb t;
   8.100 -    fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack)
   8.101 +    fun codegens brack = fold_map (invoke_codegen thy defs dep module brack)
   8.102    in (case u of
   8.103        Var ((s, i), T) =>
   8.104          let
   8.105 -          val (gr', ps) = codegens true (gr, ts);
   8.106 -          val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
   8.107 -        in SOME (gr'', mk_app brack (str (s ^
   8.108 -           (if i=0 then "" else string_of_int i))) ps)
   8.109 +          val (ps, gr') = codegens true ts gr;
   8.110 +          val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
   8.111 +        in SOME (mk_app brack (str (s ^
   8.112 +           (if i=0 then "" else string_of_int i))) ps, gr'')
   8.113          end
   8.114  
   8.115      | Free (s, T) =>
   8.116          let
   8.117 -          val (gr', ps) = codegens true (gr, ts);
   8.118 -          val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
   8.119 -        in SOME (gr'', mk_app brack (str s) ps) end
   8.120 +          val (ps, gr') = codegens true ts gr;
   8.121 +          val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
   8.122 +        in SOME (mk_app brack (str s) ps, gr'') end
   8.123  
   8.124      | Const (s, T) =>
   8.125        (case get_assoc_code thy (s, T) of
   8.126           SOME (ms, aux) =>
   8.127             let val i = num_args_of ms
   8.128             in if length ts < i then
   8.129 -               default_codegen thy defs gr dep module brack (eta_expand u ts i)
   8.130 +               default_codegen thy defs dep module brack (eta_expand u ts i) gr 
   8.131               else
   8.132                 let
   8.133                   val (ts1, ts2) = args_of ms ts;
   8.134 -                 val (gr1, ps1) = codegens false (gr, ts1);
   8.135 -                 val (gr2, ps2) = codegens true (gr1, ts2);
   8.136 -                 val (gr3, ps3) = codegens false (gr2, quotes_of ms);
   8.137 -                 val (gr4, _) = invoke_tycodegen thy defs dep module false
   8.138 -                   (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
   8.139 +                 val (ps1, gr1) = codegens false ts1 gr;
   8.140 +                 val (ps2, gr2) = codegens true ts2 gr1;
   8.141 +                 val (ps3, gr3) = codegens false (quotes_of ms) gr2;
   8.142 +                 val (_, gr4) = invoke_tycodegen thy defs dep module false
   8.143 +                   (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
   8.144                   val (module', suffix) = (case get_defn thy defs s T of
   8.145                       NONE => (if_library (thyname_of_const thy s) module, "")
   8.146                     | SOME ((U, (module', _)), NONE) =>
   8.147 @@ -687,12 +687,11 @@
   8.148                     (pretty_mixfix module module' ms ps1 ps3)) ps2
   8.149                 in SOME (case try (get_node gr4) node_id of
   8.150                     NONE => (case get_aux_code aux of
   8.151 -                       [] => (gr4, p module)
   8.152 -                     | xs => (add_edge (node_id, dep) (new_node
   8.153 -                         (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4),
   8.154 -                           p module'))
   8.155 +                       [] => (p module, gr4)
   8.156 +                     | xs => (p module', add_edge (node_id, dep) (new_node
   8.157 +                         (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
   8.158                   | SOME (_, module'', _) =>
   8.159 -                     (add_edge (node_id, dep) gr4, p module''))
   8.160 +                     (p module'', add_edge (node_id, dep) gr4))
   8.161                 end
   8.162             end
   8.163         | NONE => (case get_defn thy defs s T of
   8.164 @@ -702,8 +701,8 @@
   8.165                 val module' = if_library thyname module;
   8.166                 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
   8.167                 val node_id = s ^ suffix;
   8.168 -               val (gr', (ps, def_id)) = codegens true (gr, ts) |>>>
   8.169 -                 mk_const_id module' (s ^ suffix);
   8.170 +               val ((ps, def_id), gr') = gr |> codegens true ts
   8.171 +                 ||>> mk_const_id module' (s ^ suffix);
   8.172                 val p = mk_app brack (str (mk_qual_id module def_id)) ps
   8.173               in SOME (case try (get_node gr') node_id of
   8.174                   NONE =>
   8.175 @@ -714,21 +713,20 @@
   8.176                         if not (null args) orelse null Ts then (args, rhs) else
   8.177                           let val v = Free (new_name rhs "x", hd Ts)
   8.178                           in ([v], betapply (rhs, v)) end;
   8.179 -                     val (gr1, p') = invoke_codegen thy defs node_id module' false
   8.180 -                       (add_edge (node_id, dep)
   8.181 -                          (new_node (node_id, (NONE, "", "")) gr'), rhs');
   8.182 -                     val (gr2, xs) = codegens false (gr1, args');
   8.183 -                     val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T);
   8.184 -                     val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U);
   8.185 -                   in (map_node node_id (K (NONE, module', string_of
   8.186 +                     val (p', gr1) = invoke_codegen thy defs node_id module' false
   8.187 +                       rhs' (add_edge (node_id, dep)
   8.188 +                          (new_node (node_id, (NONE, "", "")) gr'));
   8.189 +                     val (xs, gr2) = codegens false args' gr1;
   8.190 +                     val (_, gr3) = invoke_tycodegen thy defs dep module false T gr2;
   8.191 +                     val (ty, gr4) = invoke_tycodegen thy defs node_id module' false U gr3;
   8.192 +                   in (p, map_node node_id (K (NONE, module', string_of
   8.193                         (Pretty.block (separate (Pretty.brk 1)
   8.194                           (if null args' then
   8.195                              [str ("val " ^ snd def_id ^ " :"), ty]
   8.196                            else str ("fun " ^ snd def_id) :: xs) @
   8.197 -                        [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4,
   8.198 -                     p)
   8.199 +                        [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
   8.200                     end
   8.201 -               | SOME _ => (add_edge (node_id, dep) gr', p))
   8.202 +               | SOME _ => (p, add_edge (node_id, dep) gr'))
   8.203               end))
   8.204  
   8.205      | Abs _ =>
   8.206 @@ -736,44 +734,43 @@
   8.207          val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
   8.208          val t = strip_abs_body u
   8.209          val bs' = new_names t bs;
   8.210 -        val (gr1, ps) = codegens true (gr, ts);
   8.211 -        val (gr2, p) = invoke_codegen thy defs dep module false
   8.212 -          (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
   8.213 +        val (ps, gr1) = codegens true ts gr;
   8.214 +        val (p, gr2) = invoke_codegen thy defs dep module false
   8.215 +          (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
   8.216        in
   8.217 -        SOME (gr2, mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
   8.218 -          [str ")"])) ps)
   8.219 +        SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
   8.220 +          [str ")"])) ps, gr2)
   8.221        end
   8.222  
   8.223      | _ => NONE)
   8.224    end;
   8.225  
   8.226 -fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
   8.227 -      SOME (gr, str (s ^ (if i = 0 then "" else string_of_int i)))
   8.228 -  | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
   8.229 -      SOME (gr, str s)
   8.230 -  | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   8.231 +fun default_tycodegen thy defs dep module brack (TVar ((s, i), _)) gr =
   8.232 +      SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
   8.233 +  | default_tycodegen thy defs dep module brack (TFree (s, _)) gr =
   8.234 +      SOME (str s, gr)
   8.235 +  | default_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   8.236        (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
   8.237           NONE => NONE
   8.238         | SOME (ms, aux) =>
   8.239             let
   8.240 -             val (gr', ps) = foldl_map
   8.241 +             val (ps, gr') = fold_map
   8.242                 (invoke_tycodegen thy defs dep module false)
   8.243 -               (gr, fst (args_of ms Ts));
   8.244 -             val (gr'', qs) = foldl_map
   8.245 +               (fst (args_of ms Ts)) gr;
   8.246 +             val (qs, gr'') = fold_map
   8.247                 (invoke_tycodegen thy defs dep module false)
   8.248 -               (gr', quotes_of ms);
   8.249 +               (quotes_of ms) gr';
   8.250               val module' = if_library (thyname_of_type thy s) module;
   8.251               val node_id = s ^ " (type)";
   8.252               fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
   8.253             in SOME (case try (get_node gr'') node_id of
   8.254                 NONE => (case get_aux_code aux of
   8.255 -                   [] => (gr'', p module')
   8.256 -                 | xs => (fst (mk_type_id module' s
   8.257 +                   [] => (p module', gr'')
   8.258 +                 | xs => (p module', snd (mk_type_id module' s
   8.259                         (add_edge (node_id, dep) (new_node (node_id,
   8.260 -                         (NONE, module', cat_lines xs ^ "\n")) gr''))),
   8.261 -                     p module'))
   8.262 +                         (NONE, module', cat_lines xs ^ "\n")) gr'')))))
   8.263               | SOME (_, module'', _) =>
   8.264 -                 (add_edge (node_id, dep) gr'', p module''))
   8.265 +                 (p module'', add_edge (node_id, dep) gr''))
   8.266             end);
   8.267  
   8.268  fun mk_tuple [p] = p
   8.269 @@ -846,9 +843,9 @@
   8.270      fun expand (t as Abs _) = t
   8.271        | expand t = (case fastype_of t of
   8.272            Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
   8.273 -    val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   8.274 -      (invoke_codegen thy defs "<Top>" module false (gr, t)))
   8.275 -        (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs);
   8.276 +    val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
   8.277 +      (invoke_codegen thy defs "<Top>" module false t gr))
   8.278 +        (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
   8.279      val code = map_filter
   8.280        (fn ("", _) => NONE
   8.281          | (s', p) => SOME (string_of (Pretty.block
   8.282 @@ -891,7 +888,7 @@
   8.283    | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
   8.284        (Pretty.block (separate (Pretty.brk 1)
   8.285          (str (mk_qual_id module
   8.286 -          (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
   8.287 +          (get_type_id' (fn s' => "term_of_" ^ s') gr s)) ::
   8.288          maps (fn T =>
   8.289            [mk_term_of gr module true T, mk_type true T]) Ts)));
   8.290  
   8.291 @@ -903,7 +900,7 @@
   8.292    | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
   8.293    | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
   8.294        (Pretty.block (separate (Pretty.brk 1)
   8.295 -        (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
   8.296 +        (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^
   8.297            (if member (op =) xs s then "'" else "")) ::
   8.298           (case tyc of
   8.299              ("fun", [T, U]) =>