{-# LANGUAGE CPP #-}

module Agda.TypeChecking.DisplayForm where

import Control.Applicative
import Control.Monad
import Control.Monad.Error

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.Syntax.Scope.Base
import Agda.Utils.Size

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

displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
displayForm c vs = do
    odfs  <- defDisplay <$> getConstInfo c
    unless (null odfs) $ verboseS "tc.display.top" 30 $ do
      n <- getContextId
      let fvs = map (\(OpenThing n _) -> n) odfs
      reportSLn "" 0 $ "displayForm: context = " ++ show n ++ ", dfs = " ++ show fvs
    dfs	  <- do
      xs <- mapM tryOpen odfs
      return [ df | Just df <- xs ]
    scope <- getScope
    let matches dfs vs = [ m | Just m <- map (flip matchDisplayForm vs) dfs, inScope scope m ]
    -- Not safe when printing non-terminating terms.
    -- (nfdfs, us) <- normalise (dfs, vs)
    unless (null odfs) $ reportSLn "tc.display.top" 20 $ unlines
      [ "displayForms: " ++ show dfs
      , "arguments   : " ++ show vs
      , "matches     : " ++ show (matches dfs vs)
      ]
    return $ foldr (const . Just) Nothing $ matches dfs vs -- ++ matches nfdfs us
  `catchError` \_ -> return Nothing
  where
    inScope _ _ = True  -- TODO: distinguish between with display forms and other display forms
--     inScope scope d = case hd d of
--       Just h  -> maybe False (const True) $ inverseScopeLookupName h scope
--       Nothing -> __IMPOSSIBLE__ -- TODO: currently all display forms have heads
    hd (DTerm (Def x _))    = Just x
    hd (DTerm (Con x _))    = Just x
    hd (DWithApp (d : _) _) = hd d
    hd _		    = Nothing

matchDisplayForm :: DisplayForm -> Args -> Maybe DisplayTerm
matchDisplayForm (Display n ps v) vs
  | length ps > length vs = Nothing
  | otherwise             = do
    us <- match n ps $ raise 1 (map unArg vs0)
    return $ substs (reverse us) v `apply` vs1
  where
    (vs0, vs1) = splitAt (length ps) vs

class Match a where
  match :: Nat -> a -> a -> Maybe [Term]

instance Match a => Match [a] where
  match n xs ys = concat <$> zipWithM (match n) xs ys

instance Match a => Match (Arg a) where
  match n p v = match n (unArg p) (unArg v)

instance Match Term where
  match n p v = case (p, v) of
    (Var 0 [], v)                  -> return [subst __IMPOSSIBLE__ v]
    (Var i ps, Var j vs) | i == j  -> match n ps vs
    (Def c ps, Def d vs) | c == d  -> match n ps vs
    (Con c ps, Con d vs) | c == d  -> match n ps vs
    (Lit l, Lit l')      | l == l' -> return []
    (p, v)               | p == v  -> return []
    _                              -> fail ""