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.Free
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.Pretty (prettyShow)
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
splitTelForWith
:: Telescope
-> Type
-> [Type]
-> [Term]
-> ( Telescope
, Telescope
, Permutation
, Type
, [Type]
, [Term]
)
splitTelForWith delta t as vs = let
fv = allFreeVars as
SplitTel delta1 delta2 perm = splitTelescope fv delta
pi = renaming (reverseP perm)
rho = strengthenS __IMPOSSIBLE__ $ size delta2
rhopi = composeS rho pi
t' = applySubst pi t
as' = applySubst rhopi as
vs' = applySubst pi vs
in (delta1, delta2, perm, t', as', vs')
withFunctionType
:: Telescope
-> [Term]
-> [Type]
-> Telescope
-> Type
-> TCM Type
withFunctionType delta1 vs as delta2 b = addCtxTel delta1 $ do
reportSLn "tc.with.abstract" 20 $ "preparing for with-abstraction"
as <- etaContract =<< normalise as
reportSDoc "tc.with.abstract" 20 $ text " as = " <+> prettyTCM as
d2b <- return $ telePi_ delta2 b
reportSDoc "tc.with.abstract" 30 $ text "normalizing d2b = " <+> prettyTCM d2b
d2b <- normalise d2b
reportSDoc "tc.with.abstract" 30 $ text "eta-contracting d2b = " <+> prettyTCM d2b
d2b <- etaContract d2b
reportSDoc "tc.with.abstract" 20 $ text " d2b = " <+> prettyTCM d2b
let n2 = size delta2
TelV delta2 b <- telViewUpTo n2 d2b
addContext delta2 $ do
vs <- etaContract =<< normalise vs
reportSDoc "tc.with.abstract" 20 $ text " vs = " <+> prettyTCM vs
reportSDoc "tc.with.abstract" 40 $
sep [ text "abstracting"
, nest 2 $ vcat $
[ text "vs = " <+> prettyTCM vs
, text "as = " <+> escapeContext n2 (prettyTCM as)
, text "delta2 = " <+> escapeContext n2 (prettyTCM delta2)
, text "b = " <+> prettyTCM b ]
]
reportSLn "tc.with.abstract" 50 $ " raw vs = " ++ show vs ++ "\n raw b = " ++ show b
let TelV wtel0 b0 = telView'UpTo (size as) $
foldr (uncurry piAbstractTerm) b $ zip vs $ raise n2 as
let wtel = applySubst (strengthenS __IMPOSSIBLE__ n2) wtel0
let m = n2 + size wtel
let rho = (map var $ [n2..m1] ++ [0..n21]) ++# raiseS m
let b' = applySubst rho b0
let delta2flat = flattenTel delta2
let abstrvs t = foldl (flip abstractTerm) t $ zipWith raise [0..] vs
let delta2abs = abstrvs delta2flat
let delta2flat' = applySubst rho delta2abs
let delta2' = unflattenTel (teleNames delta2) delta2flat'
let ty = telePi_ delta1 $ telePi_ wtel $ telePi_ delta2' b'
reportSDoc "tc.with.abstract" 20 $ sep $
[ text "finished with-abstraction"
, text " wtel0 = " <+> prettyTCM wtel0
, text " wtel = " <+> do escapeContext n2 $ prettyTCM wtel
, text " b0 = " <+> addContext wtel (prettyTCM b0)
, text " b' = " <+> do escapeContext n2 $ addContext wtel $ addContext delta2 $ prettyTCM b'
, text " delta2flat = " <+> prettyTCM delta2flat
, text " delta2flat' = " <+> do addContext wtel $ prettyTCM delta2flat'
, text " delta2' = " <+> do escapeContext n2 $ addContext wtel $ prettyTCM delta2'
, text " ty = " <+> do escapeContext n2 $ escapeContext (size delta1) $ prettyTCM delta2'
]
return ty
buildWithFunction
:: QName
-> QName
-> Type
-> [I.NamedArg Pattern]
-> Permutation
-> Nat
-> Nat
-> [A.SpineClause]
-> TCM [A.SpineClause]
buildWithFunction f 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 f 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
-> QName
-> Type
-> [I.NamedArg Pattern]
-> Permutation
-> [A.NamedArg A.Pattern]
-> TCM [A.NamedArg A.Pattern]
stripWithClausePatterns parent 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 parent []) 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 "self=" <+> prettyTCM self
, 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
self' = tel' `abstract` apply1 (raise (size tel') self) 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' 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)
++ map (Just . (m +)) [0..top1]
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 =" <+> sep (map (prettyTCM . namedArg) qs)
, text "qsToTm =" <+> prettyTCM tqs0
, text "ys =" <+> text (show ys)
, text "rho =" <+> text (prettyShow rho)
, text "qs[rho]=" <+> do addFullCtx $ prettyTCM tqs
, text "dt =" <+> do addFullCtx $ prettyTCM dt
]
]
reportSDoc "tc.with.display" 70 $ nest 2 $ vcat
[ text "raw =" <+> text (show display)
]
return display
where
sub top ys wild = parallelS $ map term [0 .. m + top 1]
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