module Agda.TypeChecking.Free.Base where

import Control.Applicative hiding (empty)
import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, Reader, runReader )

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

import Agda.Syntax.Common.Pretty
import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List1 (List1)
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Semigroup
import Agda.Utils.Singleton
import Agda.Utils.Size

---------------------------------------------------------------------------
-- * Set of meta variables.

-- | A set of meta variables.  Forms a monoid under union.

newtype MetaSet = MetaSet { MetaSet -> HashSet MetaId
theMetaSet :: HashSet MetaId }
  deriving (MetaSet -> MetaSet -> Bool
(MetaSet -> MetaSet -> Bool)
-> (MetaSet -> MetaSet -> Bool) -> Eq MetaSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaSet -> MetaSet -> Bool
== :: MetaSet -> MetaSet -> Bool
$c/= :: MetaSet -> MetaSet -> Bool
/= :: MetaSet -> MetaSet -> Bool
Eq, Int -> MetaSet -> ShowS
[MetaSet] -> ShowS
MetaSet -> String
(Int -> MetaSet -> ShowS)
-> (MetaSet -> String) -> ([MetaSet] -> ShowS) -> Show MetaSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaSet -> ShowS
showsPrec :: Int -> MetaSet -> ShowS
$cshow :: MetaSet -> String
show :: MetaSet -> String
$cshowList :: [MetaSet] -> ShowS
showList :: [MetaSet] -> ShowS
Show, MetaSet
MetaSet -> Bool
MetaSet -> (MetaSet -> Bool) -> Null MetaSet
forall a. a -> (a -> Bool) -> Null a
$cempty :: MetaSet
empty :: MetaSet
$cnull :: MetaSet -> Bool
null :: MetaSet -> Bool
Null, NonEmpty MetaSet -> MetaSet
MetaSet -> MetaSet -> MetaSet
(MetaSet -> MetaSet -> MetaSet)
-> (NonEmpty MetaSet -> MetaSet)
-> (forall b. Integral b => b -> MetaSet -> MetaSet)
-> Semigroup MetaSet
forall b. Integral b => b -> MetaSet -> MetaSet
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: MetaSet -> MetaSet -> MetaSet
<> :: MetaSet -> MetaSet -> MetaSet
$csconcat :: NonEmpty MetaSet -> MetaSet
sconcat :: NonEmpty MetaSet -> MetaSet
$cstimes :: forall b. Integral b => b -> MetaSet -> MetaSet
stimes :: forall b. Integral b => b -> MetaSet -> MetaSet
Semigroup, Semigroup MetaSet
MetaSet
Semigroup MetaSet =>
MetaSet
-> (MetaSet -> MetaSet -> MetaSet)
-> ([MetaSet] -> MetaSet)
-> Monoid MetaSet
[MetaSet] -> MetaSet
MetaSet -> MetaSet -> MetaSet
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: MetaSet
mempty :: MetaSet
$cmappend :: MetaSet -> MetaSet -> MetaSet
mappend :: MetaSet -> MetaSet -> MetaSet
$cmconcat :: [MetaSet] -> MetaSet
mconcat :: [MetaSet] -> MetaSet
Monoid)

instance Singleton MetaId MetaSet where
  singleton :: MetaId -> MetaSet
singleton = HashSet MetaId -> MetaSet
MetaSet (HashSet MetaId -> MetaSet)
-> (MetaId -> HashSet MetaId) -> MetaId -> MetaSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> HashSet MetaId
forall el coll. Singleton el coll => el -> coll
singleton

insertMetaSet :: MetaId -> MetaSet -> MetaSet
insertMetaSet :: MetaId -> MetaSet -> MetaSet
insertMetaSet MetaId
m (MetaSet HashSet MetaId
ms) = HashSet MetaId -> MetaSet
MetaSet (HashSet MetaId -> MetaSet) -> HashSet MetaId -> MetaSet
forall a b. (a -> b) -> a -> b
$ MetaId -> HashSet MetaId -> HashSet MetaId
forall a. Hashable a => a -> HashSet a -> HashSet a
HashSet.insert MetaId
m HashSet MetaId
ms

foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet :: forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet MetaId -> a -> a
f a
e MetaSet
ms = (MetaId -> a -> a) -> a -> HashSet MetaId -> a
forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr MetaId -> a -> a
f a
e (HashSet MetaId -> a) -> HashSet MetaId -> a
forall a b. (a -> b) -> a -> b
$ MetaSet -> HashSet MetaId
theMetaSet MetaSet
ms

