<commit_before>{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances, FlexibleInstances, TemplateHaskell #-}
{-|
  A module containing the routines necessary to construct a skeletal environment
  for the type decision prodecure.
-}
module Language.K3.TypeSystem.TypeDecision.SkeletalEnvironment
( TSkelAliasEnv
, TypeDecideSkelM
, StubInfo(..)
, constructSkeletalAEnv
) where

import Control.Applicative
import Control.Arrow
import Control.Monad.Trans
import Control.Monad.Trans.Writer
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import qualified Data.Traversable as Trav

import Language.K3.Core.Annotation
import Language.K3.Core.Declaration
import Language.K3.Core.Type
import Language.K3.Logger
import Language.K3.Pretty
import qualified Language.K3.TypeSystem.ConstraintSetLike as CSL
import Language.K3.TypeSystem.Annotations
import Language.K3.TypeSystem.Data
import Language.K3.TypeSystem.Error
import Language.K3.TypeSystem.Monad.Iface.FreshVar
import Language.K3.TypeSystem.Monad.Iface.TypeError
import Language.K3.TypeSystem.TypeDecision.AnnotationInlining
import Language.K3.TypeSystem.TypeDecision.Data
import Language.K3.TypeSystem.TypeDecision.Monad
import Language.K3.TypeSystem.Utils
import Language.K3.TypeSystem.Utils.K3Tree

$(loggingFunctions)

-- |A type alias for skeletal type alias environments.
type TSkelAliasEnv = TEnv (TypeAliasEntry StubbedConstraintSet)

-- |A type alias for the skeletal construction monad.  The writer output maps
--  each used stub to the information associated with it.
type TypeDecideSkelM = WriterT (Map Stub StubInfo) TypeDecideM

-- |A data type for tracking the information suspended by a stub.
data StubInfo
  = StubInfo
    { stubTypeExpr :: K3 Type
        -- ^ The type expression deferred by this stub.
    , stubVar :: QVar
        -- ^ The type variable to be bounded by the type expression.
    , stubParamEnv :: TParamEnv
        -- ^ The type parameter environment for the annotation in this stub.
    }
  deriving (Show)

instance TypeErrorI TypeDecideSkelM where
  typeError = lift . typeError

-- |A function which constructs a skeletal type environment for the type
--  decision procedure.
constructSkeletalAEnv :: FlatAnnotationDecls -> TypeDecideSkelM TSkelAliasEnv
constructSkeletalAEnv anns = do
  -- First, get a structure for each declaration
  base <- Trav.mapM constructTypeForDecl anns
  _debug $ boxToString $
    ["Base skeletal environment: "] %+ indent 2 (
        vconcats $ map (\(k,(b,p,scs)) -> [k] %+ [" → "] %+
                          prettyLines (AnnType p b scs)) $
                      Map.toList base
      )
  -- Next, join all of the constraint sets together (because each annotation can
  -- refer to the others) and make an environment from it.
  let scs = CSL.unions $ map ((\(_,_,scs') -> scs') . snd) $ Map.toList base
  let aEnv = Map.fromList $
              map (\(i,(b,p,_)) ->
                  (TEnvIdentifier i, AnnAlias $ AnnType p b scs)) $
                Map.toList base
  _debug $ boxToString $
    ["Skeletal environment: "] %+ indent 2 (
        vconcats $ map (\(k,v) -> prettyLines k %+ [" → "] %+ prettyLines v) $
                      Map.toList aEnv
      )
  return aEnv

-- |Constructs a skeletal type environment for a single declaration.
constructTypeForDecl :: (FlatAnnotation, K3 Declaration)
                             -> TypeDecideSkelM
                                  (AnnBodyType, TParamEnv, StubbedConstraintSet)
constructTypeForDecl ((lAtts,sAtts),decl) = do
  u <- uidOf decl
  -- Prepare an appropriate environment
  aP_c <- lift $ freshUVar $ TVarSourceOrigin u
  aP_f <- lift $ freshUVar $ TVarSourceOrigin u
  aP_s <- lift $ freshUVar $ TVarSourceOrigin u
  let p = Map.fromList [ (TEnvIdContent, aP_c)
                       , (TEnvIdFinal, aP_f)
                       , (TEnvIdSelf, aP_s) ]
  -- Calculate the horizon part of the schema and the constraints generated by
  -- it.  Note that we do not constraint a_Hp to be a subtype of a_C; the
  -- horizon will be the GLB of those two types.
  (sAttTs, scs_H) <- second mconcat <$> unzip <$>
                      gatherParallelSkelErrors (map (memDeclToMemType p) sAtts)
  (a_Hp, cs_Hp) <- liftEither (AnnotationDepolarizationFailure u) $
                    depolarize sAttTs
  -- Calculate the type of self and the corresponding constraints
  (lAttTs, scs_S) <- second mconcat <$> unzip <$>
                      gatherParallelSkelErrors (map (memDeclToMemType p) lAtts)
  let b = AnnBodyType lAttTs sAttTs
  let annType = AnnType p b csEmpty
  inst <- lift $ instantiateCollection annType aP_c
  (a_S,cs_S) <- liftEither (InvalidCollectionInstantiation u) inst
  -- Construct an appropriate stubbed constraint set
  let cs = csUnions [cs_S,cs_Hp,csFromList
                      [aP_f <: a_Hp, a_S <: aP_s] ]
  let scs = CSL.unions [scs_H, scs_S, CSL.promote cs]
  -- We now have a result for a single annotation
  return (b,p,scs)
  where<commit_msg>Added missing constraint.<commit_after>{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances, FlexibleInstances, TemplateHaskell #-}
{-|
  A module containing the routines necessary to construct a skeletal environment
  for the type decision prodecure.
-}
module Language.K3.TypeSystem.TypeDecision.SkeletalEnvironment
( TSkelAliasEnv
, TypeDecideSkelM
, StubInfo(..)
, constructSkeletalAEnv
) where

import Control.Applicative
import Control.Arrow
import Control.Monad.Trans
import Control.Monad.Trans.Writer
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import qualified Data.Traversable as Trav

import Language.K3.Core.Annotation
import Language.K3.Core.Declaration
import Language.K3.Core.Type
import Language.K3.Logger
import Language.K3.Pretty
import qualified Language.K3.TypeSystem.ConstraintSetLike as CSL
import Language.K3.TypeSystem.Annotations
import Language.K3.TypeSystem.Data
import Language.K3.TypeSystem.Error
import Language.K3.TypeSystem.Monad.Iface.FreshVar
import Language.K3.TypeSystem.Monad.Iface.TypeError
import Language.K3.TypeSystem.TypeDecision.AnnotationInlining
import Language.K3.TypeSystem.TypeDecision.Data
import Language.K3.TypeSystem.TypeDecision.Monad
import Language.K3.TypeSystem.Utils
import Language.K3.TypeSystem.Utils.K3Tree

$(loggingFunctions)

-- |A type alias for skeletal type alias environments.
type TSkelAliasEnv = TEnv (TypeAliasEntry StubbedConstraintSet)

-- |A type alias for the skeletal construction monad.  The writer output maps
--  each used stub to the information associated with it.
type TypeDecideSkelM = WriterT (Map Stub StubInfo) TypeDecideM

-- |A data type for tracking the information suspended by a stub.
data StubInfo
  = StubInfo
    { stubTypeExpr :: K3 Type
        -- ^ The type expression deferred by this stub.
    , stubVar :: QVar
        -- ^ The type variable to be bounded by the type expression.
    , stubParamEnv :: TParamEnv
        -- ^ The type parameter environment for the annotation in this stub.
    }
  deriving (Show)

instance TypeErrorI TypeDecideSkelM where
  typeError = lift . typeError

-- |A function which constructs a skeletal type environment for the type
--  decision procedure.
constructSkeletalAEnv :: FlatAnnotationDecls -> TypeDecideSkelM TSkelAliasEnv
constructSkeletalAEnv anns = do
  -- First, get a structure for each declaration
  base <- Trav.mapM constructTypeForDecl anns
  _debug $ boxToString $
    ["Base skeletal environment: "] %+ indent 2 (
        vconcats $ map (\(k,(b,p,scs)) -> [k] %+ [" → "] %+
                          prettyLines (AnnType p b scs)) $
                      Map.toList base
      )
  -- Next, join all of the constraint sets together (because each annotation can
  -- refer to the others) and make an environment from it.
  let scs = CSL.unions $ map ((\(_,_,scs') -> scs') . snd) $ Map.toList base
  let aEnv = Map.fromList $
              map (\(i,(b,p,_)) ->
                  (TEnvIdentifier i, AnnAlias $ AnnType p b scs)) $
                Map.toList base
  _debug $ boxToString $
    ["Skeletal environment: "] %+ indent 2 (
        vconcats $ map (\(k,v) -> prettyLines k %+ [" → "] %+ prettyLines v) $
                      Map.toList aEnv
      )
  return aEnv

-- |Constructs a skeletal type environment for a single declaration.
constructTypeForDecl :: (FlatAnnotation, K3 Declaration)
                             -> TypeDecideSkelM
                                  (AnnBodyType, TParamEnv, StubbedConstraintSet)
constructTypeForDecl ((lAtts,sAtts),decl) = do
  u <- uidOf decl
  -- Prepare an appropriate environment
  aP_c <- lift $ freshUVar $ TVarSourceOrigin u
  aP_f <- lift $ freshUVar $ TVarSourceOrigin u
  aP_s <- lift $ freshUVar $ TVarSourceOrigin u
  let p = Map.fromList [ (TEnvIdContent, aP_c)
                       , (TEnvIdFinal, aP_f)
                       , (TEnvIdSelf, aP_s) ]
  -- Calculate the horizon part of the schema and the constraints generated by
  -- it.  Note that we do not constraint a_Hp to be a subtype of a_C; the
  -- horizon will be the GLB of those two types.
  (sAttTs, scs_H) <- second mconcat <$> unzip <$>
                      gatherParallelSkelErrors (map (memDeclToMemType p) sAtts)
  (a_Hp, cs_Hp) <- liftEither (AnnotationDepolarizationFailure u) $
                    depolarize sAttTs
  -- Calculate the type of self and the corresponding constraints
  (lAttTs, scs_S) <- second mconcat <$> unzip <$>
                      gatherParallelSkelErrors (map (memDeclToMemType p) lAtts)
  let b = AnnBodyType lAttTs sAttTs
  let annType = AnnType p b csEmpty
  inst <- lift $ instantiateCollection annType aP_c
  (a_S,cs_S) <- liftEither (InvalidCollectionInstantiation u) inst
  -- Construct an appropriate stubbed constraint set
  let cs = csUnions [cs_S,cs_Hp,csFromList
                      [aP_f <: a_Hp, aP_f <: aP_c, a_S <: aP_s] ]
  let scs = CSL.unions [scs_H, scs_S, CSL.promote cs]
  -- We now have a result for a single annotation
  return (b,p,scs)
  where
{'fraction_non_alphanumeric': 0.08545127076245747, 'fraction_numerical': 0.004402641584950971, 'mean_word_length': 3.051479529793271, 'pattern_counts': {'":': 0, '<': 36, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6540026', 'n_tokens_mistral': 3176, 'n_tokens_neox': 3039, 'n_words': 955}