-- | This module contains the top-level structures that hold
--   information about specifications.

{-# 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 (
  -- * Different types of specifications
  -- $differentSpecTypes
  -- * TargetInfo
  -- $targetInfo
    TargetInfo(..)
  -- * Gathering information about a module
  , TargetSrc(..)
  -- * TargetSpec
  -- $targetSpec
  , TargetSpec(..)
  -- * BareSpec
  -- $bareSpec
  , BareSpec
  , BareSpecLHName
  , BareSpecParsed
  -- * LiftedSpec
  -- $liftedSpec
  , LiftedSpec(..)
  -- * Tracking dependencies
  -- $trackingDeps
  , TargetDependencies(..)
  , dropDependency
  -- * Predicates on spec types
  -- $predicates
  , isPLEVar
  , isExportedVar
  -- * Other types
  , QImports(..)
  , Spec(..)
  , GhcSpecVars(..)
  , GhcSpecSig(..)
  , GhcSpecNames(..)
  , GhcSpecTerm(..)
  , GhcSpecRefl(..)
  , GhcSpecData(..)
  , GhcSpecQual(..)
  , BareDef
  , BareMeasure
  , SpecMeasure
  , VarOrLocSymbol
  , emapSpecM
  , fromBareSpecLHName
  , fromBareSpecParsed
  , mapSpecLName
  , mapSpecTy
  -- * Legacy data structures
  -- $legacyDataStructures
  , GhcSrc(..)
  , GhcSpec(..)
  -- * Provisional compatibility exports & optics
  -- $provisionalBackCompat
  , 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 (($$))


{- $differentSpecTypes

There are different types or \"flavours\" for a specification, depending on its lifecycle. The main goal
is always the same, i.e. refining the Haskell types and produce a final statement (i.e. safe or unsafe)
about the input program. In order to do so, a /specification/ is transformed in the way described by this
picture:

@
    +---------------+                                +-------------------+
    |   BareSpec    |                                |                   |  checked by liquid/liquidOne
    |               |                    ------------|    TargetSpec     |----------------------------- ..
    |(input module) |                   /            |                   |
    +---------------+  makeTargetSpec  /             +-------------------+
           +         -----------------/
    +---------------+                 \\              +-------------------+
    | {LiftedSpec}  |                  \\             |                   |    serialised on disk
    |               |                   -------------|    LiftedSpec     |----------------------------- ..
    |(dependencies) |                                |                   |
    +---------------+                                +-------------------+
          ^                                                    |
          |                   used-as                          |
          +----------------------------------------------------+
@

More specifically, we distinguish:

* 'BareSpec' - is the specification obtained by parsing the Liquid annotations of the input Haskell file.
  It typically contains information about the associated input Haskell module, with the exceptions of
  /assumptions/ that can refer to functions defined in other modules.

* 'LiftedSpec' - is the specification we obtain by \"lifting\" the 'BareSpec'. Most importantly, a
  'LiftedSpec' gets serialised on disk and becomes a /dependency/ for the verification of other 'BareSpec's.

   Lifting in this context consist of:

    1. Perform name-resolution (e.g. make all the relevant GHC's 'Var's qualified, resolve GHC's 'Name's, etc);
    2. Strip the final 'LiftedSpec' with information which are relevant (read: local) to just the input
       'BareSpec'. An example would be /local signatures/, used to annotate internal, auxiliary functions
       within a 'Module';
    3. Strip termination checks, which are /required/ (if specified) for a 'BareSpec' but not for the
       'LiftedSpec'.

* 'TargetSpec' - is the specification we /actually use for refinement/, and is conceptually an
  \"augmented\" 'BareSpec'. You can create a 'TargetSpec' by calling 'makeTargetSpec'.

In order to produce these spec types we have to gather information about the module being compiled by using
the GHC API and retain enough context of the compiled 'Module' in order to be able to construct the types
introduced aboves. The rest of this module introduced also these intermediate structures.
-}

-- $targetInfo
-- The following is the overall type for /specifications/ obtained from
-- parsing the target source and dependent libraries.
-- /IMPORTANT/: A 'TargetInfo' is what is /checked/ by LH itself and it /NEVER/ contains the 'LiftedSpec',
-- because the checking happens only on the 'BareSpec' of the target module.
data TargetInfo = TargetInfo
  { TargetInfo -> TargetSrc
giSrc  :: !TargetSrc
    -- ^ The 'TargetSrc' of the module being checked.
  , TargetInfo -> TargetSpec
giSpec :: !TargetSpec
    -- ^ The 'TargetSpec' of the module being checked.
  }

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

-- | The 'TargetSrc' type is a collection of all the things we know about a module being currently
-- checked. It include things like the name of the module, the list of 'CoreBind's,
-- the 'TyCon's declared in this module (that includes 'TyCon's for classes), typeclass instances
-- and so and so forth. It might be consider a sort of 'ModGuts' embellished with LH-specific
-- information (for example, 'giDefVars' are populated with datacons from the module plus the
-- let vars derived from the A-normalisation).
data TargetSrc = TargetSrc
  { TargetSrc -> String
giTarget    :: !FilePath              -- ^ Source file for module
  , TargetSrc -> ModName
giTargetMod :: !ModName               -- ^ Name for module
  , TargetSrc -> [CoreBind]
giCbs       :: ![CoreBind]            -- ^ Source Code
  , TargetSrc -> [TyCon]
gsTcs       :: ![TyCon]               -- ^ All used Type constructors
  , TargetSrc -> Maybe [ClsInst]
gsCls       :: !(Maybe [ClsInst])     -- ^ Class instances?
  , TargetSrc -> HashSet Var
giDerVars   :: !(HashSet Var)         -- ^ Binders created by GHC eg dictionaries
  , TargetSrc -> [Var]
giImpVars   :: ![Var]                 -- ^ Binders that are _read_ in module (but not defined?)
  , TargetSrc -> [Var]
giDefVars   :: ![Var]                 -- ^ (Top-level) binders that are _defined_ in module
  , TargetSrc -> [Var]
giUseVars   :: ![Var]                 -- ^ Binders that are _read_ in module
  , TargetSrc -> HashSet StableName
gsExports   :: !(HashSet StableName)  -- ^ `Name`s exported by the module being verified
  , TargetSrc -> [TyCon]
gsFiTcs     :: ![TyCon]               -- ^ Family instance TyCons
  , TargetSrc -> [(Symbol, DataCon)]
gsFiDcs     :: ![(F.Symbol, DataCon)] -- ^ Family instance DataCons
  , TargetSrc -> [TyCon]
gsPrimTcs   :: ![TyCon]               -- ^ Primitive GHC TyCons (from TysPrim.primTyCons)
  }

-- | 'QImports' is a map of qualified imports.
data QImports = QImports
  { QImports -> HashSet Symbol
qiModules :: !(S.HashSet F.Symbol)            -- ^ All the modules that are imported qualified
  , QImports -> HashMap Symbol [Symbol]
qiNames   :: !(M.HashMap F.Symbol [F.Symbol]) -- ^ Map from qualification to full module name
  } 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

-- $targetSpec

-- | A 'TargetSpec' is what we /actually check via LiquidHaskell/. It is created as part of 'mkTargetSpec'
-- alongside the 'LiftedSpec'. It shares a similar structure with a 'BareSpec', but manipulates and
-- transforms the data in preparation to the checking process.
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)]  -- ^ Imported Environment
  , 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

