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

{-# LANGUAGE TypeSynonymInstances       #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RecordWildCards            #-}

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
  , StableModule(..)
  , toStableModule
  , renderModule
  , 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
  , targetSrcIso
  , targetSpecGetter
  , bareSpecIso
  , liftedSpecGetter
  , unsafeFromLiftedSpec
  ) where 

import           Optics
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           Language.Haskell.Liquid.GHC.API 
import           Language.Haskell.Liquid.GHC.Types
import           Text.PrettyPrint.HughesPJ              (text, (<+>)) 


{- $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 -> FilePath
giIncDir    :: !FilePath              -- ^ Path for LH include/prelude directory
  , 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
(Int -> QImports -> ShowS)
-> (QImports -> FilePath) -> ([QImports] -> ShowS) -> Show QImports
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 
  }

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
  }

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 -> [(Var, [Int])]
gsDecr       :: ![(Var, [Int])]               -- ^ Lexicographic order of decreasing args (DEPRECATED) 
  , GhcSpecTerm -> HashSet Var
gsNonStTerm  :: !(S.HashSet Var)              -- ^ Binders to CHECK using REFINEMENT-TYPES/termination metrics 
  }

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]
  }

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. BareSpec -> Rep BareSpec x)
-> (forall x. Rep BareSpec x -> BareSpec) -> Generic BareSpec
forall x. Rep BareSpec x -> BareSpec
forall x. BareSpec -> Rep BareSpec x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BareSpec x -> BareSpec
$cfrom :: forall x. BareSpec -> Rep BareSpec x
Generic, Int -> BareSpec -> ShowS
[BareSpec] -> ShowS
BareSpec -> FilePath
(Int -> BareSpec -> ShowS)
-> (BareSpec -> FilePath) -> ([BareSpec] -> ShowS) -> Show BareSpec
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [BareSpec] -> ShowS
$cshowList :: [BareSpec] -> ShowS
show :: BareSpec -> FilePath
$cshow :: BareSpec -> FilePath
showsPrec :: Int -> BareSpec -> ShowS
$cshowsPrec :: Int -> BareSpec -> ShowS
Show, b -> BareSpec -> BareSpec
NonEmpty BareSpec -> BareSpec
BareSpec -> BareSpec -> BareSpec
(BareSpec -> BareSpec -> BareSpec)
-> (NonEmpty BareSpec -> BareSpec)
-> (forall b. Integral b => b -> BareSpec -> BareSpec)
-> Semigroup BareSpec
forall b. Integral b => b -> BareSpec -> BareSpec
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> BareSpec -> BareSpec
$cstimes :: forall b. Integral b => b -> BareSpec -> BareSpec
sconcat :: NonEmpty BareSpec -> BareSpec
$csconcat :: NonEmpty BareSpec -> BareSpec
<> :: BareSpec -> BareSpec -> BareSpec
$c<> :: BareSpec -> BareSpec -> BareSpec
Semigroup, Semigroup BareSpec
BareSpec
Semigroup BareSpec
-> BareSpec
-> (BareSpec -> BareSpec -> BareSpec)
-> ([BareSpec] -> BareSpec)
-> Monoid BareSpec
[BareSpec] -> BareSpec
BareSpec -> BareSpec -> BareSpec
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [BareSpec] -> BareSpec
$cmconcat :: [BareSpec] -> BareSpec
mappend :: BareSpec -> BareSpec -> BareSpec
$cmappend :: BareSpec -> BareSpec -> BareSpec
mempty :: BareSpec
$cmempty :: BareSpec
$cp1Monoid :: Semigroup BareSpec
Monoid, Get BareSpec
[BareSpec] -> Put
BareSpec -> Put
(BareSpec -> Put)
-> Get BareSpec -> ([BareSpec] -> Put) -> Binary BareSpec
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)

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

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

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

-- $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, [Int])
liftedDecr       :: HashSet (F.LocSymbol, [Int])
    -- ^ Information on decreasing arguments
  , 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 -> 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
