{-# LANGUAGE DeriveAnyClass #-}
-- | This module contains the top-level structures that hold
--   information about specifications.

{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingVia                #-}

{-# 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(..)
  -- * LiftedSpec
  -- $liftedSpec
  , LiftedSpec(..)
  -- * Tracking dependencies
  -- $trackingDeps
  , TargetDependencies(..)
  , dropDependency
  -- * Predicates on spec types
  -- $predicates
  , isPLEVar
  , isExportedVar
  -- * Other types
  , QImports(..)
  , Spec(..)
  , GhcSpecVars(..)
  , GhcSpecSig(..)
  , GhcSpecNames(..)
  , GhcSpecTerm(..)
  , GhcSpecRefl(..)
  , GhcSpecLaws(..)
  , GhcSpecData(..)
  , GhcSpecQual(..)
  , BareDef
  , BareMeasure
  , SpecMeasure
  , VarOrLocSymbol
  , LawInstance(..)
  -- * Legacy data structures
  -- $legacyDataStructures
  , GhcSrc(..)
  , GhcSpec(..)
  -- * Provisional compatibility exports & optics
  -- $provisionalBackCompat
  , toTargetSrc
  , fromTargetSrc
  , toTargetSpec
  , toBareSpec
  , fromBareSpec
  , toLiftedSpec
  , unsafeFromLiftedSpec
  , emptyLiftedSpec
  ) where

import           GHC.Generics            hiding (to, moduleName)
import           Data.Binary
import qualified Language.Fixpoint.Types as F
import           Language.Fixpoint.Misc (sortNub)
import           Data.Hashable
import qualified Data.HashSet            as S
import           Data.HashSet            (HashSet)
import qualified Data.HashMap.Strict     as M
import           Data.HashMap.Strict     (HashMap)
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Generics
import           Language.Haskell.Liquid.Types.Variance
import           Language.Haskell.Liquid.Types.Bounds
import           Liquid.GHC.API hiding (text, (<+>))
import           Language.Haskell.Liquid.GHC.Types
import           Text.PrettyPrint.HughesPJ              (text, (<+>))
import           Text.PrettyPrint.HughesPJ as HughesPJ (($$))


{- $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 = forall t. HasConfig t => t -> Config
getConfig 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 -> FilePath
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)
  , TargetSrc -> QImports
gsQualImps  :: !QImports              -- ^ Map of qualified imports
  , TargetSrc -> HashSet Symbol
gsAllImps   :: !(HashSet F.Symbol)    -- ^ Set of _all_ imported modules
  , TargetSrc -> [TyThing]
gsTyThings  :: ![TyThing]             -- ^ All the @TyThing@s known to GHC
  }

-- | '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 -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [QImports] -> ShowS
$cshowList :: [QImports] -> ShowS
show :: QImports -> FilePath
$cshow :: QImports -> FilePath
showsPrec :: Int -> QImports -> ShowS
$cshowsPrec :: Int -> 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 -> GhcSpecLaws
gsLaws   :: !GhcSpecLaws
  , TargetSpec -> [(Symbol, Sort)]
gsImps   :: ![(F.Symbol, F.Sort)]  -- ^ Imported Environment
  , TargetSpec -> Config
gsConfig :: !Config
  }

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
  }

instance Semigroup GhcSpecVars where
  GhcSpecVars
sv1 <> :: GhcSpecVars -> GhcSpecVars -> GhcSpecVars
<> GhcSpecVars
sv2 = SpVar
    { gsTgtVars :: [Var]
gsTgtVars    = GhcSpecVars -> [Var]
gsTgtVars    GhcSpecVars
sv1 forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> [Var]
gsTgtVars    GhcSpecVars
sv2
    , gsIgnoreVars :: HashSet Var
gsIgnoreVars = GhcSpecVars -> HashSet Var
gsIgnoreVars GhcSpecVars
sv1 forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> HashSet Var
gsIgnoreVars GhcSpecVars
sv2
    , gsLvars :: HashSet Var
gsLvars      = GhcSpecVars -> HashSet Var
gsLvars      GhcSpecVars
sv1 forall a. Semigroup a => a -> a -> a
<> GhcSpecVars -> HashSet Var
gsLvars      GhcSpecVars
sv2
    , gsCMethods :: [Var]
gsCMethods   = GhcSpecVars -> [Var]
gsCMethods   GhcSpecVars
sv1 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 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty 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)
  }

data GhcSpecSig = SpSig
  { GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs   :: ![(Var, LocSpecType)]           -- ^ Asserted Reftypes
  , GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs  :: ![(Var, LocSpecType)]           -- ^ Assumed Reftypes
  , 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)]
  }

instance Semigroup GhcSpecSig where
  GhcSpecSig
x <> :: GhcSpecSig -> GhcSpecSig -> GhcSpecSig
<> GhcSpecSig
y = SpSig
    { gsTySigs :: [(Var, LocSpecType)]
gsTySigs   = GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
x   forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
y
    , gsAsmSigs :: [(Var, LocSpecType)]
gsAsmSigs  = GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
x  forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs GhcSpecSig
y
    , gsRefSigs :: [(Var, LocSpecType)]
gsRefSigs  = GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
x  forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs GhcSpecSig
y
    , gsInSigs :: [(Var, LocSpecType)]
gsInSigs   = GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
x   forall a. Semigroup a => a -> a -> a
<> GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs GhcSpecSig
y
    , gsNewTypes :: [(TyCon, LocSpecType)]
gsNewTypes = GhcSpecSig -> [(TyCon, LocSpecType)]
gsNewTypes GhcSpecSig
x 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    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  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   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 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   forall a. Semigroup a => a -> a -> a
<> GhcSpecSig
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel GhcSpecSig
y
    }







instance Monoid GhcSpecSig where
  mempty :: GhcSpecSig
mempty = [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(TyCon, LocSpecType)]
-> DEnv Var LocSpecType
-> [(Var, MethodType LocSpecType)]
-> [(Var, LocSpecType, [Located Expr])]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> [(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
-> GhcSpecSig
SpSig forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty 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 SpecType DataCon]
gsMeasures   :: ![Measure SpecType DataCon]   -- ^ Measure definitions
  , GhcSpecData -> [UnSortedExpr]
gsUnsorted   :: ![UnSortedExpr]
  }