-- | The collection of GHC 'Var's that a 'TargetSpec' needs to verify (or skip).
data GhcSpecVars = SpVar
  { GhcSpecVars -> [Var]
gsTgtVars    :: ![Var]                        -- ^ Top-level Binders To Verify (empty means ALL binders)
  , GhcSpecVars -> HashSet Var
gsIgnoreVars :: !(S.HashSet Var)              -- ^ Top-level Binders To NOT Verify (empty means ALL binders)
  , GhcSpecVars -> HashSet Var
gsLvars      :: !(S.HashSet Var)              -- ^ Variables that should be checked "lazily" in the environment they are used
  , GhcSpecVars -> [Var]
gsCMethods   :: ![Var]                        -- ^ Refined Class methods
  }
  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]                -- ^ Qualifiers in Source/Spec files e.g tests/pos/qualTest.hs
  , GhcSpecQual -> [Located SpecRTAlias]
gsRTAliases  :: ![F.Located SpecRTAlias]      -- ^ Refinement type aliases (only used for qualifiers)
  }
  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)]           -- ^ Asserted Reftypes
  , GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs  :: ![(Var, LocSpecType)]           -- ^ Assumed Reftypes
  , GhcSpecSig -> [(Var, Var)]
gsAsmReflects  :: ![(Var, Var)]               -- ^ Assumed Reftypes (left is the actual function name and right the pretended one)
  , GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs  :: ![(Var, LocSpecType)]           -- ^ Reflected Reftypes
  , GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs   :: ![(Var, LocSpecType)]           -- ^ Auto generated Signatures
  , GhcSpecSig -> [(TyCon, LocSpecType)]
