{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Translation.ConcreteToAbstract
( ToAbstract(..), localToAbstract
, concreteToAbstract_
, concreteToAbstract
, NewModuleQName(..)
, OldName(..)
, TopLevel(..)
, TopLevelInfo(..)
, topLevelModuleName
, AbstractRHS
, NewModuleName, OldModuleName
, NewName, OldQName
, PatName, APatName
) where
import Prelude hiding ( mapM, null )
import Control.Applicative
import Control.Arrow (second)
import Control.Monad.Reader hiding (mapM)
import Data.Foldable (Foldable, traverse_)
import Data.Traversable (mapM, traverse)
import Data.Set (Set)
import Data.Map (Map)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
import Data.Void
import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
import Agda.Syntax.Concrete.Generic
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Concrete.Pattern
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern ( patternVars, checkPatternLinearity )
import Agda.Syntax.Abstract.Pretty
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Concrete.Definitions as C
import Agda.Syntax.Fixity
import Agda.Syntax.Concrete.Fixity (DoWarn(..))
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base as A
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.AbstractToConcrete (ToConcrete)
import Agda.Syntax.DoNotation
import Agda.Syntax.IdiomBrackets
import Agda.TypeChecking.Monad.Base hiding (ModuleInfo, MetaInfo)
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.Debug
import Agda.TypeChecking.Monad.Env (insideDotPattern, isInsideDotPattern, getCurrentPath)
import Agda.TypeChecking.Rules.Builtin (isUntypedBuiltin, bindUntypedBuiltin, builtinKindOfName)
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty hiding (pretty, prettyA)
import Agda.TypeChecking.Warnings
import Agda.Interaction.FindFile (checkModuleName, rootNameModule, SourceFile(SourceFile))
import {-# SOURCE #-} Agda.Interaction.Imports (scopeCheckImport)
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Options.Warnings
import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Either
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
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 qualified Agda.Utils.Pretty as P
import Agda.Utils.Pretty (render, Pretty, pretty, prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Tuple
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
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
noDotorEqPattern :: String -> A.Pattern' e -> ScopeM (A.Pattern' Void)
noDotorEqPattern err = dot
where
dot :: A.Pattern' e -> ScopeM (A.Pattern' Void)
dot p = case p of
A.VarP x -> pure $ A.VarP x
A.ConP i c args -> A.ConP i c <$> (traverse $ traverse $ traverse dot) args
A.ProjP i o d -> pure $ A.ProjP i o d
A.WildP i -> pure $ A.WildP i
A.AsP i x p -> A.AsP i x <$> dot p
A.DotP{} -> genericError err
A.EqualP{} -> genericError err
A.AbsurdP i -> pure $ A.AbsurdP i
A.LitP l -> pure $ A.LitP l
A.DefP i f args -> A.DefP i f <$> (traverse $ traverse $ traverse dot) args
A.PatternSynP i c args -> A.PatternSynP i c <$> (traverse $ traverse $ traverse dot) args
A.RecP i fs -> A.RecP i <$> (traverse $ traverse dot) fs
A.WithP i p -> A.WithP i <$> dot p
newtype RecordConstructorType = RecordConstructorType [C.Declaration]
instance ToAbstract RecordConstructorType A.Expr where
toAbstract (RecordConstructorType ds) = recordConstructorType ds
recordConstructorType :: [C.Declaration] -> ScopeM A.Expr
recordConstructorType decls =
niceDecls NoWarn decls $ buildType . takeFields
where
takeFields = List.dropWhileEnd notField
notField NiceField{} = False
notField _ = True
buildType :: [C.NiceDeclaration] -> ScopeM A.Expr
buildType ds = do
tel <- mapM makeBinding ds
return $ A.Pi (ExprRange (getRange ds)) tel (A.Set exprNoRange 0)
makeBinding :: C.NiceDeclaration -> ScopeM A.TypedBinding
makeBinding d = do
let failure = typeError $ NotValidBeforeField d
r = getRange d
info = ExprRange r
mkLet d = A.TLet r <$> toAbstract (LetDef d)
traceCall (SetRange r) $ case d of
C.NiceField r pr ab inst tac x a -> do
fx <- getConcreteFixity x
let bv = unnamed (C.mkBinder $ (C.mkBoundName x fx) { bnameTactic = tac }) <$ a
tel <- toAbstract $ C.TBind r [bv] (unArg a)
return tel
C.NiceOpen r m dir -> do
mkLet $ C.NiceOpen r m dir{ publicOpen = Nothing }
C.NiceModuleMacro r p x modapp open dir -> do
mkLet $ C.NiceModuleMacro r p x modapp open dir{ publicOpen = Nothing }
C.NiceMutual _ _ _ _
[ C.FunSig _ _ _ _ macro _ _ _ _ _
, C.FunDef _ _ abstract _ _ _ _
[ C.Clause _ _ (C.LHS _p [] [] NoEllipsis) (C.RHS _) NoWhere [] ]
] | abstract /= AbstractDef && macro /= MacroDef -> do
mkLet d
C.NiceMutual{} -> failure
C.Axiom{} -> failure
C.PrimitiveFunction{} -> failure
C.NiceModule{} -> failure
C.NiceImport{} -> failure
C.NicePragma{} -> failure
C.NiceRecSig{} -> failure
C.NiceDataSig{} -> failure
C.NiceFunClause{} -> failure
C.FunSig{} -> failure
C.FunDef{} -> failure
C.NiceDataDef{} -> failure
C.NiceRecDef{} -> failure
C.NicePatternSyn{} -> failure
C.NiceGeneralize{} -> failure
C.NiceUnquoteDecl{} -> failure
C.NiceUnquoteDef{} -> failure
checkModuleApplication
:: C.ModuleApplication
-> ModuleName
-> C.Name
-> C.ImportDirective
-> ScopeM (A.ModuleApplication, ScopeCopyInfo, A.ImportDirective)
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 <- toAbstract $ OldModuleName m
args' <- toAbstractCtx (ArgumentCtx PreferParen) args
(adir, s) <- applyImportDirectiveM (C.QName x) dir' =<< getNamedScope m1
(s', copyInfo) <- copyScope m m0 s
modifyCurrentScope $ const s'
printScope "mod.inst" 20 "copied source module"
reportSDoc "scope.mod.inst" 30 $ return $ pretty copyInfo
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, copyInfo, adir)
checkModuleApplication (C.RecordModuleInstance _ recN) m0 x dir' =
withCurrentModule m0 $ do
m1 <- toAbstract $ OldModuleName recN
s <- getNamedScope m1
(adir, s) <- applyImportDirectiveM recN dir' s
(s', copyInfo) <- copyScope recN m0 s
modifyCurrentScope $ const s'
printScope "mod.inst" 20 "copied record module"
return (A.RecordModuleInstance m1, copyInfo, adir)
checkModuleMacro
:: (Pretty c, ToConcrete a c)
=> (ModuleInfo
-> ModuleName
-> A.ModuleApplication
-> ScopeCopyInfo
-> A.ImportDirective
-> a)
-> OpenKind
-> Range
-> Access
-> C.Name
-> C.ModuleApplication
-> OpenShortHand
-> C.ImportDirective
-> ScopeM [a]
checkModuleMacro apply kind r p x modapp open dir = do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking ModuleMacro " ++ prettyShow x
]
dir <- notPublicWithoutOpen open dir
m0 <- toAbstract (NewModuleName x)
reportSDoc "scope.decl" 90 $ "NewModuleName: m0 =" <+> prettyA m0
printScope "mod.inst" 20 "module macro"
let (moduleDir, openDir) = case (open, isNoName x) of
(DoOpen, False) -> (defaultImportDir, dir)
(DoOpen, True) -> ( dir { publicOpen = Nothing }
, defaultImportDir { publicOpen = publicOpen dir }
)
(DontOpen, _) -> (dir, defaultImportDir)
(modapp', copyInfo, adir') <- withLocalVars $ checkModuleApplication modapp m0 x moduleDir
printScope "mod.inst.app" 20 "checkModuleMacro, after checkModuleApplication"
reportSDoc "scope.decl" 90 $ "after mod app: trying to print m0 ..."
reportSDoc "scope.decl" 90 $ "after mod app: m0 =" <+> prettyA m0
bindModule p x m0
reportSDoc "scope.decl" 90 $ "after bindMod: m0 =" <+> prettyA m0
printScope "mod.inst.copy.after" 20 "after copying"
adir <- case open of
DontOpen -> return adir'
DoOpen -> openModule kind (Just m0) (C.QName x) openDir
printScope "mod.inst" 20 $ show open
reportSDoc "scope.decl" 90 $ "after open : m0 =" <+> prettyA m0
stripNoNames
printScope "mod.inst" 10 $ "after stripping"
reportSDoc "scope.decl" 90 $ "after stripNo: m0 =" <+> prettyA m0
let m = m0 `withRangesOf` [x]
adecls = [ apply info m modapp' copyInfo adir ]
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked ModuleMacro " ++ prettyShow x
]
reportSLn "scope.decl" 90 $ "info = " ++ show info
reportSLn "scope.decl" 90 $ "m = " ++ prettyShow m
reportSLn "scope.decl" 90 $ "modapp' = " ++ show modapp'
reportSDoc "scope.decl" 90 $ return $ pretty copyInfo
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 -> C.ImportDirective -> ScopeM C.ImportDirective
notPublicWithoutOpen DoOpen dir = return dir
notPublicWithoutOpen DontOpen dir = do
whenJust (publicOpen dir) $ \ r ->
setCurrentRange r $ warning UselessPublic
return $ dir { publicOpen = Nothing }
renamingRange :: C.ImportDirective -> Range
renamingRange = getRange . map renToRange . impRenaming
checkOpen
:: Range
-> Maybe A.ModuleName
-> C.QName
-> C.ImportDirective
-> ScopeM (ModuleInfo, A.ModuleName, A.ImportDirective)
checkOpen r mam x dir = do
reportSDoc "scope.decl" 70 $ do
cm <- getCurrentModule
vcat $
[ text "scope checking NiceOpen " <> return (pretty x)
, text " getCurrentModule = " <> prettyA cm
, text $ " getCurrentModule (raw) = " ++ show cm
, text $ " C.ImportDirective = " ++ prettyShow dir
]
whenJust (publicOpen dir) $ \ r -> do
whenM ((A.noModuleName ==) <$> getCurrentModule) $ do
setCurrentRange r $ warning UselessPublic
m <- caseMaybe mam (toAbstract (OldModuleName x)) return
printScope "open" 20 $ "opening " ++ prettyShow x
adir <- openModule TopOpenModule (Just m) 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 adir]
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked NiceOpen " ++ prettyShow x
] ++ map (nest 2 . prettyA) adecls
return (minfo, m, adir)
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a
concreteToAbstract_ = toAbstract
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
toAbstractHiding :: (LensHiding h, ToAbstract c a) => h -> c -> ScopeM a
toAbstractHiding h | visible h = toAbstract
toAbstractHiding _ = toAbstractCtx TopCtx
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 () () where
toAbstract = pure
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)
instance {-# OVERLAPPABLE #-} ToAbstract c a => ToAbstract [c] [a] where
toAbstract = mapM toAbstract
instance (ToAbstract c1 a1, ToAbstract c2 a2) =>
ToAbstract (Either c1 c2) (Either a1 a2) where
toAbstract = traverseEither toAbstract toAbstract
instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
toAbstract = traverse toAbstract
data NewName a = NewName
{ newBinder :: A.BindingSource
, newName :: a
} deriving (Functor)
data OldQName = OldQName
C.QName
(Maybe (Set A.Name))
data MaybeOldQName = MaybeOldQName OldQName
newtype OldName a = OldName a
data ResolveQName = ResolveQName C.QName
data PatName = PatName C.QName (Maybe (Set A.Name))
instance ToAbstract (NewName C.Name) A.Name where
toAbstract (NewName b x) = do
y <- freshAbstractName_ x
bindVariable b x y
return y
instance ToAbstract (NewName C.BoundName) A.BindName where
toAbstract NewName{ newBinder = b, newName = BName{ boundName = x, bnameFixity = fx }} = do
y <- freshAbstractName fx x
bindVariable b x y
return $ A.BindName y
instance ToAbstract OldQName A.Expr where
toAbstract q@(OldQName x _) =
fromMaybeM (notInScopeError x) $ toAbstract (MaybeOldQName q)
instance ToAbstract MaybeOldQName (Maybe A.Expr) where
toAbstract (MaybeOldQName (OldQName x ns)) = do
qx <- resolveName' allKindsOfNames ns x
reportSLn "scope.name" 10 $ "resolved " ++ prettyShow x ++ ": " ++ prettyShow qx
case qx of
VarName x' _ -> return $ Just $ A.Var x'
DefinedName _ d -> do
reportSDoc "scope.warning" 50 $ text $ "Checking usage of " ++ prettyShow d
mstr <- Map.lookup (anameName d) <$> getUserWarnings
forM_ mstr (warning . UserWarning)
case anameKind d of
GeneralizeName -> do
gvs <- useTC stGeneralizedVars
case gvs of
Just s -> stGeneralizedVars `setTCLens` Just (s `Set.union` Set.singleton (anameName d))
Nothing -> typeError $ GeneralizeNotSupportedHere $ anameName d
DisallowedGeneralizeName -> do
typeError . GenericDocError =<<
text "Cannot use generalized variable from let-opened module:" <+> prettyTCM (anameName d)
_ -> return ()
return $ Just $ nameToExpr d
FieldName ds -> return $ Just $ A.Proj ProjPrefix $ AmbQ (fmap anameName ds)
ConstructorName ds -> return $ Just $ A.Con $ AmbQ (fmap anameName ds)
UnknownName -> pure Nothing
PatternSynResName ds -> return $ Just $ A.PatternSyn $ AmbQ (fmap anameName ds)
instance ToAbstract ResolveQName ResolvedName where
toAbstract (ResolveQName x) = resolveName x >>= \case
UnknownName -> notInScopeError x
q -> return q
data APatName = VarPatName A.Name
| ConPatName (NonEmpty AbstractName)
| PatternSynPatName (NonEmpty AbstractName)
instance ToAbstract PatName APatName where
toAbstract (PatName x ns) = do
reportSLn "scope.pat" 10 $ "checking pattern name: " ++ prettyShow x
rx <- resolveName' (someKindsOfNames [ConName, PatternSynName]) ns x
case (rx, x) of
(VarName y _, C.QName x) -> bindPatVar x
(FieldName d, C.QName x) -> bindPatVar x
(DefinedName _ d, C.QName x) | isDefName (anameKind d)-> bindPatVar x
(UnknownName, C.QName x) -> bindPatVar x
(ConstructorName ds, _) -> patCon ds
(PatternSynResName d, _) -> patSyn d
_ -> genericError $ "Cannot pattern match on non-constructor " ++ prettyShow x
where
bindPatVar = VarPatName <.> bindPatternVariable
patCon ds = do
reportSLn "scope.pat" 10 $ "it was a con: " ++ prettyShow (fmap anameName ds)
return $ ConPatName ds
patSyn ds = do
reportSLn "scope.pat" 10 $ "it was a pat syn: " ++ prettyShow (fmap anameName ds)
return $ PatternSynPatName ds
bindPatternVariable :: C.Name -> ScopeM A.Name
bindPatternVariable x = do
reportSLn "scope.pat" 10 $ "it was a var: " ++ prettyShow x
y <- (AssocList.lookup x <$> getVarsToBind) >>= \case
Just (LocalVar y _ _) -> return $ setRange (getRange x) y
Nothing -> freshAbstractName_ x
addVarToBind x $ LocalVar y PatternBound []
return y
class ToQName a where
toQName :: a -> C.QName
instance ToQName C.Name where toQName = C.QName
instance ToQName C.QName where toQName = id
instance (Show a, ToQName a) => ToAbstract (OldName a) A.QName where
toAbstract (OldName x) = do
rx <- resolveName (toQName x)
case rx of
DefinedName _ d -> return $ anameName d
ConstructorName ds -> return $ anameName (NonEmpty.head ds)
FieldName ds -> return $ anameName (NonEmpty.head ds)
PatternSynResName ds -> return $ anameName (NonEmpty.head ds)
VarName x _ -> genericError $ "Not a defined name: " ++ prettyShow x
UnknownName -> notInScopeError (toQName x)
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 :: [AbstractModule] <- scopeLookup (C.QName x) <$> getScope
unless (null ms) $ do
reportSLn "scope.clash" 20 $ "clashing modules ms = " ++ prettyShow ms
reportSLn "scope.clash" 60 $ "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 Nothing 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 Nothing 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
mkArg' :: ArgInfo -> C.Expr -> Arg C.Expr
mkArg' info (C.HiddenArg _ e) = Arg (hide info) $ namedThing e
mkArg' info (C.InstanceArg _ e) = Arg (makeInstance info) $ namedThing e
mkArg' info e = Arg (setHiding NotHidden info) e
inferParenPreference :: C.Expr -> ParenPreference
inferParenPreference C.Paren{} = PreferParen
inferParenPreference _ = PreferParenless
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)
toAbstractLam :: Range -> [C.LamBinding] -> C.Expr -> Precedence -> ScopeM A.Expr
toAbstractLam r bs e ctx = do
lvars0 <- getLocalVars
localToAbstract (map (C.DomainFull . makeDomainFull) bs) $ \ bs -> do
lvars1 <- getLocalVars
checkNoShadowing lvars0 lvars1
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.LamClause] -> ScopeM A.Expr
scopeCheckExtendedLam r cs = do
whenM isInsideDotPattern $
genericError "Extended lambdas are not allowed in dot patterns"
cname <- freshConcreteName r 0 extendedLambdaName
name <- freshAbstractName_ cname
a <- asksTC (^. lensIsAbstract)
reportSDoc "scope.extendedLambda" 10 $ vcat
[ text $ "new extended lambda name (" ++ show a ++ "): " ++ prettyShow name
]
verboseS "scope.extendedLambda" 60 $ do
forM_ cs $ \ c -> do
reportSLn "scope.extendedLambda" 60 $ "extended lambda lhs: " ++ show (C.lamLHS c)
qname <- qualifyName_ name
bindName (PrivateAccess Inserted) FunName cname qname
let
insertApp :: C.Pattern -> ScopeM C.Pattern
insertApp (C.RawAppP r es) = return $ C.RawAppP r $ IdentP (C.QName cname) : es
insertApp (C.AppP p1 p2) = return $ (IdentP (C.QName cname) `C.AppP` defaultNamedArg p1) `C.AppP` p2
insertApp p = return $ C.RawAppP r $ IdentP (C.QName cname) : [p]
where r = getRange p
d <- C.FunDef r [] a NotInstanceDef __IMPOSSIBLE__ __IMPOSSIBLE__ cname <$> do
forM cs $ \ (LamClause lhs rhs wh ca) -> do
lhs' <- mapLhsOriginalPatternM insertApp lhs
return $ C.Clause cname ca 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__
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 ->
case l of
LitNat r n -> do
let builtin | n < 0 = Just <$> primFromNeg
| otherwise = ensureInScope =<< getBuiltin' builtinFromNat
l' = LitNat r (abs n)
info = defaultAppInfo r
conv <- builtin
case conv of
Just (I.Def q _) -> return $ A.App info (A.Def q) $ defaultNamedArg (A.Lit l')
_ -> return $ A.Lit l
LitString r s -> do
conv <- ensureInScope =<< getBuiltin' builtinFromString
let info = defaultAppInfo r
case conv of
Just (I.Def q _) -> return $ A.App info (A.Def q) $ defaultNamedArg (A.Lit l)
_ -> return $ A.Lit l
_ -> return $ A.Lit l
where
ensureInScope :: Maybe I.Term -> ScopeM (Maybe I.Term)
ensureInScope v@(Just (I.Def q _)) = ifM (isNameInScope q <$> getScope) (return v) (return Nothing)
ensureInScope _ = return Nothing
C.QuestionMark r n -> do
scope <- getScope
ii <- registerInteractionPoint True 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
let parenPref = inferParenPreference (namedArg e2)
info = (defaultAppInfo r) { appOrigin = UserWritten, appParens = parenPref }
e1 <- toAbstractCtx FunctionCtx e1
e2 <- toAbstractCtx (ArgumentCtx parenPref) e2
return $ A.App info 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 (Arg info1 e1) e2 -> do
Arg info (e0, dotted) <- traverse (toAbstractDot FunctionSpaceDomainCtx) $ mkArg' info1 e1
let e1 = 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) -> do
lvars0 <- getLocalVars
localToAbstract tel $ \tel -> do
lvars1 <- getLocalVars
checkNoShadowing lvars0 lvars1
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) 0
C.PropN _ n -> return $ A.Prop (ExprRange $ getRange e) n
e0@(C.Let _ ds (Just 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.Let _ _ Nothing -> genericError "Missing body in let-expression"
C.Rec r fs -> do
fs' <- toAbstractCtx TopCtx fs
let ds' = [ d | Right (_, ds) <- fs', d <- ds ]
fs'' = map (mapRight fst) fs'
i = ExprRange r
return $ A.mkLet i ds' (A.Rec i fs'')
C.RecUpdate r e fs -> do
A.RecUpdate (ExprRange r) <$> toAbstract e <*> toAbstractCtx TopCtx fs
C.Paren _ e -> toAbstractCtx TopCtx e
C.IdiomBrackets r es ->
toAbstractCtx TopCtx =<< parseIdiomBracketsSeq r es
C.DoBlock r ss ->
toAbstractCtx TopCtx =<< desugarDoNotation r ss
C.Dot r e -> A.Dot (ExprRange r) <$> toAbstract e
C.As _ _ _ -> notAnExpression e
C.Absurd _ -> notAnExpression e
C.ETel _ -> __IMPOSSIBLE__
C.Equal{} -> genericError "Parse error: unexpected '='"
C.Ellipsis _ -> genericError "Parse error: unexpected '...'"
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 -> do
let AppView e' args = appView e
e' <- toAbstract e'
args <- toAbstract args
return $ A.Tactic (ExprRange r) e' args
C.DontCare e -> A.DontCare <$> toAbstract e
C.Generalized e -> do
(s, e) <- collectGeneralizables $ toAbstract e
pure $ A.generalized s e
instance ToAbstract C.ModuleAssignment (A.ModuleName, [A.LetBinding]) where
toAbstract (C.ModuleAssignment m es i)
| null es && isDefaultImportDir i = (, []) <$> toAbstract (OldModuleName m)
| otherwise = do
x <- C.NoName (getRange m) <$> fresh
r <- checkModuleMacro LetApply LetOpenModule (getRange (m, es, i)) PublicAccess x
(C.SectionApp (getRange (m , es)) [] (RawApp (fuseRange m es) (Ident m : es)))
DontOpen i
case r of
(LetApply _ m' _ _ _ : _) -> return (m', r)
_ -> __IMPOSSIBLE__
instance ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) where
toAbstract = traverse toAbstract
instance ToAbstract (C.Binder' (NewName C.BoundName)) A.Binder where
toAbstract (C.Binder p n) = do
let name = C.boundName $ newName n
n <- if not (isNoName name && isJust p) then pure n else do
n' <- freshConcreteName (getRange $ newName n) 0 patternInTeleName
pure $ fmap (\ n -> n { C.boundName = n' }) n
n <- toAbstract n
p <- traverse parsePattern p
p <- toAbstract p
checkPatternLinearity p $ \ys ->
typeError $ RepeatedVariablesInPattern ys
bindVarsToBind
p <- toAbstract p
pure $ A.Binder p n
instance ToAbstract C.LamBinding A.LamBinding where
toAbstract (C.DomainFree x) = do
tac <- traverse toAbstract $ bnameTactic $ C.binderName $ namedArg x
A.DomainFree tac <$> toAbstract (updateNamedArg (fmap $ NewName LambdaBound) x)
toAbstract (C.DomainFull tb) = A.DomainFull <$> toAbstract tb
makeDomainFull :: C.LamBinding -> C.TypedBinding
makeDomainFull (C.DomainFull b) = b
makeDomainFull (C.DomainFree x) = C.TBind r [x] $ C.Underscore r Nothing
where r = getRange x
instance ToAbstract C.TypedBinding A.TypedBinding where
toAbstract (C.TBind r xs t) = do
t' <- toAbstractCtx TopCtx t
tac <- traverse toAbstract $
case mapMaybe (bnameTactic . C.binderName . namedArg) xs of
[] -> Nothing
tac : _ -> Just tac
xs' <- toAbstract $ map (updateNamedArg (fmap $ NewName LambdaBound)) xs
return $ A.TBind r tac 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 Inserted, 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 $
void $
openModule TopOpenModule (Just aname) (C.QName name) $
defaultImportDir { publicOpen = boolToMaybe (p == PublicAccess) noRange }
return ds
telHasOpenStmsOrModuleMacros :: C.Telescope -> Bool
telHasOpenStmsOrModuleMacros = any yesBind
where
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 ()
default ensureNoLetStms :: (Foldable t, EnsureNoLetStms b, t b ~ a) => a -> ScopeM ()
ensureNoLetStms = traverse_ ensureNoLetStms
instance EnsureNoLetStms C.Binder where
ensureNoLetStms arg@(C.Binder p n) =
when (isJust p) $ typeError $ IllegalPatternInTelescope arg
instance EnsureNoLetStms C.TypedBinding where
ensureNoLetStms = \case
tb@C.TLet{} -> typeError $ IllegalLetInTelescope tb
C.TBind _ xs _ -> traverse_ (ensureNoLetStms . namedArg) xs
instance EnsureNoLetStms a => EnsureNoLetStms (LamBinding' a) where
instance EnsureNoLetStms a => EnsureNoLetStms [a] where
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 " ++ prettyShow x
res <- withLocalVars $ do
tel <- toAbstract (GenTel tel)
withCurrentModule qm $ do
printScope "module" 20 $ "inside module " ++ prettyShow x
ds <- checkDs
scope <- getScope
return (scope, [ A.Section info (qm `withRangesOfQ` x) tel ds ])
printScope "module" 20 $ "after module " ++ prettyShow x
return res
where
info = ModuleInfo r noRange Nothing Nothing Nothing
data TopLevel a = TopLevel
{ topLevelPath :: AbsolutePath
, topLevelExpectedName :: C.TopLevelModuleName
, topLevelTheThing :: a
}
data TopLevelInfo = TopLevelInfo
{ topLevelDecls :: [A.Declaration]
, topLevelScope :: ScopeInfo
}
topLevelModuleName :: TopLevelInfo -> A.ModuleName
topLevelModuleName = (^. scopeCurrent) . topLevelScope
instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
toAbstract (TopLevel file expectedMName ds) =
case C.spanAllowedBeforeModule ds of
(_, C.Module{} : d : _) -> traceCall (SetRange $ getRange d) $
genericError $ "No declarations allowed after top-level module."
(outsideDecls, [ C.Module r m0 tel insideDecls ]) -> do
m <- if isNoName m0
then do
case flip span insideDecls $ \case { C.Module{} -> False; _ -> True } of
(ds0, (C.Module _ m1 _ _ : _))
| C.toTopLevelModuleName m1 == expectedMName
, r == beginningOfFile (getRange insideDecls) -> do
traceCall (SetRange $ getRange ds0) $ genericError
"Illegal declaration(s) before top-level module"
_ -> return $ C.QName $ C.Name (getRange m0) C.InScope
[Id $ stringToRawName $ rootNameModule file]
else do
checkModuleName (C.toTopLevelModuleName m0) (SourceFile file) $ Just expectedMName
return m0
setTopLevelModule m
am <- toAbstract (NewModuleQName m)
outsideDecls <- toAbstract outsideDecls
(insideScope, insideDecls) <- scopeCheckModule r m am tel $
toAbstract insideDecls
let scope = over scopeModules (fmap $ restrictLocalPrivate am) insideScope
setScope scope
return $ TopLevelInfo (outsideDecls ++ insideDecls) scope
_ -> __IMPOSSIBLE__
niceDecls :: DoWarn -> [C.Declaration] -> ([NiceDeclaration] -> ScopeM a) -> ScopeM a
niceDecls warn ds ret = setCurrentRange ds $ computeFixitiesAndPolarities warn ds $ do
fixs <- useScope scopeFixities
let (result, warns') = runNice $ niceDeclarations fixs ds
isSafe <- Lens.getSafeMode <$> pragmaOptions
isBuiltin <- Lens.isBuiltinModule . filePath =<< getCurrentPath
let warns = if isSafe && not isBuiltin then warns' else filter notOnlyInSafeMode warns'
unless (warn == NoWarn || null warns) $ do
when isSafe $ do
let isUnsafe w = declarationWarningName w `elem`
[ PragmaNoTerminationCheck_
, PragmaCompiled_
, MissingDefinitions_
]
let (errs, ws) = List.partition isUnsafe warns
unless (null errs) $ do
warnings $ NicifierIssue <$> ws
tcerrs <- mapM warning_ $ NicifierIssue <$> errs
setCurrentRange errs $ typeError $ NonFatalErrors tcerrs
warnings $ NicifierIssue <$> warns
case result of
Left e -> throwError $ Exception (getRange e) $ pretty e
Right ds -> ret ds
where notOnlyInSafeMode = (PragmaCompiled_ /=) . declarationWarningName
instance {-# OVERLAPPING #-} ToAbstract [C.Declaration] [A.Declaration] where
toAbstract ds = do
ds <- ifM (Lens.getSafeMode <$> pragmaOptions)
(mapM noUnsafePragma ds)
(return ds)
niceDecls DoWarn ds toAbstract
where
noUnsafePragma :: C.Declaration -> TCM C.Declaration
noUnsafePragma = \case
C.Pragma pr -> warnUnsafePragma pr
C.RecordDef r n ind eta ins lams ds -> C.RecordDef r n ind eta ins lams <$> mapM noUnsafePragma ds
C.Record r n ind eta ins lams e ds -> C.Record r n ind eta ins lams e <$> mapM noUnsafePragma ds
C.Mutual r ds -> C.Mutual r <$> mapM noUnsafePragma ds
C.Abstract r ds -> C.Abstract r <$> mapM noUnsafePragma ds
C.Private r o ds -> C.Private r o <$> mapM noUnsafePragma ds
C.InstanceB r ds -> C.InstanceB r <$> mapM noUnsafePragma ds
C.Macro r ds -> C.Macro r <$> mapM noUnsafePragma ds
d -> pure d
warnUnsafePragma :: C.Pragma -> TCM C.Declaration
warnUnsafePragma pr = C.Pragma pr <$ do
ifM (Lens.isBuiltinModuleWithSafePostulates . filePath =<< getCurrentPath)
(pure ())
$ case unsafePragma pr of
Nothing -> pure ()
Just w -> setCurrentRange pr $ warning w
unsafePragma :: C.Pragma -> Maybe Warning
unsafePragma = \case
C.NoCoverageCheckPragma{} -> Just SafeFlagNoCoverageCheck
C.NoPositivityCheckPragma{} -> Just SafeFlagNoPositivityCheck
C.PolarityPragma{} -> Just SafeFlagPolarity
C.NoUniverseCheckPragma{} -> Just SafeFlagNoUniverseCheck
C.InjectivePragma{} -> Just SafeFlagInjective
C.TerminationCheckPragma _ m -> case m of
NonTerminating -> Just SafeFlagNonTerminating
Terminating -> Just SafeFlagTerminating
TerminationCheck -> Nothing
TerminationMeasure{} -> Nothing
NoTerminationCheck -> Nothing
C.OptionsPragma{} -> Nothing
C.BuiltinPragma{} -> Nothing
C.ForeignPragma{} -> Nothing
C.StaticPragma{} -> Nothing
C.InlinePragma{} -> Nothing
C.ImpossiblePragma{} -> Nothing
C.EtaPragma{} -> Nothing
C.WarningOnUsage{} -> Nothing
C.WarningOnImport{} -> Nothing
C.DisplayPragma{} -> Nothing
C.CatchallPragma{} -> Nothing
C.RewritePragma{} -> Nothing
C.CompilePragma{} -> Nothing
newtype LetDefs = LetDefs [C.Declaration]
newtype LetDef = LetDef NiceDeclaration
instance ToAbstract LetDefs [A.LetBinding] where
toAbstract (LetDefs ds) =
concat <$> (niceDecls DoWarn ds $ toAbstract . map LetDef)
instance ToAbstract LetDef [A.LetBinding] where
toAbstract (LetDef d) =
case d of
NiceMutual _ _ _ _ d@[C.FunSig _ _ _ instanc macro info _ _ x t, C.FunDef _ _ abstract _ _ _ _ [cl]] ->
do when (abstract == AbstractDef) $ do
genericError $ "abstract not allowed in let expressions"
when (macro == MacroDef) $ do
genericError $ "Macros cannot be defined in a let expression."
t <- toAbstract t
fx <- getConcreteFixity x
x <- A.unBind <$> toAbstract (NewName LetBound $ mkBoundName x fx)
(x', e) <- letToAbstract cl
let info' | instanc == InstanceDef = makeInstance info
| otherwise = info
return [ A.LetDeclaredVariable (A.mkBindName (setRange (getRange x') x))
, A.LetBind (LetRange $ getRange d) info' (A.mkBindName x) t e
]
NiceFunClause r PublicAccess ConcreteDef tc cc catchall d@(C.FunClause lhs@(C.LHS p [] [] NoEllipsis) (C.RHS rhs) NoWhere ca) -> do
mp <- setCurrentRange p $
(Right <$> parsePattern p)
`catchError`
(return . Left)
case mp of
Right p -> do
rhs <- toAbstract rhs
p <- toAbstract p
checkPatternLinearity p $ \ys ->
typeError $ RepeatedVariablesInPattern ys
bindVarsToBind
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 tc cc YesPositivityCheck
[ C.FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef defaultArgInfo tc cc x (C.Underscore (getRange x) Nothing)
, C.FunDef r __IMPOSSIBLE__ ConcreteDef NotInstanceDef __IMPOSSIBLE__ __IMPOSSIBLE__ __IMPOSSIBLE__
[C.Clause x (ca || catchall) 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.EqualP{} = Nothing
definedName C.LitP{} = Nothing
definedName C.RecP{} = Nothing
definedName C.QuoteP{} = Nothing
definedName C.HiddenP{} = Nothing
definedName C.InstanceP{} = Nothing
definedName C.WithP{} = Nothing
definedName (C.RawAppP _ []) = __IMPOSSIBLE__
definedName C.AppP{} = __IMPOSSIBLE__
definedName C.OpAppP{} = __IMPOSSIBLE__
definedName C.EllipsisP{} = Nothing
NiceOpen r x dirs -> do
whenJust (publicOpen dirs) $ \r -> setCurrentRange r $ warning UselessPublic
m <- toAbstract (OldModuleName x)
adir <- openModule_ LetOpenModule x dirs
let minfo = ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dirs
, minfoOpenShort = Nothing
, minfoDirective = Just dirs
}
return [A.LetOpen minfo m adir]
NiceModuleMacro r p x modapp open dir -> do
whenJust (publicOpen dir) $ \ r -> setCurrentRange r $ warning UselessPublic
checkModuleMacro LetApply LetOpenModule r (PrivateAccess Inserted) x modapp open dir
_ -> notAValidLetBinding d
where
letToAbstract (C.Clause top catchall clhs@(C.LHS p [] [] NoEllipsis) (C.RHS rhs) NoWhere []) = do
(x, args) <- do
res <- setCurrentRange p $ parseLHS (C.QName top) p
case res of
C.LHSHead x args -> return (x, args)
C.LHSProj{} -> genericError $ "copatterns not allowed in let bindings"
C.LHSWith{} -> genericError $ "with-patterns not allowed in let bindings"
e <- localToAbstract args $ \args -> do
bindVarsToBind
rhs <- unbindVariable top $ toAbstract rhs
foldM lambda rhs (reverse args)
return (x, e)
letToAbstract _ = notAValidLetBinding d
lambda e (Arg info (Named Nothing (A.VarP x))) =
return $ A.Lam i (A.mkDomainFree $ unnamedArg info $ A.mkBinder x) e
where i = ExprRange (fuseRange x e)
lambda e (Arg info (Named Nothing (A.WildP i))) =
do x <- freshNoName (getRange i)
return $ A.Lam i' (A.mkDomainFree $ unnamedArg info $ A.mkBinder_ x) e
where i' = ExprRange (fuseRange i e)
lambda _ _ = notAValidLetBinding d
instance ToAbstract NiceDeclaration A.Declaration where
toAbstract d = annotateDecls $
traceS "scope.decl.trace" 50
[ "scope checking declaration"
, " " ++ prettyShow d
] $
traceS "scope.decl.trace" 80
[ "scope checking declaration (raw)"
, " " ++ show d
] $
traceCall (ScopeCheckDeclaration d) $
caseMaybe (niceHasAbstract d) id (\ a -> localTC $ \ e -> e { envAbstractMode = aDefToMode a }) $
case d of
C.Axiom r p a i rel x t -> do
whenM ((return . Lens.getSafeMode =<< commandLineOptions) `and2M`
(not <$> (Lens.isBuiltinModuleWithSafePostulates . filePath =<< getCurrentPath)))
(warning $ SafeFlagPostulate x)
toAbstractNiceAxiom A.NoFunSig NotMacroDef d
C.NiceGeneralize r p i tac x t -> do
reportSLn "scope.decl" 10 $ "found nice generalize: " ++ prettyShow x
tac <- traverse (toAbstractCtx TopCtx) tac
t_ <- toAbstractCtx TopCtx t
let (s, t) = unGeneralized t_
reportSLn "scope.decl" 50 $ "generalizations: " ++ show (Set.toList s, t)
f <- getConcreteFixity x
y <- freshAbstractQName f x
bindName p GeneralizeName x y
let info = (mkDefInfoInstance x f p ConcreteDef NotInstanceDef NotMacroDef r)
{ defTactic = tac }
return [A.Generalize s info i y t]
C.NiceField r p a i tac 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
tac <- traverse (toAbstractCtx TopCtx) tac
t' <- toAbstractCtx TopCtx $ mapExpr maskIP t
f <- getConcreteFixity x
y <- freshAbstractQName f x
bindName p FldName x y
let info = (mkDefInfoInstance x f p a i NotMacroDef r) { defTactic = tac }
return [ A.Field info y t' ]
PrimitiveFunction r p a x t -> do
t' <- toAbstractCtx TopCtx t
f <- getConcreteFixity x
y <- freshAbstractQName f x
bindName p PrimName x y
return [ A.Primitive (mkDefInfo x f p a r) y t' ]
NiceMutual r tc cc pc ds -> do
ds' <- toAbstract ds
return [ A.Mutual (MutualInfo tc cc pc r) ds' ]
C.NiceRecSig r p a _pc _uc x ls t -> do
ensureNoLetStms ls
withLocalVars $ do
(ls', _) <- withCheckNoShadowing $
toAbstract (GenTelAndType (map makeDomainFull ls) t)
t' <- toAbstract t
f <- getConcreteFixity x
x' <- freshAbstractQName f x
bindName' p RecName (GeneralizedVarsMetadata $ generalizeTelVars ls') x x'
return [ A.RecSig (mkDefInfo x f p a r) x' ls' t' ]
C.NiceDataSig r p a _pc _uc x ls t -> do
reportSLn "scope.data.sig" 20 ("checking DataSig for " ++ prettyShow x)
ensureNoLetStms ls
withLocalVars $ do
ls' <- withCheckNoShadowing $
toAbstract $ GenTel $ map makeDomainFull ls
t' <- toAbstract $ C.Generalized t
f <- getConcreteFixity x
x' <- freshAbstractQName f x
bindName' p DataName (GeneralizedVarsMetadata $ generalizeTelVars ls') x x'
return [ A.DataSig (mkDefInfo x f p a r) x' ls' t' ]
C.FunSig r p a i m rel _ _ x t ->
toAbstractNiceAxiom A.FunSig m (C.Axiom r p a i rel x t)
C.FunDef r ds a i _ _ x cs -> do
printLocals 10 $ "checking def " ++ prettyShow x
(x',cs) <- toAbstract (OldName x,cs)
unlessM ((A.qnameModule x' ==) <$> getCurrentModule) $
__IMPOSSIBLE__
let delayed = NotDelayed
f <- getConcreteFixity x
return [ A.FunDef (mkDefInfoInstance x f PublicAccess a i NotMacroDef r) x' delayed cs ]
C.NiceFunClause _ _ _ _ _ _ (C.FunClause lhs _ _ _) ->
genericError $
"Missing type signature for left hand side " ++ prettyShow lhs
C.NiceFunClause{} -> __IMPOSSIBLE__
C.NiceDataDef r o a _ uc x pars cons -> do
reportSLn "scope.data.def" 20 ("checking " ++ show o ++ " DataDef for " ++ prettyShow x)
(p, ax) <- resolveName (C.QName x) >>= \case
DefinedName p ax -> do
clashUnless x DataName ax
livesInCurrentModule ax
clashIfModuleAlreadyDefinedInCurrentModule x ax
return (p, ax)
_ -> genericError $ "Missing type signature for data definition " ++ prettyShow x
ensureNoLetStms pars
withLocalVars $ do
gvars <- bindGeneralizablesIfInserted o ax
do cs <- mapM conName cons
unlessNull (duplicates cs) $ \ dups -> do
let bad = filter (`elem` dups) cs
setCurrentRange bad $
typeError $ DuplicateConstructors dups
pars <- toAbstract pars
let x' = anameName ax
checkForModuleClash x
let m = mnameFromList $ qnameToList x'
createModule (Just IsData) m
bindModule p x m
cons <- toAbstract (map (ConstrDecl m a p) cons)
printScope "data" 20 $ "Checked data " ++ prettyShow x
f <- getConcreteFixity x
return [ A.DataDef (mkDefInfo x f PublicAccess a r) x' uc (DataDefParams gvars pars) cons ]
where
conName (C.Axiom _ _ _ _ _ c _) = return c
conName d = errorNotConstrDecl d
C.NiceRecDef r o a _ uc x ind eta cm pars fields -> do
reportSLn "scope.rec.def" 20 ("checking " ++ show o ++ " RecDef for " ++ prettyShow x)
(p, ax) <- resolveName (C.QName x) >>= \case
DefinedName p ax -> do
clashUnless x RecName ax
livesInCurrentModule ax
clashIfModuleAlreadyDefinedInCurrentModule x ax
return (p, ax)
_ -> genericError $ "Missing type signature for record definition " ++ prettyShow x
ensureNoLetStms pars
withLocalVars $ do
gvars <- bindGeneralizablesIfInserted o ax
checkForModuleClash x
pars <- toAbstract pars
let x' = anameName ax
contel <- localToAbstract (RecordConstructorType fields) return
m0 <- getCurrentModule
let m = A.qualifyM m0 $ mnameFromList [ last $ qnameToList x' ]
printScope "rec" 15 "before record"
createModule (Just IsRecord) m
afields <- withCurrentModule m $ do
afields <- toAbstract fields
printScope "rec" 15 "checked fields"
return afields
do let fs :: [C.Name]
fs = concat $ forMaybe fields $ \case
C.Field _ fs -> Just $ fs <&> \case
C.FieldSig _ _ f _ -> f
_ -> __IMPOSSIBLE__
_ -> Nothing
unlessNull (duplicates fs) $ \ dups -> do
let bad = filter (`elem` dups) fs
setCurrentRange bad $
typeError $ DuplicateFields dups
bindModule p x m
cm' <- forM cm $ \ (c, _) -> bindRecordConstructorName c a p
let inst = caseMaybe cm NotInstanceDef snd
printScope "rec" 15 "record complete"
f <- getConcreteFixity x
let params = DataDefParams gvars pars
return [ A.RecDef (mkDefInfoInstance x f PublicAccess a inst NotMacroDef r) x' uc ind eta cm' params 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 TopOpenModule 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
(minfo, m, adir) <- checkOpen r Nothing x dir
return [A.Open minfo m adir]
NicePragma r p -> do
ps <- toAbstract p
return $ map (A.Pragma r) ps
NiceImport r x as open dir -> setCurrentRange r $ do
dir <- notPublicWithoutOpen open dir
let illformedAs s = traceCall (SetRange $ getRange as) $ do
Nothing <$ warning (IllformedAsClause s)
as <- case as of
Nothing -> return Nothing
Just (AsName (Right asName) r) -> return $ Just $ AsName asName r
Just (AsName (Left (C.Ident (C.QName asName))) r) -> return $ Just $ AsName asName r
Just (AsName (Left (C.Ident C.Qual{})) r) -> illformedAs "; a qualified name is not allowed here"
Just (AsName (Left C.Underscore{}) r) -> illformedAs "; an underscore is not allowed here"
Just (AsName (Left e) r) -> illformedAs ""
(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 Inserted) x m
Just y -> bindModule (PrivateAccess Inserted) (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))
adir <- case open of
DoOpen -> do
(_minfo, _m, adir) <- checkOpen r (Just m) name dir
return adir
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 adir ]
NiceUnquoteDecl r p a i tc cc xs e -> do
fxs <- mapM getConcreteFixity xs
ys <- zipWithM freshAbstractQName fxs xs
zipWithM_ (bindName p QuotableName) xs ys
e <- toAbstract e
zipWithM_ (rebindName p OtherDefName) xs ys
let mi = MutualInfo tc cc YesPositivityCheck r
return [ A.Mutual mi [A.UnquoteDecl mi [ mkDefInfoInstance x fx p a i NotMacroDef r | (fx, x) <- zip fxs xs ] ys e] ]
NiceUnquoteDef r p a _ _ xs e -> do
fxs <- mapM getConcreteFixity xs
ys <- mapM (toAbstract . OldName) xs
zipWithM_ (rebindName p QuotableName) xs ys
e <- toAbstract e
zipWithM_ (rebindName p OtherDefName) xs ys
return [ A.UnquoteDef [ mkDefInfo x fx PublicAccess a r | (fx, x) <- zip fxs xs ] ys e ]
NicePatternSyn r a n as p -> do
reportSLn "scope.pat" 10 $ "found nice pattern syn: " ++ prettyShow n
(as, p) <- withLocalVars $ do
p <- toAbstract =<< parsePatternSyn p
checkPatternLinearity p $ \ys ->
typeError $ RepeatedVariablesInPattern ys
bindVarsToBind
let err = "Dot or equality patterns are not allowed in pattern synonyms. Maybe use '_' instead."
p <- noDotorEqPattern err p
as <- (traverse . mapM) (unVarName <=< resolveName . C.QName) as
unlessNull (patternVars p List.\\ map unArg as) $ \ xs -> do
typeError . GenericDocError =<< do
"Unbound variables in pattern synonym: " <+>
sep (map prettyA xs)
return (as, p)
y <- freshAbstractQName' n
bindName a PatternSynName n y
ep <- expandPatternSynonyms p
modifyPatternSyns (Map.insert y (as, ep))
return [A.PatternSynDef y as p]
where unVarName (VarName a _) = return a
unVarName _ = typeError $ UnusedVariableInPatternSynonym
where
toAbstractNiceAxiom funSig isMacro (C.Axiom r p a i info x t) = do
t' <- toAbstractCtx TopCtx t
f <- getConcreteFixity x
mp <- getConcretePolarity x
y <- freshAbstractQName f x
let kind | isMacro == MacroDef = MacroName
| otherwise = OtherDefName
bindName p kind x y
return [ A.Axiom funSig (mkDefInfoInstance x f p a i isMacro r) info mp y t' ]
toAbstractNiceAxiom _ _ _ = __IMPOSSIBLE__
unGeneralized :: A.Expr -> (Set.Set I.QName, A.Expr)
unGeneralized (A.Generalized s t) = (s, t)
unGeneralized (A.ScopedExpr si e) = A.ScopedExpr si <$> unGeneralized e
unGeneralized t = (mempty, t)
collectGeneralizables :: ScopeM a -> ScopeM (Set I.QName, a)
collectGeneralizables m = bracket_ open close $ do
a <- m
s <- useTC stGeneralizedVars
case s of
Nothing -> __IMPOSSIBLE__
Just s -> return (s, a)
where
open = do
gvs <- useTC stGeneralizedVars
stGeneralizedVars `setTCLens` Just mempty
pure gvs
close = (stGeneralizedVars `setTCLens`)
createBoundNamesForGeneralizables :: Set I.QName -> ScopeM (Map I.QName I.Name)
createBoundNamesForGeneralizables vs =
flip Map.traverseWithKey (Map.fromSet (const ()) vs) $ \ q _ -> do
let x = nameConcrete $ qnameName q
fx = nameFixity $ qnameName q
freshAbstractName fx x
collectAndBindGeneralizables :: ScopeM a -> ScopeM (Map I.QName I.Name, a)
collectAndBindGeneralizables m = do
fvBefore <- length <$> getLocalVars
(s, res) <- collectGeneralizables m
fvAfter <- length <$> getLocalVars
binds <- createBoundNamesForGeneralizables s
outsideLocalVars (fvAfter - fvBefore) $ bindGeneralizables binds
return (binds, res)
bindGeneralizables :: Map A.QName A.Name -> ScopeM ()
bindGeneralizables vars =
forM_ (Map.toList vars) $ \ (q, y) ->
bindVariable LambdaBound (nameConcrete $ qnameName q) y
bindGeneralizablesIfInserted :: Origin -> AbstractName -> ScopeM (Set A.Name)
bindGeneralizablesIfInserted Inserted y = bound <$ bindGeneralizables gvars
where gvars = case anameMetadata y of
GeneralizedVarsMetadata gvars -> gvars
NoMetadata -> Map.empty
bound = Set.fromList (Map.elems gvars)
bindGeneralizablesIfInserted UserWritten _ = return Set.empty
bindGeneralizablesIfInserted _ _ = __IMPOSSIBLE__
newtype GenTel = GenTel C.Telescope
data GenTelAndType = GenTelAndType C.Telescope C.Expr
instance ToAbstract GenTel A.GeneralizeTelescope where
toAbstract (GenTel tel) =
uncurry A.GeneralizeTel <$> collectAndBindGeneralizables (toAbstract tel)
instance ToAbstract GenTelAndType (A.GeneralizeTelescope, A.Expr) where
toAbstract (GenTelAndType tel t) = do
(binds, (tel, t)) <- collectAndBindGeneralizables $
(,) <$> toAbstract tel <*> toAbstract t
return (A.GeneralizeTel binds tel, t)
class LivesInCurrentModule a where
livesInCurrentModule :: a -> ScopeM ()
instance LivesInCurrentModule AbstractName where
livesInCurrentModule = livesInCurrentModule . anameName
instance LivesInCurrentModule A.QName where
livesInCurrentModule x = do
m <- getCurrentModule
reportS "scope.data.def" 30
[ " A.QName of data type: " ++ show x
, " current module: " ++ show m
]
unless (A.qnameModule x == m) $
genericError $ "Definition in different module than its type signature"
clashUnless :: C.Name -> KindOfName -> AbstractName -> ScopeM ()
clashUnless x k ax = unless (anameKind ax == k) $
typeError $ ClashingDefinition (C.QName x) (anameName ax)
clashIfModuleAlreadyDefinedInCurrentModule :: C.Name -> AbstractName -> ScopeM ()
clashIfModuleAlreadyDefinedInCurrentModule x ax = do
datRecMods <- catMaybes <$> do
mapM (isDatatypeModule . amodName) =<< lookupModuleInCurrentModule x
unlessNull datRecMods $ const $
typeError $ ClashingDefinition (C.QName x) (anameName ax)
lookupModuleInCurrentModule :: C.Name -> ScopeM [AbstractModule]
lookupModuleInCurrentModule x =
fromMaybe [] . Map.lookup x . nsModules . thingsInScope [PublicNS, PrivateNS] <$> getCurrentScope
data ConstrDecl = ConstrDecl A.ModuleName IsAbstract Access C.NiceDeclaration
bindConstructorName
:: ModuleName
-> C.Name
-> IsAbstract
-> Access
-> ScopeM A.QName
bindConstructorName m x a p = do
f <- getConcreteFixity x
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 Inserted
_ -> p
p'' = case a of
AbstractDef -> PrivateAccess Inserted
_ -> PublicAccess
bindRecordConstructorName :: C.Name -> IsAbstract -> Access -> ScopeM A.QName
bindRecordConstructorName x a p = do
y <- freshAbstractQName' x
bindName p' ConName x y
return y
where
p' = case a of
AbstractDef -> PrivateAccess Inserted
_ -> p
instance ToAbstract ConstrDecl A.Declaration where
toAbstract (ConstrDecl m a p d) = do
case d of
C.Axiom r p1 a1 i info x t -> do
unless (a1 == a) __IMPOSSIBLE__
t' <- toAbstractCtx TopCtx t
f <- getConcreteFixity x
y <- bindConstructorName m x a p
printScope "con" 15 "bound constructor"
return $ A.Axiom NoFunSig (mkDefInfoInstance x f p a i NotMacroDef r)
info Nothing y t'
_ -> errorNotConstrDecl d
errorNotConstrDecl :: C.NiceDeclaration -> ScopeM a
errorNotConstrDecl d = typeError . GenericDocError $
"Illegal declaration in data type definition " P.$$
P.nest 2 (P.vcat $ map pretty (notSoNiceDeclarations d))
instance ToAbstract C.Pragma [A.Pragma] where
toAbstract (C.ImpossiblePragma _) = impossibleTest
toAbstract (C.OptionsPragma _ opts) = return [ A.OptionsPragma opts ]
toAbstract (C.RewritePragma _ []) = [] <$ warning EmptyRewritePragma
toAbstract (C.RewritePragma _ xs) = singleton . A.RewritePragma . concat <$> do
forM xs $ \ x -> do
e <- toAbstract $ OldQName x Nothing
case e of
A.Def x -> return [ x ]
A.Proj _ p | Just x <- getUnambiguous p -> return [ x ]
A.Proj _ x -> genericError $ "REWRITE used on ambiguous name " ++ prettyShow x
A.Con c | Just x <- getUnambiguous c -> return [ x ]
A.Con x -> genericError $ "REWRITE used on ambiguous name " ++ prettyShow x
A.Var x -> genericError $ "REWRITE used on parameter " ++ prettyShow x ++ " instead of on a defined symbol"
_ -> __IMPOSSIBLE__
toAbstract (C.ForeignPragma _ b s) = [] <$ addForeignCode b s
toAbstract (C.CompilePragma _ b x s) = do
me <- toAbstract $ MaybeOldQName $ OldQName x Nothing
case me of
Nothing -> [] <$ notInScopeWarning x
Just e -> do
let err what = genericError $ "Cannot COMPILE " ++ what ++ " " ++ prettyShow x
y <- case e of
A.Def x -> return x
A.Proj _ p | Just x <- getUnambiguous p -> return x
A.Proj _ x -> err "ambiguous projection"
A.Con c | Just x <- getUnambiguous c -> return x
A.Con x -> err "ambiguous constructor"
A.PatternSyn{} -> err "pattern synonym"
A.Var{} -> err "local variable"
_ -> __IMPOSSIBLE__
return [ A.CompilePragma b y s ]
toAbstract (C.StaticPragma _ x) = do
e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj _ p | Just x <- getUnambiguous p -> return x
A.Proj _ x -> genericError $
"STATIC used on ambiguous name " ++ prettyShow x
_ -> genericError "Target of STATIC pragma should be a function"
return [ A.StaticPragma y ]
toAbstract (C.InjectivePragma _ x) = do
e <- toAbstract $ OldQName x Nothing
y <- case e of
A.Def x -> return x
A.Proj _ p | Just x <- getUnambiguous p -> return x
A.Proj _ x -> genericError $
"INJECTIVE used on ambiguous name " ++ prettyShow x
_ -> genericError "Target of INJECTIVE pragma should be a defined symbol"
return [ A.InjectivePragma y ]
toAbstract (C.InlinePragma _ b x) = do
e <- toAbstract $ OldQName x Nothing
let sINLINE = if b then "INLINE" else "NOINLINE"
y <- case e of
A.Def x -> return x
A.Proj _ p | Just x <- getUnambiguous p -> return x
A.Proj _ x -> genericError $
sINLINE ++ " used on ambiguous name " ++ prettyShow x
_ -> genericError $ "Target of " ++ sINLINE ++ " pragma should be a function"
return [ A.InlinePragma b y ]
toAbstract (C.BuiltinPragma _ b q) | isUntypedBuiltin b = do
bindUntypedBuiltin b =<< toAbstract (ResolveQName q)
return []
toAbstract (C.BuiltinPragma _ b q) = do
if b `elem` builtinsNoDef then do
case q of
C.QName x -> do
unlessM ((UnknownName ==) <$> resolveName q) $ do
genericWarning $ P.text $
"BUILTIN " ++ b ++ " declares an identifier " ++
"(no longer expects an already defined identifier)"
modifyCurrentScope $ removeNameFromScope PublicNS x
y <- freshAbstractQName' x
let kind = fromMaybe __IMPOSSIBLE__ $ builtinKindOfName b
bindName PublicAccess kind x y
return [ A.BuiltinNoDefPragma b y ]
_ -> genericError $
"Pragma BUILTIN " ++ b ++ ": expected unqualified identifier, " ++
"but found " ++ prettyShow q
else do
q <- toAbstract $ ResolveQName q
return [ A.BuiltinPragma b q ]
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.DisplayPragma _ lhs rhs) = withLocalVars $ do
let err = genericError "DISPLAY pragma left-hand side must have form 'f e1 .. en'"
getHead (C.IdentP x) = return x
getHead (C.RawAppP _ (p : _)) = getHead p
getHead _ = err
top <- getHead lhs
(isPatSyn, hd) <- do
qx <- resolveName' allKindsOfNames Nothing top
case qx of
VarName x' _ -> return . (False,) $ A.qnameFromList [x']
DefinedName _ d -> return . (False,) $ anameName d
FieldName (d :| []) -> return . (False,) $ anameName d
FieldName ds -> genericError $ "Ambiguous projection " ++ prettyShow top ++ ": " ++ prettyShow (fmap anameName ds)
ConstructorName (d :| []) -> return . (False,) $ anameName d
ConstructorName ds -> genericError $ "Ambiguous constructor " ++ prettyShow top ++ ": " ++ prettyShow (fmap anameName ds)
UnknownName -> notInScopeError top
PatternSynResName (d :| []) -> return . (True,) $ anameName d
PatternSynResName ds -> genericError $ "Ambiguous pattern synonym" ++ prettyShow top ++ ": " ++ prettyShow (fmap anameName ds)
lhs <- toAbstract $ LeftHandSide top lhs NoEllipsis
ps <- case lhs of
A.LHS _ (A.LHSHead _ ps) -> return ps
_ -> err
(hd, ps) <- do
let mkP | isPatSyn = A.PatternSynP (PatRange $ getRange lhs) (unambiguous hd)
| otherwise = A.DefP (PatRange $ getRange lhs) (unambiguous hd)
p <- expandPatternSynonyms $ mkP ps
case p of
A.DefP _ f ps | Just hd <- getUnambiguous f -> return (hd, ps)
A.ConP _ c ps | Just hd <- getUnambiguous c -> return (hd, ps)
A.PatternSynP{} -> __IMPOSSIBLE__
_ -> err
rhs <- toAbstract rhs
return [A.DisplayPragma hd ps rhs]
toAbstract (C.WarningOnUsage _ oqn str) = do
qn <- toAbstract $ OldName oqn
stLocalUserWarnings `modifyTCLens` Map.insert qn str
pure []
toAbstract (C.WarningOnImport _ str) = do
stWarningOnImport `setTCLens` Just str
pure []
toAbstract C.TerminationCheckPragma{} = __IMPOSSIBLE__
toAbstract C.NoCoverageCheckPragma{} = __IMPOSSIBLE__
toAbstract C.NoPositivityCheckPragma{} = __IMPOSSIBLE__
toAbstract C.NoUniverseCheckPragma{} = __IMPOSSIBLE__
toAbstract C.CatchallPragma{} = __IMPOSSIBLE__
toAbstract C.PolarityPragma{} = __IMPOSSIBLE__
instance ToAbstract C.Clause A.Clause where
toAbstract (C.Clause top catchall lhs@(C.LHS p eqs with ell) rhs wh wcs) = withLocalVars $ do
modifyScope_ $ updateScopeLocals $ map $ second patternToModuleBound
vars0 <- getLocalVars
lhs' <- toAbstract $ LeftHandSide (C.QName top) p ell
printLocals 10 "after lhs:"
vars1 <- getLocalVars
eqs <- mapM (toAbstractCtx TopCtx) eqs
vars2 <- getLocalVars
let vars = dropEnd (length vars1) vars2 ++ vars0
let wcs' = for wcs $ \ c -> setLocalVars vars $> c
let (whname, whds) = case wh of
NoWhere -> (Nothing, [])
AnyWhere ds -> (Nothing, [C.Private noRange Inserted ds])
SomeWhere m a ds -> (Just (m, a), ds)
let isTerminationPragma :: C.Declaration -> Bool
isTerminationPragma (C.Private _ _ ds) = any isTerminationPragma ds
isTerminationPragma (C.Pragma (TerminationCheckPragma _ _)) = True
isTerminationPragma _ = False
if not (null eqs)
then do
rhs <- toAbstract =<< toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs whname whds)
return $ A.Clause lhs' [] rhs A.noWhereDecls catchall
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 Nothing [])
rhs <- toAbstract rhs
return $ A.Clause lhs' [] rhs ds catchall
whereToAbstract
:: Range
-> Maybe (C.Name, Access)
-> [C.Declaration]
-> ScopeM a
-> ScopeM (a, A.WhereDeclarations)
whereToAbstract _ whname [] inner = (, A.noWhereDecls) <$> inner
whereToAbstract r whname whds inner = do
(m, acc) <- do
case whname of
Just (m, acc) | not (isNoName m) -> return (m, acc)
_ -> fresh <&> \ x -> (C.NoName (getRange whname) x, PrivateAccess Inserted)
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 anonymousSomeWhere = maybe False (isNoName . fst) whname
when anonymousSomeWhere $
void $
openModule TopOpenModule (Just am) (C.QName m) $
defaultImportDir { publicOpen = Just noRange }
return (x, A.WhereDecls (am <$ whname) ds)
data RightHandSide = RightHandSide
{ _rhsRewriteEqn :: [RewriteEqn' () A.Pattern A.Expr]
, _rhsWithExpr :: [WithHiding C.WithExpr]
, _rhsSubclauses :: [ScopeM C.Clause]
, _rhs :: C.RHS
, _rhsWhereName :: Maybe (C.Name, Access)
, _rhsWhereDecls :: [C.Declaration]
}
data AbstractRHS
= AbsurdRHS'
| WithRHS' [WithHiding A.Expr] [ScopeM C.Clause]
| RHS' A.Expr C.Expr
| RewriteRHS' [RewriteEqn' () A.Pattern A.Expr] AbstractRHS A.WhereDeclarations
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 (RewriteEqn' () A.Pattern A.Expr) A.RewriteEqn where
toAbstract = \case
Rewrite es -> fmap Rewrite $ forM es $ \ (_, e) -> do
qn <- withFunctionName "-rewrite"
pure (qn, e)
Invert _ pes -> do
qn <- withFunctionName "-invert"
pure $ Invert qn pes
instance ToAbstract C.RewriteEqn (RewriteEqn' () A.Pattern A.Expr) where
toAbstract = \case
Rewrite es -> Rewrite <$> mapM toAbstract es
Invert _ pes -> Invert () <$> do
let (ps, es) = unzip pes
es <- toAbstract es
ps <- forM ps $ \ p -> do
p <- parsePattern p
p <- toAbstract p
checkPatternLinearity p (typeError . RepeatedVariablesInPattern)
bindVarsToBind
toAbstract p
pure $ zip ps es
instance ToAbstract AbstractRHS A.RHS where
toAbstract AbsurdRHS' = return A.AbsurdRHS
toAbstract (RHS' e c) = return $ A.RHS e $ Just c
toAbstract (RewriteRHS' eqs rhs wh) = do
eqs <- toAbstract eqs
rhs <- toAbstract rhs
return $ RewriteRHS 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 whname wh) = do
(rhs, ds) <- whereToAbstract (getRange wh) whname wh $
toAbstract (RightHandSide [] es cs rhs Nothing [])
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 <*> pure e
data LeftHandSide = LeftHandSide C.QName C.Pattern ExpandedEllipsis
instance ToAbstract LeftHandSide A.LHS where
toAbstract (LeftHandSide top lhs ell) =
traceCall (ScopeCheckLHS top lhs) $ do
lhscore <- parseLHS top lhs
reportSLn "scope.lhs" 5 $ "parsed lhs: " ++ show lhscore
printLocals 10 "before lhs:"
unlessM (optCopatterns <$> pragmaOptions) $
when (hasCopatterns lhscore) $
typeError $ NeedOptionCopatterns
lhscore <- toAbstract lhscore
bindVarsToBind
reportSLn "scope.lhs" 5 $ "parsed lhs patterns: " ++ show lhscore
printLocals 10 "checked pattern:"
lhscore <- toAbstract lhscore
reportSLn "scope.lhs" 5 $ "parsed lhs dot patterns: " ++ show lhscore
printLocals 10 "checked dots:"
return $ A.LHS (LHSInfo (getRange lhs) ell) lhscore
mergeEqualPs :: [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
mergeEqualPs = go Nothing
where
go acc (Arg i (Named n (A.EqualP r es)) : ps) = go (fmap (fmap (++es)) acc `mplus` Just ((i,n,r),es)) ps
go Nothing [] = []
go Nothing (p : ps) = p : go Nothing ps
go (Just ((i,n,r),es)) ps = Arg i (Named n (A.EqualP r es)) :
case ps of
(p : ps) -> p : go Nothing ps
[] -> []
instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
toAbstract (C.LHSHead x ps) = do
x <- withLocalVars $ do
setLocalVars []
toAbstract (OldName x)
A.LHSHead x . mergeEqualPs <$> toAbstract ps
toAbstract (C.LHSProj d ps1 l ps2) = do
unless (null ps1) $ typeError $ GenericDocError $
"Ill-formed projection pattern" P.<+> P.pretty (foldl C.AppP (C.IdentP d) ps1)
qx <- resolveName d
ds <- case qx of
FieldName ds -> return $ fmap anameName ds
UnknownName -> notInScopeError d
_ -> genericError $
"head of copattern needs to be a field identifier, but "
++ prettyShow d ++ " isn't one"
A.LHSProj (AmbQ ds) <$> toAbstract l <*> (mergeEqualPs <$> toAbstract ps2)
toAbstract (C.LHSWith core wps ps) = do
liftA3 A.LHSWith
(toAbstract core)
(toAbstract wps)
(toAbstract ps)
instance ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) where
toAbstract (WithHiding h a) = WithHiding h <$> toAbstractHiding h a
instance ToAbstract c a => ToAbstract (Arg c) (Arg a) where
toAbstract (Arg info e) =
Arg 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 lhscore ps) = A.LHSProj d <$> mapM toAbstract lhscore <*> mapM toAbstract ps
toAbstract (A.LHSWith core wps ps) = liftA3 A.LHSWith (toAbstract core) (toAbstract wps) (toAbstract ps)
instance ToAbstract (A.Pattern' C.Expr) (A.Pattern' A.Expr) where
toAbstract = traverse $ insideDotPattern . toAbstractCtx DotPatternCtx
resolvePatternIdentifier ::
Range -> C.QName -> Maybe (Set A.Name) -> ScopeM (A.Pattern' C.Expr)
resolvePatternIdentifier r x ns = do
reportSLn "scope.pat" 60 $ "resolvePatternIdentifier " ++ show x ++ " at source position " ++ show r
px <- toAbstract (PatName x ns)
case px of
VarPatName y -> do
reportSLn "scope.pat" 60 $ " resolved to VarPatName " ++ show y ++ " with range " ++ show (getRange y)
return $ VarP $ A.mkBindName y
ConPatName ds -> return $ ConP (ConPatInfo ConOCon (PatRange r) ConPatEager)
(AmbQ $ fmap anameName ds) []
PatternSynPatName ds -> return $ PatternSynP (PatRange r)
(AmbQ $ fmap anameName ds) []
applyAPattern
:: C.Pattern
-> A.Pattern' C.Expr
-> NAPs C.Expr
-> ScopeM (A.Pattern' C.Expr)
applyAPattern p0 p ps = do
setRange (getRange p0) <$> do
case p of
A.ConP i x as -> return $ A.ConP i x (as ++ ps)
A.DefP i x as -> return $ A.DefP i x (as ++ ps)
A.PatternSynP i x as -> return $ A.PatternSynP i x (as ++ ps)
A.DotP i (Ident x) -> resolveName x >>= \case
ConstructorName ds -> do
let cpi = ConPatInfo ConOCon i ConPatLazy
c = AmbQ (fmap anameName ds)
return $ A.ConP cpi c ps
_ -> failure
A.DotP{} -> failure
A.VarP{} -> failure
A.ProjP{} -> failure
A.WildP{} -> failure
A.AsP{} -> failure
A.AbsurdP{} -> failure
A.LitP{} -> failure
A.RecP{} -> failure
A.EqualP{} -> failure
A.WithP{} -> failure
where
failure = typeError $ InvalidPattern p0
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,
visible p = do
e <- toAbstract (OldQName x Nothing)
let quoted (A.Def x) = return x
quoted (A.Macro x) = return x
quoted (A.Proj _ p)
| Just x <- getUnambiguous p = return x
| otherwise = genericError $ "quote: Ambigous name: " ++ prettyShow (unAmbQ p)
quoted (A.Con c)
| Just x <- getUnambiguous c = return x
| otherwise = genericError $ "quote: Ambigous name: " ++ prettyShow (unAmbQ c)
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
reportSLn "scope.pat" 50 $ "distributeDots before = " ++ show p
p <- distributeDots p
reportSLn "scope.pat" 50 $ "distributeDots after = " ++ show p
(p', q') <- toAbstract (p, q)
applyAPattern p0 p' [q']
where
distributeDots :: C.Pattern -> ScopeM C.Pattern
distributeDots p@(C.DotP r e) = distributeDotsExpr r e
distributeDots p = return p
distributeDotsExpr :: Range -> C.Expr -> ScopeM C.Pattern
distributeDotsExpr r e = parseRawApp e >>= \case
C.App r e a ->
AppP <$> distributeDotsExpr r e
<*> (traverse . traverse) (distributeDotsExpr r) a
OpApp r q ns as ->
case (traverse . traverse . traverse) fromNoPlaceholder as of
Just as -> OpAppP r q ns <$>
(traverse . traverse . traverse) (distributeDotsExpr r) as
Nothing -> return $ C.DotP r e
Paren r e -> ParenP r <$> distributeDotsExpr r e
_ -> return $ C.DotP r e
fromNoPlaceholder :: MaybePlaceholder (OpApp a) -> Maybe a
fromNoPlaceholder (NoPlaceholder _ (Ordinary e)) = Just e
fromNoPlaceholder _ = Nothing
parseRawApp :: C.Expr -> ScopeM C.Expr
parseRawApp (RawApp r es) = parseApplication es
parseRawApp e = return e
toAbstract p0@(OpAppP r op ns ps) = do
reportSLn "scope.pat" 60 $ "ConcreteToAbstract.toAbstract OpAppP{}: " ++ show p0
p <- resolvePatternIdentifier (getRange op) op (Just ns)
ps <- toAbstract ps
applyAPattern p0 p ps
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
toAbstract (InstanceP _ _) = __IMPOSSIBLE__
toAbstract (RawAppP _ _) = __IMPOSSIBLE__
toAbstract (EllipsisP _) = __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) = do
x <- bindPatternVariable x
p <- toAbstract p
return $ A.AsP (PatRange r) (A.mkBindName x) p
toAbstract p0@(C.EqualP r es) = return $ A.EqualP (PatRange r) es
toAbstract p0@(C.DotP r e) = do
let fallback = return $ A.DotP (PatRange r) e
case e of
C.Ident x -> resolveName x >>= \case
FieldName xs -> return $ A.ProjP (PatRange r) ProjPostfix $ AmbQ $
fmap anameName xs
_ -> fallback
_ -> fallback
toAbstract p0@(C.AbsurdP r) = return $ A.AbsurdP (PatRange r)
toAbstract (C.RecP r fs) = A.RecP (PatRange r) <$> mapM (traverse toAbstract) fs
toAbstract (C.WithP r p) = A.WithP (PatRange r) <$> toAbstract p
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
toAbstractOpApp :: C.QName -> Set A.Name ->
[NamedArg (MaybePlaceholder (OpApp C.Expr))] ->
ScopeM A.Expr
toAbstractOpApp op ns es = do
(binders, es) <- replacePlaceholders es
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))
es <- left (notaFixity nota) nonBindingParts es
let body = List.foldl' app op es
return $ foldr (A.Lam (ExprRange (getRange body))) body binders
where
app e (pref, arg) = A.App info e arg
where info = (defaultAppInfo r) { appOrigin = getOrigin arg
, appParens = pref }
r = fuseRange e arg
inferParenPref :: NamedArg (Either A.Expr (OpApp C.Expr)) -> ParenPreference
inferParenPref e =
case namedArg e of
Right (Ordinary e) -> inferParenPreference e
Left{} -> PreferParenless
Right{} -> PreferParenless
toAbsOpArg :: Precedence ->
NamedArg (Either A.Expr (OpApp C.Expr)) ->
ScopeM (ParenPreference, NamedArg A.Expr)
toAbsOpArg cxt e = (pref,) <$> (traverse . traverse) (either return (toAbstractOpArg cxt)) e
where pref = inferParenPref e
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
let pref = inferParenPref e
e <- toAbsOpArg (RightOperandCtx f pref) e
return [e]
right _ _ _ = __IMPOSSIBLE__
replacePlaceholders ::
[NamedArg (MaybePlaceholder (OpApp e))] ->
ScopeM ([A.LamBinding], [NamedArg (Either A.Expr (OpApp e))])
replacePlaceholders [] = return ([], [])
replacePlaceholders (a : as) = case namedArg a of
NoPlaceholder _ x -> mapSnd (set (Right x) a :) <$>
replacePlaceholders as
Placeholder _ -> do
x <- freshName noRange "section"
let i = setOrigin Inserted $ argInfo a
(ls, ns) <- replacePlaceholders as
return ( A.mkDomainFree (unnamedArg i $ A.mkBinder_ x) : ls
, set (Left (Var x)) a : ns
)
where
set :: a -> NamedArg b -> NamedArg a
set x arg = fmap (fmap (const x)) arg
instance ToAbstract C.HoleContent A.HoleContent where
toAbstract = \case
HoleContentExpr e -> HoleContentExpr <$> toAbstract e
HoleContentRewrite es -> HoleContentRewrite <$> toAbstract es