packages feed

beautifHOL-0.10: PrintHOL.hs

{-
# Prettyprinter for beautifHOL, a HOL prettyprinter
# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html
# Lee Pike <lee-pike-@-gma-il-.com> (remove dashes)
# Copyright 2008

#  This file is part of beautifHOL.
# BSD3.
-}

-- | Module handles the actual pretty-printing.
module PrintHOL where

-- Library imports --
-- We use the reader monad to pass the pretty-print environment around.
import Control.Monad.Reader
import Data.List

-- Program imports.
import AbsHOL
import Char
import ConfigHOL -- Constants are defined here

-- |Possible flags to the program.
type Flags = [String]

-- |List of possible arguments.  Do not modify the ordering of this list (add new
-- flags to the end).
arglst :: Flags
arglst = ["--silent", "--notree", "--showinput", "--nolabels", "--help", "--f"]

-- |Defne flags here so they can be easily renamed.
silentArg, notreeArg, showinputArg :: String
silentArg = arglst !! 0
notreeArg = arglst !! 1
showinputArg = arglst !! 2
nolabelsArg = arglst !! 3
helpArg = arglst !! 4
fileArg = arglst !! 5

-- |The major datatype passed around holding the pretty-printing state.
data Env = 
    EnvDT { label :: Int   -- ^ Line label
          , newLn :: Bool   -- ^ If true, then we're on a new line.  Note: binary
                            --   operators are always on a new line; this tells us
                            --   whether some other sentence or term is on its own
                            --   line.
          , unOp :: Int   -- ^ How many negations we've seen
          , absInd :: Int   -- ^ Indentation after label stuff.  Where the line begins.
          , relInd :: Int   -- ^ Relative indentation (from last operator)
          , defaultInd :: Int   -- ^ Default indendtation (up to the longest label of a
                                -- formula)
          , prevSameBinOp :: Bool   -- ^ Was this binary operator the argument to the
                                    -- same binary operator?  (If so, we don't indent.)
          , splitArgs :: Bool   -- ^ True: put args to functions & predicates on their
                                -- own line.  The number is the length of the
                                -- identifier, plus other args and identifiers, up to
                                -- this term.
          , innerTerm :: Bool   -- ^ Is this term inside another term?  (The only case
                                -- in which it is not is if it is an argument to = .)
          , showLabels :: Bool  -- ^ Show labels?  This is only for whether labels
                                -- should currently be suppressed (e.g., in let
                                -- defs).  For no labels at all, we set a global
                                -- flag.
          , noLabels :: Bool -- ^ Are we showing labels at all (or are they globally suppressed)?

          }


-- |The initial environment.
mkinitEnv :: Flags -> Env
mkinitEnv fs = EnvDT 1 True 0 0 0 0 False False False True getLabelFlag
    where getLabelFlag = not $ elem nolabelsArg fs

-- |"Resets" the environment except for the default indentation (from the length of
-- the longest label).
resetEnv :: Env -> Env
resetEnv env = EnvDT 1 True 0 0 0 (defaultInd env) False False False (showLabels env) (noLabels env)

printTree :: Print a => a -> Flags -> String
printTree t fs = render $ runReader (prt t) (mkinitEnv fs)

type Doc = [ShowS] -> [ShowS]

doc :: ShowS -> Doc
doc = (:)

-- |Takes the final Doc and returns the output.  Ideally, the Doc should be considered
-- the logical structure of the pretty-printed formula and the render assigns
-- concrete syntax.
render :: Doc -> String
render d = rend 0 (map ($ "") $ d []) "" 
    where rend i ss = 
              case ss of
                -- For curried args.
                "( " : ts -> showChar '(' . spaces 1 . rend i ts
                t : "("  :ts -> showString t . showChar '(' . rend i ts
                ";"      :ts -> 
                    showString preStr . new . showString postStr . rend i ts
              -- Another hack for curried preds where the pred is one char long.
              -- If there's a space, a 2nd gets added by rend; if there's no
              -- space, nothing gets added. So I can only have 0 or 2 spaces.
                "\n" : "( "     :ts -> new . spaces 1 . showChar '(' . spaces 1 . rend i ts
              -- I need this: I don't want a space after \n because it'll carry
              -- to the next line.
                "\n"     :ts -> new . rend i ts
                t  : "." :ts -> showString t . space quantVarsMark . rend i ts
          -- Hack: The comma wasn't picked up in the case of odd number of
          -- parens in a row. e.g., Foo(h(g(f(a))), 4 );
                t  : ")" :"," :ts -> 
                  showString t . spaces 1 . showChar ')' . space argSepStr . rend i ts
                t  : ")" :ts -> 
                    showString t . spaces 1 . showChar ')' . spaces 1 . rend i ts
                t  : "," :ts -> showString t . space argSepStr . rend i ts
                ""       :ts -> rend i ts 
                t        :ts -> showString t . spaces 1 . rend i ts 
                _            -> id
          new   = showChar brkChar 
          space t = showString t . (\s -> if null s then "" else  (' ':s))

concatS :: [ShowS] -> ShowS
concatS = foldr (.) id

concatD :: [Doc] -> Doc
concatD = foldr (.) id

replicateS :: Int -> ShowS -> ShowS
replicateS n f = concatS (replicate n f)

spaces :: Int -> ShowS
spaces n = replicateS n (showString spaceStr)

type EnvT = Reader Env Doc

prtList :: Print a => [a] -> [Env] -> [Doc]
prtList [] _ = []
prtList ls envs = 
  let zp = zip envs ls 
  in map (\(env,a) -> runReader (prt a) env) zp


-- |The Print class.  Each constructor of the grammar instantiates this.  The prt
-- function tells how to pretty-print each construct.
class Print a 
    where prt :: a -> EnvT

instance Print Char 
    where prt s = return $ doc (showChar '\'' . mkEsc '\'' s . showChar '\'')

-- |Escape characters for rendering.
mkEsc :: Char -> Char -> ShowS
mkEsc q s = case s of
  _ | s == q -> showChar '\\' . showChar s
  '\\'-> showString "\\\\"
  '\n' -> showString "\\n"
  '\t' -> showString "\\t"
  _ -> showChar s

instance Print Integer where
  prt x = return $ doc (shows x)

instance Print Double where
  prt x = return $ doc (shows x)

instance Print Int where
  prt x = return $ doc (shows x)

instance Print Idents where
  prt (Idents i) = return $ doc (showString i)

instance Print PredId where
  prt (PredId i) = return $ doc (showString i)

instance Print FunctId where
  prt (FunctId i) = return $ doc (showString i)

maxLabels :: [SENT] -> Env -> [Env]
maxLabels sents env = 
  if (noLabels env) --getLabelFlag env --(showLabels env) 
  then map (\x -> env {defaultInd = x + 1}) $ map countBins sents 
  else map (\_ -> env ) sents
    where
      -- Sets up how far to indent the formula, to give space for labels.
      countBins s = 
          case s of
            AndSent s0 s1 -> binCnt s0 s1
            OrSent s0 s1 -> binCnt s0 s1
            ImpSent s0 s1 -> binCnt s0 s1
            ASentEq _ _ -> 1
            ForallSent _ s0 -> unCnt s0
            ExistsSent _ s0 -> unCnt s0
            IfSent s0 s1 s2 -> triCnt s0 s1 s2
            LetSent _ s0 -> countBins s0
            NegSent s0 -> if negCnt s0 then unCnt s0 else countBins s0
            _ -> 0
          where triCnt s0 s1 s2 = 1 + (max (countBins s0) $ max (countBins s1) (countBins s2))
                binCnt s0 s1 = 1 + max (countBins s0) (countBins s1)
                unCnt s0 = 1 + countBins s0
                -- See if there's ever another label to be applied.  If so, we
                -- count the not label; o/w, we don't.  (E.g., not forall
                -- x. P()) shouldn't count forall label.)
                negCnt s = case s of
                             AndSent _ _ -> True
                             OrSent _ _ -> True
                             ImpSent _ _ -> True
                             ASentEq _ _ -> True
                             IfSent _ _ _ -> True
                             LetSent _ _ -> True
                             ForallSent _ s0 -> negCnt' s0
                             ExistsSent _ s0 -> negCnt' s0
                             NegSent s0 -> negCnt' s0
                             _ -> False
                negCnt' s = case s of
                              AndSent _ _ -> True
                              OrSent _ _ -> True
                              ImpSent _ _ -> True
                              ASentEq _ _ -> True
                              IfSent _ _ _ -> True
                              LetSent _ _ -> True
                              ForallSent _ _ -> True
                              ExistsSent _ _ -> True
                              NegSent s0 -> negCnt s0
                              _ -> False


