-- {-# LANGUAGE CPP #-}

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

module Agda.TypeChecking.Rules.Builtin.Coinduction where

import qualified Data.Map as Map
import qualified Data.Set as Set

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.Monad.Builtin
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.Permutation

-- | The type of @∞@.

typeOfInf :: TCM Type
typeOfInf = hPi "a" (el primLevel) $
            (return . sort $ varSort 0) --> (return . sort $ varSort 0)

-- | The type of @♯_@.

typeOfSharp :: TCM Type
typeOfSharp = hPi "a" (el primLevel) $
              hPi "A" (return . sort $ varSort 0) $
              (El (varSort 1) <$> varM 0) -->
              (El (varSort 1) <$> primInf <#> varM 1 <@> varM 0)

-- | The type of @♭@.

typeOfFlat :: TCM Type
typeOfFlat = hPi "a" (el primLevel) $
             hPi "A" (return . sort $ varSort 0) $
             (El (varSort 1) <$> primInf <#> varM 1 <@> varM 0) -->
             (El (varSort 1) <$> varM 0)

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

bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinInf x = bindPostulatedName builtinInf x $ \inf _ ->
  instantiateFull =<< checkExpr (A.Def inf) =<< typeOfInf

-- | 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 x =
  bindPostulatedName builtinSharp x $ \sharp sharpDefn -> do
    sharpType <- typeOfSharp
    TelV fieldTel _ <- telView sharpType
    sharpE    <- instantiateFull =<< checkExpr (A.Def sharp) sharpType
    Def inf _ <- primInf
    infDefn   <- getConstInfo inf
    addConstant (defName infDefn) $
      infDefn { defPolarity       = [] -- not monotone
              , defArgOccurrences = [Unused, StrictPos]
              , theDef = Record
                  { recPars           = 2
                  , recInduction      = Just CoInductive
                  , recClause         = Nothing
                  , recConHead        = ConHead sharp CoInductive []  -- flat is added later
                  , recNamedCon       = True
                  , recFields         = []  -- flat is added later
                  , recTel            = fieldTel
                  , recEtaEquality'   = Inferred NoEta
                  , recMutual         = Just []
                  , recAbstr          = ConcreteDef
                  , recComp           = emptyCompKit
                  }
              }
    addConstant sharp $
      sharpDefn { theDef = Constructor
                    { conPars   = 2
                    , conArity  = 1
                    , conSrcCon = ConHead sharp CoInductive [] -- flat is added as field later
                    , conData   = defName infDefn
                    , conAbstr  = ConcreteDef
                    , conInd    = CoInductive
                    , conComp   = (emptyCompKit, Nothing)
                    , conForced = []
                    , conErased = []
                    }
                }
    return sharpE

-- | 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 x =
  bindPostulatedName builtinFlat x $ \ flat flatDefn -> do
    flatE       <- instantiateFull =<< checkExpr (A.Def flat) =<< typeOfFlat
    Def sharp _ <- primSharp
    kit         <- requireLevels
    Def inf _   <- primInf
    let sharpCon = ConHead sharp CoInductive [defaultArg flat]
        level    = El (mkType 0) $ Def (typeName kit) []
        tel     :: Telescope
        tel      = ExtendTel (domH $ level)                  $ Abs "a" $
                   ExtendTel (domH $ sort $ varSort 0)       $ Abs "A" $
                   ExtendTel (domN $ El (varSort 1) $ var 0) $ Abs "x" $
                   EmptyTel
        infA     = El (varSort 2) $ Def inf [ Apply $ defaultArg $ var 1 ]
        cpi      = noConPatternInfo { conPType = Just $ defaultArg infA
                                    , conPLazy = True }
    let clause   = Clause
          { clauseLHSRange  = noRange
          , clauseFullRange = noRange
          , clauseTel       = tel
          , namedClausePats = [ argN $ Named Nothing $
              ConP sharpCon cpi [ argN $ Named Nothing $ debruijnNamedVar "x" 0 ] ]
          , clauseBody      = Just $ var 0
          , clauseType      = Just $ defaultArg $ El (varSort 2) $ var 1
          , clauseCatchall  = False
          , clauseUnreachable = Just False
          }
        cc = Case (defaultArg 0) $ conCase sharp False $ WithArity 1 $ Done [defaultArg "x"] $ var 0
        projection = Projection
          { projProper   = Just inf
          , projOrig     = flat
          , projFromType = defaultArg inf
          , projIndex    = 3
          , projLams     = ProjLams $ [ argH "a" , argH "A" , argN "x" ]
          }
    addConstant flat $
      flatDefn { defPolarity       = []
               , defArgOccurrences = [StrictPos]  -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
               , theDef = emptyFunction
                   { funClauses      = [clause]
                   , funCompiled     = Just $ cc
                   , funProjection   = Just projection
                   , funMutual       = Just []
                   , funTerminates   = Just True
                   , funCopatternLHS = hasProjectionPatterns cc
                   }
                }

    -- register flat as record field for constructor sharp
    modifySignature $ updateDefinition sharp $ updateTheDef $ \ def ->
      def { conSrcCon = sharpCon }
    modifySignature $ updateDefinition inf $ updateTheDef $ \ def ->
      def { recConHead = sharpCon, recFields = [defaultArg flat] }
    return flatE

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