module Agda.TypeChecking.Rules.LHS.Problem
       ( FlexibleVars , FlexibleVarKind(..) , FlexibleVar(..) , allFlexVars
       , FlexChoice(..) , ChooseFlex(..)
       , ProblemEq(..) , Problem(..) , problemEqs
       , problemRestPats, problemCont, problemInPats
       , AsBinding(..) , DotPattern(..) , AbsurdPattern(..), AnnotationPattern(..)
       , LHSState(..) , lhsTel , lhsOutPat , lhsProblem , lhsTarget
       , LeftoverPatterns(..), getLeftoverPatterns, getUserVariableNames
       ) where

import Prelude hiding (null)

import Control.Arrow        ( (***) )
import Control.Monad        ( zipWithM )
import Control.Monad.Writer ( MonadWriter(..), Writer, runWriter )

import Data.Functor (($>))
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.List ( partition )
import Data.Semigroup ( Semigroup, (<>) )
import qualified Data.Set as Set

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Abstract (ProblemEq(..))
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty

import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.Pretty as PP

type FlexibleVars   = [FlexibleVar Nat]

-- | When we encounter a flexible variable in the unifier, where did it come from?
--   The alternatives are ordered such that we will assign the higher one first,
--   i.e., first we try to assign a @DotFlex@, then...
data FlexibleVarKind
  = RecordFlex [FlexibleVarKind]
      -- ^ From a record pattern ('ConP').
      --   Saves the 'FlexibleVarKind' of its subpatterns.
  | ImplicitFlex -- ^ From a hidden formal argument or underscore ('WildP').
  | DotFlex      -- ^ From a dot pattern ('DotP').
  | OtherFlex    -- ^ From a non-record constructor or literal ('ConP' or 'LitP').
  deriving (FlexibleVarKind -> FlexibleVarKind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FlexibleVarKind -> FlexibleVarKind -> Bool
$c/= :: FlexibleVarKind -> FlexibleVarKind -> Bool
== :: FlexibleVarKind -> FlexibleVarKind -> Bool
$c== :: FlexibleVarKind -> FlexibleVarKind -> Bool
Eq, Int -> FlexibleVarKind -> ShowS
[FlexibleVarKind] -> ShowS
FlexibleVarKind -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [FlexibleVarKind] -> ShowS
$cshowList :: [FlexibleVarKind] -> ShowS
show :: FlexibleVarKind -> ArgName
$cshow :: FlexibleVarKind -> ArgName
showsPrec :: Int -> FlexibleVarKind -> ShowS
$cshowsPrec :: Int -> FlexibleVarKind -> ShowS
Show)