data GhcSpecNames = SpNames
  { GhcSpecNames -> [(Symbol, Var)]
gsFreeSyms   :: ![(F.Symbol, Var)]            -- ^ List of `Symbol` free in spec and corresponding GHC var, eg. (Cons, Cons#7uz) from tests/pos/ex1.hs
  , 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" from include/Data/Set.spec
  , GhcSpecNames -> [DataDecl]
gsADTs       :: ![F.DataDecl]                 -- ^ ADTs extracted from Haskell 'data' definitions
  , GhcSpecNames -> TyConMap
gsTyconEnv   :: !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
  }

instance Semigroup GhcSpecTerm where
  GhcSpecTerm
t1 <> :: GhcSpecTerm -> GhcSpecTerm -> GhcSpecTerm
<> GhcSpecTerm
t2 = SpTerm
    { gsStTerm :: HashSet Var
gsStTerm    = GhcSpecTerm -> HashSet Var
gsStTerm GhcSpecTerm
t1    forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet Var
gsStTerm GhcSpecTerm
t2
    , gsAutosize :: HashSet TyCon
gsAutosize  = GhcSpecTerm -> HashSet TyCon
gsAutosize GhcSpecTerm
t1  forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet TyCon
gsAutosize GhcSpecTerm
t2
    , gsLazy :: HashSet Var
gsLazy      = GhcSpecTerm -> HashSet Var
gsLazy GhcSpecTerm
t1      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      forall a. Semigroup a => a -> a -> a
<> GhcSpecTerm -> HashSet (Located Var)
gsFail GhcSpecTerm
t2
    , gsNonStTerm :: HashSet Var
gsNonStTerm = GhcSpecTerm -> HashSet Var
gsNonStTerm GhcSpecTerm
t1 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 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
data GhcSpecRefl = SpRefl
  { GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst     :: !(M.HashMap Var (Maybe Int))      -- ^ 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 -> [Var]
gsWiredReft    :: ![Var]
  , GhcSpecRefl -> HashSet (Located Var)
gsRewrites     :: S.HashSet (F.Located Var)
  , GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith :: M.HashMap Var [Var]
  }

instance Semigroup GhcSpecRefl where
  GhcSpecRefl
x <> :: GhcSpecRefl -> GhcSpecRefl -> GhcSpecRefl
<> GhcSpecRefl
y = SpRefl
    { gsAutoInst :: HashMap Var (Maybe Int)
gsAutoInst = GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst GhcSpecRefl
y
    , gsHAxioms :: [(Var, LocSpecType, Equation)]
gsHAxioms  = GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [(Var, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
y
    , gsImpAxioms :: [Equation]
gsImpAxioms = GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Equation]
gsImpAxioms GhcSpecRefl
y
    , gsMyAxioms :: [Equation]
gsMyAxioms = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
y
    , gsReflects :: [Var]
gsReflects = GhcSpecRefl -> [Var]
gsReflects GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Var]
gsReflects GhcSpecRefl
y
    , gsLogicMap :: LogicMap
gsLogicMap = GhcSpecRefl -> LogicMap
gsLogicMap GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> LogicMap
gsLogicMap GhcSpecRefl
y
    , gsWiredReft :: [Var]
gsWiredReft = GhcSpecRefl -> [Var]
gsWiredReft GhcSpecRefl
x forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> [Var]
gsWiredReft GhcSpecRefl
y
    , gsRewrites :: HashSet (Located Var)
gsRewrites = GhcSpecRefl -> HashSet (Located Var)
gsRewrites GhcSpecRefl
x 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 forall a. Semigroup a => a -> a -> a
<> GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith GhcSpecRefl
y
    }

instance Monoid GhcSpecRefl where
  mempty :: GhcSpecRefl
mempty = HashMap Var (Maybe Int)
-> [(Var, LocSpecType, Equation)]
-> [Equation]
-> [Equation]
-> [Var]
-> LogicMap
-> [Var]
-> HashSet (Located Var)
-> HashMap Var [Var]
-> GhcSpecRefl
SpRefl forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
                  forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
                  forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
data GhcSpecLaws = SpLaws
  { GhcSpecLaws -> [(Class, [(Var, LocSpecType)])]
gsLawDefs :: ![(Class, [(Var, LocSpecType)])]
  , GhcSpecLaws -> [LawInstance]
gsLawInst :: ![LawInstance]
  }

data LawInstance = LawInstance
  { LawInstance -> Class
lilName   :: Class
  , LawInstance -> [LocSpecType]
liSupers  :: [LocSpecType]
  , LawInstance -> [LocSpecType]
lilTyArgs :: [LocSpecType]
  , LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus   :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
  , LawInstance -> SrcSpan
lilPos    :: SrcSpan
  }

type VarOrLocSymbol = Either Var LocSymbol
type BareMeasure   = Measure LocBareType F.LocSymbol
type BareDef       = Def     LocBareType F.LocSymbol
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.
newtype BareSpec =
  MkBareSpec { BareSpec -> Spec LocBareType LocSymbol
getBareSpec :: Spec LocBareType F.LocSymbol }
  deriving (forall x. Rep BareSpec x -> BareSpec
forall x. BareSpec -> Rep BareSpec x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BareSpec x -> BareSpec
$cfrom :: forall x. BareSpec -> Rep BareSpec x
Generic, Int -> BareSpec -> ShowS
[BareSpec] -> ShowS
BareSpec -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [BareSpec] -> ShowS
$cshowList :: [BareSpec] -> ShowS
show :: BareSpec -> FilePath
$cshow :: BareSpec -> FilePath
showsPrec :: Int -> BareSpec -> ShowS
$cshowsPrec :: Int -> BareSpec -> ShowS
Show, Get BareSpec
[BareSpec] -> Put
BareSpec -> Put
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
putList :: [BareSpec] -> Put
$cputList :: [BareSpec] -> Put
get :: Get BareSpec
$cget :: Get BareSpec
put :: BareSpec -> Put
$cput :: BareSpec -> Put
Binary)

instance Semigroup BareSpec where
  BareSpec
x <> :: BareSpec -> BareSpec -> BareSpec
<> BareSpec
y = MkBareSpec { getBareSpec :: Spec LocBareType LocSymbol
getBareSpec = BareSpec -> Spec LocBareType LocSymbol
getBareSpec BareSpec
x forall a. Semigroup a => a -> a -> a
<> BareSpec -> Spec LocBareType LocSymbol
getBareSpec BareSpec
y }

instance Monoid BareSpec where
  mempty :: BareSpec
mempty = MkBareSpec { getBareSpec :: Spec LocBareType LocSymbol
getBareSpec = forall a. Monoid a => a
mempty }


-- instance Semigroup (Spec ty bndr) where

-- | A generic 'Spec' type, polymorphic over the inner choice of type and binder.
data Spec ty bndr  = Spec
  { forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   :: ![Measure ty bndr]                                  -- ^ User-defined properties for ADTs
  , forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs    :: ![(F.Symbol, F.Sort)]                               -- ^ Imported variables types
  , forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs    :: ![(F.Symbol, F.Sort)]                               -- ^ Exported variables types
  , forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    :: ![(F.LocSymbol, ty)]                                -- ^ Assumed (unchecked) types; including reflected signatures
  , forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       :: ![(F.LocSymbol, ty)]                                -- ^ Imported functions and types
  , forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  :: ![(F.LocSymbol, ty)]                                -- ^ Local type signatures
  , forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs   :: ![(F.LocSymbol, ty)]                                -- ^ Reflected type signatures
  , forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants :: ![(Maybe F.LocSymbol, ty)]                          -- ^ Data type invariants; the Maybe is the generating measure
  , forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases   :: ![(ty, ty)]                                         -- ^ Data type invariants to be checked
  , forall ty bndr. Spec ty bndr -> [Symbol]
imports    :: ![F.Symbol]                                         -- ^ Loaded spec module names
  , forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  :: ![DataDecl]                                         -- ^ Predicated data definitions
  , forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls :: ![DataDecl]                                         -- ^ Predicated new type definitions
  , forall ty bndr. Spec ty bndr -> [FilePath]
includes   :: ![FilePath]                                         -- ^ Included qualifier files
  , forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases    :: ![F.Located (RTAlias F.Symbol BareType)]            -- ^ RefType aliases
  , forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases   :: ![F.Located (RTAlias F.Symbol F.Expr)]              -- ^ Expression aliases
  , forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds     :: !(F.TCEmb F.LocSymbol)                              -- ^ GHC-Tycon-to-fixpoint Tycon map
  , forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers :: ![F.Qualifier]                                      -- ^ Qualifiers in source/spec files
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars      :: !(S.HashSet F.LocSymbol)                            -- ^ Variables that should be checked in the environment they are used
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lazy       :: !(S.HashSet F.LocSymbol)                            -- ^ Ignore Termination Check in these Functions
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
rewrites    :: !(S.HashSet F.LocSymbol)                           -- ^ Theorems turned into rewrite rules
  , forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol])             -- ^ Definitions using rewrite rules
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
fails      :: !(S.HashSet F.LocSymbol)                            -- ^ These Functions should be unsafe
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
reflects   :: !(S.HashSet F.LocSymbol)                            -- ^ Binders to reflect
  , forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois     :: !(M.HashMap F.LocSymbol (Maybe Int))                -- ^ Automatically instantiate axioms in these Functions with maybe specified fuel
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hmeas      :: !(S.HashSet F.LocSymbol)                            -- ^ Binders to turn into measures using haskell definitions
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hbounds    :: !(S.HashSet F.LocSymbol)                            -- ^ Binders to turn into bounds using haskell definitions
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
inlines    :: !(S.HashSet F.LocSymbol)                            -- ^ Binders to turn into logic inline using haskell definitions
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
ignores    :: !(S.HashSet F.LocSymbol)                            -- ^ Binders to ignore during checking; that is DON't check the corebind.
  , forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize   :: !(S.HashSet F.LocSymbol)                            -- ^ Type Constructors that get automatically sizing info
  , forall ty bndr. Spec ty bndr -> [Located FilePath]
pragmas    :: ![F.Located String]                                 -- ^ Command-line configurations passed in through source
  , forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures  :: ![Measure ty ()]                                    -- ^ Measures attached to a type-class
  , forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures  :: ![Measure ty bndr]                                  -- ^ Mappings from (measure,type) -> measure
  , forall ty bndr. Spec ty bndr -> [RClass ty]
classes    :: ![RClass ty]                                        -- ^ Refined Type-Classes
  , forall ty bndr. Spec ty bndr -> [RClass ty]
claws      :: ![RClass ty]                                        -- ^ Refined Type-Classe Laws
  , forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)] -- ^ Relational types
  , forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel     :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)] -- ^ Assumed relational types
  , forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
