{-# 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 #-}

module Language.Haskell.Liquid.GHC.Interface (

  -- * Printer
    pprintCBs

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

  -- * Internal exports (provisional)
  , extractSpecComments
  , extractSpecQuotes'
  , makeLogicMap
  , classCons
  , derivedVars
  , importVars
  , allImports
  , qualifiedImports
  , modSummaryHsFile
  , makeFamInstEnv
  , parseSpecFile
  , clearSpec
  , checkFilePragmas
  , keepRawTokenStream
  , ignoreInline
  , lookupTyThings
  , availableTyCons
  , availableVars
  , 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.Data
import Data.List hiding (intersperse)
import Data.Maybe

import Data.Generics.Aliases (mkT)
import Data.Generics.Schemes (everywhere)

import qualified Data.HashSet        as S

import System.IO
import Text.Megaparsec.Error
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 qualified Language.Haskell.Liquid.Misc     as Misc
import Language.Haskell.Liquid.Parse
import Language.Haskell.Liquid.Types hiding (Spec)
-- import Language.Haskell.Liquid.Types.PrettyPrint
-- import Language.Haskell.Liquid.Types.Visitors
import Language.Haskell.Liquid.UX.QuasiQuoter
import Language.Haskell.Liquid.UX.Tidy

import qualified Debug.Trace as Debug


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

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

derivedVars :: Config -> MGIModGuts -> [Var]
derivedVars :: Config -> MGIModGuts -> [Var]
derivedVars Config
cfg MGIModGuts
mg  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([CoreBind] -> Var -> [Var]
dFunIdVars [CoreBind]
cbs forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Var
is_dfun) [ClsInst]
derInsts
  where
    derInsts :: [ClsInst]
derInsts
      | Bool
checkDer    = [ClsInst]
insts
      | Bool
otherwise   = 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 = forall a. a -> Maybe a -> a
fromMaybe [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. MGIModGuts -> Maybe [ClsInst]
mgi_cls_inst

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

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

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

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

_definedVars :: CoreProgram -> [Id]
_definedVars :: [CoreBind] -> [Var]
_definedVars = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 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)    = forall a b. (a -> b) -> [a] -> [b]
map 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 forall a. Monoid a => a -> a -> a
`mappend` BareSpec
s2

clearSpec :: Ms.BareSpec -> Ms.BareSpec
clearSpec :: BareSpec -> BareSpec
clearSpec BareSpec
s = BareSpec
s { sigs :: [(Located Symbol, Located BareType)]
sigs = [], asmSigs :: [(Located Symbol, Located BareType)]
asmSigs = [], aliases :: [Located (RTAlias Symbol BareType)]
aliases = [], ealiases :: [Located (RTAlias Symbol Expr)]
ealiases = [], qualifiers :: [Qualifier]
qualifiers = [], dataDecls :: [DataDecl]
dataDecls = [] }

keepRawTokenStream :: ModSummary -> ModSummary
keepRawTokenStream :: ModSummary -> ModSummary
keepRawTokenStream ModSummary
modSummary = ModSummary
modSummary
  { ms_hspp_opts :: DynFlags
ms_hspp_opts = ModSummary -> DynFlags
ms_hspp_opts ModSummary
modSummary DynFlags -> GeneralFlag -> DynFlags
`gopt_set` GeneralFlag
Opt_KeepRawTokenStream }

_impThings :: [Var] -> [TyThing] -> [TyThing]
_impThings :: [Var] -> [TyThing] -> [TyThing]
_impThings [Var]
vars  = forall a. (a -> Bool) -> [a] -> [a]
filter TyThing -> Bool
ok
  where
    vs :: HashSet Var
vs          = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Var]
vars
    ok :: TyThing -> Bool
ok (AnId Var
x) = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x HashSet Var
vs
    ok TyThing
_        = Bool
True

allImports :: [LImportDecl GhcRn] -> S.HashSet Symbol
allImports :: [LImportDecl GhcRn] -> HashSet Symbol
allImports = \case
  []-> forall a. String -> a -> a
Debug.trace String
"WARNING: Missing RenamedSource" forall a. Monoid a => a
mempty
  [LImportDecl GhcRn]
imps -> forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall pass. ImportDecl pass -> XRec pass ModuleName
ideclName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l e. GenLocated l e -> e
unLoc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LImportDecl GhcRn]
imps)

