module Agda.Auto.Syntax where

import Data.IORef
import qualified Data.Set as Set

import Agda.Syntax.Common (Hiding)
import Agda.Auto.NarrowingSearch

import Agda.Utils.Impossible

-- | Unique identifiers for variable occurrences in unification.
type UId o = Metavar (Exp o) (RefInfo o)

data HintMode = HMNormal
              | HMRecCall

data EqReasoningConsts o = EqReasoningConsts
  { forall o. EqReasoningConsts o -> ConstRef o
eqrcId    -- "_≡_"
  , forall o. EqReasoningConsts o -> ConstRef o
eqrcBegin -- "begin_"
  , forall o. EqReasoningConsts o -> ConstRef o
eqrcStep  -- "_≡⟨_⟩_"
  , forall o. EqReasoningConsts o -> ConstRef o
eqrcEnd   -- "_∎"
  , forall o. EqReasoningConsts o -> ConstRef o
eqrcSym   -- "sym"
  , forall o. EqReasoningConsts o -> ConstRef o
eqrcCong  -- "cong"
  :: ConstRef o
  }

data EqReasoningState = EqRSNone | EqRSChain | EqRSPrf1 | EqRSPrf2 | EqRSPrf3
 deriving (EqReasoningState -> EqReasoningState -> Bool
(EqReasoningState -> EqReasoningState -> Bool)
-> (EqReasoningState -> EqReasoningState -> Bool)
-> Eq EqReasoningState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EqReasoningState -> EqReasoningState -> Bool
== :: EqReasoningState -> EqReasoningState -> Bool
$c/= :: EqReasoningState -> EqReasoningState -> Bool
/= :: EqReasoningState -> EqReasoningState -> Bool
Eq, Int -> EqReasoningState -> ShowS
[EqReasoningState] -> ShowS
EqReasoningState -> String
(Int -> EqReasoningState -> ShowS)
-> (EqReasoningState -> String)
-> ([EqReasoningState] -> ShowS)
-> Show EqReasoningState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EqReasoningState -> ShowS
showsPrec :: Int -> EqReasoningState -> ShowS
$cshow :: EqReasoningState -> String
show :: EqReasoningState -> String
$cshowList :: [EqReasoningState] -> ShowS
showList :: [EqReasoningState] -> ShowS
Show)

-- | The concrete instance of the 'blk' parameter in 'Metavar'.
--   I.e., the information passed to the search control.

data RefInfo o
  = RIEnv
    { forall o. RefInfo o -> [(ConstRef o, HintMode)]
rieHints :: [(ConstRef o, HintMode)]
    , forall o. RefInfo o -> Int
rieDefFreeVars :: Nat
      -- ^ Nat - deffreevars
      --   (to make cost of using module parameters correspond to that of hints).
    , forall o. RefInfo o -> Maybe (EqReasoningConsts o)
rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
    }
  | RIMainInfo
    { forall o. RefInfo o -> Int
riMainCxtLength :: Nat
      -- ^ Size of typing context in which meta was created.
    , forall o. RefInfo o -> HNExp o
riMainType      :: HNExp o
      -- ^ Head normal form of type of meta.
    , forall o. RefInfo o -> Bool
riMainIota      :: Bool
       -- ^ True if iota steps performed when normalising target type
       --   (used to put cost when traversing a definition
       --    by construction instantiation).
    }
  | RIUnifInfo [CAction o] (HNExp o)
    -- meta environment, opp hne
  | RICopyInfo (ICExp o)
  | RIIotaStep Bool -- True - semiflex
  | RIInferredTypeUnknown
  | RINotConstructor
  | RIUsedVars [UId o] [Elr o]
  | RIPickSubsvar

  | RIEqRState EqReasoningState


  | RICheckElim Bool -- isdep
  | RICheckProjIndex [ConstRef o] -- noof proj functions


type MyPB o = PB (RefInfo o)
type MyMB a o = MB a (RefInfo o)

type Nat = Int

data MId = Id String
         | NoId

-- | Abstraction with maybe a name.
--
--   Different from Agda, where there is also info
--   whether function is constant.
data Abs a = Abs MId a

-- | Constant signatures.

data ConstDef o = ConstDef
  { forall o. ConstDef o -> String
cdname        :: String
    -- ^ For debug printing.
  , forall o. ConstDef o -> o
cdorigin      :: o
    -- ^ Reference to the Agda constant.
  , forall o. ConstDef o -> MExp o
cdtype        :: MExp o
    -- ^ Type of constant.
  , forall o. ConstDef o -> DeclCont o
cdcont        :: DeclCont o
    -- ^ Constant definition.
  , forall o. ConstDef o -> Int
cddeffreevars :: Nat
    -- ^ Free vars of the module where the constant is defined..
  } -- contains no metas