gsNewTypes :: ![(TyCon, LocSpecType)]         -- ^ Mapping of 'newtype' type constructors with their refined types.
  , GhcSpecSig -> DEnv Var LocSpecType
gsDicts    :: !(DEnv Var LocSpecType)            -- ^ Refined Classes from Instances
  , GhcSpecSig -> [(Var, MethodType LocSpecType)]
gsMethods  :: ![(Var, MethodType LocSpecType)]   -- ^ Refined Classes from Classes
  , GhcSpecSig -> [(Var, LocSpecType, [Located Expr])]
gsTexprs   :: ![(Var, LocSpecType, [F.Located F.Expr])]  -- ^ Lexicographically ordered expressions for termination
  , 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)]         -- ^ Data Constructor Measure Sigs
  , GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas       :: ![(F.Symbol, LocSpecType)]    -- ^ Measure Types eg.  len :: [a] -> Int
  , GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants :: ![(Maybe Var, LocSpecType)]   -- ^ Data type invariants from measure definitions, e.g forall a. {v: [a] | len(v) >= 0}
  , GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases   :: ![(LocSpecType, LocSpecType)] -- ^ Data type invariant aliases
  , GhcSpecData
-> [Measure (RTypeV Symbol RTyCon RTyVar RReft) DataCon]
gsMeasures   :: ![Measure SpecType DataCon]   -- ^ Measure definitions
  , GhcSpecData -> [Var]
gsOpaqueRefls:: ![Var]                        -- ^ List of opaque reflected measures
  , 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]          -- ^ Predicated Data-Constructors, e.g. see tests/pos/Map.hs
  , GhcSpecNames -> [TyConP]
gsTconsP     :: ![TyConP]                     -- ^ Predicated Type-Constructors, e.g. see tests/pos/Map.hs
  , GhcSpecNames -> TCEmb TyCon
gsTcEmbeds   :: !(F.TCEmb TyCon)              -- ^ Embedding GHC Tycons into fixpoint sorts e.g. "embed Set as Set_set"
  , GhcSpecNames -> [DataDecl]
gsADTs       :: ![F.DataDecl]                 -- ^ ADTs extracted from Haskell 'data' definitions
  , 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)              -- ^ Binders to CHECK by structural termination
  , GhcSpecTerm -> HashSet TyCon
gsAutosize   :: !(S.HashSet TyCon)            -- ^ Binders to IGNORE during termination checking
  , GhcSpecTerm -> HashSet Var
gsLazy       :: !(S.HashSet Var)              -- ^ Binders to IGNORE during termination checking
  , GhcSpecTerm -> HashSet (Located Var)
gsFail       :: !(S.HashSet (F.Located Var))    -- ^ Binders to fail type checking
  , GhcSpecTerm -> HashSet Var