-- | Flexible variables are equipped with information where they come from,
--   in order to make a choice which one to assign when two flexibles are unified.
data FlexibleVar a = FlexibleVar
  { forall a. FlexibleVar a -> ArgInfo
flexArgInfo :: ArgInfo
  , forall a. FlexibleVar a -> IsForced
flexForced  :: IsForced
  , forall a. FlexibleVar a -> FlexibleVarKind
flexKind    :: FlexibleVarKind
  , forall a. FlexibleVar a -> Maybe Int
flexPos     :: Maybe Int
  , forall a. FlexibleVar a -> a
flexVar     :: a
  } deriving (FlexibleVar a -> FlexibleVar a -> Bool
forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FlexibleVar a -> FlexibleVar a -> Bool
$c/= :: forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
== :: FlexibleVar a -> FlexibleVar a -> Bool
$c== :: forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
Eq, Int -> FlexibleVar a -> ShowS
forall a. Show a => Int -> FlexibleVar a -> ShowS
forall a. Show a => [FlexibleVar a] -> ShowS
forall a. Show a => FlexibleVar a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [FlexibleVar a] -> ShowS
$cshowList :: forall a. Show a => [FlexibleVar a] -> ShowS
show :: FlexibleVar a -> ArgName
$cshow :: forall a. Show a => FlexibleVar a -> ArgName
showsPrec :: Int -> FlexibleVar a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FlexibleVar a -> ShowS
Show, forall a b. a -> FlexibleVar b -> FlexibleVar a
forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
$c<$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
fmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
$cfmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
Functor, forall a. Eq a => a -> FlexibleVar a -> Bool
forall a. Num a => FlexibleVar a -> a
forall a. Ord a => FlexibleVar a -> a
forall m. Monoid m => FlexibleVar m -> m
forall a. FlexibleVar a -> Bool
forall a. FlexibleVar a -> Int
forall a. FlexibleVar a -> [a]
forall a. (a -> a -> a) -> FlexibleVar a -> a
forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => FlexibleVar a -> a
$cproduct :: forall a. Num a => FlexibleVar a -> a
sum :: forall a. Num a => FlexibleVar a -> a
$csum :: forall a. Num a => FlexibleVar a -> a
minimum :: forall a. Ord a => FlexibleVar a -> a
$cminimum :: forall a. Ord a => FlexibleVar a -> a
maximum :: forall a. Ord a => FlexibleVar a -> a
$cmaximum :: forall a. Ord a => FlexibleVar a -> a
elem :: forall a. Eq a => a -> FlexibleVar a -> Bool
$celem :: forall a. Eq a => a -> FlexibleVar a -> Bool
length :: forall a. FlexibleVar a -> Int
$clength :: forall a. FlexibleVar a -> Int
null :: forall a. FlexibleVar a -> Bool
$cnull :: forall a. FlexibleVar a -> Bool
toList :: forall a. FlexibleVar a -> [a]
$ctoList :: forall a. FlexibleVar a -> [a]
foldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
foldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
fold :: forall m. Monoid m => FlexibleVar m -> m
$cfold :: forall m. Monoid m => FlexibleVar m -> m
Foldable, Functor FlexibleVar
Foldable FlexibleVar
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
FlexibleVar (m a) -> m (FlexibleVar a)
forall (f :: * -> *) a.
Applicative f =>
FlexibleVar (f a) -> f (FlexibleVar a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
sequence :: forall (m :: * -> *) a.
Monad m =>
FlexibleVar (m a) -> m (FlexibleVar a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FlexibleVar (m a) -> m (FlexibleVar a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FlexibleVar (f a) -> f (FlexibleVar a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FlexibleVar (f a) -> f (FlexibleVar a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
Traversable)

instance LensArgInfo (FlexibleVar a) where
  getArgInfo :: FlexibleVar a -> ArgInfo
getArgInfo = forall a. FlexibleVar a -> ArgInfo
flexArgInfo
  setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a
setArgInfo ArgInfo
ai FlexibleVar a
fl = FlexibleVar a
fl { flexArgInfo :: ArgInfo
flexArgInfo = ArgInfo
ai }
  mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a
mapArgInfo ArgInfo -> ArgInfo
f  FlexibleVar a
fl = FlexibleVar a
fl { flexArgInfo :: ArgInfo
flexArgInfo = ArgInfo -> ArgInfo
f (forall a. FlexibleVar a -> ArgInfo
flexArgInfo FlexibleVar a
fl) }

instance LensHiding (FlexibleVar a)
instance LensOrigin (FlexibleVar a)
instance LensModality (FlexibleVar a)

-- UNUSED
-- defaultFlexibleVar :: a -> FlexibleVar a
-- defaultFlexibleVar a = FlexibleVar Hidden Inserted ImplicitFlex Nothing a

-- UNUSED
-- flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a
-- flexibleVarFromHiding h a = FlexibleVar h ImplicitFlex Nothing a

allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
forced Telescope
tel = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 forall {a}.
LensArgInfo a =>
Int -> a -> IsForced -> FlexibleVar Int
makeFlex (forall a. Integral a => a -> [a]
downFrom Int
n) (forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel) [IsForced]
fs
  where
    n :: Int
n  = forall a. Sized a => a -> Int
size Telescope
tel
    fs :: [IsForced]
fs = [IsForced]
forced forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat IsForced
NotForced
    makeFlex :: Int -> a -> IsForced -> FlexibleVar Int
makeFlex Int
i a
d IsForced
f = forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo a
d) IsForced
f FlexibleVarKind
ImplicitFlex (forall a. a -> Maybe a
Just Int
i) Int
i

data FlexChoice = ChooseLeft | ChooseRight | ChooseEither | ExpandBoth
  deriving (FlexChoice -> FlexChoice -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FlexChoice -> FlexChoice -> Bool
$c/= :: FlexChoice -> FlexChoice -> Bool
== :: FlexChoice -> FlexChoice -> Bool
$c== :: FlexChoice -> FlexChoice -> Bool
Eq, Int -> FlexChoice -> ShowS
[FlexChoice] -> ShowS
FlexChoice -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [FlexChoice] -> ShowS
$cshowList :: [FlexChoice] -> ShowS
show :: FlexChoice -> ArgName
$cshow :: FlexChoice -> ArgName
showsPrec :: Int -> FlexChoice -> ShowS
$cshowsPrec :: Int -> FlexChoice -> ShowS
Show)

instance Semigroup FlexChoice where
  FlexChoice
ExpandBoth   <> :: FlexChoice -> FlexChoice -> FlexChoice
<> FlexChoice
_            = FlexChoice
ExpandBoth
  FlexChoice
_            <> FlexChoice
ExpandBoth   = FlexChoice
ExpandBoth
  FlexChoice
ChooseEither <> FlexChoice
y            = FlexChoice
y
  FlexChoice
x            <> FlexChoice
ChooseEither = FlexChoice
x
  FlexChoice
ChooseLeft   <> FlexChoice
ChooseRight  = FlexChoice
ExpandBoth -- If there's dot patterns on both sides,
  FlexChoice
ChooseRight  <> FlexChoice
ChooseLeft   = FlexChoice
ExpandBoth -- we need to eta-expand
  FlexChoice
ChooseLeft   <> FlexChoice
ChooseLeft   = FlexChoice
ChooseLeft
  FlexChoice
ChooseRight  <> FlexChoice
ChooseRight  = FlexChoice
ChooseRight

instance Monoid FlexChoice where
  mempty :: FlexChoice
mempty  = FlexChoice
ChooseEither
  mappend :: FlexChoice -> FlexChoice -> FlexChoice
mappend = forall a. Semigroup a => a -> a -> a
(<>)

class ChooseFlex a where
  chooseFlex :: a -> a -> FlexChoice

instance ChooseFlex FlexibleVarKind where
  chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice
chooseFlex FlexibleVarKind
DotFlex         FlexibleVarKind
DotFlex         = FlexChoice
ChooseEither
  chooseFlex FlexibleVarKind
DotFlex         FlexibleVarKind
_               = FlexChoice
ChooseLeft
  chooseFlex FlexibleVarKind
_               FlexibleVarKind
DotFlex         = FlexChoice
ChooseRight
  chooseFlex (RecordFlex [FlexibleVarKind]
xs) (RecordFlex [FlexibleVarKind]
ys) = forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex [FlexibleVarKind]
xs [FlexibleVarKind]
ys
  chooseFlex (RecordFlex [FlexibleVarKind]
xs) FlexibleVarKind
y               = forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex [FlexibleVarKind]
xs (forall a. a -> [a]
repeat FlexibleVarKind
y)
  chooseFlex FlexibleVarKind
x               (RecordFlex [FlexibleVarKind]
ys) = forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex (forall a. a -> [a]
repeat FlexibleVarKind
x) [FlexibleVarKind]
ys
  chooseFlex FlexibleVarKind
ImplicitFlex    FlexibleVarKind
ImplicitFlex    = FlexChoice
ChooseEither
  chooseFlex FlexibleVarKind
ImplicitFlex    FlexibleVarKind
_               = FlexChoice
ChooseLeft
  chooseFlex FlexibleVarKind
_               FlexibleVarKind
ImplicitFlex    = FlexChoice
ChooseRight
  chooseFlex FlexibleVarKind
OtherFlex       FlexibleVarKind
OtherFlex       = FlexChoice
ChooseEither

instance ChooseFlex a => ChooseFlex [a] where
  chooseFlex :: [a] -> [a] -> FlexChoice
chooseFlex [a]
xs [a]
ys = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex [a]
xs [a]
ys

instance ChooseFlex a => ChooseFlex (Maybe a) where
  chooseFlex :: Maybe a -> Maybe a -> FlexChoice
chooseFlex Maybe a
Nothing Maybe a
Nothing = FlexChoice
ChooseEither
  chooseFlex Maybe a
Nothing (Just a
y) = FlexChoice
ChooseLeft
  chooseFlex (Just a
x) Maybe a
Nothing = FlexChoice
ChooseRight
  chooseFlex (Just a
x) (Just a
y) = forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex a
x a
y

instance ChooseFlex ArgInfo where
  chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice
chooseFlex ArgInfo
ai1 ArgInfo
ai2 = [FlexChoice] -> FlexChoice
firstChoice [ forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex (forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai1) (forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai2)
                                   , forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai1) (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai2) ]

instance ChooseFlex IsForced where
  chooseFlex :: IsForced -> IsForced -> FlexChoice
chooseFlex IsForced
NotForced IsForced
NotForced = FlexChoice
ChooseEither
  chooseFlex IsForced
NotForced IsForced
Forced    = FlexChoice
ChooseRight
  chooseFlex IsForced
Forced    IsForced
NotForced = FlexChoice
ChooseLeft
  chooseFlex IsForced
Forced    IsForced
Forced    = FlexChoice
ChooseEither

instance ChooseFlex Hiding where
  chooseFlex :: Hiding -> Hiding -> FlexChoice
chooseFlex Hiding
Hidden     Hiding
Hidden     = FlexChoice
ChooseEither
  chooseFlex Hiding
Hidden     Hiding
_          = FlexChoice
ChooseLeft
  chooseFlex Hiding
_          Hiding
Hidden     = FlexChoice
ChooseRight
  chooseFlex Instance{} Instance{} = FlexChoice
ChooseEither
  chooseFlex Instance{} Hiding
_          = FlexChoice
ChooseLeft
  chooseFlex Hiding
_          Instance{} = FlexChoice
ChooseRight
  chooseFlex Hiding
_          Hiding
_          = FlexChoice
ChooseEither

instance ChooseFlex Origin where
  chooseFlex :: Origin -> Origin -> FlexChoice
chooseFlex Origin
Inserted  Origin
Inserted  = FlexChoice
ChooseEither
  chooseFlex Origin
Inserted  Origin
_         = FlexChoice
ChooseLeft
  chooseFlex Origin
_         Origin
Inserted  = FlexChoice
ChooseRight
  chooseFlex Origin
Reflected Origin
Reflected = FlexChoice
ChooseEither
  chooseFlex Origin
Reflected Origin
_         = FlexChoice
ChooseLeft
  chooseFlex Origin
_         Origin
Reflected = FlexChoice
ChooseRight
  chooseFlex Origin
_         Origin
_         = FlexChoice
ChooseEither

instance ChooseFlex Int where
  chooseFlex :: Int -> Int -> FlexChoice
chooseFlex Int
x Int
y = case forall a. Ord a => a -> a -> Ordering
compare Int
x Int
y of
    Ordering
LT -> FlexChoice
ChooseLeft
    Ordering
EQ -> FlexChoice
ChooseEither
    Ordering
GT -> FlexChoice
ChooseRight

instance (ChooseFlex a) => ChooseFlex (FlexibleVar a) where
  chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice
chooseFlex (FlexibleVar ArgInfo
ai1 IsForced
fc1 FlexibleVarKind
f1 Maybe Int
p1 a
i1) (FlexibleVar ArgInfo
ai2 IsForced
fc2 FlexibleVarKind
f2 Maybe Int
p2 a
i2) =
    [FlexChoice] -> FlexChoice
firstChoice [ forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex FlexibleVarKind
f1 FlexibleVarKind
f2, forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex IsForced
fc1 IsForced
fc2, forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex ArgInfo
ai1 ArgInfo
ai2
                , forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex Maybe Int
p1 Maybe Int
p2, forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex a
i1 a
i2]

firstChoice :: [FlexChoice] -> FlexChoice
firstChoice :: [FlexChoice] -> FlexChoice
firstChoice []                  = FlexChoice
ChooseEither
firstChoice (FlexChoice
ChooseEither : [FlexChoice]
xs) = [FlexChoice] -> FlexChoice
firstChoice [FlexChoice]
xs
firstChoice (FlexChoice
x            : [FlexChoice]
_ ) = FlexChoice
x

-- | The user patterns we still have to split on.
data Problem a = Problem
  { forall a. Problem a -> [ProblemEq]
_problemEqs      :: [ProblemEq]
    -- ^ User patterns which are typed
    --   (including the ones generated from implicit arguments).
  , forall a. Problem a -> [NamedArg Pattern]
_problemRestPats :: [NamedArg A.Pattern]
    -- ^ List of user patterns which could not yet be typed.
    --   Example:
    --   @
    --      f : (b : Bool) -> if b then Nat else Nat -> Nat
    --      f true          = zero
    --      f false zero    = zero
    --      f false (suc n) = n
    --   @
    --   In this sitation, for clause 2, we construct an initial problem
    --   @
    --      problemEqs      = [false = b]
    --      problemRestPats = [zero]
    --   @
    --   As we instantiate @b@ to @false@, the 'targetType' reduces to
    --   @Nat -> Nat@ and we can move pattern @zero@ over to @problemEqs@.
  , forall a. Problem a -> LHSState a -> TCM a
_problemCont     :: LHSState a -> TCM a
    -- ^ The code that checks the RHS.
  }
  deriving Int -> Problem a -> ShowS
forall a. Int -> Problem a -> ShowS
forall a. [Problem a] -> ShowS
forall a. Problem a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Problem a] -> ShowS
$cshowList :: forall a. [Problem a] -> ShowS
show :: Problem a -> ArgName
$cshow :: forall a. Problem a -> ArgName
showsPrec :: Int -> Problem a -> ShowS
$cshowsPrec :: forall a. Int -> Problem a -> ShowS
Show

problemEqs :: Lens' [ProblemEq] (Problem a)
problemEqs :: forall a. Lens' [ProblemEq] (Problem a)
problemEqs [ProblemEq] -> f [ProblemEq]
f Problem a
p = [ProblemEq] -> f [ProblemEq]
f (forall a. Problem a -> [ProblemEq]
_problemEqs Problem a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \[ProblemEq]
x -> Problem a
p {_problemEqs :: [ProblemEq]
_problemEqs = [ProblemEq]
x}

problemRestPats :: Lens' [NamedArg A.Pattern] (Problem a)
problemRestPats :: forall a. Lens' [NamedArg Pattern] (Problem a)
problemRestPats [NamedArg Pattern] -> f [NamedArg Pattern]
f Problem a
p = [NamedArg Pattern] -> f [NamedArg Pattern]
f (forall a. Problem a -> [NamedArg Pattern]
_problemRestPats Problem a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \[NamedArg Pattern]
x -> Problem a
p {_problemRestPats :: [NamedArg Pattern]
_problemRestPats = [NamedArg Pattern]
x}

problemCont :: Lens' (LHSState a -> TCM a) (Problem a)
problemCont :: forall a. Lens' (LHSState a -> TCM a) (Problem a)
problemCont (LHSState a -> TCM a) -> f (LHSState a -> TCM a)
f Problem a
p = (LHSState a -> TCM a) -> f (LHSState a -> TCM a)
f (forall a. Problem a -> LHSState a -> TCM a
_problemCont Problem a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \LHSState a -> TCM a
x -> Problem a
p {_problemCont :: LHSState a -> TCM a
_problemCont = LHSState a -> TCM a
x}

problemInPats :: Problem a -> [A.Pattern]
problemInPats :: forall a. Problem a -> [Pattern]
problemInPats = forall a b. (a -> b) -> [a] -> [b]
map ProblemEq -> Pattern
problemInPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall o i. o -> Lens' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
problemEqs)

data AsBinding = AsB Name Term Type Modality
data DotPattern = Dot A.Expr Term (Dom Type)
data AbsurdPattern = Absurd Range Type
data AnnotationPattern = Ann A.Expr Type

-- | State worked on during the main loop of checking a lhs.
--   [Ulf Norell's PhD, page. 35]
data LHSState a = LHSState
  { forall a. LHSState a -> Telescope
_lhsTel     :: Telescope
    -- ^ The types of the pattern variables.
  , forall a. LHSState a -> [NamedArg DeBruijnPattern]
_lhsOutPat  :: [NamedArg DeBruijnPattern]
    -- ^ Patterns after splitting.
    --   The de Bruijn indices refer to positions in the list of abstract syntax
    --   patterns in the problem, counted from the back (right-to-left).
  , forall a. LHSState a -> Problem a
_lhsProblem :: Problem a
    -- ^ User patterns of supposed type @delta@.
  , forall a. LHSState a -> Arg Type
_lhsTarget  :: Arg Type
    -- ^ Type eliminated by 'problemRestPats' in the problem.
    --   Can be 'Irrelevant' to indicate that we came by
    --   an irrelevant projection and, hence, the rhs must
    --   be type-checked in irrelevant mode.
  , forall a. LHSState a -> [Maybe Int]
_lhsPartialSplit :: ![Maybe Int]
    -- ^ have we splitted with a PartialFocus?
  , forall a. LHSState a -> Bool
_lhsIndexedSplit :: !Bool
    -- ^ Have we split on any indexed inductive types?
  }

lhsTel :: Lens' Telescope (LHSState a)
lhsTel :: forall a. Lens' Telescope (LHSState a)
lhsTel Telescope -> f Telescope
f LHSState a
p = Telescope -> f Telescope
f (forall a. LHSState a -> Telescope
_lhsTel LHSState a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \Telescope
x -> LHSState a
p {_lhsTel :: Telescope
_lhsTel = Telescope
x}

lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a)
lhsOutPat :: forall a. Lens' [NamedArg DeBruijnPattern] (LHSState a)
lhsOutPat [NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]
f LHSState a
p = [NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]
f (forall a. LHSState a -> [NamedArg DeBruijnPattern]
_lhsOutPat LHSState a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \[NamedArg DeBruijnPattern]
x -> LHSState a
p {_lhsOutPat :: [NamedArg DeBruijnPattern]
_lhsOutPat = [NamedArg DeBruijnPattern]
x}

lhsProblem :: Lens' (Problem a) (LHSState a)
lhsProblem :: forall a. Lens' (Problem a) (LHSState a)
lhsProblem Problem a -> f (Problem a)
f LHSState a
p = Problem a -> f (Problem a)
f (forall a. LHSState a -> Problem a
_lhsProblem LHSState a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \Problem a
x -> LHSState a
p {_lhsProblem :: Problem a
_lhsProblem = Problem a
x}

lhsTarget :: Lens' (Arg Type) (LHSState a)
lhsTarget :: forall a. Lens' (Arg Type) (LHSState a)
lhsTarget Arg Type -> f (Arg Type)
f LHSState a
p = Arg Type -> f (Arg Type)
f (forall a. LHSState a -> Arg Type
_lhsTarget LHSState a
p) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \Arg Type
x -> LHSState a
p {_lhsTarget :: Arg Type
_lhsTarget = Arg Type
x}

-- UNUSED Liang-Ting Chen 2019-07-16
--lhsPartialSplit :: Lens' [Maybe Int] (LHSState a)
--lhsPartialSplit f p = f (_lhsPartialSplit p) <&> \x -> p {_lhsPartialSplit = x}

data PatVarPosition = PVLocal | PVParam
  deriving (Int -> PatVarPosition -> ShowS
[PatVarPosition] -> ShowS
PatVarPosition -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [PatVarPosition] -> ShowS
$cshowList :: [PatVarPosition] -> ShowS
show :: PatVarPosition -> ArgName
$cshow :: PatVarPosition -> ArgName
showsPrec :: Int -> PatVarPosition -> ShowS
$cshowsPrec :: Int -> PatVarPosition -> ShowS
Show, PatVarPosition -> PatVarPosition -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatVarPosition -> PatVarPosition -> Bool
$c/= :: PatVarPosition -> PatVarPosition -> Bool
== :: PatVarPosition -> PatVarPosition -> Bool
$c== :: PatVarPosition -> PatVarPosition -> Bool
Eq)

data LeftoverPatterns = LeftoverPatterns
  { LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables :: IntMap [(A.Name,PatVarPosition)]
  , LeftoverPatterns -> [AsBinding]
asPatterns       :: [AsBinding]
  , LeftoverPatterns -> [DotPattern]
dotPatterns      :: [DotPattern]
  , LeftoverPatterns -> [AbsurdPattern]
absurdPatterns   :: [AbsurdPattern]
  , LeftoverPatterns -> [AnnotationPattern]
typeAnnotations  :: [AnnotationPattern]
  , LeftoverPatterns -> [Pattern]
otherPatterns    :: [A.Pattern]
  }

instance Semigroup LeftoverPatterns where
  LeftoverPatterns
x <> :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
<> LeftoverPatterns
y = LeftoverPatterns
    { patternVariables :: IntMap [(Name, PatVarPosition)]
patternVariables = forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. [a] -> [a] -> [a]
(++) (LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables LeftoverPatterns
x) (LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables LeftoverPatterns
y)
    , asPatterns :: [AsBinding]
asPatterns       = LeftoverPatterns -> [AsBinding]
asPatterns LeftoverPatterns
x forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [AsBinding]
asPatterns LeftoverPatterns
y
    , dotPatterns :: [DotPattern]
dotPatterns      = LeftoverPatterns -> [DotPattern]
dotPatterns LeftoverPatterns
x forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [DotPattern]
dotPatterns LeftoverPatterns
y
    , absurdPatterns :: [AbsurdPattern]
absurdPatterns   = LeftoverPatterns -> [AbsurdPattern]
absurdPatterns LeftoverPatterns
x forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [AbsurdPattern]
absurdPatterns LeftoverPatterns
y
    , typeAnnotations :: [AnnotationPattern]
typeAnnotations  = LeftoverPatterns -> [AnnotationPattern]
typeAnnotations LeftoverPatterns
x forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [AnnotationPattern]
typeAnnotations LeftoverPatterns
y
    , otherPatterns :: [Pattern]
otherPatterns    = LeftoverPatterns -> [Pattern]
otherPatterns LeftoverPatterns
x forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [Pattern]
otherPatterns LeftoverPatterns
y
    }

instance Null LeftoverPatterns where
  empty :: LeftoverPatterns
empty = IntMap [(Name, PatVarPosition)]
-> [AsBinding]
-> [DotPattern]
-> [AbsurdPattern]
-> [AnnotationPattern]
-> [Pattern]
-> LeftoverPatterns
LeftoverPatterns forall a. Null a => a
empty [] [] [] [] []
  null :: LeftoverPatterns -> Bool
null (LeftoverPatterns IntMap [(Name, PatVarPosition)]
as [AsBinding]
bs [DotPattern]
cs [AbsurdPattern]
ds [AnnotationPattern]
es [Pattern]
fs) = forall a. Null a => a -> Bool
null IntMap [(Name, PatVarPosition)]
as Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null [AsBinding]
bs Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null [DotPattern]
cs Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null [AbsurdPattern]
ds Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null [AnnotationPattern]
es Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null [Pattern]
fs


instance Monoid LeftoverPatterns where
  mempty :: LeftoverPatterns
mempty  = forall a. Null a => a
empty
  mappend :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance PP.Pretty PatVarPosition where
  pretty :: PatVarPosition -> Doc
pretty = ArgName -> Doc
PP.text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show

instance PrettyTCM LeftoverPatterns where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => LeftoverPatterns -> m Doc
prettyTCM (LeftoverPatterns IntMap [(Name, PatVarPosition)]
varp [AsBinding]
asb [DotPattern]
dotp [AbsurdPattern]
absurdp [AnnotationPattern]
annp [Pattern]
otherp) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ m Doc
"pattern variables: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap [(Name, PatVarPosition)]
varp)
    , m Doc
"as bindings:       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [AsBinding]
asb)
    , m Doc
"dot patterns:      " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [DotPattern]
dotp)
    , m Doc
"absurd patterns:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [AbsurdPattern]
absurdp)
    , m Doc
"type annotations:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [AnnotationPattern]
annp)
    , m Doc
"other patterns:    " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Pattern]
otherp)
    ]

