{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Rules.LHS.Instantiate where

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

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

import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.Split ( asView )

import Agda.Utils.Permutation
import Agda.Utils.Size

#include "../../../undefined.h"
import Agda.Utils.Impossible

-- | Instantiate a telescope with a substitution. Might reorder the telescope.
--   @instantiateTel (Γ : Tel)(σ : Γ --> Γ) = Γσ~@
--   Monadic only for debugging purposes.
instantiateTel :: MonadTCM tcm => Substitution -> Telescope -> tcm (Telescope, Permutation, [Term], [Type])
instantiateTel s tel = liftTCM $ do

  reportSDoc "tc.lhs.inst" 10 $ sep
    [ text "instantiateTel "
    , nest 2 $ fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) s
    , nest 2 $ prettyTCM tel
    ]

  -- Shrinking permutation (removing Justs) (and its complement, and reverse)
  let ps  = Perm (size s) [ i | (i, Nothing) <- zip [0..] $ reverse s ]
      psR = reverseP ps
      psC = Perm (size s) [ i | (i, Just _)  <- zip [0..] $ reverse s ]

  reportS "tc.lhs.inst" 10 $ unlines
    [ "ps  = " ++ show ps
    , "psR = " ++ show psR
    , "psC = " ++ show psC
    ]

  -- s' : Substitution Γσ
  let s' = rename psR s

  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
    text "s'   =" <+> fsep (punctuate comma $ map (maybe (text "_") prettyTCM) s')

  -- rho : [Tm Γσ]Γ
  let rho = mkSubst s'

  -- tel1 : [Type Γ]Γ
  let tel1   = flattenTel tel
      names1 = teleNames tel

  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
    text "tel1 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel1)

  -- tel2 : [Type Γσ]Γ
  let tel2 = substs rho tel1

  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
    text "tel2 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel2)

  -- tel3 : [Type Γσ]Γσ
  tel3 <- instantiateFull $ permute ps tel2
  let names3 = permute ps names1

  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
    text "tel3 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel3)

  -- p : Permutation (Γσ -> Γσ~)
  let p = reorderTel tel3

  reportSLn "tc.lhs.inst" 10 $ "p   = " ++ show p

  -- rho' : [Term Γσ~]Γσ
  let rho' = renaming (reverseP p)

  -- tel4 : [Type Γσ~]Γσ~
  let tel4   = substs rho' (permute p tel3)
      names4 = permute p names3

  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
    text "tel4 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel4)

  -- tel5 = Γσ~
  let tel5 = unflattenTel names4 tel4

  reportSDoc "tc.lhs.inst" 15 $ nest 2 $
    text "tel5 =" <+> prettyTCM tel5

  -- remember the types of the instantiations
  -- itypes : [Type Γσ~]Γ*
  let itypes = substs rho' $ permute psC $ map unArg tel2

  return (tel5, composeP p ps, substs rho' rho, itypes)
  where

    -- Turn a Substitution ([Maybe Term]) into a substitution ([Term])
    -- (The result is an infinite list)
    mkSubst :: [Maybe Term] -> [Term]
    mkSubst s = rho 0 s'
      where s'  = s ++ repeat Nothing
	    rho i (Nothing : s) = Var i [] : rho (i + 1) s
	    rho i (Just u  : s) = u : rho i s
	    rho _ []		= __IMPOSSIBLE__

-- | Produce a nice error message when splitting failed
nothingToSplitError :: Problem -> TCM a
nothingToSplitError (Problem ps _ tel) = splitError ps tel
  where
    splitError []	EmptyTel    = __IMPOSSIBLE__
    splitError (_:_)	EmptyTel    = __IMPOSSIBLE__
    splitError []	ExtendTel{} = __IMPOSSIBLE__
    splitError (p : ps) (ExtendTel a tel)
      | isBad p   = traceCall (CheckPattern (strip p) EmptyTel (unArg a)) $ case strip p of
	  A.DotP _ e -> typeError $ UninstantiatedDotPattern e
	  p	     -> typeError $ IlltypedPattern p (unArg a)
      | otherwise = underAbstraction a tel $ \tel -> splitError ps tel
      where
	strip = snd . asView . namedThing . unArg
	isBad p = case strip p of
	  A.DotP _ _   -> True
	  A.ConP _ _ _ -> True
	  A.LitP _     -> True
	  _	       -> False