{-# LANGUAGE NondecreasingIndentation #-}

{-| SplitClause and CoverResult types.

 -}

module Agda.TypeChecking.Coverage.SplitClause where

import Prelude hiding (null, (!!))  -- do not use partial functions like !!

import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans ( lift )

import Data.Foldable (for_)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal hiding (DataOrRecord(..))
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Translation.InternalToAbstract (NamedClause(..))

import Agda.TypeChecking.Names
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad

import Agda.TypeChecking.Rules.LHS (DataOrRecord(..), checkSortOfSplitVar)
import Agda.TypeChecking.Rules.LHS.Problem (allFlexVars)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.Term (unquoteTactic)

import Agda.TypeChecking.Coverage.Match
import Agda.TypeChecking.Coverage.SplitTree

import Agda.TypeChecking.Conversion (tryConversion, equalType)
import Agda.TypeChecking.Datatypes (getConForm)
import {-# SOURCE #-} Agda.TypeChecking.Empty ( checkEmptyTel, isEmptyTel, isEmptyType )
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Warnings

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.WithDefault

import Agda.Utils.Impossible


data SplitClause = SClause
  { SplitClause -> Telescope
scTel    :: Telescope
    -- ^ Type of variables in @scPats@.
  , SplitClause -> [NamedArg SplitPattern]
scPats   :: [NamedArg SplitPattern]
    -- ^ The patterns leading to the currently considered branch of
    --   the split tree.
  , SplitClause -> Substitution' SplitPattern
scSubst  :: Substitution' SplitPattern
    -- ^ Substitution from 'scTel' to old context.
    --   Only needed directly after split on variable:
    --   * To update 'scTarget'
    --   * To rename other split variables when splitting on
    --     multiple variables.
    --   @scSubst@ is not ``transitive'', i.e., does not record
    --   the substitution from the original context to 'scTel'
    --   over a series of splits.  It is freshly computed
    --   after each split by 'computeNeighborhood'; also
    --   'splitResult', which does not split on a variable,
    --   should reset it to the identity 'idS', lest it be
    --   applied to 'scTarget' again, leading to Issue 1294.
  , SplitClause -> Map CheckpointId Substitution
scCheckpoints :: Map CheckpointId Substitution
    -- ^ We need to keep track of the module parameter checkpoints for the
    -- clause for the purpose of inferring missing instance clauses.
  , SplitClause -> Maybe (Dom Type)
scTarget :: Maybe (Dom Type)
    -- ^ The type of the rhs, living in context 'scTel'.
    --   'fixTargetType' computes the new 'scTarget' by applying
    --   substitution 'scSubst'.
  }

data UnifyEquiv = UE { UnifyEquiv -> Telescope
infoTel0 :: Telescope          -- Γ0
                     , UnifyEquiv -> Telescope
infoTel :: Telescope           -- Γ'
                     , UnifyEquiv -> Telescope
infoEqTel :: Telescope         -- Γ0 ⊢ Δ
                     , UnifyEquiv -> [Term]
infoEqLHS :: [Term]            -- Γ0 ⊢ us : Δ
                     , UnifyEquiv -> [Term]
infoEqRHS :: [Term]            -- Γ0 ⊢ vs : Δ
                     , UnifyEquiv -> PatternSubstitution
infoRho :: PatternSubstitution -- Γ' ⊢ ρ : Γ0
                                                      -- Γ = Γ0,(φ : I),(eqs : Paths Δ us vs)
                                                      -- Γ' ⊢ ρ,i1,refls : Γ
                     , UnifyEquiv -> Substitution
infoTau :: Substitution        -- Γ  ⊢ τ           : Γ'
                     , UnifyEquiv -> Substitution
infoLeftInv :: Substitution    -- Γ | (i : I) ⊢ leftInv : Γ
                     -- leftInv[i=0] = ρ[τ],i1s,refls
                     -- leftInv[i=1] = idS
                     }
                  deriving Int -> UnifyEquiv -> ShowS
[UnifyEquiv] -> ShowS
UnifyEquiv -> String
(Int -> UnifyEquiv -> ShowS)
-> (UnifyEquiv -> String)
-> ([UnifyEquiv] -> ShowS)
-> Show UnifyEquiv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnifyEquiv -> ShowS
showsPrec :: Int -> UnifyEquiv -> ShowS
$cshow :: UnifyEquiv -> String
show :: UnifyEquiv -> String
$cshowList :: [UnifyEquiv] -> ShowS
showList :: [UnifyEquiv] -> ShowS
Show

data IInfo = TheInfo UnifyEquiv | NoInfo deriving Int -> IInfo -> ShowS
[IInfo] -> ShowS
IInfo -> String
(Int -> IInfo -> ShowS)
-> (IInfo -> String) -> ([IInfo] -> ShowS) -> Show IInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IInfo -> ShowS
showsPrec :: Int -> IInfo -> ShowS
$cshow :: IInfo -> String
show :: IInfo -> String
$cshowList :: [IInfo] -> ShowS
showList :: [IInfo] -> ShowS
Show

-- | A @Covering@ is the result of splitting a 'SplitClause'.
data Covering = Covering
  { Covering -> Arg Int
covSplitArg     :: Arg Nat
     -- ^ De Bruijn level (counting dot patterns) of argument we split on.
  , Covering -> [(SplitTag, (SplitClause, IInfo))]
covSplitClauses :: [(SplitTag, (SplitClause, IInfo))]
      -- ^ Covering clauses, indexed by constructor/literal these clauses share.
  }

-- | Project the split clauses out of a covering.
splitClauses :: Covering -> [SplitClause]
splitClauses :: Covering -> [SplitClause]
splitClauses (Covering Arg Int
_ [(SplitTag, (SplitClause, IInfo))]
qcs) = ((SplitTag, (SplitClause, IInfo)) -> SplitClause)
-> [(SplitTag, (SplitClause, IInfo))] -> [SplitClause]
forall a b. (a -> b) -> [a] -> [b]
map ((SplitClause, IInfo) -> SplitClause
forall a b. (a, b) -> a
fst ((SplitClause, IInfo) -> SplitClause)
-> ((SplitTag, (SplitClause, IInfo)) -> (SplitClause, IInfo))
-> (SplitTag, (SplitClause, IInfo))
-> SplitClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitTag, (SplitClause, IInfo)) -> (SplitClause, IInfo)
forall a b. (a, b) -> b
snd) [(SplitTag, (SplitClause, IInfo))]
qcs

-- | Create a split clause from a clause in internal syntax. Used by make-case.
clauseToSplitClause :: Clause -> SplitClause
clauseToSplitClause :: Clause -> SplitClause
clauseToSplitClause Clause
cl = SClause
  { scTel :: Telescope
scTel    = Clause -> Telescope
clauseTel Clause
cl
  , scPats :: [NamedArg SplitPattern]
scPats   = [NamedArg (Pattern' DBPatVar)] -> [NamedArg SplitPattern]
toSplitPatterns ([NamedArg (Pattern' DBPatVar)] -> [NamedArg SplitPattern])
-> [NamedArg (Pattern' DBPatVar)] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg (Pattern' DBPatVar)]
namedClausePats Clause
cl
  , scSubst :: Substitution' SplitPattern
scSubst  = Substitution' SplitPattern
forall a. Substitution' a
idS  -- Andreas, 2014-07-15  TODO: Is this ok?
  , scCheckpoints :: Map CheckpointId Substitution
scCheckpoints = Map CheckpointId Substitution
forall k a. Map k a
Map.empty -- #2996: not __IMPOSSIBLE__ for debug printing
  , scTarget :: Maybe (Dom Type)
scTarget = Arg Type -> Dom Type
forall a. Arg a -> Dom a
domFromArg (Arg Type -> Dom Type) -> Maybe (Arg Type) -> Maybe (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Clause -> Maybe (Arg Type)
clauseType Clause
cl
  }


---------------------------------------------
-- Record type for the results of @cover@
---------------------------------------------

data CoverResult = CoverResult
  { CoverResult -> SplitTree
coverSplitTree       :: SplitTree
  , CoverResult -> IntSet
coverUsedClauses     :: IntSet -- Set Nat
  , CoverResult -> [(Telescope, [NamedArg (Pattern' DBPatVar)])]
coverMissingClauses  :: [(Telescope, [NamedArg DeBruijnPattern])]
  , CoverResult -> [Clause]
coverPatterns        :: [Clause]
  -- ^ The set of patterns used as cover.
  , CoverResult -> IntSet
coverNoExactClauses  :: IntSet -- Set Nat
  }