-- | 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 ( MonadReader(..), asks, ReaderT, Reader, runReader )

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


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

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

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

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

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

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

insertMetaSet :: MetaId -> MetaSet -> MetaSet
insertMetaSet :: MetaId -> MetaSet -> MetaSet
insertMetaSet MetaId
m (MetaSet HashSet MetaId
ms) = HashSet MetaId -> MetaSet
MetaSet (HashSet MetaId -> MetaSet) -> HashSet MetaId -> MetaSet
forall a b. (a -> b) -> a -> b
$ MetaId -> HashSet MetaId -> HashSet MetaId
forall a. (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 = (MetaId -> a -> a) -> a -> HashSet MetaId -> a
forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr MetaId -> a -> a
f a
e (HashSet MetaId -> a) -> HashSet MetaId -> a
forall a b. (a -> b) -> a -> b
$ MetaSet -> HashSet MetaId
theMetaSet MetaSet
ms

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

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

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

type FlexRig = FlexRig' MetaSet

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

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

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

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

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

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

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

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

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

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

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

-- | Unit for 'composeFlexRig'.
oneFlexRig :: FlexRig' a
oneFlexRig :: forall a. 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
  { forall a. VarOcc' a -> FlexRig' a
varFlexRig   :: FlexRig' a
  , forall a. VarOcc' a -> Modality
varModality  :: Modality
  }
  deriving (Variable -> VarOcc' a -> ShowS
[VarOcc' a] -> ShowS
VarOcc' a -> String
(Variable -> VarOcc' a -> ShowS)
-> (VarOcc' a -> String)
-> ([VarOcc' a] -> ShowS)
-> Show (VarOcc' a)
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
$cshowsPrec :: forall a. Show a => Variable -> VarOcc' a -> ShowS
showsPrec :: Variable -> VarOcc' a -> ShowS
$cshow :: forall a. Show a => VarOcc' a -> String
show :: VarOcc' a -> String
$cshowList :: forall a. Show a => [VarOcc' a] -> ShowS
showList :: [VarOcc' a] -> ShowS
Show)
type VarOcc = VarOcc' MetaSet

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

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

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

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


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

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

-- | The neutral element for variable occurrence aggregation is least serious
--   occurrence: flexible, irrelevant.
--   This is also the absorptive element for 'composeVarOcc', if we ignore
--   the 'MetaSet' in 'Flexible'.
instance (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 :: forall a. VarOcc' a
topVarOcc = FlexRig' a -> Modality -> VarOcc' a
forall a. FlexRig' a -> Modality -> VarOcc' a
VarOcc FlexRig' a
forall a. FlexRig' a
StronglyRigid Modality
topModality

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

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

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

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

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

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

lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap :: forall a. Variable -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap Variable
i = Variable -> IntMap (VarOcc' a) -> Maybe (VarOcc' a)
forall a. Variable -> IntMap a -> Maybe a
IntMap.lookup Variable
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 a b. (a -> b) -> IntMap a -> IntMap b
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 (Variable -> FlexRigMap -> ShowS
[FlexRigMap] -> ShowS
FlexRigMap -> String
(Variable -> FlexRigMap -> ShowS)
-> (FlexRigMap -> String)
-> ([FlexRigMap] -> ShowS)
-> Show FlexRigMap
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Variable -> FlexRigMap -> ShowS
showsPrec :: Variable -> FlexRigMap -> ShowS
$cshow :: FlexRigMap -> String
show :: FlexRigMap -> String
$cshowList :: [FlexRigMap] -> ShowS
showList :: [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 a b. (a -> b) -> IntMap a -> IntMap b
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 a b. a -> FlexRig' b -> FlexRig' a
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
$c== :: IgnoreSorts -> IgnoreSorts -> Bool
== :: IgnoreSorts -> IgnoreSorts -> Bool
$c/= :: IgnoreSorts -> IgnoreSorts -> Bool
/= :: IgnoreSorts -> IgnoreSorts -> Bool
Eq, Variable -> IgnoreSorts -> ShowS
[IgnoreSorts] -> ShowS
IgnoreSorts -> String
(Variable -> IgnoreSorts -> ShowS)
-> (IgnoreSorts -> String)
-> ([IgnoreSorts] -> ShowS)
-> Show IgnoreSorts
forall a.
(Variable -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Variable -> IgnoreSorts -> ShowS
showsPrec :: Variable -> IgnoreSorts -> ShowS
$cshow :: IgnoreSorts -> String
show :: IgnoreSorts -> String
$cshowList :: [IgnoreSorts] -> ShowS
showList :: [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 = FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a b c. FreeEnv' a b c -> b
feExtra

instance LensFlexRig (FreeEnv' a b c) a where
  lensFlexRig :: Lens' (FreeEnv' a b c) (FlexRig' a)
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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FlexRig' a
fr -> FreeEnv' a b c
e { feFlexRig = 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 = f (feModality 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     = FlexRig' a
forall a. FlexRig' a
Unguarded
  , feModality :: Modality
feModality    = Modality
unitModality      -- multiplicative monoid
  , feSingleton :: Maybe Variable -> c
feSingleton   = c -> SingleVar c -> Maybe Variable -> 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 :: forall a c.
IsVarSet a c =>
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 (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 a. a -> ReaderT (FreeEnv' a b c) m a
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)
forall (m :: * -> *) a. Monad m => [m a] -> m [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
  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
  r <- asks feModality
  s <- asks feSingleton
  return $ withVarOcc (VarOcc o r) (s $ Just 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
  i <- Maybe Variable
x
  guard $ i >= n
  return $ i - 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 = Variable -> m z -> m z
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 = (FreeEnv' a b c -> FreeEnv' a b c) -> m z -> m z
forall a. (FreeEnv' a b c -> FreeEnv' a b c) -> m a -> m a
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 = feSingleton e . subVar 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 = (r -> r) -> m z -> m z
forall a. (r -> r) -> m a -> m a
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 :: forall r (m :: * -> *) o z.
(MonadReader r m, LensRelevance r, LensRelevance o) =>
o -> m z -> m z
underRelevance = (r -> r) -> m z -> m z
forall a. (r -> r) -> m a -> m a
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

-- | In the given computation the 'Quantity' is locally scaled using
-- the 'Quantity' of the first argument.
underQuantity ::
  (MonadReader r m, LensQuantity r, LensQuantity o) => o -> m a -> m a
underQuantity :: forall r (m :: * -> *) o a.
(MonadReader r m, LensQuantity r, LensQuantity o) =>
o -> m a -> m a
underQuantity = (r -> r) -> m a -> m a
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> m a -> m a) -> (o -> r -> r) -> o -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantity -> Quantity) -> r -> r
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity ((Quantity -> Quantity) -> r -> r)
-> (o -> Quantity -> Quantity) -> o -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> Quantity -> Quantity
composeQuantity (Quantity -> Quantity -> Quantity)
-> (o -> Quantity) -> o -> Quantity -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. o -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity

-- | Changing the 'FlexRig' context.
underFlexRig :: (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) => o -> m z -> m z
underFlexRig :: forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig = (r -> r) -> m z -> m z
forall a. (r -> r) -> m a -> m a
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' r (FlexRig' a) -> LensMap r (FlexRig' a)
forall o i. Lens' o i -> LensMap o i
over (FlexRig' a -> f (FlexRig' a)) -> r -> f r
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' r (FlexRig' a)
lensFlexRig LensMap r (FlexRig' a)
-> (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' o (FlexRig' a) -> o -> FlexRig' a
forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
view (FlexRig' a -> f (FlexRig' a)) -> o -> f o
forall o a. LensFlexRig o a => Lens' o (FlexRig' a)
Lens' o (FlexRig' a)
lensFlexRig

-- | What happens to the variables occurring under a constructor?
underConstructor :: (MonadReader r m, LensFlexRig r a, Semigroup a) => ConHead -> Elims -> m z -> m z
underConstructor :: forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig r a, 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 -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid
    -- Inductive constructors do not admit infinite cycles:
    Induction
Inductive   | Elims -> Peano
forall a. Sized a => a -> Peano
natSize Elims
es Peano -> Peano -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg QName] -> Peano
forall a. Sized a => a -> Peano
natSize [Arg QName]
fs -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
StronglyRigid
                | Bool
otherwise                -> FlexRig' a -> m z -> m z
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid
    -- Jesper, 2020-10-22: Issue #4995: treat occurrences in non-fully
    -- applied constructors as weakly rigid.
    -- Ulf, 2019-10-18: Now the termination checker treats inductive recursive records
    -- the same as datatypes, so absense of infinite cycles can be proven in Agda, and thus
    -- the unifier is allowed to do it too. Test case: test/Succeed/Issue1271a.agda
    -- WAS:
    -- -- Inductive record constructors do not admit infinite cycles,
    -- -- but this cannot be proven inside Agda.
    -- -- Thus, unification should not prove it either.

---------------------------------------------------------------------------
-- * 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 m a. Monoid m => (a -> m) -> f a -> m
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
forall a c. IsVarSet a c => b -> 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     -> Variable -> FreeM a c
forall (m :: * -> *) a c b.
(Monad m, IsVarSet a c) =>
Variable -> FreeT a b m c
variable Variable
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 r a, Semigroup a, LensFlexRig o a) =>
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
forall a c. IsVarSet a c => Elims -> 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      -> FlexRig' a -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
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
$ Abs Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Abs Term -> 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 r a, Semigroup a, LensFlexRig o a) =>
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
forall a c. IsVarSet a c => Elims -> 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 -> Elims -> FreeM a c -> FreeM a c
forall r (m :: * -> *) a z.
(MonadReader r m, LensFlexRig r a, Semigroup a) =>
ConHead -> Elims -> m z -> m z
underConstructor ConHead
c Elims
ts (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
forall a c. IsVarSet a c => Elims -> 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
forall a c. IsVarSet a c => (Dom Type, Abs Type) -> 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
forall a c. IsVarSet a c => Sort -> 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
forall a c. IsVarSet a c => Level -> 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 r a, Semigroup a, LensFlexRig o a) =>
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
forall a c. IsVarSet a c => Elims -> 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 -> PolarityModality -> Modality
Modality Relevance
irrelevant Quantity
unitQuantity Cohesion
unitCohesion PolarityModality
unitPolarity) (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
forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' Term
mt
    Dummy{}      -> FreeM a c
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) =
    ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((FreeEnv' a IgnoreSorts c -> Bool)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
forall a. Eq a => a -> a -> Bool
==) (IgnoreSorts -> Bool)
-> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
-> FreeEnv' a IgnoreSorts c
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts))
      {- then -} ((Sort, t) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Sort, t) -> FreeM a c
freeVars' (Sort
s, t
t))
      {- else -} (t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. 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 =
    ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((FreeEnv' a IgnoreSorts c -> Bool)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreAll IgnoreSorts -> IgnoreSorts -> Bool
forall a. Eq a => a -> a -> Bool
==) (IgnoreSorts -> Bool)
-> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
-> FreeEnv' a IgnoreSorts c
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts)) ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ {- else -}
    case Sort
s of
      Univ Univ
_ Level
a   -> Level -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Level -> FreeM a c
freeVars' Level
a
      Inf Univ
_ Integer
_    -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
      Sort
SizeUniv   -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
      Sort
LockUniv   -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
      Sort
LevelUniv  -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
      Sort
IntervalUniv -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a
mempty
      PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig (a -> FlexRig' a
forall a. a -> FlexRig' a
Flexible a
forall a. Monoid a => a
mempty) (Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' (Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Term
forall t e. Dom' t e -> e
unDom Dom' Term Term
a) ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a -> a -> a
`mappend`
                        FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid ((Sort, Abs Sort) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Sort, Abs Sort) -> FreeM a c
freeVars' (Sort
s1, Abs Sort
s2))
      FunSort Sort
s1 Sort
s2 -> Sort -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s1 ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a. Monoid a => a -> a -> a
`mappend` Sort -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s2
      UnivSort Sort
s -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Sort -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s
      MetaS MetaId
x Elims
es -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
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) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Elims -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Elims -> FreeM a c
freeVars' Elims
es
      DefS QName
_ Elims
es  -> FlexRig' a
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall r (m :: * -> *) a o z.
(MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) =>
o -> m z -> m z
underFlexRig FlexRig' a
forall a. FlexRig' a
WeaklyRigid (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Elims -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Elims -> FreeM a c
freeVars' Elims
es
      DummyS{}   -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
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) = [PlusLevel' Term] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => [PlusLevel' Term] -> 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)    = t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => t -> FreeM a c
freeVars' t
l

instance Free t => Free [t]
instance Free t => Free (List1 t)
instance Free t => Free (Maybe t)
instance Free t => Free (WithHiding t)
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) = t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. 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
forall a c. IsVarSet a c => u -> 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) = t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. 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
forall a c. IsVarSet a c => u -> 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
forall a c. IsVarSet a c => v -> 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) = Arg t -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Arg 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
forall a c. IsVarSet a c => (t, t, 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 = Modality
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity 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) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => t -> FreeM a c
freeVars' (t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity 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' :: forall a c. IsVarSet a c => 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
forall a c. IsVarSet a c => (Maybe Term, 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' :: forall a c. IsVarSet a c => Abs t -> FreeM a c
freeVars' (Abs   String
_ t
b) = ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
m z -> m z
underBinder (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => t -> FreeM a c
freeVars' t
b
  freeVars' (NoAbs String
_ t
b) = t -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. 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          = 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
forall a c. IsVarSet a c => (t, Abs (Tele 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 = Variable
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b c (m :: * -> *) z.
MonadReader (FreeEnv' a b c) m =>
Variable -> m z -> m z
underBinder' (Telescope -> Variable
forall a. Sized a => a -> Variable
size (Telescope -> Variable) -> Telescope -> Variable
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
cl) (ReaderT (FreeEnv' a IgnoreSorts c) Identity c
 -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall a b. (a -> b) -> a -> b
$ Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Maybe Term -> FreeM a c
freeVars' (Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c)
-> Maybe Term -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
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 -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
    IdiomType Type
t -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
    EqualityType Sort
s QName
_eq Args
l Arg Term
t Arg Term
a Arg Term
b -> (Sort, Args, Args) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Sort, Args, Args) -> FreeM a c
freeVars' (Sort
s, Args
l, [Arg Term
t, Arg Term
a, Arg Term
b])