{-| SplitClause and CoverResult types.
 -}

module Mikan.TypeChecking.Coverage.SplitClause where

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

import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.IntSet (IntSet)
import Data.IntSet qualified as IntSet

import Mikan.Syntax.Common hiding (DataOrRecord)
import Mikan.Syntax.Common.Pretty (Pretty, pretty, prettyShow)
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Internal

import Mikan.TypeChecking.Coverage.Match
import Mikan.TypeChecking.Coverage.SplitPattern
import Mikan.TypeChecking.Coverage.SplitTree
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Telescope.Path
import Mikan.TypeChecking.MetaVars
import Mikan.TypeChecking.Warnings

import Mikan.Interaction.Options

import Mikan.Utils.Either
import Mikan.Utils.Functor
import Mikan.Utils.List
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Permutation
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.Utils.WithDefault

import Mikan.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'.
  }
  deriving Int -> SplitClause -> ShowS
[SplitClause] -> ShowS
SplitClause -> String
(Int -> SplitClause -> ShowS)
-> (SplitClause -> String)
-> ([SplitClause] -> ShowS)
-> Show SplitClause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SplitClause -> ShowS
showsPrec :: Int -> SplitClause -> ShowS
$cshow :: SplitClause -> String
show :: SplitClause -> String
$cshowList :: [SplitClause] -> ShowS
showList :: [SplitClause] -> ShowS
Show

instance Pretty SplitClause where
  pretty :: SplitClause -> Doc
pretty (SClause Telescope
tel [NamedArg SplitPattern]
ps Substitution' SplitPattern
_rho Map CheckpointId Substitution
_cps Maybe (Dom Type)
mt) =
    [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat
      [ Doc
"SplitClause"
      , String -> Doc
forall a. String -> Doc a
P.text String
"tel =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Telescope -> Doc
forall a. Pretty a => a -> Doc
P.pretty Telescope
tel
      , String -> Doc
forall a. String -> Doc a
P.text String
"ps  =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> [NamedArg SplitPattern] -> Doc
forall a. Pretty a => a -> Doc
P.pretty [NamedArg SplitPattern]
ps
      , String -> Doc
forall a. String -> Doc a
P.text String
"mt  =" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Maybe (Dom Type) -> Doc
forall a. Pretty a => a -> Doc
P.pretty Maybe (Dom Type)
mt
      ]

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 t. Arg a -> Dom' t 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
  }