{-# OPTIONS_GHC -Wunused-imports #-}

------------------------------------------------------------------------
-- | Handling of the INFINITY, SHARP and FLAT builtins.
------------------------------------------------------------------------

module Agda.TypeChecking.Rules.Builtin.Coinduction where

import Agda.Interaction.Options.Base

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Term

import Agda.Utils.Lens

-- | The type of @∞@.

typeOfInf :: TCM Type
typeOfInf :: TCM Type
typeOfInf = ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
            (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0)

-- | The type of @♯_@.

typeOfSharp :: TCM Type
typeOfSharp :: TCM Type
typeOfSharp = ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
              ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
              (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
              (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)

-- | The type of @♭@.

typeOfFlat :: TCM Type
typeOfFlat :: TCM Type
typeOfFlat = ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"a" (TCMT IO Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
             ArgName -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
ArgName -> m Type -> m Type -> m Type
hPi ArgName
"A" (Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
sort (Sort -> TCM Type) -> Sort -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
             (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
             (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)

-- | Binds the INFINITY builtin, but does not change the type's
-- definition.

bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x = BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinInf ResolvedName
x ((QName -> Definition -> TCMT IO Term) -> TCM ())
-> (QName -> Definition -> TCMT IO Term) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \QName
inf Definition
_ -> do
  Term
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
inf) (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
typeOfInf
  Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
inf []

-- | Binds the SHARP builtin, and changes the definitions of INFINITY
-- and SHARP.

-- The following (no longer supported) definition is used:
--
-- codata ∞ {a} (A : Set a) : Set a where
--   ♯_ : (x : A) → ∞ A

bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x =
  BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinSharp ResolvedName
x ((QName -> Definition -> TCMT IO Term) -> TCM ())
-> (QName -> Definition -> TCMT IO Term) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \QName
sharp Definition
sharpDefn -> do
    Type
sharpType <- TCM Type
typeOfSharp
    TelV Tele (Dom Type)
fieldTel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
sharpType
    Term
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
sharp) Type
sharpType
    Def QName
inf Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
    Definition
infDefn   <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
inf
    Bool
erasure   <- PragmaOptions -> Bool
optErasure (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    QName -> Definition -> TCM ()
addConstant (Definition -> QName
defName Definition
infDefn) (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Definition
infDefn { defPolarity       = [] -- not monotone
              , defArgOccurrences = [Unused, StrictPos]
              , theDef = Record
                  { recPars           = 2
                  , recInduction      = Just CoInductive
                  , recClause         = Nothing
                  , recConHead        = ConHead sharp (IsRecord CopatternMatching) CoInductive []  -- flat is added later
                  , recNamedCon       = True
                  , recFields         = []  -- flat is added later
                  , recTel            = fieldTel
                  , recEtaEquality'   = Inferred $ NoEta CopatternMatching
                  , recPatternMatching= CopatternMatching
                  , recMutual         = Just []
                  , recTerminates     = Just True  -- not recursive
                  , recAbstr          = ConcreteDef
                  , recComp           = emptyCompKit
                  }
              }
    QName -> Definition -> TCM ()
addConstant QName
sharp (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Definition
sharpDefn { theDef = Constructor
                    { conPars   = 2
                    , conArity  = 1
                    , conSrcCon = ConHead sharp (IsRecord CopatternMatching) CoInductive [] -- flat is added as field later
                    , conData   = defName infDefn
                    , conAbstr  = ConcreteDef
                    , conComp   = emptyCompKit
                    , conProj   = Nothing
                    , conForced = []
                    , conErased = Nothing
                    , conErasure = erasure
                    , conInline  = True  -- This might make the sharp-translation superfluous.
                    }
                }
    Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
sharp []

-- | Binds the FLAT builtin, and changes its definition.

-- The following (no longer supported) definition is used:
--
--   ♭ : ∀ {a} {A : Set a} → ∞ A → A
--   ♭ (♯ x) = x

bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat :: ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x =
  BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtinFlat ResolvedName
x ((QName -> Definition -> TCMT IO Term) -> TCM ())
-> (QName -> Definition -> TCMT IO Term) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
flat Definition
flatDefn -> do
    Term
_ <- Expr -> Type -> TCMT IO Term
checkExpr (QName -> Expr
A.Def QName
flat) (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
typeOfFlat
    Def QName
sharp Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSharp
    LevelKit
kit         <- TCMT IO LevelKit
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m LevelKit
requireLevels
    Def QName
inf Elims
_   <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
    let sharpCon :: ConHead
sharpCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive [QName -> Arg QName
forall a. a -> Arg a
defaultArg QName
flat]
        level :: Type
level    = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def (LevelKit -> QName
typeName LevelKit
kit) []
        tel     :: Telescope
        tel :: Tele (Dom Type)
tel      = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall e. e -> Dom e
domH (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type
level)                  (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"a" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
                   Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall e. e -> Dom e
domH (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0)       (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"A" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
                   Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall e. e -> Dom e
domN (Type -> Dom Type) -> Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0) (Abs (Tele (Dom Type)) -> Tele (Dom Type))
-> Abs (Tele (Dom Type)) -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
"x" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
-> Tele (Dom Type) -> Abs (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$
                   Tele (Dom Type)
forall a. Tele a
EmptyTel
        infA :: Type
infA     = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
inf [ Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
1 ]
        cpi :: ConPatternInfo
cpi      = ConPatternInfo
noConPatternInfo { conPType = Just $ defaultArg infA
                                    , conPLazy = True }
    let clause :: Clause
clause   = Clause
          { clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
          , clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
          , clauseTel :: Tele (Dom Type)
clauseTel       = Tele (Dom Type)
tel
          , namedClausePats :: NAPs
namedClausePats = [ Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a. a -> Arg a
argN (Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar)))
-> Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
forall a. Maybe a
Nothing (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
-> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$
              ConHead -> ConPatternInfo -> NAPs -> Pattern' DBPatVar
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
sharpCon ConPatternInfo
cpi [ Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a. a -> Arg a
argN (Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar)))
-> Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
forall a b. (a -> b) -> a -> b
$ Maybe NamedName -> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
forall a. Maybe a
Nothing (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
-> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> Pattern' DBPatVar
forall a. DeBruijn a => ArgName -> Int -> a
debruijnNamedVar ArgName
"x" Int
0 ] ]
          , 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
$ Int -> Term
var Int
0
          , 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 a. a -> Arg a
defaultArg (Type -> Arg Type) -> Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
1
          , clauseCatchall :: Bool
clauseCatchall    = Bool
False
          , clauseExact :: Maybe Bool
clauseExact       = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
          , clauseRecursive :: Maybe Bool
clauseRecursive   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
          , 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
          }
        cc :: CompiledClauses' Term
cc = Arg Int -> Case (CompiledClauses' Term) -> CompiledClauses' Term
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Int -> Arg Int
forall a. a -> Arg a
defaultArg Int
0) (Case (CompiledClauses' Term) -> CompiledClauses' Term)
-> Case (CompiledClauses' Term) -> CompiledClauses' Term
forall a b. (a -> b) -> a -> b
$ QName
-> Bool
-> WithArity (CompiledClauses' Term)
-> Case (CompiledClauses' Term)
forall c. QName -> Bool -> WithArity c -> Case c
conCase QName
sharp Bool
False (WithArity (CompiledClauses' Term) -> Case (CompiledClauses' Term))
-> WithArity (CompiledClauses' Term)
-> Case (CompiledClauses' Term)
forall a b. (a -> b) -> a -> b
$ Int -> CompiledClauses' Term -> WithArity (CompiledClauses' Term)
forall c. Int -> c -> WithArity c
WithArity Int
1 (CompiledClauses' Term -> WithArity (CompiledClauses' Term))
-> CompiledClauses' Term -> WithArity (CompiledClauses' Term)
forall a b. (a -> b) -> a -> b
$ [Arg ArgName] -> Term -> CompiledClauses' Term
forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [ArgName -> Arg ArgName
forall a. a -> Arg a
defaultArg ArgName
"x"] (Term -> CompiledClauses' Term) -> Term -> CompiledClauses' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0
        projection :: Projection
projection = Projection
          { projProper :: Maybe QName
projProper   = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
inf
          , projOrig :: QName
projOrig     = QName
flat
          , projFromType :: Arg QName
projFromType = QName -> Arg QName
forall a. a -> Arg a
defaultArg QName
inf
          , projIndex :: Int
projIndex    = Int
3
          , projLams :: ProjLams
projLams     = [Arg ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$ [ ArgName -> Arg ArgName
forall a. a -> Arg a
argH ArgName
"a" , ArgName -> Arg ArgName
forall a. a -> Arg a
argH ArgName
"A" , ArgName -> Arg ArgName
forall a. a -> Arg a
argN ArgName
"x" ]
          }
    FunctionData
fun <- TCMT IO FunctionData
forall (m :: * -> *). HasOptions m => m FunctionData
emptyFunctionData
    QName -> Definition -> TCM ()
addConstant QName
flat (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Definition
flatDefn { defPolarity       = []
               , defArgOccurrences = [StrictPos]  -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
               , defCopatternLHS = hasProjectionPatterns cc
               , theDef = FunctionDefn fun
                   { _funClauses      = [clause]
                   , _funCompiled     = Just $ cc
                   , _funProjection   = Right projection
                   , _funMutual       = Just []
                   , _funTerminates   = Just True
                   }
                }

    -- register flat as record field for constructor sharp
    (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
sharp ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Lens' Defn ConstructorData -> LensMap Defn ConstructorData
forall o i. Lens' o i -> LensMap o i
over (ConstructorData -> f ConstructorData) -> Defn -> f Defn
Lens' Defn ConstructorData
lensConstructor LensMap Defn ConstructorData -> LensMap Defn ConstructorData
forall a b. (a -> b) -> a -> b
$ \ ConstructorData
def ->
      ConstructorData
def { _conSrcCon = sharpCon }
    (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
inf ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Lens' Defn RecordData -> LensMap Defn RecordData
forall o i. Lens' o i -> LensMap o i
over (RecordData -> f RecordData) -> Defn -> f Defn
Lens' Defn RecordData
lensRecord LensMap Defn RecordData -> LensMap Defn RecordData
forall a b. (a -> b) -> a -> b
$ \ RecordData
def ->
      RecordData
def { _recConHead = sharpCon, _recFields = [defaultDom flat] }
    Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
flat []

-- The coinductive primitives.
-- moved to TypeChecking.Monad.Builtin