-- | Classify remaining patterns after splitting is complete into pattern
--   variables, as patterns, dot patterns, and absurd patterns.
--   Precondition: there are no more constructor patterns.
getLeftoverPatterns
  :: forall m. PureTCM m
  => [ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns :: forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns [ProblemEq]
eqs = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.lhs.top" Int
30 forall a b. (a -> b) -> a -> b
$ TCM Doc
"classifying leftover patterns"
  Set ArgName
params <- forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [ArgName]
teleNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
  let isParamName :: Name -> Bool
isParamName = (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ArgName
params) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> ArgName
nameToArgName
  forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Name -> Bool) -> ProblemEq -> m LeftoverPatterns
getLeftoverPattern Name -> Bool
isParamName) [ProblemEq]
eqs
  where
    patternVariable :: Name -> Int -> LeftoverPatterns
patternVariable Name
x Int
i  = forall a. Null a => a
empty { patternVariables :: IntMap [(Name, PatVarPosition)]
patternVariables = forall el coll. Singleton el coll => el -> coll
singleton (Int
i,[(Name
x,PatVarPosition
PVLocal)]) }
    moduleParameter :: Name -> Int -> LeftoverPatterns
moduleParameter Name
x Int
i  = forall a. Null a => a
empty { patternVariables :: IntMap [(Name, PatVarPosition)]
patternVariables = forall el coll. Singleton el coll => el -> coll
singleton (Int
i,[(Name
x,PatVarPosition
PVParam)]) }
    asPattern :: Name -> Term -> Dom' t Type -> LeftoverPatterns