metaSetToBlocker :: MetaSet -> Blocker
metaSetToBlocker :: MetaSet -> Blocker
metaSetToBlocker MetaSet
ms = Set Blocker -> Blocker
unblockOnAny (Set Blocker -> Blocker) -> Set Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set Blocker -> Set Blocker)
-> Set Blocker -> MetaSet -> Set Blocker
forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet (Blocker -> Set Blocker -> Set Blocker
forall a. Ord a => a -> Set a -> Set a
Set.insert (Blocker -> Set Blocker -> Set Blocker)
-> (MetaId -> Blocker) -> MetaId -> Set Blocker -> Set Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Blocker
unblockOnMeta) Set Blocker
forall a. Set a
Set.empty MetaSet
ms

instance Pretty MetaSet where
  pretty :: MetaSet -> Doc
pretty = Set MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty (Set MetaId -> Doc) -> (MetaSet -> Set MetaId) -> MetaSet -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList ([MetaId] -> Set MetaId)
-> (MetaSet -> [MetaId]) -> MetaSet -> Set MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet MetaId -> [MetaId]
forall a. HashSet a -> [a]
HashSet.toList (HashSet MetaId -> [MetaId])
-> (MetaSet -> HashSet MetaId) -> MetaSet -> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaSet -> HashSet MetaId
theMetaSet

---------------------------------------------------------------------------
-- * Flexible and rigid occurrences (semigroup)

