cspretty-1.0: Language/CSPM/Pretty.hs
{- |
Module : Language.CSP.Pretty
Description : Pretty printing for the CSP abstract syntax
Copyright : Draper Laboratories
The two functions in the module are used for pretty-printing the abstract CSP
syntax. The output is intended to be readable by FDR3.
-}
module Language.CSPM.Pretty (emitMod, emitMods) where
import Language.CSPM.Syntax
import Text.PrettyPrint
import Data.List
import Control.Monad
import qualified Data.Map as M
import qualified Data.Set as S
-- We need to keep track of which identifiers are in scope, so that we can use
-- simple names where possible. We use a state monad (note: not a reader
-- monad, since there are globals, though we do provide reader like
-- functionality). The state consists of three parts:
--
-- - A map of identifiers to Doc, which says how to print anything currently
-- in scope.
--
-- - A Set, which just contains the range of the map. When we see a new
-- identifier, we need to check that the way we want to print it doesn't
-- conflict with things already in scope. Keeping a around is much more
-- efficient than getting the range of the map as a list and searching that.
--
-- - A list of "warnings". If we encounter an identifier that's not in scope,
-- we have to guess about how to print it. This may not be safe, so we note
-- the problem in the warnings.
--
-- Additionally, because CSP declarations may be mutually recursive, we do a
-- first pass to add all the global variables to the monad. This first pass
-- also shows up where a block of local definitions may be mutually recursive,
-- as in let-within clauses.
data PPState = PPState {ppIdMap :: !(M.Map Id String),
ppUsedDocs :: !(S.Set String),
ppWarnings :: ![String]}
emptyPPState :: PPState
emptyPPState = PPState {ppIdMap = M.empty,
ppUsedDocs = S.empty,
ppWarnings = []}
newtype PP a = PP (PPState -> (PPState,a))
unPP :: PP a -> PPState -> (PPState,a)
unPP (PP f) = f
instance Functor PP where
fmap f (PP g) = PP (\st -> fmap f (g st))
instance Monad PP where
return x = PP $ \pps -> (pps,x)
m >>= k = PP $ \pps -> let (pps',res) = unPP m pps in unPP (k res) pps'
instance Applicative PP where
pure = return
(<*>) = ap
runPP :: PPState -> PP a -> (a,[String])
runPP st (PP f) = let (st',res) = f st in (res, ppWarnings st')
getIdMap :: PP (M.Map Id String)
getIdMap = PP $ \pps -> (pps,ppIdMap pps)
warn :: String -> PP ()
warn warning = PP $ \pps -> (pps {ppWarnings = warning : ppWarnings pps},())
addGlobal :: Id -> PP Doc
addGlobal var = PP $ \pps ->
let ppvar = if S.member niceVersion (ppUsedDocs pps)
then uglyVersion
else niceVersion
in
(pps {ppIdMap = M.insert var ppvar (ppIdMap pps),
ppUsedDocs = S.insert ppvar (ppUsedDocs pps)},
text ppvar)
where
niceVersion :: String
niceVersion = namePart var
uglyVersion :: String
uglyVersion =
case var of
Id (s,i) -> s ++ show i
Fixed s -> s
addLocal :: Id -> (Doc -> PP a) -> PP a
addLocal var action = PP $ \pps ->
case M.lookup var (ppIdMap pps) of
Just d -> unPP (action $ text d) pps
Nothing ->
let ppvar = if S.member niceVersion (ppUsedDocs pps)
then uglyVersion
else niceVersion
(pps',result) =
unPP (action $ text ppvar) $
pps {ppIdMap = M.insert var ppvar (ppIdMap pps),
ppUsedDocs = S.insert ppvar (ppUsedDocs pps)}
in
(pps' {ppIdMap = M.delete var (ppIdMap pps'),
ppUsedDocs = S.delete ppvar (ppUsedDocs pps')},
result)
where
niceVersion :: String
niceVersion = namePart var
uglyVersion :: String
uglyVersion =
case var of
Id (s,i) -> s ++ show i
Fixed s -> s
addLocals :: [Id] -> ([Doc] -> PP a) -> PP a
addLocals vars action = addLocalsRec vars []
where
addLocalsRec [] ds = action $ reverse ds
addLocalsRec (v:vs) ds =
addLocal v $ \d -> addLocalsRec vs (d:ds)
---
ppId :: Id -> PP Doc
ppId var = do
idmap <- getIdMap
case M.lookup var idmap of
Just d -> return $ text d
Nothing -> do
pp <-
case var of
Fixed s -> return s
Id (s,i) -> do
warn $ "Identifier " ++ show var ++ " not found."
return $ s ++ show i
return $ text pp
-------------------------------
commas :: [Doc] -> Doc
commas es = hsep $ punctuate comma es
dots :: [Doc] -> Doc
dots es = hcat $ punctuate (char '.') es
ppFDRMod :: FDRMod -> PP Doc
ppFDRMod tops = do
addTLGlobals tops
ttops <- mapM ppDefinition $ topLevels tops
return $ vcat $ punctuate (text "\n") ttops
-- This takes a pattern and does two things: tells you how it should be
-- displayed, and extends the local scope with the relevant identifiers for
-- the duration of the pretty printing.
ppPattern :: Pat -> (Doc -> PP a) -> PP a
ppPattern (PId var) f = addLocal var f
ppPattern (PConcat p1 p2) f = ppBinaryPattern p1 p2 (char '^') f
ppPattern (PDot p1 ps) f = ppPatList (p1:ps) (char '.') f
ppPattern (PDouble p1 p2) f = ppBinaryPattern p1 p2 (text "@@") f
ppPattern (PList pats) f =
ppPatList pats comma $ \ppats -> f $ char '<' <> ppats <> char '>'
ppPattern (PConst c) f = f $ ppConst c
ppPattern PEmptySet f = f $ text "{}"
ppPattern (PSingletonSet p) f = ppPattern p $ \pp -> f $ braces pp
ppPattern (PTuple pats) f =
ppPatList pats comma $ \ppats -> f $ parens ppats
ppPattern PWildCard f = f $ char '_'
-- abstract out the common case of printing a binary pattern
ppBinaryPattern :: Pat -> Pat -> Doc -> (Doc -> PP a) -> PP a
ppBinaryPattern p1 p2 pnct f = do
ppPatParens p1 $ \pp1 ->
ppPatParens p2 $ \pp2 ->
f $ pp1 <> pnct <> pp2
-- abstract out the common case of printing a list of patterns
ppPatList :: [Pat] -> Doc -> (Doc -> PP a) -> PP a
ppPatList pats pnct f = patList pats []
where
-- patList :: [Exp] -> [Doc] -> PP a
patList [] ds = f $ hcat $ punctuate pnct $ reverse ds
patList (p:ps) ds = ppPatParens p $ \d -> patList ps (d:ds)
-- prints the pattern with an extra set of parens if it's not a var
ppPatParens :: Pat -> (Doc -> PP a) -> PP a
ppPatParens p@(PId _) f = ppPattern p f
ppPatParens p f = ppPattern p (\d -> f $ parens d)
-- print a datatype constructor declaration
ppConstructor :: (Id,[Exp]) -> PP Doc
ppConstructor (c,tys) = do
tc <- ppId c
ttys <- mapM ppExp tys
return $ dots (tc : map parens ttys)
ppDefinition :: Definition -> PP Doc
ppDefinition (DVar p e) = do
-- Note that this may "double add" the variables in the pattern to the map,
-- since they were probably added when we entered the scope of this definition
-- as part of handling mutually recursive definitions. This is fine, because
-- ppPattern calls addLocal, which handles existing variables declarations
-- gracefully.
ppPattern p $ \pp -> do
pe <- ppExp e
return $ pp <+> char '=' <+> pe
ppDefinition (DFun funName funClauses) = do
tname <- ppId funName
vcat <$> mapM (ppFunClause tname) funClauses
where
ppFunClause :: Doc -> ([Pat],Exp) -> PP Doc
ppFunClause fnm (pats,body) = ppPatList pats (char ',') $ \ppats -> do
pbody <- ppExp body
return $ fnm <+> parens ppats <+> char '=' $+$ (nest 2 $ pbody)
ppDefinition (DAnnot x t) = do
px <- ppId x
pt <- ppType t
return $ px <+> text "::" <+> pt
ppDefinition (DDataType nm cnstrs) = do
tnm <- ppId nm
tcnstrs <- mapM ppConstructor cnstrs
return $
text "datatype" <+> tnm <+> char '='
<+> (hcat $ punctuate (text " | ") tcnstrs)
ppDefinition (DSubType nm cnstrs) = do
tnm <- ppId nm
tcnstrs <- mapM ppConstructor cnstrs
return $
text "subtype" <+> tnm <+> char '='
<+> (hcat $ punctuate (text " | ") tcnstrs)
ppDefinition (DChan xs []) = do
pxs <- commas <$> mapM ppId xs
return $ text "channel" <+> pxs
ppDefinition (DChan xs tys) = do
pxs <- commas <$> mapM ppId xs
ptys <- mapM ppType tys
return $ text "channel" <+> pxs <+> colon <+> dots ptys
ppDefinition (DInclude str) =
return $ text "include" <+> text (show str) --- XXXX hack for escape chars
ppDefinition (DExternal x) = do
px <- ppId x
return $ text "external" <+> px
ppDefinition (DTransparent x) = do
px <- ppId x
return $ text "transparent" <+> px
ppDefinition (DAssert a m) = do
pa <- ppAssertion a m
return $ text "assert" <+> pa
--just the letter part, not the brackets or [T=
modelLetter :: Model -> String
modelLetter MT = "T"
modelLetter MF = "F"
modelLetter MFD = "FD"
--This is [T] or [FD], etc.
ppModel :: Model -> Doc
ppModel = brackets . text . modelLetter
ppAssertion :: Assertion -> Model -> PP Doc
ppAssertion (ARefines p q) m = do
pp <- ppExp p
pq <- ppExp q
return $ pp <+> text ('[' : pm ++ "=") <+> pq
where
pm = modelLetter m
ppAssertion (ADeadlockFree p) m = do
pp <- ppExp p
let pm = ppModel m
return $ pp <+> text ":[deadlock free" <+> pm <> char ']'
ppAssertion (ADivergenceFree p) m = do
pp <- ppExp p
let pm = ppModel m
return $ pp <+> text ":[divergence free" <+> pm <> char ']'
ppAssertion (ADeterministic p) m = do
pp <- ppExp p
let pm = ppModel m
return $ pp <+> text ":[deterministic" <+> pm <> char ']'
ppAssertion (AHasTrace p t) m = do
pp <- ppExp p
pe <- ppExp t
let pm = ppModel m
return $ pp <+> text ":[has trace" <+> pm <> text "]:" <+> pe
ppType :: Type -> PP Doc
ppType TEvent = return $ text "Event"
ppType TChar = return $ text "Char"
ppType TBool = return $ text "Bool"
ppType TInt = return $ text "Int"
ppType TUnit = return $ text "Unit"
ppType (TList t) = do
pt <- ppType t
return $ char '<' <+> pt <+> char '>'
ppType (TSet t) = do
pt <- ppType t
return $ braces pt
ppType (TMap t1 t2) = do
pt1 <- ppType t1
pt2 <- ppType t2
return $ text "(|" <+> pt1 <+> text "=>" <+> pt2 <+> text "|)"
ppType (TData x) = ppId x
ppType (TRange a b) = do
pa <- ppExpParens a
pb <- ppExpParens b
return $ braces $ (parens pa) <> text ".." <> (parens pb)
ppType TProc = return $ text "Proc"
-- Printing comprehension/set statements. Three notes:
--
-- 1) We take in a list of comprehension statements rather than each
-- individually for reasons of scope. In particular, you can write
-- comprehensions like:
--
-- < x+1 | x <- xs, isOdd(x) >
--
-- Here, the later comprehension statement "isOdd(x)" needs "x" to be in
-- scope.
--
-- 2) For the same reason, ppCompStmts takes in an argument indicating the
-- monadic scope of the local variables declared in the patterns (much like
-- addLocal and ppPattern).
--
-- 3) FDR3 appears to support both the "x <- a" syntax that is natural in
-- comprehensions, as in:
--
-- < x+1 | x <- xs >
--
-- and the "x : a" syntax that is natural in replicated operations, as in:
--
-- [] x : {0..5} @ P(x)
--
-- These mean the same thing, and it appears you can use either syntax in
-- either place. For uniformity, we use only the "<-" syntax, since it is
-- the one mentioned on the relevant fdr page:
--
-- https://www.cs.ox.ac.uk/projects/fdr/manual/cspm/syntax.html#csp-statements
ppCompStmt :: [CompStmt] -> (Doc -> PP a) -> PP a
ppCompStmt cs f = ppCS cs []
where
-- ppCS :: [CompStmt] -> [Doc] -> PP a
ppCS [] ds =
f $ commas $ reverse ds
ppCS (CSGen p e : css) ds = do
pe <- ppExp e
ppPattern p $ \pp -> ppCS css (pp <+> text "<-" <+> pe : ds)
ppCS (CSPred e : css) ds = do
pe <- ppExp e
ppCS css (pe : ds)
-- Printing expressions
ppExp :: Exp -> PP Doc
ppExp (EId x) = ppId x
ppExp (ELambda pats e) =
ppPatList pats comma $ \ppats -> do
te <- ppExp e
return $ char '\\' <+> ppats <+> char '@' <+> te
ppExp (EApp fun es) = do
tfun <- ppExpParens fun
tes <- mapM ppExp es
return $ tfun <> (parens $ commas tes)
ppExp (ELet defs e) = do
addTLLocals (FDRMod defs) $ do
pdefs <- mapM ppDefinition defs
pe <- ppExp e
return $ text "let" $$ nest 2 (vcat $ punctuate (text "\n") pdefs)
$$ text "within" $$ (nest 2 pe)
ppExp (EIfThenElse c e1 e2) = do
tc <- ppExp c
te1 <- ppExp e1
te2 <- ppExp e2
return $
text "if" <+> tc <+> text "then" $+$ (nest 2 te1)
$$ text "else" $+$ (nest 2 te2)
ppExp (EUOp op e) = do
te <- ppExpParens e
return $ ppUOp op <+> te
ppExp (EBinOp e1 op e2) = ppBOpExp e1 (ppBinOp op) e2
ppExp (EConst c) = return $ ppConst c
ppExp (EError s) = return $ text "error" <> (parens $ text $ show s)
ppExp (EDot e es) = do
te <- ppExpParens e
tes <- mapM ppExpParens es
return $ dots (te:tes)
ppExp (EExtChoice e1 e2) = ppBOpExp e1 (text "[]") e2
ppExp (EGuarded e1 e2) = ppBOpExp e1 (char '&') e2
ppExp (EHide e1 e2) = ppBOpExp e1 (char '\\') e2
ppExp (EIntChoice e1 e2) = ppBOpExp e1 (text "|~|") e2
ppExp (EPrefix e1 ces e2) = do
te1 <- ppExpParens e1
tces_te2 <- ppCommsPrefix ces []
return $ te1 <> tces_te2
where
ppCommsPrefix :: [(CommField)] -> [Doc] -> PP Doc
ppCommsPrefix [] ds = do
te2 <- ppExpParens e2
return $ hcat $ reverse $ te2 : (text " -> ") : ds
ppCommsPrefix (comm:comms) ds =
case ppComm comm of
(d,Left e) -> do
pe <- ppExpParens e
ppCommsPrefix comms ((d <> pe) : ds)
(d,Right p) ->
ppPattern p $ \pp ->
ppCommsPrefix comms ((d <> pp) : ds)
where
-- How to display the comm, and whether the thing that comes after it
-- is a binder (as in the case of "c?x -> ...") or not (as in the case
-- of "c!x -> ..."
ppComm :: CommField -> (Doc,Either Exp Pat)
ppComm (CFPlain e) = (char '.', Left e)
ppComm (CFInput p) = (char '?', Right p)
ppComm (CFOutput e) = (char '!', Left e)
ppComm (CFNDInput p) = (char '$', Right p)
ppExp (EProject e1 e2) = ppBOpExp e1 (text "|\\") e2
ppExp (ERename e1 nms) = do
pe1 <- ppExpParens e1
pnms <- mapM (\(n1,n2) -> (,) <$> ppExpParens n1 <*> ppExpParens n2) nms
let prnms = map (\(pn1,pn2) -> pn1 <+> text "<-" <+> pn2) pnms
return $ pe1 <+> text "[[" <+> commas prnms <+> text "]]"
ppExp (EAlphaParallel p a b q) = do
pa <- ppExpParens a
pb <- ppExpParens b
ppBOpExp p (brackets $ pa <+> text "||" <+> pb) q
ppExp (EGenParallel p a q) = do
pa <- ppExp a
ppBOpExp p (text "[|" <+> pa <+> text "|]") q
ppExp (EInterleave e1 e2) = ppBOpExp e1 (text "|||") e2
ppExp (EException p a q) = do
pa <- ppExp a
ppBOpExp p (text "[|" <+> pa <+> text "|>") q
ppExp (EInterrupt e1 e2) = ppBOpExp e1 (text "/\\") e2
ppExp (ESeq e1 e2) = ppBOpExp e1 (char ';') e2
ppExp (ELinkedParallel p nms q) = do
pnms <- mapM (\(c,d) -> (,) <$> ppExpParens c <*> ppExpParens d) nms
let ppnms = commas $ map (\(pc,pd) -> pc <+> text "<->" <+> pd) pnms
ppBOpExp p ppnms q
ppExp (ETimeout e1 e2) = ppBOpExp e1 (text "[>") e2
ppExp (ESyncExtChoice p a q) = do
pa <- ppExp a
ppBOpExp p (text "[+" <+> pa <+> text "+]") q
ppExp (ESyncInterrupt p a q) = do
pa <- ppExp a
ppBOpExp p (text "/+" <+> pa <+> text "+\\") q
ppExp (ERepAlphaParallel cs a p) =
ppCompStmt cs $ \pstmts -> do
pa <- ppExp a
pp <- ppExpParens p
return $ text "||" <+> pstmts <+> char '@' <+> brackets pa <+> pp
ppExp (ERepExtChoice cs p) = ppRepExp (text "[]") cs p
ppExp (ERepGenParallel a cs p) = do
pa <- ppExp a
ppRepExp (text "[|" <+> pa <+> text "|]") cs p
ppExp (ERepInterleave cs p) = ppRepExp (text "|||") cs p
ppExp (ERepIntChoice cs p) = ppRepExp (text "|~|") cs p
ppExp (ERepLinkedParallel links cs p) = do
plinks <- mapM (\(l,r) -> (,) <$> ppExpParens l <*> ppExpParens r) links
let linkedLinks = map (\(pl,pr) -> pl <+> text "<->" <+> pr) plinks
ppRepExp (brackets $ commas linkedLinks) cs p
ppExp (ERepSeq cs p) = ppRepExp (char ';') cs p
ppExp (ERepSyncExtChoice a cs p) = do
pa <- ppExp a
ppRepExp (text "[+" <+> pa <+> text "+]") cs p
ppExp (EList es) = do
tes <- mapM ppExpParens es
return $ char '<' <+> commas tes <+> char '>'
ppExp (EListComp es cs) =
ppCompStmt cs $ \pcs -> do
pes <- mapM ppExpParens es
return $ char '<' <+> commas pes <+> char '|' <+> pcs <+> char '>'
ppExp (EListFrom e) = do
pe <- ppExpParens e
return $ char '<' <+> pe <+> text "..>"
ppExp (EListFromComp e cs) =
ppCompStmt cs $ \pcs -> do
pe <- ppExpParens e
return $ char '<' <+> pe <+> text ".. |" <+> pcs <+> char '>'
ppExp (EListFromTo e1 e2) = do
pe1 <- ppExpParens e1
pe2 <- ppExpParens e2
return $ char '<' <+> pe1 <+> text ".." <+> pe2 <+> char '>'
ppExp (EListFromToComp e1 e2 cs) =
ppCompStmt cs $ \pcs -> do
pe1 <- ppExpParens e1
pe2 <- ppExpParens e2
return $ char '<' <+> pe1 <+> text ".." <+> pe2
<+> char '|' <+> pcs <+> char '>'
ppExp (EListConcat e1 e2) = ppBOpExp e1 (char '^') e2
ppExp (EListLength e) = do
pe <- ppExp e
return $ char '#' <+> pe
ppExp (ETuple es) = parens . commas <$> mapM ppExp es
ppExp (ESet es) = braces . commas <$> mapM ppExp es
ppExp (ESetComp es cs) =
ppCompStmt cs $ \pcs -> do
pes <- mapM ppExp es
return $ braces $ commas pes <+> char '|' <+> pcs
ppExp (ESetFrom e) = do
pe <- ppExp e
return $ braces $ pe <+> text ".."
ppExp (ESetFromComp e cs) =
ppCompStmt cs $ \pcs -> do
pe <- ppExp e
return $ braces $ pe <+> text ".. |" <+> pcs
ppExp (ESetFromTo e1 e2) = do
pe1 <- ppExp e1
pe2 <- ppExp e2
return $ braces $ pe1 <+> text ".." <+> pe2
ppExp (ESetFromToComp e1 e2 cs) =
ppCompStmt cs $ \pcs -> do
pe1 <- ppExp e1
pe2 <- ppExp e2
return $ braces $ pe1 <+> text ".." <+> pe2 <+> char '|' <+> pcs
ppExp ESetInt = return $ text "Int"
ppExp ESetBool = return $ text "Bool"
ppExp (EEnumSet es) = do
pes <- commas <$> mapM ppExp es
return $ text "{|" <+> pes <+> text "|}"
ppExp (EEnumSetComp es cs) =
ppCompStmt cs $ \pcs -> do
pes <- commas <$> mapM ppExp es
return $ text "{|" <+> pes <+> char '|' <+> pcs <+> text "|}"
ppExp (EMap es) = do
tes <- mapM ppMapPair es
return $ text "(|" <+> commas tes <+> text "|)"
where
ppMapPair (e1, e2) = do te1 <- ppExpParens e1
te2 <- ppExpParens e2
return $ te1 <+> text "=>" <+> te2
-- parens around compound things only
ppExpParens :: Exp -> PP Doc
ppExpParens e@(EId _) = ppExp e
ppExpParens e@(EConst _) = ppExp e
ppExpParens e@(EList _) = ppExp e
ppExpParens e@(EListComp _ _) = ppExp e
ppExpParens e@(EListFrom _) = ppExp e
ppExpParens e@(EListFromComp _ _) = ppExp e
ppExpParens e@(EListFromTo _ _) = ppExp e
ppExpParens e@(EListFromToComp _ _ _) = ppExp e
ppExpParens e@(ETuple _) = ppExp e
ppExpParens e@(ESet _) = ppExp e
ppExpParens e@(ESetComp _ _) = ppExp e
ppExpParens e@(ESetFrom _) = ppExp e
ppExpParens e@(ESetFromComp _ _) = ppExp e
ppExpParens e@(ESetFromTo _ _) = ppExp e
ppExpParens e@(ESetFromToComp _ _ _) = ppExp e
ppExpParens e@(ESetInt) = ppExp e
ppExpParens e@(ESetBool) = ppExp e
ppExpParens e@(EEnumSet _) = ppExp e
ppExpParens e@(EEnumSetComp _ _) = ppExp e
ppExpParens e@(EMap _) = ppExp e
ppExpParens e = parens <$> ppExp e
-- Abstract the common case of "binary" operators, which actually comes up much
-- more than just the arithmetic ones.
ppBOpExp :: Exp -> Doc -> Exp -> PP Doc
ppBOpExp e1 pop e2 = do
pe1 <- ppExpParens e1
pe2 <- ppExpParens e2
return $ pe1 <+> pop <+> pe2
-- Abstract the common case of "replicated" operators
ppRepExp :: Doc -> [CompStmt] -> Exp -> PP Doc
ppRepExp op stmts e = do
ppCompStmt stmts $ \pstmts -> do
pe <- ppExp e
return $ op <+> pstmts <+> char '@' <+> pe
ppConst :: Const -> Doc
ppConst CStop = text "STOP"
ppConst CSkip = text "SKIP"
ppConst (CInt n) = integer n
ppConst (CChar c) = char '\'' <> char c <> char '\''
ppConst (CBool b) = if b then text "True" else text "False"
ppConst (CString s) = text $ show s -- XXX hack. I think this escapes things that matter?
ppConst CUnit = text "UnitVal"
ppUOp :: UOp -> Doc
ppUOp UNeg = char '-'
ppUOp UNot = text "not"
--ppUOp (Hide _) = error "Internal error: ppUOpApp called on hide"
ppBinOp :: BinOp -> Doc
ppBinOp BEq = text "=="
ppBinOp BLeq = text "<="
ppBinOp BLt = char '<'
ppBinOp BGeq = text ">="
ppBinOp BGt = char '>'
ppBinOp BAnd = text "and"
ppBinOp BOr = text "or"
ppBinOp BNeq = text "!="
ppBinOp BPlus = char '+'
ppBinOp BMinus = char '-'
ppBinOp BTimes = char '*'
ppBinOp BDiv = char '\\'
ppBinOp BMod = char '%'
------------------
------------------ Top-level identifiers
------------------
topLevelIDs :: FDRMod -> [Id]
topLevelIDs m = concatMap tlIDs $ topLevels m
where
tlIDs :: Definition -> [Id]
tlIDs (DFun nm _) = [nm]
tlIDs (DVar pat _) = patIDs pat
tlIDs (DAnnot _ _) = []
tlIDs (DDataType nm cnstrs) = nm : map fst cnstrs
tlIDs (DSubType nm _) = [nm]
tlIDs (DChan x _) = x
tlIDs (DInclude _) = []
tlIDs (DExternal f) = [f]
tlIDs (DTransparent f) = [f]
tlIDs (DAssert _ _) = []
-- The IDs inside a pattern
patIDs :: Pat -> [Id]
patIDs (PId x) = [x]
patIDs (PConcat p1 p2) = patIDs p1 ++ patIDs p2
patIDs (PDot p1 p2) = concatMap patIDs (p1:p2)
patIDs (PDouble p1 p2) = patIDs p1 ++ patIDs p2
patIDs (PList ps) = concatMap patIDs ps
patIDs (PConst _) = []
patIDs PEmptySet = []
patIDs (PSingletonSet p) = patIDs p
patIDs (PTuple ps) = concatMap patIDs ps
patIDs PWildCard = []
---- This scans a module and adds any top-level names to the monad, since they
---- may be used mutually recursively.
addTLGlobals :: FDRMod -> PP ()
addTLGlobals m = mapM_ addGlobal $ topLevelIDs m
-- The `PP a` arg here is the scope of these locals
addTLLocals :: FDRMod -> PP a -> PP a
addTLLocals m a = addLocals (topLevelIDs m) $ \_ -> a
--------------
--------------
--------------
genStyle :: Style
genStyle = Style {mode = LeftMode, lineLength = 0, ribbonsPerLine = 0}
preludeNames :: [Id]
preludeNames = []
prelude :: PPState
prelude = foldl' addName emptyPPState preludeNames
where
addName :: PPState -> Id -> PPState
addName pps nm@(Fixed s) =
pps {ppIdMap = M.insert nm s (ppIdMap pps),
ppUsedDocs = S.insert s (ppUsedDocs pps)}
addName pps nm@(Id (s,_)) =
pps {ppIdMap = M.insert nm s (ppIdMap pps),
ppUsedDocs = S.insert s (ppUsedDocs pps),
ppWarnings = w : (ppWarnings pps)}
where
w = "Non-fixed id " ++ show nm ++ " in prelude,"
-- | Pretty-prints an FDR3 module.
-- Returns the pretty-printed module as a string, and a list of warnings. The
-- module string should be valid FDR3 input. The warnings will mention any
-- non-fixed identifiers that are used out of their scope.
emitMod :: FDRMod -> (String,[String])
emitMod m = let (d,ws) = runPP prelude $ ppFDRMod m in
(renderStyle genStyle d, ws)
-- | Pretty-prints an FDR3 module.
-- Returns two lists of strings. The strings in the first list are the
-- pretty-printed input modules, and should be valid input for FDR3. The
-- strings in the second list are warnings, and will mention any non-fixed
-- identifiers used out of scope. Globals with non-fixed identifiers in each
-- input module are considered in scope for subsequent modules in the list.
emitMods :: [FDRMod] -> ([String],[String])
emitMods mds =
let (ds,ws) = runPP prelude $ mapM ppFDRMod mds in
(map (renderStyle genStyle) ds, ws)