{-# LANGUAGE CPP #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wno-redundant-bang-patterns #-}

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

-- | Free variable check that reduces the subject to make certain variables not
--   free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs.
module Agda.TypeChecking.Free.Reduce
  ( ForceNotFree
  , forceNotFree
  , forceNoAbs
  , forceNoAbsSort
  , reallyFree
  , IsFree(..)
  , nonFreeVars
  ) where

import Prelude hiding (null)

import Data.Maybe
import qualified Data.IntMap.Strict as IntMap
import Data.IntMap.Strict (IntMap)
import GHC.Exts

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Base (constructorFlexRig, addFlexRig, oneFlexRig)
import Agda.TypeChecking.Free.Precompute

import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.VarSet (VarSet)
import Agda.Utils.StrictState
import Agda.Utils.StrictReader
import Agda.Utils.ExpandCase
import Agda.Utils.Singleton
import Agda.Utils.Impossible


-- | A variable can either not occur (`NotFree`) or it does occur
--   (`MaybeFree`).  In the latter case, the occurrence may disappear
--   depending on the instantiation of some set of metas.
data IsFree
  = MaybeFree FlexRig
  | NotFree
  deriving (IsFree -> IsFree -> Bool
(IsFree -> IsFree -> Bool)
-> (IsFree -> IsFree -> Bool) -> Eq IsFree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IsFree -> IsFree -> Bool
== :: IsFree -> IsFree -> Bool
$c/= :: IsFree -> IsFree -> Bool
/= :: IsFree -> IsFree -> Bool
Eq, Int -> IsFree -> ShowS
[IsFree] -> ShowS
IsFree -> String
(Int -> IsFree -> ShowS)
-> (IsFree -> String) -> ([IsFree] -> ShowS) -> Show IsFree
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IsFree -> ShowS
showsPrec :: Int -> IsFree -> ShowS
$cshow :: IsFree -> String
show :: IsFree -> String
$cshowList :: [IsFree] -> ShowS
showList :: [IsFree] -> ShowS
Show)

-- local scope size, VarSet to enforce not occurring, FlexRig we're under, ReduceEnv
-- András, 2026-02-12: the ReduceEnv is put in the FREnv because I don't want to bother
-- fixing GHC code generation (i.e. not returning closures from case splits) for ReduceM.
data FREnv = FREnv Int VarSet FlexRig ReduceEnv

-- This is equivalent to IntMap IsFree, where the NotFree cases are factored out into
-- a VarSet for efficiency.
data FRState = FRState VarSet (IntMap FlexRig)
type FreeRed = StateT FRState (Reader FREnv)

{-# SPECIALIZE forceNotFree :: VarSet -> Term -> ReduceM (IntMap IsFree, Term) #-}
-- | Try to enforce a set of variables not occurring in a given
--   type. Returns a possibly reduced version of the type and for each
--   of the given variables whether it is either not free, or
--   maybe free depending on some metavariables.
forceNotFree :: (ForceNotFree a, Reduce a) => VarSet -> a -> ReduceM (IntMap IsFree, a)
forceNotFree :: forall a.
(ForceNotFree a, Reduce a) =>
VarSet -> a -> ReduceM (IntMap IsFree, a)
forceNotFree VarSet
xs a
a = (ReduceEnv -> (IntMap IsFree, a)) -> ReduceM (IntMap IsFree, a)
forall a. (ReduceEnv -> a) -> ReduceM a
ReduceM \ReduceEnv
env ->
  let (a
a', FRState VarSet
notfree IntMap FlexRig
mxs) =
        Reader FREnv (a, FRState) -> FREnv -> (a, FRState)
forall r a. Reader r a -> r -> a
runReader (StateT FRState (Reader FREnv) a
-> FRState -> Reader FREnv (a, FRState)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m (a, s)
runStateT (a -> StateT FRState (Reader FREnv) a
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR (a -> StateT FRState (Reader FREnv) a)
-> a -> StateT FRState (Reader FREnv) a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ a
a) (VarSet -> IntMap FlexRig -> FRState
FRState VarSet
xs IntMap FlexRig
forall a. Monoid a => a
mempty))
                  (Int -> VarSet -> FlexRig -> ReduceEnv -> FREnv
FREnv Int
0 VarSet
xs FlexRig
forall a. FlexRig' a
oneFlexRig ReduceEnv
env) in
  let mxs' :: IntMap IsFree
mxs' = (Int -> IntMap IsFree -> IntMap IsFree)
-> IntMap IsFree -> VarSet -> IntMap IsFree
forall a. (Int -> a -> a) -> a -> VarSet -> a
VarSet.foldl' (\Int
k -> Int -> IsFree -> IntMap IsFree -> IntMap IsFree
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
k IsFree
NotFree) (FlexRig -> IsFree
MaybeFree (FlexRig -> IsFree) -> IntMap FlexRig -> IntMap IsFree
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap FlexRig
mxs) VarSet
notfree in
  (IntMap IsFree
mxs', a
a')

{-# SPECIALIZE reallyFree :: VarSet -> Term -> ReduceM (Either Blocked_ (Maybe Term)) #-}
-- | Checks if the given term contains any free variables that are in
--   the given set of variables, possibly reducing the term in the
--   process.  Returns `Right Nothing` if there are such variables,
--   `Right (Just v')` if there are none (where v' is the possibly
--   reduced version of the given term) or `Left b` if the problem is
--   blocked on a meta.
reallyFree :: (Reduce a, ForceNotFree a) => VarSet -> a -> ReduceM (Either Blocked_ (Maybe a))
reallyFree :: forall a.
(Reduce a, ForceNotFree a) =>
VarSet -> a -> ReduceM (Either Blocked_ (Maybe a))
reallyFree VarSet
xs a
v = do
  (mxs , v') <- VarSet -> a -> ReduceM (IntMap IsFree, a)
forall a.
(ForceNotFree a, Reduce a) =>
VarSet -> a -> ReduceM (IntMap IsFree, a)
forceNotFree VarSet
xs a
v
  case IntMap.foldr pickFree NotFree mxs of
    MaybeFree (Flexible MetaSet
ms) -> do
      let !blocker :: Blocker
blocker = MetaSet -> Blocker
metaSetToBlocker MetaSet
ms
      Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Either Blocked_ (Maybe a)
forall a b. a -> Either a b
Left (Blocked_ -> Either Blocked_ (Maybe a))
-> Blocked_ -> Either Blocked_ (Maybe a)
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
blocker ()
    MaybeFree FlexRig
_ -> Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocked_ (Maybe a)
forall a b. b -> Either a b
Right Maybe a
forall a. Maybe a
Nothing
    IsFree
NotFree     -> Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a))
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a)))
-> Either Blocked_ (Maybe a) -> ReduceM (Either Blocked_ (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Either Blocked_ (Maybe a)
forall a b. b -> Either a b
Right (a -> Maybe a
forall a. a -> Maybe a
Just a
v')
  where
    -- Check if any of the variables occur freely.
    pickFree :: IsFree -> IsFree -> IsFree
    pickFree :: IsFree -> IsFree -> IsFree
pickFree (MaybeFree FlexRig
ms1) (MaybeFree FlexRig
ms2) = FlexRig -> IsFree
MaybeFree (FlexRig -> IsFree) -> FlexRig -> IsFree
forall a b. (a -> b) -> a -> b
$! (FlexRig
ms1 FlexRig -> FlexRig -> FlexRig
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
`addFlexRig` FlexRig
ms2)
    pickFree IsFree
f1 IsFree
NotFree = IsFree
f1
    pickFree IsFree
NotFree IsFree
f2 = IsFree
f2

-- | Try to force a binder to be a NoAbs by reducing the body as needed
--   to get rid of the bound variable. Returns either the reduced abstraction
--   and the occurrence of the variable (if removing it failed) or else
--   the strengthened body.
forceNoAbs :: (Reduce a, ForceNotFree a)
           => Dom Type -> Abs a -> ReduceM (Either (Abs a, FlexRig) a)
forceNoAbs :: forall a.
(Reduce a, ForceNotFree a) =>
Dom Type -> Abs a -> ReduceM (Either (Abs a, FlexRig) a)
forceNoAbs Dom Type
dom (NoAbs String
_ a
x) = Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a)
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a))
-> Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a)
forall a b. (a -> b) -> a -> b
$ a -> Either (Abs a, FlexRig) a
forall a b. b -> Either a b
Right a
x
forceNoAbs Dom Type
dom (Abs String
n a
x)   = Dom Type
-> Abs a
-> (a -> ReduceM (Either (Abs a, FlexRig) a))
-> ReduceM (Either (Abs a, FlexRig) a)
forall a b. Dom Type -> Abs a -> (a -> ReduceM b) -> ReduceM b
underAbsReduceM Dom Type
dom (String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
n a
x) \a
x -> do
  (fvm, x) <- VarSet -> a -> ReduceM (IntMap IsFree, a)
