{-# LANGUAGE DeriveAnyClass #-}

-- | This module contains the top-level structures that hold

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE DeriveGeneric #-}

{-# LANGUAGE DerivingVia #-}

{-# LANGUAGE StandaloneDeriving #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.Types.Specs (

-- * Different types of specifications

-- $differentSpecTypes

-- * TargetInfo

-- $targetInfo

TargetInfo(..)

-- * Gathering information about a module

, TargetSrc(..)

-- * TargetSpec

-- $targetSpec

, TargetSpec(..)

-- * BareSpec

-- $bareSpec

, BareSpec(..)

-- * LiftedSpec

-- $liftedSpec

, LiftedSpec(..)

-- * Tracking dependencies

-- $trackingDeps

, TargetDependencies(..)

, dropDependency

-- * Predicates on spec types

-- $predicates

, isPLEVar

, isExportedVar

-- * Other types

, QImports(..)

, Spec(..)

, GhcSpecVars(..)

, GhcSpecSig(..)

, GhcSpecNames(..)

, GhcSpecTerm(..)

, GhcSpecRefl(..)

, GhcSpecLaws(..)

, GhcSpecData(..)

, GhcSpecQual(..)

, BareDef

, BareMeasure

, SpecMeasure

, VarOrLocSymbol

, LawInstance(..)

-- * Legacy data structures

-- $legacyDataStructures

, GhcSrc(..)

, GhcSpec(..)

-- * Provisional compatibility exports & optics

-- $provisionalBackCompat

, toTargetSrc

, fromTargetSrc

, toTargetSpec

, toBareSpec

, fromBareSpec

, toLiftedSpec

, unsafeFromLiftedSpec

, emptyLiftedSpec

) where

import GHC.Generics hiding (to, moduleName)

import Data.Binary

import qualified Language.Fixpoint.Types as F

import Language.Fixpoint.Misc (sortNub)

import Data.Hashable

import qualified Data.HashSet as S

import Data.HashSet (HashSet)

import qualified Data.HashMap.Strict as M

import Data.HashMap.Strict (HashMap)

import Language.Haskell.Liquid.Types.Types

import Language.Haskell.Liquid.Types.Variance

import Language.Haskell.Liquid.Types.Bounds

import Liquid.GHC.API hiding (text, (<+>))

import Language.Haskell.Liquid.GHC.Types

import Text.PrettyPrint.HughesPJ (text, (<+>))

import Text.PrettyPrint.HughesPJ as HughesPJ (($$))

data TargetInfo = TargetInfo

{ giSrc :: !TargetSrc

-- ^ The 'TargetSrc' of the module being checked.

, giSpec :: !TargetSpec

-- ^ The 'TargetSpec' of the module being checked.

}

instance HasConfig TargetInfo where

getConfig = getConfig . giSpec

-- | The 'TargetSrc' type is a collection of all the things we know about a module being currently

data TargetSrc = TargetSrc

{ giTarget :: !FilePath -- ^ Source file for module

, giTargetMod :: !ModName -- ^ Name for module

, giCbs :: ![CoreBind] -- ^ Source Code

, gsTcs :: ![TyCon] -- ^ All used Type constructors

, gsCls :: !(Maybe [ClsInst]) -- ^ Class instances?

, giDerVars :: !(HashSet Var) -- ^ Binders created by GHC eg dictionaries

, giImpVars :: ![Var] -- ^ Binders that are _read_ in module (but not defined?)

, giDefVars :: ![Var] -- ^ (Top-level) binders that are _defined_ in module

, giUseVars :: ![Var] -- ^ Binders that are _read_ in module

, gsExports :: !(HashSet StableName) -- ^ `Name`s exported by the module being verified

, gsFiTcs :: ![TyCon] -- ^ Family instance TyCons

, gsFiDcs :: ![(F.Symbol, DataCon)] -- ^ Family instance DataCons

, gsPrimTcs :: ![TyCon] -- ^ Primitive GHC TyCons (from TysPrim.primTyCons)

, gsQualImps :: !QImports -- ^ Map of qualified imports

, gsAllImps :: !(HashSet F.Symbol) -- ^ Set of _all_ imported modules

, gsTyThings :: ![TyThing] -- ^ All the @TyThing@s known to GHC

}

-- | 'QImports' is a map of qualified imports.

data QImports = QImports

{ qiModules :: !(S.HashSet F.Symbol) -- ^ All the modules that are imported qualified

, qiNames :: !(M.HashMap F.Symbol [F.Symbol]) -- ^ Map from qualification to full module name

} deriving Show

-- | A 'TargetSpec' is what we /actually check via LiquidHaskell/. It is created as part of 'mkTargetSpec'

data TargetSpec = TargetSpec

{ gsSig :: !GhcSpecSig

, gsQual :: !GhcSpecQual

, gsData :: !GhcSpecData

, gsName :: !GhcSpecNames

, gsVars :: !GhcSpecVars

, gsTerm :: !GhcSpecTerm

, gsRefl :: !GhcSpecRefl

, gsLaws :: !GhcSpecLaws

, gsImps :: ![(F.Symbol, F.Sort)] -- ^ Imported Environment

, gsConfig :: !Config

}

deriving Show

instance HasConfig TargetSpec where

getConfig = gsConfig

-- | The collection of GHC 'Var's that a 'TargetSpec' needs to verify (or skip).

data GhcSpecVars = SpVar

{ gsTgtVars :: ![Var] -- ^ Top-level Binders To Verify (empty means ALL binders)

, gsIgnoreVars :: !(S.HashSet Var) -- ^ Top-level Binders To NOT Verify (empty means ALL binders)

, gsLvars :: !(S.HashSet Var) -- ^ Variables that should be checked "lazily" in the environment they are used

, gsCMethods :: ![Var] -- ^ Refined Class methods

}

deriving Show

instance Semigroup GhcSpecVars where

sv1 <> sv2 = SpVar

{ gsTgtVars = gsTgtVars sv1 <> gsTgtVars sv2

, gsIgnoreVars = gsIgnoreVars sv1 <> gsIgnoreVars sv2

, gsLvars = gsLvars sv1 <> gsLvars sv2

, gsCMethods = gsCMethods sv1 <> gsCMethods sv2

}

instance Monoid GhcSpecVars where

mempty = SpVar mempty mempty mempty mempty

data GhcSpecQual = SpQual

{ gsQualifiers :: ![F.Qualifier] -- ^ Qualifiers in Source/Spec files e.g tests/pos/qualTest.hs

, gsRTAliases :: ![F.Located SpecRTAlias] -- ^ Refinement type aliases (only used for qualifiers)

}

deriving Show

data GhcSpecSig = SpSig

{ gsTySigs :: ![(Var, LocSpecType)] -- ^ Asserted Reftypes

, gsAsmSigs :: ![(Var, LocSpecType)] -- ^ Assumed Reftypes

, gsRefSigs :: ![(Var, LocSpecType)] -- ^ Reflected Reftypes

, gsInSigs :: ![(Var, LocSpecType)] -- ^ Auto generated Signatures

, gsNewTypes :: ![(TyCon, LocSpecType)] -- ^ Mapping of 'newtype' type constructors with their refined types.

, gsDicts :: !(DEnv Var LocSpecType) -- ^ Refined Classes from Instances

, gsMethods :: ![(Var, MethodType LocSpecType)] -- ^ Refined Classes from Classes

, gsTexprs :: ![(Var, LocSpecType, [F.Located F.Expr])] -- ^ Lexicographically ordered expressions for termination

, gsRelation :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]

, gsAsmRel :: ![(Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]

}

deriving Show

instance Semigroup GhcSpecSig where

x <> y = SpSig

{ gsTySigs = gsTySigs x <> gsTySigs y

, gsAsmSigs = gsAsmSigs x <> gsAsmSigs y

, gsRefSigs = gsRefSigs x <> gsRefSigs y

, gsInSigs = gsInSigs x <> gsInSigs y

, gsNewTypes = gsNewTypes x <> gsNewTypes y

, gsDicts = gsDicts x <> gsDicts y

, gsMethods = gsMethods x <> gsMethods y

, gsTexprs = gsTexprs x <> gsTexprs y

, gsRelation = gsRelation x <> gsRelation y

, gsAsmRel = gsAsmRel x <> gsAsmRel y

}

instance Monoid GhcSpecSig where

mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty

data GhcSpecData = SpData

{ gsCtors :: ![(Var, LocSpecType)] -- ^ Data Constructor Measure Sigs

, gsMeas :: ![(F.Symbol, LocSpecType)] -- ^ Measure Types eg. len :: [a] -> Int

, gsInvariants :: ![(Maybe Var, LocSpecType)] -- ^ Data type invariants from measure definitions, e.g forall a. {v: [a] | len(v) >= 0}

, gsIaliases :: ![(LocSpecType, LocSpecType)] -- ^ Data type invariant aliases

, gsMeasures :: ![Measure SpecType DataCon] -- ^ Measure definitions

, gsUnsorted :: ![UnSortedExpr]

}

deriving Show

data GhcSpecNames = SpNames

{ gsFreeSyms :: ![(F.Symbol, Var)] -- ^ List of `Symbol` free in spec and corresponding GHC var, eg. (Cons, Cons#7uz) from tests/pos/ex1.hs

, gsDconsP :: ![F.Located DataCon] -- ^ Predicated Data-Constructors, e.g. see tests/pos/Map.hs

, gsTconsP :: ![TyConP] -- ^ Predicated Type-Constructors, e.g. see tests/pos/Map.hs

, gsTcEmbeds :: !(F.TCEmb TyCon) -- ^ Embedding GHC Tycons into fixpoint sorts e.g. "embed Set as Set_set" from include/Data/Set.spec

, gsADTs :: ![F.DataDecl] -- ^ ADTs extracted from Haskell 'data' definitions

, gsTyconEnv :: !TyConMap

}

deriving Show

deriving instance Show TyConP

deriving instance Show TyConMap

data GhcSpecTerm = SpTerm

{ gsStTerm :: !(S.HashSet Var) -- ^ Binders to CHECK by structural termination

, gsAutosize :: !(S.HashSet TyCon) -- ^ Binders to IGNORE during termination checking

, gsLazy :: !(S.HashSet Var) -- ^ Binders to IGNORE during termination checking

, gsFail :: !(S.HashSet (F.Located Var)) -- ^ Binders to fail type checking

, gsNonStTerm :: !(S.HashSet Var) -- ^ Binders to CHECK using REFINEMENT-TYPES/termination metrics

}

deriving Show

instance Semigroup GhcSpecTerm where

t1 <> t2 = SpTerm

{ gsStTerm = gsStTerm t1 <> gsStTerm t2

, gsAutosize = gsAutosize t1 <> gsAutosize t2

, gsLazy = gsLazy t1 <> gsLazy t2

, gsFail = gsFail t1 <> gsFail t2

, gsNonStTerm = gsNonStTerm t1 <> gsNonStTerm t2

}

instance Monoid GhcSpecTerm where

mempty = SpTerm mempty mempty mempty mempty mempty

data GhcSpecRefl = SpRefl

{ gsAutoInst :: !(M.HashMap Var (Maybe Int)) -- ^ Binders to USE PLE

, gsHAxioms :: ![(Var, LocSpecType, F.Equation)] -- ^ Lifted definitions

, gsImpAxioms :: ![F.Equation] -- ^ Axioms from imported reflected functions

, gsMyAxioms :: ![F.Equation] -- ^ Axioms from my reflected functions

, gsReflects :: ![Var] -- ^ Binders for reflected functions

, gsLogicMap :: !LogicMap

, gsWiredReft :: ![Var]

, gsRewrites :: S.HashSet (F.Located Var)

, gsRewritesWith :: M.HashMap Var [Var]

}

deriving Show

instance Semigroup GhcSpecRefl where

x <> y = SpRefl

{ gsAutoInst = gsAutoInst x <> gsAutoInst y

, gsHAxioms = gsHAxioms x <> gsHAxioms y

, gsImpAxioms = gsImpAxioms x <> gsImpAxioms y

, gsMyAxioms = gsMyAxioms x <> gsMyAxioms y

, gsReflects = gsReflects x <> gsReflects y

, gsLogicMap = gsLogicMap x <> gsLogicMap y

, gsWiredReft = gsWiredReft x <> gsWiredReft y

, gsRewrites = gsRewrites x <> gsRewrites y

, gsRewritesWith = gsRewritesWith x <> gsRewritesWith y

}

instance Monoid GhcSpecRefl where

mempty = SpRefl mempty mempty mempty

mempty mempty mempty

mempty mempty mempty

data GhcSpecLaws = SpLaws

{ gsLawDefs :: ![(Class, [(Var, LocSpecType)])]

, gsLawInst :: ![LawInstance]

}

deriving Show

data LawInstance = LawInstance

{ lilName :: Class

, liSupers :: [LocSpecType]

, lilTyArgs :: [LocSpecType]

, lilEqus :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]

, lilPos :: SrcSpan

}

deriving Show

type VarOrLocSymbol = Either Var LocSymbol

type BareMeasure = Measure LocBareType F.LocSymbol

type BareDef = Def LocBareType F.LocSymbol

type SpecMeasure = Measure LocSpecType DataCon

-- | A 'BareSpec' is the spec we derive by parsing the Liquid Haskell annotations of a single file. As

newtype BareSpec =

MkBareSpec { getBareSpec :: Spec LocBareType F.LocSymbol }

deriving (Generic, Show, Binary)

instance Semigroup BareSpec where

x <> y = MkBareSpec { getBareSpec = getBareSpec x <> getBareSpec y }

instance Monoid BareSpec where

mempty = MkBareSpec { getBareSpec = mempty }

-- | A generic 'Spec' type, polymorphic over the inner choice of type and binder.

data Spec ty bndr = Spec

{ measures :: ![Measure ty bndr] -- ^ User-defined properties for ADTs

, impSigs :: ![(F.Symbol, F.Sort)] -- ^ Imported variables types

, expSigs :: ![(F.Symbol, F.Sort)] -- ^ Exported variables types

, asmSigs :: ![(F.LocSymbol, ty)] -- ^ Assumed (unchecked) types; including reflected signatures

, sigs :: ![(F.LocSymbol, ty)] -- ^ Imported functions and types

, localSigs :: ![(F.LocSymbol, ty)] -- ^ Local type signatures

, reflSigs :: ![(F.LocSymbol, ty)] -- ^ Reflected type signatures

, invariants :: ![(Maybe F.LocSymbol, ty)] -- ^ Data type invariants; the Maybe is the generating measure

, ialiases :: ![(ty, ty)] -- ^ Data type invariants to be checked

, imports :: ![F.Symbol] -- ^ Loaded spec module names

, dataDecls :: ![DataDecl] -- ^ Predicated data definitions

, newtyDecls :: ![DataDecl] -- ^ Predicated new type definitions

, includes :: ![FilePath] -- ^ Included qualifier files

, aliases :: ![F.Located (RTAlias F.Symbol BareType)] -- ^ RefType aliases

, ealiases :: ![F.Located (RTAlias F.Symbol F.Expr)] -- ^ Expression aliases

, embeds :: !(F.TCEmb F.LocSymbol) -- ^ GHC-Tycon-to-fixpoint Tycon map

, qualifiers :: ![F.Qualifier] -- ^ Qualifiers in source/spec files

, lvars :: !(S.HashSet F.LocSymbol) -- ^ Variables that should be checked in the environment they are used

, lazy :: !(S.HashSet F.LocSymbol) -- ^ Ignore Termination Check in these Functions

, rewrites :: !(S.HashSet F.LocSymbol) -- ^ Theorems turned into rewrite rules

, rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol]) -- ^ Definitions using rewrite rules

, fails :: !(S.HashSet F.LocSymbol) -- ^ These Functions should be unsafe

, reflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to reflect

, autois :: !(M.HashMap F.LocSymbol (Maybe Int)) -- ^ Automatically instantiate axioms in these Functions with maybe specified fuel

, hmeas :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into measures using haskell definitions

, hbounds :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into bounds using haskell definitions

, inlines :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into logic inline using haskell definitions

, ignores :: !(S.HashSet F.LocSymbol) -- ^ Binders to ignore during checking; that is DON't check the corebind.

, autosize :: !(S.HashSet F.LocSymbol) -- ^ Type Constructors that get automatically sizing info

, pragmas :: ![F.Located String] -- ^ Command-line configurations passed in through source

, cmeasures :: ![Measure ty ()] -- ^ Measures attached to a type-class

, imeasures :: ![Measure ty bndr] -- ^ Mappings from (measure,type) -> measure

, classes :: ![RClass ty] -- ^ Refined Type-Classes

, claws :: ![RClass ty] -- ^ Refined Type-Classe Laws

, relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)] -- ^ Relational types

