<commit_before>{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-} 
{-# LANGUAGE OverlappingInstances  #-}
{-# LANGUAGE ViewPatterns          #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE OverloadedStrings     #-}

-- | This module should contain all the global type definitions and basic instances.

module Language.Haskell.Liquid.Types (

  -- * Options
    Config (..), canonicalizePaths
  
  -- * Ghc Information
  , GhcInfo (..)
  , GhcSpec (..)
  , TargetVars (..)

  -- * Located Things
  , Located (..)
  , dummyLoc

  -- * Symbols
  , LocSymbol
  , LocText

  -- * Default unknown name
  , dummyName, isDummy

  -- * Refinement Types 
  , RType (..), Ref(..), RTProp (..)
  , RTyCon(..), TyConInfo(..)
  , RTyVar (..)
  , RTAlias (..)

  -- * Classes describing operations on `RTypes` 
  , TyConable (..)
  , RefTypable (..)
  , SubsTy (..)

  -- * Refinements
  , PVar (..)
  , Predicate (..)
  , UReft(..)

  -- * Parse-time entities describing refined data types
  , DataDecl (..)
  , DataConP (..)
  , TyConP (..)

  -- * Pre-instantiated RType
  , RRType, BRType, RRProp
  , BSort, BPVar

  -- * Instantiated RType
  , BareType, RefType, PrType
  , SpecType, SpecProp 
  , RSort
  , UsedPVar, RPVar, RReft
  , REnv (..)

  -- * Constructing & Destructing RTypes
  , RTypeRep(..), fromRTypeRep, toRTypeRep
  , mkArrow, bkArrowDeep, bkArrow, safeBkArrow 
  , mkUnivs, bkUniv, bkClass
  , rFun

  -- * Manipulating `Predicates`
  , pvars, pappSym, pToRef, pApp

  -- * Some tests on RTypes
  , isBase
  , isFunTy
  , isTrivial

  -- * Traversing `RType` 
  , efoldReft, foldReft
  , mapReft, mapReftM
  , mapBot, mapBind
 
  -- * ???
  , Oblig(..)
  , ignoreOblig
  , addTermCond
  , addInvCond


  -- * Inferred Annotations 
  , AnnInfo (..)
  , Annot (..)

  -- * Overall Output
  , Output (..)

  -- * Refinement Hole
  , hole, isHole

  -- * Converting To and From Sort
  , ofRSort, toRSort
  , rTypeValueVar
  , rTypeReft
  , stripRTypeBase 

  -- * Class for values that can be pretty printed 
  , PPrint (..)
  , showpp
   
  -- * Printer Configuration 
  , PPEnv (..)
  , Tidy  (..)
  , ppEnv
  , ppEnvShort

  -- * Modules and Imports
  , ModName (..), ModType (..)
  , isSrcImport, isSpecImport
  , getModName, getModString

  -- * Refinement Type Aliases
  , RTEnv (..)
  , RTBareOrSpec
  , mapRT
  , mapRP

  -- * Final Result
  , Result (..)

  -- * Errors and Error Messages
  , Error
  , TError (..)
  , EMsg (..)
  , LParseError (..)
  , ErrorResult
  , errSpan
  , errOther

  -- * Source information (associated with constraints)
  , Cinfo (..)

  -- * Measures
  , Measure (..)
  , CMeasure (..)
  , Def (..)
  , Body (..)

  -- * Type Classes
  , RClass (..)

  -- * KV Profiling
  , KVKind (..)   -- types of kvars
  , KVProf        -- profile table
  , emptyKVProf   -- empty profile
  , updKVProf     -- extend profile

  -- * Misc 
  , classToRApp
  , mapRTAVars
  , insertsSEnv

  -- * Strata
  , Stratum(..), Strata
  , isSVar
  , getStrata
  , makeDivType, makeFinType

  )
  where

import FastString                               (fsLit)
import SrcLoc                                   (noSrcSpan, mkGeneralSrcSpan, SrcSpan)
import TyCon
import DataCon
import Name                                     (getName)
import NameSet
import Module                                   (moduleNameFS)
import Class                                    (classTyCon)
import TypeRep                          hiding  (maybeParen, pprArrowChain)  
import Var
import Unique
import Literal
import Text.Printf
import GHC                                      (Class, HscEnv, ModuleName, Name, moduleNameString)
import GHC.Generics
import Language.Haskell.Liquid.GhcMisc 

import Control.Arrow                            (second)
import Control.Monad                            (liftM, liftM2, liftM3)
import qualified Control.Monad.Error as Ex
import Control.DeepSeq
import Control.Applicative                      ((<$>), (<*>))
import Data.Typeable                            (Typeable)
import Data.Generics                            (Data)   
import Data.Monoid                              hiding ((<>))
import qualified  Data.Foldable as F
import            Data.Hashable
import qualified  Data.HashMap.Strict as M
import qualified  Data.HashSet as S
import            Data.Function                (on)
import            Data.Maybe                   (maybeToList, fromMaybe)
import            Data.Traversable             hiding (mapM)
import            Data.List                    (isSuffixOf, nub, union, unionBy)
import            Data.Text                    (Text)
import qualified  Data.Text                    as T
import            Data.Aeson        hiding     (Result)      
import Text.Parsec.Pos              (SourcePos, newPos, sourceName, sourceLine, sourceColumn) 
import Text.Parsec.Error            (ParseError) 
import Text.PrettyPrint.HughesPJ    
import Language.Fixpoint.Config     hiding (Config) 
import Language.Fixpoint.Misc
import Language.Fixpoint.Types      hiding (Predicate, Def, R)
-- import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Names      (symSepName, isSuffixOfSym, singletonSym)
import CoreSyn (CoreBind)

import System.Directory (canonicalizePath)
import System.FilePath ((</>), isAbsolute, takeDirectory)
import System.Posix.Files (getFileStatus, isDirectory)

import Data.Default
-----------------------------------------------------------------------------
-- | Command Line Config Options --------------------------------------------
-----------------------------------------------------------------------------

-- NOTE: adding strictness annotations breaks the help message
data Config = Config { 
    files          :: [FilePath] -- ^ source files to check
  , idirs          :: [FilePath] -- ^ path to directory for including specs
  , diffcheck      :: Bool       -- ^ check subset of binders modified (+ dependencies) since last check 
  , real           :: Bool       -- ^ supports real number arithmetic
  , fullcheck      :: Bool       -- ^ check all binders (overrides diffcheck)
  , binders        :: [String]   -- ^ set of binders to check
  , noCheckUnknown :: Bool       -- ^ whether to complain about specifications for unexported and unused values
  , notermination  :: Bool       -- ^ disable termination check
  , nocaseexpand   :: Bool       -- ^ disable case expand
  , strata         :: Bool       -- ^ enable strata analysis
  , notruetypes    :: Bool       -- ^ disable truing top level types
  , totality       :: Bool       -- ^ check totality in definitions
  , noPrune        :: Bool       -- ^ disable prunning unsorted Refinements
  , maxParams      :: Int        -- ^ the maximum number of parameters to accept when mining qualifiers
  , smtsolver      :: SMTSolver  -- ^ name of smtsolver to use [default: z3-API]
  , shortNames     :: Bool       -- ^ drop module qualifers from pretty-printed names.
  , shortErrors    :: Bool       -- ^ don't show subtyping errors and contexts. 
  , ghcOptions     :: [String]   -- ^ command-line options to pass to GHC
  , cFiles         :: [String]   -- ^ .c files to compile and link against (for GHC)
  } deriving (Data, Typeable, Show, Eq)

-- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
--   to worry about relative paths.
canonicalizePaths :: Config -> FilePath -> IO Config
canonicalizePaths cfg tgt
  = do st  <- getFileStatus tgt
       tgt <- canonicalizePath tgt
       let canonicalize f
             | isAbsolute f   = return f
             | isDirectory st = canonicalizePath (tgt </> f)
             | otherwise      = canonicalizePath (takeDirectory tgt </> f)
       is <- mapM canonicalize $ idirs cfg
       cs <- mapM canonicalize $ cFiles cfg
       return $ cfg { idirs = is, cFiles = cs }


-----------------------------------------------------------------------------
-- | Printer ----------------------------------------------------------------
-----------------------------------------------------------------------------

data Tidy = Lossy | Full deriving (Eq, Ord)

class PPrint a where
  pprint     :: a -> Doc

  pprintTidy :: Tidy -> a -> Doc
  pprintTidy _ = pprint

showpp :: (PPrint a) => a -> String 
showpp = render . pprint 

showEMsg :: (PPrint a) => a -> EMsg 
showEMsg = EMsg . showpp 

instance PPrint a => PPrint (Maybe a) where
  pprint = maybe (text "Nothing") ((text "Just" <+>) . pprint)

instance PPrint a => PPrint [a] where
  pprint = brackets . intersperse comma . map pprint

instance (PPrint a, PPrint b) => PPrint (a,b) where
  pprint (x, y)  = pprint x <+> text ":" <+> pprint y

data PPEnv 
  = PP { ppPs    :: Bool
       , ppTyVar :: Bool -- TODO if set to True all Bare fails
       , ppSs    :: Bool
       , ppShort :: Bool
       }

ppEnv           = ppEnvPrintPreds
ppEnvCurrent    = PP False False False False
ppEnvPrintPreds = PP True False False False
ppEnvShort pp   = pp { ppShort = True }



------------------------------------------------------------------
-- | GHC Information :  Code & Spec ------------------------------
------------------------------------------------------------------
 
data GhcInfo = GI { 
    env      :: !HscEnv
  , cbs      :: ![CoreBind]
  , derVars  :: ![Var]
  , impVars  :: ![Var]
  , defVars  :: ![Var]
  , useVars  :: ![Var]
  , hqFiles  :: ![FilePath]
  , imports  :: ![String]
  , includes :: ![FilePath]
  , spec     :: !GhcSpec
  }

-- | The following is the overall type for /specifications/ obtained from
-- parsing the target source and dependent libraries

data GhcSpec = SP {
    tySigs     :: ![(Var, Located SpecType)]     -- ^ Asserted Reftypes
                                                 -- eg.  see include/Prelude.spec
  , asmSigs    :: ![(Var, Located SpecType)]     -- ^ Assumed Reftypes
  , ctors      :: ![(Var, Located SpecType)]     -- ^ Data Constructor Measure Sigs
                                                 -- eg.  (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }
  , meas       :: ![(Symbol, Located RefType)]   -- ^ Measure Types  
                                                 -- eg.  len :: [a] -> Int
  , invariants :: ![Located SpecType]            -- ^ Data Type Invariants

  , ialiases   :: ![(Located SpecType, Located SpecType)] -- ^ Data Type Invariant Aliases
                                                 -- eg.  forall a. {v: [a] | len(v) >= 0}
  , dconsP     :: ![(DataCon, DataConP)]         -- ^ Predicated Data-Constructors
                                                 -- e.g. see tests/pos/Map.hs
  , tconsP     :: ![(TyCon, TyConP)]             -- ^ Predicated Type-Constructors
                                                 -- eg.  see tests/pos/Map.hs
  , freeSyms   :: ![(Symbol, Var)]               -- ^ List of `Symbol` free in spec and corresponding GHC var 
                                                 -- eg. (Cons, Cons#7uz) from tests/pos/ex1.hs
  , tcEmbeds   :: TCEmb TyCon                    -- ^ How to embed GHC Tycons into fixpoint sorts
                                                 -- e.g. "embed Set as Set_set" from include/Data/Set.spec
  , qualifiers :: ![Qualifier]                   -- ^ Qualifiers in Source/Spec files
                                                 -- e.g tests/pos/qualTest.hs
  , tgtVars    :: ![Var]                         -- ^ Top-level Binders To Verify (empty means ALL binders)
  , decr       :: ![(Var, [Int])]                -- ^ Lexicographically ordered size witnesses for termination
  , texprs     :: ![(Var, [Expr])]               -- ^ Lexicographically ordered expressions for termination
  , lvars      :: !(S.HashSet Var)               -- ^ Variables that should be checked in the environment they are used
  , lazy       :: !(S.HashSet Var)               -- ^ Binders to IGNORE during termination checking
  , config     :: !Config                        -- ^ Configuration Options
  , exports    :: !NameSet                       -- ^ `Name`s exported by the module being verified
  , measures   :: [Measure SpecType DataCon]
  , tyconEnv   :: M.HashMap TyCon RTyCon
  }


data TyConP = TyConP { freeTyVarsTy :: ![RTyVar]
                     , freePredTy   :: ![PVar RSort]
                     , freeLabelTy  :: ![Symbol]
                     , covPs        :: ![Int]    -- ^ indexes of covariant predicate arguments
                     , contravPs    :: ![Int]    -- ^ indexes of contravariant predicate arguments
                     , sizeFun      :: !(Maybe (Symbol -> Expr))
                     } deriving (Data, Typeable)

data DataConP = DataConP { dc_loc     :: !SourcePos
                         , freeTyVars :: ![RTyVar]
                         , freePred   :: ![PVar RSort]
                         , freeLabels :: ![Symbol]
                         , tyConsts   :: ![SpecType]
                         , tyArgs     :: ![(Symbol, SpecType)]
                         , tyRes      :: !SpecType
                         } deriving (Data, Typeable)


-- | Which Top-Level Binders Should be Verified
data TargetVars = AllVars | Only ![Var]


--------------------------------------------------------------------
-- | Predicate Variables -------------------------------------------
--------------------------------------------------------------------

data PVar t
  = PV { pname :: !Symbol
       , ptype :: !t
       , parg  :: !Symbol
       , pargs :: ![(t, Symbol, Expr)]
       }
	deriving (Generic, Data, Typeable, Show)

instance Eq (PVar t) where
  pv == pv' = pname pv == pname pv' {- UNIFY: What about: && eqArgs pv pv' -}

instance Ord (PVar t) where
  compare (PV n _ _ _)  (PV n' _ _ _) = compare n n'
<commit_msg>adding PVKind<commit_after>{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-} 
{-# LANGUAGE OverlappingInstances  #-}
{-# LANGUAGE ViewPatterns          #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE OverloadedStrings     #-}

-- | This module should contain all the global type definitions and basic instances.

module Language.Haskell.Liquid.Types (

  -- * Options
    Config (..), canonicalizePaths
  
  -- * Ghc Information
  , GhcInfo (..)
  , GhcSpec (..)
  , TargetVars (..)

  -- * Located Things
  , Located (..)
  , dummyLoc

  -- * Symbols
  , LocSymbol
  , LocText

  -- * Default unknown name
  , dummyName, isDummy

  -- * Refinement Types 
  , RType (..), Ref(..), RTProp (..)
  , RTyCon(..), TyConInfo(..)
  , RTyVar (..)
  , RTAlias (..)

  -- * Classes describing operations on `RTypes` 
  , TyConable (..)
  , RefTypable (..)
  , SubsTy (..)

  -- * Refinements
  , PVar (..)
  , PVKind (..)
  , Predicate (..)
  , UReft(..)

  -- * Parse-time entities describing refined data types
  , DataDecl (..)
  , DataConP (..)
  , TyConP (..)

  -- * Pre-instantiated RType
  , RRType, BRType, RRProp
  , BSort, BPVar

  -- * Instantiated RType
  , BareType, RefType, PrType
  , SpecType, SpecProp 
  , RSort
  , UsedPVar, RPVar, RReft
  , REnv (..)

  -- * Constructing & Destructing RTypes
  , RTypeRep(..), fromRTypeRep, toRTypeRep
  , mkArrow, bkArrowDeep, bkArrow, safeBkArrow 
  , mkUnivs, bkUniv, bkClass
  , rFun

  -- * Manipulating `Predicates`
  , pvars, pappSym, pToRef, pApp

  -- * Some tests on RTypes
  , isBase
  , isFunTy
  , isTrivial

  -- * Traversing `RType` 
  , efoldReft, foldReft
  , mapReft, mapReftM
  , mapBot, mapBind
 
  -- * ???
  , Oblig(..)
  , ignoreOblig
  , addTermCond
  , addInvCond


  -- * Inferred Annotations 
  , AnnInfo (..)
  , Annot (..)

  -- * Overall Output
  , Output (..)

  -- * Refinement Hole
  , hole, isHole

  -- * Converting To and From Sort
  , ofRSort, toRSort
  , rTypeValueVar
  , rTypeReft
  , stripRTypeBase 

  -- * Class for values that can be pretty printed 
  , PPrint (..)
  , showpp
   
  -- * Printer Configuration 
  , PPEnv (..)
  , Tidy  (..)
  , ppEnv
  , ppEnvShort

  -- * Modules and Imports
  , ModName (..), ModType (..)
  , isSrcImport, isSpecImport
  , getModName, getModString

  -- * Refinement Type Aliases
  , RTEnv (..)
  , RTBareOrSpec
  , mapRT
  , mapRP

  -- * Final Result
  , Result (..)

  -- * Errors and Error Messages
  , Error
  , TError (..)
  , EMsg (..)
  , LParseError (..)
  , ErrorResult
  , errSpan
  , errOther

  -- * Source information (associated with constraints)
  , Cinfo (..)

  -- * Measures
  , Measure (..)
  , CMeasure (..)
  , Def (..)
  , Body (..)

  -- * Type Classes
  , RClass (..)

  -- * KV Profiling
  , KVKind (..)   -- types of kvars
  , KVProf        -- profile table
  , emptyKVProf   -- empty profile
  , updKVProf     -- extend profile

  -- * Misc 
  , classToRApp
  , mapRTAVars
  , insertsSEnv

  -- * Strata
  , Stratum(..), Strata
  , isSVar
  , getStrata
  , makeDivType, makeFinType

  )
  where

import FastString                               (fsLit)
import SrcLoc                                   (noSrcSpan, mkGeneralSrcSpan, SrcSpan)
import TyCon
import DataCon
import Name                                     (getName)
import NameSet
import Module                                   (moduleNameFS)
import Class                                    (classTyCon)
import TypeRep                          hiding  (maybeParen, pprArrowChain)  
import Var
import Unique
import Literal
import Text.Printf
import GHC                                      (Class, HscEnv, ModuleName, Name, moduleNameString)
import GHC.Generics
import Language.Haskell.Liquid.GhcMisc 

import Control.Arrow                            (second)
import Control.Monad                            (liftM, liftM2, liftM3)
import qualified Control.Monad.Error as Ex
import Control.DeepSeq
import Control.Applicative                      ((<$>), (<*>))
import Data.Typeable                            (Typeable)
import Data.Generics                            (Data)   
import Data.Monoid                              hiding ((<>))
import qualified  Data.Foldable as F
import            Data.Hashable
import qualified  Data.HashMap.Strict as M
import qualified  Data.HashSet as S
import            Data.Function                (on)
import            Data.Maybe                   (maybeToList, fromMaybe)
import            Data.Traversable             hiding (mapM)
import            Data.List                    (isSuffixOf, nub, union, unionBy)
import            Data.Text                    (Text)
import qualified  Data.Text                    as T
import            Data.Aeson        hiding     (Result)      
import Text.Parsec.Pos              (SourcePos, newPos, sourceName, sourceLine, sourceColumn) 
import Text.Parsec.Error            (ParseError) 
import Text.PrettyPrint.HughesPJ    
import Language.Fixpoint.Config     hiding (Config) 
import Language.Fixpoint.Misc
import Language.Fixpoint.Types      hiding (Predicate, Def, R)
-- import qualified Language.Fixpoint.Types as F
import Language.Fixpoint.Names      (symSepName, isSuffixOfSym, singletonSym)
import CoreSyn (CoreBind)

import System.Directory (canonicalizePath)
import System.FilePath ((</>), isAbsolute, takeDirectory)
import System.Posix.Files (getFileStatus, isDirectory)

import Data.Default
-----------------------------------------------------------------------------
-- | Command Line Config Options --------------------------------------------
-----------------------------------------------------------------------------

-- NOTE: adding strictness annotations breaks the help message
data Config = Config { 
    files          :: [FilePath] -- ^ source files to check
  , idirs          :: [FilePath] -- ^ path to directory for including specs
  , diffcheck      :: Bool       -- ^ check subset of binders modified (+ dependencies) since last check 
  , real           :: Bool       -- ^ supports real number arithmetic
  , fullcheck      :: Bool       -- ^ check all binders (overrides diffcheck)
  , binders        :: [String]   -- ^ set of binders to check
  , noCheckUnknown :: Bool       -- ^ whether to complain about specifications for unexported and unused values
  , notermination  :: Bool       -- ^ disable termination check
  , nocaseexpand   :: Bool       -- ^ disable case expand
  , strata         :: Bool       -- ^ enable strata analysis
  , notruetypes    :: Bool       -- ^ disable truing top level types
  , totality       :: Bool       -- ^ check totality in definitions
  , noPrune        :: Bool       -- ^ disable prunning unsorted Refinements
  , maxParams      :: Int        -- ^ the maximum number of parameters to accept when mining qualifiers
  , smtsolver      :: SMTSolver  -- ^ name of smtsolver to use [default: z3-API]
  , shortNames     :: Bool       -- ^ drop module qualifers from pretty-printed names.
  , shortErrors    :: Bool       -- ^ don't show subtyping errors and contexts. 
  , ghcOptions     :: [String]   -- ^ command-line options to pass to GHC
  , cFiles         :: [String]   -- ^ .c files to compile and link against (for GHC)
  } deriving (Data, Typeable, Show, Eq)

-- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have
--   to worry about relative paths.
canonicalizePaths :: Config -> FilePath -> IO Config
canonicalizePaths cfg tgt
  = do st  <- getFileStatus tgt
       tgt <- canonicalizePath tgt
       let canonicalize f
             | isAbsolute f   = return f
             | isDirectory st = canonicalizePath (tgt </> f)
             | otherwise      = canonicalizePath (takeDirectory tgt </> f)
       is <- mapM canonicalize $ idirs cfg
       cs <- mapM canonicalize $ cFiles cfg
       return $ cfg { idirs = is, cFiles = cs }


-----------------------------------------------------------------------------
-- | Printer ----------------------------------------------------------------
-----------------------------------------------------------------------------

data Tidy = Lossy | Full deriving (Eq, Ord)

class PPrint a where
  pprint     :: a -> Doc

  pprintTidy :: Tidy -> a -> Doc
  pprintTidy _ = pprint

showpp :: (PPrint a) => a -> String 
showpp = render . pprint 

showEMsg :: (PPrint a) => a -> EMsg 
showEMsg = EMsg . showpp 

instance PPrint a => PPrint (Maybe a) where
  pprint = maybe (text "Nothing") ((text "Just" <+>) . pprint)

instance PPrint a => PPrint [a] where
  pprint = brackets . intersperse comma . map pprint

instance (PPrint a, PPrint b) => PPrint (a,b) where
  pprint (x, y)  = pprint x <+> text ":" <+> pprint y

data PPEnv 
  = PP { ppPs    :: Bool
       , ppTyVar :: Bool -- TODO if set to True all Bare fails
       , ppSs    :: Bool
       , ppShort :: Bool
       }

ppEnv           = ppEnvPrintPreds
ppEnvCurrent    = PP False False False False
ppEnvPrintPreds = PP True False False False
ppEnvShort pp   = pp { ppShort = True }



------------------------------------------------------------------
-- | GHC Information :  Code & Spec ------------------------------
------------------------------------------------------------------
 
data GhcInfo = GI { 
    env      :: !HscEnv
  , cbs      :: ![CoreBind]
  , derVars  :: ![Var]
  , impVars  :: ![Var]
  , defVars  :: ![Var]
  , useVars  :: ![Var]
  , hqFiles  :: ![FilePath]
  , imports  :: ![String]
  , includes :: ![FilePath]
  , spec     :: !GhcSpec
  }

-- | The following is the overall type for /specifications/ obtained from
-- parsing the target source and dependent libraries

data GhcSpec = SP {
    tySigs     :: ![(Var, Located SpecType)]     -- ^ Asserted Reftypes
                                                 -- eg.  see include/Prelude.spec
  , asmSigs    :: ![(Var, Located SpecType)]     -- ^ Assumed Reftypes
  , ctors      :: ![(Var, Located SpecType)]     -- ^ Data Constructor Measure Sigs
                                                 -- eg.  (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }
  , meas       :: ![(Symbol, Located RefType)]   -- ^ Measure Types  
                                                 -- eg.  len :: [a] -> Int
  , invariants :: ![Located SpecType]            -- ^ Data Type Invariants

  , ialiases   :: ![(Located SpecType, Located SpecType)] -- ^ Data Type Invariant Aliases
                                                 -- eg.  forall a. {v: [a] | len(v) >= 0}
  , dconsP     :: ![(DataCon, DataConP)]         -- ^ Predicated Data-Constructors
                                                 -- e.g. see tests/pos/Map.hs
  , tconsP     :: ![(TyCon, TyConP)]             -- ^ Predicated Type-Constructors
                                                 -- eg.  see tests/pos/Map.hs
  , freeSyms   :: ![(Symbol, Var)]               -- ^ List of `Symbol` free in spec and corresponding GHC var 
                                                 -- eg. (Cons, Cons#7uz) from tests/pos/ex1.hs
  , tcEmbeds   :: TCEmb TyCon                    -- ^ How to embed GHC Tycons into fixpoint sorts
                                                 -- e.g. "embed Set as Set_set" from include/Data/Set.spec
  , qualifiers :: ![Qualifier]                   -- ^ Qualifiers in Source/Spec files
                                                 -- e.g tests/pos/qualTest.hs
  , tgtVars    :: ![Var]                         -- ^ Top-level Binders To Verify (empty means ALL binders)
  , decr       :: ![(Var, [Int])]                -- ^ Lexicographically ordered size witnesses for termination
  , texprs     :: ![(Var, [Expr])]               -- ^ Lexicographically ordered expressions for termination
  , lvars      :: !(S.HashSet Var)               -- ^ Variables that should be checked in the environment they are used
  , lazy       :: !(S.HashSet Var)               -- ^ Binders to IGNORE during termination checking
  , config     :: !Config                        -- ^ Configuration Options
  , exports    :: !NameSet                       -- ^ `Name`s exported by the module being verified
  , measures   :: [Measure SpecType DataCon]
  , tyconEnv   :: M.HashMap TyCon RTyCon
  }


data TyConP = TyConP { freeTyVarsTy :: ![RTyVar]
                     , freePredTy   :: ![PVar RSort]
                     , freeLabelTy  :: ![Symbol]
                     , covPs        :: ![Int]    -- ^ indexes of covariant predicate arguments
                     , contravPs    :: ![Int]    -- ^ indexes of contravariant predicate arguments
                     , sizeFun      :: !(Maybe (Symbol -> Expr))
                     } deriving (Data, Typeable)

data DataConP = DataConP { dc_loc     :: !SourcePos
                         , freeTyVars :: ![RTyVar]
                         , freePred   :: ![PVar RSort]
                         , freeLabels :: ![Symbol]
                         , tyConsts   :: ![SpecType]
                         , tyArgs     :: ![(Symbol, SpecType)]
                         , tyRes      :: !SpecType
                         } deriving (Data, Typeable)


-- | Which Top-Level Binders Should be Verified
data TargetVars = AllVars | Only ![Var]


--------------------------------------------------------------------
-- | Predicate Variables -------------------------------------------
--------------------------------------------------------------------

data PVar t
  = PV { pname :: !Symbol
       , ptype :: !(PVKind t)
       , parg  :: !Symbol
       , pargs :: ![(t, Symbol, Expr)]
       }
    deriving (Generic, Data, Typeable, Show)

data PVKind t
  = PVProp t | PVHProp
    deriving (Generic, Data, Typeable, Show)

instance Eq (PVar t) where
  pv == pv' = pname pv == pname pv' {- UNIFY: What about: && eqArgs pv pv' -}

instance Ord (PVar t) where
  compare (PV n _ _ _)  (PV n' _ _ _) = compare n n'

{'fraction_non_alphanumeric': 0.16195492493460892, 'fraction_numerical': 0.0005016302984700275, 'mean_word_length': 1.5092151398004137, 'pattern_counts': {'":': 2, '<': 29, '<?xml version=': 0, '>': 55, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 50, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5308094', 'n_tokens_mistral': 8326, 'n_tokens_neox': 7955, 'n_words': 2268}