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)
import Control.Applicative
import Control.Monad.Reader hiding (mapM)
import Control.Monad.Error hiding (mapM)
import Data.Typeable
import Data.Traversable (mapM)
import Data.List ((\\), nub)
import qualified Data.Map as Map
import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Abstract as A
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Concrete.Definitions as C
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Concrete.Pretty
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Strict
import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
TCErr(..), TCErr'(..))
import Agda.TypeChecking.Monad.Trace (traceCall, traceCallCPS, setCurrentRange)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Options
import Agda.Interaction.Imports (scopeCheckImport)
import Agda.Utils.Monad
import Agda.Utils.Tuple
import Agda.Utils.List
import Agda.Utils.Fresh
import Agda.Utils.Pretty
#include "../../undefined.h"
import Agda.Utils.Impossible
instance ToAbstract C.Pragma [A.Pragma] where
toAbstract (C.ImpossiblePragma _) = __IMPOSSIBLE__
toAbstract (C.OptionsPragma _ opts) = return [ A.OptionsPragma opts ]
toAbstract (C.CompiledTypePragma _ x hs) = do
e <- toAbstract $ OldQName x
case e of
A.Def x -> return [ A.CompiledTypePragma x hs ]
_ -> fail $ "Bad compiled type: " ++ show x
toAbstract (C.CompiledDataPragma _ x hs hcs) = do
e <- toAbstract $ OldQName x
case e of
A.Def x -> return [ A.CompiledDataPragma x hs hcs ]
_ -> fail $ "Not a datatype: " ++ show x
toAbstract (C.CompiledPragma _ x hs) = do
e <- toAbstract $ OldQName x
y <- case e of
A.Def x -> return x
A.Con _ -> fail "Use COMPILED_DATA for constructors"
_ -> __IMPOSSIBLE__
return [ A.CompiledPragma y hs ]
toAbstract (C.BuiltinPragma _ b e) = 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
case e of
A.Def x -> return [ A.EtaPragma x ]
_ -> fail "Bad ETA pragma"
notAModuleExpr e = typeError $ NotAModuleExpr e
notAnExpression e = typeError $ NotAnExpression e
notAValidLetBinding d = typeError $ NotAValidLetBinding d
nothingAppliedToHiddenArg e = typeError $ NothingAppliedToHiddenArg e
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- scopeLocals <$> getScope
reportSLn "" 0 $ s ++ " " ++ show locals
printScope :: String -> Int -> String -> ScopeM ()
printScope tag v s = verboseS ("scope." ++ tag) v $ do
scope <- getScope
reportSLn "" 0 $ s ++ " " ++ show scope
lhsArgs :: C.Pattern -> (C.Name, [NamedArg C.Pattern])
lhsArgs p = case appView p of
Arg _ _ (Named _ (IdentP (C.QName x))) : ps -> (x, ps)
_ -> __IMPOSSIBLE__
where
mkHead = Arg NotHidden Relevant . unnamed
notHidden = Arg NotHidden Relevant . unnamed
appView p = case p of
AppP p arg -> appView p ++ [arg]
OpAppP _ x ps -> mkHead (IdentP $ C.QName x) : map notHidden ps
ParenP _ p -> appView p
RawAppP _ _ -> __IMPOSSIBLE__
_ -> [ mkHead p ]
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
annotateDefn :: ScopeM A.Definition -> ScopeM A.Definition
annotateDefn m = do
d <- m
s <- getScope
return $ ScopedDef s d
annotateExpr :: ScopeM A.Expr -> ScopeM A.Expr
annotateExpr m = do
e <- m
s <- getScope
return $ ScopedExpr s e
expandEllipsis :: C.Pattern -> [C.Pattern] -> C.Clause -> C.Clause
expandEllipsis _ _ c@(C.Clause _ C.LHS{} _ _ _) = c
expandEllipsis p ps (C.Clause x (C.Ellipsis _ ps' eqs es) rhs wh wcs) =
C.Clause x (C.LHS p (ps ++ ps') eqs es) rhs wh wcs
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
checkPatternLinearity ps = case xs \\ nub xs of
[] -> return ()
ys -> typeError $ RepeatedVariablesInPattern $ nub 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 . namedThing . unArg) args
A.WildP _ -> []
A.AsP _ x p -> nameConcrete x : vars p
A.DotP _ _ -> []
A.AbsurdP _ -> []
A.LitP _ -> []
A.DefP _ _ args -> __IMPOSSIBLE__
A.ImplicitP _ -> __IMPOSSIBLE__
recordConstructorType :: [NiceDeclaration] -> C.Expr
recordConstructorType fields = build fs
where
fs = reverse $ dropWhile notField $ reverse fields
notField NiceField{} = False
notField _ = True
build (NiceField r f _ _ x (Arg h rel e) : fs) =
C.Pi [C.TypedBindings r $ Arg h rel [C.TBind r [BName x f] e]] $ build fs
where r = getRange x
build (d : fs) = C.Let noRange (notSoNiceDeclarations [d]) $ build fs
build [] = C.SetN noRange 0
checkModuleMacro apply r p x tel m args open dir = withLocalVars $ do
notPublicWithoutOpen open dir
tel' <- toAbstract tel
(m0,m1,args') <- toAbstract ( NewModuleName x
, OldModuleName m
, args
)
printScope "mod.inst" 20 "module macro"
let dir' = case open of
DontOpen -> dir
DoOpen -> defaultImportDir
(renD, renM) <- withCurrentModule m0 $ do
s <- getNamedScope m1
(s', (renM, renD)) <- copyScope m0 =<< 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
return (renD, renM)
bindModule p x m0
printScope "mod.inst.copy.after" 20 "after copying"
case open of
DoOpen -> openModule_ (C.QName x) dir
DontOpen -> return ()
printScope "mod.inst" 20 $ show open
stripNoNames
printScope "mod.inst" 10 $ "after stripping"
return [ apply info (m0 `withRangesOf` [x]) tel' m1 args' renD renM ]
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 = 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
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)
instance ToAbstract c a => ToAbstract [c] [a] where
toAbstract = mapM toAbstract
instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
toAbstract Nothing = return Nothing
toAbstract (Just x) = Just <$> toAbstract x
newtype NewName a = NewName a
newtype OldQName = OldQName C.QName
newtype OldName = OldName C.Name
newtype PatName = PatName C.QName
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 x 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 = Def
mk ConName = Con . AmbQ . (:[])
instance ToAbstract OldQName A.Expr where
toAbstract (OldQName x) = do
qx <- resolveName x
reportSLn "scope.name" 10 $ "resolved " ++ show x ++ ": " ++ show qx
case qx of
VarName x' -> return $ A.Var x'
DefinedName d -> return $ nameExpr d
ConstructorName ds -> return $ A.Con $ AmbQ (map anameName ds)
UnknownName -> notInScope x
data APatName = VarPatName A.Name
| ConPatName [AbstractName]
instance ToAbstract PatName APatName where
toAbstract (PatName x) = do
reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
rx <- resolveName x
z <- case (rx, x) of
(VarName y, 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 ds
_ ->
typeError $ GenericError $
"Cannot pattern match on " ++ show x ++ ", because it is not a constructor"
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 cs -> do
reportSLn "scope.pat" 10 $ "it was a con: " ++ show (map anameName cs)
return $ ConPatName cs
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) $
setCurrentRange (getRange x) $
typeError $ ShadowedModule $
map ((`withRangeOf` x) . amodName) ms
instance ToAbstract NewModuleName A.ModuleName where
toAbstract (NewModuleName x) = do
checkForModuleClash x
m <- getCurrentModule
y <- freshQModule m x
createModule 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 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) = amodName <$> resolveModule q
mkNamedArg :: C.Expr -> NamedArg C.Expr
mkNamedArg (C.HiddenArg _ e) = Arg Hidden Relevant e
mkNamedArg e = Arg NotHidden Relevant $ unnamed e
mkArg' :: Relevance -> C.Expr -> Arg C.Expr
mkArg' r (C.HiddenArg _ e) = Arg Hidden r $ namedThing e
mkArg' r e = Arg NotHidden r e
mkArg :: C.Expr -> Arg C.Expr
mkArg e = mkArg' Relevant 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)
instance ToAbstract C.Expr A.Expr where
toAbstract e =
traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of
Ident x -> toAbstract (OldQName x)
C.Lit l -> return $ A.Lit l
C.QuestionMark r n -> do
scope <- getScope
return $ A.QuestionMark $ MetaInfo
{ metaRange = r
, metaScope = scope
, metaNumber = n
}
C.Underscore r n -> do
scope <- getScope
return $ A.Underscore $ MetaInfo
{ metaRange = r
, metaScope = scope
, metaNumber = 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 es -> toAbstractOpApp op 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.AbsurdLam r h -> return $ A.AbsurdLam (ExprRange r) h
e0@(C.Lam r bs e) -> do
localToAbstract bs $ \(b:bs') -> do
e <- toAbstractCtx TopCtx e
let info = ExprRange r
return $ A.Lam info b $ foldr mkLam e bs'
where
mkLam b e = A.Lam (ExprRange $ fuseRange b e) b e
C.Fun r e1 e2 -> do
Arg h rel (e0, dotted) <- fmapM (toAbstractDot FunctionSpaceDomainCtx) $ mkArg e1
let e1 = Arg h (if dotted then Irrelevant else rel) e0
e2 <- toAbstractCtx TopCtx e2
let info = ExprRange r
return $ A.Fun info 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) ->
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.Paren _ e -> toAbstractCtx TopCtx e
C.Dot _ _ -> notAnExpression e
C.As _ _ _ -> notAnExpression e
C.Absurd _ -> notAnExpression e
C.ETel _ -> __IMPOSSIBLE__
C.QuoteGoal _ x e -> do
x' <- toAbstract (NewName x)
e' <- toAbstract e
return $ A.QuoteGoal (ExprRange $ getRange e) x' e'
C.Quote r -> return $ A.Quote (ExprRange r)
instance ToAbstract C.LamBinding A.LamBinding where
toAbstract (C.DomainFree h x) = A.DomainFree h <$> toAbstract (NewName x)
toAbstract (C.DomainFull tb) = A.DomainFull <$> toAbstract tb
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 NewName xs)
return $ A.TBind r xs' t'
toAbstract (C.TNoBind e) = do
e <- toAbstractCtx TopCtx e
return (A.TNoBind e)
scopeCheckModule :: Range -> C.QName -> A.ModuleName -> C.Telescope -> [C.Declaration] ->
ScopeM (ScopeInfo, [A.Declaration])
scopeCheckModule r x qm tel ds = do
printScope "module" 20 $ "checking module " ++ show x
res <- withCurrentModule qm $ do
printScope "module" 20 $ "inside module " ++ show x
ds <- withLocalVars $ do
tel <- toAbstract tel
(:[]) . A.Section info (qm `withRangesOfQ` x) tel <$>
toAbstract ds
scope <- getScope
return (scope, ds)
printScope "module" 20 $ "after module " ++ show x
return res
where
info = ModuleInfo r noRange Nothing Nothing Nothing
newtype TopLevel a = TopLevel 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 ds) = case splitAt (length ds 1) ds of
(ds', [C.Module r m tel ds]) -> do
setTopLevelModule m
am <- toAbstract (NewModuleQName m)
ds' <- toAbstract ds'
(scope0, ds) <- scopeCheckModule r m am tel ds
scope <- getScope
return $ TopLevelInfo (ds' ++ ds) scope scope0
_ -> __IMPOSSIBLE__
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
niceDecls ds = case runNice $ niceDeclarations ds of
Left e -> throwError $ TCErr Nothing $ Exception (getRange e) (show e)
Right ds -> return ds
instance ToAbstract [C.Declaration] [A.Declaration] where
toAbstract ds = toAbstract =<< niceDecls ds
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
NiceDef _ c [C.Axiom _ _ _ _ x t] [C.FunDef _ _ _ _ _ _ [cl]] ->
do e <- letToAbstract cl
t <- toAbstract t
x <- toAbstract (NewName x)
return [ A.LetBind (LetRange $ getRange c) x t e ]
NiceOpen r x dirs | not (C.publicOpen dirs) -> do
m <- toAbstract (OldModuleName x)
n <- length . scopeLocals <$> getScope
openModule_ x dirs
return [A.LetOpen (ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dirs
, minfoOpenShort = Nothing
, minfoDirective = Just dirs
})
m
]
NiceModuleMacro r p a x tel e open dir | not (C.publicOpen dir) -> case appView e of
AppView (Ident m) args -> checkModuleMacro LetApply r p x tel m args open dir
_ -> notAModuleExpr e
_ -> notAValidLetBinding d
where
letToAbstract (C.Clause top clhs@(C.LHS p [] [] []) (C.RHS rhs) NoWhere []) = do
p <- parseLHS (Just top) p
localToAbstract (snd $ lhsArgs p) $ \args ->
do rhs <- toAbstract rhs
foldM lambda rhs (reverse args)
letToAbstract _ = notAValidLetBinding d
lambda e (Arg h r (Named Nothing (A.VarP x))) = return $ A.Lam i (A.DomainFree h x) e
where
i = ExprRange (fuseRange x e)
lambda e (Arg h r (Named Nothing (A.WildP i))) =
do x <- freshNoName (getRange i)
return $ A.Lam i' (A.DomainFree h x) e
where
i' = ExprRange (fuseRange i e)
lambda _ _ = notAValidLetBinding d
instance ToAbstract NiceDefinition Definition where
toAbstract d = annotateDefn $ case d of
C.FunDef r ds f p a x cs ->
traceCall (ScopeCheckDefinition d) $ do
(x',cs') <- toAbstract (OldName x,cs)
return $ A.FunDef (mkDefInfo x f p a r) x' cs'
C.DataDef r f p a x pars cons ->
traceCall (ScopeCheckDefinition d) $
withLocalVars $ do
do let cs = map conName cons
dups = nub $ cs \\ nub cs
bad = filter (`elem` dups) cs
unless (distinct cs) $
setCurrentRange (getRange bad) $
typeError $ DuplicateConstructors dups
pars <- toAbstract pars
x' <- toAbstract (OldName x)
checkForModuleClash x
let m = mnameFromList $ qnameToList x'
createModule m
bindModule p x m
cons <- toAbstract (map (ConstrDecl m) cons)
printScope "data" 20 $ "Checked data " ++ show x
return $ A.DataDef (mkDefInfo x f p a r) x' pars cons
where
conName (C.Axiom _ _ _ _ c _) = c
conName _ = __IMPOSSIBLE__
C.RecDef r f p a x c pars fields ->
traceCall (ScopeCheckDefinition d) $
withLocalVars $ do
checkForModuleClash x
pars <- toAbstract pars
x' <- toAbstract (OldName x)
contel <- toAbstract $ recordConstructorType fields
m0 <- getCurrentModule
let m = A.qualifyM m0 $ mnameFromList $ (:[]) $ last $ qnameToList x'
printScope "rec" 15 "before record"
createModule m
afields <- withCurrentModule m $ do
afields <- toAbstract fields
printScope "rec" 15 "checked fields"
return afields
bindModule p x m
c' <- mapM (toAbstract . ConstrDecl m) c
printScope "rec" 15 "record complete"
return $ A.RecDef (mkDefInfo x f p a r) x' c' pars contel afields
instance ToAbstract NiceDeclaration A.Declaration where
toAbstract d = annotateDecls $
traceCall (ScopeCheckDeclaration d) $
case d of
C.Axiom r f p a x t -> do
t' <- toAbstractCtx TopCtx t
y <- freshAbstractQName f x
bindName p DefName x y
return [ A.Axiom (mkDefInfo x f p a r) y t' ]
C.NiceField r f p a x t -> do
t' <- toAbstractCtx TopCtx t
y <- freshAbstractQName f x
unless (argRelevance t == Irrelevant) $
bindName p DefName 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' ]
NiceDef r cs ts ds -> do
(ts', ds') <- toAbstract (ts, ds)
return [ Definition (DeclInfo C.noName_ r) ts' ds' ]
NiceModule r p a (C.QName name) tel ds -> do
aname <- toAbstract (NewModuleName name)
x <- snd <$> scopeCheckModule r (C.QName name) aname tel ds
bindModule p name aname
return x
NiceModule _ _ _ C.Qual{} _ _ -> __IMPOSSIBLE__
NiceModuleMacro r p a x tel e open dir -> case appView e of
AppView (Ident m) args -> checkModuleMacro Apply r p x tel m args open dir
_ -> notAModuleExpr e
NiceOpen r x dir -> do
m <- toAbstract (OldModuleName x)
printScope "open" 20 $ "opening " ++ show x
openModule_ x dir
printScope "open" 20 $ "result:"
return [A.Open (ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dir
, minfoOpenShort = Nothing
, minfoDirective = Just dir
})
m]
NicePragma r p -> do
ps <- toAbstract p
return $ map (A.Pragma r) ps
NiceImport r x as open dir -> 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)
modifyScopeInfo $ \s -> s { scopeModules = Map.unionWith mergeScope
(Map.delete m $ scopeModules s) 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 -> do
toAbstract [ C.Open r name dir ]
return ()
DontOpen -> do
modifyNamedScopeM m $ applyImportDirectiveM x dir
return [ A.Import (ModuleInfo
{ minfoRange = r
, minfoAsName = theAsName
, minfoAsTo =
getRange (theAsSymbol, renamingRange dir)
, minfoOpenShort = Just open
, minfoDirective = Just dir
})
m ]
data ConstrDecl = ConstrDecl A.ModuleName C.NiceDeclaration
instance ToAbstract ConstrDecl A.Declaration where
toAbstract (ConstrDecl m (C.Axiom r f p a x t)) = do
t' <- toAbstractCtx TopCtx t
y <- withCurrentModule m $ freshAbstractQName f x
bindName p' ConName x y
withCurrentModule m $ bindName p' ConName x y
printScope "con" 15 "bound constructor"
return $ A.Axiom (mkDefInfo x f p a r) y t'
where
p' = case (a, p) of
(AbstractDef, _) -> PrivateAccess
(_, p) -> p
toAbstract _ = __IMPOSSIBLE__
instance ToAbstract C.Clause A.Clause where
toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'"
toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
let wcs' = map (expandEllipsis p wps) wcs
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)
if not (null eqs)
then do
rhs <- toAbstract =<< toAbstractCtx TopCtx (RightHandSide eqs with wcs' rhs whds)
return $ A.Clause lhs' rhs []
else do
(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 = do
x <- inner
return (x, [])
whereToAbstract r whname whds inner = do
m <- maybe (nameConcrete <$> freshNoName noRange) return whname
let acc = maybe PrivateAccess (const PublicAccess) whname
let tel = []
old <- getCurrentModule
am <- toAbstract (NewModuleName m)
(scope, ds) <- scopeCheckModule r (C.QName m) am tel whds
setScope scope
x <- inner
setCurrentModule old
bindModule acc m am
return (x, ds)
data RightHandSide = RightHandSide [C.Expr] [C.Expr] [C.Clause] C.RHS [C.Declaration]
data AbstractRHS = AbsurdRHS'
| WithRHS' [A.Expr] [C.Clause]
| RHS' A.Expr
| RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
withFunctionName :: String -> ScopeM A.QName
withFunctionName s = do
m <- getCurrentModule
NameId i _ <- fresh
A.qualify m <$> 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 auxs eqs rhs wh
toAbstract (WithRHS' es cs) = do
aux <- withFunctionName "with-"
A.WithRHS aux es <$> toAbstract 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
p <- parseLHS (Just top) lhs
printLocals 10 "before lhs:"
let (x, ps) = lhsArgs p
x <- toAbstract (OldName x)
args <- toAbstract ps
wps <- toAbstract =<< mapM (parseLHS Nothing) wps
checkPatternLinearity (map (namedThing . unArg) args ++ wps)
printLocals 10 "checked pattern:"
args <- toAbstract args
wps <- toAbstract wps
printLocals 10 "checked dots:"
return $ A.LHS (LHSRange $ getRange (lhs, wps)) x args wps
instance ToAbstract c a => ToAbstract (Arg c) (Arg a) where
toAbstract (Arg h r e) = Arg h r <$> toAbstractCtx (hiddenArgumentCtx h) e
instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
toAbstract (Named n e) = Named n <$> toAbstract e
instance ToAbstract c a => ToAbstract (A.Pattern' c) (A.Pattern' a) where
toAbstract = mapM toAbstract
instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
toAbstract p@(C.IdentP x) = do
px <- toAbstract (PatName x)
case px of
VarPatName y -> return $ VarP y
ConPatName ds -> return $ ConP (PatRange (getRange p))
(AmbQ $ map anameName ds)
[]
toAbstract p0@(AppP p q) = do
(p', q') <- toAbstract (p,q)
case p' of
ConP _ x as -> return $ ConP info x (as ++ [q'])
DefP _ x as -> return $ DefP info x (as ++ [q'])
_ -> typeError $ InvalidPattern p0
where
r = getRange p0
info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
toAbstract p0@(OpAppP r op ps) = do
p <- toAbstract (IdentP $ C.QName op)
ps <- toAbstract ps
case p of
ConP _ x as -> return $ ConP info x (as ++ map (Arg NotHidden Relevant . unnamed) ps)
DefP _ x as -> return $ DefP info x (as ++ map (Arg NotHidden Relevant. unnamed) ps)
_ -> __IMPOSSIBLE__
where
r = getRange p0
info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
toAbstract (RawAppP _ _) = __IMPOSSIBLE__
toAbstract p@(C.WildP r) = return $ A.WildP (PatSource r $ const p)
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 = PatSource r $ \_ -> p0
toAbstract p0@(C.AbsurdP r) = return $ A.AbsurdP info
where
info = PatSource r $ \_ -> p0
toAbstractOpApp :: C.Name -> [C.Expr] -> ScopeM A.Expr
toAbstractOpApp op@(C.NoName _ _) es = __IMPOSSIBLE__
toAbstractOpApp op@(C.Name _ _) es = do
f <- getFixity (C.QName op)
let (_,_,parts) = oldToNewNotation $ (op, f)
op <- toAbstract (OldQName $ C.QName op)
foldl app op <$> left (theFixity f) [p | p <- parts, not (isBindingHole p)] es
where
app e arg = A.App (ExprRange (fuseRange e arg)) e
$ Arg NotHidden Relevant $ unnamed arg
left f (IdPart _ : xs) es = inside f xs es
left f (_ : xs) (e : es) = do
e <- toAbstractCtx (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 <- toAbstractCtx InsideOperandCtx e
es <- inside f xs es
return (e : es)
inside _ (_ : _) [] = __IMPOSSIBLE__
inside _ [] _ = __IMPOSSIBLE__
right _ (IdPart _) [] = return []
right f _ [e] = do
e <- toAbstractCtx (RightOperandCtx f) e
return [e]
right _ _ _ = __IMPOSSIBLE__