, asmRel :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)] -- ^ Assumed relational types

, termexprs :: ![(F.LocSymbol, [F.Located F.Expr])] -- ^ Terminating Conditions for functions

, rinstance :: ![RInstance ty]

, ilaws :: ![RILaws ty]

, dvariance :: ![(F.LocSymbol, [Variance])] -- ^ TODO ? Where do these come from ?!

, dsize :: ![([ty], F.LocSymbol)] -- ^ Size measure to enforce fancy termination

, bounds :: !(RRBEnv ty)

, defs :: !(M.HashMap F.LocSymbol F.Symbol) -- ^ Temporary (?) hack to deal with dictionaries in specifications

-- see tests/pos/NatClass.hs

, axeqs :: ![F.Equation] -- ^ Equalities used for Proof-By-Evaluation

} deriving (Generic, 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 k sp = text "dataDecls = " <+> pprintTidy k (dataDecls sp)

HughesPJ.$$

text "classes = " <+> pprintTidy k (classes sp)

HughesPJ.$$

text "sigs = " <+> pprintTidy k (sigs sp)

instance Semigroup (Spec ty bndr) where

s1 <> s2

= Spec { measures = measures s1 ++ measures s2

, impSigs = impSigs s1 ++ impSigs s2

, expSigs = expSigs s1 ++ expSigs s2

, asmSigs = asmSigs s1 ++ asmSigs s2

, sigs = sigs s1 ++ sigs s2

, localSigs = localSigs s1 ++ localSigs s2

, reflSigs = reflSigs s1 ++ reflSigs s2

, invariants = invariants s1 ++ invariants s2

, ialiases = ialiases s1 ++ ialiases s2

, imports = sortNub $ imports s1 ++ imports s2

, dataDecls = dataDecls s1 ++ dataDecls s2

, newtyDecls = newtyDecls s1 ++ newtyDecls s2

, includes = sortNub $ includes s1 ++ includes s2

, aliases = aliases s1 ++ aliases s2

, ealiases = ealiases s1 ++ ealiases s2

, qualifiers = qualifiers s1 ++ qualifiers s2

, pragmas = pragmas s1 ++ pragmas s2

, cmeasures = cmeasures s1 ++ cmeasures s2

, imeasures = imeasures s1 ++ imeasures s2

, classes = classes s1 ++ classes s2

, claws = claws s1 ++ claws s2

, relational = relational s1 ++ relational s2

, asmRel = asmRel s1 ++ asmRel s2

, termexprs = termexprs s1 ++ termexprs s2

, rinstance = rinstance s1 ++ rinstance s2

, ilaws = ilaws s1 ++ ilaws s2

, dvariance = dvariance s1 ++ dvariance s2

, dsize = dsize s1 ++ dsize s2

, axeqs = axeqs s1 ++ axeqs s2

, embeds = mappend (embeds s1) (embeds s2)

, lvars = S.union (lvars s1) (lvars s2)

, lazy = S.union (lazy s1) (lazy s2)

, rewrites = S.union (rewrites s1) (rewrites s2)

, rewriteWith = M.union (rewriteWith s1) (rewriteWith s2)

, fails = S.union (fails s1) (fails s2)

, reflects = S.union (reflects s1) (reflects s2)

, hmeas = S.union (hmeas s1) (hmeas s2)

, hbounds = S.union (hbounds s1) (hbounds s2)

, inlines = S.union (inlines s1) (inlines s2)

, ignores = S.union (ignores s1) (ignores s2)

, autosize = S.union (autosize s1) (autosize s2)

, bounds = M.union (bounds s1) (bounds s2)

, defs = M.union (defs s1) (defs s2)

, autois = M.union (autois s1) (autois s2)

}

instance Monoid (Spec ty bndr) where

mappend = (<>)

mempty

= Spec { measures = []

, impSigs = []

, expSigs = []

, asmSigs = []

, sigs = []

, localSigs = []

, reflSigs = []

, invariants = []

, ialiases = []

, imports = []

, dataDecls = []

, newtyDecls = []

, includes = []

, aliases = []

, ealiases = []

, embeds = mempty

, qualifiers = []

, lvars = S.empty

, lazy = S.empty

, rewrites = S.empty

, rewriteWith = M.empty

, fails = S.empty

, autois = M.empty

, hmeas = S.empty

, reflects = S.empty

, hbounds = S.empty

, inlines = S.empty

, ignores = S.empty

, autosize = S.empty

, pragmas = []

, cmeasures = []

, imeasures = []

, classes = []

, claws = []

, relational = []

, asmRel = []

, termexprs = []

, rinstance = []

, ilaws = []

, dvariance = []

, dsize = []

, axeqs = []

, bounds = M.empty

, defs = M.empty

}

-- | A 'LiftedSpec' is derived from an input 'BareSpec' and a set of its dependencies.

data LiftedSpec = LiftedSpec

{ liftedMeasures :: HashSet (Measure LocBareType F.LocSymbol)

-- ^ User-defined properties for ADTs

, liftedImpSigs :: HashSet (F.Symbol, F.Sort)

-- ^ Imported variables types

, liftedExpSigs :: HashSet (F.Symbol, F.Sort)

-- ^ Exported variables types

, liftedAsmSigs :: HashSet (F.LocSymbol, LocBareType)

-- ^ Assumed (unchecked) types; including reflected signatures

, liftedSigs :: HashSet (F.LocSymbol, LocBareType)

-- ^ Imported functions and types

, liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareType)

-- ^ Data type invariants; the Maybe is the generating measure

, liftedIaliases :: HashSet (LocBareType, LocBareType)

-- ^ Data type invariants to be checked

, liftedImports :: HashSet F.Symbol

-- ^ Loaded spec module names

, liftedDataDecls :: HashSet DataDecl

-- ^ Predicated data definitions

, liftedNewtyDecls :: HashSet DataDecl

-- ^ Predicated new type definitions

, liftedAliases :: HashSet (F.Located (RTAlias F.Symbol BareType))

-- ^ RefType aliases

, liftedEaliases :: HashSet (F.Located (RTAlias F.Symbol F.Expr))

-- ^ Expression aliases

, liftedEmbeds :: F.TCEmb F.LocSymbol

-- ^ GHC-Tycon-to-fixpoint Tycon map

, liftedQualifiers :: HashSet F.Qualifier

-- ^ Qualifiers in source/spec files

, liftedLvars :: HashSet F.LocSymbol

-- ^ Variables that should be checked in the environment they are used

, liftedAutois :: M.HashMap F.LocSymbol (Maybe Int)

-- ^ Automatically instantiate axioms in these Functions with maybe specified fuel

, liftedAutosize :: HashSet F.LocSymbol

-- ^ Type Constructors that get automatically sizing info

, liftedCmeasures :: HashSet (Measure LocBareType ())

-- ^ Measures attached to a type-class

, liftedImeasures :: HashSet (Measure LocBareType F.LocSymbol)

-- ^ Mappings from (measure,type) -> measure

, liftedClasses :: HashSet (RClass LocBareType)

-- ^ Refined Type-Classes

, liftedClaws :: HashSet (RClass LocBareType)

-- ^ Refined Type-Classe Laws

, liftedRinstance :: HashSet (RInstance LocBareType)

, liftedIlaws :: HashSet (RILaws LocBareType)

, liftedDsize :: [([LocBareType], F.LocSymbol)]

, liftedDvariance :: HashSet (F.LocSymbol, [Variance])

-- ^ ? Where do these come from ?!

, liftedBounds :: RRBEnv LocBareType

, liftedDefs :: M.HashMap F.LocSymbol F.Symbol

-- ^ Temporary (?) hack to deal with dictionaries in specifications

-- see tests/pos/NatClass.hs

, liftedAxeqs :: HashSet F.Equation

-- ^ Equalities used for Proof-By-Evaluation

} deriving (Eq, Generic, Show)

