Debug.hs

-- Specifies communication with user: Debugging, Error reporting, ...
{-# LANGUAGE GADTs,FlexibleContexts #-}
module Debug where

import Prelude hiding ((<>))

import BwdFwd
import Syntax
import ParserCommon
import RefineSyntaxCommon
import TypeCheckCommon

import Control.Monad
import Control.Monad.Except
import qualified Data.Map.Strict as M
import qualified Data.Set as S
import Data.List

import Debug.Trace

import Data.IORef
import System.IO.Unsafe

import Shonky.Syntax
import Shonky.Renaming

import qualified Text.PrettyPrint as PP

-- Is set by the main entry point if relevant flag detected.
-- 1) isDebugVerboseOn
-- 2) isDebugParserOn
-- 3) isDebugTypeCheckOn
debugMode :: IORef (Bool, Bool, Bool)
{-# NOINLINE debugMode #-}
debugMode = unsafePerformIO (newIORef (False, False, False))

-- Hack: Use () argument to prevent caching
getDebugMode :: () -> (Bool, Bool, Bool)
{-# NOINLINE getDebugMode #-}
getDebugMode () = unsafePerformIO (readIORef debugMode)

-- Output full (untrimmed) ty var names
-- Hack: Use () argument to prevent caching
isDebugVerboseOn :: () -> Bool
isDebugVerboseOn () = case getDebugMode () of (b, _, _) -> b

-- Output parsing process
-- Hack: Use () argument to prevent caching
isDebugParserOn :: () -> Bool
isDebugParserOn () = case getDebugMode () of (_, b, _) -> b

-- Output type checking process
-- Hack: Use () argument to prevent caching
isDebugTypeCheckOn :: () -> Bool
isDebugTypeCheckOn () = case getDebugMode () of (_, _, b) -> b

ifDebugTypeCheckOnThen :: Contextual () -> Contextual ()
ifDebugTypeCheckOnThen f = when (isDebugTypeCheckOn ()) f

{- Error messages (only producing the output strings) -}

errorRefNoMainFunction :: String
errorRefNoMainFunction = "no main function defined"

errorRefDuplParamData :: DataT Raw -> String
errorRefDuplParamData dt@(DT x _ _ _) = "duplicate parameter in datatype " ++ x ++ " (" ++ (show $ ppSourceOf dt) ++ ")"

errorRefDuplParamItf :: Itf Raw -> String
errorRefDuplParamItf itf@(Itf x _ _ _) = "duplicate parameter in interface " ++ x ++ " (" ++ (show $ ppSourceOf itf) ++ ")"

errorRefDuplParamItfAl :: ItfAlias Raw -> String
errorRefDuplParamItfAl itfAl@(ItfAlias x _ _ _) = "duplicate parameter in interface alias " ++ x ++ " (" ++ (show $ ppSourceOf itfAl) ++ ")"

errorRefDuplParamCmd :: Cmd Raw -> String
errorRefDuplParamCmd cmd@(Cmd x _ _ _ _) = "duplicate parameter in command " ++ x ++ " (" ++ (show $ ppSourceOf cmd) ++ ")"

errorRefAbMultEffVars :: Ab Raw -> [Id] -> String
errorRefAbMultEffVars ab@(Ab v m a) es = "ability has multiple effect variables " ++ show es ++ " (" ++ (show $ ppSourceOf ab) ++ ")"

errorRefEffVarNoParams :: Id -> String
errorRefEffVarNoParams x = "effect variable " ++ x ++ " may not take parameters"

errorRefIdNotDeclared :: String -> Id -> Raw -> String
errorRefIdNotDeclared sort x a = "no " ++ sort ++ " named " ++ x ++ " declared (" ++ (show $ ppSourceOf a) ++ ")"

errorRefExpectedUse :: Tm Refined -> String
errorRefExpectedUse tm = "expected use but got term: " ++ show tm ++ "(" ++ (show $ ppSourceOf tm) ++ ")"

errorRefEntryAlreadyDefined :: String -> Id -> String
errorRefEntryAlreadyDefined sort x = sort ++ " " ++ x ++ " already defined"

errorRefDuplTopTm :: String -> Id -> Source -> String
errorRefDuplTopTm sort x a = "duplicate " ++ sort ++ ": " ++ x ++ " already defined (" ++ show a ++ ")"

errorNumberOfArguments :: HasSource a => Id -> Int -> Int -> a -> String
errorNumberOfArguments x exp act a =
  x ++ " expects " ++ show exp ++ " argument(s) but " ++ show act ++
  " given (" ++ (show $ ppSourceOf a) ++ ")"

errorRefItfAlCycle :: Id -> String
errorRefItfAlCycle x = "interface alias " ++ show x ++ " is defined in terms of itself (cycle)"

errorTCNotInScope :: Operator Desugared -> String
errorTCNotInScope op = "'" ++ getOpName op ++ "' not in scope (" ++ (show $ ppSourceOf op) ++ ")"

errorTCPatternPortMismatch :: Clause Desugared -> String
errorTCPatternPortMismatch cls = "number of patterns not equal to number of ports (" ++ (show $ ppSourceOf cls) ++ ")"

errorTCCmdNotFoundInPort :: Id -> Int -> Port Desugared -> String
errorTCCmdNotFoundInPort cmd n port = "command " ++ cmd ++ "." ++ show n ++ " not found in adjustments of port " ++ (show $ ppPort port) ++ " (" ++ (show $ ppSourceOf port) ++ ")"

errorTCNotACtr :: Id -> String
errorTCNotACtr x = "'" ++ x ++ "' is not a constructor"

errorUnifDiffNumberArgs :: VType Desugared -> VType Desugared -> String
errorUnifDiffNumberArgs v1 v2 =
  "failed to unify " ++ (show $ ppVType v1) ++ " (" ++ (show $ ppSourceOf v1) ++ ") with " ++ (show $ ppVType v2) ++ " (" ++ (show $ ppSourceOf v2) ++ ")" ++ " because they have different numbers of type arguments"

errorUnifTys :: VType Desugared -> VType Desugared -> String
errorUnifTys t1 t2 =
  "failed to unify " ++ (show $ ppVType t1) ++ " (" ++ (show $ ppSourceOf t1) ++ ") with " ++ (show $ ppVType t2) ++ " (" ++ (show $ ppSourceOf t2) ++ ")"

errorUnifTyArgs :: TyArg Desugared -> TyArg Desugared -> String
errorUnifTyArgs t1 t2 =
  "failed to unify type arguments " ++ (show $ ppTyArg t1) ++ " (" ++ (show $ ppSourceOf t1) ++ ")" ++ " with " ++ (show $ ppTyArg t2) ++ " (" ++ (show $ ppSourceOf t2) ++ ")"

errorUnifAbs :: Ab Desugared -> Ab Desugared -> String
errorUnifAbs ab1 ab2 =
  "cannot unify abilities " ++ (show $ ppAb ab1) ++ " (" ++ (show $ ppSourceOf ab1) ++ ")" ++ " and " ++ (show $ ppAb ab2) ++ " (" ++ (show $ ppSourceOf ab2) ++ ")"

errorUnifItfMaps :: ItfMap Desugared -> ItfMap Desugared -> String
errorUnifItfMaps m1 m2 =
  "cannot unify interface maps " ++ (show $ ppItfMap m1) ++ " (" ++ (show $ ppSourceOf m1) ++ ")" ++ " and " ++ (show $ ppItfMap m2) ++ " (" ++ (show $ ppSourceOf m2) ++ ")"

errorAdaptor :: Adaptor Desugared -> Ab Desugared -> String
errorAdaptor adpd@(Adp x ns k _) ab =
  "Adaptor " ++ (show $ ppAdaptor adpd) ++
  " is not a valid adaptor in ambient " ++ (show $ ppAb ab) ++
  " (" ++  (show $ ppSourceOf adpd) ++ ")"
errorAdaptor adpd@(CompilableAdp x m ns _) ab =
  "Adaptor " ++ (show $ ppAdaptor adpd) ++
  " is not a valid adaptor in ambient " ++ (show $ ppAb ab) ++
  " (" ++  (show $ ppSourceOf adpd) ++ ")"

errorUnifSolveOccurCheck :: String
errorUnifSolveOccurCheck = "solve: occurs check failure"

errorFindCmdNotPermit :: String -> Desugared -> String -> Ab Desugared -> String
errorFindCmdNotPermit cmd loc itf amb = "command " ++ cmd ++ " belonging to interface " ++ itf ++ " not permitted by ambient ability: " ++ (show $ ppAb amb) ++ " (" ++ (show $ ppSourceOf amb) ++ ")"

{- Logging (output if debug mode is on) -}

logBeginFindCmd :: Id -> Id -> Maybe [TyArg Desugared] -> Contextual ()
logBeginFindCmd x itf mps = ifDebugTypeCheckOnThen $
  debugTypeCheckM $ "find command " ++ show x ++ " of interface " ++ show itf ++
                    " with instantiation " ++ show (mps >>= Just . (map (show . ppTyArg))) ++ "\n\n"

logEndFindCmd :: Id -> VType Desugared -> Contextual ()
logEndFindCmd x ty = ifDebugTypeCheckOnThen $
  debugTypeCheckM $ "ended find command " ++ show x ++ ", resulting type is: " ++
                    show (ppVType ty)

logBeginInferUse :: Use Desugared -> Contextual ()
logBeginInferUse u@(Op x _) = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "begin infer use of single: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show (ppUse u) ++ "\n\n"
  ctx <- getContext
  debugTypeCheckM ("cur. context is:\n" ++ (show $ ppContext ctx) ++ "\n\n")
logBeginInferUse u@(App f xs _) = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "begin infer use of app: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show (ppUse u) ++ "\n\n"
logBeginInferUse u@(Adapted rs t _) = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "begin infer use of app: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show (ppUse u) ++ "\n\n"


logEndInferUse :: Use Desugared -> VType Desugared -> Contextual ()
logEndInferUse u@(Op x _) ty = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "ended infer use of single: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show (ppUse u) ++ "\n   gives " ++ show (ppVType ty)
  ctx <- getContext
  debugTypeCheckM ("cur. context is:\n" ++ (show $ ppContext ctx) ++ "\n\n")
logEndInferUse u@(App f xs _) ty = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "ended infer use of app: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show (ppUse u) ++ "\n   gives " ++ show (ppVType ty) ++ "\n\n"
logEndInferUse u@(Adapted rs t _) ty = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "ended infer use of redirected: Under curr. amb. " ++
    show (ppAb amb) ++ " redirected by <" ++ (show rs) ++
    ">\n   infer type of " ++ show (ppUse u) ++
    "\n   gives " ++ show (ppVType ty) ++ "\n\n"

logBeginUnify :: VType Desugared -> VType Desugared -> Contextual ()
logBeginUnify t0 t1 = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "begin to unify\n   " ++ show (ppVType t0) ++ "\nwith\n   " ++ show (ppVType t1) ++ "\nCurrent context:\n" ++ show (ppContext ctx) ++ "\n\n"

logEndUnify :: VType Desugared -> VType Desugared -> Contextual ()
logEndUnify t0 t1 = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "ended unifying\n   " ++ show (ppVType t0) ++ "\nwith\n   " ++ show (ppVType t1) ++ "\nCurrent context:\n" ++ show (ppContext ctx) ++ "\n\n"

logBeginUnifyAb :: Ab Desugared -> Ab Desugared -> Contextual ()
logBeginUnifyAb ab0 ab1 = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "begin to unify ab. \n   " ++ show (ppAb ab0) ++ "\nwith\n   " ++ show (ppAb ab1) ++ "\nCurrent context:\n" ++ show (ppContext ctx) ++ "\n\n"

logEndUnifyAb :: Ab Desugared -> Ab Desugared -> Contextual ()
logEndUnifyAb ab0 ab1 = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "ended unifying ab. \n   " ++ show (ppAb ab0) ++ "\nwith\n   " ++ show (ppAb ab1) ++ "\nCurrent context:\n" ++ show (ppContext ctx) ++ "\n\n"

logBeginSolve :: Id -> Suffix -> VType Desugared -> Contextual ()
logBeginSolve a ext ty = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "begin to solve " ++ show a ++ " = " ++ show (ppVType ty) ++ "\n under suffix\n   " ++ show (ppSuffix ext) ++ "\n\n"

logSolveStep :: (Bool, Bool, Decl) -> Contextual ()
logSolveStep p = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "solving step: "
  case p of
    (_,     _,     TyDefn bty) -> debugTypeCheckM "\"inst-subs\""
    (True,  True,  Hole)       -> return ()
    (True,  False, Hole)       -> debugTypeCheckM "\"inst-define\""
    (False, True,  _)          -> debugTypeCheckM "\"inst-depend\""
    (False, False, d)          -> debugTypeCheckM $ "\"inst-skip-ty\", decl=" ++ show d
    (_,     _,     AbDefn _)   -> return ()
  debugTypeCheckM $ "current context:\n" ++ show (ppContext ctx) ++ "\n\n"

logEndSolve :: Id -> Suffix -> VType Desugared -> Contextual ()
logEndSolve a ext ty = ifDebugTypeCheckOnThen $ do
  ctx <- getContext
  debugTypeCheckM $ "ended solving " ++ show a ++ " = " ++ show (ppVType ty) ++ "\n under suffix\n   " ++ show (ppSuffix ext) ++ "\n\n"

-- logBeginSolveForEVar :: Id -> Suffix -> VType Desugared -> Contextual ()
-- logBeginSolve a ext ty = ifDebugTypeCheckOnThen $ do
--   ctx <- getContext
--   debugTypeCheckM $ "begin to solve " ++ show a ++ " = " ++ show (ppVType ty) ++ "\n under suffix\n   " ++ show (ppSuffix ext) ++ "\n\n"
--
-- logEndSolveForEVar :: Id -> Suffix -> VType Desugared -> Contextual ()
-- logEndSolve a ext ty = ifDebugTypeCheckOnThen $ do
--   ctx <- getContext
--   debugTypeCheckM $ "ended solving " ++ show a ++ " = " ++ show (ppVType ty) ++ "\n under suffix\n   " ++ show (ppSuffix ext) ++ "\n\n"

debugParserM :: (MonadicParsing m) => String -> m ()
debugParserM = traceM

debugRefineM :: String -> Refine ()
debugRefineM = traceM

checkArgs :: (HasSource a, MonadError String m) =>
             Id -> Int -> Int -> a -> m ()
checkArgs x exp act a =
  when (exp /= act) $
    throwError $ errorNumberOfArguments x exp act a

debugRefine :: String -> a -> a
debugRefine = trace

-- Uses the hack of of first retrieving context but without printing it.
-- This achieves that calls of this function are not cached and newly executed
-- every time.
debugTypeCheckM :: String -> Contextual ()
debugTypeCheckM str = do
  cxt <- getContext
  seq (ppContext cxt) traceM str

debugM :: (Monad m) => String -> m ()
debugM = traceM

{- Syntax pretty printers -}

(<+>) = (PP.<+>)
(<>) = (PP.<>)
($$) = (PP.$$)
($+$) = (PP.$+$)
text = PP.text
sep = PP.sep
nest = PP.nest
vcat = PP.vcat
hcat = PP.hcat
hsep = PP.hsep
colon = PP.colon
comma = PP.comma
empty = PP.empty
int = PP.int
punctuate = PP.punctuate
semi = PP.semi
rbrack = PP.rbrack
lbrack = PP.lbrack
doubleQuotes = PP.doubleQuotes
ppBrackets = PP.brackets
ppParens = PP.parens
ppChar = PP.char
vsep :: [PP.Doc] -> PP.Doc
vsep = foldr ($+$) empty

type Doc = PP.Doc

ppProg :: (Show a, HasSource a) => Prog a -> PP.Doc
ppProg (MkProg tts) = foldl (PP.$+$ ) PP.empty (map ppTopTm tts)

ppTopTm :: (Show a, HasSource a) => TopTm a -> PP.Doc
ppTopTm (DataTm dt _) = ppDataT dt
ppTopTm (ItfTm itf _) = ppItf itf
ppTopTm (SigTm sig _) = text $ show sig
ppTopTm (ClsTm cls _) = text $ show cls
ppTopTm (DefTm def _) = ppMHDef def

ppDataT :: (Show a, HasSource a) => DataT a -> PP.Doc
ppDataT (DT id tyVars ctrs a) = text "data" <+>
                              text id <+>
                              sep (map (text . show) tyVars) <+>
                              text "=" <+>
                              sep (map (text . show) ctrs)

ppItf :: (Show a, HasSource a) => Itf a -> PP.Doc
ppItf (Itf id tyVars cmds a) = text "interface" <+>
                           text id <+>
                           sep (map (text . show) tyVars) <+>
                           text "=" <+>
                           sep (map (text . show) cmds)

ppMHDef :: (Show a, HasSource a) => MHDef a -> PP.Doc
ppMHDef (Def id cty cls _) = text id <+> text ":" <+>
                             ppCType cty $$
                             sep (map (ppClause id) cls)

ppClause :: (Show a, HasSource a) => Id -> Clause a -> PP.Doc
ppClause id (Cls ps tm _) = text id <+>
                            (vcat . map ppPattern) ps <+> text "=" $$
                            (nest 3 . ppTm) tm

ppPattern :: (Show a, HasSource a) => Pattern a -> PP.Doc
ppPattern (VPat vp _) = ppValuePat vp
ppPattern (CmdPat x n vps k _) = text "<" <+>
                                 text x <>
                                 (if n == 0 then empty
                                            else text "." <> int n) <+>
                                 (hcat . map ppValuePat) vps <+>
                                 text "->" <+>
                                 text k <+>
                                 text ">"
ppPattern (ThkPat x _) = text x

ppValuePat :: (Show a, HasSource a) => ValuePat a -> PP.Doc
ppValuePat (VarPat x _) = text x
ppValuePat (DataPat x vps _) = text x <+> (hcat . map ppValuePat) vps
ppValuePat (IntPat n _) = (text . show) n
ppValuePat (CharPat c _) = (text . show) c
ppValuePat (StrPat s _) = (text . show) s
ppValuePat (ConsPat vp1 vp2 _) = ppValuePat vp1 <+> text "::" <+> ppValuePat vp2
ppValuePat (ListPat vps _) = (hcat . map ppValuePat) vps

ppCType :: (Show a, HasSource a) => CType a -> PP.Doc
ppCType (CType ps q _) = text "{" <> ports <> peg <> text "}"
  where
    ports = case map ppPort ps of
      [] -> PP.empty
      xs -> foldl (\acc x -> x <+> text "-> " <> acc) PP.empty (reverse xs)
    peg = ppPeg q

ppVType :: (Show a, HasSource a) => VType a -> PP.Doc
ppVType (DTTy x ts _) = text x <+> foldl (<+>) PP.empty (map ppTyArg ts)
ppVType (SCTy cty _) = ppCType cty
ppVType (TVar x _) = text x
ppVType (RTVar x _) = if isDebugVerboseOn () then text x else text $ trimVar x
ppVType (FTVar x _) = if isDebugVerboseOn () then text x else text $ trimVar x
ppVType (StringTy _) = text "String"
ppVType (IntTy _) = text "Int"
ppVType (CharTy _) = text "Char"

ppTyArg :: (Show a, HasSource a) => TyArg a -> PP.Doc
ppTyArg (VArg t _) = ppParenVType t
ppTyArg (EArg ab _) = ppAb ab

ppParenVType :: (Show a, HasSource a) => VType a -> PP.Doc
ppParenVType v@(DTTy _ _ _) = text "(" <+> ppVType v <+> text ")"
ppParenVType v = ppVType v

ppPort :: (Show a, HasSource a) => Port a -> PP.Doc
ppPort (Port []   ty _) = ppVType ty
ppPort (Port adjs ty _) = text "<" <> (PP.hsep $ intersperse PP.comma $ map ppAdj adjs) <> text ">" <> ppVType ty

ppPeg :: (Show a, HasSource a) => Peg a -> PP.Doc
ppPeg (Peg ab ty _) = ppAb ab <> ppVType ty

ppAdj :: (Show a, HasSource a) => Adjustment a -> PP.Doc
ppAdj (ConsAdj x ts _) = ppItfInstance (x, ts)
ppAdj (AdaptorAdj adp _) = ppAdaptor adp

ppAb :: (Show a, HasSource a) => Ab a -> PP.Doc
ppAb (Ab v (ItfMap m _) _) | M.null m = text "[" <> ppAbMod v <> text "]"
ppAb (Ab v m _) =
  text "[" <> ppAbMod v <+> text "|" <+> ppItfMap m <> text "]"

ppAbMod :: (Show a, HasSource a) => AbMod a -> PP.Doc
ppAbMod (EmpAb _) = text "0"
ppAbMod (AbVar x _) = text x
ppAbMod (AbRVar x _) = if isDebugVerboseOn () then text x else text $ trimVar x
ppAbMod (AbFVar x _) = if isDebugVerboseOn () then text x else text $ trimVar x

ppItfMap :: (Show a, HasSource a) => ItfMap a -> PP.Doc
ppItfMap (ItfMap m _) =
  PP.hsep $ intersperse PP.comma $ map ppItfInstances $ M.toList m

ppItfInstances :: (Show a, HasSource a) => (Id, Bwd [TyArg a]) -> PP.Doc
ppItfInstances (x, instants) =
        PP.hsep $ intersperse PP.comma $ map (\args -> foldl (<+>) (text x) $ map ppTyArg args) (bwd2fwd instants)

ppItfInstance :: (Show a, HasSource a) => (Id, [TyArg a]) -> PP.Doc
ppItfInstance (x, ts) = text x <+> (PP.hsep $ map ppTyArg ts)

ppSource :: Source -> PP.Doc
ppSource (InCode (line, col)) = text "line" <+> text (show line) <+> text ", column" <+> text (show col)
ppSource BuiltIn = text "built-in"
ppSource Implicit = text "implicit"
ppSource (ImplicitNear (line, col)) = text "implicit near line" <+> text (show line) <+> text ", column" <+> text (show col)
ppSource Generated = text "generated"


ppSourceOf :: (HasSource a) => a -> PP.Doc
ppSourceOf x = ppSource (getSource x)

ppTm :: (Show a, HasSource a) => Tm a -> PP.Doc
ppTm (SC sc _) = ppSComp sc
ppTm (StrTm str _) = text "{" <+> text str <+> text "}"
ppTm (IntTm n _) = text (show n)
ppTm (CharTm c _) = text (show c)
ppTm (ListTm xs _) = text "[" <+> sep (map ppTm xs) <+> text "]"
ppTm (TmSeq t1 t2 _) = PP.parens $ ppTm t1 <+> text "; " <+> ppTm t2
ppTm (Use u _) = PP.parens $ ppUse u
ppTm (DCon dc _) = PP.parens $ ppDataCon dc

ppSComp :: (Show a, HasSource a) => SComp a -> PP.Doc
ppSComp (SComp cls _) = text "{" <+> sep (map (ppClause "") cls) <+> text "}"

ppUse :: (Show a, HasSource a) => Use a -> PP.Doc
ppUse (RawId x _) = text x
ppUse (RawComb u args _) = PP.lparen <> ppUse u <+> ppArgs args <> PP.rparen
ppUse (Op op _) = ppOperator op
ppUse (App u args _) = PP.lparen <> ppUse u <+> ppArgs args <> PP.rparen
ppUse (Adapted rs t _) =
  PP.parens $ text "<" <> ppAdaptors rs <> text ">" <+> ppUse t

-- TODO: LC: fix parenthesis output...
ppArgs :: (Show a, HasSource a) => [Tm a] -> PP.Doc
ppArgs [] = text "!"
ppArgs args = sep (map ppTm args)

ppOperator :: (Show a, HasSource a) => Operator a -> PP.Doc
ppOperator (Mono x _) = text x
ppOperator (Poly x _) = text x
ppOperator (VarId x _) = text x
ppOperator (CmdId x _) = text x

ppDataCon :: (Show a, HasSource a) => DataCon a -> PP.Doc
ppDataCon (DataCon x tms _) = text x <+> sep (map ppTm tms)

ppAdaptors :: (Show a, HasSource a) => [Adaptor a] -> PP.Doc
ppAdaptors rs = PP.hsep $ intersperse PP.comma $ map ppAdaptor rs

ppAdaptor :: (Show a, HasSource a) => Adaptor a -> PP.Doc
ppAdaptor (RawAdp x liat left right _) =
  text x <> text "(" <> text (show liat) <+> sep (punctuate (text " ") (map (text . show) left)) <+> text "->" <+> sep (punctuate (text " ") (map (text . show) right)) <> text ")"
ppAdaptor (Adp x mm ns _) =
  text x <> text "(" <> text (show mm) <> comma <+> sep (punctuate comma (map int ns)) <> text ")"
ppAdaptor (CompilableAdp x m ns _) =
  text x <> text "(" <> sep (punctuate comma (map int ns)) <> text ")(" <>
  int m <> text ")"

{- TypeCheckCommon pretty printers -}

ppContext :: Context -> PP.Doc
ppContext = ppFwd . (map ppEntry) . bwd2fwd

ppEntry :: Entry -> PP.Doc
ppEntry (FlexMVar x decl) = text "FlexMVar " <+> text x <+> text "\t=\t\t" <+> (ppDecl decl)
ppEntry (TermVar op ty)   = text "TermVar " <+> text (show op) <+> text "\t:=\t" <+> (ppVType ty)
ppEntry Mark              = text "<Mark>"

ppDecl :: Decl -> PP.Doc
ppDecl Hole        = text "?"
ppDecl (TyDefn ty) = text "val.ty. " <+> ppVType ty
ppDecl (AbDefn ab) = text "eff.ty. " <+> ppAb ab

ppSuffix :: Suffix -> PP.Doc
ppSuffix = ppFwd . (map (\(x, d) -> "(" ++ show x ++ "," ++
                                    show (ppDecl d) ++ ")"))

ppItfs :: [Id] -> PP.Doc
ppItfs p = PP.hsep $ intersperse PP.comma $ map text p

{- BWDFWD pretty printers -}

ppFwd :: Show a => [a] -> PP.Doc
ppFwd [] = text "[]"
ppFwd xs = text "[" $$
           sep (map ((nest 3) . text . show) xs) $$
           text "]"

ppBwd :: Show a => Bwd a -> PP.Doc
ppBwd = ppFwd . bwd2fwd

{- Shonky pretty printers -}

-- Pretty printing routines

ppProgShonky :: [Def Exp] -> PP.Doc
ppProgShonky xs = vcat (punctuate (text "\n") (map ppDef xs))

ppDef :: Def Exp -> PP.Doc
ppDef (id := e) = text id <+> text "->" <+> ppExp e
ppDef (DF id [] []) = error "ppDef invariant broken: empty Def Exp detected."
ppDef p@(DF id hss es) = header $+$ vcat cs
  where header = text id <> PP.parens (hsep portAnnots) <> colon
        portAnnots = punctuate comma $ map ppPort hss
        cs = punctuate comma $
               map (\x -> text id <> (nest 3 (ppClauseShonky ($$) x))) es
        ppPort :: ([Adap], [String]) -> PP.Doc
        ppPort (adps, cmds) = PP.parens ((hsep $ punctuate comma (map ppAdap adps))
                            <+> comma <+> (hsep $ punctuate comma (map text cmds)))
        ppAdap :: Adap -> PP.Doc
        ppAdap (cmds, r) = text "([" <> (hsep $ punctuate comma (map text cmds)) <> text "]" <+>
                           comma <+> ppRenaming r <+> text ")"
-- TODO: LC: refactor above pretty-printer

ppText :: (a -> PP.Doc) -> [Either Char a] -> PP.Doc
ppText f ((Left c) : xs) = (text $ escChar c) <> (ppText f xs)
ppText f ((Right x) : xs) = text "`" <> f x <> text "`" <> (ppText f xs)
ppText f [] = text "|]"

isEscChar :: Char -> Bool
isEscChar c = any (c ==) ['\n','\t','\b']

escChar :: Char -> String
escChar c = f [('\n', "\\n"),('\t', "\\t"),('\b', "\\b")]
  where f ((c',s):xs) = if c == c' then s else f xs
        f [] = [c]

ppClauseShonky :: (PP.Doc -> PP.Doc -> PP.Doc) -> ([Pat], Exp) -> PP.Doc
ppClauseShonky comb (ps, e) =
  let rhs = PP.parens (hsep $ punctuate comma (map ppPat ps))
      lhs = ppExp e in
  rhs <+> text "->" `comb` lhs

ppExp :: Exp -> PP.Doc
ppExp (EV x) = text x
ppExp (EI n) = int n
ppExp (EA x) = text $ "'" ++ x
ppExp (e :& e') | isListExp e = text "[" <> ppListExp e'
ppExp p@(_ :& _) = text "[" <> ppExp' p
ppExp (f :$ xs) = let args = hcat $ punctuate comma (map ppExp xs) in
  ppExp f <> text "(" <> args <> text ")"
ppExp (e :! e') = ppExp e <> semi <> ppExp e'
ppExp (e :// e') = ppExp e <> text "/" <> ppExp e'
ppExp (EF xs ys) =
-- TODO: LC: Print xs
  let clauses = map (ppClauseShonky (<+>)) ys in
  PP.braces $ hcat (punctuate comma clauses)
ppExp (EX xs) = text "[|" <> ppText ppExp xs
ppExp (ER (cs, r) e) = text "<(" <+> (hcat $ punctuate comma (map text cs))
                    <> text ")" <+> ppRenaming r <> text ">"
                    <+> PP.parens (ppExp e)

ppExp' :: Exp -> PP.Doc
ppExp' (e :& EA "") = ppExp e <> rbrack
ppExp' (e :& es) = ppExp e <> comma <> ppExp' es
ppExp' e = ppExp e

isListExp :: Exp -> Bool
isListExp (e :& _) = isListExp e
isListExp _ = False

-- Special case for lists
ppListExp :: Exp -> PP.Doc
ppListExp (e :& EA "") = ppExp e <> text "]"
ppListExp (e :& es) = ppExp e <> text "|" <> ppListExp es
ppListExp (EA "") = text "]"
ppListExp _ = text "ppListExp: invariant broken"

ppPat :: Pat -> PP.Doc
ppPat (PV x) = ppVPat x
ppPat (PT x) = PP.braces $ text x
ppPat (PC cmd n ps k) = let args = hcat $ punctuate comma (map ppVPat ps) in
  let cmdtxt = text (cmd ++ ".") <> int n in
  PP.braces $ text "'" <> cmdtxt <> PP.parens args <+> text "->" <+> text k

ppVPat :: VPat -> PP.Doc
ppVPat (VPV x) = text x
ppVPat (VPI n) = int n
ppVPat (VPA x) = text $ "'" ++ x
ppVPat (VPX xs) = text "[|" <> ppText ppVPat xs
ppVPat (v1 :&: v2 :&: v3) = ppVPat (v1 :&: (v2 :&: v3))
ppVPat (v :&: v') | isListPat v = lbrack <> ppVPatList v'
ppVPat p@(_ :&: _) = lbrack <> ppVPat' p

ppVPatList :: VPat -> PP.Doc
ppVPatList (v :&: VPA "") = ppVPat v <> rbrack
ppVPatList (v :&: vs) = ppVPat v <> text "|" <> ppVPatList vs
ppVPatList (VPA "") = lbrack
ppVPatList _ = error "ppVPatList: broken invariant"

ppVPat' :: VPat -> PP.Doc
ppVPat' (v :&: VPA "") = ppVPat v <> text "]"
ppVPat' (v :&: vs) = ppVPat v <> comma <> ppVPat' vs
ppVPat' v = ppVPat v

isListPat :: VPat -> Bool
isListPat (v :&: _) = isListPat v
isListPat _ = False