{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
module Language.Haskell.Liquid.Bare (
makeTargetSpec
, loadLiftedSpec
, saveLiftedSpec
) where
import Prelude hiding (error)
import Control.Monad (forM, mplus)
import Control.Applicative ((<|>))
import qualified Control.Exception as Ex
import qualified Data.Binary as B
import qualified Data.Maybe as Mb
import qualified Data.List as L
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Text.PrettyPrint.HughesPJ hiding (first, (<>))
import System.FilePath (dropExtension)
import System.Directory (doesFileExist)
import System.Console.CmdArgs.Verbosity (whenLoud)
import Language.Fixpoint.Utils.Files as Files
import Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Types hiding (dcFields, DataDecl, Error, panic)
import qualified Language.Fixpoint.Types as F
import qualified Language.Haskell.Liquid.Misc as Misc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import qualified Liquid.GHC.API as Ghc
import Language.Haskell.Liquid.GHC.Types (StableName)
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.WiredIn
import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Haskell.Liquid.Bare.Types as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve as Bare
import qualified Language.Haskell.Liquid.Bare.DataType as Bare
import Language.Haskell.Liquid.Bare.Elaborate
import qualified Language.Haskell.Liquid.Bare.Expand as Bare
import qualified Language.Haskell.Liquid.Bare.Measure as Bare
import qualified Language.Haskell.Liquid.Bare.Plugged as Bare
import qualified Language.Haskell.Liquid.Bare.Axiom as Bare
import qualified Language.Haskell.Liquid.Bare.ToBare as Bare
import qualified Language.Haskell.Liquid.Bare.Class as Bare
import qualified Language.Haskell.Liquid.Bare.Check as Bare
import qualified Language.Haskell.Liquid.Bare.Laws as Bare
import qualified Language.Haskell.Liquid.Bare.Typeclass as Bare
import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic
import Control.Arrow (second)
import Data.Hashable (Hashable)
import qualified Language.Haskell.Liquid.Bare.Slice as Dg
loadLiftedSpec :: Config -> FilePath -> IO (Maybe Ms.BareSpec)
loadLiftedSpec :: Config -> [Char] -> IO (Maybe (Spec LocBareType LocSymbol))
loadLiftedSpec Config
cfg [Char]
srcF
| Config -> Bool
noLiftedImport Config
cfg = [Char] -> IO ()
putStrLn [Char]
"No LIFTED Import" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
| Bool
otherwise = do
let specF :: [Char]
specF = Ext -> [Char] -> [Char]
extFileName Ext
BinSpec [Char]
srcF
Bool
ex <- [Char] -> IO Bool
doesFileExist [Char]
specF
IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Loading Binary Lifted Spec: " forall a. [a] -> [a] -> [a]
++ [Char]
specF forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ [Char]
"for source-file: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
srcF forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Bool
ex
Maybe (Spec LocBareType LocSymbol)
lSp <- if Bool
ex
then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Binary a => [Char] -> IO a
B.decodeFile [Char]
specF
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
forall a. a -> IO a
Ex.evaluate Maybe (Spec LocBareType LocSymbol)
lSp
saveLiftedSpec :: FilePath -> Ms.BareSpec -> IO ()
saveLiftedSpec :: [Char] -> Spec LocBareType LocSymbol -> IO ()
saveLiftedSpec [Char]
srcF Spec LocBareType LocSymbol
lspec = do
[Char] -> IO ()
ensurePath [Char]
specF
forall a. Binary a => [Char] -> a -> IO ()
B.encodeFile [Char]
specF Spec LocBareType LocSymbol
lspec
where
specF :: [Char]
specF = Ext -> [Char] -> [Char]
extFileName Ext
BinSpec [Char]
srcF
makeTargetSpec :: Config
-> LogicMap
-> TargetSrc
-> BareSpec
-> TargetDependencies
-> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec :: Config
-> LogicMap
-> TargetSrc
-> BareSpec
-> TargetDependencies
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec Config
cfg LogicMap
lmap TargetSrc
targetSrc BareSpec
bareSpec TargetDependencies
dependencies = do
let targDiagnostics :: Either Diagnostics ()
targDiagnostics = Config -> TargetSrc -> Either Diagnostics ()
Bare.checkTargetSrc Config
cfg TargetSrc
targetSrc
let depsDiagnostics :: Either Diagnostics [()]
depsDiagnostics = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ModName -> Spec LocBareType LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec) [(ModName, Spec LocBareType LocSymbol)]
legacyDependencies
let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = ModName -> Spec LocBareType LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc) Spec LocBareType LocSymbol
legacyBareSpec
case Either Diagnostics ()
targDiagnostics forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics [()]
depsDiagnostics forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics ()
bareSpecDiagnostics of
Left Diagnostics
d | Diagnostics -> Bool
noErrors Diagnostics
d -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase (Diagnostics -> [Warning]
allWarnings Diagnostics
d)
Left Diagnostics
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Diagnostics
d
Right () -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase forall a. Monoid a => a
mempty
where
secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase :: [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Warning]
phaseOneWarns = do
Either Diagnostics ([Warning], GhcSpec)
diagOrSpec <- Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec LocBareType LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg (TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
targetSrc) LogicMap
lmap (Spec LocBareType LocSymbol
-> [(ModName, Spec LocBareType LocSymbol)]
allSpecs Spec LocBareType LocSymbol
legacyBareSpec)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
([Warning]
warns, GhcSpec
ghcSpec) <- Either Diagnostics ([Warning], GhcSpec)
diagOrSpec
let (TargetSpec
targetSpec, LiftedSpec
liftedSpec) = GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec GhcSpec
ghcSpec
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
phaseOneWarns forall a. Semigroup a => a -> a -> a
<> [Warning]
warns, TargetSpec
targetSpec, LiftedSpec
liftedSpec)
toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
toLegacyDep :: (StableModule, LiftedSpec) -> (ModName, Spec LocBareType LocSymbol)
toLegacyDep (StableModule
sm, LiftedSpec
ls) = (ModType -> ModuleName -> ModName
ModName ModType
SrcImport (forall unit. GenModule unit -> ModuleName
Ghc.moduleName forall b c a. (b -> c) -> (a -> b) -> a -> c
. StableModule -> Module
Ghc.unStableModule forall a b. (a -> b) -> a -> b
$ StableModule
sm), LiftedSpec -> Spec LocBareType LocSymbol
unsafeFromLiftedSpec LiftedSpec
ls)
toLegacyTarget :: Ms.BareSpec -> (ModName, Ms.BareSpec)
toLegacyTarget :: Spec LocBareType LocSymbol -> (ModName, Spec LocBareType LocSymbol)
toLegacyTarget Spec LocBareType LocSymbol
validatedSpec = (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc, Spec LocBareType LocSymbol
validatedSpec)
legacyDependencies :: [(ModName, Ms.BareSpec)]
legacyDependencies :: [(ModName, Spec LocBareType LocSymbol)]
legacyDependencies = forall a b. (a -> b) -> [a] -> [b]
map (StableModule, LiftedSpec) -> (ModName, Spec LocBareType LocSymbol)
toLegacyDep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies forall a b. (a -> b) -> a -> b
$ TargetDependencies
dependencies
allSpecs :: Ms.BareSpec -> [(ModName, Ms.BareSpec)]
allSpecs :: Spec LocBareType LocSymbol
-> [(ModName, Spec LocBareType LocSymbol)]
allSpecs Spec LocBareType LocSymbol
validSpec = Spec LocBareType LocSymbol -> (ModName, Spec LocBareType LocSymbol)
toLegacyTarget Spec LocBareType LocSymbol
validSpec forall a. a -> [a] -> [a]
: [(ModName, Spec LocBareType LocSymbol)]
legacyDependencies
legacyBareSpec :: Spec LocBareType F.LocSymbol
legacyBareSpec :: Spec LocBareType LocSymbol
legacyBareSpec = BareSpec -> Spec LocBareType LocSymbol
fromBareSpec BareSpec
bareSpec
makeGhcSpec :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Ms.BareSpec)]
-> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec LocBareType LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec LocBareType LocSymbol)]
validatedSpecs = do
(Diagnostics
dg0, GhcSpec
sp) <- Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec LocBareType LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec LocBareType LocSymbol)]
validatedSpecs
let diagnostics :: Either Diagnostics ()
diagnostics = [Spec LocBareType LocSymbol]
-> TargetSrc
-> SEnv SortedReft
-> [CoreBind]
-> TargetSpec
-> Either Diagnostics ()
Bare.checkTargetSpec (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(ModName, Spec LocBareType LocSymbol)]
validatedSpecs)
(GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src)
(GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp)
(GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
(forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec forall a b. (a -> b) -> a -> b
$ GhcSpec
sp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not (Diagnostics -> Bool
noErrors Diagnostics
dg0) then forall a b. a -> Either a b
Left Diagnostics
dg0 else
case Either Diagnostics ()
diagnostics of
Left Diagnostics
dg1
| Diagnostics -> Bool
noErrors Diagnostics
dg1 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics -> [Warning]
allWarnings Diagnostics
dg1, GhcSpec
sp)
| Bool
otherwise -> forall a b. a -> Either a b
Left Diagnostics
dg1
Right () -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Monoid a => a
mempty, GhcSpec
sp)
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RENV" forall a b. (a -> b) -> a -> b
$ forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(Symbol, SortedReft)]
binds
where
emb :: TCEmb TyCon
emb = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp)
binds :: [(Symbol, SortedReft)]
binds = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"binds" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [(Symbol
x, forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort SpecType
t) | (Symbol
x, Loc SourcePos
_ SourcePos
_ SpecType
t) <- GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
, [(forall a. Symbolic a => a -> Symbol
symbol TyVar
v, forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort SpecType
t) | (TyVar
v, Loc SourcePos
_ SourcePos
_ SpecType
t) <- GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
, [(forall a. Symbolic a => a -> Symbol
symbol TyVar
v, TyVar -> SortedReft
vSort TyVar
v) | TyVar
v <- GhcSpecRefl -> [TyVar]
gsReflects (GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
sp)]
, [(Symbol
x, TyVar -> SortedReft
vSort TyVar
v) | (Symbol
x, TyVar
v) <- GhcSpecNames -> [(Symbol, TyVar)]
gsFreeSyms (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp), TyVar -> Bool
Ghc.isConLikeId TyVar
v ]
, [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s forall a. Monoid a => a
mempty) | (Symbol
x, Sort
s) <- [(Symbol, Sort)]
wiredSortedSyms ]
, [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s forall a. Monoid a => a
mempty) | (Symbol
x, Sort
s) <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp ]
]
vSort :: TyVar -> SortedReft
vSort = forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. Bool -> RType c tv r -> RType c tv r
classRFInfoType (Config -> Bool
typeclass forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig GhcSpec
sp) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(forall r. Monoid r => Type -> RRType r
ofType :: Ghc.Type -> SpecType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
rSort :: RRType r -> SortedReft
rSort = forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb
makeGhcSpec0 :: Config -> GhcSrc -> LogicMap -> [(ModName, Ms.BareSpec)] ->
Ghc.TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec LocBareType LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec LocBareType LocSymbol)]
mspecsNoCls = do
TycEnv
tycEnv <- ModName
-> Env
-> (TycEnv, [Located DataConP])
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> TcRn TycEnv
makeTycEnv1 ModName
name Env
env (TycEnv
tycEnv0, [Located DataConP]
datacons) CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier
let tyi :: TyConMap
tyi = TycEnv -> TyConMap
Bare.tcTyConMap TycEnv
tycEnv
let sigEnv :: SigEnv
sigEnv = TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
makeSigEnv TCEmb TyCon
embs TyConMap
tyi (GhcSrc -> HashSet StableName
_gsExports GhcSrc
src) BareRTEnv
rtEnv
let lSpec1 :: Spec LocBareType LocSymbol
lSpec1 = Spec LocBareType LocSymbol
lSpec0 forall a. Semigroup a => a -> a -> a
<> Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec LocBareType LocSymbol
mySpec1
let mySpec :: Spec LocBareType LocSymbol
mySpec = Spec LocBareType LocSymbol
mySpec2 forall a. Semigroup a => a -> a -> a
<> Spec LocBareType LocSymbol
lSpec1
let specs :: HashMap ModName (Spec LocBareType LocSymbol)
specs = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec LocBareType LocSymbol
mySpec HashMap ModName (Spec LocBareType LocSymbol)
iSpecs2
let myRTE :: BareRTEnv
myRTE = GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv
let (Diagnostics
dg5, MeasEnv
measEnv) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
let (Diagnostics
dg4, GhcSpecSig
sig) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
GhcSpecSig
elaboratedSig <-
if Bool
allowTC then (SpecType -> TcRn SpecType)
-> [Located DataConP]
-> [(ClsInst, [TyVar])]
-> TcRn [(TyVar, LocSpecType)]
Bare.makeClassAuxTypes ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) [Located DataConP]
datacons [(ClsInst, [TyVar])]
instMethods
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GhcSpecSig
-> [(TyVar, LocSpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
elaborateSig GhcSpecSig
sig
else forall (f :: * -> *) a. Applicative f => a -> f a
pure GhcSpecSig
sig
let qual :: GhcSpecQual
qual = Config
-> Env
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecQual
makeSpecQual Config
cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
let sData :: GhcSpecData
sData = GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
elaboratedSig HashMap ModName (Spec LocBareType LocSymbol)
specs
let (Diagnostics
dg1, GhcSpecVars
spcVars) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> Spec LocBareType LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec LocBareType LocSymbol
mySpec Env
env MeasEnv
measEnv
let (Diagnostics
dg2, GhcSpecTerm
spcTerm) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> Spec LocBareType LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec LocBareType LocSymbol
mySpec Env
env ModName
name
let (Diagnostics
dg3, GhcSpecRefl
refl) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> MeasEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
measEnv HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env ModName
name GhcSpecSig
elaboratedSig TycEnv
tycEnv
let laws :: GhcSpecLaws
laws = Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> MeasEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
elaboratedSig forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
elaboratedSig) MeasEnv
measEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
let finalLiftedSpec :: Spec LocBareType LocSymbol
finalLiftedSpec = ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
elaboratedSig GhcSpecQual
qual BareRTEnv
myRTE Spec LocBareType LocSymbol
lSpec1
let diags :: Diagnostics
diags = forall a. Monoid a => [a] -> a
mconcat [Diagnostics
dg0, Diagnostics
dg1, Diagnostics
dg2, Diagnostics
dg3, Diagnostics
dg4, Diagnostics
dg5]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics
diags, SP
{ _gsConfig :: Config
_gsConfig = Config
cfg
, _gsImps :: [(Symbol, Sort)]
_gsImps = [(ModName, Spec LocBareType LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec LocBareType LocSymbol)]
mspecs
, _gsSig :: GhcSpecSig
_gsSig = Env
-> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs Env
env ModName
name BareRTEnv
rtEnv GhcSpecRefl
refl GhcSpecSig
elaboratedSig
, _gsRefl :: GhcSpecRefl
_gsRefl = GhcSpecRefl
refl
, _gsLaws :: GhcSpecLaws
_gsLaws = GhcSpecLaws
laws
, _gsData :: GhcSpecData
_gsData = GhcSpecData
sData
, _gsQual :: GhcSpecQual
_gsQual = GhcSpecQual
qual
, _gsName :: GhcSpecNames
_gsName = Env -> TycEnv -> MeasEnv -> ModName -> GhcSpecNames
makeSpecName Env
env TycEnv
tycEnv MeasEnv
measEnv ModName
name
, _gsVars :: GhcSpecVars
_gsVars = GhcSpecVars
spcVars
, _gsTerm :: GhcSpecTerm
_gsTerm = GhcSpecTerm
spcTerm
, _gsLSpec :: Spec LocBareType LocSymbol
_gsLSpec = Spec LocBareType LocSymbol
finalLiftedSpec
{ impSigs :: [(Symbol, Sort)]
impSigs = [(ModName, Spec LocBareType LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec LocBareType LocSymbol)]
mspecs
, expSigs :: [(Symbol, Sort)]
expSigs = [ (forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v, SortedReft -> Sort
F.sr_sort forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> TyVar -> SortedReft
Bare.varSortedReft TCEmb TyCon
embs TyVar
v) | TyVar
v <- GhcSpecRefl -> [TyVar]
gsReflects GhcSpecRefl
refl ]
, dataDecls :: [DataDecl]
dataDecls = Spec LocBareType LocSymbol -> [DataDecl] -> [DataDecl]
Bare.dataDeclSize Spec LocBareType LocSymbol
mySpec forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls Spec LocBareType LocSymbol
mySpec
, measures :: [Measure LocBareType LocSymbol]
measures = forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures Spec LocBareType LocSymbol
mySpec
, asmSigs :: [(LocSymbol, LocBareType)]
asmSigs = forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
mySpec
, imeasures :: [Measure LocBareType LocSymbol]
imeasures = forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures Spec LocBareType LocSymbol
mySpec
, dvariance :: [(LocSymbol, [Variance])]
dvariance = forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance Spec LocBareType LocSymbol
mySpec
, rinstance :: [RInstance LocBareType]
rinstance = forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance Spec LocBareType LocSymbol
mySpec
}
})
where
coreToLg :: CoreExpr -> Expr
coreToLg CoreExpr
ce =
case forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
CoreToLogic.runToLogic
TCEmb TyCon
embs
LogicMap
lmap
DataConMap
dm
(\[Char]
x -> forall a. Maybe SrcSpan -> [Char] -> a
todo forall a. Maybe a
Nothing ([Char]
"coreToLogic not working " forall a. [a] -> [a] -> [a]
++ [Char]
x))
(Bool -> CoreExpr -> LogicM Expr
CoreToLogic.coreToLogic Bool
allowTC CoreExpr
ce) of
Left Error
msg -> forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing (forall a. PPrint a => a -> [Char]
F.showpp Error
msg)
Right Expr
e -> Expr
e
elaborateSig :: GhcSpecSig
-> [(TyVar, LocSpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
elaborateSig GhcSpecSig
si [(TyVar, LocSpecType)]
auxsig = do
[(TyVar, LocSpecType)]
tySigs <-
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
si) forall a b. (a -> b) -> a -> b
$ \(TyVar
x, LocSpecType
t) ->
if forall a. NamedThing a => a -> Bool
GM.isFromGHCReal TyVar
x then
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
t)
else do LocSpecType
t' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) LocSpecType
t
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
t')
forall (f :: * -> *) a. Applicative f => a -> f a
pure
GhcSpecSig
si
{ gsTySigs :: [(TyVar, LocSpecType)]
gsTySigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"asmSigs" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
si)) [(TyVar, LocSpecType)]
tySigs forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
auxsig }
simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
simplifier :: CoreExpr -> TcRn CoreExpr
simplifier = forall (f :: * -> *) a. Applicative f => a -> f a
pure
allowTC :: Bool
allowTC = Config -> Bool
typeclass Config
cfg
mySpec2 :: Spec LocBareType LocSymbol
mySpec2 = forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [] Spec LocBareType LocSymbol
mySpec1 where l :: SourcePos
l = [Char] -> SourcePos
F.dummyPos [Char]
"expand-mySpec2"
iSpecs2 :: HashMap ModName (Spec LocBareType LocSymbol)
iSpecs2 = forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [] HashMap ModName (Spec LocBareType LocSymbol)
iSpecs0 where l :: SourcePos
l = [Char] -> SourcePos
F.dummyPos [Char]
"expand-iSpecs2"
rtEnv :: BareRTEnv
rtEnv = Env
-> ModName
-> Spec LocBareType LocSymbol
-> HashMap ModName (Spec LocBareType LocSymbol)
-> LogicMap
-> BareRTEnv
Bare.makeRTEnv Env
env ModName
name Spec LocBareType LocSymbol
mySpec1 HashMap ModName (Spec LocBareType LocSymbol)
iSpecs0 LogicMap
lmap
mspecs :: [(ModName, Spec LocBareType LocSymbol)]
mspecs = if Bool
allowTC then forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec LocBareType LocSymbol
mySpec0 HashMap ModName (Spec LocBareType LocSymbol)
iSpecs0 else [(ModName, Spec LocBareType LocSymbol)]
mspecsNoCls
(Spec LocBareType LocSymbol
mySpec0, [(ClsInst, [TyVar])]
instMethods) = if Bool
allowTC
then GhcSrc
-> Env
-> (ModName, Spec LocBareType LocSymbol)
-> [(ModName, Spec LocBareType LocSymbol)]
-> (Spec LocBareType LocSymbol, [(ClsInst, [TyVar])])
Bare.compileClasses GhcSrc
src Env
env (ModName
name, Spec LocBareType LocSymbol
mySpec0NoCls) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
iSpecs0)
else (Spec LocBareType LocSymbol
mySpec0NoCls, [])
mySpec1 :: Spec LocBareType LocSymbol
mySpec1 = Spec LocBareType LocSymbol
mySpec0 forall a. Semigroup a => a -> a -> a
<> Spec LocBareType LocSymbol
lSpec0
lSpec0 :: Spec LocBareType LocSymbol
lSpec0 = Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec LocBareType LocSymbol
mySpec0
embs :: TCEmb TyCon
embs = GhcSrc
-> Env -> [(ModName, Spec LocBareType LocSymbol)] -> TCEmb TyCon
makeEmbeds GhcSrc
src Env
env ((ModName
name, Spec LocBareType LocSymbol
mySpec0) forall a. a -> [a] -> [a]
: forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
iSpecs0)
dm :: DataConMap
dm = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv0
(Diagnostics
dg0, [Located DataConP]
datacons, TycEnv
tycEnv0) = Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec LocBareType LocSymbol
-> HashMap ModName (Spec LocBareType LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
name Env
env TCEmb TyCon
embs Spec LocBareType LocSymbol
mySpec2 HashMap ModName (Spec LocBareType LocSymbol)
iSpecs2
env :: Env
env = Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec LocBareType LocSymbol)]
-> Env
Bare.makeEnv Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec LocBareType LocSymbol)]
mspecsNoCls
(Spec LocBareType LocSymbol
mySpec0NoCls, HashMap ModName (Spec LocBareType LocSymbol)
iSpecs0) = ModName
-> GhcSrc
-> [(ModName, Spec LocBareType LocSymbol)]
-> (Spec LocBareType LocSymbol,
HashMap ModName (Spec LocBareType LocSymbol))
splitSpecs ModName
name GhcSrc
src [(ModName, Spec LocBareType LocSymbol)]
mspecsNoCls
name :: ModName
name = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"ALL-SPECS" forall a. [a] -> [a] -> [a]
++ [Char]
zzz) forall a b. (a -> b) -> a -> b
$ GhcSrc -> ModName
_giTargetMod GhcSrc
src
zzz :: [Char]
zzz = forall a. PPrint a => a -> [Char]
F.showpp (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec LocBareType LocSymbol)]
mspecs)
splitSpecs :: ModName -> GhcSrc -> [(ModName, Ms.BareSpec)] -> (Ms.BareSpec, Bare.ModSpecs)
splitSpecs :: ModName
-> GhcSrc
-> [(ModName, Spec LocBareType LocSymbol)]
-> (Spec LocBareType LocSymbol,
HashMap ModName (Spec LocBareType LocSymbol))
splitSpecs ModName
name GhcSrc
src [(ModName, Spec LocBareType LocSymbol)]
specs = (Spec LocBareType LocSymbol
mySpec, HashMap ModName (Spec LocBareType LocSymbol)
iSpecm)
where
iSpecm :: HashMap ModName (Spec LocBareType LocSymbol)
iSpecm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group forall a b. (a -> b) -> a -> b
$ [(ModName, Spec LocBareType LocSymbol)]
iSpecs
iSpecs :: [(ModName, Spec LocBareType LocSymbol)]
iSpecs = GhcSrc
-> Spec LocBareType LocSymbol
-> [(ModName, Spec LocBareType LocSymbol)]
-> [(ModName, Spec LocBareType LocSymbol)]
Dg.sliceSpecs GhcSrc
src Spec LocBareType LocSymbol
mySpec [(ModName, Spec LocBareType LocSymbol)]
iSpecs'
mySpec :: Spec LocBareType LocSymbol
mySpec = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec LocBareType LocSymbol)]
mySpecs)
([(ModName, Spec LocBareType LocSymbol)]
mySpecs, [(ModName, Spec LocBareType LocSymbol)]
iSpecs') = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((ModName
name forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(ModName, Spec LocBareType LocSymbol)]
specs
makeImports :: [(ModName, Ms.BareSpec)] -> [(F.Symbol, F.Sort)]
makeImports :: [(ModName, Spec LocBareType LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec LocBareType LocSymbol)]
specs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(ModName, Spec LocBareType LocSymbol)]
specs'
where specs' :: [(ModName, Spec LocBareType LocSymbol)]
specs' = forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> Bool
isSrcImport forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(ModName, Spec LocBareType LocSymbol)]
specs
makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon
makeEmbeds :: GhcSrc
-> Env -> [(ModName, Spec LocBareType LocSymbol)] -> TCEmb TyCon
makeEmbeds GhcSrc
src Env
env
= Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon
Bare.addClassEmbeds (GhcSrc -> Maybe [ClsInst]
_gsCls GhcSrc
src) (GhcSrc -> [TyCon]
_gsFiTcs GhcSrc
src)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Env -> (ModName, Spec LocBareType LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env)
makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: Env -> (ModName, Spec LocBareType LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env (ModName
name, Spec LocBareType LocSymbol
spec)
= forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
F.tceFromList [ (TyCon
tc, (Sort, TCArgs)
t) | (LocSymbol
c,(Sort, TCArgs)
t) <- forall a. TCEmb a -> [(a, (Sort, TCArgs))]
F.tceToList (forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds Spec LocBareType LocSymbol
spec), TyCon
tc <- forall {a}. ResolveSym a => LocSymbol -> [a]
symTc LocSymbol
c ]
where
symTc :: LocSymbol -> [a]
symTc = forall a. Maybe a -> [a]
Mb.maybeToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"embed-tycon"
makeLiftedSpec1 :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
-> Ms.BareSpec
makeLiftedSpec1 :: Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec1 Config
config GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec LocBareType LocSymbol
mySpec = forall a. Monoid a => a
mempty
{ measures :: [Measure LocBareType LocSymbol]
Ms.measures = Bool
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec LocBareType LocSymbol
-> [Measure LocBareType LocSymbol]
Bare.makeHaskellMeasures (Config -> Bool
typeclass Config
config) GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec LocBareType LocSymbol
mySpec }
makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
-> Ms.BareSpec
makeLiftedSpec0 :: Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec LocBareType LocSymbol
mySpec = forall a. Monoid a => a
mempty
{ ealiases :: [Located (RTAlias Symbol Expr)]
Ms.ealiases = LMap -> Located (RTAlias Symbol Expr)
lmapEAlias forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec LocBareType LocSymbol
-> [(LocSymbol, LMap)]
Bare.makeHaskellInlines (Config -> Bool
typeclass Config
cfg) GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec LocBareType LocSymbol
mySpec
, reflects :: HashSet LocSymbol
Ms.reflects = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec LocBareType LocSymbol
mySpec
, dataDecls :: [DataDecl]
Ms.dataDecls = Config
-> ModName -> Spec LocBareType LocSymbol -> [TyCon] -> [DataDecl]
Bare.makeHaskellDataDecls Config
cfg ModName
name Spec LocBareType LocSymbol
mySpec [TyCon]
tcs
, embeds :: TCEmb LocSymbol
Ms.embeds = forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds Spec LocBareType LocSymbol
mySpec
, cmeasures :: [Measure LocBareType ()]
Ms.cmeasures = forall ty bndr. Spec ty bndr -> [Measure ty ()]
Ms.cmeasures Spec LocBareType LocSymbol
mySpec
}
where
tcs :: [TyCon]
tcs = forall a. Uniquable a => [a] -> [a]
uniqNub (GhcSrc -> [TyCon]
_gsTcs GhcSrc
src forall a. [a] -> [a] -> [a]
++ [TyCon]
refTcs)
refTcs :: [TyCon]
refTcs = Config
-> TCEmb TyCon
-> [CoreBind]
-> Spec LocBareType LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs Spec LocBareType LocSymbol
mySpec
cbs :: [CoreBind]
cbs = GhcSrc -> [CoreBind]
_giCbs GhcSrc
src
name :: ModName
name = GhcSrc -> ModName
_giTargetMod GhcSrc
src
uniqNub :: (Ghc.Uniquable a) => [a] -> [a]
uniqNub :: forall a. Uniquable a => [a] -> [a]
uniqNub [a]
xs = forall k v. HashMap k v -> [v]
M.elems forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall {a}. Uniquable a => a -> Int
index a
x, a
x) | a
x <- [a]
xs ]
where
index :: a -> Int
index = Unique -> Int
Ghc.getKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Uniquable a => a -> Unique
Ghc.getUnique
reflectedTyCons :: Config -> TCEmb Ghc.TyCon -> [Ghc.CoreBind] -> Ms.BareSpec -> [Ghc.TyCon]
reflectedTyCons :: Config
-> TCEmb TyCon
-> [CoreBind]
-> Spec LocBareType LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs Spec LocBareType LocSymbol
spec
| forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs)
forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyVar -> [TyCon]
varTyCons
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec LocBareType LocSymbol
spec [CoreBind]
cbs forall a. [a] -> [a] -> [a]
++ Spec LocBareType LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec LocBareType LocSymbol
spec [CoreBind]
cbs
| Bool
otherwise = []
isEmbedded :: TCEmb Ghc.TyCon -> Ghc.TyCon -> Bool
isEmbedded :: TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs TyCon
c = forall a. (Eq a, Hashable a) => a -> TCEmb a -> Bool
F.tceMember TyCon
c TCEmb TyCon
embs
varTyCons :: Ghc.Var -> [Ghc.TyCon]
varTyCons :: TyVar -> [TyCon]
varTyCons = SpecType -> [TyCon]
specTypeCons forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Type -> RRType r
ofType forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
specTypeCons :: SpecType -> [Ghc.TyCon]
specTypeCons :: SpecType -> [TyCon]
specTypeCons = forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType forall {tv} {r}. [TyCon] -> RType RTyCon tv r -> [TyCon]
tc []
where
tc :: [TyCon] -> RType RTyCon tv r -> [TyCon]
tc [TyCon]
acc t :: RType RTyCon tv r
t@RApp {} = RTyCon -> TyCon
rtc_tc (forall c tv r. RType c tv r -> c
rt_tycon RType RTyCon tv r
t) forall a. a -> [a] -> [a]
: [TyCon]
acc
tc [TyCon]
acc RType RTyCon tv r
_ = [TyCon]
acc
reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
reflectedVars :: Spec LocBareType LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec LocBareType LocSymbol
spec [CoreBind]
cbs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
where
xDefs :: [(TyVar, CoreExpr)]
xDefs = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
reflSyms
reflSyms :: [Symbol]
reflSyms = forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec LocBareType LocSymbol
spec)
measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
measureVars :: Spec LocBareType LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec LocBareType LocSymbol
spec [CoreBind]
cbs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
where
xDefs :: [(TyVar, CoreExpr)]
xDefs = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
measureSyms
measureSyms :: [Symbol]
measureSyms = forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec LocBareType LocSymbol
spec)
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
-> Bare.Lookup GhcSpecVars
makeSpecVars :: Config
-> GhcSrc
-> Spec LocBareType LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec LocBareType LocSymbol
mySpec Env
env MeasEnv
measEnv = do
[TyVar]
tgtVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> Lookup TyVar
resolveStringVar Env
env ModName
name) (Config -> [[Char]]
checks Config
cfg)
HashSet TyVar
igVars <- forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-ignores") (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.ignores Spec LocBareType LocSymbol
mySpec)
HashSet TyVar
lVars <- forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-lvars" ) (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lvars Spec LocBareType LocSymbol
mySpec)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar] -> HashSet TyVar -> HashSet TyVar -> [TyVar] -> GhcSpecVars
SpVar [TyVar]
tgtVars HashSet TyVar
igVars HashSet TyVar
lVars [TyVar]
cMethods)
where
name :: ModName
name = GhcSrc -> ModName
_giTargetMod GhcSrc
src
cMethods :: [TyVar]
cMethods = forall a b c. (a, b, c) -> b
snd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(ModName, TyVar, LocSpecType)]
Bare.meMethods MeasEnv
measEnv
sMapM :: (Monad m, Eq b, Hashable b) => (a -> m b) -> S.HashSet a -> m (S.HashSet b)
sMapM :: forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM a -> m b
f HashSet a
xSet = do
[b]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f (forall a. HashSet a -> [a]
S.toList HashSet a
xSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [b]
ys)
sForM :: (Monad m, Eq b, Hashable b) =>S.HashSet a -> (a -> m b) -> m (S.HashSet b)
sForM :: forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM HashSet a
xs a -> m b
f = forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM a -> m b
f HashSet a
xs
qualifySymbolic :: (F.Symbolic a) => ModName -> a -> F.Symbol
qualifySymbolic :: forall a. Symbolic a => ModName -> a -> Symbol
qualifySymbolic ModName
name a
s = Symbol -> Symbol -> Symbol
GM.qualifySymbol (forall a. Symbolic a => a -> Symbol
F.symbol ModName
name) (forall a. Symbolic a => a -> Symbol
F.symbol a
s)
resolveStringVar :: Bare.Env -> ModName -> String -> Bare.Lookup Ghc.Var
resolveStringVar :: Env -> ModName -> [Char] -> Lookup TyVar
resolveStringVar Env
env ModName
name [Char]
s = Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolve-string-var" LocSymbol
lx
where
lx :: LocSymbol
lx = forall a. a -> Located a
dummyLoc (forall a. Symbolic a => ModName -> a -> Symbol
qualifySymbolic ModName
name [Char]
s)
makeSpecQual :: Config -> Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> BareRTEnv -> Bare.ModSpecs
-> GhcSpecQual
makeSpecQual :: Config
-> Env
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecQual
makeSpecQual Config
_cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
_rtEnv HashMap ModName (Spec LocBareType LocSymbol)
specs = SpQual
{ gsQualifiers :: [Qualifier]
gsQualifiers = forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. (PPrint a, Subable a) => a -> Bool
okQual [Qualifier]
quals
, gsRTAliases :: [Located SpecRTAlias]
gsRTAliases = []
}
where
quals :: [Qualifier]
quals = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall ty bndr.
Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
okQual :: a -> Bool
okQual a
q = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"okQual: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp a
q)
forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
mSyms) (forall a. Subable a => a -> [Symbol]
F.syms a
q)
mSyms :: HashSet Symbol
mSyms = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"MSYMS" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
forall a b. (a -> b) -> a -> b
$ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
wiredSortedSyms)
forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv)
forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv)
makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty bndr) -> [F.Qualifier]
makeQualifiers :: forall ty bndr.
Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv (ModName
modn, Spec ty bndr
spec)
= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
modn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams Env
env TycEnv
tycEnv ModName
modn)
forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> [Qualifier]
Ms.qualifiers Spec ty bndr
spec
resolveQParams :: Bare.Env -> Bare.TycEnv -> ModName -> F.Qualifier -> Maybe F.Qualifier
resolveQParams :: Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams Env
env TycEnv
tycEnv ModName
name Qualifier
q = do
[QualParam]
qps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QualParam -> Maybe QualParam
goQP (Qualifier -> [QualParam]
F.qParams Qualifier
q)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Qualifier
q { qParams :: [QualParam]
F.qParams = [QualParam]
qps }
where
goQP :: QualParam -> Maybe QualParam
goQP QualParam
qp = do { Sort
s <- Sort -> Maybe Sort
go (QualParam -> Sort
F.qpSort QualParam
qp) ; forall (m :: * -> *) a. Monad m => a -> m a
return QualParam
qp { qpSort :: Sort
F.qpSort = Sort
s } }
go :: F.Sort -> Maybe F.Sort
go :: Sort -> Maybe Sort
go (FAbs Int
i Sort
s) = Int -> Sort -> Sort
FAbs Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s
go (FFunc Sort
s1 Sort
s2) = Sort -> Sort -> Sort
FFunc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Maybe Sort
go Sort
s2
go (FApp Sort
s1 Sort
s2) = Sort -> Sort -> Sort
FApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Maybe Sort
go Sort
s2
go (FTC FTycon
c) = Env -> TycEnv -> ModName -> FTycon -> Maybe Sort
qualifyFTycon Env
env TycEnv
tycEnv ModName
name FTycon
c
go Sort
s = forall a. a -> Maybe a
Just Sort
s
qualifyFTycon :: Bare.Env -> Bare.TycEnv -> ModName -> F.FTycon -> Maybe F.Sort
qualifyFTycon :: Env -> TycEnv -> ModName -> FTycon -> Maybe Sort
qualifyFTycon Env
env TycEnv
tycEnv ModName
name FTycon
c
| Bool
isPrimFTC = forall a. a -> Maybe a
Just (FTycon -> Sort
FTC FTycon
c)
| Bool
otherwise = TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
tcs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a}. ResolveSym a => Maybe a
ty
where
ty :: Maybe a
ty = forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"qualify-FTycon" LocSymbol
tcs
isPrimFTC :: Bool
isPrimFTC = forall a. Located a -> a
F.val LocSymbol
tcs forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Symbol
F.prims
tcs :: LocSymbol
tcs = FTycon -> LocSymbol
F.fTyconSymbol FTycon
c
embs :: TCEmb TyCon
embs = TycEnv -> TCEmb TyCon
Bare.tcEmbs TycEnv
tycEnv
tyConSort :: F.TCEmb Ghc.TyCon -> F.Located Ghc.TyCon -> F.Sort
tyConSort :: TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs Located TyCon
lc = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Sort
s0 forall a b. (a, b) -> a
fst (forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
F.tceLookup TyCon
c TCEmb TyCon
embs)
where
c :: TyCon
c = forall a. Located a -> a
F.val Located TyCon
lc
s0 :: Sort
s0 = Located TyCon -> Sort
tyConSortRaw Located TyCon
lc
tyConSortRaw :: F.Located Ghc.TyCon -> F.Sort
tyConSortRaw :: Located TyCon -> Sort
tyConSortRaw = FTycon -> Sort
FTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> FTycon
F.symbolFTycon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Symbolic a => a -> Symbol
F.symbol
makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName ->
Bare.Lookup GhcSpecTerm
makeSpecTerm :: Config
-> Spec LocBareType LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec LocBareType LocSymbol
mySpec Env
env ModName
name = do
HashSet TyVar
sizes <- if forall t. HasConfig t => t -> Bool
structuralTerm Config
cfg then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty else Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeSize Env
env ModName
name Spec LocBareType LocSymbol
mySpec
HashSet TyVar
lazies <- Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeLazy Env
env ModName
name Spec LocBareType LocSymbol
mySpec
HashSet TyCon
autos <- Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name Spec LocBareType LocSymbol
mySpec
HashSet (Located TyVar)
gfail <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec LocBareType LocSymbol
mySpec
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpTerm
{ gsLazy :: HashSet TyVar
gsLazy = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert TyVar
dictionaryVar (HashSet TyVar
lazies forall a. Monoid a => a -> a -> a
`mappend` HashSet TyVar
sizes)
, gsFail :: HashSet (Located TyVar)
gsFail = HashSet (Located TyVar)
gfail
, gsStTerm :: HashSet TyVar
gsStTerm = HashSet TyVar
sizes
, gsAutosize :: HashSet TyCon
gsAutosize = HashSet TyCon
autos
, gsNonStTerm :: HashSet TyVar
gsNonStTerm = forall a. Monoid a => a
mempty
}
makeRelation :: Bare.Env -> ModName -> Bare.SigEnv ->
[(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr, RelExpr)] -> Bare.Lookup [(Ghc.Var, Ghc.Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation :: Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {e} {f}.
(LocSymbol, LocSymbol, LocBareType, LocBareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go
where
go :: (LocSymbol, LocSymbol, LocBareType, LocBareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go (LocSymbol
x, LocSymbol
y, LocBareType
tx, LocBareType
ty, e
a, f
e) = do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
TyVar
vy <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
y
forall (m :: * -> *) a. Monad m => a -> m a
return
( TyVar
vx
, TyVar
vy
, Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.HsTV TyVar
vx) LocBareType
tx
, Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.HsTV TyVar
vy) LocBareType
ty
, e
a
, f
e
)
makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy :: Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeLazy Env
env ModName
name Spec LocBareType LocSymbol
spec =
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var") (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lazy Spec LocBareType LocSymbol
spec)
makeFail :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeFail :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec LocBareType LocSymbol
spec =
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.fails Spec LocBareType LocSymbol
spec) forall a b. (a -> b) -> a -> b
$ \LocSymbol
x -> do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
forall (m :: * -> *) a. Monad m => a -> m a
return LocSymbol
x { val :: TyVar
val = TyVar
vx }
makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeRewrite :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec LocBareType LocSymbol
spec =
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.rewrites Spec LocBareType LocSymbol
spec) forall a b. (a -> b) -> a -> b
$ \LocSymbol
x -> do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
forall (m :: * -> *) a. Monad m => a -> m a
return LocSymbol
x { val :: TyVar
val = TyVar
vx }
makeRewriteWith :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
makeRewriteWith :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec LocBareType LocSymbol
spec = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr.
Env -> ModName -> Spec ty bndr -> Lookup [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec LocBareType LocSymbol
spec
makeRewriteWith' :: Bare.Env -> ModName -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' :: forall ty bndr.
Env -> ModName -> Spec ty bndr -> Lookup [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec ty bndr
spec =
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
Ms.rewriteWith Spec ty bndr
spec) forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [LocSymbol]
xs) -> do
TyVar
xv <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var1" LocSymbol
x
[TyVar]
xvs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var2") [LocSymbol]
xs
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
xv, [TyVar]
xvs)
makeAutoSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon)
makeAutoSize :: Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name
= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyCon
Bare.lookupGhcTyCon Env
env ModName
name [Char]
"TyCon")
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> [a]
S.toList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.autosize
makeSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeSize :: Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeSize Env
env ModName
name
= forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var")
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe LocSymbol
getSizeFuns
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls
getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns DataDecl
decl
| Just SizeFun
x <- DataDecl -> Maybe SizeFun
tycSFun DataDecl
decl
, SymSizeFun LocSymbol
f <- SizeFun
x
= forall a. a -> Maybe a
Just LocSymbol
f
| Bool
otherwise
= forall a. Maybe a
Nothing
makeSpecLaws :: Bare.Env -> Bare.SigEnv -> [(Ghc.Var,LocSpecType)] -> Bare.MeasEnv -> Bare.ModSpecs
-> GhcSpecLaws
makeSpecLaws :: Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> MeasEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs MeasEnv
menv HashMap ModName (Spec LocBareType LocSymbol)
specs = SpLaws
{ gsLawDefs :: [(Class, [(TyVar, LocSpecType)])]
gsLawDefs = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall a b. (a -> b) -> [a] -> [b]
map (\(ModName
_,TyVar
x,LocSpecType
y) -> (TyVar
x,LocSpecType
y))) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
menv
, gsLawInst :: [LawInstance]
gsLawInst = Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> HashMap ModName (Spec LocBareType LocSymbol)
-> [LawInstance]
Bare.makeInstanceLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs HashMap ModName (Spec LocBareType LocSymbol)
specs
}
makeSpecRefl :: Config -> GhcSrc -> Bare.MeasEnv -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
-> Bare.Lookup GhcSpecRefl
makeSpecRefl :: Config
-> GhcSrc
-> MeasEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
menv HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv = do
HashMap TyVar (Maybe Int)
autoInst <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec LocBareType LocSymbol
mySpec
HashSet (Located TyVar)
rwr <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec LocBareType LocSymbol
mySpec
HashMap TyVar [TyVar]
rwrWith <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec LocBareType LocSymbol
mySpec
[TyVar]
wRefls <- Config -> Env -> ModName -> GhcSpecSig -> Either [Error] [TyVar]
Bare.wiredReflects Config
cfg Env
env ModName
name GhcSpecSig
sig
[(TyVar, LocSpecType, Equation)]
xtes <- Config
-> GhcSrc
-> Env
-> TycEnv
-> ModName
-> LogicMap
-> GhcSpecSig
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocSpecType, Equation)]
Bare.makeHaskellAxioms Config
cfg GhcSrc
src Env
env TycEnv
tycEnv ModName
name LogicMap
lmap GhcSpecSig
sig Spec LocBareType LocSymbol
mySpec
let myAxioms :: [Equation]
myAxioms =
[ forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop
Env
env
ModName
name
(forall a. Located a -> SourcePos
F.loc LocSpecType
lt)
Equation
e {eqName :: Symbol
eqName = Symbol
s, eqRec :: Bool
eqRec = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
s (Expr -> HashSet Symbol
exprSymbolsSet (Equation -> Expr
eqBody Equation
e))}
| (TyVar
x, LocSpecType
lt, Equation
e) <- [(TyVar, LocSpecType, Equation)]
xtes
, let s :: Symbol
s = forall a. Symbolic a => a -> Symbol
symbol TyVar
x
]
let sigVars :: [TyVar]
sigVars = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SIGVARS" forall a b. (a -> b) -> a -> b
$ (forall a b c. (a, b, c) -> a
fst3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType, Equation)]
xtes)
forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
sig)
forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsRefSigs GhcSpecSig
sig)
forall (m :: * -> *) a. Monad m => a -> m a
return SpRefl
{ gsLogicMap :: LogicMap
gsLogicMap = LogicMap
lmap
, gsAutoInst :: HashMap TyVar (Maybe Int)
gsAutoInst = HashMap TyVar (Maybe Int)
autoInst
, gsImpAxioms :: [Equation]
gsImpAxioms = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall ty bndr. Spec ty bndr -> [Equation]
Ms.axeqs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
, gsMyAxioms :: [Equation]
gsMyAxioms = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsMyAxioms" [Equation]
myAxioms
, gsReflects :: [TyVar]
gsReflects = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsReflects" ([TyVar]
lawMethods forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (HashSet Symbol -> TyVar -> Bool
isReflectVar HashSet Symbol
rflSyms) [TyVar]
sigVars forall a. [a] -> [a] -> [a]
++ [TyVar]
wRefls)
, gsHAxioms :: [(TyVar, LocSpecType, Equation)]
gsHAxioms = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsHAxioms" [(TyVar, LocSpecType, Equation)]
xtes
, gsWiredReft :: [TyVar]
gsWiredReft = [TyVar]
wRefls
, gsRewrites :: HashSet (Located TyVar)
gsRewrites = HashSet (Located TyVar)
rwr
, gsRewritesWith :: HashMap TyVar [TyVar]
gsRewritesWith = HashMap TyVar [TyVar]
rwrWith
}
where
lawMethods :: [TyVar]
lawMethods = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"Law Methods" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Class -> [TyVar]
Ghc.classMethods (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
menv)
mySpec :: Spec LocBareType LocSymbol
mySpec = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
rflSyms :: HashSet Symbol
rflSyms = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (HashMap ModName (Spec LocBareType LocSymbol) -> [Symbol]
getReflects HashMap ModName (Spec LocBareType LocSymbol)
specs)
lmap :: LogicMap
lmap = Env -> LogicMap
Bare.reLMap Env
env
isReflectVar :: S.HashSet F.Symbol -> Ghc.Var -> Bool
isReflectVar :: HashSet Symbol -> TyVar -> Bool
isReflectVar HashSet Symbol
reflSyms TyVar
v = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
vx HashSet Symbol
reflSyms
where
vx :: Symbol
vx = Symbol -> Symbol
GM.dropModuleNames (forall a. Symbolic a => a -> Symbol
symbol TyVar
v)
getReflects :: Bare.ModSpecs -> [Symbol]
getReflects :: HashMap ModName (Spec LocBareType LocSymbol) -> [Symbol]
getReflects = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
names forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList
where
names :: Spec ty bndr -> HashSet LocSymbol
names Spec ty bndr
z = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions [ forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec ty bndr
z, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Spec ty bndr
z, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec ty bndr
z ]
addReflSigs :: Bare.Env -> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs :: Env
-> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs Env
env ModName
name BareRTEnv
rtEnv GhcSpecRefl
refl GhcSpecSig
sig =
GhcSpecSig
sig { gsRefSigs :: [(TyVar, LocSpecType)]
gsRefSigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"gsRefSigs for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (TyVar, LocSpecType) -> (TyVar, LocSpecType)
expandReflectedSignature [(TyVar, LocSpecType)]
reflSigs
, gsAsmSigs :: [(TyVar, LocSpecType)]
gsAsmSigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"gsAsmSigs for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name) ([(TyVar, LocSpecType)]
wreflSigs forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (TyVar, b) -> Bool
notReflected (GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
sig))
}
where
expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
expandReflectedSignature :: (TyVar, LocSpecType) -> (TyVar, LocSpecType)
expandReflectedSignature = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-refSigs") [])
([(TyVar, LocSpecType)]
wreflSigs, [(TyVar, LocSpecType)]
reflSigs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
[ (TyVar
x, LocSpecType
t) | (TyVar
x, LocSpecType
t, Equation
_) <- GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl ]
reflected :: [TyVar]
reflected = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(TyVar, LocSpecType)]
wreflSigs forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
reflSigs)
notReflected :: (TyVar, b) -> Bool
notReflected (TyVar, b)
xt = forall a b. (a, b) -> a
fst (TyVar, b)
xt forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [TyVar]
reflected
makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec ->
Bare.Lookup (M.HashMap Ghc.Var (Maybe Int))
makeAutoInst :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec LocBareType LocSymbol
spec = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [(TyVar, Maybe Int)]
kvs
where
kvs :: Either [Error] [(TyVar, Maybe Int)]
kvs = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k v. HashMap k v -> [(k, v)]
M.toList (forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
Ms.autois Spec LocBareType LocSymbol
spec)) forall a b. (a -> b) -> a -> b
$ \(LocSymbol
k, Maybe Int
val) -> do
TyVar
vk <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
k
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
vk, Maybe Int
val)
makeSpecSig :: Config -> ModName -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
-> Bare.Lookup GhcSpecSig
makeSpecSig :: Config
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv [CoreBind]
cbs = do
[(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs <- Env
-> SigEnv
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec LocBareType LocSymbol
mySpec
[(TyVar, LocSpecType)]
aSigs <- forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"makeSpecSig aSigs " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name) forall a b. (a -> b) -> a -> b
$ Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
let asmSigs :: [(TyVar, LocSpecType)]
asmSigs = TycEnv -> [(TyVar, LocSpecType)]
Bare.tcSelVars TycEnv
tycEnv
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
aSigs
forall a. [a] -> [a] -> [a]
++ [ (TyVar
x,LocSpecType
t) | (ModName
_, TyVar
x, LocSpecType
t) <- forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd (MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
measEnv) ]
let tySigs :: [(TyVar, LocSpecType)]
tySigs = [(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)]
strengthenSigs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
[ [(TyVar
v, (Int
0, LocSpecType
t)) | (TyVar
v, LocSpecType
t,Maybe [Located Expr]
_) <- [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs ]
, [(TyVar
v, (Int
1, LocSpecType
t)) | (TyVar
v, LocSpecType
t ) <- MeasEnv -> [(TyVar, LocSpecType)]
makeMthSigs MeasEnv
measEnv ]
, [(TyVar
v, (Int
2, LocSpecType
t)) | (TyVar
v, LocSpecType
t ) <- Env
-> BareRTEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName, Spec LocBareType LocSymbol)]
allSpecs ]
, [(TyVar
v, (Int
3, LocSpecType
t)) | (TyVar
v, LocSpecType
t ) <- Env
-> BareRTEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName, Spec LocBareType LocSymbol)]
allSpecs ]
]
[(TyCon, LocSpecType)]
newTys <- Env
-> SigEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec LocBareType LocSymbol)]
allSpecs
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
relation <- Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.relational Spec LocBareType LocSymbol
mySpec)
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
asmRel <- Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.asmRel Spec LocBareType LocSymbol
mySpec)
forall (m :: * -> *) a. Monad m => a -> m a
return SpSig
{ gsTySigs :: [(TyVar, LocSpecType)]
gsTySigs = [(TyVar, LocSpecType)]
tySigs
, gsAsmSigs :: [(TyVar, LocSpecType)]
gsAsmSigs = [(TyVar, LocSpecType)]
asmSigs
, gsRefSigs :: [(TyVar, LocSpecType)]
gsRefSigs = []
, gsDicts :: DEnv TyVar LocSpecType
gsDicts = DEnv TyVar LocSpecType
dicts
, gsMethods :: [(TyVar, MethodType LocSpecType)]
gsMethods = if Config -> Bool
noclasscheck Config
cfg then [] else Bool
-> DEnv TyVar LocSpecType
-> [DataConP]
-> [CoreBind]
-> [(TyVar, MethodType LocSpecType)]
Bare.makeMethodTypes (Config -> Bool
typeclass Config
cfg) DEnv TyVar LocSpecType
dicts (MeasEnv -> [DataConP]
Bare.meClasses MeasEnv
measEnv) [CoreBind]
cbs
, gsInSigs :: [(TyVar, LocSpecType)]
gsInSigs = forall a. Monoid a => a
mempty
, gsNewTypes :: [(TyCon, LocSpecType)]
gsNewTypes = [(TyCon, LocSpecType)]
newTys
, gsTexprs :: [(TyVar, LocSpecType, [Located Expr])]
gsTexprs = [ (TyVar
v, LocSpecType
t, [Located Expr]
es) | (TyVar
v, LocSpecType
t, Just [Located Expr]
es) <- [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs ]
, gsRelation :: [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsRelation = [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
relation
, gsAsmRel :: [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel = [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
asmRel
}
where
dicts :: DEnv TyVar LocSpecType
dicts = Env
-> SigEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> DEnv TyVar LocSpecType
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
mySpec :: Spec LocBareType LocSymbol
mySpec = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
allSpecs :: [(ModName, Spec LocBareType LocSymbol)]
allSpecs = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs
rtEnv :: BareRTEnv
rtEnv = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
strengthenSigs :: [(Ghc.Var, (Int, LocSpecType))] ->[(Ghc.Var, LocSpecType)]
strengthenSigs :: [(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)]
strengthenSigs [(TyVar, (Int, LocSpecType))]
sigs = forall {a} {b}.
(PPrint a, Ord b) =>
(a, [(b, LocSpecType)]) -> (a, LocSpecType)
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(TyVar, (Int, LocSpecType))]
sigs
where
go :: (a, [(b, LocSpecType)]) -> (a, LocSpecType)
go (a
v, [(b, LocSpecType)]
ixs) = (a
v,) forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> [a] -> a
L.foldl1' (forall a b c. (a -> b -> c) -> b -> a -> c
flip LocSpecType -> LocSpecType -> LocSpecType
meetLoc) (forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"STRENGTHEN-SIGS: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp a
v) (forall {b} {b}. Ord b => [(b, b)] -> [b]
prio [(b, LocSpecType)]
ixs))
prio :: [(b, b)] -> [b]
prio = 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
. forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn forall a b. (a, b) -> a
fst
meetLoc :: LocSpecType -> LocSpecType -> LocSpecType
meetLoc :: LocSpecType -> LocSpecType -> LocSpecType
meetLoc LocSpecType
t1 LocSpecType
t2 = LocSpecType
t1 {val :: SpecType
val = forall a. Located a -> a
val LocSpecType
t1 forall r. Reftable r => r -> r -> r
`F.meet` forall a. Located a -> a
val LocSpecType
t2}
makeMthSigs :: Bare.MeasEnv -> [(Ghc.Var, LocSpecType)]
makeMthSigs :: MeasEnv -> [(TyVar, LocSpecType)]
makeMthSigs MeasEnv
measEnv = [ (TyVar
v, LocSpecType
t) | (ModName
_, TyVar
v, LocSpecType
t) <- MeasEnv -> [(ModName, TyVar, LocSpecType)]
Bare.meMethods MeasEnv
measEnv ]
makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeInlSigs :: Env
-> BareRTEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv
= BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> TyVar -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec LocBareType LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hinlines" forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Env
env
makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeMsrSigs :: Env
-> BareRTEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv
= BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> TyVar -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec LocBareType LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hmeas" forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Env
env
makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
makeLiftedSigs :: BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv TyVar -> SpecType
f [TyVar]
xs
= [(TyVar
x, LocSpecType
lt) | TyVar
x <- [TyVar]
xs
, let lx :: Located TyVar
lx = forall a. NamedThing a => a -> Located a
GM.locNamedThing TyVar
x
, let lt :: LocSpecType
lt = LocSpecType -> LocSpecType
expand forall a b. (a -> b) -> a -> b
$ Located TyVar
lx {val :: SpecType
val = TyVar -> SpecType
f TyVar
x}
]
where
expand :: LocSpecType -> LocSpecType
expand = BareRTEnv -> LocSpecType -> LocSpecType
Bare.specExpandType BareRTEnv
rtEnv
makeFromSet :: String -> (Ms.BareSpec -> S.HashSet LocSymbol) -> Bare.Env -> [(ModName, Ms.BareSpec)]
-> [Ghc.Var]
makeFromSet :: [Char]
-> (Spec LocBareType LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> [TyVar]
makeFromSet [Char]
msg Spec LocBareType LocSymbol -> HashSet LocSymbol
f Env
env [(ModName, Spec LocBareType LocSymbol)]
specs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ forall {b}. ResolveSym b => ModName -> [LocSymbol] -> [b]
mk ModName
n [LocSymbol]
xs | (ModName
n, Spec LocBareType LocSymbol
s) <- [(ModName, Spec LocBareType LocSymbol)]
specs, let xs :: [LocSymbol]
xs = forall a. HashSet a -> [a]
S.toList (Spec LocBareType LocSymbol -> HashSet LocSymbol
f Spec LocBareType LocSymbol
s)]
where
mk :: ModName -> [LocSymbol] -> [b]
mk ModName
name = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
msg)
makeTySigs :: Bare.Env -> Bare.SigEnv -> ModName -> Ms.BareSpec
-> Bare.Lookup [(Ghc.Var, LocSpecType, Maybe [Located F.Expr])]
makeTySigs :: Env
-> SigEnv
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec LocBareType LocSymbol
spec = do
[(TyVar, LocBareType)]
bareSigs <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType)]
bareTySigs Env
env ModName
name Spec LocBareType LocSymbol
spec
[(TyVar, LocBareType, Maybe [Located Expr])]
expSigs <- Env
-> ModName
-> [(TyVar, LocBareType)]
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(TyVar, LocBareType)]
bareSigs BareRTEnv
rtEnv Spec LocBareType LocSymbol
spec
let rawSigs :: [(TyVar, LocBareType, Maybe [Located Expr])]
rawSigs = Env
-> [(TyVar, LocBareType, Maybe [Located Expr])]
-> [(TyVar, LocBareType, Maybe [Located Expr])]
Bare.resolveLocalBinds Env
env [(TyVar, LocBareType, Maybe [Located Expr])]
expSigs
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, TyVar -> LocBareType -> LocSpecType
cook TyVar
x LocBareType
bt, Maybe [Located Expr]
z) | (TyVar
x, LocBareType
bt, Maybe [Located Expr]
z) <- [(TyVar, LocBareType, Maybe [Located Expr])]
rawSigs ]
where
rtEnv :: BareRTEnv
rtEnv = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
cook :: TyVar -> LocBareType -> LocSpecType
cook TyVar
x LocBareType
bt = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.HsTV TyVar
x) LocBareType
bt
bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
bareTySigs :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType)]
bareTySigs Env
env ModName
name Spec LocBareType LocSymbol
spec = forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lookup [(TyVar, LocBareType)]
vts
where
vts :: Lookup [(TyVar, LocBareType)]
vts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec LocBareType LocSymbol
spec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.localSigs Spec LocBareType LocSymbol
spec ) forall a b. (a -> b) -> a -> b
$ \ (LocSymbol
x, LocBareType
t) -> do
TyVar
v <- forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LOOKUP-GHC-VAR" forall a b. (a -> b) -> a -> b
$ Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"rawTySigs" LocSymbol
x
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
v, LocBareType
t)
checkDuplicateSigs :: (Symbolic x) => [(x, F.Located t)] -> [(x, F.Located t)]
checkDuplicateSigs :: forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs [(x, Located t)]
xts = case forall k v. (Eq k, Hashable k) => [(k, v)] -> Either (k, [v]) [v]
Misc.uniqueByKey [(Symbol, SourcePos)]
symXs of
Left (Symbol
k, [SourcePos]
ls) -> forall a. UserError -> a
uError (forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (forall a. PPrint a => a -> Doc
pprint Symbol
k) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourcePos]
ls))
Right [SourcePos]
_ -> [(x, Located t)]
xts
where
symXs :: [(Symbol, SourcePos)]
symXs = [ (forall a. Symbolic a => a -> Symbol
F.symbol x
x, forall a. Located a -> SourcePos
F.loc Located t
t) | (x
x, Located t
t) <- [(x, Located t)]
xts ]
makeAsmSigs :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.ModSpecs -> Bare.Lookup [(Ghc.Var, LocSpecType)]
makeAsmSigs :: Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs = do
[(ModName, TyVar, LocBareType)]
raSigs <- Env
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(ModName, TyVar, LocBareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, LocSpecType
t) | (ModName
name, TyVar
x, LocBareType
bt) <- [(ModName, TyVar, LocBareType)]
raSigs, let t :: LocSpecType
t = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.LqTV TyVar
x) LocBareType
bt ]
rawAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> Bare.Lookup [(ModName, Ghc.Var, LocBareType)]
rawAsmSigs :: Env
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(ModName, TyVar, LocBareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs = do
[(TyVar, [(Bool, ModName, LocBareType)])]
aSigs <- Env
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, LocBareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs
forall (m :: * -> *) a. Monad m => a -> m a
return [ (ModName
m, TyVar
v, LocBareType
t) | (TyVar
v, [(Bool, ModName, LocBareType)]
sigs) <- [(TyVar, [(Bool, ModName, LocBareType)])]
aSigs, let (ModName
m, LocBareType
t) = TyVar -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig TyVar
v [(Bool, ModName, LocBareType)]
sigs ]
myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: TyVar -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig TyVar
v [(Bool, ModName, LocBareType)]
sigs = forall a. a -> Maybe a -> a
Mb.fromMaybe forall {a}. a
errImp (Maybe (ModName, LocBareType)
mbHome forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (ModName, LocBareType)
mbImp)
where
mbHome :: Maybe (ModName, LocBareType)
mbHome = forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique forall {a} {a}. [(a, Located a)] -> UserError
mkErr [(ModName, LocBareType)]
sigsHome
mbImp :: Maybe (ModName, LocBareType)
mbImp = forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique forall {a} {a}. [(a, Located a)] -> UserError
mkErr (forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int, (ModName, LocBareType))]
sigsImp)
sigsHome :: [(ModName, LocBareType)]
sigsHome = [(ModName
m, LocBareType
t) | (Bool
True, ModName
m, LocBareType
t) <- [(Bool, ModName, LocBareType)]
sigs ]
sigsImp :: [(Int, (ModName, LocBareType))]
sigsImp = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"SIGS-IMP: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp TyVar
v)
[(Int
d, (ModName
m, LocBareType
t)) | (Bool
False, ModName
m, LocBareType
t) <- [(Bool, ModName, LocBareType)]
sigs, let d :: Int
d = Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
m]
mkErr :: [(a, Located a)] -> UserError
mkErr [(a, Located a)]
ts = forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyVar
v) (forall a. PPrint a => a -> Doc
F.pprint TyVar
v) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> SourcePos
F.loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Located a)]
ts) :: UserError
errImp :: a
errImp = forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"myAsmSig: cannot happen as sigs is non-null"
vName :: Symbol
vName = Symbol -> Symbol
GM.takeModuleNames (forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v)
makeTExpr :: Bare.Env -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
-> Bare.Lookup [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
makeTExpr :: Env
-> ModName
-> [(TyVar, LocBareType)]
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(TyVar, LocBareType)]
tySigs BareRTEnv
rtEnv Spec LocBareType LocSymbol
spec = do
HashMap TyVar [Located Expr]
vExprs <- forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec LocBareType LocSymbol
spec
let vSigExprs :: HashMap TyVar (LocBareType, Maybe [Located Expr])
vSigExprs = forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\TyVar
v LocBareType
t -> (LocBareType
t, forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyVar
v HashMap TyVar [Located Expr]
vExprs)) HashMap TyVar LocBareType
vSigs
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
v, LocBareType
t, forall {f :: * -> *}.
Functor f =>
LocBareType -> f (Located Expr) -> f (Located Expr)
qual LocBareType
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Located Expr]
es) | (TyVar
v, (LocBareType
t, Maybe [Located Expr]
es)) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyVar (LocBareType, Maybe [Located Expr])
vSigExprs ]
where
qual :: LocBareType -> f (Located Expr) -> f (Located Expr)
qual LocBareType
t f (Located Expr)
es = Env
-> ModName
-> BareRTEnv
-> LocBareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv LocBareType
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Located Expr)
es
vSigs :: HashMap TyVar LocBareType
vSigs = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyVar, LocBareType)]
tySigs
qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
-> Located F.Expr
qualifyTermExpr :: Env
-> ModName
-> BareRTEnv
-> LocBareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv LocBareType
t Located Expr
le
= forall l b. Loc l => l -> b -> Located b
F.atLoc Located Expr
le (forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs Expr
e)
where
l :: SourcePos
l = forall a. Located a -> SourcePos
F.loc Located Expr
le
e :: Expr
e = forall a. Located a -> a
F.val Located Expr
le
bs :: [Symbol]
bs = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ LocBareType
t
makeVarTExprs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec LocBareType LocSymbol
spec =
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
Ms.termexprs Spec LocBareType LocSymbol
spec) forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [Located Expr]
es) -> do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
vx, [Located Expr]
es)
nameDistance :: F.Symbol -> ModName -> Int
nameDistance :: Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
tName
| Symbol
vName forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
F.symbol ModName
tName = Int
0
| Bool
otherwise = Int
1
takeUnique :: Ex.Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique :: forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [a] -> e
_ [] = forall a. Maybe a
Nothing
takeUnique [a] -> e
_ [a
x] = forall a. a -> Maybe a
Just a
x
takeUnique [a] -> e
f [a]
xs = forall a e. Exception e => e -> a
Ex.throw ([a] -> e
f [a]
xs)
allAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs ->
Bare.Lookup [(Ghc.Var, [(Bool, ModName, LocBareType)])]
allAsmSigs :: Env
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, LocBareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs = do
let aSigs :: [(ModName, Bool, LocSymbol, LocBareType)]
aSigs = [ (ModName
name, Bool
locallyDefined, LocSymbol
x, LocBareType
t) | (ModName
name, Spec LocBareType LocSymbol
spec) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs
, (Bool
locallyDefined, LocSymbol
x, LocBareType
t) <- ModName
-> ModName
-> Spec LocBareType LocSymbol
-> [(Bool, LocSymbol, LocBareType)]
getAsmSigs ModName
myName ModName
name Spec LocBareType LocSymbol
spec ]
[(Maybe TyVar, (Bool, ModName, LocBareType))]
vSigs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, Bool, LocSymbol, LocBareType)]
aSigs forall a b. (a -> b) -> a -> b
$ \(ModName
name, Bool
locallyDefined, LocSymbol
x, LocBareType
t) -> do
let (Maybe Symbol
mm, Symbol
s) = Symbol -> (Maybe Symbol, Symbol)
Bare.unQualifySymbol (forall a. Located a -> a
val LocSymbol
x)
Maybe TyVar
vMb <- if Bool -> Bool
not (Maybe Symbol -> Bool
isAbsoluteQualifiedSym Maybe Symbol
mm) then Env -> ModName -> Bool -> LocSymbol -> Lookup (Maybe TyVar)
resolveAsmVar Env
env ModName
name Bool
locallyDefined LocSymbol
x
else if Bool
locallyDefined then
LocSymbol -> (Maybe Symbol, Symbol) -> Lookup (Maybe TyVar)
lookupImportedSym LocSymbol
x (Maybe Symbol
mm, Symbol
s)
else
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol
mm, Symbol
s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar
vMb, (Bool
locallyDefined, ModName
name, LocBareType
t))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [ (TyVar
v, (Bool, ModName, LocBareType)
z) | (Just TyVar
v, (Bool, ModName, LocBareType)
z) <- [(Maybe TyVar, (Bool, ModName, LocBareType))]
vSigs ]
where
lookupImportedSym :: LocSymbol -> (Maybe Symbol, Symbol) -> Lookup (Maybe TyVar)
lookupImportedSym LocSymbol
x (Maybe Symbol, Symbol)
qp =
let errRes :: Either [Error] b
errRes = forall a b. a -> Either a b
Left [Doc -> [Char] -> LocSymbol -> Error
Bare.errResolve Doc
"variable" [Char]
"Var" LocSymbol
x]
in forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {b}. Either [Error] b
errRes (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) forall a b. (a -> b) -> a -> b
$
(Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol, Symbol)
qp
lookupImportedSymMaybe :: (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol
mm, Symbol
s) = do
[(Symbol, TyThing)]
mts <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
s (Env -> TyThingMap
Bare._reTyThings Env
env)
Symbol
m <- Maybe Symbol
mm
forall a. [a] -> Maybe a
Mb.listToMaybe [ TyVar
v | (Symbol
k, Ghc.AnId TyVar
v) <- [(Symbol, TyThing)]
mts, Symbol
k forall a. Eq a => a -> a -> Bool
== Symbol
m ]
isAbsoluteQualifiedSym :: Maybe Symbol -> Bool
isAbsoluteQualifiedSym (Just Symbol
m) =
Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
m forall a b. (a -> b) -> a -> b
$ QImports -> HashMap Symbol [Symbol]
qiNames (Env -> QImports
Bare.reQualImps Env
env)
isAbsoluteQualifiedSym Maybe Symbol
Nothing =
Bool
False
resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Bare.Lookup (Maybe Ghc.Var)
resolveAsmVar :: Env -> ModName -> Bool -> LocSymbol -> Lookup (Maybe TyVar)
resolveAsmVar Env
env ModName
name Bool
True LocSymbol
lx = forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolveAsmVar-True" LocSymbol
lx
resolveAsmVar Env
env ModName
name Bool
False LocSymbol
lx = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"resolveAsmVar-False" LocSymbol
lx forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Maybe TyVar
GM.maybeAuxVar (forall a. Located a -> a
F.val LocSymbol
lx)
getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, LocSymbol, LocBareType)]
getAsmSigs :: ModName
-> ModName
-> Spec LocBareType LocSymbol
-> [(Bool, LocSymbol, LocBareType)]
getAsmSigs ModName
myName ModName
name Spec LocBareType LocSymbol
spec
| ModName
myName forall a. Eq a => a -> a -> Bool
== ModName
name = [ (Bool
True, LocSymbol
x, LocBareType
t) | (LocSymbol
x, LocBareType
t) <- forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
spec ]
| Bool
otherwise = [ (Bool
False, LocSymbol
x', LocBareType
t) | (LocSymbol
x, LocBareType
t) <- forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
spec
forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec LocBareType LocSymbol
spec
, let x' :: LocSymbol
x' = forall {f :: * -> *}. Functor f => f Symbol -> f Symbol
qSym LocSymbol
x ]
where
qSym :: f Symbol -> f Symbol
qSym = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> Symbol -> Symbol
GM.qualifySymbol Symbol
ns)
ns :: Symbol
ns = forall a. Symbolic a => a -> Symbol
F.symbol ModName
name
_grepClassAssumes :: [RInstance t] -> [(Located F.Symbol, t)]
_grepClassAssumes :: forall t. [RInstance t] -> [(LocSymbol, t)]
_grepClassAssumes = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {b}. RInstance b -> [(LocSymbol, b)]
go
where
go :: RInstance b -> [(LocSymbol, b)]
go RInstance b
xts = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe forall {f :: * -> *} {b}.
Functor f =>
(f Symbol, RISig b) -> Maybe (f Symbol, b)
goOne (forall t. RInstance t -> [(LocSymbol, RISig t)]
risigs RInstance b
xts)
goOne :: (f Symbol, RISig b) -> Maybe (f Symbol, b)
goOne (f Symbol
x, RIAssumed b
t) = forall a. a -> Maybe a
Just (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
".$c" forall a. [a] -> [a] -> [a]
++ ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
F.symbolString) f Symbol
x, b
t)
goOne (f Symbol
_, RISig b
_) = forall a. Maybe a
Nothing
makeSigEnv :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> S.HashSet StableName -> BareRTEnv -> Bare.SigEnv
makeSigEnv :: TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
makeSigEnv TCEmb TyCon
embs TyConMap
tyi HashSet StableName
exports BareRTEnv
rtEnv = Bare.SigEnv
{ sigEmbs :: TCEmb TyCon
sigEmbs = TCEmb TyCon
embs
, sigTyRTyMap :: TyConMap
sigTyRTyMap = TyConMap
tyi
, sigExports :: HashSet StableName
sigExports = HashSet StableName
exports
, sigRTEnv :: BareRTEnv
sigRTEnv = BareRTEnv
rtEnv
}
makeNewTypes :: Bare.Env -> Bare.SigEnv -> [(ModName, Ms.BareSpec)] ->
Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewTypes :: Env
-> SigEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec LocBareType LocSymbol)]
specs = do
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, DataDecl)]
nameDecls forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Env
-> SigEnv -> ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv)
where
nameDecls :: [(ModName, DataDecl)]
nameDecls = [(ModName
name, DataDecl
d) | (ModName
name, Spec LocBareType LocSymbol
spec) <- [(ModName, Spec LocBareType LocSymbol)]
specs, DataDecl
d <- forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.newtyDecls Spec LocBareType LocSymbol
spec]
makeNewType :: Bare.Env -> Bare.SigEnv -> ModName -> DataDecl ->
Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewType :: Env
-> SigEnv -> ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv ModName
name DataDecl
d = do
Maybe TyCon
tcMb <- Env -> ModName -> [Char] -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name [Char]
"makeNewType" DataName
tcName
case Maybe TyCon
tcMb of
Just TyCon
tc -> forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCon
tc, LocSpecType
lst)]
Maybe TyCon
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
where
tcName :: DataName
tcName = DataDecl -> DataName
tycName DataDecl
d
lst :: LocSpecType
lst = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.GenTV LocBareType
bt
bt :: LocBareType
bt = forall {a}. PPrint a => a -> SourcePos -> [DataCtor] -> LocBareType
getTy DataName
tcName (DataDecl -> SourcePos
tycSrcPos DataDecl
d) (forall a. a -> Maybe a -> a
Mb.fromMaybe [] (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d))
getTy :: a -> SourcePos -> [DataCtor] -> LocBareType
getTy a
_ SourcePos
l [DataCtor
c]
| [(Symbol
_, RType BTyCon BTyVar RReft
t)] <- DataCtor -> [(Symbol, RType BTyCon BTyVar RReft)]
dcFields DataCtor
c = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l RType BTyCon BTyVar RReft
t
getTy a
n SourcePos
l [DataCtor]
_ = forall a e. Exception e => e -> a
Ex.throw (forall {a}. PPrint a => a -> SourcePos -> UserError
mkErr a
n SourcePos
l)
mkErr :: a -> SourcePos -> UserError
mkErr a
n SourcePos
l = forall t. SrcSpan -> Doc -> TError t
ErrOther (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (Doc
"Bad new type declaration:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
F.pprint a
n) :: UserError
makeSpecData :: GhcSrc -> Bare.Env -> Bare.SigEnv -> Bare.MeasEnv -> GhcSpecSig -> Bare.ModSpecs
-> GhcSpecData
makeSpecData :: GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig HashMap ModName (Spec LocBareType LocSymbol)
specs = SpData
{ gsCtors :: [(TyVar, LocSpecType)]
gsCtors = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"GS-CTORS"
[ (TyVar
x, if Bool
allowTC then LocSpecType
t else LocSpecType
tt)
| (TyVar
x, LocSpecType
t) <- MeasEnv -> [(TyVar, LocSpecType)]
Bare.meDataCons MeasEnv
measEnv
, let tt :: LocSpecType
tt = Bool
-> SigEnv -> ModName -> PlugTV TyVar -> LocSpecType -> LocSpecType
Bare.plugHoles (Config -> Bool
typeclass forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig Env
env) SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.LqTV TyVar
x) LocSpecType
t
]
, gsMeas :: [(Symbol, LocSpecType)]
gsMeas = [ (forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (RRType Reft)
t) | (Symbol
x, Located (RRType Reft)
t) <- [(Symbol, Located (RRType Reft))]
measVars ]
, gsMeasures :: [Measure SpecType DataCon]
gsMeasures = forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Measure SpecType DataCon]
ms1 forall a. [a] -> [a] -> [a]
++ [Measure SpecType DataCon]
ms2)
, gsInvariants :: [(Maybe TyVar, LocSpecType)]
gsInvariants = forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (forall a. Located a -> SourcePos
F.loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Maybe TyVar, LocSpecType)]
invs
, gsIaliases :: [(LocSpecType, LocSpecType)]
gsIaliases = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec LocBareType LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
, gsUnsorted :: [UnSortedExpr]
gsUnsorted = [UnSortedExpr]
usI forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty ctor. Measure ty ctor -> [UnSortedExpr]
msUnSorted (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures HashMap ModName (Spec LocBareType LocSymbol)
specs)
}
where
allowTC :: Bool
allowTC = Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env)
measVars :: [(Symbol, Located (RRType Reft))]
measVars = MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv
forall a. [a] -> [a] -> [a]
++ MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv
forall a. [a] -> [a] -> [a]
++ forall r. Monoid r => Env -> [(Symbol, Located (RRType r))]
Bare.varMeasures Env
env
measuresSp :: MSpec SpecType DataCon
measuresSp = MeasEnv -> MSpec SpecType DataCon
Bare.meMeasureSpec MeasEnv
measEnv
ms1 :: [Measure SpecType DataCon]
ms1 = forall k v. HashMap k v -> [v]
M.elems (forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
Ms.measMap MSpec SpecType DataCon
measuresSp)
ms2 :: [Measure SpecType DataCon]
ms2 = forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
Ms.imeas MSpec SpecType DataCon
measuresSp
mySpec :: Spec LocBareType LocSymbol
mySpec = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
name :: ModName
name = GhcSrc -> ModName
_giTargetMod GhcSrc
src
([(Maybe TyVar, LocSpecType)]
minvs,[UnSortedExpr]
usI) = Env
-> ModName
-> GhcSpecSig
-> Spec LocBareType LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec LocBareType LocSymbol
mySpec
invs :: [(Maybe TyVar, LocSpecType)]
invs = [(Maybe TyVar, LocSpecType)]
minvs forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec LocBareType LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases :: Env
-> SigEnv
-> (ModName, Spec LocBareType LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv (ModName
name, Spec LocBareType LocSymbol
spec)
= [ (LocSpecType, LocSpecType)
z | Right (LocSpecType, LocSpecType)
z <- (LocBareType, LocBareType)
-> Either [Error] (LocSpecType, LocSpecType)
mkIA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr. Spec ty bndr -> [(ty, ty)]
Ms.ialiases Spec LocBareType LocSymbol
spec ]
where
mkIA :: (LocBareType, LocBareType)
-> Either [Error] (LocSpecType, LocSpecType)
mkIA (LocBareType
t1, LocBareType
t2) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocBareType -> Lookup LocSpecType
mkI' LocBareType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LocBareType -> Lookup LocSpecType
mkI' LocBareType
t2
mkI' :: LocBareType -> Lookup LocSpecType
mkI' = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> LocBareType
-> Lookup LocSpecType
Bare.cookSpecTypeE Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.GenTV
makeInvariants :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(Maybe Ghc.Var, Located SpecType)]
makeInvariants :: Env
-> SigEnv
-> (ModName, Spec LocBareType LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv (ModName
name, Spec LocBareType LocSymbol
spec) =
[ (forall a. Maybe a
Nothing, LocSpecType
t)
| (Maybe LocSymbol
_, LocBareType
bt) <- forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
Ms.invariants Spec LocBareType LocSymbol
spec
, Env -> ModName -> LocBareType -> Bool
Bare.knownGhcType Env
env ModName
name LocBareType
bt
, let t :: LocSpecType
t = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.GenTV LocBareType
bt
] forall a. [a] -> [a] -> [a]
++
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (forall a. Maybe a
Nothing,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> LocSpecType -> LocSpecType
makeSizeInv LocSymbol
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSpecType]
ts
| ([LocBareType]
bts, LocSymbol
l) <- forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
Ms.dsize Spec LocBareType LocSymbol
spec
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> ModName -> LocBareType -> Bool
Bare.knownGhcType Env
env ModName
name) [LocBareType]
bts
, let ts :: [LocSpecType]
ts = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.GenTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocBareType]
bts
]
makeSizeInv :: F.LocSymbol -> Located SpecType -> Located SpecType
makeSizeInv :: LocSymbol -> LocSpecType -> LocSpecType
makeSizeInv LocSymbol
s LocSpecType
lst = LocSpecType
lst{val :: SpecType
val = forall {c} {tv}. RType c tv RReft -> RType c tv RReft
go (forall a. Located a -> a
val LocSpecType
lst)}
where go :: RType c tv RReft -> RType c tv RReft
go (RApp c
c [RType c tv RReft]
ts [RTProp c tv RReft]
rs RReft
r) = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv RReft]
ts [RTProp c tv RReft]
rs (RReft
r forall r. Reftable r => r -> r -> r
`meet` RReft
nat)
go (RAllT RTVU c tv
a RType c tv RReft
t RReft
r) = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv RReft -> RType c tv RReft
go RType c tv RReft
t) RReft
r
go RType c tv RReft
t = RType c tv RReft
t
nat :: RReft
nat = forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
Reft (Symbol
vv_, Brel -> Expr -> Expr -> Expr
PAtom Brel
Le (Constant -> Expr
ECon forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0) (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSymbol
s) (forall a. Symbolic a => a -> Expr
eVar Symbol
vv_))))
forall a. Monoid a => a
mempty
makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec
-> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants :: Env
-> ModName
-> GhcSpecSig
-> Spec LocBareType LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec LocBareType LocSymbol
mySpec
= forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd forall a. [Maybe a] -> [a]
Mb.catMaybes forall a b. (a -> b) -> a -> b
$
forall a b. [(a, b)] -> ([a], [b])
unzip (Env
-> ModName
-> (LocSymbol, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv Env
env ModName
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol
x, (TyVar
y, LocSpecType
ty)) | LocSymbol
x <- [LocSymbol]
xs, (TyVar
y, LocSpecType
ty) <- [(TyVar, LocSpecType)]
sigs
, Symbol -> TyVar -> Bool
isSymbolOfVar (forall a. Located a -> a
val LocSymbol
x) TyVar
y ])
where
sigs :: [(TyVar, LocSpecType)]
sigs = GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
sig
xs :: [LocSymbol]
xs = forall a. HashSet a -> [a]
S.toList (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec LocBareType LocSymbol
mySpec)
isSymbolOfVar :: Symbol -> Ghc.Var -> Bool
isSymbolOfVar :: Symbol -> TyVar -> Bool
isSymbolOfVar Symbol
x TyVar
v = Symbol
x forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
symbol' TyVar
v
where
symbol' :: Ghc.Var -> Symbol
symbol' :: TyVar -> Symbol
symbol' = Symbol -> Symbol
GM.dropModuleNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedThing a => a -> Name
Ghc.getName
measureTypeToInv :: Bare.Env -> ModName -> (LocSymbol, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv :: Env
-> ModName
-> (LocSymbol, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv Env
env ModName
name (LocSymbol
x, (TyVar
v, LocSpecType
t))
= forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"measureTypeToInv" ((forall a. a -> Maybe a
Just TyVar
v, LocSpecType
t {val :: SpecType
val = forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop Env
env ModName
name (forall a. Located a -> SourcePos
F.loc LocSymbol
x) SpecType
mtype}), Maybe UnSortedExpr
usorted)
where
trep :: RTypeRep RTyCon RTyVar RReft
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (forall a. Located a -> a
val LocSpecType
t)
rts :: [SpecType]
rts = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep
args :: [Symbol]
args = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep
res :: SpecType
res = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep
z :: Symbol
z = forall a. [a] -> a
last [Symbol]
args
tz :: SpecType
tz = forall a. [a] -> a
last [SpecType]
rts
usorted :: Maybe UnSortedExpr
usorted = if forall {c} {tv} {r}. RType c tv r -> Bool
isSimpleADT SpecType
tz then forall a. Maybe a
Nothing else forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft (forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v) Symbol
z SpecType
tz SpecType
res
mtype :: SpecType
mtype
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecType]
rts
= forall a. UserError -> a
uError forall a b. (a -> b) -> a -> b
$ forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc LocSpecType
t) (forall a. PPrint a => a -> Doc
pprint LocSymbol
x) Doc
"Measure has no arguments!"
| Bool
otherwise
= LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant LocSymbol
x Symbol
z SpecType
tz SpecType
res
isSimpleADT :: RType c tv r -> Bool
isSimpleADT (RApp c
_ [RType c tv r]
ts [RTProp c tv r]
_ r
_) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {c} {tv} {r}. RType c tv r -> Bool
isRVar [RType c tv r]
ts
isSimpleADT RType c tv r
_ = Bool
False
mkInvariant :: LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant :: LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant LocSymbol
x Symbol
z SpecType
t SpecType
tr = forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen (forall r. Reftable r => r -> r
top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t) (forall r. r -> Predicate -> UReft r
MkUReft Reft
reft' forall a. Monoid a => a
mempty)
where
reft' :: Reft
reft' = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe forall a. Monoid a => a
mempty (Symbol, Expr) -> Reft
Reft Maybe (Symbol, Expr)
mreft
mreft :: Maybe (Symbol, Expr)
mreft = LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft LocSymbol
x Symbol
z SpecType
t SpecType
tr
mkReft :: LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft :: LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft LocSymbol
x Symbol
z SpecType
_t SpecType
tr
| Just RReft
q <- forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
tr
= let Reft (Symbol
v, Expr
p) = forall r. Reftable r => r -> Reft
toReft RReft
q
su :: Subst
su = [(Symbol, Expr)] -> Subst
mkSubst [(Symbol
v, LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
x [Symbol -> Expr
EVar Symbol
v]), (Symbol
z,Symbol -> Expr
EVar Symbol
v)]
in forall a. a -> Maybe a
Just (Symbol
v, forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p)
mkReft LocSymbol
_ Symbol
_ SpecType
_ SpecType
_
= forall a. Maybe a
Nothing
makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
makeSpecName :: Env -> TycEnv -> MeasEnv -> ModName -> GhcSpecNames
makeSpecName Env
env TycEnv
tycEnv MeasEnv
measEnv ModName
name = SpNames
{ gsFreeSyms :: [(Symbol, TyVar)]
gsFreeSyms = Env -> [(Symbol, TyVar)]
Bare.reSyms Env
env
, gsDconsP :: [Located DataCon]
gsDconsP = [ forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dc (DataConP -> DataCon
dcpCon DataConP
dc) | DataConP
dc <- [DataConP]
datacons forall a. [a] -> [a] -> [a]
++ [DataConP]
cls ]
, gsTconsP :: [TyConP]
gsTconsP = forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyConP]
tycons
, gsTcEmbeds :: TCEmb TyCon
gsTcEmbeds = TycEnv -> TCEmb TyCon
Bare.tcEmbs TycEnv
tycEnv
, gsADTs :: [DataDecl]
gsADTs = TycEnv -> [DataDecl]
Bare.tcAdts TycEnv
tycEnv
, gsTyconEnv :: TyConMap
gsTyconEnv = TycEnv -> TyConMap
Bare.tcTyConMap TycEnv
tycEnv
}
where
datacons, cls :: [DataConP]
datacons :: [DataConP]
datacons = TycEnv -> [DataConP]
Bare.tcDataCons TycEnv
tycEnv
cls :: [DataConP]
cls = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"meClasses" forall a b. (a -> b) -> a -> b
$ MeasEnv -> [DataConP]
Bare.meClasses MeasEnv
measEnv
tycons :: [TyConP]
tycons = TycEnv -> [TyConP]
Bare.tcTyCons TycEnv
tycEnv
makeTycEnv0 :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs
-> (Diagnostics, [Located DataConP], Bare.TycEnv)
makeTycEnv0 :: Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec LocBareType LocSymbol
-> HashMap ModName (Spec LocBareType LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
myName Env
env TCEmb TyCon
embs Spec LocBareType LocSymbol
mySpec HashMap ModName (Spec LocBareType LocSymbol)
iSpecs = (Diagnostics
diag0 forall a. Semigroup a => a -> a -> a
<> Diagnostics
diag1, [Located DataConP]
datacons, Bare.TycEnv
{ tcTyCons :: [TyConP]
tcTyCons = [TyConP]
tycons
, tcDataCons :: [DataConP]
tcDataCons = forall a. Monoid a => a
mempty
, tcSelMeasures :: [Measure SpecType DataCon]
tcSelMeasures = [Measure SpecType DataCon]
dcSelectors
, tcSelVars :: [(TyVar, LocSpecType)]
tcSelVars = forall a. Monoid a => a
mempty
, tcTyConMap :: TyConMap
tcTyConMap = TyConMap
tyi
, tcAdts :: [DataDecl]
tcAdts = [DataDecl]
adts
, tcDataConMap :: DataConMap
tcDataConMap = DataConMap
dm
, tcEmbs :: TCEmb TyCon
tcEmbs = TCEmb TyCon
embs
, tcName :: ModName
tcName = ModName
myName
})
where
([(ModName, TyConP, Maybe DataPropDecl)]
tcDds, [[Located DataConP]]
dcs) = ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
conTys
(Diagnostics
diag0, ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
conTys) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ ModName
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes ModName
myName Env
env [(ModName, Spec LocBareType LocSymbol)]
specs
specs :: [(ModName, Spec LocBareType LocSymbol)]
specs = (ModName
myName, Spec LocBareType LocSymbol
mySpec) forall a. a -> [a] -> [a]
: forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
iSpecs
tcs :: [TyConP]
tcs = forall a b c. (a, b, c) -> b
Misc.snd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, TyConP, Maybe DataPropDecl)]
tcDds
tyi :: TyConMap
tyi = forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
myName (TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
makeTyConInfo TCEmb TyCon
embs [TyCon]
fiTcs [TyConP]
tycons)
tycons :: [TyConP]
tycons = [TyConP]
tcs forall a. [a] -> [a] -> [a]
++ Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
myName
datacons :: [Located DataConP]
datacons = Bool
-> TCEmb TyCon -> TyConMap -> Located DataConP -> Located DataConP
Bare.makePluggedDataCon (Config -> Bool
typeclass Config
cfg) TCEmb TyCon
embs TyConMap
tyi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs forall a. [a] -> [a] -> [a]
++ Env -> ModName -> [Located DataConP]
knownWiredDataCons Env
env ModName
myName)
tds :: [(ModName, TyCon, DataPropDecl)]
tds = [(ModName
name, TyConP -> TyCon
tcpCon TyConP
tcp, DataPropDecl
dd) | (ModName
name, TyConP
tcp, Just DataPropDecl
dd) <- [(ModName, TyConP, Maybe DataPropDecl)]
tcDds]
(Diagnostics
diag1, [DataDecl]
adts) = Config
-> TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [DataDecl])
Bare.makeDataDecls Config
cfg TCEmb TyCon
embs ModName
myName [(ModName, TyCon, DataPropDecl)]
tds [Located DataConP]
datacons
dm :: DataConMap
dm = [DataDecl] -> DataConMap
Bare.dataConMap [DataDecl]
adts
dcSelectors :: [Measure SpecType DataCon]
dcSelectors = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Config
-> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
Bare.makeMeasureSelectors Config
cfg DataConMap
dm) (if Config -> Bool
reflection Config
cfg then Located DataConP
charDataConforall a. a -> [a] -> [a]
:[Located DataConP]
datacons else [Located DataConP]
datacons)
fiTcs :: [TyCon]
fiTcs = GhcSrc -> [TyCon]
_gsFiTcs (Env -> GhcSrc
Bare.reSrc Env
env)
makeTycEnv1 ::
ModName
-> Bare.Env
-> (Bare.TycEnv, [Located DataConP])
-> (Ghc.CoreExpr -> F.Expr)
-> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr)
-> Ghc.TcRn Bare.TycEnv
makeTycEnv1 :: ModName
-> Env
-> (TycEnv, [Located DataConP])
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> TcRn TycEnv
makeTycEnv1 ModName
myName Env
env (TycEnv
tycEnv, [Located DataConP]
datacons) CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier = do
[Located (DataConP, DataConP)]
lclassdcs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Located DataConP]
classdcs forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> TcRn (DataConP, DataConP)
Bare.elaborateClassDcp CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
let recSelectors :: [(TyVar, LocSpecType)]
recSelectors = Env -> ModName -> [Located DataConP] -> [(TyVar, LocSpecType)]
Bare.makeRecordSelectorSigs Env
env ModName
myName ([Located DataConP]
dcs forall a. [a] -> [a] -> [a]
++ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a b. (a, b) -> b
snd [Located (DataConP, DataConP)]
lclassdcs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
TycEnv
tycEnv {tcSelVars :: [(TyVar, LocSpecType)]
Bare.tcSelVars = [(TyVar, LocSpecType)]
recSelectors, tcDataCons :: [DataConP]
Bare.tcDataCons = forall a. Located a -> a
F.val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a b. (a, b) -> a
fst [Located (DataConP, DataConP)]
lclassdcs forall a. [a] -> [a] -> [a]
++ [Located DataConP]
dcs )}
where
([Located DataConP]
classdcs, [Located DataConP]
dcs) =
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition
(TyCon -> Bool
Ghc.isClassTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCon
Ghc.dataConTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val) [Located DataConP]
datacons
knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP]
knownWiredDataCons :: Env -> ModName -> [Located DataConP]
knownWiredDataCons Env
env ModName
name = forall a. (a -> Bool) -> [a] -> [a]
filter Located DataConP -> Bool
isKnown [Located DataConP]
wiredDataCons
where
isKnown :: Located DataConP -> Bool
isKnown = Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcDataCon Env
env ModName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val
knownWiredTyCons :: Bare.Env -> ModName -> [TyConP]
knownWiredTyCons :: Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
name = forall a. (a -> Bool) -> [a] -> [a]
filter TyConP -> Bool
isKnown [TyConP]
wiredTyCons
where
isKnown :: TyConP -> Bool
isKnown = Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcTyCon Env
env ModName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConP -> TyCon
tcpCon
makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs ->
Bare.Lookup Bare.MeasEnv
makeMeasEnv :: Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec LocBareType LocSymbol)
specs = do
[(Class, [(ModName, TyVar, LocSpecType)])]
laws <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.makeCLaws Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
([DataConP]
cls, [(ModName, TyVar, LocSpecType)]
mts) <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup ([DataConP], [(ModName, TyVar, LocSpecType)])
Bare.makeClasses Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
let dms :: [(ModName, TyVar, LocSpecType)]
dms = Env
-> [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
Bare.makeDefaultMethods Env
env [(ModName, TyVar, LocSpecType)]
mts
[MSpec SpecType DataCon]
measures0 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env
-> SigEnv
-> ModName
-> (ModName, Spec LocBareType LocSymbol)
-> Lookup (MSpec SpecType DataCon)
Bare.makeMeasureSpec Env
env SigEnv
sigEnv ModName
name) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
let measures :: MSpec SpecType DataCon
measures = forall a. Monoid a => [a] -> a
mconcat (forall ctor ty. Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
Ms.mkMSpec' [Measure SpecType DataCon]
dcSelectors forall a. a -> [a] -> [a]
: [MSpec SpecType DataCon]
measures0)
let ([(TyVar, SpecType)]
cs, [(LocSymbol, RRType Reft)]
ms) = Bool
-> MSpec SpecType DataCon
-> ([(TyVar, SpecType)], [(LocSymbol, RRType Reft)])
Bare.makeMeasureSpec' (Config -> Bool
typeclass forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig Env
env) MSpec SpecType DataCon
measures
let cms :: [(LocSymbol, CMeasure (RRType Reft))]
cms = forall c tv r2 t.
MSpec (RType c tv (UReft r2)) t
-> [(LocSymbol, CMeasure (RType c tv r2))]
Bare.makeClassMeasureSpec MSpec SpecType DataCon
measures
let cms' :: [(Symbol, Located (RRType Reft))]
cms' = [ (Symbol
x, forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' forall a b. (a -> b) -> a -> b
$ forall ty. CMeasure ty -> ty
cSort CMeasure (RRType Reft)
t) | (Loc SourcePos
l SourcePos
l' Symbol
x, CMeasure (RRType Reft)
t) <- [(LocSymbol, CMeasure (RRType Reft))]
cms ]
let ms' :: [(Symbol, Located (RRType Reft))]
ms' = [ (forall a. Located a -> a
F.val LocSymbol
lx, forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lx RRType Reft
t) | (LocSymbol
lx, RRType Reft
t) <- [(LocSymbol, RRType Reft)]
ms
, forall a. Maybe a -> Bool
Mb.isNothing (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall a. Located a -> a
val LocSymbol
lx) [(Symbol, Located (RRType Reft))]
cms') ]
let cs' :: [(TyVar, LocSpecType)]
cs' = [ (TyVar
v, forall {b}. NamedThing b => b -> SpecType -> LocSpecType
txRefs TyVar
v SpecType
t) | (TyVar
v, SpecType
t) <- Bool
-> TCEmb TyCon
-> [(TyVar, SpecType)]
-> [DataConP]
-> [(TyVar, SpecType)]
Bare.meetDataConSpec (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(TyVar, SpecType)]
cs ([DataConP]
datacons forall a. [a] -> [a] -> [a]
++ [DataConP]
cls)]
forall (m :: * -> *) a. Monad m => a -> m a
return Bare.MeasEnv
{ meMeasureSpec :: MSpec SpecType DataCon
meMeasureSpec = MSpec SpecType DataCon
measures
, meClassSyms :: [(Symbol, Located (RRType Reft))]
meClassSyms = [(Symbol, Located (RRType Reft))]
cms'
, meSyms :: [(Symbol, Located (RRType Reft))]
meSyms = [(Symbol, Located (RRType Reft))]
ms'
, meDataCons :: [(TyVar, LocSpecType)]
meDataCons = [(TyVar, LocSpecType)]
cs'
, meClasses :: [DataConP]
meClasses = [DataConP]
cls
, meMethods :: [(ModName, TyVar, LocSpecType)]
meMethods = [(ModName, TyVar, LocSpecType)]
mts forall a. [a] -> [a] -> [a]
++ [(ModName, TyVar, LocSpecType)]
dms
, meCLaws :: [(Class, [(ModName, TyVar, LocSpecType)])]
meCLaws = [(Class, [(ModName, TyVar, LocSpecType)])]
laws
}
where
txRefs :: b -> SpecType -> LocSpecType
txRefs b
v SpecType
t = TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (SpecType
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. NamedThing a => a -> Located a
GM.locNamedThing b
v)
tyi :: TyConMap
tyi = TycEnv -> TyConMap
Bare.tcTyConMap TycEnv
tycEnv
dcSelectors :: [Measure SpecType DataCon]
dcSelectors = TycEnv -> [Measure SpecType DataCon]
Bare.tcSelMeasures TycEnv
tycEnv
datacons :: [DataConP]
datacons = TycEnv -> [DataConP]
Bare.tcDataCons TycEnv
tycEnv
embs :: TCEmb TyCon
embs = TycEnv -> TCEmb TyCon
Bare.tcEmbs TycEnv
tycEnv
name :: ModName
name = TycEnv -> ModName
Bare.tcName TycEnv
tycEnv
makeLiftedSpec :: ModName -> GhcSrc -> Bare.Env
-> GhcSpecRefl -> GhcSpecData -> GhcSpecSig -> GhcSpecQual -> BareRTEnv
-> Ms.BareSpec -> Ms.BareSpec
makeLiftedSpec :: ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
_env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE Spec LocBareType LocSymbol
lSpec0 = Spec LocBareType LocSymbol
lSpec0
{ asmSigs :: [(LocSymbol, LocBareType)]
Ms.asmSigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"makeLiftedSpec : ASSUMED-SIGS " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name ) ([(LocSymbol, LocBareType)]
xbs forall a. [a] -> [a] -> [a]
++ [(LocSymbol, LocBareType)]
myDCs)
, reflSigs :: [(LocSymbol, LocBareType)]
Ms.reflSigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"REFL-SIGS" [(LocSymbol, LocBareType)]
xbs
, sigs :: [(LocSymbol, LocBareType)]
Ms.sigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"makeLiftedSpec : LIFTED-SIGS " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name ) forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
sig)
, invariants :: [(Maybe LocSymbol, LocBareType)]
Ms.invariants = [ (TyVar -> LocSymbol
varLocSym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe TyVar
x, SpecType -> RType BTyCon BTyVar RReft
Bare.specToBare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSpecType
t)
| (Maybe TyVar
x, LocSpecType
t) <- GhcSpecData -> [(Maybe TyVar, LocSpecType)]
gsInvariants GhcSpecData
sData
, forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF LocSpecType
t
]
, axeqs :: [Equation]
Ms.axeqs = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
refl
, aliases :: [Located BareRTAlias]
Ms.aliases = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"MY-ALIASES" forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases forall a b. (a -> b) -> a -> b
$ BareRTEnv
myRTE
, ealiases :: [Located (RTAlias Symbol Expr)]
Ms.ealiases = forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases forall a b. (a -> b) -> a -> b
$ BareRTEnv
myRTE
, qualifiers :: [Qualifier]
Ms.qualifiers = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) (GhcSpecQual -> [Qualifier]
gsQualifiers GhcSpecQual
qual)
}
where
myDCs :: [(LocSymbol, LocBareType)]
myDCs = [(LocSymbol
x,LocBareType
t) | (LocSymbol
x,LocBareType
t) <- forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs (GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors GhcSpecData
sData)
, forall a. Symbolic a => a -> Symbol
F.symbol ModName
name forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst (Symbol -> (Symbol, Symbol)
GM.splitModuleName forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSymbol
x)]
mkSigs :: [(TyVar, f SpecType)]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs [(TyVar, f SpecType)]
xts = [ forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare (TyVar
x, f SpecType
t) | (TyVar
x, f SpecType
t) <- [(TyVar, f SpecType)]
xts
, forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyVar
x HashSet TyVar
sigVars Bool -> Bool -> Bool
&& TargetSrc -> TyVar -> Bool
isExportedVar (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src) TyVar
x
]
toBare :: (TyVar, f SpecType) -> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare (TyVar
x, f SpecType
t) = (TyVar -> LocSymbol
varLocSym TyVar
x, SpecType -> RType BTyCon BTyVar RReft
Bare.specToBare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SpecType
t)
xbs :: [(LocSymbol, LocBareType)]
xbs = forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs
sigVars :: HashSet TyVar
sigVars = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet TyVar
defVars HashSet TyVar
reflVars
defVars :: HashSet TyVar
defVars = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (GhcSrc -> [TyVar]
_giDefVars GhcSrc
src)
reflTySigs :: [(TyVar, LocSpecType)]
reflTySigs = [(TyVar
x, LocSpecType
t) | (TyVar
x,LocSpecType
t,Equation
_) <- GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl, TyVar
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl]
reflVars :: HashSet TyVar
reflVars = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs)
srcF :: [Char]
srcF = GhcSrc -> [Char]
_giTarget GhcSrc
src
isLocInFile :: (F.Loc a) => FilePath -> a -> Bool
isLocInFile :: forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
f a
lx = [Char]
f forall a. Eq a => a -> a -> Bool
== [Char]
lifted Bool -> Bool -> Bool
|| Bool
isCompanion
where
lifted :: FilePath
lifted :: [Char]
lifted = forall a. Loc a => a -> [Char]
locFile a
lx
isCompanion :: Bool
isCompanion :: Bool
isCompanion =
forall a. Eq a => a -> a -> Bool
(==) ([Char] -> [Char]
dropExtension [Char]
f) ([Char] -> [Char]
dropExtension [Char]
lifted)
Bool -> Bool -> Bool
&& Ext -> [Char] -> Bool
isExtFile Ext
Hs [Char]
f
Bool -> Bool -> Bool
&& Ext -> [Char] -> Bool
isExtFile Ext
Files.Spec [Char]
lifted
locFile :: (F.Loc a) => a -> FilePath
locFile :: forall a. Loc a => a -> [Char]
locFile = forall a b c. (a, b, c) -> a
Misc.fst3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> ([Char], Line, Line)
F.sourcePosElts forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> SourcePos
F.sp_start forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Loc a => a -> SrcSpan
F.srcSpan
varLocSym :: Ghc.Var -> LocSymbol
varLocSym :: TyVar -> LocSymbol
varLocSym TyVar
v = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedThing a => a -> Located a
GM.locNamedThing TyVar
v
myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv :: GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv = forall x a.
[Located (RTAlias x a)]
-> [Located (RTAlias Symbol Expr)] -> RTEnv x a
mkRTE [Located BareRTAlias]
tAs' [Located (RTAlias Symbol Expr)]
eAs
where
tAs' :: [Located BareRTAlias]
tAs' = Env
-> SigEnv -> ModName -> Located BareRTAlias -> Located BareRTAlias
normalizeBareAlias Env
env SigEnv
sigEnv ModName
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareRTAlias]
tAs
tAs :: [Located BareRTAlias]
tAs = forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases
eAs :: [Located (RTAlias Symbol Expr)]
eAs = forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases
myAliases :: (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap k a
fld = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> HashMap k a
fld forall a b. (a -> b) -> a -> b
$ BareRTEnv
rtEnv
srcF :: [Char]
srcF = GhcSrc -> [Char]
_giTarget GhcSrc
src
name :: ModName
name = GhcSrc -> ModName
_giTargetMod GhcSrc
src
mkRTE :: [Located (RTAlias x a)] -> [Located (RTAlias F.Symbol F.Expr)] -> RTEnv x a
mkRTE :: forall x a.
[Located (RTAlias x a)]
-> [Located (RTAlias Symbol Expr)] -> RTEnv x a
mkRTE [Located (RTAlias x a)]
tAs [Located (RTAlias Symbol Expr)]
eAs = RTE
{ typeAliases :: HashMap Symbol (Located (RTAlias x a))
typeAliases = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall {x} {a}. Located (RTAlias x a) -> Symbol
aName Located (RTAlias x a)
a, Located (RTAlias x a)
a) | Located (RTAlias x a)
a <- [Located (RTAlias x a)]
tAs ]
, exprAliases :: HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall {x} {a}. Located (RTAlias x a) -> Symbol
aName Located (RTAlias Symbol Expr)
a, Located (RTAlias Symbol Expr)
a) | Located (RTAlias Symbol Expr)
a <- [Located (RTAlias Symbol Expr)]
eAs ]
}
where aName :: Located (RTAlias x a) -> Symbol
aName = forall x a. RTAlias x a -> Symbol
rtName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val
normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> Located BareRTAlias
-> Located BareRTAlias
normalizeBareAlias :: Env
-> SigEnv -> ModName -> Located BareRTAlias -> Located BareRTAlias
normalizeBareAlias Env
env SigEnv
sigEnv ModName
name Located BareRTAlias
lx = BareRTAlias -> BareRTAlias
fixRTA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareRTAlias
lx
where
fixRTA :: BareRTAlias -> BareRTAlias
fixRTA :: BareRTAlias -> BareRTAlias
fixRTA = forall a b ty. (a -> b) -> RTAlias a ty -> RTAlias b ty
mapRTAVars Symbol -> Symbol
fixArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RType BTyCon BTyVar RReft -> RType BTyCon BTyVar RReft
fixBody
fixArg :: Symbol -> Symbol
fixArg :: Symbol -> Symbol
fixArg = forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TyVar
GM.symbolTyVar
fixBody :: BareType -> BareType
fixBody :: RType BTyCon BTyVar RReft -> RType BTyCon BTyVar RReft
fixBody = SpecType -> RType BTyCon BTyVar RReft
Bare.specToBare
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.RawTV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l b. Loc l => l -> b -> Located b
F.atLoc Located BareRTAlias
lx
withDiagnostics :: (Monoid a) => Bare.Lookup a -> (Diagnostics, a)
withDiagnostics :: forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Left [Error]
es) = ([Warning] -> [Error] -> Diagnostics
mkDiagnostics [] [Error]
es, forall a. Monoid a => a
mempty)
withDiagnostics (Right a
v) = (Diagnostics
emptyDiagnostics, a
v)