termexprs  :: ![(F.LocSymbol, [F.Located F.Expr])]                -- ^ Terminating Conditions for functions
  , forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance  :: ![RInstance ty]
  , forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws      :: ![RILaws ty]
  , forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance  :: ![(F.LocSymbol, [Variance])]                        -- ^ TODO ? Where do these come from ?!
  , forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize      :: ![([ty], F.LocSymbol)]                              -- ^ Size measure to enforce fancy termination
  , forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds     :: !(RRBEnv ty)
  , forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs       :: !(M.HashMap F.LocSymbol F.Symbol)                   -- ^ Temporary (?) hack to deal with dictionaries in specifications
                                                                      --   see tests/pos/NatClass.hs
  , forall ty bndr. Spec ty bndr -> [Equation]
axeqs      :: ![F.Equation]                                       -- ^ Equalities used for Proof-By-Evaluation
  } deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ty bndr x. Rep (Spec ty bndr) x -> Spec ty bndr
forall ty bndr x. Spec ty bndr -> Rep (Spec ty bndr) x
$cto :: forall ty bndr x. Rep (Spec ty bndr) x -> Spec ty bndr
$cfrom :: forall ty bndr x. Spec ty bndr -> Rep (Spec ty bndr) x
Generic, Int -> Spec ty bndr -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Int -> Spec ty bndr -> ShowS
forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
[Spec ty bndr] -> ShowS
forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Spec ty bndr -> FilePath
showList :: [Spec ty bndr] -> ShowS
$cshowList :: forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
[Spec ty bndr] -> ShowS
show :: Spec ty bndr -> FilePath
$cshow :: forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Spec ty bndr -> FilePath
showsPrec :: Int -> Spec ty bndr -> ShowS
$cshowsPrec :: forall ty bndr.
(PPrint ty, PPrint bndr, Show ty) =>
Int -> Spec ty bndr -> ShowS
Show)

instance Binary (Spec LocBareType F.LocSymbol)

instance (Show ty, Show bndr, F.PPrint ty, F.PPrint bndr) => F.PPrint (Spec ty bndr) where
    pprintTidy :: Tidy -> Spec ty bndr -> Doc
pprintTidy Tidy
k Spec ty bndr
sp = FilePath -> Doc
text FilePath
"dataDecls = " Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k  (forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls Spec ty bndr
sp)
                         Doc -> Doc -> Doc
HughesPJ.$$
                      FilePath -> Doc
text FilePath
"classes = " Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall ty bndr. Spec ty bndr -> [RClass ty]
classes Spec ty bndr
sp)
                         Doc -> Doc -> Doc
HughesPJ.$$
                      FilePath -> Doc
text FilePath
"sigs = " Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs Spec ty bndr
sp)

-- /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 ty bndr) where
  Spec ty bndr
s1 <> :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr
<> Spec ty bndr
s2
    = Spec { measures :: [Measure ty bndr]
measures   =           forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   Spec ty bndr
s2
           , impSigs :: [(Symbol, Sort)]
impSigs    =           forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs    Spec ty bndr
s2
           , expSigs :: [(Symbol, Sort)]
expSigs    =           forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs    Spec ty bndr
s2
           , asmSigs :: [(LocSymbol, ty)]
asmSigs    =           forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    Spec ty bndr
s2
           , sigs :: [(LocSymbol, ty)]
sigs       =           forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       Spec ty bndr
s2
           , localSigs :: [(LocSymbol, ty)]
localSigs  =           forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  Spec ty bndr
s2
           , reflSigs :: [(LocSymbol, ty)]
reflSigs   =           forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs   Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs   Spec ty bndr
s2
           , invariants :: [(Maybe LocSymbol, ty)]
invariants =           forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants Spec ty bndr
s2
           , ialiases :: [(ty, ty)]
ialiases   =           forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases   Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases   Spec ty bndr
s2
           , imports :: [Symbol]
imports    = forall a. Ord a => [a] -> [a]
sortNub forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> [Symbol]
imports    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Symbol]
imports    Spec ty bndr
s2
           , dataDecls :: [DataDecl]
dataDecls  =           forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  Spec ty bndr
s2
           , newtyDecls :: [DataDecl]
newtyDecls =           forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls Spec ty bndr
s2
           , includes :: [FilePath]
