content: {-| SplitClause and CoverResult types.
   -}
  
  module Agda.TypeChecking.Coverage.SplitClause where
  
  import Prelude hiding (null, (!!))  -- do not use partial functions like !!
  
  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.Common.Pretty (prettyShow)
  import Agda.Syntax.Internal hiding (DataOrRecord)
  
  import Agda.TypeChecking.Coverage.Match
  import Agda.TypeChecking.Coverage.SplitTree
  import Agda.TypeChecking.Monad
  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.Singleton
  import Agda.Utils.Size
  import Agda.Utils.WithDefault
  
  import Agda.Utils.Impossible
  
  
  data SplitClause = SClause
    { scTel    :: Telescope
      -- ^ Type of variables in @scPats@.
    , scPats   :: [NamedArg SplitPattern]
      -- ^ The patterns leading to the currently considered branch of
      --   the split tree.
    , 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.
    , 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.
    , 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 { infoTel0 :: Telescope          -- Γ0
                       , infoTel :: Telescope           -- Γ'
                       , infoEqTel :: Telescope         -- Γ0 ⊢ Δ
                       , infoEqLHS :: [Term]            -- Γ0 ⊢ us : Δ
                       , infoEqRHS :: [Term]            -- Γ0 ⊢ vs : Δ
                       , infoRho :: PatternSubstitution -- Γ' ⊢ ρ : Γ0
                                                        -- Γ = Γ0,(φ : I),(eqs : Paths Δ us vs)
                                                        -- Γ' ⊢ ρ,i1,refls : Γ
                       , infoTau :: Substitution        -- Γ  ⊢ τ           : Γ'
                       , infoLeftInv :: Substitution    -- Γ | (i : I) ⊢ leftInv : Γ
                       -- leftInv[i=0] = ρ[τ],i1s,refls
                       -- leftInv[i=1] = idS
                       }
                    deriving Show
  
  data IInfo = TheInfo UnifyEquiv | NoInfo deriving Show
  
  -- | A @Covering@ is the result of splitting a 'SplitClause'.
  data Covering = Covering
    { covSplitArg     :: Arg Nat
       -- ^ De Bruijn level (counting dot patterns) of argument we split on.
    , 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 _ qcs) = map (fst . snd) qcs
  
  -- | Create a split clause from a clause in internal syntax. Used by make-case.
  clauseToSplitClause :: Clause -> SplitClause
  clauseToSplitClause cl = SClause
    { scTel    = clauseTel cl
    , scPats   = toSplitPatterns $ namedClausePats cl
    , scSubst  = idS  -- Andreas, 2014-07-15  TODO: Is this ok?
    , scCheckpoints = Map.empty -- #2996: not __IMPOSSIBLE__ for debug printing
    , scTarget = domFromArg <$> clauseType cl
    }
  
  
  ---------------------------------------------
  -- Record type for the results of @cover@
  ---------------------------------------------
  
  data CoverResult = CoverResult
    { coverSplitTree       :: SplitTree
    , coverUsedClauses     :: IntSet -- Set Nat
    , coverMissingClauses  :: [(Telescope, [NamedArg DeBruijnPattern])]
    , coverPatterns        :: [Clause]
    -- ^ The set of patterns used as cover.
    , coverNoExactClauses  :: IntSet -- Set Nat
    }
  