-- |Takes the list of sentences in the program and returns a corresponding list of
-- initial environments in which the defaultInd (i.e., the length of the longest
-- label for that sentence) is set.
instance Print PROGRAM where
  prt e = 
      case e of
        PROGRAM sents -> 
             do 
               env <- ask
               return $ 
                 concatD $ 
                   intersperse 
                   (doc $ showString ";") $
                     (doc $ showString preStr):(prtList sents (maxLabels sents env))

instance Print TERM where
  prt e = do
    env <- ask
    let initInd = if innerTerm env then doc $ spaces 0 else simpInd env
        in return $ case e of
               FunctTerm functid ((Terms terms):termsLst) -> 
                   concatD $ initInd:
                               (runReader (prt functid) env):
                               (intersperseTerms env' terms) ++ 
                               (prtList termsLst (repeat env''))
                           where env' = env { splitArgs = newSplit terms 
                                            , absInd = absIndUp 
                                                       env 
                                                       (functIdLen functid) 
                                            , innerTerm = True
                                            }
                                 i = if (innerTerm env) then 1
                                     else 2
                                 env'' = env {absInd = 
                                              (absInd env) + 
                                              (functIdLen functid) - i}
               ConstVarTerm idents -> concatD [ initInd
                                              , runReader (prt idents) env]
               _ -> concatD [] -- Should be unreachable.


