module Agda.TypeChecking.Rules.LHS.Problem where
import Prelude hiding (null)
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 hiding (empty)
import Agda.Utils.Except ( Error(noMsg, strMsg) )
import Agda.Utils.Null
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
{ splitLPats :: ProblemPart
, splitAsNames :: [Name]
, splitFocus :: I.Arg Focus
, splitRPats :: Abs ProblemPart
}
|
SplitRest
{ splitProjection :: I.Arg QName
, splitRestType :: Type
}
consSplitProblem
:: A.NamedArg A.Pattern
-> ArgName
-> I.Dom Type
-> SplitProblem
-> SplitProblem
consSplitProblem p x dom s@SplitRest{} = s
consSplitProblem p x dom s@Split{ splitLPats = ps } = s{ splitLPats = consProblem' ps }
where
consProblem' (Problem ps () tel pr) =
Problem (p:ps) () (ExtendTel dom $ Abs x tel) pr
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 Null ProblemRest where
null = null . restPats
empty = ProblemRest { restPats = [], restType = defaultArg typeDontCare }
instance Null a => Null (Problem' a) where
null p = null (problemInPat p) && null (problemRest p)
empty = Problem empty empty empty empty