asPattern Name
x Term
v Dom' t Type
a      = forall a. Null a => a
empty { asPatterns :: [AsBinding]
asPatterns       = forall el coll. Singleton el coll => el -> coll
singleton (Name -> Term -> Type -> Modality -> AsBinding
AsB Name
x Term
v (forall t e. Dom' t e -> e
unDom Dom' t Type
a) (forall a. LensModality a => a -> Modality
getModality Dom' t Type
a)) }
    dotPattern :: Expr -> Term -> Dom Type -> LeftoverPatterns
dotPattern Expr
e Term
v Dom Type
a     = forall a. Null a => a
empty { dotPatterns :: [DotPattern]
dotPatterns      = forall el coll. Singleton el coll => el -> coll
singleton (Expr -> Term -> Dom Type -> DotPattern
Dot Expr
e Term
v Dom Type
a) }
    absurdPattern :: Range -> Type -> LeftoverPatterns
absurdPattern Range
info Type
a = forall a. Null a => a
empty { absurdPatterns :: [AbsurdPattern]
absurdPatterns   = forall el coll. Singleton el coll => el -> coll
singleton (Range -> Type -> AbsurdPattern
Absurd Range
info Type
a) }
    annPattern :: Expr -> Type -> LeftoverPatterns
annPattern Expr
t Type
a       = forall a. Null a => a
empty { typeAnnotations :: [AnnotationPattern]
typeAnnotations  = forall el coll. Singleton el coll => el -> coll
singleton (Expr -> Type -> AnnotationPattern
Ann Expr
t Type
a) }
    otherPattern :: Pattern -> LeftoverPatterns