qualifiedImports :: [LImportDecl GhcRn] -> QImports
qualifiedImports :: [LImportDecl GhcRn] -> QImports
qualifiedImports = \case
  []   -> forall a. String -> a -> a
Debug.trace String
"WARNING: Missing RenamedSource" ([(Symbol, Symbol)] -> QImports
qImports forall a. Monoid a => a
mempty)
  [LImportDecl GhcRn]
imps -> [(Symbol, Symbol)] -> QImports
qImports [ (Symbol
qn, Symbol
n) | GenLocated SrcSpanAnnA (ImportDecl GhcRn)
i         <- [LImportDecl GhcRn]
imps
                                          , let decl :: ImportDecl GhcRn
decl   = forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpanAnnA (ImportDecl GhcRn)
i
                                          , let m :: ModuleName
m      = forall l e. GenLocated l e -> e
unLoc (forall pass. ImportDecl pass -> XRec pass ModuleName
ideclName ImportDecl GhcRn
decl)
                                          , ModuleName
qm        <- forall a. Maybe a -> [a]
maybeToList (forall l e. GenLocated l e -> e
unLoc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall pass. ImportDecl pass -> Maybe (XRec pass ModuleName)
ideclAs ImportDecl GhcRn
decl)
                                          , let [Symbol
n,Symbol
qn] = forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ModuleName
m, ModuleName
qm]
                                          ]

qImports :: [(Symbol, Symbol)] -> QImports
qImports :: [(Symbol, Symbol)] -> QImports
qImports [(Symbol, Symbol)]
qns  = QImports
  { qiNames :: HashMap Symbol [Symbol]
qiNames   = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(Symbol, Symbol)]
qns
  , qiModules :: HashSet Symbol
qiModules = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Symbol)]
qns)
  }


---------------------------------------------------------------------------------------
-- | @lookupTyThings@ grabs all the @Name@s and associated @TyThing@ known to GHC
--   for this module; we will use this to create our name-resolution environment
--   (see `Bare.Resolve`)
---------------------------------------------------------------------------------------
lookupTyThings :: HscEnv -> ModSummary -> TcGblEnv -> IO [(Name, Maybe TyThing)]
lookupTyThings :: HscEnv -> ModSummary -> TcGblEnv -> IO [(Name, Maybe TyThing)]
lookupTyThings HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
names (HscEnv
-> ModSummary -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)
lookupTyThing HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv)
  where
    names :: [Ghc.Name]
    names :: [Name]
names  = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. [a] -> [a] -> [a]
(++)
             (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GlobalRdrElt -> Name
Ghc.greMangledName forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrEnv -> [GlobalRdrElt]
Ghc.globalRdrEnvElts forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcGblEnv -> GlobalRdrEnv
tcg_rdr_env)
             (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ClsInst -> Name
is_dfun_name forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcGblEnv -> [ClsInst]
tcg_insts) TcGblEnv
tcGblEnv
-- | Lookup a single 'Name' in the GHC environment, yielding back the 'Name' alongside the 'TyThing',
-- if one is found.
lookupTyThing :: HscEnv -> ModSummary -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)
lookupTyThing :: HscEnv
-> ModSummary -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)
lookupTyThing HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv Name
n = do
  Maybe TyThing