-- | Constant definitions.

data DeclCont o
  = Def Nat [Clause o] (Maybe Nat) -- maybe an index to elimand argument
                       (Maybe Nat) -- maybe index to elim arg if semiflex
  | Datatype [ConstRef o] -- constructors
             [ConstRef o] -- projection functions (in case it is a record)

  | Constructor Nat -- number of omitted args
  | Postulate

type Clause o = ([Pat o], MExp o)

data Pat o
  = PatConApp (ConstRef o) [Pat o]
  | PatVar String
  | PatExp
    -- ^ Dot pattern.
  | PatProj (ConstRef o)
    -- ^ Projection pattern.

type ConstRef o = IORef (ConstDef o)

-- | Head of application (elimination).
data Elr o
  = Var Nat
  | Const (ConstRef o)
  deriving (Elr o -> Elr o -> Bool
(Elr o -> Elr o -> Bool) -> (Elr o -> Elr o -> Bool) -> Eq (Elr o)
forall o. Elr o -> Elr o -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall o. Elr o -> Elr o -> Bool
== :: Elr o -> Elr o -> Bool
$c/= :: forall o. Elr o -> Elr o -> Bool
/= :: Elr o -> Elr o -> Bool
Eq)

getVar :: Elr o -> Maybe Nat
getVar :: forall o. Elr o -> Maybe Int
getVar (Var Int
n) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
getVar Const{} = Maybe Int
forall a. Maybe a
Nothing

getConst :: Elr o -> Maybe (ConstRef o)
getConst :: forall o. Elr o -> Maybe (ConstRef o)
getConst (Const ConstRef o
c) = ConstRef o -> Maybe (ConstRef o)
forall a. a -> Maybe a
Just ConstRef o
c
getConst Var{}     = Maybe (ConstRef o)
forall a. Maybe a
Nothing

data Sort
  = Set Nat
  | UnknownSort
  | Type

-- | Agsy's internal syntax.
data Exp o
  = App
    { forall o. Exp o -> Maybe (UId o)
appUId   :: Maybe (UId o)
      -- ^ Unique identifier of the head.
    , forall o. Exp o -> OKHandle (RefInfo o)
appOK    :: OKHandle (RefInfo o)
      -- ^ This application has been type-checked.
    , forall o. Exp o -> Elr o
appHead  :: Elr o
      -- ^ Head.
    , forall o. Exp o -> MArgList o
appElims :: MArgList o
      -- ^ Arguments.
    }
  | Lam Hiding (Abs (MExp o))
    -- ^ Lambda with hiding information.
  | Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))
    -- ^ @True@ if possibly dependent (var not known to not occur).
    --   @False@ if non-dependent.
  | Sort Sort
  | AbsurdLambda Hiding
    -- ^ Absurd lambda with hiding information.

dontCare :: Exp o
dontCare :: forall o. Exp o
dontCare = Sort -> Exp o
forall o. Sort -> Exp o
Sort Sort
UnknownSort

-- | "Maybe expression":  Expression or reference to meta variable.
type MExp o = MM (Exp o) (RefInfo o)

data ArgList o
  = ALNil
    -- ^ No more eliminations.
  | ALCons Hiding (MExp o) (MArgList o)
    -- ^ Application and tail.

  | ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)
    -- ^ proj pre args, projfcn idx, tail

  | ALConPar (MArgList o)
    -- ^ Constructor parameter (missing in Agda).
    --   Agsy has monomorphic constructors.
    --   Inserted to cover glitch of polymorphic constructor
    --   applications coming from Agda

type MArgList o = MM (ArgList o) (RefInfo o)

data WithSeenUIds a o = WithSeenUIds
  { forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds :: [Maybe (UId o)]
  , forall a o. WithSeenUIds a o -> a
rawValue :: a
  }

