Replaced Pretty.str and Pretty.string_of by specific functions that
authorberghofe
Fri May 23 16:37:57 2008 +0200 (2008-05-23)
changeset 2697483adc1eaeaab
parent 26973 6d52187fc2a6
child 26975 103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions that
set print_mode and margin appropriately.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Fri May 23 16:10:25 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Fri May 23 16:37:57 2008 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4    val message : string -> unit
     1.5    val mode : string list ref
     1.6    val margin : int ref
     1.7 +  val string_of : Pretty.T -> string
     1.8 +  val str : string -> Pretty.T
     1.9  
    1.10    datatype 'a mixfix =
    1.11        Arg
    1.12 @@ -106,6 +108,12 @@
    1.13  
    1.14  val margin = ref 80;
    1.15  
    1.16 +fun string_of p = (Pretty.string_of |>
    1.17 +  PrintMode.setmp [] |>
    1.18 +  Pretty.setmp_margin (!margin)) p;
    1.19 +
    1.20 +val str = PrintMode.setmp [] Pretty.str;
    1.21 +
    1.22  (**** Mixfix syntax ****)
    1.23  
    1.24  datatype 'a mixfix =
    1.25 @@ -594,10 +602,10 @@
    1.26  
    1.27  (**** code generator for mixfix expressions ****)
    1.28  
    1.29 -fun parens p = Pretty.block [Pretty.str "(", p, Pretty.str ")"];
    1.30 +fun parens p = Pretty.block [str "(", p, str ")"];
    1.31  
    1.32  fun pretty_fn [] p = [p]
    1.33 -  | pretty_fn (x::xs) p = Pretty.str ("fn " ^ x ^ " =>") ::
    1.34 +  | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") ::
    1.35        Pretty.brk 1 :: pretty_fn xs p;
    1.36  
    1.37  fun pretty_mixfix _ _ [] [] _ = []
    1.38 @@ -607,7 +615,7 @@
    1.39        pretty_mixfix module module' ms ps qs
    1.40    | pretty_mixfix module module' (Module :: ms) ps qs =
    1.41        (if module <> module'
    1.42 -       then cons (Pretty.str (module' ^ ".")) else I)
    1.43 +       then cons (str (module' ^ ".")) else I)
    1.44        (pretty_mixfix module module' ms ps qs)
    1.45    | pretty_mixfix module module' (Pretty p :: ms) ps qs =
    1.46        p :: pretty_mixfix module module' ms ps qs
    1.47 @@ -641,8 +649,8 @@
    1.48  
    1.49  fun mk_app _ p [] = p
    1.50    | mk_app brack p ps = if brack then
    1.51 -       Pretty.block (Pretty.str "(" ::
    1.52 -         separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"])
    1.53 +       Pretty.block (str "(" ::
    1.54 +         separate (Pretty.brk 1) (p :: ps) @ [str ")"])
    1.55       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
    1.56  
    1.57  fun new_names t xs = Name.variant_list
    1.58 @@ -662,7 +670,7 @@
    1.59          let
    1.60            val (gr', ps) = codegens true (gr, ts);
    1.61            val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
    1.62 -        in SOME (gr'', mk_app brack (Pretty.str (s ^
    1.63 +        in SOME (gr'', mk_app brack (str (s ^
    1.64             (if i=0 then "" else string_of_int i))) ps)
    1.65          end
    1.66  
    1.67 @@ -670,7 +678,7 @@
    1.68          let
    1.69            val (gr', ps) = codegens true (gr, ts);
    1.70            val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
    1.71 -        in SOME (gr'', mk_app brack (Pretty.str s) ps) end
    1.72 +        in SOME (gr'', mk_app brack (str s) ps) end
    1.73  
    1.74      | Const (s, T) =>
    1.75        (case get_assoc_code thy (s, T) of
    1.76 @@ -714,7 +722,7 @@
    1.77                 val node_id = s ^ suffix;
    1.78                 val (gr', (ps, def_id)) = codegens true (gr, ts) |>>>
    1.79                   mk_const_id module' (s ^ suffix);
    1.80 -               val p = mk_app brack (Pretty.str (mk_qual_id module def_id)) ps
    1.81 +               val p = mk_app brack (str (mk_qual_id module def_id)) ps
    1.82               in SOME (case try (get_node gr') node_id of
    1.83                   NONE =>
    1.84                     let
    1.85 @@ -730,12 +738,12 @@
    1.86                       val (gr2, xs) = codegens false (gr1, args');
    1.87                       val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T);
    1.88                       val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U);
    1.89 -                   in (map_node node_id (K (NONE, module', Pretty.string_of
    1.90 +                   in (map_node node_id (K (NONE, module', string_of
    1.91                         (Pretty.block (separate (Pretty.brk 1)
    1.92                           (if null args' then
    1.93 -                            [Pretty.str ("val " ^ snd def_id ^ " :"), ty]
    1.94 -                          else Pretty.str ("fun " ^ snd def_id) :: xs) @
    1.95 -                        [Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4,
    1.96 +                            [str ("val " ^ snd def_id ^ " :"), ty]
    1.97 +                          else str ("fun " ^ snd def_id) :: xs) @
    1.98 +                        [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4,
    1.99                       p)
   1.100                     end
   1.101                 | SOME _ => (add_edge (node_id, dep) gr', p))
   1.102 @@ -750,17 +758,17 @@
   1.103          val (gr2, p) = invoke_codegen thy defs dep module false
   1.104            (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
   1.105        in
   1.106 -        SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @
   1.107 -          [Pretty.str ")"])) ps)
   1.108 +        SOME (gr2, mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
   1.109 +          [str ")"])) ps)
   1.110        end
   1.111  
   1.112      | _ => NONE)
   1.113    end;
   1.114  
   1.115  fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
   1.116 -      SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i)))
   1.117 +      SOME (gr, str (s ^ (if i = 0 then "" else string_of_int i)))
   1.118    | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
   1.119 -      SOME (gr, Pretty.str s)
   1.120 +      SOME (gr, str s)
   1.121    | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   1.122        (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
   1.123           NONE => NONE
   1.124 @@ -792,17 +800,17 @@
   1.125  
   1.126  
   1.127  fun mk_tuple [p] = p
   1.128 -  | mk_tuple ps = Pretty.block (Pretty.str "(" ::
   1.129 -      List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single ps)) @
   1.130 -        [Pretty.str ")"]);
   1.131 +  | mk_tuple ps = Pretty.block (str "(" ::
   1.132 +      List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @
   1.133 +        [str ")"]);
   1.134  
   1.135  fun mk_let bindings body =
   1.136 -  Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
   1.137 +  Pretty.blk (0, [str "let", Pretty.brk 1,
   1.138      Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
   1.139 -      Pretty.block [Pretty.str "val ", pat, Pretty.str " =", Pretty.brk 1,
   1.140 -      rhs, Pretty.str ";"]) bindings)),
   1.141 -    Pretty.brk 1, Pretty.str "in", Pretty.brk 1, body,
   1.142 -    Pretty.brk 1, Pretty.str "end"]);
   1.143 +      Pretty.block [str "val ", pat, str " =", Pretty.brk 1,
   1.144 +      rhs, str ";"]) bindings)),
   1.145 +    Pretty.brk 1, str "in", Pretty.brk 1, body,
   1.146 +    Pretty.brk 1, str "end"]);
   1.147  
   1.148  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
   1.149  
   1.150 @@ -842,8 +850,7 @@
   1.151      else [(module, implode (map (#3 o snd) code))]
   1.152    end;
   1.153  
   1.154 -fun gen_generate_code prep_term thy modules module =
   1.155 -  PrintMode.setmp [] (Pretty.setmp_margin (!margin) (fn xs =>
   1.156 +fun gen_generate_code prep_term thy modules module xs =
   1.157    let
   1.158      val _ = (module <> "" orelse
   1.159          member (op =) (!mode) "library" andalso forall (equal "" o fst) xs)
   1.160 @@ -867,8 +874,8 @@
   1.161          (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs);
   1.162      val code = map_filter
   1.163        (fn ("", _) => NONE
   1.164 -        | (s', p) => SOME (Pretty.string_of (Pretty.block
   1.165 -          [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps;
   1.166 +        | (s', p) => SOME (string_of (Pretty.block
   1.167 +          [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps;
   1.168      val code' = space_implode "\n\n" code ^ "\n\n";
   1.169      val code'' =
   1.170        map_filter (fn (name, s) =>
   1.171 @@ -880,7 +887,7 @@
   1.172             (output_code (fst gr') (if_library "" module) ["<Top>"]))
   1.173    in
   1.174      (code'', del_nodes ["<Top>"] gr')
   1.175 -  end));
   1.176 +  end;
   1.177  
   1.178  val generate_code_i = gen_generate_code Sign.cert_term;
   1.179  val generate_code = gen_generate_code Sign.read_term;
   1.180 @@ -890,23 +897,23 @@
   1.181  
   1.182  val strip_tname = implode o tl o explode;
   1.183  
   1.184 -fun pretty_list xs = Pretty.block (Pretty.str "[" ::
   1.185 -  flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
   1.186 -  [Pretty.str "]"]);
   1.187 +fun pretty_list xs = Pretty.block (str "[" ::
   1.188 +  flat (separate [str ",", Pretty.brk 1] (map single xs)) @
   1.189 +  [str "]"]);
   1.190  
   1.191 -fun mk_type p (TVar ((s, i), _)) = Pretty.str
   1.192 +fun mk_type p (TVar ((s, i), _)) = str
   1.193        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T")
   1.194 -  | mk_type p (TFree (s, _)) = Pretty.str (strip_tname s ^ "T")
   1.195 +  | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T")
   1.196    | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.197 -      [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
   1.198 -       Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
   1.199 +      [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","),
   1.200 +       Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]);
   1.201  
   1.202 -fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str
   1.203 +fun mk_term_of gr module p (TVar ((s, i), _)) = str
   1.204        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
   1.205 -  | mk_term_of gr module p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   1.206 +  | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F")
   1.207    | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
   1.208        (Pretty.block (separate (Pretty.brk 1)
   1.209 -        (Pretty.str (mk_qual_id module
   1.210 +        (str (mk_qual_id module
   1.211            (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
   1.212          maps (fn T =>
   1.213            [mk_term_of gr module true T, mk_type true T]) Ts)));
   1.214 @@ -914,12 +921,12 @@
   1.215  
   1.216  (**** Test data generators ****)
   1.217  
   1.218 -fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str
   1.219 +fun mk_gen gr module p xs a (TVar ((s, i), _)) = str
   1.220        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
   1.221 -  | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   1.222 +  | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
   1.223    | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
   1.224        (Pretty.block (separate (Pretty.brk 1)
   1.225 -        (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
   1.226 +        (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
   1.227            (if member (op =) xs s then "'" else "")) ::
   1.228           (case tyc of
   1.229              ("fun", [T, U]) =>
   1.230 @@ -927,7 +934,7 @@
   1.231                 mk_gen gr module true xs a U, mk_type true U]
   1.232            | _ => maps (fn T =>
   1.233                [mk_gen gr module true xs a T, mk_type true T]) Ts) @
   1.234 -         (if member (op =) xs s then [Pretty.str a] else []))));
   1.235 +         (if member (op =) xs s then [str a] else []))));
   1.236  
   1.237  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
   1.238  
   1.239 @@ -942,27 +949,27 @@
   1.240        map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
   1.241      val (code, gr) = setmp mode ["term_of", "test"]
   1.242        (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
   1.243 -    val s = PrintMode.setmp [] (fn () => "structure TestTerm =\nstruct\n\n" ^
   1.244 +    val s = "structure TestTerm =\nstruct\n\n" ^
   1.245        cat_lines (map snd code) ^
   1.246 -      "\nopen Generated;\n\n" ^ Pretty.string_of
   1.247 -        (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
   1.248 -          Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
   1.249 +      "\nopen Generated;\n\n" ^ string_of
   1.250 +        (Pretty.block [str "val () = Codegen.test_fn :=",
   1.251 +          Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
   1.252            mk_let (map (fn ((s, T), s') =>
   1.253 -              (mk_tuple [Pretty.str s', Pretty.str (s' ^ "_t")],
   1.254 +              (mk_tuple [str s', str (s' ^ "_t")],
   1.255                 Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
   1.256 -                 Pretty.str "i"])) frees')
   1.257 -            (Pretty.block [Pretty.str "if ",
   1.258 -              mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'),
   1.259 -              Pretty.brk 1, Pretty.str "then NONE",
   1.260 -              Pretty.brk 1, Pretty.str "else ",
   1.261 -              Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" ::
   1.262 -                flat (separate [Pretty.str ",", Pretty.brk 1]
   1.263 +                 str "i"])) frees')
   1.264 +            (Pretty.block [str "if ",
   1.265 +              mk_app false (str "testf") (map (str o snd) frees'),
   1.266 +              Pretty.brk 1, str "then NONE",
   1.267 +              Pretty.brk 1, str "else ",
   1.268 +              Pretty.block [str "SOME ", Pretty.block (str "[" ::
   1.269 +                flat (separate [str ",", Pretty.brk 1]
   1.270                    (map (fn ((s, T), s') => [Pretty.block
   1.271 -                    [Pretty.str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   1.272 -                     Pretty.str (s' ^ "_t ())")]]) frees')) @
   1.273 -                  [Pretty.str "]"])]]),
   1.274 -          Pretty.str ");"]) ^
   1.275 -      "\n\nend;\n") ();
   1.276 +                    [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   1.277 +                     str (s' ^ "_t ())")]]) frees')) @
   1.278 +                  [str "]"])]]),
   1.279 +          str ");"]) ^
   1.280 +      "\n\nend;\n";
   1.281      val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
   1.282      fun iter f k = if k > i then NONE
   1.283        else (case (f () handle Match =>
   1.284 @@ -1034,7 +1041,7 @@
   1.285  val eval_result = ref (fn () => Bound 0);
   1.286  
   1.287  fun eval_term thy t =
   1.288 -  let val e = PrintMode.setmp [] (fn () =>
   1.289 +  let val e =
   1.290      let
   1.291        val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
   1.292          error "Term to be evaluated contains type variables";
   1.293 @@ -1045,15 +1052,15 @@
   1.294          [("result", Abs ("x", TFree ("'a", []), t))];
   1.295        val s = "structure EvalTerm =\nstruct\n\n" ^
   1.296          cat_lines (map snd code) ^
   1.297 -        "\nopen Generated;\n\n" ^ Pretty.string_of
   1.298 -          (Pretty.block [Pretty.str "val () = Codegen.eval_result := (fn () =>",
   1.299 +        "\nopen Generated;\n\n" ^ string_of
   1.300 +          (Pretty.block [str "val () = Codegen.eval_result := (fn () =>",
   1.301              Pretty.brk 1,
   1.302              mk_app false (mk_term_of gr "Generated" false (fastype_of t))
   1.303 -              [Pretty.str "(result ())"],
   1.304 -            Pretty.str ");"]) ^
   1.305 +              [str "(result ())"],
   1.306 +            str ");"]) ^
   1.307          "\n\nend;\n";
   1.308        val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
   1.309 -    in !eval_result end) ();
   1.310 +    in !eval_result end;
   1.311    in e () end;
   1.312  
   1.313  fun print_evaluated_term s = Toplevel.keep (fn state =>
   1.314 @@ -1083,8 +1090,6 @@
   1.315  
   1.316  (**** Interface ****)
   1.317  
   1.318 -val str = PrintMode.setmp [] Pretty.str;
   1.319 -
   1.320  fun parse_mixfix rd s =
   1.321    (case Scan.finite Symbol.stopper (Scan.repeat
   1.322       (   $$ "_" >> K Arg