summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Translation/InternalToAbstract.hs')
-rw-r--r--src/full/Agda/Syntax/Translation/InternalToAbstract.hs961
1 files changed, 479 insertions, 482 deletions
diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
index 2091338..ef2664f 100644
--- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs
@@ -1,11 +1,7 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}
{-|
@@ -21,23 +17,24 @@
-}
module Agda.Syntax.Translation.InternalToAbstract
( Reify(..)
- , NamedClause
+ , NamedClause(..)
, reifyPatterns
) where
-import Prelude hiding (mapM_, mapM)
-import Control.Applicative
+import Prelude hiding (mapM_, mapM, null)
+import Control.Applicative hiding (empty)
import Control.Monad.State hiding (mapM_, mapM)
import Control.Monad.Reader hiding (mapM_, mapM)
import Data.Foldable (foldMap)
-import Data.List hiding (sort)
+import Data.List hiding (null, sort)
import qualified Data.Map as Map
import Data.Maybe
-import Data.Monoid
+import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend)
import Data.Set (Set)
import qualified Data.Set as Set
-import Data.Traversable as Trav
+import Data.Traversable (traverse, mapM)
+import qualified Data.Traversable as Trav
import Agda.Syntax.Literal
import Agda.Syntax.Position
@@ -51,7 +48,7 @@ import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Scope.Base (isNameInScope, inverseScopeLookupName)
-import Agda.TypeChecking.Monad as M hiding (MetaInfo, tick)
+import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Records
@@ -64,13 +61,19 @@ import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.DropArgs
+import Agda.Interaction.Options ( optPostfixProjections )
+
import Agda.Utils.Except ( MonadError(catchError) )
+import Agda.Utils.Function
+import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.Permutation
-import Agda.Utils.Pretty
+import Agda.Utils.Pretty hiding ((<>))
+import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
@@ -79,44 +82,38 @@ import Agda.Utils.Impossible
-- Composition of reified applications ------------------------------------
+-- | Drops hidden arguments unless --show-implicit.
napps :: Expr -> [NamedArg Expr] -> TCM Expr
-napps e args = do
- dontShowImp <- not <$> showImplicitArguments
- let apply1 e arg | notVisible arg && dontShowImp = e
- | otherwise = App exprInfo e arg
- foldl' apply1 e <$> reify args
+napps e = nelims e . map I.Apply
+-- | Drops hidden arguments unless --show-implicit.
apps :: Expr -> [Arg Expr] -> TCM Expr
-apps e args = napps e $ map (fmap unnamed) args
-
-reifyApp :: Expr -> [Arg Term] -> TCM Expr
-reifyApp e vs = apps e =<< reifyIArgs vs
-
-reifyIArg :: Reify i a => Arg i -> TCM (Arg a)
-reifyIArg i = Arg (argInfo i) <$> reify (unArg i)
-
-reifyIArgs :: Reify i a => [Arg i] -> TCM [Arg a]
-reifyIArgs = mapM reifyIArg
+apps e = elims e . map I.Apply
-- Composition of reified eliminations ------------------------------------
+-- | Drops hidden arguments unless --show-implicit.
+nelims :: Expr -> [I.Elim' (Named_ Expr)] -> TCM Expr
+nelims e [] = return e
+nelims e (I.Apply arg : es) = do
+ arg <- reify arg -- This replaces the arg by _ if irrelevant
+ dontShowImp <- not <$> showImplicitArguments
+ let hd | notVisible arg && dontShowImp = e
+ | otherwise = A.App noExprInfo e arg
+ nelims hd es
+nelims e (I.Proj o@ProjPrefix d : es) =
+ nelims (A.App noExprInfo (A.Proj o $ AmbQ [d]) $ defaultNamedArg e) es
+nelims e (I.Proj o d : es) =
+ nelims (A.App noExprInfo e (defaultNamedArg $ A.Proj o $ AmbQ [d])) es
+
+-- | Drops hidden arguments unless --show-implicit.
elims :: Expr -> [I.Elim' Expr] -> TCM Expr
-elims e [] = return e
-elims e (I.Apply arg : es) =
- elims (A.App exprInfo e $ fmap unnamed arg) es
-elims e (I.Proj d : es) = elims (A.App exprInfo (A.Proj d) $ defaultNamedArg e) es
-
-reifyIElim :: Reify i a => I.Elim' i -> TCM (I.Elim' a)
-reifyIElim (I.Apply i) = I.Apply <$> traverse reify i
-reifyIElim (I.Proj d) = return $ I.Proj d
-
-reifyIElims :: Reify i a => [I.Elim' i] -> TCM [I.Elim' a]
-reifyIElims = mapM reifyIElim
+elims e = nelims e . map (fmap unnamed)
-- Omitting information ---------------------------------------------------
-exprInfo :: ExprInfo
-exprInfo = ExprRange noRange
+noExprInfo :: ExprInfo
+noExprInfo = ExprRange noRange
-- Conditional reification to omit terms that are not shown --------------
@@ -144,16 +141,16 @@ instance Reify Expr Expr where
instance Reify MetaId Expr where
reifyWhen = reifyWhenE
reify x@(MetaId n) = liftTCM $ do
+ b <- asks envPrintMetasBare
mi <- mvInfo <$> lookupMeta x
let mi' = Info.MetaInfo
{ metaRange = getRange $ miClosRange mi
- , metaScope = M.clScope $ miClosRange mi
- , metaNumber = Just x
- , metaNameSuggestion = miNameSuggestion mi
+ , metaScope = clScope $ miClosRange mi
+ , metaNumber = if b then Nothing else Just x
+ , metaNameSuggestion = if b then "" else miNameSuggestion mi
}
underscore = return $ A.Underscore mi'
- ifNotM shouldReifyInteractionPoints underscore $ {- else -}
- caseMaybeM (isInteractionMeta x) underscore $ \ ii@InteractionId{} ->
+ caseMaybeM (isInteractionMeta x) underscore $ \ ii@InteractionId{} ->
return $ A.QuestionMark mi' ii
-- Does not print with-applications correctly:
@@ -166,20 +163,20 @@ instance Reify DisplayTerm Expr where
reify d = case d of
DTerm v -> reifyTerm False v
DDot v -> reify v
- DCon c vs -> apps (A.Con (AmbQ [conName c])) =<< reifyIArgs vs
- DDef f es -> elims (A.Def f) =<< reifyIElims es
- DWithApp u us vs -> do
+ DCon c ci vs -> apps (A.Con (AmbQ [conName c])) =<< reify vs
+ DDef f es -> elims (A.Def f) =<< reify es
+ DWithApp u us es0 -> do
(e, es) <- reify (u, us)
- reifyApp (if null es then e else A.WithApp exprInfo e es) vs
+ elims (if null es then e else A.WithApp noExprInfo e es) =<< reify es0
-- | @reifyDisplayForm f vs fallback@
-- tries to rewrite @f vs@ with a display form for @f@.
-- If successful, reifies the resulting display term,
-- otherwise, does @fallback@.
-reifyDisplayForm :: QName -> I.Args -> TCM A.Expr -> TCM A.Expr
-reifyDisplayForm f vs fallback = do
+reifyDisplayForm :: QName -> I.Elims -> TCM A.Expr -> TCM A.Expr
+reifyDisplayForm f es fallback = do
ifNotM displayFormsEnabled fallback $ {- else -} do
- caseMaybeM (liftTCM $ displayForm f vs) fallback reify
+ caseMaybeM (liftTCM $ displayForm f es) fallback reify
-- | @reifyDisplayFormP@ tries to recursively
-- rewrite a lhs with a display form.
@@ -188,9 +185,6 @@ reifyDisplayForm f vs fallback = do
reifyDisplayFormP :: A.SpineLHS -> TCM A.SpineLHS
reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
ifNotM displayFormsEnabled (return lhs) $ {- else -} do
- let vs = [ setHiding h $ defaultArg $ I.var i
- | (i, h) <- zip [0..] $ map getHiding ps
- ]
-- Try to rewrite @f 0 1 2 ... |ps|-1@ to a dt.
-- Andreas, 2014-06-11 Issue 1177:
-- I thought we need to add the placeholders for ps to the context,
@@ -199,7 +193,7 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
-- But apparently, it has no influence...
-- Ulf, can you add an explanation?
md <- liftTCM $ -- addContext (replicate (length ps) "x") $
- displayForm f vs
+ displayForm f $ zipWith (\ p i -> I.Apply $ p $> I.var i) ps [0..]
reportSLn "reify.display" 60 $
"display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n " ++ show md
case md of
@@ -226,8 +220,8 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
-- can serve as a valid left-hand side. That means checking that it is a
-- defined name applied to valid lhs eliminators (projections or
-- applications to constructor patterns).
- okDisplayForm (DWithApp d ds args) =
- okDisplayForm d && all okDisplayTerm ds && all okToDrop args
+ okDisplayForm (DWithApp d ds es) =
+ okDisplayForm d && all okDisplayTerm ds && all okToDropE es
-- Andreas, 2016-05-03, issue #1950.
-- We might drop trailing hidden trivial (=variable) patterns.
okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
@@ -245,6 +239,9 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okDElim (I.Apply v) = okDisplayTerm $ unArg v
okDElim I.Proj{} = True
+ okToDropE (I.Apply v) = okToDrop v
+ okToDropE I.Proj{} = False
+
okToDrop arg = notVisible arg && case ignoreSharing $ unArg arg of
I.Var _ [] -> True
I.DontCare{} -> True -- no matching on irrelevant things. __IMPOSSIBLE__ anyway?
@@ -257,30 +254,29 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
okElim (I.Proj{}) = True
okTerm (I.Var _ []) = True
- okTerm (I.Con c vs) = all okArg vs
+ okTerm (I.Con c ci vs) = all okArg vs
okTerm (I.Def x []) = isNoName $ qnameToConcrete x -- Handling wildcards in display forms
okTerm _ = False
-- Flatten a dt into (parentName, parentElims, withArgs).
- flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [DisplayTerm])
- flattenWith (DWithApp d ds1 ds2) = case flattenWith d of
- (f, es, ds0) -> (f, es, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
+ flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm])
+ flattenWith (DWithApp d ds1 es2) =
+ let (f, es, ds0) = flattenWith d
+ in (f, es, ds0 ++ map (I.Apply . defaultArg) ds1 ++ map (fmap DTerm) es2)
flattenWith (DDef f es) = (f, es, []) -- .^ hacky, but we should only hit this when printing debug info
flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, [])
flattenWith _ = __IMPOSSIBLE__
displayLHS :: [A.Pattern] -> [A.Pattern] -> DisplayTerm -> TCM A.SpineLHS
- displayLHS ps wps d = case flattenWith d of
- (f, vs, ds) -> do
- ds <- mapM termToPat ds
+ displayLHS ps wps d = do
+ let (f, vs, es) = flattenWith d
+ ds <- mapM (namedArg <.> elimToPat) es
vs <- mapM elimToPat vs
return $ SpineLHS i f vs (ds ++ wps)
where
- ci = ConPatInfo ConPCon patNoRange
-
argToPat arg = fmap unnamed <$> traverse termToPat arg
elimToPat (I.Apply arg) = argToPat arg
- elimToPat (I.Proj d) = return $ defaultNamedArg $ A.DefP patNoRange d []
+ elimToPat (I.Proj o d) = return $ defaultNamedArg $ A.ProjP patNoRange o $ AmbQ [d]
termToPat :: DisplayTerm -> TCM A.Pattern
@@ -288,17 +284,17 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
Nothing -> __IMPOSSIBLE__
Just p -> p
- termToPat (DCon c vs) = tryRecPFromConP =<< do
- A.ConP ci (AmbQ [conName c]) <$> mapM argToPat vs
+ termToPat (DCon c ci vs) = tryRecPFromConP =<< do
+ A.ConP (ConPatInfo ci patNoRange) (AmbQ [conName c]) <$> mapM argToPat vs
- termToPat (DTerm (I.Con c vs)) = tryRecPFromConP =<< do
- A.ConP ci (AmbQ [conName c]) <$> mapM (argToPat . fmap DTerm) vs
+ termToPat (DTerm (I.Con c ci vs)) = tryRecPFromConP =<< do
+ A.ConP (ConPatInfo ci patNoRange) (AmbQ [conName c]) <$> mapM (argToPat . fmap DTerm) vs
termToPat (DTerm (I.Def _ [])) = return $ A.WildP patNoRange
termToPat (DDef _ []) = return $ A.WildP patNoRange
- termToPat (DDot v) = A.DotP patNoRange <$> termToExpr v
- termToPat v = A.DotP patNoRange <$> reify v -- __IMPOSSIBLE__
+ termToPat (DDot v) = A.DotP patNoRange Inserted <$> termToExpr v
+ termToPat v = A.DotP patNoRange Inserted <$> reify v -- __IMPOSSIBLE__
len = genericLength ps
@@ -310,7 +306,7 @@ reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
reportSLn "reify.display" 60 $ "termToExpr " ++ show v
-- After unSpine, a Proj elimination is __IMPOSSIBLE__!
case unSpine v of
- I.Con c vs ->
+ I.Con c ci vs ->
apps (A.Con (AmbQ [conName c])) =<< argsToExpr vs
I.Def f es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
@@ -337,32 +333,35 @@ instance Reify Term Expr where
reifyTerm :: Bool -> Term -> TCM Expr
reifyTerm expandAnonDefs0 v = do
+ metasBare <- asks envPrintMetasBare
-- Ulf 2014-07-10: Don't expand anonymous when display forms are disabled
-- (i.e. when we don't care about nice printing)
expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
- v <- unSpine <$> instantiate v
- case v of
+ -- Andreas, 2016-07-21 if --postfix-projections
+ -- then we print system-generated projections as postfix, else prefix.
+ havePfp <- optPostfixProjections <$> pragmaOptions
+ let pred = if havePfp then (== ProjPrefix) else (/= ProjPostfix)
+ v <- ignoreSharing <$> instantiate v
+ case applyUnless metasBare (unSpine' pred) v of
I.Var n es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
- reifyApp (A.Var x) vs
+ elims (A.Var x) =<< reify es
I.Def x es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
- reifyDisplayForm x vs $ reifyDef expandAnonDefs x vs
- I.Con c vs -> do
+ reifyDisplayForm x es $ reifyDef expandAnonDefs x es
+ I.Con c ci vs -> do
let x = conName c
isR <- isGeneratedRecordConstructor x
- case isR of
+ case isR || ci == ConORec of
True -> do
showImp <- showImplicitArguments
let keep (a, v) = showImp || notHidden a
r <- getConstructorData x
xs <- getRecordFieldNames r
- vs <- map unArg <$> reifyIArgs vs
- return $ A.Rec exprInfo $ map (Left . uncurry FieldAssignment . mapFst unArg) $ filter keep $ zip xs vs
- False -> reifyDisplayForm x vs $ do
- ci <- getConstInfo x
- let Constructor{conPars = np} = theDef ci
+ vs <- map unArg <$> reify vs
+ return $ A.Rec noExprInfo $ map (Left . uncurry FieldAssignment . mapFst unArg) $ filter keep $ zip xs vs
+ False -> reifyDisplayForm x (map I.Apply vs) $ do
+ def <- getConstInfo x
+ let Constructor{conPars = np} = theDef def
-- if we are the the module that defines constructor x
-- then we have to drop at least the n module parameters
n <- getDefFreeVars x
@@ -371,7 +370,7 @@ reifyTerm expandAnonDefs0 v = do
when (n > np) __IMPOSSIBLE__
let h = A.Con (AmbQ [x])
if null vs then return h else do
- es <- reifyIArgs vs
+ es <- reify vs
-- Andreas, 2012-04-20: do not reify parameter arguments of constructor
-- if the first regular constructor argument is hidden
-- we turn it into a named argument, in order to avoid confusion
@@ -387,38 +386,30 @@ reifyTerm expandAnonDefs0 v = do
-- Here, we need the reducing version of @telView@
-- because target of constructor could be a definition
-- expanding into a function type. See test/succeed/NameFirstIfHidden.agda.
- TelV tel _ <- telView (defType ci)
- case genericDrop np $ telToList tel of
+ TelV tel _ <- telView (defType def)
+ let (pars, rest) = splitAt np $ telToList tel
+ case rest of
-- Andreas, 2012-09-18
-- If the first regular constructor argument is hidden,
-- we keep the parameters to avoid confusion.
- (Dom info _ : _) | isHidden info -> do
- let us = genericReplicate (np - n) $
- setRelevance Relevant $ Arg info underscore
- apps h $ us ++ es
+ (Dom info _ : _) | notVisible info -> do
+ let us = for (drop n pars) $ \ (Dom ai _) ->
+ -- setRelevance Relevant $
+ hideOrKeepInstance $ Arg ai underscore
+ apps h $ us ++ es -- Note: unless --show-implicit, @apps@ will drop @us@.
-- otherwise, we drop all parameters
_ -> apps h es
-{- CODE FROM 2012-04-xx
- let doms = genericDrop np $ telToList tel
- reportSLn "syntax.reify.con" 30 $ unlines
- [ "calling nameFirstIfHidden"
- , "doms = " ++ show doms
- , "es = " ++ show es
- , "n = " ++ show n
- , "np = " ++ show np
- ]
- napps h $ genericDrop (n - np) $ nameFirstIfHidden doms es
--}
--- I.Lam info b | isAbsurdBody b -> return $ A.AbsurdLam exprInfo $ getHiding info
+
+-- I.Lam info b | isAbsurdBody b -> return $ A. AbsurdLam noExprInfo $ getHiding info
I.Lam info b -> do
(x,e) <- reify b
- return $ A.Lam exprInfo (DomainFree info x) e
+ return $ A.Lam noExprInfo (DomainFree info x) e
-- Andreas, 2011-04-07 we do not need relevance information at internal Lambda
I.Lit l -> reify l
I.Level l -> reify l
I.Pi a b -> case b of
NoAbs _ b'
- | notHidden a -> uncurry (A.Fun $ exprInfo) <$> reify (a, b')
+ | notHidden a -> uncurry (A.Fun $ noExprInfo) <$> reify (a, b')
-- Andreas, 2013-11-11 Hidden/Instance I.Pi must be A.Pi
-- since (a) the syntax {A} -> B or {{A}} -> B is not legal
-- and (b) the name of the binder might matter.
@@ -431,7 +422,7 @@ reifyTerm expandAnonDefs0 v = do
where
mkPi b (Arg info a) = do
(x, b) <- reify b
- return $ A.Pi exprInfo [TypedBindings noRange $ Arg info (TBind noRange [pure x] a)] b
+ return $ A.Pi noExprInfo [TypedBindings noRange $ Arg info (TBind noRange [pure x] a)] b
-- We can omit the domain type if it doesn't have any free variables
-- and it's mentioned in the target type.
domainFree a b = do
@@ -440,9 +431,9 @@ reifyTerm expandAnonDefs0 v = do
I.Sort s -> reify s
I.MetaV x es -> do
- let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
x' <- reify x
- apps x' =<< reifyIArgs vs
+ ifM (asks envPrintMetasBare) {-then-} (return x') {-else-} $
+ elims x' =<< reify es
I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
I.Shared p -> reifyTerm expandAnonDefs $ derefPtr p
where
@@ -450,10 +441,10 @@ reifyTerm expandAnonDefs0 v = do
-- to improve error messages.
-- Don't do this if we have just expanded into a display form,
-- otherwise we loop!
- reifyDef :: Bool -> QName -> I.Args -> TCM Expr
- reifyDef True x vs =
- ifM (not . null . inverseScopeLookupName x <$> getScope) (reifyDef' x vs) $ do
- r <- reduceDefCopy x vs
+ reifyDef :: Bool -> QName -> I.Elims -> TCM Expr
+ reifyDef True x es =
+ ifM (not . null . inverseScopeLookupName x <$> getScope) (reifyDef' x es) $ do
+ r <- reduceDefCopy x es
case r of
YesReduction _ v -> do
reportSLn "reify.anon" 60 $ unlines
@@ -466,31 +457,53 @@ reifyTerm expandAnonDefs0 v = do
reportSLn "reify.anon" 60 $ unlines
[ "no reduction on defined ident. in anonymous module"
, "x = " ++ show x
- , "vs = " ++ show vs
+ , "es = " ++ show es
]
- reifyDef' x vs
- reifyDef _ x vs = reifyDef' x vs
+ reifyDef' x es
+ reifyDef _ x es = reifyDef' x es
- reifyDef' :: QName -> I.Args -> TCM Expr
- reifyDef' x@(QName _ name) vs = do
+ reifyDef' :: QName -> I.Elims -> TCM Expr
+ reifyDef' x es = do
+ reportSLn "reify.def" 60 $ "reifying call to " ++ show x
-- We should drop this many arguments from the local context.
n <- getDefFreeVars x
- mdefn <- liftTCM $ (Just <$> getConstInfo x) `catchError` \_ -> return Nothing
- -- check if we have an absurd lambda
- let reifyAbsurdLambda cont =
- case theDef <$> mdefn of
- Just Function{ funCompiled = Just Fail, funClauses = [cl] }
+ -- If the definition is not (yet) in the signature,
+ -- we just do the obvious.
+ let fallback = elims (A.Def x) =<< reify (drop n es)
+ caseMaybeM (tryMaybe $ getConstInfo x) fallback $ \ defn -> do
+ let def = theDef defn
+
+ -- Check if we have an absurd lambda.
+ case def of
+ Function{ funCompiled = Just Fail, funClauses = [cl] }
| isAbsurdLambdaName x -> do
-- get hiding info from last pattern, which should be ()
- let h = getHiding $ last (clausePats cl)
- apps (A.AbsurdLam exprInfo h) =<< reifyIArgs vs
- _ -> cont
- reifyAbsurdLambda $ do
- (pad, vs :: [NamedArg Term]) <- do
- case mdefn of
- Nothing -> return ([], map (fmap unnamed) $ genericDrop n vs)
- Just defn -> do
- let def = theDef defn
+ let h = getHiding $ last $ namedClausePats cl
+ elims (A.AbsurdLam noExprInfo h) =<< reify (drop n es)
+
+ -- Otherwise (no absurd lambda):
+ _ -> do
+
+ -- Andrea(s), 2016-07-06
+ -- Extended lambdas are not considered to be projection like,
+ -- as they are mutually recursive with their parent.
+ -- Thus we do not have to consider padding them.
+
+ -- Check whether we have an extended lambda and display forms are on.
+ df <- displayFormsEnabled
+ toppars <- size <$> do lookupSection $ qnameModule x
+ let extLam = case def of
+ Function{ funExtLam = Just{}, funProjection = Just{} } -> __IMPOSSIBLE__
+ Function{ funExtLam = Just (ExtLamInfo h nh) } -> Just (toppars + h + nh)
+ _ -> Nothing
+ case extLam of
+ Just pars | df -> reifyExtLam x pars (defClauses defn) es
+
+ -- Otherwise (ordinary function call):
+ _ -> do
+ (pad, nes :: [Elim' (Named_ Term)]) <- case def of
+
+ Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do
-- This is tricky:
-- * getDefFreeVars x tells us how many arguments
-- are part of the local context
@@ -499,57 +512,99 @@ reifyTerm expandAnonDefs0 v = do
-- * when showImplicits is on we'd like to see the dropped
-- projection arguments
+ TelV tel _ <- telViewUpTo np (defType defn)
+ let (as, rest) = splitAt (np - 1) $ telToList tel
+ dom = fromMaybe __IMPOSSIBLE__ $ headMaybe rest
+
-- These are the dropped projection arguments
- (np, pad, dom) <-
- case def of
- Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do
- TelV tel _ <- telView (defType defn)
- scope <- getScope
- let (as, dom:_) = splitAt (np - 1) $ telToList tel
- whocares = A.Underscore $ Info.emptyMetaInfo { metaScope = scope }
- return (np, map (argFromDom . (fmap $ const whocares)) as, dom)
- _ -> return (0, [], __IMPOSSIBLE__)
- -- Now pad' ++ vs' = drop n (pad ++ vs)
- let pad' = genericDrop n pad
- vs' = genericDrop (max 0 (n - size pad)) vs
- -- Andreas, 2012-04-21: get rid of hidden underscores {_}
- -- Keep non-hidden arguments of the padding
+ scope <- getScope
+ let underscore = A.Underscore $ Info.emptyMetaInfo { metaScope = scope }
+ let pad = for as $ \ (Dom ai (x, _)) ->
+ Arg ai $ Named (Just $ unranged x) underscore
+
+ -- Now pad' ++ es' = drop n (pad ++ es)
+ let pad' = drop n pad
+ es' = drop (max 0 (n - size pad)) es
+ -- Andreas, 2012-04-21: get rid of hidden underscores {_} and {{_}}
+ -- Keep non-hidden arguments of the padding.
+ --
+ -- Andreas, 2016-12-20, issue #2348:
+ -- Let @padTail@ be the list of arguments of the padding
+ -- (*) after the last visible argument of the padding, and
+ -- (*) with the same visibility as the first regular argument.
+ -- If @padTail@ is not empty, we need to
+ -- print the first regular argument with name.
+ -- We further have to print all elements of @padTail@
+ -- which have the same name and visibility of the
+ -- first regular argument.
showImp <- showImplicitArguments
- return (filter visible pad',
- if not (null pad) && showImp && notVisible (last pad)
- then nameFirstIfHidden [dom] vs'
- else map (fmap unnamed) vs')
- df <- displayFormsEnabled
- let extLam = case mdefn of
- Nothing -> Nothing
- Just defn -> case theDef defn of
- Function{ funExtLam = Just (ExtLamInfo h nh) } -> Just (h + nh)
- _ -> Nothing
- case extLam of
- Just pars | df -> do
- info <- getConstInfo x
- reifyExtLam x pars (defClauses info) vs
- _ -> do
- let apps = foldl' (\e a -> A.App exprInfo e (fmap unnamed a))
- napps (A.Def x `apps` pad) =<< reifyIArgs vs
-
- reifyExtLam :: QName -> Int -> [I.Clause] -> [NamedArg Term] -> TCM Expr
- reifyExtLam x n cls vs = do
- reportSLn "reify.def" 10 $ "reifying extended lambda with definition: x = " ++ show x
- -- drop lambda lifted arguments
- cls <- mapM (reify . QNamed x . dropArgs n) $ cls
+
+ -- Get the visible arguments of the padding and the rest
+ -- after the last visible argument.
+ let (padVisNamed, padRest) = filterAndRest visible pad'
+
+ -- Remove the names from the visible arguments.
+ let padVis = map (fmap (unnamed . namedThing)) padVisNamed
+
+ -- Keep only the rest with the same visibility of @dom@...
+ let padTail = filter ((getHiding dom ==) . getHiding) padRest
+
+ -- ... and even the same name.
+ let padSame = filter ((Just (fst (unDom dom)) ==) . fmap rangedThing . nameOf . unArg) padTail
+
+ return $ if null padTail || not showImp
+ then (padVis , map (fmap unnamed) es')
+ else (padVis ++ padSame, nameFirstIfHidden dom es')
+
+ -- If it is not a projection(-like) function, we need no padding.
+ _ -> return ([], map (fmap unnamed) $ drop n es)
+ let hd = foldl' (A.App noExprInfo) (A.Def x) pad
+ nelims hd =<< reify nes
+
+ -- Andreas, 2016-07-06 Issue #2047
+
+ -- With parameter refinement, the "parameter" patterns of an extended
+ -- lambda can now be different from variable patterns. If we just drop
+ -- them (plus the associated arguments to the extended lambda), we produce
+ -- something
+
+ -- * that violates internal invariants. In particular, the permutation
+ -- dbPatPerm from the patterns to the telescope can no longer be
+ -- computed. (And in fact, dropping from the start of the telescope is
+ -- just plainly unsound then.)
+
+ -- * prints the wrong thing (old fix for #2047)
+
+ -- What we do now, is more sound, although not entirely satisfying:
+ -- When the "parameter" patterns of an external lambdas are not variable
+ -- patterns, we fall back to printing the internal function created for the
+ -- extended lambda, instead trying to construct the nice syntax.
+
+ reifyExtLam :: QName -> Int -> [I.Clause] -> I.Elims -> TCM Expr
+ reifyExtLam x npars cls es = do
+ reportSLn "reify.def" 10 $ "reifying extended lambda " ++ show x
+ reportSLn "reify.def" 50 $ show $ nest 2 $ vcat
+ [ text "npars =" <+> pretty npars
+ , text "es =" <+> fsep (map (prettyPrec 10) es)
+ , text "def =" <+> vcat (map pretty cls) ]
+ -- As extended lambda clauses live in the top level, we add the whole
+ -- section telescope to the number of parameters.
+ let (pars, rest) = splitAt npars es
+ -- Since we applying the clauses to the parameters,
+ -- we do not need to drop their initial "parameter" patterns
+ -- (this is taken care of by @apply@).
+ cls <- mapM (reify . NamedClause x False . (`applyE` pars)) cls
let cx = nameConcrete $ qnameName x
dInfo = mkDefInfo cx noFixity' PublicAccess ConcreteDef (getRange x)
- napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
-
--- | @nameFirstIfHidden n (a1->...an->{x:a}->b) ({e} es) = {x = e} es@
-nameFirstIfHidden :: [Dom (ArgName, t)] -> [Arg a] -> [NamedArg a]
-nameFirstIfHidden _ [] = []
-nameFirstIfHidden [] (_ : _) = __IMPOSSIBLE__
-nameFirstIfHidden (dom : _) (Arg info e : es) | isHidden info =
- Arg info (Named (Just $ unranged $ fst $ unDom dom) e) :
+ elims (A.ExtendedLam noExprInfo dInfo x cls) =<< reify rest
+
+-- | @nameFirstIfHidden (x:a) ({e} es) = {x = e} es@
+nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
+nameFirstIfHidden dom (I.Apply (Arg info e) : es) | notVisible info =
+ I.Apply (Arg info (Named (Just $ unranged $ fst $ unDom dom) e)) :
+ map (fmap unnamed) es
+nameFirstIfHidden _ es =
map (fmap unnamed) es
-nameFirstIfHidden _ es = map (fmap unnamed) es
instance Reify i a => Reify (Named n i) (Named n a) where
reify = traverse reify
@@ -562,124 +617,35 @@ instance (Reify i a) => Reify (Arg i) (Arg a) where
`and2M` (return (argInfoRelevance info /= Irrelevant) `or2M` showIrrelevantArguments)
reifyWhen b i = traverse (reifyWhen b) i
-instance Reify Elim Expr where
- reifyWhen = reifyWhenE
- reify e = case e of
- I.Apply v -> appl "apply" <$> reify v
- I.Proj f -> appl "proj" <$> reify ((defaultArg $ I.Def f []) :: Arg Term)
- where
- appl :: String -> Arg Expr -> Expr
- appl s v = A.App exprInfo (A.Lit (LitString noRange s)) $ fmap unnamed v
-
-type NamedClause = QNamed I.Clause
--- data NamedClause = NamedClause QName I.Clause
-
-instance Reify ClauseBody RHS where
- reify NoBody = return AbsurdRHS
- reify (Body v) = RHS <$> reify v
- reify (Bind b) = reify $ absBody b -- the variables should already be bound
--- Local data types to shuffleDots
-data DotBind = BindFirstExplicit | BindFirstImplicit | AlreadyBound deriving (Show)
-data DoBind = YesBind | NoBind | DontTouch deriving (Eq, Show)
+data NamedClause = NamedClause QName Bool I.Clause
+ -- ^ Also tracks whether module parameters should be dropped from the patterns.
-- The Monoid instance for Data.Map doesn't require that the values are a
-- monoid.
newtype MonoidMap k v = MonoidMap { unMonoidMap :: Map.Map k v }
+instance (Ord k, Monoid v) => Semigroup (MonoidMap k v) where
+ MonoidMap m1 <> MonoidMap m2 = MonoidMap (Map.unionWith mappend m1 m2)
+
instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where
mempty = MonoidMap Map.empty
- mappend (MonoidMap m1) (MonoidMap m2) = MonoidMap (Map.unionWith mappend m1 m2)
-
--- | Move dots on variables so that each variable is bound at its first
--- non-hidden occurrence (if any). If all occurrences are hidden it's bound
--- at the first occurrence.
-shuffleDots :: ([NamedArg A.Pattern], [A.Pattern]) -> TCM ([NamedArg A.Pattern], [A.Pattern])
-shuffleDots (ps, wps) = do
- return $ (`evalState` xs)
- $ (`runReaderT` NotHidden)
- $ (,) <$> redotArgs ps <*> redotPats wps
- where
- -- An argument is explicit if _all_ Arg's on the way are explicit. In the
- -- map we store if _any_ of the variable occurrences were explicit.
- implicit = All False
- explicit = All True
- -- compute binding strategy
- xs = Map.map (\(_, h) -> if getAny h then BindFirstExplicit else BindFirstImplicit)
- $ Map.filter (getAny . fst) -- remove vars that don't appear dotted
- $ unMonoidMap
- $ argsVars explicit ps `mappend` foldMap (patVars explicit) wps
-
- -- Compute a map from pattern vars to (AppearsDotted, AppearsInANonHiddenPosition)
- argsVars h = foldMap (argVars h)
- argVars h a = (foldMap $ foldMap $ patVars (h `mappend` h')) a
- where h' = if getHiding a == NotHidden then explicit else implicit
- patVars h p = case p of
- A.VarP x -> MonoidMap $ Map.singleton x (Any False, Any $ getAll h)
- A.DotP _ (A.Var x) -> MonoidMap $ Map.singleton x (Any True, Any $ getAll h)
- A.DotP{} -> mempty
- A.ConP _ _ ps -> argsVars h ps
- A.DefP _ _ ps -> argsVars h ps
- A.PatternSynP _ _ ps -> argsVars h ps
- A.WildP{} -> mempty
- A.AbsurdP{} -> mempty
- A.LitP{} -> mempty
- A.AsP{} -> __IMPOSSIBLE__
- A.RecP _ as -> foldMap (foldMap (patVars h)) as
-
- shouldBind x = do
- xs <- get
- h <- ask
- let b = case Map.lookup x xs of
- Nothing -> DontTouch
- Just s -> case s of
- BindFirstExplicit | h == NotHidden -> YesBind
- | otherwise -> NoBind
- BindFirstImplicit -> YesBind -- in this case we know h isn't NotHidden
- AlreadyBound -> NoBind
- when (b == YesBind) $ put $ Map.adjust (const AlreadyBound) x xs
- return b
-
- redotArgs = traverse redotArg
- redotArg a = hide $ traverse (traverse redotPat) a
- where hide | getHiding a /= NotHidden = local (const Hidden)
- | otherwise = id
- redotPats = traverse redotPat
- redotPat p = case p of
- A.VarP x -> redotVar p x
- A.DotP _ (A.Var x) -> redotVar p x
- A.DotP{} -> pure p
- A.ConP i c ps -> A.ConP i c <$> redotArgs ps
- A.DefP i f ps -> A.DefP i f <$> redotArgs ps
- A.PatternSynP i x ps -> A.PatternSynP i x <$> redotArgs ps
- A.WildP{} -> pure p
- A.AbsurdP{} -> pure p
- A.LitP{} -> pure p
- A.AsP{} -> __IMPOSSIBLE__
- A.RecP i as -> A.RecP i <$> traverse (traverse redotPat) as
-
- redotVar p x = do
- b <- shouldBind x
- return $ case b of
- DontTouch -> p
- YesBind -> A.VarP x
- NoBind -> A.DotP (Info.PatRange $ getRange p) (A.Var x)
+ mappend = (<>)
-- | Removes implicit arguments that are not needed, that is, that don't bind
-- any variables that are actually used and doesn't do pattern matching.
+-- Doesn't strip any arguments that were written explicitly by the user.
stripImplicits :: ([NamedArg A.Pattern], [A.Pattern]) ->
TCM ([NamedArg A.Pattern], [A.Pattern])
stripImplicits (ps, wps) = do -- v if show-implicit we don't need the names
ifM showImplicitArguments (return (map (unnamed . namedThing <$>) ps, wps)) $ do
- let vars = dotVars (ps, wps)
reportSLn "reify.implicit" 30 $ unlines
[ "stripping implicits"
, " ps = " ++ show ps
, " wps = " ++ show wps
- , " vars = " ++ show vars
]
let allps = ps ++ map defaultNamedArg wps
- sps = blankDots $ foldl (.) (strip Set.empty) (map rearrangeBinding $ Set.toList vars) $ allps
+ sps = blankDots $ strip allps
(ps', wps') = splitAt (length sps - length wps) sps
reportSLn "reify.implicit" 30 $ unlines
[ " ps' = " ++ show ps'
@@ -687,64 +653,40 @@ stripImplicits (ps, wps) = do -- v if show-implicit we don't need the n
]
return (ps', map namedArg wps')
where
- argsVars = Set.unions . map argVars
- argVars = patVars . namedArg
- patVars p = case p of
- A.VarP x -> Set.singleton x
- A.ConP _ _ ps -> argsVars ps
- A.DefP _ _ ps -> Set.empty
- A.DotP _ e -> Set.empty
- A.WildP _ -> Set.empty
- A.AbsurdP _ -> Set.empty
- A.LitP _ -> Set.empty
- A.AsP _ _ p -> patVars p
- A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- Set.empty
- A.RecP _ as -> foldMap (foldMap patVars) as
-
- -- Replace dot variables by ._ if they use implicitly bound variables. This
- -- is slightly nicer than making the implicts explicit.
- blankDots ps = (map . fmap . fmap . fmap) blank ps
- where
- bound = argsVars ps
- blank e | Set.null (Set.difference (dotVars e) bound) = e
- | otherwise = A.Underscore emptyMetaInfo
-
- -- Pick the "best" place to bind the variable. Best in this case
- -- is the left-most explicit binding site. But, of course we can't
- -- do this since binding site might be forced by a parent clause.
- -- Why? Because the binding site we pick might not exist in the
- -- generated with function if it corresponds to a dot pattern.
- rearrangeBinding x ps = ps
-
- strip dvs ps = stripArgs True ps
+ -- Replace variables in dot patterns by an underscore _ if they are hidden
+ -- in the pattern. This is slightly nicer than making the implicts explicit.
+ blankDots ps = blank (varsBoundIn ps) ps
+
+ strip ps = stripArgs True ps
where
stripArgs _ [] = []
stripArgs fixedPos (a : as) =
- case getHiding a of
- Hidden | canStrip a as -> stripArgs False as
- Instance | canStrip a as -> stripArgs False as
- _ -> stripName fixedPos (stripArg a) :
- stripArgs True as
+ if canStrip a
+ then if all canStrip $ takeWhile isUnnamedHidden as
+ then stripArgs False as
+ else let a' = fmap ($> A.WildP (Info.PatRange $ getRange a)) a
+ in stripName fixedPos a' : stripArgs True as
+ else stripName fixedPos (stripArg a) : stripArgs True as
stripName True = fmap (unnamed . namedThing)
stripName False = id
- canStrip a as = and
- [ varOrDot p
- , noInterestingBindings p
- , all (flip canStrip []) $ takeWhile isUnnamedHidden as
+ canStrip a = and
+ [ notVisible a
+ , getOrigin a /= UserWritten
+ , varOrDot (namedArg a)
]
- where p = namedArg a
- isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
+ isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing && isNothing (isProjP x)
stripArg a = fmap (fmap stripPat) a
stripPat p = case p of
A.VarP _ -> p
A.ConP i c ps -> A.ConP i c $ stripArgs True ps
+ A.ProjP{} -> p
A.DefP _ _ _ -> p
- A.DotP _ e -> p
+ A.DotP _ _ e -> p
A.WildP _ -> p
A.AbsurdP _ -> p
A.LitP _ -> p
@@ -752,88 +694,94 @@ stripImplicits (ps, wps) = do -- v if show-implicit we don't need the n
A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- p
A.RecP i fs -> A.RecP i $ map (fmap stripPat) fs -- TODO Andreas: is this right?
- noInterestingBindings p =
- Set.null $ dvs `Set.intersection` patVars p
-
varOrDot A.VarP{} = True
varOrDot A.WildP{} = True
varOrDot A.DotP{} = True
+ varOrDot (A.ConP cpi _ ps) | patOrigin cpi == ConOSystem
+ = all varOrDot $ map namedArg ps
varOrDot _ = False
--- | @dotVars ps@ gives all the variables inside of dot patterns of @ps@
--- It is only invoked for patternish things. (Ulf O-tone!)
--- Use it for printing l.h.sides: which of the implicit arguments
--- have to be made explicit.
-class DotVars a where
- dotVars :: a -> Set Name
- isConPat :: a -> Bool
- isConPat _ = False
-
-instance DotVars a => DotVars (Arg a) where
- dotVars a = if notVisible a && not (isConPat a) -- Hidden constructor patterns are visible!
- then Set.empty
- else dotVars (unArg a)
- isConPat = isConPat . unArg
-
-instance DotVars a => DotVars (Named s a) where
- dotVars = dotVars . namedThing
- isConPat = isConPat . namedThing
-
-instance DotVars a => DotVars [a] where
- dotVars = Set.unions . map dotVars
-
-instance (DotVars a, DotVars b) => DotVars (a, b) where
- dotVars (x, y) = Set.union (dotVars x) (dotVars y)
-
-instance (DotVars a, DotVars b) => DotVars (Either a b) where
- dotVars = either dotVars dotVars
-
-instance DotVars A.Clause where
- dotVars (A.Clause _ rhs [] _) = dotVars rhs
- dotVars (A.Clause _ rhs (_:_) _) = __IMPOSSIBLE__ -- cannot contain where clauses?
-
-instance DotVars A.Pattern where
- dotVars p = case p of
- A.VarP _ -> Set.empty -- do not add pattern vars
- A.ConP _ _ ps -> dotVars ps
- A.DefP _ _ ps -> dotVars ps
- A.DotP _ e -> dotVars e
- A.WildP _ -> Set.empty
- A.AbsurdP _ -> Set.empty
- A.LitP _ -> Set.empty
- A.AsP _ _ p -> dotVars p
- A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- Set.empty
- A.RecP _ fs -> dotVars fs
-
- isConPat A.ConP{} = True
- isConPat A.LitP{} = True
- isConPat _ = False
-
--- | Getting all(!) variables of an expression.
--- It should only get free ones, but it does not matter to include
--- the bound ones.
-instance DotVars A.Expr where
- dotVars e = case e of
- A.ScopedExpr _ e -> dotVars e
- A.Var x -> Set.singleton x -- add any expression variable
- A.Def _ -> Set.empty
- A.Proj _ -> Set.empty
- A.Con _ -> Set.empty
- A.Lit _ -> Set.empty
- A.QuestionMark{} -> Set.empty
- A.Underscore _ -> Set.empty
- A.App _ e1 e2 -> dotVars (e1, e2)
- A.WithApp _ e es -> dotVars (e, es)
- A.Lam _ _ e -> dotVars e
- A.AbsurdLam _ _ -> Set.empty
- A.ExtendedLam _ _ _ cs -> dotVars cs
- A.Pi _ tel e -> dotVars (tel, e)
- A.Fun _ a b -> dotVars (a, b)
- A.Set _ _ -> Set.empty
- A.Prop _ -> Set.empty
+-- | @blank bound x@ replaces all variables in @x@ that are not in @bound@ by
+-- an underscore @_@. It is used for printing dot patterns: we don't want to
+-- make implicit variables explicit, so we blank them out in the dot patterns
+-- instead (this is fine since dot patterns can be inferred anyway).
+class BlankVars a where
+ blank :: Set Name -> a -> a
+
+instance BlankVars a => BlankVars (Arg a) where
+ blank bound = fmap $ blank bound
+
+instance BlankVars a => BlankVars (Named s a) where
+ blank bound = fmap $ blank bound
+
+instance BlankVars a => BlankVars [a] where
+ blank bound = fmap $ blank bound
+
+instance (BlankVars a, BlankVars b) => BlankVars (a, b) where
+ blank bound (x, y) = (blank bound x, blank bound y)
+
+instance (BlankVars a, BlankVars b) => BlankVars (Either a b) where
+ blank bound (Left x) = Left $ blank bound x
+ blank bound (Right y) = Right $ blank bound y
+
+instance BlankVars A.NamedDotPattern where
+ blank bound = id
+
+instance BlankVars A.Clause where
+ blank bound (A.Clause lhs namedDots rhs [] ca) =
+ let bound' = varsBoundIn lhs `Set.union` bound
+ in A.Clause (blank bound' lhs)
+ (blank bound' namedDots)
+ (blank bound' rhs) [] ca
+ blank bound (A.Clause lhs namedDots rhs (_:_) ca) = __IMPOSSIBLE__
+
+instance BlankVars A.LHS where
+ blank bound (A.LHS i core wps) = uncurry (A.LHS i) $ blank bound (core, wps)
+
+instance BlankVars A.LHSCore where
+ blank bound (A.LHSHead f ps) = A.LHSHead f $ blank bound ps
+ blank bound (A.LHSProj p b ps) = uncurry (A.LHSProj p) $ blank bound (b, ps)
+
+instance BlankVars A.Pattern where
+ blank bound p = case p of
+ A.VarP _ -> p -- do not blank pattern vars
+ A.ConP c i ps -> A.ConP c i $ blank bound ps
+ A.ProjP{} -> p
+ A.DefP i f ps -> A.DefP i f $ blank bound ps
+ A.DotP i o e -> A.DotP i o $ blank bound e
+ A.WildP _ -> p
+ A.AbsurdP _ -> p
+ A.LitP _ -> p
+ A.AsP i n p -> A.AsP i n $ blank bound p
+ A.PatternSynP _ _ _ -> __IMPOSSIBLE__
+ A.RecP i fs -> A.RecP i $ blank bound fs
+
+instance BlankVars A.Expr where
+ blank bound e = case e of
+ A.ScopedExpr i e -> A.ScopedExpr i $ blank bound e
+ A.Var x -> if x `Set.member` bound then e
+ else A.Underscore emptyMetaInfo
+ A.Def _ -> e
+ A.Proj{} -> e
+ A.Con _ -> e
+ A.Lit _ -> e
+ A.QuestionMark{} -> e
+ A.Underscore _ -> e
+ A.Dot i e -> A.Dot i $ blank bound e
+ A.App i e1 e2 -> uncurry (A.App i) $ blank bound (e1, e2)
+ A.WithApp i e es -> uncurry (A.WithApp i) $ blank bound (e, es)
+ A.Lam i b e -> let bound' = varsBoundIn b `Set.union` bound
+ in A.Lam i (blank bound b) (blank bound' e)
+ A.AbsurdLam _ _ -> e
+ A.ExtendedLam i d f cs -> A.ExtendedLam i d f $ blank bound cs
+ A.Pi i tel e -> let bound' = varsBoundIn tel `Set.union` bound
+ in uncurry (A.Pi i) $ blank bound' (tel, e)
+ A.Fun i a b -> uncurry (A.Fun i) $ blank bound (a, b)
+ A.Set _ _ -> e
+ A.Prop _ -> e
A.Let _ _ _ -> __IMPOSSIBLE__
- A.Rec _ es -> dotVars es
- A.RecUpdate _ e es -> dotVars (e, es)
+ A.Rec i es -> A.Rec i $ blank bound es
+ A.RecUpdate i e es -> uncurry (A.RecUpdate i) $ blank bound (e, es)
A.ETel _ -> __IMPOSSIBLE__
A.QuoteGoal {} -> __IMPOSSIBLE__
A.QuoteContext {} -> __IMPOSSIBLE__
@@ -841,89 +789,122 @@ instance DotVars A.Expr where
A.QuoteTerm {} -> __IMPOSSIBLE__
A.Unquote {} -> __IMPOSSIBLE__
A.Tactic {} -> __IMPOSSIBLE__
- A.DontCare v -> dotVars v
- A.PatternSyn {} -> Set.empty
- A.Macro {} -> Set.empty
-
-instance DotVars a => DotVars (FieldAssignment' a) where
- dotVars a = dotVars (a ^. exprFieldA)
-
-instance DotVars A.ModuleName where
- dotVars _ = Set.empty
-
-instance DotVars RHS where
- dotVars (RHS e) = dotVars e
- dotVars AbsurdRHS = Set.empty
- dotVars (WithRHS _ es clauses) = __IMPOSSIBLE__ -- NZ
- dotVars (RewriteRHS xes rhs _) = __IMPOSSIBLE__ -- NZ
-
-instance DotVars TypedBindings where
- dotVars (TypedBindings _ bs) = dotVars bs
-
-instance DotVars TypedBinding where
- dotVars (TBind _ _ e) = dotVars e
- dotVars (TLet _ _) = __IMPOSSIBLE__ -- Since the internal syntax has no let bindings left
-
-class MonadTick m where
- tick :: m Nat
-
-newtype TickT m a = TickT { unTickT :: StateT Nat m a }
- deriving (Functor, Applicative, Monad, MonadReader r, MonadTrans, MonadIO) -- MonadExcept e,
-
-instance Monad m => MonadTick (TickT m) where
- tick = TickT $ do i <- get; put (i + 1); return i
-
-instance MonadState s m => MonadState s (TickT m) where
- state f = lift $ state f -- TickT $ StateT $ \ n -> (,n) <$> state f
-
-instance MonadTCM tcm => MonadTCM (TickT tcm) where
- liftTCM = lift . liftTCM
-
-runTickT :: Monad m => TickT m a -> m a
-runTickT m = evalStateT (unTickT m) 0
-
--- TODO: implement reifyPatterns on de Bruijn patterns ( numberPatVars )
-reifyPatterns :: I.Telescope -> Permutation -> [NamedArg I.Pattern] -> TCM [NamedArg A.Pattern]
-reifyPatterns tel perm ps = runTickT (reifyArgs ps)
+ A.DontCare v -> A.DontCare $ blank bound v
+ A.PatternSyn {} -> e
+ A.Macro {} -> e
+
+instance BlankVars a => BlankVars (FieldAssignment' a) where
+ blank bound = over exprFieldA (blank bound)
+
+instance BlankVars A.ModuleName where
+ blank bound = id
+
+instance BlankVars RHS where
+ blank bound (RHS e mc) = RHS (blank bound e) mc
+ blank bound AbsurdRHS = AbsurdRHS
+ blank bound (WithRHS _ es clauses) = __IMPOSSIBLE__ -- NZ
+ blank bound (RewriteRHS xes rhs _) = __IMPOSSIBLE__ -- NZ
+
+instance BlankVars A.LamBinding where
+ blank bound b@A.DomainFree{} = b
+ blank bound (A.DomainFull bs) = A.DomainFull $ blank bound bs
+
+instance BlankVars TypedBindings where
+ blank bound (TypedBindings r bs) = TypedBindings r $ blank bound bs
+
+instance BlankVars TypedBinding where
+ blank bound (TBind r n e) = TBind r n $ blank bound e
+ blank bound (TLet _ _) = __IMPOSSIBLE__ -- Since the internal syntax has no let bindings left
+
+class Binder a where
+ varsBoundIn :: a -> Set Name
+
+instance Binder A.LHS where
+ varsBoundIn (A.LHS _ core ps) = varsBoundIn (core, ps)
+
+instance Binder A.LHSCore where
+ varsBoundIn (A.LHSHead _ ps) = varsBoundIn ps
+ varsBoundIn (A.LHSProj _ b ps) = varsBoundIn (b, ps)
+
+instance Binder A.Pattern where
+ varsBoundIn p = case p of
+ A.VarP x -> if show x == "()" then empty else singleton x
+ A.ConP _ _ ps -> varsBoundIn ps
+ A.ProjP{} -> empty
+ A.DefP _ _ ps -> varsBoundIn ps
+ A.WildP{} -> empty
+ A.AsP _ _ p -> varsBoundIn p
+ A.DotP{} -> empty
+ A.AbsurdP{} -> empty
+ A.LitP{} -> empty
+ A.PatternSynP _ _ ps -> varsBoundIn ps
+ A.RecP _ fs -> varsBoundIn fs
+
+instance Binder A.LamBinding where
+ varsBoundIn (A.DomainFree _ x) = singleton x
+ varsBoundIn (A.DomainFull b) = varsBoundIn b
+
+instance Binder TypedBindings where
+ varsBoundIn (TypedBindings _ b) = varsBoundIn b
+
+instance Binder TypedBinding where
+ varsBoundIn (TBind _ xs _) = varsBoundIn xs
+ varsBoundIn (TLet _ bs) = varsBoundIn bs
+
+instance Binder LetBinding where
+ varsBoundIn (LetBind _ _ x _ _) = singleton x
+ varsBoundIn (LetPatBind _ p _) = varsBoundIn p
+ varsBoundIn LetApply{} = empty
+ varsBoundIn LetOpen{} = empty
+ varsBoundIn LetDeclaredVariable{} = empty
+
+instance Binder a => Binder (FieldAssignment' a) where
+ varsBoundIn = varsBoundIn . (^. exprFieldA)
+
+instance Binder a => Binder (Arg a) where
+ varsBoundIn = varsBoundIn . unArg
+
+instance Binder a => Binder (Named x a) where
+ varsBoundIn = varsBoundIn . namedThing
+
+instance Binder (WithHiding Name) where
+ varsBoundIn (WithHiding _ x) = singleton x
+
+instance Binder a => Binder [a] where
+ varsBoundIn xs = Set.unions $ map varsBoundIn xs
+
+instance (Binder a, Binder b) => Binder (a, b) where
+ varsBoundIn (x, y) = varsBoundIn x `Set.union` varsBoundIn y
+
+
+-- | Assumes that pattern variables have been added to the context already.
+-- Picks pattern variable names from context.
+reifyPatterns :: MonadTCM tcm => [NamedArg I.DeBruijnPattern] -> tcm [NamedArg A.Pattern]
+reifyPatterns = mapM $ stripNameFromExplicit <.> traverse (traverse reifyPat)
where
- reifyArgs :: [NamedArg I.Pattern] -> TickT TCM [NamedArg A.Pattern]
- reifyArgs is = mapM reifyArg is
-
- reifyArg :: NamedArg I.Pattern -> TickT TCM (NamedArg A.Pattern)
- reifyArg i = stripNameFromExplicit <$>
- traverse (traverse reifyPat) i
-
+ stripNameFromExplicit :: NamedArg p -> NamedArg p
stripNameFromExplicit a
| getHiding a == NotHidden = fmap (unnamed . namedThing) a
| otherwise = a
- translate n = fromMaybe __IMPOSSIBLE__ $ vars !!! n
- where
- vars = permPicks $ invertP __IMPOSSIBLE__ perm
-
- reifyPat :: I.Pattern -> TickT TCM A.Pattern
+ reifyPat :: MonadTCM tcm => I.DeBruijnPattern -> tcm A.Pattern
reifyPat p = do
liftTCM $ reportSLn "reify.pat" 80 $ "reifying pattern " ++ show p
case p of
- I.VarP "()" -> A.AbsurdP patNoRange <$ tick -- HACK
- I.VarP s -> do
- i <- tick
- let j = translate i
- liftTCM $ A.VarP <$> nameOfBV (size tel - 1 - j)
+ I.VarP x | isAbsurdPatternName (dbPatVarName x)
+ -> return $ A.AbsurdP patNoRange -- HACK
+ I.VarP x -> liftTCM $ A.VarP <$> nameOfBV (dbPatVarIndex x)
I.DotP v -> do
t <- liftTCM $ reify v
- _ <- tick
- let vars = Set.map show (dotVars t)
- t' = if Set.member "()" vars then underscore else t
- return $ A.DotP patNoRange t'
+ return $ A.DotP patNoRange Inserted t
I.LitP l -> return $ A.LitP l
- I.ProjP d -> return $ A.DefP patNoRange d []
+ I.ProjP o d -> return $ A.ProjP patNoRange o $ AmbQ [d]
I.ConP c cpi ps -> do
liftTCM $ reportSLn "reify.pat" 60 $ "reifying pattern " ++ show p
- tryRecPFromConP =<< do A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
+ tryRecPFromConP =<< do A.ConP ci (AmbQ [conName c]) <$> reifyPatterns ps
where
- origin = fromMaybe ConPCon $ I.conPRecord cpi
ci = ConPatInfo origin patNoRange
+ origin = fromMaybe ConOCon $ I.conPRecord cpi
-- | If the record constructor is generated or the user wrote a record pattern,
-- turn constructor pattern into record pattern.
@@ -937,7 +918,7 @@ tryRecPFromConP p = do
-- If the record constructor is generated or the user wrote a record pattern,
-- print record pattern.
-- Otherwise, print constructor pattern.
- if recNamedCon def && patOrigin ci /= ConPRec then fallback else do
+ if recNamedCon def && patOrigin ci /= ConORec then fallback else do
fs <- liftTCM $ getRecordFieldNames r
unless (length fs == length ps) __IMPOSSIBLE__
return $ A.RecP patNoRange $ zipWith mkFA fs ps
@@ -945,26 +926,37 @@ tryRecPFromConP p = do
mkFA ax nap = FieldAssignment (unArg ax) (namedArg nap)
_ -> __IMPOSSIBLE__
+instance Reify (QNamed I.Clause) A.Clause where
+ reify (QNamed f cl) = reify (NamedClause f True cl)
+
instance Reify NamedClause A.Clause where
- reify (QNamed f (I.Clause _ tel ps' body _ catchall)) = addCtxTel tel $ do
- ps <- reifyPatterns tel perm ps
+ reify (NamedClause f toDrop cl) = addContext (clauseTel cl) $ do
+ reportSLn "reify.clause" 60 $ "reifying NamedClause"
+ ++ "\n f = " ++ show f
+ ++ "\n toDrop = " ++ show toDrop
+ ++ "\n cl = " ++ show cl
+ ps <- reifyPatterns $ namedClausePats cl
lhs <- liftTCM $ reifyDisplayFormP $ SpineLHS info f ps [] -- LHS info (LHSHead f ps) []
- nfv <- getDefFreeVars f `catchError` \_ -> return 0
- lhs <- stripImps $ dropParams nfv lhs
+ -- Unless @toDrop@ we have already dropped the module patterns from the clauses
+ -- (e.g. for extended lambdas).
+ lhs <- if not toDrop then return lhs else do
+ nfv <- getDefFreeVars f `catchError` \_ -> return 0
+ return $ dropParams nfv lhs
+ lhs <- stripImps lhs
reportSLn "reify.clause" 60 $ "reifying NamedClause, lhs = " ++ show lhs
- rhs <- reify $ renameP (reverseP perm) <$> body
+ rhs <- caseMaybe (clauseBody cl) (return AbsurdRHS) $ \ e -> do
+ RHS <$> reify e <*> pure Nothing
reportSLn "reify.clause" 60 $ "reifying NamedClause, rhs = " ++ show rhs
- let result = A.Clause (spineToLhs lhs) rhs [] catchall
+ let result = A.Clause (spineToLhs lhs) [] rhs [] (I.clauseCatchall cl)
reportSLn "reify.clause" 60 $ "reified NamedClause, result = " ++ show result
return result
where
+ perm = fromMaybe __IMPOSSIBLE__ $ clausePerm cl
info = LHSRange noRange
- ps = unnumberPatVars ps'
- perm = dbPatPerm ps'
dropParams n (SpineLHS i f ps wps) = SpineLHS i f (genericDrop n ps) wps
stripImps (SpineLHS i f ps wps) = do
- (ps, wps) <- stripImplicits =<< shuffleDots (ps, wps)
+ (ps, wps) <- stripImplicits (ps, wps)
return $ SpineLHS i f ps wps
instance Reify Type Expr where
@@ -976,12 +968,12 @@ instance Reify Sort Expr where
reify s = do
s <- instantiateFull s
case s of
- I.Type (I.Max []) -> return $ A.Set exprInfo 0
- I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set exprInfo n
+ I.Type (I.Max []) -> return $ A.Set noExprInfo 0
+ I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set noExprInfo n
I.Type a -> do
a <- reify a
- return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
- I.Prop -> return $ A.Prop exprInfo
+ return $ A.App noExprInfo (A.Set noExprInfo 0) (defaultNamedArg a)
+ I.Prop -> return $ A.Prop noExprInfo
I.Inf -> A.Var <$> freshName_ ("SetĪ‰" :: String)
I.SizeUniv -> do
I.Def sizeU [] <- primSizeUniv
@@ -989,7 +981,7 @@ instance Reify Sort Expr where
I.DLub s1 s2 -> do
lub <- freshName_ ("dLub" :: String) -- TODO: hack
(e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
- let app x y = A.App exprInfo x (defaultNamedArg y)
+ let app x y = A.App noExprInfo x (defaultNamedArg y)
return $ A.Var lub `app` e1 `app` e2
instance Reify Level Expr where
@@ -1005,7 +997,7 @@ instance (Free i, Reify i a) => Reify (Abs i) (Name, a) where
s <- return $ if isUnderscore s && 0 `freeIn` v then "z" else s
x <- freshName_ s
- e <- addContext x -- type doesn't matter
+ e <- addContext' x -- type doesn't matter
$ reify v
return (x,e)
@@ -1020,8 +1012,13 @@ instance Reify I.Telescope A.Telescope where
instance Reify i a => Reify (Dom i) (Arg a) where
reify (Dom info i) = Arg info <$> reify i
+instance Reify i a => Reify (I.Elim' i) (I.Elim' a) where
+ reify = traverse reify
+ reifyWhen b = traverse (reifyWhen b)
+
instance Reify i a => Reify [i] [a] where
- reify = traverse reify
+ reify = traverse reify
+ reifyWhen b = traverse (reifyWhen b)
instance (Reify i1 a1, Reify i2 a2) => Reify (i1,i2) (a1,a2) where
reify (x,y) = (,) <$> reify x <*> reify y