src/Tools/Metis/src/Print.sml

echo prover input via raw_messages, for improved protocol tracing;

(* ========================================================================= *)
(* PRETTY-PRINTING                                                           *)
(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

structure Print :> Print =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Constants.                                                                *)
(* ------------------------------------------------------------------------- *)

val initialLineLength = 75;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

fun revAppend xs s =
    case xs of
      [] => s ()
    | x :: xs => revAppend xs (K (Stream.Cons (x,s)));

fun revConcat strm =
    case strm of
      Stream.Nil => Stream.Nil
    | Stream.Cons (h,t) => revAppend h (revConcat o t);

local
  fun calcSpaces n = nChars #" " n;

  val cacheSize = 2 * initialLineLength;

  val cachedSpaces = Vector.tabulate (cacheSize,calcSpaces);
in
  fun nSpaces n =
      if n < cacheSize then Vector.sub (cachedSpaces,n)
      else calcSpaces n;
end;

(* ------------------------------------------------------------------------- *)
(* Escaping strings.                                                         *)
(* ------------------------------------------------------------------------- *)

fun escapeString {escape} =
    let
      val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape

      fun escapeChar c =
          case c of
            #"\\" => "\\\\"
          | #"\n" => "\\n"
          | #"\t" => "\\t"
          | _ =>
            case List.find (equal c o fst) escapeMap of
              SOME (_,s) => s
            | NONE => str c
    in
      String.translate escapeChar
    end;

(* ------------------------------------------------------------------------- *)
(* A type of strings annotated with their size.                              *)
(* ------------------------------------------------------------------------- *)

type stringSize = string * int;

fun mkStringSize s = (s, size s);

val emptyStringSize = mkStringSize "";