otherPattern Pattern
p       = forall a. Null a => a
empty { otherPatterns :: [Pattern]
otherPatterns    = forall el coll. Singleton el coll => el -> coll
singleton Pattern
p }

    getLeftoverPattern :: (A.Name -> Bool) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern :: (Name -> Bool) -> ProblemEq -> m LeftoverPatterns
getLeftoverPattern Name -> Bool
isParamName (ProblemEq Pattern
p Term
v Dom Type
a) = case Pattern
p of
      (A.VarP A.BindName{unBind :: BindName -> Name
unBind = Name
x}) -> forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
v (forall t e. Dom' t e -> e
unDom Dom Type
a) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just Int
i  | Name -> Bool
isParamName Name
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Int -> LeftoverPatterns
moduleParameter Name
x Int
i
                | Bool
otherwise     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Int -> LeftoverPatterns
patternVariable Name
x Int
i
        Maybe Int
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {t}. Name -> Term -> Dom' t Type -> LeftoverPatterns
asPattern Name
x Term
v Dom Type
a
      (A.WildP PatInfo
_)       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
      (A.AsP PatInfo
info A.BindName{unBind :: BindName -> Name
unBind = Name
x} Pattern
p)  -> (forall {t}. Name -> Term -> Dom' t Type -> LeftoverPatterns
asPattern Name
x Term
v Dom Type
a forall a. Monoid a => a -> a -> a
`mappend`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        (Name -> Bool) -> ProblemEq -> m LeftoverPatterns
getLeftoverPattern Name -> Bool
isParamName forall a b. (a -> b) -> a -> b
$ Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
v Dom Type
a
      (A.DotP PatInfo
info Expr
e)   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Expr -> Term -> Dom Type -> LeftoverPatterns
dotPattern Expr
e Term
v Dom Type
a
      (A.AbsurdP PatInfo
info)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Type -> LeftoverPatterns
absurdPattern (forall a. HasRange a => a -> Range
getRange PatInfo
info) (forall t e. Dom' t e -> e
unDom Dom Type
a)
      (A.AnnP PatInfo
info Expr
t Pattern
p) -> (Expr -> Type -> LeftoverPatterns
annPattern Expr
t (forall t e. Dom' t e -> e
unDom Dom Type
a) forall a. Monoid a => a -> a -> a
`mappend`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        (Name -> Bool) -> ProblemEq -> m LeftoverPatterns
getLeftoverPattern Name -> Bool
isParamName forall a b. (a -> b) -> a -> b
$ Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
v Dom Type
a
      Pattern
_                 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pattern -> LeftoverPatterns
otherPattern Pattern
p

-- | Build a renaming for the internal patterns using variable names from
--   the user patterns. If there are multiple user names for the same internal
--   variable, the unused ones are returned as as-bindings.
--   Names that are not also module parameters are preferred over
--   those that are.
getUserVariableNames
  :: Telescope                         -- ^ The telescope of pattern variables
  -> IntMap [(A.Name,PatVarPosition)]  -- ^ The list of user names for each pattern variable
  -> ([Maybe A.Name], [AsBinding])
getUserVariableNames :: Telescope
-> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
getUserVariableNames Telescope
tel IntMap [(Name, PatVarPosition)]
names = forall w a. Writer w a -> (a, w)
runWriter forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Dom Type -> Int -> Writer [AsBinding] (Maybe Name)
makeVar (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel) (forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Telescope
tel)

  where
    makeVar :: Dom Type -> Int -> Writer [AsBinding] (Maybe A.Name)
    makeVar :: Dom Type -> Int -> Writer [AsBinding] (Maybe Name)
makeVar Dom Type
a Int
i = case [(Name, PatVarPosition)] -> ([Name], [Name])
partitionIsParam (forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault [] Int
i IntMap [(Name, PatVarPosition)]
names) of
      ([]     , [])   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      ((Name
x:[Name]
xs) , [])   -> [Name] -> WriterT [AsBinding] Identity ()
tellAsBindings [Name]
xs forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (forall a. a -> Maybe a
Just Name
x)
      ([Name]
xs     , Name
y:[Name]
ys) -> [Name] -> WriterT [AsBinding] Identity ()
tellAsBindings ([Name]
xs forall a. [a] -> [a] -> [a]
++ [Name]
ys) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (forall a. a -> Maybe a
Just Name
y)
      where
        tellAsBindings :: [Name] -> WriterT [AsBinding] Identity ()
tellAsBindings = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\Name
y -> Name -> Term -> Type -> Modality -> AsBinding
AsB Name
y (Int -> Term
var Int
i) (forall t e. Dom' t e -> e
unDom Dom Type
a) (forall a. LensModality a => a -> Modality
getModality Dom Type
a))

    partitionIsParam :: [(A.Name,PatVarPosition)] -> ([A.Name],[A.Name])
    partitionIsParam :: [(Name, PatVarPosition)] -> ([Name], [Name])
partitionIsParam = (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((forall a. Eq a => a -> a -> Bool
== PatVarPosition
PVParam) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)


instance Subst (Problem a) where
  type SubstArg (Problem a) = Term
  applySubst :: Substitution' (SubstArg (Problem a)) -> Problem a -> Problem a
applySubst Substitution' (SubstArg (Problem a))
rho (Problem [ProblemEq]
eqs [NamedArg Pattern]
rps LHSState a -> TCM a
cont) = forall a.
[ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
Problem (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Problem a))
rho [ProblemEq]
eqs) [NamedArg Pattern]
rps LHSState a -> TCM a
cont

instance Subst AsBinding where
  type SubstArg AsBinding = Term
  applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding
applySubst Substitution' (SubstArg AsBinding)
rho (AsB Name
x Term
v Type
a Modality
m) = (\(Term
v,Type
a) -> Name -> Term -> Type -> Modality -> AsBinding
AsB Name
x Term
v Type
a Modality
m) forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg AsBinding)
rho (Term
v, Type
a)

