{-# 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
-> Telescope
-> [Arg QName]
-> Telescope
-> Type
-> TCM ()
addCompositionForRecord QName
name EtaEquality
eta ConHead
con Telescope
tel [Arg QName]
fs Telescope
ftel Type
rect = do
  cxt <- TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
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
-> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
defineCompKitR QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
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
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCMT IO (Maybe QName)
defineKanOperationR Command
cmd QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
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, Telescope, Type, [Dom Type], [Term]), Substitution)
 -> (QName, Telescope, Type, [Dom Type], [Term]))
-> Maybe
     ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-> Maybe (QName, Telescope, Type, [Dom Type], [Term])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-> (QName, Telescope, Type, [Dom Type], [Term])
forall a b. (a, b) -> a
fst (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
 -> Maybe (QName, Telescope, Type, [Dom Type], [Term]))
-> TCMT
     IO
     (Maybe
        ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
-> TCMT IO (Maybe (QName, Telescope, Type, [Dom Type], [Term]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Command
-> Maybe Term
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCMT
     IO
     (Maybe
        ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineKanOperationForFields Command
cmd Maybe Term
forall a. Maybe a
Nothing Term -> QName -> Term
project QName
name Telescope
params Telescope
fsT [Arg QName]
fns Type
rect

  caseMaybe stuff (return Nothing) $ \ (QName
theName, Telescope
gamma, Type
rtype, [Dom Type]
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` Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma

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

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

              c = Clause { clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
                         , clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
                         , clauseTel :: Telescope
clauseTel       = Telescope
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)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall e. e -> Arg e
argN Type
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
clause_ty, Term
body) -> do
          let
              pats :: [NamedArg (Pattern' DBPatVar)]
pats = Telescope -> [NamedArg (Pattern' DBPatVar)]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
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 :: Telescope
clauseTel       = Telescope
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)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall e. e -> Arg e
argN (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
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) -> String
forall a. Show a => a -> String
show (Clause -> Maybe (Arg Type)
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> TCMT IO Doc) -> Type -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
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 (Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
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