mty <- forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$
         forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (HscEnv -> Name -> IO (Maybe TyThing)
Ghc.hscTcRcLookupName HscEnv
hscEnv Name
n)
         forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
         forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (
           do ModuleInfoLH
mi  <- HscEnv -> ModSummary -> TcGblEnv -> IO ModuleInfoLH
moduleInfoTc HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv
              HscEnv -> ModuleInfoLH -> Name -> IO (Maybe TyThing)
modInfoLookupNameIO HscEnv
hscEnv ModuleInfoLH
mi Name
n
           )
  forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Maybe TyThing
mty)

availableTyThings :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyThing]
availableTyThings :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyThing]
availableTyThings HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv [AvailInfo]
avails =
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. HscEnv
-> ModSummary -> TcGblEnv -> Name -> IO (Name, Maybe TyThing)
lookupTyThing HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv) forall a b. (a -> b) -> a -> b
$
      [AvailInfo] -> [Name]
availableNames [AvailInfo]
avails

-- | Returns all the available (i.e. exported) 'TyCon's (type constructors) for the input 'Module'.
availableTyCons :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Ghc.TyCon]
availableTyCons :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyCon]
availableTyCons HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv [AvailInfo]
avails =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[TyThing]
things -> [TyCon
tyCon | (ATyCon TyCon
tyCon) <- [TyThing]
things]) (HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyThing]
availableTyThings HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv [AvailInfo]
avails)

-- | Returns all the available (i.e. exported) 'Var's for the input 'Module'.
availableVars :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Ghc.Var]
availableVars :: HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Var]
availableVars HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv [AvailInfo]
avails =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[TyThing]
things -> [Var
var | (AnId Var
var) <- [TyThing]
things]) (HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyThing]
availableTyThings HscEnv
hscEnv ModSummary
modSum TcGblEnv
tcGblEnv [AvailInfo]
avails)

availableNames :: [AvailInfo] -> [Name]
availableNames :: [AvailInfo] -> [Name]
availableNames =
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a -> b) -> a -> b
$ \case
      Avail GreName
n -> [GreName -> Name
Ghc.greNameMangledName GreName
n]
      AvailTC Name
n [GreName]
ns -> Name
n forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map GreName -> Name
Ghc.greNameMangledName [GreName]
ns

_dumpTypeEnv :: TypecheckedModule -> IO ()
_dumpTypeEnv :: TypecheckedModule -> IO ()
_dumpTypeEnv TypecheckedModule
tm = do
  forall a. Show a => a -> IO ()
print (String
"DUMP-TYPE-ENV" :: String)
  forall a. Show a => a -> IO ()
print (forall a. PPrint a => a -> String
showpp 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
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypecheckedModule -> ModuleInfo
tm_checked_module_info

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

checkFilePragmas :: [Located String] -> IO ()
checkFilePragmas :: [Located String] -> IO ()
checkFilePragmas = forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a e. Exception e => e -> a
throw forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Located String -> Maybe Error
err
  where
    err :: Located String -> Maybe Error
err Located String
pragma
      | String -> Bool
check (forall a. Located a -> a
val Located String
pragma) = forall a. a -> Maybe a
Just (forall t. SrcSpan -> TError t
ErrFilePragma forall a b. (a -> b) -> a -> b
$ forall a. Loc a => a -> SrcSpan
fSrcSpan Located String
pragma :: Error)
      | Bool
otherwise          = forall a. Maybe a
Nothing
    check :: String -> Bool
check String
pragma           = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
pragma) 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 = [ (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 :: ParsedModule -> [(Maybe RealSrcLoc, String)]
extractSpecComments :: ParsedModule -> [(Maybe RealSrcLoc, String)]
extractSpecComments = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Located ApiComment -> Maybe (Maybe RealSrcLoc, String)
extractSpecComment forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsedModule -> [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, String)
extractSpecComment (Ghc.L SrcSpan
sp (ApiBlockComment String
txt))
  | forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"{-@" String
txt Bool -> Bool -> Bool
&& forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf String
"@-}" String
txt          -- valid   specification
  = forall a. a -> Maybe a
Just (Maybe RealSrcLoc
offsetPos, forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
txt forall a. Num a => a -> a -> a
- Int
6) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
3 String
txt)
  | forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"{-@" String
txt                                   -- invalid specification
  = forall a. UserError -> a
uError forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. RealSrcSpan -> RealSrcLoc
realSrcSpanStart 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 forall a. Num a => a -> a -> a
+ Int
3)