deriving Hashable via Generically LiftedSpec

deriving Binary via Generically LiftedSpec

instance Binary F.Equation

emptyLiftedSpec :: LiftedSpec

emptyLiftedSpec = LiftedSpec

{ liftedMeasures = mempty

, liftedImpSigs = mempty

, liftedExpSigs = mempty

, liftedAsmSigs = mempty

, liftedSigs = mempty

, liftedInvariants = mempty

, liftedIaliases = mempty

, liftedImports = mempty

, liftedDataDecls = mempty

, liftedNewtyDecls = mempty

, liftedAliases = mempty

, liftedEaliases = mempty

, liftedEmbeds = mempty

, liftedQualifiers = mempty

, liftedLvars = mempty

, liftedAutois = mempty

, liftedAutosize = mempty

, liftedCmeasures = mempty

, liftedImeasures = mempty

, liftedClasses = mempty

, liftedClaws = mempty

, liftedRinstance = mempty

, liftedIlaws = mempty

, liftedDvariance = mempty

, liftedDsize = mempty

, liftedBounds = mempty

, liftedDefs = mempty

, liftedAxeqs = mempty

}

-- | The /target/ dependencies that concur to the creation of a 'TargetSpec' and a 'LiftedSpec'.

newtype TargetDependencies =

TargetDependencies { getDependencies :: HashMap StableModule LiftedSpec }