instance Subst DotPattern where
  type SubstArg DotPattern = Term
  applySubst :: Substitution' (SubstArg DotPattern) -> DotPattern -> DotPattern
applySubst Substitution' (SubstArg DotPattern)
rho (Dot Expr
e Term
v Dom Type
a) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Expr -> Term -> Dom Type -> DotPattern
Dot Expr
e) forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg DotPattern)
rho (Term
v, Dom Type
a)

instance Subst AbsurdPattern where
  type SubstArg AbsurdPattern = Term
  applySubst :: Substitution' (SubstArg AbsurdPattern)
-> AbsurdPattern -> AbsurdPattern
applySubst Substitution' (SubstArg AbsurdPattern)
rho (Absurd Range
r Type
a) = Range -> Type -> AbsurdPattern
Absurd Range
r forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg AbsurdPattern)
rho Type
a

instance PrettyTCM ProblemEq where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ProblemEq -> m Doc
prettyTCM (ProblemEq Pattern
p Term
v Dom Type
a) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"="
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
    ]

instance PrettyTCM AsBinding where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => AsBinding -> m Doc
prettyTCM (AsB Name
x Term
v Type
a Modality
m) =
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x forall a. Semigroup a => a -> a -> a
<> m Doc
"@" forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v)
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
        ]

