<commit_before>{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
--------------------------------------------------------------------
-- |
-- Module    :  Ermine.Unification.Kind
-- Copyright :  (c) <NAME> 2011-2013
-- License   :  BSD3
-- Maintainer:  <NAME> <<EMAIL>>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ermine.Unification.Kind
  ( MetaK, KindM
  , unifyKind
  , unifyKindVar
  , kindOccurs
  , generalize
  ) where

import Bound
import Control.Applicative
import Control.Arrow hiding ((<+>))
import Control.Lens
import Control.Monad.ST
import Control.Monad.ST.Class
import Control.Monad.State.Strict
import Control.Monad.Writer.Strict
import Data.IntMap as IntMap
import Data.IntSet as IntSet
import Data.Set as Set
import Data.Set.Lens
import Data.STRef
import Data.Traversable
import Ermine.Diagnostic
import Ermine.Syntax.Kind as Kind
import Ermine.Unification.Meta
import Ermine.Unification.Sharing
import Ermine.Pretty
import Ermine.Pretty.Kind

-- $setup
-- >>> :set -XFlexibleContexts -XConstraintKinds -XTypeFamilies
-- >>> import Ermine.Syntax
-- >>> import Text.Trifecta.Rendering
-- >>> let test :: (forall m s. (MonadWriter Any m, MonadMeta s m) => m (KindM s)) -> Schema b; test mk = fst $ runM_ emptyRendering (runWriterT (mk >>= generalize))

-- | A kind meta-variable
type MetaK s = Meta s Kind ()

-- | A kind filled with meta-variables
type KindM s = Kind (MetaK s)

-- | Die with an error message due to a cycle between the specified kinds.
--
-- >>> test $ do k <- Var <$> newMeta (); unifyKind mempty k (star ~> k)
-- *** Exception: (interactive):1:1: error: infinite kind detected
-- cyclic kind: a = * -> a
--
-- >>> test $ do k1 <- Var <$> newMeta (); k2 <- Var <$> newMeta (); unifyKind mempty k1 (k1 ~> k2); unifyKind mempty k2 (k1 ~> k2); return (k1 ~> k2)
-- *** Exception: (interactive):1:1: error: infinite kinds detected
-- cyclic kind: a = a -> b
-- cyclic kind: b = a -> b
kindOccurs :: (MonadMeta s m, MonadWriter Any m) => KindM s -> (MetaK s -> Bool) -> m (KindM s)
kindOccurs k p = occurs k p $ do
  zk <- zonk k
  let s = setOf kindVars zk
      m = IntMap.fromList $ zipWith (\m n -> (m^.metaId, n)) (Set.toList s) names
      v = m ^?! ix (s ^?! folded.filtered p.metaId)
  kd <- prettyKind zk False $ \v _ -> pure $ text $ m ^?! ix (v^.metaId)
  r <- view rendering
  throwM $ die r "infinite kind detected" & footnotes .~ [text "cyclic kind:" <+> hang 4 (group (pretty v </> char '=' </> kd))]
{-# INLINE kindOccurs #-}

-- | Generalize a 'Kind', checking for escaped Skolems.
generalize :: MonadMeta s m => KindM s -> m (Schema a)
generalize k0 = do
  k <- runSharing k0 $ zonk k0
  (r,(_,n)) <- runStateT (traverse go k) (IntMap.empty, 0)
  return $ Schema n (Scope r)
  where
   go Skolem{}   = StateT $ \ _ -> fail "escaped skolem"
   go (Meta _ i _ _ _) = StateT $ \imn@(im, n) -> case im^.at i of
     Just b  -> return (B b, imn)
     Nothing -> let n' = n + 1 in n' `seq` return (B n, (im & at i ?~ n, n'))

-- | Returns the a unified form if different from the left argument.
--<commit_msg>Fixed doctests: no more visited sets or multiple cycles<commit_after>{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
--------------------------------------------------------------------
-- |
-- Module    :  Ermine.Unification.Kind
-- Copyright :  (c) <NAME> 2011-2013
-- License   :  BSD3
-- Maintainer:  <NAME> <<EMAIL>>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ermine.Unification.Kind
  ( MetaK, KindM
  , unifyKind
  , unifyKindVar
  , kindOccurs
  , generalize
  ) where

import Bound
import Control.Applicative
import Control.Arrow hiding ((<+>))
import Control.Lens
import Control.Monad.ST
import Control.Monad.ST.Class
import Control.Monad.State.Strict
import Control.Monad.Writer.Strict
import Data.IntMap as IntMap
import Data.IntSet as IntSet
import Data.Set as Set
import Data.Set.Lens
import Data.STRef
import Data.Traversable
import Ermine.Diagnostic
import Ermine.Syntax.Kind as Kind
import Ermine.Unification.Meta
import Ermine.Unification.Sharing
import Ermine.Pretty
import Ermine.Pretty.Kind

-- $setup
-- >>> :set -XFlexibleContexts -XConstraintKinds -XTypeFamilies
-- >>> import Ermine.Syntax
-- >>> import Text.Trifecta.Rendering
-- >>> let test :: (forall m s. (MonadWriter Any m, MonadMeta s m) => m (KindM s)) -> Schema b; test mk = fst $ runM_ emptyRendering (runWriterT (mk >>= generalize))

-- | A kind meta-variable
type MetaK s = Meta s Kind ()

-- | A kind filled with meta-variables
type KindM s = Kind (MetaK s)

-- | Die with an error message due to a cycle between the specified kinds.
--
-- >>> test $ do k <- Var <$> newMeta (); unifyKind k (star ~> k)
-- *** Exception: (interactive):1:1: error: infinite kind detected
-- cyclic kind: a = * -> a
--
-- >>> test $ do k1 <- Var <$> newMeta (); k2 <- Var <$> newMeta (); unifyKind k1 (k1 ~> k2); unifyKind k2 (k1 ~> k2); return (k1 ~> k2)
-- *** Exception: (interactive):1:1: error: infinite kind detected
-- cyclic kind: a = a -> b
kindOccurs :: (MonadMeta s m, MonadWriter Any m) => KindM s -> (MetaK s -> Bool) -> m (KindM s)
kindOccurs k p = occurs k p $ do
  zk <- zonk k
  let s = setOf kindVars zk
      m = IntMap.fromList $ zipWith (\m n -> (m^.metaId, n)) (Set.toList s) names
      v = m ^?! ix (s ^?! folded.filtered p.metaId)
  kd <- prettyKind zk False $ \v _ -> pure $ text $ m ^?! ix (v^.metaId)
  r <- view rendering
  throwM $ die r "infinite kind detected" & footnotes .~ [text "cyclic kind:" <+> hang 4 (group (pretty v </> char '=' </> kd))]
{-# INLINE kindOccurs #-}

-- | Generalize a 'Kind', checking for escaped Skolems.
generalize :: MonadMeta s m => KindM s -> m (Schema a)
generalize k0 = do
  k <- runSharing k0 $ zonk k0
  (r,(_,n)) <- runStateT (traverse go k) (IntMap.empty, 0)
  return $ Schema n (Scope r)
  where
   go Skolem{}   = StateT $ \ _ -> fail "escaped skolem"
   go (Meta _ i _ _ _) = StateT $ \imn@(im, n) -> case im^.at i of
     Just b  -> return (B b, imn)
     Nothing -> let n' = n + 1 in n' `seq` return (B n, (im & at i ?~ n, n'))

-- | Returns the a unified form if different from the left argument.
--
{'fraction_non_alphanumeric': 0.18632918632918632, 'fraction_numerical': 0.00858000858000858, 'mean_word_length': 2.7581945190757655, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 106, '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': '1531157', 'n_tokens_mistral': 2511, 'n_tokens_neox': 2427, 'n_words': 770}