-- | Computing the free variables of a term lazily.
--
-- We implement a reduce (traversal into monoid) over internal syntax
-- for a generic collection (monoid with singletons).  This should allow
-- a more efficient test for the presence of a particular variable.
--
-- Worst-case complexity does not change (i.e. the case when a variable
-- does not occur), but best case-complexity does matter.  For instance,
-- see 'Agda.TypeChecking.Substitute.mkAbs': each time we construct
-- a dependent function type, we check whether it is actually dependent.
--
-- The distinction between rigid and strongly rigid occurrences comes from:
--   Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)
--
-- The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly
-- in t.  It might have a solution if the occurrence is not strongly rigid, e.g.
--
--   x = \f -> suc (f (x (\ y -> k)))  has  x = \f -> suc (f (suc k))
--
-- [Jason C. Reed, PhD thesis, page 106]
--
-- Under coinductive constructors, occurrences are never strongly rigid.
-- Also, function types and lambdas do not establish strong rigidity.
-- Only inductive constructors do so.
-- (See issue 1271).
--
-- For further reading on semirings and semimodules for variable occurrence,
-- see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016).
-- There, he treats the "quantity" dimension of variable occurrences.
--
-- The semiring has an additive operation for combining occurrences of subterms,
-- and a multiplicative operation of representing function composition.  E.g.
-- if variable @x@ appears @o@ in term @u@, but @u@ appears in context @q@ in
-- term @t@ then occurrence of variable @x@ coming from @u@ is accounted for
-- as @q o@ in @t@.
--
-- Consider example @(λ{ x → (x,x)}) y@:
--
--   * Variable @x@ occurs once unguarded in @x@.
--
--   * It occurs twice unguarded in the aggregation @x@ @x@
--
--   * Inductive constructor @,@ turns this into two strictly rigid occurrences.
--
--     If @,@ is a record constructor, then we stay unguarded.
--
--   * The function @({λ x → (x,x)})@ provides a context for variable @y@.
--     This context can be described as weakly rigid with quantity two.
--
--   * The final occurrence of @y@ is obtained as composing the context with
--     the occurrence of @y@ in itself (which is the unit for composition).
--     Thus, @y@ occurs weakly rigid with quantity two.
--
-- It is not a given that the context can be described in the same way
-- as the variable occurrence.  However, for quantity it is the case
-- and we obtain a semiring of occurrences with 0, 1, and even ω, which
-- is an absorptive element for addition.

module Agda.TypeChecking.Free.Lazy where

import Control.Applicative hiding (empty)
import Control.Monad        ( guard )
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.Semigroup ( Semigroup, (<>) )
import qualified Data.Set as Set
import Data.Set (Set)


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

import Agda.Utils.Functor
import Agda.Utils.Lens
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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MetaSet -> MetaSet -> Bool
$c/= :: MetaSet -> MetaSet -> Bool
== :: MetaSet -> MetaSet -> Bool
$c== :: MetaSet -> MetaSet -> Bool
Eq, Variable -> MetaSet -> ShowS
[MetaSet] -> ShowS
MetaSet -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MetaSet] -> ShowS
$cshowList :: [MetaSet] -> ShowS
show :: MetaSet -> String
$cshow :: MetaSet -> String
showsPrec :: Variable -> MetaSet -> ShowS
$cshowsPrec :: Variable -> MetaSet -> ShowS
Show, MetaSet
MetaSet -> Bool
forall a. a -> (a -> Bool) -> Null a
null :: MetaSet -> Bool
$cnull :: MetaSet -> Bool
empty :: MetaSet
$cempty :: MetaSet
Null, NonEmpty MetaSet -> MetaSet
MetaSet -> MetaSet -> 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
stimes :: forall b. Integral b => b -> MetaSet -> MetaSet
$cstimes :: forall b. Integral b => b -> MetaSet -> MetaSet
sconcat :: NonEmpty MetaSet -> MetaSet
$csconcat :: NonEmpty MetaSet -> MetaSet
<> :: MetaSet -> MetaSet -> MetaSet
$c<> :: MetaSet -> MetaSet -> MetaSet
Semigroup, Semigroup MetaSet
MetaSet
[MetaSet] -> MetaSet
MetaSet -> MetaSet -> MetaSet
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [MetaSet] -> MetaSet
$cmconcat :: [MetaSet] -> MetaSet
mappend :: MetaSet -> MetaSet -> MetaSet
$cmappend :: MetaSet -> MetaSet -> MetaSet
mempty :: MetaSet
$cmempty :: MetaSet
Monoid)

