Debug.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}

module Debug where

import BwdFwd
import Syntax
import ParserCommon
import TypeCheckCommon

import qualified Data.Map.Strict as M
import Data.List

import Debug.Trace

import Data.IORef
import System.IO.Unsafe

import qualified Text.PrettyPrint as PP

-- Set by the main entry point if relevant flag detected.
-- 1) debugVerboseOn
-- 2) debugParserOn
-- 3) debugTypeCheckOn
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)

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

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

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

ifDebugParserOnThen :: MonadicParsing m => m () -> m ()
ifDebugParserOnThen f = if debugParserOn () then f else return ()

ifDebugTypeCheckOnThen :: Contextual () -> Contextual ()
ifDebugTypeCheckOnThen f = if debugTypeCheckOn () then f else return ()

{- 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 $ ppHasSource dt) ++ ")"

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

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

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

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

errorRefEffVarNoParams :: Id -> [TyArg Raw] -> String
errorRefEffVarNoParams x tyArgs = "effect variable " ++ x ++ " may not take parameters"

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

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

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

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

errorRefNumberOfArguments :: Id -> Int -> Int -> Raw -> String
errorRefNumberOfArguments x exp act a = x ++ " expects " ++ show exp ++ " argument(s) but " ++ show act ++ " given (" ++ (show $ ppHasSource 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 $ ppHasSource op) ++ ")"

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

errorTCCmdNotFoundInAdj :: Id -> Adj Desugared -> String
errorTCCmdNotFoundInAdj cmd adj = "command " ++ cmd ++ " not found in adjustment " ++ (show $ ppAdj adj) ++ " (" ++ (show $ ppHasSource adj) ++ ")"

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 $ ppHasSource v1) ++ ") with " ++ (show $ ppVType v2) ++ " (" ++ (show $ ppHasSource 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 $ ppHasSource t1) ++ ") with " ++ (show $ ppVType t2) ++ " (" ++ (show $ ppHasSource t2) ++ ")"

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

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

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

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 $ ppHasSource 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 ++ "\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 (Op x _) = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "begin infer use of single: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show x ++ "\n\n"
  ctx <- getContext
  debugTypeCheckM ("cur. context is:\n" ++ (show $ ppContext ctx) ++ "\n\n")
logBeginInferUse (App f xs _) = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "begin infer use of app: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show f ++ " " ++ show xs ++ "\n\n"

logEndInferUse :: Use Desugared -> VType Desugared -> Contextual ()
logEndInferUse (Op x _) ty = ifDebugTypeCheckOnThen $ do
  amb <- getAmbient
  debugTypeCheckM $ "ended infer use of single: Under curr. amb. " ++ show (ppAb amb) ++ "\n   infer type of " ++ show x ++ "\n   gives " ++ show (ppVType ty)
  ctx <- getContext
  debugTypeCheckM ("cur. context is:\n" ++ (show $ ppContext ctx) ++ "\n\n")
logEndInferUse (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 f ++ " " ++ show xs ++ "\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"

-- 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 = ifDebugTypeCheckOnThen $ do
  cxt <- getContext
  seq (ppContext cxt) traceM str

debugParserM :: (MonadicParsing m) => String -> m ()
debugParserM str = ifDebugParserOnThen $ do
  traceM str

{- Syntax pretty printers -}

(<+>) = (PP.<+>)
(<>) = (PP.<>)
($$) = (PP.$$)
text = PP.text
sep = PP.sep
nest = PP.nest
vcat = PP.vcat

type Doc = PP.Doc

ppProg :: (Show a, HasSource a) => Prog a -> Doc
ppProg (MkProg tts) = vcat (map ((text "" $$) . ppTopTm) tts)

ppTopTm :: (Show a, HasSource a) => TopTm a -> Doc
ppTopTm (DataTm dt _) = ppDataT dt
ppTopTm (ItfTm itf _) = text $ show 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 -> Doc
ppDataT (DT id tyVars ctrs a) = text "data" <+>
                              text id <+>
                              sep (map (text . show) tyVars) <+>
                              text "=" <+>
                              sep (map (text . show) ctrs)

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

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

ppPattern :: (Show a, HasSource a) => Pattern a -> Doc
ppPattern = text . show

ppCType :: (Show a, HasSource a) => CType a -> 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 -> 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 debugVerboseOn () then text x else text $ trimVar x
ppVType (FTVar x _) = if debugVerboseOn () 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 -> Doc
ppTyArg (VArg t _) = ppParenVType t
ppTyArg (EArg ab _) = ppAb ab

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

ppPort :: (Show a, HasSource a) => Port a -> Doc
ppPort (Port adj ty _) = ppAdj adj <> ppVType ty

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

ppAdj :: (Show a, HasSource a) => Adj a -> Doc
ppAdj (Adj (ItfMap m _) _) | M.null m = PP.empty
ppAdj (Adj m _) = text "<" <> ppItfMap m <> text ">"

ppAb :: (Show a, HasSource a) => Ab a -> 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 -> Doc
ppAbMod (EmpAb _) = text "0"
ppAbMod (AbVar x _) = text x
ppAbMod (AbRVar x _) = if debugVerboseOn () then text x else text $ trimVar x
ppAbMod (AbFVar x _) = if debugVerboseOn () then text x else text $ trimVar x

ppItfMap :: (Show a, HasSource a) => ItfMap a -> Doc
ppItfMap (ItfMap m _) = PP.hsep $ intersperse PP.comma $ map ppItfMapPair $ M.toList m
 where ppItfMapPair :: (Show a, HasSource a) => (Id, [TyArg a]) -> Doc
       ppItfMapPair (x, args) =
         text x <+> (foldl (<+>) PP.empty $ map ppTyArg args)

ppSource :: Source -> 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"


ppHasSource :: (HasSource a) => a -> Doc
ppHasSource x = ppSource (getSource x)

{- TypeCheckCommon pretty printers -}

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

ppEntry :: Entry -> 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 -> Doc
ppDecl Hole        = text "?"
ppDecl (TyDefn ty) = text "val.ty. " <+> ppVType ty
ppDecl (AbDefn ab) = text "eff.ty. " <+> ppAb ab

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

{- BwdFwd pretty printers -}

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

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