<commit_before>{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE TemplateHaskell            #-}
module Ling.Check.Base where

import           Ling.Abs                  (Name)
import           Ling.Constraint
import           Ling.Equiv
import           Ling.ErrM
import           Ling.Norm
import           Ling.Print
import           Ling.Proto
import           Ling.Scoped
import           Ling.Session
import           Ling.Subst                (Subst, unScoped)
import           Ling.Utils                hiding (subst1)

import           Control.Lens
import           Control.Monad.Except
import           Control.Monad.Reader
import           Data.List                 (sort)
import           Data.Map                  (Map, empty)
import qualified Data.Set                  as Set

data ProcDef = ProcDef Name [ChanDec] Proc Proto

data TCEnv = TCEnv
  { _verbosity :: Verbosity
  , _evars     :: Map Name Typ
  -- ^ Term types
  , _edefs     :: Map Name Term
  -- ^ Term definitions
  , _pdefs     :: Map Name ProcDef
  -- ^ Processes definitions
  , _ddefs     :: Map Name [Name]
  -- ^ Datatypes definitions
  , _ctyps     :: Map Name Name
  -- ^ Data constructor ↦ type name
  }

$(makeLenses ''TCEnv)

emptyTCEnv :: TCEnv
emptyTCEnv = TCEnv False empty empty empty empty empty

newtype TC a = MkTC { unTC :: ReaderT TCEnv Err a }
  deriving (Functor, Applicative, Monad, MonadReader TCEnv)

instance MonadError String TC where
  throwError = MkTC . lift . Bad
  catchError = error "catchError: not implemented for TC"

checkEquality :: (Print a, Eq a) => String -> a -> a -> TC ()
checkEquality msg t0 t1 = assertEqual t0 t1
  [msg
  ,"Expected:"
  ,"  " ++ pretty t0
  ,"Inferred:"
  ,"  " ++ pretty t1
  ]

tcEqEnv :: TC EqEnv
tcEqEnv = emptyEqEnv <$> view edefs

checkEquivalence :: (Print a, Eq a, Equiv a, Subst a)
                 => String -> Scoped a -> Scoped a -> TC ()
checkEquivalence msg t0 t1 = do
  env <- tcEqEnv
  whenDebug $ do
    when (t0 /= t1) . debug $
      ["checkEquivalence:"
      ,"  " ++ pretty t0
      ,"against"
      ,"  " ++ pretty t1
      ]<commit_msg>Remove now unused ProcDef and pdefs from TCEnv<commit_after>{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE TemplateHaskell            #-}
module Ling.Check.Base where

import           Ling.Abs                  (Name)
import           Ling.Constraint
import           Ling.Equiv
import           Ling.ErrM
import           Ling.Norm
import           Ling.Print
import           Ling.Proto
import           Ling.Scoped
import           Ling.Session
import           Ling.Subst                (Subst, unScoped)
import           Ling.Utils                hiding (subst1)

import           Control.Lens
import           Control.Monad.Except
import           Control.Monad.Reader
import           Data.List                 (sort)
import           Data.Map                  (Map, empty)
import qualified Data.Set                  as Set

data TCEnv = TCEnv
  { _verbosity :: Verbosity
  , _evars     :: Map Name Typ
  -- ^ Term types
  , _edefs     :: Map Name Term
  -- ^ Term definitions
  , _ddefs     :: Map Name [Name]
  -- ^ Datatypes definitions
  , _ctyps     :: Map Name Name
  -- ^ Data constructor ↦ type name
  }

$(makeLenses ''TCEnv)

emptyTCEnv :: TCEnv
emptyTCEnv = TCEnv False empty empty empty empty

newtype TC a = MkTC { unTC :: ReaderT TCEnv Err a }
  deriving (Functor, Applicative, Monad, MonadReader TCEnv)

instance MonadError String TC where
  throwError = MkTC . lift . Bad
  catchError = error "catchError: not implemented for TC"

checkEquality :: (Print a, Eq a) => String -> a -> a -> TC ()
checkEquality msg t0 t1 = assertEqual t0 t1
  [msg
  ,"Expected:"
  ,"  " ++ pretty t0
  ,"Inferred:"
  ,"  " ++ pretty t1
  ]

tcEqEnv :: TC EqEnv
tcEqEnv = emptyEqEnv <$> view edefs

checkEquivalence :: (Print a, Eq a, Equiv a, Subst a)
                 => String -> Scoped a -> Scoped a -> TC ()
checkEquivalence msg t0 t1 = do
  env <- tcEqEnv
  whenDebug $ do
    when (t0 /= t1) . debug $
      ["checkEquivalence:"
      ,"  " ++ pretty t0
      ,"against"
      ,"  " ++ pretty t1
      ]
{'fraction_non_alphanumeric': 0.09837162614320767, 'fraction_numerical': 0.006245817532902075, 'mean_word_length': 1.8854568854568854, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3467652', 'n_tokens_mistral': 1468, 'n_tokens_neox': 1401, 'n_words': 419}