summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs')
-rw-r--r--src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs44
1 files changed, 29 insertions, 15 deletions
diff --git a/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs b/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs
index 260e74a..d0b7a90 100644
--- a/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
@@ -25,8 +22,10 @@ import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.Syntax.Scope.Monad (getCurrentModule)
import Agda.Utils.Maybe
+import Agda.Utils.Monad
import Agda.Utils.List
import Agda.Utils.Functor
+import Agda.Utils.Size
type Names = [Name]
@@ -93,14 +92,20 @@ instance ToAbstract Literal Expr where
instance ToAbstract Term Expr where
toAbstract t = case t of
R.Var i es -> do
- let fallback = withName ("@" ++ show i) return
- name <- fromMaybeM fallback $ askName i
- toAbstract (A.Var name, es)
+ mname <- askName i
+ case mname of
+ Nothing -> do
+ cxt <- lift $ getContextTelescope
+ names <- asks $ drop (size cxt) . reverse
+ lift $ withShowAllArguments' False $ typeError $ DeBruijnIndexOutOfScope i cxt names
+ Just name -> toAbstract (A.Var name, es)
R.Con c es -> toAbstract (A.Con (AmbQ [killRange c]), es)
- R.Def f es -> toAbstract (A.Def (killRange f), es)
+ R.Def f es -> do
+ af <- lift $ mkDef (killRange f)
+ toAbstract (af, es)
R.Lam h t -> do
(e, name) <- toAbstract t
- let info = setHiding h defaultArgInfo
+ let info = setHiding h $ setOrigin Reflected defaultArgInfo
return $ A.Lam exprNoRange (DomainFree info name) e
R.ExtLam cs es -> do
name <- freshName_ extendedLambdaName
@@ -120,6 +125,12 @@ instance ToAbstract Term Expr where
where info = emptyMetaInfo{ metaNumber = Just x }
R.Unknown -> return $ Underscore emptyMetaInfo
+mkDef :: QName -> TCM A.Expr
+mkDef f =
+ ifM (isMacro . theDef <$> getConstInfo f)
+ (return $ A.Macro f)
+ (return $ A.Def f)
+
mkSet :: Expr -> Expr
mkSet e = App exprNoRange (A.Set exprNoRange 0) $ defaultNamedArg e
@@ -132,13 +143,16 @@ instance ToAbstract R.Pattern (Names, A.Pattern) where
toAbstract pat = case pat of
R.ConP c args -> do
(names, args) <- toAbstractPats args
- return (names, A.ConP (ConPatInfo ConPCon patNoRange) (AmbQ [killRange c]) args)
- R.DotP -> return ([], A.DotP patNoRange (Underscore emptyMetaInfo))
- R.VarP s -> withName s' $ \name -> return ([name], A.VarP name)
- where s' = if (isNoName s) then "z" else s --TODO: only do this when var is free
+ return (names, A.ConP (ConPatInfo ConOCon patNoRange) (AmbQ [killRange c]) args)
+ R.DotP -> return ([], A.WildP patNoRange)
+ R.VarP s | isNoName s -> withName "z" $ \ name -> return ([name], A.VarP name)
+ -- Ulf, 2016-08-09: Also bind noNames (#2129). This to make the
+ -- behaviour consistent with lambda and pi.
+ -- return ([], A.WildP patNoRange)
+ R.VarP s -> withName s $ \ name -> return ([name], A.VarP name)
R.LitP l -> return ([], A.LitP l)
R.AbsurdP -> return ([], A.AbsurdP patNoRange)
- R.ProjP p -> return ([], A.DefP patNoRange p [])
+ R.ProjP d -> return ([], A.ProjP patNoRange ProjSystem $ AmbQ [killRange d])
toAbstractPats :: [Arg R.Pattern] -> WithNames (Names, [NamedArg A.Pattern])
toAbstractPats pats = case pats of
@@ -153,11 +167,11 @@ instance ToAbstract (QNamed R.Clause) A.Clause where
(names, pats) <- toAbstractPats pats
rhs <- local (names++) $ toAbstract rhs
let lhs = spineToLhs $ SpineLHS (LHSRange noRange) name pats []
- return $ A.Clause lhs (RHS rhs) [] False
+ return $ A.Clause lhs [] (RHS rhs Nothing) [] False
toAbstract (QNamed name (R.AbsurdClause pats)) = do
(_, pats) <- toAbstractPats pats
let lhs = spineToLhs $ SpineLHS (LHSRange noRange) name pats []
- return $ A.Clause lhs AbsurdRHS [] False
+ return $ A.Clause lhs [] AbsurdRHS [] False
instance ToAbstract [QNamed R.Clause] [A.Clause] where
toAbstract = traverse toAbstract