includes   = forall a. Ord a => [a] -> [a]
sortNub forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> [FilePath]
includes   Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [FilePath]
includes   Spec ty bndr
s2
           , aliases :: [Located (RTAlias Symbol BareType)]
aliases    =           forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases    Spec ty bndr
s2
           , ealiases :: [Located (RTAlias Symbol Expr)]
ealiases   =           forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases   Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases   Spec ty bndr
s2
           , qualifiers :: [Qualifier]
qualifiers =           forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers Spec ty bndr
s2
           , pragmas :: [Located FilePath]
pragmas    =           forall ty bndr. Spec ty bndr -> [Located FilePath]
pragmas    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Located FilePath]
pragmas    Spec ty bndr
s2
           , cmeasures :: [Measure ty ()]
cmeasures  =           forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures  Spec ty bndr
s2
           , imeasures :: [Measure ty bndr]
imeasures  =           forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures  Spec ty bndr
s2
           , classes :: [RClass ty]
classes    =           forall ty bndr. Spec ty bndr -> [RClass ty]
classes    Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [RClass ty]
classes    Spec ty bndr
s2
           , claws :: [RClass ty]
claws      =           forall ty bndr. Spec ty bndr -> [RClass ty]
claws      Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [RClass ty]
claws      Spec ty bndr
s2
           , relational :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational =           forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational Spec ty bndr
s2
           , asmRel :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel     =           forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel     Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel     Spec ty bndr
s2
           , termexprs :: [(LocSymbol, [Located Expr])]
termexprs  =           forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
termexprs  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
termexprs  Spec ty bndr
s2
           , rinstance :: [RInstance ty]
rinstance  =           forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance  Spec ty bndr
s2
           , ilaws :: [RILaws ty]
ilaws      =               forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws      Spec ty bndr
s2
           , dvariance :: [(LocSymbol, [Variance])]
dvariance  =           forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance  Spec ty bndr
s2
           , dsize :: [([ty], LocSymbol)]
dsize      =               forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize  Spec ty bndr
s1 forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize      Spec ty bndr
s2
           , axeqs :: [Equation]
axeqs      =           forall ty bndr. Spec ty bndr -> [Equation]
axeqs Spec ty bndr
s1      forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Equation]
axeqs Spec ty bndr
s2
           , embeds :: TCEmb LocSymbol
embeds     = forall a. Monoid a => a -> a -> a
mappend   (forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds   Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds   Spec ty bndr
s2)
           , lvars :: HashSet LocSymbol
lvars      = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars    Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars    Spec ty bndr
s2)
           , lazy :: HashSet LocSymbol
lazy       = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lazy     Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lazy     Spec ty bndr
s2)
           , rewrites :: HashSet LocSymbol
rewrites   = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
rewrites    Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
rewrites    Spec ty bndr
s2)
           , rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union  (forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
rewriteWith Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
rewriteWith Spec ty bndr
s2)
           , fails :: HashSet LocSymbol
fails      = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
fails    Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
fails    Spec ty bndr
s2)
           , reflects :: HashSet LocSymbol
reflects   = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
reflects Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
reflects Spec ty bndr
s2)
           , hmeas :: HashSet LocSymbol
hmeas      = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hmeas    Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hmeas    Spec ty bndr
s2)
           , hbounds :: HashSet LocSymbol
hbounds    = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hbounds  Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
hbounds  Spec ty bndr
s2)
           , inlines :: HashSet LocSymbol
inlines    = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
inlines  Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
inlines  Spec ty bndr
s2)
           , ignores :: HashSet LocSymbol
ignores    = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
ignores  Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
ignores  Spec ty bndr
s2)
           , autosize :: HashSet LocSymbol
autosize   = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union   (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize Spec ty bndr
s2)
           , bounds :: RRBEnv ty
bounds     = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union   (forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds   Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds   Spec ty bndr
s2)
           , defs :: HashMap LocSymbol Symbol
defs       = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union   (forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs     Spec ty bndr
s1)  (forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs     Spec ty bndr
s2)
           , autois :: HashMap LocSymbol (Maybe Int)
autois     = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
M.union   (forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois Spec ty bndr
s1)      (forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois Spec ty bndr
s2)
           }

instance Monoid (Spec ty bndr) where
  mappend :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr
