Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.
--- a/src/HOL/Code_Setup.thy Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Code_Setup.thy Fri May 23 16:41:39 2008 +0200
@@ -52,7 +52,7 @@
val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
in
SOME (gr''', Codegen.parens
- (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
+ (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
end
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
--- a/src/HOL/Int.thy Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Int.thy Fri May 23 16:41:39 2008 +0200
@@ -1979,7 +1979,7 @@
let val i = HOLogic.dest_numeral (strip_number_of t)
in
SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
- Pretty.str (string_of_int i))
+ Codegen.str (string_of_int i))
end handle TERM _ => NONE;
in
--- a/src/HOL/List.thy Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/List.thy Fri May 23 16:41:39 2008 +0200
@@ -3410,7 +3410,7 @@
val i = HOLogic.dest_char t;
val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
(gr, fastype_of t)
- in SOME (gr', Pretty.str (ML_Syntax.print_string (chr i)))
+ in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i)))
end handle TERM _ => NONE;
in
--- a/src/HOL/Product_Type.thy Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Product_Type.thy Fri May 23 16:41:39 2008 +0200
@@ -1008,12 +1008,12 @@
(Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
in
SOME (gr3, Codegen.mk_app brack
- (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat
- (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
- [Pretty.block [Pretty.str "val ", pl, Pretty.str " =",
+ (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
+ (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
+ [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
Pretty.brk 1, pr]]) qs))),
- Pretty.brk 1, Pretty.str "in ", pu,
- Pretty.brk 1, Pretty.str "end"])) pargs)
+ Pretty.brk 1, Codegen.str "in ", pu,
+ Pretty.brk 1, Codegen.str "end"])) pargs)
end
end
| _ => NONE);
@@ -1029,8 +1029,8 @@
(Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
in
SOME (gr2, Codegen.mk_app brack
- (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>",
- Pretty.brk 1, pu, Pretty.str ")"]) pargs)
+ (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
+ Pretty.brk 1, pu, Codegen.str ")"]) pargs)
end
| _ => NONE)
| _ => NONE);
--- a/src/HOL/Tools/datatype_codegen.ML Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Fri May 23 16:41:39 2008 +0200
@@ -62,23 +62,23 @@
val (gr''', rest) = mk_dtdef gr'' "and " xs
in
(gr''',
- Pretty.block (Pretty.str prfx ::
+ Pretty.block (str prfx ::
(if null tvs then [] else
- [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @
- [Pretty.str (type_id ^ " ="), Pretty.brk 1] @
- List.concat (separate [Pretty.brk 1, Pretty.str "| "]
+ [mk_tuple (map str tvs), str " "]) @
+ [str (type_id ^ " ="), Pretty.brk 1] @
+ List.concat (separate [Pretty.brk 1, str "| "]
(map (fn (ps', (_, cname)) => [Pretty.block
- (Pretty.str cname ::
+ (str cname ::
(if null ps' then [] else
- List.concat ([Pretty.str " of", Pretty.brk 1] ::
- separate [Pretty.str " *", Pretty.brk 1]
+ List.concat ([str " of", Pretty.brk 1] ::
+ separate [str " *", Pretty.brk 1]
(map single ps'))))]) ps))) :: rest)
end;
fun mk_constr_term cname Ts T ps =
- List.concat (separate [Pretty.str " $", Pretty.brk 1]
- ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
- mk_type false (Ts ---> T), Pretty.str ")"] :: ps));
+ List.concat (separate [str " $", Pretty.brk 1]
+ ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
+ mk_type false (Ts ---> T), str ")"] :: ps));
fun mk_term_of_def gr prfx [] = []
| mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
@@ -89,14 +89,14 @@
val rest = mk_term_of_def gr "and " xs;
val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) =>
let val args = map (fn i =>
- Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts)
+ str ("x" ^ string_of_int i)) (1 upto length Ts)
in (" | ", Pretty.blk (4,
- [Pretty.str prfx, mk_term_of gr module' false T, Pretty.brk 1,
- if null Ts then Pretty.str (snd (get_const_id cname gr))
+ [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
+ if null Ts then str (snd (get_const_id cname gr))
else parens (Pretty.block
- [Pretty.str (snd (get_const_id cname gr)),
+ [str (snd (get_const_id cname gr)),
Pretty.brk 1, mk_tuple args]),
- Pretty.str " =", Pretty.brk 1] @
+ str " =", Pretty.brk 1] @
mk_constr_term cname Ts T
(map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U,
Pretty.brk 1, x]]) (args ~~ Ts))))
@@ -114,20 +114,20 @@
val SOME (cname, _) = find_nonempty descr [i] i;
fun mk_delay p = Pretty.block
- [Pretty.str "fn () =>", Pretty.brk 1, p];
+ [str "fn () =>", Pretty.brk 1, p];
- fun mk_force p = Pretty.block [p, Pretty.brk 1, Pretty.str "()"];
+ fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"];
fun mk_constr s b (cname, dts) =
let
val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
(DatatypeAux.typ_of_dtyp descr sorts dt))
- [Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0"
+ [str (if b andalso DatatypeAux.is_rec_type dt then "0"
else "j")]) dts;
val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
- val xs = map Pretty.str
+ val xs = map str
(DatatypeProp.indexify_names (replicate (length dts) "x"));
- val ts = map Pretty.str
+ val ts = map str
(DatatypeProp.indexify_names (replicate (length dts) "t"));
val (_, id) = get_const_id cname gr
in
@@ -136,52 +136,52 @@
(mk_tuple
[case xs of
_ :: _ :: _ => Pretty.block
- [Pretty.str id, Pretty.brk 1, mk_tuple xs]
- | _ => mk_app false (Pretty.str id) xs,
+ [str id, Pretty.brk 1, mk_tuple xs]
+ | _ => mk_app false (str id) xs,
mk_delay (Pretty.block (mk_constr_term cname Ts T
(map (single o mk_force) ts)))])
end;
fun mk_choice [c] = mk_constr "(i-1)" false c
- | mk_choice cs = Pretty.block [Pretty.str "one_of",
- Pretty.brk 1, Pretty.blk (1, Pretty.str "[" ::
- List.concat (separate [Pretty.str ",", Pretty.fbrk]
+ | mk_choice cs = Pretty.block [str "one_of",
+ Pretty.brk 1, Pretty.blk (1, str "[" ::
+ List.concat (separate [str ",", Pretty.fbrk]
(map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
- [Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"];
+ [str "]"]), Pretty.brk 1, str "()"];
val gs = maps (fn s =>
let val s' = strip_tname s
- in [Pretty.str (s' ^ "G"), Pretty.str (s' ^ "T")] end) tvs;
+ in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
val gen_name = "gen_" ^ snd (get_type_id tname gr)
in
Pretty.blk (4, separate (Pretty.brk 1)
- (Pretty.str (prfx ^ gen_name ^
+ (str (prfx ^ gen_name ^
(if null cs1 then "" else "'")) :: gs @
- (if null cs1 then [] else [Pretty.str "i"]) @
- [Pretty.str "j"]) @
- [Pretty.str " =", Pretty.brk 1] @
+ (if null cs1 then [] else [str "i"]) @
+ [str "j"]) @
+ [str " =", Pretty.brk 1] @
(if not (null cs1) andalso not (null cs2)
- then [Pretty.str "frequency", Pretty.brk 1,
- Pretty.blk (1, [Pretty.str "[",
- mk_tuple [Pretty.str "i", mk_delay (mk_choice cs1)],
- Pretty.str ",", Pretty.fbrk,
- mk_tuple [Pretty.str "1", mk_delay (mk_choice cs2)],
- Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"]
+ then [str "frequency", Pretty.brk 1,
+ Pretty.blk (1, [str "[",
+ mk_tuple [str "i", mk_delay (mk_choice cs1)],
+ str ",", Pretty.fbrk,
+ mk_tuple [str "1", mk_delay (mk_choice cs2)],
+ str "]"]), Pretty.brk 1, str "()"]
else if null cs2 then
- [Pretty.block [Pretty.str "(case", Pretty.brk 1,
- Pretty.str "i", Pretty.brk 1, Pretty.str "of",
- Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
+ [Pretty.block [str "(case", Pretty.brk 1,
+ str "i", Pretty.brk 1, str "of",
+ Pretty.brk 1, str "0 =>", Pretty.brk 1,
mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
- Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
- mk_choice cs1, Pretty.str ")"]]
+ Pretty.brk 1, str "| _ =>", Pretty.brk 1,
+ mk_choice cs1, str ")"]]
else [mk_choice cs2])) ::
(if null cs1 then []
else [Pretty.blk (4, separate (Pretty.brk 1)
- (Pretty.str ("and " ^ gen_name) :: gs @ [Pretty.str "i"]) @
- [Pretty.str " =", Pretty.brk 1] @
- separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @
- [Pretty.str "i", Pretty.str "i"]))]) @
+ (str ("and " ^ gen_name) :: gs @ [str "i"]) @
+ [str " =", Pretty.brk 1] @
+ separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @
+ [str "i", str "i"]))]) @
mk_gen_of_def gr "and " xs
end
@@ -194,15 +194,15 @@
val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
in
map_node node_id (K (NONE, module',
- Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
- [Pretty.str ";"])) ^ "\n\n" ^
+ string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
+ [str ";"])) ^ "\n\n" ^
(if "term_of" mem !mode then
- Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
- (mk_term_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
+ string_of (Pretty.blk (0, separate Pretty.fbrk
+ (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
else "") ^
(if "test" mem !mode then
- Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
- (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
+ string_of (Pretty.blk (0, separate Pretty.fbrk
+ (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
else ""))) gr2
end,
module')
@@ -236,17 +236,17 @@
val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t');
val (ps, gr2) = pcase gr1 cs ts Us;
in
- ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2)
+ ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
end;
val (ps1, gr1) = pcase gr constrs ts1 Ts;
- val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1);
+ val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t);
val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2)
in (gr3, (if not (null ts2) andalso brack then parens else I)
(Pretty.block (separate (Pretty.brk 1)
- (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of",
- Pretty.brk 1] @ ps @ [Pretty.str ")"]) :: ps2))))
+ (Pretty.block ([str "(case ", p, str " of",
+ Pretty.brk 1] @ ps @ [str ")"]) :: ps2))))
end
end;
@@ -264,8 +264,8 @@
(invoke_codegen thy defs dep module (i = 1)) (gr, ts);
in (case args of
_ :: _ :: _ => (gr', (if brack then parens else I)
- (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps]))
- | _ => (gr', mk_app brack (Pretty.str id) ps))
+ (Pretty.block [str id, Pretty.brk 1, mk_tuple ps]))
+ | _ => (gr', mk_app brack (str id) ps))
end
end;
@@ -304,8 +304,8 @@
val (gr''', tyid) = mk_type_id module' s gr''
in SOME (gr''',
Pretty.block ((if null Ts then [] else
- [mk_tuple ps, Pretty.str " "]) @
- [Pretty.str (mk_qual_id module tyid)]))
+ [mk_tuple ps, str " "]) @
+ [str (mk_qual_id module tyid)]))
end)
| datatype_tycodegen _ _ _ _ _ _ _ = NONE;
--- a/src/HOL/Tools/inductive_codegen.ML Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri May 23 16:41:39 2008 +0200
@@ -260,12 +260,12 @@
fun mk_eq (x::xs) =
let fun mk_eqs _ [] = []
- | mk_eqs a (b::cs) = Pretty.str (a ^ " = " ^ b) :: mk_eqs b cs
+ | mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs
in mk_eqs x xs end;
-fun mk_tuple xs = Pretty.block (Pretty.str "(" ::
- List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
- [Pretty.str ")"]);
+fun mk_tuple xs = Pretty.block (str "(" ::
+ List.concat (separate [str ",", Pretty.brk 1] (map single xs)) @
+ [str ")"]);
fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
NONE => ((names, (s, [s])::vs), s)
@@ -287,18 +287,18 @@
| is_exhaustive _ = false;
fun compile_match nvs eq_ps out_ps success_p can_fail =
- let val eqs = List.concat (separate [Pretty.str " andalso", Pretty.brk 1]
+ let val eqs = List.concat (separate [str " andalso", Pretty.brk 1]
(map single (List.concat (map (mk_eq o snd) nvs) @ eq_ps)));
in
Pretty.block
- ([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @
- (Pretty.block ((if eqs=[] then [] else Pretty.str "if " ::
- [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @
+ ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
+ (Pretty.block ((if eqs=[] then [] else str "if " ::
+ [Pretty.block eqs, Pretty.brk 1, str "then "]) @
(success_p ::
- (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else DSeq.empty"]))) ::
+ (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
(if can_fail then
- [Pretty.brk 1, Pretty.str "| _ => DSeq.empty)"]
- else [Pretty.str ")"])))
+ [Pretty.brk 1, str "| _ => DSeq.empty)"]
+ else [str ")"])))
end;
fun modename module s (iss, is) gr =
@@ -310,14 +310,14 @@
end;
fun mk_funcomp brack s k p = (if brack then parens else I)
- (Pretty.block [Pretty.block ((if k = 0 then [] else [Pretty.str "("]) @
- separate (Pretty.brk 1) (Pretty.str s :: replicate k (Pretty.str "|> ???")) @
- (if k = 0 then [] else [Pretty.str ")"])), Pretty.brk 1, p]);
+ (Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @
+ separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @
+ (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]);
fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) =
apsnd single (invoke_codegen thy defs dep module brack (gr, t))
| compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
- (gr, [Pretty.str name])
+ (gr, [str name])
| compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) =
(case strip_comb t of
(Const (name, _), args) =>
@@ -328,13 +328,13 @@
(compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
modename module name mode;
val (gr'', ps') = (case mode of
- ([], []) => (gr', [Pretty.str "()"])
+ ([], []) => (gr', [str "()"])
| _ => foldl_map
(invoke_codegen thy defs dep module true) (gr', args2))
in (gr', (if brack andalso not (null ps andalso null ps') then
single o parens o Pretty.block else I)
(List.concat (separate [Pretty.brk 1]
- ([Pretty.str mode_id] :: ps @ map single ps'))))
+ ([str mode_id] :: ps @ map single ps'))))
end
else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
(invoke_codegen thy defs dep module true (gr, t))
@@ -353,7 +353,7 @@
in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
fun compile_eq (gr, (s, t)) =
- apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
+ apsnd (Pretty.block o cons (str (s ^ " = ")) o single)
(invoke_codegen thy defs dep module false (gr, t));
val (in_ts, out_ts) = get_args is 1 ts;
@@ -374,7 +374,7 @@
val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
in
(gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
- (Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
+ (Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
(exists (not o is_exhaustive) out_ts'''))
end
| compile_prems out_ts vs names gr ps =
@@ -405,13 +405,13 @@
(compile_expr thy defs dep module false modes
(gr2, (mode, t)))
else
- apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p])
+ apsnd (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
(invoke_codegen thy defs dep module true (gr2, t));
val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
in
(gr4, compile_match (snd nvs) eq_ps out_ps
(Pretty.block (ps @
- [Pretty.str " :->", Pretty.brk 1, rest]))
+ [str " :->", Pretty.brk 1, rest]))
(exists (not o is_exhaustive) out_ts''))
end
| Sidecond t =>
@@ -420,21 +420,21 @@
val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
in
(gr3, compile_match (snd nvs) eq_ps out_ps
- (Pretty.block [Pretty.str "?? ", side_p,
- Pretty.str " :->", Pretty.brk 1, rest])
+ (Pretty.block [str "?? ", side_p,
+ str " :->", Pretty.brk 1, rest])
(exists (not o is_exhaustive) out_ts''))
end)
end;
val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
in
- (gr', Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, inp,
- Pretty.str " :->", Pretty.brk 1, prem_p])
+ (gr', Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
+ str " :->", Pretty.brk 1, prem_p])
end;
fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
let
- val xs = map Pretty.str (Name.variant_list arg_vs
+ val xs = map str (Name.variant_list arg_vs
(map (fn i => "x" ^ string_of_int i) (snd mode)));
val (gr', (cl_ps, mode_id)) =
foldl_map (fn (gr, cl) => compile_clause thy defs
@@ -443,12 +443,12 @@
in
((gr', "and "), Pretty.block
([Pretty.block (separate (Pretty.brk 1)
- (Pretty.str (prfx ^ mode_id) ::
- map Pretty.str arg_vs @
- (case mode of ([], []) => [Pretty.str "()"] | _ => xs)) @
- [Pretty.str " ="]),
+ (str (prfx ^ mode_id) ::
+ map str arg_vs @
+ (case mode of ([], []) => [str "()"] | _ => xs)) @
+ [str " ="]),
Pretty.brk 1] @
- List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
+ List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))))
end;
fun compile_preds thy defs gr dep module all_vs arg_vs modes preds =
@@ -457,7 +457,7 @@
dep module prfx' all_vs arg_vs modes s cls mode)
((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
in
- (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
+ (gr', space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n")
end;
(**** processing of introduction rules ****)
@@ -605,11 +605,11 @@
val (gr', (fun_id, mode_id)) = gr |>
mk_const_id module' name |>>>
modename module' pname ([], mode);
- val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
- val s = Pretty.string_of (Pretty.block
- [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =",
- Pretty.brk 1, Pretty.str "DSeq.hd", Pretty.brk 1,
- parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id ::
+ val vars = map (fn i => str ("x" ^ string_of_int i)) mode;
+ val s = string_of (Pretty.block
+ [mk_app false (str ("fun " ^ snd fun_id)) vars, str " =",
+ Pretty.brk 1, str "DSeq.hd", Pretty.brk 1,
+ parens (Pretty.block (separate (Pretty.brk 1) (str mode_id ::
vars)))]) ^ ";\n\n";
val gr'' = mk_ind_def thy defs (add_edge (name, dep)
(new_node (name, (NONE, module', s)) gr')) name [pname] module'
@@ -626,7 +626,7 @@
fun conv_ntuple fs ts p =
let
val k = length fs;
- val xs = map (fn i => Pretty.str ("x" ^ string_of_int i)) (0 upto k);
+ val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k);
val xs' = map (fn Bound i => nth xs (k - i)) ts;
fun conv xs js =
if js mem fs then
@@ -638,9 +638,9 @@
in
if k > 0 then
Pretty.block
- [Pretty.str "DSeq.map (fn", Pretty.brk 1,
- mk_tuple xs', Pretty.str " =>", Pretty.brk 1, fst (conv xs []),
- Pretty.str ")", Pretty.brk 1, parens p]
+ [str "DSeq.map (fn", Pretty.brk 1,
+ mk_tuple xs', str " =>", Pretty.brk 1, fst (conv xs []),
+ str ")", Pretty.brk 1, parens p]
else p
end;
@@ -664,8 +664,8 @@
let val (gr', call_p) = mk_ind_call thy defs gr dep module true
s T (ts1 @ ts2') names thyname k intrs
in SOME (gr', (if brack then parens else I) (Pretty.block
- [Pretty.str "DSeq.list_of", Pretty.brk 1, Pretty.str "(",
- conv_ntuple fs ots call_p, Pretty.str ")"]))
+ [str "DSeq.list_of", Pretty.brk 1, str "(",
+ conv_ntuple fs ots call_p, str ")"]))
end
else NONE
end
@@ -690,7 +690,7 @@
dep module (if_library thyname module) gr;
val (gr'', ps) = foldl_map
(invoke_codegen thy defs dep module true) (gr', ts);
- in SOME (gr'', mk_app brack (Pretty.str id) ps)
+ in SOME (gr'', mk_app brack (str id) ps)
end)
| _ => NONE);
--- a/src/HOL/Tools/recfun_codegen.ML Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Fri May 23 16:41:39 2008 +0200
@@ -105,13 +105,13 @@
val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);
val (gr3, rest) = mk_fundef module fname' false gr2 xs
in
- (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then " | " else prfx),
- pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
+ (gr3, Pretty.blk (4, [str (if fname = fname' then " | " else prfx),
+ pl, str " =", Pretty.brk 1, pr]) :: rest)
end;
fun put_code module fundef = map_node dname
- (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0,
- separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
+ (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
+ separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
in
(case try (get_node gr) dname of
@@ -162,7 +162,7 @@
add_rec_funs thy defs gr' dep (map prop_of eqns) module';
val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr''
in
- SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps)
+ SOME (gr''', mk_app brack (str (mk_qual_id module fname)) ps)
end)
| _ => NONE);
--- a/src/HOL/Tools/typedef_codegen.ML Fri May 23 16:37:57 2008 +0200
+++ b/src/HOL/Tools/typedef_codegen.ML Fri May 23 16:41:39 2008 +0200
@@ -23,7 +23,7 @@
val (gr'', ps) =
foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
- in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
+ in SOME (gr'', Codegen.mk_app brack (Codegen.str id) ps) end;
fun lookup f T =
(case TypedefPackage.get_info thy (get_name T) of
NONE => ""
@@ -41,8 +41,8 @@
| _ => NONE)
end;
-fun mk_tyexpr [] s = Pretty.str s
- | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
+fun mk_tyexpr [] s = Codegen.str s
+ | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
@@ -69,31 +69,31 @@
(Codegen.add_edge (node_id, dep)
(Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
val s =
- Pretty.string_of (Pretty.block [Pretty.str "datatype ",
+ Codegen.string_of (Pretty.block [Codegen.str "datatype ",
mk_tyexpr ps (snd ty_id),
- Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
- Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
- Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
- Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
- Pretty.str "x) = x;"]) ^ "\n\n" ^
+ Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
+ Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
+ Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
+ Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
+ Codegen.str "x) = x;"]) ^ "\n\n" ^
(if "term_of" mem !Codegen.mode then
- Pretty.string_of (Pretty.block [Pretty.str "fun ",
+ Codegen.string_of (Pretty.block [Codegen.str "fun ",
Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
- Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
- Pretty.str "x) =", Pretty.brk 1,
- Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
+ Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
+ Codegen.str "x) =", Pretty.brk 1,
+ Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
- Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
+ Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
- Pretty.str "x;"]) ^ "\n\n"
+ Codegen.str "x;"]) ^ "\n\n"
else "") ^
(if "test" mem !Codegen.mode then
- Pretty.string_of (Pretty.block [Pretty.str "fun ",
+ Codegen.string_of (Pretty.block [Codegen.str "fun ",
Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
- Pretty.str "i =", Pretty.brk 1,
- Pretty.block [Pretty.str (Abs_id ^ " ("),
+ Codegen.str "i =", Pretty.brk 1,
+ Pretty.block [Codegen.str (Abs_id ^ " ("),
Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
- Pretty.str "i);"]]) ^ "\n\n"
+ Codegen.str "i);"]]) ^ "\n\n"
else "")
in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
| SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)