module Agda.TypeChecking.DisplayForm where
import Prelude hiding (all)
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Maybe
import Data.Foldable (all)
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names
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
import Agda.Utils.Except
#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) <$> getDisplayForms q
displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
displayForm q vs = do
odfs <- getDisplayForms q `catchError` \_ -> return []
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 (d, m) <- ms, wellScoped scope d ]
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
wellScoped scope (Display _ _ d)
| isWithDisplay d = True
| otherwise = all (inScope scope) $ namesIn d
inScope scope x = not $ null $ inverseScopeLookupName x scope
isWithDisplay DWithApp{} = True
isWithDisplay _ = False
matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM (DisplayForm, DisplayTerm)
matchDisplayForm d@(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 (d, 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