<commit_before>{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts, PatternGuards, FlexibleInstances #-}
{-# LANGUAGE CPP #-}
module PTS.Statics.Typing where

import Control.Monad
import Control.Monad.Environment
import Control.Monad.Errors.Class
import Control.Monad.Log
import Control.Monad.Reader
import Control.Monad.Trans

import Data.Set (Set)
import qualified Data.Set as Set

import PTS.Dynamics
import PTS.Error
import PTS.Instances
import PTS.Options
import PTS.Syntax

import Text.PrettyPrint.HughesPJ hiding (int)
import Text.Show (Show (show))

-- implementation of pure type systems as described on p.98 in Barendregt's "Lambda Calculi with Types"
-- ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z
-- Restrictions: The PTS must be full and functional

-- some ideas regarding conversion to algorithmic style have been taken
-- from van Benthem et al's "Checking algorithms for Pure Type Systems"
-- http://www.springerlink.com/content/f510r63138068632/
--

-- Bidirectional type checking following the first part of:
-- <NAME> and <NAME>. Local Type Inference. In
-- ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
-- (POPL), San Diego, California, 1998. Full version in ACM
-- Transactions on Programming Languages and Systems (TOPLAS), 22(1),
-- January 2000, pp. 1-44.
-- Full version: http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf

import Debug.Trace

-- safe bind
safebind :: MonadEnvironment Name (Binding Eval) m => Name -> Value Eval -> Maybe C -> Term -> (Name -> Term -> m a) -> m a
safebind x t s b f = do
  result <- lookupType x
  case result of
    Nothing -> do
      bind x (Binding False (ResidualVar x) t s) (f x b)
    Just _ -> do
      vars <- keys
      let nx = freshvarl (freevars b `Set.union` vars) x
      bind nx (Binding False (ResidualVar nx) t s) (f nx (subst b x (mkVar nx)))

debug :: (MonadEnvironment Name (Binding Eval) m, MonadLog m) => String -> Term -> m (TypedTerm Eval) -> m (TypedTerm Eval)
debug n t result = do
#ifndef DEBUG_TYPING
  result
#else
  enter n
  ctx <- getEnvironment
  -- log $ "Context: " ++ showCtx [(n, (x, y)) | (n, (_, x, y)) <- ctx]
  log $ "Subject: " ++ showPretty t
  x <- result
  log $ "Result:  " ++ showPretty x
  tx <- liftEval (reify (typeOf x))
  log $ "         : " ++ showPretty tx
  exit
  return x
#endif

debugPush ::
  (MonadEnvironment Name (Binding Eval) m, MonadLog m) =>
  String -> Term -> Value Eval -> m (TypedTerm Eval) -> m (TypedTerm Eval)
debugPush n t q result = do
#ifndef DEBUG_TYPING
  result
#else
  enter n
  ctx <- getEnvironment
  -- log $ "Context: " ++ showCtx [(n, (bindingValue b, bindingType b)) | (n, b) <- ctx]
  log $ "Subject: " ++ showPretty t
  q <- liftEval (reify q)
  log $ "Push type: " ++ showPretty q
  x <- result
  log $ "Result:  " ++ showPretty x
  tx <- liftEval (reify (typeOf x))
  log $ "         : " ++ showPretty tx
  exit
  return x
#endif


-- error messages and generic error checking

checkProperType t context info = do
  let t' = typeOf t
  pts <- asks optInstance
  env <- getEnvironment

  case t' of
    Constant s | sorts pts s -> return s
    _ -> do
      t' <- liftEval (reify t')
      prettyFail $ msgNotProperType context info t t'

msgNotProperType context info t t'
  = text "Type Error" <+> context <+> text ": Expected proper type" <+> info <> text "." $$ nest 2 (
    sep [text "Explanation:", nest 2 (text "The type is not a sort, so the term is not a proper type and therefore not valid at this position.")] $$
    sep [text "Term:", nest 2 (pretty 0 t)] $$
    sep [text "Type:", nest 2 (pretty 0 t')])

checkLamBodyHasSort body s1 context = do
  pts <- asks optInstance
  s2 <- case sortOf body of
    Just s | sorts pts s -> return s
    Just s -> fail "Internal Error."
    Nothing -> do
      rangeT <- liftEval . reify . typeOf $ body
      prettyFail $ msgBodyNoSort (text "in lambda abstraction") body rangeT

  s3 <- prettyRelations pts s1 s2
  return (s2, s3)

-- adapted from msgNotProperType.
msgBodyNoSort context body t
  = text "Type Error" <+> context <+> text ": Expected function body to have a sort." $$ nest 2 (
    sep [text "Explanation:", nest 2 (text "The function body does not have a sort, that is, its type has no type. Therefore this term cannot be used as a function body.")] $$
    sep [text "Body:", nest 2 (pretty 0 body)] $$
    sep [text "Type:", nest 2 (pretty 0 t)])

checkIsEquiv s' t' s t context info1 info2 = do
  same <- liftEval (equiv s' t') 
  if same
    then return ()
    else do
      s'' <- liftEval (reify s')
      t'' <- liftEval (reify t')
      prettyFail $ msgNotSame context info1 info2 s t s'' t''

msgNotSame context info1 info2 s t s' t'
  = let (s'', t'') = showDiff 0 (diff (strip s') (strip t'))
     in text "Type Error" <+> context <> text ": Types do not match." $$ nest 2 (
        sep [text "Explanation:", nest 2 (text "The types of the" <+> info1 <+> text "and the" <+> info2 <+> text "should be beta-equivalent.")] $$
        sep [info1 <> text ":", nest 2 (pretty 0 s)] $$
        sep [info2 <> text ":", nest 2 (pretty 0 t)] $$
        sep [text "Type of" <+> info1 <> text ":", nest 2 (text s'')] $$
        sep [text "Type of" <+> info2 <> text ":", nest 2 (text t'')])

normalizeToInt :: (MonadLog m, Functor m, MonadEnvironment Name (Binding Eval) m, MonadReader Options m, MonadErrors Errors m) => TypedTerm Eval -> TypedTerm Eval -> Doc -> Doc -> m (TypedTerm Eval)
normalizeToInt t' t context info = do
  env <- getEnvironment
  expected <- typecheckPull (mkConst int)
  if equivTerm env t' expected
    then return expected
    else let t'' = nbe env t'
          in prettyFail $ msgNotInt context info t t'' int

msgNotInt context info t t' int
  = let expected :: Term
        expected = mkConst int in
    text "Type Error" <+> context <> text ": Types do not match." $$ nest 2 (
    sep [text "Explanation:", nest 2 (text "The type of the" <+> info <+> text "should be beta-equivalent to" <+> pretty 0 expected <> text ".")] $$
    sep [info <> text ":", nest 2 (pretty 0 t)] $$
    sep [text "Type of" <+> info <> text ":", nest 2 (pretty 0 t')] $$
    sep [text "Expected Type:" <+> nest 2 (pretty 0 expected)])

liftEval :: MonadEnvironment Name (Binding Eval) m => Eval a -> m a
liftEval action = do
  env <- getEnvironment
  return (runEval env action)

checkIsPi ::
  (MonadReader Options m, MonadErrors Errors m, MonadEnvironment Name (Binding Eval) m) =>
  Value Eval -> TypedTerm Eval -> Doc -> Doc -> m (Value Eval)
checkIsPi v t context info = do
  case v of
    result@(PiType _ _ _ _) ->
      return result
    _ -> do
      t' <- liftEval $ reify v<commit_msg>Drop unused normalizeToInt<commit_after>{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts, PatternGuards, FlexibleInstances #-}
{-# LANGUAGE CPP #-}
module PTS.Statics.Typing where

import Control.Monad
import Control.Monad.Environment
import Control.Monad.Errors.Class
import Control.Monad.Log
import Control.Monad.Reader
import Control.Monad.Trans

import Data.Set (Set)
import qualified Data.Set as Set

import PTS.Dynamics
import PTS.Error
import PTS.Instances
import PTS.Options
import PTS.Syntax

import Text.PrettyPrint.HughesPJ hiding (int)
import Text.Show (Show (show))

-- implementation of pure type systems as described on p.98 in Barendregt's "Lambda Calculi with Types"
-- ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z
-- Restrictions: The PTS must be full and functional

-- some ideas regarding conversion to algorithmic style have been taken
-- from <NAME> et al's "Checking algorithms for Pure Type Systems"
-- http://www.springerlink.com/content/f510r63138068632/
--

-- Bidirectional type checking following the first part of:
-- <NAME> and <NAME>. Local Type Inference. In
-- ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
-- (POPL), San Diego, California, 1998. Full version in ACM
-- Transactions on Programming Languages and Systems (TOPLAS), 22(1),
-- January 2000, pp. 1-44.
-- Full version: http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf

import Debug.Trace

-- safe bind
safebind :: MonadEnvironment Name (Binding Eval) m => Name -> Value Eval -> Maybe C -> Term -> (Name -> Term -> m a) -> m a
safebind x t s b f = do
  result <- lookupType x
  case result of
    Nothing -> do
      bind x (Binding False (ResidualVar x) t s) (f x b)
    Just _ -> do
      vars <- keys
      let nx = freshvarl (freevars b `Set.union` vars) x
      bind nx (Binding False (ResidualVar nx) t s) (f nx (subst b x (mkVar nx)))

debug :: (MonadEnvironment Name (Binding Eval) m, MonadLog m) => String -> Term -> m (TypedTerm Eval) -> m (TypedTerm Eval)
debug n t result = do
#ifndef DEBUG_TYPING
  result
#else
  enter n
  ctx <- getEnvironment
  -- log $ "Context: " ++ showCtx [(n, (x, y)) | (n, (_, x, y)) <- ctx]
  log $ "Subject: " ++ showPretty t
  x <- result
  log $ "Result:  " ++ showPretty x
  tx <- liftEval (reify (typeOf x))
  log $ "         : " ++ showPretty tx
  exit
  return x
#endif

debugPush ::
  (MonadEnvironment Name (Binding Eval) m, MonadLog m) =>
  String -> Term -> Value Eval -> m (TypedTerm Eval) -> m (TypedTerm Eval)
debugPush n t q result = do
#ifndef DEBUG_TYPING
  result
#else
  enter n
  ctx <- getEnvironment
  -- log $ "Context: " ++ showCtx [(n, (bindingValue b, bindingType b)) | (n, b) <- ctx]
  log $ "Subject: " ++ showPretty t
  q <- liftEval (reify q)
  log $ "Push type: " ++ showPretty q
  x <- result
  log $ "Result:  " ++ showPretty x
  tx <- liftEval (reify (typeOf x))
  log $ "         : " ++ showPretty tx
  exit
  return x
#endif


-- error messages and generic error checking

checkProperType t context info = do
  let t' = typeOf t
  pts <- asks optInstance
  env <- getEnvironment

  case t' of
    Constant s | sorts pts s -> return s
    _ -> do
      t' <- liftEval (reify t')
      prettyFail $ msgNotProperType context info t t'

msgNotProperType context info t t'
  = text "Type Error" <+> context <+> text ": Expected proper type" <+> info <> text "." $$ nest 2 (
    sep [text "Explanation:", nest 2 (text "The type is not a sort, so the term is not a proper type and therefore not valid at this position.")] $$
    sep [text "Term:", nest 2 (pretty 0 t)] $$
    sep [text "Type:", nest 2 (pretty 0 t')])

checkLamBodyHasSort body s1 context = do
  pts <- asks optInstance
  s2 <- case sortOf body of
    Just s | sorts pts s -> return s
    Just s -> fail "Internal Error."
    Nothing -> do
      rangeT <- liftEval . reify . typeOf $ body
      prettyFail $ msgBodyNoSort (text "in lambda abstraction") body rangeT

  s3 <- prettyRelations pts s1 s2
  return (s2, s3)

-- adapted from msgNotProperType.
msgBodyNoSort context body t
  = text "Type Error" <+> context <+> text ": Expected function body to have a sort." $$ nest 2 (
    sep [text "Explanation:", nest 2 (text "The function body does not have a sort, that is, its type has no type. Therefore this term cannot be used as a function body.")] $$
    sep [text "Body:", nest 2 (pretty 0 body)] $$
    sep [text "Type:", nest 2 (pretty 0 t)])

checkIsEquiv s' t' s t context info1 info2 = do
  same <- liftEval (equiv s' t') 
  if same
    then return ()
    else do
      s'' <- liftEval (reify s')
      t'' <- liftEval (reify t')
      prettyFail $ msgNotSame context info1 info2 s t s'' t''

msgNotSame context info1 info2 s t s' t'
  = let (s'', t'') = showDiff 0 (diff (strip s') (strip t'))
     in text "Type Error" <+> context <> text ": Types do not match." $$ nest 2 (
        sep [text "Explanation:", nest 2 (text "The types of the" <+> info1 <+> text "and the" <+> info2 <+> text "should be beta-equivalent.")] $$
        sep [info1 <> text ":", nest 2 (pretty 0 s)] $$
        sep [info2 <> text ":", nest 2 (pretty 0 t)] $$
        sep [text "Type of" <+> info1 <> text ":", nest 2 (text s'')] $$
        sep [text "Type of" <+> info2 <> text ":", nest 2 (text t'')])

liftEval :: MonadEnvironment Name (Binding Eval) m => Eval a -> m a
liftEval action = do
  env <- getEnvironment
  return (runEval env action)

checkIsPi ::
  (MonadReader Options m, MonadErrors Errors m, MonadEnvironment Name (Binding Eval) m) =>
  Value Eval -> TypedTerm Eval -> Doc -> Doc -> m (Value Eval)
checkIsPi v t context info = do
  case v of
    result@(PiType _ _ _ _) ->
      return result
    _ -> do
      t' <- liftEval $ reify v
{'fraction_non_alphanumeric': 0.12760627121383547, 'fraction_numerical': 0.01204137708097624, 'mean_word_length': 3.011345218800648, 'pattern_counts': {'":': 17, '<': 102, '<?xml version=': 0, '>': 125, 'https://': 0, 'lorem ipsum': 0, 'www.': 4, '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': '1337059', 'n_tokens_mistral': 4271, 'n_tokens_neox': 3999, 'n_words': 1629}