<commit_before>{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TupleSections        #-}
{-# LANGUAGE EmptyDataDecls       #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}


module Language.Haskell.Liquid.Constraint.Types
  ( -- * Constraint Generation Monad
    CG

    -- * Constraint information
  , CGInfo (..)

    -- * Constraint Generation Environment
  , CGEnv (..)

    -- * Logical constraints (FIXME: related to bounds?)
  , LConstraint (..)

    -- * Fixpoint environment
  , FEnv (..)
  , initFEnv
  , insertsFEnv
  -- , removeFEnv

   -- * Hole Environment
  , HEnv
  , fromListHEnv
  , elemHEnv

   -- * Subtyping Constraints
  , SubC (..)
  , FixSubC

  , subVar

   -- * Well-formedness Constraints
  , WfC (..)
  , FixWfC

   -- * Invariants
  , RTyConInv
  , mkRTyConInv
  , addRTyConInv
  , addRInv

  -- * Aliases?
  , RTyConIAl
  , mkRTyConIAl

  , removeInvariant, restoreInvariant, makeRecInvariants

  , addArgument, addArguments

  , getTemplates
  ) where

import Prelude hiding (error)
import           CoreSyn
import           Type (TyThing( AnId ))
import           Var
import           SrcLoc
import           Unify (tcUnifyTy)
import qualified TyCon   as TC
import qualified DataCon as DC
import           Text.PrettyPrint.HughesPJ hiding ((<>)) 
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
import qualified Data.List           as L
import           Control.DeepSeq
import           Data.Maybe               (catMaybes, isJust)
import           Control.Monad.State
-- import           Control.Monad.Fail 

import           Language.Haskell.Liquid.GHC.SpanStack
import           Language.Haskell.Liquid.Types hiding   (binds)
-- import           Language.Haskell.Liquid.Types.Strata
import           Language.Haskell.Liquid.Misc           (fourth4)
-- import           Language.Haskell.Liquid.Types.RefType  (shiftVV, toType)
import           Language.Haskell.Liquid.WiredIn        (wiredSortedSyms)
import qualified Language.Fixpoint.Types            as F
import Language.Fixpoint.Misc

import qualified Language.Haskell.Liquid.UX.CTags      as Tg

type CG = State CGInfo

data CGEnv = CGE
  { cgLoc    :: !SpanStack         -- ^ Location in original source file
  , renv     :: !REnv              -- ^ SpecTypes for Bindings in scope
  , syenv    :: !(F.SEnv Var)      -- ^ Map from free Symbols (e.g. datacons) to Var
  , denv     :: !RDEnv             -- ^ Dictionary Environment
  , litEnv   :: !(F.SEnv F.Sort)   -- ^ Global  literals
  , constEnv :: !(F.SEnv F.Sort)   -- ^ Distinct literals
  , fenv   :: !FEnv              -- ^ Fixpoint Environment
  , recs   :: !(S.HashSet Var)   -- ^ recursive defs being processed (for annotations)
  , fargs  :: !(S.HashSet Var)   -- ^ recursive defs being processed (for annotations)
  , invs   :: !RTyConInv         -- ^ Datatype invariants
  , rinvs  :: !RTyConInv         -- ^ Datatype recursive invariants: ignored in the base case assumed in rec call
  , ial    :: !RTyConIAl         -- ^ Datatype checkable invariants
  , grtys  :: !REnv              -- ^ Top-level variables with (assert)-guarantees to verify
  , assms  :: !REnv              -- ^ Top-level variables with assumed types
  , intys  :: !REnv              -- ^ Top-level variables with auto generated internal types
  , emb    :: F.TCEmb TC.TyCon   -- ^ How to embed GHC Tycons into fixpoint sorts
  , tgEnv  :: !Tg.TagEnv          -- ^ Map from top-level binders to fixpoint tag
  , tgKey  :: !(Maybe Tg.TagKey)                     -- ^ Current top-level binder
  , trec   :: !(Maybe (M.HashMap F.Symbol SpecType)) -- ^ Type of recursive function with decreasing constraints
  , lcb    :: !(M.HashMap F.Symbol CoreExpr)         -- ^ Let binding that have not been checked (c.f. LAZYVARs)
  , forallcb :: !(M.HashMap Var F.Expr)              -- ^ Polymorhic let bindings 
  , holes  :: !HEnv                                  -- ^ Types with holes, will need refreshing
  , lcs    :: !LConstraint                           -- ^ Logical Constraints
  , aenv   :: !(M.HashMap Var F.Symbol)              -- ^ axiom environment maps reflected Haskell functions to the logical functions
  , cerr   :: !(Maybe (TError SpecType))             -- ^ error that should be reported at the user
  -- , cgCfg  :: !Config                                -- ^ top-level config options
  , cgInfo :: !GhcInfo                               -- ^ top-level GhcInfo
  , cgVar  :: !(Maybe Var)                           -- ^ top level function being checked
  } -- deriving (Data, Typeable)

instance HasConfig CGEnv where
  getConfig = getConfig . cgInfo

data LConstraint = LC [[(F.Symbol, SpecType)]]

instance Monoid LConstraint where
  mempty  = LC []
  mappend = (<>)

instance Semigroup LConstraint where
  LC cs1 <> LC cs2 = LC (cs1 ++ cs2)

instance PPrint CGEnv where<commit_msg>do we still need forallcb?<commit_after>{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TupleSections        #-}
{-# LANGUAGE EmptyDataDecls       #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}


module Language.Haskell.Liquid.Constraint.Types
  ( -- * Constraint Generation Monad
    CG

    -- * Constraint information
  , CGInfo (..)

    -- * Constraint Generation Environment
  , CGEnv (..)

    -- * Logical constraints (FIXME: related to bounds?)
  , LConstraint (..)

    -- * Fixpoint environment
  , FEnv (..)
  , initFEnv
  , insertsFEnv
  -- , removeFEnv

   -- * Hole Environment
  , HEnv
  , fromListHEnv
  , elemHEnv

   -- * Subtyping Constraints
  , SubC (..)
  , FixSubC

  , subVar

   -- * Well-formedness Constraints
  , WfC (..)
  , FixWfC

   -- * Invariants
  , RTyConInv
  , mkRTyConInv
  , addRTyConInv
  , addRInv

  -- * Aliases?
  , RTyConIAl
  , mkRTyConIAl

  , removeInvariant, restoreInvariant, makeRecInvariants

  , addArgument, addArguments

  , getTemplates
  ) where

import Prelude hiding (error)
import           CoreSyn
import           Type (TyThing( AnId ))
import           Var
import           SrcLoc
import           Unify (tcUnifyTy)
import qualified TyCon   as TC
import qualified DataCon as DC
import           Text.PrettyPrint.HughesPJ hiding ((<>)) 
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
import qualified Data.List           as L
import           Control.DeepSeq
import           Data.Maybe               (catMaybes, isJust)
import           Control.Monad.State
-- import           Control.Monad.Fail 

import           Language.Haskell.Liquid.GHC.SpanStack
import           Language.Haskell.Liquid.Types hiding   (binds)
-- import           Language.Haskell.Liquid.Types.Strata
import           Language.Haskell.Liquid.Misc           (fourth4)
-- import           Language.Haskell.Liquid.Types.RefType  (shiftVV, toType)
import           Language.Haskell.Liquid.WiredIn        (wiredSortedSyms)
import qualified Language.Fixpoint.Types            as F
import Language.Fixpoint.Misc

import qualified Language.Haskell.Liquid.UX.CTags      as Tg

type CG = State CGInfo

data CGEnv = CGE
  { cgLoc    :: !SpanStack         -- ^ Location in original source file
  , renv     :: !REnv              -- ^ SpecTypes for Bindings in scope
  , syenv    :: !(F.SEnv Var)      -- ^ Map from free Symbols (e.g. datacons) to Var
  , denv     :: !RDEnv             -- ^ Dictionary Environment
  , litEnv   :: !(F.SEnv F.Sort)   -- ^ Global  literals
  , constEnv :: !(F.SEnv F.Sort)   -- ^ Distinct literals
  , fenv   :: !FEnv              -- ^ Fixpoint Environment
  , recs   :: !(S.HashSet Var)   -- ^ recursive defs being processed (for annotations)
  , fargs  :: !(S.HashSet Var)   -- ^ recursive defs being processed (for annotations)
  , invs   :: !RTyConInv         -- ^ Datatype invariants
  , rinvs  :: !RTyConInv         -- ^ Datatype recursive invariants: ignored in the base case assumed in rec call
  , ial    :: !RTyConIAl         -- ^ Datatype checkable invariants
  , grtys  :: !REnv              -- ^ Top-level variables with (assert)-guarantees to verify
  , assms  :: !REnv              -- ^ Top-level variables with assumed types
  , intys  :: !REnv              -- ^ Top-level variables with auto generated internal types
  , emb    :: F.TCEmb TC.TyCon   -- ^ How to embed GHC Tycons into fixpoint sorts
  , tgEnv  :: !Tg.TagEnv          -- ^ Map from top-level binders to fixpoint tag
  , tgKey  :: !(Maybe Tg.TagKey)                     -- ^ Current top-level binder
  , trec   :: !(Maybe (M.HashMap F.Symbol SpecType)) -- ^ Type of recursive function with decreasing constraints
  , lcb    :: !(M.HashMap F.Symbol CoreExpr)         -- ^ Let binding that have not been checked (c.f. LAZYVARs)
  , holes  :: !HEnv                                  -- ^ Types with holes, will need refreshing
  , lcs    :: !LConstraint                           -- ^ Logical Constraints
  , aenv   :: !(M.HashMap Var F.Symbol)              -- ^ axiom environment maps reflected Haskell functions to the logical functions
  , cerr   :: !(Maybe (TError SpecType))             -- ^ error that should be reported at the user
  -- , cgCfg  :: !Config                                -- ^ top-level config options
  , cgInfo :: !GhcInfo                               -- ^ top-level GhcInfo
  , cgVar  :: !(Maybe Var)                           -- ^ top level function being checked
  } -- deriving (Data, Typeable)

instance HasConfig CGEnv where
  getConfig = getConfig . cgInfo

data LConstraint = LC [[(F.Symbol, SpecType)]]

instance Monoid LConstraint where
  mempty  = LC []
  mappend = (<>)

instance Semigroup LConstraint where
  LC cs1 <> LC cs2 = LC (cs1 ++ cs2)

instance PPrint CGEnv where
{'fraction_non_alphanumeric': 0.10304641177673278, 'fraction_numerical': 0.0010222858311183807, 'mean_word_length': 2.0194444444444444, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6073521', 'n_tokens_mistral': 3108, 'n_tokens_neox': 2983, 'n_words': 832}