instance Singleton MetaId MetaSet where
  singleton :: MetaId -> MetaSet
singleton = HashSet MetaId -> MetaSet
MetaSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ forall a. (Eq 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 = forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr MetaId -> a -> a
f a
e 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 forall a b. (a -> b) -> a -> b
$ forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet (forall a. Ord a => a -> Set a -> Set a
Set.insert forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Blocker
unblockOnMeta) forall a. Set a
Set.empty MetaSet
ms

---------------------------------------------------------------------------
-- * 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
forall a. Eq a => FlexRig' a -> FlexRig' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FlexRig' a -> FlexRig' a -> Bool
$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
Eq, Variable -> FlexRig' a -> ShowS
forall a. Show a => Variable -> FlexRig' a -> ShowS
forall a. Show a => [FlexRig' a] -> ShowS
forall a. Show a => FlexRig' a -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FlexRig' a] -> ShowS
$cshowList :: forall a. Show a => [FlexRig' a] -> ShowS
show :: FlexRig' a -> String
$cshow :: forall a. Show a => FlexRig' a -> String
showsPrec :: Variable -> FlexRig' a -> ShowS
$cshowsPrec :: forall a. Show a => Variable -> FlexRig' a -> ShowS
Show, 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
<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
$c<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
fmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
$cfmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
Functor, 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 -> Variable
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 -> Variable)
-> (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
product :: forall a. Num a => FlexRig' a -> a
$cproduct :: forall a. Num a => FlexRig' a -> a
sum :: forall a. Num a => FlexRig' a -> a
$csum :: forall a. Num a => FlexRig' a -> a
minimum :: forall a. Ord a => FlexRig' a -> a
$cminimum :: forall a. Ord a => FlexRig' a -> a
maximum :: forall a. Ord a => FlexRig' a -> a
$cmaximum :: forall a. Ord a => FlexRig' a -> a
elem :: forall a. Eq a => a -> FlexRig' a -> Bool
$celem :: forall a. Eq a => a -> FlexRig' a -> Bool
length :: forall a. FlexRig' a -> Variable
$clength :: forall a. FlexRig' a -> Variable
null :: forall a. FlexRig' a -> Bool
$cnull :: forall a. FlexRig' a -> Bool
toList :: forall a. FlexRig' a -> [a]
$ctoList :: forall a. FlexRig' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
fold :: forall m. Monoid m => FlexRig' m -> m
$cfold :: forall m. Monoid m => FlexRig' m -> m
Foldable)

type FlexRig = FlexRig' MetaSet

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

instance LensFlexRig a (FlexRig' a) where
  lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f FlexRig' a
x = FlexRig' a -> f (FlexRig' a)
f FlexRig' a
x

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

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

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

isStronglyRigid :: LensFlexRig a o => o -> Bool
isStronglyRigid :: forall a o. LensFlexRig a o => o -> Bool
isStronglyRigid o
o = case o
o forall o i. o -> Lens' i o -> i
^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
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 = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
  -- StronglyRigid is dominant
  (FlexRig' a
StronglyRigid, FlexRig' a
_) -> forall a. FlexRig' a
StronglyRigid
  (FlexRig' a
_, FlexRig' a
StronglyRigid) -> forall a. FlexRig' a
StronglyRigid
  -- Next is Unguarded
  (FlexRig' a
Unguarded, FlexRig' a
_) -> forall a. FlexRig' a
Unguarded
  (FlexRig' a
_, FlexRig' a
Unguarded) -> forall a. FlexRig' a
Unguarded
  -- Then WeaklyRigid
  (FlexRig' a
WeaklyRigid, FlexRig' a
_) -> forall a. FlexRig' a
WeaklyRigid
  (FlexRig' a
_, FlexRig' a
WeaklyRigid) -> 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) -> forall a. a -> FlexRig' a
Flexible forall a b. (a -> b) -> a -> b
$ a
ms1 forall a. Semigroup a => a -> a -> a
<> a
ms2

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

