module Agda.TypeChecking.With where
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Data.List
import Data.Maybe
import qualified Data.Traversable as Trav (traverse)
import Agda.Syntax.Common as Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Abstract
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS (isFlexiblePattern)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type
withFunctionType delta1 vs as delta2 b = do
(vas, b) <- addCtxTel delta1 $ do
reportSLn "tc.with.abstract" 20 $ "preparing for with-abstraction"
vs <- etaContract =<< normalise vs
reportSDoc "tc.with.abstract" 20 $ text " vs = " <+> prettyTCM vs
as <- etaContract =<< normalise as
reportSDoc "tc.with.abstract" 20 $ text " as = " <+> prettyTCM as
b <- return $ telePi_ delta2 b
reportSDoc "tc.with.abstract" 30 $ text "normalizing b = " <+> prettyTCM b
b <- normalise b
reportSDoc "tc.with.abstract" 30 $ text "eta-contracting b = " <+> prettyTCM b
b <- etaContract b
reportSDoc "tc.with.abstract" 20 $ text " b = " <+> prettyTCM b
reportSDoc "tc.with.abstract" 40 $
sep [ text "abstracting"
, nest 2 $ vcat $
[ text "vs = " <+> prettyTCM vs
, text "as = " <+> prettyTCM as
, text "b = " <+> prettyTCM b ]
]
reportSLn "tc.with.abstract" 50 $ " raw vs = " ++ show vs ++ "\n raw b = " ++ show b
return (zip vs as, b)
return $ telePi_ delta1 $ foldr (uncurry piAbstractTerm) b vas
buildWithFunction
:: QName
-> Type
-> [I.NamedArg Pattern]
-> Permutation
-> Nat
-> Nat
-> [A.SpineClause]
-> TCM [A.SpineClause]
buildWithFunction aux t qs perm n1 n cs = mapM buildWithClause cs
where
buildWithClause (A.Clause (A.SpineLHS i _ ps wps) rhs wh) = do
let (wps0, wps1) = genericSplitAt n wps
ps0 = map defaultNamedArg wps0
rhs <- buildRHS rhs
(ps1, ps2) <- genericSplitAt n1 <$> stripWithClausePatterns aux t qs perm ps
let result = A.Clause (A.SpineLHS i aux (ps1 ++ ps0 ++ ps2) wps1) rhs wh
reportSDoc "tc.with" 20 $ vcat
[ text "buildWithClause returns" <+> prettyA result
]
return result
buildRHS rhs@(A.RHS _) = return rhs
buildRHS rhs@A.AbsurdRHS = return rhs
buildRHS (A.WithRHS q es cs) = A.WithRHS q es <$>
mapM (A.spineToLhs <.> buildWithClause . A.lhsToSpine) cs
buildRHS (A.RewriteRHS qes rhs wh) = flip (A.RewriteRHS qes) wh <$> buildRHS rhs
stripWithClausePatterns
:: QName
-> Type
-> [I.NamedArg Pattern]
-> Permutation
-> [A.NamedArg A.Pattern]
-> TCM [A.NamedArg A.Pattern]
stripWithClausePatterns f t qs perm ps = do
ps <- expandPatternSynonyms ps
psi <- insertImplicitPatternsT ExpandLast ps t
reportSDoc "tc.with.strip" 10 $ vcat
[ text "stripping patterns"
, nest 2 $ text "t = " <+> prettyTCM t
, nest 2 $ text "psi = " <+> fsep (punctuate comma $ map prettyA psi)
, nest 2 $ text "qs = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
]
ps' <- strip (Def f []) t psi $ numberPatVars perm qs
let psp = permute perm ps'
reportSDoc "tc.with.strip" 10 $ vcat
[ nest 2 $ text "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
, nest 2 $ text "psp = " <+> fsep (punctuate comma $ map prettyA $ psp)
]
if True then return psp else do
forM_ (permute (droppedP perm) ps') $ \ p -> setCurrentRange p $ do
reportSDoc "tc.with.strip" 10 $ text "warning: dropped pattern " <+> prettyA p
reportSDoc "tc.with.strip" 60 $ text $ show p
case namedArg p of
A.DotP info e -> case unScope e of
A.Underscore{} -> return ()
e | getRange info /= noRange -> typeError $ GenericError $
"This inaccessible pattern is never checked, so only _ allowed here"
_ -> return ()
_ -> return ()
return psp
where
strip
:: Term
-> Type
-> [A.NamedArg A.Pattern]
-> [I.NamedArg DeBruijnPattern]
-> TCM [A.NamedArg A.Pattern]
strip self t [] qs@(_ : _) = do
ps <- insertImplicitPatternsT ExpandLast [] t
if null ps then
typeError $ GenericError $ "Too few arguments given in with-clause"
else strip self t ps qs
strip _ _ ps [] = do
let implicit (A.WildP{}) = True
implicit (A.ConP ci _ _) = patOrigin ci == ConPImplicit
implicit _ = False
unless (all (implicit . namedArg) ps) $
typeError $ GenericError $ "Too many arguments given in with-clause"
return []
strip self t ps0@(p0 : ps) qs0@(q : qs) = do
p <- expandLitPattern p0
reportSDoc "tc.with.strip" 15 $ vcat
[ text "strip"
, nest 2 $ text "ps0 =" <+> fsep (punctuate comma $ map prettyA ps0)
, nest 2 $ text "exp =" <+> prettyA p
, nest 2 $ text "qs0 =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs0)
, nest 2 $ text "t =" <+> prettyTCM t
]
let failDotPat = do
d <- prettyA p
typeError $ GenericError $
"Inaccessible (dotted) patterns from the parent clause must " ++
"also be inaccessible in the with clause, when checking the " ++
"pattern " ++ show d ++ ","
case namedArg q of
ProjP d -> case A.isProjP p of
Just d' -> do
d' <- getOriginalProjection d'
if d /= d' then mismatch else do
t <- reduce t
(self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t d
strip self1 t1 ps qs
Nothing -> mismatch
VarP (i, _x) -> do
ps <- intro1 t $ \ t -> strip (self `apply1` var i) t ps qs
return $ p : ps
DotP v -> case namedArg p of
A.DotP _ _ -> ok p
A.WildP _ -> ok p
A.ConP ci _ _ | patOrigin ci == ConPImplicit -> okFlex p
p'@A.ConP{} -> ifM (isFlexiblePattern p') (okFlex p) failDotPat
p@(A.PatternSynP pi' c' [ps']) -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
_ -> failDotPat
where
okFlex = ok . makeImplicitP
ok p = do
t' <- piApply1 t v
(p :) <$> strip (self `apply1` v) t' ps qs
q'@(ConP c ci qs') -> do
reportSDoc "tc.with.strip" 60 $
text "parent pattern is constructor " <+> prettyTCM c
(a, b) <- mustBePi t
case namedArg p of
A.DotP{} -> ifNotM (isFlexiblePattern q') mismatch $ do
maybe __IMPOSSIBLE__ (\ p -> strip self t (p : ps) qs0) =<< do
expandImplicitPattern' (unDom a) $ makeImplicitP p
A.WildP{} | Just _ <- conPRecord ci -> do
maybe __IMPOSSIBLE__ (\ p -> strip self t (p : ps) qs0) =<<
expandImplicitPattern' (unDom a) p
A.ConP _ (A.AmbQ cs') ps' -> do
c <- (`withRangeOf` c) <$> do getConForm $ conName c
cs' <- mapM getConForm cs'
unless (elem c cs') mismatch
Def d es <- ignoreSharing <$> normalise (unEl $ unDom a)
let us = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
Defn {defType = ct, theDef = Constructor{conPars = np}} <- getConInfo c
let ct' = ct `apply` genericTake np us
TelV tel' _ <- telView ct'
reportSDoc "tc.with.strip" 20 $
vcat [ text "ct = " <+> prettyTCM ct
, text "ct' = " <+> prettyTCM ct'
, text "np = " <+> text (show np)
, text "us = " <+> prettyList (map prettyTCM us)
, text "us' = " <+> prettyList (map prettyTCM $ genericTake np us)
]
let v = Con c [ Arg info (var i) | (i, Arg info _) <- zip (downFrom $ size qs') qs' ]
t' = tel' `abstract` absApp (raise (size tel') b) v
reportSDoc "tc.with.strip" 15 $ sep
[ text "inserting implicit"
, nest 2 $ prettyList $ map prettyA (ps' ++ ps)
, nest 2 $ text ":" <+> prettyTCM t'
]
psi' <- insertImplicitPatterns ExpandLast ps' tel'
unless (size psi' == size tel') $ typeError $
WrongNumberOfConstructorArguments (conName c) (size tel') (size psi')
strip (self `apply1` v) t' (psi' ++ ps) (qs' ++ qs)
p@(A.PatternSynP pi' c' ps') -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
p -> do
reportSDoc "tc.with.strip" 60 $
text $ "with clause pattern is " ++ show p
mismatch
LitP lit -> case namedArg p of
A.LitP lit' | lit == lit' -> do
(a, b) <- mustBePi t
let v = Lit lit
strip (self `apply1` v) (b `absApp` v) ps qs
p@(A.PatternSynP pi' c' [ps']) -> do
reportSDoc "impossible" 10 $
text "stripWithClausePatterns: encountered pattern synonym " <+> prettyA p
__IMPOSSIBLE__
_ -> mismatch
where
mismatch = typeError $
WithClausePatternMismatch (namedArg p0) (snd <$> namedArg q)
makeImplicitP :: A.NamedArg A.Pattern -> A.NamedArg A.Pattern
makeImplicitP = updateNamedArg $ const $ A.WildP patNoRange
withDisplayForm
:: QName
-> QName
-> Telescope
-> Telescope
-> Nat
-> [I.NamedArg Pattern]
-> Permutation
-> Permutation
-> TCM DisplayForm
withDisplayForm f aux delta1 delta2 n qs perm@(Perm m _) lhsPerm = do
let arity0 = n + size delta1 + size delta2
topArgs <- raise arity0 <$> getContextArgs
let top = length topArgs
arity = arity0 + top
wild <- freshNoName_ <&> \ x -> Def (qualify_ x) []
let
tqs0 = patsToElims lhsPerm qs
(ys0, ys1) = splitAt (size delta1) $ permute perm $ downFrom m
ys = reverse $ map Just ys0 ++ replicate n Nothing ++ map Just ys1
rho = sub top ys wild
tqs = applySubst rho tqs0
es = map (Apply . fmap DTerm) topArgs ++ tqs
withArgs = map var $ take n $ downFrom $ size delta2 + n
dt = DWithApp (DDef f es) (map DTerm withArgs) []
let display = Display arity (replicate arity $ var 0) dt
let addFullCtx = addCtxTel delta1
. flip (foldr addContext) (for [1..n] $ \ i -> "w" ++ show i)
. addCtxTel delta2
reportSDoc "tc.with.display" 20 $ vcat
[ text "withDisplayForm"
, nest 2 $ vcat
[ text "f =" <+> text (show f)
, text "aux =" <+> text (show aux)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> do addCtxTel delta1 $ prettyTCM delta2
, text "n =" <+> text (show n)
, text "perm =" <+> text (show perm)
, text "top =" <+> do addFullCtx $ prettyTCM topArgs
, text "qs =" <+> text (show qs)
, text "dt =" <+> do addFullCtx $ prettyTCM dt
, text "ys =" <+> text (show ys)
, text "raw =" <+> text (show display)
, text "qsToTm =" <+> prettyTCM tqs0
, text "sub qs =" <+> prettyTCM tqs
]
]
return display
where
sub top ys wild = map term [0 .. m 1] ++# raiseS (length qs)
where
term i = maybe wild var $ findIndex (Just i ==) ys
patsToElims :: Permutation -> [I.NamedArg Pattern] -> [I.Elim' DisplayTerm]
patsToElims perm ps = toElims $ numberPatVars perm ps
where
toElims :: [I.NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm]
toElims = map $ toElim . fmap namedThing
toElim :: I.Arg DeBruijnPattern -> I.Elim' DisplayTerm
toElim (Common.Arg ai p) = case p of
ProjP d -> I.Proj d
p -> I.Apply $ Common.Arg ai $ toTerm p
toTerms :: [I.NamedArg DeBruijnPattern] -> [I.Arg DisplayTerm]
toTerms = map $ fmap $ toTerm . namedThing
toTerm :: DeBruijnPattern -> DisplayTerm
toTerm p = case p of
ProjP d -> DDef d []
VarP (i, x) -> DTerm $ var i
DotP t -> DDot $ t
ConP c _ ps -> DCon c $ toTerms ps
LitP l -> DTerm $ Lit l