extractSpecComment Located ApiComment
_ = forall a. Maybe a
Nothing

extractSpecQuotes' :: (a -> Module) -> (a -> [Annotation]) -> a -> [BPspec]
extractSpecQuotes' :: forall a. (a -> Module) -> (a -> [Annotation]) -> a -> [BPspec]
extractSpecQuotes' a -> Module
thisModule a -> [Annotation]
getAnns a
a = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe AnnPayload -> Maybe BPspec
extractSpecQuote [AnnPayload]
anns
  where
    anns :: [AnnPayload]
anns = forall a b. (a -> b) -> [a] -> [b]
map Annotation -> AnnPayload
ann_value forall a b. (a -> b) -> a -> b
$
           forall a. (a -> Bool) -> [a] -> [a]
filter (AnnTarget Name -> Bool
isOurModTarget forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annotation -> AnnTarget Name
ann_target) forall a b. (a -> b) -> a -> b
$
           a -> [Annotation]
getAnns a
a

    isOurModTarget :: AnnTarget Name -> Bool
isOurModTarget (ModuleTarget Module
mod1) = Module
mod1 forall a. Eq a => a -> a -> Bool
== a -> Module
thisModule a
a
    isOurModTarget AnnTarget Name
_ = Bool
False

extractSpecQuote :: AnnPayload -> Maybe BPspec
extractSpecQuote :: AnnPayload -> Maybe BPspec
extractSpecQuote AnnPayload
payload =
  case forall a. Typeable a => ([Word8] -> a) -> AnnPayload -> Maybe a
Ghc.fromSerialized forall a. Data a => [Word8] -> a
Ghc.deserializeWithData AnnPayload
payload of
    Maybe LiquidQuote
Nothing -> forall a. Maybe a
Nothing
    Just LiquidQuote
qt -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Data a => a -> a
refreshSymbols forall a b. (a -> b) -> a -> b
$ LiquidQuote -> BPspec
liquidQuoteSpec LiquidQuote
qt

refreshSymbols :: Data a => a -> a
refreshSymbols :: forall a. Data a => a -> a
refreshSymbols = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Symbol -> Symbol
refreshSymbol)

refreshSymbol :: Symbol -> Symbol
refreshSymbol :: Symbol -> Symbol
refreshSymbol = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText

--------------------------------------------------------------------------------
-- | Finding & Parsing Files ---------------------------------------------------
--------------------------------------------------------------------------------

-- | Parse a spec file by path.
--
-- On a parse error, we fail.
--
-- TODO, Andres: It would be better to fail more systematically, but currently we
-- seem to have an option between throwing an error which will be reported badly,
-- or printing the error ourselves.
--
parseSpecFile :: FilePath -> IO (ModName, Ms.BareSpec)
parseSpecFile :: String -> IO (ModName, BareSpec)
parseSpecFile String
file = do
  String
contents <- String -> IO String
Misc.sayReadFile String
file
  case String
-> String
-> Either (ParseErrorBundle String Void) (ModName, BareSpec)
specSpecificationP String
file String
contents of
    Left ParseErrorBundle String Void
peb -> do
      Handle -> String -> IO ()
hPutStrLn Handle
stderr (forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
peb)
      forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"parsing spec file failed"
    Right (ModName, BareSpec)
x  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModName, BareSpec)
x

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

makeLogicMap :: IO LogicMap
makeLogicMap :: IO LogicMap
makeLogicMap = do
  String
lg    <- IO String
Misc.getCoreToLogicPath
  String
