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
, focusDatatype :: QName
, focusParams :: [Arg Term]
, focusIndices :: [Arg Term]
, focusType :: Type
}
| LitFocus Literal OneHolePatterns Int Type
data SplitProblem = Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)
data SplitError = NothingToSplit
| SplitPanic String
type ProblemPart = Problem' ()
instance Raise (Problem' p) where
raiseFrom m k p = p { problemTel = raiseFrom m k $ problemTel p }
renameFrom m k p = p { problemTel = renameFrom m k $ problemTel p }
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)