gsNonStTerm  :: !(S.HashSet Var)              -- ^ Binders to CHECK using REFINEMENT-TYPES/termination metrics
  }
  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)                  -- ^ Binders to USE PLE
  , GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms      :: ![(Var, LocSpecType, F.Equation)] -- ^ Lifted definitions
  , GhcSpecRefl -> [Equation]
gsImpAxioms    :: ![F.Equation]                     -- ^ Axioms from imported reflected functions
  , GhcSpecRefl -> [Equation]
gsMyAxioms     :: ![F.Equation]                     -- ^ Axioms from my reflected functions
  , GhcSpecRefl -> [Var]
gsReflects     :: ![Var]                            -- ^ Binders for reflected functions
  , 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

-- $bareSpec

-- | A 'BareSpec' is the spec we derive by parsing the Liquid Haskell annotations of a single file. As
-- such, it contains things which are relevant for validation and lifting; it contains things like
-- the pragmas the user defined, the termination condition (if termination-checking is enabled) and so
-- on and so forth. /Crucially/, as a 'BareSpec' is still subject to \"preflight checks\", it may contain
-- duplicates (e.g. duplicate measures, duplicate type declarations etc.) and therefore most of the fields
-- for a 'BareSpec' are lists, so that we can report these errors to the end user: it would be an error
-- to silently ignore the duplication and leave the duplicate resolution to whichever 'Eq' instance is
-- implemented for the relevant field.
--
-- Also, a 'BareSpec' has not yet been subject to name resolution, so it may refer
-- to undefined or out-of-scope entities.
type BareSpec = Spec F.Symbol BareType
type BareSpecLHName = Spec LHName BareTypeLHName
type BareSpecParsed = Spec LocSymbol BareTypeParsed

-- | A generic 'Spec' type, polymorphic over the inner choice of type and binders.
--
-- @lname@ corresponds to the names used for entities only known to LH like
-- non-interpreted functions and type aliases.
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)] -- ^ User-defined properties for ADTs
  , forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs    :: ![(lname, F.Sort)]                                  -- ^ Exported logic symbols originated by reflecting functions
  , forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
asmSigs    :: ![(F.Located LHName, F.Located ty)]                 -- ^ Assumed (unchecked) types; including reflected signatures
  , forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
asmReflectSigs :: ![(F.Located LHName, F.Located LHName)]         -- ^ Assume reflects : left is the actual function and right the pretended one
  , forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs       :: ![(F.Located LHName, F.Located (BareTypeV lname))]  -- ^ Asserted spec signatures
  , forall lname ty. Spec lname ty -> [(Maybe LocSymbol, Located ty)]
invariants :: ![(Maybe F.LocSymbol, F.Located ty)]                -- ^ Data type invariants; the Maybe is the generating measure
  , forall lname ty. Spec lname ty -> [(Located ty, Located ty)]
ialiases   :: ![(F.Located ty, F.Located ty)]                     -- ^ Data type invariants to be checked
  , forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls  :: ![DataDeclP lname ty]                               -- ^ Predicated data definitions
  , forall lname ty. Spec lname ty -> [DataDeclP lname ty]
newtyDecls :: ![DataDeclP lname ty]                               -- ^ Predicated new type definitions
  , forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
aliases    :: ![F.Located (RTAlias F.Symbol (BareTypeV lname))]   -- ^ RefType aliases
  , forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases   :: ![F.Located (RTAlias F.Symbol (F.ExprV lname))]     -- ^ Expression aliases
  , forall lname ty. Spec lname ty -> TCEmb (Located LHName)
embeds     :: !(F.TCEmb (F.Located LHName))                       -- ^ GHC-Tycon-to-fixpoint Tycon map
  , forall lname ty. Spec lname ty -> [QualifierV lname]
