{-# LANGUAGE AllowAmbiguousTypes, CPP #-}
{-# OPTIONS_GHC -Wunused-imports #-}

#if  __GLASGOW_HASKELL__ > 902
{-# OPTIONS_GHC -fworker-wrapper-cbv #-}
#endif

{- |
Computing free variables of a term generically. Different queries can be specialized to the
appropriate short-circuiting behavior and to only pass around the necessary data. A query can be
written as an instance to the 'ComputeFree' class which bundles all parameters of the generic
traversal. The traversal itself is defined in the instance of the 'Free' class. See
Agda.TypeChecking.Free for examples of queries.

Background notes:

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 the 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 the purpose of 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.Generic where

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Free.Base

import Agda.Utils.ExpandCase
import Agda.Utils.Lens
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.Monad
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.StrictReader

--------------------------------------------------------------------------------

-- | Instances of 'ComputeFree' are inputs to the generic traveral implemented by 'Free' instances.
--   The @r@ type parameter denotes the 'Reader' environment of the traversal.
class (ExpandCase (Collect r), Monoid (Collect r)) => ComputeFree r where
  type Collect r
  -- ^ The result type of the traversal. Most commonly, this is either a newtype wrapper on 'Bool'
  --   or some instantiation of 'StrictEndo' from 'Agda.Utils.StrictEndo'. The latter is used to
  --   efficiently accummulate sets or maps.
  underBinders'     :: Int -> r -> r
  -- ^ Update the environment when going under some number of binders.
  underConstructor' :: ConHead -> Elims -> r -> r
  -- ^ Update the environment when descending into the spine of a constructor.
  underModality'    :: Maybe (Modality -> r -> r)
  -- ^ Update the environment when going under a modality. 'Nothing' has the identity action.
  underFlexRig'     :: Maybe (FlexRig -> r -> r)
  -- ^ Update the environment when the rigidity of the current position changes, e.g. we switch to
  --   flexible mode when going into the spine of an unsolved metavariable. See the 'Free' instances
  --   for details. 'Nothing' has the identity action. NOTE: since 'Modality' contains 'FlexRig'
  --   information, if you implement a non-trivial 'FlexRig' update, you must also implement a
  --   non-trivial modality update, in order to handle the 'FlexRig'-s there!
  underRelevance'   :: Maybe (Relevance -> r -> r)
  -- ^ Update the environment with relevance information. 'Nothing' has the identity action. NOTE:
  --   since 'Modality' contains relevances, if you implement non-trivial 'Relevance' update, you
  --   must also implement a non-trivial modality update, to handle the relevances there!
  variable'         :: Int -> r -> Collect r
  -- ^ Evaluating a single variable. NOTE: you have to disambiguate bound and free variables yourself!
  --   For example, when we collect all free variables in a set, we need to store an 'Int' in the reader
  --   environment to keep track of the size of the local scope, which allows us to distinguish bound and
  --   free vars.
  ignoreSorts'      :: IgnoreSorts
  -- ^ Do we want to skip over sorts of types?

  ignoreSorts'            = IgnoreSorts
IgnoreNot; {-# INLINE ignoreSorts' #-}
  underConstructor' ConHead
_ Elims
_ r
r = r
r;         {-# INLINE underConstructor' #-}
  underModality'          = Maybe (Modality -> r -> r)
forall a. Maybe a
Nothing;   {-# INLINE underModality'    #-}
  underFlexRig'           = Maybe (FlexRig -> r -> r)
forall a. Maybe a
Nothing;   {-# INLINE underFlexRig'     #-}
  underRelevance'         = Maybe (Relevance -> r -> r)
forall a. Maybe a
Nothing;   {-# INLINE underRelevance'   #-}

{-# INLINE underBinders #-}
underBinders :: ComputeFree r => Int -> Reader r (Collect r) -> Reader r (Collect r)
underBinders :: forall r.
ComputeFree r =>
Int -> Reader r (Collect r) -> Reader r (Collect r)
underBinders = (r -> r) -> Reader r (Collect r) -> Reader r (Collect r)
forall a. (r -> r) -> Reader r a -> Reader r a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((r -> r) -> Reader r (Collect r) -> Reader r (Collect r))
-> (Int -> r -> r)
-> Int
-> Reader r (Collect r)
-> Reader r (Collect r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> r -> r
forall r. ComputeFree r => Int -> r -> r
underBinders'

{-# INLINE underBinder #-}
underBinder :: ComputeFree r => Reader r (Collect r) -> Reader r (Collect r)
underBinder :: forall r.
ComputeFree r =>
Reader r (Collect r) -> Reader r (Collect r)
underBinder = Int -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
Int -> Reader r (Collect r) -> Reader r (Collect r)
underBinders Int
1

{-# INLINE underConstructor #-}
underConstructor :: ComputeFree r => ConHead -> Elims -> Reader r (Collect r) -> Reader r (Collect r)
underConstructor :: forall r.
ComputeFree r =>
ConHead -> Elims -> Reader r (Collect r) -> Reader r (Collect r)
underConstructor ConHead
hd Elims
es = (r -> r) -> Reader r (Collect r) -> Reader r (Collect r)
forall a. (r -> r) -> Reader r a -> Reader r a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ConHead -> Elims -> r -> r
forall r. ComputeFree r => ConHead -> Elims -> r -> r
underConstructor' ConHead
hd Elims
es)

{-# INLINE underModality #-}
underModality :: ComputeFree r => Modality -> Reader r (Collect r) -> Reader r (Collect r)
underModality :: forall r.
ComputeFree r =>
Modality -> Reader r (Collect r) -> Reader r (Collect r)
underModality Modality
m Reader r (Collect r)
act = case Maybe (Modality -> r -> r)
forall r. ComputeFree r => Maybe (Modality -> r -> r)
underModality' of
  Maybe (Modality -> r -> r)
Nothing -> Reader r (Collect r)
act
  Just Modality -> r -> r
f  -> (r -> r) -> Reader r (Collect r) -> Reader r (Collect r)
forall a. (r -> r) -> Reader r a -> Reader r a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Modality -> r -> r
f Modality
m) Reader r (Collect r)
act

{-# INLINE underRelevance #-}
underRelevance :: ComputeFree r => Relevance -> Reader r (Collect r) -> Reader r (Collect r)
underRelevance :: forall r.
ComputeFree r =>
Relevance -> Reader r (Collect r) -> Reader r (Collect r)
underRelevance Relevance
rel Reader r (Collect r)
act = case Maybe (Relevance -> r -> r)
forall r. ComputeFree r => Maybe (Relevance -> r -> r)
underRelevance' of
  Maybe (Relevance -> r -> r)
Nothing -> Reader r (Collect r)
act
  Just Relevance -> r -> r
f  -> (r -> r) -> Reader r (Collect r) -> Reader r (Collect r)
forall a. (r -> r) -> Reader r a -> Reader r a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Relevance -> r -> r
f Relevance
rel) Reader r (Collect r)
act

{-# INLINE underFlexRig #-}
underFlexRig :: ComputeFree r => FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig :: forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
fr Reader r (Collect r)
act = case Maybe (FlexRig -> r -> r)
forall r. ComputeFree r => Maybe (FlexRig -> r -> r)
underFlexRig' of
  Maybe (FlexRig -> r -> r)
Nothing -> Reader r (Collect r)
act
  Just FlexRig -> r -> r
f  -> (r -> r) -> Reader r (Collect r) -> Reader r (Collect r)
forall a. (r -> r) -> Reader r a -> Reader r a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (FlexRig -> r -> r
f FlexRig
fr) Reader r (Collect r)
act

{-# INLINE variable #-}
variable :: ComputeFree r => Int -> Reader r (Collect r)
variable :: forall r. ComputeFree r => Int -> Reader r (Collect r)
variable Int
x = Int -> r -> Collect r
forall r. ComputeFree r => Int -> r -> Collect r
variable' Int
x (r -> Collect r) -> Reader r r -> Reader r (Collect r)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Reader r r
forall r (m :: * -> *). MonadReader r m => m r
ask

--------------------------------------------------------------------------------

class Free t where
  freeVars :: ComputeFree r => t -> Reader r (Collect r)

--------------------------------------------------------------------------------

instance Free Term where
  freeVars :: forall r. ComputeFree r => Term -> Reader r (Collect r)
  freeVars :: forall r. ComputeFree r => Term -> Reader r (Collect r)
freeVars Term
t = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret ->

    let t' :: Term
t' = case (forall r. ComputeFree r => Maybe (Modality -> r -> r)
underModality' @r, forall r. ComputeFree r => Maybe (FlexRig -> r -> r)
underFlexRig' @r) of
               (Maybe (Modality -> r -> r)
Nothing, Maybe (FlexRig -> r -> r)
Nothing) -> Term
t
               (Maybe (Modality -> r -> r), Maybe (FlexRig -> r -> r))
_                  -> Term -> Term
unSpine Term
t
    in case Term
t' of
      Var Int
n Elims
ts   -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Int -> Reader r (Collect r)
forall r. ComputeFree r => Int -> Reader r (Collect r)
variable Int
n Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Elims -> Reader r (Collect r)
freeVars Elims
ts))
      Def QName
_ Elims
ts   -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Elims -> Reader r (Collect r)
freeVars Elims
ts)
      MetaV MetaId
m Elims
ts -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig (MetaSet -> FlexRig
forall a. a -> FlexRig' a
Flexible (MetaId -> MetaSet
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m)) (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Elims -> Reader r (Collect r)
freeVars Elims
ts)

      -- λ is not considered guarding, as
      -- we cannot prove that x ≡ λy.x is impossible.
      Lam ArgInfo
_ Abs Term
t      -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Abs Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Abs Term -> Reader r (Collect r)
freeVars Abs Term
t)
      Lit Literal
_        -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret Reader r (Collect r)
forall a. Monoid a => a
mempty

        -- 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   ->  Reader r (Collect r) -> Result (Reader r (Collect r))
ret (ConHead -> Elims -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
ConHead -> Elims -> Reader r (Collect r) -> Reader r (Collect r)
underConstructor ConHead
c Elims
ts (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Elims -> Reader r (Collect r)
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).

      -- András 2026-01-22: the above comment is wrong if we use occurrence computation in RHS unification
      Pi Dom Type
a Abs Type
b       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Type) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r.
ComputeFree r =>
(Dom Type, Abs Type) -> Reader r (Collect r)
freeVars (Dom Type
a, Abs Type
b)
      Sort Sort
s       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Relevance -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
Relevance -> Reader r (Collect r) -> Reader r (Collect r)
underRelevance Relevance
shapeIrrelevant (Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Sort -> Reader r (Collect r)
freeVars Sort
s)
      Level Level
l      -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Level -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Level -> Reader r (Collect r)
freeVars Level
l
      DontCare Term
mt  -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Modality -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
Modality -> Reader r (Collect r) -> Reader r (Collect r)
underModality (Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality
Modality Relevance
irrelevant Quantity
unitQuantity Cohesion
unitCohesion PolarityModality
unitPolarity) (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Term -> Reader r (Collect r)
freeVars Term
mt
      Dummy{}      -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty

instance Free t => Free (Elim' t) where
  freeVars :: forall r. ComputeFree r => Elim' t -> Reader r (Collect r)
freeVars Elim' t
e = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case Elim' t
e of
    Apply Arg t
t      -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Arg t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Arg t -> Reader r (Collect r)
freeVars Arg t
t
    Proj{}       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
    IApply t
x t
y t
r -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (t, t, t) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => (t, t, t) -> Reader r (Collect r)
freeVars (t
x,t
y,t
r)

instance Free t => Free (Type' t) where
  freeVars :: forall r. ComputeFree r => Type' t -> Reader r (Collect r)
  freeVars :: forall r. ComputeFree r => Type' t -> Reader r (Collect r)
freeVars Type' t
ty = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case Type' t
ty of
    El Sort
s t
t -> case forall r. ComputeFree r => IgnoreSorts
ignoreSorts' @r of
      IgnoreSorts
IgnoreNot -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Sort, t) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => (Sort, t) -> Reader r (Collect r)
freeVars (Sort
s, t
t)
      IgnoreSorts
_         -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
t

instance Free Sort where
  freeVars :: forall r. ComputeFree r => Sort -> Reader r (Collect r)
  freeVars :: forall r. ComputeFree r => Sort -> Reader r (Collect r)
freeVars Sort
s = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret ->
    case forall r. ComputeFree r => IgnoreSorts
ignoreSorts' @r of
      IgnoreSorts
IgnoreAll -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret Reader r (Collect r)
forall a. Monoid a => a
mempty
      IgnoreSorts
_         -> case Sort
s of
        Univ Univ
_ Level
a       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Level -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Level -> Reader r (Collect r)
freeVars Level
a
        Inf Univ
_ Integer
_        -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
        Sort
SizeUniv       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
        Sort
LockUniv       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
        Sort
LevelUniv      -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
        Sort
IntervalUniv   -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
        PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig (MetaSet -> FlexRig
forall a. a -> FlexRig' a
Flexible MetaSet
forall a. Monoid a => a
mempty) (Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Term -> Reader r (Collect r)
freeVars (Term -> Reader r (Collect r)) -> Term -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Term
forall t e. Dom' t e -> e
unDom Dom' Term Term
a) Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<>
                                FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid ((Sort, Abs Sort) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => (Sort, Abs Sort) -> Reader r (Collect r)
freeVars (Sort
s1, Abs Sort
s2))
        FunSort Sort
s1 Sort
s2  -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Sort -> Reader r (Collect r)
freeVars Sort
s1 Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Sort -> Reader r (Collect r)
freeVars Sort
s2
        UnivSort Sort
s     -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Sort -> Reader r (Collect r)
freeVars Sort
s
        MetaS MetaId
x Elims
es     -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig (MetaSet -> FlexRig
forall a. a -> FlexRig' a
Flexible (MetaSet -> FlexRig) -> MetaSet -> FlexRig
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaSet
forall el coll. Singleton el coll => el -> coll
singleton MetaId
x) (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Elims -> Reader r (Collect r)
freeVars Elims
es
        DefS QName
_ Elims
es      -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
FlexRig -> Reader r (Collect r) -> Reader r (Collect r)
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Elims -> Reader r (Collect r)
freeVars Elims
es
        DummyS{}       -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty

instance Free t => Free (Maybe t) where
  freeVars :: forall r. ComputeFree r => Maybe t -> Reader r (Collect r)
freeVars Maybe t
mt = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case Maybe t
mt of
    Maybe t
Nothing -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret Reader r (Collect r)
forall a. Monoid a => a
mempty
    Just t
t  -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
t

instance Free t => Free [t] where
  freeVars :: forall r. ComputeFree r => [t] -> Reader r (Collect r)
freeVars [t]
ts = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case [t]
ts of
    []   -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret Reader r (Collect r)
forall a. Monoid a => a
mempty
    t
t:[t]
ts -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
t Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> [t] -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => [t] -> Reader r (Collect r)
freeVars [t]
ts

instance Free t => Free (List1 t) where
  freeVars :: forall r. ComputeFree r => List1 t -> Reader r (Collect r)
freeVars List1 t
ts = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case List1 t
ts of
    t
t :| [t]
ts -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
t Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> [t] -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => [t] -> Reader r (Collect r)
freeVars [t]
ts

instance (Free a, Free b) => Free (a, b) where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => (a, b) -> Reader r (Collect r)
freeVars (a, b)
ab = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case (a, b)
ab of (a
a, b
b) -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
freeVars a
a Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => b -> Reader r (Collect r)
freeVars b
b

instance (Free a, Free b, Free c) => Free (a, b, c) where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => (a, b, c) -> Reader r (Collect r)
freeVars (a, b, c)
abc = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case (a, b, c)
abc of (a
a, b
b, c
c) -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
freeVars a
a Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => b -> Reader r (Collect r)
freeVars b
b Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> c -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => c -> Reader r (Collect r)
freeVars c
c

instance (Free a, Free b, Free c, Free d) => Free (a, b, c, d) where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => (a, b, c, d) -> Reader r (Collect r)
freeVars (a, b, c, d)
abc = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case (a, b, c, d)
abc of
    (a
a, b
b, c
c, d
d) -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
freeVars a
a Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => b -> Reader r (Collect r)
freeVars b
b Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> c -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => c -> Reader r (Collect r)
freeVars c
c Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> d -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => d -> Reader r (Collect r)
freeVars d
d

instance (Free a, Free b, Free c, Free d, Free e) => Free (a, b, c, d, e) where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => (a, b, c, d, e) -> Reader r (Collect r)
freeVars (a, b, c, d, e)
abc = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case (a, b, c, d, e)
abc of
    (a
a, b
b, c
c, d
d, e
e) -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
freeVars a
a Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => b -> Reader r (Collect r)
freeVars b
b Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> c -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => c -> Reader r (Collect r)
freeVars c
c Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> d -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => d -> Reader r (Collect r)
freeVars d
d Reader r (Collect r)
-> Reader r (Collect r) -> Reader r (Collect r)
forall a. Semigroup a => a -> a -> a
<> e -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => e -> Reader r (Collect r)
freeVars e
e

instance Free Level where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => Level -> Reader r (Collect r)
freeVars Level
l = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case Level
l of Max Integer
_ [PlusLevel' Term]
as -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ [PlusLevel' Term] -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r.
ComputeFree r =>
[PlusLevel' Term] -> Reader r (Collect r)
freeVars [PlusLevel' Term]
as

instance Free t => Free (PlusLevel' t) where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => PlusLevel' t -> Reader r (Collect r)
freeVars PlusLevel' t
pl = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case PlusLevel' t
pl of Plus Integer
_ t
l -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
l

instance Free t => Free (Arg t) where
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => Arg t -> Reader r (Collect r)
freeVars Arg t
t = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret ->
    Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Modality -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
Modality -> Reader r (Collect r) -> Reader r (Collect r)
underModality (Arg t -> Modality
forall a. LensModality a => a -> Modality
getModality Arg t
t) (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars (t -> Reader r (Collect r)) -> t -> Reader r (Collect r)
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
  {-# INLINE freeVars #-}
  freeVars :: forall r. ComputeFree r => Dom t -> Reader r (Collect r)
freeVars Dom t
d = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Maybe Term, t) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => (Maybe Term, t) -> Reader r (Collect r)
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 r. ComputeFree r => Abs t -> Reader r (Collect r)
freeVars Abs t
t = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case Abs t
t of
    Abs   ArgName
_ t
b -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
Reader r (Collect r) -> Reader r (Collect r)
underBinder (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
b
    NoAbs ArgName
_ t
b -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
freeVars t
b

instance Free t => Free (Tele t) where
  freeVars :: forall r. ComputeFree r => Tele t -> Reader r (Collect r)
freeVars Tele t
tel = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case Tele t
tel of
    Tele t
EmptyTel        -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
    ExtendTel t
t Abs (Tele t)
tel -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (t, Abs (Tele t)) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r.
ComputeFree r =>
(t, Abs (Tele t)) -> Reader r (Collect r)
freeVars (t
t, Abs (Tele t)
tel)

instance Free Clause where
  freeVars :: forall r. ComputeFree r => Clause -> Reader r (Collect r)
freeVars Clause
cl = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret ->
    Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Int -> Reader r (Collect r) -> Reader r (Collect r)
forall r.
ComputeFree r =>
Int -> Reader r (Collect r) -> Reader r (Collect r)
underBinders (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) (Reader r (Collect r) -> Reader r (Collect r))
-> Reader r (Collect r) -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Maybe Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Maybe Term -> Reader r (Collect r)
freeVars (Maybe Term -> Reader r (Collect r))
-> Maybe Term -> Reader r (Collect r)
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
cl

instance Free EqualityView where
  freeVars :: forall r. ComputeFree r => EqualityView -> Reader r (Collect r)
freeVars EqualityView
ev = ((Reader r (Collect r) -> Result (Reader r (Collect r)))
 -> Result (Reader r (Collect r)))
-> Reader r (Collect r)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \Reader r (Collect r) -> Result (Reader r (Collect r))
ret -> case EqualityView
ev of
    OtherType Type
t                   -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Type -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Type -> Reader r (Collect r)
freeVars Type
t
    IdiomType Type
t                   -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Type -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r. ComputeFree r => Type -> Reader r (Collect r)
freeVars Type
t
    EqualityType Range
_r Sort
s QName
_eq Args
l Arg Term
t Arg Term
a Arg Term
b -> Reader r (Collect r) -> Result (Reader r (Collect r))
ret (Reader r (Collect r) -> Result (Reader r (Collect r)))
-> Reader r (Collect r) -> Result (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Sort, Args, (Arg Term, Arg Term, Arg Term))
-> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
forall r.
ComputeFree r =>
(Sort, Args, (Arg Term, Arg Term, Arg Term))
-> Reader r (Collect r)
freeVars (Sort
s, Args
l, (Arg Term
t, Arg Term
a, Arg Term
b))

{-# INLINE defaultUnderConstructor #-}
defaultUnderConstructor :: (Semigroup a, LensFlexRig r a) => ConHead -> Elims -> r -> r
defaultUnderConstructor :: forall a r.
(Semigroup a, LensFlexRig r a) =>
ConHead -> Elims -> r -> r
defaultUnderConstructor ConHead
c Elims
h = 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 (FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig (ConHead -> Elims -> FlexRig' a
forall a. ConHead -> Elims -> FlexRig' a
constructorFlexRig ConHead
c Elims
h))

{-# INLINE defaultUnderFlexRig #-}
defaultUnderFlexRig :: (Semigroup a, LensFlexRig r a) => Maybe (FlexRig' a -> r -> r)
defaultUnderFlexRig :: forall a r.
(Semigroup a, LensFlexRig r a) =>
Maybe (FlexRig' a -> r -> r)
defaultUnderFlexRig = (FlexRig' a -> r -> r) -> Maybe (FlexRig' a -> r -> r)
forall a. a -> Maybe a
Just \FlexRig' a
fr -> 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 (FlexRig' a -> FlexRig' a -> FlexRig' a
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig FlexRig' a
fr)

{-# INLINE defaultUnderModality #-}
defaultUnderModality :: LensModality r => Maybe (Modality -> r -> r)
defaultUnderModality :: forall r. LensModality r => Maybe (Modality -> r -> r)
defaultUnderModality = (Modality -> r -> r) -> Maybe (Modality -> r -> r)
forall a. a -> Maybe a
Just \Modality
m -> (Modality -> Modality) -> r -> r
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality (Modality -> Modality -> Modality
composeModality Modality
m)

{-# INLINE defaultUnderRelevance #-}
defaultUnderRelevance :: LensRelevance r => Maybe (Relevance -> r -> r)
defaultUnderRelevance :: forall r. LensRelevance r => Maybe (Relevance -> r -> r)
defaultUnderRelevance = (Relevance -> r -> r) -> Maybe (Relevance -> r -> r)
forall a. a -> Maybe a
Just \Relevance
rel -> (Relevance -> Relevance) -> r -> r
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance (Relevance -> Relevance -> Relevance
composeRelevance Relevance
rel)