--- a/Admin/polyml/build Mon Feb 22 22:44:37 2016 +0100
+++ b/Admin/polyml/build Tue Feb 23 16:20:12 2016 +0100
@@ -80,7 +80,7 @@
cd "$SOURCE"
make distclean
- { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
+ { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" --enable-intinf-as-int "${USER_OPTIONS[@]}" && \
make compiler && \
make compiler && \
make install; } || fail "Build failed"
--- a/src/Pure/General/pretty.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/General/pretty.ML Tue Feb 23 16:20:12 2016 +0100
@@ -375,14 +375,16 @@
(** ML toplevel pretty printing **)
fun to_ML (Block (m, consistent, indent, prts, _)) =
- ML_Pretty.Block (m, consistent, indent, map to_ML prts)
- | to_ML (Break b) = ML_Pretty.Break b
- | to_ML (Str s) = ML_Pretty.String s;
+ ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map to_ML prts)
+ | to_ML (Break (force, wd, ind)) =
+ ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
+ | to_ML (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
- make_block m consistent indent (map from_ML prts)
- | from_ML (ML_Pretty.Break b) = Break b
- | from_ML (ML_Pretty.String s) = Str s;
+ make_block m consistent (FixedInt.toInt indent) (map from_ML prts)
+ | from_ML (ML_Pretty.Break (force, wd, ind)) =
+ Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
+ | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
end;
--- a/src/Pure/ML/exn_output.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/ML/exn_output.ML Tue Feb 23 16:20:12 2016 +0100
@@ -19,6 +19,8 @@
| SOME loc => Exn_Properties.position_of loc);
fun pretty (exn: exn) =
- Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
+ Pretty.from_ML
+ (pretty_ml
+ (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
end;
--- a/src/Pure/ML/exn_properties.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML Tue Feb 23 16:20:12 2016 +0100
@@ -26,9 +26,9 @@
fun position_of loc =
Position.make
- {line = #startLine loc,
- offset = #startPosition loc,
- end_offset = #endPosition loc,
+ {line = FixedInt.toInt (#startLine loc),
+ offset = FixedInt.toInt (#startPosition loc),
+ end_offset = FixedInt.toInt (#endPosition loc),
props = props_of loc};
--- a/src/Pure/ML/install_pp_polyml.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML Tue Feb 23 16:20:12 2016 +0100
@@ -59,10 +59,10 @@
ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
- ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
+ ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
- ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
+ ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
pretty (Synchronized.value var, depth));
@@ -87,13 +87,13 @@
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
-fun prt_term parens dp t =
+fun prt_term parens (dp: FixedInt.int) t =
if dp <= 0 then Pretty.str "..."
else
(case t of
_ $ _ =>
op :: (strip_comb t)
- |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
+ |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
|> Pretty.separate " $"
|> (if parens then Pretty.enclose "(" ")" else Pretty.block)
| Abs (a, T, b) =>
@@ -142,7 +142,8 @@
and prt_proofs parens dp prf =
let
val (head, args) = strip_proof prf [];
- val prts = head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - i - 2)) args);
+ val prts =
+ head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
and strip_proof (p % t) res =
--- a/src/Pure/ML/ml_compiler.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Tue Feb 23 16:20:12 2016 +0100
@@ -201,7 +201,7 @@
(* results *)
- val depth = ML_Options.get_print_depth ();
+ val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
fun apply_result {fixes, types, signatures, structures, functors, values} =
let
--- a/src/Pure/RAW/ROOT_polyml.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Tue Feb 23 16:20:12 2016 +0100
@@ -12,6 +12,9 @@
then use "RAW/ml_name_space_polyml-5.6.ML"
else use "RAW/ml_name_space_polyml.ML";
+if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
+else use "RAW/fixed_int_dummy.ML";
+
structure ML_Name_Space =
struct
open ML_Name_Space;
@@ -144,7 +147,8 @@
val len' = property "length" len;
in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
| convert len (PolyML.PrettyString s) =
- ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+ ML_Pretty.String
+ (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
in convert "" end;
fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
@@ -157,9 +161,11 @@
(if en = "" then [] else [PolyML.ContextProperty ("end", en)])
in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
| ml_pretty (ML_Pretty.String (s, len)) =
- if len = size s then PolyML.PrettyString s
- else PolyML.PrettyBlock
- (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
+ if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
+ else
+ PolyML.PrettyBlock
+ (0, false,
+ [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
(* ML compiler *)
@@ -189,8 +195,8 @@
then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
fun ml_make_string struct_name =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
- struct_name ^ ".ML_print_depth ())))))";
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
+ struct_name ^ ".ML_print_depth ()))))))";
(* ML debugger *)
--- a/src/Pure/RAW/compiler_polyml.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML Tue Feb 23 16:20:12 2016 +0100
@@ -29,7 +29,7 @@
(put (if hard then "Error: " else "Warning: ");
PolyML.prettyPrint (put, 76) msg1;
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
- put ("At" ^ str_of_pos message_line file ^ "\n"));
+ put ("At" ^ str_of_pos (FixedInt.toInt message_line) file ^ "\n"));
val parameters =
[PolyML.Compiler.CPOutStream put,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/fixed_int_dummy.ML Tue Feb 23 16:20:12 2016 +0100
@@ -0,0 +1,6 @@
+(* Title: Pure/RAW/fixed_int_dummy.ML
+
+FixedInt dummy that is not fixed (up to Poly/ML 5.6).
+*)
+
+structure FixedInt = IntInf;
--- a/src/Pure/RAW/ml_debugger_polyml-5.6.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/RAW/ml_debugger_polyml-5.6.ML Tue Feb 23 16:20:12 2016 +0100
@@ -44,7 +44,7 @@
val _ =
PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
let val s = print_exn_id exn_id
- in ml_pretty (ML_Pretty.String (s, size s)) end);
+ in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
(* hooks *)
--- a/src/Pure/RAW/ml_pretty.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/RAW/ml_pretty.ML Tue Feb 23 16:20:12 2016 +0100
@@ -8,23 +8,23 @@
struct
datatype pretty =
- Block of (string * string) * bool * int * pretty list |
- String of string * int |
- Break of bool * int * int;
+ Block of (string * string) * bool * FixedInt.int * pretty list |
+ String of string * FixedInt.int |
+ Break of bool * FixedInt.int * FixedInt.int;
fun block prts = Block (("", ""), false, 2, prts);
-fun str s = String (s, size s);
+fun str s = String (s, FixedInt.fromInt (size s));
fun brk width = Break (false, width, 0);
-fun pair pretty1 pretty2 ((x, y), depth: int) =
+fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
-fun enum sep lpar rpar pretty (args, depth) =
+fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
let
fun elems _ [] = []
| elems 0 _ = [str "..."]
| elems d [x] = [pretty (x, d)]
| elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
- in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
+ in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
end;
--- a/src/Pure/ROOT Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/ROOT Tue Feb 23 16:20:12 2016 +0100
@@ -9,6 +9,7 @@
"RAW/compiler_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace_polyml-5.5.1.ML"
+ "RAW/fixed_int_dummy.ML"
"RAW/ml_compiler_parameters.ML"
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
@@ -40,6 +41,7 @@
"RAW/compiler_polyml.ML"
"RAW/exn.ML"
"RAW/exn_trace_polyml-5.5.1.ML"
+ "RAW/fixed_int_dummy.ML"
"RAW/ml_compiler_parameters.ML"
"RAW/ml_compiler_parameters_polyml-5.6.ML"
"RAW/ml_debugger.ML"
--- a/src/Pure/Tools/debugger.ML Mon Feb 22 22:44:37 2016 +0100
+++ b/src/Pure/Tools/debugger.ML Tue Feb 23 16:20:12 2016 +0100
@@ -189,7 +189,8 @@
val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
fun print x =
- Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
+ Pretty.from_ML
+ (ML_Name_Space.display_val (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
fun print_all () =
#allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
|> sort_by #1 |> map (Pretty.item o single o print o #2)