instance Print TERMS where
  prt e = do
    env <- ask
    return $ case e of
               Terms terms -> 
                     concatD $ (nextLnArgs env):
                                 (doc $ showString "( "):
                                 (intersperseTerms env' terms)
                         where a = absInd env
                               env' = env { splitArgs = newSplit terms 
                                          , innerTerm = True
                                          , absInd = a + 2
                                          }

-- |For a list of terms, we intersperse the argument separator string.
intersperseTerms :: Env -> [TERM] -> [Doc]
intersperseTerms env terms = 
    intersperse 
    (argSeparators env) 
    (prtList terms $ repeat env)++
    [doc $ showString ")"]

instance Print DEF where
    prt def = do
      env <- ask
      return $ 
             case def of 
               DefSent ids sent ->
                   concatD $ [ runReader (prt ids) env
                             , doc $ showString eqStr
                             , runReader (prt sent) $ letEnv env varEqsLn 0 False
                             ]
                       where varEqsLn = 
                                 (length $ render $ runReader (prt ids) env) + (length eqStr)

instance Print SENT where
  prt e = do 
    env <- ask
    return $ 
      case e of
        IdentSent idents -> let initInd = if innerTerm env then doc $ spaces 0 else simpInd env
                            in concatD [ initInd
                                       , runReader (prt idents) env]
        ASentPred predid ((Terms terms):termsLst) -> 
            concatD $ (simpInd env):
                      (runReader (prt predid) env):
                        (intersperseTerms env' terms) ++
                      (prtList termsLst (repeat env''))
                where predLen = predIdLen predid
                      newAbs = absIndUp env predLen 
                      env' = env { splitArgs = newSplit terms
                                 , absInd = newAbs
                                 , innerTerm = True}
                      env'' = env {absInd = (absInd env) + predLen - 2}

        TrueSent  -> concatD [ simpInd env 
                             , doc (showString trueStr)
                             ]
        FalseSent  -> concatD [ simpInd env  
                              , doc (showString falseStr)
                              ]
        ASentEq term0 term -> 
            concatD [runReader (prt term0) env1
                    , binaryOpInd env eqStr
                    , runReader (prt term) env2
                    ]
                where env1 = binEnv1 env eqTab False 0 -- arbitrary label (suppressed for eq)
                      env2 = binEnv2 env eqTab False 1 -- arbitrary label (suppressed for eq)

        ForallSent vars sent -> 
            quantDoc env vars sent forallStr forallTab forallSent

        ExistsSent vars sent -> 
            quantDoc env vars sent existsStr existsTab existsSent

        NegSent sent -> 
            concatD [ quantOpInd env negStr 
                    , runReader (prt sent) e
                    ]
                where e = notEnv env negTab True

        AndSent sent0 sent -> 
            binOpDoc env sent0 sent andStr andTab andSent 
        OrSent sent0 sent -> 
            binOpDoc env sent0 sent orStr orTab orSent 
        ImpSent sent0 sent -> 
            binOpDoc env sent0 sent impStr impTab impSent 
        IfSent sent0 sent1 sent2 ->
            ifDoc env sent0 sent1 sent2
        LetSent defs sent ->
            letDoc env defs sent
        _ -> concatD [] -- Should be unreachable.


