module Agda.TypeChecking.Rules.LHS.Problem where
import Prelude hiding (null)
import Data.Foldable ( Foldable )
import Data.Maybe ( fromMaybe )
import Data.Monoid (Monoid, mempty, mappend, mconcat)
import Data.Traversable
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.TypeChecking.Substitute.Pattern
import Agda.TypeChecking.Pretty
import Agda.Utils.Null
import Agda.Utils.Permutation
type Substitution = [Maybe Term]
type FlexibleVars = [FlexibleVar Nat]
data FlexibleVarKind
= RecordFlex [FlexibleVarKind]
| ImplicitFlex
| DotFlex
deriving (Eq, 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
data FlexChoice = ChooseLeft | ChooseRight | ChooseEither | ExpandBoth
deriving (Eq, Show)
instance Monoid FlexChoice where
mempty = ChooseEither
ExpandBoth `mappend` _ = ExpandBoth
_ `mappend` ExpandBoth = ExpandBoth
ChooseEither `mappend` y = y
x `mappend` ChooseEither = x
ChooseLeft `mappend` ChooseRight = ExpandBoth
ChooseRight `mappend` ChooseLeft = ExpandBoth
ChooseLeft `mappend` ChooseLeft = ChooseLeft
ChooseRight `mappend` ChooseRight = ChooseRight
class ChooseFlex a where
chooseFlex :: a -> a -> FlexChoice
instance ChooseFlex FlexibleVarKind where
chooseFlex DotFlex DotFlex = ChooseEither
chooseFlex DotFlex _ = ChooseLeft
chooseFlex _ DotFlex = ChooseRight
chooseFlex (RecordFlex xs) (RecordFlex ys) = chooseFlex xs ys
chooseFlex (RecordFlex xs) y = chooseFlex xs (repeat y)
chooseFlex x (RecordFlex ys) = chooseFlex (repeat x) ys
chooseFlex ImplicitFlex ImplicitFlex = ChooseEither
instance ChooseFlex a => ChooseFlex [a] where
chooseFlex xs ys = mconcat $ zipWith chooseFlex xs ys
instance ChooseFlex Hiding where
chooseFlex Hidden Hidden = ChooseEither
chooseFlex Hidden _ = ChooseLeft
chooseFlex _ Hidden = ChooseRight
chooseFlex Instance Instance = ChooseEither
chooseFlex Instance _ = ChooseLeft
chooseFlex _ Instance = ChooseRight
chooseFlex _ _ = ChooseEither
instance ChooseFlex Int where
chooseFlex x y = case compare x y of
LT -> ChooseLeft
EQ -> ChooseEither
GT -> ChooseRight
instance (ChooseFlex a) => ChooseFlex (FlexibleVar a) where
chooseFlex (FlexibleVar h1 f1 i1) (FlexibleVar h2 f2 i2) =
firstChoice [chooseFlex f1 f2, chooseFlex h1 h2, chooseFlex i1 i2]
where
firstChoice :: [FlexChoice] -> FlexChoice
firstChoice [] = ChooseEither
firstChoice (ChooseEither : xs) = firstChoice xs
firstChoice (x : _ ) = x
data Problem' p = Problem
{ problemInPat :: [NamedArg A.Pattern]
, problemOutPat :: p
, problemTel :: Telescope
, problemRest :: ProblemRest
}
deriving Show
type Problem = Problem' [NamedArg DeBruijnPattern]
type ProblemPart = Problem' ()
data ProblemRest = ProblemRest
{ restPats :: [NamedArg A.Pattern]
, restType :: Arg Type
}
deriving Show
data Focus
= Focus
{ focusCon :: QName
, focusPatOrigin:: ConPOrigin
, focusConArgs :: [NamedArg A.Pattern]
, focusRange :: Range
, focusOutPat :: [NamedArg DeBruijnPattern]
, focusDatatype :: QName
, focusParams :: [Arg Term]
, focusIndices :: [Arg Term]
, focusType :: Type
}
| LitFocus Literal [NamedArg DeBruijnPattern] Type
data SplitProblem
=
Split
{ splitLPats :: ProblemPart
, splitAsNames :: [Name]
, splitFocus :: Arg Focus
, splitRPats :: Abs ProblemPart
}
|
SplitRest
{ splitProjection :: Arg QName
, splitRestType :: Type
}
consSplitProblem
:: NamedArg A.Pattern
-> ArgName
-> 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 DotPatternInst = DPI
{ dotPatternUserExpr :: Maybe A.Expr
, dotPatternInst :: Term
, dotPatternType :: Dom Type
}
data AsBinding = AsB Name Term Type
data LHSState = LHSState
{ lhsProblem :: Problem
, lhsSubst :: PatternSubstitution
, lhsDPI :: [DotPatternInst]
, lhsAsB :: [AsBinding]
}
instance Subst Term ProblemRest where
applySubst rho p = p { restType = applySubst rho $ restType p }
instance Subst Term (Problem' p) where
applySubst rho p = p { problemTel = applySubst rho $ problemTel p
, problemRest = applySubst rho $ problemRest p }
instance Subst Term DotPatternInst where
applySubst rho (DPI e v a) = uncurry (DPI e) $ applySubst rho (v,a)
instance Subst Term AsBinding where
applySubst rho (AsB x v a) = uncurry (AsB x) $ applySubst rho (v, a)
instance PrettyTCM DotPatternInst where
prettyTCM (DPI me v a) = sep
[ prettyA e <+> text "="
, nest 2 $ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a
]
where e = fromMaybe underscore me
instance PrettyTCM AsBinding where
prettyTCM (AsB x v a) =
sep [ prettyTCM x <> text "@" <> parens (prettyTCM v)
, nest 2 $ text ":" <+> prettyTCM a
]
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