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

module Agda.TypeChecking.Rules.Builtin.Coinduction where

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.Reduce
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 = ArgName
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName ArgName
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 =
  ArgName
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName ArgName
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
    QName -> Definition -> TCM ()
addConstant (Definition -> QName
defName Definition
infDefn) (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Definition
infDefn { defPolarity :: [Polarity]
defPolarity       = [] -- not monotone
              , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
Unused, Occurrence
StrictPos]
              , theDef :: Defn
theDef = Record
                  { recPars :: Int
recPars           = Int
2
                  , recInduction :: Maybe Induction
recInduction      = Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive
                  , recClause :: Maybe Clause
recClause         = Maybe Clause
forall a. Maybe a
Nothing
                  , recConHead :: ConHead
recConHead        = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive []  -- flat is added later
                  , recNamedCon :: Bool
recNamedCon       = Bool
True
                  , recFields :: [Dom QName]
recFields         = []  -- flat is added later
                  , recTel :: Tele (Dom Type)
recTel            = Tele (Dom Type)
fieldTel
                  , recEtaEquality' :: EtaEquality
recEtaEquality'   = HasEta -> EtaEquality
Inferred (HasEta -> EtaEquality) -> HasEta -> EtaEquality
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> HasEta
forall a. a -> HasEta' a
NoEta PatternOrCopattern
CopatternMatching
                  , recPatternMatching :: PatternOrCopattern
recPatternMatching= PatternOrCopattern
CopatternMatching
                  , recMutual :: Maybe [QName]
recMutual         = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
                  , recTerminates :: Maybe Bool
recTerminates     = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True  -- not recursive
                  , recAbstr :: IsAbstract
recAbstr          = IsAbstract
ConcreteDef
                  , recComp :: CompKit
recComp           = CompKit
emptyCompKit
                  }
              }
    QName -> Definition -> TCM ()
addConstant QName
sharp (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Definition
sharpDefn { theDef :: Defn
theDef = Constructor
                    { conPars :: Int
conPars   = Int
2
                    , conArity :: Int
conArity  = Int
1
                    , conSrcCon :: ConHead
conSrcCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
sharp (PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
CopatternMatching) Induction
CoInductive [] -- flat is added as field later
                    , conData :: QName
conData   = Definition -> QName
defName Definition
infDefn
                    , conAbstr :: IsAbstract
conAbstr  = IsAbstract
ConcreteDef
                    , conInd :: Induction
conInd    = Induction
CoInductive
                    , conComp :: CompKit
conComp   = CompKit
emptyCompKit
                    , conProj :: Maybe [QName]
conProj   = Maybe [QName]
forall a. Maybe a
Nothing
                    , conForced :: [IsForced]
conForced = []
                    , conErased :: Maybe [Bool]
conErased = Maybe [Bool]
forall a. Maybe a
Nothing
                    }
                }
    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 =
  ArgName
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName ArgName
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 :: Maybe (Arg Type)
conPType = 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
infA
                                    , conPLazy :: Bool
conPLazy = Bool
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" ]
          }
    QName -> Definition -> TCM ()
addConstant QName
flat (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Definition
flatDefn { defPolarity :: [Polarity]
defPolarity       = []
               , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
StrictPos]  -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
               , defCopatternLHS :: Bool
defCopatternLHS = CompiledClauses' Term -> Bool
hasProjectionPatterns CompiledClauses' Term
cc
               , theDef :: Defn
theDef = FunctionData -> Defn
FunctionDefn FunctionData
emptyFunctionData
                   { _funClauses :: [Clause]
_funClauses      = [Clause
clause]
                   , _funCompiled :: Maybe (CompiledClauses' Term)
_funCompiled     = CompiledClauses' Term -> Maybe (CompiledClauses' Term)
forall a. a -> Maybe a
Just (CompiledClauses' Term -> Maybe (CompiledClauses' Term))
-> CompiledClauses' Term -> Maybe (CompiledClauses' Term)
forall a b. (a -> b) -> a -> b
$ CompiledClauses' Term
cc
                   , _funProjection :: Either ProjectionLikenessMissing Projection
_funProjection   = Projection -> Either ProjectionLikenessMissing Projection
forall a b. b -> Either a b
Right Projection
projection
                   , _funMutual :: Maybe [QName]
_funMutual       = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
                   , _funTerminates :: Maybe Bool
_funTerminates   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
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' ConstructorData Defn -> LensMap ConstructorData Defn
forall i o. Lens' i o -> LensMap i o
over (ConstructorData -> f ConstructorData) -> Defn -> f Defn
Lens' ConstructorData Defn
lensConstructor LensMap ConstructorData Defn -> LensMap ConstructorData Defn
forall a b. (a -> b) -> a -> b
$ \ ConstructorData
def ->
      ConstructorData
def { _conSrcCon :: ConHead
_conSrcCon = ConHead
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' RecordData Defn -> LensMap RecordData Defn
forall i o. Lens' i o -> LensMap i o
over (RecordData -> f RecordData) -> Defn -> f Defn
Lens' RecordData Defn
lensRecord LensMap RecordData Defn -> LensMap RecordData Defn
forall a b. (a -> b) -> a -> b
$ \ RecordData
def ->
      RecordData
def { _recConHead :: ConHead
_recConHead = ConHead
sharpCon, _recFields :: [Dom QName]
_recFields = [QName -> Dom QName
forall e. e -> Dom e
defaultDom QName
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