{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE TypeFamilies               #-}

-- | 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.Reader


import Data.Foldable (Foldable, foldMap)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Monoid ( Monoid, mempty, mappend, mconcat )
import Data.Semigroup ( Semigroup, (<>) )



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.Singleton
import Agda.Utils.Size

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

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

newtype MetaSet = MetaSet { MetaSet -> IntSet
theMetaSet :: IntSet }
  deriving (MetaSet -> MetaSet -> Bool
(MetaSet -> MetaSet -> Bool)
-> (MetaSet -> MetaSet -> Bool) -> Eq MetaSet
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, 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
showList :: [MetaSet] -> ShowS
$cshowList :: [MetaSet] -> ShowS
show :: MetaSet -> String
$cshow :: MetaSet -> String
showsPrec :: Int -> MetaSet -> ShowS
$cshowsPrec :: Int -> MetaSet -> ShowS
Show, MetaSet
MetaSet -> Bool
MetaSet -> (MetaSet -> Bool) -> Null MetaSet
forall a. a -> (a -> Bool) -> Null a
null :: MetaSet -> Bool
$cnull :: MetaSet -> Bool
empty :: MetaSet
$cempty :: MetaSet
Null, b -> MetaSet -> MetaSet
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
stimes :: 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
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
mconcat :: [MetaSet] -> MetaSet
$cmconcat :: [MetaSet] -> MetaSet
mappend :: MetaSet -> MetaSet -> MetaSet
$cmappend :: MetaSet -> MetaSet -> MetaSet
mempty :: MetaSet
$cmempty :: MetaSet
$cp1Monoid :: Semigroup MetaSet
Monoid)

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

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

foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet MetaId -> a -> a
f a
e MetaSet
ms = (Int -> a -> a) -> a -> IntSet -> a
forall b. (Int -> b -> b) -> b -> IntSet -> b
IntSet.foldr (MetaId -> a -> a
f (MetaId -> a -> a) -> (Int -> MetaId) -> Int -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MetaId
MetaId) a
e (IntSet -> a) -> IntSet -> a
forall a b. (a -> b) -> a -> b
$ MetaSet -> IntSet
theMetaSet 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
(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
/= :: 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, 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
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 :: Int -> FlexRig' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FlexRig' a -> ShowS
Show, a -> FlexRig' b -> FlexRig' a
(a -> b) -> FlexRig' a -> FlexRig' b
(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
<$ :: a -> FlexRig' b -> FlexRig' a
$c<$ :: forall a b. a -> FlexRig' b -> FlexRig' a
fmap :: (a -> b) -> FlexRig' a -> FlexRig' b
$cfmap :: forall a b. (a -> b) -> FlexRig' a -> FlexRig' b
Functor, FlexRig' a -> Bool
(a -> m) -> FlexRig' a -> m
(a -> b -> b) -> b -> FlexRig' a -> b
(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
product :: FlexRig' a -> a
$cproduct :: forall a. Num a => FlexRig' a -> a
sum :: FlexRig' a -> a
$csum :: forall a. Num a => FlexRig' a -> a
minimum :: FlexRig' a -> a
$cminimum :: forall a. Ord a => FlexRig' a -> a
maximum :: FlexRig' a -> a
$cmaximum :: forall a. Ord a => FlexRig' a -> a
elem :: a -> FlexRig' a -> Bool
$celem :: forall a. Eq a => a -> FlexRig' a -> Bool
length :: FlexRig' a -> Int
$clength :: forall a. FlexRig' a -> Int
null :: FlexRig' a -> Bool
$cnull :: forall a. FlexRig' a -> Bool
toList :: FlexRig' a -> [a]
$ctoList :: forall a. FlexRig' a -> [a]
foldl1 :: (a -> a -> a) -> FlexRig' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldr1 :: (a -> a -> a) -> FlexRig' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FlexRig' a -> a
foldl' :: (b -> a -> b) -> b -> FlexRig' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
foldl :: (b -> a -> b) -> b -> FlexRig' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FlexRig' a -> b
foldr' :: (a -> b -> b) -> b -> FlexRig' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
foldr :: (a -> b -> b) -> b -> FlexRig' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> FlexRig' a -> b
foldMap' :: (a -> m) -> FlexRig' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
foldMap :: (a -> m) -> FlexRig' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexRig' a -> m
fold :: 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 :: (FlexRig' a -> f (FlexRig' a)) -> FlexRig' a -> f (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 :: o -> Bool
isFlexible o
o = case o
o o -> Lens' (FlexRig' a) o -> FlexRig' a
forall o i. o -> Lens' i o -> i
^. forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
Lens' (FlexRig' a) o
lensFlexRig of
  Flexible {} -> Bool
True
  FlexRig' a
_ -> Bool
False

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

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

isStronglyRigid :: LensFlexRig a o => o -> Bool
isStronglyRigid :: o -> Bool
isStronglyRigid o
o = case o
o o -> Lens' (FlexRig' a) o -> FlexRig' a
forall o i. o -> Lens' i o -> i
^. forall a o. LensFlexRig a o => Lens' (FlexRig' 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 :: 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