mappend = forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: Spec ty bndr
mempty
    = Spec { measures :: [Measure ty bndr]
measures   = []
           , impSigs :: [(Symbol, Sort)]
impSigs    = []
           , expSigs :: [(Symbol, Sort)]
expSigs    = []
           , asmSigs :: [(LocSymbol, ty)]
asmSigs    = []
           , sigs :: [(LocSymbol, ty)]
sigs       = []
           , localSigs :: [(LocSymbol, ty)]
localSigs  = []
           , reflSigs :: [(LocSymbol, ty)]
reflSigs   = []
           , invariants :: [(Maybe LocSymbol, ty)]
invariants = []
           , ialiases :: [(ty, ty)]
ialiases   = []
           , imports :: [Symbol]
imports    = []
           , dataDecls :: [DataDecl]
dataDecls  = []
           , newtyDecls :: [DataDecl]
newtyDecls = []
           , includes :: [FilePath]
includes   = []
           , aliases :: [Located (RTAlias Symbol BareType)]
aliases    = []
           , ealiases :: [Located (RTAlias Symbol Expr)]
ealiases   = []
           , embeds :: TCEmb LocSymbol
embeds     = forall a. Monoid a => a
mempty
           , qualifiers :: [Qualifier]
qualifiers = []
           , lvars :: HashSet LocSymbol
lvars      = forall a. HashSet a
S.empty
           , lazy :: HashSet LocSymbol
lazy       = forall a. HashSet a
S.empty
           , rewrites :: HashSet LocSymbol
rewrites   = forall a. HashSet a
S.empty
           , rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = forall k v. HashMap k v
M.empty
           , fails :: HashSet LocSymbol
fails      = forall a. HashSet a
S.empty
           , autois :: HashMap LocSymbol (Maybe Int)
autois     = forall k v. HashMap k v
M.empty
           , hmeas :: HashSet LocSymbol
hmeas      = forall a. HashSet a
S.empty
           , reflects :: HashSet LocSymbol
reflects   = forall a. HashSet a
S.empty
           , hbounds :: HashSet LocSymbol
hbounds    = forall a. HashSet a
S.empty
           , inlines :: HashSet LocSymbol
inlines    = forall a. HashSet a
S.empty
           , ignores :: HashSet LocSymbol
ignores    = forall a. HashSet a
S.empty
           , autosize :: HashSet LocSymbol
autosize   = forall a. HashSet a
S.empty
           , pragmas :: [Located FilePath]
pragmas    = []
           , cmeasures :: [Measure ty ()]
cmeasures  = []
           , imeasures :: [Measure ty bndr]
imeasures  = []
           , classes :: [RClass ty]
classes    = []
           , claws :: [RClass ty]
claws      = []
           , relational :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
relational = []
           , asmRel :: [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
asmRel     = []
           , termexprs :: [(LocSymbol, [Located Expr])]
termexprs  = []
           , rinstance :: [RInstance ty]
rinstance  = []
           , ilaws :: [RILaws ty]
ilaws      = []
           , dvariance :: [(LocSymbol, [Variance])]
dvariance  = []
           , dsize :: [([ty], LocSymbol)]
dsize      = []
           , axeqs :: [Equation]
axeqs      = []
           , bounds :: RRBEnv ty
bounds     = forall k v. HashMap k v
M.empty
           , defs :: HashMap LocSymbol Symbol
defs       = forall k v. HashMap k v
M.empty
           }

-- $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 'localSigs', as it's not necessary/visible to clients;
-- * The 'includes', as they are probably not reachable for clients anyway;
-- * 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 'hbounds', ditto as 'hmeas';
-- * 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
  { LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedMeasures   :: HashSet (Measure LocBareType F.LocSymbol)
    -- ^ User-defined properties for ADTs
  , LiftedSpec -> HashSet (Symbol, Sort)
liftedImpSigs    :: HashSet (F.Symbol, F.Sort)
    -- ^ Imported variables types
  , LiftedSpec -> HashSet (Symbol, Sort)
liftedExpSigs    :: HashSet (F.Symbol, F.Sort)
    -- ^ Exported variables types
  , LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedAsmSigs    :: HashSet (F.LocSymbol, LocBareType)
    -- ^ Assumed (unchecked) types; including reflected signatures
  , LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedSigs       :: HashSet (F.LocSymbol, LocBareType)
    -- ^ Imported functions and types
  , LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareType)
    -- ^ Data type invariants; the Maybe is the generating measure
  , LiftedSpec -> HashSet (LocBareType, LocBareType)
liftedIaliases   :: HashSet (LocBareType, LocBareType)
    -- ^ Data type invariants to be checked
  , LiftedSpec -> HashSet Symbol
liftedImports    :: HashSet F.Symbol
    -- ^ Loaded spec module names
  , LiftedSpec -> HashSet DataDecl
liftedDataDecls  :: HashSet DataDecl
    -- ^ Predicated data definitions
  , LiftedSpec -> HashSet DataDecl
liftedNewtyDecls :: HashSet DataDecl
    -- ^ Predicated new type definitions
  , LiftedSpec -> HashSet (Located (RTAlias Symbol BareType))
liftedAliases    :: HashSet (F.Located (RTAlias F.Symbol BareType))
    -- ^ RefType aliases
  , LiftedSpec -> HashSet (Located (RTAlias Symbol Expr))
liftedEaliases   :: HashSet (F.Located (RTAlias F.Symbol F.Expr))
    -- ^ Expression aliases
  , LiftedSpec -> TCEmb LocSymbol
liftedEmbeds     :: F.TCEmb F.LocSymbol
    -- ^ GHC-Tycon-to-fixpoint Tycon map
  , LiftedSpec -> HashSet Qualifier
liftedQualifiers :: HashSet F.Qualifier
    -- ^ Qualifiers in source/spec files
  , LiftedSpec -> HashSet LocSymbol
liftedLvars      :: HashSet F.LocSymbol
    -- ^ Variables that should be checked in the environment they are used
  , LiftedSpec -> HashMap LocSymbol (Maybe Int)
liftedAutois     :: M.HashMap F.LocSymbol (Maybe Int)
    -- ^ Automatically instantiate axioms in these Functions with maybe specified fuel
  , LiftedSpec -> HashSet LocSymbol
liftedAutosize   :: HashSet F.LocSymbol
    -- ^ Type Constructors that get automatically sizing info
  , LiftedSpec -> HashSet (Measure LocBareType ())
liftedCmeasures  :: HashSet (Measure LocBareType ())
    -- ^ Measures attached to a type-class
  , LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedImeasures  :: HashSet (Measure LocBareType F.LocSymbol)
    -- ^ Mappings from (measure,type) -> measure
  , LiftedSpec -> HashSet (RClass LocBareType)
liftedClasses    :: HashSet (RClass LocBareType)
    -- ^ Refined Type-Classes
  , LiftedSpec -> HashSet (RClass LocBareType)
liftedClaws      :: HashSet (RClass LocBareType)
    -- ^ Refined Type-Classe Laws
  , LiftedSpec -> HashSet (RInstance LocBareType)
liftedRinstance  :: HashSet (RInstance LocBareType)
  , LiftedSpec -> HashSet (RILaws LocBareType)
liftedIlaws      :: HashSet (RILaws LocBareType)
  , LiftedSpec -> [([LocBareType], LocSymbol)]
liftedDsize      :: [([LocBareType], F.LocSymbol)]
  , LiftedSpec -> HashSet (LocSymbol, [Variance])
liftedDvariance  :: HashSet (F.LocSymbol, [Variance])
    -- ^ ? Where do these come from ?!
  , LiftedSpec -> RRBEnv LocBareType
liftedBounds     :: RRBEnv LocBareType
  , LiftedSpec -> HashMap LocSymbol Symbol
liftedDefs       :: M.HashMap F.LocSymbol F.Symbol
    -- ^ Temporary (?) hack to deal with dictionaries in specifications
    --   see tests/pos/NatClass.hs
  , LiftedSpec -> HashSet Equation
liftedAxeqs      :: HashSet F.Equation
    -- ^ Equalities used for Proof-By-Evaluation
  } deriving (LiftedSpec -> LiftedSpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LiftedSpec -> LiftedSpec -> Bool
$c/= :: LiftedSpec -> LiftedSpec -> Bool
== :: LiftedSpec -> LiftedSpec -> Bool
$c== :: LiftedSpec -> LiftedSpec -> Bool
Eq, 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
$cto :: forall x. Rep LiftedSpec x -> LiftedSpec
$cfrom :: forall x. LiftedSpec -> Rep LiftedSpec x
Generic, Int -> LiftedSpec -> ShowS
[LiftedSpec] -> ShowS
LiftedSpec -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LiftedSpec] -> ShowS
$cshowList :: [LiftedSpec] -> ShowS
show :: LiftedSpec -> FilePath
$cshow :: LiftedSpec -> FilePath
showsPrec :: Int -> LiftedSpec -> ShowS
$cshowsPrec :: Int -> LiftedSpec -> ShowS
Show)
    deriving Eq LiftedSpec
Int -> LiftedSpec -> Int
LiftedSpec -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: LiftedSpec -> Int
$chash :: LiftedSpec -> Int
hashWithSalt :: Int -> LiftedSpec -> Int
$chashWithSalt :: Int -> LiftedSpec -> Int
Hashable via Generically LiftedSpec
    deriving Get LiftedSpec
[LiftedSpec] -> Put
LiftedSpec -> Put
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
putList :: [LiftedSpec] -> Put
$cputList :: [LiftedSpec] -> Put
get :: Get LiftedSpec
$cget :: Get LiftedSpec
put :: LiftedSpec -> Put
$cput :: LiftedSpec -> Put
Binary   via Generically LiftedSpec

instance Binary F.Equation