(* ------------------------------------------------------------------------- *)
(* 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;

fun breakStyleToString style =
    case style of
      Consistent => "Consistent"
    | Inconsistent => "Inconsistent";

fun stepToString 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;

val skip : ppstream = Stream.Nil;

fun sequence pp1 pp2 : ppstream = Stream.append pp1 (K pp2);

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 ();
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;

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

            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 "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 "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;

  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 ("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 "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 "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

                        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 "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 "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 "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

(*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;

(* ------------------------------------------------------------------------- *)
(* 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,
         ppA a,
         addString r]
    end;

fun ppOp' s = sequence (addString s) (addBreak 1);

fun ppOp2' ab ppA ppB (a,b) =
    blockProgram Inconsistent 0
      [ppA a,
       ppOp' ab,
       ppB b];

fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
    blockProgram Inconsistent 0
      [ppA a,
       ppOp' ab,
       ppB b,
       ppOp' bc,
       ppC c];

fun ppOpList' s ppA =
    let
      fun ppOpA a = sequence (ppOp' s) (ppA a)
    in
      fn [] => skip
       | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
    end;

fun ppOpStream' s ppA =
    let
      fun ppOpA a = sequence (ppOp' s) (ppA a)
    in
      fn Stream.Nil => skip
       | Stream.Cons (h,t) =>
         blockProgram Inconsistent 0
           [ppA h,
            Stream.concat (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);

(* ------------------------------------------------------------------------- *)
(* Pretty-printers for common types.                                         *)
(* ------------------------------------------------------------------------- *)

fun ppChar c = addString (str c, 1);

fun ppString s = addString (mkStringSize s);

fun ppEscapeString escape = ppMap (escapeString escape) ppString;

local
  val pp = ppString "()";
in
  fun ppUnit () = pp;
end;

local
  val ppTrue = ppString "true"
  and ppFalse = ppString "false";
in
  fun ppBool b = if b then ppTrue else ppFalse;
end;

val ppInt = ppMap Int.toString ppString;

local
  val ppNeg = ppString "~"
  and ppSep = ppString ","
  and ppZero = ppString "0"
  and ppZeroZero = ppString "00";

  fun ppIntBlock i =
      if i < 10 then sequence ppZeroZero (ppInt i)
      else if i < 100 then sequence ppZero (ppInt i)
      else ppInt i;

  fun ppIntBlocks i =
      if i < 1000 then ppInt i
      else sequence (ppIntBlocks (i div 1000))
             (sequence ppSep (ppIntBlock (i mod 1000)));
in
  fun ppPrettyInt i =
      if i < 0 then sequence ppNeg (ppIntBlocks (~i))
      else ppIntBlocks i;
end;

val ppReal = ppMap Real.toString ppString;

val ppPercent = ppMap percentToString ppString;

local
  val ppLess = ppString "Less"
  and ppEqual = ppString "Equal"
  and ppGreater = ppString "Greater";
in
  fun ppOrder ord =
      case ord of
        LESS => ppLess
      | EQUAL => ppEqual
      | GREATER => ppGreater;
end;

local
  val left = mkStringSize "["
  and right = mkStringSize "]"
  and sep = mkStringSize ",";
in
  fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;

  fun ppStream ppX xs = ppBracket' left right (ppOpStream' sep ppX) xs;
end;

local
  val ppNone = ppString "-";
in
  fun ppOption ppX xo =
      case xo of
        SOME x => ppX x
      | NONE => ppNone;
end;

local
  val left = mkStringSize "("
  and right = mkStringSize ")"
  and sep = mkStringSize ",";
in
  fun ppPair ppA ppB =
      ppBracket' left right (ppOp2' sep ppA ppB);

  fun ppTriple ppA ppB ppC =
      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);

(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators.                                          *)
(* ------------------------------------------------------------------------- *)

type token = string;

datatype assoc =
    LeftAssoc
  | NonAssoc
  | RightAssoc;

datatype infixes =
    Infixes of
      {token : token,
       precedence : int,
       assoc : assoc} list;

local
  fun comparePrecedence (io1,io2) =
      let
        val {token = _, precedence = p1, assoc = _} = io1
        and {token = _, precedence = p2, assoc = _} = io2
      in
        Int.compare (p2,p1)
      end;

  fun equalAssoc a a' =
      case a of
        LeftAssoc => (case a' of LeftAssoc => true | _ => false)
      | NonAssoc => (case a' of NonAssoc => true | _ => false)
      | RightAssoc => (case a' of RightAssoc => true | _ => false);

  fun new t a acc = {tokens = StringSet.singleton t, assoc = a} :: acc;

  fun add t a' acc =
      case acc of
        [] => raise Bug "Print.layerInfixes: null"
      | {tokens = ts, assoc = a} :: acc =>
        if equalAssoc a a' then {tokens = StringSet.add ts t, assoc = a} :: acc
        else raise Bug "Print.layerInfixes: mixed assocs";

  fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) =
      let
        val acc = if p = p' then add t a acc else new t a acc
      in
        (acc,p)
      end;
in
  fun layerInfixes (Infixes ios) =
      case sort comparePrecedence ios of
        [] => []
      | {token = t, precedence = p, assoc = a} :: ios =>
        let
          val acc = new t a []

          val (acc,_) = List.foldl layer (acc,p) ios
        in
          acc
        end;
end;

local
  fun add ({tokens = ts, assoc = _}, tokens) = StringSet.union ts tokens;
in
  fun tokensLayeredInfixes l = List.foldl add StringSet.empty l;
end;

fun tokensInfixes ios = tokensLayeredInfixes (layerInfixes ios);

fun destInfixOp dest tokens tm =
    case dest tm of
      NONE => NONE
    | s as SOME (t,a,b) => if StringSet.member t tokens then s else NONE;

fun ppLayeredInfixes dest ppTok {tokens,assoc} ppLower ppSub =
    let
      fun isLayer t = StringSet.member t tokens

      fun ppTerm aligned (tm,r) =
          case dest tm of
            NONE => ppSub (tm,r)
          | SOME (t,a,b) =>
            if aligned andalso isLayer t then ppLayer (tm,t,a,b,r)
            else ppLower (tm,t,a,b,r)

      and ppLeft tm_r =
          let
            val aligned = case assoc of LeftAssoc => true | _ => false
          in
            ppTerm aligned tm_r
          end

      and ppLayer (tm,t,a,b,r) =
          program
            [ppLeft (a,true),
             ppTok (tm,t),
             ppRight (b,r)]

      and ppRight tm_r =
          let
            val aligned = case assoc of RightAssoc => true | _ => false
          in
            ppTerm aligned tm_r
          end
    in
      fn tm_t_a_b_r as (_,t,_,_,_) =>
         if isLayer t then block Inconsistent 0 (ppLayer tm_t_a_b_r)
         else ppLower tm_t_a_b_r
    end;

local
  val leftBrack = mkStringSize "("
  and rightBrack = mkStringSize ")";
in
  fun ppInfixes ops =
      let
        val layers = layerInfixes ops

        val toks = tokensLayeredInfixes layers
      in
        fn dest => fn ppTok => fn ppSub =>
           let
             fun destOp tm = destInfixOp dest toks tm

             fun ppInfix tm_t_a_b_r = ppLayers layers tm_t_a_b_r

             and ppLayers ls (tm,t,a,b,r) =
                 case ls of
                   [] =>
                   ppBracket' leftBrack rightBrack ppInfix (tm,t,a,b,false)
                 | l :: ls =>
                   let
                     val ppLower = ppLayers ls
                   in
                     ppLayeredInfixes destOp ppTok l ppLower ppSub (tm,t,a,b,r)
                   end
           in
             fn (tm,r) =>
                case destOp tm of
                  SOME (t,a,b) => ppInfix (tm,t,a,b,r)
                | NONE => ppSub (tm,r)
           end
      end;
end;

(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers with a global line length.                      *)
(* ------------------------------------------------------------------------- *)

val lineLength = ref initialLineLength;

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
        Stream.Nil => ""
      | Stream.Cons (h,t) =>
        let
          val lines = Stream.foldl incn (inc h []) (t ())
        in
          String.concat (rev lines)
        end;
end;

fun toString ppA a = toLines (!lineLength) ppA a;

fun toLine ppA a = toLines 100000 ppA a;

fun toStream ppA a =
    Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
      (execute {lineLength = !lineLength} (ppA a));

local
  val sep = mkStringSize " =";
in
  fun trace ppX nameX x =
      Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
end;

end