(LiftedSpec -> LiftedSpec -> Bool)
-> (LiftedSpec -> LiftedSpec -> Bool) -> Eq LiftedSpec
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. 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
$cto :: forall x. Rep LiftedSpec x -> LiftedSpec
$cfrom :: forall x. LiftedSpec -> Rep LiftedSpec x
Generic, Int -> LiftedSpec -> ShowS
[LiftedSpec] -> ShowS
LiftedSpec -> FilePath
(Int -> LiftedSpec -> ShowS)
-> (LiftedSpec -> FilePath)
-> ([LiftedSpec] -> ShowS)
-> Show LiftedSpec
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LiftedSpec] -> ShowS
$cshowList :: [LiftedSpec] -> ShowS
show :: LiftedSpec -> FilePath
$cshow :: LiftedSpec -> FilePath
showsPrec :: Int -> LiftedSpec -> ShowS
$cshowsPrec :: Int -> LiftedSpec -> ShowS
Show)
    deriving Int -> LiftedSpec -> Int
LiftedSpec -> Int
(Int -> LiftedSpec -> Int)
-> (LiftedSpec -> Int) -> Hashable LiftedSpec
forall 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
(LiftedSpec -> Put)
-> Get LiftedSpec -> ([LiftedSpec] -> Put) -> Binary LiftedSpec
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 


-- $trackingDeps

-- | A newtype wrapper around a 'Module' which:
--
-- * Allows a 'Module' to be serialised (i.e. it has a 'Binary' instance)
-- * It tries to use stable comparison and equality under the hood.
--
newtype StableModule = 
  StableModule { StableModule -> Module
unStableModule :: Module } 
  deriving (forall x. StableModule -> Rep StableModule x)
-> (forall x. Rep StableModule x -> StableModule)
-> Generic StableModule
forall x. Rep StableModule x -> StableModule
forall x. StableModule -> Rep StableModule x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep StableModule x -> StableModule
$cfrom :: forall x. StableModule -> Rep StableModule x
Generic

-- | Converts a 'Module' into a 'StableModule'.
toStableModule :: Module -> StableModule
toStableModule :: Module -> StableModule
toStableModule = Module -> StableModule
StableModule

renderModule :: Module -> String
renderModule :: Module -> FilePath
renderModule Module
m =    FilePath
"Module { unitId = " FilePath -> ShowS
forall a. Semigroup a => a -> a -> a
<> UnitId -> FilePath
forall a. Show a => a -> FilePath
show (Module -> UnitId
moduleUnitId Module
m)
                 FilePath -> ShowS
forall a. Semigroup a => a -> a -> a
<> FilePath
", name = " FilePath -> ShowS
forall a. Semigroup a => a -> a -> a
<> ModuleName -> FilePath
forall a. Show a => a -> FilePath
show (Module -> ModuleName
moduleName Module
m) 
                 FilePath -> ShowS
forall a. Semigroup a => a -> a -> a
<> FilePath
" }"

instance Hashable StableModule where
  hashWithSalt :: Int -> StableModule -> Int
hashWithSalt Int
s (StableModule Module
mdl) = Int -> FilePath -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Module -> FilePath
moduleStableString Module
mdl)

instance Ord StableModule where
  (StableModule Module
m1) compare :: StableModule -> StableModule -> Ordering
`compare` (StableModule Module
m2) = Module -> Module -> Ordering
stableModuleCmp Module
m1 Module
m2

instance Eq StableModule where
  (StableModule Module
m1) == :: StableModule -> StableModule -> Bool
== (StableModule Module
m2) = (Module
m1 Module -> Module -> Ordering
`stableModuleCmp` Module
m2) Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Show StableModule where
    show :: StableModule -> FilePath
show (StableModule Module
mdl) = FilePath
"Stable" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Module -> FilePath
renderModule Module
mdl

instance Binary StableModule where

    put :: StableModule -> Put
put (StableModule Module
mdl) = do
      FilePath -> Put
