{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Record.Cubical
  ( addCompositionForRecord
  ) where

import Prelude hiding (null, not, (&&), (||))

import Control.Monad
import Data.Maybe

import Agda.Interaction.Options

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Rules.Data (defineCompData, defineKanOperationForFields)

import Agda.Utils.Boolean
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Impossible
import Agda.Utils.Size


addCompositionForRecord
  :: QName       -- ^ Datatype name.
  -> EtaEquality
  -> ConHead
  -> Telescope   -- ^ @Γ@ parameters.
  -> [Arg QName] -- ^ Projection names.
  -> Telescope   -- ^ @Γ ⊢ Φ@ field types.
  -> Type        -- ^ @Γ ⊢ T@ target type.
  -> TCM ()
addCompositionForRecord :: QName
-> EtaEquality
-> ConHead
-> Tele (Dom (Type'' Term Term))
-> [Arg QName]
-> Tele (Dom (Type'' Term Term))
-> Type'' Term Term
-> TCM ()
addCompositionForRecord QName
name EtaEquality
eta ConHead
con Tele (Dom (Type'' Term Term))
tel [Arg QName]
fs Tele (Dom (Type'' Term Term))
ftel Type'' Term Term
rect = do
  cxt <- TCMT IO (Tele (Dom (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom (Type'' Term Term)))
getContextTelescope
  inTopContext $ do

    -- Record has no fields: attach composition data to record constructor
    if null fs then do
      kit <- defineCompData name con (abstract cxt tel) [] ftel rect empty
      modifySignature $ updateDefinition (conName con) $ updateTheDef $ \case
        r :: Defn
r@Constructor{} -> Defn
r { conComp = kit, conProj = Just [] }  -- no projections
        Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- No-eta record with pattern matching (i.e., withOUT copattern
    -- matching): define composition as for a data type, attach it to
    -- the record.
    else if theEtaEquality eta == NoEta PatternMatching then do
      kit <- defineCompData name con (abstract cxt tel) (unArg <$> fs) ftel rect empty
      modifySignature $ updateDefinition name $ updateTheDef $ \case
        r :: Defn
r@Record{} -> Defn
r { recComp = kit }
        Defn
_ -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Record has fields: attach composition data to record type
    else do
      -- If record has irrelevant fields but irrelevant projections are disabled,
      -- we cannot generate composition data.
      kit <- ifM (return (any isIrrelevant fs)
                  `and2M` do not . optIrrelevantProjections <$> pragmaOptions)
        {-then-} (return emptyCompKit)
        {-else-} (defineCompKitR name (abstract cxt tel) ftel fs rect)
      modifySignature $ updateDefinition name $ updateTheDef $ \case
        r :: Defn
r@Record{} -> Defn
r { recComp = kit }
        Defn
_          -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__


defineCompKitR ::
    QName          -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Telescope   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM CompKit
defineCompKitR :: QName
-> Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term))
-> [Arg QName]
-> Type'' Term Term
-> TCM CompKit
defineCompKitR QName
name Tele (Dom (Type'' Term Term))
params Tele (Dom (Type'' Term Term))
fsT [Arg QName]
fns Type'' Term Term
rect = do
  required <- (SomeBuiltin -> TCMT IO (Maybe Term))
-> [SomeBuiltin] -> TCMT IO [Maybe Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SomeBuiltin -> TCMT IO (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm'
        [ BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinInterval
        , BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinIZero
        , BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinIOne
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinIMin
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinIMax
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinINeg
        , PrimitiveId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin PrimitiveId
builtinPOr
        , BuiltinId -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin BuiltinId
builtinItIsOne
        ]
  reportSDoc "tc.rec.cxt" 30 $ prettyTCM params
  reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT
  reportSDoc "tc.rec.cxt" 30 $ pretty rect
  if not $ all isJust required then return $ emptyCompKit else do
    transp <- whenDefined [builtinTrans]              (defineKanOperationR DoTransp name params fsT fns rect)
    hcomp  <- whenDefined [builtinTrans,builtinHComp] (defineKanOperationR DoHComp name params fsT fns rect)
    return $ CompKit
      { nameOfTransp = transp
      , nameOfHComp  = hcomp
      }
  where
    whenDefined :: t a -> m (Maybe a) -> m (Maybe a)
whenDefined t a
xs m (Maybe a)
m = do
      xs <- (a -> m (Maybe Term)) -> t a -> m (t (Maybe Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM a -> m (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' t a
xs
      if all isJust xs then m else return Nothing


defineKanOperationR
  :: Command
  -> QName       -- ^ some name, e.g. record name
  -> Telescope   -- ^ param types Δ
  -> Telescope   -- ^ fields' types Δ ⊢ Φ
  -> [Arg QName] -- ^ fields' names
  -> Type        -- ^ record type Δ ⊢ T
  -> TCM (Maybe QName)
defineKanOperationR :: Command
-> QName
-> Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term))
-> [Arg QName]
-> Type'' Term Term
-> TCMT IO (Maybe QName)
defineKanOperationR Command
cmd QName
name Tele (Dom (Type'' Term Term))
params Tele (Dom (Type'' Term Term))
fsT [Arg QName]
fns Type'' Term Term
rect = do
  let project :: Term -> QName -> Term
project = (\ Term
t QName
fn -> Term
t Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
fn])
  stuff <- (((QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
   [Dom (Type'' Term Term)], [Term]),
  Substitution)
 -> (QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
     [Dom (Type'' Term Term)], [Term]))
-> Maybe
     ((QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
       [Dom (Type'' Term Term)], [Term]),
      Substitution)
-> Maybe
     (QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
      [Dom (Type'' Term Term)], [Term])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
  [Dom (Type'' Term Term)], [Term]),
 Substitution)