-- | Unit for 'addFlexRig'.
zeroFlexRig :: Monoid a => FlexRig' a
zeroFlexRig :: 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 :: 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 :: 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

-- | Unit for 'composeFlexRig'.
oneFlexRig :: FlexRig' a
oneFlexRig :: FlexRig' a
oneFlexRig = FlexRig' a
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
  { VarOcc' a -> FlexRig' a
varFlexRig   :: FlexRig' a
  , VarOcc' a -> Modality
varModality  :: 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
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 :: Int -> VarOcc' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> 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 a (VarOcc' a) where
  lensFlexRig :: (FlexRig' a -> f (FlexRig' a)) -> VarOcc' a -> f (VarOcc' 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ FlexRig' a
fr' -> FlexRig' a -> Modality -> VarOcc' a
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' = 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 (Semigroup a, 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 :: 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 :: 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
m Modality -> Modality -> Modality
forall a. Semigroup a => a -> a -> a
<> Modality
m')
  -- We use the multipicative modality monoid (composition).

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

---------------------------------------------------------------------------
-- * 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 { 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
/= :: 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, 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
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 :: Int -> VarMap' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> 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 :: (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 :: 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

instance (Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) where
  withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a
withVarOcc VarOcc' a
o = (TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a
forall a b.
(TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
mapVarMap ((TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a)
-> (TheVarMap' a -> TheVarMap' a) -> VarMap' a -> VarMap' a
forall a b. (a -> b) -> a -> b
$ (VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a)
-> (VarOcc' a -> VarOcc' a) -> TheVarMap' a -> TheVarMap' a
forall a b. (a -> b) -> a -> b
$ VarOcc' a -> VarOcc' a -> VarOcc' a
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 (Int -> FlexRigMap -> ShowS
[FlexRigMap] -> ShowS
FlexRigMap -> String
(Int -> FlexRigMap -> ShowS)
-> (FlexRigMap -> String)
-> ([FlexRigMap] -> ShowS)
-> Show FlexRigMap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FlexRigMap] -> ShowS
$cshowList :: [FlexRigMap] -> ShowS
show :: FlexRigMap -> String
$cshow :: FlexRigMap -> String
showsPrec :: Int -> FlexRigMap -> ShowS
$cshowsPrec :: Int -> FlexRigMap -> ShowS
Show, Singleton (Variable, FlexRig' ()))

mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
mapFlexRigMap TheFlexRigMap -> TheFlexRigMap
f = TheFlexRigMap -> FlexRigMap
FlexRigMap (TheFlexRigMap -> FlexRigMap)
-> (FlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheFlexRigMap -> TheFlexRigMap
f (TheFlexRigMap -> TheFlexRigMap)
-> (FlexRigMap -> TheFlexRigMap) -> FlexRigMap -> TheFlexRigMap
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 (TheFlexRigMap -> FlexRigMap) -> TheFlexRigMap -> FlexRigMap
forall a b. (a -> b) -> a -> b
$ (FlexRig' () -> FlexRig' () -> FlexRig' ())
-> TheFlexRigMap -> TheFlexRigMap -> TheFlexRigMap
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith FlexRig' () -> FlexRig' () -> FlexRig' ()
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 TheFlexRigMap
forall a. IntMap a
IntMap.empty
  mappend :: FlexRigMap -> FlexRigMap -> FlexRigMap
mappend = FlexRigMap -> FlexRigMap -> FlexRigMap
forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [FlexRigMap] -> FlexRigMap
mconcat = TheFlexRigMap -> FlexRigMap
FlexRigMap (TheFlexRigMap -> FlexRigMap)
-> ([FlexRigMap] -> TheFlexRigMap) -> [FlexRigMap] -> FlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlexRig' () -> FlexRig' () -> FlexRig' ())
-> [TheFlexRigMap] -> TheFlexRigMap
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> f (IntMap a) -> IntMap a
IntMap.unionsWith FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
addFlexRig ([TheFlexRigMap] -> TheFlexRigMap)
-> ([FlexRigMap] -> [TheFlexRigMap])
-> [FlexRigMap]
-> TheFlexRigMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FlexRigMap -> TheFlexRigMap) -> [FlexRigMap] -> [TheFlexRigMap]
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 ((TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap)
-> (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
forall a b. (a -> b) -> a -> b
$ (FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap)
-> (FlexRig' () -> FlexRig' ()) -> TheFlexRigMap -> TheFlexRigMap
forall a b. (a -> b) -> a -> b
$ FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig (FlexRig' () -> FlexRig' () -> FlexRig' ())
-> FlexRig' () -> FlexRig' () -> FlexRig' ()
forall a b. (a -> b) -> a -> b
$ () () -> FlexRig' () -> FlexRig' ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VarOcc' () -> FlexRig' ()
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
(IgnoreSorts -> IgnoreSorts -> Bool)
-> (IgnoreSorts -> IgnoreSorts -> Bool) -> Eq IgnoreSorts
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, 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
showList :: [IgnoreSorts] -> ShowS
$cshowList :: [IgnoreSorts] -> ShowS
show :: IgnoreSorts -> String
$cshow :: IgnoreSorts -> String
showsPrec :: Int -> IgnoreSorts -> ShowS
$cshowsPrec :: Int -> IgnoreSorts -> ShowS
Show)

-- | The current context.

data FreeEnv' a b c = FreeEnv
  { FreeEnv' a b c -> b
feExtra     :: !b
    -- ^ Additional context, e.g., whether to ignore free variables in sorts.
  , FreeEnv' a b c -> FlexRig' a
feFlexRig   :: !(FlexRig' a)
    -- ^ Are we flexible or rigid?
  , FreeEnv' a b c -> Modality
feModality  :: !Modality
    -- ^ What is the current relevance and quantity?
  , FreeEnv' a b c -> Maybe Int -> 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 :: FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts = FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a b c. FreeEnv' a b c -> b
feExtra

instance LensFlexRig a (FreeEnv' a b c) where
  lensFlexRig :: (FlexRig' a -> f (FlexRig' a))
-> FreeEnv' a b c -> f (FreeEnv' a b c)
lensFlexRig FlexRig' a -> f (FlexRig' a)
f FreeEnv' a b c
e = FlexRig' a -> f (FlexRig' a)
f (FreeEnv' a b c -> FlexRig' a
forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig FreeEnv' a b c
e) f (FlexRig' a)
-> (FlexRig' a -> FreeEnv' a b c) -> f (FreeEnv' a b c)
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 = FreeEnv' a b c -> Modality
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 (FreeEnv' a b c -> Modality
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 :: b -> SingleVar c -> FreeEnv' a b c
initFreeEnv b
e SingleVar c
sing = FreeEnv :: forall a b c.
b -> FlexRig' a -> Modality -> (Maybe Int -> c) -> FreeEnv' a b c
FreeEnv
  { feExtra :: b
feExtra       = b
e
  , feFlexRig :: FlexRig' a
feFlexRig     = FlexRig' a
forall a. FlexRig' a
Unguarded
  , feModality :: Modality
feModality    = Modality
forall a. Monoid a => a
mempty            -- multiplicative monoid
  , feSingleton :: Maybe Int -> c
feSingleton   = c -> SingleVar c -> Maybe Int -> c
forall b a. b -> (a -> b) -> Maybe a -> b
maybe c
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 :: SingleVar c -> IgnoreSorts -> FreeM a c -> c
runFreeM SingleVar c
single IgnoreSorts
i FreeM a c
m = FreeM a c -> FreeEnv' a IgnoreSorts c -> c
forall r a. Reader r a -> r -> a
runReader FreeM a c
m (FreeEnv' a IgnoreSorts c -> c) -> FreeEnv' a IgnoreSorts c -> c
forall a b. (a -> b) -> a -> b
$ IgnoreSorts -> SingleVar c -> FreeEnv' a IgnoreSorts c
forall c b a. Monoid c => b -> SingleVar c -> FreeEnv' a b c
initFreeEnv IgnoreSorts
i SingleVar c
single

instance (Applicative m, Semigroup c) => Semigroup (FreeT a b m c) where
  <> :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c
(<>) = (c -> c -> c) -> FreeT a b m c -> FreeT a b m c -> FreeT a b m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 c -> c -> c
forall a. Semigroup a => a -> a -> a
(<>)

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  = c -> FreeT a b m c
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
forall a. Monoid a => a
mempty
  mappend :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c
mappend = FreeT a b m c -> FreeT a b m c -> FreeT a b m c
forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [FreeT a b m c] -> FreeT a b m c
mconcat = [c] -> c
forall a. Monoid a => [a] -> a
mconcat ([c] -> c)
-> ([FreeT a b m c] -> ReaderT (FreeEnv' a b c) m [c])
-> [FreeT a b m c]
-> FreeT a b m c
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> [FreeT a b m c] -> ReaderT (FreeEnv' a b c) 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 :: Int -> FreeT a b m c
variable Int
n = do
  FlexRig' a
o <- (FreeEnv' a b c -> FlexRig' a)
-> ReaderT (FreeEnv' a b c) m (FlexRig' a)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FreeEnv' a b c -> FlexRig' a
forall a b c. FreeEnv' a b c -> FlexRig' a
feFlexRig
  Modality
r <- (FreeEnv' a b c -> Modality) -> ReaderT (FreeEnv' a b c) m Modality
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FreeEnv' a b c -> Modality
forall a b c. FreeEnv' a b c -> Modality
feModality
  Maybe Int -> c
s <- (FreeEnv' a b c -> Maybe Int -> c)
-> ReaderT (FreeEnv' a b c) m (Maybe Int -> c)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FreeEnv' a b c -> Maybe Int -> c
forall a b c. FreeEnv' a b c -> Maybe Int -> c
feSingleton
  c -> FreeT a b m c
forall (m :: * -> *) a. Monad m => a -> m a
return (c -> FreeT a b m c) -> c -> FreeT a b m c
forall a b. (a -> b) -> a -> b
$ VarOcc' a -> c -> c
forall a c. IsVarSet a c => VarOcc' a -> c -> c
withVarOcc (FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
o Modality
r) (Maybe Int -> c
s (Maybe Int -> c) -> Maybe Int -> c
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
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 :: Int -> Maybe Int -> Maybe Int
subVar Int
n Maybe Int
x = do
  Int
i <- Maybe Int
x
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n
  Int -> Maybe Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n

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

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

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

-- | Changing the 'Relevance'.
underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z
underRelevance :: o -> m z -> m z
underRelevance = (r -> r) -> m z -> m z
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Relevance -> Relevance) -> r -> r
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance ((Relevance -> Relevance) -> r -> r)
-> (o -> Relevance -> Relevance) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relevance -> Relevance -> Relevance
composeRelevance (Relevance -> Relevance -> Relevance)
-> (o -> Relevance) -> o -> Relevance -> Relevance
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Relevance
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 :: o -> m z -> m z
underFlexRig = (r -> r) -> m z -> m z
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m z -> m z) -> (o -> r -> r) -> o -> m z -> m z
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (FlexRig' a) r -> LensMap (FlexRig' a) r
forall i o. Lens' i o -> LensMap i o
over forall a o. LensFlexRig a o => Lens' (FlexRig' a) o
Lens' (FlexRig' a) r
lensFlexRig LensMap (FlexRig' a) r
-> (o -> FlexRig' a -> FlexRig' a) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig (FlexRig' a -> FlexRig' a -> FlexRig' a)
-> (o -> FlexRig' a) -> o -> FlexRig' a -> FlexRig' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (FlexRig' a) o -> o -> FlexRig' a
forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view forall a o. LensFlexRig a o => Lens' (FlexRig' 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 -> m z -> m z
underConstructor :: ConHead -> m z -> m z
underConstructor (ConHead QName
c Induction
i [Arg QName]
fs) =
  case (Induction
i,[Arg QName]
fs) of
    -- Coinductive (record) constructors admit infinite cycles:
    (Induction
CoInductive, [Arg QName]
_)   -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid
    -- Inductive constructors do not admit infinite cycles:
    (Induction
Inductive, [Arg QName]
_)    -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
StronglyRigid
    -- 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.
    -- (Inductive, (_:_)) -> id

---------------------------------------------------------------------------
-- * 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' = (b -> FreeM a c) -> f b -> FreeM a c
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> FreeM a c
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' :: 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 Int
n Elims
ts     -> Int -> FreeM a c
forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Int -> FreeT a b m c
variable Int
n FreeM a c -> FreeM a c -> FreeM a c
forall a. Monoid a => a -> a -> a
`mappend` do FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
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      -> Abs Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Abs Term
t
    Lit Literal
_        -> FreeM a c
forall a. Monoid a => a
mempty
    Def QName
_ Elims
ts     -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
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   -> ConHead -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig a r, Semigroup a) =>
ConHead -> m z -> m z
underConstructor ConHead
c (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
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       -> (Dom Type, Abs Type) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Dom Type
a,Abs Type
b)
    Sort Sort
s       -> Sort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Sort
s
    Level Level
l      -> Level -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Level
l
    MetaV MetaId
m Elims
ts   -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ MetaId -> a
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
ts
    DontCare Term
mt  -> Modality -> FreeM a c -> FreeM a c
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
forall a. Monoid a => a
mempty Cohesion
forall a. Monoid a => a
mempty) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
mt
    Dummy{}      -> FreeM a c
forall a. Monoid a => a
mempty

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

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

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

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

instance Free LevelAtom where
  freeVars' :: LevelAtom' Term -> FreeM a c
freeVars' LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
m Elims
vs   -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) =>
o -> m z -> m z
underFlexRig (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible (a -> FlexRig' a) -> a -> FlexRig' a
forall a b. (a -> b) -> a -> b
$ MetaId -> a
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Elims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Elims
vs
    NeutralLevel NotBlocked
_ Term
v -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
v
    BlockedLevel MetaId
_ Term
v -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
v
    UnreducedLevel Term
v -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
v

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

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

instance Free t => Free (Elim' t) where
  freeVars' :: Elim' t -> FreeM a c
freeVars' (Apply Arg t
t) = Arg t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Arg t
t
  freeVars' (Proj{} ) = FreeM a c
forall a. Monoid a => a
mempty
  freeVars' (IApply t
x t
y t
r) = (t, t, t) -> FreeM a c
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' :: Arg t -> FreeM a c
freeVars' Arg t
t = Modality -> FreeM a c -> FreeM a c
forall r (m :: * -> *) o z.
(MonadReader r m, LensModality r, LensModality o) =>
o -> m z -> m z
underModality (Arg t -> Modality
forall a. LensModality a => a -> Modality
getModality Arg t
t) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (t -> FreeM a c) -> t -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Arg t -> t
forall e. Arg e -> e
unArg Arg t
t

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

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

instance Free t => Free (Tele t) where
  freeVars' :: Tele t -> FreeM a c
freeVars' Tele t
EmptyTel          = FreeM a c
forall a. Monoid a => a
mempty
  freeVars' (ExtendTel t
t Abs (Tele t)
tel) = (t, Abs (Tele t)) -> FreeM a c
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' :: Clause -> FreeM a c
freeVars' Clause
cl = Int -> FreeM a c -> FreeM a c
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Int -> m z -> m z
underBinder' (Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
cl) (FreeM a c -> FreeM a c) -> FreeM a c -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Maybe Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Maybe Term -> FreeM a c) -> Maybe Term -> FreeM a c
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl

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