module Agda.TypeChecking.DisplayForm where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Maybe
import Data.Traversable (traverse)
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Base (inverseScopeLookupName)
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
dtermToTerm :: DisplayTerm -> Term
dtermToTerm dt = case dt of
DWithApp d ds vs -> dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs)
DCon c args -> Con c $ map (fmap dtermToTerm) args
DDef f es -> Def f $ map (fmap dtermToTerm) es
DDot v -> v
DTerm v -> v
displayFormArities :: QName -> TCM [Int]
displayFormArities q = map (length . dfPats . openThing) . defDisplay <$> getConstInfo q
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 (headMaybe ms)
]
return $ headMaybe ms
where
inScope _ d | isWithDisplay d = True
inScope scope d = case hd d of
Just h -> not . null $ inverseScopeLookupName h scope
Nothing -> __IMPOSSIBLE__
isWithDisplay DWithApp{} = True
isWithDisplay _ = False
hd (DTerm (Def x _)) = Just x
hd (DTerm (Con x _)) = Just $ conName x
hd (DTerm (Shared p)) = hd (DTerm $ derefPtr p)
hd (DWithApp d _ _) = hd d
hd _ = Nothing
matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm
matchDisplayForm (Display _ ps v) vs
| length ps > length vs = mzero
| otherwise = do
let (vs0, vs1) = splitAt (length ps) vs
us <- match ps $ raise 1 $ map unArg vs0
return $ applySubst (parallelS $ reverse us) v `apply` vs1
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 [strengthen __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