module Agda.TypeChecking.Rules.LHS.Problem where

import Control.Monad.Error
import Data.Monoid

import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Substitute

import Agda.Utils.Permutation

type Substitution   = [Maybe Term]
type FlexibleVars   = [Nat]

data Problem' p	    = Problem { problemInPat  :: [NamedArg A.Pattern]
			      , problemOutPat :: p
			      , problemTel    :: Telescope
			      }
data Focus	    = Focus   { focusCon      :: QName
			      , focusConArgs  :: [NamedArg A.Pattern]
			      , focusRange    :: Range
			      , focusOutPat   :: OneHolePatterns
			      , focusHoleIx   :: Int  -- ^ index of focused variable in the out patterns
			      , focusDatatype :: QName
			      , focusParams   :: [Arg Term]
			      , focusIndices  :: [Arg Term]
			      }
		    | LitFocus Literal OneHolePatterns Int Type
data SplitProblem   = Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)
                      -- ^ the [Name]s give the as-bindings for the focus

data SplitError	    = NothingToSplit
		    | SplitPanic String

type ProblemPart = Problem' ()

-- | The permutation should permute @allHoles@ of the patterns to correspond to
--   the abstract patterns in the problem.
type Problem	 = Problem' (Permutation, [Arg Pattern])

instance Error SplitError where
  noMsg  = NothingToSplit
  strMsg = SplitPanic

instance Monoid p => Monoid (Problem' p) where
  mempty = Problem [] mempty EmptyTel
  Problem ps1 qs1 tel1 `mappend` Problem ps2 qs2 tel2 =
    Problem (ps1 ++ ps2) (mappend qs1 qs2) (abstract tel1 tel2)