module Agda.TypeChecking.Rules.LHS.Problem where
import Control.Monad.Error
import Data.Monoid ( Monoid(mappend,mempty) )
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 as S
import Agda.TypeChecking.Pretty
import Agda.Utils.Permutation
type Substitution = [Maybe Term]
type FlexibleVars = [Nat]
data Problem' p = Problem { problemInPat :: [NamedArg A.Pattern]
, problemOutPat :: p
, problemTel :: Telescope
, problemRest :: ProblemRest
}
data ProblemRest = ProblemRest
{ restPats :: [NamedArg A.Pattern]
, restType :: Type
}
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 Problem = Problem' (Permutation, [Arg Pattern])
type ProblemPart = Problem' ()
data DotPatternInst = DPI A.Expr Term (Dom Type)
data AsBinding = AsB Name Term Type
data LHSState = LHSState
{ lhsProblem :: Problem
, lhsSubst :: S.Substitution
, lhsDPI :: [DotPatternInst]
, lhsAsB :: [AsBinding]
}
instance Subst ProblemRest where
applySubst rho p = p { restType = applySubst rho $ restType p }
instance Subst (Problem' p) where
applySubst rho p = p { problemTel = applySubst rho $ problemTel p
, problemRest = applySubst rho $ problemRest p }
instance Subst DotPatternInst where
applySubst rho (DPI e v a) = uncurry (DPI e) $ applySubst rho (v,a)
instance Subst AsBinding where
applySubst rho (AsB x v a) = uncurry (AsB x) $ applySubst rho (v, a)
instance PrettyTCM DotPatternInst where
prettyTCM (DPI e v a) = sep
[ prettyA e <+> text "="
, nest 2 $ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a
]
instance PrettyTCM AsBinding where
prettyTCM (AsB x v a) =
sep [ prettyTCM x <> text "@" <> parens (prettyTCM v)
, nest 2 $ text ":" <+> prettyTCM a
]
instance Error SplitError where
noMsg = NothingToSplit
strMsg = SplitPanic
instance Monoid ProblemRest where
mempty = ProblemRest [] typeDontCare
mappend pr (ProblemRest [] _) = pr
mappend _ pr = pr
instance Monoid p => Monoid (Problem' p) where
mempty = Problem [] mempty EmptyTel mempty
Problem ps1 qs1 tel1 pr1 `mappend` Problem ps2 qs2 tel2 pr2 =
Problem (ps1 ++ ps2) (mappend qs1 qs2) (abstract tel1 tel2) (mappend pr1 pr2)