forall t. Binary t => t -> Put
put (UnitId -> FilePath
unitIdString (UnitId -> FilePath) -> (Module -> UnitId) -> Module -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> UnitId
moduleUnitId (Module -> FilePath) -> Module -> FilePath
forall a b. (a -> b) -> a -> b
$ Module
mdl)
      FilePath -> Put
forall t. Binary t => t -> Put
put (ModuleName -> FilePath
moduleNameString (ModuleName -> FilePath)
-> (Module -> ModuleName) -> Module -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> ModuleName
moduleName (Module -> FilePath) -> Module -> FilePath
forall a b. (a -> b) -> a -> b
$ Module
mdl)

    get :: Get StableModule
get = do
      FilePath
uidStr <- Get FilePath
forall t. Binary t => Get t
get
      FilePath
mnStr  <- Get FilePath
forall t. Binary t => Get t
get
      StableModule -> Get StableModule
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StableModule -> Get StableModule)
-> StableModule -> Get StableModule
forall a b. (a -> b) -> a -> b
$ Module -> StableModule
StableModule (UnitId -> ModuleName -> Module
Module (FilePath -> UnitId
stringToUnitId FilePath
uidStr) (FilePath -> ModuleName
mkModuleName FilePath
mnStr))

-- | 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
(TargetDependencies -> TargetDependencies -> Bool)
-> (TargetDependencies -> TargetDependencies -> Bool)
-> Eq TargetDependencies
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
(Int -> TargetDependencies -> ShowS)
-> (TargetDependencies -> FilePath)
-> ([TargetDependencies] -> ShowS)
-> Show TargetDependencies
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, b -> TargetDependencies -> TargetDependencies
NonEmpty TargetDependencies -> TargetDependencies
TargetDependencies -> TargetDependencies -> TargetDependencies
(TargetDependencies -> TargetDependencies -> TargetDependencies)
-> (NonEmpty TargetDependencies -> TargetDependencies)
-> (forall b.
    Integral b =>
    b -> TargetDependencies -> TargetDependencies)