-> (QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
    [Dom (Type'' Term Term)], [Term])
forall a b. (a, b) -> a
fst (Maybe
   ((QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
     [Dom (Type'' Term Term)], [Term]),
    Substitution)
 -> Maybe
      (QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
       [Dom (Type'' Term Term)], [Term]))
-> TCMT
     IO
     (Maybe
        ((QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
          [Dom (Type'' Term Term)], [Term]),
         Substitution))
-> TCMT
     IO
     (Maybe
        (QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
         [Dom (Type'' Term Term)], [Term]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Command
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Tele (Dom (Type'' Term Term))
-> Tele (Dom (Type'' Term Term))
-> [Arg QName]
-> Type'' Term Term
-> TCMT
     IO
     (Maybe
        ((QName, Tele (Dom (Type'' Term Term)), Type'' Term Term,
          [Dom (Type'' Term Term)], [Term]),
         Substitution))
defineKanOperationForFields Command
cmd Maybe Term
forall a. Maybe a
Nothing Term -> QName -> Term
project QName
name Tele (Dom (Type'' Term Term))
params Tele (Dom (Type'' Term Term))
fsT [Arg QName]
fns Type'' Term Term
rect

  caseMaybe stuff (return Nothing) $ \ (QName
theName, Tele (Dom (Type'' Term Term))
gamma, Type'' Term Term
rtype, [Dom (Type'' Term Term)]
clause_types, [Term]
bodies) -> do
  -- phi = 1 clause
  c' <- do
           io <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
           Just io_name <- getBuiltinName' builtinIOne
           one <- primItIsOne
           tInterval <- primIntervalType
           let
              (ix,rhs) =
                case cmd of
                  -- TranspRArgs = phi : I, a0 : ..
                  -- Γ = Δ^I , CompRArgs
                  -- pats = ... | phi = i1
                  -- body = a0
                  Command
DoTransp -> (Int
1,Int -> Elims -> Term
Var Int
0 [])
                  -- HCompRArgs = phi : I, u : .., a0 : ..
                  -- Γ = Δ, CompRArgs
                  -- pats = ... | phi = i1
                  -- body = u i1 itIsOne
                  Command
DoHComp  -> (Int
2,Int -> Elims -> Term
Var Int
1 [] Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
io, Relevance -> Arg Term -> Arg Term
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
irrelevant (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall e. e -> Arg e
argN Term
one])

              p = ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' DBPatVar)]
-> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
io_name DataOrRecord
forall p. DataOrRecord' p
IsData Induction
Inductive [])
                       (ConPatternInfo
noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval)
                                         , conPFallThrough = True })
                         []

              -- gamma, rtype

              s = Int -> Pattern' DBPatVar -> Substitution' (Pattern' DBPatVar)
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
ix Pattern' DBPatVar
p

              pats :: [NamedArg DeBruijnPattern]
              pats = Substitution' (Pattern' DBPatVar)
Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
s Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom (Type'' Term Term)) -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom (Type'' Term Term))
gamma

              t :: Type
              t = Substitution' (Pattern' DBPatVar)
s Substitution' (Pattern' DBPatVar)
-> Type'' Term Term -> Type'' Term Term
forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
`applyPatSubst` Type'' Term Term
rtype

              gamma' :: Telescope
              gamma' = [String]
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
unflattenTel ([String]
ns0 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ns1) ([Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term)))
-> [Dom (Type'' Term Term)] -> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Substitution' (Pattern' DBPatVar)
s Substitution' (Pattern' DBPatVar)
-> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a.
TermSubst a =>
Substitution' (Pattern' DBPatVar) -> a -> a
`applyPatSubst` ([Dom (Type'' Term Term)]
g0 [Dom (Type'' Term Term)]
-> [Dom (Type'' Term Term)] -> [Dom (Type'' Term Term)]
forall a. [a] -> [a] -> [a]
++ [Dom (Type'' Term Term)]
g1)
               where
                ([Dom (Type'' Term Term)]
g0,Dom (Type'' Term Term)
_:[Dom (Type'' Term Term)]
g1) = Int
-> [Dom (Type'' Term Term)]
-> ([Dom (Type'' Term Term)], [Dom (Type'' Term Term)])
forall a. Int -> [a] -> ([a], [a])
splitAt (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
ix) ([Dom (Type'' Term Term)]
 -> ([Dom (Type'' Term Term)], [Dom (Type'' Term Term)]))