-------------------------------------------------------------
-- Helper functions
-------------------------------------------------------------

-- |Returns the String to bring for binary operator sentences.
binOpDoc :: Env -> SENT -> SENT -> String -> Int -> (SENT -> Bool) -> Doc
binOpDoc env sent0 sent binOpStr binOpTab binOpTest =
    concatD [runReader (prt sent0) env1 
            , binaryOpInd env binOpStr
            , runReader (prt sent) env2
            ]
        where env1 = binEnv1 env binOpTab (binOpTest sent0) binOpLabel1
              env2 = binEnv2 env binOpTab (binOpTest sent) binOpLabel2
              -- what are the labels?
              binOpLabel1 = case binOpStr of
                              _ | binOpStr == andStr -> 1
                                | binOpStr == orStr || binOpStr == impStr -> 3
                                | otherwise -> 0 -- should be unreachableb
              binOpLabel2 = case binOpStr of
                              _ | binOpStr == andStr -> 2
                                | binOpStr == orStr || binOpStr == impStr -> 4
                                | otherwise -> 0 -- should be unreachableb

-- |Returns the String to print for a forall/exists sentence.
quantDoc :: Env -> [TERM] -> SENT -> String -> Int -> (SENT -> Bool) -> Doc
quantDoc env vars sent quantStr quantTab quantTest =
    concatD $ [ quantOpInd env quantStr
              , concatD $ 
                        intersperse 
                        (argSeparators env)
                        (prtList vars (repeat ((resetEnv env) {innerTerm = True})))
              , doc (showString quantVarsMark)
              , doc (showString brkStr)
              , runReader (prt sent) env1
              ]
        where env1 = quantEnv1 env quantTab (quantTest sent) quantLabel
              quantLabel = case quantStr of 
                             _ | quantStr == forallStr -> 8
                               | quantStr == existsStr -> 9
                               | otherwise -> 0 --should be unreachable

-- |Returns the string to print for if-then-else sentences.
ifDoc :: Env -> SENT -> SENT -> SENT -> Doc
ifDoc env sent0 sent1 sent2 =
    concatD $ [ quantOpInd env ifStr
              , runReader (prt sent0) e1
              , doc (showString brkStr)
              , quantOpInd e2 thenStr 
              , runReader (prt sent1) e3
              , doc (showString brkStr)
              , quantOpInd e2 elseStr
              , runReader (prt sent2) e4
              ]
        where l = ifTab
              e1 = ifEnv env l (l - (length ifStr)) 5
              e3 = ifEnv env l (l - (length thenStr)) 6
              e4 = ifEnv env l (l - (length elseStr)) 7
              e2 = env {newLn = True}

-- |New environment for the second argument to a binary operator.
ifEnv :: Env 
      -> Int -- ^ length of ifTab 
      -> Int -- ^ extra space needed because "if" is shorter than "then" and "else"
      -> Int -- ^ operand label
      -> Env
