#if __GLASGOW_HASKELL__ <= 708
#endif
module Agda.Syntax.Translation.ConcreteToAbstract
( ToAbstract(..), localToAbstract
, concreteToAbstract_
, concreteToAbstract
, NewModuleQName(..)
, OldName(..)
, TopLevel(..)
, TopLevelInfo(..)
, topLevelModuleName
, AbstractRHS
, NewModuleName, OldModuleName
, NewName, OldQName
, LeftHandSide, RightHandSide
, PatName, APatName, LetDef, LetDefs
) where
import Prelude hiding (mapM, null)
import Control.Applicative
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
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)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Info
import Agda.Syntax.Concrete.Definitions as C
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.AbstractToConcrete (ToConcrete)
import Agda.TypeChecking.Monad.Base
( TypeError(..) , Call(..) , typeError , genericError , TCErr(..)
, fresh , freshName , freshName_ , freshNoName , extendedLambdaName
, envAbstractMode , AbstractMode(..)
)
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)
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Env (insideDotPattern, isInsideDotPattern)
import Agda.TypeChecking.Pretty hiding (pretty, prettyA)
import Agda.Interaction.FindFile (checkModuleName)
import Agda.Interaction.Imports (scopeCheckImport)
import Agda.Interaction.Options
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Pretty (render, Pretty, pretty, prettyShow)
#include "undefined.h"
import Agda.Utils.Impossible
import Agda.ImpossibleTest (impossibleTest)
notAnExpression :: C.Expr -> ScopeM A.Expr
notAnExpression e = typeError $ NotAnExpression e
nothingAppliedToHiddenArg :: C.Expr -> ScopeM A.Expr
nothingAppliedToHiddenArg e = typeError $ NothingAppliedToHiddenArg e
nothingAppliedToInstanceArg :: C.Expr -> ScopeM A.Expr
nothingAppliedToInstanceArg e = typeError $ NothingAppliedToInstanceArg e
notAValidLetBinding :: NiceDeclaration -> ScopeM a
notAValidLetBinding d = typeError $ NotAValidLetBinding d
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- getLocalVars
reportSLn "scope.top" v $ s ++ " " ++ show locals
annotateDecl :: ScopeM A.Declaration -> ScopeM A.Declaration
annotateDecl m = annotateDecls $ (:[]) <$> m
annotateDecls :: ScopeM [A.Declaration] -> ScopeM A.Declaration
annotateDecls m = do
ds <- m
s <- getScope
return $ ScopedDecl s ds
annotateExpr :: ScopeM A.Expr -> ScopeM A.Expr
annotateExpr m = do
e <- m
s <- getScope
return $ ScopedExpr s e
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
checkPatternLinearity ps = unlessNull (duplicates xs) $ \ ys -> do
typeError $ RepeatedVariablesInPattern ys
where
xs = concatMap vars ps
vars :: A.Pattern' e -> [C.Name]
vars p = case p of
A.VarP x -> [nameConcrete x]
A.ConP _ _ args -> concatMap (vars . namedArg) args
A.WildP _ -> []
A.AsP _ x p -> nameConcrete x : vars p
A.DotP _ _ -> []
A.AbsurdP _ -> []
A.LitP _ -> []
A.DefP _ _ args -> concatMap (vars . namedArg) args
A.PatternSynP _ _ args -> concatMap (vars . namedArg) args
recordConstructorType :: [NiceDeclaration] -> C.Expr
recordConstructorType fields = build fs
where
fs = reverse $ dropWhile notField $ reverse fields
notField NiceField{} = False
notField _ = True
build (NiceOpen r m dir@ImportDirective{ publicOpen = True } : fs) =
build (NiceOpen r m dir{ publicOpen = False } : fs)
build (NiceModuleMacro r p x modapp open dir@ImportDirective{ publicOpen = True } : 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 [pure $ mkBoundName x f] e)] $ build fs
where r = getRange x
build (d : fs) = C.Let (getRange d) [notSoNiceDeclaration d] $
build fs
build [] = C.SetN noRange 0
checkModuleApplication
:: C.ModuleApplication
-> ModuleName
-> C.Name
-> ImportDirective
-> ScopeM (A.ModuleApplication, Ren A.QName, Ren ModuleName)
checkModuleApplication (C.SectionApp _ tel e) m0 x dir' = do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking ModuleApplication " ++ prettyShow x
]
withCurrentModule m0 $ do
(m, args) <- parseModuleApplication e
tel' <- toAbstract tel
(m1, args') <- toAbstract (OldModuleName m, args)
let noRecConstr | null args = id
| otherwise = removeOnlyQualified
(s', (renM, renD)) <- copyScope m m0 . noRecConstr =<< getNamedScope m1
s' <- applyImportDirectiveM (C.QName x) dir' s'
modifyCurrentScope $ const s'
printScope "mod.inst" 20 "copied source module"
reportSLn "scope.mod.inst" 30 $ "renamings:\n " ++ show renD ++ "\n " ++ show renM
let amodapp = A.SectionApp tel' m1 args'
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked ModuleApplication " ++ prettyShow x
]
reportSDoc "scope.decl" 70 $ vcat $
[ nest 2 $ prettyA amodapp
]
return (amodapp, renD, renM)
checkModuleApplication (C.RecordModuleIFS _ recN) m0 x dir' =
withCurrentModule m0 $ do
m1 <- toAbstract $ OldModuleName recN
s <- getNamedScope m1
(s', (renM, renD)) <- copyScope recN m0 s
s' <- applyImportDirectiveM recN dir' s'
modifyCurrentScope $ const s'
printScope "mod.inst" 20 "copied record module"
return ((A.RecordModuleIFS m1), renD, renM)
checkModuleMacro
:: (Pretty c, ToConcrete a c)
=> (ModuleInfo -> ModuleName -> A.ModuleApplication -> Ren A.QName -> Ren ModuleName -> a)
-> Range
-> Access
-> C.Name
-> C.ModuleApplication
-> OpenShortHand
-> ImportDirective
-> ScopeM [a]
checkModuleMacro apply r p x modapp open dir = do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking ModuleMacro " ++ prettyShow x
]
notPublicWithoutOpen open dir
m0 <- toAbstract (NewModuleName x)
reportSDoc "scope.decl" 90 $ text "NewModuleName: m0 =" <+> prettyA m0
printScope "mod.inst" 20 "module macro"
let dir' = case open of
DontOpen -> dir
DoOpen -> defaultImportDir
(modapp', renD, renM) <- withLocalVars $ checkModuleApplication modapp m0 x dir'
printScope "mod.inst.app" 20 "checkModuleMacro, after checkModuleApplication"
reportSDoc "scope.decl" 90 $ text "after mod app: trying to print m0 ..."
reportSDoc "scope.decl" 90 $ text "after mod app: m0 =" <+> prettyA m0
bindModule p x m0
reportSDoc "scope.decl" 90 $ text "after bindMod: m0 =" <+> prettyA m0
printScope "mod.inst.copy.after" 20 "after copying"
when (open == DoOpen) $
openModule_ (C.QName x) dir
printScope "mod.inst" 20 $ show open
reportSDoc "scope.decl" 90 $ text "after open : m0 =" <+> prettyA m0
stripNoNames
printScope "mod.inst" 10 $ "after stripping"
reportSDoc "scope.decl" 90 $ text "after stripNo: m0 =" <+> prettyA m0
let m = m0 `withRangesOf` [x]
adecls = [ apply info m modapp' renD renM ]
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked ModuleMacro " ++ prettyShow x
]
reportSLn "scope.decl" 90 $ "info = " ++ show info
reportSLn "scope.decl" 90 $ "m = " ++ show m
reportSLn "scope.decl" 90 $ "modapp' = " ++ show modapp'
reportSLn "scope.decl" 90 $ "renD = " ++ show renD
reportSLn "scope.decl" 90 $ "renM = " ++ show renM
reportSDoc "scope.decl" 70 $ vcat $
map (nest 2 . prettyA) adecls
return adecls
where
info = ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dir
, minfoOpenShort = Just open
, minfoDirective = Just dir
}
notPublicWithoutOpen :: OpenShortHand -> ImportDirective -> ScopeM ()
notPublicWithoutOpen DoOpen dir = return ()
notPublicWithoutOpen DontOpen dir = when (publicOpen dir) $ typeError $
GenericError
"The public keyword must only be used together with the open keyword"
renamingRange :: ImportDirective -> Range
renamingRange = getRange . map renToRange . renaming
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a
concreteToAbstract_ x = toAbstract x
concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a
concreteToAbstract scope x = withScope_ scope (toAbstract x)
class ToAbstract concrete abstract | concrete -> abstract where
toAbstract :: concrete -> ScopeM abstract
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
p' <- getContextPrecedence
withContextPrecedence p $ f $ withContextPrecedence p' . ret
localToAbstractCtx :: ToAbstract concrete abstract =>
Precedence -> concrete -> (abstract -> ScopeM a) -> ScopeM a
localToAbstractCtx ctx c ret = setContextCPS ctx ret (localToAbstract c)
localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b
localToAbstract x ret = fst <$> localToAbstract' x ret
localToAbstract' :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM (b, ScopeInfo)
localToAbstract' x ret = do
scope <- getScope
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
instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
ToAbstract (c1,c2,c3) (a1,a2,a3) where
toAbstract (x,y,z) = flatten <$> toAbstract (x,(y,z))
where
flatten (x,(y,z)) = (x,y,z)
#if __GLASGOW_HASKELL__ >= 710
instance ToAbstract c a => ToAbstract [c] [a] where
#else
instance ToAbstract c a => ToAbstract [c] [a] where
#endif
toAbstract = mapM toAbstract
instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
toAbstract = traverse toAbstract
newtype NewName a = NewName a
data OldQName = OldQName C.QName (Maybe (Set A.Name))
newtype OldName = OldName C.Name
data PatName = PatName C.QName (Maybe (Set A.Name))
instance ToAbstract (NewName C.Name) A.Name where
toAbstract (NewName x) = do
y <- freshAbstractName_ x
bindVariable x y
return y
instance ToAbstract (NewName C.BoundName) A.Name where
toAbstract (NewName BName{ boundName = x, bnameFixity = fx }) = do
y <- freshAbstractName fx x
bindVariable x y
return y
nameExpr :: AbstractName -> A.Expr
nameExpr d = mk (anameKind d) $ anameName d
where
mk DefName x = A.Def x
mk FldName x = A.Proj x
mk ConName x = A.Con $ AmbQ [x]
mk PatternSynName x = A.PatternSyn x
mk QuotableName x = A.App i (A.Quote i) (defaultNamedArg $ A.Def x)
where i = ExprRange (getRange x)
instance ToAbstract OldQName A.Expr where
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'
DefinedName _ d -> return $ nameExpr d
FieldName d -> return $ nameExpr d
ConstructorName ds -> return $ A.Con $ AmbQ (map anameName ds)
UnknownName -> notInScope x
PatternSynResName d -> return $ nameExpr d
data APatName = VarPatName A.Name
| ConPatName [AbstractName]
| PatternSynPatName AbstractName
instance ToAbstract PatName APatName where
toAbstract (PatName x ns) = do
reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
rx <- resolveName' [ConName, PatternSynName] ns x
z <- case (rx, x) of
(VarName y, C.QName x) -> return $ Left x
(FieldName d, C.QName x) -> return $ Left x
(DefinedName _ d, C.QName x) | DefName == anameKind d -> return $ Left x
(UnknownName, C.QName x) -> return $ Left x
(ConstructorName ds, _) -> return $ Right (Left ds)
(PatternSynResName d, _) -> return $ Right (Right d)
_ -> 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
p <- VarPatName <$> toAbstract (NewName x)
printLocals 10 "bound it:"
return p
Right (Left ds) -> do
reportSLn "scope.pat" 10 $ "it was a con: " ++ show (map anameName ds)
return $ ConPatName ds
Right (Right d) -> do
reportSLn "scope.pat" 10 $ "it was a pat syn: " ++ show (anameName d)
return $ PatternSynPatName d
instance ToAbstract OldName A.QName where
toAbstract (OldName x) = do
rx <- resolveName (C.QName x)
case rx of
DefinedName _ d -> return $ anameName d
_ -> __IMPOSSIBLE__
newtype NewModuleName = NewModuleName C.Name
newtype NewModuleQName = NewModuleQName C.QName
newtype OldModuleName = OldModuleName C.QName
freshQModule :: A.ModuleName -> C.Name -> ScopeM A.ModuleName
freshQModule m x = A.qualifyM m . mnameFromList . (:[]) <$> freshAbstractName_ x
checkForModuleClash :: C.Name -> ScopeM ()
checkForModuleClash x = do
ms <- scopeLookup (C.QName x) <$> getScope
unless (null ms) $ do
reportSLn "scope.clash" 20 $ "clashing modules ms = " ++ show ms
setCurrentRange x $
typeError $ ShadowedModule x $
map ((`withRangeOf` x) . amodName) ms
instance ToAbstract NewModuleName A.ModuleName where
toAbstract (NewModuleName x) = do
checkForModuleClash x
m <- getCurrentModule
y <- freshQModule m x
createModule False y
return y
instance ToAbstract NewModuleQName A.ModuleName where
toAbstract (NewModuleQName m) = toAbs noModuleName m
where
toAbs m (C.QName x) = do
y <- freshQModule m x
createModule False y
return y
toAbs m (C.Qual x q) = do
m' <- freshQModule m x
toAbs m' q
instance ToAbstract OldModuleName A.ModuleName where
toAbstract (OldModuleName q) = setCurrentRange q $ do
amodName <$> resolveModule q
mkNamedArg :: C.Expr -> C.NamedArg C.Expr
mkNamedArg (C.HiddenArg _ e) = Common.Arg (setHiding Hidden defaultArgInfo) e
mkNamedArg (C.InstanceArg _ e) = Common.Arg (setHiding Instance defaultArgInfo) e
mkNamedArg e = Common.Arg defaultArgInfo $ unnamed e
mkArg' :: C.ArgInfo -> C.Expr -> C.Arg C.Expr
mkArg' info (C.HiddenArg _ e) = Common.Arg (setHiding Hidden info) $ namedThing e
mkArg' info (C.InstanceArg _ e) = Common.Arg (setHiding Instance info) $ namedThing e
mkArg' info e = Common.Arg (setHiding NotHidden info) e
mkArg :: C.Expr -> C.Arg C.Expr
mkArg e = mkArg' defaultArgInfo e
toAbstractDot :: Precedence -> C.Expr -> ScopeM (A.Expr, Bool)
toAbstractDot prec e = do
reportSLn "scope.irrelevance" 100 $ "toAbstractDot: " ++ (render $ pretty e)
traceCall (ScopeCheckExpr e) $ case e of
C.Dot _ e -> do
e <- toAbstractCtx prec e
return (e, True)
C.RawApp r es -> do
e <- parseApplication es
toAbstractDot prec e
C.Paren _ e -> toAbstractDot TopCtx e
e -> do
e <- toAbstractCtx prec e
return (e, False)
toAbstractOpArg :: Precedence -> OpApp C.Expr -> ScopeM A.Expr
toAbstractOpArg ctx (Ordinary e) = toAbstractCtx ctx e
toAbstractOpArg ctx (SyntaxBindingLambda r bs e) = toAbstractLam r bs e ctx
toAbstractLam :: Range -> [C.LamBinding] -> C.Expr -> Precedence -> ScopeM A.Expr
toAbstractLam r bs e ctx = do
localToAbstract (map (C.DomainFull . makeDomainFull) bs) $ \ bs -> do
e <- toAbstractCtx ctx e
caseList bs __IMPOSSIBLE__ $ \ b bs -> do
return $ A.Lam (ExprRange r) b $ foldr mkLam e bs
where
mkLam b e = A.Lam (ExprRange $ fuseRange b e) b e
scopeCheckExtendedLam :: Range -> [(C.LHS, C.RHS, WhereClause)] -> ScopeM A.Expr
scopeCheckExtendedLam r cs = do
whenM isInsideDotPattern $
genericError "Extended lambdas are not allowed in dot patterns"
cname <- nextlamname r 0 extendedLambdaName
name <- freshAbstractName_ cname
reportSLn "scope.extendedLambda" 10 $ "new extended lambda name: " ++ show name
qname <- qualifyName_ name
bindName PrivateAccess DefName cname qname
a <- aModeToDef <$> asks envAbstractMode
let
insertApp (C.RawAppP r es) = C.RawAppP r $ IdentP (C.QName cname) : es
insertApp (C.IdentP q ) = C.RawAppP r $ IdentP (C.QName cname) : [C.IdentP q]
where r = getRange q
insertApp _ = __IMPOSSIBLE__
d = C.FunDef r [] defaultFixity' a __IMPOSSIBLE__ cname $
for cs $ \ (lhs, rhs, wh) ->
C.Clause cname (mapLhsOriginalPattern insertApp lhs) rhs wh []
scdef <- toAbstract d
case scdef of
A.ScopedDecl si [A.FunDef di qname' NotDelayed cs] -> do
setScope si
return $ A.ExtendedLam (ExprRange r) di qname' cs
_ -> __IMPOSSIBLE__
where
nextlamname :: Range -> Int -> String -> ScopeM C.Name
nextlamname r i s = do
let cname = C.Name r [Id $ stringToRawName $ s ++ show i]
rn <- resolveName $ C.QName cname
case rn of
UnknownName -> return cname
_ -> nextlamname r (i+1) s
instance ToAbstract C.Expr A.Expr where
toAbstract e =
traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of
Ident x -> toAbstract (OldQName x Nothing)
C.Lit l -> return $ A.Lit l
C.QuestionMark r n -> do
scope <- getScope
ii <- registerInteractionPoint r n
let info = MetaInfo
{ metaRange = r
, metaScope = scope
, metaNumber = Nothing
, metaNameSuggestion = ""
}
return $ A.QuestionMark info ii
C.Underscore r n -> do
scope <- getScope
return $ A.Underscore $ MetaInfo
{ metaRange = r
, metaScope = scope
, metaNumber = maybe Nothing __IMPOSSIBLE__ n
, metaNameSuggestion = fromMaybe "" n
}
C.RawApp r es -> do
e <- parseApplication es
toAbstract e
C.App r e1 e2 -> do
e1 <- toAbstractCtx FunctionCtx e1
e2 <- toAbstractCtx ArgumentCtx e2
return $ A.App (ExprRange r) e1 e2
C.OpApp r op ns es -> toAbstractOpApp op ns es
C.WithApp r e es -> do
e <- toAbstractCtx WithFunCtx e
es <- mapM (toAbstractCtx WithArgCtx) es
return $ A.WithApp (ExprRange r) e es
C.HiddenArg _ _ -> nothingAppliedToHiddenArg e
C.InstanceArg _ _ -> nothingAppliedToInstanceArg e
C.AbsurdLam r h -> return $ A.AbsurdLam (ExprRange r) h
C.Lam r bs e -> toAbstractLam r bs e TopCtx
C.ExtendedLam r cs -> scopeCheckExtendedLam r cs
C.Fun r e1 e2 -> do
Common.Arg info (e0, dotted) <- traverse (toAbstractDot FunctionSpaceDomainCtx) $ mkArg e1
info <- toAbstract info
let e1 = Common.Arg ((if dotted then setRelevance Irrelevant else id) info) e0
e2 <- toAbstractCtx TopCtx e2
return $ A.Fun (ExprRange r) e1 e2
e0@(C.Pi tel e) ->
localToAbstract tel $ \tel -> do
e <- toAbstractCtx TopCtx e
let info = ExprRange (getRange e0)
return $ A.Pi info tel e
C.Set _ -> return $ A.Set (ExprRange $ getRange e) 0
C.SetN _ n -> return $ A.Set (ExprRange $ getRange e) n
C.Prop _ -> return $ A.Prop $ ExprRange $ getRange e
e0@(C.Let _ ds e) ->
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)
return $ A.Let info ds' e
C.Rec r fs -> do
let (xs, es) = unzip fs
es <- toAbstractCtx TopCtx es
return $ A.Rec (ExprRange r) $ zip xs es
C.RecUpdate r e fs -> do
let (xs, es) = unzip fs
e <- toAbstract e
es <- toAbstractCtx TopCtx es
return $ A.RecUpdate (ExprRange r) e $ zip xs es
C.Paren _ e -> toAbstractCtx TopCtx e
C.Dot _ _ -> notAnExpression e
C.As _ _ _ -> notAnExpression e
C.Absurd _ -> notAnExpression e
C.ETel _ -> __IMPOSSIBLE__
C.Equal{} -> genericError "Parse error: unexpected '='"
C.QuoteGoal _ x e -> do
x' <- toAbstract (NewName x)
e' <- toAbstract e
return $ A.QuoteGoal (ExprRange $ getRange e) x' e'
C.QuoteContext _ x e -> do
x' <- toAbstract (NewName x)
e' <- toAbstract e
return $ A.QuoteContext (ExprRange $ getRange e) x' e'
C.Quote r -> return $ A.Quote (ExprRange r)
C.QuoteTerm r -> return $ A.QuoteTerm (ExprRange r)
C.Unquote r -> return $ A.Unquote (ExprRange r)
C.Tactic r e es -> do
g <- freshName r "g"
let re = ExprRange (getRange e)
e : es <- toAbstract (e : es)
let tac = A.App re e (defaultNamedArg $ A.Var g)
return $ A.QuoteGoal (ExprRange r) g $ foldl (A.App re) (A.Unquote re) (map defaultNamedArg $ tac : es)
C.DontCare e -> A.DontCare <$> toAbstract e
instance ToAbstract C.LamBinding A.LamBinding where
toAbstract (C.DomainFree info x) = A.DomainFree <$> toAbstract info <*> toAbstract (NewName x)
toAbstract (C.DomainFull tb) = A.DomainFull <$> toAbstract tb
makeDomainFull :: C.LamBinding -> C.TypedBindings
makeDomainFull (C.DomainFull b) = b
makeDomainFull (C.DomainFree info x) =
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
toAbstract (C.TypedBindings r bs) = A.TypedBindings r <$> toAbstract bs
instance ToAbstract C.TypedBinding A.TypedBinding where
toAbstract (C.TBind r xs t) = do
t' <- toAbstractCtx TopCtx t
xs' <- toAbstract $ map (fmap NewName) xs
return $ A.TBind r xs' t'
toAbstract (C.TLet r ds) = A.TLet r <$> toAbstract (LetDefs ds)
scopeCheckNiceModule
:: Range
-> Access
-> C.Name
-> C.Telescope
-> ScopeM [A.Declaration]
-> ScopeM [A.Declaration]
scopeCheckNiceModule r p name tel checkDs
| telHasOpenStmsOrModuleMacros tel = do
scopeCheckNiceModule noRange p noName_ [] $
scopeCheckNiceModule_
| otherwise = do
scopeCheckNiceModule_
where
scopeCheckNiceModule_ = do
(name, p, open) <- do
if isNoName name then do
(i :: NameId) <- fresh
return (C.NoName (getRange name) i, PrivateAccess, True)
else return (name, p, False)
aname <- toAbstract (NewModuleName name)
ds <- snd <$> do
scopeCheckModule r (C.QName name) aname tel checkDs
bindModule p name aname
when open $
openModule_ (C.QName name) $
defaultImportDir { publicOpen = True }
return ds
telHasOpenStmsOrModuleMacros :: C.Telescope -> Bool
telHasOpenStmsOrModuleMacros = any yesBinds
where
yesBinds (C.TypedBindings _ tb) = yesBind $ unArg tb
yesBind C.TBind{} = False
yesBind (C.TLet _ ds) = any yes ds
yes C.ModuleMacro{} = True
yes C.Open{} = True
yes C.Import{} = True
yes (C.Mutual _ ds) = any yes ds
yes (C.Abstract _ ds) = any yes ds
yes (C.Private _ ds) = any yes ds
yes _ = False
class EnsureNoLetStms a where
ensureNoLetStms :: a -> ScopeM ()
instance EnsureNoLetStms C.TypedBinding where
ensureNoLetStms tb =
case tb of
C.TLet{} -> typeError $ IllegalLetInTelescope tb
C.TBind{} -> return ()
instance EnsureNoLetStms a => EnsureNoLetStms (LamBinding' a) where
ensureNoLetStms = traverse_ ensureNoLetStms
instance EnsureNoLetStms a => EnsureNoLetStms (TypedBindings' a) where
ensureNoLetStms = traverse_ ensureNoLetStms
instance EnsureNoLetStms a => EnsureNoLetStms [a] where
ensureNoLetStms = traverse_ ensureNoLetStms
scopeCheckModule
:: Range
-> C.QName
-> A.ModuleName
-> C.Telescope
-> ScopeM [A.Declaration]
-> ScopeM (ScopeInfo, [A.Declaration])
scopeCheckModule r x qm tel checkDs = do
printScope "module" 20 $ "checking module " ++ show x
res <- withLocalVars $ do
tel <- toAbstract tel
withCurrentModule qm $ do
printScope "module" 20 $ "inside module " ++ show x
ds <- checkDs
scope <- getScope
return (scope, [ A.Section info (qm `withRangesOfQ` x) tel ds ])
printScope "module" 20 $ "after module " ++ show x
return res
where
info = ModuleInfo r noRange Nothing Nothing Nothing
data TopLevel a = TopLevel
{ topLevelPath :: AbsolutePath
, topLevelTheThing :: a
}
data TopLevelInfo = TopLevelInfo
{ topLevelDecls :: [A.Declaration]
, outsideScope :: ScopeInfo
, insideScope :: ScopeInfo
}
topLevelModuleName :: TopLevelInfo -> A.ModuleName
topLevelModuleName topLevel = scopeCurrent (insideScope topLevel)
instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
toAbstract (TopLevel file ds) =
caseMaybe (initLast ds) __IMPOSSIBLE__ $
\ (outsideDecls, C.Module r m0 tel insideDecls) -> do
m <- if isNoName m0
then return $ C.QName $ C.Name noRange [Id $ stringToRawName $ rootName file]
else do
checkModuleName (C.toTopLevelModuleName m0) file
return m0
setTopLevelModule m
am <- toAbstract (NewModuleQName m)
outsideDecls <- toAbstract outsideDecls
(insideScope, insideDecls) <- scopeCheckModule r m am tel $
toAbstract insideDecls
outsideScope <- getScope
return $ TopLevelInfo (outsideDecls ++ insideDecls) outsideScope insideScope
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
niceDecls ds = case runNice $ niceDeclarations ds of
Left e -> throwError $ Exception (getRange e) $ pretty e
Right ds -> return ds
#if __GLASGOW_HASKELL__ >= 710
instance ToAbstract [C.Declaration] [A.Declaration] where
#else
instance ToAbstract [C.Declaration] [A.Declaration] where
#endif
toAbstract ds = do
ds <- ifM (optSafe <$> commandLineOptions) (mapM noNoTermCheck ds) (return ds)
toAbstract =<< niceDecls ds
where
noNoTermCheck (C.Pragma (C.TerminationCheckPragma r NoTerminationCheck)) =
typeError $ SafeFlagNoTerminationCheck
noNoTermCheck (C.Pragma (C.TerminationCheckPragma r NonTerminating)) =
typeError $ SafeFlagNonTerminating
noNoTermCheck (C.Pragma (C.TerminationCheckPragma r Terminating)) =
typeError $ SafeFlagTerminating
noNoTermCheck d = return d
newtype LetDefs = LetDefs [C.Declaration]
newtype LetDef = LetDef NiceDeclaration
instance ToAbstract LetDefs [A.LetBinding] where
toAbstract (LetDefs ds) =
concat <$> (toAbstract =<< map LetDef <$> niceDecls ds)
instance ToAbstract LetDef [A.LetBinding] where
toAbstract (LetDef d) =
case d of
NiceMutual _ _ d@[C.FunSig _ fx _ instanc info _ x t, C.FunDef _ _ _ abstract _ _ [cl]] ->
do when (abstract == AbstractDef) $ do
genericError $ "abstract not allowed in let expressions"
when (instanc == InstanceDef) $ do
genericError $ "Using instance is useless here, let expressions are always eligible for instance search."
(x', e) <- letToAbstract cl
t <- toAbstract t
x <- setRange (fuseRange x x') <$> toAbstract (NewName $ mkBoundName x fx)
info <- toAbstract info
return [ A.LetBind (LetRange $ getRange d) info x t e ]
NiceFunClause r PublicAccess ConcreteDef termCheck d@(C.FunClause lhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere) -> do
mp <- setCurrentRange p $
(Right <$> parsePattern p)
`catchError`
(return . Left)
case mp of
Right p -> do
rhs <- toAbstract rhs
p <- toAbstract p
checkPatternLinearity [p]
p <- toAbstract p
return [ A.LetPatBind (LetRange r) p rhs ]
Left err ->
case definedName p of
Nothing -> throwError err
Just x -> toAbstract $ LetDef $ NiceMutual r termCheck
[ C.FunSig r defaultFixity' PublicAccess NotInstanceDef defaultArgInfo termCheck x (C.Underscore (getRange x) Nothing)
, C.FunDef r __IMPOSSIBLE__ __IMPOSSIBLE__ ConcreteDef __IMPOSSIBLE__ __IMPOSSIBLE__
[C.Clause x lhs (C.RHS rhs) NoWhere []]
]
where
definedName (C.IdentP (C.QName x)) = Just x
definedName C.IdentP{} = Nothing
definedName (C.RawAppP _ (p : _)) = definedName p
definedName (C.ParenP _ p) = definedName p
definedName C.WildP{} = Nothing
definedName C.AbsurdP{} = Nothing
definedName C.AsP{} = Nothing
definedName C.DotP{} = Nothing
definedName C.LitP{} = Nothing
definedName C.QuoteP{} = Nothing
definedName C.HiddenP{} = __IMPOSSIBLE__
definedName C.InstanceP{} = __IMPOSSIBLE__
definedName C.RawAppP{} = __IMPOSSIBLE__
definedName C.AppP{} = __IMPOSSIBLE__
definedName C.OpAppP{} = __IMPOSSIBLE__
NiceOpen r x dirs | not (C.publicOpen dirs) -> do
m <- toAbstract (OldModuleName x)
openModule_ x dirs
let minfo = ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dirs
, minfoOpenShort = Nothing
, minfoDirective = Just dirs
}
return [A.LetOpen minfo m]
NiceModuleMacro r p x modapp open dir | not (C.publicOpen dir) ->
checkModuleMacro LetApply r PrivateAccess x modapp open dir
_ -> notAValidLetBinding d
where
letToAbstract (C.Clause top clhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere []) = do
(x, args) <- do
res <- setCurrentRange p $ parseLHS top p
case res of
C.LHSHead x args -> return (x, args)
C.LHSProj{} -> genericError $ "copatterns not allowed in let bindings"
e <- localToAbstract args $ \args ->
do rhs <- toAbstract rhs
foldM lambda rhs (reverse args)
return (x, e)
letToAbstract _ = notAValidLetBinding d
lambda e (Common.Arg info (Named Nothing (A.VarP x))) =
return $ A.Lam i (A.DomainFree info x) e
where
i = ExprRange (fuseRange x e)
lambda e (Common.Arg info (Named Nothing (A.WildP i))) =
do x <- freshNoName (getRange i)
return $ A.Lam i' (A.DomainFree info x) e
where
i' = ExprRange (fuseRange i e)
lambda _ _ = notAValidLetBinding d
newtype Blind a = Blind { unBlind :: a }
instance ToAbstract (Blind a) (Blind a) where
toAbstract = return
aDefToMode :: IsAbstract -> AbstractMode
aDefToMode AbstractDef = AbstractMode
aDefToMode ConcreteDef = ConcreteMode
aModeToDef :: AbstractMode -> IsAbstract
aModeToDef AbstractMode = AbstractDef
aModeToDef ConcreteMode = ConcreteDef
aModeToDef _ = __IMPOSSIBLE__
instance ToAbstract NiceDeclaration A.Declaration where
toAbstract d = annotateDecls $
traceCall (ScopeCheckDeclaration d) $
caseMaybe (niceHasAbstract d) id (\ a -> local $ \ e -> e { envAbstractMode = aDefToMode a }) $
case d of
C.Axiom r f p i rel x t -> do
clo <- commandLineOptions
when (optSafe clo) (typeError (SafeFlagPostulate x))
toAbstractNiceAxiom A.NoFunSig d
C.NiceField r f p a x t -> do
unless (p == PublicAccess) $ genericError "Record fields can not be private"
let maskIP (C.QuestionMark r _) = C.Underscore r Nothing
maskIP e = e
t' <- toAbstractCtx TopCtx $ mapExpr maskIP t
y <- freshAbstractQName f x
irrProj <- optIrrelevantProjections <$> pragmaOptions
unless (isIrrelevant t && not irrProj) $
bindName p FldName x y
return [ A.Field (mkDefInfo x f p a r) y t' ]
PrimitiveFunction r f p a x t -> do
t' <- toAbstractCtx TopCtx t
y <- freshAbstractQName f x
bindName p DefName x y
return [ A.Primitive (mkDefInfo x f p a r) y t' ]
NiceMutual r termCheck ds -> do
ds' <- toAbstract ds
return [ A.Mutual (MutualInfo termCheck r) ds' ]
C.NiceRecSig r f a x ls t -> do
ensureNoLetStms ls
withLocalVars $ do
ls' <- toAbstract (map makeDomainFull ls)
x' <- freshAbstractQName f x
bindName a DefName x x'
t' <- toAbstract t
return [ A.RecSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]
C.NiceDataSig r f a x ls t -> withLocalVars $ do
printScope "scope.data.sig" 20 ("checking DataSig for " ++ show x)
ensureNoLetStms ls
ls' <- toAbstract (map makeDomainFull ls)
x' <- freshAbstractQName f x
bindName a DefName x x'
t' <- toAbstract t
return [ A.DataSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]
C.FunSig r f p i rel tc x t -> toAbstractNiceAxiom A.FunSig (C.Axiom r f p i rel x t)
C.FunDef r ds f a tc x cs -> do
printLocals 10 $ "checking def " ++ show x
(x',cs) <- toAbstract (OldName x,cs)
let delayed = NotDelayed
return [ A.FunDef (mkDefInfo x f PublicAccess a r) x' delayed cs ]
C.NiceFunClause r acc abs termCheck (C.FunClause lhs rhs wcls) ->
genericError $
"Missing type signature for left hand side " ++ show lhs
C.NiceFunClause{} -> __IMPOSSIBLE__
C.DataDef r f a x pars cons -> withLocalVars $ do
printScope "scope.data.def" 20 ("checking DataDef for " ++ show x)
ensureNoLetStms pars
do let cs = map conName cons
dups = nub $ cs \\ nub cs
bad = filter (`elem` dups) cs
unless (distinct cs) $
setCurrentRange bad $
typeError $ DuplicateConstructors dups
pars <- toAbstract pars
DefinedName p ax <- resolveName (C.QName x)
let x' = anameName ax
checkForModuleClash x
let m = mnameFromList $ qnameToList x'
createModule True m
bindModule p x m
cons <- toAbstract (map (ConstrDecl NoRec m a p) cons)
printScope "data" 20 $ "Checked data " ++ show x
return [ A.DataDef (mkDefInfo x f PublicAccess a r) x' pars cons ]
where
conName (C.Axiom _ _ _ _ _ c _) = c
conName _ = __IMPOSSIBLE__
C.RecDef r f a x ind cm pars fields -> do
ensureNoLetStms pars
withLocalVars $ do
checkForModuleClash x
pars <- toAbstract pars
DefinedName p ax <- resolveName (C.QName x)
let x' = anameName ax
contel <- toAbstract $ recordConstructorType fields
m0 <- getCurrentModule
let m = A.qualifyM m0 $ mnameFromList $ (:[]) $ last $ qnameToList x'
printScope "rec" 15 "before record"
createModule False m
afields <- withCurrentModule m $ do
afields <- toAbstract fields
printScope "rec" 15 "checked fields"
return afields
bindModule p x m
cm' <- mapM (\(ThingWithFixity c f) -> bindConstructorName m c f a p YesRec) cm
printScope "rec" 15 "record complete"
return [ A.RecDef (mkDefInfo x f PublicAccess a r) x' ind cm' pars contel afields ]
NiceModule r p a x@(C.QName name) tel ds -> do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking NiceModule " ++ prettyShow x
]
adecls <- traceCall (ScopeCheckDeclaration $ NiceModule r p a x tel []) $ do
scopeCheckNiceModule r p name tel $ toAbstract ds
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked NiceModule " ++ prettyShow x
] ++ map (nest 2 . prettyA) adecls
return adecls
NiceModule _ _ _ m@C.Qual{} _ _ ->
genericError $ "Local modules cannot have qualified names"
NiceModuleMacro r p x modapp open dir -> do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking NiceModuleMacro " ++ prettyShow x
]
adecls <- checkModuleMacro Apply r p x modapp open dir
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked NiceModuleMacro " ++ prettyShow x
] ++ map (nest 2 . prettyA) adecls
return adecls
NiceOpen r x dir -> do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking NiceOpen " ++ prettyShow x
]
m <- toAbstract (OldModuleName x)
printScope "open" 20 $ "opening " ++ show x
openModule_ x dir
printScope "open" 20 $ "result:"
let minfo = ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dir
, minfoOpenShort = Nothing
, minfoDirective = Just dir
}
let adecls = [A.Open minfo m]
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked NiceOpen " ++ prettyShow x
] ++ map (nest 2 . prettyA) adecls
return adecls
NicePragma r p -> do
ps <- toAbstract p
return $ map (A.Pragma r) ps
NiceImport r x as open dir -> setCurrentRange r $ do
notPublicWithoutOpen open dir
(m, i) <- withCurrentModule noModuleName $ withTopLevelModule x $ do
m <- toAbstract $ NewModuleQName x
printScope "import" 10 "before import:"
(m, i) <- scopeCheckImport m
printScope "import" 10 $ "scope checked import: " ++ show i
return (m, Map.delete noModuleName i)
modifyScopes $ \ ms -> Map.unionWith mergeScope (Map.delete m ms) i
case as of
Nothing -> bindQModule PrivateAccess x m
Just y -> bindModule PrivateAccess (asName y) m
printScope "import" 10 "merged imported sig:"
let (name, theAsSymbol, theAsName) = case as of
Nothing -> (x, noRange, Nothing)
Just a -> (C.QName (asName a), asRange a, Just (asName a))
case open of
DoOpen -> void $ toAbstract [ C.Open r name dir ]
DontOpen -> modifyNamedScopeM m $ applyImportDirectiveM x dir
let minfo = ModuleInfo
{ minfoRange = r
, minfoAsName = theAsName
, minfoAsTo = getRange (theAsSymbol, renamingRange dir)
, minfoOpenShort = Just open
, minfoDirective = Just dir
}
return [ A.Import minfo m ]
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 (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
y <- freshAbstractQName fx n
bindName PublicAccess PatternSynName n y
defn@(as, p) <- withLocalVars $ do
p <- toAbstract =<< toAbstract =<< parsePatternSyn p
checkPatternLinearity [p]
as <- (traverse . mapM) (unVarName <=< resolveName . C.QName) as
as <- (map . fmap) unBlind <$> toAbstract ((map . fmap) Blind as)
return (as, p)
modifyPatternSyns (Map.insert y defn)
return [A.PatternSynDef y as p]
where unVarName (VarName a) = return a
unVarName _ = typeError $ UnusedVariableInPatternSynonym
where
toAbstractNiceAxiom funSig (C.Axiom r f p i info x t) = do
t' <- toAbstractCtx TopCtx t
y <- freshAbstractQName f x
info <- toAbstract info
bindName p DefName x y
return [ A.Axiom funSig (mkDefInfoInstance x f p ConcreteDef i r) info y t' ]
toAbstractNiceAxiom _ _ = __IMPOSSIBLE__
data IsRecordCon = YesRec | NoRec
data ConstrDecl = ConstrDecl IsRecordCon A.ModuleName IsAbstract Access C.NiceDeclaration
bindConstructorName :: ModuleName -> C.Name -> Fixity'-> IsAbstract ->
Access -> IsRecordCon -> ScopeM A.QName
bindConstructorName m x f a p record = do
y <- withCurrentModule m $ freshAbstractQName f x
bindName p' ConName x y
withCurrentModule m $ bindName p'' ConName x y
return y
where
p' = case a of
AbstractDef -> PrivateAccess
_ -> p
p'' = case (a, record) of
(AbstractDef, _) -> PrivateAccess
(_, YesRec) -> OnlyQualified
_ -> PublicAccess
instance ToAbstract ConstrDecl A.Declaration where
toAbstract (ConstrDecl record m a p d) = do
case d of
C.Axiom r f _ i info x t -> do
t' <- toAbstractCtx TopCtx t
y <- bindConstructorName m x f a p record
info <- toAbstract info
printScope "con" 15 "bound constructor"
return $ A.Axiom NoFunSig (mkDefInfoInstance x f p ConcreteDef i r) info y t'
_ -> typeError . GenericDocError $
P.text "Illegal declaration in data type definition " P.$$
P.nest 2 (pretty (notSoNiceDeclaration d))
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 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 -> 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 Nothing
case e of
A.Def x -> return [ A.CompiledTypePragma x hs ]
_ -> genericError $ "Bad compiled type: " ++ prettyShow x
toAbstract (C.CompiledDataPragma _ x hs hcs) = do
e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ A.CompiledDataPragma x hs hcs ]
_ -> genericError $ "Not a datatype: " ++ prettyShow x
toAbstract (C.CompiledPragma _ x hs) = do
e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj x -> return x
A.Con _ -> genericError "Use COMPILED_DATA for constructors"
_ -> __IMPOSSIBLE__
return [ A.CompiledPragma y hs ]
toAbstract (C.CompiledExportPragma _ x hs) = do
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 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 Nothing
y <- case e of
A.Def x -> return x
A.Proj x -> return x
A.Con (AmbQ [x]) -> return 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 Nothing
y <- case e of
A.Def x -> return x
_ -> __IMPOSSIBLE__
return [ A.StaticPragma y ]
toAbstract (C.BuiltinPragma _ b e) = do
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 Nothing
case e of
A.Def x -> return [ A.EtaPragma x ]
_ -> do
e <- showA e
genericError $ "Pragma ETA: expected identifier, " ++
"but found expression " ++ e
toAbstract C.TerminationCheckPragma{} = __IMPOSSIBLE__
instance ToAbstract C.Clause A.Clause where
toAbstract (C.Clause top C.Ellipsis{} _ _ _) = genericError "bad '...'"
toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
vars <- getLocalVars
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, [])
AnyWhere ds -> (Nothing, ds)
SomeWhere m ds -> (Just m, ds)
let isTerminationPragma :: C.Declaration -> Bool
isTerminationPragma (C.Pragma (TerminationCheckPragma _ _)) = True
isTerminationPragma _ = False
if not (null eqs)
then do
rhs <- toAbstract =<< toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs whds)
return $ A.Clause lhs' rhs []
else do
when (any isTerminationPragma whds) $
genericError "Termination pragmas are not allowed inside where clauses"
(rhs, ds) <- whereToAbstract (getRange wh) whname whds $
toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs [])
rhs <- toAbstract rhs
return $ A.Clause lhs' rhs ds
whereToAbstract :: Range -> Maybe C.Name -> [C.Declaration] -> ScopeM a -> ScopeM (a, [A.Declaration])
whereToAbstract _ _ [] inner = (,[]) <$> inner
whereToAbstract r whname whds inner = do
m <- case whname of
Just m | not (isNoName m) -> return m
_ -> C.NoName (getRange whname) <$> fresh
let acc = maybe PrivateAccess (const PublicAccess) whname
let tel = []
old <- getCurrentModule
am <- toAbstract (NewModuleName m)
(scope, ds) <- scopeCheckModule r (C.QName m) am tel $ toAbstract whds
setScope scope
x <- inner
setCurrentModule old
bindModule acc m am
let anonymous = maybe False isNoName whname
when anonymous $
openModule_ (C.QName m) $
defaultImportDir { publicOpen = True }
return (x, ds)
data RightHandSide = RightHandSide
{ rhsRewriteEqn :: [C.RewriteEqn]
, rhsWithExpr :: [C.WithExpr]
, rhsSubclauses :: [ScopeM C.Clause]
, rhs :: C.RHS
, rhsWhereDecls :: [C.Declaration]
}
data AbstractRHS
= AbsurdRHS'
| WithRHS' [A.Expr] [ScopeM C.Clause]
| RHS' A.Expr
| RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
qualifyName_ :: A.Name -> ScopeM A.QName
qualifyName_ x = do
m <- getCurrentModule
return $ A.qualify m x
withFunctionName :: String -> ScopeM A.QName
withFunctionName s = do
NameId i _ <- fresh
qualifyName_ =<< freshName_ (s ++ show i)
instance ToAbstract AbstractRHS A.RHS where
toAbstract AbsurdRHS' = return A.AbsurdRHS
toAbstract (RHS' e) = return $ A.RHS e
toAbstract (RewriteRHS' eqs rhs wh) = do
auxs <- replicateM (length eqs) $ withFunctionName "rewrite-"
rhs <- toAbstract rhs
return $ RewriteRHS (zip auxs eqs) rhs wh
toAbstract (WithRHS' es cs) = do
aux <- withFunctionName "with-"
A.WithRHS aux es <$> do toAbstract =<< sequence cs
instance ToAbstract RightHandSide AbstractRHS where
toAbstract (RightHandSide eqs@(_:_) es cs rhs wh) = do
eqs <- toAbstractCtx TopCtx eqs
(rhs, ds) <- whereToAbstract (getRange wh) Nothing wh $
toAbstract (RightHandSide [] es cs rhs [])
return $ RewriteRHS' eqs rhs ds
toAbstract (RightHandSide [] [] (_ : _) _ _) = __IMPOSSIBLE__
toAbstract (RightHandSide [] (_ : _) _ (C.RHS _) _) = typeError $ BothWithAndRHS
toAbstract (RightHandSide [] [] [] rhs []) = toAbstract rhs
toAbstract (RightHandSide [] es cs C.AbsurdRHS []) = do
es <- toAbstractCtx TopCtx es
return $ WithRHS' es cs
toAbstract (RightHandSide [] (_ : _) _ C.AbsurdRHS (_ : _)) = __IMPOSSIBLE__
toAbstract (RightHandSide [] [] [] (C.RHS _) (_ : _)) = __IMPOSSIBLE__
toAbstract (RightHandSide [] [] [] C.AbsurdRHS (_ : _)) = __IMPOSSIBLE__
instance ToAbstract C.RHS AbstractRHS where
toAbstract C.AbsurdRHS = return $ AbsurdRHS'
toAbstract (C.RHS e) = RHS' <$> toAbstract e
data LeftHandSide = LeftHandSide C.Name C.Pattern [C.Pattern]
instance ToAbstract LeftHandSide A.LHS where
toAbstract (LeftHandSide top lhs wps) =
traceCall (ScopeCheckLHS top lhs) $ do
lhscore <- parseLHS top lhs
reportSLn "scope.lhs" 5 $ "parsed lhs: " ++ show lhscore
printLocals 10 "before lhs:"
unlessM (optCopatterns <$> pragmaOptions) $
case lhscore of
C.LHSProj{} -> typeError $ NeedOptionCopatterns
C.LHSHead{} -> return ()
lhscore <- toAbstract lhscore
reportSLn "scope.lhs" 5 $ "parsed lhs patterns: " ++ show lhscore
wps <- toAbstract =<< mapM parsePattern wps
checkPatternLinearity $ lhsCoreAllPatterns lhscore ++ wps
printLocals 10 "checked pattern:"
lhscore <- toAbstract lhscore
reportSLn "scope.lhs" 5 $ "parsed lhs dot patterns: " ++ show lhscore
wps <- toAbstract wps
printLocals 10 "checked dots:"
return $ A.LHS (LHSRange $ getRange (lhs, wps)) lhscore wps
instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
toAbstract (C.LHSHead x ps) = do
x <- withLocalVars $ setLocalVars [] >> toAbstract (OldName x)
args <- toAbstract ps
return $ A.LHSHead x args
toAbstract (C.LHSProj d ps1 l ps2) = do
qx <- resolveName d
d <- case qx of
FieldName d -> return $ anameName d
UnknownName -> notInScope d
_ -> genericError $
"head of copattern needs to be a field identifier, but "
++ show d ++ " isn't one"
args1 <- toAbstract ps1
l <- toAbstract l
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 <*> toAbstractHiding info e
instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
toAbstract (Named n e) = Named n <$> toAbstract e
instance ToAbstract (A.LHSCore' C.Expr) (A.LHSCore' A.Expr) where
toAbstract (A.LHSHead f ps) = A.LHSHead f <$> mapM toAbstract ps
toAbstract (A.LHSProj d ps lhscore ps') = A.LHSProj d <$> mapM toAbstract ps
<*> mapM toAbstract lhscore <*> mapM toAbstract ps'
instance ToAbstract c a => ToAbstract (A.NamedArg c) (A.NamedArg a) where
toAbstract (Common.Arg info c) = liftM2 Common.Arg (return info) (toAbstract c)
instance ToAbstract C.ArgInfo A.ArgInfo where
toAbstract info = do cs <- mapM toAbstract $ argInfoColors info
return $ info { argInfoColors = cs }
instance ToAbstract (A.Pattern' C.Expr) (A.Pattern' A.Expr) where
toAbstract (A.VarP x) = return $ A.VarP x
toAbstract (A.ConP i ds as) = A.ConP i ds <$> mapM toAbstract as
toAbstract (A.DefP i x as) = A.DefP i x <$> mapM toAbstract as
toAbstract (A.WildP i) = return $ A.WildP i
toAbstract (A.AsP i x p) = A.AsP i x <$> toAbstract p
toAbstract (A.DotP i e) = A.DotP i <$> insideDotPattern (toAbstract e)
toAbstract (A.AbsurdP i) = return $ A.AbsurdP i
toAbstract (A.LitP l) = return $ A.LitP l
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 ConPCon $ PatRange r)
(AmbQ $ map anameName ds)
[]
PatternSynPatName d -> return $ PatternSynP (PatRange r)
(anameName d) []
instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
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 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)) = genericError $ "quote: Ambigous name: " ++ show xs
quoted (A.ScopedExpr _ e) = quoted e
quoted _ = genericError $ "quote: not a defined name"
A.LitP . LitQName (getRange x) <$> quoted e
toAbstract (QuoteP r) =
genericError "quote must be applied to an identifier"
toAbstract p0@(AppP p q) = do
(p', q') <- toAbstract (p,q)
case p' of
ConP i x as -> return $ ConP (i {patInfo = info}) x (as ++ [q'])
DefP _ x as -> return $ DefP info x (as ++ [q'])
PatternSynP _ x as -> return $ PatternSynP info x (as ++ [q'])
_ -> typeError $ InvalidPattern p0
where
r = getRange p0
info = PatRange r
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)
_ -> __IMPOSSIBLE__
where
info = PatRange r
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
toAbstract (InstanceP _ _) = __IMPOSSIBLE__
toAbstract (RawAppP _ _) = __IMPOSSIBLE__
toAbstract p@(C.WildP r) = return $ A.WildP (PatRange r)
toAbstract (C.ParenP _ p) = toAbstract p
toAbstract (C.LitP l) = return $ A.LitP l
toAbstract p0@(C.AsP r x p) = typeError $ NotSupported "@-patterns"
toAbstract p0@(C.DotP r e) = return $ A.DotP info e
where info = PatRange r
toAbstract p0@(C.AbsurdP r) = return $ A.AbsurdP info
where info = PatRange r
toAbstractOpApp :: C.QName -> Set A.Name -> [C.NamedArg (OpApp C.Expr)] -> ScopeM A.Expr
toAbstractOpApp op ns es = do
nota <- getNotation op ns
let parts = notation nota
let nonBindingParts = filter (not . isBindingHole) parts
unless (length (filter isAHole nonBindingParts) == length es) __IMPOSSIBLE__
op <- toAbstract (OldQName op (Just ns))
foldl' app op <$> left (notaFixity nota) nonBindingParts es
where
app e arg = A.App (ExprRange (fuseRange e arg)) e (setArgColors [] arg)
toAbsOpArg cxt = traverse $ traverse $ toAbstractOpArg cxt
left f (IdPart _ : xs) es = inside f xs es
left f (_ : xs) (e : es) = do
e <- toAbsOpArg (LeftOperandCtx f) e
es <- inside f xs es
return (e : es)
left f (_ : _) [] = __IMPOSSIBLE__
left f [] _ = __IMPOSSIBLE__
inside f [x] es = right f x es
inside f (IdPart _ : xs) es = inside f xs es
inside f (_ : xs) (e : es) = do
e <- toAbsOpArg InsideOperandCtx e
es <- inside f xs es
return (e : es)
inside _ (_ : _) [] = __IMPOSSIBLE__
inside _ [] _ = __IMPOSSIBLE__
right _ (IdPart _) [] = return []
right f _ [e] = do
e <- toAbsOpArg (RightOperandCtx f) e
return [e]
right _ _ _ = __IMPOSSIBLE__