module Agda.TypeChecking.Rules.LHS.Problem
( FlexibleVars , FlexibleVarKind(..) , FlexibleVar(..) , allFlexVars
, FlexChoice(..) , ChooseFlex(..)
, ProblemEq(..) , Problem(..) , problemEqs
, problemRestPats, problemCont, problemInPats
, AsBinding(..) , DotPattern(..) , AbsurdPattern(..)
, LHSState(..) , lhsTel , lhsOutPat , lhsProblem , lhsTarget
) where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Data.Foldable ( Foldable )
import Data.Maybe ( fromMaybe )
import Data.Monoid ( Monoid, mempty, mappend, mconcat )
import Data.Semigroup ( Semigroup, (<>) )
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (ProblemEq(..))
import qualified Agda.Syntax.Abstract as A
import Agda.TypeChecking.Monad (TCM)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import qualified Agda.Utils.Pretty as PP
type FlexibleVars = [FlexibleVar Nat]
data FlexibleVarKind
= RecordFlex [FlexibleVarKind]
| ImplicitFlex
| DotFlex
| OtherFlex
deriving (Eq, Show)
data FlexibleVar a = FlexibleVar
{ flexHiding :: Hiding
, flexOrigin :: Origin
, 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) }
instance LensOrigin (FlexibleVar a) where
getOrigin = flexOrigin
mapOrigin f x = x { flexOrigin = f (flexOrigin x) }
allFlexVars :: Telescope -> FlexibleVars
allFlexVars tel = zipWith makeFlex (downFrom $ size tel) $ telToList tel
where
makeFlex i d = FlexibleVar (getHiding d) (getOrigin 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
chooseFlex ImplicitFlex _ = ChooseLeft
chooseFlex _ ImplicitFlex = ChooseRight
chooseFlex OtherFlex OtherFlex = 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 Origin where
chooseFlex Inserted Inserted = ChooseEither
chooseFlex Inserted _ = ChooseLeft
chooseFlex _ Inserted = ChooseRight
chooseFlex Reflected Reflected = ChooseEither
chooseFlex Reflected _ = ChooseLeft
chooseFlex _ Reflected = 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 o1 f1 p1 i1) (FlexibleVar h2 o2 f2 p2 i2) =
firstChoice [ chooseFlex f1 f2, chooseFlex o1 o2, 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 a = Problem
{ _problemEqs :: [ProblemEq]
, _problemRestPats :: [NamedArg A.Pattern]
, _problemCont :: LHSState a -> TCM a
}
deriving Show
problemEqs :: Lens' [ProblemEq] (Problem a)
problemEqs f p = f (_problemEqs p) <&> \x -> p {_problemEqs = x}
problemRestPats :: Lens' [NamedArg A.Pattern] (Problem a)
problemRestPats f p = f (_problemRestPats p) <&> \x -> p {_problemRestPats = x}
problemCont :: Lens' (LHSState a -> TCM a) (Problem a)
problemCont f p = f (_problemCont p) <&> \x -> p {_problemCont = x}
problemInPats :: Problem a -> [A.Pattern]
problemInPats = map problemInPat . (^. problemEqs)
data AsBinding = AsB Name Term Type
data DotPattern = Dot A.Expr Term (Dom Type)
data AbsurdPattern = Absurd Range Type
data LHSState a = LHSState
{ _lhsTel :: Telescope
, _lhsOutPat :: [NamedArg DeBruijnPattern]
, _lhsProblem :: Problem a
, _lhsTarget :: Arg Type
}
lhsTel :: Lens' Telescope (LHSState a)
lhsTel f p = f (_lhsTel p) <&> \x -> p {_lhsTel = x}
lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a)
lhsOutPat f p = f (_lhsOutPat p) <&> \x -> p {_lhsOutPat = x}
lhsProblem :: Lens' (Problem a) (LHSState a)
lhsProblem f p = f (_lhsProblem p) <&> \x -> p {_lhsProblem = x}
lhsTarget :: Lens' (Arg Type) (LHSState a)
lhsTarget f p = f (_lhsTarget p) <&> \x -> p {_lhsTarget = x}
instance Subst Term (Problem a) where
applySubst rho (Problem eqs rps cont) = Problem (applySubst rho eqs) rps cont
instance Subst Term AsBinding where
applySubst rho (AsB x v a) = uncurry (AsB x) $ applySubst rho (v, a)
instance Subst Term DotPattern where
applySubst rho (Dot e v a) = uncurry (Dot e) $ applySubst rho (v, a)
instance Subst Term AbsurdPattern where
applySubst rho (Absurd r a) = Absurd r $ applySubst rho a
instance PrettyTCM ProblemEq where
prettyTCM (ProblemEq p v a) = sep
[ prettyA p <+> text "="
, nest 2 $ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a
]
instance PrettyTCM AsBinding where
prettyTCM (AsB x v a) =
sep [ prettyTCM x P.<> text "@" P.<> parens (prettyTCM v)
, nest 2 $ text ":" <+> prettyTCM a
]
instance PrettyTCM DotPattern where
prettyTCM (Dot e v a) = sep
[ prettyA e <+> text "="
, nest 2 $ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a
]
instance PrettyTCM AbsurdPattern where
prettyTCM (Absurd r a) = text "() :" <+> prettyTCM a
instance PP.Pretty AsBinding where
pretty (AsB x v a) =
PP.pretty x PP.<+> PP.text "=" 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