-- | Absorptive for 'addFlexRig'.
omegaFlexRig :: FlexRig' a
omegaFlexRig :: forall a. FlexRig' a
omegaFlexRig = 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 = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
    (Flexible a
ms1, Flexible a
ms2) -> forall a. a -> FlexRig' a
Flexible forall a b. (a -> b) -> a -> b
$ a
ms1 forall a. Semigroup a => a -> a -> a
<> a
ms2
    (Flexible a
ms1, FlexRig' a
_) -> forall a. a -> FlexRig' a
Flexible a
ms1
    (FlexRig' a
_, Flexible a
ms2) -> forall a. a -> FlexRig' a
Flexible a
ms2
    (FlexRig' a
WeaklyRigid, FlexRig' a
_) -> forall a. FlexRig' a
WeaklyRigid
    (FlexRig' a
_, FlexRig' a
WeaklyRigid) -> forall a. FlexRig' a
WeaklyRigid
    (FlexRig' a
StronglyRigid, FlexRig' a
_) -> forall a. FlexRig' a
StronglyRigid
    (FlexRig' a
_, FlexRig' a
StronglyRigid) -> forall a. FlexRig' a
StronglyRigid
    (FlexRig' a
Unguarded, FlexRig' a
Unguarded) -> forall a. FlexRig' a
Unguarded

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

