{-# LANGUAGE CPP           #-}

module Agda.TypeChecking.Rules.LHS.ProblemRest where

import Control.Arrow (first, second)
import Control.Monad

import Data.Functor ((<$))
import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract.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.List
import Agda.Utils.Size
import Agda.Utils.Permutation

#include "undefined.h"
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 ps tel = telFromList (zipWith ren ps telList ++ telRemaining)
  where
    telList = telToList tel
    telRemaining = drop (length ps) telList -- telescope entries beyond patterns
    ren (Arg ai (Named nm p)) dom@(Dom info (y, a)) =
      case 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 x) | not (isNoName x)
                 , visible info || (getOrigin ai == UserWritten && nm == Nothing) ->
          Dom info (nameToArgName x, a)
        A.PatternSynP{} -> __IMPOSSIBLE__  -- ensure there are no syns left
        -- Andreas, 2016-05-10, issue 1848: if context variable has no name, call it "x"
        _ | visible info && isNoName y -> Dom info (stringToArgName "x", a)
          | otherwise                  -> dom

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

-- | Are there any untyped user patterns left?
noProblemRest :: Problem a -> Bool
noProblemRest (Problem _ rp _) = null 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 ["_", "just a"] [] [] []
--      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 delta eqs ps a ret = do
  let problem = Problem eqs ps ret
      qs0     = teleNamedArgs delta

  updateProblemRest $ LHSState delta qs0 problem (defaultArg a)

-- | 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 :: LHSState a -> TCM (LHSState a)
updateProblemRest st@(LHSState tel0 qs0 p@(Problem oldEqs ps ret) a) = do
  ps <- addContext tel0 $ insertImplicitPatternsT ExpandLast ps $ unArg a
  reportSDoc "tc.lhs.imp" 20 $
    text "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
  -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
  let m = length $ takeWhile (isNothing . A.maybePostfixProjP) ps
  TelV gamma b <- telViewUpTo m $ unArg a
  forM_ (zip ps (telToList gamma)) $ \(p, a) ->
    unless (sameHiding p a) $ typeError WrongHidingInLHS
  let tel1      = useNamesFromPattern ps gamma
      n         = size tel1
      (ps1,ps2) = splitAt n ps
      tel       = telFromList $ telToList tel0 ++ telToList tel1
      qs1       = teleNamedArgs tel1
      newEqs    = zipWith3 ProblemEq
                    (map namedArg ps1)
                    (map (patternToTerm . namedArg) qs1)
                    (flattenTel tel1 `useOriginFrom` ps1)
      tau       = raiseS n
  reportSDoc "tc.lhs.problem" 10 $ addContext tel0 $ vcat
    [ text "checking lhs -- updated split problem:"
    , nest 2 $ vcat
      [ text "ps    =" <+> fsep (map prettyA ps)
      , text "a     =" <+> prettyTCM a
      , text "tel1  =" <+> prettyTCM tel1
      , text "ps1   =" <+> fsep (map prettyA ps1)
      , text "ps2   =" <+> fsep (map prettyA ps2)
      , text "b     =" <+> addContext tel1 (prettyTCM b)
      ]
    ]
  reportSDoc "tc.lhs.problem" 60 $ addContext tel0 $ vcat
    [ nest 2 $ vcat
      [ text "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
    }