type HNExp o = WithSeenUIds (HNExp' o) o

data HNExp' o =
    HNApp  (Elr o) (ICArgList o)
  | HNLam  Hiding (Abs (ICExp o))
  | HNPi   Hiding Bool (ICExp o) (Abs (ICExp o))
  | HNSort Sort

-- | Head-normal form of 'ICArgList'.  First entry is exposed.
--
--   Q: Why are there no projection eliminations?
data HNArgList o = HNALNil
                 | HNALCons Hiding (ICExp o) (ICArgList o)
                 | HNALConPar (ICArgList o)

-- | Lazy concatenation of argument lists under explicit substitutions.
data ICArgList o = CALNil
                 | CALConcat (Clos (MArgList o) o) (ICArgList o)

-- | An expression @a@ in an explicit substitution @[CAction a]@.
type ICExp o  = Clos (MExp o) o
data Clos a o = Clos [CAction o] a

type CExp o   = TrBr (ICExp o) o
data TrBr a o = TrBr [MExp o] a

-- | Entry of an explicit substitution.
--
--   An explicit substitution is a list of @CAction@s.
--   This is isomorphic to the usual presentation where
--   @Skip@ and @Weak@ would be constructors of exp. substs.

data CAction o
  = Sub (ICExp o)
    -- ^ Instantation of variable.
  | Skip
    -- ^ For going under a binder, often called "Lift".
  | Weak Nat
    -- ^ Shifting substitution (going to a larger context).

type Ctx o = [(MId, CExp o)]

type EE = IO

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

detecteliminand :: [Clause o] -> Maybe Nat
detecteliminand :: forall o. [Clause o] -> Maybe Int
detecteliminand [Clause o]
cls =
 case (Clause o -> Maybe Int) -> [Clause o] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Clause o -> Maybe Int
forall {t} {o} {b}. Num t => ([Pat o], b) -> Maybe t
cleli [Clause o]
cls of
  [] -> Maybe Int
forall a. Maybe a
Nothing
  (Maybe Int
i:[Maybe Int]
is) -> if (Maybe Int -> Bool) -> [Maybe Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Int
i Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) [Maybe Int]
is then Maybe Int
i else Maybe Int
forall a. Maybe a
Nothing
 where
  cleli :: ([Pat o], b) -> Maybe t
cleli ([Pat o]
pats, b
_) = t -> [Pat o] -> Maybe t
forall {t} {o}. Num t => t -> [Pat o] -> Maybe t
pateli t
0 [Pat o]
pats
  pateli :: t -> [Pat o] -> Maybe t
pateli t
i (PatConApp ConstRef o
_ [Pat o]
args : [Pat o]
pats) = if (Pat o -> Bool) -> [Pat o] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Pat o -> Bool
forall {o}. Pat o -> Bool
notcon ([Pat o]
args [Pat o] -> [Pat o] -> [Pat o]
forall a. [a] -> [a] -> [a]
++ [Pat o]
pats) then t -> Maybe t
forall a. a -> Maybe a
Just t
i else Maybe t
forall a. Maybe a
Nothing
  pateli t
i (Pat o
_ : [Pat o]
pats) = t -> [Pat o] -> Maybe t
pateli (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [Pat o]
pats
  pateli t
i [] = Maybe t
forall a. Maybe a
Nothing
  notcon :: Pat o -> Bool
notcon PatConApp{} = Bool
False
  notcon Pat o
_ = Bool
True

detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
detectsemiflex :: forall o. ConstRef o -> [Clause o] -> IO Bool
detectsemiflex ConstRef o
_ [Clause o]
_ = Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- disabled

categorizedecl :: ConstRef o -> IO ()
categorizedecl :: forall o. ConstRef o -> IO ()
categorizedecl ConstRef o
c = do
 ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
 case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of
  Def Int
narg [Clause o]
cls Maybe Int
_ Maybe Int
_ -> do
   Bool
semif <- ConstRef o -> [Clause o] -> IO Bool
forall o. ConstRef o -> [Clause o] -> IO Bool
detectsemiflex ConstRef o
c [Clause o]
cls
   let elim :: Maybe Int
elim = [Clause o] -> Maybe Int
forall o. [Clause o] -> Maybe Int
detecteliminand [Clause o]
cls
       semifb :: Maybe Int
semifb = case (Bool
semif, Maybe Int
elim) of
                 (Bool
True, Just Int
i) -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i -- just copying val of elim arg. this should be changed
                 (Bool
_, Maybe Int
_) -> Maybe Int
forall a. Maybe a
Nothing
   ConstRef o -> ConstDef o -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef ConstRef o
c (ConstDef o
cd {cdcont :: DeclCont o
cdcont = Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
forall o. Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
Def Int
narg [Clause o]
cls Maybe Int
elim Maybe Int
semifb})
  DeclCont o
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

class MetaliseOKH t where
  metaliseOKH :: t -> IO t

instance MetaliseOKH t => MetaliseOKH (MM t a) where
  metaliseOKH :: MM t a -> IO (MM t a)
metaliseOKH = \case
    Meta Metavar t a
m -> MM t a -> IO (MM t a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MM t a -> IO (MM t a)) -> MM t a -> IO (MM t a)
forall a b. (a -> b) -> a -> b
$ Metavar t a -> MM t a
forall a blk. Metavar a blk -> MM a blk
Meta Metavar t a
m
    NotM t
e -> t -> MM t a
forall a blk. a -> MM a blk
NotM (t -> MM t a) -> IO t -> IO (MM t a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> IO t
forall t. MetaliseOKH t => t -> IO t
metaliseOKH t
e

instance MetaliseOKH t => MetaliseOKH (Abs t) where
  metaliseOKH :: Abs t -> IO (Abs t)
metaliseOKH (Abs MId
id t
b) = MId -> t -> Abs t
forall a. MId -> a -> Abs a
Abs MId
id (t -> Abs t) -> IO t -> IO (Abs t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> IO t
forall t. MetaliseOKH t => t -> IO t
metaliseOKH t
b

instance MetaliseOKH (Exp o) where
  metaliseOKH :: Exp o -> IO (Exp o)
metaliseOKH = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
okh Elr o
elr MArgList o
args ->
      (\ OKHandle (RefInfo o)
m -> Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
m Elr o
elr) (OKHandle (RefInfo o) -> MArgList o -> Exp o)
-> IO (OKHandle (RefInfo o)) -> IO (MArgList o -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Metavar OKVal (RefInfo o) -> OKHandle (RefInfo o)
forall a blk. Metavar a blk -> MM a blk
Meta (Metavar OKVal (RefInfo o) -> OKHandle (RefInfo o))
-> IO (Metavar OKVal (RefInfo o)) -> IO (OKHandle (RefInfo o))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Metavar OKVal (RefInfo o))
forall a blk. IO (Metavar a blk)
initMeta) IO (MArgList o -> Exp o) -> IO (MArgList o) -> IO (Exp o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MArgList o -> IO (MArgList o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MArgList o
args
    Lam Hiding
hid Abs (MExp o)
b -> Hiding -> Abs (MExp o) -> Exp o
forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (MExp o) -> IO (Abs (MExp o))
forall t. MetaliseOKH t => t -> IO t
metaliseOKH Abs (MExp o)
b
    Pi Maybe (UId o)
uid Hiding
hid Bool
dep MExp o
it Abs (MExp o)
ot ->
      Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
dep (MExp o -> Abs (MExp o) -> Exp o)
-> IO (MExp o) -> IO (Abs (MExp o) -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MExp o -> IO (MExp o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MExp o
it IO (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs (MExp o) -> IO (Abs (MExp o))
forall t. MetaliseOKH t => t -> IO t
metaliseOKH Abs (MExp o)
ot
    e :: Exp o
e@Sort{} -> Exp o -> IO (Exp o)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp o
e
    e :: Exp o
e@AbsurdLambda{} -> Exp o -> IO (Exp o)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp o
e

instance MetaliseOKH (ArgList o) where
  metaliseOKH :: ArgList o -> IO (ArgList o)
metaliseOKH = \case
    ArgList o
ALNil -> ArgList o -> IO (ArgList o)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgList o
forall o. ArgList o
ALNil
    ALCons Hiding
hid MExp o
a MArgList o
as -> Hiding -> MExp o -> MArgList o -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid (MExp o -> MArgList o -> ArgList o)
-> IO (MExp o) -> IO (MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MExp o -> IO (MExp o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MExp o
a IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MArgList o -> IO (MArgList o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MArgList o
as
    ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
idx Hiding
hid MArgList o
as ->
      (\ MArgList o
eas -> MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
forall o.
MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
idx Hiding
hid) (MArgList o -> MArgList o -> ArgList o)
-> IO (MArgList o) -> IO (MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MArgList o -> IO (MArgList o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MArgList o
eas IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MArgList o -> IO (MArgList o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MArgList o
as
    ALConPar MArgList o
as -> MArgList o -> ArgList o
forall o. MArgList o -> ArgList o
ALConPar (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MArgList o -> IO (MArgList o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH MArgList o
as

metaliseokh :: MExp o -> IO (MExp o)
metaliseokh :: forall o. MExp o -> IO (MExp o)
metaliseokh = MExp o -> IO (MExp o)
forall t. MetaliseOKH t => t -> IO t
metaliseOKH

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

class ExpandMetas t where
  expandMetas :: t -> IO t

instance ExpandMetas t => ExpandMetas (MM t a) where
  expandMetas :: MM t a -> IO (MM t a)
expandMetas = \case
    NotM t
e -> t -> MM t a
forall a blk. a -> MM a blk
NotM (t -> MM t a) -> IO t -> IO (MM t a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> IO t
forall t. ExpandMetas t => t -> IO t
expandMetas t
e
    Meta Metavar t a
m -> do
      Maybe t
mb <- IORef (Maybe t) -> IO (Maybe t)
forall a. IORef a -> IO a
readIORef (Metavar t a -> IORef (Maybe t)
forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar t a
m)
      case Maybe t
mb of
        Maybe t
Nothing -> MM t a -> IO (MM t a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MM t a -> IO (MM t a)) -> MM t a -> IO (MM t a)
forall a b. (a -> b) -> a -> b
$ Metavar t a -> MM t a
forall a blk. Metavar a blk -> MM a blk
Meta Metavar t a
m
        Just t
e  -> t -> MM t a
forall a blk. a -> MM a blk
NotM (t -> MM t a) -> IO t -> IO (MM t a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> IO t
forall t. ExpandMetas t => t -> IO t
expandMetas t
e

instance ExpandMetas t => ExpandMetas (Abs t) where
  expandMetas :: Abs t -> IO (Abs t)
expandMetas (Abs MId
id t
b) = MId -> t -> Abs t
forall a. MId -> a -> Abs a
Abs MId
id (t -> Abs t) -> IO t -> IO (Abs t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> IO t
forall t. ExpandMetas t => t -> IO t
expandMetas t
b

instance ExpandMetas (Exp o) where
  expandMetas :: Exp o -> IO (Exp o)
expandMetas = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
okh Elr o
elr MArgList o
args -> Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
okh Elr o
elr (MArgList o -> Exp o) -> IO (MArgList o) -> IO (Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MArgList o -> IO (MArgList o)
forall t. ExpandMetas t => t -> IO t
expandMetas MArgList o
args
    Lam Hiding
hid Abs (MExp o)
b -> Hiding -> Abs (MExp o) -> Exp o
forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (MExp o) -> IO (Abs (MExp o))
forall t. ExpandMetas t => t -> IO t
expandMetas Abs (MExp o)
b
    Pi Maybe (UId o)
uid Hiding
hid Bool
dep MExp o
it Abs (MExp o)
ot ->
      Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
dep (MExp o -> Abs (MExp o) -> Exp o)
-> IO (MExp o) -> IO (Abs (MExp o) -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MExp o -> IO (MExp o)
forall t. ExpandMetas t => t -> IO t
expandMetas MExp o
it IO (Abs (MExp o) -> Exp o) -> IO (Abs (MExp o)) -> IO (Exp o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs (MExp o) -> IO (Abs (MExp o))
forall t. ExpandMetas t => t -> IO t
expandMetas Abs (MExp o)
ot
    t :: Exp o
t@Sort{} -> Exp o -> IO (Exp o)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp o
t
    t :: Exp o
t@AbsurdLambda{} -> Exp o -> IO (Exp o)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp o
t

instance ExpandMetas (ArgList o) where
  expandMetas :: ArgList o -> IO (ArgList o)
expandMetas = \case
    ArgList o
ALNil -> ArgList o -> IO (ArgList o)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgList o
forall o. ArgList o
ALNil
    ALCons Hiding
hid MExp o
a MArgList o
as -> Hiding -> MExp o -> MArgList o -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid (MExp o -> MArgList o -> ArgList o)
-> IO (MExp o) -> IO (MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MExp o -> IO (MExp o)
forall t. ExpandMetas t => t -> IO t
expandMetas MExp o
a IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MArgList o -> IO (MArgList o)
forall t. ExpandMetas t => t -> IO t
expandMetas MArgList o
as
    ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
idx Hiding
hid MArgList o
as ->
      (\ MArgList o
a MM (ConstRef o) (RefInfo o)
b -> MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
forall o.
MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
ALProj MArgList o
a MM (ConstRef o) (RefInfo o)
b Hiding
hid) (MArgList o
 -> MM (ConstRef o) (RefInfo o) -> MArgList o -> ArgList o)
-> IO (MArgList o)
-> IO (MM (ConstRef o) (RefInfo o) -> MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MArgList o -> IO (MArgList o)
forall t. ExpandMetas t => t -> IO t
expandMetas MArgList o
eas
      IO (MM (ConstRef o) (RefInfo o) -> MArgList o -> ArgList o)
-> IO (MM (ConstRef o) (RefInfo o)) -> IO (MArgList o -> ArgList o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MM (ConstRef o) (RefInfo o) -> IO (MM (ConstRef o) (RefInfo o))
forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MM (ConstRef o) (RefInfo o)
idx IO (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MArgList o -> IO (MArgList o)
forall t. ExpandMetas t => t -> IO t
expandMetas MArgList o
as
    ALConPar MArgList o
as -> MArgList o -> ArgList o
forall o. MArgList o -> ArgList o
ALConPar (MArgList o -> ArgList o) -> IO (MArgList o) -> IO (ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MArgList o -> IO (MArgList o)
forall t. ExpandMetas t => t -> IO t
expandMetas MArgList o
as

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

addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs :: forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs Clos (MArgList o) o
newargs ICArgList o
CALNil = Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat Clos (MArgList o) o
newargs ICArgList o
forall o. ICArgList o
CALNil
addtrailingargs Clos (MArgList o) o
newargs (CALConcat Clos (MArgList o) o
x ICArgList o
xs) = Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat Clos (MArgList o) o
x (Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
addtrailingargs Clos (MArgList o) o
newargs ICArgList o
xs)

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

closify :: MExp o -> CExp o
closify :: forall o. MExp o -> CExp o
closify MExp o
e = [MExp o] -> ICExp o -> TrBr (ICExp o) o
forall a o. [MExp o] -> a -> TrBr a o
TrBr [MExp o
e] ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [] MExp o
e)

sub :: MExp o -> CExp o -> CExp o
-- sub e (Clos [] x) = Clos [Sub e] x
sub :: forall o. MExp o -> CExp o -> CExp o
sub MExp o
e (TrBr [MExp o]
trs (Clos (CAction o
Skip : [CAction o]
as) MExp o
x)) = [MExp o] -> ICExp o -> TrBr (ICExp o) o
forall a o. [MExp o] -> a -> TrBr a o
TrBr (MExp o
e MExp o -> [MExp o] -> [MExp o]
forall a. a -> [a] -> [a]
: [MExp o]
trs) ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos (ICExp o -> CAction o
forall o. ICExp o -> CAction o
Sub ([CAction o] -> MExp o -> ICExp o
forall a o. [CAction o] -> a -> Clos a o
Clos [] MExp o
e) CAction o -> [CAction o] -> [CAction o]
forall a. a -> [a] -> [a]
: [CAction o]
as) MExp o
x)
{-sub e (Clos (Weak n : as) x) = if n == 1 then
                                Clos as x
                               else
                                Clos (Weak (n - 1) : as) x-}
sub MExp o
_ TrBr (ICExp o) o
_ = TrBr (ICExp o) o
forall a. HasCallStack => a
__IMPOSSIBLE__

subi :: MExp o -> ICExp o -> ICExp o
subi :: forall o. MExp o -> ICExp o -> ICExp o
subi MExp o
e (Clos (CAction o
Skip : [CAction o]
as) MExp o
x) = [CAction o] -> MExp o -> Clos (MExp o) o
forall a o. [CAction o] -> a -> Clos a o
Clos (Clos (MExp o) o -> CAction o
forall o. ICExp o -> CAction o
Sub ([CAction o] -> MExp o -> Clos (MExp o) o
forall a o. [CAction o] -> a -> Clos a o
Clos [] MExp o
e) CAction o -> [CAction o] -> [CAction o]
forall a. a -> [a] -> [a]
: [CAction o]
as) MExp o
x
subi MExp o
_ Clos (MExp o) o
_ = Clos (MExp o) o
forall a. HasCallStack => a
__IMPOSSIBLE__

weak :: Weakening t => Nat -> t -> t
weak :: forall t. Weakening t => Int -> t -> t
weak Int
0 = t -> t
forall a. a -> a
id
weak Int
n = Int -> t -> t
forall t. Weakening t => Int -> t -> t
weak' Int
n

class Weakening t where
  weak' :: Nat -> t -> t

instance Weakening a => Weakening (TrBr a o) where
  weak' :: Int -> TrBr a o -> TrBr a o
weak' Int
n (TrBr [MExp o]
trs a
e) = [MExp o] -> a -> TrBr a o
forall a o. [MExp o] -> a -> TrBr a o
TrBr [MExp o]
trs (Int -> a -> a
forall t. Weakening t => Int -> t -> t
weak' Int
n a
e)

instance Weakening (Clos a o) where
  weak' :: Int -> Clos a o -> Clos a o
weak' Int
n (Clos [CAction o]
as a
x) = [CAction o] -> a -> Clos a o
forall a o. [CAction o] -> a -> Clos a o
Clos (Int -> CAction o
forall o. Int -> CAction o
Weak Int
n CAction o -> [CAction o] -> [CAction o]
forall a. a -> [a] -> [a]
: [CAction o]
as) a
x

instance Weakening (ICArgList o) where
  weak' :: Int -> ICArgList o -> ICArgList o
weak' Int
n = \case
    ICArgList o
CALNil         -> ICArgList o
forall o. ICArgList o
CALNil
    CALConcat Clos (MArgList o) o
a ICArgList o
as -> Clos (MArgList o) o -> ICArgList o -> ICArgList o
forall o. Clos (MArgList o) o -> ICArgList o -> ICArgList o
CALConcat (Int -> Clos (MArgList o) o -> Clos (MArgList o) o
forall t. Weakening t => Int -> t -> t
weak' Int
n Clos (MArgList o) o
a) (Int -> ICArgList o -> ICArgList o
forall t. Weakening t => Int -> t -> t
weak' Int
n ICArgList o
as)

instance Weakening (Elr o) where
  weak' :: Int -> Elr o -> Elr o
weak' Int
n = (Int -> Int) -> Elr o -> Elr o
forall t. Renaming t => (Int -> Int) -> t -> t
rename (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+)

-- | Substituting for a variable.
doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)
doclos :: forall o. [CAction o] -> Int -> Either Int (ICExp o)
doclos = Int -> [CAction o] -> Int -> Either Int (ICExp o)
forall {o}. Int -> [CAction o] -> Int -> Either Int (ICExp o)
f Int
0
 where
  -- ns is the number of weakenings
  f :: Int -> [CAction o] -> Int -> Either Int (ICExp o)
f Int
ns []            Int
i = Int -> Either Int (ICExp o)
forall a b. a -> Either a b
Left (Int
ns Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)
  f Int
ns (Weak Int
n : [CAction o]
xs) Int
i = Int -> [CAction o] -> Int -> Either Int (ICExp o)
f (Int
ns Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) [CAction o]
xs Int
i
  f Int
ns (Sub ICExp o
s  : [CAction o]
_ ) Int
0 = ICExp o -> Either Int (ICExp o)
forall a b. b -> Either a b
Right (Int -> ICExp o -> ICExp o
forall t. Weakening t => Int -> t -> t
weak Int
ns ICExp o
s)
  f Int
ns (CAction o
Skip   : [CAction o]
_ ) Int
0 = Int -> Either Int (ICExp o)
forall a b. a -> Either a b
Left Int
ns
  f Int
ns (CAction o
Skip   : [CAction o]
xs) Int
i = Int -> [CAction o] -> Int -> Either Int (ICExp o)
f (Int
ns Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [CAction o]
xs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  f Int
ns (Sub ICExp o
_  : [CAction o]
xs) Int
i = Int -> [CAction o] -> Int -> Either Int (ICExp o)
f Int
ns [CAction o]
xs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)


-- | FreeVars class and instances

freeVars :: FreeVars t => t -> Set.Set Nat
freeVars :: forall t. FreeVars t => t -> Set Int
freeVars = Int -> t -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
0

class FreeVars t where
  freeVarsOffset :: Nat -> t -> Set.Set Nat

instance (FreeVars a, FreeVars b) => FreeVars (a, b) where
  freeVarsOffset :: Int -> (a, b) -> Set Int
freeVarsOffset Int
n (a
a, b
b) = Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Int -> a -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n a
a) (Int -> b -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n b
b)

instance FreeVars t => FreeVars (MM t a) where
  freeVarsOffset :: Int -> MM t a -> Set Int
freeVarsOffset Int
n MM t a
e = Int -> t -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n (Empty -> MM t a -> t
forall a b. Empty -> MM a b -> a
rm Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ MM t a
e)

instance FreeVars t => FreeVars (Abs t) where
  freeVarsOffset :: Int -> Abs t -> Set Int
freeVarsOffset Int
n (Abs MId
id t
e) = Int -> t -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) t
e

instance FreeVars (Elr o) where
  freeVarsOffset :: Int -> Elr o -> Set Int
freeVarsOffset Int
n = \case
    Var Int
v   -> Int -> Set Int
forall a. a -> Set a
Set.singleton (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n)
    Const{} -> Set Int
forall a. Set a
Set.empty

instance FreeVars (Exp o) where
  freeVarsOffset :: Int -> Exp o -> Set Int
freeVarsOffset Int
n = \case
   App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr MArgList o
args -> Int -> (Elr o, MArgList o) -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n (Elr o
elr, MArgList o
args)
   Lam Hiding
_ Abs (MExp o)
b          -> Int -> Abs (MExp o) -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n Abs (MExp o)
b
   Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it Abs (MExp o)
ot   -> Int -> (MExp o, Abs (MExp o)) -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n (MExp o
it, Abs (MExp o)
ot)
   Sort{}           -> Set Int
forall a. Set a
Set.empty
   AbsurdLambda{}   -> Set Int
forall a. Set a
Set.empty

instance FreeVars (ArgList o) where
  freeVarsOffset :: Int -> ArgList o -> Set Int
freeVarsOffset Int
n ArgList o
es = case ArgList o
es of
    ArgList o
ALNil         -> Set Int
forall a. Set a
Set.empty
    ALCons Hiding
_ MExp o
e MArgList o
es -> Int -> (MExp o, MArgList o) -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n (MExp o
e, MArgList o
es)
    ALConPar MArgList o
es   -> Int -> MArgList o -> Set Int
forall t. FreeVars t => Int -> t -> Set Int
freeVarsOffset Int
n MArgList o
es
    ALProj{}      -> Set Int
forall a. HasCallStack => a
__IMPOSSIBLE__


-- | Renaming Typeclass and instances
rename :: Renaming t => (Nat -> Nat) -> t -> t
rename :: forall t. Renaming t => (Int -> Int) -> t -> t
rename = Int -> (Int -> Int) -> t -> t
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
0

class Renaming t where
  renameOffset :: Nat -> (Nat -> Nat) -> t -> t

instance (Renaming a, Renaming b) => Renaming (a, b) where
  renameOffset :: Int -> (Int -> Int) -> (a, b) -> (a, b)
renameOffset Int
j Int -> Int
ren (a
a, b
b) = (Int -> (Int -> Int) -> a -> a
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren a
a, Int -> (Int -> Int) -> b -> b
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren b
b)

instance Renaming t => Renaming (MM t a) where
  renameOffset :: Int -> (Int -> Int) -> MM t a -> MM t a
renameOffset Int
j Int -> Int
ren MM t a
e = t -> MM t a
forall a blk. a -> MM a blk
NotM (t -> MM t a) -> t -> MM t a
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Int) -> t -> t
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren (Empty -> MM t a -> t
forall a b. Empty -> MM a b -> a
rm Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ MM t a
e)

instance Renaming t => Renaming (Abs t) where
  renameOffset :: Int -> (Int -> Int) -> Abs t -> Abs t
renameOffset Int
j Int -> Int
ren (Abs MId
id t
e) = MId -> t -> Abs t
forall a. MId -> a -> Abs a
Abs MId
id (t -> Abs t) -> t -> Abs t
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Int) -> t -> t
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Int
ren t
e

instance Renaming (Elr o) where
  renameOffset :: Int -> (Int -> Int) -> Elr o -> Elr o
renameOffset Int
j Int -> Int
ren = \case
    Var Int
v | Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
j -> Int -> Elr o
forall o. Int -> Elr o
Var (Int -> Int
ren (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)
    Elr o
e              -> Elr o
e

instance Renaming (Exp o) where
  renameOffset :: Int -> (Int -> Int) -> Exp o -> Exp o
renameOffset Int
j Int -> Int
ren = \case
    App Maybe (UId o)
uid OKHandle (RefInfo o)
ok Elr o
elr MArgList o
args -> (Elr o -> MArgList o -> Exp o) -> (Elr o, MArgList o) -> Exp o
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
uid OKHandle (RefInfo o)
ok) ((Elr o, MArgList o) -> Exp o) -> (Elr o, MArgList o) -> Exp o
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Int) -> (Elr o, MArgList o) -> (Elr o, MArgList o)
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren (Elr o
elr, MArgList o
args)
    Lam Hiding
hid Abs (MExp o)
e -> Hiding -> Abs (MExp o) -> Exp o
forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid (Int -> (Int -> Int) -> Abs (MExp o) -> Abs (MExp o)
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren Abs (MExp o)
e)
    Pi Maybe (UId o)
a Hiding
b Bool
c MExp o
it Abs (MExp o)
ot -> (MExp o -> Abs (MExp o) -> Exp o)
-> (MExp o, Abs (MExp o)) -> Exp o
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
a Hiding
b Bool
c) ((MExp o, Abs (MExp o)) -> Exp o)
-> (MExp o, Abs (MExp o)) -> Exp o
forall a b. (a -> b) -> a -> b
$ Int
-> (Int -> Int) -> (MExp o, Abs (MExp o)) -> (MExp o, Abs (MExp o))
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren (MExp o
it, Abs (MExp o)
ot)
    e :: Exp o
e@Sort{}         -> Exp o
e
    e :: Exp o
e@AbsurdLambda{} -> Exp o
e

instance Renaming (ArgList o) where
  renameOffset :: Int -> (Int -> Int) -> ArgList o -> ArgList o
renameOffset Int
j Int -> Int
ren = \case
    ArgList o
ALNil           -> ArgList o
forall o. ArgList o
ALNil
    ALCons Hiding
hid MExp o
a MArgList o
as -> (MExp o -> MArgList o -> ArgList o)
-> (MExp o, MArgList o) -> ArgList o
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Hiding -> MExp o -> MArgList o -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid) ((MExp o, MArgList o) -> ArgList o)
-> (MExp o, MArgList o) -> ArgList o
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Int) -> (MExp o, MArgList o) -> (MExp o, MArgList o)
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren (MExp o
a, MArgList o
as)
    ALConPar MArgList o
as     -> MArgList o -> ArgList o
forall o. MArgList o -> ArgList o
ALConPar (Int -> (Int -> Int) -> MArgList o -> MArgList o
forall t. Renaming t => Int -> (Int -> Int) -> t -> t
renameOffset Int
j Int -> Int
ren MArgList o
as)
    ALProj{}        -> ArgList o
forall a. HasCallStack => a
__IMPOSSIBLE__