module Agda.TypeChecking.Rules.LHS.Problem where
import Control.Monad.Error
import Data.Monoid ( Monoid(mappend,mempty) )
import Data.Foldable
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
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 = [FlexibleVar Nat]
data FlexibleVarKind
= RecordFlex
| ImplicitFlex
| DotFlex
deriving (Eq, Ord, Show)
data FlexibleVar a = FlexibleVar
{ flexHiding :: Hiding
, flexKind :: FlexibleVarKind
, flexVar :: a
} deriving (Eq, Show, Functor, Foldable, Traversable)
instance LensHiding (FlexibleVar a) where
getHiding = flexHiding
mapHiding f x = x { flexHiding = f (flexHiding x) }
defaultFlexibleVar :: a -> FlexibleVar a
defaultFlexibleVar a = FlexibleVar Hidden ImplicitFlex a
flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a
flexibleVarFromHiding h a = FlexibleVar h ImplicitFlex a
instance Ord (FlexibleVar Nat) where
(FlexibleVar h2 f2 i2) <= (FlexibleVar h1 f1 i1) =
f1 > f2 || (f1 == f2 && (hgt h1 h2 || (h1 == h2 && i1 <= i2)))
where
hgt x y | x == y = False
hgt Hidden _ = True
hgt _ Hidden = False
hgt Instance _ = True
hgt _ _ = False
data Problem' p = Problem
{ problemInPat :: [A.NamedArg A.Pattern]
, problemOutPat :: p
, problemTel :: Telescope
, problemRest :: ProblemRest
}
deriving Show
type Problem = Problem' (Permutation, [I.NamedArg Pattern])
type ProblemPart = Problem' ()
data ProblemRest = ProblemRest
{ restPats :: [A.NamedArg A.Pattern]
, restType :: I.Arg Type
}
deriving Show
data Focus
= Focus
{ focusCon :: QName
, focusImplicit :: Bool
, focusConArgs :: [A.NamedArg A.Pattern]
, focusRange :: Range
, focusOutPat :: OneHolePatterns
, focusHoleIx :: Int
, focusDatatype :: QName
, focusParams :: [I.Arg Term]
, focusIndices :: [I.Arg Term]
, focusType :: Type
}
| LitFocus Literal OneHolePatterns Int Type
data SplitProblem
= Split ProblemPart [Name] (I.Arg Focus) (Abs ProblemPart)
| SplitRest { splitProjection :: I.Arg QName, splitRestType :: Type }
data SplitError
= NothingToSplit
| SplitPanic String
data DotPatternInst = DPI A.Expr Term (I.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 [] (defaultArg 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)