{-# 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 (Located BareType) LocSymbol))
loadLiftedSpec Config
cfg [Char]
srcF
| Config -> Bool
noLiftedImport Config
cfg = [Char] -> IO ()
putStrLn [Char]
"No LIFTED Import" IO ()
-> IO (Maybe (Spec (Located BareType) LocSymbol))
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Spec (Located BareType) LocSymbol)
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 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Loading Binary Lifted Spec: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
specF [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"for source-file: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
srcF [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Show a => a -> [Char]
show Bool
ex
Maybe (Spec (Located BareType) LocSymbol)
lSp <- if Bool
ex
then Spec (Located BareType) LocSymbol
-> Maybe (Spec (Located BareType) LocSymbol)
forall a. a -> Maybe a
Just (Spec (Located BareType) LocSymbol
-> Maybe (Spec (Located BareType) LocSymbol))
-> IO (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO (Spec (Located BareType) LocSymbol)
forall a. Binary a => [Char] -> IO a
B.decodeFile [Char]
specF
else Maybe (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Spec (Located BareType) LocSymbol)
forall a. Maybe a
Nothing
Maybe (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a. a -> IO a
Ex.evaluate Maybe (Spec (Located BareType) LocSymbol)
lSp
saveLiftedSpec :: FilePath -> Ms.BareSpec -> IO ()
saveLiftedSpec :: [Char] -> Spec (Located BareType) LocSymbol -> IO ()
saveLiftedSpec [Char]
srcF Spec (Located BareType) LocSymbol
lspec = do
[Char] -> IO ()
ensurePath [Char]
specF
[Char] -> Spec (Located BareType) LocSymbol -> IO ()
forall a. Binary a => [Char] -> a -> IO ()
B.encodeFile [Char]
specF Spec (Located BareType) 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 = ((ModName, Spec (Located BareType) LocSymbol)
-> Either Diagnostics ())
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Either Diagnostics [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((ModName
-> Spec (Located BareType) LocSymbol -> Either Diagnostics ())
-> (ModName, Spec (Located BareType) LocSymbol)
-> Either Diagnostics ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ModName
-> Spec (Located BareType) LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec) [(ModName, Spec (Located BareType) LocSymbol)]
legacyDependencies
let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = ModName
-> Spec (Located BareType) LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc) Spec (Located BareType) LocSymbol
legacyBareSpec
case Either Diagnostics ()
targDiagnostics Either Diagnostics ()
-> Either Diagnostics [()] -> Either Diagnostics [()]
forall a b.
Either Diagnostics a
-> Either Diagnostics b -> Either Diagnostics b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics [()]
depsDiagnostics Either Diagnostics [()]
-> Either Diagnostics () -> Either Diagnostics ()
forall a b.
Either Diagnostics a
-> Either Diagnostics b -> Either Diagnostics b
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 -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a b. (a -> b) -> a -> b
$ Diagnostics
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a b. a -> Either a b
Left Diagnostics
d
Right () -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Warning]
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 (Located BareType) LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg (TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
targetSrc) LogicMap
lmap (Spec (Located BareType) LocSymbol
-> [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs Spec (Located BareType) LocSymbol
legacyBareSpec)
Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
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
([Warning], TargetSpec, LiftedSpec)
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
phaseOneWarns [Warning] -> [Warning] -> [Warning]
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 (Located BareType) LocSymbol)
toLegacyDep (StableModule
sm, LiftedSpec
ls) = (ModType -> ModuleName -> ModName
ModName ModType
SrcImport (GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
Ghc.moduleName (GenModule Unit -> ModuleName)
-> (StableModule -> GenModule Unit) -> StableModule -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StableModule -> GenModule Unit
Ghc.unStableModule (StableModule -> ModuleName) -> StableModule -> ModuleName
forall a b. (a -> b) -> a -> b
$ StableModule
sm), LiftedSpec -> Spec (Located BareType) LocSymbol
unsafeFromLiftedSpec LiftedSpec
ls)
toLegacyTarget :: Ms.BareSpec -> (ModName, Ms.BareSpec)
toLegacyTarget :: Spec (Located BareType) LocSymbol
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyTarget Spec (Located BareType) LocSymbol
validatedSpec = (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc, Spec (Located BareType) LocSymbol
validatedSpec)
legacyDependencies :: [(ModName, Ms.BareSpec)]
legacyDependencies :: [(ModName, Spec (Located BareType) LocSymbol)]
legacyDependencies = ((StableModule, LiftedSpec)
-> (ModName, Spec (Located BareType) LocSymbol))
-> [(StableModule, LiftedSpec)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map (StableModule, LiftedSpec)
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyDep ([(StableModule, LiftedSpec)]
-> [(ModName, Spec (Located BareType) LocSymbol)])
-> (TargetDependencies -> [(StableModule, LiftedSpec)])
-> TargetDependencies
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)])
-> (TargetDependencies -> HashMap StableModule LiftedSpec)
-> TargetDependencies
-> [(StableModule, LiftedSpec)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies (TargetDependencies
-> [(ModName, Spec (Located BareType) LocSymbol)])
-> TargetDependencies
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a b. (a -> b) -> a -> b
$ TargetDependencies
dependencies
allSpecs :: Ms.BareSpec -> [(ModName, Ms.BareSpec)]
allSpecs :: Spec (Located BareType) LocSymbol
-> [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs Spec (Located BareType) LocSymbol
validSpec = Spec (Located BareType) LocSymbol
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyTarget Spec (Located BareType) LocSymbol
validSpec (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. a -> [a] -> [a]
: [(ModName, Spec (Located BareType) LocSymbol)]
legacyDependencies
legacyBareSpec :: Spec LocBareType F.LocSymbol
legacyBareSpec :: Spec (Located BareType) LocSymbol
legacyBareSpec = BareSpec -> Spec (Located BareType) LocSymbol
fromBareSpec BareSpec
bareSpec
makeGhcSpec :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Ms.BareSpec)]
-> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
validatedSpecs = do
(Diagnostics
dg0, GhcSpec
sp) <- Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
validatedSpecs
let diagnostics :: Either Diagnostics ()
diagnostics = [Spec (Located BareType) LocSymbol]
-> TargetSrc
-> SEnv SortedReft
-> [CoreBind]
-> TargetSpec
-> Either Diagnostics ()
Bare.checkTargetSpec (((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [Spec (Located BareType) LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd [(ModName, Spec (Located BareType) LocSymbol)]
validatedSpecs)
(GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src)
(GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp)
(GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
((TargetSpec, LiftedSpec) -> TargetSpec
forall a b. (a, b) -> a
fst ((TargetSpec, LiftedSpec) -> TargetSpec)
-> (GhcSpec -> (TargetSpec, LiftedSpec)) -> GhcSpec -> TargetSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec (GhcSpec -> TargetSpec) -> GhcSpec -> TargetSpec
forall a b. (a -> b) -> a -> b
$ GhcSpec
sp)
Either Diagnostics ([Warning], GhcSpec)
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Diagnostics ([Warning], GhcSpec)
-> TcRn (Either Diagnostics ([Warning], GhcSpec)))
-> Either Diagnostics ([Warning], GhcSpec)
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not (Diagnostics -> Bool
noErrors Diagnostics
dg0) then Diagnostics -> Either Diagnostics ([Warning], GhcSpec)
forall a b. a -> Either a b
Left Diagnostics
dg0 else
case Either Diagnostics ()
diagnostics of
Left Diagnostics
dg1
| Diagnostics -> Bool
noErrors Diagnostics
dg1 -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics -> [Warning]
allWarnings Diagnostics
dg1, GhcSpec
sp)
| Bool
otherwise -> Diagnostics -> Either Diagnostics ([Warning], GhcSpec)
forall a b. a -> Either a b
Left Diagnostics
dg1
Right () -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
forall a. Monoid a => a
mempty, GhcSpec
sp)
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp = [Char] -> SEnv SortedReft -> SEnv SortedReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RENV" (SEnv SortedReft -> SEnv SortedReft)
-> SEnv SortedReft -> SEnv SortedReft
forall a b. (a -> b) -> a -> b
$ [(Symbol, SortedReft)] -> SEnv SortedReft
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 = [Char] -> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"binds" ([(Symbol, SortedReft)] -> [(Symbol, SortedReft)])
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> a -> b
$ [[(Symbol, SortedReft)]] -> [(Symbol, SortedReft)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [(Symbol
x, SpecType -> SortedReft
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)]
, [(TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v, SpecType -> SortedReft
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)]
, [(TyVar -> Symbol
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 Reft
forall a. Monoid a => a
mempty) | (Symbol
x, Sort
s) <- [(Symbol, Sort)]
wiredSortedSyms ]
, [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s Reft
forall a. Monoid a => a
mempty) | (Symbol
x, Sort
s) <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp ]
]
vSort :: TyVar -> SortedReft
vSort = SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort (SpecType -> SortedReft)
-> (TyVar -> SpecType) -> TyVar -> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SpecType -> SpecType
forall c tv r. Bool -> RType c tv r -> RType c tv r
classRFInfoType (Config -> Bool
typeclass (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ GhcSpec -> Config
forall t. HasConfig t => t -> Config
getConfig GhcSpec
sp) (SpecType -> SpecType) -> (TyVar -> SpecType) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType :: Ghc.Type -> SpecType) (Type -> SpecType) -> (TyVar -> Type) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
rSort :: RRType r -> SortedReft
rSort = TCEmb TyCon -> RRType r -> SortedReft
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 (Located BareType) LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) 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 (Located BareType) LocSymbol
lSpec1 = Spec (Located BareType) LocSymbol
lSpec0 Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a. Semigroup a => a -> a -> a
<> Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec1
let mySpec :: Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
mySpec2 Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a. Semigroup a => a -> a -> a
<> Spec (Located BareType) LocSymbol
lSpec1
let specs :: HashMap ModName (Spec (Located BareType) LocSymbol)
specs = ModName
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec (Located BareType) LocSymbol
mySpec HashMap ModName (Spec (Located BareType) 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) = Lookup MeasEnv -> (Diagnostics, MeasEnv)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup MeasEnv -> (Diagnostics, MeasEnv))
-> Lookup MeasEnv -> (Diagnostics, MeasEnv)
forall a b. (a -> b) -> a -> b
$ Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
let (Diagnostics
dg4, GhcSpecSig
sig) = Lookup GhcSpecSig -> (Diagnostics, GhcSpecSig)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecSig -> (Diagnostics, GhcSpecSig))
-> Lookup GhcSpecSig -> (Diagnostics, GhcSpecSig)
forall a b. (a -> b) -> a -> b
$ Config
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec (Located BareType) 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
TcRn [(TyVar, LocSpecType)]
-> ([(TyVar, LocSpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig)
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> (a -> IOEnv (Env TcGblEnv TcLclEnv) b)
-> IOEnv (Env TcGblEnv TcLclEnv) b
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 GhcSpecSig -> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GhcSpecSig
sig
let qual :: GhcSpecQual
qual = Config
-> Env
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecQual
makeSpecQual Config
cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
let sData :: GhcSpecData
sData = GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
elaboratedSig HashMap ModName (Spec (Located BareType) LocSymbol)
specs
let (Diagnostics
dg1, GhcSpecVars
spcVars) = Lookup GhcSpecVars -> (Diagnostics, GhcSpecVars)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecVars -> (Diagnostics, GhcSpecVars))
-> Lookup GhcSpecVars -> (Diagnostics, GhcSpecVars)
forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> Spec (Located BareType) LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec (Located BareType) LocSymbol
mySpec Env
env MeasEnv
measEnv
let (Diagnostics
dg2, GhcSpecTerm
spcTerm) = Lookup GhcSpecTerm -> (Diagnostics, GhcSpecTerm)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecTerm -> (Diagnostics, GhcSpecTerm))
-> Lookup GhcSpecTerm -> (Diagnostics, GhcSpecTerm)
forall a b. (a -> b) -> a -> b
$ Config
-> Spec (Located BareType) LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec (Located BareType) LocSymbol
mySpec Env
env ModName
name
let (Diagnostics
dg3, GhcSpecRefl
refl) = Lookup GhcSpecRefl -> (Diagnostics, GhcSpecRefl)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecRefl -> (Diagnostics, GhcSpecRefl))
-> Lookup GhcSpecRefl -> (Diagnostics, GhcSpecRefl)
forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> MeasEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
measEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env ModName
name GhcSpecSig
elaboratedSig TycEnv
tycEnv
let laws :: GhcSpecLaws
laws = Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> MeasEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
elaboratedSig [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
elaboratedSig) MeasEnv
measEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
let finalLiftedSpec :: Spec (Located BareType) LocSymbol
finalLiftedSpec = ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
elaboratedSig GhcSpecQual
qual BareRTEnv
myRTE Spec (Located BareType) LocSymbol
lSpec1
let diags :: Diagnostics
diags = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat [Diagnostics
dg0, Diagnostics
dg1, Diagnostics
dg2, Diagnostics
dg3, Diagnostics
dg4, Diagnostics
dg5]
(Diagnostics, GhcSpec) -> TcRn (Diagnostics, GhcSpec)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics
diags, SP
{ _gsConfig :: Config
_gsConfig = Config
cfg
, _gsImps :: [(Symbol, Sort)]
_gsImps = [(ModName, Spec (Located BareType) LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec (Located BareType) 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 (Located BareType) LocSymbol
_gsLSpec = Spec (Located BareType) LocSymbol
finalLiftedSpec
{ impSigs = makeImports mspecs
, expSigs = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
, dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
, measures = Ms.measures mySpec
, asmSigs = Ms.asmSigs finalLiftedSpec ++ Ms.asmSigs mySpec
, imeasures = Ms.imeasures finalLiftedSpec ++ Ms.imeasures mySpec
, dvariance = Ms.dvariance finalLiftedSpec ++ Ms.dvariance mySpec
, rinstance = Ms.rinstance finalLiftedSpec ++ Ms.rinstance mySpec
}
})
where
coreToLg :: CoreExpr -> Expr
coreToLg CoreExpr
ce =
case TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM Expr
-> Either Error Expr
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
CoreToLogic.runToLogic
TCEmb TyCon
embs
LogicMap
lmap
DataConMap
dm
(\[Char]
x -> Maybe SrcSpan -> [Char] -> Error
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"coreToLogic not working " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x))
(Bool -> CoreExpr -> LogicM Expr
CoreToLogic.coreToLogic Bool
allowTC CoreExpr
ce) of
Left Error
msg -> Maybe SrcSpan -> [Char] -> Expr
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (Error -> [Char]
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 <-
[(TyVar, LocSpecType)]
-> ((TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
si) (((TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)])
-> ((TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ \(TyVar
x, LocSpecType
t) ->
if TyVar -> Bool
forall a. NamedThing a => a -> Bool
GM.isFromGHCReal TyVar
x then
(TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
t)
else do LocSpecType
t' <- (SpecType -> TcRn SpecType)
-> LocSpecType -> IOEnv (Env TcGblEnv TcLclEnv) LocSpecType
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) LocSpecType
t
(TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
t')
GhcSpecSig -> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
GhcSpecSig
si
{ gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig }
simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
simplifier :: CoreExpr -> TcRn CoreExpr
simplifier = CoreExpr -> TcRn CoreExpr
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
allowTC :: Bool
allowTC = Config -> Bool
typeclass Config
cfg
mySpec2 :: Spec (Located BareType) LocSymbol
mySpec2 = Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
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 (Located BareType) LocSymbol
mySpec1 where l :: SourcePos
l = [Char] -> SourcePos
F.dummyPos [Char]
"expand-mySpec2"
iSpecs2 :: HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs2 = Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
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 (Located BareType) LocSymbol)
iSpecs0 where l :: SourcePos
l = [Char] -> SourcePos
F.dummyPos [Char]
"expand-iSpecs2"
rtEnv :: BareRTEnv
rtEnv = Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> LogicMap
-> BareRTEnv
Bare.makeRTEnv Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec1 HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0 LogicMap
lmap
mspecs :: [(ModName, Spec (Located BareType) LocSymbol)]
mspecs = if Bool
allowTC then HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a b. (a -> b) -> a -> b
$ ModName
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec (Located BareType) LocSymbol
mySpec0 HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0 else [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls
(Spec (Located BareType) LocSymbol
mySpec0, [(ClsInst, [TyVar])]
instMethods) = if Bool
allowTC
then GhcSrc
-> Env
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> (Spec (Located BareType) LocSymbol, [(ClsInst, [TyVar])])
Bare.compileClasses GhcSrc
src Env
env (ModName
name, Spec (Located BareType) LocSymbol
mySpec0NoCls) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0)
else (Spec (Located BareType) LocSymbol
mySpec0NoCls, [])
mySpec1 :: Spec (Located BareType) LocSymbol
mySpec1 = Spec (Located BareType) LocSymbol
mySpec0 Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a. Semigroup a => a -> a -> a
<> Spec (Located BareType) LocSymbol
lSpec0
lSpec0 :: Spec (Located BareType) LocSymbol
lSpec0 = Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec0
embs :: TCEmb TyCon
embs = GhcSrc
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
makeEmbeds GhcSrc
src Env
env ((ModName
name, Spec (Located BareType) LocSymbol
mySpec0) (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. a -> [a] -> [a]
: HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0)
dm :: DataConMap
dm = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv0
(Diagnostics
dg0, [Located DataConP]
datacons, TycEnv
tycEnv0) = Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
name Env
env TCEmb TyCon
embs Spec (Located BareType) LocSymbol
mySpec2 HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs2
env :: Env
env = Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Env
Bare.makeEnv Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls
(Spec (Located BareType) LocSymbol
mySpec0NoCls, HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0) = ModName
-> GhcSrc
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> (Spec (Located BareType) LocSymbol,
HashMap ModName (Spec (Located BareType) LocSymbol))
splitSpecs ModName
name GhcSrc
src [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls
name :: ModName
name = [Char] -> ModName -> ModName
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"ALL-SPECS" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
zzz) (ModName -> ModName) -> ModName -> ModName
forall a b. (a -> b) -> a -> b
$ GhcSrc -> ModName
_giTargetMod GhcSrc
src
zzz :: [Char]
zzz = [ModName] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ((ModName, Spec (Located BareType) LocSymbol) -> ModName
forall a b. (a, b) -> a
fst ((ModName, Spec (Located BareType) LocSymbol) -> ModName)
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [ModName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec (Located BareType) LocSymbol)]
mspecs)
splitSpecs :: ModName -> GhcSrc -> [(ModName, Ms.BareSpec)] -> (Ms.BareSpec, Bare.ModSpecs)
splitSpecs :: ModName
-> GhcSrc
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> (Spec (Located BareType) LocSymbol,
HashMap ModName (Spec (Located BareType) LocSymbol))
splitSpecs ModName
name GhcSrc
src [(ModName, Spec (Located BareType) LocSymbol)]
specs = (Spec (Located BareType) LocSymbol
mySpec, HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecm)
where
iSpecm :: HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecm = ([Spec (Located BareType) LocSymbol]
-> Spec (Located BareType) LocSymbol)
-> HashMap ModName [Spec (Located BareType) LocSymbol]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall a b. (a -> b) -> HashMap ModName a -> HashMap ModName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Spec (Located BareType) LocSymbol]
-> Spec (Located BareType) LocSymbol
forall a. Monoid a => [a] -> a
mconcat (HashMap ModName [Spec (Located BareType) LocSymbol]
-> HashMap ModName (Spec (Located BareType) LocSymbol))
-> ([(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName [Spec (Located BareType) LocSymbol])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName [Spec (Located BareType) LocSymbol]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group ([(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName (Spec (Located BareType) LocSymbol))
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall a b. (a -> b) -> a -> b
$ [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs
iSpecs :: [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs = GhcSrc
-> Spec (Located BareType) LocSymbol
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
Dg.sliceSpecs GhcSrc
src Spec (Located BareType) LocSymbol
mySpec [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs'
mySpec :: Spec (Located BareType) LocSymbol
mySpec = [Spec (Located BareType) LocSymbol]
-> Spec (Located BareType) LocSymbol
forall a. Monoid a => [a] -> a
mconcat ((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd ((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [Spec (Located BareType) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec (Located BareType) LocSymbol)]
mySpecs)
([(ModName, Spec (Located BareType) LocSymbol)]
mySpecs, [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs') = ((ModName, Spec (Located BareType) LocSymbol) -> Bool)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> ([(ModName, Spec (Located BareType) LocSymbol)],
[(ModName, Spec (Located BareType) LocSymbol)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((ModName
name ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
==) (ModName -> Bool)
-> ((ModName, Spec (Located BareType) LocSymbol) -> ModName)
-> (ModName, Spec (Located BareType) LocSymbol)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol) -> ModName
forall a b. (a, b) -> a
fst) [(ModName, Spec (Located BareType) LocSymbol)]
specs
makeImports :: [(ModName, Ms.BareSpec)] -> [(F.Symbol, F.Sort)]
makeImports :: [(ModName, Spec (Located BareType) LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec (Located BareType) LocSymbol)]
specs = ((ModName, Spec (Located BareType) LocSymbol) -> [(Symbol, Sort)])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(Symbol, Sort)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Spec (Located BareType) LocSymbol -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs (Spec (Located BareType) LocSymbol -> [(Symbol, Sort)])
-> ((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol)
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd) [(ModName, Spec (Located BareType) LocSymbol)]
specs'
where specs' :: [(ModName, Spec (Located BareType) LocSymbol)]
specs' = ((ModName, Spec (Located BareType) LocSymbol) -> Bool)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> Bool
isSrcImport (ModName -> Bool)
-> ((ModName, Spec (Located BareType) LocSymbol) -> ModName)
-> (ModName, Spec (Located BareType) LocSymbol)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol) -> ModName
forall a b. (a, b) -> a
fst) [(ModName, Spec (Located BareType) LocSymbol)]
specs
makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon
makeEmbeds :: GhcSrc
-> Env
-> [(ModName, Spec (Located BareType) 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)
(TCEmb TyCon -> TCEmb TyCon)
-> ([(ModName, Spec (Located BareType) LocSymbol)] -> TCEmb TyCon)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCEmb TyCon] -> TCEmb TyCon
forall a. Monoid a => [a] -> a
mconcat
([TCEmb TyCon] -> TCEmb TyCon)
-> ([(ModName, Spec (Located BareType) LocSymbol)]
-> [TCEmb TyCon])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, Spec (Located BareType) LocSymbol) -> TCEmb TyCon)
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [TCEmb TyCon]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (ModName, Spec (Located BareType) LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env)
makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: Env -> (ModName, Spec (Located BareType) LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env (ModName
name, Spec (Located BareType) LocSymbol
spec)
= [(TyCon, (Sort, TCArgs))] -> TCEmb TyCon
forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
F.tceFromList [ (TyCon
tc, (Sort, TCArgs)
t) | (LocSymbol
c,(Sort, TCArgs)
t) <- TCEmb LocSymbol -> [(LocSymbol, (Sort, TCArgs))]
forall a. TCEmb a -> [(a, (Sort, TCArgs))]
F.tceToList (Spec (Located BareType) LocSymbol -> TCEmb LocSymbol
forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds Spec (Located BareType) LocSymbol
spec), TyCon
tc <- LocSymbol -> [TyCon]
forall {a}. ResolveSym a => LocSymbol -> [a]
symTc LocSymbol
c ]
where
symTc :: LocSymbol -> [a]
symTc = Maybe a -> [a]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe a -> [a]) -> (LocSymbol -> Maybe a) -> LocSymbol -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> [Char] -> LocSymbol -> Maybe a
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 (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec1 Config
config GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty
{ Ms.measures = Bare.makeHaskellMeasures (typeclass config) src tycEnv lmap mySpec }
makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
-> Ms.BareSpec
makeLiftedSpec0 :: Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty
{ Ms.ealiases = lmapEAlias . snd <$> Bare.makeHaskellInlines (typeclass cfg) src embs lmap mySpec
, Ms.reflects = Ms.reflects mySpec
, Ms.dataDecls = Bare.makeHaskellDataDecls cfg name mySpec tcs
, Ms.embeds = Ms.embeds mySpec
, Ms.cmeasures = Ms.cmeasures mySpec
}
where
tcs :: [TyCon]
tcs = [TyCon] -> [TyCon]
forall a. Uniquable a => [a] -> [a]
uniqNub (GhcSrc -> [TyCon]
_gsTcs GhcSrc
src [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ [TyCon]
refTcs)
refTcs :: [TyCon]
refTcs = Config
-> TCEmb TyCon
-> [CoreBind]
-> Spec (Located BareType) LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs Spec (Located BareType) 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 = HashMap Int a -> [a]
forall k v. HashMap k v -> [v]
M.elems (HashMap Int a -> [a]) -> HashMap Int a -> [a]
forall a b. (a -> b) -> a -> b
$ [(Int, a)] -> HashMap Int a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (a -> Int
forall {a}. Uniquable a => a -> Int
index a
x, a
x) | a
x <- [a]
xs ]
where
index :: a -> Int
index = Unique -> Int
Ghc.getKey (Unique -> Int) -> (a -> Unique) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unique
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 (Located BareType) LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs Spec (Located BareType) LocSymbol
spec
| Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs)
([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ (TyVar -> [TyCon]) -> [TyVar] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyVar -> [TyCon]
varTyCons
([TyVar] -> [TyCon]) -> [TyVar] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs
| Bool
otherwise = []
isEmbedded :: TCEmb Ghc.TyCon -> Ghc.TyCon -> Bool
isEmbedded :: TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs TyCon
c = TyCon -> TCEmb TyCon -> Bool
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 (SpecType -> [TyCon]) -> (TyVar -> SpecType) -> TyVar -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Type -> SpecType) -> (TyVar -> Type) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
specTypeCons :: SpecType -> [Ghc.TyCon]
specTypeCons :: SpecType -> [TyCon]
specTypeCons = ([TyCon] -> SpecType -> [TyCon]) -> [TyCon] -> SpecType -> [TyCon]
forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType [TyCon] -> SpecType -> [TyCon]
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 (RType RTyCon tv r -> RTyCon
forall c tv r. RType c tv r -> c
rt_tycon RType RTyCon tv r
t) TyCon -> [TyCon] -> [TyCon]
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 (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs = (TyVar, CoreExpr) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, CoreExpr) -> TyVar) -> [(TyVar, CoreExpr)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
where
xDefs :: [(TyVar, CoreExpr)]
xDefs = (Symbol -> Maybe (TyVar, CoreExpr))
-> [Symbol] -> [(TyVar, CoreExpr)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
reflSyms
reflSyms :: [Symbol]
reflSyms = LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec (Located BareType) LocSymbol
spec)
measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
measureVars :: Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs = (TyVar, CoreExpr) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, CoreExpr) -> TyVar) -> [(TyVar, CoreExpr)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
where
xDefs :: [(TyVar, CoreExpr)]
xDefs = (Symbol -> Maybe (TyVar, CoreExpr))
-> [Symbol] -> [(TyVar, CoreExpr)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
measureSyms
measureSyms :: [Symbol]
measureSyms = LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec (Located BareType) LocSymbol
spec)
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
-> Bare.Lookup GhcSpecVars
makeSpecVars :: Config
-> GhcSrc
-> Spec (Located BareType) LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec (Located BareType) LocSymbol
mySpec Env
env MeasEnv
measEnv = do
[TyVar]
tgtVars <- ([Char] -> Either [Error] TyVar)
-> [[Char]] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> Either [Error] TyVar
resolveStringVar Env
env ModName
name) (Config -> [[Char]]
checks Config
cfg)
HashSet TyVar
igVars <- (LocSymbol -> Either [Error] TyVar)
-> HashSet LocSymbol -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-ignores") (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.ignores Spec (Located BareType) LocSymbol
mySpec)
HashSet TyVar
lVars <- (LocSymbol -> Either [Error] TyVar)
-> HashSet LocSymbol -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-lvars" ) (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lvars Spec (Located BareType) LocSymbol
mySpec)
GhcSpecVars -> Lookup GhcSpecVars
forall a. a -> Either [Error] a
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 = (ModName, TyVar, LocSpecType) -> TyVar
forall a b c. (a, b, c) -> b
snd3 ((ModName, TyVar, LocSpecType) -> TyVar)
-> [(ModName, TyVar, LocSpecType)] -> [TyVar]
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 <- (a -> m b) -> [a] -> m [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM a -> m b
f (HashSet a -> [a]
forall a. HashSet a -> [a]
S.toList HashSet a
xSet)
HashSet b -> m (HashSet b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> HashSet b
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 = (a -> m b) -> HashSet a -> m (HashSet b)
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 (ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name) (a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
s)
resolveStringVar :: Bare.Env -> ModName -> String -> Bare.Lookup Ghc.Var
resolveStringVar :: Env -> ModName -> [Char] -> Either [Error] TyVar
resolveStringVar Env
env ModName
name [Char]
s = Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolve-string-var" LocSymbol
lx
where
lx :: LocSymbol
lx = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (ModName -> [Char] -> Symbol
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 (Located BareType) LocSymbol)
-> GhcSpecQual
makeSpecQual Config
_cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
_rtEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs = SpQual
{ gsQualifiers :: [Qualifier]
gsQualifiers = (Qualifier -> Bool) -> [Qualifier] -> [Qualifier]
forall a. (a -> Bool) -> [a] -> [a]
filter Qualifier -> Bool
forall {a}. (PPrint a, Subable a) => a -> Bool
okQual [Qualifier]
quals
, gsRTAliases :: [Located SpecRTAlias]
gsRTAliases = []
}
where
quals :: [Qualifier]
quals = ((ModName, Spec (Located BareType) LocSymbol) -> [Qualifier])
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> TycEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [Qualifier]
forall ty bndr.
Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
okQual :: a -> Bool
okQual a
q = [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"okQual: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp a
q)
(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
mSyms) (a -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms a
q)
mSyms :: HashSet Symbol
mSyms = [Char] -> HashSet Symbol -> HashSet Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"MSYMS" (HashSet Symbol -> HashSet Symbol)
-> ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
wiredSortedSyms)
[Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Located (RRType Reft)) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType Reft)) -> Symbol)
-> [(Symbol, Located (RRType Reft))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv)
[Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Located (RRType Reft)) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType Reft)) -> Symbol)
-> [(Symbol, Located (RRType Reft))] -> [Symbol]
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)
= (Qualifier -> Qualifier) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> Qualifier -> Qualifier
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
modn)
([Qualifier] -> [Qualifier])
-> ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Qualifier -> Maybe Qualifier) -> [Qualifier] -> [Qualifier]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams Env
env TycEnv
tycEnv ModName
modn)
([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> [Qualifier]
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 <- (QualParam -> Maybe QualParam) -> [QualParam] -> Maybe [QualParam]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM QualParam -> Maybe QualParam
goQP (Qualifier -> [QualParam]
F.qParams Qualifier
q)
Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Qualifier -> Maybe Qualifier) -> Qualifier -> Maybe Qualifier
forall a b. (a -> b) -> a -> b
$ Qualifier
q { F.qParams = qps }
where
goQP :: QualParam -> Maybe QualParam
goQP QualParam
qp = do { Sort
s <- Sort -> Maybe Sort
go (QualParam -> Sort
F.qpSort QualParam
qp) ; QualParam -> Maybe QualParam
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return QualParam
qp { F.qpSort = s } }
go :: F.Sort -> Maybe F.Sort
go :: Sort -> Maybe Sort
go (FAbs Int
i Sort
s) = Int -> Sort -> Sort
FAbs Int
i (Sort -> Sort) -> Maybe Sort -> Maybe Sort
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 (Sort -> Sort -> Sort) -> Maybe Sort -> Maybe (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 Maybe (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
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 (Sort -> Sort -> Sort) -> Maybe Sort -> Maybe (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 Maybe (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
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 = Sort -> Maybe Sort
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 = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (FTycon -> Sort
FTC FTycon
c)
| Bool
otherwise = TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs (Located TyCon -> Sort)
-> (TyCon -> Located TyCon) -> TyCon -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
tcs (TyCon -> Sort) -> Maybe TyCon -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe TyCon
forall {a}. ResolveSym a => Maybe a
ty
where
ty :: Maybe a
ty = Env -> ModName -> [Char] -> LocSymbol -> Maybe a
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"qualify-FTycon" LocSymbol
tcs
isPrimFTC :: Bool
isPrimFTC = LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
tcs Symbol -> HashSet Symbol -> Bool
forall a. Eq a => a -> HashSet a -> Bool
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 = Sort -> ((Sort, TCArgs) -> Sort) -> Maybe (Sort, TCArgs) -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Sort
s0 (Sort, TCArgs) -> Sort
forall a b. (a, b) -> a
fst (TyCon -> TCEmb TyCon -> Maybe (Sort, TCArgs)
forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
F.tceLookup TyCon
c TCEmb TyCon
embs)
where
c :: TyCon
c = Located TyCon -> TyCon
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 (FTycon -> Sort)
-> (Located TyCon -> FTycon) -> Located TyCon -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> FTycon
F.symbolFTycon (LocSymbol -> FTycon)
-> (Located TyCon -> LocSymbol) -> Located TyCon -> FTycon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Symbol) -> Located TyCon -> LocSymbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol
makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName ->
Bare.Lookup GhcSpecTerm
makeSpecTerm :: Config
-> Spec (Located BareType) LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec (Located BareType) LocSymbol
mySpec Env
env ModName
name = do
HashSet TyVar
sizes <- if Config -> Bool
forall t. HasConfig t => t -> Bool
structuralTerm Config
cfg then HashSet TyVar -> Either [Error] (HashSet TyVar)
forall a. a -> Either [Error] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet TyVar
forall a. Monoid a => a
mempty else Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeSize Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
HashSet TyVar
lazies <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeLazy Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
HashSet TyCon
autos <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
HashSet (Located TyVar)
gfail <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
GhcSpecTerm -> Lookup GhcSpecTerm
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (GhcSpecTerm -> Lookup GhcSpecTerm)
-> GhcSpecTerm -> Lookup GhcSpecTerm
forall a b. (a -> b) -> a -> b
$ SpTerm
{ gsLazy :: HashSet TyVar
gsLazy = TyVar -> HashSet TyVar -> HashSet TyVar
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert TyVar
dictionaryVar (HashSet TyVar
lazies HashSet TyVar -> HashSet TyVar -> HashSet TyVar
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 = HashSet TyVar
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, Located BareType, Located BareType,
RelExpr, RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv = ((LocSymbol, LocSymbol, Located BareType, Located BareType,
RelExpr, RelExpr)
-> Either
[Error] (TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr))
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
RelExpr, RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (LocSymbol, LocSymbol, Located BareType, Located BareType, RelExpr,
RelExpr)
-> Either
[Error] (TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)
forall {e} {f}.
(LocSymbol, LocSymbol, Located BareType, Located BareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go
where
go :: (LocSymbol, LocSymbol, Located BareType, Located BareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go (LocSymbol
x, LocSymbol
y, Located BareType
tx, Located BareType
ty, e
a, f
e) = do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
TyVar
vy <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
y
(TyVar, TyVar, LocSpecType, LocSpecType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return
( TyVar
vx
, TyVar
vy
, Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.HsTV TyVar
vx) Located BareType
tx
, Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.HsTV TyVar
vy) Located BareType
ty
, e
a
, f
e
)
makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeLazy Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
(LocSymbol -> Either [Error] TyVar)
-> HashSet LocSymbol -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var") (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lazy Spec (Located BareType) LocSymbol
spec)
makeFail :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeFail :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
HashSet LocSymbol
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.fails Spec (Located BareType) LocSymbol
spec) ((LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar)))
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall a b. (a -> b) -> a -> b
$ \LocSymbol
x -> do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
Located TyVar -> Either [Error] (Located TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return LocSymbol
x { val = vx }
makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeRewrite :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
HashSet LocSymbol
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.rewrites Spec (Located BareType) LocSymbol
spec) ((LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar)))
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall a b. (a -> b) -> a -> b
$ \LocSymbol
x -> do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
Located TyVar -> Either [Error] (Located TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return LocSymbol
x { val = vx }
makeRewriteWith :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
makeRewriteWith :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec (Located BareType) LocSymbol
spec = [(TyVar, [TyVar])] -> HashMap TyVar [TyVar]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(TyVar, [TyVar])] -> HashMap TyVar [TyVar])
-> Either [Error] [(TyVar, [TyVar])]
-> Lookup (HashMap TyVar [TyVar])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] [(TyVar, [TyVar])]
forall ty bndr.
Env -> ModName -> Spec ty bndr -> Either [Error] [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec (Located BareType) LocSymbol
spec
makeRewriteWith' :: Bare.Env -> ModName -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' :: forall ty bndr.
Env -> ModName -> Spec ty bndr -> Either [Error] [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec ty bndr
spec =
[(LocSymbol, [LocSymbol])]
-> ((LocSymbol, [LocSymbol]) -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])])
-> HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> HashMap LocSymbol [LocSymbol]
forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
Ms.rewriteWith Spec ty bndr
spec) (((LocSymbol, [LocSymbol]) -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])])
-> ((LocSymbol, [LocSymbol]) -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])]
forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [LocSymbol]
xs) -> do
TyVar
xv <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var1" LocSymbol
x
[TyVar]
xvs <- (LocSymbol -> Either [Error] TyVar)
-> [LocSymbol] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var2") [LocSymbol]
xs
(TyVar, [TyVar]) -> Either [Error] (TyVar, [TyVar])
forall a. a -> Either [Error] a
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 (Located BareType) LocSymbol
-> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name
= ([TyCon] -> HashSet TyCon)
-> Either [Error] [TyCon] -> Lookup (HashSet TyCon)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TyCon] -> HashSet TyCon
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
(Either [Error] [TyCon] -> Lookup (HashSet TyCon))
-> (Spec (Located BareType) LocSymbol -> Either [Error] [TyCon])
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet TyCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol -> Either [Error] TyCon)
-> [LocSymbol] -> Either [Error] [TyCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyCon
Bare.lookupGhcTyCon Env
env ModName
name [Char]
"TyCon")
([LocSymbol] -> Either [Error] [TyCon])
-> (Spec (Located BareType) LocSymbol -> [LocSymbol])
-> Spec (Located BareType) LocSymbol
-> Either [Error] [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList
(HashSet LocSymbol -> [LocSymbol])
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Spec (Located BareType) LocSymbol
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec (Located BareType) LocSymbol -> HashSet LocSymbol
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 (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeSize Env
env ModName
name
= ([TyVar] -> HashSet TyVar)
-> Either [Error] [TyVar] -> Either [Error] (HashSet TyVar)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
(Either [Error] [TyVar] -> Either [Error] (HashSet TyVar))
-> (Spec (Located BareType) LocSymbol -> Either [Error] [TyVar])
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol -> Either [Error] TyVar)
-> [LocSymbol] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var")
([LocSymbol] -> Either [Error] [TyVar])
-> (Spec (Located BareType) LocSymbol -> [LocSymbol])
-> Spec (Located BareType) LocSymbol
-> Either [Error] [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Maybe LocSymbol) -> [DataDecl] -> [LocSymbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe LocSymbol
getSizeFuns
([DataDecl] -> [LocSymbol])
-> (Spec (Located BareType) LocSymbol -> [DataDecl])
-> Spec (Located BareType) LocSymbol
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec (Located BareType) LocSymbol -> [DataDecl]
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
= LocSymbol -> Maybe LocSymbol
forall a. a -> Maybe a
Just LocSymbol
f
| Bool
otherwise
= Maybe LocSymbol
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 (Located BareType) LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs MeasEnv
menv HashMap ModName (Spec (Located BareType) LocSymbol)
specs = SpLaws
{ gsLawDefs :: [(Class, [(TyVar, LocSpecType)])]
gsLawDefs = ([(ModName, TyVar, LocSpecType)] -> [(TyVar, LocSpecType)])
-> (Class, [(ModName, TyVar, LocSpecType)])
-> (Class, [(TyVar, LocSpecType)])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (((ModName, TyVar, LocSpecType) -> (TyVar, LocSpecType))
-> [(ModName, TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a b. (a -> b) -> [a] -> [b]
map (\(ModName
_,TyVar
x,LocSpecType
y) -> (TyVar
x,LocSpecType
y))) ((Class, [(ModName, TyVar, LocSpecType)])
-> (Class, [(TyVar, LocSpecType)]))
-> [(Class, [(ModName, TyVar, LocSpecType)])]
-> [(Class, [(TyVar, LocSpecType)])]
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 (Located BareType) LocSymbol)
-> [LawInstance]
Bare.makeInstanceLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs HashMap ModName (Spec (Located BareType) 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 (Located BareType) LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
menv HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv = do
HashMap TyVar (Maybe Int)
autoInst <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
HashSet (Located TyVar)
rwr <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
HashMap TyVar [TyVar]
rwrWith <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec (Located BareType) 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 (Located BareType) LocSymbol
-> Lookup [(TyVar, LocSpecType, Equation)]
Bare.makeHaskellAxioms Config
cfg GhcSrc
src Env
env TycEnv
tycEnv ModName
name LogicMap
lmap GhcSpecSig
sig Spec (Located BareType) LocSymbol
mySpec
let myAxioms :: [Equation]
myAxioms =
[ Env -> ModName -> SourcePos -> Equation -> Equation
forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop
Env
env
ModName
name
(LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSpecType
lt)
Equation
e {eqName = s, eqRec = S.member s (exprSymbolsSet (eqBody e))}
| (TyVar
x, LocSpecType
lt, Equation
e) <- [(TyVar, LocSpecType, Equation)]
xtes
, let s :: Symbol
s = TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x
]
let sigVars :: [TyVar]
sigVars = [Char] -> [TyVar] -> [TyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SIGVARS" ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ ((TyVar, LocSpecType, Equation) -> TyVar
forall a b c. (a, b, c) -> a
fst3 ((TyVar, LocSpecType, Equation) -> TyVar)
-> [(TyVar, LocSpecType, Equation)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType, Equation)]
xtes)
[TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
sig)
[TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsRefSigs GhcSpecSig
sig)
GhcSpecRefl -> Lookup GhcSpecRefl
forall a. a -> Either [Error] a
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 = ((ModName, Spec (Located BareType) LocSymbol) -> [Equation])
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [Equation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Spec (Located BareType) LocSymbol -> [Equation]
forall ty bndr. Spec ty bndr -> [Equation]
Ms.axeqs (Spec (Located BareType) LocSymbol -> [Equation])
-> ((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol)
-> (ModName, Spec (Located BareType) LocSymbol)
-> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
, gsMyAxioms :: [Equation]
gsMyAxioms = [Char] -> [Equation] -> [Equation]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsMyAxioms" [Equation]
myAxioms
, gsReflects :: [TyVar]
gsReflects = [Char] -> [TyVar] -> [TyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsReflects" ([TyVar]
lawMethods [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (HashSet Symbol -> TyVar -> Bool
isReflectVar HashSet Symbol
rflSyms) [TyVar]
sigVars [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
wRefls)
, gsHAxioms :: [(TyVar, LocSpecType, Equation)]
gsHAxioms = [Char]
-> [(TyVar, LocSpecType, Equation)]
-> [(TyVar, LocSpecType, Equation)]
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 = [Char] -> [TyVar] -> [TyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"Law Methods" ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ (Class -> [TyVar]) -> [Class] -> [TyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Class -> [TyVar]
Ghc.classMethods ((Class, [(ModName, TyVar, LocSpecType)]) -> Class
forall a b. (a, b) -> a
fst ((Class, [(ModName, TyVar, LocSpecType)]) -> Class)
-> [(Class, [(ModName, TyVar, LocSpecType)])] -> [Class]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
menv)
mySpec :: Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
rflSyms :: HashSet Symbol
rflSyms = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (HashMap ModName (Spec (Located BareType) LocSymbol) -> [Symbol]
getReflects HashMap ModName (Spec (Located BareType) 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 = Symbol -> HashSet Symbol -> Bool
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 (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v)
getReflects :: Bare.ModSpecs -> [Symbol]
getReflects :: HashMap ModName (Spec (Located BareType) LocSymbol) -> [Symbol]
getReflects = (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSymbol -> Symbol
forall a. Located a -> a
val ([LocSymbol] -> [Symbol])
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [LocSymbol])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet LocSymbol -> [LocSymbol])
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashSet LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HashSet LocSymbol] -> HashSet LocSymbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet LocSymbol] -> HashSet LocSymbol)
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [HashSet LocSymbol])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, Spec (Located BareType) LocSymbol) -> HashSet LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [HashSet LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
names (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> ((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol)
-> (ModName, Spec (Located BareType) LocSymbol)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd) ([(ModName, Spec (Located BareType) LocSymbol)]
-> [HashSet LocSymbol])
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [HashSet LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList
where
names :: Spec ty bndr -> HashSet LocSymbol
names Spec ty bndr
z = [HashSet LocSymbol] -> HashSet LocSymbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions [ Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec ty bndr
z, Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Spec ty bndr
z, Spec ty bndr -> HashSet LocSymbol
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 = F.notracepp ("gsRefSigs for " ++ F.showpp name) $ map expandReflectedSignature reflSigs
, gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) (wreflSigs ++ filter notReflected (gsAsmSigs sig))
}
where
expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
expandReflectedSignature :: (TyVar, LocSpecType) -> (TyVar, LocSpecType)
expandReflectedSignature = (LocSpecType -> LocSpecType)
-> (TyVar, LocSpecType) -> (TyVar, LocSpecType)
forall a b. (a -> b) -> (TyVar, a) -> (TyVar, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> LocSpecType
-> LocSpecType
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) = ((TyVar, LocSpecType) -> Bool)
-> [(TyVar, LocSpecType)]
-> ([(TyVar, LocSpecType)], [(TyVar, LocSpecType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((TyVar -> [TyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl) (TyVar -> Bool)
-> ((TyVar, LocSpecType) -> TyVar) -> (TyVar, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar, LocSpecType) -> TyVar
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 = (TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(TyVar, LocSpecType)]
wreflSigs [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
reflSigs)
notReflected :: (TyVar, b) -> Bool
notReflected (TyVar, b)
xt = (TyVar, b) -> TyVar
forall a b. (a, b) -> a
fst (TyVar, b)
xt TyVar -> [TyVar] -> Bool
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 (Located BareType) LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec (Located BareType) LocSymbol
spec = [(TyVar, Maybe Int)] -> HashMap TyVar (Maybe Int)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(TyVar, Maybe Int)] -> HashMap TyVar (Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)]
-> Lookup (HashMap TyVar (Maybe Int))
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 = [(LocSymbol, Maybe Int)]
-> ((LocSymbol, Maybe Int) -> Either [Error] (TyVar, Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashMap LocSymbol (Maybe Int) -> [(LocSymbol, Maybe Int)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Spec (Located BareType) LocSymbol -> HashMap LocSymbol (Maybe Int)
forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
Ms.autois Spec (Located BareType) LocSymbol
spec)) (((LocSymbol, Maybe Int) -> Either [Error] (TyVar, Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)])
-> ((LocSymbol, Maybe Int) -> Either [Error] (TyVar, Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)]
forall a b. (a -> b) -> a -> b
$ \(LocSymbol
k, Maybe Int
val) -> do
TyVar
vk <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
k
(TyVar, Maybe Int) -> Either [Error] (TyVar, Maybe Int)
forall a. a -> Either [Error] a
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 (Located BareType) LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv [CoreBind]
cbs = do
[(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs <- Env
-> SigEnv
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec (Located BareType) LocSymbol
mySpec
[(TyVar, LocSpecType)]
aSigs <- [Char]
-> Lookup [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"makeSpecSig aSigs " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModName -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ModName
name) (Lookup [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)])
-> Lookup [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
let asmSigs :: [(TyVar, LocSpecType)]
asmSigs = TycEnv -> [(TyVar, LocSpecType)]
Bare.tcSelVars TycEnv
tycEnv
[(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
aSigs
[(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [ (TyVar
x,LocSpecType
t) | (ModName
_, TyVar
x, LocSpecType
t) <- ((Class, [(ModName, TyVar, LocSpecType)])
-> [(ModName, TyVar, LocSpecType)])
-> [(Class, [(ModName, TyVar, LocSpecType)])]
-> [(ModName, TyVar, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Class, [(ModName, TyVar, LocSpecType)])
-> [(ModName, TyVar, LocSpecType)]
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 ([(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)])
-> ([[(TyVar, (Int, LocSpecType))]]
-> [(TyVar, (Int, LocSpecType))])
-> [[(TyVar, (Int, LocSpecType))]]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(TyVar, (Int, LocSpecType))]] -> [(TyVar, (Int, LocSpecType))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(TyVar, (Int, LocSpecType))]] -> [(TyVar, LocSpecType)])
-> [[(TyVar, (Int, LocSpecType))]] -> [(TyVar, LocSpecType)]
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 (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs ]
, [(TyVar
v, (Int
3, LocSpecType
t)) | (TyVar
v, LocSpecType
t ) <- Env
-> BareRTEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs ]
]
[(TyCon, LocSpecType)]
newTys <- Env
-> SigEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
relation <- Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
RelExpr, RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (Spec (Located BareType) LocSymbol
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.relational Spec (Located BareType) LocSymbol
mySpec)
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
asmRel <- Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
RelExpr, RelExpr)]
-> Lookup
[(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (Spec (Located BareType) LocSymbol
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.asmRel Spec (Located BareType) LocSymbol
mySpec)
GhcSpecSig -> Lookup GhcSpecSig
forall a. a -> Either [Error] a
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 = [(TyVar, LocSpecType)]
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 (Located BareType) LocSymbol)
-> DEnv TyVar LocSpecType
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
mySpec :: Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
allSpecs :: [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs = HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) 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 = (TyVar, [(Int, LocSpecType)]) -> (TyVar, LocSpecType)
forall {a} {b}.
(PPrint a, Ord b) =>
(a, [(b, LocSpecType)]) -> (a, LocSpecType)
go ((TyVar, [(Int, LocSpecType)]) -> (TyVar, LocSpecType))
-> [(TyVar, [(Int, LocSpecType)])] -> [(TyVar, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, (Int, LocSpecType))] -> [(TyVar, [(Int, LocSpecType)])]
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,) (LocSpecType -> (a, LocSpecType))
-> LocSpecType -> (a, LocSpecType)
forall a b. (a -> b) -> a -> b
$ (LocSpecType -> LocSpecType -> LocSpecType)
-> [LocSpecType] -> LocSpecType
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
L.foldl1' ((LocSpecType -> LocSpecType -> LocSpecType)
-> LocSpecType -> LocSpecType -> LocSpecType
forall a b c. (a -> b -> c) -> b -> a -> c
flip LocSpecType -> LocSpecType -> LocSpecType
meetLoc) ([Char] -> [LocSpecType] -> [LocSpecType]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"STRENGTHEN-SIGS: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp a
v) ([(b, LocSpecType)] -> [LocSpecType]
forall {b} {b}. Ord b => [(b, b)] -> [b]
prio [(b, LocSpecType)]
ixs))
prio :: [(b, b)] -> [b]
prio = ((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b, b) -> b
forall a b. (a, b) -> b
snd ([(b, b)] -> [b]) -> ([(b, b)] -> [(b, b)]) -> [(b, b)] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> b) -> [(b, b)] -> [(b, b)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn (b, b) -> b
forall a b. (a, b) -> a
fst
meetLoc :: LocSpecType -> LocSpecType -> LocSpecType
meetLoc :: LocSpecType -> LocSpecType -> LocSpecType
meetLoc LocSpecType
t1 LocSpecType
t2 = LocSpecType
t1 {val = val t1 `F.meet` val 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 (Located BareType) 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 (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
([TyVar] -> [(TyVar, LocSpecType)])
-> ([(ModName, Spec (Located BareType) LocSymbol)] -> [TyVar])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hinlines" Spec (Located BareType) LocSymbol -> HashSet LocSymbol
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 (Located BareType) 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 (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
([TyVar] -> [(TyVar, LocSpecType)])
-> ([(ModName, Spec (Located BareType) LocSymbol)] -> [TyVar])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hmeas" Spec (Located BareType) LocSymbol -> HashSet LocSymbol
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 = TyVar -> Located TyVar
forall a. NamedThing a => a -> Located a
GM.locNamedThing TyVar
x
, let lt :: LocSpecType
lt = LocSpecType -> LocSpecType
expand (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ Located TyVar
lx {val = f 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 (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [TyVar]
makeFromSet [Char]
msg Spec (Located BareType) LocSymbol -> HashSet LocSymbol
f Env
env [(ModName, Spec (Located BareType) LocSymbol)]
specs = [[TyVar]] -> [TyVar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ ModName -> [LocSymbol] -> [TyVar]
forall {b}. ResolveSym b => ModName -> [LocSymbol] -> [b]
mk ModName
n [LocSymbol]
xs | (ModName
n, Spec (Located BareType) LocSymbol
s) <- [(ModName, Spec (Located BareType) LocSymbol)]
specs, let xs :: [LocSymbol]
xs = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
f Spec (Located BareType) LocSymbol
s)]
where
mk :: ModName -> [LocSymbol] -> [b]
mk ModName
name = (LocSymbol -> Maybe b) -> [LocSymbol] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> ModName -> [Char] -> LocSymbol -> Maybe b
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 (Located BareType) LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec (Located BareType) LocSymbol
spec = do
[(TyVar, Located BareType)]
bareSigs <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType)]
bareTySigs Env
env ModName
name Spec (Located BareType) LocSymbol
spec
[(TyVar, Located BareType, Maybe [Located Expr])]
expSigs <- Env
-> ModName
-> [(TyVar, Located BareType)]
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(TyVar, Located BareType)]
bareSigs BareRTEnv
rtEnv Spec (Located BareType) LocSymbol
spec
let rawSigs :: [(TyVar, Located BareType, Maybe [Located Expr])]
rawSigs = Env
-> [(TyVar, Located BareType, Maybe [Located Expr])]
-> [(TyVar, Located BareType, Maybe [Located Expr])]
Bare.resolveLocalBinds Env
env [(TyVar, Located BareType, Maybe [Located Expr])]
expSigs
[(TyVar, LocSpecType, Maybe [Located Expr])]
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, TyVar -> Located BareType -> LocSpecType
cook TyVar
x Located BareType
bt, Maybe [Located Expr]
z) | (TyVar
x, Located BareType
bt, Maybe [Located Expr]
z) <- [(TyVar, Located BareType, Maybe [Located Expr])]
rawSigs ]
where
rtEnv :: BareRTEnv
rtEnv = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
cook :: TyVar -> Located BareType -> LocSpecType
cook TyVar
x Located BareType
bt = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.HsTV TyVar
x) Located BareType
bt
bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
bareTySigs :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType)]
bareTySigs Env
env ModName
name Spec (Located BareType) LocSymbol
spec = [(TyVar, Located BareType)] -> [(TyVar, Located BareType)]
forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs ([(TyVar, Located BareType)] -> [(TyVar, Located BareType)])
-> Lookup [(TyVar, Located BareType)]
-> Lookup [(TyVar, Located BareType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lookup [(TyVar, Located BareType)]
vts
where
vts :: Lookup [(TyVar, Located BareType)]
vts = [(LocSymbol, Located BareType)]
-> ((LocSymbol, Located BareType)
-> Either [Error] (TyVar, Located BareType))
-> Lookup [(TyVar, Located BareType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec (Located BareType) LocSymbol
spec [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
forall a. [a] -> [a] -> [a]
++ Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.localSigs Spec (Located BareType) LocSymbol
spec ) (((LocSymbol, Located BareType)
-> Either [Error] (TyVar, Located BareType))
-> Lookup [(TyVar, Located BareType)])
-> ((LocSymbol, Located BareType)
-> Either [Error] (TyVar, Located BareType))
-> Lookup [(TyVar, Located BareType)]
forall a b. (a -> b) -> a -> b
$ \ (LocSymbol
x, Located BareType
t) -> do
TyVar
v <- [Char] -> Either [Error] TyVar -> Either [Error] TyVar
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LOOKUP-GHC-VAR" (Either [Error] TyVar -> Either [Error] TyVar)
-> Either [Error] TyVar -> Either [Error] TyVar
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"rawTySigs" LocSymbol
x
(TyVar, Located BareType)
-> Either [Error] (TyVar, Located BareType)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
v, Located BareType
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 [(Symbol, SourcePos)] -> Either (Symbol, [SourcePos]) [SourcePos]
forall k v. (Eq k, Hashable k) => [(k, v)] -> Either (k, [v]) [v]
Misc.uniqueByKey [(Symbol, SourcePos)]
symXs of
Left (Symbol
k, [SourcePos]
ls) -> UserError -> [(x, Located t)]
forall a. UserError -> a
uError (Doc -> ListNE SrcSpan -> UserError
forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
k) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> [SourcePos] -> ListNE SrcSpan
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 = [ (x -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol x
x, Located t -> SourcePos
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 (Located BareType) LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
[(ModName, TyVar, Located BareType)]
raSigs <- Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(ModName, TyVar, Located BareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs
[(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, LocSpecType
t) | (ModName
name, TyVar
x, Located BareType
bt) <- [(ModName, TyVar, Located BareType)]
raSigs, let t :: LocSpecType
t = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.LqTV TyVar
x) Located BareType
bt ]
rawAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> Bare.Lookup [(ModName, Ghc.Var, LocBareType)]
rawAsmSigs :: Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(ModName, TyVar, Located BareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
[(TyVar, [(Bool, ModName, Located BareType)])]
aSigs <- Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs
[(ModName, TyVar, Located BareType)]
-> Lookup [(ModName, TyVar, Located BareType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (ModName
m, TyVar
v, Located BareType
t) | (TyVar
v, [(Bool, ModName, Located BareType)]
sigs) <- [(TyVar, [(Bool, ModName, Located BareType)])]
aSigs, let (ModName
m, Located BareType
t) = TyVar
-> [(Bool, ModName, Located BareType)]
-> (ModName, Located BareType)
myAsmSig TyVar
v [(Bool, ModName, Located BareType)]
sigs ]
myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: TyVar
-> [(Bool, ModName, Located BareType)]
-> (ModName, Located BareType)
myAsmSig TyVar
v [(Bool, ModName, Located BareType)]
sigs = (ModName, Located BareType)
-> Maybe (ModName, Located BareType) -> (ModName, Located BareType)
forall a. a -> Maybe a -> a
Mb.fromMaybe (ModName, Located BareType)
forall {a}. a
errImp (Maybe (ModName, Located BareType)
mbHome Maybe (ModName, Located BareType)
-> Maybe (ModName, Located BareType)
-> Maybe (ModName, Located BareType)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (ModName, Located BareType)
mbImp)
where
mbHome :: Maybe (ModName, Located BareType)
mbHome = ([(ModName, Located BareType)] -> UserError)
-> [(ModName, Located BareType)]
-> Maybe (ModName, Located BareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, Located BareType)] -> UserError
forall {a} {a}. [(a, Located a)] -> UserError
mkErr [(ModName, Located BareType)]
sigsHome
mbImp :: Maybe (ModName, Located BareType)
mbImp = ([(ModName, Located BareType)] -> UserError)
-> [(ModName, Located BareType)]
-> Maybe (ModName, Located BareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, Located BareType)] -> UserError
forall {a} {a}. [(a, Located a)] -> UserError
mkErr ([(Int, (ModName, Located BareType))]
-> [(ModName, Located BareType)]
forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int, (ModName, Located BareType))]
sigsImp)
sigsHome :: [(ModName, Located BareType)]
sigsHome = [(ModName
m, Located BareType
t) | (Bool
True, ModName
m, Located BareType
t) <- [(Bool, ModName, Located BareType)]
sigs ]
sigsImp :: [(Int, (ModName, Located BareType))]
sigsImp = [Char]
-> [(Int, (ModName, Located BareType))]
-> [(Int, (ModName, Located BareType))]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"SIGS-IMP: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyVar -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp TyVar
v)
[(Int
d, (ModName
m, Located BareType
t)) | (Bool
False, ModName
m, Located BareType
t) <- [(Bool, ModName, Located BareType)]
sigs, let d :: Int
d = Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
m]
mkErr :: [(a, Located a)] -> UserError
mkErr [(a, Located a)]
ts = SrcSpan -> Doc -> ListNE SrcSpan -> UserError
forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (TyVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyVar
v) (TyVar -> Doc
forall a. PPrint a => a -> Doc
F.pprint TyVar
v) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan)
-> ((a, Located a) -> SourcePos) -> (a, Located a) -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located a -> SourcePos)
-> ((a, Located a) -> Located a) -> (a, Located a) -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Located a) -> Located a
forall a b. (a, b) -> b
snd ((a, Located a) -> SrcSpan) -> [(a, Located a)] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Located a)]
ts) :: UserError
errImp :: a
errImp = Maybe SrcSpan -> [Char] -> a
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"myAsmSig: cannot happen as sigs is non-null"
vName :: Symbol
vName = Symbol -> Symbol
GM.takeModuleNames (TyVar -> Symbol
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, Located BareType)]
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(TyVar, Located BareType)]
tySigs BareRTEnv
rtEnv Spec (Located BareType) LocSymbol
spec = do
HashMap TyVar [Located Expr]
vExprs <- [(TyVar, [Located Expr])] -> HashMap TyVar [Located Expr]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(TyVar, [Located Expr])] -> HashMap TyVar [Located Expr])
-> Either [Error] [(TyVar, [Located Expr])]
-> Either [Error] (HashMap TyVar [Located Expr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec (Located BareType) LocSymbol
spec
let vSigExprs :: HashMap TyVar (Located BareType, Maybe [Located Expr])
vSigExprs = (TyVar
-> Located BareType -> (Located BareType, Maybe [Located Expr]))
-> HashMap TyVar (Located BareType)
-> HashMap TyVar (Located BareType, Maybe [Located Expr])
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\TyVar
v Located BareType
t -> (Located BareType
t, TyVar -> HashMap TyVar [Located Expr] -> Maybe [Located Expr]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyVar
v HashMap TyVar [Located Expr]
vExprs)) HashMap TyVar (Located BareType)
vSigs
[(TyVar, Located BareType, Maybe [Located Expr])]
-> Lookup [(TyVar, Located BareType, Maybe [Located Expr])]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
v, Located BareType
t, Located BareType -> [Located Expr] -> [Located Expr]
forall {f :: * -> *}.
Functor f =>
Located BareType -> f (Located Expr) -> f (Located Expr)
qual Located BareType
t ([Located Expr] -> [Located Expr])
-> Maybe [Located Expr] -> Maybe [Located Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Located Expr]
es) | (TyVar
v, (Located BareType
t, Maybe [Located Expr]
es)) <- HashMap TyVar (Located BareType, Maybe [Located Expr])
-> [(TyVar, (Located BareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyVar (Located BareType, Maybe [Located Expr])
vSigExprs ]
where
qual :: Located BareType -> f (Located Expr) -> f (Located Expr)
qual Located BareType
t f (Located Expr)
es = Env
-> ModName
-> BareRTEnv
-> Located BareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv Located BareType
t (Located Expr -> Located Expr)
-> f (Located Expr) -> f (Located Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Located Expr)
es
vSigs :: HashMap TyVar (Located BareType)
vSigs = [(TyVar, Located BareType)] -> HashMap TyVar (Located BareType)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyVar, Located BareType)]
tySigs
qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
-> Located F.Expr
qualifyTermExpr :: Env
-> ModName
-> BareRTEnv
-> Located BareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv Located BareType
t Located Expr
le
= Located Expr -> Expr -> Located Expr
forall l b. Loc l => l -> b -> Located b
F.atLoc Located Expr
le (Env
-> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> Expr -> Expr
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 = Located Expr -> SourcePos
forall a. Located a -> SourcePos
F.loc Located Expr
le
e :: Expr
e = Located Expr -> Expr
forall a. Located a -> a
F.val Located Expr
le
bs :: [Symbol]
bs = RTypeRep BTyCon BTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (RTypeRep BTyCon BTyVar RReft -> [Symbol])
-> (Located BareType -> RTypeRep BTyCon BTyVar RReft)
-> Located BareType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (BareType -> RTypeRep BTyCon BTyVar RReft)
-> (Located BareType -> BareType)
-> Located BareType
-> RTypeRep BTyCon BTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located BareType -> BareType
forall a. Located a -> a
val (Located BareType -> [Symbol]) -> Located BareType -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Located BareType
t
makeVarTExprs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
[(LocSymbol, [Located Expr])]
-> ((LocSymbol, [Located Expr])
-> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec (Located BareType) LocSymbol -> [(LocSymbol, [Located Expr])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
Ms.termexprs Spec (Located BareType) LocSymbol
spec) (((LocSymbol, [Located Expr])
-> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])])
-> ((LocSymbol, [Located Expr])
-> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])]
forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [Located Expr]
es) -> do
TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
(TyVar, [Located Expr]) -> Either [Error] (TyVar, [Located Expr])
forall a. a -> Either [Error] a
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 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> Symbol
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
_ [] = Maybe a
forall a. Maybe a
Nothing
takeUnique [a] -> e
_ [a
x] = a -> Maybe a
forall a. a -> Maybe a
Just a
x
takeUnique [a] -> e
f [a]
xs = e -> Maybe a
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 (Located BareType) LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
let aSigs :: [(ModName, Bool, LocSymbol, Located BareType)]
aSigs = [ (ModName
name, Bool
locallyDefined, LocSymbol
x, Located BareType
t) | (ModName
name, Spec (Located BareType) LocSymbol
spec) <- HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs
, (Bool
locallyDefined, LocSymbol
x, Located BareType
t) <- ModName
-> ModName
-> Spec (Located BareType) LocSymbol
-> [(Bool, LocSymbol, Located BareType)]
getAsmSigs ModName
myName ModName
name Spec (Located BareType) LocSymbol
spec ]
[(Maybe TyVar, (Bool, ModName, Located BareType))]
vSigs <- [(ModName, Bool, LocSymbol, Located BareType)]
-> ((ModName, Bool, LocSymbol, Located BareType)
-> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType)))
-> Either
[Error] [(Maybe TyVar, (Bool, ModName, Located BareType))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, Bool, LocSymbol, Located BareType)]
aSigs (((ModName, Bool, LocSymbol, Located BareType)
-> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType)))
-> Either
[Error] [(Maybe TyVar, (Bool, ModName, Located BareType))])
-> ((ModName, Bool, LocSymbol, Located BareType)
-> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType)))
-> Either
[Error] [(Maybe TyVar, (Bool, ModName, Located BareType))]
forall a b. (a -> b) -> a -> b
$ \(ModName
name, Bool
locallyDefined, LocSymbol
x, Located BareType
t) -> do
let (Maybe Symbol
mm, Symbol
s) = Symbol -> (Maybe Symbol, Symbol)
Bare.unQualifySymbol (LocSymbol -> Symbol
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
Maybe TyVar -> Lookup (Maybe TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol
mm, Symbol
s)
(Maybe TyVar, (Bool, ModName, Located BareType))
-> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType))
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar
vMb, (Bool
locallyDefined, ModName
name, Located BareType
t))
[(TyVar, [(Bool, ModName, Located BareType)])]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TyVar, [(Bool, ModName, Located BareType)])]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])])
-> [(TyVar, [(Bool, ModName, Located BareType)])]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
forall a b. (a -> b) -> a -> b
$ [(TyVar, (Bool, ModName, Located BareType))]
-> [(TyVar, [(Bool, ModName, Located BareType)])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [ (TyVar
v, (Bool, ModName, Located BareType)
z) | (Just TyVar
v, (Bool, ModName, Located BareType)
z) <- [(Maybe TyVar, (Bool, ModName, Located BareType))]
vSigs ]
where
lookupImportedSym :: LocSymbol -> (Maybe Symbol, Symbol) -> Lookup (Maybe TyVar)
lookupImportedSym LocSymbol
x (Maybe Symbol, Symbol)
qp =
let errRes :: Either [Error] b
errRes = [Error] -> Either [Error] b
forall a b. a -> Either a b
Left [Doc -> [Char] -> LocSymbol -> Error
Bare.errResolve Doc
"variable" [Char]
"Var" LocSymbol
x]
in Lookup (Maybe TyVar)
-> (TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar
-> Lookup (Maybe TyVar)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Lookup (Maybe TyVar)
forall {b}. Either [Error] b
errRes (Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. b -> Either a b
Right (Maybe TyVar -> Lookup (Maybe TyVar))
-> (TyVar -> Maybe TyVar) -> TyVar -> Lookup (Maybe TyVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just) (Maybe TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar -> Lookup (Maybe TyVar)
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 <- Symbol
-> HashMap Symbol [(Symbol, TyThing)] -> Maybe [(Symbol, TyThing)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
s (Env -> HashMap Symbol [(Symbol, TyThing)]
Bare._reTyThings Env
env)
Symbol
m <- Maybe Symbol
mm
[TyVar] -> Maybe TyVar
forall a. [a] -> Maybe a
Mb.listToMaybe [ TyVar
v | (Symbol
k, Ghc.AnId TyVar
v) <- [(Symbol, TyThing)]
mts, Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
m ]
isAbsoluteQualifiedSym :: Maybe Symbol -> Bool
isAbsoluteQualifiedSym (Just Symbol
m) =
Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol [Symbol] -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
m (HashMap Symbol [Symbol] -> Bool)
-> HashMap Symbol [Symbol] -> Bool
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 = TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just (TyVar -> Maybe TyVar)
-> Either [Error] TyVar -> Lookup (Maybe TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolveAsmVar-True" LocSymbol
lx
resolveAsmVar Env
env ModName
name Bool
False LocSymbol
lx = Maybe TyVar -> Lookup (Maybe TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> [Char] -> LocSymbol -> Maybe TyVar
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"resolveAsmVar-False" LocSymbol
lx Maybe TyVar -> Maybe TyVar -> Maybe TyVar
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Maybe TyVar
GM.maybeAuxVar (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)
getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, LocSymbol, LocBareType)]
getAsmSigs :: ModName
-> ModName
-> Spec (Located BareType) LocSymbol
-> [(Bool, LocSymbol, Located BareType)]
getAsmSigs ModName
myName ModName
name Spec (Located BareType) LocSymbol
spec
| ModName
myName ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
name = [ (Bool
True, LocSymbol
x, Located BareType
t) | (LocSymbol
x, Located BareType
t) <- Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec (Located BareType) LocSymbol
spec ]
| Bool
otherwise = [ (Bool
False, LocSymbol
x', Located BareType
t) | (LocSymbol
x, Located BareType
t) <- Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec (Located BareType) LocSymbol
spec
[(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
forall a. [a] -> [a] -> [a]
++ Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec (Located BareType) LocSymbol
spec
, let x' :: LocSymbol
x' = LocSymbol -> LocSymbol
forall {f :: * -> *}. Functor f => f Symbol -> f Symbol
qSym LocSymbol
x ]
where
qSym :: f Symbol -> f Symbol
qSym = (Symbol -> Symbol) -> f Symbol -> f Symbol
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> Symbol -> Symbol
GM.qualifySymbol Symbol
ns)
ns :: Symbol
ns = ModName -> Symbol
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 = (RInstance t -> [(LocSymbol, t)])
-> [RInstance t] -> [(LocSymbol, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RInstance t -> [(LocSymbol, t)]
forall {b}. RInstance b -> [(LocSymbol, b)]
go
where
go :: RInstance b -> [(LocSymbol, b)]
go RInstance b
xts = ((LocSymbol, RISig b) -> Maybe (LocSymbol, b))
-> [(LocSymbol, RISig b)] -> [(LocSymbol, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (LocSymbol, RISig b) -> Maybe (LocSymbol, b)
forall {f :: * -> *} {b}.
Functor f =>
(f Symbol, RISig b) -> Maybe (f Symbol, b)
goOne (RInstance b -> [(LocSymbol, RISig b)]
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) = (f Symbol, b) -> Maybe (f Symbol, b)
forall a. a -> Maybe a
Just ((Symbol -> Symbol) -> f Symbol -> f Symbol
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Symbol -> [Char]) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
".$c" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ) ([Char] -> [Char]) -> (Symbol -> [Char]) -> Symbol -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
F.symbolString) f Symbol
x, b
t)
goOne (f Symbol
_, RISig b
_) = Maybe (f Symbol, 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 (Located BareType) LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec (Located BareType) LocSymbol)]
specs = do
([[(TyCon, LocSpecType)]] -> [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)]
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(TyCon, LocSpecType)]] -> [(TyCon, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)]
forall a b. (a -> b) -> a -> b
$
[(ModName, DataDecl)]
-> ((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, DataDecl)]
nameDecls (((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]])
-> ((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
forall a b. (a -> b) -> a -> b
$ (ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)])
-> (ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)]
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 (Located BareType) LocSymbol
spec) <- [(ModName, Spec (Located BareType) LocSymbol)]
specs, DataDecl
d <- Spec (Located BareType) LocSymbol -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.newtyDecls Spec (Located BareType) 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 -> [(TyCon, LocSpecType)] -> Lookup [(TyCon, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCon
tc, LocSpecType
lst)]
Maybe TyCon
_ -> [(TyCon, LocSpecType)] -> Lookup [(TyCon, LocSpecType)]
forall a. a -> Either [Error] a
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
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV Located BareType
bt
bt :: Located BareType
bt = DataName -> SourcePos -> [DataCtor] -> Located BareType
forall {a}.
PPrint a =>
a -> SourcePos -> [DataCtor] -> Located BareType
getTy DataName
tcName (DataDecl -> SourcePos
tycSrcPos DataDecl
d) ([DataCtor] -> Maybe [DataCtor] -> [DataCtor]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d))
getTy :: a -> SourcePos -> [DataCtor] -> Located BareType
getTy a
_ SourcePos
l [DataCtor
c]
| [(Symbol
_, BareType
t)] <- DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
c = SourcePos -> SourcePos -> BareType -> Located BareType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l BareType
t
getTy a
n SourcePos
l [DataCtor]
_ = UserError -> Located BareType
forall a e. Exception e => e -> a
Ex.throw (a -> SourcePos -> UserError
forall {a}. PPrint a => a -> SourcePos -> UserError
mkErr a
n SourcePos
l)
mkErr :: a -> SourcePos -> UserError
mkErr a
n SourcePos
l = SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrOther (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (Doc
"Bad new type declaration:" Doc -> Doc -> Doc
<+> a -> 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 (Located BareType) LocSymbol)
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig HashMap ModName (Spec (Located BareType) LocSymbol)
specs = SpData
{ gsCtors :: [(TyVar, LocSpecType)]
gsCtors = [Char] -> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
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 (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env) SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.LqTV TyVar
x) LocSpecType
t
]
, gsMeas :: [(Symbol, LocSpecType)]
gsMeas = [ (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, RRType Reft -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RRType Reft -> SpecType) -> Located (RRType Reft) -> LocSpecType
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 = Env
-> ModName -> Measure SpecType DataCon -> Measure SpecType DataCon
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name (Measure SpecType DataCon -> Measure SpecType DataCon)
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Measure SpecType DataCon]
ms1 [Measure SpecType DataCon]
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall a. [a] -> [a] -> [a]
++ [Measure SpecType DataCon]
ms2)
, gsInvariants :: [(Maybe TyVar, LocSpecType)]
gsInvariants = ((Maybe TyVar, LocSpecType) -> SourcePos)
-> [(Maybe TyVar, LocSpecType)] -> [(Maybe TyVar, LocSpecType)]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc (LocSpecType -> SourcePos)
-> ((Maybe TyVar, LocSpecType) -> LocSpecType)
-> (Maybe TyVar, LocSpecType)
-> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe TyVar, LocSpecType) -> LocSpecType
forall a b. (a, b) -> b
snd) [(Maybe TyVar, LocSpecType)]
invs
, gsIaliases :: [(LocSpecType, LocSpecType)]
gsIaliases = ((ModName, Spec (Located BareType) LocSymbol)
-> [(LocSpecType, LocSpecType)])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(LocSpecType, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
, gsUnsorted :: [UnSortedExpr]
gsUnsorted = [UnSortedExpr]
usI [UnSortedExpr] -> [UnSortedExpr] -> [UnSortedExpr]
forall a. [a] -> [a] -> [a]
++ (Measure (Located BareType) LocSymbol -> [UnSortedExpr])
-> [Measure (Located BareType) LocSymbol] -> [UnSortedExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure (Located BareType) LocSymbol -> [UnSortedExpr]
forall ty ctor. Measure ty ctor -> [UnSortedExpr]
msUnSorted ((Spec (Located BareType) LocSymbol
-> [Measure (Located BareType) LocSymbol])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [Measure (Located BareType) LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Spec (Located BareType) LocSymbol
-> [Measure (Located BareType) LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
}
where
allowTC :: Bool
allowTC = Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)
measVars :: [(Symbol, Located (RRType Reft))]
measVars = MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv
[(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv
[(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ Env -> [(Symbol, Located (RRType Reft))]
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 = HashMap LocSymbol (Measure SpecType DataCon)
-> [Measure SpecType DataCon]
forall k v. HashMap k v -> [v]
M.elems (MSpec SpecType DataCon
-> HashMap LocSymbol (Measure SpecType DataCon)
forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
Ms.measMap MSpec SpecType DataCon
measuresSp)
ms2 :: [Measure SpecType DataCon]
ms2 = MSpec SpecType DataCon -> [Measure SpecType DataCon]
forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
Ms.imeas MSpec SpecType DataCon
measuresSp
mySpec :: Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
name :: ModName
name = GhcSrc -> ModName
_giTargetMod GhcSrc
src
([(Maybe TyVar, LocSpecType)]
minvs,[UnSortedExpr]
usI) = Env
-> ModName
-> GhcSpecSig
-> Spec (Located BareType) LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec (Located BareType) LocSymbol
mySpec
invs :: [(Maybe TyVar, LocSpecType)]
invs = [(Maybe TyVar, LocSpecType)]
minvs [(Maybe TyVar, LocSpecType)]
-> [(Maybe TyVar, LocSpecType)] -> [(Maybe TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ ((ModName, Spec (Located BareType) LocSymbol)
-> [(Maybe TyVar, LocSpecType)])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(Maybe TyVar, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases :: Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv (ModName
name, Spec (Located BareType) LocSymbol
spec)
= [ (LocSpecType, LocSpecType)
z | Right (LocSpecType, LocSpecType)
z <- (Located BareType, Located BareType)
-> Either [Error] (LocSpecType, LocSpecType)
mkIA ((Located BareType, Located BareType)
-> Either [Error] (LocSpecType, LocSpecType))
-> [(Located BareType, Located BareType)]
-> [Either [Error] (LocSpecType, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec (Located BareType) LocSymbol
-> [(Located BareType, Located BareType)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
Ms.ialiases Spec (Located BareType) LocSymbol
spec ]
where
mkIA :: (Located BareType, Located BareType)
-> Either [Error] (LocSpecType, LocSpecType)
mkIA (Located BareType
t1, Located BareType
t2) = (,) (LocSpecType -> LocSpecType -> (LocSpecType, LocSpecType))
-> Either [Error] LocSpecType
-> Either [Error] (LocSpecType -> (LocSpecType, LocSpecType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareType -> Either [Error] LocSpecType
mkI' Located BareType
t1 Either [Error] (LocSpecType -> (LocSpecType, LocSpecType))
-> Either [Error] LocSpecType
-> Either [Error] (LocSpecType, LocSpecType)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Located BareType -> Either [Error] LocSpecType
mkI' Located BareType
t2
mkI' :: Located BareType -> Either [Error] LocSpecType
mkI' = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> Either [Error] LocSpecType
Bare.cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV
makeInvariants :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(Maybe Ghc.Var, Located SpecType)]
makeInvariants :: Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv (ModName
name, Spec (Located BareType) LocSymbol
spec) =
[ (Maybe TyVar
forall a. Maybe a
Nothing, LocSpecType
t)
| (Maybe LocSymbol
_, Located BareType
bt) <- Spec (Located BareType) LocSymbol
-> [(Maybe LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
Ms.invariants Spec (Located BareType) LocSymbol
spec
, Env -> ModName -> Located BareType -> Bool
Bare.knownGhcType Env
env ModName
name Located BareType
bt
, let t :: LocSpecType
t = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV Located BareType
bt
] [(Maybe TyVar, LocSpecType)]
-> [(Maybe TyVar, LocSpecType)] -> [(Maybe TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++
[[(Maybe TyVar, LocSpecType)]] -> [(Maybe TyVar, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Maybe TyVar
forall a. Maybe a
Nothing,) (LocSpecType -> (Maybe TyVar, LocSpecType))
-> (LocSpecType -> LocSpecType)
-> LocSpecType
-> (Maybe TyVar, LocSpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> LocSpecType -> LocSpecType
makeSizeInv LocSymbol
l (LocSpecType -> (Maybe TyVar, LocSpecType))
-> [LocSpecType] -> [(Maybe TyVar, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSpecType]
ts
| ([Located BareType]
bts, LocSymbol
l) <- Spec (Located BareType) LocSymbol
-> [([Located BareType], LocSymbol)]
forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
Ms.dsize Spec (Located BareType) LocSymbol
spec
, (Located BareType -> Bool) -> [Located BareType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> ModName -> Located BareType -> Bool
Bare.knownGhcType Env
env ModName
name) [Located BareType]
bts
, let ts :: [LocSpecType]
ts = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV (Located BareType -> LocSpecType)
-> [Located BareType] -> [LocSpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareType]
bts
]
makeSizeInv :: F.LocSymbol -> Located SpecType -> Located SpecType
makeSizeInv :: LocSymbol -> LocSpecType -> LocSpecType
makeSizeInv LocSymbol
s LocSpecType
lst = LocSpecType
lst{val = go (val 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) = c
-> [RType c tv RReft]
-> [RTProp c tv RReft]
-> RReft
-> RType c tv RReft
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 RReft -> RReft -> RReft
forall r. Reftable r => r -> r -> r
`meet` RReft
nat)
go (RAllT RTVU c tv
a RType c tv RReft
t RReft
r) = RTVU c tv -> RType c tv RReft -> RReft -> RType c tv RReft
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 = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
Reft (Symbol
vv_, Brel -> Expr -> Expr -> Expr
PAtom Brel
Le (Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0) (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s) (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
vv_))))
Predicate
forall a. Monoid a => a
mempty
makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec
-> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants :: Env
-> ModName
-> GhcSpecSig
-> Spec (Located BareType) LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec (Located BareType) LocSymbol
mySpec
= ([Maybe UnSortedExpr] -> [UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
forall b c d. (b -> c) -> (d, b) -> (d, c)
mapSnd [Maybe UnSortedExpr] -> [UnSortedExpr]
forall a. [Maybe a] -> [a]
Mb.catMaybes (([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr]))
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
forall a b. (a -> b) -> a -> b
$
[((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)]
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip (Env
-> ModName
-> (LocSymbol, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv Env
env ModName
name ((LocSymbol, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr))
-> [(LocSymbol, (TyVar, LocSpecType))]
-> [((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)]
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 (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) TyVar
y ])
where
sigs :: [(TyVar, LocSpecType)]
sigs = GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
sig
xs :: [LocSymbol]
xs = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec (Located BareType) LocSymbol
mySpec)
isSymbolOfVar :: Symbol -> Ghc.Var -> Bool
isSymbolOfVar :: Symbol -> TyVar -> Bool
isSymbolOfVar Symbol
x TyVar
v = Symbol
x Symbol -> Symbol -> Bool
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 (Symbol -> Symbol) -> (TyVar -> Symbol) -> TyVar -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> Symbol) -> (TyVar -> Name) -> TyVar -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Name
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))
= [Char]
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"measureTypeToInv" ((TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just TyVar
v, LocSpecType
t {val = Bare.qualifyTop env name (F.loc x) mtype}), Maybe UnSortedExpr
usorted)
where
trep :: RTypeRep RTyCon RTyVar RReft
trep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t)
rts :: [SpecType]
rts = RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep
args :: [Symbol]
args = RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep
res :: SpecType
res = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep
z :: Symbol
z = [Symbol] -> Symbol
forall a. HasCallStack => [a] -> a
last [Symbol]
args
tz :: SpecType
tz = [SpecType] -> SpecType
forall a. HasCallStack => [a] -> a
last [SpecType]
rts
usorted :: Maybe UnSortedExpr
usorted = if SpecType -> Bool
forall {c} {tv} {r}. RType c tv r -> Bool
isSimpleADT SpecType
tz then Maybe UnSortedExpr
forall a. Maybe a
Nothing else (Symbol -> [Symbol]) -> (Symbol, Expr) -> UnSortedExpr
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[]) ((Symbol, Expr) -> UnSortedExpr)
-> Maybe (Symbol, Expr) -> Maybe UnSortedExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v) Symbol
z SpecType
tz SpecType
res
mtype :: SpecType
mtype
| [SpecType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecType]
rts
= UserError -> SpecType
forall a. UserError -> a
uError (UserError -> SpecType) -> UserError -> SpecType
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SourcePos
forall a. Located a -> SourcePos
loc LocSpecType
t) (LocSymbol -> Doc
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
_) = (RType c tv r -> Bool) -> [RType c tv r] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RType c tv r -> Bool
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 = SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen (RReft -> RReft
forall r. Reftable r => r -> r
top (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t) (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft Reft
reft' Predicate
forall a. Monoid a => a
mempty)
where
reft' :: Reft
reft' = Reft -> ((Symbol, Expr) -> Reft) -> Maybe (Symbol, Expr) -> Reft
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Reft
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 <- SpecType -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
tr
= let Reft (Symbol
v, Expr
p) = RReft -> Reft
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 (Symbol, Expr) -> Maybe (Symbol, Expr)
forall a. a -> Maybe a
Just (Symbol
v, Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p)
mkReft LocSymbol
_ Symbol
_ SpecType
_ SpecType
_
= Maybe (Symbol, Expr)
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 = [ DataConP -> DataCon -> Located DataCon
forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dc (DataConP -> DataCon
dcpCon DataConP
dc) | DataConP
dc <- [DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls ]
, gsTconsP :: [TyConP]
gsTconsP = Env -> ModName -> TyConP -> TyConP
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name (TyConP -> TyConP) -> [TyConP] -> [TyConP]
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 = [Char] -> [DataConP] -> [DataConP]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"meClasses" ([DataConP] -> [DataConP]) -> [DataConP] -> [DataConP]
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 (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
myName Env
env TCEmb TyCon
embs Spec (Located BareType) LocSymbol
mySpec HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs = (Diagnostics
diag0 Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Diagnostics
diag1, [Located DataConP]
datacons, Bare.TycEnv
{ tcTyCons :: [TyConP]
tcTyCons = [TyConP]
tycons
, tcDataCons :: [DataConP]
tcDataCons = [DataConP]
forall a. Monoid a => a
mempty
, tcSelMeasures :: [Measure SpecType DataCon]
tcSelMeasures = [Measure SpecType DataCon]
dcSelectors
, tcSelVars :: [(TyVar, LocSpecType)]
tcSelVars = [(TyVar, LocSpecType)]
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) = Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])))
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
forall a b. (a -> b) -> a -> b
$ ModName
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes ModName
myName Env
env [(ModName, Spec (Located BareType) LocSymbol)]
specs
specs :: [(ModName, Spec (Located BareType) LocSymbol)]
specs = (ModName
myName, Spec (Located BareType) LocSymbol
mySpec) (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. a -> [a] -> [a]
: HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs
tcs :: [TyConP]
tcs = (ModName, TyConP, Maybe DataPropDecl) -> TyConP
forall a b c. (a, b, c) -> b
Misc.snd3 ((ModName, TyConP, Maybe DataPropDecl) -> TyConP)
-> [(ModName, TyConP, Maybe DataPropDecl)] -> [TyConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, TyConP, Maybe DataPropDecl)]
tcDds
tyi :: TyConMap
tyi = Env -> ModName -> TyConMap -> TyConMap
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 [TyConP] -> [TyConP] -> [TyConP]
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 (Located DataConP -> Located DataConP)
-> [Located DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([[Located DataConP]] -> [Located DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs [Located DataConP] -> [Located DataConP] -> [Located DataConP]
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 = (Located DataConP -> [Measure SpecType DataCon])
-> [Located DataConP] -> [Measure SpecType DataCon]
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
charDataConLocated DataConP -> [Located DataConP] -> [Located DataConP]
forall 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 <- [Located DataConP]
-> (Located DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP)))
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (DataConP, DataConP)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Located DataConP]
classdcs ((Located DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP)))
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (DataConP, DataConP)])
-> (Located DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP)))
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (DataConP, DataConP)]
forall a b. (a -> b) -> a -> b
$ (DataConP -> IOEnv (Env TcGblEnv TcLclEnv) (DataConP, DataConP))
-> Located DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (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 [Located DataConP] -> [Located DataConP] -> [Located DataConP]
forall a. [a] -> [a] -> [a]
++ ((Located (DataConP, DataConP) -> Located DataConP)
-> [Located (DataConP, DataConP)] -> [Located DataConP]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Located (DataConP, DataConP) -> Located DataConP)
-> [Located (DataConP, DataConP)] -> [Located DataConP])
-> (((DataConP, DataConP) -> DataConP)
-> Located (DataConP, DataConP) -> Located DataConP)
-> ((DataConP, DataConP) -> DataConP)
-> [Located (DataConP, DataConP)]
-> [Located DataConP]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DataConP, DataConP) -> DataConP)
-> Located (DataConP, DataConP) -> Located DataConP
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (DataConP, DataConP) -> DataConP
forall a b. (a, b) -> b
snd [Located (DataConP, DataConP)]
lclassdcs)
TycEnv -> TcRn TycEnv
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TycEnv -> TcRn TycEnv) -> TycEnv -> TcRn TycEnv
forall a b. (a -> b) -> a -> b
$
TycEnv
tycEnv {Bare.tcSelVars = recSelectors, Bare.tcDataCons = F.val <$> ((fmap . fmap) fst lclassdcs ++ dcs )}
where
([Located DataConP]
classdcs, [Located DataConP]
dcs) =
(Located DataConP -> Bool)
-> [Located DataConP] -> ([Located DataConP], [Located DataConP])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition
(TyCon -> Bool
Ghc.isClassTyCon (TyCon -> Bool)
-> (Located DataConP -> TyCon) -> Located DataConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCon
Ghc.dataConTyCon (DataCon -> TyCon)
-> (Located DataConP -> DataCon) -> Located DataConP -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
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 = (Located DataConP -> Bool)
-> [Located DataConP] -> [Located DataConP]
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 (LocSymbol -> Bool)
-> (Located DataConP -> LocSymbol) -> Located DataConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (DataCon -> LocSymbol)
-> (Located DataConP -> DataCon) -> Located DataConP -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
val
knownWiredTyCons :: Bare.Env -> ModName -> [TyConP]
knownWiredTyCons :: Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
name = (TyConP -> Bool) -> [TyConP] -> [TyConP]
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 (LocSymbol -> Bool) -> (TyConP -> LocSymbol) -> TyConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (TyCon -> LocSymbol) -> (TyConP -> TyCon) -> TyConP -> LocSymbol
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 (Located BareType) LocSymbol)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
[(Class, [(ModName, TyVar, LocSpecType)])]
laws <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.makeCLaws Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
([DataConP]
cls, [(ModName, TyVar, LocSpecType)]
mts) <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup ([DataConP], [(ModName, TyVar, LocSpecType)])
Bare.makeClasses Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec (Located BareType) 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 <- ((ModName, Spec (Located BareType) LocSymbol)
-> Either [Error] (MSpec SpecType DataCon))
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Either [Error] [MSpec SpecType DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env
-> SigEnv
-> ModName
-> (ModName, Spec (Located BareType) LocSymbol)
-> Either [Error] (MSpec SpecType DataCon)
Bare.makeMeasureSpec Env
env SigEnv
sigEnv ModName
name) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
let measures :: MSpec SpecType DataCon
measures = [MSpec SpecType DataCon] -> MSpec SpecType DataCon
forall a. Monoid a => [a] -> a
mconcat ([Measure SpecType DataCon] -> MSpec SpecType DataCon
forall ctor ty. Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
Ms.mkMSpec' [Measure SpecType DataCon]
dcSelectors MSpec SpecType DataCon
-> [MSpec SpecType DataCon] -> [MSpec SpecType DataCon]
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 (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env) MSpec SpecType DataCon
measures
let cms :: [(LocSymbol, CMeasure (RRType Reft))]
cms = MSpec SpecType DataCon -> [(LocSymbol, CMeasure (RRType Reft))]
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, SourcePos -> SourcePos -> RRType Reft -> Located (RRType Reft)
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (RRType Reft -> Located (RRType Reft))
-> RRType Reft -> Located (RRType Reft)
forall a b. (a -> b) -> a -> b
$ CMeasure (RRType Reft) -> RRType Reft
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' = [ (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx, LocSymbol -> RRType Reft -> Located (RRType Reft)
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
, Maybe (Located (RRType Reft)) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (Symbol
-> [(Symbol, Located (RRType Reft))]
-> Maybe (Located (RRType Reft))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx) [(Symbol, Located (RRType Reft))]
cms') ]
let cs' :: [(TyVar, LocSpecType)]
cs' = [ (TyVar
v, TyVar -> SpecType -> LocSpecType
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 (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(TyVar, SpecType)]
cs ([DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls)]
MeasEnv -> Lookup MeasEnv
forall a. a -> Either [Error] a
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 [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
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 SpecType -> Located b -> LocSpecType
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ b -> Located b
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 (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
_env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE Spec (Located BareType) LocSymbol
lSpec0 = Spec (Located BareType) LocSymbol
lSpec0
{ Ms.asmSigs = F.notracepp ("makeLiftedSpec : ASSUMED-SIGS " ++ F.showpp name ) (xbs ++ myDCs)
, Ms.reflSigs = F.notracepp "REFL-SIGS" xbs
, Ms.sigs = F.notracepp ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name ) $ mkSigs (gsTySigs sig)
, Ms.invariants = [ (varLocSym <$> x, Bare.specToBare <$> t)
| (x, t) <- gsInvariants sData
, isLocInFile srcF t
]
, Ms.axeqs = gsMyAxioms refl
, Ms.aliases = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
, Ms.ealiases = M.elems . exprAliases $ myRTE
, Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
}
where
myDCs :: [(LocSymbol, Located BareType)]
myDCs = [(LocSymbol
x,Located BareType
t) | (LocSymbol
x,Located BareType
t) <- [(TyVar, LocSpecType)] -> [(LocSymbol, Located BareType)]
forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)] -> [(LocSymbol, f BareType)]
mkSigs (GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors GhcSpecData
sData)
, ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== (Symbol, Symbol) -> Symbol
forall a b. (a, b) -> a
fst (Symbol -> (Symbol, Symbol)
GM.splitModuleName (Symbol -> (Symbol, Symbol)) -> Symbol -> (Symbol, Symbol)
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x)]
mkSigs :: [(TyVar, f SpecType)] -> [(LocSymbol, f BareType)]
mkSigs [(TyVar, f SpecType)]
xts = [ (TyVar, f SpecType) -> (LocSymbol, f BareType)
forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f BareType)
toBare (TyVar
x, f SpecType
t) | (TyVar
x, f SpecType
t) <- [(TyVar, f SpecType)]
xts
, TyVar -> HashSet TyVar -> Bool
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 BareType)
toBare (TyVar
x, f SpecType
t) = (TyVar -> LocSymbol
varLocSym TyVar
x, SpecType -> BareType
Bare.specToBare (SpecType -> BareType) -> f SpecType -> f BareType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SpecType
t)
xbs :: [(LocSymbol, Located BareType)]
xbs = (TyVar, LocSpecType) -> (LocSymbol, Located BareType)
forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f BareType)
toBare ((TyVar, LocSpecType) -> (LocSymbol, Located BareType))
-> [(TyVar, LocSpecType)] -> [(LocSymbol, Located BareType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs
sigVars :: HashSet TyVar
sigVars = HashSet TyVar -> HashSet TyVar -> HashSet TyVar
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet TyVar
defVars HashSet TyVar
reflVars
defVars :: HashSet TyVar
defVars = [TyVar] -> HashSet TyVar
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 TyVar -> [TyVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl]
reflVars :: HashSet TyVar
reflVars = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
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 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
lifted Bool -> Bool -> Bool
|| Bool
isCompanion
where
lifted :: FilePath
lifted :: [Char]
lifted = a -> [Char]
forall a. Loc a => a -> [Char]
locFile a
lx
isCompanion :: Bool
isCompanion :: Bool
isCompanion =
[Char] -> [Char] -> Bool
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 = ([Char], Line, Line) -> [Char]
forall a b c. (a, b, c) -> a
Misc.fst3 (([Char], Line, Line) -> [Char])
-> (a -> ([Char], Line, Line)) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> ([Char], Line, Line)
F.sourcePosElts (SourcePos -> ([Char], Line, Line))
-> (a -> SourcePos) -> a -> ([Char], Line, Line)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> SourcePos
F.sp_start (SrcSpan -> SourcePos) -> (a -> SrcSpan) -> a -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan
varLocSym :: Ghc.Var -> LocSymbol
varLocSym :: TyVar -> LocSymbol
varLocSym TyVar
v = TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyVar -> Symbol) -> Located TyVar -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> Located TyVar
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 = [Located BareRTAlias]
-> [Located (RTAlias Symbol Expr)] -> BareRTEnv
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 (Located BareRTAlias -> Located BareRTAlias)
-> [Located BareRTAlias] -> [Located BareRTAlias]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareRTAlias]
tAs
tAs :: [Located BareRTAlias]
tAs = (BareRTEnv -> HashMap Symbol (Located BareRTAlias))
-> [Located BareRTAlias]
forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap Symbol (Located BareRTAlias)
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases
eAs :: [Located (RTAlias Symbol Expr)]
eAs = (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr)))
-> [Located (RTAlias Symbol Expr)]
forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr))
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 = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> a -> Bool
forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) ([a] -> [a]) -> (BareRTEnv -> [a]) -> BareRTEnv -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap k a -> [a]
forall k v. HashMap k v -> [v]
M.elems (HashMap k a -> [a])
-> (BareRTEnv -> HashMap k a) -> BareRTEnv -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> HashMap k a
fld (BareRTEnv -> [a]) -> BareRTEnv -> [a]
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 = [(Symbol, Located (RTAlias x a))]
-> HashMap Symbol (Located (RTAlias x a))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Located (RTAlias x a) -> Symbol
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 = [(Symbol, Located (RTAlias Symbol Expr))]
-> HashMap Symbol (Located (RTAlias Symbol Expr))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Located (RTAlias Symbol Expr) -> Symbol
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 = RTAlias x a -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias x a -> Symbol)
-> (Located (RTAlias x a) -> RTAlias x a)
-> Located (RTAlias x a)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias x a) -> RTAlias x a
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 (BareRTAlias -> BareRTAlias)
-> Located BareRTAlias -> Located BareRTAlias
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareRTAlias
lx
where
fixRTA :: BareRTAlias -> BareRTAlias
fixRTA :: BareRTAlias -> BareRTAlias
fixRTA = (Symbol -> Symbol) -> BareRTAlias -> BareRTAlias
forall a b ty. (a -> b) -> RTAlias a ty -> RTAlias b ty
mapRTAVars Symbol -> Symbol
fixArg (BareRTAlias -> BareRTAlias)
-> (BareRTAlias -> BareRTAlias) -> BareRTAlias -> BareRTAlias
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareType -> BareType) -> BareRTAlias -> BareRTAlias
forall a b. (a -> b) -> RTAlias Symbol a -> RTAlias Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BareType -> BareType
fixBody
fixArg :: Symbol -> Symbol
fixArg :: Symbol -> Symbol
fixArg = TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyVar -> Symbol) -> (Symbol -> TyVar) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TyVar
GM.symbolTyVar
fixBody :: BareType -> BareType
fixBody :: BareType -> BareType
fixBody = SpecType -> BareType
Bare.specToBare
(SpecType -> BareType)
-> (BareType -> SpecType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> SpecType
forall a. Located a -> a
F.val
(LocSpecType -> SpecType)
-> (BareType -> LocSpecType) -> BareType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.RawTV
(Located BareType -> LocSpecType)
-> (BareType -> Located BareType) -> BareType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located BareRTAlias -> BareType -> Located BareType
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, a
forall a. Monoid a => a
mempty)
withDiagnostics (Right a
v) = (Diagnostics
emptyDiagnostics, a
v)