summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Quote.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Quote.hs')
-rw-r--r--src/full/Agda/TypeChecking/Quote.hs79
1 files changed, 43 insertions, 36 deletions
diff --git a/src/full/Agda/TypeChecking/Quote.hs b/src/full/Agda/TypeChecking/Quote.hs
index 9672082..197127b 100644
--- a/src/full/Agda/TypeChecking/Quote.hs
+++ b/src/full/Agda/TypeChecking/Quote.hs
@@ -1,7 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE RankNTypes #-}
module Agda.TypeChecking.Quote where
@@ -17,6 +14,7 @@ import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
+import Agda.Syntax.Internal.Pattern ( dbPatPerm' )
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Translation.InternalToAbstract
@@ -38,7 +36,7 @@ import Agda.TypeChecking.Telescope
import Agda.Utils.Except
import Agda.Utils.Impossible
import Agda.Utils.Monad ( ifM )
-import Agda.Utils.Permutation ( Permutation(Perm), compactP )
+import Agda.Utils.Permutation ( Permutation(Perm), compactP, reverseP )
import Agda.Utils.String ( Str(Str), unStr )
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as Set
@@ -97,8 +95,8 @@ quotingKit = do
sucLevel <- primLevelSuc
lub <- primLevelMax
lkit <- requireLevels
- Con z _ <- ignoreSharing <$> primZero
- Con s _ <- ignoreSharing <$> primSuc
+ Con z _ _ <- ignoreSharing <$> primZero
+ Con s _ _ <- ignoreSharing <$> primSuc
unsupported <- primAgdaTermUnsupported
agdaDefinitionFunDef <- primAgdaDefinitionFunDef
@@ -130,16 +128,15 @@ quotingKit = do
quoteRelevance UnusedArg = pure relevant
quoteArgInfo :: ArgInfo -> ReduceM Term
- quoteArgInfo (ArgInfo h r) = arginfo !@ quoteHiding h
- @@ quoteRelevance r
+ quoteArgInfo (ArgInfo h r _ _) = arginfo !@ quoteHiding h @@ quoteRelevance r
quoteLit :: Literal -> ReduceM Term
- quoteLit l@LitNat{} = lit !@ (litNat !@! Lit l)
- quoteLit l@LitFloat{} = lit !@ (litFloat !@! Lit l)
- quoteLit l@LitChar{} = lit !@ (litChar !@! Lit l)
- quoteLit l@LitString{} = lit !@ (litString !@! Lit l)
- quoteLit l@LitQName{} = lit !@ (litQName !@! Lit l)
- quoteLit l@LitMeta {} = lit !@ (litMeta !@! Lit l)
+ quoteLit l@LitNat{} = litNat !@! Lit l
+ quoteLit l@LitFloat{} = litFloat !@! Lit l
+ quoteLit l@LitChar{} = litChar !@! Lit l
+ quoteLit l@LitString{} = litString !@! Lit l
+ quoteLit l@LitQName{} = litQName !@! Lit l
+ quoteLit l@LitMeta {} = litMeta !@! Lit l
-- We keep no ranges in the quoted term, so the equality on terms
-- is only on the structure.
@@ -165,23 +162,21 @@ quotingKit = do
quotePats ps = list $ map (quoteArg quotePat . fmap namedThing) ps
quotePat :: DeBruijnPattern -> ReduceM Term
- quotePat (VarP (_,"()")) = pure absurdP
- quotePat (VarP (_,x)) = varP !@! quoteString x
+ quotePat (VarP x) | isAbsurdPatternName (dbPatVarName x) = pure absurdP
+ quotePat (VarP x) = varP !@! quoteString (dbPatVarName x)
quotePat (DotP _) = pure dotP
quotePat (ConP c _ ps) = conP !@ quoteQName (conName c) @@ quotePats ps
- quotePat (LitP l) = litP !@! Lit l
- quotePat (ProjP x) = projP !@ quoteQName x
-
- quoteBody :: I.ClauseBody -> Maybe (ReduceM Term)
- quoteBody (Body a) = Just (quoteTerm a)
- quoteBody (Bind b) = quoteBody (absBody b)
- quoteBody NoBody = Nothing
+ quotePat (LitP l) = litP !@ quoteLit l
+ quotePat (ProjP _ x) = projP !@ quoteQName x
quoteClause :: Clause -> ReduceM Term
- quoteClause Clause{namedClausePats = ps, clauseBody = body} =
- case quoteBody body of
+ quoteClause cl@Clause{namedClausePats = ps, clauseBody = body} =
+ case body of
Nothing -> absurdClause !@ quotePats ps
- Just b -> normalClause !@ quotePats ps @@ b
+ Just b ->
+ let perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm' False ps -- Dot patterns don't count (#2203)
+ v = applySubst (renamingR perm) b
+ in normalClause !@ quotePats ps @@ quoteTerm v
list :: [ReduceM Term] -> ReduceM Term
list [] = pure nil
@@ -211,32 +206,44 @@ quotingKit = do
in var !@! Lit (LitNat noRange $ fromIntegral n) @@ quoteArgs ts
Lam info t -> lam !@ quoteHiding (getHiding info) @@ quoteAbs quoteTerm t
Def x es -> do
- d <- theDef <$> getConstInfo x
+ def <- getConstInfo x
+ let d = theDef def
n <- getDefFreeVars x
- qx d @@ quoteArgs (drop n ts)
+ -- #2220: remember to restore dropped parameters
+ qx d @@ list (drop n $ defParameters def ++ map (quoteArg quoteTerm) ts)
where
ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
qx Function{ funExtLam = Just (ExtLamInfo h nh), funClauses = cs } =
extlam !@ list (map (quoteClause . dropArgs (h + nh)) cs)
qx Function{ funCompiled = Just Fail, funClauses = [cl] } =
- extlam !@ list [quoteClause $ dropArgs (length (clausePats cl) - 1) cl]
+ extlam !@ list [quoteClause $ dropArgs (length (namedClausePats cl) - 1) cl]
qx _ = def !@! quoteName x
- Con x ts -> do
- Constructor{conPars = np} <- theDef <$> getConstInfo (conName x)
- let par = arg !@ (arginfo !@ pure hidden @@ pure relevant) @@ pure unsupported
- pars = replicate np $ par
- args = list $ pars ++ map (quoteArg quoteTerm) ts
+ Con x ci ts -> do
+ cDef <- getConstInfo (conName x)
+ n <- getDefFreeVars (conName x)
+ let args = list $ drop n $ defParameters cDef ++ map (quoteArg quoteTerm) ts
con !@! quoteConName x @@ args
Pi t u -> pi !@ quoteDom quoteType t
@@ quoteAbs quoteType u
Level l -> quoteTerm (unlevelWithKit lkit l)
- Lit lit -> quoteLit lit
+ Lit l -> lit !@ quoteLit l
Sort s -> sort !@ quoteSort s
Shared p -> quoteTerm $ derefPtr p
MetaV x es -> meta !@! quoteMeta currentFile x @@ quoteArgs vs
where vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
DontCare{} -> pure unsupported -- could be exposed at some point but we have to take care
+ defParameters :: Definition -> [ReduceM Term]
+ defParameters def = map par hiding
+ where
+ np = case theDef def of
+ Constructor{ conPars = np } -> np
+ Function{ funProjection = Just p } -> projIndex p - 1
+ _ -> 0
+ TelV tel _ = telView' (defType def)
+ hiding = map getHiding $ take np $ telToList tel
+ par h = arg !@ (arginfo !@ quoteHiding h @@ pure relevant) @@ pure unsupported
+
quoteDefn :: Definition -> ReduceM Term
quoteDefn def =
case theDef def of
@@ -247,6 +254,7 @@ quotingKit = do
Record{recConHead = c} ->
agdaDefinitionRecordDef !@! quoteName (conName c)
Axiom{} -> pure agdaDefinitionPostulate
+ AbstractDefn{}-> pure agdaDefinitionPostulate
Primitive{primClauses = cs} | not $ null cs ->
agdaDefinitionFunDef !@ quoteList quoteClause cs
Primitive{} -> pure agdaDefinitionPrimitive
@@ -296,4 +304,3 @@ quoteList :: [Term] -> TCM Term
quoteList xs = do
kit <- quotingKit
runReduceM (quoteListWithKit kit pure xs)
-