module Agda.TypeChecking.Rules.LHS.Problem where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Data.Foldable ( Foldable )
import Data.Maybe ( fromMaybe )
import Data.Semigroup (Semigroup, 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.Reduce
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import qualified Agda.Utils.Pretty as PP
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
, flexPos :: Maybe Int
, 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 Nothing a
flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a
flexibleVarFromHiding h a = FlexibleVar h ImplicitFlex Nothing a
allFlexVars :: Telescope -> FlexibleVars
allFlexVars tel = zipWith makeFlex (downFrom $ size tel) $ telToList tel
where
makeFlex i d = FlexibleVar (getHiding d) ImplicitFlex (Just i) i
data FlexChoice = ChooseLeft | ChooseRight | ChooseEither | ExpandBoth
deriving (Eq, Show)
instance Semigroup FlexChoice where
ExpandBoth <> _ = ExpandBoth
_ <> ExpandBoth = ExpandBoth
ChooseEither <> y = y
x <> ChooseEither = x
ChooseLeft <> ChooseRight = ExpandBoth
ChooseRight <> ChooseLeft = ExpandBoth
ChooseLeft <> ChooseLeft = ChooseLeft
ChooseRight <> ChooseRight = ChooseRight
instance Monoid FlexChoice where
mempty = ChooseEither
mappend = (<>)
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 a => ChooseFlex (Maybe a) where
chooseFlex Nothing Nothing = ChooseEither
chooseFlex Nothing (Just y) = ChooseLeft
chooseFlex (Just x) Nothing = ChooseRight
chooseFlex (Just x) (Just y) = chooseFlex x y
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 p1 i1) (FlexibleVar h2 f2 p2 i2) =
firstChoice [ chooseFlex f1 f2, chooseFlex h1 h2
, chooseFlex p1 p2, 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:: ConOrigin
, 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
, splitFocus :: Arg Focus
, splitRPats :: Abs ProblemPart
}
|
SplitRest
{ splitProjection :: Arg QName
, splitProjOrigin :: ProjOrigin
, 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
{ dotPatternName :: Maybe A.Name
, dotPatternUserExpr :: Maybe A.Expr
, dotPatternInst :: Term
, dotPatternType :: Dom Type
}
data AsBinding = AsB Name Term Type
data LHSState = LHSState
{ lhsProblem :: Problem
, lhsDPI :: [DotPatternInst]
}
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 x e v a) = uncurry (DPI x 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 mx me v a) = sep
[ x <+> text "=" <+> text "." P.<> prettyA e
, nest 2 $ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a
]
where x = maybe (text "_") prettyA mx
e = fromMaybe underscore me
instance PrettyTCM AsBinding where
prettyTCM (AsB x v a) =
sep [ prettyTCM x P.<> text "@" P.<> parens (prettyTCM v)
, nest 2 $ text ":" <+> prettyTCM a
]
instance PP.Pretty AsBinding where
pretty (AsB x v a) =
PP.text (show x ++ " =") PP.<+> PP.hang (PP.pretty v PP.<+> PP.text ":") 2
(PP.pretty a)
instance InstantiateFull AsBinding where
instantiateFull' (AsB x v a) = AsB x <$> instantiateFull' v <*> instantiateFull' 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