{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Rules.LHS.ProblemRest where

import Control.Monad
import Control.Monad.Except

import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A

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

import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.Implicit

import Agda.Utils.Functor
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | Rename the variables in a telescope using the names from a given pattern.
--
--   If there are not at least as many patterns as entries as in the telescope,
--   the names of the remaining entries in the telescope are unchanged.
--   If there are too many patterns, there should be a type error later.
--
useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
useNamesFromPattern [NamedArg Pattern]
ps Telescope
tel = ListTel -> Telescope
telFromList ((NamedArg Pattern
 -> Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type))
-> [NamedArg Pattern] -> ListTel -> ListTel
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith NamedArg Pattern
-> Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type)
forall {a} {e} {t} {b}.
Arg (Named a (Pattern' e))
-> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
ren [NamedArg Pattern]
ps ListTel
telList ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ ListTel
telRemaining)
  where
    telList :: ListTel
telList = Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
    telRemaining :: ListTel
telRemaining = Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop ([NamedArg Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg Pattern]
ps) ListTel
telList -- telescope entries beyond patterns
    ren :: Arg (Named a (Pattern' e))
-> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
ren (Arg ArgInfo
ai (Named Maybe a
nm Pattern' e
p)) dom :: Dom' t (ArgName, b)
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = (ArgName
y, b
a) } =
      case Pattern' e
p of
        -- Andreas, 2017-10-12, issue #2803, also preserve user-written hidden names.
        -- However, not if the argument is named, because then the name in the telescope
        -- is significant for implicit insertion.
        A.VarP A.BindName{unBind :: BindName -> Name
unBind = Name
x}
          | Bool -> Bool
not (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x)
          , Dom' t (ArgName, b) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom Bool -> Bool -> Bool
|| (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
UserWritten Bool -> Bool -> Bool
&& Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing Maybe a
nm) ->
          Dom' t (ArgName, b)
dom{ unDom = (nameToArgName x, a) }
        A.AbsurdP{} | Dom' t (ArgName, b) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom -> Dom' t (ArgName, b)
dom{ unDom = (stringToArgName "()", a) }
        A.PatternSynP{} -> Dom' t (ArgName, b)
forall a. HasCallStack => a
__IMPOSSIBLE__  -- ensure there are no syns left
        -- Andreas, 2016-05-10, issue 1848: if context variable has no name, call it "x"
        Pattern' e
_ | Dom' t (ArgName, b) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom Bool -> Bool -> Bool
&& ArgName -> Bool
forall a. IsNoName a => a -> Bool
isNoName ArgName
y -> Dom' t (ArgName, b)
dom{ unDom = (stringToArgName "x", a) }
          | Bool
otherwise                  -> Dom' t (ArgName, b)
dom

useNamesFromProblemEqs
  :: forall m. PureTCM m
  => [ProblemEq] -> Telescope -> m Telescope
useNamesFromProblemEqs :: forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> Telescope -> m Telescope
useNamesFromProblemEqs [ProblemEq]
eqs Telescope
tel = Telescope -> m Telescope -> m Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Telescope -> m Telescope) -> m Telescope -> m Telescope
forall a b. (a -> b) -> a -> b
$ do
  names <- ([Maybe Name], [AsBinding]) -> [Maybe Name]
forall a b. (a, b) -> a
fst (([Maybe Name], [AsBinding]) -> [Maybe Name])
-> (LeftoverPatterns -> ([Maybe Name], [AsBinding]))
-> LeftoverPatterns
-> [Maybe Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope
-> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
getUserVariableNames Telescope
tel (IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding]))
-> (LeftoverPatterns -> IntMap [(Name, PatVarPosition)])
-> LeftoverPatterns
-> ([Maybe Name], [AsBinding])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables (LeftoverPatterns -> [Maybe Name])
-> m LeftoverPatterns -> m [Maybe Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProblemEq] -> m LeftoverPatterns
forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns [ProblemEq]
eqs
  let argNames = (Maybe Name -> Maybe ArgName) -> [Maybe Name] -> [Maybe ArgName]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> ArgName) -> Maybe Name -> Maybe ArgName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> ArgName