deriving (Eq, Show, Generic)

deriving Binary via Generically TargetDependencies

instance Semigroup TargetDependencies where

x <> y = TargetDependencies

{ getDependencies = getDependencies x <> getDependencies y

}

instance Monoid TargetDependencies where

mempty = TargetDependencies mempty

-- | Drop the given 'StableModule' from the dependencies.

dropDependency :: StableModule -> TargetDependencies -> TargetDependencies

dropDependency sm (TargetDependencies deps) = TargetDependencies (M.delete sm deps)

-- | Returns 'True' if the input 'Var' is a /PLE/ one.

isPLEVar :: TargetSpec -> Var -> Bool

isPLEVar sp x = M.member x (gsAutoInst (gsRefl sp))

-- | Returns 'True' if the input 'Var' was exported in the module the input 'TargetSrc' represents.

isExportedVar :: TargetSrc -> Var -> Bool

isExportedVar src v = mkStableName n `S.member` ns

where

n = getName v

ns = gsExports src

data GhcSrc = Src

{ _giTarget :: !FilePath -- ^ Source file for module

, _giTargetMod :: !ModName -- ^ Name for module

, _giCbs :: ![CoreBind] -- ^ Source Code

, _gsTcs :: ![TyCon] -- ^ All used Type constructors

, _gsCls :: !(Maybe [ClsInst]) -- ^ Class instances?

, _giDerVars :: !(S.HashSet Var) -- ^ Binders created by GHC eg dictionaries

, _giImpVars :: ![Var] -- ^ Binders that are _read_ in module (but not defined?)

, _giDefVars :: ![Var] -- ^ (Top-level) binders that are _defined_ in module

, _giUseVars :: ![Var] -- ^ Binders that are _read_ in module

, _gsExports :: !(HashSet StableName) -- ^ `Name`s exported by the module being verified

, _gsFiTcs :: ![TyCon] -- ^ Family instance TyCons

, _gsFiDcs :: ![(F.Symbol, DataCon)] -- ^ Family instance DataCons

, _gsPrimTcs :: ![TyCon] -- ^ Primitive GHC TyCons (from TysPrim.primTyCons)

, _gsQualImps :: !QImports -- ^ Map of qualified imports

, _gsAllImps :: !(S.HashSet F.Symbol) -- ^ Set of _all_ imported modules

, _gsTyThings :: ![TyThing] -- ^ All the @TyThing@s known to GHC

}

