module Agda.TypeChecking.DisplayForm where
import Control.Applicative
import Control.Monad.Error
import Control.Monad.Trans.Maybe
import Data.Traversable (traverse)
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Level
import Agda.Utils.List
import Agda.Utils.Maybe
#include "../undefined.h"
import Agda.Utils.Impossible
displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
displayForm q vs = do
odfs <- defDisplay <$> getConstInfo q
unless (null odfs) $ verboseS "tc.display.top" 100 $ do
n <- getContextId
reportSLn "tc.display.top" 100 $
"displayForm: context = " ++ show n ++
", dfs = " ++ show (map openThingCtxIds odfs)
dfs <- catMaybes <$> mapM tryOpen odfs
scope <- getScope
ms <- do
ms <- mapM (runMaybeT . (`matchDisplayForm` vs)) dfs
return [ m | Just m <- ms, inScope scope m ]
unless (null odfs) $ reportSLn "tc.display.top" 100 $ unlines
[ "name : " ++ show q
, "displayForms: " ++ show dfs
, "arguments : " ++ show vs
, "matches : " ++ show ms
, "result : " ++ show (foldr (const . Just) Nothing ms)
]
return $ mhead ms
where
inScope _ _ = True
matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm
matchDisplayForm (Display _ ps v) vs
| length ps > length vs = mzero
| otherwise = do
us <- match ps $ raise 1 $ map unArg vs0
return $ applySubst (parallelS $ reverse us) v `apply` vs1
where
(vs0, vs1) = splitAt (length ps) vs
class Match a where
match :: a -> a -> MaybeT TCM [Term]
instance Match a => Match [a] where
match xs ys = concat <$> zipWithM match xs ys
instance Match a => Match (Arg a) where
match p v = match (unArg p) (unArg v)
instance Match a => Match (Elim' a) where
match p v =
case (p, v) of
(Proj f, Proj f') | f == f' -> return []
(Apply a, Apply a') -> match a a'
_ -> mzero
instance Match Term where
match p v = case (ignoreSharing p, ignoreSharing v) of
(Var 0 [], v) -> return [subst __IMPOSSIBLE__ v]
(Var i ps, Var j vs) | i == j -> match ps vs
(Def c ps, Def d vs) | c == d -> match ps vs
(Con c ps, Con d vs) | c == d -> match ps vs
(Lit l, Lit l') | l == l' -> return []
(p, v) | p == v -> return []
(p, Level l) -> match p =<< reallyUnLevelView l
(Sort ps, Sort pv) -> match ps pv
(p, Sort (Type v)) -> match p =<< reallyUnLevelView v
_ -> mzero
instance Match Sort where
match p v = case (p, v) of
(Type pl, Type vl) -> match pl vl
_ | p == v -> return []
_ -> mzero
instance Match Level where
match p v = do
p <- reallyUnLevelView p
v <- reallyUnLevelView v
match p v