{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Patterns.Match where

import Control.Monad
import Data.Monoid
import Data.Traversable

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal

import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive

import Agda.Utils.Monad

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

-- | If matching is inconclusive (@DontKnow@) we want to know whether
--   it is due to a particular meta variable.
data Match = Yes [Term] | No | DontKnow (Maybe MetaId)

instance Monoid Match where
    mempty = Yes []

    Yes us     `mappend` Yes vs		  = Yes (us ++ vs)
    Yes _      `mappend` No		  = No
    Yes _      `mappend` DontKnow m	  = DontKnow m
    No	       `mappend` _		  = No

    -- Nothing means blocked by a variable.  In this case no instantiation of
    -- meta-variables will make progress.
    DontKnow _ `mappend` DontKnow Nothing = DontKnow Nothing

    -- One could imagine DontKnow _ `mappend` No = No, but would break the
    -- equivalence to case-trees.
    DontKnow m `mappend` _		  = DontKnow m

matchPatterns :: MonadTCM tcm => [Arg Pattern] -> [Arg Term] -> tcm (Match, [Arg Term])
matchPatterns ps vs =
    do	(ms,vs) <- unzip <$> zipWithM' matchPattern ps vs
	return (mconcat ms, vs)

matchPattern :: MonadTCM tcm => Arg Pattern -> Arg Term -> tcm (Match, Arg Term)
matchPattern (Arg h' (VarP _))	  arg@(Arg _ v) = return (Yes [v], arg)
matchPattern (Arg _  (DotP _))    arg@(Arg _ v) = return (Yes [v], arg)
matchPattern (Arg h' (LitP l))	  arg@(Arg h v) = do
    w <- reduceB v
    let v = ignoreBlocking w
    case w of
	NotBlocked (Lit l')
	    | l == l'          -> return (Yes [], Arg h v)
	    | otherwise        -> return (No, Arg h v)
	NotBlocked (MetaV x _) -> return (DontKnow $ Just x, Arg h v)
	Blocked x _            -> return (DontKnow $ Just x, Arg h v)
	_                      -> return (DontKnow Nothing, Arg h v)
matchPattern (Arg h' (ConP c ps))     (Arg h v) =
    do	w <- traverse constructorForm =<< reduceB v
        -- Unfold delayed (corecursive) definitions one step. This is
        -- only necessary if c is a coinductive constructor, but
        -- 1) it does not hurt to do it all the time, and
        -- 2) whatInduction c sometimes crashes because c may point to
        --    an axiom at this stage (if we are checking the
        --    projection functions for a record type).
        w <- case w of
               NotBlocked (Def f args) ->
                 unfoldDefinition True reduceB (Def f []) f args
                   -- reduceB is used here because some constructors
                   -- are actually definitions which need to be
                   -- unfolded (due to open public).
               _ -> return w
        let v = ignoreBlocking w
	case w of
	  NotBlocked (Con c' vs)
	    | c == c'             -> do
		(m, vs) <- matchPatterns ps vs
		return (m, Arg h $ Con c' vs)
	    | otherwise           -> return (No, Arg h v)
	  NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg h v)
	  Blocked x _             -> return (DontKnow $ Just x, Arg h v)
          _                       -> return (DontKnow Nothing, Arg h v)