{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE TypeSynonymInstances       #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PartialTypeSignatures      #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE ViewPatterns               #-}

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wwarn=deprecations #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

module Language.Haskell.Liquid.GHC.Interface (

  -- * Printer
    pprintCBs

  -- * predicates
  -- , isExportedVar
  -- , exportedVars

  -- * Internal exports (provisional)
  , extractSpecComments
  , listLMap
  , classCons
  , derivedVars
  , importVars
  , modSummaryHsFile
  , makeFamInstEnv
  , clearSpec
  , checkFilePragmas
  , lookupTyThing
  , updLiftedSpec
  ) where

import Prelude hiding (error)

import           Liquid.GHC.API as Ghc hiding ( text
                                                               , (<+>)
                                                               , panic
                                                               , vcat
                                                               , showPpr
                                                               , mkStableModule
                                                               , Located
                                                               )
import qualified Liquid.GHC.API as Ghc

import Control.Exception
import Control.Monad
import Control.Monad.Trans.Maybe

import Data.List hiding (intersperse)
import Data.Maybe

import qualified Data.HashSet        as S

import Text.PrettyPrint.HughesPJ        hiding (first, (<>))
import Language.Fixpoint.Types          hiding (err, panic, Error, Result, Expr)
import qualified Language.Fixpoint.Misc as Misc
import Language.Haskell.Liquid.GHC.Misc
import Language.Haskell.Liquid.GHC.Types (MGIModGuts(..))
import Language.Haskell.Liquid.GHC.Play
import Language.Haskell.Liquid.WiredIn (isDerivedInstance)
import qualified Language.Haskell.Liquid.Measure  as Ms
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.PrettyPrint
import Language.Haskell.Liquid.Types.Specs
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.Visitors
import Language.Haskell.Liquid.UX.Config
import Language.Haskell.Liquid.UX.Tidy


--------------------------------------------------------------------------------
-- | Extract Ids ---------------------------------------------------------------
--------------------------------------------------------------------------------

classCons :: Maybe [ClsInst] -> [Id]
classCons :: Maybe [ClsInst] -> [DFunId]
classCons Maybe [ClsInst]
Nothing   = []
classCons (Just [ClsInst]
cs) = (ClsInst -> [DFunId]) -> [ClsInst] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DataCon -> [DFunId]
dataConImplicitIds (DataCon -> [DFunId])
-> (ClsInst -> DataCon) -> ClsInst -> [DFunId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataCon] -> DataCon
forall a. (?callStack::CallStack) => [a] -> a
head ([DataCon] -> DataCon)
-> (ClsInst -> [DataCon]) -> ClsInst -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
tyConDataCons (TyCon -> [DataCon]) -> (ClsInst -> TyCon) -> ClsInst -> [DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> TyCon
classTyCon (Class -> TyCon) -> (ClsInst -> Class) -> ClsInst -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Class
is_cls) [ClsInst]
cs

derivedVars :: Config -> MGIModGuts -> [Var]
derivedVars :: Config -> MGIModGuts -> [DFunId]
derivedVars Config
cfg MGIModGuts
mg  = (ClsInst -> [DFunId]) -> [ClsInst] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([CoreBind] -> DFunId -> [DFunId]
dFunIdVars [CoreBind]
cbs (DFunId -> [DFunId]) -> (ClsInst -> DFunId) -> ClsInst -> [DFunId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> DFunId
is_dfun) [ClsInst]
derInsts
  where
    derInsts :: [ClsInst]
derInsts
      | Bool
checkDer    = [ClsInst]
insts
      | Bool
otherwise   = (ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> Bool) -> [a] -> [a]
filter ClsInst -> Bool
isDerivedInstance [ClsInst]
insts
    insts :: [ClsInst]
insts           = MGIModGuts -> [ClsInst]
mgClsInstances MGIModGuts
mg
    checkDer :: Bool
checkDer        = Config -> Bool
checkDerived Config
cfg
    cbs :: [CoreBind]
cbs             = MGIModGuts -> [CoreBind]
mgi_binds MGIModGuts
mg


mgClsInstances :: MGIModGuts -> [ClsInst]
mgClsInstances :: MGIModGuts -> [ClsInst]
mgClsInstances = [ClsInst] -> Maybe [ClsInst] -> [ClsInst]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [ClsInst] -> [ClsInst])
-> (MGIModGuts -> Maybe [ClsInst]) -> MGIModGuts -> [ClsInst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MGIModGuts -> Maybe [ClsInst]
mgi_cls_inst

dFunIdVars :: CoreProgram -> DFunId -> [Id]
dFunIdVars :: [CoreBind] -> DFunId -> [DFunId]
dFunIdVars [CoreBind]
cbs DFunId
fd  = [Char] -> [DFunId] -> [DFunId]
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
msg ([DFunId] -> [DFunId]) -> [DFunId] -> [DFunId]
forall a b. (a -> b) -> a -> b
$ (CoreBind -> [DFunId]) -> [CoreBind] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [DFunId]
forall b. Bind b -> [b]
bindersOf [CoreBind]
cbs' [DFunId] -> [DFunId] -> [DFunId]
forall a. [a] -> [a] -> [a]
++ [DFunId]
deps
  where
    msg :: [Char]
msg            = [Char]
"DERIVED-VARS-OF: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DFunId -> [Char]
forall a. PPrint a => a -> [Char]
showpp DFunId
fd
    cbs' :: [CoreBind]
cbs'           = (CoreBind -> Bool) -> [CoreBind] -> [CoreBind]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreBind -> Bool
f [CoreBind]
cbs
    f :: CoreBind -> Bool
f (NonRec DFunId
x CoreExpr
_) = DFunId -> Bool
eqFd DFunId
x
    f (Rec [(DFunId, CoreExpr)]
xes)    = (DFunId -> Bool) -> [DFunId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DFunId -> Bool
eqFd ((DFunId, CoreExpr) -> DFunId
forall a b. (a, b) -> a
fst ((DFunId, CoreExpr) -> DFunId) -> [(DFunId, CoreExpr)] -> [DFunId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(DFunId, CoreExpr)]
xes)
    eqFd :: DFunId -> Bool
eqFd DFunId
x         = DFunId -> Name
varName DFunId
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== DFunId -> Name
varName DFunId
fd
    deps :: [DFunId]
deps           = (Unfolding -> [DFunId]) -> [Unfolding] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Unfolding -> [DFunId]
unfoldDep [Unfolding]
unfolds
    unfolds :: [Unfolding]
unfolds        = IdInfo -> Unfolding
realUnfoldingInfo (IdInfo -> Unfolding) -> (DFunId -> IdInfo) -> DFunId -> Unfolding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => DFunId -> IdInfo
DFunId -> IdInfo
idInfo (DFunId -> Unfolding) -> [DFunId] -> [Unfolding]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CoreBind -> [DFunId]) -> [CoreBind] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [DFunId]
forall b. Bind b -> [b]
bindersOf [CoreBind]
cbs'

unfoldDep :: Unfolding -> [Id]
unfoldDep :: Unfolding -> [DFunId]
unfoldDep (DFunUnfolding [DFunId]
_ DataCon
_ [CoreExpr]
e)       = (CoreExpr -> [DFunId]) -> [CoreExpr] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreExpr -> [DFunId]
exprDep [CoreExpr]
e
unfoldDep CoreUnfolding {uf_tmpl :: Unfolding -> CoreExpr
uf_tmpl = CoreExpr
e} = CoreExpr -> [DFunId]
exprDep CoreExpr
e
unfoldDep Unfolding
_                           = []

exprDep :: CoreExpr -> [Id]
exprDep :: CoreExpr -> [DFunId]
exprDep = HashSet DFunId -> CoreExpr -> [DFunId]
forall a. CBVisitable a => HashSet DFunId -> a -> [DFunId]
freeVars HashSet DFunId
forall a. HashSet a
S.empty

importVars :: CoreProgram -> [Id]
importVars :: [CoreBind] -> [DFunId]
importVars = HashSet DFunId -> [CoreBind] -> [DFunId]
forall a. CBVisitable a => HashSet DFunId -> a -> [DFunId]
freeVars HashSet DFunId
forall a. HashSet a
S.empty

_definedVars :: CoreProgram -> [Id]
_definedVars :: [CoreBind] -> [DFunId]
_definedVars = (CoreBind -> [DFunId]) -> [CoreBind] -> [DFunId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [DFunId]
forall b. Bind b -> [b]
defs
  where
    defs :: Bind a -> [a]
defs (NonRec a
x Expr a
_) = [a
x]
    defs (Rec [(a, Expr a)]
xes)    = ((a, Expr a) -> a) -> [(a, Expr a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Expr a) -> a
forall a b. (a, b) -> a
fst [(a, Expr a)]
xes

--------------------------------------------------------------------------------
-- | Per-Module Pipeline -------------------------------------------------------
--------------------------------------------------------------------------------

updLiftedSpec :: Ms.BareSpec -> Maybe Ms.BareSpec -> Ms.BareSpec
updLiftedSpec :: BareSpec -> Maybe BareSpec -> BareSpec
updLiftedSpec BareSpec
s1 Maybe BareSpec
Nothing   = BareSpec
s1
updLiftedSpec BareSpec
s1 (Just BareSpec
s2) = BareSpec -> BareSpec
clearSpec BareSpec
s1 BareSpec -> BareSpec -> BareSpec
forall a. Monoid a => a -> a -> a
`mappend` BareSpec
s2

clearSpec :: Ms.BareSpec -> Ms.BareSpec
clearSpec :: BareSpec -> BareSpec
clearSpec BareSpec
s = BareSpec
s { sigs = [], asmSigs = [], aliases = [], ealiases = [], qualifiers = [], dataDecls = [] }

lookupTyThing :: (GhcMonad m) => Ghc.TypeEnv -> Name -> m (Maybe TyThing)
lookupTyThing :: forall (m :: * -> *).
GhcMonad m =>
TypeEnv -> Name -> m (Maybe TyThing)
lookupTyThing TypeEnv
tyEnv Name
name = do
    MaybeT m TyThing -> m (Maybe TyThing)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m TyThing -> m (Maybe TyThing))
-> ([m (Maybe TyThing)] -> MaybeT m TyThing)
-> [m (Maybe TyThing)]
-> m (Maybe TyThing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MaybeT m TyThing] -> MaybeT m TyThing
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([MaybeT m TyThing] -> MaybeT m TyThing)
-> ([m (Maybe TyThing)] -> [MaybeT m TyThing])
-> [m (Maybe TyThing)]
-> MaybeT m TyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (Maybe TyThing) -> MaybeT m TyThing)
-> [m (Maybe TyThing)] -> [MaybeT m TyThing]
forall a b. (a -> b) -> [a] -> [b]
map m (Maybe TyThing) -> MaybeT m TyThing
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT ([m (Maybe TyThing)] -> m (Maybe TyThing))
-> [m (Maybe TyThing)] -> m (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$
        [ Maybe TyThing -> m (Maybe TyThing)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeEnv -> Name -> Maybe TyThing
lookupTypeEnv TypeEnv
tyEnv Name
name)
        , Name -> m (Maybe TyThing)
forall (m :: * -> *). GhcMonad m => Name -> m (Maybe TyThing)
lookupName Name
name
        ]

_dumpTypeEnv :: TypecheckedModule -> IO ()
_dumpTypeEnv :: TypecheckedModule -> IO ()
_dumpTypeEnv TypecheckedModule
tm = do
  [Char] -> IO ()
forall a. Show a => a -> IO ()
print ([Char]
"DUMP-TYPE-ENV" :: String)
  Maybe [Char] -> IO ()
forall a. Show a => a -> IO ()
print ([Name] -> [Char]
forall a. PPrint a => a -> [Char]
showpp ([Name] -> [Char]) -> Maybe [Name] -> Maybe [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypecheckedModule -> Maybe [Name]
tcmTyThings TypecheckedModule
tm)

tcmTyThings :: TypecheckedModule -> Maybe [Name]
tcmTyThings :: TypecheckedModule -> Maybe [Name]
tcmTyThings
  =
  -- typeEnvElts
  -- . tcg_type_env . fst
  -- . md_types . snd
  -- . tm_internals_
  ModuleInfo -> Maybe [Name]
modInfoTopLevelScope
  (ModuleInfo -> Maybe [Name])
-> (TypecheckedModule -> ModuleInfo)
-> TypecheckedModule
-> Maybe [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypecheckedModule -> ModuleInfo
tm_checked_module_info

modSummaryHsFile :: ModSummary -> FilePath
modSummaryHsFile :: ModSummary -> [Char]
modSummaryHsFile ModSummary
modSummary =
  [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe
    (Maybe SrcSpan -> [Char] -> [Char]
forall a. (?callStack::CallStack) => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$
      [Char]
"modSummaryHsFile: missing .hs file for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
      Module -> [Char]
forall a. Outputable a => a -> [Char]
showPpr (ModSummary -> Module
ms_mod ModSummary
modSummary))
    (ModLocation -> Maybe [Char]
ml_hs_file (ModLocation -> Maybe [Char]) -> ModLocation -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ ModSummary -> ModLocation
ms_location ModSummary
modSummary)

checkFilePragmas :: [Located String] -> IO ()
checkFilePragmas :: [Located [Char]] -> IO ()
checkFilePragmas = IO () -> ([Error] -> IO ()) -> [Error] -> IO ()
forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) [Error] -> IO ()
forall a e. (?callStack::CallStack, Exception e) => e -> a
throw ([Error] -> IO ())
-> ([Located [Char]] -> [Error]) -> [Located [Char]] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located [Char] -> Maybe Error) -> [Located [Char]] -> [Error]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Located [Char] -> Maybe Error
err
  where
    err :: Located [Char] -> Maybe Error
err Located [Char]
pragma
      | [Char] -> Bool
check (Located [Char] -> [Char]
forall a. Located a -> a
val Located [Char]
pragma) = Error -> Maybe Error
forall a. a -> Maybe a
Just (SrcSpan -> Error
forall t. SrcSpan -> TError t
ErrFilePragma (SrcSpan -> Error) -> SrcSpan -> Error
forall a b. (a -> b) -> a -> b
$ Located [Char] -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located [Char]
pragma :: Error)
      | Bool
otherwise          = Maybe Error
forall a. Maybe a
Nothing
    check :: [Char] -> Bool
check [Char]
pragma           = ([Char] -> Bool) -> [[Char]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
pragma) [[Char]]
forall {a}. IsString a => [a]
bad
    bad :: [a]
bad =
      [ a
"-i", a
"--idirs"
      , a
"-g", a
"--ghc-option"
      , a
"--c-files", a
"--cfiles"
      ]

--------------------------------------------------------------------------------
-- | Family instance information
--------------------------------------------------------------------------------
makeFamInstEnv :: [FamInst] -> ([Ghc.TyCon], [(Symbol, DataCon)])
makeFamInstEnv :: [FamInst] -> ([TyCon], [(Symbol, DataCon)])
makeFamInstEnv [FamInst]
famInsts =
  let fiTcs :: [TyCon]
fiTcs = [ TyCon
tc            | FamInst { fi_flavor :: FamInst -> FamFlavor
fi_flavor = DataFamilyInst TyCon
tc } <- [FamInst]
famInsts ]
      fiDcs :: [(Symbol, DataCon)]
fiDcs = [ (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCon
d, DataCon
d) | TyCon
tc <- [TyCon]
fiTcs, DataCon
d <- TyCon -> [DataCon]
tyConDataCons TyCon
tc ]
  in ([TyCon]
fiTcs, [(Symbol, DataCon)]
fiDcs)

--------------------------------------------------------------------------------
-- | Extract Specifications from GHC -------------------------------------------
--------------------------------------------------------------------------------
extractSpecComments :: HsParsedModule -> [(Maybe RealSrcLoc, String)]
extractSpecComments :: HsParsedModule -> [(Maybe RealSrcLoc, [Char])]
extractSpecComments = (Located ApiComment -> Maybe (Maybe RealSrcLoc, [Char]))
-> [Located ApiComment] -> [(Maybe RealSrcLoc, [Char])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Located ApiComment -> Maybe (Maybe RealSrcLoc, [Char])
extractSpecComment ([Located ApiComment] -> [(Maybe RealSrcLoc, [Char])])
-> (HsParsedModule -> [Located ApiComment])
-> HsParsedModule
-> [(Maybe RealSrcLoc, [Char])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsParsedModule -> [Located ApiComment]
apiComments

-- | 'extractSpecComment' pulls out the specification part from a full comment
--   string, i.e. if the string is of the form:
--   1. '{-@ S @-}' then it returns the substring 'S',
--   2. '{-@ ... -}' then it throws a malformed SPECIFICATION ERROR, and
--   3. Otherwise it is just treated as a plain comment so we return Nothing.

extractSpecComment :: Ghc.Located ApiComment -> Maybe (Maybe RealSrcLoc, String)
extractSpecComment :: Located ApiComment -> Maybe (Maybe RealSrcLoc, [Char])
extractSpecComment (Ghc.L SrcSpan
sp (ApiBlockComment [Char]
txt))
  | [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Char]
"{-@" [Char]
txt Bool -> Bool -> Bool
&& [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf [Char]
"@-}" [Char]
txt          -- valid   specification
  = (Maybe RealSrcLoc, [Char]) -> Maybe (Maybe RealSrcLoc, [Char])
forall a. a -> Maybe a
Just (Maybe RealSrcLoc
offsetPos, Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
txt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
6) ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
3 [Char]
txt)
  | [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Char]
"{-@" [Char]
txt                                   -- invalid specification
  = UserError -> Maybe (Maybe RealSrcLoc, [Char])
forall a. UserError -> a
uError (UserError -> Maybe (Maybe RealSrcLoc, [Char]))
-> UserError -> Maybe (Maybe RealSrcLoc, [Char])
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrParseAnn SrcSpan
sp Doc
"A valid specification must have a closing '@-}'."
  where
    offsetPos :: Maybe RealSrcLoc
offsetPos = RealSrcLoc -> RealSrcLoc
offsetRealSrcLoc (RealSrcLoc -> RealSrcLoc)
-> (RealSrcSpan -> RealSrcLoc) -> RealSrcSpan -> RealSrcLoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RealSrcSpan -> RealSrcLoc
realSrcSpanStart (RealSrcSpan -> RealSrcLoc)
-> Maybe RealSrcSpan -> Maybe RealSrcLoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Maybe RealSrcSpan
srcSpanToRealSrcSpan SrcSpan
sp
    offsetRealSrcLoc :: RealSrcLoc -> RealSrcLoc
offsetRealSrcLoc RealSrcLoc
s =
      FastString -> Int -> Int -> RealSrcLoc
mkRealSrcLoc (RealSrcLoc -> FastString
srcLocFile RealSrcLoc
s) (RealSrcLoc -> Int
srcLocLine RealSrcLoc
s) (RealSrcLoc -> Int
srcLocCol RealSrcLoc
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
3)

extractSpecComment Located ApiComment
_ = Maybe (Maybe RealSrcLoc, [Char])
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- Information for Spec Extraction ---------------------------------------------
--------------------------------------------------------------------------------

listLMap :: LogicMap -- TODO-REBARE: move to wiredIn
listLMap :: LogicMap
listLMap  = [(LocSymbol, ([Symbol], ExprV Symbol))] -> LogicMap
toLogicMap [ (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
nilName , ([]     , ExprV Symbol
hNil))
                       , (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc Symbol
consName, ([Symbol
forall {a}. IsString a => a
x, Symbol
forall {a}. IsString a => a
xs], [ExprV Symbol] -> ExprV Symbol
hCons (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol
forall {a}. IsString a => a
x, Symbol
forall {a}. IsString a => a
xs]))) ]
  where
    x :: a
x     = a
"x"
    xs :: a
xs    = a
"xs"
    hNil :: ExprV Symbol
hNil  = LocSymbol -> [ExprV Symbol] -> ExprV Symbol
mkEApp (DataCon -> LocSymbol
forall {a}. Symbolic a => a -> LocSymbol
dcSym DataCon
Ghc.nilDataCon ) []
    hCons :: [ExprV Symbol] -> ExprV Symbol
hCons = LocSymbol -> [ExprV Symbol] -> ExprV Symbol
mkEApp (DataCon -> LocSymbol
forall {a}. Symbolic a => a -> LocSymbol
dcSym DataCon
Ghc.consDataCon)
    dcSym :: a -> LocSymbol
dcSym = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> (a -> Symbol) -> a -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleUnique (Symbol -> Symbol) -> (a -> Symbol) -> a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol



--------------------------------------------------------------------------------
-- | Pretty Printing -----------------------------------------------------------
--------------------------------------------------------------------------------

instance PPrint TargetSpec where
  pprintTidy :: Tidy -> TargetSpec -> Doc
pprintTidy Tidy
k TargetSpec
spec = [Doc] -> Doc
vcat
    [ Doc
"******* Target Variables ********************"
    , Tidy -> [DFunId] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ([DFunId] -> Doc) -> [DFunId] -> Doc
forall a b. (a -> b) -> a -> b
$ GhcSpecVars -> [DFunId]
gsTgtVars (TargetSpec -> GhcSpecVars
gsVars TargetSpec
spec)
    , Doc
"******* Type Signatures *********************"
    , Tidy -> [(DFunId, LocSpecType)] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecSig -> [(DFunId, LocSpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
spec))
    , Doc
"******* Assumed Type Signatures *************"
    , Tidy -> [(DFunId, LocSpecType)] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecSig -> [(DFunId, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
spec))
    , Doc
"******* DataCon Specifications (Measure) ****"
    , Tidy -> [(DFunId, LocSpecType)] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecData -> [(DFunId, LocSpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
spec))
    , Doc
"******* Measure Specifications **************"
    , Tidy -> [(Symbol, LocSpecType)] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (TargetSpec -> GhcSpecData
gsData TargetSpec
spec))       ]

instance PPrint TargetInfo where
  pprintTidy :: Tidy -> TargetInfo -> Doc
pprintTidy Tidy
k TargetInfo
info = [Doc] -> Doc
vcat
    [ -- "*************** Imports *********************"
      -- , intersperse comma $ text <$> imports info
      -- , "*************** Includes ********************"
      -- , intersperse comma $ text <$> includes info
      Doc
"*************** Imported Variables **********"
    , [DFunId] -> Doc
forall a. Outputable a => a -> Doc
pprDoc ([DFunId] -> Doc) -> [DFunId] -> Doc
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [DFunId]
_giImpVars (TargetSrc -> GhcSrc
fromTargetSrc (TargetSrc -> GhcSrc) -> TargetSrc -> GhcSrc
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    , Doc
"*************** Defined Variables ***********"
    , [DFunId] -> Doc
forall a. Outputable a => a -> Doc
pprDoc ([DFunId] -> Doc) -> [DFunId] -> Doc
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [DFunId]
_giDefVars (TargetSrc -> GhcSrc
fromTargetSrc (TargetSrc -> GhcSrc) -> TargetSrc -> GhcSrc
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    , Doc
"*************** Specification ***************"
    , Tidy -> TargetSpec -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (TargetSpec -> Doc) -> TargetSpec -> Doc
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info
    , Doc
"*************** Core Bindings ***************"
    , [CoreBind] -> Doc
pprintCBs ([CoreBind] -> Doc) -> [CoreBind] -> Doc
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [CoreBind]
_giCbs (TargetSrc -> GhcSrc
fromTargetSrc (TargetSrc -> GhcSrc) -> TargetSrc -> GhcSrc
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info) ]

pprintCBs :: [CoreBind] -> Doc
pprintCBs :: [CoreBind] -> Doc
pprintCBs = [CoreBind] -> Doc
forall a. Outputable a => a -> Doc
pprDoc ([CoreBind] -> Doc)
-> ([CoreBind] -> [CoreBind]) -> [CoreBind] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CoreBind] -> [CoreBind]
tidyCBs
    -- To print verbosely
    --    = text . O.showSDocDebug unsafeGlobalDynFlags . O.ppr . tidyCBs

instance Show TargetInfo where
  show :: TargetInfo -> [Char]
show = TargetInfo -> [Char]
forall a. PPrint a => a -> [Char]
showpp

------------------------------------------------------------------------
-- Dealing with Errors ---------------------------------------------------
------------------------------------------------------------------------

instance Result SourceError where
  result :: SourceError -> FixResult UserError
result SourceError
e = [(UserError, Maybe [Char])] -> [Char] -> FixResult UserError
forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash ((, Maybe [Char]
forall a. Maybe a
Nothing) (UserError -> (UserError, Maybe [Char]))
-> [UserError] -> [(UserError, Maybe [Char])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> SourceError -> [UserError]
forall t. [Char] -> SourceError -> [TError t]
sourceErrors [Char]
"" SourceError
e) [Char]
"Invalid Source"