data GhcSpec = SP

{ _gsSig :: !GhcSpecSig

, _gsQual :: !GhcSpecQual

, _gsData :: !GhcSpecData

, _gsName :: !GhcSpecNames

, _gsVars :: !GhcSpecVars

, _gsTerm :: !GhcSpecTerm

, _gsRefl :: !GhcSpecRefl

, _gsLaws :: !GhcSpecLaws

, _gsImps :: ![(F.Symbol, F.Sort)] -- ^ Imported Environment

, _gsConfig :: !Config

, _gsLSpec :: !(Spec LocBareType F.LocSymbol) -- ^ Lifted specification for the target module

}

instance HasConfig GhcSpec where

getConfig = _gsConfig

toTargetSrc :: GhcSrc -> TargetSrc

toTargetSrc a = TargetSrc

{ giTarget = _giTarget a

, giTargetMod = _giTargetMod a

, giCbs = _giCbs a

, gsTcs = _gsTcs a

, gsCls = _gsCls a

, giDerVars = _giDerVars a

, giImpVars = _giImpVars a

, giDefVars = _giDefVars a

, giUseVars = _giUseVars a

, gsExports = _gsExports a

, gsFiTcs = _gsFiTcs a

, gsFiDcs = _gsFiDcs a

, gsPrimTcs = _gsPrimTcs a

, gsQualImps = _gsQualImps a

, gsAllImps = _gsAllImps a

, gsTyThings = _gsTyThings a

}

