{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Haskell.Liquid.Types.Specs (
TargetInfo(..)
, TargetSrc(..)
, TargetSpec(..)
, BareSpec
, BareSpecLHName
, BareSpecParsed
, LiftedSpec(..)
, TargetDependencies(..)
, dropDependency
, isPLEVar
, isExportedVar
, QImports(..)
, Spec(..)
, GhcSpecVars(..)
, GhcSpecSig(..)
, GhcSpecNames(..)
, GhcSpecTerm(..)
, GhcSpecRefl(..)
, GhcSpecData(..)
, GhcSpecQual(..)
, BareDef
, BareMeasure
, SpecMeasure
, VarOrLocSymbol
, emapSpecM
, fromBareSpecLHName
, fromBareSpecParsed
, mapSpecLName
, mapSpecTy
, GhcSrc(..)
, GhcSpec(..)
, toTargetSrc
, fromTargetSrc
, toTargetSpec
, toLiftedSpec
, unsafeFromLiftedSpec
, emptyLiftedSpec
) where
import GHC.Generics hiding (to, moduleName)
import Data.Bifunctor (bimap, first, second)
import Data.Bitraversable (bimapM)
import Data.Binary
import qualified Language.Fixpoint.Types as F
import Data.Data (Data)
import Data.Hashable
import qualified Data.HashSet as S
import Data.HashSet (HashSet)
import qualified Data.HashMap.Lazy as Lazy.M
import qualified Data.HashMap.Strict as M
import Data.HashMap.Strict (HashMap)
import Language.Haskell.Liquid.GHC.Misc (dropModuleNames)
import Language.Haskell.Liquid.Types.DataDecl
import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RTypeOp
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.Types.Bounds
import Language.Haskell.Liquid.UX.Config
import Liquid.GHC.API hiding (Binary, text, (<+>), panic)
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 -> String
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]
}
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 -> String
(Int -> QImports -> ShowS)
-> (QImports -> String) -> ([QImports] -> ShowS) -> Show QImports
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QImports -> ShowS
showsPrec :: Int -> QImports -> ShowS
$cshow :: QImports -> String
show :: QImports -> String
$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 -> [(Symbol, Sort)]
gsImps :: ![(F.Symbol, F.Sort)]
, TargetSpec -> Config
gsConfig :: !Config
}
deriving Int -> TargetSpec -> ShowS
[TargetSpec] -> ShowS
TargetSpec -> String
(Int -> TargetSpec -> ShowS)
-> (TargetSpec -> String)
-> ([TargetSpec] -> ShowS)
-> Show TargetSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TargetSpec -> ShowS
showsPrec :: Int -> TargetSpec -> ShowS
$cshow :: TargetSpec -> String
show :: TargetSpec -> String
$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 -> String
(Int -> GhcSpecVars -> ShowS)
-> (GhcSpecVars -> String)
-> ([GhcSpecVars] -> ShowS)
-> Show GhcSpecVars
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecVars -> ShowS
showsPrec :: Int -> GhcSpecVars -> ShowS
$cshow :: GhcSpecVars -> String
show :: GhcSpecVars -> String
$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 -> String
(Int -> GhcSpecQual -> ShowS)
-> (GhcSpecQual -> String)
-> ([GhcSpecQual] -> ShowS)
-> Show GhcSpecQual
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecQual -> ShowS
showsPrec :: Int -> GhcSpecQual -> ShowS
$cshow :: GhcSpecQual -> String
show :: GhcSpecQual -> String
$cshowList :: [GhcSpecQual] -> ShowS
showList :: [GhcSpecQual] -> ShowS
Show
data GhcSpecSig = SpSig
{ GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs :: ![(Var, LocSpecType)]
, GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs :: ![(Var, LocSpecType)]
, GhcSpecSig -> [(Var, Var)]
gsAsmReflects :: ![(Var, Var)]
, 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 -> String
(Int -> GhcSpecSig -> ShowS)
-> (GhcSpecSig -> String)
-> ([GhcSpecSig] -> ShowS)
-> Show GhcSpecSig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecSig -> ShowS
showsPrec :: Int -> GhcSpecSig -> ShowS
$cshow :: GhcSpecSig -> String
show :: GhcSpecSig -> String
$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
, gsAsmReflects :: [(Var, Var)]
gsAsmReflects = GhcSpecSig -> [(Var, Var)]
gsAsmReflects GhcSpecSig
x [(Var, Var)] -> [(Var, Var)] -> [(Var, Var)]
forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, Var)]
gsAsmReflects 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, Var)]
-> [(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, Var)]
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 (RTypeV Symbol RTyCon RTyVar RReft) DataCon]
gsMeasures :: ![Measure SpecType DataCon]
, GhcSpecData -> [Var]
gsOpaqueRefls:: ![Var]
, GhcSpecData -> [UnSortedExpr]
gsUnsorted :: ![UnSortedExpr]
}
deriving Int -> GhcSpecData -> ShowS
[GhcSpecData] -> ShowS
GhcSpecData -> String
(Int -> GhcSpecData -> ShowS)
-> (GhcSpecData -> String)
-> ([GhcSpecData] -> ShowS)
-> Show GhcSpecData
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecData -> ShowS
showsPrec :: Int -> GhcSpecData -> ShowS
$cshow :: GhcSpecData -> String
show :: GhcSpecData -> String
$cshowList :: [GhcSpecData] -> ShowS
showList :: [GhcSpecData] -> ShowS
Show
data GhcSpecNames = SpNames
{ 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
, GhcSpecNames -> [Var]
gsDataConIds :: [Var]
}
deriving Int -> GhcSpecNames -> ShowS
[GhcSpecNames] -> ShowS
GhcSpecNames -> String
(Int -> GhcSpecNames -> ShowS)
-> (GhcSpecNames -> String)
-> ([GhcSpecNames] -> ShowS)
-> Show GhcSpecNames
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecNames -> ShowS
showsPrec :: Int -> GhcSpecNames -> ShowS
$cshow :: GhcSpecNames -> String
show :: GhcSpecNames -> String
$cshowList :: [GhcSpecNames] -> ShowS
showList :: [GhcSpecNames] -> ShowS
Show
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 -> String
(Int -> GhcSpecTerm -> ShowS)
-> (GhcSpecTerm -> String)
-> ([GhcSpecTerm] -> ShowS)
-> Show GhcSpecTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecTerm -> ShowS
showsPrec :: Int -> GhcSpecTerm -> ShowS
$cshow :: GhcSpecTerm -> String
show :: GhcSpecTerm -> String
$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 -> HashSet Var
gsAutoInst :: !(S.HashSet Var)
, 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 -> 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 -> String
(Int -> GhcSpecRefl -> ShowS)
-> (GhcSpecRefl -> String)
-> ([GhcSpecRefl] -> ShowS)
-> Show GhcSpecRefl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GhcSpecRefl -> ShowS
showsPrec :: Int -> GhcSpecRefl -> ShowS
$cshow :: GhcSpecRefl -> String
show :: GhcSpecRefl -> String
$cshowList :: [GhcSpecRefl] -> ShowS
showList :: [GhcSpecRefl] -> ShowS
Show
instance Semigroup GhcSpecRefl where
GhcSpecRefl
x <> :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl
<> GhcSpecRefl
y = SpRefl
{ gsAutoInst :: HashSet Var
gsAutoInst = GhcSpecRefl -> HashSet Var
gsAutoInst GhcSpecRefl
x HashSet Var -> HashSet Var -> HashSet Var
forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> HashSet Var
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
, 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 = HashSet Var
-> [(Var, LocSpecType, Equation)]
-> [Equation]
-> [Equation]
-> [Var]
-> LogicMap
-> HashSet (Located Var)
-> HashMap Var [Var]
-> GhcSpecRefl
SpRefl HashSet Var
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
HashSet (Located Var)
forall a. Monoid a => a
mempty HashMap Var [Var]
forall a. Monoid a => a
mempty
type VarOrLocSymbol = Either Var LocSymbol
type BareMeasure = Measure LocBareType (F.Located LHName)
type BareDef = Def LocBareType (F.Located LHName)
type SpecMeasure = Measure LocSpecType DataCon
type BareSpec = Spec F.Symbol BareType
type BareSpecLHName = Spec LHName BareTypeLHName
type BareSpecParsed = Spec LocSymbol BareTypeParsed
data Spec lname ty = Spec
{ forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures :: ![MeasureV lname (F.Located ty) (F.Located LHName)]
, forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs :: ![(lname, F.Sort)]
, forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmSigs :: ![(F.Located LHName, F.Located ty)]
, forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
asmReflectSigs :: ![(F.Located LHName, F.Located LHName)]
, forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs :: ![(F.Located LHName, F.Located (BareTypeV lname))]
, forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
invariants :: ![(Maybe F.LocSymbol, F.Located ty)]
, forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
ialiases :: ![(F.Located ty, F.Located ty)]
, forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls :: ![DataDeclP lname ty]
, forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls :: ![DataDeclP lname ty]
, forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
aliases :: ![F.Located (RTAlias F.Symbol (BareTypeV lname))]
, forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases :: ![F.Located (RTAlias F.Symbol (F.ExprV lname))]
, forall lname ty. Spec lname ty -> TCEmb (Located LHName)
embeds :: !(F.TCEmb (F.Located LHName))
, forall lname ty. Spec lname ty -> [QualifierV lname]
qualifiers :: ![F.QualifierV lname]
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
lvars :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
lazy :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewrites :: !(S.HashSet (F.Located LHName))
, forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName])
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
fails :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects :: !(S.HashSet F.LocSymbol)
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
opaqueReflects :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
ignores :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize :: !(S.HashSet (F.Located LHName))
, forall lname ty. Spec lname ty -> [Located String]
pragmas :: ![F.Located String]
, forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures :: ![MeasureV lname (F.Located ty) ()]
, forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures :: ![MeasureV lname (F.Located ty) (F.Located LHName)]
, forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures :: ![MeasureV lname (F.Located ty) (F.Located LHName)]
, forall lname ty. Spec lname ty -> [RClass (Located ty)]
classes :: ![RClass (F.Located ty)]
, forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
relational :: ![(F.Located LHName, F.Located LHName, F.Located (BareTypeV lname), F.Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
, forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel :: ![(F.Located LHName, F.Located LHName, F.Located (BareTypeV lname), F.Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
, forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
termexprs :: ![(F.Located LHName, [F.Located (F.ExprV lname)])]
, forall lname ty. Spec lname ty -> [RInstance (Located ty)]
rinstance :: ![RInstance (F.Located ty)]
, forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
dvariance :: ![(F.Located LHName, [Variance])]
, forall lname ty. Spec lname ty -> [([Located ty], lname)]
dsize :: ![([F.Located ty], lname)]
, forall lname ty. Spec lname ty -> RRBEnvV lname (Located ty)
bounds :: !(RRBEnvV lname (F.Located ty))
, forall lname ty. Spec lname ty -> [EquationV lname]
axeqs :: ![F.EquationV lname]
, forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines :: ![(F.Located LHName, LMapV lname)]
, forall lname ty. Spec lname ty -> HashSet LHName
usedDataCons :: S.HashSet LHName
} deriving (Typeable (Spec lname ty)
Typeable (Spec lname ty) =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Spec lname ty -> c (Spec lname ty))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Spec lname ty))
-> (Spec lname ty -> Constr)
-> (Spec lname ty -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Spec lname ty)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Spec lname ty)))
-> ((forall b. Data b => b -> b) -> Spec lname ty -> Spec lname ty)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r)
-> (forall u. (forall d. Data d => d -> u) -> Spec lname ty -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Spec lname ty -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty))
-> Data (Spec lname ty)
Spec lname ty -> Constr
Spec lname ty -> DataType
(forall b. Data b => b -> b) -> Spec lname ty -> Spec lname ty
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Spec lname ty -> u
forall u. (forall d. Data d => d -> u) -> Spec lname ty -> [u]
forall lname ty. (Data lname, Data ty) => Typeable (Spec lname ty)
forall lname ty. (Data lname, Data ty) => Spec lname ty -> Constr
forall lname ty. (Data lname, Data ty) => Spec lname ty -> DataType
forall lname ty.
(Data lname, Data ty) =>
(forall b. Data b => b -> b) -> Spec lname ty -> Spec lname ty
forall lname ty u.
(Data lname, Data ty) =>
Int -> (forall d. Data d => d -> u) -> Spec lname ty -> u
forall lname ty u.
(Data lname, Data ty) =>
(forall d. Data d => d -> u) -> Spec lname ty -> [u]
forall lname ty r r'.
(Data lname, Data ty) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
forall lname ty r r'.
(Data lname, Data ty) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
forall lname ty (m :: * -> *).
(Data lname, Data ty, Monad m) =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
forall lname ty (m :: * -> *).
(Data lname, Data ty, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
forall lname ty (c :: * -> *).
(Data lname, Data ty) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Spec lname ty)
forall lname ty (c :: * -> *).
(Data lname, Data ty) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Spec lname ty -> c (Spec lname ty)
forall lname ty (t :: * -> *) (c :: * -> *).
(Data lname, Data ty, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Spec lname ty))
forall lname ty (t :: * -> * -> *) (c :: * -> *).
(Data lname, Data ty, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Spec lname ty))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Spec lname ty)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Spec lname ty -> c (Spec lname ty)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Spec lname ty))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Spec lname ty))
$cgfoldl :: forall lname ty (c :: * -> *).
(Data lname, Data ty) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Spec lname ty -> c (Spec lname ty)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Spec lname ty -> c (Spec lname ty)
$cgunfold :: forall lname ty (c :: * -> *).
(Data lname, Data ty) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Spec lname ty)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Spec lname ty)
$ctoConstr :: forall lname ty. (Data lname, Data ty) => Spec lname ty -> Constr
toConstr :: Spec lname ty -> Constr
$cdataTypeOf :: forall lname ty. (Data lname, Data ty) => Spec lname ty -> DataType
dataTypeOf :: Spec lname ty -> DataType
$cdataCast1 :: forall lname ty (t :: * -> *) (c :: * -> *).
(Data lname, Data ty, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Spec lname ty))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Spec lname ty))
$cdataCast2 :: forall lname ty (t :: * -> * -> *) (c :: * -> *).
(Data lname, Data ty, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Spec lname ty))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Spec lname ty))
$cgmapT :: forall lname ty.
(Data lname, Data ty) =>
(forall b. Data b => b -> b) -> Spec lname ty -> Spec lname ty
gmapT :: (forall b. Data b => b -> b) -> Spec lname ty -> Spec lname ty
$cgmapQl :: forall lname ty r r'.
(Data lname, Data ty) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
$cgmapQr :: forall lname ty r r'.
(Data lname, Data ty) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Spec lname ty -> r
$cgmapQ :: forall lname ty u.
(Data lname, Data ty) =>
(forall d. Data d => d -> u) -> Spec lname ty -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Spec lname ty -> [u]
$cgmapQi :: forall lname ty u.
(Data lname, Data ty) =>
Int -> (forall d. Data d => d -> u) -> Spec lname ty -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Spec lname ty -> u
$cgmapM :: forall lname ty (m :: * -> *).
(Data lname, Data ty, Monad m) =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
$cgmapMp :: forall lname ty (m :: * -> *).
(Data lname, Data ty, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
$cgmapMo :: forall lname ty (m :: * -> *).
(Data lname, Data ty, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Spec lname ty -> m (Spec lname ty)
Data, (forall x. Spec lname ty -> Rep (Spec lname ty) x)
-> (forall x. Rep (Spec lname ty) x -> Spec lname ty)
-> Generic (Spec lname ty)
forall x. Rep (Spec lname ty) x -> Spec lname ty
forall x. Spec lname ty -> Rep (Spec lname ty) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall lname ty x. Rep (Spec lname ty) x -> Spec lname ty
forall lname ty x. Spec lname ty -> Rep (Spec lname ty) x
$cfrom :: forall lname ty x. Spec lname ty -> Rep (Spec lname ty) x
from :: forall x. Spec lname ty -> Rep (Spec lname ty) x
$cto :: forall lname ty x. Rep (Spec lname ty) x -> Spec lname ty
to :: forall x. Rep (Spec lname ty) x -> Spec lname ty
Generic)
instance (Show lname, F.PPrint lname, Show ty, F.PPrint ty, F.PPrint (RTypeV lname BTyCon BTyVar (RReftV lname))) => F.PPrint (Spec lname ty) where
pprintTidy :: Tidy -> Spec lname ty -> Doc
pprintTidy Tidy
k Spec lname ty
sp = String -> Doc
text String
"dataDecls = " Doc -> Doc -> Doc
<+> Tidy -> [DataDeclP lname ty] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Spec lname ty -> [DataDeclP lname ty]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls Spec lname ty
sp)
Doc -> Doc -> Doc
HughesPJ.$$
String -> Doc
text String
"classes = " Doc -> Doc -> Doc
<+> Tidy -> [RClass (Located ty)] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Spec lname ty -> [RClass (Located ty)]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
classes Spec lname ty
sp)
Doc -> Doc -> Doc
HughesPJ.$$
String -> Doc
text String
"sigs = " Doc -> Doc -> Doc
<+> Tidy
-> [(Located LHName,
Located (RTypeV lname BTyCon BTyVar (RReftV lname)))]
-> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Spec lname ty
-> [(Located LHName,
Located (RTypeV lname BTyCon BTyVar (RReftV lname)))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs Spec lname ty
sp)
deriving instance Show BareSpec
emapSpecM
:: Monad m
=>
Bool
-> (LHName -> [F.Symbol])
-> ([F.Symbol] -> lname0 -> m lname1)
-> ([F.Symbol] -> ty0 -> m ty1)
-> Spec lname0 ty0
-> m (Spec lname1 ty1)
emapSpecM :: forall (m :: * -> *) lname0 lname1 ty0 ty1.
Monad m =>
Bool
-> (LHName -> [Symbol])
-> ([Symbol] -> lname0 -> m lname1)
-> ([Symbol] -> ty0 -> m ty1)
-> Spec lname0 ty0
-> m (Spec lname1 ty1)
emapSpecM Bool
bscp LHName -> [Symbol]
lenv [Symbol] -> lname0 -> m lname1
vf [Symbol] -> ty0 -> m ty1
f Spec lname0 ty0
sp = do
measures <- (MeasureV lname0 (Located ty0) (Located LHName)
-> m (MeasureV lname1 (Located ty1) (Located LHName)))
-> [MeasureV lname0 (Located ty0) (Located LHName)]
-> m [MeasureV lname1 (Located ty1) (Located LHName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (([Symbol] -> lname0 -> m lname1)
-> ([Symbol] -> Located ty0 -> m (Located ty1))
-> MeasureV lname0 (Located ty0) (Located LHName)
-> m (MeasureV lname1 (Located ty1) (Located LHName))
forall (m :: * -> *) v0 v1 ty0 ty1 ctor.
Monad m =>
([Symbol] -> v0 -> m v1)
-> ([Symbol] -> ty0 -> m ty1)
-> MeasureV v0 ty0 ctor
-> m (MeasureV v1 ty1 ctor)
emapMeasureM [Symbol] -> lname0 -> m lname1
vf ((ty0 -> m ty1) -> Located ty0 -> m (Located ty1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((ty0 -> m ty1) -> Located ty0 -> m (Located ty1))
-> ([Symbol] -> ty0 -> m ty1)
-> [Symbol]
-> Located ty0
-> m (Located ty1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> ty0 -> m ty1
f)) (Spec lname0 ty0 -> [MeasureV lname0 (Located ty0) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures Spec lname0 ty0
sp)
expSigs <- sequence [ (,s) <$> vf [] n | (n, s) <- expSigs sp ]
asmSigs <- mapM (\(Located LHName, Located ty0)
p -> (Located ty0 -> m (Located ty1))
-> (Located LHName, Located ty0) -> m (Located LHName, Located ty1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Located LHName, a) -> f (Located LHName, b)
traverse ((ty0 -> m ty1) -> Located ty0 -> m (Located ty1)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ([Symbol] -> ty0 -> m ty1
f ([Symbol] -> ty0 -> m ty1) -> [Symbol] -> ty0 -> m ty1
forall a b. (a -> b) -> a -> b
$ LHName -> [Symbol]
lenv (LHName -> [Symbol]) -> LHName -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ (Located LHName, Located ty0) -> Located LHName
forall a b. (a, b) -> a
fst (Located LHName, Located ty0)
p)) (Located LHName, Located ty0)
p) (asmSigs sp)
sigs <-
mapM
(\(Located LHName, Located (BareTypeV lname0))
p -> (Located (BareTypeV lname0) -> m (Located (BareTypeV lname1)))
-> (Located LHName, Located (BareTypeV lname0))
-> m (Located LHName, Located (BareTypeV lname1))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Located LHName, a) -> f (Located LHName, b)
traverse ((BareTypeV lname0 -> m (BareTypeV lname1))
-> Located (BareTypeV lname0) -> m (Located (BareTypeV lname1))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse (Bool
-> ([Symbol] -> lname0 -> m lname1)
-> [Symbol]
-> BareTypeV lname0
-> m (BareTypeV lname1)
forall (m :: * -> *) v1 v2.
Monad m =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> [Symbol]
-> BareTypeV v1
-> m (BareTypeV v2)
emapBareTypeVM Bool
bscp [Symbol] -> lname0 -> m lname1
vf (LHName -> [Symbol]
lenv (LHName -> [Symbol]) -> LHName -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ (Located LHName, Located (BareTypeV lname0)) -> Located LHName
forall a b. (a, b) -> a
fst (Located LHName, Located (BareTypeV lname0))
p))) (Located LHName, Located (BareTypeV lname0))
p)
(sigs sp)
invariants <- mapM (traverse (traverse fnull)) (invariants sp)
ialiases <- mapM (bimapM (traverse fnull) (traverse fnull)) (ialiases sp)
dataDecls <- mapM (emapDataDeclM bscp vf f) (dataDecls sp)
newtyDecls <- mapM (emapDataDeclM bscp vf f) (newtyDecls sp)
aliases <- mapM (traverse (emapRTAlias (emapBareTypeVM bscp vf))) (aliases sp)
ealiases <- mapM (traverse (emapRTAlias (\[Symbol]
e -> ([Symbol] -> lname0 -> m lname1)
-> ExprV lname0 -> m (ExprV lname1)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')
emapExprVM ([Symbol] -> lname0 -> m lname1
vf ([Symbol] -> lname0 -> m lname1)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> lname0 -> m lname1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
e))))) $ ealiases sp
qualifiers <- mapM (emapQualifierM vf) $ qualifiers sp
cmeasures <- mapM (emapMeasureM vf (traverse . f)) (cmeasures sp)
imeasures <- mapM (emapMeasureM vf (traverse . f)) (imeasures sp)
omeasures <- mapM (emapMeasureM vf (traverse . f)) (omeasures sp)
classes <- mapM (traverse (traverse fnull)) (classes sp)
relational <- mapM (emapRelationalM vf) (relational sp)
asmRel <- mapM (emapRelationalM vf) (asmRel sp)
let mbinds = [(LHName, [Symbol])] -> HashMap LHName [Symbol]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Lazy.M.fromList [ (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lx, RTypeRepV lname1 BTyCon BTyVar (RReftV lname1) -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds (RTypeRepV lname1 BTyCon BTyVar (RReftV lname1) -> [Symbol])
-> RTypeRepV lname1 BTyCon BTyVar (RReftV lname1) -> [Symbol]
forall a b. (a -> b) -> a -> b
$ BareTypeV lname1 -> RTypeRepV lname1 BTyCon BTyVar (RReftV lname1)
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (BareTypeV lname1
-> RTypeRepV lname1 BTyCon BTyVar (RReftV lname1))
-> BareTypeV lname1
-> RTypeRepV lname1 BTyCon BTyVar (RReftV lname1)
forall a b. (a -> b) -> a -> b
$ Located (BareTypeV lname1) -> BareTypeV lname1
forall a. Located a -> a
val Located (BareTypeV lname1)
lty) | (Located LHName
lx, Located (BareTypeV lname1)
lty) <- [(Located LHName, Located (BareTypeV lname1))]
sigs ]
termexprs <-
mapM
(\(Located LHName, [Located (ExprV lname0)])
p -> do
let bs0 :: [Symbol]
bs0 = LHName -> [Symbol]
lenv (LHName -> [Symbol]) -> LHName -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ (Located LHName, [Located (ExprV lname0)]) -> Located LHName
forall a b. (a, b) -> a
fst (Located LHName, [Located (ExprV lname0)])
p
mbs :: [Symbol]
mbs = [Symbol] -> LHName -> HashMap LHName [Symbol] -> [Symbol]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.findWithDefault [] (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ (Located LHName, [Located (ExprV lname0)]) -> Located LHName
forall a b. (a, b) -> a
fst (Located LHName, [Located (ExprV lname0)])
p) HashMap LHName [Symbol]
mbinds
([Located (ExprV lname0)] -> m [Located (ExprV lname1)])
-> (Located LHName, [Located (ExprV lname0)])
-> m (Located LHName, [Located (ExprV lname1)])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Located LHName, a) -> f (Located LHName, b)
traverse
((Located (ExprV lname0) -> m (Located (ExprV lname1)))
-> [Located (ExprV lname0)] -> m [Located (ExprV lname1)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((ExprV lname0 -> m (ExprV lname1))
-> Located (ExprV lname0) -> m (Located (ExprV lname1))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse (([Symbol] -> lname0 -> m lname1)
-> ExprV lname0 -> m (ExprV lname1)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')
emapExprVM ([Symbol] -> lname0 -> m lname1
vf ([Symbol] -> lname0 -> m lname1)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> lname0 -> m lname1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ([Symbol]
mbs [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
bs0))))))
(Located LHName, [Located (ExprV lname0)])
p
)
(termexprs sp)
rinstance <- mapM (traverse (traverse fnull)) (rinstance sp)
dsize <- mapM (bimapM (mapM (traverse fnull)) (vf [])) (dsize sp)
bounds <- M.fromList <$>
mapM
(traverse (emapBoundM (traverse . f) (\[Symbol]
e -> ([Symbol] -> lname0 -> m lname1)
-> ExprV lname0 -> m (ExprV lname1)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')
emapExprVM ([Symbol] -> lname0 -> m lname1
vf ([Symbol] -> lname0 -> m lname1)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> lname0 -> m lname1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
e)))))
(M.toList $ bounds sp)
axeqs <- mapM (emapEquationM vf) $ axeqs sp
defines <- mapM (traverse (emapLMapM vf)) $ defines sp
return sp
{ measures
, expSigs
, asmSigs
, sigs
, invariants
, ialiases
, dataDecls
, newtyDecls
, aliases
, ealiases
, qualifiers
, cmeasures
, imeasures
, omeasures
, classes
, relational
, asmRel
, termexprs
, rinstance
, dsize
, bounds
, axeqs
, defines
}
where
fnull :: ty0 -> m ty1
fnull = [Symbol] -> ty0 -> m ty1
f []
emapRelationalM :: ([Symbol] -> v0 -> m v1)
-> (a, b, Located (BareTypeV v0), Located (BareTypeV v0),
RelExprV v0, RelExprV v0)
-> m (a, b, Located (BareTypeV v1), Located (BareTypeV v1),
RelExprV v1, RelExprV v1)
emapRelationalM [Symbol] -> v0 -> m v1
vf1 (a
n0, b
n1, Located (BareTypeV v0)
t0, Located (BareTypeV v0)
t1, RelExprV v0
e0, RelExprV v0
e1) = do
t0' <- (BareTypeV v0 -> m (BareTypeV v1))
-> Located (BareTypeV v0) -> m (Located (BareTypeV v1))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse (Bool
-> ([Symbol] -> v0 -> m v1)
-> [Symbol]
-> BareTypeV v0
-> m (BareTypeV v1)
forall (m :: * -> *) v1 v2.
Monad m =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> [Symbol]
-> BareTypeV v1
-> m (BareTypeV v2)
emapBareTypeVM Bool
bscp [Symbol] -> v0 -> m v1
vf1 []) Located (BareTypeV v0)
t0
t1' <- traverse (emapBareTypeVM bscp vf1 []) t1
let bs = [String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol String
"r1", String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol String
"r2"] [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ BareTypeV v1 -> [Symbol]
forall {v} {c} {tv} {r}. RTypeV v c tv r -> [Symbol]
tArgs (Located (BareTypeV v1) -> BareTypeV v1
forall a. Located a -> a
val Located (BareTypeV v1)
t0') [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ BareTypeV v1 -> [Symbol]
forall {v} {c} {tv} {r}. RTypeV v c tv r -> [Symbol]
tArgs (Located (BareTypeV v1) -> BareTypeV v1
forall a. Located a -> a
val Located (BareTypeV v1)
t1')
e0' <- emapRelExprV (vf1 . (++ bs)) e0
e1' <- emapRelExprV (vf1 . (++ bs)) e1
return (n0, n1, t0', t1', e0', e1')
tArgs :: RTypeV v c tv r -> [Symbol]
tArgs RTypeV v c tv r
t =
let rt :: RTypeRepV v c tv r
rt = RTypeV v c tv r -> RTypeRepV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep RTypeV v c tv r
t
in RTypeRepV v c tv r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV v c tv r
rt [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RTypeV v c tv r -> [Symbol]) -> [RTypeV v c tv r] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeV v c tv r -> [Symbol]
tArgs (RTypeRepV v c tv r -> [RTypeV v c tv r]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV v c tv r
rt)
emapRTAlias :: Monad m => ([F.Symbol] -> r0 -> m r1) -> RTAlias F.Symbol r0 -> m (RTAlias F.Symbol r1)
emapRTAlias :: forall (m :: * -> *) r0 r1.
Monad m =>
([Symbol] -> r0 -> m r1)
-> RTAlias Symbol r0 -> m (RTAlias Symbol r1)
emapRTAlias [Symbol] -> r0 -> m r1
f RTAlias Symbol r0
rt = do
rtBody <- [Symbol] -> r0 -> m r1
f (RTAlias Symbol r0 -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol r0
rt [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTAlias Symbol r0 -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol r0
rt) (RTAlias Symbol r0 -> r0
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol r0
rt)
return rt{rtBody}
emapQualifierM :: Monad m => ([F.Symbol] -> v0 -> m v1) -> F.QualifierV v0 -> m (F.QualifierV v1)
emapQualifierM :: forall (m :: * -> *) v0 v1.
Monad m =>
([Symbol] -> v0 -> m v1) -> QualifierV v0 -> m (QualifierV v1)
emapQualifierM [Symbol] -> v0 -> m v1
f QualifierV v0
q = do
qBody <- ([Symbol] -> v0 -> m v1) -> ExprV v0 -> m (ExprV v1)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')
emapExprVM ([Symbol] -> v0 -> m v1
f ([Symbol] -> v0 -> m v1)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> v0 -> m v1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (QualParam -> Symbol) -> [QualParam] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map QualParam -> Symbol
F.qpSym (QualifierV v0 -> [QualParam]
forall v. QualifierV v -> [QualParam]
F.qParams QualifierV v0
q))) (QualifierV v0 -> ExprV v0
forall v. QualifierV v -> ExprV v
F.qBody QualifierV v0
q)
return q{F.qBody}
emapEquationM :: Monad m => ([F.Symbol] -> v0 -> m v1) -> F.EquationV v0 -> m (F.EquationV v1)
emapEquationM :: forall (m :: * -> *) v0 v1.
Monad m =>
([Symbol] -> v0 -> m v1) -> EquationV v0 -> m (EquationV v1)
emapEquationM [Symbol] -> v0 -> m v1
f EquationV v0
e = do
eqBody <- ([Symbol] -> v0 -> m v1) -> ExprV v0 -> m (ExprV v1)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')
emapExprVM ([Symbol] -> v0 -> m v1
f ([Symbol] -> v0 -> m v1)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> v0 -> m v1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst (EquationV v0 -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
F.eqArgs EquationV v0
e))) (EquationV v0 -> ExprV v0
forall v. EquationV v -> ExprV v
F.eqBody EquationV v0
e)
return e{F.eqBody}
mapSpecTy :: (ty0 -> ty1) -> Spec lname ty0 -> Spec lname ty1
mapSpecTy :: forall ty0 ty1 lname.
(ty0 -> ty1) -> Spec lname ty0 -> Spec lname ty1
mapSpecTy ty0 -> ty1
f Spec {[(lname, Sort)]
[([Located ty0], lname)]
[(Maybe LocSymbol, Located ty0)]
[(Located ty0, Located ty0)]
[(Located LHName, [Located (ExprV lname)])]
[(Located LHName, [Variance])]
[(Located LHName, Located ty0)]
[(Located LHName, Located LHName)]
[(Located LHName, Located (BareTypeV lname))]
[(Located LHName, LMapV lname)]
[(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
[Located String]
[Located (RTAlias Symbol (ExprV lname))]
[Located (RTAlias Symbol (BareTypeV lname))]
[EquationV lname]
[QualifierV lname]
[DataDeclP lname ty0]
[RClass (Located ty0)]
[MeasureV lname (Located ty0) ()]
[MeasureV lname (Located ty0) (Located LHName)]
[RInstance (Located ty0)]
RRBEnvV lname (Located ty0)
HashMap (Located LHName) [Located LHName]
TCEmb (Located LHName)
HashSet LocSymbol
HashSet (Located LHName)
HashSet LHName
measures :: forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
expSigs :: forall lname ty. Spec lname ty -> [(lname, Sort)]
asmSigs :: forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmReflectSigs :: forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
sigs :: forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
invariants :: forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
ialiases :: forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
dataDecls :: forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls :: forall lname ty. Spec lname ty -> [DataDeclP lname ty]
aliases :: forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
ealiases :: forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
embeds :: forall lname ty. Spec lname ty -> TCEmb (Located LHName)
qualifiers :: forall lname ty. Spec lname ty -> [QualifierV lname]
lvars :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
lazy :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewrites :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewriteWith :: forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
fails :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
privateReflects :: forall lname ty. Spec lname ty -> HashSet LocSymbol
opaqueReflects :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
ignores :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
pragmas :: forall lname ty. Spec lname ty -> [Located String]
cmeasures :: forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
imeasures :: forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures :: forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
classes :: forall lname ty. Spec lname ty -> [RClass (Located ty)]
relational :: forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel :: forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
termexprs :: forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
rinstance :: forall lname ty. Spec lname ty -> [RInstance (Located ty)]
dvariance :: forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
dsize :: forall lname ty. Spec lname ty -> [([Located ty], lname)]
bounds :: forall lname ty. Spec lname ty -> RRBEnvV lname (Located ty)
axeqs :: forall lname ty. Spec lname ty -> [EquationV lname]
defines :: forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
usedDataCons :: forall lname ty. Spec lname ty -> HashSet LHName
measures :: [MeasureV lname (Located ty0) (Located LHName)]
expSigs :: [(lname, Sort)]
asmSigs :: [(Located LHName, Located ty0)]
asmReflectSigs :: [(Located LHName, Located LHName)]
sigs :: [(Located LHName, Located (BareTypeV lname))]
invariants :: [(Maybe LocSymbol, Located ty0)]
ialiases :: [(Located ty0, Located ty0)]
dataDecls :: [DataDeclP lname ty0]
newtyDecls :: [DataDeclP lname ty0]
aliases :: [Located (RTAlias Symbol (BareTypeV lname))]
ealiases :: [Located (RTAlias Symbol (ExprV lname))]
embeds :: TCEmb (Located LHName)
qualifiers :: [QualifierV lname]
lvars :: HashSet (Located LHName)
lazy :: HashSet (Located LHName)
rewrites :: HashSet (Located LHName)
rewriteWith :: HashMap (Located LHName) [Located LHName]
fails :: HashSet (Located LHName)
reflects :: HashSet (Located LHName)
privateReflects :: HashSet LocSymbol
opaqueReflects :: HashSet (Located LHName)
autois :: HashSet (Located LHName)
hmeas :: HashSet (Located LHName)
inlines :: HashSet (Located LHName)
ignores :: HashSet (Located LHName)
autosize :: HashSet (Located LHName)
pragmas :: [Located String]
cmeasures :: [MeasureV lname (Located ty0) ()]
imeasures :: [MeasureV lname (Located ty0) (Located LHName)]
omeasures :: [MeasureV lname (Located ty0) (Located LHName)]
classes :: [RClass (Located ty0)]
relational :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
termexprs :: [(Located LHName, [Located (ExprV lname)])]
rinstance :: [RInstance (Located ty0)]
dvariance :: [(Located LHName, [Variance])]
dsize :: [([Located ty0], lname)]
bounds :: RRBEnvV lname (Located ty0)
axeqs :: [EquationV lname]
defines :: [(Located LHName, LMapV lname)]
usedDataCons :: HashSet LHName
..} =
Spec
{ measures :: [MeasureV lname (Located ty1) (Located LHName)]
measures = (MeasureV lname (Located ty0) (Located LHName)
-> MeasureV lname (Located ty1) (Located LHName))
-> [MeasureV lname (Located ty0) (Located LHName)]
-> [MeasureV lname (Located ty1) (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> MeasureV lname (Located ty0) (Located LHName)
-> MeasureV lname (Located ty1) (Located LHName)
forall ty0 ty1 v ctor.
(ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor
mapMeasureTy ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [MeasureV lname (Located ty0) (Located LHName)]
measures
, asmSigs :: [(Located LHName, Located ty1)]
asmSigs = ((Located LHName, Located ty0) -> (Located LHName, Located ty1))
-> [(Located LHName, Located ty0)]
-> [(Located LHName, Located ty1)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> (Located LHName, Located ty0) -> (Located LHName, Located ty1)
forall a b. (a -> b) -> (Located LHName, a) -> (Located LHName, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [(Located LHName, Located ty0)]
asmSigs
, invariants :: [(Maybe LocSymbol, Located ty1)]
invariants = ((Maybe LocSymbol, Located ty0) -> (Maybe LocSymbol, Located ty1))
-> [(Maybe LocSymbol, Located ty0)]
-> [(Maybe LocSymbol, Located ty1)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> (Maybe LocSymbol, Located ty0) -> (Maybe LocSymbol, Located ty1)
forall a b.
(a -> b) -> (Maybe LocSymbol, a) -> (Maybe LocSymbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [(Maybe LocSymbol, Located ty0)]
invariants
, ialiases :: [(Located ty1, Located ty1)]
ialiases = ((Located ty0, Located ty0) -> (Located ty1, Located ty1))
-> [(Located ty0, Located ty0)] -> [(Located ty1, Located ty1)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> (Located ty0 -> Located ty1)
-> (Located ty0, Located ty0)
-> (Located ty1, Located ty1)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f) ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [(Located ty0, Located ty0)]
ialiases
, dataDecls :: [DataDeclP lname ty1]
dataDecls = (DataDeclP lname ty0 -> DataDeclP lname ty1)
-> [DataDeclP lname ty0] -> [DataDeclP lname ty1]
forall a b. (a -> b) -> [a] -> [b]
map ((ty0 -> ty1) -> DataDeclP lname ty0 -> DataDeclP lname ty1
forall a b. (a -> b) -> DataDeclP lname a -> DataDeclP lname b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f) [DataDeclP lname ty0]
dataDecls
, newtyDecls :: [DataDeclP lname ty1]
newtyDecls = (DataDeclP lname ty0 -> DataDeclP lname ty1)
-> [DataDeclP lname ty0] -> [DataDeclP lname ty1]
forall a b. (a -> b) -> [a] -> [b]
map ((ty0 -> ty1) -> DataDeclP lname ty0 -> DataDeclP lname ty1
forall a b. (a -> b) -> DataDeclP lname a -> DataDeclP lname b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f) [DataDeclP lname ty0]
newtyDecls
, cmeasures :: [MeasureV lname (Located ty1) ()]
cmeasures = (MeasureV lname (Located ty0) ()
-> MeasureV lname (Located ty1) ())
-> [MeasureV lname (Located ty0) ()]
-> [MeasureV lname (Located ty1) ()]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> MeasureV lname (Located ty0) ()
-> MeasureV lname (Located ty1) ()
forall ty0 ty1 v ctor.
(ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor
mapMeasureTy ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [MeasureV lname (Located ty0) ()]
cmeasures
, imeasures :: [MeasureV lname (Located ty1) (Located LHName)]
imeasures = (MeasureV lname (Located ty0) (Located LHName)
-> MeasureV lname (Located ty1) (Located LHName))
-> [MeasureV lname (Located ty0) (Located LHName)]
-> [MeasureV lname (Located ty1) (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> MeasureV lname (Located ty0) (Located LHName)
-> MeasureV lname (Located ty1) (Located LHName)
forall ty0 ty1 v ctor.
(ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor
mapMeasureTy ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [MeasureV lname (Located ty0) (Located LHName)]
imeasures
, omeasures :: [MeasureV lname (Located ty1) (Located LHName)]
omeasures = (MeasureV lname (Located ty0) (Located LHName)
-> MeasureV lname (Located ty1) (Located LHName))
-> [MeasureV lname (Located ty0) (Located LHName)]
-> [MeasureV lname (Located ty1) (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> MeasureV lname (Located ty0) (Located LHName)
-> MeasureV lname (Located ty1) (Located LHName)
forall ty0 ty1 v ctor.
(ty0 -> ty1) -> MeasureV v ty0 ctor -> MeasureV v ty1 ctor
mapMeasureTy ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [MeasureV lname (Located ty0) (Located LHName)]
omeasures
, classes :: [RClass (Located ty1)]
classes = (RClass (Located ty0) -> RClass (Located ty1))
-> [RClass (Located ty0)] -> [RClass (Located ty1)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> RClass (Located ty0) -> RClass (Located ty1)
forall a b. (a -> b) -> RClass a -> RClass b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [RClass (Located ty0)]
classes
, rinstance :: [RInstance (Located ty1)]
rinstance = (RInstance (Located ty0) -> RInstance (Located ty1))
-> [RInstance (Located ty0)] -> [RInstance (Located ty1)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located ty0 -> Located ty1)
-> RInstance (Located ty0) -> RInstance (Located ty1)
forall a b. (a -> b) -> RInstance a -> RInstance b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) [RInstance (Located ty0)]
rinstance
, dsize :: [([Located ty1], lname)]
dsize = (([Located ty0], lname) -> ([Located ty1], lname))
-> [([Located ty0], lname)] -> [([Located ty1], lname)]
forall a b. (a -> b) -> [a] -> [b]
map (([Located ty0] -> [Located ty1])
-> ([Located ty0], lname) -> ([Located ty1], lname)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Located ty0 -> Located ty1) -> [Located ty0] -> [Located ty1]
forall a b. (a -> b) -> [a] -> [b]
map ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f))) [([Located ty0], lname)]
dsize
, bounds :: RRBEnvV lname (Located ty1)
bounds = (Bound (Located ty0) (ExprV lname) -> RRBoundV lname (Located ty1))
-> RRBEnvV lname (Located ty0) -> RRBEnvV lname (Located ty1)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((Located ty0 -> Located ty1)
-> Bound (Located ty0) (ExprV lname)
-> RRBoundV lname (Located ty1)
forall a b c. (a -> b) -> Bound a c -> Bound b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((ty0 -> ty1) -> Located ty0 -> Located ty1
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ty0 -> ty1
f)) RRBEnvV lname (Located ty0)
bounds
, [(lname, Sort)]
[(Located LHName, [Located (ExprV lname)])]
[(Located LHName, [Variance])]
[(Located LHName, Located LHName)]
[(Located LHName, Located (BareTypeV lname))]
[(Located LHName, LMapV lname)]
[(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
[Located String]
[Located (RTAlias Symbol (ExprV lname))]
[Located (RTAlias Symbol (BareTypeV lname))]
[EquationV lname]
[QualifierV lname]
HashMap (Located LHName) [Located LHName]
TCEmb (Located LHName)
HashSet LocSymbol
HashSet (Located LHName)
HashSet LHName
expSigs :: [(lname, Sort)]
asmReflectSigs :: [(Located LHName, Located LHName)]
sigs :: [(Located LHName, Located (BareTypeV lname))]
aliases :: [Located (RTAlias Symbol (BareTypeV lname))]
ealiases :: [Located (RTAlias Symbol (ExprV lname))]
embeds :: TCEmb (Located LHName)
qualifiers :: [QualifierV lname]
lvars :: HashSet (Located LHName)
lazy :: HashSet (Located LHName)
rewrites :: HashSet (Located LHName)
rewriteWith :: HashMap (Located LHName) [Located LHName]
fails :: HashSet (Located LHName)
reflects :: HashSet (Located LHName)
privateReflects :: HashSet LocSymbol
opaqueReflects :: HashSet (Located LHName)
autois :: HashSet (Located LHName)
hmeas :: HashSet (Located LHName)
inlines :: HashSet (Located LHName)
ignores :: HashSet (Located LHName)
autosize :: HashSet (Located LHName)
pragmas :: [Located String]
relational :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
termexprs :: [(Located LHName, [Located (ExprV lname)])]
dvariance :: [(Located LHName, [Variance])]
axeqs :: [EquationV lname]
defines :: [(Located LHName, LMapV lname)]
usedDataCons :: HashSet LHName
expSigs :: [(lname, Sort)]
asmReflectSigs :: [(Located LHName, Located LHName)]
sigs :: [(Located LHName, Located (BareTypeV lname))]
aliases :: [Located (RTAlias Symbol (BareTypeV lname))]
ealiases :: [Located (RTAlias Symbol (ExprV lname))]
embeds :: TCEmb (Located LHName)
qualifiers :: [QualifierV lname]
lvars :: HashSet (Located LHName)
lazy :: HashSet (Located LHName)
rewrites :: HashSet (Located LHName)
rewriteWith :: HashMap (Located LHName) [Located LHName]
fails :: HashSet (Located LHName)
reflects :: HashSet (Located LHName)
privateReflects :: HashSet LocSymbol
opaqueReflects :: HashSet (Located LHName)
autois :: HashSet (Located LHName)
hmeas :: HashSet (Located LHName)
inlines :: HashSet (Located LHName)
ignores :: HashSet (Located LHName)
autosize :: HashSet (Located LHName)
pragmas :: [Located String]
relational :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
termexprs :: [(Located LHName, [Located (ExprV lname)])]
dvariance :: [(Located LHName, [Variance])]
axeqs :: [EquationV lname]
defines :: [(Located LHName, LMapV lname)]
usedDataCons :: HashSet LHName
..
}
mapSpecLName :: (lname0 -> lname1) -> Spec lname0 ty -> Spec lname1 ty
mapSpecLName :: forall lname0 lname1 ty.
(lname0 -> lname1) -> Spec lname0 ty -> Spec lname1 ty
mapSpecLName lname0 -> lname1
f Spec {[(lname0, Sort)]
[([Located ty], lname0)]
[(Maybe LocSymbol, Located ty)]
[(Located ty, Located ty)]
[(Located LHName, [Located (ExprV lname0)])]
[(Located LHName, [Variance])]
[(Located LHName, Located ty)]
[(Located LHName, Located LHName)]
[(Located LHName, Located (BareTypeV lname0))]
[(Located LHName, LMapV lname0)]
[(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
[Located String]
[Located (RTAlias Symbol (ExprV lname0))]
[Located (RTAlias Symbol (BareTypeV lname0))]
[EquationV lname0]
[QualifierV lname0]
[DataDeclP lname0 ty]
[RClass (Located ty)]
[MeasureV lname0 (Located ty) ()]
[MeasureV lname0 (Located ty) (Located LHName)]
[RInstance (Located ty)]
RRBEnvV lname0 (Located ty)
HashMap (Located LHName) [Located LHName]
TCEmb (Located LHName)
HashSet LocSymbol
HashSet (Located LHName)
HashSet LHName
measures :: forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
expSigs :: forall lname ty. Spec lname ty -> [(lname, Sort)]
asmSigs :: forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmReflectSigs :: forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
sigs :: forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
invariants :: forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
ialiases :: forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
dataDecls :: forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls :: forall lname ty. Spec lname ty -> [DataDeclP lname ty]
aliases :: forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
ealiases :: forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
embeds :: forall lname ty. Spec lname ty -> TCEmb (Located LHName)
qualifiers :: forall lname ty. Spec lname ty -> [QualifierV lname]
lvars :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
lazy :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewrites :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewriteWith :: forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
fails :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
privateReflects :: forall lname ty. Spec lname ty -> HashSet LocSymbol
opaqueReflects :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
ignores :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize :: forall lname ty. Spec lname ty -> HashSet (Located LHName)
pragmas :: forall lname ty. Spec lname ty -> [Located String]
cmeasures :: forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
imeasures :: forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures :: forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
classes :: forall lname ty. Spec lname ty -> [RClass (Located ty)]
relational :: forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel :: forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
termexprs :: forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
rinstance :: forall lname ty. Spec lname ty -> [RInstance (Located ty)]
dvariance :: forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
dsize :: forall lname ty. Spec lname ty -> [([Located ty], lname)]
bounds :: forall lname ty. Spec lname ty -> RRBEnvV lname (Located ty)
axeqs :: forall lname ty. Spec lname ty -> [EquationV lname]
defines :: forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
usedDataCons :: forall lname ty. Spec lname ty -> HashSet LHName
measures :: [MeasureV lname0 (Located ty) (Located LHName)]
expSigs :: [(lname0, Sort)]
asmSigs :: [(Located LHName, Located ty)]
asmReflectSigs :: [(Located LHName, Located LHName)]
sigs :: [(Located LHName, Located (BareTypeV lname0))]
invariants :: [(Maybe LocSymbol, Located ty)]
ialiases :: [(Located ty, Located ty)]
dataDecls :: [DataDeclP lname0 ty]
newtyDecls :: [DataDeclP lname0 ty]
aliases :: [Located (RTAlias Symbol (BareTypeV lname0))]
ealiases :: [Located (RTAlias Symbol (ExprV lname0))]
embeds :: TCEmb (Located LHName)
qualifiers :: [QualifierV lname0]
lvars :: HashSet (Located LHName)
lazy :: HashSet (Located LHName)
rewrites :: HashSet (Located LHName)
rewriteWith :: HashMap (Located LHName) [Located LHName]
fails :: HashSet (Located LHName)
reflects :: HashSet (Located LHName)
privateReflects :: HashSet LocSymbol
opaqueReflects :: HashSet (Located LHName)
autois :: HashSet (Located LHName)
hmeas :: HashSet (Located LHName)
inlines :: HashSet (Located LHName)
ignores :: HashSet (Located LHName)
autosize :: HashSet (Located LHName)
pragmas :: [Located String]
cmeasures :: [MeasureV lname0 (Located ty) ()]
imeasures :: [MeasureV lname0 (Located ty) (Located LHName)]
omeasures :: [MeasureV lname0 (Located ty) (Located LHName)]
classes :: [RClass (Located ty)]
relational :: [(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
termexprs :: [(Located LHName, [Located (ExprV lname0)])]
rinstance :: [RInstance (Located ty)]
dvariance :: [(Located LHName, [Variance])]
dsize :: [([Located ty], lname0)]
bounds :: RRBEnvV lname0 (Located ty)
axeqs :: [EquationV lname0]
defines :: [(Located LHName, LMapV lname0)]
usedDataCons :: HashSet LHName
..} =
Spec
{ measures :: [MeasureV lname1 (Located ty) (Located LHName)]
measures = (MeasureV lname0 (Located ty) (Located LHName)
-> MeasureV lname1 (Located ty) (Located LHName))
-> [MeasureV lname0 (Located ty) (Located LHName)]
-> [MeasureV lname1 (Located ty) (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> MeasureV lname0 (Located ty) (Located LHName)
-> MeasureV lname1 (Located ty) (Located LHName)
forall v v' ty ctor.
(v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor
mapMeasureV lname0 -> lname1
f) [MeasureV lname0 (Located ty) (Located LHName)]
measures
, expSigs :: [(lname1, Sort)]
expSigs = ((lname0, Sort) -> (lname1, Sort))
-> [(lname0, Sort)] -> [(lname1, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1) -> (lname0, Sort) -> (lname1, Sort)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first lname0 -> lname1
f) [(lname0, Sort)]
expSigs
, sigs :: [(Located LHName, Located (BareTypeV lname1))]
sigs = ((Located LHName, Located (BareTypeV lname0))
-> (Located LHName, Located (BareTypeV lname1)))
-> [(Located LHName, Located (BareTypeV lname0))]
-> [(Located LHName, Located (BareTypeV lname1))]
forall a b. (a -> b) -> [a] -> [b]
map ((Located (BareTypeV lname0) -> Located (BareTypeV lname1))
-> (Located LHName, Located (BareTypeV lname0))
-> (Located LHName, Located (BareTypeV lname1))
forall a b. (a -> b) -> (Located LHName, a) -> (Located LHName, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BareTypeV lname0 -> BareTypeV lname1)
-> Located (BareTypeV lname0) -> Located (BareTypeV lname1)
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((lname0 -> lname1)
-> RTypeV lname0 BTyCon BTyVar (RReftV lname1) -> BareTypeV lname1
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV lname0 -> lname1
f (RTypeV lname0 BTyCon BTyVar (RReftV lname1) -> BareTypeV lname1)
-> (BareTypeV lname0
-> RTypeV lname0 BTyCon BTyVar (RReftV lname1))
-> BareTypeV lname0
-> BareTypeV lname1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UReftV lname0 (ReftV lname0) -> RReftV lname1)
-> BareTypeV lname0 -> RTypeV lname0 BTyCon BTyVar (RReftV lname1)
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((lname0 -> lname1)
-> (ReftV lname0 -> ReftV lname1)
-> UReftV lname0 (ReftV lname0)
-> RReftV lname1
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV lname0 -> lname1
f ((lname0 -> lname1) -> ReftV lname0 -> ReftV lname1
forall a b. (a -> b) -> ReftV a -> ReftV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f))))) [(Located LHName, Located (BareTypeV lname0))]
sigs
, dataDecls :: [DataDeclP lname1 ty]
dataDecls = (DataDeclP lname0 ty -> DataDeclP lname1 ty)
-> [DataDeclP lname0 ty] -> [DataDeclP lname1 ty]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1) -> DataDeclP lname0 ty -> DataDeclP lname1 ty
forall v v' ty. (v -> v') -> DataDeclP v ty -> DataDeclP v' ty
mapDataDeclV lname0 -> lname1
f) [DataDeclP lname0 ty]
dataDecls
, newtyDecls :: [DataDeclP lname1 ty]
newtyDecls = (DataDeclP lname0 ty -> DataDeclP lname1 ty)
-> [DataDeclP lname0 ty] -> [DataDeclP lname1 ty]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1) -> DataDeclP lname0 ty -> DataDeclP lname1 ty
forall v v' ty. (v -> v') -> DataDeclP v ty -> DataDeclP v' ty
mapDataDeclV lname0 -> lname1
f) [DataDeclP lname0 ty]
newtyDecls
, aliases :: [Located (RTAlias Symbol (BareTypeV lname1))]
aliases = (Located (RTAlias Symbol (BareTypeV lname0))
-> Located (RTAlias Symbol (BareTypeV lname1)))
-> [Located (RTAlias Symbol (BareTypeV lname0))]
-> [Located (RTAlias Symbol (BareTypeV lname1))]
forall a b. (a -> b) -> [a] -> [b]
map ((RTAlias Symbol (BareTypeV lname0)
-> RTAlias Symbol (BareTypeV lname1))
-> Located (RTAlias Symbol (BareTypeV lname0))
-> Located (RTAlias Symbol (BareTypeV lname1))
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BareTypeV lname0 -> BareTypeV lname1)
-> RTAlias Symbol (BareTypeV lname0)
-> RTAlias Symbol (BareTypeV lname1)
forall a b. (a -> b) -> RTAlias Symbol a -> RTAlias Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((lname0 -> lname1)
-> RTypeV lname0 BTyCon BTyVar (RReftV lname1) -> BareTypeV lname1
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV lname0 -> lname1
f (RTypeV lname0 BTyCon BTyVar (RReftV lname1) -> BareTypeV lname1)
-> (BareTypeV lname0
-> RTypeV lname0 BTyCon BTyVar (RReftV lname1))
-> BareTypeV lname0
-> BareTypeV lname1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UReftV lname0 (ReftV lname0) -> RReftV lname1)
-> BareTypeV lname0 -> RTypeV lname0 BTyCon BTyVar (RReftV lname1)
forall a b.
(a -> b)
-> RTypeV lname0 BTyCon BTyVar a -> RTypeV lname0 BTyCon BTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((lname0 -> lname1)
-> (ReftV lname0 -> ReftV lname1)
-> UReftV lname0 (ReftV lname0)
-> RReftV lname1
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV lname0 -> lname1
f ((lname0 -> lname1) -> ReftV lname0 -> ReftV lname1
forall a b. (a -> b) -> ReftV a -> ReftV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f))))) [Located (RTAlias Symbol (BareTypeV lname0))]
aliases
, ealiases :: [Located (RTAlias Symbol (ExprV lname1))]
ealiases = (Located (RTAlias Symbol (ExprV lname0))
-> Located (RTAlias Symbol (ExprV lname1)))
-> [Located (RTAlias Symbol (ExprV lname0))]
-> [Located (RTAlias Symbol (ExprV lname1))]
forall a b. (a -> b) -> [a] -> [b]
map ((RTAlias Symbol (ExprV lname0) -> RTAlias Symbol (ExprV lname1))
-> Located (RTAlias Symbol (ExprV lname0))
-> Located (RTAlias Symbol (ExprV lname1))
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ExprV lname0 -> ExprV lname1)
-> RTAlias Symbol (ExprV lname0) -> RTAlias Symbol (ExprV lname1)
forall a b. (a -> b) -> RTAlias Symbol a -> RTAlias Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((lname0 -> lname1) -> ExprV lname0 -> ExprV lname1
forall a b. (a -> b) -> ExprV a -> ExprV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f))) [Located (RTAlias Symbol (ExprV lname0))]
ealiases
, qualifiers :: [QualifierV lname1]
qualifiers = (QualifierV lname0 -> QualifierV lname1)
-> [QualifierV lname0] -> [QualifierV lname1]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1) -> QualifierV lname0 -> QualifierV lname1
forall a b. (a -> b) -> QualifierV a -> QualifierV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f) [QualifierV lname0]
qualifiers
, cmeasures :: [MeasureV lname1 (Located ty) ()]
cmeasures = (MeasureV lname0 (Located ty) ()
-> MeasureV lname1 (Located ty) ())
-> [MeasureV lname0 (Located ty) ()]
-> [MeasureV lname1 (Located ty) ()]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> MeasureV lname0 (Located ty) ()
-> MeasureV lname1 (Located ty) ()
forall v v' ty ctor.
(v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor
mapMeasureV lname0 -> lname1
f) [MeasureV lname0 (Located ty) ()]
cmeasures
, imeasures :: [MeasureV lname1 (Located ty) (Located LHName)]
imeasures = (MeasureV lname0 (Located ty) (Located LHName)
-> MeasureV lname1 (Located ty) (Located LHName))
-> [MeasureV lname0 (Located ty) (Located LHName)]
-> [MeasureV lname1 (Located ty) (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> MeasureV lname0 (Located ty) (Located LHName)
-> MeasureV lname1 (Located ty) (Located LHName)
forall v v' ty ctor.
(v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor
mapMeasureV lname0 -> lname1
f) [MeasureV lname0 (Located ty) (Located LHName)]
imeasures
, omeasures :: [MeasureV lname1 (Located ty) (Located LHName)]
omeasures = (MeasureV lname0 (Located ty) (Located LHName)
-> MeasureV lname1 (Located ty) (Located LHName))
-> [MeasureV lname0 (Located ty) (Located LHName)]
-> [MeasureV lname1 (Located ty) (Located LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> MeasureV lname0 (Located ty) (Located LHName)
-> MeasureV lname1 (Located ty) (Located LHName)
forall v v' ty ctor.
(v -> v') -> MeasureV v ty ctor -> MeasureV v' ty ctor
mapMeasureV lname0 -> lname1
f) [MeasureV lname0 (Located ty) (Located LHName)]
omeasures
, relational :: [(Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1)]
relational = ((Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)
-> (Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1))
-> [(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
-> [(Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> (Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)
-> (Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1)
forall {f :: * -> *} {f :: * -> *} {f :: * -> *} {f :: * -> *}
{f :: * -> *} {f :: * -> *} {a} {b} {a} {b} {c} {tv} {c} {tv}.
(Functor f, Functor f, Functor f, Functor f, Functor f,
Functor f) =>
(a -> b)
-> (a, b, f (RTypeV a c tv (UReftV a (f a))),
f (RTypeV a c tv (UReftV a (f a))), f a, f a)
-> (a, b, f (RTypeV b c tv (UReftV b (f b))),
f (RTypeV b c tv (UReftV b (f b))), f b, f b)
mapRelationalV lname0 -> lname1
f) [(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
relational
, asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1)]
asmRel = ((Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)
-> (Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1))
-> [(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
-> [(Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> (Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)
-> (Located LHName, Located LHName, Located (BareTypeV lname1),
Located (BareTypeV lname1), RelExprV lname1, RelExprV lname1)
forall {f :: * -> *} {f :: * -> *} {f :: * -> *} {f :: * -> *}
{f :: * -> *} {f :: * -> *} {a} {b} {a} {b} {c} {tv} {c} {tv}.
(Functor f, Functor f, Functor f, Functor f, Functor f,
Functor f) =>
(a -> b)
-> (a, b, f (RTypeV a c tv (UReftV a (f a))),
f (RTypeV a c tv (UReftV a (f a))), f a, f a)
-> (a, b, f (RTypeV b c tv (UReftV b (f b))),
f (RTypeV b c tv (UReftV b (f b))), f b, f b)
mapRelationalV lname0 -> lname1
f) [(Located LHName, Located LHName, Located (BareTypeV lname0),
Located (BareTypeV lname0), RelExprV lname0, RelExprV lname0)]
asmRel
, termexprs :: [(Located LHName, [Located (ExprV lname1)])]
termexprs = ((Located LHName, [Located (ExprV lname0)])
-> (Located LHName, [Located (ExprV lname1)]))
-> [(Located LHName, [Located (ExprV lname0)])]
-> [(Located LHName, [Located (ExprV lname1)])]
forall a b. (a -> b) -> [a] -> [b]
map (([Located (ExprV lname0)] -> [Located (ExprV lname1)])
-> (Located LHName, [Located (ExprV lname0)])
-> (Located LHName, [Located (ExprV lname1)])
forall a b. (a -> b) -> (Located LHName, a) -> (Located LHName, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Located (ExprV lname0) -> Located (ExprV lname1))
-> [Located (ExprV lname0)] -> [Located (ExprV lname1)]
forall a b. (a -> b) -> [a] -> [b]
map ((ExprV lname0 -> ExprV lname1)
-> Located (ExprV lname0) -> Located (ExprV lname1)
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((lname0 -> lname1) -> ExprV lname0 -> ExprV lname1
forall a b. (a -> b) -> ExprV a -> ExprV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f)))) [(Located LHName, [Located (ExprV lname0)])]
termexprs
, bounds :: RRBEnvV lname1 (Located ty)
bounds = (Bound (Located ty) (ExprV lname0) -> RRBoundV lname1 (Located ty))
-> RRBEnvV lname0 (Located ty) -> RRBEnvV lname1 (Located ty)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((ExprV lname0 -> ExprV lname1)
-> Bound (Located ty) (ExprV lname0)
-> RRBoundV lname1 (Located ty)
forall a b.
(a -> b) -> Bound (Located ty) a -> Bound (Located ty) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((lname0 -> lname1) -> ExprV lname0 -> ExprV lname1
forall a b. (a -> b) -> ExprV a -> ExprV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f)) RRBEnvV lname0 (Located ty)
bounds
, axeqs :: [EquationV lname1]
axeqs = (EquationV lname0 -> EquationV lname1)
-> [EquationV lname0] -> [EquationV lname1]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1) -> EquationV lname0 -> EquationV lname1
forall a b. (a -> b) -> EquationV a -> EquationV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f) [EquationV lname0]
axeqs
, dsize :: [([Located ty], lname1)]
dsize = (([Located ty], lname0) -> ([Located ty], lname1))
-> [([Located ty], lname0)] -> [([Located ty], lname1)]
forall a b. (a -> b) -> [a] -> [b]
map ((lname0 -> lname1)
-> ([Located ty], lname0) -> ([Located ty], lname1)
forall a b. (a -> b) -> ([Located ty], a) -> ([Located ty], b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f) [([Located ty], lname0)]
dsize
, defines :: [(Located LHName, LMapV lname1)]
defines = ((Located LHName, LMapV lname0) -> (Located LHName, LMapV lname1))
-> [(Located LHName, LMapV lname0)]
-> [(Located LHName, LMapV lname1)]
forall a b. (a -> b) -> [a] -> [b]
map ((LMapV lname0 -> LMapV lname1)
-> (Located LHName, LMapV lname0) -> (Located LHName, LMapV lname1)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((LMapV lname0 -> LMapV lname1)
-> (Located LHName, LMapV lname0)
-> (Located LHName, LMapV lname1))
-> (LMapV lname0 -> LMapV lname1)
-> (Located LHName, LMapV lname0)
-> (Located LHName, LMapV lname1)
forall a b. (a -> b) -> a -> b
$ (lname0 -> lname1) -> LMapV lname0 -> LMapV lname1
forall a b. (a -> b) -> LMapV a -> LMapV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap lname0 -> lname1
f) [(Located LHName, LMapV lname0)]
defines
, [(Maybe LocSymbol, Located ty)]
[(Located ty, Located ty)]
[(Located LHName, [Variance])]
[(Located LHName, Located ty)]
[(Located LHName, Located LHName)]
[Located String]
[RClass (Located ty)]
[RInstance (Located ty)]
HashMap (Located LHName) [Located LHName]
TCEmb (Located LHName)
HashSet LocSymbol
HashSet (Located LHName)
HashSet LHName
asmSigs :: [(Located LHName, Located ty)]
asmReflectSigs :: [(Located LHName, Located LHName)]
invariants :: [(Maybe LocSymbol, Located ty)]
ialiases :: [(Located ty, Located ty)]
embeds :: TCEmb (Located LHName)
lvars :: HashSet (Located LHName)
lazy :: HashSet (Located LHName)
rewrites :: HashSet (Located LHName)
rewriteWith :: HashMap (Located LHName) [Located LHName]
fails :: HashSet (Located LHName)
reflects :: HashSet (Located LHName)
privateReflects :: HashSet LocSymbol
opaqueReflects :: HashSet (Located LHName)
autois :: HashSet (Located LHName)
hmeas :: HashSet (Located LHName)
inlines :: HashSet (Located LHName)
ignores :: HashSet (Located LHName)
autosize :: HashSet (Located LHName)
pragmas :: [Located String]
classes :: [RClass (Located ty)]
rinstance :: [RInstance (Located ty)]
dvariance :: [(Located LHName, [Variance])]
usedDataCons :: HashSet LHName
asmSigs :: [(Located LHName, Located ty)]
asmReflectSigs :: [(Located LHName, Located LHName)]
invariants :: [(Maybe LocSymbol, Located ty)]
ialiases :: [(Located ty, Located ty)]
embeds :: TCEmb (Located LHName)
lvars :: HashSet (Located LHName)
lazy :: HashSet (Located LHName)
rewrites :: HashSet (Located LHName)
rewriteWith :: HashMap (Located LHName) [Located LHName]
fails :: HashSet (Located LHName)
reflects :: HashSet (Located LHName)
privateReflects :: HashSet LocSymbol
opaqueReflects :: HashSet (Located LHName)
autois :: HashSet (Located LHName)
hmeas :: HashSet (Located LHName)
inlines :: HashSet (Located LHName)
ignores :: HashSet (Located LHName)
autosize :: HashSet (Located LHName)
pragmas :: [Located String]
classes :: [RClass (Located ty)]
rinstance :: [RInstance (Located ty)]
dvariance :: [(Located LHName, [Variance])]
usedDataCons :: HashSet LHName
..
}
where
mapRelationalV :: (a -> b)
-> (a, b, f (RTypeV a c tv (UReftV a (f a))),
f (RTypeV a c tv (UReftV a (f a))), f a, f a)
-> (a, b, f (RTypeV b c tv (UReftV b (f b))),
f (RTypeV b c tv (UReftV b (f b))), f b, f b)
mapRelationalV a -> b
f1 (a
n0, b
n1, f (RTypeV a c tv (UReftV a (f a)))
a, f (RTypeV a c tv (UReftV a (f a)))
b, f a
e0, f a
e1) =
(a
n0, b
n1, (RTypeV a c tv (UReftV a (f a)) -> RTypeV b c tv (UReftV b (f b)))
-> f (RTypeV a c tv (UReftV a (f a)))
-> f (RTypeV b c tv (UReftV b (f b)))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b)
-> RTypeV a c tv (UReftV b (f b)) -> RTypeV b c tv (UReftV b (f b))
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV a -> b
f1 (RTypeV a c tv (UReftV b (f b)) -> RTypeV b c tv (UReftV b (f b)))
-> (RTypeV a c tv (UReftV a (f a))
-> RTypeV a c tv (UReftV b (f b)))
-> RTypeV a c tv (UReftV a (f a))
-> RTypeV b c tv (UReftV b (f b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UReftV a (f a) -> UReftV b (f b))
-> RTypeV a c tv (UReftV a (f a)) -> RTypeV a c tv (UReftV b (f b))
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((a -> b) -> (f a -> f b) -> UReftV a (f a) -> UReftV b (f b)
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV a -> b
f1 ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f1))) f (RTypeV a c tv (UReftV a (f a)))
a, (RTypeV a c tv (UReftV a (f a)) -> RTypeV b c tv (UReftV b (f b)))
-> f (RTypeV a c tv (UReftV a (f a)))
-> f (RTypeV b c tv (UReftV b (f b)))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b)
-> RTypeV a c tv (UReftV b (f b)) -> RTypeV b c tv (UReftV b (f b))
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV a -> b
f1 (RTypeV a c tv (UReftV b (f b)) -> RTypeV b c tv (UReftV b (f b)))
-> (RTypeV a c tv (UReftV a (f a))
-> RTypeV a c tv (UReftV b (f b)))
-> RTypeV a c tv (UReftV a (f a))
-> RTypeV b c tv (UReftV b (f b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UReftV a (f a) -> UReftV b (f b))
-> RTypeV a c tv (UReftV a (f a)) -> RTypeV a c tv (UReftV b (f b))
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((a -> b) -> (f a -> f b) -> UReftV a (f a) -> UReftV b (f b)
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV a -> b
f1 ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f1))) f (RTypeV a c tv (UReftV a (f a)))
b, (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f1 f a
e0, (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f1 f a
e1)
instance Semigroup (Spec lname ty) where
Spec lname ty
s1 <> :: Spec lname ty -> Spec lname ty -> Spec lname ty
<> Spec lname ty
s2
= Spec { measures :: [MeasureV lname (Located ty) (Located LHName)]
measures = Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures Spec lname ty
s1 [MeasureV lname (Located ty) (Located LHName)]
-> [MeasureV lname (Located ty) (Located LHName)]
-> [MeasureV lname (Located ty) (Located LHName)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures Spec lname ty
s2
, expSigs :: [(lname, Sort)]
expSigs = Spec lname ty -> [(lname, Sort)]
forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs Spec lname ty
s1 [(lname, Sort)] -> [(lname, Sort)] -> [(lname, Sort)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(lname, Sort)]
forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs Spec lname ty
s2
, asmSigs :: [(Located LHName, Located ty)]
asmSigs = Spec lname ty -> [(Located LHName, Located ty)]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmSigs Spec lname ty
s1 [(Located LHName, Located ty)]
-> [(Located LHName, Located ty)] -> [(Located LHName, Located ty)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located LHName, Located ty)]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmSigs Spec lname ty
s2
, asmReflectSigs :: [(Located LHName, Located LHName)]
asmReflectSigs = Spec lname ty -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
asmReflectSigs Spec lname ty
s1 [(Located LHName, Located LHName)]
-> [(Located LHName, Located LHName)]
-> [(Located LHName, Located LHName)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
asmReflectSigs Spec lname ty
s2
, sigs :: [(Located LHName, Located (BareTypeV lname))]
sigs = Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs Spec lname ty
s1 [(Located LHName, Located (BareTypeV lname))]
-> [(Located LHName, Located (BareTypeV lname))]
-> [(Located LHName, Located (BareTypeV lname))]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs Spec lname ty
s2
, invariants :: [(Maybe LocSymbol, Located ty)]
invariants = Spec lname ty -> [(Maybe LocSymbol, Located ty)]
forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
invariants Spec lname ty
s1 [(Maybe LocSymbol, Located ty)]
-> [(Maybe LocSymbol, Located ty)]
-> [(Maybe LocSymbol, Located ty)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Maybe LocSymbol, Located ty)]
forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
invariants Spec lname ty
s2
, ialiases :: [(Located ty, Located ty)]
ialiases = Spec lname ty -> [(Located ty, Located ty)]
forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
ialiases Spec lname ty
s1 [(Located ty, Located ty)]
-> [(Located ty, Located ty)] -> [(Located ty, Located ty)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located ty, Located ty)]
forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
ialiases Spec lname ty
s2
, dataDecls :: [DataDeclP lname ty]
dataDecls = Spec lname ty -> [DataDeclP lname ty]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls Spec lname ty
s1 [DataDeclP lname ty]
-> [DataDeclP lname ty] -> [DataDeclP lname ty]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [DataDeclP lname ty]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls Spec lname ty
s2
, newtyDecls :: [DataDeclP lname ty]
newtyDecls = Spec lname ty -> [DataDeclP lname ty]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls Spec lname ty
s1 [DataDeclP lname ty]
-> [DataDeclP lname ty] -> [DataDeclP lname ty]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [DataDeclP lname ty]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls Spec lname ty
s2
, aliases :: [Located (RTAlias Symbol (BareTypeV lname))]
aliases = Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
aliases Spec lname ty
s1 [Located (RTAlias Symbol (BareTypeV lname))]
-> [Located (RTAlias Symbol (BareTypeV lname))]
-> [Located (RTAlias Symbol (BareTypeV lname))]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
aliases Spec lname ty
s2
, ealiases :: [Located (RTAlias Symbol (ExprV lname))]
ealiases = Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases Spec lname ty
s1 [Located (RTAlias Symbol (ExprV lname))]
-> [Located (RTAlias Symbol (ExprV lname))]
-> [Located (RTAlias Symbol (ExprV lname))]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases Spec lname ty
s2
, qualifiers :: [QualifierV lname]
qualifiers = Spec lname ty -> [QualifierV lname]
forall lname ty. Spec lname ty -> [QualifierV lname]
qualifiers Spec lname ty
s1 [QualifierV lname] -> [QualifierV lname] -> [QualifierV lname]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [QualifierV lname]
forall lname ty. Spec lname ty -> [QualifierV lname]
qualifiers Spec lname ty
s2
, pragmas :: [Located String]
pragmas = Spec lname ty -> [Located String]
forall lname ty. Spec lname ty -> [Located String]
pragmas Spec lname ty
s1 [Located String] -> [Located String] -> [Located String]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [Located String]
forall lname ty. Spec lname ty -> [Located String]
pragmas Spec lname ty
s2
, cmeasures :: [MeasureV lname (Located ty) ()]
cmeasures = Spec lname ty -> [MeasureV lname (Located ty) ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures Spec lname ty
s1 [MeasureV lname (Located ty) ()]
-> [MeasureV lname (Located ty) ()]
-> [MeasureV lname (Located ty) ()]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [MeasureV lname (Located ty) ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures Spec lname ty
s2
, imeasures :: [MeasureV lname (Located ty) (Located LHName)]
imeasures = Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures Spec lname ty
s1 [MeasureV lname (Located ty) (Located LHName)]
-> [MeasureV lname (Located ty) (Located LHName)]
-> [MeasureV lname (Located ty) (Located LHName)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures Spec lname ty
s2
, omeasures :: [MeasureV lname (Located ty) (Located LHName)]
omeasures = Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures Spec lname ty
s1 [MeasureV lname (Located ty) (Located LHName)]
-> [MeasureV lname (Located ty) (Located LHName)]
-> [MeasureV lname (Located ty) (Located LHName)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures Spec lname ty
s2
, classes :: [RClass (Located ty)]
classes = Spec lname ty -> [RClass (Located ty)]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
classes Spec lname ty
s1 [RClass (Located ty)]
-> [RClass (Located ty)] -> [RClass (Located ty)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [RClass (Located ty)]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
classes Spec lname ty
s2
, relational :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
relational = Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
relational Spec lname ty
s1 [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
relational Spec lname ty
s2
, asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel = Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel Spec lname ty
s1 [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
forall lname ty.
Spec lname ty
-> [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel Spec lname ty
s2
, termexprs :: [(Located LHName, [Located (ExprV lname)])]
termexprs = Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
termexprs Spec lname ty
s1 [(Located LHName, [Located (ExprV lname)])]
-> [(Located LHName, [Located (ExprV lname)])]
-> [(Located LHName, [Located (ExprV lname)])]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
termexprs Spec lname ty
s2
, rinstance :: [RInstance (Located ty)]
rinstance = Spec lname ty -> [RInstance (Located ty)]
forall lname ty. Spec lname ty -> [RInstance (Located ty)]
rinstance Spec lname ty
s1 [RInstance (Located ty)]
-> [RInstance (Located ty)] -> [RInstance (Located ty)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [RInstance (Located ty)]
forall lname ty. Spec lname ty -> [RInstance (Located ty)]
rinstance Spec lname ty
s2
, dvariance :: [(Located LHName, [Variance])]
dvariance = Spec lname ty -> [(Located LHName, [Variance])]
forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
dvariance Spec lname ty
s1 [(Located LHName, [Variance])]
-> [(Located LHName, [Variance])] -> [(Located LHName, [Variance])]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located LHName, [Variance])]
forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
dvariance Spec lname ty
s2
, dsize :: [([Located ty], lname)]
dsize = Spec lname ty -> [([Located ty], lname)]
forall lname ty. Spec lname ty -> [([Located ty], lname)]
dsize Spec lname ty
s1 [([Located ty], lname)]
-> [([Located ty], lname)] -> [([Located ty], lname)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [([Located ty], lname)]
forall lname ty. Spec lname ty -> [([Located ty], lname)]
dsize Spec lname ty
s2
, axeqs :: [EquationV lname]
axeqs = Spec lname ty -> [EquationV lname]
forall lname ty. Spec lname ty -> [EquationV lname]
axeqs Spec lname ty
s1 [EquationV lname] -> [EquationV lname] -> [EquationV lname]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [EquationV lname]
forall lname ty. Spec lname ty -> [EquationV lname]
axeqs Spec lname ty
s2
, embeds :: TCEmb (Located LHName)
embeds = TCEmb (Located LHName)
-> TCEmb (Located LHName) -> TCEmb (Located LHName)
forall a. Monoid a => a -> a -> a
mappend (Spec lname ty -> TCEmb (Located LHName)
forall lname ty. Spec lname ty -> TCEmb (Located LHName)
embeds Spec lname ty
s1) (Spec lname ty -> TCEmb (Located LHName)
forall lname ty. Spec lname ty -> TCEmb (Located LHName)
embeds Spec lname ty
s2)
, lvars :: HashSet (Located LHName)
lvars = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
lvars Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
lvars Spec lname ty
s2)
, lazy :: HashSet (Located LHName)
lazy = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
lazy Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
lazy Spec lname ty
s2)
, rewrites :: HashSet (Located LHName)
rewrites = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewrites Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewrites Spec lname ty
s2)
, rewriteWith :: HashMap (Located LHName) [Located LHName]
rewriteWith = HashMap (Located LHName) [Located LHName]
-> HashMap (Located LHName) [Located LHName]
-> HashMap (Located LHName) [Located LHName]
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union (Spec lname ty -> HashMap (Located LHName) [Located LHName]
forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
rewriteWith Spec lname ty
s1) (Spec lname ty -> HashMap (Located LHName) [Located LHName]
forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
rewriteWith Spec lname ty
s2)
, fails :: HashSet (Located LHName)
fails = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
fails Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
fails Spec lname ty
s2)
, reflects :: HashSet (Located LHName)
reflects = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects Spec lname ty
s2)
, privateReflects :: HashSet LocSymbol
privateReflects = HashSet LocSymbol -> HashSet LocSymbol -> HashSet LocSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects Spec lname ty
s1) (Spec lname ty -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects Spec lname ty
s2)
, opaqueReflects :: HashSet (Located LHName)
opaqueReflects = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
opaqueReflects Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
opaqueReflects Spec lname ty
s2)
, hmeas :: HashSet (Located LHName)
hmeas = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas Spec lname ty
s2)
, inlines :: HashSet (Located LHName)
inlines = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines Spec lname ty
s2)
, ignores :: HashSet (Located LHName)
ignores = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
ignores Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
ignores Spec lname ty
s2)
, autosize :: HashSet (Located LHName)
autosize = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize Spec lname ty
s2)
, bounds :: RRBEnvV lname (Located ty)
bounds = RRBEnvV lname (Located ty)
-> RRBEnvV lname (Located ty) -> RRBEnvV lname (Located ty)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union (Spec lname ty -> RRBEnvV lname (Located ty)
forall lname ty. Spec lname ty -> RRBEnvV lname (Located ty)
bounds Spec lname ty
s1) (Spec lname ty -> RRBEnvV lname (Located ty)
forall lname ty. Spec lname ty -> RRBEnvV lname (Located ty)
bounds Spec lname ty
s2)
, autois :: HashSet (Located LHName)
autois = HashSet (Located LHName)
-> HashSet (Located LHName) -> HashSet (Located LHName)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois Spec lname ty
s1) (Spec lname ty -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois Spec lname ty
s2)
, defines :: [(Located LHName, LMapV lname)]
defines = Spec lname ty -> [(Located LHName, LMapV lname)]
forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines Spec lname ty
s1 [(Located LHName, LMapV lname)]
-> [(Located LHName, LMapV lname)]
-> [(Located LHName, LMapV lname)]
forall a. [a] -> [a] -> [a]
++ Spec lname ty -> [(Located LHName, LMapV lname)]
forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines Spec lname ty
s2
, usedDataCons :: HashSet LHName
usedDataCons = HashSet LHName -> HashSet LHName -> HashSet LHName
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Spec lname ty -> HashSet LHName
forall lname ty. Spec lname ty -> HashSet LHName
usedDataCons Spec lname ty
s1) (Spec lname ty -> HashSet LHName
forall lname ty. Spec lname ty -> HashSet LHName
usedDataCons Spec lname ty
s2)
}
instance Monoid (Spec lname ty) where
mappend :: Spec lname ty -> Spec lname ty -> Spec lname ty
mappend = Spec lname ty -> Spec lname ty -> Spec lname ty
forall a. Semigroup a => a -> a -> a
(<>)
mempty :: Spec lname ty
mempty
= Spec { measures :: [MeasureV lname (Located ty) (Located LHName)]
measures = []
, expSigs :: [(lname, Sort)]
expSigs = []
, asmSigs :: [(Located LHName, Located ty)]
asmSigs = []
, asmReflectSigs :: [(Located LHName, Located LHName)]
asmReflectSigs = []
, sigs :: [(Located LHName, Located (BareTypeV lname))]
sigs = []
, invariants :: [(Maybe LocSymbol, Located ty)]
invariants = []
, ialiases :: [(Located ty, Located ty)]
ialiases = []
, dataDecls :: [DataDeclP lname ty]
dataDecls = []
, newtyDecls :: [DataDeclP lname ty]
newtyDecls = []
, aliases :: [Located (RTAlias Symbol (BareTypeV lname))]
aliases = []
, ealiases :: [Located (RTAlias Symbol (ExprV lname))]
ealiases = []
, embeds :: TCEmb (Located LHName)
embeds = TCEmb (Located LHName)
forall a. Monoid a => a
mempty
, qualifiers :: [QualifierV lname]
qualifiers = []
, lvars :: HashSet (Located LHName)
lvars = HashSet (Located LHName)
forall a. HashSet a
S.empty
, lazy :: HashSet (Located LHName)
lazy = HashSet (Located LHName)
forall a. HashSet a
S.empty
, rewrites :: HashSet (Located LHName)
rewrites = HashSet (Located LHName)
forall a. HashSet a
S.empty
, rewriteWith :: HashMap (Located LHName) [Located LHName]
rewriteWith = HashMap (Located LHName) [Located LHName]
forall k v. HashMap k v
M.empty
, fails :: HashSet (Located LHName)
fails = HashSet (Located LHName)
forall a. HashSet a
S.empty
, autois :: HashSet (Located LHName)
autois = HashSet (Located LHName)
forall a. HashSet a
S.empty
, hmeas :: HashSet (Located LHName)
hmeas = HashSet (Located LHName)
forall a. HashSet a
S.empty
, reflects :: HashSet (Located LHName)
reflects = HashSet (Located LHName)
forall a. HashSet a
S.empty
, privateReflects :: HashSet LocSymbol
privateReflects = HashSet LocSymbol
forall a. HashSet a
S.empty
, opaqueReflects :: HashSet (Located LHName)
opaqueReflects = HashSet (Located LHName)
forall a. HashSet a
S.empty
, inlines :: HashSet (Located LHName)
inlines = HashSet (Located LHName)
forall a. HashSet a
S.empty
, ignores :: HashSet (Located LHName)
ignores = HashSet (Located LHName)
forall a. HashSet a
S.empty
, autosize :: HashSet (Located LHName)
autosize = HashSet (Located LHName)
forall a. HashSet a
S.empty
, pragmas :: [Located String]
pragmas = []
, cmeasures :: [MeasureV lname (Located ty) ()]
cmeasures = []
, imeasures :: [MeasureV lname (Located ty) (Located LHName)]
imeasures = []
, omeasures :: [MeasureV lname (Located ty) (Located LHName)]
omeasures = []
, classes :: [RClass (Located ty)]
classes = []
, relational :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
relational = []
, asmRel :: [(Located LHName, Located LHName, Located (BareTypeV lname),
Located (BareTypeV lname), RelExprV lname, RelExprV lname)]
asmRel = []
, termexprs :: [(Located LHName, [Located (ExprV lname)])]
termexprs = []
, rinstance :: [RInstance (Located ty)]
rinstance = []
, dvariance :: [(Located LHName, [Variance])]
dvariance = []
, dsize :: [([Located ty], lname)]
dsize = []
, axeqs :: [EquationV lname]
axeqs = []
, bounds :: RRBEnvV lname (Located ty)
bounds = RRBEnvV lname (Located ty)
forall k v. HashMap k v
M.empty
, defines :: [(Located LHName, LMapV lname)]
defines = []
, usedDataCons :: HashSet LHName
usedDataCons = HashSet LHName
forall a. Monoid a => a
mempty
}
data LiftedSpec = LiftedSpec
{
LiftedSpec
-> HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedMeasures :: HashMap F.Symbol (MeasureV LHName LocBareTypeLHName (F.Located LHName))
, LiftedSpec -> HashSet (LHName, Sort)
liftedExpSigs :: HashSet (LHName, F.Sort)
, LiftedSpec -> HashSet LocSymbol
liftedPrivateReflects :: HashSet F.LocSymbol
, LiftedSpec -> HashSet (Located LHName, Located (BareTypeV LHName))
liftedAsmSigs :: HashSet (F.Located LHName, LocBareTypeLHName)
, LiftedSpec -> HashSet (Located LHName, Located (BareTypeV LHName))
liftedSigs :: HashSet (F.Located LHName, LocBareTypeLHName)
, LiftedSpec -> HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareTypeLHName)
, LiftedSpec
-> HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
liftedIaliases :: HashSet (LocBareTypeLHName, LocBareTypeLHName)
, LiftedSpec -> HashSet DataDeclLHName
liftedDataDecls :: HashSet DataDeclLHName
, LiftedSpec -> HashSet DataDeclLHName
liftedNewtyDecls :: HashSet DataDeclLHName
, LiftedSpec -> HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
liftedAliases :: HashSet (F.Located (RTAlias F.Symbol BareTypeLHName))
, LiftedSpec -> HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases :: HashSet (F.Located (RTAlias F.Symbol (F.ExprV LHName)))
, LiftedSpec -> TCEmb (Located LHName)
liftedEmbeds :: F.TCEmb (F.Located LHName)
, LiftedSpec -> HashSet (QualifierV LHName)
liftedQualifiers :: HashSet (F.QualifierV LHName)
, LiftedSpec -> HashSet (Located LHName)
liftedLvars :: HashSet (F.Located LHName)
, LiftedSpec -> HashSet (Located LHName)
liftedAutois :: S.HashSet (F.Located LHName)
, LiftedSpec -> HashSet (Located LHName)
liftedAutosize :: HashSet (F.Located LHName)
, LiftedSpec
-> HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
liftedCmeasures :: HashMap F.Symbol (MeasureV LHName LocBareTypeLHName ())
, LiftedSpec
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedImeasures :: HashSet (MeasureV LHName LocBareTypeLHName (F.Located LHName))
, LiftedSpec
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedOmeasures :: HashSet (MeasureV LHName LocBareTypeLHName (F.Located LHName))
, LiftedSpec -> HashSet (RClass (Located (BareTypeV LHName)))
liftedClasses :: HashSet (RClass LocBareTypeLHName)
, LiftedSpec -> HashSet (RInstance (Located (BareTypeV LHName)))
liftedRinstance :: HashSet (RInstance LocBareTypeLHName)
, LiftedSpec -> [([Located (BareTypeV LHName)], LHName)]
liftedDsize :: [([LocBareTypeLHName], LHName)]
, LiftedSpec -> HashSet (Located LHName, [Variance])
liftedDvariance :: HashSet (F.Located LHName, [Variance])
, LiftedSpec -> RRBEnvV LHName (Located (BareTypeV LHName))
liftedBounds :: RRBEnvV LHName LocBareTypeLHName
, LiftedSpec -> HashSet (EquationV LHName)
liftedAxeqs :: HashSet (F.EquationV LHName)
, LiftedSpec -> HashMap Symbol (LMapV LHName)
liftedDefines :: HashMap F.Symbol (LMapV LHName)
, LiftedSpec -> HashSet LHName
liftedUsedDataCons :: HashSet LHName
} 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, Typeable LiftedSpec
Typeable LiftedSpec =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiftedSpec -> c LiftedSpec)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiftedSpec)
-> (LiftedSpec -> Constr)
-> (LiftedSpec -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiftedSpec))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LiftedSpec))
-> ((forall b. Data b => b -> b) -> LiftedSpec -> LiftedSpec)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r)
-> (forall u. (forall d. Data d => d -> u) -> LiftedSpec -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> LiftedSpec -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec)
-> Data LiftedSpec
LiftedSpec -> Constr
LiftedSpec -> DataType
(forall b. Data b => b -> b) -> LiftedSpec -> LiftedSpec
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LiftedSpec -> u
forall u. (forall d. Data d => d -> u) -> LiftedSpec -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiftedSpec
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiftedSpec -> c LiftedSpec
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiftedSpec)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LiftedSpec)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiftedSpec -> c LiftedSpec
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LiftedSpec -> c LiftedSpec
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiftedSpec
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LiftedSpec
$ctoConstr :: LiftedSpec -> Constr
toConstr :: LiftedSpec -> Constr
$cdataTypeOf :: LiftedSpec -> DataType
dataTypeOf :: LiftedSpec -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiftedSpec)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LiftedSpec)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LiftedSpec)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LiftedSpec)
$cgmapT :: (forall b. Data b => b -> b) -> LiftedSpec -> LiftedSpec
gmapT :: (forall b. Data b => b -> b) -> LiftedSpec -> LiftedSpec
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LiftedSpec -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LiftedSpec -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LiftedSpec -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LiftedSpec -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LiftedSpec -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LiftedSpec -> m LiftedSpec
Data, (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)
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 Show LiftedSpec where
show :: LiftedSpec -> String
show = (BareSpec -> String
forall a. Show a => a -> String
show :: BareSpec -> String) (BareSpec -> String)
-> (LiftedSpec -> BareSpec) -> LiftedSpec -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> BareSpec
fromBareSpecLHName (BareSpecLHName -> BareSpec)
-> (LiftedSpec -> BareSpecLHName) -> LiftedSpec -> BareSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> BareSpecLHName
unsafeFromLiftedSpec
fromBareSpecLHName :: BareSpecLHName -> BareSpec
fromBareSpecLHName :: BareSpecLHName -> BareSpec
fromBareSpecLHName BareSpecLHName
sp =
(BareTypeV LHName -> BareType)
-> Spec Symbol (BareTypeV LHName) -> BareSpec
forall ty0 ty1 lname.
(ty0 -> ty1) -> Spec lname ty0 -> Spec lname ty1
mapSpecTy
( (LHName -> Symbol) -> RTypeV LHName BTyCon BTyVar RReft -> BareType
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV LHName -> Symbol
lhNameToResolvedSymbol (RTypeV LHName BTyCon BTyVar RReft -> BareType)
-> (BareTypeV LHName -> RTypeV LHName BTyCon BTyVar RReft)
-> BareTypeV LHName
-> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(UReftV LHName (ReftV LHName) -> RReft)
-> BareTypeV LHName -> RTypeV LHName BTyCon BTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((LHName -> Symbol)
-> (ReftV LHName -> ReftV Symbol)
-> UReftV LHName (ReftV LHName)
-> RReft
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV LHName -> Symbol
lhNameToResolvedSymbol ((LHName -> Symbol) -> ReftV LHName -> ReftV Symbol
forall a b. (a -> b) -> ReftV a -> ReftV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
lhNameToResolvedSymbol))
) (Spec Symbol (BareTypeV LHName) -> BareSpec)
-> Spec Symbol (BareTypeV LHName) -> BareSpec
forall a b. (a -> b) -> a -> b
$
(LHName -> Symbol)
-> BareSpecLHName -> Spec Symbol (BareTypeV LHName)
forall lname0 lname1 ty.
(lname0 -> lname1) -> Spec lname0 ty -> Spec lname1 ty
mapSpecLName LHName -> Symbol
lhNameToResolvedSymbol BareSpecLHName
sp
fromBareSpecParsed :: BareSpecParsed -> BareSpec
fromBareSpecParsed :: BareSpecParsed -> BareSpec
fromBareSpecParsed BareSpecParsed
sp =
(RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))
-> BareType)
-> Spec
Symbol
(RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol)))
-> BareSpec
forall ty0 ty1 lname.
(ty0 -> ty1) -> Spec lname ty0 -> Spec lname ty1
mapSpecTy
( (LocSymbol -> Symbol)
-> RTypeV LocSymbol BTyCon BTyVar RReft -> BareType
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV LocSymbol -> Symbol
forall a. Located a -> a
val (RTypeV LocSymbol BTyCon BTyVar RReft -> BareType)
-> (RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))
-> RTypeV LocSymbol BTyCon BTyVar RReft)
-> RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))
-> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(UReftV LocSymbol (ReftV LocSymbol) -> RReft)
-> RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))
-> RTypeV LocSymbol BTyCon BTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((LocSymbol -> Symbol)
-> (ReftV LocSymbol -> ReftV Symbol)
-> UReftV LocSymbol (ReftV LocSymbol)
-> RReft
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV LocSymbol -> Symbol
forall a. Located a -> a
val ((LocSymbol -> Symbol) -> ReftV LocSymbol -> ReftV Symbol
forall a b. (a -> b) -> ReftV a -> ReftV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSymbol -> Symbol
forall a. Located a -> a
val))
) (Spec
Symbol
(RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol)))
-> BareSpec)
-> Spec
Symbol
(RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol)))
-> BareSpec
forall a b. (a -> b) -> a -> b
$
(LocSymbol -> Symbol)
-> BareSpecParsed
-> Spec
Symbol
(RTypeV
LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol)))
forall lname0 lname1 ty.
(lname0 -> lname1) -> Spec lname0 ty -> Spec lname1 ty
mapSpecLName LocSymbol -> Symbol
forall a. Located a -> a
val BareSpecParsed
sp
emptyLiftedSpec :: LiftedSpec
emptyLiftedSpec :: LiftedSpec
emptyLiftedSpec = LiftedSpec
{ liftedMeasures :: HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedMeasures = HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a. Monoid a => a
mempty
, liftedExpSigs :: HashSet (LHName, Sort)
liftedExpSigs = HashSet (LHName, Sort)
forall a. Monoid a => a
mempty
, liftedPrivateReflects :: HashSet LocSymbol
liftedPrivateReflects = HashSet LocSymbol
forall a. Monoid a => a
mempty
, liftedAsmSigs :: HashSet (Located LHName, Located (BareTypeV LHName))
liftedAsmSigs = HashSet (Located LHName, Located (BareTypeV LHName))
forall a. Monoid a => a
mempty
, liftedSigs :: HashSet (Located LHName, Located (BareTypeV LHName))
liftedSigs = HashSet (Located LHName, Located (BareTypeV LHName))
forall a. Monoid a => a
mempty
, liftedInvariants :: HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
liftedInvariants = HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
forall a. Monoid a => a
mempty
, liftedIaliases :: HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
liftedIaliases = HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
forall a. Monoid a => a
mempty
, liftedDataDecls :: HashSet DataDeclLHName
liftedDataDecls = HashSet DataDeclLHName
forall a. Monoid a => a
mempty
, liftedNewtyDecls :: HashSet DataDeclLHName
liftedNewtyDecls = HashSet DataDeclLHName
forall a. Monoid a => a
mempty
, liftedAliases :: HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
liftedAliases = HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
forall a. Monoid a => a
mempty
, liftedEaliases :: HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases = HashSet (Located (RTAlias Symbol (ExprV LHName)))
forall a. Monoid a => a
mempty
, liftedEmbeds :: TCEmb (Located LHName)
liftedEmbeds = TCEmb (Located LHName)
forall a. Monoid a => a
mempty
, liftedQualifiers :: HashSet (QualifierV LHName)
liftedQualifiers = HashSet (QualifierV LHName)
forall a. Monoid a => a
mempty
, liftedLvars :: HashSet (Located LHName)
liftedLvars = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, liftedAutois :: HashSet (Located LHName)
liftedAutois = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, liftedAutosize :: HashSet (Located LHName)
liftedAutosize = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, liftedCmeasures :: HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
liftedCmeasures = HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
forall a. Monoid a => a
mempty
, liftedImeasures :: HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedImeasures = HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a. Monoid a => a
mempty
, liftedOmeasures :: HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedOmeasures = HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a. Monoid a => a
mempty
, liftedClasses :: HashSet (RClass (Located (BareTypeV LHName)))
liftedClasses = HashSet (RClass (Located (BareTypeV LHName)))
forall a. Monoid a => a
mempty
, liftedRinstance :: HashSet (RInstance (Located (BareTypeV LHName)))
liftedRinstance = HashSet (RInstance (Located (BareTypeV LHName)))
forall a. Monoid a => a
mempty
, liftedDvariance :: HashSet (Located LHName, [Variance])
liftedDvariance = HashSet (Located LHName, [Variance])
forall a. Monoid a => a
mempty
, liftedDsize :: [([Located (BareTypeV LHName)], LHName)]
liftedDsize = [([Located (BareTypeV LHName)], LHName)]
forall a. Monoid a => a
mempty
, liftedBounds :: RRBEnvV LHName (Located (BareTypeV LHName))
liftedBounds = RRBEnvV LHName (Located (BareTypeV LHName))
forall a. Monoid a => a
mempty
, liftedAxeqs :: HashSet (EquationV LHName)
liftedAxeqs = HashSet (EquationV LHName)
forall a. Monoid a => a
mempty
, liftedDefines :: HashMap Symbol (LMapV LHName)
liftedDefines = HashMap Symbol (LMapV LHName)
forall a. Monoid a => a
mempty
, liftedUsedDataCons :: HashSet LHName
liftedUsedDataCons = HashSet LHName
forall a. Monoid a => a
mempty
}
newtype TargetDependencies =
TargetDependencies { TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies :: HashMap StableModule LiftedSpec }
deriving (Typeable TargetDependencies
Typeable TargetDependencies =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TargetDependencies
-> c TargetDependencies)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TargetDependencies)
-> (TargetDependencies -> Constr)
-> (TargetDependencies -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TargetDependencies))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TargetDependencies))
-> ((forall b. Data b => b -> b)
-> TargetDependencies -> TargetDependencies)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r)
-> (forall u.
(forall d. Data d => d -> u) -> TargetDependencies -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> TargetDependencies -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies)
-> Data TargetDependencies
TargetDependencies -> Constr
TargetDependencies -> DataType
(forall b. Data b => b -> b)
-> TargetDependencies -> TargetDependencies
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> TargetDependencies -> u
forall u. (forall d. Data d => d -> u) -> TargetDependencies -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TargetDependencies
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TargetDependencies
-> c TargetDependencies
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TargetDependencies)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TargetDependencies)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TargetDependencies
-> c TargetDependencies
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TargetDependencies
-> c TargetDependencies
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TargetDependencies
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TargetDependencies
$ctoConstr :: TargetDependencies -> Constr
toConstr :: TargetDependencies -> Constr
$cdataTypeOf :: TargetDependencies -> DataType
dataTypeOf :: TargetDependencies -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TargetDependencies)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TargetDependencies)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TargetDependencies)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TargetDependencies)
$cgmapT :: (forall b. Data b => b -> b)
-> TargetDependencies -> TargetDependencies
gmapT :: (forall b. Data b => b -> b)
-> TargetDependencies -> TargetDependencies
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TargetDependencies -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TargetDependencies -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TargetDependencies -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> TargetDependencies -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> TargetDependencies -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TargetDependencies -> m TargetDependencies
Data, 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 -> String
(Int -> TargetDependencies -> ShowS)
-> (TargetDependencies -> String)
-> ([TargetDependencies] -> ShowS)
-> Show TargetDependencies
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TargetDependencies -> ShowS
showsPrec :: Int -> TargetDependencies -> ShowS
$cshow :: TargetDependencies -> String
show :: TargetDependencies -> String
$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 -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x (GhcSpecRefl -> HashSet Var
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 -> String
_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]
}
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 -> [(Symbol, Sort)]
_gsImps :: ![(F.Symbol, F.Sort)]
, GhcSpec -> Config
_gsConfig :: !Config
, GhcSpec -> BareSpec
_gsLSpec :: !(Spec F.Symbol BareType)
}
instance HasConfig GhcSpec where
getConfig :: GhcSpec -> Config
getConfig = GhcSpec -> Config
_gsConfig
toTargetSrc :: GhcSrc -> TargetSrc
toTargetSrc :: GhcSrc -> TargetSrc
toTargetSrc GhcSrc
a = TargetSrc
{ giTarget :: String
giTarget = GhcSrc -> String
_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
}
fromTargetSrc :: TargetSrc -> GhcSrc
fromTargetSrc :: TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
a = Src
{ _giTarget :: String
_giTarget = TargetSrc -> String
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
}
toTargetSpec :: GhcSpec -> TargetSpec
toTargetSpec :: GhcSpec -> TargetSpec
toTargetSpec GhcSpec
ghcSpec = 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
, gsImps :: [(Symbol, Sort)]
gsImps = GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
ghcSpec
, gsConfig :: Config
gsConfig = GhcSpec -> Config
_gsConfig GhcSpec
ghcSpec
}
toLiftedSpec :: BareSpecLHName -> LiftedSpec
toLiftedSpec :: BareSpecLHName -> LiftedSpec
toLiftedSpec BareSpecLHName
a = LiftedSpec
{ liftedMeasures :: HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedMeasures =
[(Symbol,
MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))]
-> HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
[ (Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol LHName
n, MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)
m)
| MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)
m <- BareSpecLHName
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures BareSpecLHName
a
, let n :: LHName
n = Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)
m
]
, liftedExpSigs :: HashSet (LHName, Sort)
liftedExpSigs = [(LHName, Sort)] -> HashSet (LHName, Sort)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(LHName, Sort)] -> HashSet (LHName, Sort))
-> (BareSpecLHName -> [(LHName, Sort)])
-> BareSpecLHName
-> HashSet (LHName, Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [(LHName, Sort)]
forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs (BareSpecLHName -> HashSet (LHName, Sort))
-> BareSpecLHName -> HashSet (LHName, Sort)
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedPrivateReflects :: HashSet LocSymbol
liftedPrivateReflects = BareSpecLHName -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects BareSpecLHName
a
, liftedAsmSigs :: HashSet (Located LHName, Located (BareTypeV LHName))
liftedAsmSigs = [(Located LHName, Located (BareTypeV LHName))]
-> HashSet (Located LHName, Located (BareTypeV LHName))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Located LHName, Located (BareTypeV LHName))]
-> HashSet (Located LHName, Located (BareTypeV LHName)))
-> (BareSpecLHName
-> [(Located LHName, Located (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (Located LHName, Located (BareTypeV LHName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [(Located LHName, Located (BareTypeV LHName))]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmSigs (BareSpecLHName
-> HashSet (Located LHName, Located (BareTypeV LHName)))
-> BareSpecLHName
-> HashSet (Located LHName, Located (BareTypeV LHName))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedSigs :: HashSet (Located LHName, Located (BareTypeV LHName))
liftedSigs = [(Located LHName, Located (BareTypeV LHName))]
-> HashSet (Located LHName, Located (BareTypeV LHName))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Located LHName, Located (BareTypeV LHName))]
-> HashSet (Located LHName, Located (BareTypeV LHName)))
-> (BareSpecLHName
-> [(Located LHName, Located (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (Located LHName, Located (BareTypeV LHName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [(Located LHName, Located (BareTypeV LHName))]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs (BareSpecLHName
-> HashSet (Located LHName, Located (BareTypeV LHName)))
-> BareSpecLHName
-> HashSet (Located LHName, Located (BareTypeV LHName))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedInvariants :: HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
liftedInvariants = [(Maybe LocSymbol, Located (BareTypeV LHName))]
-> HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Maybe LocSymbol, Located (BareTypeV LHName))]
-> HashSet (Maybe LocSymbol, Located (BareTypeV LHName)))
-> (BareSpecLHName
-> [(Maybe LocSymbol, Located (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [(Maybe LocSymbol, Located (BareTypeV LHName))]
forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
invariants (BareSpecLHName
-> HashSet (Maybe LocSymbol, Located (BareTypeV LHName)))
-> BareSpecLHName
-> HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedIaliases :: HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
liftedIaliases = [(Located (BareTypeV LHName), Located (BareTypeV LHName))]
-> HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Located (BareTypeV LHName), Located (BareTypeV LHName))]
-> HashSet
(Located (BareTypeV LHName), Located (BareTypeV LHName)))
-> (BareSpecLHName
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))]
forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
ialiases (BareSpecLHName
-> HashSet
(Located (BareTypeV LHName), Located (BareTypeV LHName)))
-> BareSpecLHName
-> HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedDataDecls :: HashSet DataDeclLHName
liftedDataDecls = [DataDeclLHName] -> HashSet DataDeclLHName
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([DataDeclLHName] -> HashSet DataDeclLHName)
-> (BareSpecLHName -> [DataDeclLHName])
-> BareSpecLHName
-> HashSet DataDeclLHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [DataDeclLHName]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls (BareSpecLHName -> HashSet DataDeclLHName)
-> BareSpecLHName -> HashSet DataDeclLHName
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedNewtyDecls :: HashSet DataDeclLHName
liftedNewtyDecls = [DataDeclLHName] -> HashSet DataDeclLHName
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([DataDeclLHName] -> HashSet DataDeclLHName)
-> (BareSpecLHName -> [DataDeclLHName])
-> BareSpecLHName
-> HashSet DataDeclLHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [DataDeclLHName]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls (BareSpecLHName -> HashSet DataDeclLHName)
-> BareSpecLHName -> HashSet DataDeclLHName
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedAliases :: HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
liftedAliases = [Located (RTAlias Symbol (BareTypeV LHName))]
-> HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Located (RTAlias Symbol (BareTypeV LHName))]
-> HashSet (Located (RTAlias Symbol (BareTypeV LHName))))
-> (BareSpecLHName
-> [Located (RTAlias Symbol (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [Located (RTAlias Symbol (BareTypeV LHName))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
aliases (BareSpecLHName
-> HashSet (Located (RTAlias Symbol (BareTypeV LHName))))
-> BareSpecLHName
-> HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedEaliases :: HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases = [Located (RTAlias Symbol (ExprV LHName))]
-> HashSet (Located (RTAlias Symbol (ExprV LHName)))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Located (RTAlias Symbol (ExprV LHName))]
-> HashSet (Located (RTAlias Symbol (ExprV LHName))))
-> (BareSpecLHName -> [Located (RTAlias Symbol (ExprV LHName))])
-> BareSpecLHName
-> HashSet (Located (RTAlias Symbol (ExprV LHName)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [Located (RTAlias Symbol (ExprV LHName))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases (BareSpecLHName
-> HashSet (Located (RTAlias Symbol (ExprV LHName))))
-> BareSpecLHName
-> HashSet (Located (RTAlias Symbol (ExprV LHName)))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedEmbeds :: TCEmb (Located LHName)
liftedEmbeds = BareSpecLHName -> TCEmb (Located LHName)
forall lname ty. Spec lname ty -> TCEmb (Located LHName)
embeds BareSpecLHName
a
, liftedQualifiers :: HashSet (QualifierV LHName)
liftedQualifiers = [QualifierV LHName] -> HashSet (QualifierV LHName)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([QualifierV LHName] -> HashSet (QualifierV LHName))
-> (BareSpecLHName -> [QualifierV LHName])
-> BareSpecLHName
-> HashSet (QualifierV LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [QualifierV LHName]
forall lname ty. Spec lname ty -> [QualifierV lname]
qualifiers (BareSpecLHName -> HashSet (QualifierV LHName))
-> BareSpecLHName -> HashSet (QualifierV LHName)
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedLvars :: HashSet (Located LHName)
liftedLvars = BareSpecLHName -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
lvars BareSpecLHName
a
, liftedAutois :: HashSet (Located LHName)
liftedAutois = BareSpecLHName -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois BareSpecLHName
a
, liftedAutosize :: HashSet (Located LHName)
liftedAutosize = BareSpecLHName -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize BareSpecLHName
a
, liftedCmeasures :: HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
liftedCmeasures =
[(Symbol, MeasureV LHName (Located (BareTypeV LHName)) ())]
-> HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
[ (Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol LHName
n, MeasureV LHName (Located (BareTypeV LHName)) ()
m)
| MeasureV LHName (Located (BareTypeV LHName)) ()
m <- BareSpecLHName -> [MeasureV LHName (Located (BareTypeV LHName)) ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures BareSpecLHName
a
, let n :: LHName
n = Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ MeasureV LHName (Located (BareTypeV LHName)) () -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV LHName (Located (BareTypeV LHName)) ()
m
]
, liftedImeasures :: HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedImeasures = [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)))
-> (BareSpecLHName
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> BareSpecLHName
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures (BareSpecLHName
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)))
-> BareSpecLHName
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedOmeasures :: HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedOmeasures = [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)))
-> (BareSpecLHName
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> BareSpecLHName
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures (BareSpecLHName
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)))
-> BareSpecLHName
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedClasses :: HashSet (RClass (Located (BareTypeV LHName)))
liftedClasses = [RClass (Located (BareTypeV LHName))]
-> HashSet (RClass (Located (BareTypeV LHName)))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([RClass (Located (BareTypeV LHName))]
-> HashSet (RClass (Located (BareTypeV LHName))))
-> (BareSpecLHName -> [RClass (Located (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (RClass (Located (BareTypeV LHName)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [RClass (Located (BareTypeV LHName))]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
classes (BareSpecLHName -> HashSet (RClass (Located (BareTypeV LHName))))
-> BareSpecLHName -> HashSet (RClass (Located (BareTypeV LHName)))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedRinstance :: HashSet (RInstance (Located (BareTypeV LHName)))
liftedRinstance = [RInstance (Located (BareTypeV LHName))]
-> HashSet (RInstance (Located (BareTypeV LHName)))
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([RInstance (Located (BareTypeV LHName))]
-> HashSet (RInstance (Located (BareTypeV LHName))))
-> (BareSpecLHName -> [RInstance (Located (BareTypeV LHName))])
-> BareSpecLHName
-> HashSet (RInstance (Located (BareTypeV LHName)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [RInstance (Located (BareTypeV LHName))]
forall lname ty. Spec lname ty -> [RInstance (Located ty)]
rinstance (BareSpecLHName
-> HashSet (RInstance (Located (BareTypeV LHName))))
-> BareSpecLHName
-> HashSet (RInstance (Located (BareTypeV LHName)))
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedDvariance :: HashSet (Located LHName, [Variance])
liftedDvariance = [(Located LHName, [Variance])]
-> HashSet (Located LHName, [Variance])
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Located LHName, [Variance])]
-> HashSet (Located LHName, [Variance]))
-> (BareSpecLHName -> [(Located LHName, [Variance])])
-> BareSpecLHName
-> HashSet (Located LHName, [Variance])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [(Located LHName, [Variance])]
forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
dvariance (BareSpecLHName -> HashSet (Located LHName, [Variance]))
-> BareSpecLHName -> HashSet (Located LHName, [Variance])
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedDsize :: [([Located (BareTypeV LHName)], LHName)]
liftedDsize = BareSpecLHName -> [([Located (BareTypeV LHName)], LHName)]
forall lname ty. Spec lname ty -> [([Located ty], lname)]
dsize BareSpecLHName
a
, liftedBounds :: RRBEnvV LHName (Located (BareTypeV LHName))
liftedBounds = BareSpecLHName -> RRBEnvV LHName (Located (BareTypeV LHName))
forall lname ty. Spec lname ty -> RRBEnvV lname (Located ty)
bounds BareSpecLHName
a
, liftedAxeqs :: HashSet (EquationV LHName)
liftedAxeqs = [EquationV LHName] -> HashSet (EquationV LHName)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([EquationV LHName] -> HashSet (EquationV LHName))
-> (BareSpecLHName -> [EquationV LHName])
-> BareSpecLHName
-> HashSet (EquationV LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [EquationV LHName]
forall lname ty. Spec lname ty -> [EquationV lname]
axeqs (BareSpecLHName -> HashSet (EquationV LHName))
-> BareSpecLHName -> HashSet (EquationV LHName)
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedDefines :: HashMap Symbol (LMapV LHName)
liftedDefines = [(Symbol, LMapV LHName)] -> HashMap Symbol (LMapV LHName)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, LMapV LHName)] -> HashMap Symbol (LMapV LHName))
-> (BareSpecLHName -> [(Symbol, LMapV LHName)])
-> BareSpecLHName
-> HashMap Symbol (LMapV LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Located LHName, LMapV LHName) -> (Symbol, LMapV LHName))
-> [(Located LHName, LMapV LHName)] -> [(Symbol, LMapV LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Located LHName -> Symbol)
-> (Located LHName, LMapV LHName) -> (Symbol, LMapV LHName)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> (Located LHName -> LHName) -> Located LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
F.val)) ([(Located LHName, LMapV LHName)] -> [(Symbol, LMapV LHName)])
-> (BareSpecLHName -> [(Located LHName, LMapV LHName)])
-> BareSpecLHName
-> [(Symbol, LMapV LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecLHName -> [(Located LHName, LMapV LHName)]
forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines (BareSpecLHName -> HashMap Symbol (LMapV LHName))
-> BareSpecLHName -> HashMap Symbol (LMapV LHName)
forall a b. (a -> b) -> a -> b
$ BareSpecLHName
a
, liftedUsedDataCons :: HashSet LHName
liftedUsedDataCons = BareSpecLHName -> HashSet LHName
forall lname ty. Spec lname ty -> HashSet LHName
usedDataCons BareSpecLHName
a
}
unsafeFromLiftedSpec :: LiftedSpec -> BareSpecLHName
unsafeFromLiftedSpec :: LiftedSpec -> BareSpecLHName
unsafeFromLiftedSpec LiftedSpec
a = Spec
{ measures :: [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
measures = HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall k v. HashMap k v -> [v]
M.elems (HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
-> HashMap
Symbol
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedMeasures LiftedSpec
a
, expSigs :: [(LHName, Sort)]
expSigs = HashSet (LHName, Sort) -> [(LHName, Sort)]
forall a. HashSet a -> [a]
S.toList (HashSet (LHName, Sort) -> [(LHName, Sort)])
-> (LiftedSpec -> HashSet (LHName, Sort))
-> LiftedSpec
-> [(LHName, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LHName, Sort)
liftedExpSigs (LiftedSpec -> [(LHName, Sort)]) -> LiftedSpec -> [(LHName, Sort)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, asmSigs :: [(Located LHName, Located (BareTypeV LHName))]
asmSigs = HashSet (Located LHName, Located (BareTypeV LHName))
-> [(Located LHName, Located (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName, Located (BareTypeV LHName))
-> [(Located LHName, Located (BareTypeV LHName))])
-> (LiftedSpec
-> HashSet (Located LHName, Located (BareTypeV LHName)))
-> LiftedSpec
-> [(Located LHName, Located (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located LHName, Located (BareTypeV LHName))
liftedAsmSigs (LiftedSpec -> [(Located LHName, Located (BareTypeV LHName))])
-> LiftedSpec -> [(Located LHName, Located (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, asmReflectSigs :: [(Located LHName, Located LHName)]
asmReflectSigs = [(Located LHName, Located LHName)]
forall a. Monoid a => a
mempty
, sigs :: [(Located LHName, Located (BareTypeV LHName))]
sigs = HashSet (Located LHName, Located (BareTypeV LHName))
-> [(Located LHName, Located (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName, Located (BareTypeV LHName))
-> [(Located LHName, Located (BareTypeV LHName))])
-> (LiftedSpec
-> HashSet (Located LHName, Located (BareTypeV LHName)))
-> LiftedSpec
-> [(Located LHName, Located (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located LHName, Located (BareTypeV LHName))
liftedSigs (LiftedSpec -> [(Located LHName, Located (BareTypeV LHName))])
-> LiftedSpec -> [(Located LHName, Located (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, relational :: [(Located LHName, Located LHName, Located (BareTypeV LHName),
Located (BareTypeV LHName), RelExprV LHName, RelExprV LHName)]
relational = [(Located LHName, Located LHName, Located (BareTypeV LHName),
Located (BareTypeV LHName), RelExprV LHName, RelExprV LHName)]
forall a. Monoid a => a
mempty
, asmRel :: [(Located LHName, Located LHName, Located (BareTypeV LHName),
Located (BareTypeV LHName), RelExprV LHName, RelExprV LHName)]
asmRel = [(Located LHName, Located LHName, Located (BareTypeV LHName),
Located (BareTypeV LHName), RelExprV LHName, RelExprV LHName)]
forall a. Monoid a => a
mempty
, invariants :: [(Maybe LocSymbol, Located (BareTypeV LHName))]
invariants = HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
-> [(Maybe LocSymbol, Located (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
-> [(Maybe LocSymbol, Located (BareTypeV LHName))])
-> (LiftedSpec
-> HashSet (Maybe LocSymbol, Located (BareTypeV LHName)))
-> LiftedSpec
-> [(Maybe LocSymbol, Located (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
liftedInvariants (LiftedSpec -> [(Maybe LocSymbol, Located (BareTypeV LHName))])
-> LiftedSpec -> [(Maybe LocSymbol, Located (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, ialiases :: [(Located (BareTypeV LHName), Located (BareTypeV LHName))]
ialiases = HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))])
-> (LiftedSpec
-> HashSet
(Located (BareTypeV LHName), Located (BareTypeV LHName)))
-> LiftedSpec
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec
-> HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
liftedIaliases (LiftedSpec
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))])
-> LiftedSpec
-> [(Located (BareTypeV LHName), Located (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, dataDecls :: [DataDeclLHName]
dataDecls = HashSet DataDeclLHName -> [DataDeclLHName]
forall a. HashSet a -> [a]
S.toList (HashSet DataDeclLHName -> [DataDeclLHName])
-> (LiftedSpec -> HashSet DataDeclLHName)
-> LiftedSpec
-> [DataDeclLHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDeclLHName
liftedDataDecls (LiftedSpec -> [DataDeclLHName]) -> LiftedSpec -> [DataDeclLHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, newtyDecls :: [DataDeclLHName]
newtyDecls = HashSet DataDeclLHName -> [DataDeclLHName]
forall a. HashSet a -> [a]
S.toList (HashSet DataDeclLHName -> [DataDeclLHName])
-> (LiftedSpec -> HashSet DataDeclLHName)
-> LiftedSpec
-> [DataDeclLHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDeclLHName
liftedNewtyDecls (LiftedSpec -> [DataDeclLHName]) -> LiftedSpec -> [DataDeclLHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, aliases :: [Located (RTAlias Symbol (BareTypeV LHName))]
aliases = HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
-> [Located (RTAlias Symbol (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
-> [Located (RTAlias Symbol (BareTypeV LHName))])
-> (LiftedSpec
-> HashSet (Located (RTAlias Symbol (BareTypeV LHName))))
-> LiftedSpec
-> [Located (RTAlias Symbol (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
liftedAliases (LiftedSpec -> [Located (RTAlias Symbol (BareTypeV LHName))])
-> LiftedSpec -> [Located (RTAlias Symbol (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, ealiases :: [Located (RTAlias Symbol (ExprV LHName))]
ealiases = HashSet (Located (RTAlias Symbol (ExprV LHName)))
-> [Located (RTAlias Symbol (ExprV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (RTAlias Symbol (ExprV LHName)))
-> [Located (RTAlias Symbol (ExprV LHName))])
-> (LiftedSpec
-> HashSet (Located (RTAlias Symbol (ExprV LHName))))
-> LiftedSpec
-> [Located (RTAlias Symbol (ExprV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases (LiftedSpec -> [Located (RTAlias Symbol (ExprV LHName))])
-> LiftedSpec -> [Located (RTAlias Symbol (ExprV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, embeds :: TCEmb (Located LHName)
embeds = LiftedSpec -> TCEmb (Located LHName)
liftedEmbeds LiftedSpec
a
, qualifiers :: [QualifierV LHName]
qualifiers = HashSet (QualifierV LHName) -> [QualifierV LHName]
forall a. HashSet a -> [a]
S.toList (HashSet (QualifierV LHName) -> [QualifierV LHName])
-> (LiftedSpec -> HashSet (QualifierV LHName))
-> LiftedSpec
-> [QualifierV LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (QualifierV LHName)
liftedQualifiers (LiftedSpec -> [QualifierV LHName])
-> LiftedSpec -> [QualifierV LHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, lvars :: HashSet (Located LHName)
lvars = LiftedSpec -> HashSet (Located LHName)
liftedLvars LiftedSpec
a
, lazy :: HashSet (Located LHName)
lazy = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, fails :: HashSet (Located LHName)
fails = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, rewrites :: HashSet (Located LHName)
rewrites = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, rewriteWith :: HashMap (Located LHName) [Located LHName]
rewriteWith = HashMap (Located LHName) [Located LHName]
forall a. Monoid a => a
mempty
, reflects :: HashSet (Located LHName)
reflects = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, privateReflects :: HashSet LocSymbol
privateReflects = LiftedSpec -> HashSet LocSymbol
liftedPrivateReflects LiftedSpec
a
, opaqueReflects :: HashSet (Located LHName)
opaqueReflects = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, autois :: HashSet (Located LHName)
autois = LiftedSpec -> HashSet (Located LHName)
liftedAutois LiftedSpec
a
, hmeas :: HashSet (Located LHName)
hmeas = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, inlines :: HashSet (Located LHName)
inlines = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, ignores :: HashSet (Located LHName)
ignores = HashSet (Located LHName)
forall a. Monoid a => a
mempty
, autosize :: HashSet (Located LHName)
autosize = LiftedSpec -> HashSet (Located LHName)
liftedAutosize LiftedSpec
a
, pragmas :: [Located String]
pragmas = [Located String]
forall a. Monoid a => a
mempty
, cmeasures :: [MeasureV LHName (Located (BareTypeV LHName)) ()]
cmeasures = HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
-> [MeasureV LHName (Located (BareTypeV LHName)) ()]
forall k v. HashMap k v -> [v]
M.elems (HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
-> [MeasureV LHName (Located (BareTypeV LHName)) ()])
-> HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
-> [MeasureV LHName (Located (BareTypeV LHName)) ()]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
-> HashMap Symbol (MeasureV LHName (Located (BareTypeV LHName)) ())
liftedCmeasures LiftedSpec
a
, imeasures :: [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
imeasures = HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall a. HashSet a -> [a]
S.toList (HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> (LiftedSpec
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)))
-> LiftedSpec
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedImeasures (LiftedSpec
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> LiftedSpec
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, omeasures :: [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
omeasures = HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall a. HashSet a -> [a]
S.toList (HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> (LiftedSpec
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)))
-> LiftedSpec
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec
-> HashSet
(MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedOmeasures (LiftedSpec
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)])
-> LiftedSpec
-> [MeasureV LHName (Located (BareTypeV LHName)) (Located LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, classes :: [RClass (Located (BareTypeV LHName))]
classes = HashSet (RClass (Located (BareTypeV LHName)))
-> [RClass (Located (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (RClass (Located (BareTypeV LHName)))
-> [RClass (Located (BareTypeV LHName))])
-> (LiftedSpec -> HashSet (RClass (Located (BareTypeV LHName))))
-> LiftedSpec
-> [RClass (Located (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass (Located (BareTypeV LHName)))
liftedClasses (LiftedSpec -> [RClass (Located (BareTypeV LHName))])
-> LiftedSpec -> [RClass (Located (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, termexprs :: [(Located LHName, [Located (ExprV LHName)])]
termexprs = [(Located LHName, [Located (ExprV LHName)])]
forall a. Monoid a => a
mempty
, rinstance :: [RInstance (Located (BareTypeV LHName))]
rinstance = HashSet (RInstance (Located (BareTypeV LHName)))
-> [RInstance (Located (BareTypeV LHName))]
forall a. HashSet a -> [a]
S.toList (HashSet (RInstance (Located (BareTypeV LHName)))
-> [RInstance (Located (BareTypeV LHName))])
-> (LiftedSpec -> HashSet (RInstance (Located (BareTypeV LHName))))
-> LiftedSpec
-> [RInstance (Located (BareTypeV LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RInstance (Located (BareTypeV LHName)))
liftedRinstance (LiftedSpec -> [RInstance (Located (BareTypeV LHName))])
-> LiftedSpec -> [RInstance (Located (BareTypeV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, dvariance :: [(Located LHName, [Variance])]
dvariance = HashSet (Located LHName, [Variance])
-> [(Located LHName, [Variance])]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName, [Variance])
-> [(Located LHName, [Variance])])
-> (LiftedSpec -> HashSet (Located LHName, [Variance]))
-> LiftedSpec
-> [(Located LHName, [Variance])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located LHName, [Variance])
liftedDvariance (LiftedSpec -> [(Located LHName, [Variance])])
-> LiftedSpec -> [(Located LHName, [Variance])]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, dsize :: [([Located (BareTypeV LHName)], LHName)]
dsize = LiftedSpec -> [([Located (BareTypeV LHName)], LHName)]
liftedDsize LiftedSpec
a
, bounds :: RRBEnvV LHName (Located (BareTypeV LHName))
bounds = LiftedSpec -> RRBEnvV LHName (Located (BareTypeV LHName))
liftedBounds LiftedSpec
a
, axeqs :: [EquationV LHName]
axeqs = HashSet (EquationV LHName) -> [EquationV LHName]
forall a. HashSet a -> [a]
S.toList (HashSet (EquationV LHName) -> [EquationV LHName])
-> (LiftedSpec -> HashSet (EquationV LHName))
-> LiftedSpec
-> [EquationV LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (EquationV LHName)
liftedAxeqs (LiftedSpec -> [EquationV LHName])
-> LiftedSpec -> [EquationV LHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, defines :: [(Located LHName, LMapV LHName)]
defines = ((Symbol, LMapV LHName) -> (Located LHName, LMapV LHName))
-> [(Symbol, LMapV LHName)] -> [(Located LHName, LMapV LHName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> Located LHName)
-> (Symbol, LMapV LHName) -> (Located LHName, LMapV LHName)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (LHName -> Located LHName
forall a. a -> Located a
dummyLoc (LHName -> Located LHName)
-> (Symbol -> LHName) -> Symbol -> Located LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> LHName
makeLocalLHName)) ([(Symbol, LMapV LHName)] -> [(Located LHName, LMapV LHName)])
-> (LiftedSpec -> [(Symbol, LMapV LHName)])
-> LiftedSpec
-> [(Located LHName, LMapV LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Symbol (LMapV LHName) -> [(Symbol, LMapV LHName)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Symbol (LMapV LHName) -> [(Symbol, LMapV LHName)])
-> (LiftedSpec -> HashMap Symbol (LMapV LHName))
-> LiftedSpec
-> [(Symbol, LMapV LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashMap Symbol (LMapV LHName)
liftedDefines (LiftedSpec -> [(Located LHName, LMapV LHName)])
-> LiftedSpec -> [(Located LHName, LMapV LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
, usedDataCons :: HashSet LHName
usedDataCons = LiftedSpec -> HashSet LHName
liftedUsedDataCons LiftedSpec
a
}