module Agda.TypeChecking.DisplayForm where
import Prelude hiding (all)
import Control.Applicative
import Control.Monad
import Control.Monad.Trans (lift)
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.TypeChecking.Reduce (instantiate)
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Pretty ( prettyShow )
#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 (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 `catchError` \_ -> return []
unless (null odfs) $ verboseS "tc.display.top" 100 $ do
n <- getContextId
reportSLn "tc.display.top" 100 $
"displayForm for " ++ prettyShow q ++ ": context = " ++ show n ++
", dfs = " ++ show odfs
dfs <- catMaybes <$> mapM getLocal odfs
scope <- getScope
ms <- do
ms <- mapM (runMaybeT . (`matchDisplayForm` es)) dfs
return [ m | Just (d, m) <- ms, wellScoped scope d ]
unless (null odfs) $ 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 (ignoreSharing p, ignoreSharing 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 ignoreSharing v of
Var x [] -> case ots !!! x of
Just (WithOrigin o u) -> Arg (mapOrigin (replaceOrigin o) ai) u
Nothing -> __IMPOSSIBLE__
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 ignoreSharing 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)