forall a.
(ForceNotFree a, Reduce a) =>
VarSet -> a -> ReduceM (IntMap IsFree, a)
forceNotFree (Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
0) a
x
  case fromMaybe __IMPOSSIBLE__ (IntMap.lookup 0 fvm) of
    IsFree
NotFree           -> Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a)
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a))
-> Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a)
forall a b. (a -> b) -> a -> b
$! a -> Either (Abs a, FlexRig) a
forall a b. b -> Either a b
Right (a -> Either (Abs a, FlexRig) a) -> a -> Either (Abs a, FlexRig) a
forall a b. (a -> b) -> a -> b
$! Impossible -> Abs a -> a
forall a. Subst a => Impossible -> Abs a -> a
noabsApp Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
n a
x)
    MaybeFree FlexRig
flexRig -> Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a)
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a))
-> Either (Abs a, FlexRig) a -> ReduceM (Either (Abs a, FlexRig) a)
forall a b. (a -> b) -> a -> b
$ (Abs a, FlexRig) -> Either (Abs a, FlexRig) a
forall a b. a -> Either a b
Left (String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
n a
x , FlexRig
flexRig)

-- | András 2026-02-24: we specialize this, because TypeChecking.Reduce imports it via the hs-boot
--   file, and if it's not specialized there, it is __impossible__ to specialzie by GHC.
forceNoAbsSort :: Dom Type -> Abs Sort -> ReduceM (Either (Abs Sort, FlexRig) Sort)
forceNoAbsSort :: Dom Type -> Abs Sort -> ReduceM (Either (Abs Sort, FlexRig) Sort)
forceNoAbsSort = Dom Type -> Abs Sort -> ReduceM (Either (Abs Sort, FlexRig) Sort)
forall a.
(Reduce a, ForceNotFree a) =>
Dom Type -> Abs a -> ReduceM (Either (Abs a, FlexRig) a)
forceNoAbs