ifEnv env tab n i = EnvDT 
                    (numApp (showLabels env) (label env) i)
                    False
                    newUnOp
                    newAbsInd
                    (n-1)
                    (defaultInd env)
                    False
                    False
                    False
                    (showLabels env)
                    (noLabels env)
    where newUnOp = 0
          newAbsInd = upIndUnOp env tab

-- |Returns the doc for let [defs] in SENT.  [DEF] should be nonempty.
letDoc :: Env -> [DEF] -> SENT -> Doc
letDoc env defs sent = 
    concatD $ (quantOpInd env letStr):
            letdefs
            ++ [ doc $ showString brkStr
               , quantOpInd e1 inStr 
               , runReader (prt sent) e2
               ]
          where n = nextLnArgs e4
                m = letTab - (length inStr)
                letdefs = intersperse n (prtList defs $ repeat e3)
                e2 = letEnv env letTab  m True
                e1 = env {newLn = True}
                e3 = letEnv env letTab m False
                e4 = env { absInd = (absInd env) + letTab }

letEnv :: Env 
       -> Int -- ^ length of letTab
       -> Int -- ^ extra space needed because "let" is longer than "in"
       -> Bool -- ^ whether labels should be shown or suppressed
       -> Env
letEnv env tab n l = EnvDT 
                     --(numApp (showLabels env) (label env) 1)
                     (label env)
                     False
                     0
                     newAbsInd
                     (n-1)
                     (defaultInd env)
                     False
                     False
                     False
                     l
                     (noLabels env)
    where newAbsInd = upIndUnOp env tab


notEnv :: Env -> Int -> Bool -> Env
notEnv env tab l = EnvDT 
                   (numApp (showLabels env) (label env) 0)
                   False
                   ((unOp env) + 1)
                   newAbsInd
                   0
                   (defaultInd env)
                   False
                   False
                   False
                   l
                   (noLabels env)
    where newAbsInd = upIndUnOp env tab

-- |Takes an environment and returns separators (default is commas) for between
-- lists of variables, terms, etc. and if necessary, it inserts linebreak
-- commands.  The Doc returned is interspersed into the list of of variables or
-- terms.
argSeparators :: Env -> Doc
argSeparators env =
  concatD [ doc $ showString argSepStr
          , sepStr]
    where sepStr = if splitArgs env 
                   then nextLnArgs env
                   else doc $ spaces 0

-- |Puts either args or curried arguments on the next line with the right indenting.
nextLnArgs :: Env -> Doc
nextLnArgs env =
    doc $ concatS [ showString brkStr
                  , computeSpcs 
                    (noLabels env) --(showLabels env) 
                    (defaultInd env - 1) 
                    (absInd env)
                  ]


-------------------------------------------------------------
-- Term Helper functions
-------------------------------------------------------------

-- |Are the args long enough that we have to split
-- them, or is there a curried function that is a
-- term?
newSplit :: [TERM] -> Bool
newSplit terms = (maxArgLen <= (maxArg terms))
                 || (curriedTerm terms)
                    
curriedTerm :: [TERM] -> Bool
curriedTerm terms = 
    case terms of
      []   -> False
      t:ts -> case t of
                FunctTerm _ ((Terms _):termsLst) ->
                    if null termsLst
                    then curriedTerm ts
                    else True
                ConstVarTerm _ -> curriedTerm ts

maxArg :: [TERM] -> Int
maxArg terms = 
    let mlst = map 
               (\_ -> foldl max 0 (map (\x -> termStrLens x) terms))
               terms
    in maximum mlst
       
termStrLens :: TERM -> Int
termStrLens term = 
    case term of
      FunctTerm functid termsLst -> sumFunctTerms functid (maxTerm functid termsLst)
      ConstVarTerm (Idents i) -> length i 
    where maxTerm id ts = 
              maximumBy 
              (\x y -> compare 
                       (sumFunctTerms id x)
                       (sumFunctTerms id y))
              ts 

          sumFunctTerms :: FunctId -> TERMS -> Int
          sumFunctTerms functid termsLst = functIdLen + termsSum 
              where functIdLen = case functid of FunctId i -> length i
                    terms = case termsLst of Terms ts -> ts
                    termsSum = foldl (+) 0 (map (\x -> termStrLens x) terms) + sepLens
                    sepLens = 0