-> [Dom (Type'' Term Term)]
-> ([Dom (Type'' Term Term)], [Dom (Type'' Term Term)])
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [Dom (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom (Type'' Term Term))
gamma
                ([String]
ns0,String
_:[String]
ns1) = Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt (Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
ix) ([String] -> ([String], [String]))
-> [String] -> ([String], [String])
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> [String]
teleNames Tele (Dom (Type'' Term Term))
gamma

              c = Clause { clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseTel :: Tele (Dom (Type'' Term Term))
clauseTel       = Tele (Dom (Type'' Term Term))
gamma'
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseBody :: Maybe Term
clauseBody      = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Term
rhs
                         , clauseType :: Maybe (Arg (Type'' Term Term))
clauseType      = Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a. a -> Maybe a
Just (Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term)))
-> Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Arg (Type'' Term Term)
forall e. e -> Arg e
argN Type'' Term Term
t
                         , clauseCatchall :: Catchall
clauseCatchall    = Catchall
forall a. Null a => a
empty
                         , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
NotRecursive  -- definitely non-recursive!
                         , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                         , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                         , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                         }
           reportSDoc "trans.rec.face" 17 $ text $ show c
           return c
  cs <- forM (zip3 fns clause_types bodies) $ \ (Arg QName
fname, Dom (Type'' Term Term)
clause_ty, Term
body) -> do
          let
              pats :: [NamedArg (Pattern' DBPatVar)]
pats = Tele (Dom (Type'' Term Term)) -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom (Type'' Term Term))
gamma [NamedArg (Pattern' DBPatVar)]
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
forall a. [a] -> [a] -> [a]
++ [Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a. a -> NamedArg a
defaultNamedArg (Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar))
-> Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> Pattern' DBPatVar
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
ProjSystem (QName -> Pattern' DBPatVar) -> QName -> Pattern' DBPatVar
forall a b. (a -> b) -> a -> b
$ Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
fname]
              c :: Clause
c = Clause { clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseTel :: Tele (Dom (Type'' Term Term))
clauseTel       = Tele (Dom (Type'' Term Term))
gamma
                         , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
pats
                         , clauseBody :: Maybe Term
clauseBody      = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
body
                         , clauseType :: Maybe (Arg (Type'' Term Term))
clauseType      = Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a. a -> Maybe a
Just (Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term)))
-> Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Arg (Type'' Term Term)
forall e. e -> Arg e
argN (Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom (Type'' Term Term)
clause_ty)
                         , clauseCatchall :: Catchall
clauseCatchall    = Catchall
forall a. Null a => a
empty
                         , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
MaybeRecursive
                             -- Andreas 2020-02-06 TODO
                             -- Or: NotRecursive;  is it known to be non-recursive?
                         , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                         , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                         , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
                         }
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"trans.rec" Int
17 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Clause -> String
forall a. Show a => a -> String
show Clause
c
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"trans.rec" Int
16 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"type =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Maybe (Arg (Type'' Term Term)) -> String
forall a. Show a => a -> String
show (Clause -> Maybe (Arg (Type'' Term Term))
clauseType Clause
c))
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"trans.rec" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM (Type'' Term Term -> TCMT IO Doc)
-> Type'' Term Term -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall t. Abstract t => Tele (Dom (Type'' Term Term)) -> t -> t
abstract Tele (Dom (Type'' Term Term))
gamma (Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom (Type'' Term Term)
clause_ty)
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"trans.rec" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"body =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Tele (Dom (Type'' Term Term)) -> Term -> Term
forall t. Abstract t => Tele (Dom (Type'' Term Term)) -> t -> t
abstract Tele (Dom (Type'' Term Term))
gamma Term
body)
          Clause -> TCMT IO Clause
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
  addClauses theName $ c' : cs
  reportSDoc "trans.rec" 15 $ text $ "compiling clauses for " ++ show theName
  (mst, _, cc) <- inTopContext (compileClauses Nothing cs)
  whenJust mst $ setSplitTree theName
  setCompiledClauses theName cc
  reportSDoc "trans.rec" 15 $ text $ "compiled"
  return $ Just theName