nameToArgName) [Maybe Name]
names
  return $ renameTel argNames tel

useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
useOriginFrom :: forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
useOriginFrom = (a -> b -> a) -> [a] -> [b] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((a -> b -> a) -> [a] -> [b] -> [a])
-> (a -> b -> a) -> [a] -> [b] -> [a]
forall a b. (a -> b) -> a -> b
$ \a
x b
y -> Origin -> a -> a
forall a. LensOrigin a => Origin -> a -> a
setOrigin (b -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin b
y) a
x

-- | Are there any untyped user patterns left?
noProblemRest :: Problem a -> Bool
noProblemRest :: forall a. Problem a -> Bool
noProblemRest (Problem [ProblemEq]
_ [NamedArg Pattern]
rp LHSState a -> TCM a
_) = [NamedArg Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg Pattern]
rp

-- | Construct an initial 'LHSState' from user patterns.
--   Example:
--   @
--
--      Case : {A : Set} → Maybe A → Set → Set → Set
--      Case nothing  B C = B
--      Case (just _) B C = C
--
--      sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool)
--      sample (just a) (just b) = true
--      sample (just a) nothing  = false
--      sample nothing           = true
--   @
--   The problem generated for the first clause of @sample@
--   with patterns @just a, just b@ would be:
--   @
--      lhsTel        = [A : Set, m : Maybe A]
--      lhsOutPat     = ["A", "m"]
--      lhsProblem    = Problem ["A" = _, "just a" = "a"]
--                              ["_", "just a"]
--                              ["just b"] []
--      lhsTarget     = "Case m Bool (Maybe A -> Bool)"
--   @
initLHSState
  :: Telescope             -- ^ The initial telescope @delta@ of parameters.
  -> [ProblemEq]           -- ^ The problem equations inherited from the parent clause (living in @delta@).
  -> [NamedArg A.Pattern]  -- ^ The user patterns.
  -> Type                  -- ^ The type the user patterns eliminate (living in @delta@).
  -> (LHSState a -> TCM a) -- ^ Continuation for when checking the patterns is complete.
  -> TCM (LHSState a)      -- ^ The initial LHS state constructed from the user patterns.
initLHSState :: forall a.
Telescope
-> [ProblemEq]
-> [NamedArg Pattern]
-> Type
-> (LHSState a -> TCM a)
-> TCM (LHSState a)
initLHSState Telescope
delta [ProblemEq]
eqs [NamedArg Pattern]
ps Type
a LHSState a -> TCM a
ret = do
  ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.init" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"initLHSState"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"delta = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"a     = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a)
    ]
  let problem :: Problem a
problem = [ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
forall a.
[ProblemEq]
-> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
Problem [ProblemEq]
eqs [NamedArg Pattern]
ps LHSState a -> TCM a
ret
      qs0 :: [NamedArg DeBruijnPattern]
qs0     = Telescope -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
delta

  LHSState a -> TCMT IO (LHSState a)
forall (m :: * -> *) a.
(PureTCM m, MonadError TCErr m, MonadTrace m,
 MonadFresh NameId m) =>
LHSState a -> m (LHSState a)
updateProblemRest (LHSState a -> TCMT IO (LHSState a))
-> LHSState a -> TCMT IO (LHSState a)
forall a b. (a -> b) -> a -> b
$ Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> Bool
-> LHSState a
forall a.
Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> Bool
-> LHSState a
LHSState Telescope
delta [NamedArg DeBruijnPattern]
qs0 Problem a
problem (ArgInfo -> Type -> Arg Type
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo
defaultArgInfo { argInfoModality = unitModality }) Type
a) [] Bool
False

-- | Try to move patterns from the problem rest into the problem.
--   Possible if type of problem rest has been updated to a function type.
updateProblemRest
  :: forall m a. (PureTCM m, MonadError TCErr m, MonadTrace m, MonadFresh NameId m)
  => LHSState a -> m (LHSState a)
updateProblemRest :: forall (m :: * -> *) a.
(PureTCM m, MonadError TCErr m, MonadTrace m,
 MonadFresh NameId m) =>
