--- a/src/Tools/Metis/README Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/README Wed Dec 07 16:03:05 2011 +0100
@@ -6,7 +6,7 @@
1. The files "Makefile" and "script/mlpp" and the directory "src/"
must reflect the corresponding files in Joe Hurd's official Metis
package. The package that was used when these notes where written
- was Metis 2.3 (31 May 2011).
+ was Metis 2.3 (release 20110926).
2. The license in each source file will probably not be something we
can use in Isabelle. The "fix_metis_license" script can be run to
@@ -19,7 +19,8 @@
Isabelle BSD license.
3. Some modifications might have to be done manually to the source
- files. The ultimate way to track them down is to use Mercurial.
+ files (but probably not). The ultimate way to track them down is
+ to use Mercurial.
4. Isabelle itself cares only about "metis.ML", which is generated
from the files in "src/" by the script "make_metis". The script
@@ -46,4 +47,4 @@
Good luck!
Jasmin Blanchette
- 8 June 2011
+ 1 December 2011
--- a/src/Tools/Metis/metis.ML Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/metis.ML Wed Dec 07 16:03:05 2011 +0100
@@ -718,7 +718,7 @@
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
| z _ _ _ = raise Error "zipWith: lists different lengths";
in
- fn xs => fn ys => rev (z [] xs ys)
+ fn xs => fn ys => List.rev (z [] xs ys)
end;
fun zip xs ys = zipWith pair xs ys;
@@ -726,7 +726,7 @@
local
fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
in
- fun unzip ab = List.foldl inc ([],[]) (rev ab);
+ fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
end;
fun cartwith f =
@@ -737,15 +737,15 @@
aux xsCopy (f x y :: res) xt ys
in
fn xs => fn ys =>
- let val xs' = rev xs in aux xs' [] xs' (rev ys) end
+ let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
end;
fun cart xs ys = cartwith pair xs ys;
fun takeWhile p =
let
- fun f acc [] = rev acc
- | f acc (x :: xs) = if p x then f (x :: acc) xs else rev acc
+ fun f acc [] = List.rev acc
+ | f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
in
f []
end;
@@ -760,8 +760,8 @@
fun divideWhile p =
let
- fun f acc [] = (rev acc, [])
- | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (rev acc, l)
+ fun f acc [] = (List.rev acc, [])
+ | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
in
f []
end;
@@ -772,15 +772,15 @@
case l of
[] =>
let
- val acc = if List.null row then acc else rev row :: acc
- in
- rev acc
+ val acc = if List.null row then acc else List.rev row :: acc
+ in
+ List.rev acc
end
| h :: t =>
let
val (eor,x) = f (h,x)
in
- if eor then group (rev row :: acc) [h] x t
+ if eor then group (List.rev row :: acc) [h] x t
else group acc (h :: row) x t
end
in
@@ -831,7 +831,7 @@
fun revDivide l = revDiv [] l;
end;
-fun divide l n = let val (a,b) = revDivide l n in (rev a, b) end;
+fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
fun updateNth (n,x) l =
let
@@ -860,28 +860,28 @@
local
fun inc (v,x) = if mem v x then x else v :: x;
in
- fun setify s = rev (List.foldl inc [] s);
+ fun setify s = List.rev (List.foldl inc [] s);
end;
fun union s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc t (rev s)
+ List.foldl inc t (List.rev s)
end;
fun intersect s t =
let
fun inc (v,x) = if mem v t then v :: x else x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun difference s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun subset s t = List.all (fn x => mem x t) s;
@@ -925,13 +925,13 @@
fun sort cmp =
let
- fun findRuns acc r rs [] = rev (rev (r :: rs) :: acc)
+ fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
| findRuns acc r rs (x :: xs) =
case cmp (r,x) of
- GREATER => findRuns (rev (r :: rs) :: acc) x [] xs
+ GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
| _ => findRuns acc x (r :: rs) xs
- fun mergeAdj acc [] = rev acc
+ fun mergeAdj acc [] = List.rev acc
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
@@ -1072,7 +1072,7 @@
[] => []
| h :: t => if Char.isSpace h then chop t else l;
in
- val trim = String.implode o chop o rev o chop o rev o String.explode;
+ val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
end;
val join = String.concatWith;
@@ -1089,11 +1089,11 @@
let
val pat = String.explode sep
- fun div1 prev recent [] = stringify [] (rev recent :: prev)
+ fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
- | SOME rest => div1 (rev recent :: prev) [] rest
+ | SOME rest => div1 (List.rev recent :: prev) [] rest
in
fn s => div1 [] [] (String.explode s)
end;
@@ -1302,7 +1302,7 @@
val () = OS.FileSys.closeDir dirStrm
in
- rev filenames
+ List.rev filenames
end;
fun readTextFile {filename} =
@@ -3146,6 +3146,10 @@
type key
+val compareKey : key * key -> order
+
+val equalKey : key -> key -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite maps. *)
(* ------------------------------------------------------------------------- *)
@@ -5298,6 +5302,10 @@
type element
+val compareElement : element * element -> order
+
+val equalElement : element -> element -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
@@ -5488,6 +5496,10 @@
type element = KM.key;
+val compareElement = KM.compareKey;
+
+val equalElement = KM.equalKey;
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
@@ -6353,7 +6365,7 @@
| concatList (h :: t) = append h (fn () => concatList t);
local
- fun toLst res Nil = rev res
+ fun toLst res Nil = List.rev res
| toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
in
fun toList s = toLst [] s;
@@ -6529,41 +6541,12 @@
val escapeString : {escape : char list} -> string -> string
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int
-
-val mkStringSize : string -> stringSize
-
-(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent
-
-datatype step =
- BeginBlock of breakStyle * int
- | EndBlock
- | AddString of stringSize
- | AddBreak of int
- | AddNewline
-
-type ppstream = step Metis_Stream.stream
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-val beginBlock : breakStyle -> int -> ppstream
-
-val endBlock : ppstream
-
-val addString : stringSize -> ppstream
-
-val addBreak : int -> ppstream
-
-val addNewline : ppstream
+type ppstream
+
+type 'a pp = 'a -> ppstream
val skip : ppstream
@@ -6575,28 +6558,75 @@
val stream : ppstream Metis_Stream.stream -> ppstream
-val block : breakStyle -> int -> ppstream -> ppstream
-
-val blockProgram : breakStyle -> int -> ppstream list -> ppstream
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
-(* ------------------------------------------------------------------------- *)
-
-val execute :
- {lineLength : int} -> ppstream ->
- {indent : int, line : string} Metis_Stream.stream
+val ppPpstream : ppstream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent
+
+datatype block =
+ Block of
+ {style : style,
+ indent : int}
+
+val styleBlock : block -> style
+
+val indentBlock : block -> int
+
+val block : block -> ppstream -> ppstream
+
+val consistentBlock : int -> ppstream list -> ppstream
+
+val inconsistentBlock : int -> ppstream list -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype word = Word of {word : string, size : int}
+
+val mkWord : string -> word
+
+val emptyWord : word
+
+val charWord : char -> word
+
+val ppWord : word pp
+
+val space : ppstream
+
+val spaces : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int}
+
+val mkBreak : int -> break
+
+val ppBreak : break pp
+
+val break : ppstream
+
+val breaks : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+val newline : ppstream
+
+val newlines : int -> ppstream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream
-
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
-val ppString : string pp
-
val ppBracket : string -> string -> 'a pp -> 'a pp
val ppOp : string -> ppstream
@@ -6615,6 +6645,8 @@
val ppChar : char pp
+val ppString : string pp
+
val ppEscapeString : {escape : char list} -> string pp
val ppUnit : unit pp
@@ -6641,12 +6673,6 @@
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
-val ppBreakStyle : breakStyle pp
-
-val ppStep : step pp
-
-val ppPpstream : ppstream pp
-
val ppException : exn pp
(* ------------------------------------------------------------------------- *)
@@ -6676,15 +6702,29 @@
('a * bool) pp -> ('a * bool) pp
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
+(* Pretty-printer rendering. *)
+(* ------------------------------------------------------------------------- *)
+
+val render :
+ {lineLength : int option} -> ppstream ->
+ {indent : int, line : string} Metis_Stream.stream
+
+val toStringWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string
+
+val toStreamWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string Metis_Stream.stream
+
+val toLine : 'a pp -> 'a -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
(* ------------------------------------------------------------------------- *)
val lineLength : int Unsynchronized.ref
val toString : 'a pp -> 'a -> string
-val toLine : 'a pp -> 'a -> string
-
val toStream : 'a pp -> 'a -> string Metis_Stream.stream
val trace : 'a pp -> string -> 'a -> unit
@@ -6721,7 +6761,7 @@
fun revConcat strm =
case strm of
Metis_Stream.Nil => Metis_Stream.Nil
- | Metis_Stream.Cons (h,t) => revAppend h (revConcat o t);
+ | Metis_Stream.Cons (h,t) => revAppend h (fn () => revConcat (t ()));
local
fun calcSpaces n = nChars #" " n;
@@ -6757,56 +6797,127 @@
end;
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int;
-
-fun mkStringSize s = (s, size s);
-
-val emptyStringSize = mkStringSize "";
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent;
+
+datatype block =
+ Block of
+ {style : style,
+ indent : int};
+
+fun toStringStyle style =
+ case style of
+ Consistent => "Consistent"
+ | Inconsistent => "Inconsistent";
+
+fun isConsistentStyle style =
+ case style of
+ Consistent => true
+ | Inconsistent => false;
+
+fun isInconsistentStyle style =
+ case style of
+ Inconsistent => true
+ | Consistent => false;
+
+fun mkBlock style indent =
+ Block
+ {style = style,
+ indent = indent};
+
+val mkConsistentBlock = mkBlock Consistent;
+
+val mkInconsistentBlock = mkBlock Inconsistent;
+
+fun styleBlock (Block {style = x, ...}) = x;
+
+fun indentBlock (Block {indent = x, ...}) = x;
+
+fun isConsistentBlock block = isConsistentStyle (styleBlock block);
+
+fun isInconsistentBlock block = isInconsistentStyle (styleBlock block);
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype word = Word of {word : string, size : int};
+
+fun mkWord s = Word {word = s, size = String.size s};
+
+val emptyWord = mkWord "";
+
+fun charWord c = mkWord (str c);
+
+fun spacesWord i = Word {word = nSpaces i, size = i};
+
+fun sizeWord (Word {size = x, ...}) = x;
+
+fun renderWord (Word {word = x, ...}) = x;
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int};
+
+fun mkBreak n = Break {size = n, extraIndent = 0};
+
+fun sizeBreak (Break {size = x, ...}) = x;
+
+fun extraIndentBreak (Break {extraIndent = x, ...}) = x;
+
+fun renderBreak b = nSpaces (sizeBreak b);
+
+fun updateSizeBreak size break =
+ let
+ val Break {size = _, extraIndent} = break
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
+
+fun appendBreak break1 break2 =
+ let
+(*BasicDebug
+ val () = warn "merging consecutive pretty-printing breaks"
+*)
+ val Break {size = size1, extraIndent = extraIndent1} = break1
+ and Break {size = size2, extraIndent = extraIndent2} = break2
+
+ val size = size1 + size2
+ and extraIndent = Int.max (extraIndent1,extraIndent2)
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent;
-
datatype step =
- BeginBlock of breakStyle * int
+ BeginBlock of block
| EndBlock
- | AddString of stringSize
- | AddBreak of int
+ | AddWord of word
+ | AddBreak of break
| AddNewline;
type ppstream = step Metis_Stream.stream;
-fun breakStyleToString style =
- case style of
- Consistent => "Consistent"
- | Inconsistent => "Inconsistent";
-
-fun stepToString step =
+type 'a pp = 'a -> ppstream;
+
+fun toStringStep step =
case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
- | AddString _ => "AddString"
- | AddBreak _ => "AddBreak"
- | AddNewline => "AddNewline";
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-fun beginBlock style indent = Metis_Stream.singleton (BeginBlock (style,indent));
-
-val endBlock = Metis_Stream.singleton EndBlock;
-
-fun addString s = Metis_Stream.singleton (AddString s);
-
-fun addBreak spaces = Metis_Stream.singleton (AddBreak spaces);
-
-val addNewline = Metis_Stream.singleton AddNewline;
+ | AddWord _ => "Word"
+ | AddBreak _ => "Break"
+ | AddNewline => "Newline";
val skip : ppstream = Metis_Stream.Nil;
@@ -6815,735 +6926,90 @@
local
fun dup pp n () = if n = 1 then pp else Metis_Stream.append pp (dup pp (n - 1));
in
- fun duplicate n pp = if n = 0 then skip else dup pp n ();
+ fun duplicate n pp : ppstream =
+ let
+(*BasicDebug
+ val () = if 0 <= n then () else raise Bug "Metis_Print.duplicate"
+*)
+ in
+ if n = 0 then skip else dup pp n ()
+ end;
end;
val program : ppstream list -> ppstream = Metis_Stream.concatList;
val stream : ppstream Metis_Stream.stream -> ppstream = Metis_Stream.concat;
-fun block style indent pp = program [beginBlock style indent, pp, endBlock];
-
-fun blockProgram style indent pps = block style indent (program pps);
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
-(* ------------------------------------------------------------------------- *)
-
-datatype blockBreakStyle =
- InconsistentBlock
- | ConsistentBlock
- | BreakingBlock;
-
-datatype block =
- Block of
- {indent : int,
- style : blockBreakStyle,
- size : int,
- chunks : chunk list}
-
-and chunk =
- StringChunk of {size : int, string : string}
- | BreakChunk of int
- | BlockChunk of block;
-
-datatype state =
- State of
- {blocks : block list,
- lineIndent : int,
- lineSize : int};
-
-val initialIndent = 0;
-
-val initialStyle = Inconsistent;
-
-fun liftStyle style =
- case style of
- Inconsistent => InconsistentBlock
- | Consistent => ConsistentBlock;
-
-fun breakStyle style =
- case style of
- ConsistentBlock => BreakingBlock
- | _ => style;
-
-fun sizeBlock (Block {size,...}) = size;
-
-fun sizeChunk chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => sizeBlock block;
-
-val splitChunks =
- let
- fun split _ [] = NONE
- | split acc (chunk :: chunks) =
- case chunk of
- BreakChunk _ => SOME (rev acc, chunks)
- | _ => split (chunk :: acc) chunks
- in
- split []
- end;
-
-val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
-
-local
- fun flatten acc chunks =
- case chunks of
- [] => rev acc
- | chunk :: chunks =>
- case chunk of
- StringChunk {string = s, ...} => flatten (s :: acc) chunks
- | BreakChunk n => flatten (nSpaces n :: acc) chunks
- | BlockChunk (Block {chunks = l, ...}) =>
- flatten acc (List.revAppend (l,chunks));
-in
- fun renderChunks indent chunks =
- {indent = indent,
- line = String.concat (flatten [] (rev chunks))};
-end;
-
-fun renderChunk indent chunk = renderChunks indent [chunk];
-
-fun isEmptyBlock block =
- let
- val Block {indent = _, style = _, size, chunks} = block
-
- val empty = List.null chunks
-
-(*BasicDebug
- val _ = not empty orelse size = 0 orelse
- raise Bug "Metis_Print.isEmptyBlock: bad size"
-*)
- in
- empty
- end;
-
-(*BasicDebug
-fun checkBlock ind block =
- let
- val Block {indent, style = _, size, chunks} = block
- val _ = indent >= ind orelse raise Bug "Metis_Print.checkBlock: bad indents"
- val size' = checkChunks indent chunks
- val _ = size = size' orelse raise Bug "Metis_Print.checkBlock: wrong size"
- in
- size
- end
-
-and checkChunks ind chunks =
- case chunks of
- [] => 0
- | chunk :: chunks => checkChunk ind chunk + checkChunks ind chunks
-
-and checkChunk ind chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => checkBlock ind block;
-
-val checkBlocks =
- let
- fun check ind blocks =
- case blocks of
- [] => 0
- | block :: blocks =>
- let
- val Block {indent,...} = block
- in
- checkBlock ind block + check indent blocks
- end
- in
- check initialIndent o rev
- end;
-*)
-
-val initialBlock =
- let
- val indent = initialIndent
- val style = liftStyle initialStyle
- val size = 0
- val chunks = []
- in
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- end;
-
-val initialState =
- let
- val blocks = [initialBlock]
- val lineIndent = initialIndent
- val lineSize = 0
- in
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- end;
-
-(*BasicDebug
-fun checkState state =
- (let
- val State {blocks, lineIndent = _, lineSize} = state
- val lineSize' = checkBlocks blocks
- val _ = lineSize = lineSize' orelse
- raise Error "wrong lineSize"
- in
- ()
- end
- handle Error err => raise Bug err)
- handle Bug bug => raise Bug ("Metis_Print.checkState: " ^ bug);
-*)
-
-fun isFinalState state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- case blocks of
- [] => raise Bug "Metis_Print.isFinalState: no block"
- | [block] => isEmptyBlock block
- | _ :: _ :: _ => false
- end;
-
-local
- fun renderBreak lineIndent (chunks,lines) =
- let
- val line = renderChunks lineIndent chunks
-
- val lines = line :: lines
- in
- lines
- end;
-
- fun renderBreaks lineIndent lineIndent' breaks lines =
- case rev breaks of
- [] => raise Bug "Metis_Print.renderBreaks"
- | c :: cs =>
- let
- val lines = renderBreak lineIndent (c,lines)
- in
- List.foldl (renderBreak lineIndent') lines cs
- end;
-
- fun splitAllChunks cumulatingChunks =
- let
- fun split chunks =
- case splitChunks chunks of
- SOME (prefix,chunks) => prefix :: split chunks
- | NONE => [List.concat (chunks :: cumulatingChunks)]
- in
- split
- end;
-
- fun mkBreak style cumulatingChunks chunks =
- case splitChunks chunks of
- NONE => NONE
- | SOME (chunks,broken) =>
- let
- val breaks =
- case style of
- InconsistentBlock =>
- [List.concat (broken :: cumulatingChunks)]
- | _ => splitAllChunks cumulatingChunks broken
- in
- SOME (breaks,chunks)
- end;
-
- fun naturalBreak blocks =
- case blocks of
- [] => Right ([],[])
- | block :: blocks =>
- case naturalBreak blocks of
- Left (breaks,blocks,lineIndent,lineSize) =>
- let
- val Block {size,...} = block
-
- val blocks = block :: blocks
-
- val lineSize = lineSize + size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | Right (cumulatingChunks,blocks) =>
- let
- val Block {indent,style,size,chunks} = block
-
- val style = breakStyle style
- in
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val size = sizeChunks chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val lineIndent = indent
-
- val lineSize = size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- let
- val cumulatingChunks = chunks :: cumulatingChunks
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- Right (cumulatingChunks,blocks)
- end
- end;
-
- fun forceBreakBlock cumulatingChunks block =
- let
- val Block {indent, style, size = _, chunks} = block
-
- val style = breakStyle style
-
- val break =
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val lineSize = sizeChunks chunks
- val lineIndent = indent
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => forceBreakChunks cumulatingChunks chunks
- in
- case break of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val size = lineSize
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- in
- SOME (breaks,block,lineIndent,lineSize)
- end
- | NONE => NONE
- end
-
- and forceBreakChunks cumulatingChunks chunks =
- case chunks of
- [] => NONE
- | chunk :: chunks =>
- case forceBreakChunk (chunks :: cumulatingChunks) chunk of
- SOME (breaks,chunk,lineIndent,lineSize) =>
- let
- val chunks = [chunk]
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreakChunks cumulatingChunks chunks of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val chunks = chunk :: chunks
-
- val lineSize = lineSize + sizeChunk chunk
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => NONE
-
- and forceBreakChunk cumulatingChunks chunk =
- case chunk of
- StringChunk _ => NONE
- | BreakChunk _ => raise Bug "Metis_Print.forceBreakChunk: BreakChunk"
- | BlockChunk block =>
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val chunk = BlockChunk block
- in
- SOME (breaks,chunk,lineIndent,lineSize)
- end
- | NONE => NONE;
-
- fun forceBreak cumulatingChunks blocks' blocks =
- case blocks of
- [] => NONE
- | block :: blocks =>
- let
- val cumulatingChunks =
- case cumulatingChunks of
- [] => raise Bug "Metis_Print.forceBreak: null cumulatingChunks"
- | _ :: cumulatingChunks => cumulatingChunks
-
- val blocks' =
- case blocks' of
- [] => raise Bug "Metis_Print.forceBreak: null blocks'"
- | _ :: blocks' => blocks'
- in
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks'
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreak cumulatingChunks blocks' blocks of
- SOME (breaks,blocks,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks
-
- val Block {size,...} = block
-
- val lineSize = lineSize + size
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE => NONE
- end;
-
- fun normalize lineLength lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- if lineIndent + lineSize <= lineLength then (lines,state)
- else
- let
- val break =
- case naturalBreak blocks of
- Left break => SOME break
- | Right (c,b) => forceBreak c b blocks
- in
- case break of
- SOME (breaks,blocks,lineIndent',lineSize) =>
- let
- val lines = renderBreaks lineIndent lineIndent' breaks lines
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent',
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end
- | NONE => (lines,state)
- end
- end;
-
-(*BasicDebug
- val normalize = fn lineLength => fn lines => fn state =>
- let
- val () = checkState state
- in
- normalize lineLength lines state
- end
- handle Bug bug =>
- raise Bug ("Metis_Print.normalize: before normalize:\n" ^ bug)
-*)
-
- fun executeBeginBlock (style,ind) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val Block {indent,...} =
- case blocks of
- [] => raise Bug "Metis_Print.executeBeginBlock: no block"
- | block :: _ => block
-
- val indent = indent + ind
-
- val style = liftStyle style
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeEndBlock lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val (lineSize,blocks) =
- case blocks of
- [] => raise Bug "Metis_Print.executeEndBlock: no block"
- | topBlock :: blocks =>
- let
- val Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks} = topBlock
- in
- case topChunks of
- [] => (lineSize,blocks)
- | headTopChunks :: tailTopChunks =>
- let
- val (lineSize,topSize,topChunks) =
- case headTopChunks of
- BreakChunk spaces =>
- let
- val lineSize = lineSize - spaces
- and topSize = topSize - spaces
- and topChunks = tailTopChunks
- in
- (lineSize,topSize,topChunks)
- end
- | _ => (lineSize,topSize,topChunks)
-
- val topBlock =
- Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks}
- in
- case blocks of
- [] => raise Error "Metis_Print.executeEndBlock: no block"
- | block :: blocks =>
- let
- val Block {indent,style,size,chunks} = block
-
- val size = size + topSize
-
- val chunks = BlockChunk topBlock :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- (lineSize,blocks)
- end
- end
- end
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeAddString lineLength (s,n) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val blocks =
- case blocks of
- [] => raise Bug "Metis_Print.executeAddString: no block"
- | Block {indent,style,size,chunks} :: blocks =>
- let
- val size = size + n
-
- val chunk = StringChunk {size = n, string = s}
-
- val chunks = chunk :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- blocks
- end
-
- val lineSize = lineSize + n
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeAddBreak lineLength spaces lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val (blocks,lineSize) =
- case blocks of
- [] => raise Bug "Metis_Print.executeAddBreak: no block"
- | Block {indent,style,size,chunks} :: blocks' =>
- case chunks of
- [] => (blocks,lineSize)
- | chunk :: chunks' =>
- let
- val spaces =
- case style of
- BreakingBlock => lineLength + 1
- | _ => spaces
-
- val size = size + spaces
-
- val chunks =
- case chunk of
- BreakChunk k => BreakChunk (k + spaces) :: chunks'
- | _ => BreakChunk spaces :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks'
-
- val lineSize = lineSize + spaces
- in
- (blocks,lineSize)
- end
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeBigBreak lineLength lines state =
- executeAddBreak lineLength (lineLength + 1) lines state;
-
- fun executeAddNewline lineLength lines state =
- let
- val (lines,state) =
- executeAddString lineLength emptyStringSize lines state
-
- val (lines,state) =
- executeBigBreak lineLength lines state
- in
- executeAddString lineLength emptyStringSize lines state
- end;
-
- fun final lineLength lines state =
- let
- val lines =
- if isFinalState state then lines
- else
- let
- val (lines,state) = executeBigBreak lineLength lines state
-
-(*BasicDebug
- val _ = isFinalState state orelse raise Bug "Metis_Print.final"
-*)
- in
- lines
- end
- in
- if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
- end;
-in
- fun execute {lineLength} =
- let
- fun advance step state =
- let
- val lines = []
- in
- case step of
- BeginBlock style_ind => executeBeginBlock style_ind lines state
- | EndBlock => executeEndBlock lines state
- | AddString s => executeAddString lineLength s lines state
- | AddBreak spaces => executeAddBreak lineLength spaces lines state
- | AddNewline => executeAddNewline lineLength lines state
- end
-
-(*BasicDebug
- val advance = fn step => fn state =>
- let
- val (lines,state) = advance step state
- val () = checkState state
- in
- (lines,state)
- end
- handle Bug bug =>
- raise Bug ("Metis_Print.advance: after " ^ stepToString step ^
- " command:\n" ^ bug)
-*)
- in
- revConcat o Metis_Stream.maps advance (final lineLength []) initialState
- end;
-end;
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun beginBlock b = Metis_Stream.singleton (BeginBlock b);
+
+ val endBlock = Metis_Stream.singleton EndBlock;
+in
+ fun block b pp = program [beginBlock b, pp, endBlock];
+end;
+
+fun consistentBlock i pps = block (mkConsistentBlock i) (program pps);
+
+fun inconsistentBlock i pps = block (mkInconsistentBlock i) (program pps);
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppWord w = Metis_Stream.singleton (AddWord w);
+
+val space = ppWord (mkWord " ");
+
+fun spaces i = ppWord (spacesWord i);
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppBreak b = Metis_Stream.singleton (AddBreak b);
+
+fun breaks i = ppBreak (mkBreak i);
+
+val break = breaks 1;
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+val newline = Metis_Stream.singleton AddNewline;
+
+fun newlines i = duplicate i newline;
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream;
-
fun ppMap f ppB a : ppstream = ppB (f a);
fun ppBracket' l r ppA a =
let
- val (_,n) = l
- in
- blockProgram Inconsistent n
- [addString l,
+ val n = sizeWord l
+ in
+ inconsistentBlock n
+ [ppWord l,
ppA a,
- addString r]
- end;
-
-fun ppOp' s = sequence (addString s) (addBreak 1);
+ ppWord r]
+ end;
+
+fun ppOp' w = sequence (ppWord w) break;
fun ppOp2' ab ppA ppB (a,b) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b];
fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b,
@@ -7555,7 +7021,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
+ | h :: t => inconsistentBlock 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -7564,30 +7030,30 @@
in
fn Metis_Stream.Nil => skip
| Metis_Stream.Cons (h,t) =>
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA h,
Metis_Stream.concat (Metis_Stream.map ppOpA (t ()))]
end;
-fun ppBracket l r = ppBracket' (mkStringSize l) (mkStringSize r);
-
-fun ppOp s = ppOp' (mkStringSize s);
-
-fun ppOp2 ab = ppOp2' (mkStringSize ab);
-
-fun ppOp3 ab bc = ppOp3' (mkStringSize ab) (mkStringSize bc);
-
-fun ppOpList s = ppOpList' (mkStringSize s);
-
-fun ppOpStream s = ppOpStream' (mkStringSize s);
+fun ppBracket l r = ppBracket' (mkWord l) (mkWord r);
+
+fun ppOp s = ppOp' (mkWord s);
+
+fun ppOp2 ab = ppOp2' (mkWord ab);
+
+fun ppOp3 ab bc = ppOp3' (mkWord ab) (mkWord bc);
+
+fun ppOpList s = ppOpList' (mkWord s);
+
+fun ppOpStream s = ppOpStream' (mkWord s);
(* ------------------------------------------------------------------------- *)
(* Pretty-printers for common types. *)
(* ------------------------------------------------------------------------- *)
-fun ppChar c = addString (str c, 1);
-
-fun ppString s = addString (mkStringSize s);
+fun ppChar c = ppWord (charWord c);
+
+fun ppString s = ppWord (mkWord s);
fun ppEscapeString escape = ppMap (escapeString escape) ppString;
@@ -7644,9 +7110,9 @@
end;
local
- val left = mkStringSize "["
- and right = mkStringSize "]"
- and sep = mkStringSize ",";
+ val left = mkWord "["
+ and right = mkWord "]"
+ and sep = mkWord ",";
in
fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;
@@ -7663,9 +7129,9 @@
end;
local
- val left = mkStringSize "("
- and right = mkStringSize ")"
- and sep = mkStringSize ",";
+ val left = mkWord "("
+ and right = mkWord ")"
+ and sep = mkWord ",";
in
fun ppPair ppA ppB =
ppBracket' left right (ppOp2' sep ppA ppB);
@@ -7674,42 +7140,65 @@
ppBracket' left right (ppOp3' sep sep ppA ppB ppC);
end;
-val ppBreakStyle = ppMap breakStyleToString ppString;
-
-val ppStep = ppMap stepToString ppString;
-
-val ppStringSize =
- let
- val left = mkStringSize "\""
- and right = mkStringSize "\""
- and escape = {escape = [#"\""]}
-
- val pp = ppBracket' left right (ppEscapeString escape)
- in
- fn (s,n) => if size s = n then pp s else ppPair pp ppInt (s,n)
- end;
-
-fun ppStep step =
- blockProgram Inconsistent 2
- (ppStep step ::
- (case step of
- BeginBlock style_indent =>
- [addBreak 1,
- ppPair ppBreakStyle ppInt style_indent]
- | EndBlock => []
- | AddString s =>
- [addBreak 1,
- ppStringSize s]
- | AddBreak n =>
- [addBreak 1,
- ppInt n]
- | AddNewline => []));
-
-val ppPpstream = ppStream ppStep;
-
fun ppException e = ppString (exnMessage e);
(* ------------------------------------------------------------------------- *)
+(* A type of pretty-printers. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val ppStepType = ppMap toStringStep ppString;
+
+ val ppStyle = ppMap toStringStyle ppString;
+
+ val ppBlockInfo =
+ let
+ val sep = mkWord " "
+ in
+ fn Block {style = s, indent = i} =>
+ program [ppStyle s, ppWord sep, ppInt i]
+ end;
+
+ val ppWordInfo =
+ let
+ val left = mkWord "\""
+ and right = mkWord "\""
+ and escape = {escape = [#"\""]}
+
+ val pp = ppBracket' left right (ppEscapeString escape)
+ in
+ fn Word {word = s, size = n} =>
+ if size s = n then pp s else ppPair pp ppInt (s,n)
+ end;
+
+ val ppBreakInfo =
+ let
+ val sep = mkWord "+"
+ in
+ fn Break {size = n, extraIndent = k} =>
+ if k = 0 then ppInt n else program [ppInt n, ppWord sep, ppInt k]
+ end;
+
+ fun ppStep step =
+ inconsistentBlock 2
+ (ppStepType step ::
+ (case step of
+ BeginBlock b =>
+ [break,
+ ppBlockInfo b]
+ | EndBlock => []
+ | AddWord w =>
+ [break,
+ ppWordInfo w]
+ | AddBreak b =>
+ [break,
+ ppBreakInfo b]
+ | AddNewline => []));
+in
+ val ppPpstream = ppStream ppStep;
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
@@ -7815,13 +7304,13 @@
end
in
fn tm_t_a_b_r as (_,t,_,_,_) =>
- if isLayer t then block Inconsistent 0 (ppLayer tm_t_a_b_r)
+ if isLayer t then inconsistentBlock 0 [ppLayer tm_t_a_b_r]
else ppLower tm_t_a_b_r
end;
local
- val leftBrack = mkStringSize "("
- and rightBrack = mkStringSize ")";
+ val leftBrack = mkWord "("
+ and rightBrack = mkWord ")";
in
fun ppInfixes ops =
let
@@ -7855,37 +7344,947 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
-(* ------------------------------------------------------------------------- *)
-
-val lineLength = Unsynchronized.ref initialLineLength;
+(* A type of output lines. *)
+(* ------------------------------------------------------------------------- *)
+
+type line = {indent : int, line : string};
+
+val emptyLine =
+ let
+ val indent = 0
+ and line = ""
+ in
+ {indent = indent,
+ line = line}
+ end;
+
+fun addEmptyLine lines = emptyLine :: lines;
+
+fun addLine lines indent line = {indent = indent, line = line} :: lines;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype chunk =
+ WordChunk of word
+ | BreakChunk of break
+ | FrameChunk of frame
+
+and frame =
+ Frame of
+ {block : block,
+ broken : bool,
+ indent : int,
+ size : int,
+ chunks : chunk list};
+
+datatype state =
+ State of
+ {lineIndent : int,
+ lineSize : int,
+ stack : frame list};
+
+fun blockFrame (Frame {block = x, ...}) = x;
+
+fun brokenFrame (Frame {broken = x, ...}) = x;
+
+fun indentFrame (Frame {indent = x, ...}) = x;
+
+fun sizeFrame (Frame {size = x, ...}) = x;
+
+fun chunksFrame (Frame {chunks = x, ...}) = x;
+
+fun styleFrame frame = styleBlock (blockFrame frame);
+
+fun isConsistentFrame frame = isConsistentBlock (blockFrame frame);
+
+fun breakingFrame frame = isConsistentFrame frame andalso brokenFrame frame;
+
+fun sizeChunk chunk =
+ case chunk of
+ WordChunk w => sizeWord w
+ | BreakChunk b => sizeBreak b
+ | FrameChunk f => sizeFrame f;
+
+local
+ fun add (c,acc) = sizeChunk c + acc;
+in
+ fun sizeChunks cs = List.foldl add 0 cs;
+end;
+
+local
+ fun flattenChunks acc chunks =
+ case chunks of
+ [] => acc
+ | chunk :: chunks => flattenChunk acc chunk chunks
+
+ and flattenChunk acc chunk chunks =
+ case chunk of
+ WordChunk w => flattenChunks (renderWord w :: acc) chunks
+ | BreakChunk b => flattenChunks (renderBreak b :: acc) chunks
+ | FrameChunk f => flattenFrame acc f chunks
+
+ and flattenFrame acc frame chunks =
+ flattenChunks acc (chunksFrame frame @ chunks);
+in
+ fun renderChunks chunks = String.concat (flattenChunks [] chunks);
+end;
+
+fun addChunksLine lines indent chunks =
+ addLine lines indent (renderChunks chunks);
+
+local
+ fun add baseIndent ((extraIndent,chunks),lines) =
+ addChunksLine lines (baseIndent + extraIndent) chunks;
+in
+ fun addIndentChunksLines lines baseIndent indent_chunks =
+ List.foldl (add baseIndent) lines indent_chunks;
+end;
+
+fun isEmptyFrame frame =
+ let
+ val chunks = chunksFrame frame
+
+ val empty = List.null chunks
+
+(*BasicDebug
+ val () =
+ if not empty orelse sizeFrame frame = 0 then ()
+ else raise Bug "Metis_Print.isEmptyFrame: bad size"
+*)
+ in
+ empty
+ end;
+
+local
+ fun breakInconsistent blockIndent =
+ let
+ fun break chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case chunk of
+ BreakChunk b =>
+ let
+ val pre = chunks
+ and indent = blockIndent + extraIndentBreak b
+ and post = []
+ in
+ SOME (pre,indent,post)
+ end
+ | _ =>
+ case break chunks of
+ SOME (pre,indent,post) =>
+ let
+ val post = chunk :: post
+ in
+ SOME (pre,indent,post)
+ end
+ | NONE => NONE
+ in
+ break
+ end;
+
+ fun breakConsistent blockIndent =
+ let
+ fun break indent_chunks chunks =
+ case breakInconsistent blockIndent chunks of
+ NONE => (chunks,indent_chunks)
+ | SOME (pre,indent,post) =>
+ break ((indent,post) :: indent_chunks) pre
+ in
+ break []
+ end;
+in
+ fun breakFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent = _,
+ size = _,
+ chunks} = frame
+
+ val blockIndent = indentBlock block
+ in
+ case breakInconsistent blockIndent chunks of
+ NONE => NONE
+ | SOME (pre,indent,post) =>
+ let
+ val broken = true
+ and size = sizeChunks post
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = post}
+ in
+ case styleBlock block of
+ Inconsistent =>
+ let
+ val indent_chunks = []
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ | Consistent =>
+ let
+ val (pre,indent_chunks) = breakConsistent blockIndent pre
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ end
+ end;
+end;
+
+fun removeChunksFrame frame =
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ if broken andalso List.null chunks then NONE
+ else
+ let
+ val frame =
+ Frame
+ {block = block,
+ broken = true,
+ indent = indent,
+ size = 0,
+ chunks = []}
+ in
+ SOME (chunks,frame)
+ end
+ end;
+
+val removeChunksFrames =
+ let
+ fun remove frames =
+ case frames of
+ [] =>
+ let
+ val chunks = []
+ and frames = NONE
+ and indent = 0
+ in
+ (chunks,frames,indent)
+ end
+ | top :: rest =>
+ let
+ val (chunks,rest',indent) = remove rest
+
+ val indent = indent + indentFrame top
+
+ val (chunks,top') =
+ case removeChunksFrame top of
+ NONE => (chunks,NONE)
+ | SOME (topChunks,top) => (topChunks @ chunks, SOME top)
+
+ val frames' =
+ case (top',rest') of
+ (NONE,NONE) => NONE
+ | (SOME top, NONE) => SOME (top :: rest)
+ | (NONE, SOME rest) => SOME (top :: rest)
+ | (SOME top, SOME rest) => SOME (top :: rest)
+ in
+ (chunks,frames',indent)
+ end
+ in
+ fn frames =>
+ let
+ val (chunks,frames',indent) = remove frames
+
+ val frames = Option.getOpt (frames',frames)
+ in
+ (chunks,frames,indent)
+ end
+ end;
+
+local
+ fun breakUp lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakUp lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE =>
+ case breakFrame frame of
+ NONE => NONE
+ | SOME (frameChunks,indent_chunks,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = frameChunks @ chunks
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + indentFrame frame
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end;
+
+ fun breakInsideChunk chunk =
+ case chunk of
+ WordChunk _ => NONE
+ | BreakChunk _ => raise Bug "Metis_Print.breakInsideChunk"
+ | FrameChunk frame =>
+ case breakFrame frame of
+ SOME (pathChunks,indent_chunks,frame) =>
+ let
+ val pathIndent = 0
+ and breakIndent = indentFrame frame
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => breakInsideFrame frame
+
+ and breakInsideChunks chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case breakInsideChunk chunk of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val pathChunks = pathChunks @ chunks
+ and chunks = [FrameChunk frame]
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE =>
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val chunks = chunk :: chunks
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE => NONE
+
+ and breakInsideFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val pathIndent = pathIndent + indent
+ and broken = true
+ and size = sizeChunks chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => NONE
+ end;
+
+ fun breakInside lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakInsideFrame frame of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = pathChunks @ chunks
+ and indent = indent + pathIndent
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + breakIndent
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE => NONE;
+in
+ fun breakFrames lines lineIndent frames =
+ case breakUp lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE => NONE;
+end;
+
+(*BasicDebug
+fun checkChunk chunk =
+ case chunk of
+ WordChunk t => (false, sizeWord t)
+ | BreakChunk b => (false, sizeBreak b)
+ | FrameChunk b => checkFrame b
+
+and checkChunks chunks =
+ case chunks of
+ [] => (false,0)
+ | chunk :: chunks =>
+ let
+ val (bk,sz) = checkChunk chunk
+
+ val (bk',sz') = checkChunks chunks
+ in
+ (bk orelse bk', sz + sz')
+ end
+
+and checkFrame frame =
+ let
+ val Frame
+ {block = _,
+ broken,
+ indent = _,
+ size,
+ chunks} = frame
+
+ val (bk,sz) = checkChunks chunks
+
+ val () =
+ if size = sz then ()
+ else raise Bug "Metis_Print.checkFrame: wrong size"
+
+ val () =
+ if broken orelse not bk then ()
+ else raise Bug "Metis_Print.checkFrame: deep broken frame"
+ in
+ (broken,size)
+ end;
+
+fun checkFrames frames =
+ case frames of
+ [] => (true,0)
+ | frame :: frames =>
+ let
+ val (bk,sz) = checkFrame frame
+
+ val (bk',sz') = checkFrames frames
+
+ val () =
+ if bk' orelse not bk then ()
+ else raise Bug "Metis_Print.checkFrame: broken stack frame"
+ in
+ (bk, sz + sz')
+ end;
+*)
+
+(*BasicDebug
+fun checkState state =
+ (let
+ val State {lineIndent,lineSize,stack} = state
+
+ val () =
+ if not (List.null stack) then ()
+ else raise Error "no stack"
+
+ val (_,sz) = checkFrames stack
+
+ val () =
+ if lineSize = sz then ()
+ else raise Error "wrong lineSize"
+ in
+ ()
+ end
+ handle Error err => raise Bug err)
+ handle Bug bug => raise Bug ("Metis_Print.checkState: " ^ bug);
+*)
+
+fun isEmptyState state =
+ let
+ val State {lineSize,stack,...} = state
+ in
+ lineSize = 0 andalso List.all isEmptyFrame stack
+ end;
+
+fun isFinalState state =
+ let
+ val State {stack,...} = state
+ in
+ case stack of
+ [] => raise Bug "Metis_Print.isFinalState: empty stack"
+ | [frame] => isEmptyFrame frame
+ | _ :: _ :: _ => false
+ end;
+
+local
+ val initialBlock =
+ let
+ val indent = 0
+ and style = Inconsistent
+ in
+ Block
+ {indent = indent,
+ style = style}
+ end;
+
+ val initialFrame =
+ let
+ val block = initialBlock
+ and broken = false
+ and indent = 0
+ and size = 0
+ and chunks = []
+ in
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ end;
+in
+ val initialState =
+ let
+ val lineIndent = 0
+ and lineSize = 0
+ and stack = [initialFrame]
+ in
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ end;
+end;
+
+fun normalizeState lineLength lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val within =
+ case lineLength of
+ NONE => true
+ | SOME len => lineIndent + lineSize <= len
+ in
+ if within then (lines,state)
+ else
+ case breakFrames lines lineIndent stack of
+ NONE => (lines,state)
+ | SOME (lines,lineIndent,lineSize,stack) =>
+ let
+(*BasicDebug
+ val () = checkState state
+*)
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Metis_Print.normalizeState:\n" ^ bug)
+*)
+
+local
+ fun executeBeginBlock block lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val broken = false
+ and indent = indentBlock block
+ and size = 0
+ and chunks = []
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeEndBlock lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (lineSize,stack) =
+ case stack of
+ [] => raise Bug "Metis_Print.executeEndBlock: empty stack"
+ | topFrame :: stack =>
+ let
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+
+ val (lineSize,topSize,topChunks,topFrame) =
+ case topChunks of
+ BreakChunk break :: chunks =>
+ let
+(*BasicDebug
+ val () =
+ let
+ val mesg =
+ "ignoring a break at the end of a " ^
+ "pretty-printing block"
+ in
+ warn mesg
+ end
+*)
+ val n = sizeBreak break
+
+ val lineSize = lineSize - n
+ and topSize = topSize - n
+ and topChunks = chunks
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+ in
+ (lineSize,topSize,topChunks,topFrame)
+ end
+ | _ => (lineSize,topSize,topChunks,topFrame)
+ in
+ if List.null topChunks then (lineSize,stack)
+ else
+ case stack of
+ [] => raise Error "Metis_Print.execute: too many end blocks"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + topSize
+
+ val chunk = FrameChunk topFrame
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ (lineSize,stack)
+ end
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeAddWord lineLength word lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val n = sizeWord word
+
+ val lineSize = lineSize + n
+
+ val stack =
+ case stack of
+ [] => raise Bug "Metis_Print.executeAddWord: empty stack"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + n
+
+ val chunk = WordChunk word
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ stack
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end;
+
+ fun executeAddBreak lineLength break lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (topFrame,restFrames) =
+ case stack of
+ [] => raise Bug "Metis_Print.executeAddBreak: empty stack"
+ | topFrame :: restFrames => (topFrame,restFrames)
+
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+ in
+ case topChunks of
+ [] => (lines,state)
+ | topChunk :: restTopChunks =>
+ let
+ val (topChunks,n) =
+ case topChunk of
+ BreakChunk break' =>
+ let
+ val break = appendBreak break' break
+
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: restTopChunks
+ and n = sizeBreak break - sizeBreak break'
+ in
+ (topChunks,n)
+ end
+ | _ =>
+ let
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: topChunks
+ and n = sizeBreak break
+ in
+ (topChunks,n)
+ end
+
+ val lineSize = lineSize + n
+
+ val topSize = topSize + n
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+
+ val stack = topFrame :: restFrames
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+
+ val lineLength =
+ if breakingFrame topFrame then SOME ~1 else lineLength
+ in
+ normalizeState lineLength lines state
+ end
+ end;
+
+ fun executeBigBreak lines state =
+ let
+ val lineLength = SOME ~1
+ and break = mkBreak 0
+ in
+ executeAddBreak lineLength break lines state
+ end;
+
+ fun executeAddNewline lineLength lines state =
+ if isEmptyState state then (addEmptyLine lines, state)
+ else executeBigBreak lines state;
+
+ fun executeEof lineLength lines state =
+ if isFinalState state then (lines,state)
+ else
+ let
+ val (lines,state) = executeBigBreak lines state
+
+(*BasicDebug
+ val () =
+ if isFinalState state then ()
+ else raise Bug "Metis_Print.executeEof: not a final state"
+*)
+ in
+ (lines,state)
+ end;
+in
+ fun render {lineLength} =
+ let
+ fun execute step state =
+ let
+ val lines = []
+ in
+ case step of
+ BeginBlock block => executeBeginBlock block lines state
+ | EndBlock => executeEndBlock lines state
+ | AddWord word => executeAddWord lineLength word lines state
+ | AddBreak break => executeAddBreak lineLength break lines state
+ | AddNewline => executeAddNewline lineLength lines state
+ end
+
+(*BasicDebug
+ val execute = fn step => fn state =>
+ let
+ val (lines,state) = execute step state
+
+ val () = checkState state
+ in
+ (lines,state)
+ end
+ handle Bug bug =>
+ raise Bug ("Metis_Print.execute: after " ^ toStringStep step ^
+ " command:\n" ^ bug)
+*)
+
+ fun final state =
+ let
+ val lines = []
+
+ val (lines,state) = executeEof lineLength lines state
+
+(*BasicDebug
+ val () = checkState state
+*)
+ in
+ if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Metis_Print.final: " ^ bug)
+*)
+ in
+ fn pps =>
+ let
+ val lines = Metis_Stream.maps execute final initialState pps
+ in
+ revConcat lines
+ end
+ end;
+end;
local
fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
in
- fun toLines len ppA a =
- case execute {lineLength = len} (ppA a) of
+ fun toStringWithLineLength len ppA a =
+ case render len (ppA a) of
Metis_Stream.Nil => ""
| Metis_Stream.Cons (h,t) =>
let
val lines = Metis_Stream.foldl incn (inc h []) (t ())
in
- String.concat (rev lines)
+ String.concat (List.rev lines)
end;
end;
-fun toString ppA a = toLines (!lineLength) ppA a;
-
-fun toLine ppA a = toLines 100000 ppA a;
+local
+ fun renderLine {indent,line} = nSpaces indent ^ line ^ "\n";
+in
+ fun toStreamWithLineLength len ppA a =
+ Metis_Stream.map renderLine (render len (ppA a));
+end;
+
+fun toLine ppA a = toStringWithLineLength {lineLength = NONE} ppA a;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
+(* ------------------------------------------------------------------------- *)
+
+val lineLength = Unsynchronized.ref initialLineLength;
+
+fun toString ppA a =
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStringWithLineLength len ppA a
+ end;
fun toStream ppA a =
- Metis_Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
- (execute {lineLength = !lineLength} (ppA a));
-
-local
- val sep = mkStringSize " =";
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStreamWithLineLength len ppA a
+ end;
+
+local
+ val sep = mkWord " =";
in
fun trace ppX nameX x =
Metis_Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
@@ -8079,7 +8478,7 @@
let
fun sparser l = parser >> (fn x => x :: l)
in
- mmany sparser [] >> rev
+ mmany sparser [] >> List.rev
end;
fun atLeastOne p = (p ++ many p) >> op::;
@@ -8240,7 +8639,7 @@
| [(t,y)] => mk (t,x,y)
| _ => raise NoParse)
| Metis_Print.RightAssoc =>
- (case rev txs of
+ (case List.rev txs of
[] => x
| tx :: txs =>
let
@@ -8530,7 +8929,7 @@
(* ------------------------------------------------------------------------- *)
fun pp (n,i) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 0
+ Metis_Print.inconsistentBlock 0
[Metis_Name.pp n,
Metis_Print.ppString "/",
Metis_Print.ppInt i];
@@ -8931,7 +9330,7 @@
let
fun f (n,arg) = (n :: path, arg)
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
in
case tm of
Var _ => subtms rest acc
@@ -8960,7 +9359,7 @@
let
fun search [] = NONE
| search ((path,tm) :: rest) =
- if pred tm then SOME (rev path)
+ if pred tm then SOME (List.rev path)
else
case tm of
Var _ => search rest
@@ -9072,7 +9471,7 @@
Var _ => subtms rest acc
| Fn _ =>
let
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = (0 :: path, t) :: rest
in
subtms rest acc
@@ -9083,7 +9482,7 @@
val (_,args) = func
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = List.map f (enumerate args) @ rest
in
@@ -9220,7 +9619,7 @@
Metis_Print.program
[(if tok = "," then Metis_Print.skip else Metis_Print.ppString " "),
Metis_Print.ppString tok,
- Metis_Print.addBreak 1];
+ Metis_Print.break];
val iPrinter = Metis_Print.ppInfixes iOps destI iToken
@@ -9286,14 +9685,14 @@
fun functionArgument bv tm =
Metis_Print.sequence
- (Metis_Print.addBreak 1)
+ Metis_Print.break
(if isBrack tm then customBracket bv tm
else if isVar tm orelse isConst tm then basic bv tm
else bracket bv tm)
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
(functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
@@ -9312,21 +9711,21 @@
[Metis_Print.ppString q,
varName bv v,
Metis_Print.program
- (List.map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
+ (List.map (Metis_Print.sequence Metis_Print.break o varName bv) vs),
Metis_Print.ppString ".",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
innerQuant bv tm]
end
and quantifier bv tm =
if not (isQuant tm) then customBracket bv tm
- else Metis_Print.block Metis_Print.Inconsistent 2 (innerQuant bv tm)
+ else Metis_Print.inconsistentBlock 2 [innerQuant bv tm]
and molecule bv (tm,r) =
let
val (n,tm) = stripNeg tm
in
- Metis_Print.blockProgram Metis_Print.Inconsistent n
+ Metis_Print.inconsistentBlock n
[Metis_Print.duplicate n (Metis_Print.ppString neg),
if isI tm orelse (r andalso isQuant tm) then bracket bv tm
else quantifier bv tm]
@@ -10626,11 +11025,11 @@
(* Conjunctions *)
fun listMkConj fms =
- case rev fms of [] => True | fm :: fms => List.foldl And fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl And fm fms;
local
fun strip cs (And (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripConj True = []
| stripConj fm = strip [] fm;
@@ -10649,11 +11048,11 @@
(* Disjunctions *)
fun listMkDisj fms =
- case rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
+ case List.rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
local
fun strip cs (Or (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripDisj False = []
| stripDisj fm = strip [] fm;
@@ -10672,11 +11071,11 @@
(* Equivalences *)
fun listMkEquiv fms =
- case rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
local
fun strip cs (Iff (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripEquiv True = []
| stripEquiv fm = strip [] fm;
@@ -10706,7 +11105,7 @@
local
fun strip vs (Forall (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripForall = strip [];
end;
@@ -10725,7 +11124,7 @@
local
fun strip vs (Exists (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripExists = strip [];
end;
@@ -11030,7 +11429,7 @@
local
fun add_asms asms goal =
- if List.null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (List.rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
@@ -11810,7 +12209,7 @@
(List.map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
in
fun pp th =
- Metis_Print.blockProgram Metis_Print.Inconsistent 3
+ Metis_Print.inconsistentBlock 3
[Metis_Print.ppString "|- ",
Metis_Formula.pp (toFormula th)];
end;
@@ -12015,43 +12414,43 @@
| inferenceType (Equality _) = Metis_Thm.Equality;
local
- fun ppAssume atm = Metis_Print.sequence (Metis_Print.addBreak 1) (Metis_Atom.pp atm);
+ fun ppAssume atm = Metis_Print.sequence Metis_Print.break (Metis_Atom.pp atm);
fun ppSubst ppThm (sub,thm) =
- Metis_Print.sequence (Metis_Print.addBreak 1)
- (Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.sequence Metis_Print.break
+ (Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Subst.pp ("sub",sub),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("thm",thm),
Metis_Print.ppString "}"]);
fun ppResolve ppThm (res,pos,neg) =
- Metis_Print.sequence (Metis_Print.addBreak 1)
- (Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.sequence Metis_Print.break
+ (Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Atom.pp ("res",res),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("pos",pos),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString ppThm ("neg",neg),
Metis_Print.ppString "}"]);
- fun ppRefl tm = Metis_Print.sequence (Metis_Print.addBreak 1) (Metis_Term.pp tm);
+ fun ppRefl tm = Metis_Print.sequence Metis_Print.break (Metis_Term.pp tm);
fun ppEquality (lit,path,res) =
- Metis_Print.sequence (Metis_Print.addBreak 1)
- (Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.sequence Metis_Print.break
+ (Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Literal.pp ("lit",lit),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Term.ppPath ("path",path),
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Print.ppOp2 " =" Metis_Print.ppString Metis_Term.pp ("res",res),
Metis_Print.ppString "}"]);
@@ -12059,21 +12458,20 @@
let
val infString = Metis_Thm.inferenceTypeToString (inferenceType inf)
in
- Metis_Print.block Metis_Print.Inconsistent 2
- (Metis_Print.sequence
- (Metis_Print.ppString infString)
- (case inf of
- Axiom cl => ppAxiom cl
- | Assume x => ppAssume x
- | Metis_Subst x => ppSubst ppThm x
- | Resolve x => ppResolve ppThm x
- | Refl x => ppRefl x
- | Equality x => ppEquality x))
+ Metis_Print.inconsistentBlock 2
+ [Metis_Print.ppString infString,
+ (case inf of
+ Axiom cl => ppAxiom cl
+ | Assume x => ppAssume x
+ | Metis_Subst x => ppSubst ppThm x
+ | Resolve x => ppResolve ppThm x
+ | Refl x => ppRefl x
+ | Equality x => ppEquality x)]
end;
fun ppAxiom cl =
Metis_Print.sequence
- (Metis_Print.addBreak 1)
+ Metis_Print.break
(Metis_Print.ppMap
Metis_LiteralSet.toList
(Metis_Print.ppBracket "{" "}" (Metis_Print.ppOpList "," Metis_Literal.pp)) cl);
@@ -12103,17 +12501,17 @@
val s = thmString n
in
Metis_Print.sequence
- (Metis_Print.blockProgram Metis_Print.Consistent (1 + size s)
+ (Metis_Print.consistentBlock (1 + size s)
[Metis_Print.ppString (s ^ " "),
Metis_Thm.pp th,
- Metis_Print.addBreak 2,
+ Metis_Print.breaks 2,
Metis_Print.ppBracket "[" "]" (ppInf (K Metis_Print.skip) ppThm) inf])
- Metis_Print.addNewline
- end
- in
- Metis_Print.blockProgram Metis_Print.Consistent 0
+ Metis_Print.newline
+ end
+ in
+ Metis_Print.consistentBlock 0
[Metis_Print.ppString "START OF PROOF",
- Metis_Print.addNewline,
+ Metis_Print.newline,
Metis_Print.program (List.map ppStep prf),
Metis_Print.ppString "END OF PROOF"]
end
@@ -12215,7 +12613,7 @@
val path = i :: path
in
if Metis_Term.equal tm s andalso Metis_Term.equal tm' t then
- SOME (rev path)
+ SOME (List.rev path)
else
case (tm,tm') of
(Metis_Term.Fn f_a, Metis_Term.Fn f_a') => sync s t path f_a f_a'
@@ -12377,7 +12775,7 @@
val () = Metis_Print.trace Metis_Print.ppInt "Metis_Proof.proof: unnecessary clauses" (Metis_LiteralSetMap.size ths)
*)
in
- rev acc
+ List.rev acc
end;
in
fun proof th =
@@ -14502,7 +14900,7 @@
fun prove acc proved ths =
case ths of
- [] => rev acc
+ [] => List.rev acc
| th :: ths' =>
if isProved proved th then prove acc proved ths'
else
@@ -14934,7 +15332,7 @@
let
val (cls,_) = List.foldl add ([],initialCnf) ths
in
- rev cls
+ List.rev cls
end;
end;
@@ -15502,12 +15900,12 @@
fun mkList tag m = List.map (mkEntry tag) (Metis_NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString tag,
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_NameArity.pp source_arity,
Metis_Print.ppString " ->",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
Metis_Name.pp target];
in
fun ppFixedMap fixMap =
@@ -15517,9 +15915,9 @@
case mkList "function" fnMap @ mkList "relation" relMap of
[] => Metis_Print.skip
| entry :: entries =>
- Metis_Print.blockProgram Metis_Print.Consistent 0
+ Metis_Print.consistentBlock 0
(ppEntry entry ::
- List.map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
+ List.map (Metis_Print.sequence Metis_Print.newline o ppEntry) entries)
end;
end;
@@ -18300,9 +18698,9 @@
Metis_Print.ppOp2 (" " ^ toStringOrientOption ort) Metis_Term.pp Metis_Term.pp x_y;
fun ppField f ppA a =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString (f ^ " ="),
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppA a];
val ppKnown =
@@ -18326,21 +18724,21 @@
(Metis_Print.ppMap (Metis_IntSet.toList) (Metis_Print.ppList Metis_Print.ppInt));
in
fun pp (Metis_Rewrite {known,redexes,subterms,waiting,...}) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString "Metis_Rewrite",
- Metis_Print.addBreak 1,
- Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.break,
+ Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
ppKnown known,
(*MetisTrace5
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppRedexes redexes,
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppSubterms subterms,
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppWaiting waiting,
*)
Metis_Print.skip],
@@ -19924,9 +20322,9 @@
(*MetisDebug
local
fun ppField f ppA a =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString (f ^ " ="),
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppA a];
val ppClauses =
@@ -19945,18 +20343,18 @@
Metis_Term.pp)));
in
fun pp (Metis_Active {clauses,rewrite,subterms,...}) =
- Metis_Print.blockProgram Metis_Print.Inconsistent 2
+ Metis_Print.inconsistentBlock 2
[Metis_Print.ppString "Metis_Active",
- Metis_Print.addBreak 1,
- Metis_Print.blockProgram Metis_Print.Inconsistent 1
+ Metis_Print.break,
+ Metis_Print.inconsistentBlock 1
[Metis_Print.ppString "{",
ppClauses clauses,
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppRewrite rewrite,
(*MetisTrace5
Metis_Print.ppString ",",
- Metis_Print.addBreak 1,
+ Metis_Print.break,
ppSubterms subterms,
*)
Metis_Print.skip],
@@ -20194,7 +20592,7 @@
val acc = Metis_LiteralSet.foldl (deduceResolution literals cl) acc lits
val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
- val acc = rev acc
+ val acc = List.rev acc
(*MetisTrace5
val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Active.deduce: acc" acc
@@ -20442,7 +20840,7 @@
List.foldl factor_add active_subsume_acc cls
end;
- fun factor' active acc [] = (active, rev acc)
+ fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
--- a/src/Tools/Metis/src/Active.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Active.sml Wed Dec 07 16:03:05 2011 +0100
@@ -320,9 +320,9 @@
(*MetisDebug
local
fun ppField f ppA a =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString (f ^ " ="),
- Print.addBreak 1,
+ Print.break,
ppA a];
val ppClauses =
@@ -341,18 +341,18 @@
Term.pp)));
in
fun pp (Active {clauses,rewrite,subterms,...}) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString "Active",
- Print.addBreak 1,
- Print.blockProgram Print.Inconsistent 1
+ Print.break,
+ Print.inconsistentBlock 1
[Print.ppString "{",
ppClauses clauses,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppRewrite rewrite,
(*MetisTrace5
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppSubterms subterms,
*)
Print.skip],
@@ -590,7 +590,7 @@
val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits
val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
- val acc = rev acc
+ val acc = List.rev acc
(*MetisTrace5
val () = Print.trace (Print.ppList Clause.pp) "Active.deduce: acc" acc
@@ -838,7 +838,7 @@
List.foldl factor_add active_subsume_acc cls
end;
- fun factor' active acc [] = (active, rev acc)
+ fun factor' active acc [] = (active, List.rev acc)
| factor' active acc cls =
let
val cls = sort_utilitywise cls
--- a/src/Tools/Metis/src/ElementSet.sig Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/ElementSet.sig Wed Dec 07 16:03:05 2011 +0100
@@ -12,6 +12,10 @@
type element
+val compareElement : element * element -> order
+
+val equalElement : element -> element -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/ElementSet.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/ElementSet.sml Wed Dec 07 16:03:05 2011 +0100
@@ -16,6 +16,10 @@
type element = KM.key;
+val compareElement = KM.compareKey;
+
+val equalElement = KM.equalKey;
+
(* ------------------------------------------------------------------------- *)
(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Formula.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Formula.sml Wed Dec 07 16:03:05 2011 +0100
@@ -145,11 +145,11 @@
(* Conjunctions *)
fun listMkConj fms =
- case rev fms of [] => True | fm :: fms => List.foldl And fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl And fm fms;
local
fun strip cs (And (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripConj True = []
| stripConj fm = strip [] fm;
@@ -168,11 +168,11 @@
(* Disjunctions *)
fun listMkDisj fms =
- case rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
+ case List.rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
local
fun strip cs (Or (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripDisj False = []
| stripDisj fm = strip [] fm;
@@ -191,11 +191,11 @@
(* Equivalences *)
fun listMkEquiv fms =
- case rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
+ case List.rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
local
fun strip cs (Iff (p,q)) = strip (p :: cs) q
- | strip cs fm = rev (fm :: cs);
+ | strip cs fm = List.rev (fm :: cs);
in
fun stripEquiv True = []
| stripEquiv fm = strip [] fm;
@@ -225,7 +225,7 @@
local
fun strip vs (Forall (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripForall = strip [];
end;
@@ -244,7 +244,7 @@
local
fun strip vs (Exists (v,b)) = strip (v :: vs) b
- | strip vs tm = (rev vs, tm);
+ | strip vs tm = (List.rev vs, tm);
in
val stripExists = strip [];
end;
@@ -549,7 +549,7 @@
local
fun add_asms asms goal =
- if List.null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (List.rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
--- a/src/Tools/Metis/src/KeyMap.sig Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/KeyMap.sig Wed Dec 07 16:03:05 2011 +0100
@@ -12,6 +12,10 @@
type key
+val compareKey : key * key -> order
+
+val equalKey : key -> key -> bool
+
(* ------------------------------------------------------------------------- *)
(* A type of finite maps. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Model.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Model.sml Wed Dec 07 16:03:05 2011 +0100
@@ -271,12 +271,12 @@
fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString tag,
- Print.addBreak 1,
+ Print.break,
NameArity.pp source_arity,
Print.ppString " ->",
- Print.addBreak 1,
+ Print.break,
Name.pp target];
in
fun ppFixedMap fixMap =
@@ -286,9 +286,9 @@
case mkList "function" fnMap @ mkList "relation" relMap of
[] => Print.skip
| entry :: entries =>
- Print.blockProgram Print.Consistent 0
+ Print.consistentBlock 0
(ppEntry entry ::
- List.map (Print.sequence Print.addNewline o ppEntry) entries)
+ List.map (Print.sequence Print.newline o ppEntry) entries)
end;
end;
--- a/src/Tools/Metis/src/NameArity.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/NameArity.sml Wed Dec 07 16:03:05 2011 +0100
@@ -44,7 +44,7 @@
(* ------------------------------------------------------------------------- *)
fun pp (n,i) =
- Print.blockProgram Print.Inconsistent 0
+ Print.inconsistentBlock 0
[Name.pp n,
Print.ppString "/",
Print.ppInt i];
--- a/src/Tools/Metis/src/Normalize.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Normalize.sml Wed Dec 07 16:03:05 2011 +0100
@@ -942,7 +942,7 @@
fun prove acc proved ths =
case ths of
- [] => rev acc
+ [] => List.rev acc
| th :: ths' =>
if isProved proved th then prove acc proved ths'
else
@@ -1374,7 +1374,7 @@
let
val (cls,_) = List.foldl add ([],initialCnf) ths
in
- rev cls
+ List.rev cls
end;
end;
--- a/src/Tools/Metis/src/Options.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Options.sml Wed Dec 07 16:03:05 2011 +0100
@@ -6,8 +6,6 @@
structure Options :> Options =
struct
-infix ##
-
open Useful;
(* ------------------------------------------------------------------------- *)
@@ -227,19 +225,21 @@
val (r,f) = findOption x
val (ys,xs) = getArgs x r xs
val () = f (x,ys)
+
+ val (xys,xs) = process xs
in
- (cons (x,ys) ## I) (process xs)
+ ((x,ys) :: xys, xs)
end
in
fn l =>
- let
- val (a,b) = process l
+ let
+ val (a,b) = process l
- val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
- in
- (a,b)
- end
- handle OptionExit x => exit allopts x
+ val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (List.rev a)
+ in
+ (a,b)
+ end
+ handle OptionExit x => exit allopts x
end;
end
--- a/src/Tools/Metis/src/Parse.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Parse.sml Wed Dec 07 16:03:05 2011 +0100
@@ -65,7 +65,7 @@
let
fun sparser l = parser >> (fn x => x :: l)
in
- mmany sparser [] >> rev
+ mmany sparser [] >> List.rev
end;
fun atLeastOne p = (p ++ many p) >> op::;
@@ -226,7 +226,7 @@
| [(t,y)] => mk (t,x,y)
| _ => raise NoParse)
| Print.RightAssoc =>
- (case rev txs of
+ (case List.rev txs of
[] => x
| tx :: txs =>
let
--- a/src/Tools/Metis/src/PortableMosml.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/PortableMosml.sml Wed Dec 07 16:03:05 2011 +0100
@@ -77,7 +77,8 @@
and implode = ()
and map = ()
and null = ()
-and print = ();
+and print = ()
+and rev = ();
*)
(* ------------------------------------------------------------------------- *)
@@ -121,7 +122,7 @@
fn [] => ""
| x :: xs =>
let
- val xs = List.foldl add [] (rev xs)
+ val xs = List.foldl add [] (List.rev xs)
in
String.concat (x :: xs)
end
--- a/src/Tools/Metis/src/Print.sig Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Print.sig Wed Dec 07 16:03:05 2011 +0100
@@ -13,41 +13,12 @@
val escapeString : {escape : char list} -> string -> string
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
-(* ------------------------------------------------------------------------- *)
-
-type stringSize = string * int
-
-val mkStringSize : string -> stringSize
-
-(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent
-
-datatype step =
- BeginBlock of breakStyle * int
- | EndBlock
- | AddString of stringSize
- | AddBreak of int
- | AddNewline
-
-type ppstream = step Stream.stream
+type ppstream
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-val beginBlock : breakStyle -> int -> ppstream
-
-val endBlock : ppstream
-
-val addString : stringSize -> ppstream
-
-val addBreak : int -> ppstream
-
-val addNewline : ppstream
+type 'a pp = 'a -> ppstream
val skip : ppstream
@@ -59,28 +30,75 @@
val stream : ppstream Stream.stream -> ppstream
-val block : breakStyle -> int -> ppstream -> ppstream
+val ppPpstream : ppstream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent
-val blockProgram : breakStyle -> int -> ppstream list -> ppstream
+datatype block =
+ Block of
+ {style : style,
+ indent : int}
+
+val styleBlock : block -> style
+
+val indentBlock : block -> int
+
+val block : block -> ppstream -> ppstream
+
+val consistentBlock : int -> ppstream list -> ppstream
+
+val inconsistentBlock : int -> ppstream list -> ppstream
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
+(* Words are unbreakable strings annotated with their effective size. *)
(* ------------------------------------------------------------------------- *)
-val execute :
- {lineLength : int} -> ppstream ->
- {indent : int, line : string} Stream.stream
+datatype word = Word of {word : string, size : int}
+
+val mkWord : string -> word
+
+val emptyWord : word
+
+val charWord : char -> word
+
+val ppWord : word pp
+
+val space : ppstream
+
+val spaces : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int}
+
+val mkBreak : int -> break
+
+val ppBreak : break pp
+
+val break : ppstream
+
+val breaks : int -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+val newline : ppstream
+
+val newlines : int -> ppstream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream
-
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
-val ppString : string pp
-
val ppBracket : string -> string -> 'a pp -> 'a pp
val ppOp : string -> ppstream
@@ -99,6 +117,8 @@
val ppChar : char pp
+val ppString : string pp
+
val ppEscapeString : {escape : char list} -> string pp
val ppUnit : unit pp
@@ -125,12 +145,6 @@
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
-val ppBreakStyle : breakStyle pp
-
-val ppStep : step pp
-
-val ppPpstream : ppstream pp
-
val ppException : exn pp
(* ------------------------------------------------------------------------- *)
@@ -160,15 +174,29 @@
('a * bool) pp -> ('a * bool) pp
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
+(* Pretty-printer rendering. *)
+(* ------------------------------------------------------------------------- *)
+
+val render :
+ {lineLength : int option} -> ppstream ->
+ {indent : int, line : string} Stream.stream
+
+val toStringWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string
+
+val toStreamWithLineLength :
+ {lineLength : int option} -> 'a pp -> 'a -> string Stream.stream
+
+val toLine : 'a pp -> 'a -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
(* ------------------------------------------------------------------------- *)
val lineLength : int ref
val toString : 'a pp -> 'a -> string
-val toLine : 'a pp -> 'a -> string
-
val toStream : 'a pp -> 'a -> string Stream.stream
val trace : 'a pp -> string -> 'a -> unit
--- a/src/Tools/Metis/src/Print.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Print.sml Wed Dec 07 16:03:05 2011 +0100
@@ -26,7 +26,7 @@
fun revConcat strm =
case strm of
Stream.Nil => Stream.Nil
- | Stream.Cons (h,t) => revAppend h (revConcat o t);
+ | Stream.Cons (h,t) => revAppend h (fn () => revConcat (t ()));
local
fun calcSpaces n = nChars #" " n;
@@ -62,56 +62,127 @@
end;
(* ------------------------------------------------------------------------- *)
-(* A type of strings annotated with their size. *)
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype style = Consistent | Inconsistent;
+
+datatype block =
+ Block of
+ {style : style,
+ indent : int};
+
+fun toStringStyle style =
+ case style of
+ Consistent => "Consistent"
+ | Inconsistent => "Inconsistent";
+
+fun isConsistentStyle style =
+ case style of
+ Consistent => true
+ | Inconsistent => false;
+
+fun isInconsistentStyle style =
+ case style of
+ Inconsistent => true
+ | Consistent => false;
+
+fun mkBlock style indent =
+ Block
+ {style = style,
+ indent = indent};
+
+val mkConsistentBlock = mkBlock Consistent;
+
+val mkInconsistentBlock = mkBlock Inconsistent;
+
+fun styleBlock (Block {style = x, ...}) = x;
+
+fun indentBlock (Block {indent = x, ...}) = x;
+
+fun isConsistentBlock block = isConsistentStyle (styleBlock block);
+
+fun isInconsistentBlock block = isInconsistentStyle (styleBlock block);
+
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
(* ------------------------------------------------------------------------- *)
-type stringSize = string * int;
+datatype word = Word of {word : string, size : int};
+
+fun mkWord s = Word {word = s, size = String.size s};
+
+val emptyWord = mkWord "";
+
+fun charWord c = mkWord (str c);
+
+fun spacesWord i = Word {word = nSpaces i, size = i};
+
+fun sizeWord (Word {size = x, ...}) = x;
+
+fun renderWord (Word {word = x, ...}) = x;
+
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype break = Break of {size : int, extraIndent : int};
+
+fun mkBreak n = Break {size = n, extraIndent = 0};
+
+fun sizeBreak (Break {size = x, ...}) = x;
+
+fun extraIndentBreak (Break {extraIndent = x, ...}) = x;
-fun mkStringSize s = (s, size s);
+fun renderBreak b = nSpaces (sizeBreak b);
+
+fun updateSizeBreak size break =
+ let
+ val Break {size = _, extraIndent} = break
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
-val emptyStringSize = mkStringSize "";
+fun appendBreak break1 break2 =
+ let
+(*BasicDebug
+ val () = warn "merging consecutive pretty-printing breaks"
+*)
+ val Break {size = size1, extraIndent = extraIndent1} = break1
+ and Break {size = size2, extraIndent = extraIndent2} = break2
+
+ val size = size1 + size2
+ and extraIndent = Int.max (extraIndent1,extraIndent2)
+ in
+ Break
+ {size = size,
+ extraIndent = extraIndent}
+ end;
(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
-datatype breakStyle = Consistent | Inconsistent;
-
datatype step =
- BeginBlock of breakStyle * int
+ BeginBlock of block
| EndBlock
- | AddString of stringSize
- | AddBreak of int
+ | AddWord of word
+ | AddBreak of break
| AddNewline;
type ppstream = step Stream.stream;
-fun breakStyleToString style =
- case style of
- Consistent => "Consistent"
- | Inconsistent => "Inconsistent";
+type 'a pp = 'a -> ppstream;
-fun stepToString step =
+fun toStringStep step =
case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
- | AddString _ => "AddString"
- | AddBreak _ => "AddBreak"
- | AddNewline => "AddNewline";
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer primitives. *)
-(* ------------------------------------------------------------------------- *)
-
-fun beginBlock style indent = Stream.singleton (BeginBlock (style,indent));
-
-val endBlock = Stream.singleton EndBlock;
-
-fun addString s = Stream.singleton (AddString s);
-
-fun addBreak spaces = Stream.singleton (AddBreak spaces);
-
-val addNewline = Stream.singleton AddNewline;
+ | AddWord _ => "Word"
+ | AddBreak _ => "Break"
+ | AddNewline => "Newline";
val skip : ppstream = Stream.Nil;
@@ -120,735 +191,90 @@
local
fun dup pp n () = if n = 1 then pp else Stream.append pp (dup pp (n - 1));
in
- fun duplicate n pp = if n = 0 then skip else dup pp n ();
+ fun duplicate n pp : ppstream =
+ let
+(*BasicDebug
+ val () = if 0 <= n then () else raise Bug "Print.duplicate"
+*)
+ in
+ if n = 0 then skip else dup pp n ()
+ end;
end;
val program : ppstream list -> ppstream = Stream.concatList;
val stream : ppstream Stream.stream -> ppstream = Stream.concat;
-fun block style indent pp = program [beginBlock style indent, pp, endBlock];
-
-fun blockProgram style indent pps = block style indent (program pps);
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
(* ------------------------------------------------------------------------- *)
-
-datatype blockBreakStyle =
- InconsistentBlock
- | ConsistentBlock
- | BreakingBlock;
-
-datatype block =
- Block of
- {indent : int,
- style : blockBreakStyle,
- size : int,
- chunks : chunk list}
-
-and chunk =
- StringChunk of {size : int, string : string}
- | BreakChunk of int
- | BlockChunk of block;
-
-datatype state =
- State of
- {blocks : block list,
- lineIndent : int,
- lineSize : int};
-
-val initialIndent = 0;
-
-val initialStyle = Inconsistent;
-
-fun liftStyle style =
- case style of
- Inconsistent => InconsistentBlock
- | Consistent => ConsistentBlock;
-
-fun breakStyle style =
- case style of
- ConsistentBlock => BreakingBlock
- | _ => style;
-
-fun sizeBlock (Block {size,...}) = size;
-
-fun sizeChunk chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => sizeBlock block;
-
-val splitChunks =
- let
- fun split _ [] = NONE
- | split acc (chunk :: chunks) =
- case chunk of
- BreakChunk _ => SOME (rev acc, chunks)
- | _ => split (chunk :: acc) chunks
- in
- split []
- end;
-
-val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
-
-local
- fun flatten acc chunks =
- case chunks of
- [] => rev acc
- | chunk :: chunks =>
- case chunk of
- StringChunk {string = s, ...} => flatten (s :: acc) chunks
- | BreakChunk n => flatten (nSpaces n :: acc) chunks
- | BlockChunk (Block {chunks = l, ...}) =>
- flatten acc (List.revAppend (l,chunks));
-in
- fun renderChunks indent chunks =
- {indent = indent,
- line = String.concat (flatten [] (rev chunks))};
-end;
-
-fun renderChunk indent chunk = renderChunks indent [chunk];
-
-fun isEmptyBlock block =
- let
- val Block {indent = _, style = _, size, chunks} = block
-
- val empty = List.null chunks
-
-(*BasicDebug
- val _ = not empty orelse size = 0 orelse
- raise Bug "Print.isEmptyBlock: bad size"
-*)
- in
- empty
- end;
-
-(*BasicDebug
-fun checkBlock ind block =
- let
- val Block {indent, style = _, size, chunks} = block
- val _ = indent >= ind orelse raise Bug "Print.checkBlock: bad indents"
- val size' = checkChunks indent chunks
- val _ = size = size' orelse raise Bug "Print.checkBlock: wrong size"
- in
- size
- end
-
-and checkChunks ind chunks =
- case chunks of
- [] => 0
- | chunk :: chunks => checkChunk ind chunk + checkChunks ind chunks
-
-and checkChunk ind chunk =
- case chunk of
- StringChunk {size,...} => size
- | BreakChunk spaces => spaces
- | BlockChunk block => checkBlock ind block;
-
-val checkBlocks =
- let
- fun check ind blocks =
- case blocks of
- [] => 0
- | block :: blocks =>
- let
- val Block {indent,...} = block
- in
- checkBlock ind block + check indent blocks
- end
- in
- check initialIndent o rev
- end;
-*)
-
-val initialBlock =
- let
- val indent = initialIndent
- val style = liftStyle initialStyle
- val size = 0
- val chunks = []
- in
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- end;
-
-val initialState =
- let
- val blocks = [initialBlock]
- val lineIndent = initialIndent
- val lineSize = 0
- in
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- end;
-
-(*BasicDebug
-fun checkState state =
- (let
- val State {blocks, lineIndent = _, lineSize} = state
- val lineSize' = checkBlocks blocks
- val _ = lineSize = lineSize' orelse
- raise Error "wrong lineSize"
- in
- ()
- end
- handle Error err => raise Bug err)
- handle Bug bug => raise Bug ("Print.checkState: " ^ bug);
-*)
-
-fun isFinalState state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- case blocks of
- [] => raise Bug "Print.isFinalState: no block"
- | [block] => isEmptyBlock block
- | _ :: _ :: _ => false
- end;
+(* Pretty-printing blocks. *)
+(* ------------------------------------------------------------------------- *)
local
- fun renderBreak lineIndent (chunks,lines) =
- let
- val line = renderChunks lineIndent chunks
-
- val lines = line :: lines
- in
- lines
- end;
-
- fun renderBreaks lineIndent lineIndent' breaks lines =
- case rev breaks of
- [] => raise Bug "Print.renderBreaks"
- | c :: cs =>
- let
- val lines = renderBreak lineIndent (c,lines)
- in
- List.foldl (renderBreak lineIndent') lines cs
- end;
-
- fun splitAllChunks cumulatingChunks =
- let
- fun split chunks =
- case splitChunks chunks of
- SOME (prefix,chunks) => prefix :: split chunks
- | NONE => [List.concat (chunks :: cumulatingChunks)]
- in
- split
- end;
-
- fun mkBreak style cumulatingChunks chunks =
- case splitChunks chunks of
- NONE => NONE
- | SOME (chunks,broken) =>
- let
- val breaks =
- case style of
- InconsistentBlock =>
- [List.concat (broken :: cumulatingChunks)]
- | _ => splitAllChunks cumulatingChunks broken
- in
- SOME (breaks,chunks)
- end;
-
- fun naturalBreak blocks =
- case blocks of
- [] => Right ([],[])
- | block :: blocks =>
- case naturalBreak blocks of
- Left (breaks,blocks,lineIndent,lineSize) =>
- let
- val Block {size,...} = block
-
- val blocks = block :: blocks
+ fun beginBlock b = Stream.singleton (BeginBlock b);
- val lineSize = lineSize + size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | Right (cumulatingChunks,blocks) =>
- let
- val Block {indent,style,size,chunks} = block
-
- val style = breakStyle style
- in
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val size = sizeChunks chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val lineIndent = indent
+ val endBlock = Stream.singleton EndBlock;
+in
+ fun block b pp = program [beginBlock b, pp, endBlock];
+end;
- val lineSize = size
- in
- Left (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- let
- val cumulatingChunks = chunks :: cumulatingChunks
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- Right (cumulatingChunks,blocks)
- end
- end;
-
- fun forceBreakBlock cumulatingChunks block =
- let
- val Block {indent, style, size = _, chunks} = block
-
- val style = breakStyle style
+fun consistentBlock i pps = block (mkConsistentBlock i) (program pps);
- val break =
- case mkBreak style cumulatingChunks chunks of
- SOME (breaks,chunks) =>
- let
- val lineSize = sizeChunks chunks
- val lineIndent = indent
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => forceBreakChunks cumulatingChunks chunks
- in
- case break of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val size = lineSize
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
- in
- SOME (breaks,block,lineIndent,lineSize)
- end
- | NONE => NONE
- end
-
- and forceBreakChunks cumulatingChunks chunks =
- case chunks of
- [] => NONE
- | chunk :: chunks =>
- case forceBreakChunk (chunks :: cumulatingChunks) chunk of
- SOME (breaks,chunk,lineIndent,lineSize) =>
- let
- val chunks = [chunk]
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreakChunks cumulatingChunks chunks of
- SOME (breaks,chunks,lineIndent,lineSize) =>
- let
- val chunks = chunk :: chunks
-
- val lineSize = lineSize + sizeChunk chunk
- in
- SOME (breaks,chunks,lineIndent,lineSize)
- end
- | NONE => NONE
-
- and forceBreakChunk cumulatingChunks chunk =
- case chunk of
- StringChunk _ => NONE
- | BreakChunk _ => raise Bug "Print.forceBreakChunk: BreakChunk"
- | BlockChunk block =>
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val chunk = BlockChunk block
- in
- SOME (breaks,chunk,lineIndent,lineSize)
- end
- | NONE => NONE;
+fun inconsistentBlock i pps = block (mkInconsistentBlock i) (program pps);
- fun forceBreak cumulatingChunks blocks' blocks =
- case blocks of
- [] => NONE
- | block :: blocks =>
- let
- val cumulatingChunks =
- case cumulatingChunks of
- [] => raise Bug "Print.forceBreak: null cumulatingChunks"
- | _ :: cumulatingChunks => cumulatingChunks
-
- val blocks' =
- case blocks' of
- [] => raise Bug "Print.forceBreak: null blocks'"
- | _ :: blocks' => blocks'
- in
- case forceBreakBlock cumulatingChunks block of
- SOME (breaks,block,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks'
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE =>
- case forceBreak cumulatingChunks blocks' blocks of
- SOME (breaks,blocks,lineIndent,lineSize) =>
- let
- val blocks = block :: blocks
-
- val Block {size,...} = block
-
- val lineSize = lineSize + size
- in
- SOME (breaks,blocks,lineIndent,lineSize)
- end
- | NONE => NONE
- end;
+(* ------------------------------------------------------------------------- *)
+(* Words are unbreakable strings annotated with their effective size. *)
+(* ------------------------------------------------------------------------- *)
- fun normalize lineLength lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
- in
- if lineIndent + lineSize <= lineLength then (lines,state)
- else
- let
- val break =
- case naturalBreak blocks of
- Left break => SOME break
- | Right (c,b) => forceBreak c b blocks
- in
- case break of
- SOME (breaks,blocks,lineIndent',lineSize) =>
- let
- val lines = renderBreaks lineIndent lineIndent' breaks lines
+fun ppWord w = Stream.singleton (AddWord w);
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent',
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end
- | NONE => (lines,state)
- end
- end;
-
-(*BasicDebug
- val normalize = fn lineLength => fn lines => fn state =>
- let
- val () = checkState state
- in
- normalize lineLength lines state
- end
- handle Bug bug =>
- raise Bug ("Print.normalize: before normalize:\n" ^ bug)
-*)
+val space = ppWord (mkWord " ");
- fun executeBeginBlock (style,ind) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val Block {indent,...} =
- case blocks of
- [] => raise Bug "Print.executeBeginBlock: no block"
- | block :: _ => block
-
- val indent = indent + ind
-
- val style = liftStyle style
-
- val size = 0
-
- val chunks = []
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeEndBlock lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
+fun spaces i = ppWord (spacesWord i);
- val (lineSize,blocks) =
- case blocks of
- [] => raise Bug "Print.executeEndBlock: no block"
- | topBlock :: blocks =>
- let
- val Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks} = topBlock
- in
- case topChunks of
- [] => (lineSize,blocks)
- | headTopChunks :: tailTopChunks =>
- let
- val (lineSize,topSize,topChunks) =
- case headTopChunks of
- BreakChunk spaces =>
- let
- val lineSize = lineSize - spaces
- and topSize = topSize - spaces
- and topChunks = tailTopChunks
- in
- (lineSize,topSize,topChunks)
- end
- | _ => (lineSize,topSize,topChunks)
-
- val topBlock =
- Block
- {indent = topIndent,
- style = topStyle,
- size = topSize,
- chunks = topChunks}
- in
- case blocks of
- [] => raise Error "Print.executeEndBlock: no block"
- | block :: blocks =>
- let
- val Block {indent,style,size,chunks} = block
+(* ------------------------------------------------------------------------- *)
+(* Possible line breaks. *)
+(* ------------------------------------------------------------------------- *)
- val size = size + topSize
-
- val chunks = BlockChunk topBlock :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- (lineSize,blocks)
- end
- end
- end
+fun ppBreak b = Stream.singleton (AddBreak b);
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- (lines,state)
- end;
-
- fun executeAddString lineLength (s,n) lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val blocks =
- case blocks of
- [] => raise Bug "Print.executeAddString: no block"
- | Block {indent,style,size,chunks} :: blocks =>
- let
- val size = size + n
-
- val chunk = StringChunk {size = n, string = s}
-
- val chunks = chunk :: chunks
+fun breaks i = ppBreak (mkBreak i);
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks
- in
- blocks
- end
-
- val lineSize = lineSize + n
-
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeAddBreak lineLength spaces lines state =
- let
- val State {blocks,lineIndent,lineSize} = state
-
- val (blocks,lineSize) =
- case blocks of
- [] => raise Bug "Print.executeAddBreak: no block"
- | Block {indent,style,size,chunks} :: blocks' =>
- case chunks of
- [] => (blocks,lineSize)
- | chunk :: chunks' =>
- let
- val spaces =
- case style of
- BreakingBlock => lineLength + 1
- | _ => spaces
-
- val size = size + spaces
-
- val chunks =
- case chunk of
- BreakChunk k => BreakChunk (k + spaces) :: chunks'
- | _ => BreakChunk spaces :: chunks
-
- val block =
- Block
- {indent = indent,
- style = style,
- size = size,
- chunks = chunks}
-
- val blocks = block :: blocks'
-
- val lineSize = lineSize + spaces
- in
- (blocks,lineSize)
- end
+val break = breaks 1;
- val state =
- State
- {blocks = blocks,
- lineIndent = lineIndent,
- lineSize = lineSize}
- in
- normalize lineLength lines state
- end;
-
- fun executeBigBreak lineLength lines state =
- executeAddBreak lineLength (lineLength + 1) lines state;
-
- fun executeAddNewline lineLength lines state =
- let
- val (lines,state) =
- executeAddString lineLength emptyStringSize lines state
-
- val (lines,state) =
- executeBigBreak lineLength lines state
- in
- executeAddString lineLength emptyStringSize lines state
- end;
-
- fun final lineLength lines state =
- let
- val lines =
- if isFinalState state then lines
- else
- let
- val (lines,state) = executeBigBreak lineLength lines state
+(* ------------------------------------------------------------------------- *)
+(* Forced line breaks. *)
+(* ------------------------------------------------------------------------- *)
-(*BasicDebug
- val _ = isFinalState state orelse raise Bug "Print.final"
-*)
- in
- lines
- end
- in
- if List.null lines then Stream.Nil else Stream.singleton lines
- end;
-in
- fun execute {lineLength} =
- let
- fun advance step state =
- let
- val lines = []
- in
- case step of
- BeginBlock style_ind => executeBeginBlock style_ind lines state
- | EndBlock => executeEndBlock lines state
- | AddString s => executeAddString lineLength s lines state
- | AddBreak spaces => executeAddBreak lineLength spaces lines state
- | AddNewline => executeAddNewline lineLength lines state
- end
+val newline = Stream.singleton AddNewline;
-(*BasicDebug
- val advance = fn step => fn state =>
- let
- val (lines,state) = advance step state
- val () = checkState state
- in
- (lines,state)
- end
- handle Bug bug =>
- raise Bug ("Print.advance: after " ^ stepToString step ^
- " command:\n" ^ bug)
-*)
- in
- revConcat o Stream.maps advance (final lineLength []) initialState
- end;
-end;
+fun newlines i = duplicate i newline;
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
-type 'a pp = 'a -> ppstream;
-
fun ppMap f ppB a : ppstream = ppB (f a);
fun ppBracket' l r ppA a =
let
- val (_,n) = l
+ val n = sizeWord l
in
- blockProgram Inconsistent n
- [addString l,
+ inconsistentBlock n
+ [ppWord l,
ppA a,
- addString r]
+ ppWord r]
end;
-fun ppOp' s = sequence (addString s) (addBreak 1);
+fun ppOp' w = sequence (ppWord w) break;
fun ppOp2' ab ppA ppB (a,b) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b];
fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA a,
ppOp' ab,
ppB b,
@@ -860,7 +286,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
+ | h :: t => inconsistentBlock 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -869,30 +295,30 @@
in
fn Stream.Nil => skip
| Stream.Cons (h,t) =>
- blockProgram Inconsistent 0
+ inconsistentBlock 0
[ppA h,
Stream.concat (Stream.map ppOpA (t ()))]
end;
-fun ppBracket l r = ppBracket' (mkStringSize l) (mkStringSize r);
+fun ppBracket l r = ppBracket' (mkWord l) (mkWord r);
-fun ppOp s = ppOp' (mkStringSize s);
+fun ppOp s = ppOp' (mkWord s);
-fun ppOp2 ab = ppOp2' (mkStringSize ab);
+fun ppOp2 ab = ppOp2' (mkWord ab);
-fun ppOp3 ab bc = ppOp3' (mkStringSize ab) (mkStringSize bc);
+fun ppOp3 ab bc = ppOp3' (mkWord ab) (mkWord bc);
-fun ppOpList s = ppOpList' (mkStringSize s);
+fun ppOpList s = ppOpList' (mkWord s);
-fun ppOpStream s = ppOpStream' (mkStringSize s);
+fun ppOpStream s = ppOpStream' (mkWord s);
(* ------------------------------------------------------------------------- *)
(* Pretty-printers for common types. *)
(* ------------------------------------------------------------------------- *)
-fun ppChar c = addString (str c, 1);
+fun ppChar c = ppWord (charWord c);
-fun ppString s = addString (mkStringSize s);
+fun ppString s = ppWord (mkWord s);
fun ppEscapeString escape = ppMap (escapeString escape) ppString;
@@ -949,9 +375,9 @@
end;
local
- val left = mkStringSize "["
- and right = mkStringSize "]"
- and sep = mkStringSize ",";
+ val left = mkWord "["
+ and right = mkWord "]"
+ and sep = mkWord ",";
in
fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;
@@ -968,9 +394,9 @@
end;
local
- val left = mkStringSize "("
- and right = mkStringSize ")"
- and sep = mkStringSize ",";
+ val left = mkWord "("
+ and right = mkWord ")"
+ and sep = mkWord ",";
in
fun ppPair ppA ppB =
ppBracket' left right (ppOp2' sep ppA ppB);
@@ -979,40 +405,63 @@
ppBracket' left right (ppOp3' sep sep ppA ppB ppC);
end;
-val ppBreakStyle = ppMap breakStyleToString ppString;
+fun ppException e = ppString (exnMessage e);
-val ppStep = ppMap stepToString ppString;
+(* ------------------------------------------------------------------------- *)
+(* A type of pretty-printers. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val ppStepType = ppMap toStringStep ppString;
+
+ val ppStyle = ppMap toStringStyle ppString;
-val ppStringSize =
- let
- val left = mkStringSize "\""
- and right = mkStringSize "\""
- and escape = {escape = [#"\""]}
+ val ppBlockInfo =
+ let
+ val sep = mkWord " "
+ in
+ fn Block {style = s, indent = i} =>
+ program [ppStyle s, ppWord sep, ppInt i]
+ end;
- val pp = ppBracket' left right (ppEscapeString escape)
- in
- fn (s,n) => if size s = n then pp s else ppPair pp ppInt (s,n)
- end;
+ val ppWordInfo =
+ let
+ val left = mkWord "\""
+ and right = mkWord "\""
+ and escape = {escape = [#"\""]}
-fun ppStep step =
- blockProgram Inconsistent 2
- (ppStep step ::
- (case step of
- BeginBlock style_indent =>
- [addBreak 1,
- ppPair ppBreakStyle ppInt style_indent]
- | EndBlock => []
- | AddString s =>
- [addBreak 1,
- ppStringSize s]
- | AddBreak n =>
- [addBreak 1,
- ppInt n]
- | AddNewline => []));
+ val pp = ppBracket' left right (ppEscapeString escape)
+ in
+ fn Word {word = s, size = n} =>
+ if size s = n then pp s else ppPair pp ppInt (s,n)
+ end;
+
+ val ppBreakInfo =
+ let
+ val sep = mkWord "+"
+ in
+ fn Break {size = n, extraIndent = k} =>
+ if k = 0 then ppInt n else program [ppInt n, ppWord sep, ppInt k]
+ end;
-val ppPpstream = ppStream ppStep;
-
-fun ppException e = ppString (exnMessage e);
+ fun ppStep step =
+ inconsistentBlock 2
+ (ppStepType step ::
+ (case step of
+ BeginBlock b =>
+ [break,
+ ppBlockInfo b]
+ | EndBlock => []
+ | AddWord w =>
+ [break,
+ ppWordInfo w]
+ | AddBreak b =>
+ [break,
+ ppBreakInfo b]
+ | AddNewline => []));
+in
+ val ppPpstream = ppStream ppStep;
+end;
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
@@ -1120,13 +569,13 @@
end
in
fn tm_t_a_b_r as (_,t,_,_,_) =>
- if isLayer t then block Inconsistent 0 (ppLayer tm_t_a_b_r)
+ if isLayer t then inconsistentBlock 0 [ppLayer tm_t_a_b_r]
else ppLower tm_t_a_b_r
end;
local
- val leftBrack = mkStringSize "("
- and rightBrack = mkStringSize ")";
+ val leftBrack = mkWord "("
+ and rightBrack = mkWord ")";
in
fun ppInfixes ops =
let
@@ -1160,37 +609,947 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers with a global line length. *)
+(* A type of output lines. *)
+(* ------------------------------------------------------------------------- *)
+
+type line = {indent : int, line : string};
+
+val emptyLine =
+ let
+ val indent = 0
+ and line = ""
+ in
+ {indent = indent,
+ line = line}
+ end;
+
+fun addEmptyLine lines = emptyLine :: lines;
+
+fun addLine lines indent line = {indent = indent, line = line} :: lines;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering. *)
(* ------------------------------------------------------------------------- *)
-val lineLength = ref initialLineLength;
+datatype chunk =
+ WordChunk of word
+ | BreakChunk of break
+ | FrameChunk of frame
+
+and frame =
+ Frame of
+ {block : block,
+ broken : bool,
+ indent : int,
+ size : int,
+ chunks : chunk list};
+
+datatype state =
+ State of
+ {lineIndent : int,
+ lineSize : int,
+ stack : frame list};
+
+fun blockFrame (Frame {block = x, ...}) = x;
+
+fun brokenFrame (Frame {broken = x, ...}) = x;
+
+fun indentFrame (Frame {indent = x, ...}) = x;
+
+fun sizeFrame (Frame {size = x, ...}) = x;
+
+fun chunksFrame (Frame {chunks = x, ...}) = x;
+
+fun styleFrame frame = styleBlock (blockFrame frame);
+
+fun isConsistentFrame frame = isConsistentBlock (blockFrame frame);
+
+fun breakingFrame frame = isConsistentFrame frame andalso brokenFrame frame;
+
+fun sizeChunk chunk =
+ case chunk of
+ WordChunk w => sizeWord w
+ | BreakChunk b => sizeBreak b
+ | FrameChunk f => sizeFrame f;
+
+local
+ fun add (c,acc) = sizeChunk c + acc;
+in
+ fun sizeChunks cs = List.foldl add 0 cs;
+end;
+
+local
+ fun flattenChunks acc chunks =
+ case chunks of
+ [] => acc
+ | chunk :: chunks => flattenChunk acc chunk chunks
+
+ and flattenChunk acc chunk chunks =
+ case chunk of
+ WordChunk w => flattenChunks (renderWord w :: acc) chunks
+ | BreakChunk b => flattenChunks (renderBreak b :: acc) chunks
+ | FrameChunk f => flattenFrame acc f chunks
+
+ and flattenFrame acc frame chunks =
+ flattenChunks acc (chunksFrame frame @ chunks);
+in
+ fun renderChunks chunks = String.concat (flattenChunks [] chunks);
+end;
+
+fun addChunksLine lines indent chunks =
+ addLine lines indent (renderChunks chunks);
+
+local
+ fun add baseIndent ((extraIndent,chunks),lines) =
+ addChunksLine lines (baseIndent + extraIndent) chunks;
+in
+ fun addIndentChunksLines lines baseIndent indent_chunks =
+ List.foldl (add baseIndent) lines indent_chunks;
+end;
+
+fun isEmptyFrame frame =
+ let
+ val chunks = chunksFrame frame
+
+ val empty = List.null chunks
+
+(*BasicDebug
+ val () =
+ if not empty orelse sizeFrame frame = 0 then ()
+ else raise Bug "Print.isEmptyFrame: bad size"
+*)
+ in
+ empty
+ end;
+
+local
+ fun breakInconsistent blockIndent =
+ let
+ fun break chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case chunk of
+ BreakChunk b =>
+ let
+ val pre = chunks
+ and indent = blockIndent + extraIndentBreak b
+ and post = []
+ in
+ SOME (pre,indent,post)
+ end
+ | _ =>
+ case break chunks of
+ SOME (pre,indent,post) =>
+ let
+ val post = chunk :: post
+ in
+ SOME (pre,indent,post)
+ end
+ | NONE => NONE
+ in
+ break
+ end;
+
+ fun breakConsistent blockIndent =
+ let
+ fun break indent_chunks chunks =
+ case breakInconsistent blockIndent chunks of
+ NONE => (chunks,indent_chunks)
+ | SOME (pre,indent,post) =>
+ break ((indent,post) :: indent_chunks) pre
+ in
+ break []
+ end;
+in
+ fun breakFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent = _,
+ size = _,
+ chunks} = frame
+
+ val blockIndent = indentBlock block
+ in
+ case breakInconsistent blockIndent chunks of
+ NONE => NONE
+ | SOME (pre,indent,post) =>
+ let
+ val broken = true
+ and size = sizeChunks post
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = post}
+ in
+ case styleBlock block of
+ Inconsistent =>
+ let
+ val indent_chunks = []
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ | Consistent =>
+ let
+ val (pre,indent_chunks) = breakConsistent blockIndent pre
+ in
+ SOME (pre,indent_chunks,frame)
+ end
+ end
+ end;
+end;
+
+fun removeChunksFrame frame =
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ if broken andalso List.null chunks then NONE
+ else
+ let
+ val frame =
+ Frame
+ {block = block,
+ broken = true,
+ indent = indent,
+ size = 0,
+ chunks = []}
+ in
+ SOME (chunks,frame)
+ end
+ end;
+
+val removeChunksFrames =
+ let
+ fun remove frames =
+ case frames of
+ [] =>
+ let
+ val chunks = []
+ and frames = NONE
+ and indent = 0
+ in
+ (chunks,frames,indent)
+ end
+ | top :: rest =>
+ let
+ val (chunks,rest',indent) = remove rest
+
+ val indent = indent + indentFrame top
+
+ val (chunks,top') =
+ case removeChunksFrame top of
+ NONE => (chunks,NONE)
+ | SOME (topChunks,top) => (topChunks @ chunks, SOME top)
+
+ val frames' =
+ case (top',rest') of
+ (NONE,NONE) => NONE
+ | (SOME top, NONE) => SOME (top :: rest)
+ | (NONE, SOME rest) => SOME (top :: rest)
+ | (SOME top, SOME rest) => SOME (top :: rest)
+ in
+ (chunks,frames',indent)
+ end
+ in
+ fn frames =>
+ let
+ val (chunks,frames',indent) = remove frames
+
+ val frames = Option.getOpt (frames',frames)
+ in
+ (chunks,frames,indent)
+ end
+ end;
+
+local
+ fun breakUp lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakUp lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE =>
+ case breakFrame frame of
+ NONE => NONE
+ | SOME (frameChunks,indent_chunks,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = frameChunks @ chunks
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + indentFrame frame
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end;
+
+ fun breakInsideChunk chunk =
+ case chunk of
+ WordChunk _ => NONE
+ | BreakChunk _ => raise Bug "Print.breakInsideChunk"
+ | FrameChunk frame =>
+ case breakFrame frame of
+ SOME (pathChunks,indent_chunks,frame) =>
+ let
+ val pathIndent = 0
+ and breakIndent = indentFrame frame
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => breakInsideFrame frame
+
+ and breakInsideChunks chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case breakInsideChunk chunk of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val pathChunks = pathChunks @ chunks
+ and chunks = [FrameChunk frame]
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE =>
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val chunks = chunk :: chunks
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks)
+ end
+ | NONE => NONE
+
+ and breakInsideFrame frame =
+ let
+ val Frame
+ {block,
+ broken = _,
+ indent,
+ size = _,
+ chunks} = frame
+ in
+ case breakInsideChunks chunks of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) =>
+ let
+ val pathIndent = pathIndent + indent
+ and broken = true
+ and size = sizeChunks chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ in
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame)
+ end
+ | NONE => NONE
+ end;
+
+ fun breakInside lines lineIndent frames =
+ case frames of
+ [] => NONE
+ | frame :: frames =>
+ case breakInsideFrame frame of
+ SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) =>
+ let
+ val (chunks,frames,indent) = removeChunksFrames frames
+
+ val chunks = pathChunks @ chunks
+ and indent = indent + pathIndent
+
+ val lines = addChunksLine lines lineIndent chunks
+
+ val lines = addIndentChunksLines lines indent indent_chunks
+
+ val lineIndent = indent + breakIndent
+
+ val lineSize = sizeFrame frame
+
+ val frames = frame :: frames
+ in
+ SOME ((lines,lineIndent),lineSize,frames)
+ end
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME (lines_indent,lineSize,frames) =>
+ let
+ val lineSize = lineSize + sizeFrame frame
+ and frames = frame :: frames
+ in
+ SOME (lines_indent,lineSize,frames)
+ end
+ | NONE => NONE;
+in
+ fun breakFrames lines lineIndent frames =
+ case breakUp lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE =>
+ case breakInside lines lineIndent frames of
+ SOME ((lines,lineIndent),lineSize,frames) =>
+ SOME (lines,lineIndent,lineSize,frames)
+ | NONE => NONE;
+end;
+
+(*BasicDebug
+fun checkChunk chunk =
+ case chunk of
+ WordChunk t => (false, sizeWord t)
+ | BreakChunk b => (false, sizeBreak b)
+ | FrameChunk b => checkFrame b
+
+and checkChunks chunks =
+ case chunks of
+ [] => (false,0)
+ | chunk :: chunks =>
+ let
+ val (bk,sz) = checkChunk chunk
+
+ val (bk',sz') = checkChunks chunks
+ in
+ (bk orelse bk', sz + sz')
+ end
+
+and checkFrame frame =
+ let
+ val Frame
+ {block = _,
+ broken,
+ indent = _,
+ size,
+ chunks} = frame
+
+ val (bk,sz) = checkChunks chunks
+
+ val () =
+ if size = sz then ()
+ else raise Bug "Print.checkFrame: wrong size"
+
+ val () =
+ if broken orelse not bk then ()
+ else raise Bug "Print.checkFrame: deep broken frame"
+ in
+ (broken,size)
+ end;
+
+fun checkFrames frames =
+ case frames of
+ [] => (true,0)
+ | frame :: frames =>
+ let
+ val (bk,sz) = checkFrame frame
+
+ val (bk',sz') = checkFrames frames
+
+ val () =
+ if bk' orelse not bk then ()
+ else raise Bug "Print.checkFrame: broken stack frame"
+ in
+ (bk, sz + sz')
+ end;
+*)
+
+(*BasicDebug
+fun checkState state =
+ (let
+ val State {lineIndent,lineSize,stack} = state
+
+ val () =
+ if not (List.null stack) then ()
+ else raise Error "no stack"
+
+ val (_,sz) = checkFrames stack
+
+ val () =
+ if lineSize = sz then ()
+ else raise Error "wrong lineSize"
+ in
+ ()
+ end
+ handle Error err => raise Bug err)
+ handle Bug bug => raise Bug ("Print.checkState: " ^ bug);
+*)
+
+fun isEmptyState state =
+ let
+ val State {lineSize,stack,...} = state
+ in
+ lineSize = 0 andalso List.all isEmptyFrame stack
+ end;
+
+fun isFinalState state =
+ let
+ val State {stack,...} = state
+ in
+ case stack of
+ [] => raise Bug "Print.isFinalState: empty stack"
+ | [frame] => isEmptyFrame frame
+ | _ :: _ :: _ => false
+ end;
+
+local
+ val initialBlock =
+ let
+ val indent = 0
+ and style = Inconsistent
+ in
+ Block
+ {indent = indent,
+ style = style}
+ end;
+
+ val initialFrame =
+ let
+ val block = initialBlock
+ and broken = false
+ and indent = 0
+ and size = 0
+ and chunks = []
+ in
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+ end;
+in
+ val initialState =
+ let
+ val lineIndent = 0
+ and lineSize = 0
+ and stack = [initialFrame]
+ in
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ end;
+end;
+
+fun normalizeState lineLength lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val within =
+ case lineLength of
+ NONE => true
+ | SOME len => lineIndent + lineSize <= len
+ in
+ if within then (lines,state)
+ else
+ case breakFrames lines lineIndent stack of
+ NONE => (lines,state)
+ | SOME (lines,lineIndent,lineSize,stack) =>
+ let
+(*BasicDebug
+ val () = checkState state
+*)
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Print.normalizeState:\n" ^ bug)
+*)
+
+local
+ fun executeBeginBlock block lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val broken = false
+ and indent = indentBlock block
+ and size = 0
+ and chunks = []
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeEndBlock lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (lineSize,stack) =
+ case stack of
+ [] => raise Bug "Print.executeEndBlock: empty stack"
+ | topFrame :: stack =>
+ let
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+
+ val (lineSize,topSize,topChunks,topFrame) =
+ case topChunks of
+ BreakChunk break :: chunks =>
+ let
+(*BasicDebug
+ val () =
+ let
+ val mesg =
+ "ignoring a break at the end of a " ^
+ "pretty-printing block"
+ in
+ warn mesg
+ end
+*)
+ val n = sizeBreak break
+
+ val lineSize = lineSize - n
+ and topSize = topSize - n
+ and topChunks = chunks
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+ in
+ (lineSize,topSize,topChunks,topFrame)
+ end
+ | _ => (lineSize,topSize,topChunks,topFrame)
+ in
+ if List.null topChunks then (lineSize,stack)
+ else
+ case stack of
+ [] => raise Error "Print.execute: too many end blocks"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + topSize
+
+ val chunk = FrameChunk topFrame
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ (lineSize,stack)
+ end
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ (lines,state)
+ end;
+
+ fun executeAddWord lineLength word lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val n = sizeWord word
+
+ val lineSize = lineSize + n
+
+ val stack =
+ case stack of
+ [] => raise Bug "Print.executeAddWord: empty stack"
+ | frame :: stack =>
+ let
+ val Frame
+ {block,
+ broken,
+ indent,
+ size,
+ chunks} = frame
+
+ val size = size + n
+
+ val chunk = WordChunk word
+
+ val chunks = chunk :: chunks
+
+ val frame =
+ Frame
+ {block = block,
+ broken = broken,
+ indent = indent,
+ size = size,
+ chunks = chunks}
+
+ val stack = frame :: stack
+ in
+ stack
+ end
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+ in
+ normalizeState lineLength lines state
+ end;
+
+ fun executeAddBreak lineLength break lines state =
+ let
+ val State {lineIndent,lineSize,stack} = state
+
+ val (topFrame,restFrames) =
+ case stack of
+ [] => raise Bug "Print.executeAddBreak: empty stack"
+ | topFrame :: restFrames => (topFrame,restFrames)
+
+ val Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks} = topFrame
+ in
+ case topChunks of
+ [] => (lines,state)
+ | topChunk :: restTopChunks =>
+ let
+ val (topChunks,n) =
+ case topChunk of
+ BreakChunk break' =>
+ let
+ val break = appendBreak break' break
+
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: restTopChunks
+ and n = sizeBreak break - sizeBreak break'
+ in
+ (topChunks,n)
+ end
+ | _ =>
+ let
+ val chunk = BreakChunk break
+
+ val topChunks = chunk :: topChunks
+ and n = sizeBreak break
+ in
+ (topChunks,n)
+ end
+
+ val lineSize = lineSize + n
+
+ val topSize = topSize + n
+
+ val topFrame =
+ Frame
+ {block = topBlock,
+ broken = topBroken,
+ indent = topIndent,
+ size = topSize,
+ chunks = topChunks}
+
+ val stack = topFrame :: restFrames
+
+ val state =
+ State
+ {lineIndent = lineIndent,
+ lineSize = lineSize,
+ stack = stack}
+
+ val lineLength =
+ if breakingFrame topFrame then SOME ~1 else lineLength
+ in
+ normalizeState lineLength lines state
+ end
+ end;
+
+ fun executeBigBreak lines state =
+ let
+ val lineLength = SOME ~1
+ and break = mkBreak 0
+ in
+ executeAddBreak lineLength break lines state
+ end;
+
+ fun executeAddNewline lineLength lines state =
+ if isEmptyState state then (addEmptyLine lines, state)
+ else executeBigBreak lines state;
+
+ fun executeEof lineLength lines state =
+ if isFinalState state then (lines,state)
+ else
+ let
+ val (lines,state) = executeBigBreak lines state
+
+(*BasicDebug
+ val () =
+ if isFinalState state then ()
+ else raise Bug "Print.executeEof: not a final state"
+*)
+ in
+ (lines,state)
+ end;
+in
+ fun render {lineLength} =
+ let
+ fun execute step state =
+ let
+ val lines = []
+ in
+ case step of
+ BeginBlock block => executeBeginBlock block lines state
+ | EndBlock => executeEndBlock lines state
+ | AddWord word => executeAddWord lineLength word lines state
+ | AddBreak break => executeAddBreak lineLength break lines state
+ | AddNewline => executeAddNewline lineLength lines state
+ end
+
+(*BasicDebug
+ val execute = fn step => fn state =>
+ let
+ val (lines,state) = execute step state
+
+ val () = checkState state
+ in
+ (lines,state)
+ end
+ handle Bug bug =>
+ raise Bug ("Print.execute: after " ^ toStringStep step ^
+ " command:\n" ^ bug)
+*)
+
+ fun final state =
+ let
+ val lines = []
+
+ val (lines,state) = executeEof lineLength lines state
+
+(*BasicDebug
+ val () = checkState state
+*)
+ in
+ if List.null lines then Stream.Nil else Stream.singleton lines
+ end
+(*BasicDebug
+ handle Bug bug => raise Bug ("Print.final: " ^ bug)
+*)
+ in
+ fn pps =>
+ let
+ val lines = Stream.maps execute final initialState pps
+ in
+ revConcat lines
+ end
+ end;
+end;
local
fun inc {indent,line} acc = line :: nSpaces indent :: acc;
fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
in
- fun toLines len ppA a =
- case execute {lineLength = len} (ppA a) of
+ fun toStringWithLineLength len ppA a =
+ case render len (ppA a) of
Stream.Nil => ""
| Stream.Cons (h,t) =>
let
val lines = Stream.foldl incn (inc h []) (t ())
in
- String.concat (rev lines)
+ String.concat (List.rev lines)
end;
end;
-fun toString ppA a = toLines (!lineLength) ppA a;
+local
+ fun renderLine {indent,line} = nSpaces indent ^ line ^ "\n";
+in
+ fun toStreamWithLineLength len ppA a =
+ Stream.map renderLine (render len (ppA a));
+end;
+
+fun toLine ppA a = toStringWithLineLength {lineLength = NONE} ppA a;
-fun toLine ppA a = toLines 100000 ppA a;
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer rendering with a global line length. *)
+(* ------------------------------------------------------------------------- *)
+
+val lineLength = ref initialLineLength;
+
+fun toString ppA a =
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStringWithLineLength len ppA a
+ end;
fun toStream ppA a =
- Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
- (execute {lineLength = !lineLength} (ppA a));
+ let
+ val len = {lineLength = SOME (!lineLength)}
+ in
+ toStreamWithLineLength len ppA a
+ end;
local
- val sep = mkStringSize " =";
+ val sep = mkWord " =";
in
fun trace ppX nameX x =
Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
--- a/src/Tools/Metis/src/Proof.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Proof.sml Wed Dec 07 16:03:05 2011 +0100
@@ -34,43 +34,43 @@
| inferenceType (Equality _) = Thm.Equality;
local
- fun ppAssume atm = Print.sequence (Print.addBreak 1) (Atom.pp atm);
+ fun ppAssume atm = Print.sequence Print.break (Atom.pp atm);
fun ppSubst ppThm (sub,thm) =
- Print.sequence (Print.addBreak 1)
- (Print.blockProgram Print.Inconsistent 1
+ Print.sequence Print.break
+ (Print.inconsistentBlock 1
[Print.ppString "{",
Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString ppThm ("thm",thm),
Print.ppString "}"]);
fun ppResolve ppThm (res,pos,neg) =
- Print.sequence (Print.addBreak 1)
- (Print.blockProgram Print.Inconsistent 1
+ Print.sequence Print.break
+ (Print.inconsistentBlock 1
[Print.ppString "{",
Print.ppOp2 " =" Print.ppString Atom.pp ("res",res),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString ppThm ("pos",pos),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString ppThm ("neg",neg),
Print.ppString "}"]);
- fun ppRefl tm = Print.sequence (Print.addBreak 1) (Term.pp tm);
+ fun ppRefl tm = Print.sequence Print.break (Term.pp tm);
fun ppEquality (lit,path,res) =
- Print.sequence (Print.addBreak 1)
- (Print.blockProgram Print.Inconsistent 1
+ Print.sequence Print.break
+ (Print.inconsistentBlock 1
[Print.ppString "{",
Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path),
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppOp2 " =" Print.ppString Term.pp ("res",res),
Print.ppString "}"]);
@@ -78,21 +78,20 @@
let
val infString = Thm.inferenceTypeToString (inferenceType inf)
in
- Print.block Print.Inconsistent 2
- (Print.sequence
- (Print.ppString infString)
- (case inf of
- Axiom cl => ppAxiom cl
- | Assume x => ppAssume x
- | Subst x => ppSubst ppThm x
- | Resolve x => ppResolve ppThm x
- | Refl x => ppRefl x
- | Equality x => ppEquality x))
+ Print.inconsistentBlock 2
+ [Print.ppString infString,
+ (case inf of
+ Axiom cl => ppAxiom cl
+ | Assume x => ppAssume x
+ | Subst x => ppSubst ppThm x
+ | Resolve x => ppResolve ppThm x
+ | Refl x => ppRefl x
+ | Equality x => ppEquality x)]
end;
fun ppAxiom cl =
Print.sequence
- (Print.addBreak 1)
+ Print.break
(Print.ppMap
LiteralSet.toList
(Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl);
@@ -122,17 +121,17 @@
val s = thmString n
in
Print.sequence
- (Print.blockProgram Print.Consistent (1 + size s)
+ (Print.consistentBlock (1 + size s)
[Print.ppString (s ^ " "),
Thm.pp th,
- Print.addBreak 2,
+ Print.breaks 2,
Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf])
- Print.addNewline
+ Print.newline
end
in
- Print.blockProgram Print.Consistent 0
+ Print.consistentBlock 0
[Print.ppString "START OF PROOF",
- Print.addNewline,
+ Print.newline,
Print.program (List.map ppStep prf),
Print.ppString "END OF PROOF"]
end
@@ -234,7 +233,7 @@
val path = i :: path
in
if Term.equal tm s andalso Term.equal tm' t then
- SOME (rev path)
+ SOME (List.rev path)
else
case (tm,tm') of
(Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a'
@@ -396,7 +395,7 @@
val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths)
*)
in
- rev acc
+ List.rev acc
end;
in
fun proof th =
--- a/src/Tools/Metis/src/Rewrite.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Rewrite.sml Wed Dec 07 16:03:05 2011 +0100
@@ -85,9 +85,9 @@
Print.ppOp2 (" " ^ toStringOrientOption ort) Term.pp Term.pp x_y;
fun ppField f ppA a =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString (f ^ " ="),
- Print.addBreak 1,
+ Print.break,
ppA a];
val ppKnown =
@@ -111,21 +111,21 @@
(Print.ppMap (IntSet.toList) (Print.ppList Print.ppInt));
in
fun pp (Rewrite {known,redexes,subterms,waiting,...}) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString "Rewrite",
- Print.addBreak 1,
- Print.blockProgram Print.Inconsistent 1
+ Print.break,
+ Print.inconsistentBlock 1
[Print.ppString "{",
ppKnown known,
(*MetisTrace5
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppRedexes redexes,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppSubterms subterms,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppWaiting waiting,
*)
Print.skip],
--- a/src/Tools/Metis/src/Stream.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Stream.sml Wed Dec 07 16:03:05 2011 +0100
@@ -188,7 +188,7 @@
| concatList (h :: t) = append h (fn () => concatList t);
local
- fun toLst res Nil = rev res
+ fun toLst res Nil = List.rev res
| toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
in
fun toList s = toLst [] s;
--- a/src/Tools/Metis/src/Term.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Term.sml Wed Dec 07 16:03:05 2011 +0100
@@ -160,7 +160,7 @@
let
fun f (n,arg) = (n :: path, arg)
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
in
case tm of
Var _ => subtms rest acc
@@ -189,7 +189,7 @@
let
fun search [] = NONE
| search ((path,tm) :: rest) =
- if pred tm then SOME (rev path)
+ if pred tm then SOME (List.rev path)
else
case tm of
Var _ => search rest
@@ -301,7 +301,7 @@
Var _ => subtms rest acc
| Fn _ =>
let
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = (0 :: path, t) :: rest
in
subtms rest acc
@@ -312,7 +312,7 @@
val (_,args) = func
- val acc = (rev path, tm) :: acc
+ val acc = (List.rev path, tm) :: acc
val rest = List.map f (enumerate args) @ rest
in
@@ -449,7 +449,7 @@
Print.program
[(if tok = "," then Print.skip else Print.ppString " "),
Print.ppString tok,
- Print.addBreak 1];
+ Print.break];
val iPrinter = Print.ppInfixes iOps destI iToken
@@ -515,14 +515,14 @@
fun functionArgument bv tm =
Print.sequence
- (Print.addBreak 1)
+ Print.break
(if isBrack tm then customBracket bv tm
else if isVar tm orelse isConst tm then basic bv tm
else bracket bv tm)
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
(functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
@@ -541,21 +541,21 @@
[Print.ppString q,
varName bv v,
Print.program
- (List.map (Print.sequence (Print.addBreak 1) o varName bv) vs),
+ (List.map (Print.sequence Print.break o varName bv) vs),
Print.ppString ".",
- Print.addBreak 1,
+ Print.break,
innerQuant bv tm]
end
and quantifier bv tm =
if not (isQuant tm) then customBracket bv tm
- else Print.block Print.Inconsistent 2 (innerQuant bv tm)
+ else Print.inconsistentBlock 2 [innerQuant bv tm]
and molecule bv (tm,r) =
let
val (n,tm) = stripNeg tm
in
- Print.blockProgram Print.Inconsistent n
+ Print.inconsistentBlock n
[Print.duplicate n (Print.ppString neg),
if isI tm orelse (r andalso isQuant tm) then bracket bv tm
else quantifier bv tm]
--- a/src/Tools/Metis/src/Thm.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Thm.sml Wed Dec 07 16:03:05 2011 +0100
@@ -110,7 +110,7 @@
(List.map Literal.toFormula (LiteralSet.toList (clause th)));
in
fun pp th =
- Print.blockProgram Print.Inconsistent 3
+ Print.inconsistentBlock 3
[Print.ppString "|- ",
Formula.pp (toFormula th)];
end;
--- a/src/Tools/Metis/src/Tptp.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Tptp.sml Wed Dec 07 16:03:05 2011 +0100
@@ -631,13 +631,13 @@
case length tms of
0 => ppConst mapping f
| a =>
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[ppFnName mapping (f,a),
Print.ppString "(",
Print.ppOpList "," term tms,
Print.ppString ")"]
in
- Print.block Print.Inconsistent 0 o term
+ fn tm => Print.inconsistentBlock 0 [term tm]
end;
fun ppRelName mapping ra = Print.ppString (relToTptp mapping ra);
@@ -648,14 +648,14 @@
case length tms of
0 => ppProp mapping r
| a =>
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[ppRelName mapping (r,a),
Print.ppString "(",
Print.ppOpList "," (ppTerm mapping) tms,
Print.ppString ")"];
local
- val neg = Print.sequence (Print.ppString "~") (Print.addBreak 1);
+ val neg = Print.sequence (Print.ppString "~") Print.break;
fun fof mapping fm =
case fm of
@@ -683,7 +683,7 @@
let
val (n,fm) = Formula.stripNeg fm
in
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.duplicate n neg,
unitary mapping fm]
end)
@@ -692,7 +692,7 @@
SOME a_b => Print.ppOp2 " =" (ppTerm mapping) (ppTerm mapping) a_b
| NONE => ppAtom mapping atm)
| _ =>
- Print.blockProgram Print.Inconsistent 1
+ Print.inconsistentBlock 1
[Print.ppString "(",
fof mapping fm,
Print.ppString ")"]
@@ -701,18 +701,18 @@
let
val mapping = addVarListMapping mapping vs
in
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString q,
Print.ppString " ",
- Print.blockProgram Print.Inconsistent (String.size q)
+ Print.inconsistentBlock (String.size q)
[Print.ppString "[",
Print.ppOpList "," (ppVar mapping) vs,
Print.ppString "] :"],
- Print.addBreak 1,
+ Print.break,
unitary mapping fm]
end;
in
- fun ppFof mapping fm = Print.block Print.Inconsistent 0 (fof mapping fm);
+ fun ppFof mapping fm = Print.inconsistentBlock 0 [fof mapping fm];
end;
(* ------------------------------------------------------------------------- *)
@@ -1036,7 +1036,7 @@
val ppProofPath = Term.ppPath;
fun ppProof mapping inf =
- Print.blockProgram Print.Inconsistent 1
+ Print.inconsistentBlock 1
[Print.ppString "[",
(case inf of
Proof.Axiom _ => Print.skip
@@ -1048,10 +1048,10 @@
Print.program
[ppProofLiteral mapping lit,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProofPath path,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProofTerm mapping tm]),
Print.ppString "]"];
@@ -1077,15 +1077,15 @@
val name = nameStrip inference
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
[Print.ppString gen,
Print.ppString "(",
Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppBracket "[" "]" (ppStrip mapping) inference,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppList ppParent parents,
Print.ppString ")"]
end
@@ -1095,15 +1095,15 @@
val name = nameNormalize inference
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
[Print.ppString gen,
Print.ppString "(",
Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppBracket "[" "]" (ppNormalize mapping) inference,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppList ppParent parents,
Print.ppString ")"]
end
@@ -1125,27 +1125,27 @@
List.map (fn parent => (parent,sub)) parents
end
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
([Print.ppString gen,
Print.ppString "("] @
(if isTaut then
[Print.ppString "tautology",
Print.ppString ",",
- Print.addBreak 1,
- Print.blockProgram Print.Inconsistent 1
+ Print.break,
+ Print.inconsistentBlock 1
[Print.ppString "[",
Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProof mapping inference,
Print.ppString "]"]]
else
[Print.ppString name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppProof mapping inference,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
Print.ppList (ppProofParent mapping) parents]) @
[Print.ppString ")"])
end
@@ -1248,23 +1248,23 @@
CnfFormulaBody _ => "cnf"
| FofFormulaBody _ => "fof"
in
- Print.blockProgram Print.Inconsistent (size gen + 1)
+ Print.inconsistentBlock (size gen + 1)
([Print.ppString gen,
Print.ppString "(",
ppFormulaName name,
Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppRole role,
Print.ppString ",",
- Print.addBreak 1,
- Print.blockProgram Print.Consistent 1
+ Print.break,
+ Print.consistentBlock 1
[Print.ppString "(",
ppFormulaBody mapping body,
Print.ppString ")"]] @
(if isNoFormulaSource source then []
else
[Print.ppString ",",
- Print.addBreak 1,
+ Print.break,
ppFormulaSource mapping source]) @
[Print.ppString ")."])
end;
@@ -1645,7 +1645,7 @@
(* ------------------------------------------------------------------------- *)
fun ppInclude i =
- Print.blockProgram Print.Inconsistent 2
+ Print.inconsistentBlock 2
[Print.ppString "include('",
Print.ppString i,
Print.ppString "')."];
@@ -1686,7 +1686,7 @@
IncludeDeclaration i => (i :: il, fl)
| FormulaDeclaration f => (il, f :: fl)
in
- fn l => List.foldl part ([],[]) (rev l)
+ fn l => List.foldl part ([],[]) (List.rev l)
end;
local
@@ -1888,15 +1888,15 @@
List.foldl partitionFormula ([],[],[],[]) fms
val goal =
- case (rev cnfGoals, rev fofGoals) of
+ case (List.rev cnfGoals, List.rev fofGoals) of
([],[]) => NoGoal
| (cnfGoals,[]) => CnfGoal cnfGoals
| ([],fofGoals) => FofGoal fofGoals
| (_ :: _, _ :: _) =>
raise Error "TPTP problem has both cnf and fof conjecture formulas"
in
- {cnfAxioms = rev cnfAxioms,
- fofAxioms = rev fofAxioms,
+ {cnfAxioms = List.rev cnfAxioms,
+ fofAxioms = List.rev fofAxioms,
goal = goal}
end;
@@ -1956,7 +1956,7 @@
let
val {problem,sources} = norm
val {axioms,conjecture} = problem
- val problem = {axioms = rev axioms, conjecture = rev conjecture}
+ val problem = {axioms = List.rev axioms, conjecture = List.rev conjecture}
in
{subgoal = subgoal,
problem = problem,
@@ -2051,11 +2051,11 @@
fun stripLineComments acc strm =
case strm of
- Stream.Nil => (rev acc, Stream.Nil)
+ Stream.Nil => (List.rev acc, Stream.Nil)
| Stream.Cons (line,rest) =>
case total destLineComment line of
SOME s => stripLineComments (s :: acc) (rest ())
- | NONE => (rev acc, Stream.filter (not o isLineComment) strm);
+ | NONE => (List.rev acc, Stream.filter (not o isLineComment) strm);
fun advanceBlockComment c state =
case state of
@@ -2270,7 +2270,7 @@
val (names,ths) =
List.foldl (collectProofDeps sources) (names,[]) proof
- val normalization = Normalize.proveThms (rev ths)
+ val normalization = Normalize.proveThms (List.rev ths)
val (fofs,defs) =
List.foldl collectNormalizeDeps (fofs,defs) normalization
@@ -2554,7 +2554,7 @@
val formulas =
List.foldl (addSubgoalProofFormulas avoid fmNames) formulas proofs
in
- rev formulas
+ List.rev formulas
end
(*MetisDebug
handle Error err => raise Bug ("Tptp.fromProof: shouldn't fail:\n" ^ err);
--- a/src/Tools/Metis/src/Useful.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/Useful.sml Wed Dec 07 16:03:05 2011 +0100
@@ -213,7 +213,7 @@
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
| z _ _ _ = raise Error "zipWith: lists different lengths";
in
- fn xs => fn ys => rev (z [] xs ys)
+ fn xs => fn ys => List.rev (z [] xs ys)
end;
fun zip xs ys = zipWith pair xs ys;
@@ -221,7 +221,7 @@
local
fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
in
- fun unzip ab = List.foldl inc ([],[]) (rev ab);
+ fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
end;
fun cartwith f =
@@ -232,15 +232,15 @@
aux xsCopy (f x y :: res) xt ys
in
fn xs => fn ys =>
- let val xs' = rev xs in aux xs' [] xs' (rev ys) end
+ let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
end;
fun cart xs ys = cartwith pair xs ys;
fun takeWhile p =
let
- fun f acc [] = rev acc
- | f acc (x :: xs) = if p x then f (x :: acc) xs else rev acc
+ fun f acc [] = List.rev acc
+ | f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
in
f []
end;
@@ -255,8 +255,8 @@
fun divideWhile p =
let
- fun f acc [] = (rev acc, [])
- | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (rev acc, l)
+ fun f acc [] = (List.rev acc, [])
+ | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
in
f []
end;
@@ -267,15 +267,15 @@
case l of
[] =>
let
- val acc = if List.null row then acc else rev row :: acc
+ val acc = if List.null row then acc else List.rev row :: acc
in
- rev acc
+ List.rev acc
end
| h :: t =>
let
val (eor,x) = f (h,x)
in
- if eor then group (rev row :: acc) [h] x t
+ if eor then group (List.rev row :: acc) [h] x t
else group acc (h :: row) x t
end
in
@@ -326,7 +326,7 @@
fun revDivide l = revDiv [] l;
end;
-fun divide l n = let val (a,b) = revDivide l n in (rev a, b) end;
+fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
fun updateNth (n,x) l =
let
@@ -355,28 +355,28 @@
local
fun inc (v,x) = if mem v x then x else v :: x;
in
- fun setify s = rev (List.foldl inc [] s);
+ fun setify s = List.rev (List.foldl inc [] s);
end;
fun union s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc t (rev s)
+ List.foldl inc t (List.rev s)
end;
fun intersect s t =
let
fun inc (v,x) = if mem v t then v :: x else x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun difference s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
- List.foldl inc [] (rev s)
+ List.foldl inc [] (List.rev s)
end;
fun subset s t = List.all (fn x => mem x t) s;
@@ -420,13 +420,13 @@
fun sort cmp =
let
- fun findRuns acc r rs [] = rev (rev (r :: rs) :: acc)
+ fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
| findRuns acc r rs (x :: xs) =
case cmp (r,x) of
- GREATER => findRuns (rev (r :: rs) :: acc) x [] xs
+ GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
| _ => findRuns acc x (r :: rs) xs
- fun mergeAdj acc [] = rev acc
+ fun mergeAdj acc [] = List.rev acc
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
@@ -567,7 +567,7 @@
[] => []
| h :: t => if Char.isSpace h then chop t else l;
in
- val trim = String.implode o chop o rev o chop o rev o String.explode;
+ val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
end;
val join = String.concatWith;
@@ -584,11 +584,11 @@
let
val pat = String.explode sep
- fun div1 prev recent [] = stringify [] (rev recent :: prev)
+ fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
- | SOME rest => div1 (rev recent :: prev) [] rest
+ | SOME rest => div1 (List.rev recent :: prev) [] rest
in
fn s => div1 [] [] (String.explode s)
end;
@@ -797,7 +797,7 @@
val () = OS.FileSys.closeDir dirStrm
in
- rev filenames
+ List.rev filenames
end;
fun readTextFile {filename} =
--- a/src/Tools/Metis/src/metis.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/metis.sml Wed Dec 07 16:03:05 2011 +0100
@@ -13,7 +13,7 @@
val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20110531)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20110926)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
@@ -373,7 +373,7 @@
let
val seen = StringSet.empty
- val includes = rev includes
+ val includes = List.rev includes
val formulas = readIncludes mapping seen formulas includes
in
@@ -454,7 +454,7 @@
val () =
if !TEST then ()
- else display_proof filename tptp (rev acc)
+ else display_proof filename tptp (List.rev acc)
in
true
end
--- a/src/Tools/Metis/src/selftest.sml Wed Dec 07 15:10:29 2011 +0100
+++ b/src/Tools/Metis/src/selftest.sml Wed Dec 07 16:03:05 2011 +0100
@@ -626,7 +626,7 @@
val fm = LiteralSet.disjoin cl
in
- Print.blockProgram Print.Consistent ind
+ Print.consistentBlock ind
[Print.ppString p,
Print.ppString (nChars #" " (ind - size p)),
Formula.pp fm]