instance PrettyTCM DotPattern where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => DotPattern -> m Doc
prettyTCM (Dot Expr
e Term
v Dom Type
a) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"="
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
    ]

instance PrettyTCM AbsurdPattern where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => AbsurdPattern -> m Doc
prettyTCM (Absurd Range
r Type
a) = m Doc
"() :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a

instance PrettyTCM AnnotationPattern where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => AnnotationPattern -> m Doc
prettyTCM (Ann Expr
a Type
p) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
a

instance PP.Pretty AsBinding where
  pretty :: AsBinding -> Doc
pretty (AsB Name
x Term
v Type
a Modality
m) =
    forall a. Pretty a => a -> Doc
PP.pretty Name
x Doc -> Doc -> Doc
PP.<+> Doc
"=" Doc -> Doc -> Doc
PP.<+>
      Doc -> Int -> Doc -> Doc
PP.hang (forall a. Pretty a => a -> Doc
PP.pretty Term
v Doc -> Doc -> Doc
PP.<+> Doc
":") Int
2 (forall a. Pretty a => a -> Doc
PP.pretty Type
a)

instance InstantiateFull AsBinding where
  instantiateFull' :: AsBinding -> ReduceM AsBinding
instantiateFull' (AsB Name
x Term
v Type
a Modality
m) = Name -> Term -> Type -> Modality -> AsBinding
AsB Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Term
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Modality
m

instance PrettyTCM (LHSState a) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => LHSState a -> m Doc
prettyTCM (LHSState Telescope
tel [NamedArg DeBruijnPattern]
outPat (Problem [ProblemEq]
eqs [NamedArg Pattern]
rps LHSState a -> TCM a
_) Arg Type
target [Maybe Int]
_ Bool
_) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ m Doc
"tel             = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
    , m Doc
"outPat          = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
outPat)
    , m Doc
"problemEqs      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemEq]
eqs)
    , m Doc
"problemRestPats = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
rps)
    , m Doc
"target          = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
target)
    ]