{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Haskell.Liquid.Types.Specs (
TargetInfo(..)
, TargetSrc(..)
, TargetSpec(..)
, BareSpec(..)
, LiftedSpec(..)
, TargetDependencies(..)
, dropDependency
, isPLEVar
, isExportedVar
, QImports(..)
, Spec(..)
, GhcSpecVars(..)
, GhcSpecSig(..)
, GhcSpecNames(..)
, GhcSpecTerm(..)
, GhcSpecRefl(..)
, GhcSpecLaws(..)
, GhcSpecData(..)
, GhcSpecQual(..)
, BareDef
, BareMeasure
, SpecMeasure
, VarOrLocSymbol
, LawInstance(..)
, GhcSrc(..)
, GhcSpec(..)
, toTargetSrc
, fromTargetSrc
, toTargetSpec
, toBareSpec
, fromBareSpec
, toLiftedSpec
, unsafeFromLiftedSpec
, emptyLiftedSpec
) where
import GHC.Generics hiding (to, moduleName)
import Data.Binary
import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Misc (sortNub)
import Data.Hashable
import qualified Data.HashSet as S
import Data.HashSet (HashSet)
import qualified Data.HashMap.Strict as M
import Data.HashMap.Strict (HashMap)
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.Types.Bounds
import Liquid.GHC.API hiding (text, (<+>))
import Language.Haskell.Liquid.GHC.Types
import Text.PrettyPrint.HughesPJ (text, (<+>))
import Text.PrettyPrint.HughesPJ as HughesPJ (($$))
data TargetInfo = TargetInfo
{ TargetInfo -> TargetSrc
giSrc :: !TargetSrc
, TargetInfo -> TargetSpec
giSpec :: !TargetSpec
}
instance HasConfig TargetInfo where
getConfig :: TargetInfo -> Config
getConfig = TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig (TargetSpec -> Config)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec
data TargetSrc = TargetSrc
{ TargetSrc -> FilePath
giTarget :: !FilePath
, TargetSrc -> ModName
giTargetMod :: !ModName
, TargetSrc -> [CoreBind]
giCbs :: ![CoreBind]
, TargetSrc -> [TyCon]
gsTcs :: ![TyCon]
, TargetSrc -> Maybe [ClsInst]
gsCls :: !(Maybe [ClsInst])
, TargetSrc -> HashSet Var
giDerVars :: !(HashSet Var)
, TargetSrc -> [Var]
giImpVars :: ![Var]
, TargetSrc -> [Var]
giDefVars :: ![Var]
, TargetSrc -> [Var]
giUseVars :: ![Var]
, TargetSrc -> HashSet StableName
gsExports :: !(HashSet StableName)
, TargetSrc -> [TyCon]
gsFiTcs :: ![TyCon]
, TargetSrc -> [(Symbol, DataCon)]
gsFiDcs :: ![(F.Symbol, DataCon)]
, TargetSrc -> [TyCon]
gsPrimTcs :: ![TyCon]
, TargetSrc -> QImports
gsQualImps :: !QImports
, TargetSrc -> HashSet Symbol
gsAllImps :: !(HashSet F.Symbol)
, TargetSrc -> [TyThing]
gsTyThings :: ![TyThing]
}
data QImports = QImports
{ QImports -> HashSet Symbol
qiModules :: !(S.HashSet F.Symbol)
, QImports -> HashMap Symbol [Symbol]
qiNames :: !(M.HashMap F.Symbol [F.Symbol])
} deriving Int -> QImports -> ShowS
[QImports] -> ShowS
QImports -> FilePath
(Int -> QImports -> ShowS)
-> (QImports -> FilePath) -> ([QImports] -> ShowS) -> Show QImports
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QImports -> ShowS
showsPrec :: Int -> QImports -> ShowS
$cshow :: QImports -> FilePath
show :: QImports -> FilePath
$cshowList :: [QImports] -> ShowS
showList :: [QImports] -> ShowS
Show
data TargetSpec = TargetSpec
{ TargetSpec -> GhcSpecSig
gsSig :: !GhcSpecSig
, TargetSpec -> GhcSpecQual
gsQual :: !GhcSpecQual
, TargetSpec -> GhcSpecData
gsData :: !GhcSpecData
, TargetSpec -> GhcSpecNames
gsName :: !GhcSpecNames
, TargetSpec -> GhcSpecVars
gsVars :: !GhcSpecVars
, TargetSpec -> GhcSpecTerm
gsTerm :: !GhcSpecTerm
, TargetSpec -> GhcSpecRefl
gsRefl :: !GhcSpecRefl
, TargetSpec -> GhcSpecLaws
gsLaws :: !GhcSpecLaws
, TargetSpec -> [(Symbol, Sort)]
gsImps :: ![(F.Symbol, F.Sort)]
, TargetSpec -> Config
gsConfig :: !Config
}
deriving Int -> TargetSpec -> ShowS
[TargetSpec] -> ShowS
TargetSpec -> FilePath
(Int -> TargetSpec -> ShowS)
-> (TargetSpec -> FilePath)
-> ([TargetSpec] -> ShowS)
-> Show TargetSpec
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TargetSpec -> ShowS
showsPrec :: Int -> TargetSpec -> ShowS
$cshow :: TargetSpec -> FilePath
show :: TargetSpec -> FilePath
$cshowList :: [TargetSpec] -> ShowS
showList :: [TargetSpec] -> ShowS
Show
instance HasConfig TargetSpec where
getConfig :: TargetSpec -> Config
getConfig = TargetSpec -> Config
gsConfig
data GhcSpecVars = SpVar
{ GhcSpecVars -> [Var]
gsTgtVars :: ![Var]
, GhcSpecVars -> HashSet Var
gsIgnoreVars :: !(S.HashSet Var)
, GhcSpecVars -> HashSet Var
gsLvars :: !(S.HashSet Var)
, GhcSpecVars -> [Var]
gsCMethods :: ![Var]
}
deriving Int -> GhcSpecVars -> ShowS
[GhcSpecVars] -> ShowS
GhcSpecVars -> FilePath
(Int -> GhcSpecVars -> ShowS)
-> (GhcSpecVars -> FilePath)
-> ([GhcSpecVars] -> ShowS)
-> Show GhcSpecVars
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecVars -> ShowS
showsPrec :: Int -> GhcSpecVars -> ShowS
$cshow :: GhcSpecVars -> FilePath
show :: GhcSpecVars -> FilePath
$cshowList :: [GhcSpecVars] -> ShowS
showList :: [GhcSpecVars] -> ShowS
Show
instance Semigroup GhcSpecVars where
GhcSpecVars
sv1 <> :: GhcSpecVars -> GhcSpecVars -> GhcSpecVars
<> GhcSpecVars
sv2 = SpVar
{ gsTgtVars :: [Var]
gsTgtVars = GhcSpecVars -> [Var]
gsTgtVars GhcSpecVars
sv1 [Var] -> [Var] -> [Var]
forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> [Var]
gsTgtVars GhcSpecVars
sv2
, gsIgnoreVars :: HashSet Var
gsIgnoreVars = GhcSpecVars -> HashSet Var
gsIgnoreVars GhcSpecVars
sv1 HashSet Var -> HashSet Var -> HashSet Var
forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> HashSet Var
gsIgnoreVars GhcSpecVars
sv2
, gsLvars :: HashSet Var
gsLvars = GhcSpecVars -> HashSet Var
gsLvars GhcSpecVars
sv1 HashSet Var -> HashSet Var -> HashSet Var
forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> HashSet Var
gsLvars GhcSpecVars
sv2
, gsCMethods :: [Var]
gsCMethods = GhcSpecVars -> [Var]
gsCMethods GhcSpecVars
sv1 [Var] -> [Var] -> [Var]
forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> [Var]
gsCMethods GhcSpecVars
sv2
}
instance Monoid GhcSpecVars where
mempty :: GhcSpecVars
mempty = [Var] -> HashSet Var -> HashSet Var -> [Var] -> GhcSpecVars
SpVar [Var]
forall a. Monoid a => a
mempty HashSet Var
forall a. Monoid a => a
mempty HashSet Var
forall a. Monoid a => a
mempty [Var]
forall a. Monoid a => a
mempty
data GhcSpecQual = SpQual
{ GhcSpecQual -> [Qualifier]
gsQualifiers :: ![F.Qualifier]
, GhcSpecQual -> [Located SpecRTAlias]
gsRTAliases :: ![F.Located SpecRTAlias]
}
deriving Int -> GhcSpecQual -> ShowS
[GhcSpecQual] -> ShowS
GhcSpecQual -> FilePath
(Int -> GhcSpecQual -> ShowS)
-> (GhcSpecQual -> FilePath)
-> ([GhcSpecQual] -> ShowS)
-> Show GhcSpecQual
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecQual -> ShowS
showsPrec :: Int -> GhcSpecQual -> ShowS
$cshow :: GhcSpecQual -> FilePath
show :: GhcSpecQual -> FilePath
$cshowList :: [GhcSpecQual] -> ShowS
showList :: [GhcSpecQual] -> ShowS
Show
data GhcSpecSig = SpSig
{ GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs :: ![(Var, LocSpecType)]
, GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs :: ![(Var, LocSpecType)]
, GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs :: ![(Var, LocSpecType)]
, GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs :: ![(Var, LocSpecType)]
, GhcSpecSig -> [(TyCon, LocSpecType)]
gsNewTypes :: ![(TyCon, LocSpecType)]
, GhcSpecSig -> DEnv Var LocSpecType
gsDicts :: !(DEnv Var LocSpecType)
, GhcSpecSig -> [(Var, MethodType LocSpecType)]
gsMethods :: ![(Var, MethodType LocSpecType)]
, GhcSpecSig -> [(Var, LocSpecType, [Located Expr])]
gsTexprs :: ![(Var, LocSpecType, [F.Located F.Expr])]
, GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
, GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
}
deriving Int -> GhcSpecSig -> ShowS
[GhcSpecSig] -> ShowS
GhcSpecSig -> FilePath
(Int -> GhcSpecSig -> ShowS)
-> (GhcSpecSig -> FilePath)
-> ([GhcSpecSig] -> ShowS)
-> Show GhcSpecSig
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecSig -> ShowS
showsPrec :: Int -> GhcSpecSig -> ShowS
$cshow :: GhcSpecSig -> FilePath
show :: GhcSpecSig -> FilePath
$cshowList :: [GhcSpecSig] -> ShowS
showList :: [GhcSpecSig] -> ShowS
Show
instance Semigroup GhcSpecSig where
GhcSpecSig
x <> :: GhcSpecSig -> GhcSpecSig -> GhcSpecSig
<> GhcSpecSig
y = SpSig
{ gsTySigs :: [(Var, LocSpecType)]
gsTySigs = GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
x [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
y
, gsAsmSigs :: [(Var, LocSpecType)]
gsAsmSigs = GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
x [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
y
, gsRefSigs :: [(Var, LocSpecType)]
gsRefSigs = GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
x [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
y
, gsInSigs :: [(Var, LocSpecType)]
gsInSigs = GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
x [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
y
, gsNewTypes :: [(TyCon, LocSpecType)]
gsNewTypes = GhcSpecSig -> [(TyCon, LocSpecType)]
gsNewTypes GhcSpecSig
x [(TyCon, LocSpecType)]
-> [(TyCon, LocSpecType)] -> [(TyCon, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(TyCon, LocSpecType)]
gsNewTypes GhcSpecSig
y
, gsDicts :: DEnv Var LocSpecType
gsDicts = GhcSpecSig -> DEnv Var LocSpecType
gsDicts GhcSpecSig
x DEnv Var LocSpecType
-> DEnv Var LocSpecType -> DEnv Var LocSpecType
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> DEnv Var LocSpecType
gsDicts GhcSpecSig
y
, gsMethods :: [(Var, MethodType LocSpecType)]
gsMethods = GhcSpecSig -> [(Var, MethodType LocSpecType)]
gsMethods GhcSpecSig
x [(Var, MethodType LocSpecType)]
-> [(Var, MethodType LocSpecType)]
-> [(Var, MethodType LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, MethodType LocSpecType)]
gsMethods GhcSpecSig
y
, gsTexprs :: [(Var, LocSpecType, [Located Expr])]
gsTexprs = GhcSpecSig -> [(Var, LocSpecType, [Located Expr])]
gsTexprs GhcSpecSig
x [(Var, LocSpecType, [Located Expr])]
-> [(Var, LocSpecType, [Located Expr])]
-> [(Var, LocSpecType, [Located Expr])]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType, [Located Expr])]
gsTexprs GhcSpecSig
y
, gsRelation :: [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsRelation = GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsRelation GhcSpecSig
x [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsRelation GhcSpecSig
y
, gsAsmRel :: [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel = GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel GhcSpecSig
x [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel GhcSpecSig
y
}
instance Monoid GhcSpecSig where
mempty :: GhcSpecSig
mempty = [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(TyCon, LocSpecType)]
-> DEnv Var LocSpecType
-> [(Var, MethodType LocSpecType)]
-> [(Var, LocSpecType, [Located Expr])]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> GhcSpecSig
SpSig [(Var, LocSpecType)]
forall a. Monoid a => a
mempty [(Var, LocSpecType)]
forall a. Monoid a => a
mempty [(Var, LocSpecType)]
forall a. Monoid a => a
mempty [(Var, LocSpecType)]
forall a. Monoid a => a
mempty [(TyCon, LocSpecType)]
forall a. Monoid a => a
mempty DEnv Var LocSpecType
forall a. Monoid a => a
mempty [(Var, MethodType LocSpecType)]
forall a. Monoid a => a
mempty [(Var, LocSpecType, [Located Expr])]
forall a. Monoid a => a
mempty [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
forall a. Monoid a => a
mempty [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
forall a. Monoid a => a
mempty
data GhcSpecData = SpData
{ GhcSpecData -> [(Var, LocSpecType)]
gsCtors :: ![(Var, LocSpecType)]
, GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas :: ![(F.Symbol, LocSpecType)]
, GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants :: ![(Maybe Var, LocSpecType)]
, GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases :: ![(LocSpecType, LocSpecType)]
, GhcSpecData -> [Measure (RType RTyCon RTyVar (UReft Reft)) DataCon]
gsMeasures :: ![Measure SpecType DataCon]
, GhcSpecData -> [UnSortedExpr]
gsUnsorted :: ![UnSortedExpr]
}
deriving Int -> GhcSpecData -> ShowS
[GhcSpecData] -> ShowS
GhcSpecData -> FilePath
(Int -> GhcSpecData -> ShowS)
-> (GhcSpecData -> FilePath)
-> ([GhcSpecData] -> ShowS)
-> Show GhcSpecData
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecData -> ShowS
showsPrec :: Int -> GhcSpecData -> ShowS
$cshow :: GhcSpecData -> FilePath
show :: GhcSpecData -> FilePath
$cshowList :: [GhcSpecData] -> ShowS
showList :: [GhcSpecData] -> ShowS
Show
data GhcSpecNames = SpNames
{ GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms :: ![(F.Symbol, Var)]
, GhcSpecNames -> [Located DataCon]
gsDconsP :: ![F.Located DataCon]
, GhcSpecNames -> [TyConP]
gsTconsP :: ![TyConP]
, GhcSpecNames -> TCEmb TyCon
gsTcEmbeds :: !(F.TCEmb TyCon)
, GhcSpecNames -> [DataDecl]
gsADTs :: ![F.DataDecl]
, GhcSpecNames -> TyConMap
gsTyconEnv :: !TyConMap
}
deriving Int -> GhcSpecNames -> ShowS
[GhcSpecNames] -> ShowS
GhcSpecNames -> FilePath
(Int -> GhcSpecNames -> ShowS)
-> (GhcSpecNames -> FilePath)
-> ([GhcSpecNames] -> ShowS)
-> Show GhcSpecNames
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecNames -> ShowS
showsPrec :: Int -> GhcSpecNames -> ShowS
$cshow :: GhcSpecNames -> FilePath
show :: GhcSpecNames -> FilePath
$cshowList :: [GhcSpecNames] -> ShowS
showList :: [GhcSpecNames] -> ShowS
Show
deriving instance Show TyConP
deriving instance Show TyConMap
data GhcSpecTerm = SpTerm
{ GhcSpecTerm -> HashSet Var
gsStTerm :: !(S.HashSet Var)
, GhcSpecTerm -> HashSet TyCon
gsAutosize :: !(S.HashSet TyCon)
, GhcSpecTerm -> HashSet Var
gsLazy :: !(S.HashSet Var)
, GhcSpecTerm -> HashSet (Located Var)
gsFail :: !(S.HashSet (F.Located Var))
, GhcSpecTerm -> HashSet Var
gsNonStTerm :: !(S.HashSet Var)
}
deriving Int -> GhcSpecTerm -> ShowS
[GhcSpecTerm] -> ShowS
GhcSpecTerm -> FilePath
(Int -> GhcSpecTerm -> ShowS)
-> (GhcSpecTerm -> FilePath)
-> ([GhcSpecTerm] -> ShowS)
-> Show GhcSpecTerm
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecTerm -> ShowS
showsPrec :: Int -> GhcSpecTerm -> ShowS
$cshow :: GhcSpecTerm -> FilePath
show :: GhcSpecTerm -> FilePath
$cshowList :: [GhcSpecTerm] -> ShowS
showList :: [GhcSpecTerm] -> ShowS
Show
instance Semigroup GhcSpecTerm where
GhcSpecTerm
t1 <> :: GhcSpecTerm -> GhcSpecTerm -> GhcSpecTerm
<> GhcSpecTerm
t2 = SpTerm
{ gsStTerm :: HashSet Var
gsStTerm = GhcSpecTerm -> HashSet Var
gsStTerm GhcSpecTerm
t1 HashSet Var -> HashSet Var -> HashSet Var
forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet Var
gsStTerm GhcSpecTerm
t2
, gsAutosize :: HashSet TyCon
gsAutosize = GhcSpecTerm -> HashSet TyCon
gsAutosize GhcSpecTerm
t1 HashSet TyCon -> HashSet TyCon -> HashSet TyCon
forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet TyCon
gsAutosize GhcSpecTerm
t2
, gsLazy :: HashSet Var
gsLazy = GhcSpecTerm -> HashSet Var
gsLazy GhcSpecTerm
t1 HashSet Var -> HashSet Var -> HashSet Var
forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet Var
gsLazy GhcSpecTerm
t2
, gsFail :: HashSet (Located Var)
gsFail = GhcSpecTerm -> HashSet (Located Var)
gsFail GhcSpecTerm
t1 HashSet (Located Var)
-> HashSet (Located Var) -> HashSet (Located Var)
forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet (Located Var)
gsFail GhcSpecTerm
t2
, gsNonStTerm :: HashSet Var
gsNonStTerm = GhcSpecTerm -> HashSet Var
gsNonStTerm GhcSpecTerm
t1 HashSet Var -> HashSet Var -> HashSet Var
forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet Var
gsNonStTerm GhcSpecTerm
t2
}
instance Monoid GhcSpecTerm where
mempty :: GhcSpecTerm
mempty = HashSet Var
-> HashSet TyCon
-> HashSet Var
-> HashSet (Located Var)
-> HashSet Var
-> GhcSpecTerm
SpTerm HashSet Var
forall a. Monoid a => a
mempty HashSet TyCon
forall a. Monoid a => a
mempty HashSet Var
forall a. Monoid a => a
mempty HashSet (Located Var)
forall a. Monoid a => a
mempty HashSet Var
forall a. Monoid a => a
mempty
data GhcSpecRefl = SpRefl
{ GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst :: !(M.HashMap Var (Maybe Int))
, GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms :: ![(Var, LocSpecType, F.Equation)]
, GhcSpecRefl -> [Equation]
gsImpAxioms :: ![F.Equation]
, GhcSpecRefl -> [Equation]
gsMyAxioms :: ![F.Equation]
, GhcSpecRefl -> [Var]
gsReflects :: ![Var]
, GhcSpecRefl -> LogicMap
gsLogicMap :: !LogicMap
, GhcSpecRefl -> [Var]
gsWiredReft :: ![Var]
, GhcSpecRefl -> HashSet (Located Var)
gsRewrites :: S.HashSet (F.Located Var)
, GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith :: M.HashMap Var [Var]
}
deriving Int -> GhcSpecRefl -> ShowS
[GhcSpecRefl] -> ShowS
GhcSpecRefl -> FilePath
(Int -> GhcSpecRefl -> ShowS)
-> (GhcSpecRefl -> FilePath)
-> ([GhcSpecRefl] -> ShowS)
-> Show GhcSpecRefl
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecRefl -> ShowS
showsPrec :: Int -> GhcSpecRefl -> ShowS
$cshow :: GhcSpecRefl -> FilePath
show :: GhcSpecRefl -> FilePath
$cshowList :: [GhcSpecRefl] -> ShowS
showList :: [GhcSpecRefl] -> ShowS
Show
instance Semigroup GhcSpecRefl where
GhcSpecRefl
x <> :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl
<> GhcSpecRefl
y = SpRefl
{ gsAutoInst :: HashMap Var (Maybe Int)
gsAutoInst = GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst GhcSpecRefl
x HashMap Var (Maybe Int)
-> HashMap Var (Maybe Int) -> HashMap Var (Maybe Int)
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst GhcSpecRefl
y
, gsHAxioms :: [(Var, LocSpecType, Equation)]
gsHAxioms = GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
x [(Var, LocSpecType, Equation)]
-> [(Var, LocSpecType, Equation)] -> [(Var, LocSpecType, Equation)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
y
, gsImpAxioms :: [Equation]
gsImpAxioms = GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
x [Equation] -> [Equation] -> [Equation]
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
y
, gsMyAxioms :: [Equation]
gsMyAxioms = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
x [Equation] -> [Equation] -> [Equation]
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
y
, gsReflects :: [Var]
gsReflects = GhcSpecRefl -> [Var]
gsReflects GhcSpecRefl
x [Var] -> [Var] -> [Var]
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Var]
gsReflects GhcSpecRefl
y
, gsLogicMap :: LogicMap
gsLogicMap = GhcSpecRefl -> LogicMap
gsLogicMap GhcSpecRefl
x LogicMap -> LogicMap -> LogicMap
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> LogicMap
gsLogicMap GhcSpecRefl
y
, gsWiredReft :: [Var]
gsWiredReft = GhcSpecRefl -> [Var]
gsWiredReft GhcSpecRefl
x [Var] -> [Var] -> [Var]
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Var]
gsWiredReft GhcSpecRefl
y
, gsRewrites :: HashSet (Located Var)
gsRewrites = GhcSpecRefl -> HashSet (Located Var)
gsRewrites GhcSpecRefl
x HashSet (Located Var)
-> HashSet (Located Var) -> HashSet (Located Var)
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> HashSet (Located Var)
gsRewrites GhcSpecRefl
y
, gsRewritesWith :: HashMap Var [Var]
gsRewritesWith = GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith GhcSpecRefl
x HashMap Var [Var] -> HashMap Var [Var] -> HashMap Var [Var]
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith GhcSpecRefl
y
}
instance Monoid GhcSpecRefl where
mempty :: GhcSpecRefl
mempty = HashMap Var (Maybe Int)
-> [(Var, LocSpecType, Equation)]
-> [Equation]
-> [Equation]
-> [Var]
-> LogicMap
-> [Var]
-> HashSet (Located Var)
-> HashMap Var [Var]
-> GhcSpecRefl
SpRefl HashMap Var (Maybe Int)
forall a. Monoid a => a
mempty [(Var, LocSpecType, Equation)]
forall a. Monoid a => a
mempty [Equation]
forall a. Monoid a => a
mempty
[Equation]
forall a. Monoid a => a
mempty [Var]
forall a. Monoid a => a
mempty LogicMap
forall a. Monoid a => a
mempty
[Var]
forall a. Monoid a => a
mempty HashSet (Located Var)
forall a. Monoid a => a
mempty HashMap Var [Var]
forall a. Monoid a => a
mempty
data GhcSpecLaws = SpLaws
{ GhcSpecLaws -> [(Class, [(Var, LocSpecType)])]
gsLawDefs :: ![(Class, [(Var, LocSpecType)])]
, GhcSpecLaws -> [LawInstance]
gsLawInst :: ![LawInstance]
}
deriving Int -> GhcSpecLaws -> ShowS
[GhcSpecLaws] -> ShowS
GhcSpecLaws -> FilePath
(Int -> GhcSpecLaws -> ShowS)
-> (GhcSpecLaws -> FilePath)
-> ([GhcSpecLaws] -> ShowS)
-> Show GhcSpecLaws
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecLaws -> ShowS
showsPrec :: Int -> GhcSpecLaws -> ShowS
$cshow :: GhcSpecLaws -> FilePath
show :: GhcSpecLaws -> FilePath
$cshowList :: [GhcSpecLaws] -> ShowS
showList :: [GhcSpecLaws] -> ShowS
Show
data LawInstance = LawInstance
{ LawInstance -> Class
lilName :: Class
, LawInstance -> [LocSpecType]
liSupers :: [LocSpecType]
, LawInstance -> [LocSpecType]
lilTyArgs :: [LocSpecType]
, LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
, LawInstance -> SrcSpan
lilPos :: SrcSpan
}
deriving Int -> LawInstance -> ShowS
[LawInstance] -> ShowS
LawInstance -> FilePath
(Int -> LawInstance -> ShowS)
-> (LawInstance -> FilePath)
-> ([LawInstance] -> ShowS)
-> Show LawInstance
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LawInstance -> ShowS
showsPrec :: Int -> LawInstance -> ShowS
$cshow :: LawInstance -> FilePath
show :: LawInstance -> FilePath
$cshowList :: [LawInstance] -> ShowS
showList :: [LawInstance] -> ShowS
Show
type VarOrLocSymbol = Either Var LocSymbol
type BareMeasure = Measure LocBareType F.LocSymbol
type BareDef = Def LocBareType F.LocSymbol
type SpecMeasure = Measure LocSpecType DataCon
newtype BareSpec =
MkBareSpec { BareSpec -> Spec LocBareType LocSymbol
getBareSpec :: Spec LocBareType F.LocSymbol }
deriving ((forall x. BareSpec -> Rep BareSpec x)
-> (forall x. Rep BareSpec x -> BareSpec) -> Generic BareSpec
forall x. Rep BareSpec x -> BareSpec
forall x. BareSpec -> Rep BareSpec x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BareSpec -> Rep BareSpec x
from :: forall x. BareSpec -> Rep BareSpec x
$cto :: forall x. Rep BareSpec x -> BareSpec
to :: forall x. Rep BareSpec x -> BareSpec
Generic, Int -> BareSpec -> ShowS
[BareSpec] -> ShowS
BareSpec -> FilePath
(Int -> BareSpec -> ShowS)
-> (BareSpec -> FilePath) -> ([BareSpec] -> ShowS) -> Show BareSpec
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BareSpec -> ShowS
showsPrec :: Int -> BareSpec -> ShowS
$cshow :: BareSpec -> FilePath
show :: BareSpec -> FilePath
$cshowList :: [BareSpec] -> ShowS
showList :: [BareSpec] -> ShowS
Show, Get BareSpec
[BareSpec] -> Put
BareSpec -> Put
(BareSpec -> Put)
-> Get BareSpec -> ([BareSpec] -> Put) -> Binary BareSpec
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: BareSpec -> Put
put :: BareSpec -> Put
$cget :: Get BareSpec
get :: Get BareSpec
$cputList :: [BareSpec] -> Put
putList :: [BareSpec] -> Put
Binary)
instance Semigroup BareSpec where
BareSpec
x <> :: BareSpec -> BareSpec -> BareSpec
<> BareSpec
y = MkBareSpec { getBareSpec :: Spec LocBareType LocSymbol
getBareSpec = BareSpec -> Spec LocBareType LocSymbol
getBareSpec BareSpec
x Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol -> Spec LocBareType LocSymbol
forall a. Semigroup a => a -> a -> a
<> BareSpec -> Spec LocBareType LocSymbol
getBareSpec BareSpec
y }
instance Monoid BareSpec where
mempty :: BareSpec
mempty = MkBareSpec { getBareSpec :: Spec LocBareType LocSymbol
getBareSpec = Spec LocBareType LocSymbol
forall a. Monoid a => a
mempty }
data Spec ty bndr = Spec
{ forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures :: ![Measure ty bndr]
, forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs :: ![(F.Symbol, F.Sort)]
, forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs :: ![(F.Symbol, F.Sort)]
, forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs :: ![(F.LocSymbol, ty)]
, forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs :: ![(F.LocSymbol, ty)]
, forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs :: ![(F.LocSymbol, ty)]
, forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs :: ![(F.LocSymbol, ty)]
, forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants :: ![(Maybe F.LocSymbol, ty)]
, forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases :: ![(ty, ty)]
, forall ty bndr. Spec ty bndr -> [Symbol]
imports :: ![F.Symbol]
, forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls :: ![DataDecl]
, forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls :: ![DataDecl]
, forall ty bndr. Spec ty bndr -> [FilePath]
includes :: ![FilePath]
, forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases :: ![F.Located (RTAlias F.Symbol BareType)]
, forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases :: ![F.Located (RTAlias F.Symbol F.Expr)]
, forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds :: !(F.TCEmb F.LocSymbol)
, forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers :: ![F.Qualifier]
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lazy :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
rewrites :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol])
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
fails :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
reflects :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois :: !(M.HashMap F.LocSymbol (Maybe Int))
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hmeas :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hbounds :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
inlines :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
ignores :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize :: !(S.HashSet F.LocSymbol)
, forall ty bndr. Spec ty bndr -> [Located FilePath]
pragmas :: ![F.Located String]
, forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures :: ![Measure ty ()]
, forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures :: ![Measure ty bndr]
, forall ty bndr. Spec ty bndr -> [RClass ty]
classes :: ![RClass ty]
, forall ty bndr. Spec ty bndr -> [RClass ty]
claws :: ![RClass ty]
, forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
, forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
, forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
termexprs :: ![(F.LocSymbol, [F.Located F.Expr])]
, forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance :: ![RInstance ty]
, forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws :: ![RILaws ty]
, forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance :: ![(F.LocSymbol, [Variance])]
, forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize :: ![([ty], F.LocSymbol)]
, forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds :: !(RRBEnv ty)
, forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs :: !(M.HashMap F.LocSymbol F.Symbol)
, forall ty bndr. Spec ty bndr -> [Equation]
axeqs :: ![F.Equation]
} deriving ((forall x. Spec ty bndr -> Rep (Spec ty bndr) x)
-> (forall x. Rep (Spec ty bndr) x -> Spec ty bndr)
-> Generic (Spec ty bndr)
forall x. Rep (Spec ty bndr) x -> Spec ty bndr
forall x. Spec ty bndr -> Rep (Spec ty bndr) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ty bndr x. Rep (Spec ty bndr) x -> Spec ty bndr
forall ty bndr x. Spec ty bndr -> Rep (Spec ty bndr) x
$cfrom :: forall ty bndr x. Spec ty bndr -> Rep (Spec ty bndr) x
from :: forall x. Spec ty bndr -> Rep (Spec ty bndr) x
$cto :: forall ty bndr x. Rep (Spec ty bndr) x -> Spec ty bndr
to :: forall x. Rep (Spec ty bndr) x -> Spec ty bndr
Generic, Int -> Spec ty bndr -> ShowS
[Spec ty bndr] -> ShowS
Spec ty bndr -> FilePath
(Int -> Spec ty bndr -> ShowS)
-> (Spec ty bndr -> FilePath)
-> ([Spec ty bndr] -> ShowS)
-> Show (Spec ty bndr)
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Int -> Spec ty bndr -> ShowS
forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
[Spec ty bndr] -> ShowS
forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Spec ty bndr -> FilePath
$cshowsPrec :: forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Int -> Spec ty bndr -> ShowS
showsPrec :: Int -> Spec ty bndr -> ShowS
$cshow :: forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Spec ty bndr -> FilePath
show :: Spec ty bndr -> FilePath
$cshowList :: forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
[Spec ty bndr] -> ShowS
showList :: [Spec ty bndr] -> ShowS
Show)
instance Binary (Spec LocBareType F.LocSymbol)
instance (Show ty, Show bndr, F.PPrint ty, F.PPrint bndr) => F.PPrint (Spec ty bndr) where
pprintTidy :: Tidy -> Spec ty bndr -> Doc
pprintTidy Tidy
k Spec ty bndr
sp = FilePath -> Doc
text FilePath
"dataDecls = " Doc -> Doc -> Doc
<+> Tidy -> [DataDecl] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Spec ty bndr -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls Spec ty bndr
sp)
Doc -> Doc -> Doc
HughesPJ.$$
FilePath -> Doc
text FilePath
"classes = " Doc -> Doc -> Doc
<+> Tidy -> [RClass ty] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Spec ty bndr -> [RClass ty]
forall ty bndr. Spec ty bndr -> [RClass ty]
classes Spec ty bndr
sp)
Doc -> Doc -> Doc
HughesPJ.$$
FilePath -> Doc
text FilePath
"sigs = " Doc -> Doc -> Doc
<+> Tidy -> [(LocSymbol, ty)] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs Spec ty bndr
sp)
instance Semigroup (Spec ty bndr) where
Spec ty bndr
s1 <> :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr
<> Spec ty bndr
s2
= Spec { measures :: [Measure ty bndr]
measures = Spec ty bndr -> [Measure ty bndr]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures Spec ty bndr
s1 [Measure ty bndr] -> [Measure ty bndr] -> [Measure ty bndr]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Measure ty bndr]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures Spec ty bndr
s2
, impSigs :: [(Symbol, Sort)]
impSigs = Spec ty bndr -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs Spec ty bndr
s1 [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs Spec ty bndr
s2
, expSigs :: [(Symbol, Sort)]
expSigs = Spec ty bndr -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs Spec ty bndr
s1 [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs Spec ty bndr
s2
, asmSigs :: [(LocSymbol, ty)]
asmSigs = Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs Spec ty bndr
s1 [(LocSymbol, ty)] -> [(LocSymbol, ty)] -> [(LocSymbol, ty)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs Spec ty bndr
s2
, sigs :: [(LocSymbol, ty)]
sigs = Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs Spec ty bndr
s1 [(LocSymbol, ty)] -> [(LocSymbol, ty)] -> [(LocSymbol, ty)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs Spec ty bndr
s2
, localSigs :: [(LocSymbol, ty)]
localSigs = Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs Spec ty bndr
s1 [(LocSymbol, ty)] -> [(LocSymbol, ty)] -> [(LocSymbol, ty)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs Spec ty bndr
s2
, reflSigs :: [(LocSymbol, ty)]
reflSigs = Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs Spec ty bndr
s1 [(LocSymbol, ty)] -> [(LocSymbol, ty)] -> [(LocSymbol, ty)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs Spec ty bndr
s2
, invariants :: [(Maybe LocSymbol, ty)]
invariants = Spec ty bndr -> [(Maybe LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants Spec ty bndr
s1 [(Maybe LocSymbol, ty)]
-> [(Maybe LocSymbol, ty)] -> [(Maybe LocSymbol, ty)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(Maybe LocSymbol, ty)]
forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants Spec ty bndr
s2
, ialiases :: [(ty, ty)]
ialiases = Spec ty bndr -> [(ty, ty)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases Spec ty bndr
s1 [(ty, ty)] -> [(ty, ty)] -> [(ty, ty)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(ty, ty)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases Spec ty bndr
s2
, imports :: [Symbol]
imports = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
sortNub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> [Symbol]
forall ty bndr. Spec ty bndr -> [Symbol]
imports Spec ty bndr
s1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Symbol]
forall ty bndr. Spec ty bndr -> [Symbol]
imports Spec ty bndr
s2
, dataDecls :: [DataDecl]
dataDecls = Spec ty bndr -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls Spec ty bndr
s1 [DataDecl] -> [DataDecl] -> [DataDecl]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls Spec ty bndr
s2
, newtyDecls :: [DataDecl]
newtyDecls = Spec ty bndr -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls Spec ty bndr
s1 [DataDecl] -> [DataDecl] -> [DataDecl]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls Spec ty bndr
s2
, includes :: [FilePath]
includes = [FilePath] -> [FilePath]
forall a. Ord a => [a] -> [a]
sortNub ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> [FilePath]
forall ty bndr. Spec ty bndr -> [FilePath]
includes Spec ty bndr
s1 [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [FilePath]
forall ty bndr. Spec ty bndr -> [FilePath]
includes Spec ty bndr
s2
, aliases :: [Located (RTAlias Symbol BareType)]
aliases = Spec ty bndr -> [Located (RTAlias Symbol BareType)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases Spec ty bndr
s1 [Located (RTAlias Symbol BareType)]
-> [Located (RTAlias Symbol BareType)]
-> [Located (RTAlias Symbol BareType)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Located (RTAlias Symbol BareType)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases Spec ty bndr
s2
, ealiases :: [Located (RTAlias Symbol Expr)]
ealiases = Spec ty bndr -> [Located (RTAlias Symbol Expr)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases Spec ty bndr
s1 [Located (RTAlias Symbol Expr)]
-> [Located (RTAlias Symbol Expr)]
-> [Located (RTAlias Symbol Expr)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Located (RTAlias Symbol Expr)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases Spec ty bndr
s2
, qualifiers :: [Qualifier]
qualifiers = Spec ty bndr -> [Qualifier]
forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers Spec ty bndr
s1 [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Qualifier]
forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers Spec ty bndr
s2
, pragmas :: [Located FilePath]
pragmas = Spec ty bndr -> [Located FilePath]
forall ty bndr. Spec ty bndr -> [Located FilePath]
pragmas Spec ty bndr
s1 [Located FilePath] -> [Located FilePath] -> [Located FilePath]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Located FilePath]
forall ty bndr. Spec ty bndr -> [Located FilePath]
pragmas Spec ty bndr
s2
, cmeasures :: [Measure ty ()]
cmeasures = Spec ty bndr -> [Measure ty ()]
forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures Spec ty bndr
s1 [Measure ty ()] -> [Measure ty ()] -> [Measure ty ()]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Measure ty ()]
forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures Spec ty bndr
s2
, imeasures :: [Measure ty bndr]
imeasures = Spec ty bndr -> [Measure ty bndr]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures Spec ty bndr
s1 [Measure ty bndr] -> [Measure ty bndr] -> [Measure ty bndr]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Measure ty bndr]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures Spec ty bndr
s2
, classes :: [RClass ty]
classes = Spec ty bndr -> [RClass ty]
forall ty bndr. Spec ty bndr -> [RClass ty]
classes Spec ty bndr
s1 [RClass ty] -> [RClass ty] -> [RClass ty]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [RClass ty]
forall ty bndr. Spec ty bndr -> [RClass ty]
classes Spec ty bndr
s2
, claws :: [RClass ty]
claws = Spec ty bndr -> [RClass ty]
forall ty bndr. Spec ty bndr -> [RClass ty]
claws Spec ty bndr
s1 [RClass ty] -> [RClass ty] -> [RClass ty]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [RClass ty]
forall ty bndr. Spec ty bndr -> [RClass ty]
claws Spec ty bndr
s2
, relational :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational = Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational Spec ty bndr
s1 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
-> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
-> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational Spec ty bndr
s2
, asmRel :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel = Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel Spec ty bndr
s1 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
-> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
-> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel Spec ty bndr
s2
, termexprs :: [(LocSymbol, [Located Expr])]
termexprs = Spec ty bndr -> [(LocSymbol, [Located Expr])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
termexprs Spec ty bndr
s1 [(LocSymbol, [Located Expr])]
-> [(LocSymbol, [Located Expr])] -> [(LocSymbol, [Located Expr])]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, [Located Expr])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
termexprs Spec ty bndr
s2
, rinstance :: [RInstance ty]
rinstance = Spec ty bndr -> [RInstance ty]
forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance Spec ty bndr
s1 [RInstance ty] -> [RInstance ty] -> [RInstance ty]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [RInstance ty]
forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance Spec ty bndr
s2
, ilaws :: [RILaws ty]
ilaws = Spec ty bndr -> [RILaws ty]
forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws Spec ty bndr
s1 [RILaws ty] -> [RILaws ty] -> [RILaws ty]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [RILaws ty]
forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws Spec ty bndr
s2
, dvariance :: [(LocSymbol, [Variance])]
dvariance = Spec ty bndr -> [(LocSymbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance Spec ty bndr
s1 [(LocSymbol, [Variance])]
-> [(LocSymbol, [Variance])] -> [(LocSymbol, [Variance])]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [(LocSymbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance Spec ty bndr
s2
, dsize :: [([ty], LocSymbol)]
dsize = Spec ty bndr -> [([ty], LocSymbol)]
forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize Spec ty bndr
s1 [([ty], LocSymbol)] -> [([ty], LocSymbol)] -> [([ty], LocSymbol)]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [([ty], LocSymbol)]
forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize Spec ty bndr
s2
, axeqs :: [Equation]
axeqs = Spec ty bndr -> [Equation]
forall ty bndr. Spec ty bndr -> [Equation]
axeqs Spec ty bndr
s1 [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ Spec ty bndr -> [Equation]
forall ty bndr. Spec ty bndr -> [Equation]
axeqs Spec ty bndr
s2
, embeds :: TCEmb LocSymbol
embeds = TCEmb LocSymbol -> TCEmb LocSymbol -> TCEmb LocSymbol
forall a. Monoid a => a -> a -> a
mappend (Spec ty bndr -> TCEmb LocSymbol
forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds Spec ty bndr
s1) (Spec ty bndr -> TCEmb LocSymbol
forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds Spec ty bndr
s2)
, lvars :: HashSet LocSymbol
lvars = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars Spec ty bndr
s2)
, lazy :: HashSet LocSymbol
lazy = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lazy Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lazy Spec ty bndr
s2)
, rewrites :: HashSet LocSymbol
rewrites = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
rewrites Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
rewrites Spec ty bndr
s2)
, rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = HashMap LocSymbol [LocSymbol]
-> HashMap LocSymbol [LocSymbol] -> HashMap LocSymbol [LocSymbol]
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union (Spec ty bndr -> HashMap LocSymbol [LocSymbol]
forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
rewriteWith Spec ty bndr
s1) (Spec ty bndr -> HashMap LocSymbol [LocSymbol]
forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
rewriteWith Spec ty bndr
s2)
, fails :: HashSet LocSymbol
fails = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
fails Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
fails Spec ty bndr
s2)
, reflects :: HashSet LocSymbol
reflects = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
reflects Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
reflects Spec ty bndr
s2)
, hmeas :: HashSet LocSymbol
hmeas = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hmeas Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hmeas Spec ty bndr
s2)
, hbounds :: HashSet LocSymbol
hbounds = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hbounds Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hbounds Spec ty bndr
s2)
, inlines :: HashSet LocSymbol
inlines = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
inlines Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
inlines Spec ty bndr
s2)
, ignores :: HashSet LocSymbol
ignores = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
ignores Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
ignores Spec ty bndr
s2)
, autosize :: HashSet LocSymbol
autosize = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize Spec ty bndr
s1) (Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize Spec ty bndr
s2)
, bounds :: RRBEnv ty
bounds = RRBEnv ty -> RRBEnv ty -> RRBEnv ty
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union (Spec ty bndr -> RRBEnv ty
forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds Spec ty bndr
s1) (Spec ty bndr -> RRBEnv ty
forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds Spec ty bndr
s2)
, defs :: HashMap LocSymbol Symbol
defs = HashMap LocSymbol Symbol
-> HashMap LocSymbol Symbol -> HashMap LocSymbol Symbol
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union (Spec ty bndr -> HashMap LocSymbol Symbol
forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs Spec ty bndr
s1) (Spec ty bndr -> HashMap LocSymbol Symbol
forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs Spec ty bndr
s2)
, autois :: HashMap LocSymbol (Maybe Int)
autois = HashMap LocSymbol (Maybe Int)
-> HashMap LocSymbol (Maybe Int) -> HashMap LocSymbol (Maybe Int)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union (Spec ty bndr -> HashMap LocSymbol (Maybe Int)
forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois Spec ty bndr
s1) (Spec ty bndr -> HashMap LocSymbol (Maybe Int)
forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois Spec ty bndr
s2)
}
instance Monoid (Spec ty bndr) where
mappend :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr
mappend = Spec ty bndr -> Spec ty bndr -> Spec ty bndr
forall a. Semigroup a => a -> a -> a
(<>)
mempty :: Spec ty bndr
mempty
= Spec { measures :: [Measure ty bndr]
measures = []
, impSigs :: [(Symbol, Sort)]
impSigs = []
, expSigs :: [(Symbol, Sort)]
expSigs = []
, asmSigs :: [(LocSymbol, ty)]
asmSigs = []
, sigs :: [(LocSymbol, ty)]
sigs = []
, localSigs :: [(LocSymbol, ty)]
localSigs = []
, reflSigs :: [(LocSymbol, ty)]
reflSigs = []
, invariants :: [(Maybe LocSymbol, ty)]
invariants = []
, ialiases :: [(ty, ty)]
ialiases = []
, imports :: [Symbol]
imports = []
, dataDecls :: [DataDecl]
dataDecls = []
, newtyDecls :: [DataDecl]
newtyDecls = []
, includes :: [FilePath]
includes = []
, aliases :: [Located (RTAlias Symbol BareType)]
aliases = []
, ealiases :: [Located (RTAlias Symbol Expr)]
ealiases = []
, embeds :: TCEmb LocSymbol
embeds = TCEmb LocSymbol
forall a. Monoid a => a
mempty
, qualifiers :: [Qualifier]
qualifiers = []
, lvars :: HashSet LocSymbol
lvars = HashSet LocSymbol
forall a. HashSet a
S.empty
, lazy :: HashSet LocSymbol
lazy = HashSet LocSymbol
forall a. HashSet a
S.empty
, rewrites :: HashSet LocSymbol
rewrites = HashSet LocSymbol
forall a. HashSet a
S.empty
, rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = HashMap LocSymbol [LocSymbol]
forall k v. HashMap k v
M.empty
, fails :: HashSet LocSymbol
fails = HashSet LocSymbol
forall a. HashSet a
S.empty
, autois :: HashMap LocSymbol (Maybe Int)
autois = HashMap LocSymbol (Maybe Int)
forall k v. HashMap k v
M.empty
, hmeas :: HashSet LocSymbol
hmeas = HashSet LocSymbol
forall a. HashSet a
S.empty
, reflects :: HashSet LocSymbol
reflects = HashSet LocSymbol
forall a. HashSet a
S.empty
, hbounds :: HashSet LocSymbol
hbounds = HashSet LocSymbol
forall a. HashSet a
S.empty
, inlines :: HashSet LocSymbol
inlines = HashSet LocSymbol
forall a. HashSet a
S.empty
, ignores :: HashSet LocSymbol
ignores = HashSet LocSymbol
forall a. HashSet a
S.empty
, autosize :: HashSet LocSymbol
autosize = HashSet LocSymbol
forall a. HashSet a
S.empty
, pragmas :: [Located FilePath]
pragmas = []
, cmeasures :: [Measure ty ()]
cmeasures = []
, imeasures :: [Measure ty bndr]
imeasures = []
, classes :: [RClass ty]
classes = []
, claws :: [RClass ty]
claws = []
, relational :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational = []
, asmRel :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel = []
, termexprs :: [(LocSymbol, [Located Expr])]
termexprs = []
, rinstance :: [RInstance ty]
rinstance = []
, ilaws :: [RILaws ty]
ilaws = []
, dvariance :: [(LocSymbol, [Variance])]
dvariance = []
, dsize :: [([ty], LocSymbol)]
dsize = []
, axeqs :: [Equation]
axeqs = []
, bounds :: RRBEnv ty
bounds = RRBEnv ty
forall k v. HashMap k v
M.empty
, defs :: HashMap LocSymbol Symbol
defs = HashMap LocSymbol Symbol
forall k v. HashMap k v
M.empty
}
data LiftedSpec = LiftedSpec
{ LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedMeasures :: HashSet (Measure LocBareType F.LocSymbol)
, LiftedSpec -> HashSet (Symbol, Sort)
liftedImpSigs :: HashSet (F.Symbol, F.Sort)
, LiftedSpec -> HashSet (Symbol, Sort)
liftedExpSigs :: HashSet (F.Symbol, F.Sort)
, LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedAsmSigs :: HashSet (F.LocSymbol, LocBareType)
, LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedSigs :: HashSet (F.LocSymbol, LocBareType)
, LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareType)
, LiftedSpec -> HashSet (LocBareType, LocBareType)
liftedIaliases :: HashSet (LocBareType, LocBareType)
, LiftedSpec -> HashSet Symbol
liftedImports :: HashSet F.Symbol
, LiftedSpec -> HashSet DataDecl
liftedDataDecls :: HashSet DataDecl
, LiftedSpec -> HashSet DataDecl
liftedNewtyDecls :: HashSet DataDecl
, LiftedSpec -> HashSet (Located (RTAlias Symbol BareType))
liftedAliases :: HashSet (F.Located (RTAlias F.Symbol BareType))
, LiftedSpec -> HashSet (Located (RTAlias Symbol Expr))
liftedEaliases :: HashSet (F.Located (RTAlias F.Symbol F.Expr))
, LiftedSpec -> TCEmb LocSymbol
liftedEmbeds :: F.TCEmb F.LocSymbol
, LiftedSpec -> HashSet Qualifier
liftedQualifiers :: HashSet F.Qualifier
, LiftedSpec -> HashSet LocSymbol
liftedLvars :: HashSet F.LocSymbol
, LiftedSpec -> HashMap LocSymbol (Maybe Int)
liftedAutois :: M.HashMap F.LocSymbol (Maybe Int)
, LiftedSpec -> HashSet LocSymbol
liftedAutosize :: HashSet F.LocSymbol
, LiftedSpec -> HashSet (Measure LocBareType ())
liftedCmeasures :: HashSet (Measure LocBareType ())
, LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedImeasures :: HashSet (Measure LocBareType F.LocSymbol)
, LiftedSpec -> HashSet (RClass LocBareType)
liftedClasses :: HashSet (RClass LocBareType)
, LiftedSpec -> HashSet (RClass LocBareType)
liftedClaws :: HashSet (RClass LocBareType)
, LiftedSpec -> HashSet (RInstance LocBareType)
liftedRinstance :: HashSet (RInstance LocBareType)
, LiftedSpec -> HashSet (RILaws LocBareType)
liftedIlaws :: HashSet (RILaws LocBareType)
, LiftedSpec -> [([LocBareType], LocSymbol)]
liftedDsize :: [([LocBareType], F.LocSymbol)]
, LiftedSpec -> HashSet (LocSymbol, [Variance])
liftedDvariance :: HashSet (F.LocSymbol, [Variance])
, LiftedSpec -> RRBEnv LocBareType
liftedBounds :: RRBEnv LocBareType
, LiftedSpec -> HashMap LocSymbol Symbol
liftedDefs :: M.HashMap F.LocSymbol F.Symbol
, LiftedSpec -> HashSet Equation
liftedAxeqs :: HashSet F.Equation
} deriving (LiftedSpec -> LiftedSpec -> Bool
(LiftedSpec -> LiftedSpec -> Bool)
-> (LiftedSpec -> LiftedSpec -> Bool) -> Eq LiftedSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LiftedSpec -> LiftedSpec -> Bool
== :: LiftedSpec -> LiftedSpec -> Bool
$c/= :: LiftedSpec -> LiftedSpec -> Bool
/= :: LiftedSpec -> LiftedSpec -> Bool
Eq, (forall x. LiftedSpec -> Rep LiftedSpec x)
-> (forall x. Rep LiftedSpec x -> LiftedSpec) -> Generic LiftedSpec
forall x. Rep LiftedSpec x -> LiftedSpec
forall x. LiftedSpec -> Rep LiftedSpec x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LiftedSpec -> Rep LiftedSpec x
from :: forall x. LiftedSpec -> Rep LiftedSpec x
$cto :: forall x. Rep LiftedSpec x -> LiftedSpec
to :: forall x. Rep LiftedSpec x -> LiftedSpec
Generic, Int -> LiftedSpec -> ShowS
[LiftedSpec] -> ShowS
LiftedSpec -> FilePath
(Int -> LiftedSpec -> ShowS)
-> (LiftedSpec -> FilePath)
-> ([LiftedSpec] -> ShowS)
-> Show LiftedSpec
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LiftedSpec -> ShowS
showsPrec :: Int -> LiftedSpec -> ShowS
$cshow :: LiftedSpec -> FilePath
show :: LiftedSpec -> FilePath
$cshowList :: [LiftedSpec] -> ShowS
showList :: [LiftedSpec] -> ShowS
Show)
deriving Eq LiftedSpec
Eq LiftedSpec =>
(Int -> LiftedSpec -> Int)
-> (LiftedSpec -> Int) -> Hashable LiftedSpec
Int -> LiftedSpec -> Int
LiftedSpec -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> LiftedSpec -> Int
hashWithSalt :: Int -> LiftedSpec -> Int
$chash :: LiftedSpec -> Int
hash :: LiftedSpec -> Int
Hashable via Generically LiftedSpec
deriving Get LiftedSpec
[LiftedSpec] -> Put
LiftedSpec -> Put
(LiftedSpec -> Put)
-> Get LiftedSpec -> ([LiftedSpec] -> Put) -> Binary LiftedSpec
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: LiftedSpec -> Put
put :: LiftedSpec -> Put
$cget :: Get LiftedSpec
get :: Get LiftedSpec
$cputList :: [LiftedSpec] -> Put
putList :: [LiftedSpec] -> Put
Binary via Generically LiftedSpec
instance Binary F.Equation
emptyLiftedSpec :: LiftedSpec
emptyLiftedSpec :: LiftedSpec
emptyLiftedSpec = LiftedSpec
{ liftedMeasures :: HashSet (Measure LocBareType LocSymbol)
liftedMeasures = HashSet (Measure LocBareType LocSymbol)
forall a. Monoid a => a
mempty
, liftedImpSigs :: HashSet (Symbol, Sort)
liftedImpSigs = HashSet (Symbol, Sort)
forall a. Monoid a => a
mempty
, liftedExpSigs :: HashSet (Symbol, Sort)
liftedExpSigs = HashSet (Symbol, Sort)
forall a. Monoid a => a
mempty
, liftedAsmSigs :: HashSet (LocSymbol, LocBareType)
liftedAsmSigs = HashSet (LocSymbol, LocBareType)
forall a. Monoid a => a
mempty
, liftedSigs :: HashSet (LocSymbol, LocBareType)
liftedSigs = HashSet (LocSymbol, LocBareType)
forall a. Monoid a => a
mempty
, liftedInvariants :: HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants = HashSet (Maybe LocSymbol, LocBareType)
forall a. Monoid a => a
mempty
, liftedIaliases :: HashSet (LocBareType, LocBareType)
liftedIaliases = HashSet (LocBareType, LocBareType)
forall a. Monoid a => a
mempty
, liftedImports :: HashSet Symbol
liftedImports = HashSet Symbol
forall a. Monoid a => a
mempty
, liftedDataDecls :: HashSet DataDecl
liftedDataDecls = HashSet DataDecl
forall a. Monoid a => a
mempty
, liftedNewtyDecls :: HashSet DataDecl
liftedNewtyDecls = HashSet DataDecl
forall a. Monoid a => a
mempty
, liftedAliases :: HashSet (Located (RTAlias Symbol BareType))
liftedAliases = HashSet (Located (RTAlias Symbol BareType))
forall a. Monoid a => a
mempty
, liftedEaliases :: HashSet (Located (RTAlias Symbol Expr))
liftedEaliases = HashSet (Located (RTAlias Symbol Expr))
forall a. Monoid a => a
mempty
, liftedEmbeds :: TCEmb LocSymbol
liftedEmbeds = TCEmb LocSymbol
forall a. Monoid a => a
mempty
, liftedQualifiers :: HashSet Qualifier
liftedQualifiers = HashSet Qualifier
forall a. Monoid a => a
mempty
, liftedLvars :: HashSet LocSymbol
liftedLvars = HashSet LocSymbol
forall a. Monoid a => a
mempty
, liftedAutois :: HashMap LocSymbol (Maybe Int)
liftedAutois = HashMap LocSymbol (Maybe Int)
forall a. Monoid a => a
mempty
, liftedAutosize :: HashSet LocSymbol
liftedAutosize = HashSet LocSymbol
forall a. Monoid a => a
mempty
, liftedCmeasures :: HashSet (Measure LocBareType ())
liftedCmeasures = HashSet (Measure LocBareType ())
forall a. Monoid a => a
mempty
, liftedImeasures :: HashSet (Measure LocBareType LocSymbol)
liftedImeasures = HashSet (Measure LocBareType LocSymbol)
forall a. Monoid a => a
mempty
, liftedClasses :: HashSet (RClass LocBareType)
liftedClasses = HashSet (RClass LocBareType)
forall a. Monoid a => a
mempty
, liftedClaws :: HashSet (RClass LocBareType)
liftedClaws = HashSet (RClass LocBareType)
forall a. Monoid a => a
mempty
, liftedRinstance :: HashSet (RInstance LocBareType)
liftedRinstance = HashSet (RInstance LocBareType)
forall a. Monoid a => a
mempty
, liftedIlaws :: HashSet (RILaws LocBareType)
liftedIlaws = HashSet (RILaws LocBareType)
forall a. Monoid a => a
mempty
, liftedDvariance :: HashSet (LocSymbol, [Variance])
liftedDvariance = HashSet (LocSymbol, [Variance])
forall a. Monoid a => a
mempty
, liftedDsize :: [([LocBareType], LocSymbol)]
liftedDsize = [([LocBareType], LocSymbol)]
forall a. Monoid a => a
mempty
, liftedBounds :: RRBEnv LocBareType
liftedBounds = RRBEnv LocBareType
forall a. Monoid a => a
mempty
, liftedDefs :: HashMap LocSymbol Symbol
liftedDefs = HashMap LocSymbol Symbol
forall a. Monoid a => a
mempty
, liftedAxeqs :: HashSet Equation
liftedAxeqs = HashSet Equation
forall a. Monoid a => a
mempty
}
newtype TargetDependencies =
TargetDependencies { TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies :: HashMap StableModule LiftedSpec }
deriving (TargetDependencies -> TargetDependencies -> Bool
(TargetDependencies -> TargetDependencies -> Bool)
-> (TargetDependencies -> TargetDependencies -> Bool)
-> Eq TargetDependencies
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TargetDependencies -> TargetDependencies -> Bool
== :: TargetDependencies -> TargetDependencies -> Bool
$c/= :: TargetDependencies -> TargetDependencies -> Bool
/= :: TargetDependencies -> TargetDependencies -> Bool
Eq, Int -> TargetDependencies -> ShowS
[TargetDependencies] -> ShowS
TargetDependencies -> FilePath
(Int -> TargetDependencies -> ShowS)
-> (TargetDependencies -> FilePath)
-> ([TargetDependencies] -> ShowS)
-> Show TargetDependencies
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TargetDependencies -> ShowS
showsPrec :: Int -> TargetDependencies -> ShowS
$cshow :: TargetDependencies -> FilePath
show :: TargetDependencies -> FilePath
$cshowList :: [TargetDependencies] -> ShowS
showList :: [TargetDependencies] -> ShowS
Show, (forall x. TargetDependencies -> Rep TargetDependencies x)
-> (forall x. Rep TargetDependencies x -> TargetDependencies)
-> Generic TargetDependencies
forall x. Rep TargetDependencies x -> TargetDependencies
forall x. TargetDependencies -> Rep TargetDependencies x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TargetDependencies -> Rep TargetDependencies x
from :: forall x. TargetDependencies -> Rep TargetDependencies x
$cto :: forall x. Rep TargetDependencies x -> TargetDependencies
to :: forall x. Rep TargetDependencies x -> TargetDependencies
Generic)
deriving Get TargetDependencies
[TargetDependencies] -> Put
TargetDependencies -> Put
(TargetDependencies -> Put)
-> Get TargetDependencies
-> ([TargetDependencies] -> Put)
-> Binary TargetDependencies
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: TargetDependencies -> Put
put :: TargetDependencies -> Put
$cget :: Get TargetDependencies
get :: Get TargetDependencies
$cputList :: [TargetDependencies] -> Put
putList :: [TargetDependencies] -> Put
Binary via Generically TargetDependencies
instance Semigroup TargetDependencies where
TargetDependencies
x <> :: TargetDependencies -> TargetDependencies -> TargetDependencies
<> TargetDependencies
y = TargetDependencies
{ getDependencies :: HashMap StableModule LiftedSpec
getDependencies = TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
x HashMap StableModule LiftedSpec
-> HashMap StableModule LiftedSpec
-> HashMap StableModule LiftedSpec
forall a. Semigroup a => a -> a -> a
<> TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
y
}
instance Monoid TargetDependencies where
mempty :: TargetDependencies
mempty = HashMap StableModule LiftedSpec -> TargetDependencies
TargetDependencies HashMap StableModule LiftedSpec
forall a. Monoid a => a
mempty
dropDependency :: StableModule -> TargetDependencies -> TargetDependencies
dropDependency :: StableModule -> TargetDependencies -> TargetDependencies
dropDependency StableModule
sm (TargetDependencies HashMap StableModule LiftedSpec
deps) = HashMap StableModule LiftedSpec -> TargetDependencies
TargetDependencies (StableModule
-> HashMap StableModule LiftedSpec
-> HashMap StableModule LiftedSpec
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete StableModule
sm HashMap StableModule LiftedSpec
deps)
isPLEVar :: TargetSpec -> Var -> Bool
isPLEVar :: TargetSpec -> Var -> Bool
isPLEVar TargetSpec
sp Var
x = Var -> HashMap Var (Maybe Int) -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Var
x (GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst (TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp))
isExportedVar :: TargetSrc -> Var -> Bool
isExportedVar :: TargetSrc -> Var -> Bool
isExportedVar TargetSrc
src Var
v = Name -> StableName
mkStableName Name
n StableName -> HashSet StableName -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet StableName
ns
where
n :: Name
n = Var -> Name
forall a. NamedThing a => a -> Name
getName Var
v
ns :: HashSet StableName
ns = TargetSrc -> HashSet StableName
gsExports TargetSrc
src
data GhcSrc = Src
{ GhcSrc -> FilePath
_giTarget :: !FilePath
, GhcSrc -> ModName
_giTargetMod :: !ModName
, GhcSrc -> [CoreBind]
_giCbs :: ![CoreBind]
, GhcSrc -> [TyCon]
_gsTcs :: ![TyCon]
, GhcSrc -> Maybe [ClsInst]
_gsCls :: !(Maybe [ClsInst])
, GhcSrc -> HashSet Var
_giDerVars :: !(S.HashSet Var)
, GhcSrc -> [Var]
_giImpVars :: ![Var]
, GhcSrc -> [Var]
_giDefVars :: ![Var]
, GhcSrc -> [Var]
_giUseVars :: ![Var]
, GhcSrc -> HashSet StableName
_gsExports :: !(HashSet StableName)
, GhcSrc -> [TyCon]
_gsFiTcs :: ![TyCon]
, GhcSrc -> [(Symbol, DataCon)]
_gsFiDcs :: ![(F.Symbol, DataCon)]
, GhcSrc -> [TyCon]
_gsPrimTcs :: ![TyCon]
, GhcSrc -> QImports
_gsQualImps :: !QImports
, GhcSrc -> HashSet Symbol
_gsAllImps :: !(S.HashSet F.Symbol)
, GhcSrc -> [TyThing]
_gsTyThings :: ![TyThing]
}
data GhcSpec = SP
{ GhcSpec -> GhcSpecSig
_gsSig :: !GhcSpecSig
, GhcSpec -> GhcSpecQual
_gsQual :: !GhcSpecQual
, GhcSpec -> GhcSpecData
_gsData :: !GhcSpecData
, GhcSpec -> GhcSpecNames
_gsName :: !GhcSpecNames
, GhcSpec -> GhcSpecVars
_gsVars :: !GhcSpecVars
, GhcSpec -> GhcSpecTerm
_gsTerm :: !GhcSpecTerm
, GhcSpec -> GhcSpecRefl
_gsRefl :: !GhcSpecRefl
, GhcSpec -> GhcSpecLaws
_gsLaws :: !GhcSpecLaws
, GhcSpec -> [(Symbol, Sort)]
_gsImps :: ![(F.Symbol, F.Sort)]
, GhcSpec -> Config
_gsConfig :: !Config
, GhcSpec -> Spec LocBareType LocSymbol
_gsLSpec :: !(Spec LocBareType F.LocSymbol)
}
instance HasConfig GhcSpec where
getConfig :: GhcSpec -> Config
getConfig = GhcSpec -> Config
_gsConfig
toTargetSrc :: GhcSrc -> TargetSrc
toTargetSrc :: GhcSrc -> TargetSrc
toTargetSrc GhcSrc
a = TargetSrc
{ giTarget :: FilePath
giTarget = GhcSrc -> FilePath
_giTarget GhcSrc
a
, giTargetMod :: ModName
giTargetMod = GhcSrc -> ModName
_giTargetMod GhcSrc
a
, giCbs :: [CoreBind]
giCbs = GhcSrc -> [CoreBind]
_giCbs GhcSrc
a
, gsTcs :: [TyCon]
gsTcs = GhcSrc -> [TyCon]
_gsTcs GhcSrc
a
, gsCls :: Maybe [ClsInst]
gsCls = GhcSrc -> Maybe [ClsInst]
_gsCls GhcSrc
a
, giDerVars :: HashSet Var
giDerVars = GhcSrc -> HashSet Var
_giDerVars GhcSrc
a
, giImpVars :: [Var]
giImpVars = GhcSrc -> [Var]
_giImpVars GhcSrc
a
, giDefVars :: [Var]
giDefVars = GhcSrc -> [Var]
_giDefVars GhcSrc
a
, giUseVars :: [Var]
giUseVars = GhcSrc -> [Var]
_giUseVars GhcSrc
a
, gsExports :: HashSet StableName
gsExports = GhcSrc -> HashSet StableName
_gsExports GhcSrc
a
, gsFiTcs :: [TyCon]
gsFiTcs = GhcSrc -> [TyCon]
_gsFiTcs GhcSrc
a
, gsFiDcs :: [(Symbol, DataCon)]
gsFiDcs = GhcSrc -> [(Symbol, DataCon)]
_gsFiDcs GhcSrc
a
, gsPrimTcs :: [TyCon]
gsPrimTcs = GhcSrc -> [TyCon]
_gsPrimTcs GhcSrc
a
, gsQualImps :: QImports
gsQualImps = GhcSrc -> QImports
_gsQualImps GhcSrc
a
, gsAllImps :: HashSet Symbol
gsAllImps = GhcSrc -> HashSet Symbol
_gsAllImps GhcSrc
a
, gsTyThings :: [TyThing]
gsTyThings = GhcSrc -> [TyThing]
_gsTyThings GhcSrc
a
}
fromTargetSrc :: TargetSrc -> GhcSrc
fromTargetSrc :: TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
a = Src
{ _giTarget :: FilePath
_giTarget = TargetSrc -> FilePath
giTarget TargetSrc
a
, _giTargetMod :: ModName
_giTargetMod = TargetSrc -> ModName
giTargetMod TargetSrc
a
, _giCbs :: [CoreBind]
_giCbs = TargetSrc -> [CoreBind]
giCbs TargetSrc
a
, _gsTcs :: [TyCon]
_gsTcs = TargetSrc -> [TyCon]
gsTcs TargetSrc
a
, _gsCls :: Maybe [ClsInst]
_gsCls = TargetSrc -> Maybe [ClsInst]
gsCls TargetSrc
a
, _giDerVars :: HashSet Var
_giDerVars = TargetSrc -> HashSet Var
giDerVars TargetSrc
a
, _giImpVars :: [Var]
_giImpVars = TargetSrc -> [Var]
giImpVars TargetSrc
a
, _giDefVars :: [Var]
_giDefVars = TargetSrc -> [Var]
giDefVars TargetSrc
a
, _giUseVars :: [Var]
_giUseVars = TargetSrc -> [Var]
giUseVars TargetSrc
a
, _gsExports :: HashSet StableName
_gsExports = TargetSrc -> HashSet StableName
gsExports TargetSrc
a
, _gsFiTcs :: [TyCon]
_gsFiTcs = TargetSrc -> [TyCon]
gsFiTcs TargetSrc
a
, _gsFiDcs :: [(Symbol, DataCon)]
_gsFiDcs = TargetSrc -> [(Symbol, DataCon)]
gsFiDcs TargetSrc
a
, _gsPrimTcs :: [TyCon]
_gsPrimTcs = TargetSrc -> [TyCon]
gsPrimTcs TargetSrc
a
, _gsQualImps :: QImports
_gsQualImps = TargetSrc -> QImports
gsQualImps TargetSrc
a
, _gsAllImps :: HashSet Symbol
_gsAllImps = TargetSrc -> HashSet Symbol
gsAllImps TargetSrc
a
, _gsTyThings :: [TyThing]
_gsTyThings = TargetSrc -> [TyThing]
gsTyThings TargetSrc
a
}
toTargetSpec :: GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec :: GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec GhcSpec
ghcSpec =
(TargetSpec
targetSpec, (Spec LocBareType LocSymbol -> LiftedSpec
toLiftedSpec (Spec LocBareType LocSymbol -> LiftedSpec)
-> (GhcSpec -> Spec LocBareType LocSymbol) -> GhcSpec -> LiftedSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec -> Spec LocBareType LocSymbol
_gsLSpec) GhcSpec
ghcSpec)
where
targetSpec :: TargetSpec
targetSpec = TargetSpec
{ gsSig :: GhcSpecSig
gsSig = GhcSpec -> GhcSpecSig
_gsSig GhcSpec
ghcSpec
, gsQual :: GhcSpecQual
gsQual = GhcSpec -> GhcSpecQual
_gsQual GhcSpec
ghcSpec
, gsData :: GhcSpecData
gsData = GhcSpec -> GhcSpecData
_gsData GhcSpec
ghcSpec
, gsName :: GhcSpecNames
gsName = GhcSpec -> GhcSpecNames
_gsName GhcSpec
ghcSpec
, gsVars :: GhcSpecVars
gsVars = GhcSpec -> GhcSpecVars
_gsVars GhcSpec
ghcSpec
, gsTerm :: GhcSpecTerm
gsTerm = GhcSpec -> GhcSpecTerm
_gsTerm GhcSpec
ghcSpec
, gsRefl :: GhcSpecRefl
gsRefl = GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
ghcSpec
, gsLaws :: GhcSpecLaws
gsLaws = GhcSpec -> GhcSpecLaws
_gsLaws GhcSpec
ghcSpec
, gsImps :: [(Symbol, Sort)]
gsImps = GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
ghcSpec
, gsConfig :: Config
gsConfig = GhcSpec -> Config
_gsConfig GhcSpec
ghcSpec
}
toBareSpec :: Spec LocBareType F.LocSymbol -> BareSpec
toBareSpec :: Spec LocBareType LocSymbol -> BareSpec
toBareSpec = Spec LocBareType LocSymbol -> BareSpec
MkBareSpec
fromBareSpec :: BareSpec -> Spec LocBareType F.LocSymbol
fromBareSpec :: BareSpec -> Spec LocBareType LocSymbol
fromBareSpec = BareSpec -> Spec LocBareType LocSymbol
getBareSpec
toLiftedSpec :: Spec LocBareType F.LocSymbol -> LiftedSpec
toLiftedSpec :: Spec LocBareType LocSymbol -> LiftedSpec
toLiftedSpec Spec LocBareType LocSymbol
a = LiftedSpec
{ liftedMeasures :: HashSet (Measure LocBareType LocSymbol)
liftedMeasures = [Measure LocBareType LocSymbol]
-> HashSet (Measure LocBareType LocSymbol)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Measure LocBareType LocSymbol]
-> HashSet (Measure LocBareType LocSymbol))
-> (Spec LocBareType LocSymbol -> [Measure LocBareType LocSymbol])
-> Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType LocSymbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures (Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType LocSymbol))
-> Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType LocSymbol)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedImpSigs :: HashSet (Symbol, Sort)
liftedImpSigs = [(Symbol, Sort)] -> HashSet (Symbol, Sort)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Symbol, Sort)] -> HashSet (Symbol, Sort))
-> (Spec LocBareType LocSymbol -> [(Symbol, Sort)])
-> Spec LocBareType LocSymbol
-> HashSet (Symbol, Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs (Spec LocBareType LocSymbol -> HashSet (Symbol, Sort))
-> Spec LocBareType LocSymbol -> HashSet (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedExpSigs :: HashSet (Symbol, Sort)
liftedExpSigs = [(Symbol, Sort)] -> HashSet (Symbol, Sort)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Symbol, Sort)] -> HashSet (Symbol, Sort))
-> (Spec LocBareType LocSymbol -> [(Symbol, Sort)])
-> Spec LocBareType LocSymbol
-> HashSet (Symbol, Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs (Spec LocBareType LocSymbol -> HashSet (Symbol, Sort))
-> Spec LocBareType LocSymbol -> HashSet (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedAsmSigs :: HashSet (LocSymbol, LocBareType)
liftedAsmSigs = [(LocSymbol, LocBareType)] -> HashSet (LocSymbol, LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(LocSymbol, LocBareType)] -> HashSet (LocSymbol, LocBareType))
-> (Spec LocBareType LocSymbol -> [(LocSymbol, LocBareType)])
-> Spec LocBareType LocSymbol
-> HashSet (LocSymbol, LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs (Spec LocBareType LocSymbol -> HashSet (LocSymbol, LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (LocSymbol, LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedSigs :: HashSet (LocSymbol, LocBareType)
liftedSigs = [(LocSymbol, LocBareType)] -> HashSet (LocSymbol, LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(LocSymbol, LocBareType)] -> HashSet (LocSymbol, LocBareType))
-> (Spec LocBareType LocSymbol -> [(LocSymbol, LocBareType)])
-> Spec LocBareType LocSymbol
-> HashSet (LocSymbol, LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs (Spec LocBareType LocSymbol -> HashSet (LocSymbol, LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (LocSymbol, LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedInvariants :: HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants = [(Maybe LocSymbol, LocBareType)]
-> HashSet (Maybe LocSymbol, LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Maybe LocSymbol, LocBareType)]
-> HashSet (Maybe LocSymbol, LocBareType))
-> (Spec LocBareType LocSymbol -> [(Maybe LocSymbol, LocBareType)])
-> Spec LocBareType LocSymbol
-> HashSet (Maybe LocSymbol, LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(Maybe LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants (Spec LocBareType LocSymbol
-> HashSet (Maybe LocSymbol, LocBareType))
-> Spec LocBareType LocSymbol
-> HashSet (Maybe LocSymbol, LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedIaliases :: HashSet (LocBareType, LocBareType)
liftedIaliases = [(LocBareType, LocBareType)] -> HashSet (LocBareType, LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(LocBareType, LocBareType)]
-> HashSet (LocBareType, LocBareType))
-> (Spec LocBareType LocSymbol -> [(LocBareType, LocBareType)])
-> Spec LocBareType LocSymbol
-> HashSet (LocBareType, LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(LocBareType, LocBareType)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases (Spec LocBareType LocSymbol -> HashSet (LocBareType, LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (LocBareType, LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedImports :: HashSet Symbol
liftedImports = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> (Spec LocBareType LocSymbol -> [Symbol])
-> Spec LocBareType LocSymbol
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Symbol]
forall ty bndr. Spec ty bndr -> [Symbol]
imports (Spec LocBareType LocSymbol -> HashSet Symbol)
-> Spec LocBareType LocSymbol -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedDataDecls :: HashSet DataDecl
liftedDataDecls = [DataDecl] -> HashSet DataDecl
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([DataDecl] -> HashSet DataDecl)
-> (Spec LocBareType LocSymbol -> [DataDecl])
-> Spec LocBareType LocSymbol
-> HashSet DataDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls (Spec LocBareType LocSymbol -> HashSet DataDecl)
-> Spec LocBareType LocSymbol -> HashSet DataDecl
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedNewtyDecls :: HashSet DataDecl
liftedNewtyDecls = [DataDecl] -> HashSet DataDecl
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([DataDecl] -> HashSet DataDecl)
-> (Spec LocBareType LocSymbol -> [DataDecl])
-> Spec LocBareType LocSymbol
-> HashSet DataDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls (Spec LocBareType LocSymbol -> HashSet DataDecl)
-> Spec LocBareType LocSymbol -> HashSet DataDecl
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedAliases :: HashSet (Located (RTAlias Symbol BareType))
liftedAliases = [Located (RTAlias Symbol BareType)]
-> HashSet (Located (RTAlias Symbol BareType))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Located (RTAlias Symbol BareType)]
-> HashSet (Located (RTAlias Symbol BareType)))
-> (Spec LocBareType LocSymbol
-> [Located (RTAlias Symbol BareType)])
-> Spec LocBareType LocSymbol
-> HashSet (Located (RTAlias Symbol BareType))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Located (RTAlias Symbol BareType)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases (Spec LocBareType LocSymbol
-> HashSet (Located (RTAlias Symbol BareType)))
-> Spec LocBareType LocSymbol
-> HashSet (Located (RTAlias Symbol BareType))
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedEaliases :: HashSet (Located (RTAlias Symbol Expr))
liftedEaliases = [Located (RTAlias Symbol Expr)]
-> HashSet (Located (RTAlias Symbol Expr))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Located (RTAlias Symbol Expr)]
-> HashSet (Located (RTAlias Symbol Expr)))
-> (Spec LocBareType LocSymbol -> [Located (RTAlias Symbol Expr)])
-> Spec LocBareType LocSymbol
-> HashSet (Located (RTAlias Symbol Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Located (RTAlias Symbol Expr)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases (Spec LocBareType LocSymbol
-> HashSet (Located (RTAlias Symbol Expr)))
-> Spec LocBareType LocSymbol
-> HashSet (Located (RTAlias Symbol Expr))
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedEmbeds :: TCEmb LocSymbol
liftedEmbeds = Spec LocBareType LocSymbol -> TCEmb LocSymbol
forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds Spec LocBareType LocSymbol
a
, liftedQualifiers :: HashSet Qualifier
liftedQualifiers = [Qualifier] -> HashSet Qualifier
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Qualifier] -> HashSet Qualifier)
-> (Spec LocBareType LocSymbol -> [Qualifier])
-> Spec LocBareType LocSymbol
-> HashSet Qualifier
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Qualifier]
forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers (Spec LocBareType LocSymbol -> HashSet Qualifier)
-> Spec LocBareType LocSymbol -> HashSet Qualifier
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedLvars :: HashSet LocSymbol
liftedLvars = Spec LocBareType LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars Spec LocBareType LocSymbol
a
, liftedAutois :: HashMap LocSymbol (Maybe Int)
liftedAutois = Spec LocBareType LocSymbol -> HashMap LocSymbol (Maybe Int)
forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois Spec LocBareType LocSymbol
a
, liftedAutosize :: HashSet LocSymbol
liftedAutosize = Spec LocBareType LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize Spec LocBareType LocSymbol
a
, liftedCmeasures :: HashSet (Measure LocBareType ())
liftedCmeasures = [Measure LocBareType ()] -> HashSet (Measure LocBareType ())
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Measure LocBareType ()] -> HashSet (Measure LocBareType ()))
-> (Spec LocBareType LocSymbol -> [Measure LocBareType ()])
-> Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Measure LocBareType ()]
forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures (Spec LocBareType LocSymbol -> HashSet (Measure LocBareType ()))
-> Spec LocBareType LocSymbol -> HashSet (Measure LocBareType ())
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedImeasures :: HashSet (Measure LocBareType LocSymbol)
liftedImeasures = [Measure LocBareType LocSymbol]
-> HashSet (Measure LocBareType LocSymbol)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Measure LocBareType LocSymbol]
-> HashSet (Measure LocBareType LocSymbol))
-> (Spec LocBareType LocSymbol -> [Measure LocBareType LocSymbol])
-> Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType LocSymbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures (Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType LocSymbol))
-> Spec LocBareType LocSymbol
-> HashSet (Measure LocBareType LocSymbol)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedClasses :: HashSet (RClass LocBareType)
liftedClasses = [RClass LocBareType] -> HashSet (RClass LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([RClass LocBareType] -> HashSet (RClass LocBareType))
-> (Spec LocBareType LocSymbol -> [RClass LocBareType])
-> Spec LocBareType LocSymbol
-> HashSet (RClass LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [RClass LocBareType]
forall ty bndr. Spec ty bndr -> [RClass ty]
classes (Spec LocBareType LocSymbol -> HashSet (RClass LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (RClass LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedClaws :: HashSet (RClass LocBareType)
liftedClaws = [RClass LocBareType] -> HashSet (RClass LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([RClass LocBareType] -> HashSet (RClass LocBareType))
-> (Spec LocBareType LocSymbol -> [RClass LocBareType])
-> Spec LocBareType LocSymbol
-> HashSet (RClass LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [RClass LocBareType]
forall ty bndr. Spec ty bndr -> [RClass ty]
claws (Spec LocBareType LocSymbol -> HashSet (RClass LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (RClass LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedRinstance :: HashSet (RInstance LocBareType)
liftedRinstance = [RInstance LocBareType] -> HashSet (RInstance LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([RInstance LocBareType] -> HashSet (RInstance LocBareType))
-> (Spec LocBareType LocSymbol -> [RInstance LocBareType])
-> Spec LocBareType LocSymbol
-> HashSet (RInstance LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [RInstance LocBareType]
forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance (Spec LocBareType LocSymbol -> HashSet (RInstance LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (RInstance LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedIlaws :: HashSet (RILaws LocBareType)
liftedIlaws = [RILaws LocBareType] -> HashSet (RILaws LocBareType)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([RILaws LocBareType] -> HashSet (RILaws LocBareType))
-> (Spec LocBareType LocSymbol -> [RILaws LocBareType])
-> Spec LocBareType LocSymbol
-> HashSet (RILaws LocBareType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [RILaws LocBareType]
forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws (Spec LocBareType LocSymbol -> HashSet (RILaws LocBareType))
-> Spec LocBareType LocSymbol -> HashSet (RILaws LocBareType)
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedDvariance :: HashSet (LocSymbol, [Variance])
liftedDvariance = [(LocSymbol, [Variance])] -> HashSet (LocSymbol, [Variance])
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(LocSymbol, [Variance])] -> HashSet (LocSymbol, [Variance]))
-> (Spec LocBareType LocSymbol -> [(LocSymbol, [Variance])])
-> Spec LocBareType LocSymbol
-> HashSet (LocSymbol, [Variance])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [(LocSymbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance (Spec LocBareType LocSymbol -> HashSet (LocSymbol, [Variance]))
-> Spec LocBareType LocSymbol -> HashSet (LocSymbol, [Variance])
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
, liftedDsize :: [([LocBareType], LocSymbol)]
liftedDsize = Spec LocBareType LocSymbol -> [([LocBareType], LocSymbol)]
forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize Spec LocBareType LocSymbol
a
, liftedBounds :: RRBEnv LocBareType
liftedBounds = Spec LocBareType LocSymbol -> RRBEnv LocBareType
forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds Spec LocBareType LocSymbol
a
, liftedDefs :: HashMap LocSymbol Symbol
liftedDefs = Spec LocBareType LocSymbol -> HashMap LocSymbol Symbol
forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs Spec LocBareType LocSymbol
a
, liftedAxeqs :: HashSet Equation
liftedAxeqs = [Equation] -> HashSet Equation
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Equation] -> HashSet Equation)
-> (Spec LocBareType LocSymbol -> [Equation])
-> Spec LocBareType LocSymbol
-> HashSet Equation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec LocBareType LocSymbol -> [Equation]
forall ty bndr. Spec ty bndr -> [Equation]
axeqs (Spec LocBareType LocSymbol -> HashSet Equation)
-> Spec LocBareType LocSymbol -> HashSet Equation
forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
}
unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType F.LocSymbol
unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType LocSymbol
unsafeFromLiftedSpec LiftedSpec
a = Spec
{ measures :: [Measure LocBareType LocSymbol]
measures = HashSet (Measure LocBareType LocSymbol)
-> [Measure LocBareType LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet (Measure LocBareType LocSymbol)
-> [Measure LocBareType LocSymbol])
-> (LiftedSpec -> HashSet (Measure LocBareType LocSymbol))
-> LiftedSpec
-> [Measure LocBareType LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedMeasures (LiftedSpec -> [Measure LocBareType LocSymbol])
-> LiftedSpec -> [Measure LocBareType LocSymbol]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, impSigs :: [(Symbol, Sort)]
impSigs = HashSet (Symbol, Sort) -> [(Symbol, Sort)]
forall a. HashSet a -> [a]
S.toList (HashSet (Symbol, Sort) -> [(Symbol, Sort)])
-> (LiftedSpec -> HashSet (Symbol, Sort))
-> LiftedSpec
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Symbol, Sort)
liftedImpSigs (LiftedSpec -> [(Symbol, Sort)]) -> LiftedSpec -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, expSigs :: [(Symbol, Sort)]
expSigs = HashSet (Symbol, Sort) -> [(Symbol, Sort)]
forall a. HashSet a -> [a]
S.toList (HashSet (Symbol, Sort) -> [(Symbol, Sort)])
-> (LiftedSpec -> HashSet (Symbol, Sort))
-> LiftedSpec
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Symbol, Sort)
liftedExpSigs (LiftedSpec -> [(Symbol, Sort)]) -> LiftedSpec -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, asmSigs :: [(LocSymbol, LocBareType)]
asmSigs = HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)])
-> (LiftedSpec -> HashSet (LocSymbol, LocBareType))
-> LiftedSpec
-> [(LocSymbol, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedAsmSigs (LiftedSpec -> [(LocSymbol, LocBareType)])
-> LiftedSpec -> [(LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, sigs :: [(LocSymbol, LocBareType)]
sigs = HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)])
-> (LiftedSpec -> HashSet (LocSymbol, LocBareType))
-> LiftedSpec
-> [(LocSymbol, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedSigs (LiftedSpec -> [(LocSymbol, LocBareType)])
-> LiftedSpec -> [(LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, localSigs :: [(LocSymbol, LocBareType)]
localSigs = [(LocSymbol, LocBareType)]
forall a. Monoid a => a
mempty
, reflSigs :: [(LocSymbol, LocBareType)]
reflSigs = [(LocSymbol, LocBareType)]
forall a. Monoid a => a
mempty
, relational :: [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
relational = [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
forall a. Monoid a => a
mempty
, asmRel :: [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
asmRel = [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
RelExpr)]
forall a. Monoid a => a
mempty
, invariants :: [(Maybe LocSymbol, LocBareType)]
invariants = HashSet (Maybe LocSymbol, LocBareType)
-> [(Maybe LocSymbol, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (Maybe LocSymbol, LocBareType)
-> [(Maybe LocSymbol, LocBareType)])
-> (LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType))
-> LiftedSpec
-> [(Maybe LocSymbol, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants (LiftedSpec -> [(Maybe LocSymbol, LocBareType)])
-> LiftedSpec -> [(Maybe LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, ialiases :: [(LocBareType, LocBareType)]
ialiases = HashSet (LocBareType, LocBareType) -> [(LocBareType, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (LocBareType, LocBareType)
-> [(LocBareType, LocBareType)])
-> (LiftedSpec -> HashSet (LocBareType, LocBareType))
-> LiftedSpec
-> [(LocBareType, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocBareType, LocBareType)
liftedIaliases (LiftedSpec -> [(LocBareType, LocBareType)])
-> LiftedSpec -> [(LocBareType, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, imports :: [Symbol]
imports = HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> [Symbol])
-> (LiftedSpec -> HashSet Symbol) -> LiftedSpec -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Symbol
liftedImports (LiftedSpec -> [Symbol]) -> LiftedSpec -> [Symbol]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, dataDecls :: [DataDecl]
dataDecls = HashSet DataDecl -> [DataDecl]
forall a. HashSet a -> [a]
S.toList (HashSet DataDecl -> [DataDecl])
-> (LiftedSpec -> HashSet DataDecl) -> LiftedSpec -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDecl
liftedDataDecls (LiftedSpec -> [DataDecl]) -> LiftedSpec -> [DataDecl]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, newtyDecls :: [DataDecl]
newtyDecls = HashSet DataDecl -> [DataDecl]
forall a. HashSet a -> [a]
S.toList (HashSet DataDecl -> [DataDecl])
-> (LiftedSpec -> HashSet DataDecl) -> LiftedSpec -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDecl
liftedNewtyDecls (LiftedSpec -> [DataDecl]) -> LiftedSpec -> [DataDecl]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, includes :: [FilePath]
includes = [FilePath]
forall a. Monoid a => a
mempty
, aliases :: [Located (RTAlias Symbol BareType)]
aliases = HashSet (Located (RTAlias Symbol BareType))
-> [Located (RTAlias Symbol BareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (RTAlias Symbol BareType))
-> [Located (RTAlias Symbol BareType)])
-> (LiftedSpec -> HashSet (Located (RTAlias Symbol BareType)))
-> LiftedSpec
-> [Located (RTAlias Symbol BareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol BareType))
liftedAliases (LiftedSpec -> [Located (RTAlias Symbol BareType)])
-> LiftedSpec -> [Located (RTAlias Symbol BareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, ealiases :: [Located (RTAlias Symbol Expr)]
ealiases = HashSet (Located (RTAlias Symbol Expr))
-> [Located (RTAlias Symbol Expr)]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (RTAlias Symbol Expr))
-> [Located (RTAlias Symbol Expr)])
-> (LiftedSpec -> HashSet (Located (RTAlias Symbol Expr)))
-> LiftedSpec
-> [Located (RTAlias Symbol Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol Expr))
liftedEaliases (LiftedSpec -> [Located (RTAlias Symbol Expr)])
-> LiftedSpec -> [Located (RTAlias Symbol Expr)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, embeds :: TCEmb LocSymbol
embeds = LiftedSpec -> TCEmb LocSymbol
liftedEmbeds LiftedSpec
a
, qualifiers :: [Qualifier]
qualifiers = HashSet Qualifier -> [Qualifier]
forall a. HashSet a -> [a]
S.toList (HashSet Qualifier -> [Qualifier])
-> (LiftedSpec -> HashSet Qualifier) -> LiftedSpec -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Qualifier
liftedQualifiers (LiftedSpec -> [Qualifier]) -> LiftedSpec -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, lvars :: HashSet LocSymbol
lvars = LiftedSpec -> HashSet LocSymbol
liftedLvars LiftedSpec
a
, lazy :: HashSet LocSymbol
lazy = HashSet LocSymbol
forall a. Monoid a => a
mempty
, fails :: HashSet LocSymbol
fails = HashSet LocSymbol
forall a. Monoid a => a
mempty
, rewrites :: HashSet LocSymbol
rewrites = HashSet LocSymbol
forall a. Monoid a => a
mempty
, rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = HashMap LocSymbol [LocSymbol]
forall a. Monoid a => a
mempty
, reflects :: HashSet LocSymbol
reflects = HashSet LocSymbol
forall a. Monoid a => a
mempty
, autois :: HashMap LocSymbol (Maybe Int)
autois = LiftedSpec -> HashMap LocSymbol (Maybe Int)
liftedAutois LiftedSpec
a
, hmeas :: HashSet LocSymbol
hmeas = HashSet LocSymbol
forall a. Monoid a => a
mempty
, hbounds :: HashSet LocSymbol
hbounds = HashSet LocSymbol
forall a. Monoid a => a
mempty
, inlines :: HashSet LocSymbol
inlines = HashSet LocSymbol
forall a. Monoid a => a
mempty
, ignores :: HashSet LocSymbol
ignores = HashSet LocSymbol
forall a. Monoid a => a
mempty
, autosize :: HashSet LocSymbol
autosize = LiftedSpec -> HashSet LocSymbol
liftedAutosize LiftedSpec
a
, pragmas :: [Located FilePath]
pragmas = [Located FilePath]
forall a. Monoid a => a
mempty
, cmeasures :: [Measure LocBareType ()]
cmeasures = HashSet (Measure LocBareType ()) -> [Measure LocBareType ()]
forall a. HashSet a -> [a]
S.toList (HashSet (Measure LocBareType ()) -> [Measure LocBareType ()])
-> (LiftedSpec -> HashSet (Measure LocBareType ()))
-> LiftedSpec
-> [Measure LocBareType ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType ())
liftedCmeasures (LiftedSpec -> [Measure LocBareType ()])
-> LiftedSpec -> [Measure LocBareType ()]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, imeasures :: [Measure LocBareType LocSymbol]
imeasures = HashSet (Measure LocBareType LocSymbol)
-> [Measure LocBareType LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet (Measure LocBareType LocSymbol)
-> [Measure LocBareType LocSymbol])
-> (LiftedSpec -> HashSet (Measure LocBareType LocSymbol))
-> LiftedSpec
-> [Measure LocBareType LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedImeasures (LiftedSpec -> [Measure LocBareType LocSymbol])
-> LiftedSpec -> [Measure LocBareType LocSymbol]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, classes :: [RClass LocBareType]
classes = HashSet (RClass LocBareType) -> [RClass LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RClass LocBareType) -> [RClass LocBareType])
-> (LiftedSpec -> HashSet (RClass LocBareType))
-> LiftedSpec
-> [RClass LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass LocBareType)
liftedClasses (LiftedSpec -> [RClass LocBareType])
-> LiftedSpec -> [RClass LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, claws :: [RClass LocBareType]
claws = HashSet (RClass LocBareType) -> [RClass LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RClass LocBareType) -> [RClass LocBareType])
-> (LiftedSpec -> HashSet (RClass LocBareType))
-> LiftedSpec
-> [RClass LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass LocBareType)
liftedClaws (LiftedSpec -> [RClass LocBareType])
-> LiftedSpec -> [RClass LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, termexprs :: [(LocSymbol, [Located Expr])]
termexprs = [(LocSymbol, [Located Expr])]
forall a. Monoid a => a
mempty
, rinstance :: [RInstance LocBareType]
rinstance = HashSet (RInstance LocBareType) -> [RInstance LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RInstance LocBareType) -> [RInstance LocBareType])
-> (LiftedSpec -> HashSet (RInstance LocBareType))
-> LiftedSpec
-> [RInstance LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RInstance LocBareType)
liftedRinstance (LiftedSpec -> [RInstance LocBareType])
-> LiftedSpec -> [RInstance LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, ilaws :: [RILaws LocBareType]
ilaws = HashSet (RILaws LocBareType) -> [RILaws LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RILaws LocBareType) -> [RILaws LocBareType])
-> (LiftedSpec -> HashSet (RILaws LocBareType))
-> LiftedSpec
-> [RILaws LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RILaws LocBareType)
liftedIlaws (LiftedSpec -> [RILaws LocBareType])
-> LiftedSpec -> [RILaws LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, dvariance :: [(LocSymbol, [Variance])]
dvariance = HashSet (LocSymbol, [Variance]) -> [(LocSymbol, [Variance])]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, [Variance]) -> [(LocSymbol, [Variance])])
-> (LiftedSpec -> HashSet (LocSymbol, [Variance]))
-> LiftedSpec
-> [(LocSymbol, [Variance])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, [Variance])
liftedDvariance (LiftedSpec -> [(LocSymbol, [Variance])])
-> LiftedSpec -> [(LocSymbol, [Variance])]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, dsize :: [([LocBareType], LocSymbol)]
dsize = LiftedSpec -> [([LocBareType], LocSymbol)]
liftedDsize LiftedSpec
a
, bounds :: RRBEnv LocBareType
bounds = LiftedSpec -> RRBEnv LocBareType
liftedBounds LiftedSpec
a
, defs :: HashMap LocSymbol Symbol
defs = LiftedSpec -> HashMap LocSymbol Symbol
liftedDefs LiftedSpec
a
, axeqs :: [Equation]
axeqs = HashSet Equation -> [Equation]
forall a. HashSet a -> [a]
S.toList (HashSet Equation -> [Equation])
-> (LiftedSpec -> HashSet Equation) -> LiftedSpec -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Equation
liftedAxeqs (LiftedSpec -> [Equation]) -> LiftedSpec -> [Equation]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
}