-> Semigroup TargetDependencies
forall b.
Integral b =>
b -> TargetDependencies -> TargetDependencies
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> TargetDependencies -> TargetDependencies
$cstimes :: forall b.
Integral b =>
b -> TargetDependencies -> TargetDependencies
sconcat :: NonEmpty TargetDependencies -> TargetDependencies
$csconcat :: NonEmpty TargetDependencies -> TargetDependencies
<> :: TargetDependencies -> TargetDependencies -> TargetDependencies
$c<> :: TargetDependencies -> TargetDependencies -> TargetDependencies
Semigroup, Semigroup TargetDependencies
TargetDependencies
Semigroup TargetDependencies
-> TargetDependencies
-> (TargetDependencies -> TargetDependencies -> TargetDependencies)
-> ([TargetDependencies] -> TargetDependencies)
-> Monoid TargetDependencies
[TargetDependencies] -> TargetDependencies
TargetDependencies -> TargetDependencies -> TargetDependencies
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [TargetDependencies] -> TargetDependencies
$cmconcat :: [TargetDependencies] -> TargetDependencies
mappend :: TargetDependencies -> TargetDependencies -> TargetDependencies
$cmappend :: TargetDependencies -> TargetDependencies -> TargetDependencies
mempty :: TargetDependencies
$cmempty :: TargetDependencies
$cp1Monoid :: Semigroup TargetDependencies
Monoid, (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
$cto :: forall x. Rep TargetDependencies x -> TargetDependencies
$cfrom :: forall x. TargetDependencies -> Rep TargetDependencies x
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
putList :: [TargetDependencies] -> Put
$cputList :: [TargetDependencies] -> Put
get :: Get TargetDependencies
$cget :: Get TargetDependencies
put :: TargetDependencies -> Put
$cput :: TargetDependencies -> Put
Binary via Generically TargetDependencies

-- | 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 -> HashMap Var (Maybe Int) -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Var
x (GhcSpecRefl -> HashMap Var (Maybe Int)
gsAutoInst (TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
sp)) 

-- | 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 -> FilePath
_giIncDir    :: !FilePath              -- ^ Path for LH include/prelude directory
  , 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

{- 
instance HasConfig GhcInfo where
  getConfig = getConfig . _giSpec
-}

{- $provisionalBackCompat

In order to smooth out the migration process to this API, here we provide some /compat/ 'Iso' and 'Prism'
to convert from/to the old data structures, so that migration can be done organically over time.
-}

targetSrcIso :: Iso' GhcSrc TargetSrc
targetSrcIso :: Iso' GhcSrc TargetSrc
targetSrcIso = (GhcSrc -> TargetSrc)
-> (TargetSrc -> GhcSrc) -> Iso' GhcSrc TargetSrc
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso GhcSrc -> TargetSrc
toTargetSrc TargetSrc -> GhcSrc
fromTargetSrc
  where
    toTargetSrc :: GhcSrc -> TargetSrc
toTargetSrc GhcSrc
a = TargetSrc :: FilePath
-> FilePath
-> ModName
-> [CoreBind]
-> [TyCon]
-> Maybe [ClsInst]
-> HashSet Var
-> [Var]
-> [Var]
-> [Var]
-> HashSet StableName
-> [TyCon]
-> [(Symbol, DataCon)]
-> [TyCon]
-> QImports
-> HashSet Symbol
-> [TyThing]
-> TargetSrc
TargetSrc
      { giIncDir :: FilePath
giIncDir    = GhcSrc -> FilePath
_giIncDir GhcSrc
a
      , 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
a = Src :: FilePath
-> FilePath
-> ModName
-> [CoreBind]
-> [TyCon]
-> Maybe [ClsInst]
-> HashSet Var
-> [Var]
-> [Var]
-> [Var]
-> HashSet StableName
-> [TyCon]
-> [(Symbol, DataCon)]
-> [TyCon]
-> QImports
-> HashSet Symbol
-> [TyThing]
-> GhcSrc
Src
      { _giIncDir :: FilePath
_giIncDir    = TargetSrc -> FilePath
giIncDir TargetSrc
a
      , _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
      }

targetSpecGetter :: Getter GhcSpec (TargetSpec, LiftedSpec)
targetSpecGetter :: Getter GhcSpec (TargetSpec, LiftedSpec)
targetSpecGetter = 
  (GhcSpec -> (TargetSpec, LiftedSpec))
-> Getter GhcSpec (TargetSpec, LiftedSpec)
forall s a. (s -> a) -> Getter s a
to (\GhcSpec
ghcSpec -> (GhcSpec -> TargetSpec
toTargetSpec GhcSpec
ghcSpec, Optic' A_Getter '[] GhcSpec LiftedSpec -> GhcSpec -> LiftedSpec
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view ((GhcSpec -> Spec LocBareType LocSymbol)
-> Getter GhcSpec (Spec LocBareType LocSymbol)
forall s a. (s -> a) -> Getter s a
to GhcSpec -> Spec LocBareType LocSymbol
_gsLSpec Getter GhcSpec (Spec LocBareType LocSymbol)
-> Optic
     A_Getter
     '[]
     (Spec LocBareType LocSymbol)
     (Spec LocBareType LocSymbol)
     LiftedSpec
     LiftedSpec
-> Optic' A_Getter '[] GhcSpec LiftedSpec
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Optic
  A_Getter
  '[]
  (Spec LocBareType LocSymbol)
  (Spec LocBareType LocSymbol)
  LiftedSpec
  LiftedSpec
liftedSpecGetter) GhcSpec
ghcSpec))
  where
    toTargetSpec :: GhcSpec -> TargetSpec
toTargetSpec GhcSpec
a = TargetSpec :: GhcSpecSig
-> GhcSpecQual
-> GhcSpecData
-> GhcSpecNames
-> GhcSpecVars
-> GhcSpecTerm
-> GhcSpecRefl
-> GhcSpecLaws
-> [(Symbol, Sort)]
-> Config
-> TargetSpec
TargetSpec
      { gsSig :: GhcSpecSig
gsSig    = GhcSpec -> GhcSpecSig
_gsSig GhcSpec
a
      , gsQual :: GhcSpecQual
gsQual   = GhcSpec -> GhcSpecQual
_gsQual GhcSpec
a
      , gsData :: GhcSpecData
gsData   = GhcSpec -> GhcSpecData
_gsData GhcSpec
a
      , gsName :: GhcSpecNames
gsName   = GhcSpec -> GhcSpecNames
_gsName GhcSpec
a
      , gsVars :: GhcSpecVars
gsVars   = GhcSpec -> GhcSpecVars
_gsVars GhcSpec
a
      , gsTerm :: GhcSpecTerm
gsTerm   = GhcSpec -> GhcSpecTerm
_gsTerm GhcSpec
a
      , gsRefl :: GhcSpecRefl
gsRefl   = GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
a
      , gsLaws :: GhcSpecLaws
gsLaws   = GhcSpec -> GhcSpecLaws
_gsLaws GhcSpec
a
      , gsImps :: [(Symbol, Sort)]
gsImps   = GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
a
      , gsConfig :: Config
gsConfig = GhcSpec -> Config
_gsConfig GhcSpec
a
      }

bareSpecIso :: Iso' (Spec LocBareType F.LocSymbol) BareSpec
bareSpecIso :: Iso' (Spec LocBareType LocSymbol) BareSpec
bareSpecIso = (Spec LocBareType LocSymbol -> BareSpec)
-> (BareSpec -> Spec LocBareType LocSymbol)
-> Iso' (Spec LocBareType LocSymbol) BareSpec
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Spec LocBareType LocSymbol -> BareSpec
MkBareSpec BareSpec -> Spec LocBareType LocSymbol
getBareSpec

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

-- 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 :: forall ty bndr.
[Measure ty bndr]
-> [(Symbol, Sort)]
-> [(Symbol, Sort)]
-> [(LocSymbol, ty)]
-> [(LocSymbol, ty)]
-> [(LocSymbol, ty)]
-> [(LocSymbol, ty)]
-> [(Maybe LocSymbol, ty)]
-> [(ty, ty)]
-> [Symbol]
-> [DataDecl]
-> [DataDecl]
-> [FilePath]
-> [Located (RTAlias Symbol BareType)]
-> [Located (RTAlias Symbol Expr)]
-> TCEmb LocSymbol
-> [Qualifier]
-> [(LocSymbol, [Int])]
-> HashSet LocSymbol
-> HashSet LocSymbol
-> HashSet LocSymbol
-> HashMap LocSymbol [LocSymbol]
-> HashSet LocSymbol
-> HashSet LocSymbol
-> HashMap LocSymbol (Maybe Int)
-> HashSet LocSymbol
-> HashSet LocSymbol
-> HashSet LocSymbol
-> HashSet LocSymbol
-> HashSet LocSymbol
-> [Located FilePath]
-> [Measure ty ()]
-> [Measure ty bndr]
-> [RClass ty]
-> [RClass ty]
-> [(LocSymbol, [Located Expr])]
-> [RInstance ty]
-> [RILaws ty]
-> [(LocSymbol, [Variance])]
-> RRBEnv ty
-> HashMap LocSymbol Symbol
-> [Equation]
-> Spec ty bndr
Spec
  { measures :: [Measure LocBareType LocSymbol]
measures   = HashSet (Measure LocBareType LocSymbol)
-> [Measure LocBareType LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet (Measure LocBareType LocSymbol)
 -> [Measure LocBareType LocSymbol])
-> (LiftedSpec -> HashSet (Measure LocBareType LocSymbol))
-> LiftedSpec
-> [Measure LocBareType LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedMeasures (LiftedSpec -> [Measure LocBareType LocSymbol])
-> LiftedSpec -> [Measure LocBareType LocSymbol]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , impSigs :: [(Symbol, Sort)]
impSigs    = HashSet (Symbol, Sort) -> [(Symbol, Sort)]
forall a. HashSet a -> [a]
S.toList (HashSet (Symbol, Sort) -> [(Symbol, Sort)])
-> (LiftedSpec -> HashSet (Symbol, Sort))
-> LiftedSpec
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Symbol, Sort)
liftedImpSigs (LiftedSpec -> [(Symbol, Sort)]) -> LiftedSpec -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , expSigs :: [(Symbol, Sort)]
expSigs    = HashSet (Symbol, Sort) -> [(Symbol, Sort)]
forall a. HashSet a -> [a]
S.toList (HashSet (Symbol, Sort) -> [(Symbol, Sort)])
-> (LiftedSpec -> HashSet (Symbol, Sort))
-> LiftedSpec
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Symbol, Sort)
liftedExpSigs (LiftedSpec -> [(Symbol, Sort)]) -> LiftedSpec -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs    = HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)])
-> (LiftedSpec -> HashSet (LocSymbol, LocBareType))
-> LiftedSpec
-> [(LocSymbol, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedAsmSigs (LiftedSpec -> [(LocSymbol, LocBareType)])
-> LiftedSpec -> [(LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , sigs :: [(LocSymbol, LocBareType)]
sigs       = HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, LocBareType) -> [(LocSymbol, LocBareType)])
-> (LiftedSpec -> HashSet (LocSymbol, LocBareType))
-> LiftedSpec
-> [(LocSymbol, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, LocBareType)
liftedSigs (LiftedSpec -> [(LocSymbol, LocBareType)])
-> LiftedSpec -> [(LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , localSigs :: [(LocSymbol, LocBareType)]
localSigs  = [(LocSymbol, LocBareType)]
forall a. Monoid a => a
mempty
  , reflSigs :: [(LocSymbol, LocBareType)]
reflSigs   = [(LocSymbol, LocBareType)]
forall a. Monoid a => a
mempty
  , invariants :: [(Maybe LocSymbol, LocBareType)]
invariants = HashSet (Maybe LocSymbol, LocBareType)
-> [(Maybe LocSymbol, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (Maybe LocSymbol, LocBareType)
 -> [(Maybe LocSymbol, LocBareType)])
-> (LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType))
-> LiftedSpec
-> [(Maybe LocSymbol, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Maybe LocSymbol, LocBareType)
liftedInvariants (LiftedSpec -> [(Maybe LocSymbol, LocBareType)])
-> LiftedSpec -> [(Maybe LocSymbol, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , ialiases :: [(LocBareType, LocBareType)]
ialiases   = HashSet (LocBareType, LocBareType) -> [(LocBareType, LocBareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (LocBareType, LocBareType)
 -> [(LocBareType, LocBareType)])
-> (LiftedSpec -> HashSet (LocBareType, LocBareType))
-> LiftedSpec
-> [(LocBareType, LocBareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocBareType, LocBareType)
liftedIaliases (LiftedSpec -> [(LocBareType, LocBareType)])
-> LiftedSpec -> [(LocBareType, LocBareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , imports :: [Symbol]
imports    = HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> [Symbol])
-> (LiftedSpec -> HashSet Symbol) -> LiftedSpec -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Symbol
liftedImports (LiftedSpec -> [Symbol]) -> LiftedSpec -> [Symbol]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , dataDecls :: [DataDecl]
dataDecls  = HashSet DataDecl -> [DataDecl]
forall a. HashSet a -> [a]
S.toList (HashSet DataDecl -> [DataDecl])
-> (LiftedSpec -> HashSet DataDecl) -> LiftedSpec -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDecl
liftedDataDecls (LiftedSpec -> [DataDecl]) -> LiftedSpec -> [DataDecl]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , newtyDecls :: [DataDecl]
newtyDecls = HashSet DataDecl -> [DataDecl]
forall a. HashSet a -> [a]
S.toList (HashSet DataDecl -> [DataDecl])
-> (LiftedSpec -> HashSet DataDecl) -> LiftedSpec -> [DataDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet DataDecl
liftedNewtyDecls (LiftedSpec -> [DataDecl]) -> LiftedSpec -> [DataDecl]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , includes :: [FilePath]
includes   = [FilePath]
forall a. Monoid a => a
mempty
  , aliases :: [Located (RTAlias Symbol BareType)]
aliases    = HashSet (Located (RTAlias Symbol BareType))
-> [Located (RTAlias Symbol BareType)]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (RTAlias Symbol BareType))
 -> [Located (RTAlias Symbol BareType)])
-> (LiftedSpec -> HashSet (Located (RTAlias Symbol BareType)))
-> LiftedSpec
-> [Located (RTAlias Symbol BareType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol BareType))
liftedAliases (LiftedSpec -> [Located (RTAlias Symbol BareType)])
-> LiftedSpec -> [Located (RTAlias Symbol BareType)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , ealiases :: [Located (RTAlias Symbol Expr)]
ealiases   = HashSet (Located (RTAlias Symbol Expr))
-> [Located (RTAlias Symbol Expr)]
forall a. HashSet a -> [a]
S.toList (HashSet (Located (RTAlias Symbol Expr))
 -> [Located (RTAlias Symbol Expr)])
-> (LiftedSpec -> HashSet (Located (RTAlias Symbol Expr)))
-> LiftedSpec
-> [Located (RTAlias Symbol Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Located (RTAlias Symbol Expr))
liftedEaliases (LiftedSpec -> [Located (RTAlias Symbol Expr)])
-> LiftedSpec -> [Located (RTAlias Symbol Expr)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , embeds :: TCEmb LocSymbol
embeds     = LiftedSpec -> TCEmb LocSymbol
liftedEmbeds LiftedSpec
a
  , qualifiers :: [Qualifier]
qualifiers = HashSet Qualifier -> [Qualifier]
forall a. HashSet a -> [a]
S.toList (HashSet Qualifier -> [Qualifier])
-> (LiftedSpec -> HashSet Qualifier) -> LiftedSpec -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Qualifier
liftedQualifiers (LiftedSpec -> [Qualifier]) -> LiftedSpec -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , decr :: [(LocSymbol, [Int])]
decr       = HashSet (LocSymbol, [Int]) -> [(LocSymbol, [Int])]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, [Int]) -> [(LocSymbol, [Int])])
-> (LiftedSpec -> HashSet (LocSymbol, [Int]))
-> LiftedSpec
-> [(LocSymbol, [Int])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, [Int])
liftedDecr (LiftedSpec -> [(LocSymbol, [Int])])
-> LiftedSpec -> [(LocSymbol, [Int])]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , lvars :: HashSet LocSymbol
lvars      = LiftedSpec -> HashSet LocSymbol
liftedLvars LiftedSpec
a
  , lazy :: HashSet LocSymbol
lazy       = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , fails :: HashSet LocSymbol
fails      = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , rewrites :: HashSet LocSymbol
rewrites   = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , rewriteWith :: HashMap LocSymbol [LocSymbol]
rewriteWith = HashMap LocSymbol [LocSymbol]
forall a. Monoid a => a
mempty
  , reflects :: HashSet LocSymbol
reflects   = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , autois :: HashMap LocSymbol (Maybe Int)
autois     = LiftedSpec -> HashMap LocSymbol (Maybe Int)
liftedAutois LiftedSpec
a
  , hmeas :: HashSet LocSymbol
hmeas      = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , hbounds :: HashSet LocSymbol
hbounds    = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , inlines :: HashSet LocSymbol
inlines    = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , ignores :: HashSet LocSymbol
ignores    = HashSet LocSymbol
forall a. Monoid a => a
mempty
  , autosize :: HashSet LocSymbol
autosize   = LiftedSpec -> HashSet LocSymbol
liftedAutosize LiftedSpec
a
  , pragmas :: [Located FilePath]
pragmas    = [Located FilePath]
forall a. Monoid a => a
mempty
  , cmeasures :: [Measure LocBareType ()]
cmeasures  = HashSet (Measure LocBareType ()) -> [Measure LocBareType ()]
forall a. HashSet a -> [a]
S.toList (HashSet (Measure LocBareType ()) -> [Measure LocBareType ()])
-> (LiftedSpec -> HashSet (Measure LocBareType ()))
-> LiftedSpec
-> [Measure LocBareType ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType ())
liftedCmeasures (LiftedSpec -> [Measure LocBareType ()])
-> LiftedSpec -> [Measure LocBareType ()]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , imeasures :: [Measure LocBareType LocSymbol]
imeasures  = HashSet (Measure LocBareType LocSymbol)
-> [Measure LocBareType LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet (Measure LocBareType LocSymbol)
 -> [Measure LocBareType LocSymbol])
-> (LiftedSpec -> HashSet (Measure LocBareType LocSymbol))
-> LiftedSpec
-> [Measure LocBareType LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (Measure LocBareType LocSymbol)
liftedImeasures (LiftedSpec -> [Measure LocBareType LocSymbol])
-> LiftedSpec -> [Measure LocBareType LocSymbol]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , classes :: [RClass LocBareType]
classes    = HashSet (RClass LocBareType) -> [RClass LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RClass LocBareType) -> [RClass LocBareType])
-> (LiftedSpec -> HashSet (RClass LocBareType))
-> LiftedSpec
-> [RClass LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass LocBareType)
liftedClasses (LiftedSpec -> [RClass LocBareType])
-> LiftedSpec -> [RClass LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , claws :: [RClass LocBareType]
claws      = HashSet (RClass LocBareType) -> [RClass LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RClass LocBareType) -> [RClass LocBareType])
-> (LiftedSpec -> HashSet (RClass LocBareType))
-> LiftedSpec
-> [RClass LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RClass LocBareType)
liftedClaws (LiftedSpec -> [RClass LocBareType])
-> LiftedSpec -> [RClass LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , termexprs :: [(LocSymbol, [Located Expr])]
termexprs  = [(LocSymbol, [Located Expr])]
forall a. Monoid a => a
mempty
  , rinstance :: [RInstance LocBareType]
rinstance  = HashSet (RInstance LocBareType) -> [RInstance LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RInstance LocBareType) -> [RInstance LocBareType])
-> (LiftedSpec -> HashSet (RInstance LocBareType))
-> LiftedSpec
-> [RInstance LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RInstance LocBareType)
liftedRinstance (LiftedSpec -> [RInstance LocBareType])
-> LiftedSpec -> [RInstance LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , ilaws :: [RILaws LocBareType]
ilaws      = HashSet (RILaws LocBareType) -> [RILaws LocBareType]
forall a. HashSet a -> [a]
S.toList (HashSet (RILaws LocBareType) -> [RILaws LocBareType])
-> (LiftedSpec -> HashSet (RILaws LocBareType))
-> LiftedSpec
-> [RILaws LocBareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (RILaws LocBareType)
liftedIlaws (LiftedSpec -> [RILaws LocBareType])
-> LiftedSpec -> [RILaws LocBareType]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , dvariance :: [(LocSymbol, [Variance])]
dvariance  = HashSet (LocSymbol, [Variance]) -> [(LocSymbol, [Variance])]
forall a. HashSet a -> [a]
S.toList (HashSet (LocSymbol, [Variance]) -> [(LocSymbol, [Variance])])
-> (LiftedSpec -> HashSet (LocSymbol, [Variance]))
-> LiftedSpec
-> [(LocSymbol, [Variance])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet (LocSymbol, [Variance])
liftedDvariance (LiftedSpec -> [(LocSymbol, [Variance])])
-> LiftedSpec -> [(LocSymbol, [Variance])]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  , bounds :: RRBEnv LocBareType
bounds     = LiftedSpec -> RRBEnv LocBareType
liftedBounds LiftedSpec
a
  , defs :: HashMap LocSymbol Symbol
defs       = LiftedSpec -> HashMap LocSymbol Symbol
liftedDefs LiftedSpec
a
  , axeqs :: [Equation]
axeqs      = HashSet Equation -> [Equation]
forall a. HashSet a -> [a]
S.toList (HashSet Equation -> [Equation])
-> (LiftedSpec -> HashSet Equation) -> LiftedSpec -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashSet Equation
liftedAxeqs (LiftedSpec -> [Equation]) -> LiftedSpec -> [Equation]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
a
  }