summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs')
-rw-r--r--src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs297
1 files changed, 169 insertions, 128 deletions
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index 2c0fd75..16b3f05 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -1,12 +1,16 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverlappingInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
{-| Translation from "Agda.Syntax.Concrete" to "Agda.Syntax.Abstract". Involves scope analysis,
figuring out infix operator precedences and tidying up definitions.
@@ -34,6 +38,8 @@ import Control.Monad.Reader hiding (mapM)
import Data.Foldable (Foldable, traverse_)
import Data.Traversable (mapM, traverse)
import Data.List ((\\), nub, foldl')
+import Data.Set (Set)
+import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
@@ -41,6 +47,7 @@ import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
import Agda.Syntax.Concrete.Generic
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Abstract as A
+import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
@@ -52,11 +59,12 @@ import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
-import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
- TCErr(..), extendedLambdaName, fresh,
- freshName, freshName_, freshNoName)
-import Agda.TypeChecking.Monad.Benchmark (billTo, billTop, reimburseTop)
+import Agda.TypeChecking.Monad.Base
+ ( TypeError(..) , Call(..) , typeError , genericError , TCErr(..)
+ , fresh , freshName , freshName_ , freshNoName , extendedLambdaName
+ )
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
+import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Trace (traceCall, setCurrentRange)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.MetaVars (registerInteractionPoint)
@@ -124,11 +132,6 @@ annotateExpr m = do
s <- getScope
return $ ScopedExpr s e
-expandEllipsis :: C.Pattern -> [C.Pattern] -> C.Clause -> C.Clause
-expandEllipsis _ _ c@(C.Clause _ C.LHS{} _ _ _) = c
-expandEllipsis p ps (C.Clause x (C.Ellipsis _ ps' eqs es) rhs wh wcs) =
- C.Clause x (C.LHS p (ps ++ ps') eqs es) rhs wh wcs
-
-- | Make sure that each variable occurs only once.
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
checkPatternLinearity ps = unlessNull (duplicates xs) $ \ ys -> do
@@ -170,7 +173,7 @@ recordConstructorType fields = build fs
build (NiceModuleMacro r p x modapp open dir{ publicOpen = False } : fs)
build (NiceField r f _ _ x (Common.Arg info e) : fs) =
- C.Pi [C.TypedBindings r $ Common.Arg info (C.TBind r [mkBoundName x f] e)] $ build fs
+ C.Pi [C.TypedBindings r $ Common.Arg info (C.TBind r [pure $ mkBoundName x f] e)] $ build fs
where r = getRange x
build (d : fs) = C.Let (getRange d) [notSoNiceDeclaration d] $
build fs
@@ -302,6 +305,12 @@ toAbstractCtx :: ToAbstract concrete abstract =>
Precedence -> concrete -> ScopeM abstract
toAbstractCtx ctx c = withContextPrecedence ctx $ toAbstract c
+toAbstractTopCtx :: ToAbstract c a => c -> ScopeM a
+toAbstractTopCtx = toAbstractCtx TopCtx
+
+toAbstractHiding :: (LensHiding h, ToAbstract c a) => h -> c -> ScopeM a
+toAbstractHiding h = toAbstractCtx $ hiddenArgumentCtx $ getHiding h
+
setContextCPS :: Precedence -> (a -> ScopeM b) ->
((a -> ScopeM b) -> ScopeM b) -> ScopeM b
setContextCPS p ret f = do
@@ -325,8 +334,7 @@ localToAbstract' x ret = do
withScope scope $ ret =<< toAbstract x
instance (ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1,c2) (a1,a2) where
- toAbstract (x,y) =
- (,) <$> toAbstract x <*> toAbstract y
+ toAbstract (x,y) = (,) <$> toAbstract x <*> toAbstract y
instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
ToAbstract (c1,c2,c3) (a1,a2,a3) where
@@ -334,19 +342,26 @@ instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
where
flatten (x,(y,z)) = (x,y,z)
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} ToAbstract c a => ToAbstract [c] [a] where
+#else
instance ToAbstract c a => ToAbstract [c] [a] where
- toAbstract = mapM toAbstract
+#endif
+ toAbstract = mapM toAbstract
instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
- toAbstract Nothing = return Nothing
- toAbstract (Just x) = Just <$> toAbstract x
+ toAbstract = traverse toAbstract
-- Names ------------------------------------------------------------------
newtype NewName a = NewName a
-newtype OldQName = OldQName C.QName
+data OldQName = OldQName C.QName (Maybe (Set A.Name))
+ -- ^ If a set is given, then the first name must correspond to one
+ -- of the names in the set.
newtype OldName = OldName C.Name
-newtype PatName = PatName C.QName
+data PatName = PatName C.QName (Maybe (Set A.Name))
+ -- ^ If a set is given, then the first name must correspond to one
+ -- of the names in the set.
instance ToAbstract (NewName C.Name) A.Name where
toAbstract (NewName x) = do
@@ -371,8 +386,8 @@ nameExpr d = mk (anameKind d) $ anameName d
where i = ExprRange (getRange x)
instance ToAbstract OldQName A.Expr where
- toAbstract (OldQName x) = do
- qx <- resolveName x
+ toAbstract (OldQName x ns) = do
+ qx <- resolveName' allKindsOfNames ns x
reportSLn "scope.name" 10 $ "resolved " ++ show x ++ ": " ++ show qx
case qx of
VarName x' -> return $ A.Var x'
@@ -387,9 +402,11 @@ data APatName = VarPatName A.Name
| PatternSynPatName AbstractName
instance ToAbstract PatName APatName where
- toAbstract (PatName x) = do
+ toAbstract (PatName x ns) = do
reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
- rx <- resolveName' [ConName, PatternSynName] x -- Andreas, 2013-03-21 ignore conflicting names which cannot be meant since we are in a pattern
+ rx <- resolveName' [ConName, PatternSynName] ns x
+ -- Andreas, 2013-03-21 ignore conflicting names which cannot
+ -- be meant since we are in a pattern
z <- case (rx, x) of
-- TODO: warn about shadowing
(VarName y, C.QName x) -> return $ Left x -- typeError $ RepeatedVariableInPattern y x
@@ -398,9 +415,7 @@ instance ToAbstract PatName APatName where
(UnknownName, C.QName x) -> return $ Left x
(ConstructorName ds, _) -> return $ Right (Left ds)
(PatternSynResName d, _) -> return $ Right (Right d)
- _ ->
- typeError $ GenericError $
- "Cannot pattern match on " ++ show x ++ ", because it is not a constructor"
+ _ -> genericError $ "Cannot pattern match on non-constructor " ++ prettyShow x
case z of
Left x -> do
reportSLn "scope.pat" 10 $ "it was a var: " ++ show x
@@ -436,7 +451,7 @@ checkForModuleClash x = do
ms <- scopeLookup (C.QName x) <$> getScope
unless (null ms) $ do
reportSLn "scope.clash" 20 $ "clashing modules ms = " ++ show ms
- setCurrentRange (getRange x) $
+ setCurrentRange x $
typeError $ ShadowedModule x $
map ((`withRangeOf` x) . amodName) ms
@@ -460,7 +475,8 @@ instance ToAbstract NewModuleQName A.ModuleName where
toAbs m' q
instance ToAbstract OldModuleName A.ModuleName where
- toAbstract (OldModuleName q) = amodName <$> resolveModule q
+ toAbstract (OldModuleName q) = setCurrentRange q $ do
+ amodName <$> resolveModule q
-- Expressions ------------------------------------------------------------
@@ -518,7 +534,7 @@ toAbstractLam r bs e ctx = do
e <- toAbstractCtx ctx e
-- We have at least one binder. Get first @b@ and rest @bs@.
caseList bs __IMPOSSIBLE__ $ \ b bs -> do
- return $ A.Lam (ExprRange r) b $ foldr mkLam e bs
+ return $ A.Lam (ExprRange r) b $ foldr mkLam e bs
where
mkLam b e = A.Lam (ExprRange $ fuseRange b e) b e
@@ -526,7 +542,7 @@ toAbstractLam r bs e ctx = do
scopeCheckExtendedLam :: Range -> [(C.LHS, C.RHS, WhereClause)] -> ScopeM A.Expr
scopeCheckExtendedLam r cs = do
whenM isInsideDotPattern $
- typeError $ GenericError "Extended lambdas are not allowed in dot patterns"
+ genericError "Extended lambdas are not allowed in dot patterns"
-- Find an unused name for the extended lambda definition.
cname <- nextlamname r 0 extendedLambdaName
@@ -570,7 +586,7 @@ instance ToAbstract C.Expr A.Expr where
traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of
-- Names
- Ident x -> toAbstract (OldQName x)
+ Ident x -> toAbstract (OldQName x Nothing)
-- Literals
C.Lit l -> return $ A.Lit l
@@ -598,8 +614,7 @@ instance ToAbstract C.Expr A.Expr where
-- Raw application
C.RawApp r es -> do
- e <- reimburseTop Bench.Scoping $ billTo [Bench.Parsing, Bench.Operators] $
- parseApplication es
+ e <- parseApplication es
toAbstract e
-- Application
@@ -609,7 +624,7 @@ instance ToAbstract C.Expr A.Expr where
return $ A.App (ExprRange r) e1 e2
-- Operator application
- C.OpApp r op es -> toAbstractOpApp op es
+ C.OpApp r op ns es -> toAbstractOpApp op ns es
-- With application
C.WithApp r e es -> do
@@ -652,7 +667,7 @@ instance ToAbstract C.Expr A.Expr where
-- Let
e0@(C.Let _ ds e) ->
- ifM isInsideDotPattern (typeError $ GenericError $ "Let-expressions are not allowed in dot patterns") $
+ ifM isInsideDotPattern (genericError $ "Let-expressions are not allowed in dot patterns") $
localToAbstract (LetDefs ds) $ \ds' -> do
e <- toAbstractCtx TopCtx e
let info = ExprRange (getRange e0)
@@ -681,7 +696,7 @@ instance ToAbstract C.Expr A.Expr where
-- Impossible things
C.ETel _ -> __IMPOSSIBLE__
- C.Equal{} -> typeError $ GenericError "Parse error: unexpected '='"
+ C.Equal{} -> genericError "Parse error: unexpected '='"
-- Quoting
C.QuoteGoal _ x e -> do
@@ -713,7 +728,7 @@ instance ToAbstract C.LamBinding A.LamBinding where
makeDomainFull :: C.LamBinding -> C.TypedBindings
makeDomainFull (C.DomainFull b) = b
makeDomainFull (C.DomainFree info x) =
- C.TypedBindings r $ Common.Arg info $ C.TBind r [x] $ C.Underscore r Nothing
+ C.TypedBindings r $ Common.Arg info $ C.TBind r [pure x] $ C.Underscore r Nothing
where r = getRange x
instance ToAbstract C.TypedBindings A.TypedBindings where
@@ -722,11 +737,9 @@ instance ToAbstract C.TypedBindings A.TypedBindings where
instance ToAbstract C.TypedBinding A.TypedBinding where
toAbstract (C.TBind r xs t) = do
t' <- toAbstractCtx TopCtx t
- xs' <- toAbstract (map NewName xs)
+ xs' <- toAbstract $ map (fmap NewName) xs
return $ A.TBind r xs' t'
- toAbstract (C.TLet r ds) = do
- ds' <- toAbstract (LetDefs ds)
- return $ A.TLet r ds'
+ toAbstract (C.TLet r ds) = A.TLet r <$> toAbstract (LetDefs ds)
-- | Scope check a module (top level function).
--
@@ -915,10 +928,14 @@ instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
-- | runs Syntax.Concrete.Definitions.niceDeclarations on main module
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
niceDecls ds = case runNice $ niceDeclarations ds of
- Left e -> throwError $ Exception (getRange e) (show e)
+ Left e -> throwError $ Exception (getRange e) $ pretty e
Right ds -> return ds
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPING #-} ToAbstract [C.Declaration] [A.Declaration] where
+#else
instance ToAbstract [C.Declaration] [A.Declaration] where
+#endif
toAbstract ds = do
-- don't allow to switch off termination checker in --safe mode
ds <- ifM (optSafe <$> commandLineOptions) (mapM noNoTermCheck ds) (return ds)
@@ -944,9 +961,9 @@ instance ToAbstract LetDef [A.LetBinding] where
case d of
NiceMutual _ _ d@[C.FunSig _ fx _ instanc info _ x t, C.FunDef _ _ _ abstract _ _ [cl]] ->
do when (abstract == AbstractDef) $ do
- typeError $ GenericError $ "abstract not allowed in let expressions"
+ genericError $ "abstract not allowed in let expressions"
when (instanc == InstanceDef) $ do
- typeError $ GenericError $ "Using instance is useless here, let expressions are always eligible for instance search."
+ genericError $ "Using instance is useless here, let expressions are always eligible for instance search."
e <- letToAbstract cl
t <- toAbstract t
x <- toAbstract (NewName $ mkBoundName x fx)
@@ -955,7 +972,10 @@ instance ToAbstract LetDef [A.LetBinding] where
-- irrefutable let binding, like (x , y) = rhs
NiceFunClause r PublicAccess ConcreteDef termCheck d@(C.FunClause lhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere) -> do
- mp <- setCurrentRange (getRange p) $ (Right <$> parsePattern p) `catchError` (return . Left)
+ mp <- setCurrentRange p $
+ (Right <$> parsePattern p)
+ `catchError`
+ (return . Left)
case mp of
Right p -> do
rhs <- toAbstract rhs
@@ -1015,10 +1035,10 @@ instance ToAbstract LetDef [A.LetBinding] where
localToAbstract (snd $ lhsArgs p) $ \args ->
-}
(x, args) <- do
- res <- setCurrentRange (getRange p) $ parseLHS top p
+ res <- setCurrentRange p $ parseLHS top p
case res of
C.LHSHead x args -> return (x, args)
- C.LHSProj{} -> typeError $ GenericError $ "copatterns not allowed in let bindings"
+ C.LHSProj{} -> genericError $ "copatterns not allowed in let bindings"
localToAbstract args $ \args ->
do rhs <- toAbstract rhs
@@ -1060,7 +1080,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
-- Fields
C.NiceField r f p a x t -> do
- unless (p == PublicAccess) $ typeError $ GenericError "Record fields can not be private"
+ unless (p == PublicAccess) $ genericError "Record fields can not be private"
-- Interaction points for record fields have already been introduced
-- when checking the type of the record constructor.
-- To avoid introducing interaction points (IP) twice, we turn
@@ -1121,7 +1141,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
-- Uncategorized function clauses
C.NiceFunClause r acc abs termCheck (C.FunClause lhs rhs wcls) ->
- typeError $ GenericError $
+ genericError $
"Missing type signature for left hand side " ++ show lhs
C.NiceFunClause{} -> __IMPOSSIBLE__
@@ -1134,7 +1154,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
dups = nub $ cs \\ nub cs
bad = filter (`elem` dups) cs
unless (distinct cs) $
- setCurrentRange (getRange bad) $
+ setCurrentRange bad $
typeError $ DuplicateConstructors dups
pars <- toAbstract pars
@@ -1186,7 +1206,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
scopeCheckNiceModule r p name tel $ toAbstract ds
NiceModule _ _ _ m@C.Qual{} _ _ ->
- typeError $ GenericError $ "Local modules cannot have qualified names"
+ genericError $ "Local modules cannot have qualified names"
NiceModuleMacro r p x modapp open dir ->
checkModuleMacro Apply r p x modapp open dir
@@ -1209,7 +1229,7 @@ instance ToAbstract NiceDeclaration A.Declaration where
ps <- toAbstract p
return $ map (A.Pragma r) ps
- NiceImport r x as open dir -> traceCall (SetRange r) $ do
+ NiceImport r x as open dir -> setCurrentRange r $ do
notPublicWithoutOpen open dir
-- First scope check the imported module and return its name and
@@ -1254,13 +1274,13 @@ instance ToAbstract NiceDeclaration A.Declaration where
}
return [ A.Import minfo m ]
- NiceUnquoteDecl r fx p a tc x e -> do
+ NiceUnquoteDecl r fx p i a tc x e -> do
y <- freshAbstractQName fx x
bindName p QuotableName x y
e <- toAbstract e
rebindName p DefName x y
let mi = MutualInfo tc r
- return [A.UnquoteDecl mi (mkDefInfo x fx p a r) y e]
+ return [A.UnquoteDecl mi (mkDefInfoInstance x fx p a i r) y e]
NicePatternSyn r fx n as p -> do
reportSLn "scope.pat" 10 $ "found nice pattern syn: " ++ show r
@@ -1328,81 +1348,100 @@ instance ToAbstract C.Pragma [A.Pragma] where
toAbstract (C.ImpossiblePragma _) = impossibleTest
toAbstract (C.OptionsPragma _ opts) = return [ A.OptionsPragma opts ]
toAbstract (C.RewritePragma _ x) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.RewritePragma x ]
A.Proj x -> return [ A.RewritePragma x ]
A.Con (AmbQ [x]) -> return [ A.RewritePragma x ]
- A.Con x -> fail $ "REWRITE used on ambiguous name " ++ show x
+ A.Con x -> genericError $ "REWRITE used on ambiguous name " ++ show x
+ A.Var x -> genericError $ "REWRITE used on parameter " ++ show x ++ " instead of on a defined symbol"
_ -> __IMPOSSIBLE__
toAbstract (C.CompiledTypePragma _ x hs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.CompiledTypePragma x hs ]
- _ -> fail $ "Bad compiled type: " ++ show x -- TODO: error message
+ _ -> genericError $ "Bad compiled type: " ++ prettyShow x -- TODO: error message
toAbstract (C.CompiledDataPragma _ x hs hcs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.CompiledDataPragma x hs hcs ]
- _ -> fail $ "Not a datatype: " ++ show x -- TODO: error message
+ _ -> genericError $ "Not a datatype: " ++ prettyShow x -- TODO: error message
toAbstract (C.CompiledPragma _ x hs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj x -> return x -- TODO: do we need to do s.th. special for projections? (Andreas, 2014-10-12)
- A.Con _ -> fail "Use COMPILED_DATA for constructors" -- TODO
+ A.Con _ -> genericError "Use COMPILED_DATA for constructors" -- TODO
_ -> __IMPOSSIBLE__
return [ A.CompiledPragma y hs ]
toAbstract (C.CompiledExportPragma _ x hs) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.CompiledExportPragma y hs ]
toAbstract (C.CompiledEpicPragma _ x ep) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.CompiledEpicPragma y ep ]
toAbstract (C.CompiledJSPragma _ x ep) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj x -> return x
A.Con (AmbQ [x]) -> return x
- A.Con x -> fail ("COMPILED_JS used on ambiguous name " ++ show x)
+ A.Con x -> genericError $
+ "COMPILED_JS used on ambiguous name " ++ prettyShow x
_ -> __IMPOSSIBLE__
return [ A.CompiledJSPragma y ep ]
toAbstract (C.StaticPragma _ x) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.StaticPragma y ]
toAbstract (C.BuiltinPragma _ b e) = do
+ -- Andreas, 2015-02-14
+ -- Some builtins cannot be given a valid Agda type,
+ -- thus, they do not come with accompanying postulate or definition.
+ if b `elem` builtinsNoDef then do
+ case e of
+ C.Ident q@(C.QName x) -> do
+ unlessM ((UnknownName ==) <$> resolveName q) $ genericError $
+ "BUILTIN " ++ b ++ " declares an identifier " ++
+ "(no longer expects an already defined identifier)"
+ y <- freshAbstractQName defaultFixity' x
+ bindName PublicAccess DefName x y
+ return [ A.BuiltinNoDefPragma b y ]
+ _ -> genericError $
+ "Pragma BUILTIN " ++ b ++ ": expected unqualified identifier, " ++
+ "but found expression " ++ prettyShow e
+ else do
e <- toAbstract e
return [ A.BuiltinPragma b e ]
toAbstract (C.ImportPragma _ i) = do
addHaskellImport i
return []
toAbstract (C.EtaPragma _ x) = do
- e <- toAbstract $ OldQName x
+ e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.EtaPragma x ]
- _ -> fail "Bad ETA pragma"
+ _ -> do
+ e <- showA e
+ genericError $ "Pragma ETA: expected identifier, " ++
+ "but found expression " ++ e
-- Termination checking pragmes are handled by the nicifier
toAbstract C.TerminationCheckPragma{} = __IMPOSSIBLE__
instance ToAbstract C.Clause A.Clause where
- toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'" -- TODO: errors message
+ toAbstract (C.Clause top C.Ellipsis{} _ _ _) = genericError "bad '...'" -- TODO: error message
toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
-- Andreas, 2012-02-14: need to reset local vars before checking subclauses
vars <- getLocalVars
- let wcs' = for wcs $ \ c -> do
- setLocalVars vars
- return $ expandEllipsis p wps c
- lhs' <- toAbstract (LeftHandSide top p wps)
+ let wcs' = for wcs $ \ c -> setLocalVars vars $> c
+ lhs' <- toAbstract $ LeftHandSide top p wps
printLocals 10 "after lhs:"
let (whname, whds) = case wh of
NoWhere -> (Nothing, [])
@@ -1420,16 +1459,12 @@ instance ToAbstract C.Clause A.Clause where
return $ A.Clause lhs' rhs ds
whereToAbstract :: Range -> Maybe C.Name -> [C.Declaration] -> ScopeM a -> ScopeM (a, [A.Declaration])
-whereToAbstract _ _ [] inner = do
- x <- inner
- return (x, [])
+whereToAbstract _ _ [] inner = (,[]) <$> inner
whereToAbstract r whname whds inner = do
- m <- maybe (nameConcrete <$> freshNoName noRange) return whname
- m <- if (maybe False isNoName whname)
- then do
- (i :: NameId) <- fresh
- return (C.NoName (getRange m) i)
- else return m
+ -- Create a fresh concrete name if there isn't (a proper) one.
+ m <- case whname of
+ Just m | not (isNoName m) -> return m
+ _ -> C.NoName (getRange whname) <$> fresh
let acc = maybe PrivateAccess (const PublicAccess) whname -- unnamed where's are private
let tel = []
old <- getCurrentModule
@@ -1440,23 +1475,25 @@ whereToAbstract r whname whds inner = do
setCurrentModule old
bindModule acc m am
-- Issue 848: if the module was anonymous (module _ where) open it public
- when (maybe False isNoName whname) $
+ let anonymous = maybe False isNoName whname
+ when anonymous $
openModule_ (C.QName m) $
defaultImportDir { publicOpen = True }
return (x, ds)
data RightHandSide = RightHandSide
- { rhsRewriteEqn :: [C.RewriteEqn] -- ^ @rewrite e@ (many)
- , rhsWithExpr :: [C.WithExpr] -- ^ @with e@ (many)
+ { rhsRewriteEqn :: [C.RewriteEqn] -- ^ @rewrite e@ (many)
+ , rhsWithExpr :: [C.WithExpr] -- ^ @with e@ (many)
, rhsSubclauses :: [ScopeM C.Clause] -- ^ the subclauses spawned by a with (monadic because we need to reset the local vars before checking these clauses)
, rhs :: C.RHS
, rhsWhereDecls :: [C.Declaration]
}
-data AbstractRHS = AbsurdRHS'
- | WithRHS' [A.Expr] [ScopeM C.Clause] -- ^ The with clauses haven't been translated yet
- | RHS' A.Expr
- | RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
+data AbstractRHS
+ = AbsurdRHS'
+ | WithRHS' [A.Expr] [ScopeM C.Clause] -- ^ The with clauses haven't been translated yet
+ | RHS' A.Expr
+ | RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
qualifyName_ :: A.Name -> ScopeM A.QName
qualifyName_ x = do
@@ -1474,7 +1511,7 @@ instance ToAbstract AbstractRHS A.RHS where
toAbstract (RewriteRHS' eqs rhs wh) = do
auxs <- replicateM (length eqs) $ withFunctionName "rewrite-"
rhs <- toAbstract rhs
- return $ RewriteRHS auxs eqs rhs wh
+ return $ RewriteRHS (zip auxs eqs) rhs wh
toAbstract (WithRHS' es cs) = do
aux <- withFunctionName "with-"
A.WithRHS aux es <$> do toAbstract =<< sequence cs
@@ -1539,7 +1576,7 @@ instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
d <- case qx of
FieldName d -> return $ anameName d
UnknownName -> notInScope d
- _ -> typeError $ GenericError $
+ _ -> genericError $
"head of copattern needs to be a field identifier, but "
++ show d ++ " isn't one"
args1 <- toAbstract ps1
@@ -1547,9 +1584,12 @@ instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
args2 <- toAbstract ps2
return $ A.LHSProj d args1 l args2
+instance ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) where
+ toAbstract (WithHiding h a) = WithHiding h <$> toAbstractHiding h a
+
instance ToAbstract c a => ToAbstract (C.Arg c) (A.Arg a) where
toAbstract (Common.Arg info e) =
- Common.Arg <$> toAbstract info <*> toAbstractCtx (hiddenArgumentCtx $ getHiding info) e
+ Common.Arg <$> toAbstract info <*> toAbstractHiding info e
instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
toAbstract (Named n e) = Named n <$> toAbstract e
@@ -1587,32 +1627,37 @@ instance ToAbstract (A.Pattern' C.Expr) (A.Pattern' A.Expr) where
toAbstract (A.ImplicitP i) = return $ A.ImplicitP i
toAbstract (A.PatternSynP i x as) = A.PatternSynP i x <$> mapM toAbstract as
+resolvePatternIdentifier ::
+ Range -> C.QName -> Maybe (Set A.Name) -> ScopeM (A.Pattern' C.Expr)
+resolvePatternIdentifier r x ns = do
+ px <- toAbstract (PatName x ns)
+ case px of
+ VarPatName y -> return $ VarP y
+ ConPatName ds -> return $ ConP (ConPatInfo False $ PatRange r)
+ (AmbQ $ map anameName ds)
+ []
+ PatternSynPatName d -> return $ PatternSynP (PatRange r)
+ (anameName d) []
+
instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
- toAbstract p@(C.IdentP x) = do
- px <- toAbstract (PatName x)
- case px of
- VarPatName y -> return $ VarP y
- ConPatName ds -> return $ ConP (ConPatInfo False $ PatRange (getRange p))
- (AmbQ $ map anameName ds)
- []
- PatternSynPatName d -> return $ PatternSynP (PatRange (getRange p))
- (anameName d) []
+ toAbstract (C.IdentP x) =
+ resolvePatternIdentifier (getRange x) x Nothing
toAbstract (AppP (QuoteP _) p)
| IdentP x <- namedArg p,
getHiding p == NotHidden = do
- e <- toAbstract (OldQName x)
+ e <- toAbstract (OldQName x Nothing)
let quoted (A.Def x) = return x
quoted (A.Proj x) = return x
quoted (A.Con (AmbQ [x])) = return x
- quoted (A.Con (AmbQ xs)) = typeError $ GenericError $ "quote: Ambigous name: " ++ show xs
+ quoted (A.Con (AmbQ xs)) = genericError $ "quote: Ambigous name: " ++ show xs
quoted (A.ScopedExpr _ e) = quoted e
- quoted _ = typeError $ GenericError $ "quote: not a defined name"
+ quoted _ = genericError $ "quote: not a defined name"
A.LitP . LitQName (getRange x) <$> quoted e
toAbstract (QuoteP r) =
- typeError $ GenericError "quote must be applied to an identifier"
+ genericError "quote must be applied to an identifier"
toAbstract p0@(AppP p q) = do
(p', q') <- toAbstract (p,q)
@@ -1625,20 +1670,16 @@ instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
r = getRange p0
info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
- toAbstract p0@(OpAppP r op ps) = do
- p <- toAbstract (IdentP op)
+ toAbstract p0@(OpAppP r op ns ps) = do
+ p <- resolvePatternIdentifier (getRange op) op (Just ns)
ps <- toAbstract ps
case p of
- ConP i x as -> return $ ConP (i {patInfo = info}) x
- (as ++ ps)
- DefP _ x as -> return $ DefP info x
- (as ++ ps)
- PatternSynP _ x as -> return $ PatternSynP info x
- (as ++ ps)
+ ConP i x as -> return $ ConP (i {patInfo = info}) x (as ++ ps)
+ DefP _ x as -> return $ DefP info x (as ++ ps)
+ PatternSynP _ x as -> return $ PatternSynP info x (as ++ ps)
_ -> __IMPOSSIBLE__
where
- r = getRange p0
- info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
+ info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
-- Removed when parsing
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
@@ -1664,11 +1705,11 @@ instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
-- | Turn an operator application into abstract syntax. Make sure to record the
-- right precedences for the various arguments.
-toAbstractOpApp :: C.QName -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
-toAbstractOpApp op es = do
+toAbstractOpApp :: C.QName -> Set A.Name -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
+toAbstractOpApp op ns es = do
-- Get the notation for the operator.
- f <- getFixity op
- let parts = notation . oldToNewNotation $ (op, f)
+ nota <- getNotation op ns
+ let parts = notation nota
-- We can throw away the @BindingHoles@, since binders
-- have been preprocessed into @OpApp C.Expr@.
let nonBindingParts = filter (not . isBindingHole) parts
@@ -1676,8 +1717,8 @@ toAbstractOpApp op es = do
-- If not, crash.
unless (length (filter isAHole nonBindingParts) == length es) __IMPOSSIBLE__
-- Translate operator and its arguments (each in the right context).
- op <- toAbstract (OldQName op)
- foldl' app op <$> left (theFixity f) nonBindingParts es
+ op <- toAbstract (OldQName op (Just ns))
+ foldl' app op <$> left (notaFixity nota) nonBindingParts es
where
-- Build an application in the abstract syntax, with correct Range.
app e arg = A.App (ExprRange (fuseRange e arg)) e (setArgColors [] arg)