fromTargetSrc :: TargetSrc -> GhcSrc

fromTargetSrc a = Src

{ _giTarget = giTarget a

, _giTargetMod = giTargetMod a

, _giCbs = giCbs a

, _gsTcs = gsTcs a

, _gsCls = gsCls a

, _giDerVars = giDerVars a

, _giImpVars = giImpVars a

, _giDefVars = giDefVars a

, _giUseVars = giUseVars a

, _gsExports = gsExports a

, _gsFiTcs = gsFiTcs a

, _gsFiDcs = gsFiDcs a

, _gsPrimTcs = gsPrimTcs a

, _gsQualImps = gsQualImps a

, _gsAllImps = gsAllImps a

, _gsTyThings = gsTyThings a

}

toTargetSpec :: GhcSpec -> (TargetSpec, LiftedSpec)

toTargetSpec ghcSpec =

(targetSpec, (toLiftedSpec . _gsLSpec) ghcSpec)

where

targetSpec = TargetSpec

{ gsSig = _gsSig ghcSpec

, gsQual = _gsQual ghcSpec

, gsData = _gsData ghcSpec

, gsName = _gsName ghcSpec

, gsVars = _gsVars ghcSpec

, gsTerm = _gsTerm ghcSpec

, gsRefl = _gsRefl ghcSpec

, gsLaws = _gsLaws ghcSpec

, gsImps = _gsImps ghcSpec

, gsConfig = _gsConfig ghcSpec

}

