{-# 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 Mikan.TypeChecking.Free.Generic where

import Mikan.Syntax.Common
import Mikan.Syntax.Internal.Telescope
import Mikan.Syntax.Internal.Clause
import Mikan.Syntax.Internal.Term
import Mikan.Syntax.Internal.Dom

import Mikan.TypeChecking.Free.Base

import Mikan.Utils.ExpandCase
import Mikan.Utils.Lens
import Mikan.Utils.List1 (List1, pattern (:|))
import Mikan.Utils.Monad
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.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 LiftedRep (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 'Mikan.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.
  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.
  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' #-}
  underFlexRig'           = Maybe (FlexRig -> r -> r)
forall a. Maybe a
Nothing;   {-# INLINE underFlexRig'     #-}

{-# 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 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret ->

    let t' :: Term
t' = case forall r. ComputeFree r => Maybe (FlexRig -> r -> r)
underFlexRig' @r of
               Maybe (FlexRig -> r -> r)
Nothing -> Term
t
               Maybe (FlexRig -> r -> r)
_       -> Term -> Term
unSpine Term
t
    in case Term
t' of
      Var Int
n Elims
ts   -> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Elims
ts))
      Def QName
_ Elims
ts   -> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Elims
ts)
      MetaV MetaId
m Elims
ts -> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 LiftedRep (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 r. ComputeFree r => Abs Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Abs Term
t)
      Lit Literal
_        -> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (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 r. ComputeFree r => Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 Type 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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Type) -> Reader r (Collect r)
forall r.
ComputeFree r =>
(Dom Type, Abs Type) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars (Dom Type
a, Abs Type
b)
      Sort Sort
s       -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Sort -> Reader r (Collect r)
forall r. ComputeFree r => Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Sort
s
      Level Level
l      -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Level -> Reader r (Collect r)
forall r. ComputeFree r => Level -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Level
l
      DontCare Term
mt  -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Term -> Reader r (Collect r)
forall r. ComputeFree r => Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Term
mt
      Dummy{}      -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case Elim' t
e of
    Apply Arg t
t      -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Arg t -> Reader r (Collect r)
forall r. ComputeFree r => Arg t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Arg t
t
    Proj{}       -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (t, t, t) -> Reader r (Collect r)
forall r. ComputeFree r => (t, t, t) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Sort, t) -> Reader r (Collect r)
forall r. ComputeFree r => (Sort, t) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars (Sort
s, t
t)
      IgnoreSorts
_         -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret ->
    case forall r. ComputeFree r => IgnoreSorts
ignoreSorts' @r of
      IgnoreSorts
IgnoreAll -> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Level -> Reader r (Collect r)
forall r. ComputeFree r => Level -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Level
a
        Inf Univ
_ Integer
_        -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Reader r (Collect r)
forall a. Monoid a => a
mempty
        Sort
CofUniv        -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Term -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => (Sort, Abs Sort) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars (Sort
s1, Abs Sort
s2))
        FunSort Sort
s1 Sort
s2  -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Sort -> Reader r (Collect r)
forall r. ComputeFree r => Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Sort
s2
        UnivSort Sort
s     -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Sort -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Sort
s
        MetaS MetaId
x Elims
es     -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Elims
es
        DefS QName
_ Elims
es      -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => Elims -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Elims
es
        DummyS{}       -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case Maybe t
mt of
    Maybe t
Nothing -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret Reader r (Collect r)
forall a. Monoid a => a
mempty
    Just t
t  -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case [t]
ts of
    []   -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret Reader r (Collect r)
forall a. Monoid a => a
mempty
    t
t:[t]
ts -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 r. ComputeFree r => [t] -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case List1 t
ts of
    t
t :| [t]
ts -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 r. ComputeFree r => [t] -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case (a, b)
ab of (a
a, b
b) -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case (a, b, c)
abc of (a
a, b
b, c
c) -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => c -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => c -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => d -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ a -> Reader r (Collect r)
forall r. ComputeFree r => a -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => b -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => c -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => d -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 r. ComputeFree r => e -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case Level
l of Max Integer
_ [PlusLevel' Term]
as -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ [PlusLevel' Term] -> Reader r (Collect r)
forall r.
ComputeFree r =>
[PlusLevel' Term] -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case PlusLevel' t
pl of Plus Integer
_ t
l -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret ->
    Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Maybe Term, t) -> Reader r (Collect r)
forall r. ComputeFree r => (Maybe Term, t) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case Abs t
t of
    Abs   ArgName
_ t
b -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars t
b
    NoAbs ArgName
_ t
b -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ t -> Reader r (Collect r)
forall r. ComputeFree r => t -> Reader r (Collect r)
forall t r. (Free t, 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 LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case Tele t
tel of
    Tele t
EmptyTel        -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (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 LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (t, Abs (Tele t)) -> Reader r (Collect r)
forall r.
ComputeFree r =>
(t, Abs (Tele t)) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars (t
t, Abs (Tele t)
tel)

instance Free Teletype where
  freeVars :: forall r. ComputeFree r => Teletype -> Reader r (Collect r)
freeVars Teletype
tel = ((Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case Teletype
tel of
    EmptyTt  Type
t     -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Type -> Reader r (Collect r)
forall r. ComputeFree r => Type -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Type
t
    ExtendTt Dom Type
t Abs Teletype
tel -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Teletype) -> Reader r (Collect r)
forall r.
ComputeFree r =>
(Dom Type, Abs Teletype) -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars (Dom Type
t, Abs Teletype
tel)

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

{-# 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 = ASetter r r (FlexRig' a) (FlexRig' a)
-> (FlexRig' a -> FlexRig' a) -> r -> r
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter r r (FlexRig' a) (FlexRig' a)
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 -> ASetter r r (FlexRig' a) (FlexRig' a)
-> (FlexRig' a -> FlexRig' a) -> r -> r
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter r r (FlexRig' a) (FlexRig' a)
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)