lspec <- String -> IO String
Misc.sayReadFile String
lg
  case String -> String -> Either (ParseErrorBundle String Void) LogicMap
parseSymbolToLogic String
lg String
lspec of
    Left ParseErrorBundle String Void
peb -> do
      Handle -> String -> IO ()
hPutStrLn Handle
stderr (forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
peb)
      forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"makeLogicMap failed"
    Right LogicMap
lm -> forall (m :: * -> *) a. Monad m => a -> m a
return (LogicMap
lm forall a. Semigroup a => a -> a -> a
<> LogicMap
listLMap)

listLMap :: LogicMap -- TODO-REBARE: move to wiredIn
listLMap :: LogicMap
listLMap  = [(Located Symbol, [Symbol], Expr)] -> LogicMap
toLogicMap [ (forall a. a -> Located a
dummyLoc Symbol
nilName , []     , Expr
hNil)
                       , (forall a. a -> Located a
dummyLoc Symbol
consName, [forall {a}. IsString a => a
x, forall {a}. IsString a => a
xs], [Expr] -> Expr
hCons (Symbol -> Expr
EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [forall {a}. IsString a => a
x, forall {a}. IsString a => a
xs])) ]
  where
    x :: a
x     = a
"x"
    xs :: a
xs    = a
"xs"
    hNil :: Expr
hNil  = Located Symbol -> [Expr] -> Expr
mkEApp (forall {a}. Symbolic a => a -> Located Symbol
dcSym DataCon
Ghc.nilDataCon ) []
    hCons :: [Expr] -> Expr
hCons = Located Symbol -> [Expr] -> Expr
mkEApp (forall {a}. Symbolic a => a -> Located Symbol
dcSym DataCon
Ghc.consDataCon)
    dcSym :: a -> Located Symbol
dcSym = forall a. a -> Located a
dummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 ********************"
    , forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall a b. (a -> b) -> a -> b
$ GhcSpecVars -> [Var]
gsTgtVars (TargetSpec -> GhcSpecVars
gsVars TargetSpec
spec)
    , Doc
"******* Type Signatures *********************"
    , forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
spec))
    , Doc
"******* Assumed Type Signatures *************"
    , forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
spec))
    , Doc
"******* DataCon Specifications (Measure) ****"
    , forall a. PPrint a => Tidy -> [a] -> Doc
pprintLongList Tidy
k (GhcSpecData -> [(Var, LocSpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
spec))
    , Doc
"******* Measure Specifications **************"
    , 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 **********"
    , forall a. Outputable a => a -> Doc
pprDoc forall a b. (a -> b) -> a -> b
$ GhcSrc -> [Var]
_giImpVars (TargetSrc -> GhcSrc
fromTargetSrc forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    , Doc
"*************** Defined Variables ***********"
    , forall a. Outputable a => a -> Doc
pprDoc forall a b. (a -> b) -> a -> b
$ GhcSrc -> [Var]
_giDefVars (TargetSrc -> GhcSrc
fromTargetSrc forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info)
    , Doc
"*************** Specification ***************"
    , forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSpec
giSpec TargetInfo
info
    , Doc
"*************** Core Bindings ***************"
    , [CoreBind] -> Doc
pprintCBs forall a b. (a -> b) -> a -> b
$ GhcSrc -> [CoreBind]
_giCbs (TargetSrc -> GhcSrc
fromTargetSrc forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
info) ]

pprintCBs :: [CoreBind] -> Doc
pprintCBs :: [CoreBind] -> Doc
pprintCBs = forall a. Outputable a => a -> Doc
pprDoc 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 -> String
show = forall a. PPrint a => a -> String
showpp

instance PPrint TargetVars where
  pprintTidy :: Tidy -> TargetVars -> Doc
pprintTidy Tidy
_ TargetVars
AllVars   = String -> Doc
text String
"All Variables"
  pprintTidy Tidy
k (Only [Var]
vs) = String -> Doc
text String
"Only Variables: " Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [Var]
vs

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

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