{- # Prettyprinter for beautifHOL, a HOL prettyprinter # Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html # Lee Pike (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