qualifiers :: ![F.QualifierV lname]                               -- ^ Qualifiers in source files
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
lvars      :: !(S.HashSet (F.Located LHName))                     -- ^ Variables that should be checked in the environment they are used
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
lazy       :: !(S.HashSet (F.Located LHName))                     -- ^ Ignore Termination Check in these Functions
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
rewrites    :: !(S.HashSet (F.Located LHName))                    -- ^ Theorems turned into rewrite rules
  , forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName]) -- ^ Definitions using rewrite rules
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
fails      :: !(S.HashSet (F.Located LHName))                     -- ^ These Functions should be unsafe
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects   :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to reflect
  , forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects :: !(S.HashSet F.LocSymbol)                       -- ^ Private binders to reflect
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
opaqueReflects :: !(S.HashSet (F.Located LHName))                 -- ^ Binders to opaque-reflect
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
autois     :: !(S.HashSet (F.Located LHName))                     -- ^ Automatically instantiate axioms in these Functions
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas      :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to turn into measures using haskell definitions
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines    :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to turn into logic inline using haskell definitions
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
ignores    :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to ignore during checking; that is DON't check the corebind.
  , forall lname ty. Spec lname ty -> HashSet (Located LHName)
autosize   :: !(S.HashSet (F.Located LHName))                     -- ^ Type Constructors that get automatically sizing info
  , forall lname ty. Spec lname ty -> [Located String]
pragmas    :: ![F.Located String]                                 -- ^ Command-line configurations passed in through source
  , forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures  :: ![MeasureV lname (F.Located ty) ()]                 -- ^ Measures attached to a type-class
  , forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures  :: ![MeasureV lname (F.Located ty) (F.Located LHName)] -- ^ Mappings from (measure,type) -> measure
  , forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures  :: ![MeasureV lname (F.Located ty) (F.Located LHName)] -- ^ Opaque reflection measures.
  -- Separate field bc measures are checked for duplicates, and we want to allow for opaque-reflected measures to be duplicated.
  -- See Note [Duplicate measures and opaque reflection] in "Language.Haskell.Liquid.Measure".
  , forall lname ty. Spec lname ty -> [RClass (Located ty)]
classes    :: ![RClass (F.Located ty)]                            -- ^ Refined Type-Classes
  , 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)] -- ^ Relational types
  , 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)] -- ^ Assumed relational types
  , forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
termexprs  :: ![(F.Located LHName, [F.Located (F.ExprV lname)])]  -- ^ Terminating Conditions for functions
  , 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])]                   -- ^ TODO ? Where do these come from ?!
  , forall lname ty. Spec lname ty -> [([Located ty], lname)]
dsize      :: ![([F.Located ty], lname)]                          -- ^ Size measure to enforce fancy termination
  , 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]                                -- ^ Equalities used for Proof-By-Evaluation
  , forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines    :: ![(F.Located LHName, LMapV lname)]                  -- ^ Logic aliases
  , forall lname ty. Spec lname ty -> HashSet LHName
usedDataCons :: S.HashSet LHName                                  -- ^ Data constructors used in specs
  } 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

-- | A function to resolve names in the ty parameter of Spec
--
--
emapSpecM
  :: Monad m
  =>
     -- | The bscope setting, which affects which names
     -- are considered to be in scope in refinment types.
     Bool
     -- | For names that have a local environment return the names in scope.
  -> (LHName -> [F.Symbol])
     -- | The first parameter of the function argument are the variables in scope.
  -> ([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)

-- /NOTA BENE/: These instances below are considered legacy, because merging two 'Spec's together doesn't
-- really make sense, and we provide this only for legacy purposes.
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
           }

-- $liftedSpec