-- | Depending on the surrounding context of a variable,
--   it's occurrence can be classified as flexible or rigid,
--   with finer distinctions.
--
--   The constructors are listed in increasing order (wrt. information content).
data FlexRig' a
  = Flexible !a       -- ^ In arguments of metas.
                      --   The set of metas is used by ''Agda.TypeChecking.Rewriting.NonLinMatch''
                      --   to generate the right blocking information.
                      --   The semantics is that the status of a variable occurrence may change
                      --   if one of the metas in the set gets solved.  We may say the occurrence
                      --   is tainted by the meta variables in the set.
  | WeaklyRigid       -- ^ In arguments to variables and definitions.
  | Unguarded         -- ^ In top position, or only under inductive record constructors (unit).
  | StronglyRigid     -- ^ Under at least one and only inductive constructors.
  deriving (FlexRig' a -> FlexRig' a -> Bool
(FlexRig' a -> FlexRig' a -> Bool)
-> (FlexRig' a -> FlexRig' a -> Bool) -> Eq (FlexRig' a)
forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
== :: FlexRig' a -> FlexRig' a -> Bool
$c/= :: forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
/= :: FlexRig' a -> FlexRig' a -> Bool
Eq, Int -> FlexRig' a -> ShowS
[FlexRig' a] -> ShowS
FlexRig' a -> String
(Int -> FlexRig' a -> ShowS)
-> (FlexRig' a -> String)
-> ([FlexRig' a] -> ShowS)
-> Show (FlexRig' a)
forall a. Show a => Int -> FlexRig' a -> ShowS
forall a. Show a => [FlexRig' a] -> ShowS
forall a. Show a => FlexRig' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> FlexRig' a -> ShowS
showsPrec :: Int -> FlexRig' a -> ShowS
$cshow :: forall a. Show a => FlexRig' a -> String
show :: FlexRig' a -> String
$cshowList :: forall a. Show a => [FlexRig' a] -> ShowS
showList :: [FlexRig' a] -> ShowS
Show, (forall a b. (a -> b) -> FlexRig' a -> FlexRig' b)
-> (forall a b. a -> FlexRig' b -> FlexRig' a) -> Functor FlexRig'
forall a b. a -> FlexRig' b -> FlexRig' a
forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
fmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
$c<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
Functor, (forall m. Monoid m => FlexRig' m -> m)
-> (forall m a. Monoid m => (a -> m) -> FlexRig' a -> m)
-> (forall m a. Monoid m => (a -> m) -> FlexRig' a -> m)
-> (forall a b. (a -> b -> b) -> b -> FlexRig' a -> b)
-> (forall a b. (a -> b -> b) -> b -> FlexRig' a -> b)
-> (forall b a. (b -> a -> b) -> b -> FlexRig' a -> b)
-> (forall b a. (b -> a -> b) -> b -> FlexRig' a -> b)
-> (forall a. (a -> a -> a) -> FlexRig' a -> a)
-> (forall a. (a -> a -> a) -> FlexRig' a -> a)
-> (forall a. FlexRig' a -> [a])
-> (forall a. FlexRig' a -> Bool)
-> (forall a. FlexRig' a -> Int)
-> (forall a. Eq a => a -> FlexRig' a -> Bool)
-> (forall a. Ord a => FlexRig' a -> a)
-> (forall a. Ord a => FlexRig' a -> a)
-> (forall a. Num a => FlexRig' a -> a)
-> (forall a. Num a => FlexRig' a -> a)
-> Foldable FlexRig'
forall a. Eq a => a -> FlexRig' a -> Bool
forall a. Num a => FlexRig' a -> a
forall a. Ord a => FlexRig' a -> a
forall m. Monoid m => FlexRig' m -> m
forall a. FlexRig' a -> Bool
forall a. FlexRig' a -> Int
forall a. FlexRig' a -> [a]
forall a. (a -> a -> a) -> FlexRig' a -> a
forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => FlexRig' m -> m
fold :: forall m. Monoid m => FlexRig' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
$ctoList :: forall a. FlexRig' a -> [a]
toList :: forall a. FlexRig' a -> [a]
$cnull :: forall a. FlexRig' a -> Bool
null :: forall a. FlexRig' a -> Bool
$clength :: forall a. FlexRig' a -> Int
length :: forall a. FlexRig' a -> Int
$celem :: forall a. Eq a => a -> FlexRig' a -> Bool
elem :: forall a. Eq a => a -> FlexRig' a -> Bool
$cmaximum :: forall a. Ord a => FlexRig' a -> a
maximum :: forall a. Ord a => FlexRig' a -> a
$cminimum :: forall a. Ord a => FlexRig' a -> a
minimum :: forall a. Ord a => FlexRig' a -> a
$csum :: forall a. Num a => FlexRig' a -> a
sum :: forall a. Num a => FlexRig' a -> a
$cproduct :: forall a. Num a => FlexRig' a -> a
product :: forall a. Num a => FlexRig' a -> a
Foldable)

type FlexRig = FlexRig' MetaSet

class LensFlexRig o a | o -> a where
  lensFlexRig :: Lens' o (FlexRig' a)

instance LensFlexRig (FlexRig' a) a where
  lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)
lensFlexRig = (FlexRig' a -> f (FlexRig' a)) -> FlexRig' a -> f (FlexRig' a)
forall a. a -> a
id

isFlexible :: LensFlexRig o a => o -> Bool
isFlexible :: forall o a. LensFlexRig o a => o -> Bool
isFlexible o
o = case o
o o -> Getting (FlexRig' a) o (FlexRig' a) -> FlexRig' a
forall s a. s -> Getting a s a -> a
^. Getting (FlexRig' a) o (FlexRig' a)
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
  Flexible {} -> Bool
True
  FlexRig' a
_ -> Bool
False

isUnguarded :: LensFlexRig o a => o -> Bool
isUnguarded :: forall o a. LensFlexRig o a => o -> Bool
isUnguarded o
o = case o
o o -> Getting (FlexRig' a) o (FlexRig' a) -> FlexRig' a
forall s a. s -> Getting a s a -> a
^. Getting (FlexRig' a) o (FlexRig' a)
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
  FlexRig' a
Unguarded -> Bool
True
  FlexRig' a
_ -> Bool
False

isWeaklyRigid :: LensFlexRig o a => o -> Bool
isWeaklyRigid :: forall o a. LensFlexRig o a => o -> Bool
isWeaklyRigid o
o = case o
o o -> Getting (FlexRig' a) o (FlexRig' a) -> FlexRig' a
forall s a. s -> Getting a s a -> a
^. Getting (FlexRig' a) o (FlexRig' a)
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
   FlexRig' a
WeaklyRigid -> Bool
True
   FlexRig' a
_ -> Bool
False

isStronglyRigid :: LensFlexRig o a => o -> Bool
isStronglyRigid :: forall o a. LensFlexRig o a => o -> Bool
isStronglyRigid o
o = case o
o o -> Getting (FlexRig' a) o (FlexRig' a) -> FlexRig' a
forall s a. s -> Getting a s a -> a
^. Getting (FlexRig' a) o (FlexRig' a)
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig of
  FlexRig' a
StronglyRigid -> Bool
True
  FlexRig' a
_ -> Bool
False

-- | 'FlexRig' aggregation (additive operation of the semiring).
--   For combining occurrences of the same variable in subterms.
--   This is a refinement of the 'max' operation for 'FlexRig'
--   which would work if 'Flexible' did not have the 'MetaSet' as an argument.
--   Now, to aggregate two 'Flexible' occurrences, we union the involved 'MetaSet's.

addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig :: forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig = ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a -> FlexRig' a -> FlexRig' a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((FlexRig' a, FlexRig' a) -> FlexRig' a)
 -> FlexRig' a -> FlexRig' a -> FlexRig' a)
-> ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a
-> FlexRig' a
-> FlexRig' a
forall a b. (a -> b) -> a -> b
$ \case
  -- StronglyRigid is dominant
  (FlexRig' a
StronglyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
  (FlexRig' a
_, FlexRig' a
StronglyRigid) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
  -- Next is Unguarded
  (FlexRig' a
Unguarded, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
Unguarded
  (FlexRig' a
_, FlexRig' a
Unguarded) -> FlexRig' a
forall a. FlexRig' a
Unguarded
  -- Then WeaklyRigid
  (FlexRig' a
WeaklyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
  (FlexRig' a
_, FlexRig' a
WeaklyRigid) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
  -- Least is Flexible.  We union the meta sets, as the variable
  -- is tainted by all of the involved meta variable.
  (Flexible a
ms1, Flexible a
ms2) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ a
ms1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
ms2
{-# SPECIALIZE NOINLINE addFlexRig :: FlexRig' MetaSet -> FlexRig' MetaSet -> FlexRig' MetaSet #-}
{-# SPECIALIZE NOINLINE addFlexRig :: FlexRig' () -> FlexRig' () -> FlexRig' () #-}

-- | Unit for 'addFlexRig'.
zeroFlexRig :: Monoid a => FlexRig' a
zeroFlexRig :: forall a. Monoid a => FlexRig' a
zeroFlexRig = a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
forall a. Monoid a => a
mempty

-- | Absorptive for 'addFlexRig'.
omegaFlexRig :: FlexRig' a
omegaFlexRig :: forall a. FlexRig' a
omegaFlexRig = FlexRig' a
forall a. FlexRig' a
StronglyRigid

-- | 'FlexRig' composition (multiplicative operation of the semiring).
--   For accumulating the context of a variable.
--
--   'Flexible' is dominant.  Once we are under a meta, we are flexible
--   regardless what else comes.  We taint all variable occurrences
--   under a meta by this meta.
--
--   'WeaklyRigid' is next in strength.  Destroys strong rigidity.
--
--   'StronglyRigid' is still dominant over 'Unguarded'.
--
--   'Unguarded' is the unit.  It is the top (identity) context.
--
composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig :: forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig = ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a -> FlexRig' a -> FlexRig' a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((FlexRig' a, FlexRig' a) -> FlexRig' a)
 -> FlexRig' a -> FlexRig' a -> FlexRig' a)
-> ((FlexRig' a, FlexRig' a) -> FlexRig' a)
-> FlexRig' a
-> FlexRig' a
-> FlexRig' a
forall a b. (a -> b) -> a -> b
$ \case
    (Flexible a
ms1, Flexible a
ms2) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ a
ms1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
ms2
    (Flexible a
ms1, FlexRig' a
_) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
ms1
    (FlexRig' a
_, Flexible a
ms2) -> a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
ms2
    (FlexRig' a
WeaklyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
    (FlexRig' a
_, FlexRig' a
WeaklyRigid) -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
    (FlexRig' a
StronglyRigid, FlexRig' a
_) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
    (FlexRig' a
_, FlexRig' a
StronglyRigid) -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
    (FlexRig' a
Unguarded, FlexRig' a
Unguarded) -> FlexRig' a
forall a. FlexRig' a
Unguarded
{-# SPECIALIZE NOINLINE composeFlexRig :: FlexRig' MetaSet -> FlexRig' MetaSet -> FlexRig' MetaSet #-}
{-# SPECIALIZE NOINLINE composeFlexRig :: FlexRig' () -> FlexRig' () -> FlexRig' () #-}

-- | Unit for 'composeFlexRig'.
oneFlexRig :: FlexRig' a
oneFlexRig :: forall a. FlexRig' a
oneFlexRig = FlexRig' a
forall a. FlexRig' a
Unguarded

-- | Extract a blocker from an occurrence
flexRigToBlocker :: FlexRig -> Blocker
flexRigToBlocker :: FlexRig -> Blocker
flexRigToBlocker (Flexible MetaSet
ms) = MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
flexRigToBlocker FlexRig
_ = Blocker
neverUnblock

instance Pretty a => Pretty (FlexRig' a) where
  pretty :: FlexRig' a -> Doc
pretty = \case
    Flexible a
a    -> Doc
"FL" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a)
    FlexRig' a
WeaklyRigid   -> Doc
"WR"
    FlexRig' a
StronglyRigid -> Doc
"SR"
    FlexRig' a
Unguarded     -> Doc
forall a. Null a => a
empty

---------------------------------------------------------------------------
-- * Multi-dimensional feature vector for variable occurrence (semigroup)

-- | Occurrence of free variables is classified by several dimensions.
--   Currently, we have 'FlexRig' and 'Modality'.
data VarOcc' a = VarOcc
  { forall a. VarOcc' a -> FlexRig' a
varFlexRig   :: !(FlexRig' a)
  , forall a. VarOcc' a -> Modality
varModality  :: {-# UNPACK #-} !Modality
  }
  deriving (Int -> VarOcc' a -> ShowS
[VarOcc' a] -> ShowS
VarOcc' a -> String
(Int -> VarOcc' a -> ShowS)
-> (VarOcc' a -> String)
-> ([VarOcc' a] -> ShowS)
-> Show (VarOcc' a)
forall a. Show a => Int -> VarOcc' a -> ShowS
forall a. Show a => [VarOcc' a] -> ShowS
forall a. Show a => VarOcc' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> VarOcc' a -> ShowS
showsPrec :: Int -> VarOcc' a -> ShowS
$cshow :: forall a. Show a => VarOcc' a -> String
show :: VarOcc' a -> String
$cshowList :: forall a. Show a => [VarOcc' a] -> ShowS
showList :: [VarOcc' a] -> ShowS
Show)
type VarOcc = VarOcc' MetaSet

-- | Equality up to origin.
instance Eq a => Eq (VarOcc' a) where
  VarOcc FlexRig' a
fr Modality
m == :: VarOcc' a -> VarOcc' a -> Bool
== VarOcc FlexRig' a
fr' Modality
m' = FlexRig' a
fr FlexRig' a -> FlexRig' a -> Bool
forall a. Eq a => a -> a -> Bool
== FlexRig' a
fr' Bool -> Bool -> Bool
&& Modality -> Modality -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
m Modality
m'

instance LensModality (VarOcc' a) where
  getModality :: VarOcc' a -> Modality
getModality = VarOcc' a -> Modality
forall a. VarOcc' a -> Modality
varModality
  mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a
mapModality Modality -> Modality
f (VarOcc FlexRig' a
x Modality
r) = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
x (Modality -> VarOcc' a) -> Modality -> VarOcc' a
forall a b. (a -> b) -> a -> b
$ Modality -> Modality
f Modality
r

instance LensRelevance (VarOcc' a) where
instance LensQuantity (VarOcc' a) where

-- | Access to 'varFlexRig' in 'VarOcc'.
instance LensFlexRig (VarOcc' a) a where
  lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f (VarOcc FlexRig' a
fr Modality
m) = FlexRig' a -> f (FlexRig' a)
f FlexRig' a
fr f (FlexRig' a) -> (FlexRig' a -> VarOcc' a) -> f (VarOcc' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FlexRig' a
fr' -> FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
fr' Modality
m
-- lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a)
-- lensFlexRig f (VarOcc fr m) = f fr <&> \ fr' -> VarOcc fr' m


-- | The default way of aggregating free variable info from subterms is by adding
--   the variable occurrences.  For instance, if we have a pair @(t₁,t₂)@ then
--   and @t₁@ has @o₁@ the occurrences of a variable @x@
--   and @t₂@ has @o₂@ the occurrences of the same variable, then
--   @(t₁,t₂)@ has @mappend o₁ o₂@ occurrences of that variable.
--
--   From counting 'Quantity', we extrapolate this to 'FlexRig' and 'Relevance':
--   we care most about about 'StronglyRigid' 'Relevant' occurrences.
--   E.g., if @t₁@ has a 'StronglyRigid' occurrence and @t₂@ a 'Flexible' occurrence,
--   then @(t₁,t₂)@ still has a 'StronglyRigid' occurrence.
--   Analogously, @Relevant@ occurrences count most, as we wish e.g. to forbid
--   relevant occurrences of variables that are declared to be irrelevant.
--
--   'VarOcc' forms a semiring, and this monoid is the addition of the semiring.

instance Semigroup a => Semigroup (VarOcc' a) where
  VarOcc FlexRig' a
o Modality
m <> :: VarOcc' a -> VarOcc' a -> VarOcc' a
<> VarOcc FlexRig' a
o' Modality
m' = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig FlexRig' a
o FlexRig' a
o') (Modality -> Modality -> Modality
addModality Modality
m Modality
m')

-- | The neutral element for variable occurrence aggregation is least serious
--   occurrence: flexible, irrelevant.
--   This is also the absorptive element for 'composeVarOcc', if we ignore
--   the 'MetaSet' in 'Flexible'.
instance (Monoid a) => Monoid (VarOcc' a) where
  mempty :: VarOcc' a
mempty  = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
forall a. Monoid a => a
mempty) Modality
zeroModality
  mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a
mappend = VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => a -> a -> a
(<>)

-- | The absorptive element of variable occurrence under aggregation:
--   strongly rigid, relevant.
topVarOcc :: VarOcc' a
topVarOcc :: forall a. VarOcc' a
topVarOcc = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
forall a. FlexRig' a
StronglyRigid Modality
topModality

-- | First argument is the outer occurrence (context) and second is the inner.
--   This multiplicative operation is to modify an occurrence under a context.
composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc :: forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc (VarOcc FlexRig' a
o Modality
m) (VarOcc FlexRig' a
o' Modality
m') = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig FlexRig' a
o FlexRig' a
o') (Modality -> Modality -> Modality
composeModality Modality
m Modality
m')
  -- We use the multipicative modality monoid (composition).

oneVarOcc :: VarOcc' a
oneVarOcc :: forall a. VarOcc' a
oneVarOcc = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
forall a. FlexRig' a
Unguarded Modality
unitModality

-- | What's the rigidity of a constructor?
constructorFlexRig :: ConHead -> Elims -> FlexRig' a
constructorFlexRig :: forall a. ConHead -> Elims -> FlexRig' a
constructorFlexRig (ConHead QName
_ DataOrRecord
_ Induction
i [Arg QName]
fs) Elims
es = case Induction
i of

  -- Coinductive (record) constructors admit infinite cycles:
  Induction
CoInductive -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
  -- Inductive constructors do not admit infinite cycles:
  Induction
Inductive   | Elims -> Int
forall a. Sized a => a -> Int
size Elims
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg QName] -> Int
forall a. Sized a => a -> Int
size [Arg QName]
fs -> FlexRig' a
forall a. FlexRig' a
StronglyRigid
              | Bool
otherwise          -> FlexRig' a
forall a. FlexRig' a
WeaklyRigid
  -- Jesper, 2020-10-22: Issue #4995: treat occurrences in non-fully
  -- applied constructors as weakly rigid.
  -- Ulf, 2019-10-18: Now the termination checker treats inductive recursive records
  -- the same as datatypes, so absense of infinite cycles can be proven in Agda, and thus
  -- the unifier is allowed to do it too. Test case: test/Succeed/Issue1271a.agda
  -- WAS:
  -- -- Inductive record constructors do not admit infinite cycles,
  -- -- but this cannot be proven inside Agda.
  -- -- Thus, unification should not prove it either.

instance Pretty a => Pretty (VarOcc' a) where
  pretty :: VarOcc' a -> Doc
pretty (VarOcc FlexRig' a
a Modality
b) = FlexRig' a -> Doc
forall a. Pretty a => a -> Doc
pretty FlexRig' a
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Modality -> Doc
forall a. Pretty a => a -> Doc
pretty Modality
b

-- | Representation of a variable set as map from de Bruijn indices
--   to 'VarOcc'.
type TheVarMap' a = IntMap (VarOcc' a)
newtype VarMap' a = VarMap { forall a. VarMap' a -> TheVarMap' a
theVarMap :: TheVarMap' a }
  deriving (VarMap' a -> VarMap' a -> Bool
(VarMap' a -> VarMap' a -> Bool)
-> (VarMap' a -> VarMap' a -> Bool) -> Eq (VarMap' a)
forall a. Eq a => VarMap' a -> VarMap' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => VarMap' a -> VarMap' a -> Bool
== :: VarMap' a -> VarMap' a -> Bool
$c/= :: forall a. Eq a => VarMap' a -> VarMap' a -> Bool
/= :: VarMap' a -> VarMap' a -> Bool
Eq, Int -> VarMap' a -> ShowS
[VarMap' a] -> ShowS
VarMap' a -> String
(Int -> VarMap' a -> ShowS)
-> (VarMap' a -> String)
-> ([VarMap' a] -> ShowS)
-> Show (VarMap' a)
forall a. Show a => Int -> VarMap' a -> ShowS
forall a. Show a => [VarMap' a] -> ShowS
forall a. Show a => VarMap' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> VarMap' a -> ShowS
showsPrec :: Int -> VarMap' a -> ShowS
$cshow :: forall a. Show a => VarMap' a -> String
show :: VarMap' a -> String
$cshowList :: forall a. Show a => [VarMap' a] -> ShowS
showList :: [VarMap' a] -> ShowS
Show)

type TheVarMap = TheVarMap' MetaSet
type    VarMap =    VarMap' MetaSet

-- | A "set"-style 'Singleton' instance with default/initial variable occurrence.
instance Singleton Variable (VarMap' a) where
  singleton :: Int -> VarMap' a
singleton Int
i = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' a -> VarMap' a) -> TheVarMap' a -> VarMap' a
forall a b. (a -> b) -> a -> b
$ Int -> VarOcc' a -> TheVarMap' a
forall a. Int -> a -> IntMap a
IntMap.singleton Int
i VarOcc' a
forall a. VarOcc' a
oneVarOcc

mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap :: forall a b.
(TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap TheVarMap' a -> TheVarMap' b
f = TheVarMap' b -> VarMap' b
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' b -> VarMap' b)
-> (VarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheVarMap' a -> TheVarMap' b
f (TheVarMap' a -> TheVarMap' b)
-> (VarMap' a -> TheVarMap' a) -> VarMap' a -> TheVarMap' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap' a -> TheVarMap' a
forall a. VarMap' a -> TheVarMap' a
theVarMap

lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap :: forall a. Int -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap Int
i = Int -> IntMap (VarOcc' a) -> Maybe (VarOcc' a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i (IntMap (VarOcc' a) -> Maybe (VarOcc' a))
-> (VarMap' a -> IntMap (VarOcc' a))
-> VarMap' a
-> Maybe (VarOcc' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarMap' a -> IntMap (VarOcc' a)
forall a. VarMap' a -> TheVarMap' a
theVarMap

-- Andreas & Jesper, 2018-05-11, issue #3052:

-- | Proper monoid instance for @VarMap@ rather than inheriting the broken one from IntMap.
--   We combine two occurrences of a variable using 'mappend'.
instance Semigroup a => Semigroup (VarMap' a) where
  VarMap TheVarMap' a
m <> :: VarMap' a -> VarMap' a -> VarMap' a
<> VarMap TheVarMap' a
m' = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' a -> VarMap' a) -> TheVarMap' a -> VarMap' a
forall a b. (a -> b) -> a -> b
$ (VarOcc' a -> VarOcc' a -> VarOcc' a)
-> TheVarMap' a -> TheVarMap' a -> TheVarMap' a
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => a -> a -> a
(<>) TheVarMap' a
m TheVarMap' a
m'

instance Semigroup a => Monoid (VarMap' a) where
  mempty :: VarMap' a
mempty  = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap TheVarMap' a
forall a. IntMap a
IntMap.empty
  mappend :: VarMap' a -> VarMap' a -> VarMap' a
mappend = VarMap' a -> VarMap' a -> VarMap' a
forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [VarMap' a] -> VarMap' a
mconcat = TheVarMap' a -> VarMap' a
forall a. TheVarMap' a -> VarMap' a
VarMap (TheVarMap' a -> VarMap' a)
-> ([VarMap' a] -> TheVarMap' a) -> [VarMap' a] -> VarMap' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarOcc' a -> VarOcc' a -> VarOcc' a)
-> [TheVarMap' a] -> TheVarMap' a
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> f (IntMap a) -> IntMap a
IntMap.unionsWith VarOcc' a -> VarOcc' a -> VarOcc' a
forall a. Semigroup a => a -> a -> a
(<>) ([TheVarMap' a] -> TheVarMap' a)
-> ([VarMap' a] -> [TheVarMap' a]) -> [VarMap' a] -> TheVarMap' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VarMap' a -> TheVarMap' a) -> [VarMap' a] -> [TheVarMap' a]
forall a b. (a -> b) -> [a] -> [b]
map VarMap' a -> TheVarMap' a
forall a. VarMap' a -> TheVarMap' a
theVarMap
  -- mconcat = VarMap . IntMap.unionsWith mappend . coerce   -- ghc 8.6.5 does not seem to like this coerce

---------------------------------------------------------------------------
-- * Plain variable occurrence counting.

newtype VarCounts = VarCounts { VarCounts -> IntMap Int
varCounts :: IntMap Int }
  deriving (VarCounts -> VarCounts -> Bool
(VarCounts -> VarCounts -> Bool)
-> (VarCounts -> VarCounts -> Bool) -> Eq VarCounts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VarCounts -> VarCounts -> Bool
== :: VarCounts -> VarCounts -> Bool
$c/= :: VarCounts -> VarCounts -> Bool
/= :: VarCounts -> VarCounts -> Bool
Eq, Int -> VarCounts -> ShowS
[VarCounts] -> ShowS
VarCounts -> String
(Int -> VarCounts -> ShowS)
-> (VarCounts -> String)
-> ([VarCounts] -> ShowS)
-> Show VarCounts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VarCounts -> ShowS
showsPrec :: Int -> VarCounts -> ShowS
$cshow :: VarCounts -> String
show :: VarCounts -> String
$cshowList :: [VarCounts] -> ShowS
showList :: [VarCounts] -> ShowS
Show)

instance Semigroup VarCounts where
  VarCounts IntMap Int
fv1 <> :: VarCounts -> VarCounts -> VarCounts
<> VarCounts IntMap Int
fv2 = IntMap Int -> VarCounts
VarCounts ((Int -> Int -> Int) -> IntMap Int -> IntMap Int -> IntMap Int
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) IntMap Int
fv1 IntMap Int
fv2)

instance Monoid VarCounts where
  mempty :: VarCounts
mempty = IntMap Int -> VarCounts
VarCounts IntMap Int
forall a. IntMap a
IntMap.empty
  mappend :: VarCounts -> VarCounts -> VarCounts
mappend = VarCounts -> VarCounts -> VarCounts
forall a. Semigroup a => a -> a -> a
(<>)

-- | Where should we skip sorts in free variable analysis?
data IgnoreSorts
  = IgnoreNot            -- ^ Do not skip.
  | IgnoreInAnnotations  -- ^ Skip when annotation to a type.
  | IgnoreAll            -- ^ Skip unconditionally.
  deriving (IgnoreSorts -> IgnoreSorts -> Bool
(IgnoreSorts -> IgnoreSorts -> Bool)
-> (IgnoreSorts -> IgnoreSorts -> Bool) -> Eq IgnoreSorts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IgnoreSorts -> IgnoreSorts -> Bool
== :: IgnoreSorts -> IgnoreSorts -> Bool
$c/= :: IgnoreSorts -> IgnoreSorts -> Bool
/= :: IgnoreSorts -> IgnoreSorts -> Bool
Eq, Int -> IgnoreSorts -> ShowS
[IgnoreSorts] -> ShowS
IgnoreSorts -> String
(Int -> IgnoreSorts -> ShowS)
-> (IgnoreSorts -> String)
-> ([IgnoreSorts] -> ShowS)
-> Show IgnoreSorts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IgnoreSorts -> ShowS
showsPrec :: Int -> IgnoreSorts -> ShowS
$cshow :: IgnoreSorts -> String
show :: IgnoreSorts -> String
$cshowList :: [IgnoreSorts] -> ShowS
showList :: [IgnoreSorts] -> ShowS
Show)

type Variable = Int