emptyLiftedSpec :: LiftedSpec
emptyLiftedSpec :: LiftedSpec
emptyLiftedSpec = LiftedSpec
  { liftedMeasures :: HashSet (Measure LocBareType LocSymbol)
liftedMeasures = forall a. Monoid a => a
mempty
  , liftedImpSigs :: HashSet (Symbol, Sort)
liftedImpSigs  = forall a. Monoid a => a
mempty
  , liftedExpSigs :: HashSet (Symbol, Sort)
liftedExpSigs  = forall a. Monoid a => a
mempty
  , liftedAsmSigs :: HashSet (LocSymbol, LocBareType)
liftedAsmSigs  = forall a. Monoid a => a
mempty
  , liftedSigs :: HashSet (LocSymbol, LocBareType)
liftedSigs     = forall a. Monoid a => a
mempty
  , liftedInvariants :: HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants = forall a. Monoid a => a
mempty
  , liftedIaliases :: HashSet (LocBareType, LocBareType)
liftedIaliases   = forall a. Monoid a => a
mempty
  , liftedImports :: HashSet Symbol
liftedImports    = forall a. Monoid a => a
mempty
  , liftedDataDecls :: HashSet DataDecl
liftedDataDecls  = forall a. Monoid a => a
mempty
  , liftedNewtyDecls :: HashSet DataDecl
liftedNewtyDecls = forall a. Monoid a => a
mempty
  , liftedAliases :: HashSet (Located (RTAlias Symbol BareType))
liftedAliases    = forall a. Monoid a => a
mempty
  , liftedEaliases :: HashSet (Located (RTAlias Symbol Expr))
liftedEaliases   = forall a. Monoid a => a
mempty
  , liftedEmbeds :: TCEmb LocSymbol
liftedEmbeds     = forall a. Monoid a => a
mempty
  , liftedQualifiers :: HashSet Qualifier
liftedQualifiers = forall a. Monoid a => a
mempty
  , liftedLvars :: HashSet LocSymbol
liftedLvars      = forall a. Monoid a => a
mempty
  , liftedAutois :: HashMap LocSymbol (Maybe Int)
liftedAutois     = forall a. Monoid a => a
mempty
  , liftedAutosize :: HashSet LocSymbol
liftedAutosize   = forall a. Monoid a => a
mempty
  , liftedCmeasures :: HashSet (Measure LocBareType ())
liftedCmeasures  = forall a. Monoid a => a
mempty
  , liftedImeasures :: HashSet (Measure LocBareType LocSymbol)
liftedImeasures  = forall a. Monoid a => a
mempty
  , liftedClasses :: HashSet (RClass LocBareType)
liftedClasses    = forall a. Monoid a => a
mempty
  , liftedClaws :: HashSet (RClass LocBareType)
liftedClaws      = forall a. Monoid a => a
mempty
  , liftedRinstance :: HashSet (RInstance LocBareType)
liftedRinstance  = forall a. Monoid a => a
mempty
  , liftedIlaws :: HashSet (RILaws LocBareType)
liftedIlaws      = forall a. Monoid a => a
mempty
  , liftedDvariance :: HashSet (LocSymbol, [Variance])
liftedDvariance  = forall a. Monoid a => a
mempty
  , liftedDsize :: [([LocBareType], LocSymbol)]
liftedDsize      = forall a. Monoid a => a
mempty
  , liftedBounds :: RRBEnv LocBareType
liftedBounds     = forall a. Monoid a => a
mempty
  , liftedDefs :: HashMap LocSymbol Symbol
liftedDefs       = forall a. Monoid a => a
mempty
  , liftedAxeqs :: HashSet Equation
liftedAxeqs      = 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 (TargetDependencies -> TargetDependencies -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TargetDependencies -> TargetDependencies -> Bool
$c/= :: TargetDependencies -> TargetDependencies -> Bool
== :: TargetDependencies -> TargetDependencies -> Bool
$c== :: TargetDependencies -> TargetDependencies -> Bool
Eq, Int -> TargetDependencies -> ShowS
[TargetDependencies] -> ShowS
TargetDependencies -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [TargetDependencies] -> ShowS
$cshowList :: [TargetDependencies] -> ShowS
show :: TargetDependencies -> FilePath
$cshow :: TargetDependencies -> FilePath
showsPrec :: Int -> TargetDependencies -> ShowS
$cshowsPrec :: Int -> TargetDependencies -> ShowS
Show, 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
$cto :: forall x. Rep TargetDependencies x -> TargetDependencies
$cfrom :: forall x. TargetDependencies -> Rep TargetDependencies x
Generic)
  deriving Get TargetDependencies
[TargetDependencies] -> Put
TargetDependencies -> Put
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
putList :: [TargetDependencies] -> Put
$cputList :: [TargetDependencies] -> Put
get :: Get TargetDependencies
$cget :: Get TargetDependencies
put :: TargetDependencies -> Put
$cput :: 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 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 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 (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 = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Var
x (GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst (TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp))

-- | 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 forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet StableName
ns
  where
    n :: Name
n                = 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 -> FilePath
_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)
  , GhcSrc -> QImports
_gsQualImps  :: !QImports              -- ^ Map of qualified imports
  , GhcSrc -> HashSet Symbol
_gsAllImps   :: !(S.HashSet F.Symbol)  -- ^ Set of _all_ imported modules
  , GhcSrc -> [TyThing]
_gsTyThings  :: ![TyThing]             -- ^ All the @TyThing@s known to GHC
  }

data GhcSpec = SP
  { GhcSpec -> GhcSpecSig
_gsSig    :: !GhcSpecSig
  , GhcSpec -> GhcSpecQual
_gsQual   :: !GhcSpecQual
  , GhcSpec -> GhcSpecData
_gsData   :: !GhcSpecData
  , GhcSpec -> GhcSpecNames
_gsName   :: !GhcSpecNames
  , GhcSpec -> GhcSpecVars
_gsVars   :: !GhcSpecVars
  , GhcSpec -> GhcSpecTerm
_gsTerm   :: !GhcSpecTerm
  , GhcSpec -> GhcSpecRefl
_gsRefl   :: !GhcSpecRefl
  , GhcSpec -> GhcSpecLaws
_gsLaws   :: !GhcSpecLaws
  , GhcSpec -> [(Symbol, Sort)]
_gsImps   :: ![(F.Symbol, F.Sort)]  -- ^ Imported Environment
  , GhcSpec -> Config
_gsConfig :: !Config
  , GhcSpec -> Spec LocBareType LocSymbol
_gsLSpec  :: !(Spec LocBareType F.LocSymbol) -- ^ 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 :: FilePath
giTarget    = GhcSrc -> FilePath
_giTarget GhcSrc
a
  , giTargetMod :: ModName
giTargetMod = GhcSrc -> ModName
_giTargetMod GhcSrc
a
  , giCbs :: [CoreBind]
giCbs       = GhcSrc -> [CoreBind]
_giCbs GhcSrc
a
  , gsTcs :: [TyCon]
gsTcs       = GhcSrc -> [TyCon]
_gsTcs GhcSrc
a
  , gsCls :: Maybe [ClsInst]
gsCls       = GhcSrc -> Maybe [ClsInst]
_gsCls GhcSrc
a
  , giDerVars :: HashSet Var
giDerVars   = GhcSrc -> HashSet Var
_giDerVars GhcSrc
a
  , giImpVars :: [Var]
giImpVars   = GhcSrc -> [Var]
_giImpVars GhcSrc
a
  , giDefVars :: [Var]
giDefVars   = GhcSrc -> [Var]
_giDefVars GhcSrc
a
  , giUseVars :: [Var]
giUseVars   = GhcSrc -> [Var]
_giUseVars GhcSrc
a
  , gsExports :: HashSet StableName
gsExports   = GhcSrc -> HashSet StableName
_gsExports GhcSrc
a
  , gsFiTcs :: [TyCon]
gsFiTcs     = GhcSrc -> [TyCon]
_gsFiTcs GhcSrc
a
  , gsFiDcs :: [(Symbol, DataCon)]
gsFiDcs     = GhcSrc -> [(Symbol, DataCon)]
_gsFiDcs GhcSrc
a
  , gsPrimTcs :: [TyCon]
gsPrimTcs   = GhcSrc -> [TyCon]
_gsPrimTcs GhcSrc
a
  , gsQualImps :: QImports
gsQualImps  = GhcSrc -> QImports
_gsQualImps GhcSrc
a
  , gsAllImps :: HashSet Symbol
gsAllImps   = GhcSrc -> HashSet Symbol
_gsAllImps GhcSrc
a
  , gsTyThings :: [TyThing]
gsTyThings  = GhcSrc -> [TyThing]
_gsTyThings GhcSrc
a
  }