LHSState a -> m (LHSState a)
updateProblemRest st :: LHSState a
st@(LHSState Telescope
tel0 [NamedArg DeBruijnPattern]
qs0 p :: Problem a
p@(Problem [ProblemEq]
oldEqs [NamedArg Pattern]
ps LHSState a -> TCM a
ret) Arg Type
a [Maybe Int]
psplit Bool
ixsplit) = Telescope -> m (LHSState a) -> m (LHSState a)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel0 (m (LHSState a) -> m (LHSState a))
-> m (LHSState a) -> m (LHSState a)
forall a b. (a -> b) -> a -> b
$ do
  ps <- ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [NamedArg Pattern]
ps (Type -> m [NamedArg Pattern]) -> Type -> m [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
a
  reportSDoc "tc.lhs.imp" 20 $
    "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
  -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
  let m = [NamedArg Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([NamedArg Pattern] -> Int) -> [NamedArg Pattern] -> Int
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> Bool)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
-> (NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName))
-> NamedArg Pattern
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP) [NamedArg Pattern]
ps
  (TelV gamma b, boundary) <- telViewUpToPathBoundaryP m $ unArg a
  forM_ (zip ps (telToList gamma)) $ \(NamedArg Pattern
p, Dom' Term (ArgName, Type)
a) ->
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (NamedArg Pattern -> Dom' Term (ArgName, Type) -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg Pattern
p Dom' Term (ArgName, Type)
a) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern -> m () -> m ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
  let tel1      = [NamedArg Pattern] -> Telescope -> Telescope
useNamesFromPattern [NamedArg Pattern]
ps Telescope
gamma
      n         = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel1
      (ps1,ps2) = splitAt n ps
      tel       = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0 ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel1
      qs1       = Telescope -> Boundary -> [NamedArg DeBruijnPattern]
forall a.
DeBruijn a =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns Telescope
tel1 Boundary
boundary
      newEqs    = (Pattern -> Term -> Dom Type -> ProblemEq)
-> [Pattern] -> [Term] -> [Dom Type] -> [ProblemEq]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq
                    ((NamedArg Pattern -> Pattern) -> [NamedArg Pattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
ps1)
                    ((NamedArg DeBruijnPattern -> Term)
-> [NamedArg DeBruijnPattern] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> Term
patternToTerm (DeBruijnPattern -> Term)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs1)
                    (Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel1 [Dom Type] -> [NamedArg Pattern] -> [Dom Type]
forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
`useOriginFrom` [NamedArg Pattern]
ps1)
      tau       = Int -> Substitution' DeBruijnPattern
forall a. Int -> Substitution' a
raiseS Int
n
  reportSDoc "tc.lhs.problem" 10 $ addContext tel0 $ vcat
    [ "checking lhs -- updated split problem:"
    , nest 2 $ vcat
      [ "ps    =" <+> fsep (map prettyA ps)
      , "a     =" <+> prettyTCM a
      , "tel1  =" <+> prettyTCM tel1
      , "ps1   =" <+> fsep (map prettyA ps1)
      , "ps2   =" <+> fsep (map prettyA ps2)
      , "b     =" <+> addContext tel1 (prettyTCM b)
      ]
    ]
  reportSDoc "tc.lhs.problem" 60 $ addContext tel0 $ vcat
    [ nest 2 $ vcat
      [ "ps    =" <+> (text . show) ps
      , "a     =" <+> (text . show) a
      , "tel1  =" <+> (text . show) tel1
      , "ps1   =" <+> (text . show) ps1
      , "ps2   =" <+> (text . show) ps2
      , "b     =" <+> (text . show) b
      , "qs1   =" <+> fsep (map pretty qs1)
      ]
    ]
  return $ LHSState
    { _lhsTel     = tel
    , _lhsOutPat  = applySubst tau qs0 ++ qs1
    , _lhsProblem = Problem
                   { _problemEqs      = applyPatSubst tau oldEqs ++ newEqs
                   , _problemRestPats = ps2
                   , _problemCont     = ret
                   }
    , _lhsTarget  = a $> b
    , _lhsPartialSplit = psplit
    , _lhsIndexedSplit = ixsplit
    }