-- | Get the set of 'NotFree' variables from a variable map.
nonFreeVars :: IntMap IsFree -> VarSet
nonFreeVars :: IntMap IsFree -> VarSet
nonFreeVars =
  (VarSet -> Int -> IsFree -> VarSet)
-> VarSet -> IntMap IsFree -> VarSet
forall a b. (a -> Int -> b -> a) -> a -> IntMap b -> a
IntMap.foldlWithKey'
    (\VarSet
acc Int
k IsFree
v -> case IsFree
v of
        IsFree
NotFree -> Int -> VarSet -> VarSet
VarSet.insert Int
k VarSet
acc
        IsFree
_       -> VarSet
acc)
    VarSet
forall a. Monoid a => a
mempty


class (PrecomputeFreeVars a, Subst a) => ForceNotFree a where
  -- Reduce the argument if necessary, to make as many as possible of
  -- the variables in the state not free. Updates the state, marking
  -- the variables that couldn't be make not free as `MaybeFree`. By
  -- updating the state as soon as a variable can not be reduced away,
  -- we avoid trying to get rid of it in other places.
  forceNotFree' :: a -> FreeRed a

{-# NOINLINE notFreeInPrecomputedSlow #-}
notFreeInPrecomputedSlow :: Int# -> VarSet -> VarSet -> Bool
notFreeInPrecomputedSlow :: Int# -> VarSet -> VarSet -> Bool
notFreeInPrecomputedSlow Int#
locals VarSet
xs VarSet
precomp =
  VarSet -> VarSet -> Bool
VarSet.disjoint VarSet
xs (Int -> VarSet -> VarSet
VarSet.strengthen (Int# -> Int
I# Int#
locals) VarSet
precomp)

{-# INLINE noFreeInPrecomputed #-}
noFreeInPrecomputed :: Int -> VarSet -> VarSet -> Bool
noFreeInPrecomputed :: Int -> VarSet -> VarSet -> Bool
noFreeInPrecomputed (I# Int#
locals) VarSet
xs VarSet
precomp = case (VarSet
xs, VarSet
precomp) of
  -- fast path
  (VarSet.VS# Word#
xs, VarSet.VS# Word#
precomp) ->
    Int# -> Bool
isTrue# ((Word#
xs Word# -> Word# -> Word#
`and#` (Word#
precomp Word# -> Int# -> Word#
`shiftRL#` Int#
locals)) Word# -> Word# -> Int#
`eqWord#` Word#
0##)
  -- rare slow path
  (VarSet, VarSet)
_ -> Int# -> VarSet -> VarSet -> Bool
notFreeInPrecomputedSlow Int#
locals VarSet
xs VarSet
precomp

{-# INLINE reduceIfFreeVars #-}
-- Reduce the argument if there are offending free variables. Doesn't call the
-- continuation when no reduction is required.
reduceIfFreeVars :: (Reduce a, ForceNotFree a) => (a -> FreeRed a) -> a -> FreeRed a
reduceIfFreeVars :: forall a.
(Reduce a, ForceNotFree a) =>
(a -> FreeRed a) -> a -> FreeRed a
reduceIfFreeVars a -> FreeRed a
k = \a
a -> do
  FRState notfrees _ <- StateT FRState (Reader FREnv) FRState
forall s (m :: * -> *). MonadState s m => m s
get
  FREnv locals _ _ env <- ask
  let fvs = a -> VarSet
forall a. PrecomputeFreeVars a => a -> VarSet
precomputedFreeVars a
a
  if noFreeInPrecomputed locals notfrees fvs
    then pure a
    else k $ precomputeFreeVars_ (unReduceM (reduce a) env)

-- Careful not to define forceNotFree' = forceNotFreeR since that would loop.
forceNotFreeR :: (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR :: forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR = (a -> FreeRed a) -> a -> FreeRed a
forall a.
(Reduce a, ForceNotFree a) =>
(a -> FreeRed a) -> a -> FreeRed a
reduceIfFreeVars a -> FreeRed a
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree'

{-# INLINE underFlexRig #-}
underFlexRig :: FlexRig -> FreeRed a -> FreeRed a
underFlexRig :: forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
fr' = (FREnv -> FREnv)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) a
forall a.
(FREnv -> FREnv)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local \(FREnv Int
x VarSet
nfs FlexRig
fr ReduceEnv
e) -> Int -> VarSet -> FlexRig -> ReduceEnv -> FREnv
FREnv Int
x VarSet
nfs (FlexRig -> FlexRig -> FlexRig
forall a. Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
composeFlexRig FlexRig
fr' FlexRig
fr) ReduceEnv
e

{-# INLINE underConstructor #-}
underConstructor :: ConHead -> Elims -> FreeRed a -> FreeRed a
underConstructor :: forall a. ConHead -> Elims -> FreeRed a -> FreeRed a
underConstructor ConHead
c Elims
es = FlexRig -> FreeRed a -> FreeRed a
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig (ConHead -> Elims -> FlexRig
forall a. ConHead -> Elims -> FlexRig' a
constructorFlexRig ConHead
c Elims
es)

instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where
  -- Precomputed free variables are stored in the Arg so reduceIf outside the
  -- traverse.
  forceNotFree' :: Arg a -> FreeRed (Arg a)
forceNotFree' = (Arg a -> FreeRed (Arg a)) -> Arg a -> FreeRed (Arg a)
forall a.
(Reduce a, ForceNotFree a) =>
(a -> FreeRed a) -> a -> FreeRed a
reduceIfFreeVars ((a -> StateT FRState (Reader FREnv) a) -> Arg a -> FreeRed (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse a -> StateT FRState (Reader FREnv) a
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree')

instance (Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) where
  forceNotFree' :: Dom a -> FreeRed (Dom a)
forceNotFree' = (a -> StateT FRState (Reader FREnv) a) -> Dom a -> FreeRed (Dom a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term b)
traverse a -> StateT FRState (Reader FREnv) a
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR

instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where
  -- Reduction stops at abstractions (lambda/pi) so do reduceIf/forceNotFreeR here.
  forceNotFree' :: Abs a -> FreeRed (Abs a)
forceNotFree' Abs a
abs = ((FreeRed (Abs a) -> Result (FreeRed (Abs a)))
 -> Result (FreeRed (Abs a)))
-> FreeRed (Abs a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \FreeRed (Abs a) -> Result (FreeRed (Abs a))
ret -> case Abs a
abs of
    a :: Abs a
a@NoAbs{}   -> FreeRed (Abs a) -> Result (FreeRed (Abs a))
ret (FreeRed (Abs a) -> Result (FreeRed (Abs a)))
-> FreeRed (Abs a) -> Result (FreeRed (Abs a))
forall a b. (a -> b) -> a -> b
$ (a -> StateT FRState (Reader FREnv) a) -> Abs a -> FreeRed (Abs a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
traverse a -> StateT FRState (Reader FREnv) a
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR Abs a
a
    a :: Abs a
a@(Abs String
x a
_) -> FreeRed (Abs a) -> Result (FreeRed (Abs a))
ret do
      let updEnv :: ReduceEnv -> ReduceEnv
          updEnv :: ReduceEnv -> ReduceEnv
updEnv ReduceEnv
e = String -> Dom Type -> ReduceEnv -> ReduceEnv
extendReduceEnv String
x Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__ ReduceEnv
e
      (Abs a -> FreeRed (Abs a)) -> Abs a -> FreeRed (Abs a)
forall a.
(Reduce a, ForceNotFree a) =>
(a -> FreeRed a) -> a -> FreeRed a
reduceIfFreeVars
        ((FREnv -> FREnv) -> FreeRed (Abs a) -> FreeRed (Abs a)
forall a.
(FREnv -> FREnv)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\(FREnv Int
x VarSet
nfs FlexRig
fr ReduceEnv
e) -> Int -> VarSet -> FlexRig -> ReduceEnv -> FREnv
FREnv (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) VarSet
nfs FlexRig
fr (ReduceEnv -> ReduceEnv
updEnv ReduceEnv
e)) (FreeRed (Abs a) -> FreeRed (Abs a))
-> (Abs a -> FreeRed (Abs a)) -> Abs a -> FreeRed (Abs a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> StateT FRState (Reader FREnv) a) -> Abs a -> FreeRed (Abs a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Abs a -> f (Abs b)
traverse a -> StateT FRState (Reader FREnv) a
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree')
        Abs a
a

instance ForceNotFree a => ForceNotFree [a] where
  forceNotFree' :: [a] -> FreeRed [a]
forceNotFree' [a]
as = ((FreeRed [a] -> Result (FreeRed [a])) -> Result (FreeRed [a]))
-> FreeRed [a]
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \FreeRed [a] -> Result (FreeRed [a])
ret -> case [a]
as of
    []     -> FreeRed [a] -> Result (FreeRed [a])
ret (FreeRed [a] -> Result (FreeRed [a]))
-> FreeRed [a] -> Result (FreeRed [a])
forall a b. (a -> b) -> a -> b
$ [a] -> FreeRed [a]
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    (a
a:[a]
as) -> FreeRed [a] -> Result (FreeRed [a])
ret (FreeRed [a] -> Result (FreeRed [a]))
-> FreeRed [a] -> Result (FreeRed [a])
forall a b. (a -> b) -> a -> b
$ (:) (a -> [a] -> [a])
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT FRState (Reader FREnv) a
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' a
a StateT FRState (Reader FREnv) ([a] -> [a])
-> FreeRed [a] -> FreeRed [a]
forall a b.
StateT FRState (Reader FREnv) (a -> b)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> FreeRed [a]
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' [a]
as

instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where
  -- There's an Arg inside Elim' which stores precomputed free vars, so let's
  -- not skip over that.
  forceNotFree' :: Elim' a -> FreeRed (Elim' a)
forceNotFree' Elim' a
e = ((FreeRed (Elim' a) -> Result (FreeRed (Elim' a)))
 -> Result (FreeRed (Elim' a)))
-> FreeRed (Elim' a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
ret -> case Elim' a
e of
    Apply Arg a
arg    -> FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
ret (FreeRed (Elim' a) -> Result (FreeRed (Elim' a)))
-> FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
forall a b. (a -> b) -> a -> b
$ Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a)
-> StateT FRState (Reader FREnv) (Arg a) -> FreeRed (Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg a -> StateT FRState (Reader FREnv) (Arg a)
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Arg a
arg
    e :: Elim' a
e@Proj{}     -> FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
ret (FreeRed (Elim' a) -> Result (FreeRed (Elim' a)))
-> FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
forall a b. (a -> b) -> a -> b
$ Elim' a -> FreeRed (Elim' a)
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elim' a
e
    IApply a
x a
y a
r -> FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
ret (FreeRed (Elim' a) -> Result (FreeRed (Elim' a)))
-> FreeRed (Elim' a) -> Result (FreeRed (Elim' a))
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply (a -> a -> a -> Elim' a)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) (a -> a -> Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT FRState (Reader FREnv) a
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR a
x StateT FRState (Reader FREnv) (a -> a -> Elim' a)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) (a -> Elim' a)
forall a b.
StateT FRState (Reader FREnv) (a -> b)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> StateT FRState (Reader FREnv) a
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR a
y StateT FRState (Reader FREnv) (a -> Elim' a)
-> StateT FRState (Reader FREnv) a -> FreeRed (Elim' a)
forall a b.
StateT FRState (Reader FREnv) (a -> b)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> StateT FRState (Reader FREnv) a
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR a
r

instance ForceNotFree Type where
  forceNotFree' :: Type -> FreeRed Type
forceNotFree' Type
a = ((FreeRed Type -> Result (FreeRed Type)) -> Result (FreeRed Type))
-> FreeRed Type
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \FreeRed Type -> Result (FreeRed Type)
ret -> case Type
a of
    El Sort
s Term
t -> FreeRed Type -> Result (FreeRed Type)
ret (FreeRed Type -> Result (FreeRed Type))
-> FreeRed Type -> Result (FreeRed Type)
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type)
-> StateT FRState (Reader FREnv) Sort
-> StateT FRState (Reader FREnv) (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> StateT FRState (Reader FREnv) Sort
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Sort
s StateT FRState (Reader FREnv) (Term -> Type)
-> StateT FRState (Reader FREnv) Term -> FreeRed Type
forall a b.
StateT FRState (Reader FREnv) (a -> b)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> StateT FRState (Reader FREnv) Term
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Term
t

instance ForceNotFree Term where
  forceNotFree' :: Term -> StateT FRState (Reader FREnv) Term
forceNotFree' Term
t = ((StateT FRState (Reader FREnv) Term
  -> Result (StateT FRState (Reader FREnv) Term))
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret -> case Term
t of
    Var Int
x Elims
es -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret do
      FREnv locals wantToNotFree fr _ <- StateT FRState (Reader FREnv) FREnv
forall r (m :: * -> *). MonadReader r m => m r
ask
      FRState xs frs <- get
      let x' = Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
locals
      expand \StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret -> if (Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
locals Bool -> Bool -> Bool
&& Int -> VarSet -> Bool
VarSet.member Int
x' VarSet
wantToNotFree) then StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret do
        FRState -> StateT FRState (Reader FREnv) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (FRState -> StateT FRState (Reader FREnv) ())
-> FRState -> StateT FRState (Reader FREnv) ()
forall a b. (a -> b) -> a -> b
$! VarSet -> IntMap FlexRig -> FRState
FRState (Int -> VarSet -> VarSet
VarSet.delete Int
x' VarSet
xs) (Int -> FlexRig -> IntMap FlexRig -> IntMap FlexRig
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x' FlexRig
fr IntMap FlexRig
frs)
        Int -> Elims -> Term
Var Int
x (Elims -> Term)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
      else StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret do
        Int -> Elims -> Term
Var Int
x (Elims -> Term)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
    Def QName
f Elims
es   -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f    (Elims -> Term)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
    Con ConHead
c ConInfo
h Elims
es -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
h  (Elims -> Term)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConHead
-> Elims
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. ConHead -> Elims -> FreeRed a -> FreeRed a
underConstructor ConHead
c Elims
es (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
    MetaV MetaId
m Elims
es -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m  (Elims -> Term)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig (MetaSet -> FlexRig
forall a. a -> FlexRig' a
Flexible (MetaId -> MetaSet
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m)) (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
    Lam ArgInfo
h Abs Term
b    -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
h    (Abs Term -> Term)
-> StateT FRState (Reader FREnv) (Abs Term)
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) (Abs Term)
-> StateT FRState (Reader FREnv) (Abs Term)
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Abs Term -> StateT FRState (Reader FREnv) (Abs Term)
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Abs Term
b)
    Pi Dom Type
a Abs Type
b     -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi       (Dom Type -> Abs Type -> Term)
-> StateT FRState (Reader FREnv) (Dom Type)
-> StateT FRState (Reader FREnv) (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> StateT FRState (Reader FREnv) (Dom Type)
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Dom Type
a StateT FRState (Reader FREnv) (Abs Type -> Term)
-> StateT FRState (Reader FREnv) (Abs Type)
-> StateT FRState (Reader FREnv) Term
forall a b.
StateT FRState (Reader FREnv) (a -> b)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs Type -> StateT FRState (Reader FREnv) (Abs Type)
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Abs Type
b  -- Dom and Abs do reduceIf so not needed here
    Sort Sort
s     -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort     (Sort -> Term)
-> StateT FRState (Reader FREnv) Sort
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> StateT FRState (Reader FREnv) Sort
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Sort
s
    Level Level
l    -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ Level -> Term
Level    (Level -> Term)
-> StateT FRState (Reader FREnv) Level
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> StateT FRState (Reader FREnv) Level
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Level
l
    DontCare Term
t -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ Term -> Term
DontCare (Term -> Term)
-> StateT FRState (Reader FREnv) Term
-> StateT FRState (Reader FREnv) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> StateT FRState (Reader FREnv) Term
forall a. (Reduce a, ForceNotFree a) => a -> FreeRed a
forceNotFreeR Term
t  -- Reduction stops at DontCare so reduceIf
    t :: Term
t@Lit{}    -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ Term -> StateT FRState (Reader FREnv) Term
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
t
    t :: Term
t@Dummy{}  -> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
ret (StateT FRState (Reader FREnv) Term
 -> Result (StateT FRState (Reader FREnv) Term))
-> StateT FRState (Reader FREnv) Term
-> Result (StateT FRState (Reader FREnv) Term)
forall a b. (a -> b) -> a -> b
$ Term -> StateT FRState (Reader FREnv) Term
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
t

instance ForceNotFree Level where
  {-# INLINE forceNotFree' #-}
  forceNotFree' :: Level -> StateT FRState (Reader FREnv) Level
forceNotFree' (Max Integer
m [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m ([PlusLevel' Term] -> Level)
-> StateT FRState (Reader FREnv) [PlusLevel' Term]
-> StateT FRState (Reader FREnv) Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term]
-> StateT FRState (Reader FREnv) [PlusLevel' Term]
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' [PlusLevel' Term]
as

instance ForceNotFree PlusLevel where
  {-# INLINE forceNotFree' #-}
  forceNotFree' :: PlusLevel' Term -> FreeRed (PlusLevel' Term)
forceNotFree' (Plus Integer
k Term
a) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
k (Term -> PlusLevel' Term)
-> StateT FRState (Reader FREnv) Term -> FreeRed (PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> StateT FRState (Reader FREnv) Term
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Term
a

instance ForceNotFree Sort where
  -- Reduce for sorts already goes under all sort constructors, so we can get
  -- away without forceNotFreeR here.
  forceNotFree' :: Sort -> StateT FRState (Reader FREnv) Sort
forceNotFree' Sort
s = ((StateT FRState (Reader FREnv) Sort
  -> Result (StateT FRState (Reader FREnv) Sort))
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret -> case Sort
s of
    Univ Univ
u Level
l       -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level -> Sort)
-> StateT FRState (Reader FREnv) Level
-> StateT FRState (Reader FREnv) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> StateT FRState (Reader FREnv) Level
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Level
l
    PiSort Dom' Term Term
a Sort
b Abs Sort
c   -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret do a        <- FlexRig -> FreeRed (Dom' Term Term) -> FreeRed (Dom' Term Term)
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig (MetaSet -> FlexRig
forall a. a -> FlexRig' a
Flexible MetaSet
forall a. Monoid a => a
mempty) (Dom' Term Term -> FreeRed (Dom' Term Term)
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Dom' Term Term
a)
                             (!b, !c) <- underFlexRig WeaklyRigid ((,) <$> forceNotFree' b <*> forceNotFree' c)
                             pure $ PiSort a b c
    FunSort Sort
a Sort
b    -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort)
-> StateT FRState (Reader FREnv) Sort
-> StateT FRState (Reader FREnv) (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> StateT FRState (Reader FREnv) Sort
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Sort
a StateT FRState (Reader FREnv) (Sort -> Sort)
-> StateT FRState (Reader FREnv) Sort
-> StateT FRState (Reader FREnv) Sort
forall a b.
StateT FRState (Reader FREnv) (a -> b)
-> StateT FRState (Reader FREnv) a
-> StateT FRState (Reader FREnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> StateT FRState (Reader FREnv) Sort
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Sort
b
    UnivSort Sort
s     -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort)
-> StateT FRState (Reader FREnv) Sort
-> StateT FRState (Reader FREnv) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Sort
-> StateT FRState (Reader FREnv) Sort
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Sort -> StateT FRState (Reader FREnv) Sort
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Sort
s)
    MetaS MetaId
x Elims
es     -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig (MetaSet -> FlexRig
forall a. a -> FlexRig' a
Flexible (MetaId -> MetaSet
forall el coll. Singleton el coll => el -> coll
singleton MetaId
x)) (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
    DefS QName
d Elims
es      -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d (Elims -> Sort)
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FlexRig
-> StateT FRState (Reader FREnv) Elims
-> StateT FRState (Reader FREnv) Elims
forall a. FlexRig -> FreeRed a -> FreeRed a
underFlexRig FlexRig
forall a. FlexRig' a
WeaklyRigid (Elims -> StateT FRState (Reader FREnv) Elims
forall a. ForceNotFree a => a -> FreeRed a
forceNotFree' Elims
es)
    s :: Sort
s@(Inf Univ
_ Integer
_)    -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> StateT FRState (Reader FREnv) Sort
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
SizeUniv     -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> StateT FRState (Reader FREnv) Sort
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
LockUniv     -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> StateT FRState (Reader FREnv) Sort
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
LevelUniv    -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> StateT FRState (Reader FREnv) Sort
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
IntervalUniv -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> StateT FRState (Reader FREnv) Sort
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@DummyS{}     -> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
ret (StateT FRState (Reader FREnv) Sort
 -> Result (StateT FRState (Reader FREnv) Sort))
-> StateT FRState (Reader FREnv) Sort
-> Result (StateT FRState (Reader FREnv) Sort)
forall a b. (a -> b) -> a -> b
$ Sort -> StateT FRState (Reader FREnv) Sort
forall a. a -> StateT FRState (Reader FREnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s