-- | A 'LiftedSpec' is derived from an input 'BareSpec' and a set of its dependencies.
-- The general motivations for lifting a spec are (a) name resolution, (b) the fact that some info is
-- only relevant for checking the body of functions but does not need to be exported, e.g.
-- termination measures, or the fact that a type signature was assumed.
-- A 'LiftedSpec' is /what we serialise on disk and what the clients should will be using/.
--
-- What we /do not/ have compared to a 'BareSpec':
--
-- * The 'reflSigs', they are now just \"normal\" signatures;
-- * The 'lazy', we don't do termination checking in lifted specs;
-- * The 'reflects', the reflection has already happened at this point;
-- * The 'hmeas', we have /already/ turned these into measures at this point;
-- * The 'inlines', ditto as 'hmeas';
-- * The 'ignores', ditto as 'hmeas';
-- * The 'pragmas', we can't make any use of this information for lifted specs;
-- * The 'termexprs', we don't do termination checking in lifted specs;
--
-- Apart from less fields, a 'LiftedSpec' /replaces all instances of lists with sets/, to enforce
-- duplicate detection and removal on what we serialise on disk.
data LiftedSpec = LiftedSpec
  { -- | Measures (a.k.a.  user-defined properties for ADTs)
    --
    -- The key of the HashMap is the unqualified name of the measure.
    -- Constructing such a map discards preceding measures with the same name
    -- as later measures, which makes possible to predict which of a few
    -- conflicting measures will be exported.
    --
    -- Tested in MeasureOverlapC.hs
    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)
    -- ^ Exported logic symbols originated from reflecting functions
  , LiftedSpec -> HashSet LocSymbol
liftedPrivateReflects :: HashSet F.LocSymbol
    -- ^ Private functions that have been reflected
  , LiftedSpec -> HashSet (Located LHName, Located (BareTypeV LHName))
liftedAsmSigs    :: HashSet (F.Located LHName, LocBareTypeLHName)
    -- ^ Assumed (unchecked) types; including reflected signatures
  , LiftedSpec -> HashSet (Located LHName, Located (BareTypeV LHName))
liftedSigs       :: HashSet (F.Located LHName, LocBareTypeLHName)
    -- ^ Asserted spec signatures
  , LiftedSpec -> HashSet (Maybe LocSymbol, Located (BareTypeV LHName))
liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareTypeLHName)
    -- ^ Data type invariants; the Maybe is the generating measure
  , LiftedSpec
-> HashSet (Located (BareTypeV LHName), Located (BareTypeV LHName))
liftedIaliases   :: HashSet (LocBareTypeLHName, LocBareTypeLHName)
    -- ^ Data type invariants to be checked
  , LiftedSpec -> HashSet DataDeclLHName
liftedDataDecls  :: HashSet DataDeclLHName
    -- ^ Predicated data definitions
  , LiftedSpec -> HashSet DataDeclLHName
liftedNewtyDecls :: HashSet DataDeclLHName
    -- ^ Predicated new type definitions
  , LiftedSpec -> HashSet (Located (RTAlias Symbol (BareTypeV LHName)))
liftedAliases    :: HashSet (F.Located (RTAlias F.Symbol BareTypeLHName))
    -- ^ RefType aliases
  , LiftedSpec -> HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases   :: HashSet (F.Located (RTAlias F.Symbol (F.ExprV LHName)))
    -- ^ Expression aliases
  , LiftedSpec -> TCEmb (Located LHName)
liftedEmbeds     :: F.TCEmb (F.Located LHName)
    -- ^ GHC-Tycon-to-fixpoint Tycon map
  , LiftedSpec -> HashSet (QualifierV LHName)
liftedQualifiers :: HashSet (F.QualifierV LHName)
    -- ^ Qualifiers in source/spec files
  , LiftedSpec -> HashSet (Located LHName)
liftedLvars      :: HashSet (F.Located LHName)
    -- ^ Variables that should be checked in the environment they are used
  , LiftedSpec -> HashSet (Located LHName)
liftedAutois     :: S.HashSet (F.Located LHName)
    -- ^ Automatically instantiate axioms in these Functions
  , LiftedSpec -> HashSet (Located LHName)
liftedAutosize   :: HashSet (F.Located LHName)
    -- ^ Type Constructors that get automatically sizing info

    -- | Measures attached to a type-class
    --
    -- Imitates the arrangement for 'liftedMeasures'
  , 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))
    -- ^ Mappings from (measure,type) -> measure
  , LiftedSpec