toBareSpec :: Spec LocBareType F.LocSymbol -> BareSpec

toBareSpec = MkBareSpec

fromBareSpec :: BareSpec -> Spec LocBareType F.LocSymbol

fromBareSpec = getBareSpec

toLiftedSpec :: Spec LocBareType F.LocSymbol -> LiftedSpec

toLiftedSpec a = LiftedSpec

{ liftedMeasures = S.fromList . measures $ a

, liftedImpSigs = S.fromList . impSigs $ a

, liftedExpSigs = S.fromList . expSigs $ a

, liftedAsmSigs = S.fromList . asmSigs $ a

, liftedSigs = S.fromList . sigs $ a

, liftedInvariants = S.fromList . invariants $ a

, liftedIaliases = S.fromList . ialiases $ a

, liftedImports = S.fromList . imports $ a

, liftedDataDecls = S.fromList . dataDecls $ a

, liftedNewtyDecls = S.fromList . newtyDecls $ a

, liftedAliases = S.fromList . aliases $ a

, liftedEaliases = S.fromList . ealiases $ a

, liftedEmbeds = embeds a

, liftedQualifiers = S.fromList . qualifiers $ a

, liftedLvars = lvars a

, liftedAutois = autois a

, liftedAutosize = autosize a

, liftedCmeasures = S.fromList . cmeasures $ a

, liftedImeasures = S.fromList . imeasures $ a

, liftedClasses = S.fromList . classes $ a

, liftedClaws = S.fromList . claws $ a

, liftedRinstance = S.fromList . rinstance $ a

, liftedIlaws = S.fromList . ilaws $ a

, liftedDvariance = S.fromList . dvariance $ a

, liftedDsize = dsize a

, liftedBounds = bounds a

, liftedDefs = defs a

, liftedAxeqs = S.fromList . axeqs $ a

}

unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType F.LocSymbol

unsafeFromLiftedSpec a = Spec

{ measures = S.toList . liftedMeasures $ a

, impSigs = S.toList . liftedImpSigs $ a

, expSigs = S.toList . liftedExpSigs $ a

, asmSigs = S.toList . liftedAsmSigs $ a

, sigs = S.toList . liftedSigs $ a

, localSigs = mempty

, reflSigs = mempty

, relational = mempty

, asmRel = mempty

, invariants = S.toList . liftedInvariants $ a

, ialiases = S.toList . liftedIaliases $ a

, imports = S.toList . liftedImports $ a

, dataDecls = S.toList . liftedDataDecls $ a

, newtyDecls = S.toList . liftedNewtyDecls $ a

, includes = mempty

, aliases = S.toList . liftedAliases $ a

, ealiases = S.toList . liftedEaliases $ a

, embeds = liftedEmbeds a

, qualifiers = S.toList . liftedQualifiers $ a

, lvars = liftedLvars a

, lazy = mempty

, fails = mempty

, rewrites = mempty

, rewriteWith = mempty

, reflects = mempty

, autois = liftedAutois a

, hmeas = mempty

, hbounds = mempty

, inlines = mempty

, ignores = mempty

, autosize = liftedAutosize a

, pragmas = mempty

, cmeasures = S.toList . liftedCmeasures $ a

, imeasures = S.toList . liftedImeasures $ a

, classes = S.toList . liftedClasses $ a

, claws = S.toList . liftedClaws $ a

, termexprs = mempty

, rinstance = S.toList . liftedRinstance $ a

, ilaws = S.toList . liftedIlaws $ a

, dvariance = S.toList . liftedDvariance $ a

, dsize = liftedDsize a

, bounds = liftedBounds a

, defs = liftedDefs a

, axeqs = S.toList . liftedAxeqs $ a

}