{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.DisplayForm where
import Prelude hiding (all)
import Control.Monad
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Maybe
import Data.Foldable (all)
import qualified Data.Set as Set
import qualified Data.Map as Map
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.TypeChecking.Reduce (instantiate)
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
dtermToTerm :: DisplayTerm -> Term
dtermToTerm dt = case dt of
DWithApp d ds es ->
dtermToTerm d `apply` map (defaultArg . dtermToTerm) ds `applyE` es
DCon c ci args -> Con c ci $ map (Apply . 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 . dget) <$> getDisplayForms q
displayForm :: QName -> Elims -> TCM (Maybe DisplayTerm)
displayForm q es = do
odfs <- getDisplayForms q
if (null odfs) then do
reportSLn "tc.display.top" 101 $ "no displayForm for " ++ prettyShow q
return Nothing
else do
verboseS "tc.display.top" 100 $ unlessDebugPrinting $ do
cps <- view eCheckpoints
cxt <- getContextTelescope
reportSDoc "tc.display.top" 100 $ return $ vcat
[ text "displayForm for" <+> pretty q
, nest 2 $ text "cxt =" <+> pretty cxt
, nest 2 $ text "cps =" <+> vcat (map pretty (Map.toList cps))
, nest 2 $ text "dfs =" <+> vcat (map pshow odfs) ]
dfs <- catMaybes <$> mapM tryGetOpen odfs
scope <- getScope
ms <- do
ms <- mapM (runMaybeT . (`matchDisplayForm` es)) dfs
return [ m | Just (d, m) <- ms, wellScoped scope d ]
unlessDebugPrinting $ reportSLn "tc.display.top" 100 $ unlines
[ "name : " ++ prettyShow q
, "displayForms: " ++ show dfs
, "arguments : " ++ show es
, "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 -> Elims -> MaybeT TCM (DisplayForm, DisplayTerm)
matchDisplayForm d@(Display _ ps v) es
| length ps > length es = mzero
| otherwise = do
let (es0, es1) = splitAt (length ps) es
us <- reverse <$> do match ps $ raise 1 es0
return (d, substWithOrigin (parallelS $ map woThing us) us v `applyE` es1)
class Match a where
match :: a -> a -> MaybeT TCM [WithOrigin 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 = map (setOrigin (getOrigin 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 = lift (instantiate v) >>= \ v -> case (p, v) of
(Var 0 [], v) -> return [ WithOrigin Inserted $ 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
class SubstWithOrigin a where
substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a
instance SubstWithOrigin a => SubstWithOrigin [a] where
substWithOrigin rho ots = map (substWithOrigin rho ots)
instance SubstWithOrigin (Arg a) => SubstWithOrigin (Elim' a) where
substWithOrigin rho ots (Apply arg) = Apply $ substWithOrigin rho ots arg
substWithOrigin rho ots e@Proj{} = e
instance SubstWithOrigin (Arg Term) where
substWithOrigin rho ots (Arg ai v) =
case v of
Var x [] -> case ots !!! x of
Just (WithOrigin o u) -> Arg (mapOrigin (replaceOrigin o) ai) u
Nothing -> Arg ai $ applySubst rho v
Con c ci args -> Arg ai $ Con c ci $ substWithOrigin rho ots args
Def q es -> Arg ai $ Def q $ substWithOrigin rho ots es
_ -> Arg ai $ applySubst rho v
where
replaceOrigin _ UserWritten = UserWritten
replaceOrigin o _ = o
instance SubstWithOrigin Term where
substWithOrigin rho ots v =
case v of
Con c ci args -> Con c ci $ substWithOrigin rho ots args
Def q es -> Def q $ substWithOrigin rho ots es
_ -> applySubst rho v
instance SubstWithOrigin DisplayTerm where
substWithOrigin rho ots dt =
case dt of
DTerm v -> DTerm $ substWithOrigin rho ots v
DDot v -> DDot $ applySubst rho v
DDef q es -> DDef q $ substWithOrigin rho ots es
DCon c ci args -> DCon c ci $ substWithOrigin rho ots args
DWithApp t ts es -> DWithApp
(substWithOrigin rho ots t)
(substWithOrigin rho ots ts)
(substWithOrigin rho ots es)
instance SubstWithOrigin (Arg DisplayTerm) where
substWithOrigin rho ots (Arg ai dt) =
case dt of
DTerm v -> fmap DTerm $ substWithOrigin rho ots $ Arg ai v
DDot v -> Arg ai $ DDot $ applySubst rho v
DDef q es -> Arg ai $ DDef q $ substWithOrigin rho ots es
DCon c ci args -> Arg ai $ DCon c ci $ substWithOrigin rho ots args
DWithApp t ts es -> Arg ai $ DWithApp
(substWithOrigin rho ots t)
(substWithOrigin rho ots ts)
(substWithOrigin rho ots es)