-> HashSet
     (MeasureV LHName (Located (BareTypeV LHName)) (Located LHName))
liftedOmeasures  :: HashSet (MeasureV LHName LocBareTypeLHName (F.Located LHName))
    -- ^ Lifted opaque reflection measures
  , LiftedSpec -> HashSet (RClass (Located (BareTypeV LHName)))
liftedClasses    :: HashSet (RClass LocBareTypeLHName)
    -- ^ Refined Type-Classes
  , 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])
    -- ^ ? Where do these come from ?!
  , LiftedSpec -> RRBEnvV LHName (Located (BareTypeV LHName))
liftedBounds     :: RRBEnvV LHName LocBareTypeLHName
  , LiftedSpec -> HashSet (EquationV LHName)
liftedAxeqs      :: HashSet (F.EquationV LHName)
    -- ^ Equalities used for Proof-By-Evaluation
  , LiftedSpec -> HashMap Symbol (LMapV LHName)
liftedDefines    :: HashMap F.Symbol (LMapV LHName)
    -- ^ Logic aliases
  , LiftedSpec -> HashSet LHName
liftedUsedDataCons :: HashSet LHName
    -- ^ Data constructors used in specs
  } 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
  }

-- $trackingDeps

-- | The /target/ dependencies that concur to the creation of a 'TargetSpec' and a 'LiftedSpec'.
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 S.Store 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

-- | Drop the given 'StableModule' from the dependencies.
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)

-- $predicates

-- | Returns 'True' if the input 'Var' is a /PLE/ one.
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))

-- | Returns 'True' if the input 'Var' was exported in the module the input 'TargetSrc' represents.
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

--
-- $legacyDataStructures
--
{-
data GhcInfo = GI
  { _giSrc       :: !GhcSrc
  , _giSpec      :: !GhcSpec               -- ^ All specification information for module
  }
-}

data GhcSrc = Src
  { GhcSrc -> String
_giTarget    :: !FilePath              -- ^ Source file for module
  , GhcSrc -> ModName
_giTargetMod :: !ModName               -- ^ Name for module
  , GhcSrc -> [CoreBind]
_giCbs       :: ![CoreBind]            -- ^ Source Code
  , GhcSrc -> [TyCon]
_gsTcs       :: ![TyCon]               -- ^ All used Type constructors
  , GhcSrc -> Maybe [ClsInst]
_gsCls       :: !(Maybe [ClsInst])     -- ^ Class instances?
  , GhcSrc -> HashSet Var
_giDerVars   :: !(S.HashSet Var)       -- ^ Binders created by GHC eg dictionaries
  , GhcSrc -> [Var]
_giImpVars   :: ![Var]                 -- ^ Binders that are _read_ in module (but not defined?)
  , GhcSrc -> [Var]
_giDefVars   :: ![Var]                 -- ^ (Top-level) binders that are _defined_ in module
  , GhcSrc -> [Var]
_giUseVars   :: ![Var]                 -- ^ Binders that are _read_ in module
  , GhcSrc -> HashSet StableName
_gsExports   :: !(HashSet StableName)  -- ^ `Name`s exported by the module being verified
  , GhcSrc -> [TyCon]
_gsFiTcs     :: ![TyCon]               -- ^ Family instance TyCons
  , GhcSrc -> [(Symbol, DataCon)]
_gsFiDcs     :: ![(F.Symbol, DataCon)] -- ^ Family instance DataCons
  , GhcSrc -> [TyCon]
_gsPrimTcs   :: ![TyCon]               -- ^ Primitive GHC TyCons (from TysPrim.primTyCons)
  }

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)]  -- ^ Imported Environment
  , GhcSpec -> Config
_gsConfig :: !Config
  , GhcSpec -> BareSpec
_gsLSpec  :: !(Spec F.Symbol BareType) -- ^ Lifted specification for the target module
  }

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
  }

-- This is a temporary internal function that we use to convert the input dependencies into a format
-- suitable for 'makeGhcSpec'.
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
  }