# HG changeset patch # User blanchet # Date 1323270185 -3600 # Node ID df6e210fb44cce706e23a6a21fcb417aea982a77 # Parent c36637603821a010650e35cba4e569c4abcf06ae updated Metis to 20110926 version diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/README --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/metis.ML --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Active.sml --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/ElementSet.sig --- 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. *) (* ------------------------------------------------------------------------- *) diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/ElementSet.sml --- 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. *) (* ------------------------------------------------------------------------- *) diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Formula.sml --- 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)); diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/KeyMap.sig --- 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. *) (* ------------------------------------------------------------------------- *) diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Model.sml --- 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; diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/NameArity.sml --- 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]; diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Normalize.sml --- 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; diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Options.sml --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Parse.sml --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/PortableMosml.sml --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Print.sig --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Print.sml --- 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"); diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Proof.sml --- 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 = diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Rewrite.sml --- 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], diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Stream.sml --- 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; diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Term.sml --- 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] diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Thm.sml --- 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; diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Tptp.sml --- 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); diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/Useful.sml --- 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} = diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/metis.sml --- 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 diff -r c36637603821 -r df6e210fb44c src/Tools/Metis/src/selftest.sml --- 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]