---------------------------------------------------------------------------
-- * 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  :: Modality
  }
  deriving (Variable -> VarOcc' a -> ShowS
forall a. Show a => Variable -> VarOcc' a -> ShowS
forall a. Show a => [VarOcc' a] -> ShowS
forall a. Show a => VarOcc' a -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarOcc' a] -> ShowS
$cshowList :: forall a. Show a => [VarOcc' a] -> ShowS
show :: VarOcc' a -> String
$cshow :: forall a. Show a => VarOcc' a -> String
showsPrec :: Variable -> VarOcc' a -> ShowS
$cshowsPrec :: forall a. Show a => Variable -> 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 forall a. Eq a => a -> a -> Bool
== FlexRig' a
fr' Bool -> Bool -> 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 = forall a. VarOcc' a -> Modality
varModality
  mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a
mapModality Modality -> Modality
f (VarOcc FlexRig' a
x Modality
r) = forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
x 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 a (VarOcc' a) where
  lensFlexRig :: Lens' (FlexRig' a) (VarOcc' a)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f (VarOcc FlexRig' a
fr Modality
m) = FlexRig' a -> f (FlexRig' a)
f FlexRig' a
fr forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ FlexRig' a
fr' -> forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
fr' Modality
m
-- lensFlexRig :: Lens' (FlexRig' a) (VarOcc' 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' = forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (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 (Semigroup a, Monoid a) => Monoid (VarOcc' a) where
  mempty :: VarOcc' a
mempty  = forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (forall a. a -> FlexRig' a
Flexible forall a. Monoid a => a
mempty) Modality
zeroModality
  mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a
mappend = 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 = forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc 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') = forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc (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 = forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc forall a. FlexRig' a
Unguarded Modality
unitModality

---------------------------------------------------------------------------
-- * Storing variable occurrences (semimodule).

-- | Any representation @c@ of a set of variables need to be able to be modified by
--   a variable occurrence. This is to ensure that free variable analysis is
--   compositional. For instance, it should be possible to compute `fv (v [u/x])`
--   from `fv v` and `fv u`.
--
--   In algebraic terminology, a variable set @a@ needs to be (almost) a left semimodule
--   to the semiring 'VarOcc'.
class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where
  -- | Laws
  --    * Respects monoid operations:
  --      ```
  --        withVarOcc o mempty   == mempty
  --        withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y
  --      ```
  --    * Respects VarOcc composition:
  --      ```
  --        withVarOcc oneVarOcc             = id
  --        withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2
  --      ```
  --    * Respects VarOcc aggregation:
  --      ```
  --        withVarOcc (o1 <> o2) x = withVarOcc o1 x <> withVarOcc o2 x
  --      ```
  --      Since the corresponding unit law may fail,
  --      ```
  --        withVarOcc mempty x = mempty
  --      ```
  --      it is not quite a semimodule.
  withVarOcc :: VarOcc' a -> c -> c

-- | 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
forall a. Eq a => VarMap' a -> VarMap' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VarMap' a -> VarMap' a -> Bool
$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
Eq, Variable -> VarMap' a -> ShowS
forall a. Show a => Variable -> VarMap' a -> ShowS
forall a. Show a => [VarMap' a] -> ShowS
forall a. Show a => VarMap' a -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarMap' a] -> ShowS
$cshowList :: forall a. Show a => [VarMap' a] -> ShowS
show :: VarMap' a -> String
$cshow :: forall a. Show a => VarMap' a -> String
showsPrec :: Variable -> VarMap' a -> ShowS
$cshowsPrec :: forall a. Show a => Variable -> 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 :: Variable -> VarMap' a
singleton Variable
i = forall a. TheVarMap' a -> VarMap' a
VarMap forall a b. (a -> b) -> a -> b
$ forall a. Variable -> a -> IntMap a
IntMap.singleton Variable
i 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 = forall a. TheVarMap' a -> VarMap' a
VarMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheVarMap' a -> TheVarMap' b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. VarMap' a -> TheVarMap' a
theVarMap

lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap :: forall a. Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap Variable
i = forall a. Variable -> IntMap a -> Maybe a
IntMap.lookup Variable
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' = forall a. TheVarMap' a -> VarMap' a
VarMap forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. Semigroup a => a -> a -> a
(<>) TheVarMap' a
m TheVarMap' a
m'

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

instance (Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) where
  withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a
withVarOcc VarOcc' a
o = forall a b.
(TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a. Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
composeVarOcc VarOcc' a
o


---------------------------------------------------------------------------
-- * Simple flexible/rigid variable collection.

-- | Keep track of 'FlexRig' for every variable, but forget the involved meta vars.
type TheFlexRigMap = IntMap (FlexRig' ())
newtype FlexRigMap = FlexRigMap { FlexRigMap -> TheFlexRigMap
theFlexRigMap :: TheFlexRigMap }
  deriving (Variable -> FlexRigMap -> ShowS
[FlexRigMap] -> ShowS
FlexRigMap -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FlexRigMap] -> ShowS
$cshowList :: [FlexRigMap] -> ShowS
show :: FlexRigMap -> String
$cshow :: FlexRigMap -> String
showsPrec :: Variable -> FlexRigMap -> ShowS
$cshowsPrec :: Variable -> FlexRigMap -> ShowS
Show, Singleton (Variable, FlexRig' ()))

mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap TheFlexRigMap -> TheFlexRigMap
f = TheFlexRigMap -> FlexRigMap
FlexRigMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheFlexRigMap -> TheFlexRigMap
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlexRigMap -> TheFlexRigMap
theFlexRigMap

instance Semigroup FlexRigMap where
  FlexRigMap TheFlexRigMap
m <> :: FlexRigMap -> FlexRigMap -> FlexRigMap
<> FlexRigMap TheFlexRigMap
m' = TheFlexRigMap -> FlexRigMap
FlexRigMap forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig TheFlexRigMap
m TheFlexRigMap
m'

instance Monoid FlexRigMap where
  mempty :: FlexRigMap
mempty  = TheFlexRigMap -> FlexRigMap
FlexRigMap forall a. IntMap a
IntMap.empty
  mappend :: FlexRigMap -> FlexRigMap -> FlexRigMap
mappend = forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [FlexRigMap] -> FlexRigMap
mconcat = TheFlexRigMap -> FlexRigMap
FlexRigMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> f (IntMap a) -> IntMap a
IntMap.unionsWith forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map FlexRigMap -> TheFlexRigMap
theFlexRigMap

-- | Compose everything with the 'varFlexRig' part of the 'VarOcc'.
instance IsVarSet () FlexRigMap where
  withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap
withVarOcc VarOcc' ()
o = (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig forall a b. (a -> b) -> a -> b
$ () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. VarOcc' a -> FlexRig' a
varFlexRig VarOcc' ()
o

instance Singleton MetaId () where
  singleton :: MetaId -> ()
singleton MetaId
_ = ()

---------------------------------------------------------------------------
-- * Environment for collecting free variables.

-- | 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IgnoreSorts -> IgnoreSorts -> Bool
$c/= :: IgnoreSorts -> IgnoreSorts -> Bool
== :: IgnoreSorts -> IgnoreSorts -> Bool
$c== :: IgnoreSorts -> IgnoreSorts -> Bool
Eq, Variable -> IgnoreSorts -> ShowS
[IgnoreSorts] -> ShowS
IgnoreSorts -> String
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IgnoreSorts] -> ShowS
$cshowList :: [IgnoreSorts] -> ShowS
show :: IgnoreSorts -> String
$cshow :: IgnoreSorts -> String
showsPrec :: Variable -> IgnoreSorts -> ShowS
$cshowsPrec :: Variable -> IgnoreSorts -> ShowS
Show)

-- | The current context.

data FreeEnv' a b c = FreeEnv
  { forall a b c. FreeEnv' a b c -> b
feExtra     :: !b
    -- ^ Additional context, e.g., whether to ignore free variables in sorts.
  , forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig   :: !(FlexRig' a)
    -- ^ Are we flexible or rigid?
  , forall a b c. FreeEnv' a b c -> Modality
feModality  :: !Modality
    -- ^ What is the current relevance and quantity?
  , forall a b c. FreeEnv' a b c -> Maybe Variable -> c
feSingleton :: Maybe Variable -> c
    -- ^ Method to return a single variable.
  }

type Variable    = Int
type SingleVar c = Variable -> c

type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c

-- | Ignore free variables in sorts.
feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts :: forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts = forall a b c. FreeEnv' a b c -> b
feExtra

instance LensFlexRig a (FreeEnv' a b c) where
  lensFlexRig :: Lens' (FlexRig' a) (FreeEnv' a b c)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f FreeEnv' a b c
e = FlexRig' a -> f (FlexRig' a)
f (forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig FreeEnv' a b c
e) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ FlexRig' a
fr -> FreeEnv' a b c
e { feFlexRig :: FlexRig' a
feFlexRig = FlexRig' a
fr }

instance LensModality (FreeEnv' a b c) where
  getModality :: FreeEnv' a b c -> Modality
getModality = forall a b c. FreeEnv' a b c -> Modality
feModality
  mapModality :: (Modality -> Modality) -> FreeEnv' a b c -> FreeEnv' a b c
mapModality Modality -> Modality
f FreeEnv' a b c
e = FreeEnv' a b c
e { feModality :: Modality
feModality = Modality -> Modality
f (forall a b c. FreeEnv' a b c -> Modality
feModality FreeEnv' a b c
e) }

instance LensRelevance (FreeEnv' a b c) where
instance LensQuantity (FreeEnv' a b c) where

-- | The initial context.

initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv :: forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv b
e SingleVar c
sing = FreeEnv
  { feExtra :: b
feExtra       = b
e
  , feFlexRig :: FlexRig' a
feFlexRig     = forall a. FlexRig' a
Unguarded
  , feModality :: Modality
feModality    = Modality
unitModality      -- multiplicative monoid
  , feSingleton :: Maybe Variable -> c
feSingleton   = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty SingleVar c
sing
  }

type FreeT a b m c = ReaderT (FreeEnv' a b c) m c
type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c

-- | Run function for FreeM.
runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM :: forall a c.
IsVarSet a c =>
SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM SingleVar c
single IgnoreSorts
i FreeM a c
m = forall r a. Reader r a -> r -> a
runReader FreeM a c
m forall a b. (a -> b) -> a -> b
$ forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv IgnoreSorts
i SingleVar c
single

instance (Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c) where
  mempty :: FreeT a b m c
mempty  = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
  mappend :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c
mappend = forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [FreeT a b m c] -> FreeT a b m c
mconcat = forall a. Monoid a => [a] -> a
mconcat forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence

-- | Base case: a variable.
variable :: (Monad m, IsVarSet a c) => Int -> FreeT a b m c
variable :: forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Variable -> FreeT a b m c
variable Variable
n = do
  FlexRig' a
o <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig
  Modality
r <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b c. FreeEnv' a b c -> Modality
feModality
  Maybe Variable -> c
s <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b c. FreeEnv' a b c -> Maybe Variable -> c
feSingleton
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a c. IsVarSet a c => VarOcc' a -> c -> c
withVarOcc (forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
o Modality
r) (Maybe Variable -> c
s forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Variable
n)

-- | Subtract, but return Nothing if result is negative.
subVar :: Int -> Maybe Variable -> Maybe Variable
-- subVar n x = x >>= \ i -> (i - n) <$ guard (n <= i)
subVar :: Variable -> Maybe Variable -> Maybe Variable
subVar Variable
n Maybe Variable
x = do
  Variable
i <- Maybe Variable
x
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Variable
i forall a. Ord a => a -> a -> Bool
>= Variable
n
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Variable
i forall a. Num a => a -> a -> a
- Variable
n

-- | Going under a binder.
underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z
underBinder :: forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder = forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' Variable
1

-- | Going under @n@ binders.
underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z
underBinder' :: forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' Variable
n = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \ FreeEnv' a b c
e -> FreeEnv' a b c
e { feSingleton :: Maybe Variable -> c
feSingleton = forall a b c. FreeEnv' a b c -> Maybe Variable -> c
feSingleton FreeEnv' a b c
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable -> Maybe Variable -> Maybe Variable
subVar Variable
n }

-- | Changing the 'Modality'.
underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z
underModality :: forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> Modality -> Modality
composeModality forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => a -> Modality
getModality

-- | Changing the 'Relevance'.
underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z
underRelevance :: forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> Relevance -> Relevance
composeRelevance forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensRelevance a => a -> Relevance
getRelevance

-- | Changing the 'FlexRig' context.
underFlexRig :: (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) => o -> m z -> m z
underFlexRig :: forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i o. Lens' i o -> LensMap i o
over forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
lensFlexRig forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
lensFlexRig

-- | What happens to the variables occurring under a constructor?
underConstructor :: (MonadReader r m, LensFlexRig a r, Semigroup a) => ConHead -> Elims -> m z -> m z
underConstructor :: forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig a r, Semigroup a) =>
ConHead -> Elims -> m z -> m z
underConstructor (ConHead QName
_c DataOrRecord
_d Induction
i [Arg QName]
fs) Elims
es =
  case Induction
i of
    -- Coinductive (record) constructors admit infinite cycles:
    Induction
CoInductive -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid
    -- Inductive constructors do not admit infinite cycles:
    Induction
Inductive   | forall a. Sized a => a -> Variable
size Elims
es forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Variable
size [Arg QName]
fs -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
StronglyRigid
                | Bool
otherwise          -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig 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.

---------------------------------------------------------------------------
-- * Recursively collecting free variables.

-- | Gather free variables in a collection.
class Free t where
  -- Misplaced SPECIALIZE pragma:
  -- {-# SPECIALIZE freeVars' :: a -> FreeM Any #-}
  -- So you cannot specialize all instances in one go. :(
  freeVars' :: IsVarSet a c => t -> FreeM a c

  default freeVars' :: (t ~ f b, Foldable f, Free b) => IsVarSet a c => t -> FreeM a c
  freeVars' = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars'


instance Free Term where
  -- SPECIALIZE instance does not work as well, see
  -- https://ghc.haskell.org/trac/ghc/ticket/10434#ticket
  -- {-# SPECIALIZE instance Free Term All #-}
  -- {-# SPECIALIZE freeVars' :: Term -> FreeM Any #-}
  -- {-# SPECIALIZE freeVars' :: Term -> FreeM All #-}
  -- {-# SPECIALIZE freeVars' :: Term -> FreeM VarSet #-}
  freeVars' :: forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' Term
t = case Term -> Term
unSpine Term
t of -- #4484: unSpine to avoid projected variables being treated as StronglyRigid
    Var Variable
n Elims
ts     -> forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Variable -> FreeT a b m c
variable Variable
n forall a. Monoid a => a -> a -> a
`mappend` do forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
ts
    -- λ is not considered guarding, as
    -- we cannot prove that x ≡ λy.x is impossible.
    Lam ArgInfo
_ Abs Term
t      -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Abs Term
t
    Lit Literal
_        -> forall a. Monoid a => a
mempty
    Def QName
_ Elims
ts     -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
ts  -- because we are not in TCM
      -- we cannot query whether we are dealing with a data/record (strongly r.)
      -- or a definition by pattern matching (weakly rigid)
      -- thus, we approximate, losing that x = List x is unsolvable
    Con ConHead
c ConInfo
_ Elims
ts   -> forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig a r, Semigroup a) =>
ConHead -> Elims -> m z -> m z
underConstructor ConHead
c Elims
ts forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
ts
    -- Pi is not guarding, since we cannot prove that A ≡ B → A is impossible.
    -- Even as we do not permit infinite type expressions,
    -- we cannot prove their absence (as Set is not inductive).
    -- Also, this is incompatible with univalence (HoTT).
    Pi Dom Type
a Abs Type
b       -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Dom Type
a,Abs Type
b)
    Sort Sort
s       -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Sort
s
    Level Level
l      -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Level
l
    MetaV MetaId
m Elims
ts   -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig (forall a. a -> FlexRig' a
Flexible forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton MetaId
m) forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
ts
    DontCare Term
mt  -> forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality (Relevance -> Quantity -> Cohesion -> Modality
Modality Relevance
Irrelevant Quantity
unitQuantity Cohesion
unitCohesion) forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
mt
    Dummy{}      -> forall a. Monoid a => a
mempty

instance Free t => Free (Type' t) where
  freeVars' :: forall a c. IsVarSet a c => Type' t -> FreeM a c
freeVars' (El Sort
s t
t) =
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreNot forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts))
      {- then -} (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Sort
s, t
t))
      {- else -} (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
t)

instance Free Sort where
  freeVars' :: forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s =
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreAll forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts)) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ {- else -}
    case Sort
s of
      Type Level
a     -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Level
a
      Prop Level
a     -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Level
a
      Inf IsFibrant
_ Integer
_    -> forall a. Monoid a => a
mempty
      SSet Level
a     -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Level
a
      Sort
SizeUniv   -> forall a. Monoid a => a
mempty
      Sort
LockUniv   -> forall a. Monoid a => a
mempty
      Sort
IntervalUniv -> forall a. Monoid a => a
mempty
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig (forall a. a -> FlexRig' a
Flexible forall a. Monoid a => a
mempty) (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' Term Term
a) forall a. Monoid a => a -> a -> a
`mappend`
                        forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid (forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Sort
s1, Abs Sort
s2))
      FunSort Sort
s1 Sort
s2 -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Sort
s1 forall a. Monoid a => a -> a -> a
`mappend` forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Sort
s2
      UnivSort Sort
s -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Sort
s
      MetaS MetaId
x Elims
es -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig (forall a. a -> FlexRig' a
Flexible forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton MetaId
x) forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
es
      DefS QName
_ Elims
es  -> forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig forall a. FlexRig' a
WeaklyRigid forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
es
      DummyS{}   -> forall a. Monoid a => a
mempty

instance Free Level where
  freeVars' :: forall a c. IsVarSet a c => Level -> FreeM a c
freeVars' (Max Integer
_ [PlusLevel' Term]
as) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [PlusLevel' Term]
as

instance Free t => Free (PlusLevel' t) where
  freeVars' :: forall a c. IsVarSet a c => PlusLevel' t -> FreeM a c
freeVars' (Plus Integer
_ t
l)    = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
l

instance Free t => Free [t]            where
instance Free t => Free (Maybe t)      where
instance Free t => Free (WithHiding t) where
instance Free t => Free (Named nm t)

instance (Free t, Free u) => Free (t, u) where
  freeVars' :: forall a c. IsVarSet a c => (t, u) -> FreeM a c
freeVars' (t
t, u
u) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
t forall a. Monoid a => a -> a -> a
`mappend` forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' u
u

instance (Free t, Free u, Free v) => Free (t, u, v) where
  freeVars' :: forall a c. IsVarSet a c => (t, u, v) -> FreeM a c
freeVars' (t
t, u
u, v
v) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
t forall a. Monoid a => a -> a -> a
`mappend` forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' u
u forall a. Monoid a => a -> a -> a
`mappend` forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' v
v

instance Free t => Free (Elim' t) where
  freeVars' :: forall a c. IsVarSet a c => Elim' t -> FreeM a c
freeVars' (Apply Arg t
t) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Arg t
t
  freeVars' (Proj{} ) = forall a. Monoid a => a
mempty
  freeVars' (IApply t
x t
y t
r) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (t
x,t
y,t
r)

instance Free t => Free (Arg t) where
  freeVars' :: forall a c. IsVarSet a c => Arg t -> FreeM a c
freeVars' Arg t
t = forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality (forall a. LensModality a => a -> Modality
getModality Arg t
t) forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg t
t

instance Free t => Free (Dom t) where
  freeVars' :: forall a c. IsVarSet a c => Dom t -> FreeM a c
freeVars' Dom t
d = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (forall t e. Dom' t e -> Maybe t
domTactic Dom t
d, forall t e. Dom' t e -> e
unDom Dom t
d)

instance Free t => Free (Abs t) where
  freeVars' :: forall a c. IsVarSet a c => Abs t -> FreeM a c
freeVars' (Abs   String
_ t
b) = forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
b
  freeVars' (NoAbs String
_ t
b) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' t
b

instance Free t => Free (Tele t) where
  freeVars' :: forall a c. IsVarSet a c => Tele t -> FreeM a c
freeVars' Tele t
EmptyTel          = forall a. Monoid a => a
mempty
  freeVars' (ExtendTel t
t Abs (Tele t)
tel) = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (t
t, Abs (Tele t)
tel)

instance Free Clause where
  freeVars' :: forall a c. IsVarSet a c => Clause -> FreeM a c
freeVars' Clause
cl = forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' (forall a. Sized a => a -> Variable
size forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
cl) forall a b. (a -> b) -> a -> b
$ forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl

instance Free EqualityView where
  freeVars' :: forall a c. IsVarSet a c => EqualityView -> FreeM a c
freeVars' = \case
    OtherType Type
t -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Type
t
    IdiomType Type
t -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Type
t
    EqualityType Sort
s QName
_eq Args
l Arg Term
t Arg Term
a Arg Term
b -> forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Sort
s, Args
l, [Arg Term
t, Arg Term
a, Arg Term
b])