fromTargetSrc :: TargetSrc -> GhcSrc
fromTargetSrc :: TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
a = Src
  { _giTarget :: FilePath
_giTarget    = TargetSrc -> FilePath
giTarget TargetSrc
a
  , _giTargetMod :: ModName
_giTargetMod = TargetSrc -> ModName
giTargetMod TargetSrc
a
  , _giCbs :: [CoreBind]
_giCbs       = TargetSrc -> [CoreBind]
giCbs TargetSrc
a
  , _gsTcs :: [TyCon]
_gsTcs       = TargetSrc -> [TyCon]
gsTcs TargetSrc
a
  , _gsCls :: Maybe [ClsInst]
_gsCls       = TargetSrc -> Maybe [ClsInst]
gsCls TargetSrc
a
  , _giDerVars :: HashSet Var
_giDerVars   = TargetSrc -> HashSet Var
giDerVars TargetSrc
a
  , _giImpVars :: [Var]
_giImpVars   = TargetSrc -> [Var]
giImpVars TargetSrc
a
  , _giDefVars :: [Var]
_giDefVars   = TargetSrc -> [Var]
giDefVars TargetSrc
a
  , _giUseVars :: [Var]
_giUseVars   = TargetSrc -> [Var]
giUseVars TargetSrc
a
  , _gsExports :: HashSet StableName
_gsExports   = TargetSrc -> HashSet StableName
gsExports TargetSrc
a
  , _gsFiTcs :: [TyCon]
_gsFiTcs     = TargetSrc -> [TyCon]
gsFiTcs TargetSrc
a
  , _gsFiDcs :: [(Symbol, DataCon)]
_gsFiDcs     = TargetSrc -> [(Symbol, DataCon)]
gsFiDcs TargetSrc
a
  , _gsPrimTcs :: [TyCon]
_gsPrimTcs   = TargetSrc -> [TyCon]
gsPrimTcs TargetSrc
a
  , _gsQualImps :: QImports
_gsQualImps  = TargetSrc -> QImports
gsQualImps TargetSrc
a
  , _gsAllImps :: HashSet Symbol
_gsAllImps   = TargetSrc -> HashSet Symbol
gsAllImps TargetSrc
a
  , _gsTyThings :: [TyThing]
_gsTyThings  = TargetSrc -> [TyThing]
gsTyThings TargetSrc
a
  }

toTargetSpec :: GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec :: GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec GhcSpec
ghcSpec =
  (TargetSpec
targetSpec, (Spec LocBareType LocSymbol -> LiftedSpec
toLiftedSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec -> Spec LocBareType LocSymbol
_gsLSpec) GhcSpec
ghcSpec)
  where
    targetSpec :: TargetSpec
targetSpec = TargetSpec
      { gsSig :: GhcSpecSig
gsSig    = GhcSpec -> GhcSpecSig
_gsSig GhcSpec
ghcSpec
      , gsQual :: GhcSpecQual
gsQual   = GhcSpec -> GhcSpecQual
_gsQual GhcSpec
ghcSpec
      , gsData :: GhcSpecData
gsData   = GhcSpec -> GhcSpecData
_gsData GhcSpec
ghcSpec
      , gsName :: GhcSpecNames
gsName   = GhcSpec -> GhcSpecNames
_gsName GhcSpec
ghcSpec
      , gsVars :: GhcSpecVars
gsVars   = GhcSpec -> GhcSpecVars
_gsVars GhcSpec
ghcSpec
      , gsTerm :: GhcSpecTerm
gsTerm   = GhcSpec -> GhcSpecTerm
_gsTerm GhcSpec
ghcSpec
      , gsRefl :: GhcSpecRefl
gsRefl   = GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
ghcSpec
      , gsLaws :: GhcSpecLaws
gsLaws   = GhcSpec -> GhcSpecLaws
_gsLaws GhcSpec
ghcSpec
      , gsImps :: [(Symbol, Sort)]
gsImps   = GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
ghcSpec
      , gsConfig :: Config
gsConfig = GhcSpec -> Config
_gsConfig GhcSpec
ghcSpec
      }

toBareSpec :: Spec LocBareType F.LocSymbol -> BareSpec
toBareSpec :: Spec LocBareType LocSymbol -> BareSpec
toBareSpec = Spec LocBareType LocSymbol -> BareSpec
MkBareSpec

fromBareSpec :: BareSpec -> Spec LocBareType F.LocSymbol
fromBareSpec :: BareSpec -> Spec LocBareType LocSymbol
fromBareSpec = BareSpec -> Spec LocBareType LocSymbol
getBareSpec

toLiftedSpec :: Spec LocBareType F.LocSymbol -> LiftedSpec
toLiftedSpec :: Spec LocBareType LocSymbol -> LiftedSpec
toLiftedSpec Spec LocBareType LocSymbol
a = LiftedSpec
  { liftedMeasures :: HashSet (Measure LocBareType LocSymbol)
liftedMeasures   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedImpSigs :: HashSet (Symbol, Sort)
liftedImpSigs    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
impSigs  forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedExpSigs :: HashSet (Symbol, Sort)
liftedExpSigs    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs  forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedAsmSigs :: HashSet (LocSymbol, LocBareType)
liftedAsmSigs    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs  forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedSigs :: HashSet (LocSymbol, LocBareType)
liftedSigs       = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs     forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedInvariants :: HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
invariants forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedIaliases :: HashSet (LocBareType, LocBareType)
liftedIaliases   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedImports :: HashSet Symbol
liftedImports    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Symbol]
imports forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedDataDecls :: HashSet DataDecl
liftedDataDecls  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedNewtyDecls :: HashSet DataDecl
liftedNewtyDecls = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedAliases :: HashSet (Located (RTAlias Symbol BareType))
liftedAliases    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
aliases forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedEaliases :: HashSet (Located (RTAlias Symbol Expr))
liftedEaliases   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
ealiases forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedEmbeds :: TCEmb LocSymbol
liftedEmbeds     = forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
embeds Spec LocBareType LocSymbol
a
  , liftedQualifiers :: HashSet Qualifier