-------------------------------------------------------------

-------------------------------------------------------------
-- Labeling Helper functions
-------------------------------------------------------------

numApp :: Bool -- ^ are labels currently suppressed (e.g., in let...in statements). 
       -> Int -- ^ depth
       -> Int -- ^ which operand
       -> Int 
numApp b n m = if b
               then n * 10 + m 
               else n

showLabel :: Env -> ShowS
showLabel env = if noLabels env
                then if showLabels env
                     then showString $ show $ label env
                     else spaces $ (defaultInd env) - 1 
                else spaces 0

predIdLen :: PredId -> Int
predIdLen (PredId i) = length i

functIdLen :: FunctId -> Int
functIdLen (FunctId i) = length i

-- |Absolute indentation (for splitting across lines and not splitting).
absIndUp :: Env -> Int -> Int
absIndUp env predlen = 
    -- indentation when a predicate is split across lines.
--    if split then predlen + initAbs else initAbs
    predlen + initAbs 
    where initAbs = if innerTerm env then (absInd env) + 1 else absInd env

andSent :: SENT -> Bool
andSent s = case s of
              AndSent _ _ -> True
              _ -> False

orSent :: SENT -> Bool
orSent s = case s of
              OrSent _ _ -> True
              _ -> False

impSent :: SENT -> Bool
impSent s = case s of
              ImpSent _ _ -> True
              _ -> False

forallSent :: SENT -> Bool
forallSent s = case s of
                 ForallSent _ _ -> True
                 _ -> False

existsSent :: SENT -> Bool
existsSent s = case s of
                 ExistsSent _ _ -> True
                 _ -> False
-------------------------------------------------------------

-------------------------------------------------------------
-- Binary operator helper functions
-------------------------------------------------------------

-- |Returns the new environment for the first argument to a binary operator.
binEnv1 :: Env 
        -> Int
        -> Bool -- ^ is the same operator as we've just seen, so no indentation
        -> Int -- ^ label
        -> Env
binEnv1 env tab b l = EnvDT 
                      (numApp (showLabels env) (label env) l)
                      (newLn env)
                      0 --newunOp
                      newabsInd
                      newRelind
                      (defaultInd env)
                      b
                      False
                      False
                      (showLabels env)
                      (noLabels env)
    where newabsInd = if b then absInd env else upIndUnOp env tab
          newRelind = relPrevOp --if b then relInd env else relPrevOp 
          -- redundant code?
          relPrevOp = if prevSameBinOp env
                      then relInd env
                      else relUpdate (relInd env) tab

-- |Returns the new environment for second argument to a binary operator (see documentation for binEnv1).
binEnv2 :: Env -> Int -> Bool -> Int -> Env
binEnv2 env tab b l = EnvDT 
                      (numApp (showLabels env) (label env) l)
                      False
                      0 --newUnOp
                      newAbsInd
                      0
                      (defaultInd env)
                      b
                      False
                      False
                      (showLabels env)
                      (noLabels env)
    where newAbsInd = if b then absInd env else upIndUnOp env tab
-------------------------------------------------------------

                          

-------------------------------------------------------------
-- Sentence Helper functions
-------------------------------------------------------------

-- |If the next sentence to parse is a binary operator sentence, then don't do anything
-- the "not" will printed with the next sentence.  Otherwise, just do the indenting.
checkUnOpArg :: SENT -> String -> Doc
checkUnOpArg e s = if checkBinOp e then doc $ spaces 0
                   else if checkQuant e then doc $ spaces 0
                        else doc $ showString s

-- |True if there is a sequence of "not sentences" followed by a quantified
-- sentence.
checkQuant :: SENT -> Bool
checkQuant e = case e of 
                 NegSent e1 -> checkQuant e1
                 ExistsSent _ _ -> True
                 ForallSent _ _ -> True
                 _ -> False
                 
