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.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 ( sortOn )
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.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Syntax.Common.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
(FlexibleVarKind -> FlexibleVarKind -> Bool)
-> (FlexibleVarKind -> FlexibleVarKind -> Bool)
-> Eq FlexibleVarKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FlexibleVarKind -> FlexibleVarKind -> Bool
== :: FlexibleVarKind -> FlexibleVarKind -> Bool
$c/= :: FlexibleVarKind -> FlexibleVarKind -> Bool
/= :: FlexibleVarKind -> FlexibleVarKind -> Bool
Eq, Int -> FlexibleVarKind -> ShowS
[FlexibleVarKind] -> ShowS
FlexibleVarKind -> ArgName
(Int -> FlexibleVarKind -> ShowS)
-> (FlexibleVarKind -> ArgName)
-> ([FlexibleVarKind] -> ShowS)
-> Show FlexibleVarKind
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FlexibleVarKind -> ShowS
showsPrec :: Int -> FlexibleVarKind -> ShowS
$cshow :: FlexibleVarKind -> ArgName
show :: FlexibleVarKind -> ArgName
$cshowList :: [FlexibleVarKind] -> ShowS
showList :: [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
(FlexibleVar a -> FlexibleVar a -> Bool)
-> (FlexibleVar a -> FlexibleVar a -> Bool) -> Eq (FlexibleVar a)
forall a. Eq a => FlexibleVar a -> FlexibleVar a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: FlexibleVar a -> FlexibleVar a -> Bool
Eq, Int -> FlexibleVar a -> ShowS
[FlexibleVar a] -> ShowS
FlexibleVar a -> ArgName
(Int -> FlexibleVar a -> ShowS)
-> (FlexibleVar a -> ArgName)
-> ([FlexibleVar a] -> ShowS)
-> Show (FlexibleVar a)
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
$cshowsPrec :: forall a. Show a => Int -> FlexibleVar a -> ShowS
showsPrec :: Int -> FlexibleVar a -> ShowS
$cshow :: forall a. Show a => FlexibleVar a -> ArgName
show :: FlexibleVar a -> ArgName
$cshowList :: forall a. Show a => [FlexibleVar a] -> ShowS
showList :: [FlexibleVar a] -> ShowS
Show, (forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b)
-> (forall a b. a -> FlexibleVar b -> FlexibleVar a)
-> Functor FlexibleVar
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
$cfmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
fmap :: forall a b. (a -> b) -> FlexibleVar a -> FlexibleVar b
$c<$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
<$ :: forall a b. a -> FlexibleVar b -> FlexibleVar a
Functor, (forall m. Monoid m => FlexibleVar m -> m)
-> (forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m)
-> (forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m)
-> (forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b)
-> (forall a b. (a -> b -> b) -> b -> FlexibleVar a -> b)
-> (forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b)
-> (forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b)
-> (forall a. (a -> a -> a) -> FlexibleVar a -> a)
-> (forall a. (a -> a -> a) -> FlexibleVar a -> a)
-> (forall a. FlexibleVar a -> [a])
-> (forall a. FlexibleVar a -> Bool)
-> (forall a. FlexibleVar a -> Int)
-> (forall a. Eq a => a -> FlexibleVar a -> Bool)
-> (forall a. Ord a => FlexibleVar a -> a)
-> (forall a. Ord a => FlexibleVar a -> a)
-> (forall a. Num a => FlexibleVar a -> a)
-> (forall a. Num a => FlexibleVar a -> a)
-> Foldable FlexibleVar
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
$cfold :: forall m. Monoid m => FlexibleVar m -> m
fold :: forall m. Monoid m => FlexibleVar m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> FlexibleVar a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> FlexibleVar a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
foldr1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
foldl1 :: forall a. (a -> a -> a) -> FlexibleVar a -> a
$ctoList :: forall a. FlexibleVar a -> [a]
toList :: forall a. FlexibleVar a -> [a]
$cnull :: forall a. FlexibleVar a -> Bool
null :: forall a. FlexibleVar a -> Bool
$clength :: forall a. FlexibleVar a -> Int
length :: forall a. FlexibleVar a -> Int
$celem :: forall a. Eq a => a -> FlexibleVar a -> Bool
elem :: forall a. Eq a => a -> FlexibleVar a -> Bool
$cmaximum :: forall a. Ord a => FlexibleVar a -> a
maximum :: forall a. Ord a => FlexibleVar a -> a
$cminimum :: forall a. Ord a => FlexibleVar a -> a
minimum :: forall a. Ord a => FlexibleVar a -> a
$csum :: forall a. Num a => FlexibleVar a -> a
sum :: forall a. Num a => FlexibleVar a -> a
$cproduct :: forall a. Num a => FlexibleVar a -> a
product :: forall a. Num a => FlexibleVar a -> a
Foldable, Functor FlexibleVar
Foldable FlexibleVar
(Functor FlexibleVar, Foldable FlexibleVar) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> FlexibleVar a -> f (FlexibleVar b))
-> (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 (m :: * -> *) a.
    Monad m =>
    FlexibleVar (m a) -> m (FlexibleVar a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FlexibleVar a -> f (FlexibleVar b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FlexibleVar (f a) -> f (FlexibleVar a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FlexibleVar (f a) -> f (FlexibleVar a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FlexibleVar a -> m (FlexibleVar b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FlexibleVar (m a) -> m (FlexibleVar a)
sequence :: forall (m :: * -> *) a.
Monad m =>
FlexibleVar (m a) -> m (FlexibleVar a)
Traversable)

instance LensArgInfo (FlexibleVar a) where
  getArgInfo :: FlexibleVar a -> ArgInfo
getArgInfo = FlexibleVar a -> ArgInfo
forall a. FlexibleVar a -> ArgInfo
flexArgInfo
  setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a
setArgInfo ArgInfo
ai FlexibleVar a
fl = FlexibleVar a
fl { flexArgInfo = ai }
  mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a
mapArgInfo ArgInfo -> ArgInfo
f  FlexibleVar a
fl = FlexibleVar a
fl { flexArgInfo = f (flexArgInfo 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] -> Tele (Dom' Term Type) -> FlexibleVars
allFlexVars [IsForced]
forced Tele (Dom' Term Type)
tel = (Int -> Dom (ArgName, Type) -> IsForced -> FlexibleVar Int)
-> [Int] -> [Dom (ArgName, Type)] -> [IsForced] -> FlexibleVars
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Int -> Dom (ArgName, Type) -> IsForced -> FlexibleVar Int
forall {a}.
LensArgInfo a =>
Int -> a -> IsForced -> FlexibleVar Int
makeFlex (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) (Tele (Dom' Term Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom' Term Type)
tel) [IsForced]
fs
  where
    n :: Int
n  = Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
tel
    fs :: [IsForced]
fs = [IsForced]
forced [IsForced] -> [IsForced] -> [IsForced]
forall a. [a] -> [a] -> [a]
++ IsForced -> [IsForced]
forall a. a -> [a]
repeat IsForced
NotForced
    makeFlex :: Int -> a -> IsForced -> FlexibleVar Int
makeFlex Int
i a
d IsForced
f = ArgInfo
-> IsForced
-> FlexibleVarKind
-> Maybe Int
-> Int
-> FlexibleVar Int
forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar (a -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo a
d) IsForced
f FlexibleVarKind
ImplicitFlex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) Int
i

data FlexChoice = ChooseLeft | ChooseRight | ChooseEither | ExpandBoth
  deriving (FlexChoice -> FlexChoice -> Bool
(FlexChoice -> FlexChoice -> Bool)
-> (FlexChoice -> FlexChoice -> Bool) -> Eq FlexChoice
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FlexChoice -> FlexChoice -> Bool
== :: FlexChoice -> FlexChoice -> Bool
$c/= :: FlexChoice -> FlexChoice -> Bool
/= :: FlexChoice -> FlexChoice -> Bool
Eq, Int -> FlexChoice -> ShowS
[FlexChoice] -> ShowS
FlexChoice -> ArgName
(Int -> FlexChoice -> ShowS)
-> (FlexChoice -> ArgName)
-> ([FlexChoice] -> ShowS)
-> Show FlexChoice
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FlexChoice -> ShowS
showsPrec :: Int -> FlexChoice -> ShowS
$cshow :: FlexChoice -> ArgName
show :: FlexChoice -> ArgName
$cshowList :: [FlexChoice] -> ShowS
showList :: [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 = FlexChoice -> FlexChoice -> FlexChoice
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) = [FlexibleVarKind] -> [FlexibleVarKind] -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex [FlexibleVarKind]
xs [FlexibleVarKind]
ys
  chooseFlex (RecordFlex [FlexibleVarKind]
xs) FlexibleVarKind
y               = [FlexibleVarKind] -> [FlexibleVarKind] -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex [FlexibleVarKind]
xs (FlexibleVarKind -> [FlexibleVarKind]
forall a. a -> [a]
repeat FlexibleVarKind
y)
  chooseFlex FlexibleVarKind
x               (RecordFlex [FlexibleVarKind]
ys) = [FlexibleVarKind] -> [FlexibleVarKind] -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex (FlexibleVarKind -> [FlexibleVarKind]
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 = [FlexChoice] -> FlexChoice
forall a. Monoid a => [a] -> a
mconcat ([FlexChoice] -> FlexChoice) -> [FlexChoice] -> FlexChoice
forall a b. (a -> b) -> a -> b
$ (a -> a -> FlexChoice) -> [a] -> [a] -> [FlexChoice]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> FlexChoice
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) = a -> a -> FlexChoice
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 [ Origin -> Origin -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai1) (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai2)
                                   , Hiding -> Hiding -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
ai1) (ArgInfo -> Hiding
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 Int -> Int -> Ordering
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 [ FlexibleVarKind -> FlexibleVarKind -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex FlexibleVarKind
f1 FlexibleVarKind
f2, IsForced -> IsForced -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex IsForced
fc1 IsForced
fc2, ArgInfo -> ArgInfo -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex ArgInfo
ai1 ArgInfo
ai2
                , Maybe Int -> Maybe Int -> FlexChoice
forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex Maybe Int
p1 Maybe Int
p2, a -> a -> FlexChoice
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
[Problem a] -> ShowS
Problem a -> ArgName
(Int -> Problem a -> ShowS)
-> (Problem a -> ArgName)
-> ([Problem a] -> ShowS)
-> Show (Problem a)
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
$cshowsPrec :: forall a. Int -> Problem a -> ShowS
showsPrec :: Int -> Problem a -> ShowS
$cshow :: forall a. Problem a -> ArgName
show :: Problem a -> ArgName
$cshowList :: forall a. [Problem a] -> ShowS
showList :: [Problem a] -> ShowS
Show

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

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

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

problemInPats :: Problem a -> [A.Pattern]
problemInPats :: forall a. Problem a -> [Pattern]
problemInPats = (ProblemEq -> Pattern) -> [ProblemEq] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ProblemEq -> Pattern
problemInPat ([ProblemEq] -> [Pattern])
-> (Problem a -> [ProblemEq]) -> Problem a -> [Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Problem a
-> Getting [ProblemEq] (Problem a) [ProblemEq] -> [ProblemEq]
forall s a. s -> Getting a s a -> a
^. Getting [ProblemEq] (Problem a) [ProblemEq]
forall a (f :: * -> *).
Functor f =>
([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a)
problemEqs)

data AsBinding = AsB Name Term (Dom Type)
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 -> Tele (Dom' Term Type)
_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' (LHSState a) Telescope
lhsTel :: forall a (f :: * -> *).
Functor f =>
(Tele (Dom' Term Type) -> f (Tele (Dom' Term Type)))
-> LHSState a -> f (LHSState a)
lhsTel Tele (Dom' Term Type) -> f (Tele (Dom' Term Type))
f LHSState a
p = Tele (Dom' Term Type) -> f (Tele (Dom' Term Type))
f (LHSState a -> Tele (Dom' Term Type)
forall a. LHSState a -> Tele (Dom' Term Type)
_lhsTel LHSState a
p) f (Tele (Dom' Term Type))
-> (Tele (Dom' Term Type) -> LHSState a) -> f (LHSState a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Tele (Dom' Term Type)
x -> LHSState a
p {_lhsTel = x}

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

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

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

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

data LeftoverPatterns = LeftoverPatterns
  { LeftoverPatterns -> IntMap [(Arg Name, PatVarPosition)]
patternVariables :: IntMap [(Arg 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 [(Arg Name, PatVarPosition)]
patternVariables = ([(Arg Name, PatVarPosition)]
 -> [(Arg Name, PatVarPosition)] -> [(Arg Name, PatVarPosition)])
-> IntMap [(Arg Name, PatVarPosition)]
-> IntMap [(Arg Name, PatVarPosition)]
-> IntMap [(Arg Name, PatVarPosition)]
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith [(Arg Name, PatVarPosition)]
-> [(Arg Name, PatVarPosition)] -> [(Arg Name, PatVarPosition)]
forall a. [a] -> [a] -> [a]
(++) (LeftoverPatterns -> IntMap [(Arg Name, PatVarPosition)]
patternVariables LeftoverPatterns
x) (LeftoverPatterns -> IntMap [(Arg Name, PatVarPosition)]
patternVariables LeftoverPatterns
y)
    , asPatterns :: [AsBinding]
asPatterns       = LeftoverPatterns -> [AsBinding]
asPatterns LeftoverPatterns
x [AsBinding] -> [AsBinding] -> [AsBinding]
forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [AsBinding]
asPatterns LeftoverPatterns
y
    , dotPatterns :: [DotPattern]
dotPatterns      = LeftoverPatterns -> [DotPattern]
dotPatterns LeftoverPatterns
x [DotPattern] -> [DotPattern] -> [DotPattern]
forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [DotPattern]
dotPatterns LeftoverPatterns
y
    , absurdPatterns :: [AbsurdPattern]
absurdPatterns   = LeftoverPatterns -> [AbsurdPattern]
absurdPatterns LeftoverPatterns
x [AbsurdPattern] -> [AbsurdPattern] -> [AbsurdPattern]
forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [AbsurdPattern]
absurdPatterns LeftoverPatterns
y
    , typeAnnotations :: [AnnotationPattern]
typeAnnotations  = LeftoverPatterns -> [AnnotationPattern]
typeAnnotations LeftoverPatterns
x [AnnotationPattern] -> [AnnotationPattern] -> [AnnotationPattern]
forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [AnnotationPattern]
typeAnnotations LeftoverPatterns
y
    , otherPatterns :: [Pattern]
otherPatterns    = LeftoverPatterns -> [Pattern]
otherPatterns LeftoverPatterns
x [Pattern] -> [Pattern] -> [Pattern]
forall a. [a] -> [a] -> [a]
++ LeftoverPatterns -> [Pattern]
otherPatterns LeftoverPatterns
y
    }

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


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

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

instance PrettyTCM LeftoverPatterns where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => LeftoverPatterns -> m Doc
prettyTCM (LeftoverPatterns IntMap [(Arg Name, PatVarPosition)]
varp [AsBinding]
asb [DotPattern]
dotp [AbsurdPattern]
absurdp [AnnotationPattern]
annp [Pattern]
otherp) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ m Doc
"pattern variables: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Int, [(Arg Name, PatVarPosition)])] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (IntMap [(Arg Name, PatVarPosition)]
-> [(Int, [(Arg Name, PatVarPosition)])]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap [(Arg Name, PatVarPosition)]
varp)
    , m Doc
"as bindings:       " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((AsBinding -> m Doc) -> [AsBinding] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map AsBinding -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AsBinding -> m Doc
prettyTCM [AsBinding]
asb)
    , m Doc
"dot patterns:      " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((DotPattern -> m Doc) -> [DotPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map DotPattern -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DotPattern -> m Doc
prettyTCM [DotPattern]
dotp)
    , m Doc
"absurd patterns:   " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((AbsurdPattern -> m Doc) -> [AbsurdPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbsurdPattern -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AbsurdPattern -> m Doc
prettyTCM [AbsurdPattern]
absurdp)
    , m Doc
"type annotations:  " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((AnnotationPattern -> m Doc) -> [AnnotationPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map AnnotationPattern -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => AnnotationPattern -> m Doc
prettyTCM [AnnotationPattern]
annp)
    , m Doc
"other patterns:    " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Pattern -> m Doc) -> [Pattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> m Doc
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, MonadFresh NameId m)
  => [ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns :: forall (m :: * -> *).
(PureTCM m, MonadFresh NameId m) =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns [ProblemEq]
eqs = do
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.lhs.top" Int
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"classifying leftover patterns"
  params <- [ArgName] -> Set ArgName
forall a. Ord a => [a] -> Set a
Set.fromList ([ArgName] -> Set ArgName)
-> (Tele (Dom' Term Type) -> [ArgName])
-> Tele (Dom' Term Type)
-> Set ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom' Term Type) -> [ArgName]
teleNames (Tele (Dom' Term Type) -> Set ArgName)
-> m (Tele (Dom' Term Type)) -> m (Set ArgName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> m (Tele (Dom' Term Type))
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Tele (Dom' Term Type))
lookupSection (ModuleName -> m (Tele (Dom' Term Type)))
-> m ModuleName -> m (Tele (Dom' Term Type))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
  let isParamName Name
x = if Name -> ArgName
nameToArgName Name
x ArgName -> Set ArgName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ArgName
params then PatVarPosition
PVParam else PatVarPosition
PVLocal
  mconcat <$> mapM (getLeftoverPattern isParamName) eqs
  where
    patternVariable :: Arg Name -> Int -> PatVarPosition -> LeftoverPatterns
patternVariable Arg Name
x Int
i PatVarPosition
isPar = LeftoverPatterns
forall a. Null a => a
empty { patternVariables = singleton (i,[(x,isPar)]) }
    asPattern :: Name -> Term -> Dom' Term Type -> LeftoverPatterns
asPattern Name
x Term
v Dom' Term Type
a      = LeftoverPatterns
forall a. Null a => a
empty { asPatterns       = singleton (AsB x v a) }
    dotPattern :: Expr -> Term -> Dom' Term Type -> LeftoverPatterns
dotPattern Expr
e Term
v Dom' Term Type
a     = LeftoverPatterns
forall a. Null a => a
empty { dotPatterns      = singleton (Dot e v a) }
    absurdPattern :: Range' SrcFile -> Type -> LeftoverPatterns
absurdPattern Range' SrcFile
info Type
a = LeftoverPatterns
forall a. Null a => a
empty { absurdPatterns   = singleton (Absurd info a) }
    otherPattern :: Pattern -> LeftoverPatterns
otherPattern Pattern
p       = LeftoverPatterns
forall a. Null a => a
empty { otherPatterns    = singleton p }

    getLeftoverPattern :: (A.Name -> PatVarPosition) -> ProblemEq -> m LeftoverPatterns
    getLeftoverPattern :: (Name -> PatVarPosition) -> ProblemEq -> m LeftoverPatterns
getLeftoverPattern Name -> PatVarPosition
isParamName (ProblemEq Pattern
p Term
v Dom' Term Type
a) = case Pattern
p of
      (A.VarP A.BindName{unBind :: BindName -> Name
unBind = Name
x}) -> Term -> Type -> m (Maybe Int)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
v (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
a) m (Maybe Int)
-> (Maybe Int -> LeftoverPatterns) -> m LeftoverPatterns
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
        Just Int
i -> Arg Name -> Int -> PatVarPosition -> LeftoverPatterns
patternVariable (Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom' Term Type
a Arg Type -> Name -> Arg Name
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Name
x) Int
i (Name -> PatVarPosition
isParamName Name
x)
        Maybe Int
Nothing -> Name -> Term -> Dom' Term Type -> LeftoverPatterns
asPattern Name
x Term
v Dom' Term Type
a
      (A.WildP PatInfo
r)
        | Dom' Term Type -> Bool
forall a. LensHiding a => a -> Bool
isInstance Dom' Term Type
a ->
            -- Issue #7392: If the wildcard appears in an instance position
            -- and is not already bound as an instance in the context,
            -- add it as a let binding.
            m Bool
-> m LeftoverPatterns -> m LeftoverPatterns -> m LeftoverPatterns
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Term -> Type -> m Bool
isInstanceVar Term
v (Type -> m Bool) -> Type -> m Bool
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
a) (LeftoverPatterns -> m LeftoverPatterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return LeftoverPatterns
forall a. Monoid a => a
mempty) (m LeftoverPatterns -> m LeftoverPatterns)
-> m LeftoverPatterns -> m LeftoverPatterns
forall a b. (a -> b) -> a -> b
$ do
              -- TODO: avoid fresh name by assigning unique `NameId` to `WildP`s?
              x <- Range' SrcFile -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range' SrcFile -> m Name
freshNoName (PatInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange PatInfo
r)
              return $ asPattern x v a
        | Bool
otherwise -> LeftoverPatterns -> m LeftoverPatterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return LeftoverPatterns
forall a. Monoid a => a
mempty
      (A.AsP PatInfo
info A.BindName{unBind :: BindName -> Name
unBind = Name
x} Pattern
p)  -> (Name -> Term -> Dom' Term Type -> LeftoverPatterns
asPattern Name
x Term
v Dom' Term Type
a LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns
forall a. Monoid a => a -> a -> a
`mappend`) (LeftoverPatterns -> LeftoverPatterns)
-> m LeftoverPatterns -> m LeftoverPatterns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        (Name -> PatVarPosition) -> ProblemEq -> m LeftoverPatterns
getLeftoverPattern Name -> PatVarPosition
isParamName (ProblemEq -> m LeftoverPatterns)
-> ProblemEq -> m LeftoverPatterns
forall a b. (a -> b) -> a -> b
$ Pattern -> Term -> Dom' Term Type -> ProblemEq
ProblemEq Pattern
p Term
v Dom' Term Type
a
      (A.DotP PatInfo
info Expr
e)   -> LeftoverPatterns -> m LeftoverPatterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (LeftoverPatterns -> m LeftoverPatterns)
-> LeftoverPatterns -> m LeftoverPatterns
forall a b. (a -> b) -> a -> b
$ Expr -> Term -> Dom' Term Type -> LeftoverPatterns
dotPattern Expr
e Term
v Dom' Term Type
a
      (A.AbsurdP PatInfo
info)  -> LeftoverPatterns -> m LeftoverPatterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (LeftoverPatterns -> m LeftoverPatterns)
-> LeftoverPatterns -> m LeftoverPatterns
forall a b. (a -> b) -> a -> b
$ Range' SrcFile -> Type -> LeftoverPatterns
absurdPattern (PatInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange PatInfo
info) (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
a)
      Pattern
_                 -> LeftoverPatterns -> m LeftoverPatterns
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (LeftoverPatterns -> m LeftoverPatterns)
-> LeftoverPatterns -> m LeftoverPatterns
forall a b. (a -> b) -> a -> b
$ Pattern -> LeftoverPatterns
otherPattern Pattern
p

      where
        isInstanceVar :: Term -> Type -> m Bool
        isInstanceVar :: Term -> Type -> m Bool
isInstanceVar Term
v Type
a = Term -> Type -> m (Maybe Int)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
v Type
a m (Maybe Int) -> (Maybe Int -> m Bool) -> m Bool
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just Int
i -> Dom' Term Type -> Bool
forall a. LensHiding a => a -> Bool
isInstance (Dom' Term Type -> Bool) -> m (Dom' Term Type) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Dom' Term Type)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Dom' Term Type)
domOfBV Int
i
            Maybe Int
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | 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 [(Arg A.Name,PatVarPosition)]  -- ^ The list of user names for each pattern variable
  -> ([Maybe A.Name], [AsBinding])
getUserVariableNames :: Tele (Dom' Term Type)
-> IntMap [(Arg Name, PatVarPosition)]
-> ([Maybe Name], [AsBinding])
getUserVariableNames Tele (Dom' Term Type)
tel IntMap [(Arg Name, PatVarPosition)]
names = Writer [AsBinding] [Maybe Name] -> ([Maybe Name], [AsBinding])
forall w a. Writer w a -> (a, w)
runWriter (Writer [AsBinding] [Maybe Name] -> ([Maybe Name], [AsBinding]))
-> Writer [AsBinding] [Maybe Name] -> ([Maybe Name], [AsBinding])
forall a b. (a -> b) -> a -> b
$
  (Dom' Term Type
 -> Int -> WriterT [AsBinding] Identity (Maybe Name))
-> [Dom' Term Type] -> [Int] -> Writer [AsBinding] [Maybe Name]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Dom' Term Type -> Int -> WriterT [AsBinding] Identity (Maybe Name)
makeVar (Tele (Dom' Term Type) -> [Dom' Term Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom' Term Type)
tel) (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
tel)

  where
    makeVar :: Dom Type -> Int -> Writer [AsBinding] (Maybe A.Name)
    makeVar :: Dom' Term Type -> Int -> WriterT [AsBinding] Identity (Maybe Name)
makeVar Dom' Term Type
a Int
i =
      case ((Arg Name, PatVarPosition) -> Arg Name)
-> [(Arg Name, PatVarPosition)] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map (Arg Name, PatVarPosition) -> Arg Name
forall a b. (a, b) -> a
fst ([(Arg Name, PatVarPosition)] -> [Arg Name])
-> [(Arg Name, PatVarPosition)] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ ((Arg Name, PatVarPosition) -> Bool)
-> [(Arg Name, PatVarPosition)] -> [(Arg Name, PatVarPosition)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn ((PatVarPosition -> PatVarPosition -> Bool
forall a. Eq a => a -> a -> Bool
== PatVarPosition
PVParam) (PatVarPosition -> Bool)
-> ((Arg Name, PatVarPosition) -> PatVarPosition)
-> (Arg Name, PatVarPosition)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Name, PatVarPosition) -> PatVarPosition
forall a b. (a, b) -> b
snd) ([(Arg Name, PatVarPosition)]
-> Int
-> IntMap [(Arg Name, PatVarPosition)]
-> [(Arg Name, PatVarPosition)]
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault [] Int
i IntMap [(Arg Name, PatVarPosition)]
names) of
        [] -> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
forall a. a -> WriterT [AsBinding] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
forall a. Maybe a
Nothing
        (Arg Name
z:[Arg Name]
zs) -> do
          [Arg Name] -> WriterT [AsBinding] Identity ()
tellAsBindings ([Arg Name] -> WriterT [AsBinding] Identity ())
-> [Arg Name] -> WriterT [AsBinding] Identity ()
forall a b. (a -> b) -> a -> b
$
            -- Issue #7392: if the name that we picked comes from an instance argument
            -- but we are *not* binding it in an instance position, we should
            -- preserve the instance by *also* adding it as a let-binding.
            if Arg Name -> Bool
forall a. LensHiding a => a -> Bool
isInstance Arg Name
z Bool -> Bool -> Bool
&& Bool -> Bool
not (Dom' Term Type -> Bool
forall a. LensHiding a => a -> Bool
isInstance Dom' Term Type
a) then Arg Name
zArg Name -> [Arg Name] -> [Arg Name]
forall a. a -> [a] -> [a]
:[Arg Name]
zs else [Arg Name]
zs
          Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
forall a. a -> WriterT [AsBinding] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Name -> WriterT [AsBinding] Identity (Maybe Name))
-> Maybe Name -> WriterT [AsBinding] Identity (Maybe Name)
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Name
forall a. a -> Maybe a
Just (Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
z)
      where
        -- Use hiding status of the variable as written rather than from the telescope
        tellAsBindings :: [Arg Name] -> WriterT [AsBinding] Identity ()
tellAsBindings = [AsBinding] -> WriterT [AsBinding] Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([AsBinding] -> WriterT [AsBinding] Identity ())
-> ([Arg Name] -> [AsBinding])
-> [Arg Name]
-> WriterT [AsBinding] Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Name -> AsBinding) -> [Arg Name] -> [AsBinding]
forall a b. (a -> b) -> [a] -> [b]
map (\Arg Name
y -> Name -> Term -> Dom' Term Type -> AsBinding
AsB (Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
y) (Int -> Term
var Int
i) (Hiding -> Dom' Term Type -> Dom' Term Type
forall a. LensHiding a => Hiding -> a -> a
setHiding (Arg Name -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Arg Name
y) Dom' Term Type
a))

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) = [ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
forall a.
[ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
Problem (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [ProblemEq])
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 Dom' Term Type
a) = (\(Term
v,Dom' Term Type
a) -> Name -> Term -> Dom' Term Type -> AsBinding
AsB Name
x Term
v Dom' Term Type
a) ((Term, Dom' Term Type) -> AsBinding)
-> (Term, Dom' Term Type) -> AsBinding
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Term, Dom' Term Type))
-> (Term, Dom' Term Type) -> (Term, Dom' Term Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Term, Dom' Term Type))
Substitution' (SubstArg AsBinding)
rho (Term
v, Dom' Term 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' Term Type
a) = (Term -> Dom' Term Type -> DotPattern)
-> (Term, Dom' Term Type) -> DotPattern
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Expr -> Term -> Dom' Term Type -> DotPattern
Dot Expr
e) ((Term, Dom' Term Type) -> DotPattern)
-> (Term, Dom' Term Type) -> DotPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Term, Dom' Term Type))
-> (Term, Dom' Term Type) -> (Term, Dom' Term Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Term, Dom' Term Type))
Substitution' (SubstArg DotPattern)
rho (Term
v, Dom' Term Type
a)

instance Subst AbsurdPattern where
  type SubstArg AbsurdPattern = Term
  applySubst :: Substitution' (SubstArg AbsurdPattern)
-> AbsurdPattern -> AbsurdPattern
applySubst Substitution' (SubstArg AbsurdPattern)
rho (Absurd Range' SrcFile
r Type
a) = Range' SrcFile -> Type -> AbsurdPattern
Absurd Range' SrcFile
r (Type -> AbsurdPattern) -> Type -> AbsurdPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
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' Term Type
a) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"="
    , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":"
    , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom' Term Type -> m Doc
prettyTCM Dom' Term Type
a
    ]

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

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

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

instance PrettyTCM AnnotationPattern where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => AnnotationPattern -> m Doc
prettyTCM (Ann Expr
a Type
p) = Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
p m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> 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 Dom' Term Type
a) =
    Name -> Doc
forall a. Pretty a => a -> Doc
PP.pretty Name
x Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
PP.<+> Doc
"=" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
PP.<+>
      Doc -> Int -> Doc -> Doc
forall a. Doc a -> Int -> Doc a -> Doc a
PP.hang (Term -> Doc
forall a. Pretty a => a -> Doc
PP.pretty Term
v Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
PP.<+> Doc
":") Int
2 (Dom' Term Type -> Doc
forall a. Pretty a => a -> Doc
PP.pretty Dom' Term Type
a)

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

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