liftedQualifiers = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Qualifier]
qualifiers forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedLvars :: HashSet LocSymbol
liftedLvars      = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
lvars Spec LocBareType LocSymbol
a
  , liftedAutois :: HashMap LocSymbol (Maybe Int)
liftedAutois     = forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
autois Spec LocBareType LocSymbol
a
  , liftedAutosize :: HashSet LocSymbol
liftedAutosize   = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
autosize Spec LocBareType LocSymbol
a
  , liftedCmeasures :: HashSet (Measure LocBareType ())
liftedCmeasures  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedImeasures :: HashSet (Measure LocBareType LocSymbol)
liftedImeasures  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedClasses :: HashSet (RClass LocBareType)
liftedClasses    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [RClass ty]
classes forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedClaws :: HashSet (RClass LocBareType)
liftedClaws      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [RClass ty]
claws forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedRinstance :: HashSet (RInstance LocBareType)
liftedRinstance  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [RInstance ty]
rinstance forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedIlaws :: HashSet (RILaws LocBareType)
liftedIlaws      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [RILaws ty]
ilaws forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedDvariance :: HashSet (LocSymbol, [Variance])
liftedDvariance  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
dvariance forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  , liftedDsize :: [([LocBareType], LocSymbol)]
liftedDsize      = forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
dsize Spec LocBareType LocSymbol
a
  , liftedBounds :: RRBEnv LocBareType
liftedBounds     = forall ty bndr. Spec ty bndr -> RRBEnv ty
bounds Spec LocBareType LocSymbol
a
  , liftedDefs :: HashMap LocSymbol Symbol
liftedDefs       = forall ty bndr. Spec ty bndr -> HashMap LocSymbol Symbol
defs Spec LocBareType LocSymbol
a
  , liftedAxeqs :: HashSet Equation
liftedAxeqs      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty bndr. Spec ty bndr -> [Equation]
axeqs forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol
a
  }

-- This is a temporary internal function that we use to convert the input dependencies into a format
-- suitable for 'makeGhcSpec'.
unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType F.LocSymbol
unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType LocSymbol
unsafeFromLiftedSpec LiftedSpec
a = Spec
  { measures :: [Measure LocBareType LocSymbol]
measures   = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedMeasures forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , impSigs :: [(Symbol, Sort)]
impSigs    = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Symbol, Sort)
liftedImpSigs forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , expSigs :: [(Symbol, Sort)]
expSigs    = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Symbol, Sort)
liftedExpSigs forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs    = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedAsmSigs forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , sigs :: [(LocSymbol, LocBareType)]
sigs       = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedSigs forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , localSigs :: [(LocSymbol, LocBareType)]
localSigs  = forall a. Monoid a => a
mempty
  , reflSigs :: [(LocSymbol, LocBareType)]
reflSigs   = forall a. Monoid a => a
mempty
  , relational :: [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
  RelExpr)]
relational = forall a. Monoid a => a
mempty
  , asmRel :: [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
  RelExpr)]
asmRel     = forall a. Monoid a => a
mempty
  , invariants :: [(Maybe LocSymbol, LocBareType)]
invariants = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , ialiases :: [(LocBareType, LocBareType)]
ialiases   = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocBareType, LocBareType)
liftedIaliases forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , imports :: [Symbol]
imports    = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Symbol
liftedImports forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , dataDecls :: [DataDecl]
dataDecls  = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDecl
liftedDataDecls forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , newtyDecls :: [DataDecl]
newtyDecls = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDecl
liftedNewtyDecls forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , includes :: [FilePath]
includes   = forall a. Monoid a => a
mempty
  , aliases :: [Located (RTAlias Symbol BareType)]
aliases    = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol BareType))
liftedAliases forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , ealiases :: [Located (RTAlias Symbol Expr)]
ealiases   = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol Expr))
liftedEaliases forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , embeds :: TCEmb LocSymbol
embeds     = LiftedSpec -> TCEmb LocSymbol
liftedEmbeds LiftedSpec
a
  , qualifiers :: [Qualifier]
qualifiers = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Qualifier
liftedQualifiers forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , lvars :: HashSet LocSymbol
lvars      = LiftedSpec -> HashSet LocSymbol
liftedLvars LiftedSpec
a
  , lazy :: HashSet LocSymbol
lazy       = forall a. Monoid a => a
mempty
  , fails :: HashSet LocSymbol
fails      = forall a. Monoid a => a
mempty
  , rewrites :: HashSet LocSymbol
rewrites   = forall a. Monoid a => a
mempty
  , rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = forall a. Monoid a => a
mempty
  , reflects :: HashSet LocSymbol
reflects   = forall a. Monoid a => a
mempty
  , autois :: HashMap LocSymbol (Maybe Int)
autois     = LiftedSpec -> HashMap LocSymbol (Maybe Int)
liftedAutois LiftedSpec
a
  , hmeas :: HashSet LocSymbol
hmeas      = forall a. Monoid a => a
mempty
  , hbounds :: HashSet LocSymbol
hbounds    = forall a. Monoid a => a
mempty
  , inlines :: HashSet LocSymbol
inlines    = forall a. Monoid a => a
mempty
  , ignores :: HashSet LocSymbol
ignores    = forall a. Monoid a => a
mempty
  , autosize :: HashSet LocSymbol
autosize   = LiftedSpec -> HashSet LocSymbol
liftedAutosize LiftedSpec
a
  , pragmas :: [Located FilePath]
pragmas    = forall a. Monoid a => a
mempty
  , cmeasures :: [Measure LocBareType ()]
cmeasures  = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType ())
liftedCmeasures forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , imeasures :: [Measure LocBareType LocSymbol]
imeasures  = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedImeasures forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , classes :: [RClass LocBareType]
classes    = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass LocBareType)
liftedClasses forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , claws :: [RClass LocBareType]
claws      = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass LocBareType)
liftedClaws forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , termexprs :: [(LocSymbol, [Located Expr])]
termexprs  = forall a. Monoid a => a
mempty
  , rinstance :: [RInstance LocBareType]
rinstance  = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RInstance LocBareType)
liftedRinstance forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , ilaws :: [RILaws LocBareType]
ilaws      = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RILaws LocBareType)
liftedIlaws forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , dvariance :: [(LocSymbol, [Variance])]
dvariance  = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, [Variance])
liftedDvariance forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , dsize :: [([LocBareType], LocSymbol)]
dsize      = LiftedSpec -> [([LocBareType], LocSymbol)]
liftedDsize  LiftedSpec
a
  , bounds :: RRBEnv LocBareType
bounds     = LiftedSpec -> RRBEnv LocBareType
liftedBounds LiftedSpec
a
  , defs :: HashMap LocSymbol Symbol
defs       = LiftedSpec -> HashMap LocSymbol Symbol
liftedDefs LiftedSpec
a
  , axeqs :: [Equation]
axeqs      = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Equation
liftedAxeqs forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  }