-- |True if there is a sequence of negated sentences followed by a "binary operator
-- sentence".
checkBinOp :: SENT -> Bool
checkBinOp e = case e of
                 NegSent e1 -> checkBinOp e1
                 AndSent _ _ -> True
                 OrSent _ _ -> True
                 ImpSent _ _ -> True
                 _ -> False

negInd :: Env -> SENT -> Doc
negInd env e = if checkBinOp e then doc $ spaces 0 
               else if checkQuant e then doc $ spaces 0  
                    else simpInd env
-------------------------------------------------------------


--  |New environment for an argument to a quantifier.
quantEnv1 :: Env -> Int -> Bool -> Int -> Env
quantEnv1 env tab b l = EnvDT 
                        (numApp (showLabels env) (label env) l) 
                        True
                        0
                        newAbsInd
                        newRelInd
                        (defaultInd env)
                        b
                        False
                        False
                        (showLabels env)
                        (noLabels env)
    where newAbsInd = if b then absInd env else upIndUnOp env tab
          newRelInd = if b then relInd env else relUpdate (relInd env) tab
          
-- |If the env has not been indented yet (i==0), then just update according to the
-- operator's tab width (j); otherwise add the old relative indent, the new tab, and
-- an extra space between the strings.
relUpdate :: Int 
          -> Int -- ^ i==0 menas the environment hasn't been indented yet.
          -> Int -- ^ 
relUpdate i j = if i==0 then j else i+j+1

-- |Indentation for binary operator sentences.
simpInd :: Env -> Doc
simpInd env = doc $ concatS [indent (env {absInd=((absInd env)-1)})] where
    indent env = if (unOp env > 0) then spaces 0 -- just saw a "not"
                 else if newLn env 
                      -- binary operator, on new line
                      then computeSpcs
                               (noLabels env) --(showLabels env) 
                               (defaultInd env - 1) 
                               (absInd env)
                      -- after binary operator, either right after or arbitrarily after 
                      else spaces (relInd env)  


-- |Returns an absolute indentation depending on the operator size and whether
-- there is a preceding unary operator.  Does not indent for operators of the same
-- kind (so there's no precedence to record).
upIndUnOp :: Env 
          -> Int -- ^ operator size
          -> Int 
upIndUnOp env t = 1 + (absInd env) + t -- + (unOp env) -- + negTab * (unOp env)

-- If we're inside a "not" sentence, then put this sentence right after the not;
-- otherwise indent it by ind
quantOpInd :: Env -> String -> Doc
quantOpInd env op = 
    doc $ concatS [ putLabel 
                  , quantIndent  
--                  , makeNots (unOp env) (prevSameBinOp env)
                  , showString op
                  ] 
        where putLabel = if newLn env 
                         then showLabel env 
                         else spaces 0
              quantIndent = if newLn env -- If there's a label, I know newLn=True.
                            then labelInd env
                            -- Subtract out all the neg tabs: NegSent adds to 
                            -- relInd, but those should count for sentences on the
                            -- same line as the neg.
                            else spaces $ rel - ((negTab + 1) * unOp env)
              rel = let r = relInd env
                    in if r == 0 then r else r + 1

-- |If we're inside a "not" sentence, then put this sentence right after the "not"s.
binaryOpInd :: Env -> String -> Doc
binaryOpInd env op = 
    doc $ concatS [ showString brkStr
                  , showLabel env
                  , labelInd env
                  , showString op
                  ]

-- |Compute spaces from beginning of line.  
computeSpcs :: Bool -- ^ are there labels
            -> Int -- ^ spaces before separator
            -> Int -- ^ spaces after separator
            -> ShowS
computeSpcs b i j = 
    showString (concat $ (replicate i spaceStr)
                           ++ sep ++ 
                                  (replicate k spaceStr))
    where sep = if b then [labelSepStr] else []
          k = if b then j + 1 
              else j 

-- |Returns the indentation for directly after a label.
labelInd :: Env -> ShowS
labelInd env = 
    computeSpcs (noLabels env) --(showLabels env) 
                    ((defaultInd env) - labelLen - 1) (absInd env)
        where labelLen = if (noLabels env) --showLabels env
                         then length $ show $ label env
                         else 0