{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Translation.AbstractToConcrete
( ToConcrete(..)
, toConcreteCtx
, abstractToConcrete_
, abstractToConcreteScope
, abstractToConcreteHiding
, runAbsToCon
, RangeAndPragma(..)
, abstractToConcreteCtx
, withScope
, preserveInteractionIds
, AbsToCon, Env
, noTakenNames
) where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.State
import Data.Either
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Traversable (traverse)
import Data.Void
import Data.List (sortBy)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Info as A
import Agda.Syntax.Internal (MetaId(..))
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Fixity
import Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Abstract.Pattern as A
import Agda.Syntax.Abstract.PatternSynonyms
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad ( resolveName' )
import Agda.TypeChecking.Monad.State (getScope, getAllPatternSyns)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Builtin
import Agda.Interaction.Options
import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.NonemptyList
import Agda.Utils.Singleton
import Agda.Utils.Tuple
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
data Env = Env { takenVarNames :: Set A.Name
, takenDefNames :: Set C.Name
, currentScope :: ScopeInfo
, builtins :: Map String A.QName
, preserveIIds :: Bool
, foldPatternSynonyms :: Bool
}
makeEnv :: ScopeInfo -> TCM Env
makeEnv scope = do
let noScopeCheck b = elem b [builtinZero, builtinSuc]
name (I.Def q _) = Just q
name (I.Con q _ _) = Just (I.conName q)
name _ = Nothing
builtin b = getBuiltin' b >>= \ case
Just v | Just q <- name v,
noScopeCheck b || isNameInScope q scope -> return [(b, q)]
_ -> return []
vars <- map (fst . unDom) <$> asksTC envContext
forM_ (scopeLocals scope) $ \(y , x) -> do
pickConcreteName (localVar x) y
builtinList <- concat <$> mapM builtin [ builtinFromNat, builtinFromString, builtinFromNeg, builtinZero, builtinSuc ]
foldPatSyns <- optPrintPatternSynonyms <$> pragmaOptions
return $
Env { takenVarNames = Set.fromList vars
, takenDefNames = defs
, currentScope = scope
, builtins = Map.fromList builtinList
, preserveIIds = False
, foldPatternSynonyms = foldPatSyns
}
where
notGeneralizeName AbsName{ anameKind = k } =
not (k == GeneralizeName || k == DisallowedGeneralizeName)
defs = Map.keysSet $
Map.filter (all notGeneralizeName) $
nsNames $ everythingInScope scope
currentPrecedence :: AbsToCon PrecedenceStack
currentPrecedence = asks $ scopePrecedence . currentScope
preserveInteractionIds :: AbsToCon a -> AbsToCon a
preserveInteractionIds = local $ \ e -> e { preserveIIds = True }
withPrecedence' :: PrecedenceStack -> AbsToCon a -> AbsToCon a
withPrecedence' ps = local $ \e ->
e { currentScope = (currentScope e) { scopePrecedence = ps } }
withPrecedence :: Precedence -> AbsToCon a -> AbsToCon a
withPrecedence p ret = do
ps <- currentPrecedence
withPrecedence' (pushPrecedence p ps) ret
withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a
withScope scope = local $ \e -> e { currentScope = scope }
noTakenNames :: AbsToCon a -> AbsToCon a
noTakenNames = local $ \e -> e { takenVarNames = Set.empty }
dontFoldPatternSynonyms :: AbsToCon a -> AbsToCon a
dontFoldPatternSynonyms = local $ \ e -> e { foldPatternSynonyms = False }
addBinding :: C.Name -> A.Name -> Env -> Env
addBinding y x e =
e { takenVarNames = Set.insert x $ takenVarNames e
, currentScope = (`updateScopeLocals` currentScope e) $
AssocList.insert y (LocalVar x __IMPOSSIBLE__ [])
}
isBuiltinFun :: AbsToCon (A.QName -> String -> Bool)
isBuiltinFun = asks $ is . builtins
where is m q b = Just q == Map.lookup b m
type AbsToCon = ReaderT Env TCM
runAbsToCon :: AbsToCon c -> TCM c
runAbsToCon m = do
scope <- getScope
reportSLn "toConcrete" 50 $ render $ "entering AbsToCon with scope:" <+> prettyList_ (map (text . C.nameToRawName . fst) $ scopeLocals scope)
runReaderT m =<< makeEnv scope
abstractToConcreteScope :: ToConcrete a c => ScopeInfo -> a -> TCM c
abstractToConcreteScope scope a = runReaderT (toConcrete a) =<< makeEnv scope
abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c
abstractToConcreteCtx ctx x = runAbsToCon $ withPrecedence ctx (toConcrete x)
abstractToConcrete_ :: ToConcrete a c => a -> TCM c
abstractToConcrete_ = runAbsToCon . toConcrete
abstractToConcreteHiding :: (LensHiding i, ToConcrete a c) => i -> a -> TCM c
abstractToConcreteHiding i = runAbsToCon . toConcreteHiding i
unsafeQNameToName :: C.QName -> C.Name
unsafeQNameToName = C.unqualify
lookupQName :: AllowAmbiguousNames -> A.QName -> AbsToCon C.QName
lookupQName ambCon x | Just s <- getGeneralizedFieldName x =
return (C.QName $ C.Name noRange C.InScope $ C.stringNameParts s)
lookupQName ambCon x = do
ys <- inverseScopeLookupName' ambCon x <$> asks currentScope
lift $ reportSLn "scope.inverse" 100 $
"inverse looking up abstract name " ++ prettyShow x ++ " yields " ++ prettyShow ys
loop ys
where
loop (qy@Qual{} : _ ) = return qy
loop (qy@(C.QName y) : ys) = lookupNameInScope y >>= \case
Just x' | x' /= qnameName x -> loop ys
_ -> return qy
loop [] = case qnameToConcrete x of
qy@Qual{} -> return $ setNotInScope qy
qy@C.QName{} -> C.QName <$> chooseName (qnameName x)
lookupModule :: A.ModuleName -> AbsToCon C.QName
lookupModule (A.MName []) = return $ C.QName $ C.Name noRange InScope [Id "-1"]
lookupModule x =
do scope <- asks currentScope
case inverseScopeLookupModule x scope of
(y : _) -> return y
[] -> return $ mnameToConcrete x
lookupNameInScope :: C.Name -> AbsToCon (Maybe A.Name)
lookupNameInScope y =
fmap localVar . lookup y . scopeLocals <$> asks currentScope
hasConcreteNames :: (MonadTCState m) => A.Name -> m [C.Name]
hasConcreteNames x = Map.findWithDefault [] x <$> useTC stConcreteNames
pickConcreteName :: (MonadTCState m) => A.Name -> C.Name -> m ()
pickConcreteName x y = modifyTCLens stConcreteNames $ flip Map.alter x $ \case
Nothing -> Just $ [y]
(Just ys) -> Just $ ys ++ [y]
shadowingNames :: (MonadTCState m) => A.Name -> m (Set C.Name, Set C.Name)
shadowingNames x = do
shadows <- Map.findWithDefault [] x <$> useTC stShadowingNames
ys <- concat <$> forM shadows hasConcreteNames
let zs = map nameConcrete shadows
return (Set.fromList ys , Set.fromList zs)
toConcreteName :: A.Name -> AbsToCon C.Name
toConcreteName x | y <- nameConcrete x , isNoName y = return y
toConcreteName x = (Map.findWithDefault [] x <$> useTC stConcreteNames) >>= loop
where
loop (y:ys) = ifM (isGoodName x y) (return y) (loop ys)
loop [] = do
y <- chooseName x
pickConcreteName x y
return y
isGoodName :: A.Name -> C.Name -> AbsToCon Bool
isGoodName x y = do
zs <- Set.toList <$> asks takenVarNames
allM zs $ \z -> if x == z then return True else do
czs <- hasConcreteNames z
return $ all (/= y) czs
chooseName :: A.Name -> AbsToCon C.Name
chooseName x = lookupNameInScope (nameConcrete x) >>= \case
Just x' | x == x' -> do
reportSLn "toConcrete.bindName" 80 $
"name " ++ C.nameToRawName (nameConcrete x) ++ " already in scope, so not renaming"
return $ nameConcrete x
_ -> do
taken <- takenConcreteNames
toAvoid <- do
(mustAvoid , tryToAvoid) <- shadowingNames x
let tryToAvoid' = Set.filter ((== InScope) . isInScope) tryToAvoid
return $ case isInScope x of
InScope -> mustAvoid
C.NotInScope -> mustAvoid `Set.union` tryToAvoid'
let shouldAvoid = (`Set.member` (taken `Set.union` toAvoid))
y = firstNonTakenName shouldAvoid $ nameConcrete x
reportSLn "toConcrete.bindName" 80 $ render $ vcat
[ "picking concrete name for:" <+> text (C.nameToRawName $ nameConcrete x)
, "names already taken: " <+> prettyList_ (map C.nameToRawName $ Set.toList taken)
, "names to avoid: " <+> prettyList_ (map C.nameToRawName $ Set.toList toAvoid)
, "concrete name chosen: " <+> text (C.nameToRawName y)
]
return y
where
takenConcreteNames :: AbsToCon (Set C.Name)
takenConcreteNames = do
xs <- asks takenDefNames
ys0 <- asks takenVarNames
reportSLn "toConcrete.bindName" 90 $ render $ "abstract names of local vars: " <+> prettyList_ (map (C.nameToRawName . nameConcrete) $ Set.toList ys0)
ys <- Set.fromList . concat <$> mapM hasConcreteNames (Set.toList ys0)
return $ xs `Set.union` ys
bindName :: A.Name -> (C.Name -> AbsToCon a) -> AbsToCon a
bindName x ret = do
y <- toConcreteName x
reportSLn "toConcrete.bindName" 30 $ "adding " ++ (C.nameToRawName $ nameConcrete x) ++ " to the scope under concrete name " ++ C.nameToRawName y
local (addBinding y x) $ ret y
bindName' :: A.Name -> AbsToCon a -> AbsToCon a
bindName' x ret = do
reportSLn "toConcrete.bindName" 30 $ "adding " ++ (C.nameToRawName $ nameConcrete x) ++ " to the scope with forced name"
pickConcreteName x y
applyUnless (isNoName y) (local $ addBinding y x) ret
where y = nameConcrete x
bracket' :: (e -> e)
-> (PrecedenceStack -> Bool)
-> e -> AbsToCon e
bracket' paren needParen e =
do p <- currentPrecedence
return $ if needParen p then paren e else e
bracket :: (PrecedenceStack -> Bool) -> AbsToCon C.Expr -> AbsToCon C.Expr
bracket par m =
do e <- m
bracket' (Paren (getRange e)) par e
bracketP_ :: (PrecedenceStack -> Bool) -> AbsToCon C.Pattern -> AbsToCon C.Pattern
bracketP_ par m =
do e <- m
bracket' (ParenP (getRange e)) par e
isLambda :: NamedArg A.Expr -> Bool
isLambda e | notVisible e = False
isLambda e =
case unScope $ namedArg e of
A.Lam{} -> True
A.AbsurdLam{} -> True
A.ExtendedLam{} -> True
_ -> False
withInfixDecl :: DefInfo -> C.Name -> AbsToCon [C.Declaration] -> AbsToCon [C.Declaration]
withInfixDecl i x m = do
ds <- m
return $ fixDecl ++ synDecl ++ ds
where fixDecl = [C.Infix (theFixity $ defFixity i) [x] | theFixity (defFixity i) /= noFixity]
synDecl = [C.Syntax x (theNotation (defFixity i))]
withAbstractPrivate :: DefInfo -> AbsToCon [C.Declaration] -> AbsToCon [C.Declaration]
withAbstractPrivate i m =
priv (defAccess i)
. abst (A.defAbstract i)
. addInstanceB (A.defInstance i == InstanceDef)
<$> m
where
priv (PrivateAccess UserWritten)
ds = [ C.Private (getRange ds) UserWritten ds ]
priv _ ds = ds
abst AbstractDef ds = [ C.Abstract (getRange ds) ds ]
abst ConcreteDef ds = ds
addInstanceB :: Bool -> [C.Declaration] -> [C.Declaration]
addInstanceB True ds = [ C.InstanceB (getRange ds) ds ]
addInstanceB False ds = ds
class ToConcrete a c | a -> c where
toConcrete :: a -> AbsToCon c
bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b
toConcrete x = bindToConcrete x return
bindToConcrete x ret = ret =<< toConcrete x
toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c
toConcreteCtx p x = withPrecedence p $ toConcrete x
bindToConcreteCtx :: ToConcrete a c => Precedence -> a -> (c -> AbsToCon b) -> AbsToCon b
bindToConcreteCtx p x ret = withPrecedence p $ bindToConcrete x ret
toConcreteTop :: ToConcrete a c => a -> AbsToCon c
toConcreteTop = toConcreteCtx TopCtx
bindToConcreteTop :: ToConcrete a c => a -> (c -> AbsToCon b) -> AbsToCon b
bindToConcreteTop = bindToConcreteCtx TopCtx
toConcreteHiding :: (LensHiding h, ToConcrete a c) => h -> a -> AbsToCon c
toConcreteHiding h =
case getHiding h of
NotHidden -> toConcrete
Hidden -> toConcreteTop
Instance{} -> toConcreteTop
bindToConcreteHiding :: (LensHiding h, ToConcrete a c) => h -> a -> (c -> AbsToCon b) -> AbsToCon b
bindToConcreteHiding h =
case getHiding h of
NotHidden -> bindToConcrete
Hidden -> bindToConcreteTop
Instance{} -> bindToConcreteTop
instance ToConcrete a c => ToConcrete [a] [c] where
toConcrete = mapM toConcrete
bindToConcrete [] ret = ret []
bindToConcrete (a:as) ret = do
p <- currentPrecedence
bindToConcrete a $ \ c ->
withPrecedence' p $
bindToConcrete as $ \ cs ->
ret (c : cs)
instance (ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (Either a1 a2) (Either c1 c2) where
toConcrete = traverseEither toConcrete toConcrete
bindToConcrete (Left x) ret =
bindToConcrete x $ \x ->
ret (Left x)
bindToConcrete (Right y) ret =
bindToConcrete y $ \y ->
ret (Right y)
instance (ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (a1,a2) (c1,c2) where
toConcrete (x,y) = liftM2 (,) (toConcrete x) (toConcrete y)
bindToConcrete (x,y) ret =
bindToConcrete x $ \x ->
bindToConcrete y $ \y ->
ret (x,y)
instance (ToConcrete a1 c1, ToConcrete a2 c2, ToConcrete a3 c3) =>
ToConcrete (a1,a2,a3) (c1,c2,c3) where
toConcrete (x,y,z) = reorder <$> toConcrete (x,(y,z))
where
reorder (x,(y,z)) = (x,y,z)
bindToConcrete (x,y,z) ret = bindToConcrete (x,(y,z)) $ ret . reorder
where
reorder (x,(y,z)) = (x,y,z)
instance ToConcrete a c => ToConcrete (Arg a) (Arg c) where
toConcrete (Arg i a) = Arg i <$> toConcreteHiding i a
bindToConcrete (Arg info x) ret =
bindToConcreteHiding info x $ ret . Arg info
instance ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) where
toConcrete (WithHiding h a) = WithHiding h <$> toConcreteHiding h a
bindToConcrete (WithHiding h a) ret = bindToConcreteHiding h a $ \ a ->
ret $ WithHiding h a
instance ToConcrete a c => ToConcrete (Named name a) (Named name c) where
toConcrete (Named n x) = Named n <$> toConcrete x
bindToConcrete (Named n x) ret = bindToConcrete x $ ret . Named n
instance ToConcrete A.Name C.Name where
toConcrete = toConcreteName
bindToConcrete x = bindName x
instance ToConcrete BindName C.BoundName where
toConcrete = fmap C.mkBoundName_ . toConcreteName . unBind
bindToConcrete x = bindName (unBind x) . (. C.mkBoundName_)
instance ToConcrete A.QName C.QName where
toConcrete = lookupQName AmbiguousConProjs
instance ToConcrete A.ModuleName C.QName where
toConcrete = lookupModule
instance ToConcrete AbstractName C.QName where
toConcrete = toConcrete . anameName
instance ToConcrete ResolvedName C.QName where
toConcrete = \case
VarName x _ -> C.QName <$> toConcrete x
DefinedName _ x -> toConcrete x
FieldName xs -> toConcrete (headNe xs)
ConstructorName xs -> toConcrete (headNe xs)
PatternSynResName xs -> toConcrete (headNe xs)
UnknownName -> __IMPOSSIBLE__
instance ToConcrete A.Expr C.Expr where
toConcrete (Var x) = Ident . C.QName <$> toConcrete x
toConcrete (Def x) = Ident <$> toConcrete x
toConcrete (Proj ProjPrefix p) = Ident <$> toConcrete (headAmbQ p)
toConcrete (Proj _ p) = C.Dot noRange . Ident <$> toConcrete (headAmbQ p)
toConcrete (A.Macro x) = Ident <$> toConcrete x
toConcrete e@(Con c) = tryToRecoverPatternSyn e $ Ident <$> toConcrete (headAmbQ c)
toConcrete e@(A.Lit (LitQName r x)) = tryToRecoverPatternSyn e $ do
x <- lookupQName AmbiguousNothing x
bracket appBrackets $ return $
C.App r (C.Quote r) (defaultNamedArg $ C.Ident x)
toConcrete e@(A.Lit l) = tryToRecoverPatternSyn e $ return $ C.Lit l
toConcrete (A.QuestionMark i ii) = do
preserve <- asks preserveIIds
return $ C.QuestionMark (getRange i) $
interactionId ii <$ guard (preserve || isJust (metaNumber i))
toConcrete (A.Underscore i) = return $
C.Underscore (getRange i) $
prettyShow . NamedMeta (metaNameSuggestion i) . MetaId . metaId <$> metaNumber i
toConcrete (A.Dot i e) =
C.Dot (getRange i) <$> toConcrete e
toConcrete e@(A.App i e1 e2) = do
is <- isBuiltinFun
case (getHead e1, namedArg e2) of
(Just (HdDef q), l@A.Lit{})
| any (is q) [builtinFromNat, builtinFromString], visible e2,
getOrigin i == Inserted -> toConcrete l
(Just (HdDef q), A.Lit (LitNat r n))
| q `is` builtinFromNeg, visible e2,
getOrigin i == Inserted -> toConcrete (A.Lit (LitNat r (-n)))
_ ->
tryToRecoverPatternSyn e
$ tryToRecoverOpApp e
$ tryToRecoverNatural e
$ bracket (appBrackets' $ preferParenless (appParens i) && isLambda e2)
$ do e1' <- toConcreteCtx FunctionCtx e1
e2' <- toConcreteCtx (ArgumentCtx $ appParens i) e2
return $ C.App (getRange i) e1' e2'
toConcrete (A.WithApp i e es) =
bracket withAppBrackets $ do
e <- toConcreteCtx WithFunCtx e
es <- mapM (toConcreteCtx WithArgCtx) es
return $ C.WithApp (getRange i) e es
toConcrete (A.AbsurdLam i h) =
bracket lamBrackets $ return $ C.AbsurdLam (getRange i) h
toConcrete e@(A.Lam i _ _) =
tryToRecoverOpApp e
$ bracket lamBrackets
$ case lamView e of
(bs, e) ->
bindToConcrete (map makeDomainFree bs) $ \ bs -> do
e <- toConcreteTop e
return $ C.Lam (getRange i) bs e
where
lamView (A.Lam _ b@(A.DomainFree _) e) =
case lamView e of
([], e) -> ([b], e)
(bs@(A.DomainFree _ : _), e) -> (b:bs, e)
_ -> ([b], e)
lamView (A.Lam _ b@(A.DomainFull _) e) =
case lamView e of
([], e) -> ([b], e)
(bs@(A.DomainFull _ : _), e) -> (b:bs, e)
_ -> ([b], e)
lamView e = ([], e)
toConcrete (A.ExtendedLam i di qname cs) =
bracket lamBrackets $ do
decls <- concat <$> toConcrete cs
let namedPat np = case getHiding np of
NotHidden -> namedArg np
Hidden -> C.HiddenP noRange (unArg np)
Instance{} -> C.InstanceP noRange (unArg np)
let removeApp (C.RawAppP r (_:es)) = return $ C.RawAppP r es
removeApp (C.AppP (C.IdentP _) np) = return $ namedPat np
removeApp (C.AppP p np) = do
p <- removeApp p
return $ C.AppP p np
removeApp x@C.IdentP{} = return $ C.RawAppP (getRange x) []
removeApp p = do
lift $ reportSLn "extendedlambda" 50 $ "abstractToConcrete removeApp p = " ++ show p
return p
let decl2clause (C.FunClause lhs rhs wh ca) = do
let p = lhsOriginalPattern lhs
lift $ reportSLn "extendedlambda" 50 $ "abstractToConcrete extended lambda pattern p = " ++ show p
p' <- removeApp p
lift $ reportSLn "extendedlambda" 50 $ "abstractToConcrete extended lambda pattern p' = " ++ show p'
return $ LamClause lhs{ lhsOriginalPattern = p' } rhs wh ca
decl2clause _ = __IMPOSSIBLE__
C.ExtendedLam (getRange i) <$> mapM decl2clause decls
toConcrete (A.Pi _ [] e) = toConcrete e
toConcrete t@(A.Pi i _ _) = case piTel t of
(tel, e) ->
bracket piBrackets
$ bindToConcrete tel $ \ tel' -> do
e' <- toConcreteTop e
return $ C.Pi tel' e'
where
piTel (A.Pi _ tel e) = (tel ++) -*- id $ piTel e
piTel e = ([], e)
toConcrete (A.Generalized _ e) = C.Generalized <$> toConcrete e
toConcrete (A.Fun i a b) =
bracket piBrackets
$ do a' <- toConcreteCtx (if irr then DotPatternCtx else FunctionSpaceDomainCtx) a
b' <- toConcreteTop b
return $ C.Fun (getRange i) (defaultArg $ addRel a' $ mkArg a') b'
where
irr = getRelevance a `elem` [Irrelevant, NonStrict]
addRel a e = case getRelevance a of
Irrelevant -> addDot a e
NonStrict -> addDot a (addDot a e)
_ -> e
addDot a e = C.Dot (getRange a) e
mkArg (Arg info e) = case getHiding info of
Hidden -> HiddenArg (getRange e) (unnamed e)
Instance{} -> InstanceArg (getRange e) (unnamed e)
NotHidden -> e
toConcrete (A.Set i 0) = return $ C.Set (getRange i)
toConcrete (A.Set i n) = return $ C.SetN (getRange i) n
toConcrete (A.Prop i 0) = return $ C.Prop (getRange i)
toConcrete (A.Prop i n) = return $ C.PropN (getRange i) n
toConcrete (A.Let i ds e) =
bracket lamBrackets
$ bindToConcrete ds $ \ds' -> do
e' <- toConcreteTop e
return $ C.Let (getRange i) (concat ds') (Just e')
toConcrete (A.Rec i fs) =
bracket appBrackets $ do
C.Rec (getRange i) . map (fmap (\x -> ModuleAssignment x [] defaultImportDir)) <$> toConcreteTop fs
toConcrete (A.RecUpdate i e fs) =
bracket appBrackets $ do
C.RecUpdate (getRange i) <$> toConcrete e <*> toConcreteTop fs
toConcrete (A.ETel tel) = C.ETel <$> toConcrete tel
toConcrete (A.ScopedExpr _ e) = toConcrete e
toConcrete (A.QuoteGoal i x e) =
bracket lamBrackets $
bindToConcrete x $ \ x' -> do
e' <- toConcrete e
return $ C.QuoteGoal (getRange i) x' e'
toConcrete (A.QuoteContext i) = return $ C.QuoteContext (getRange i)
toConcrete (A.Quote i) = return $ C.Quote (getRange i)
toConcrete (A.QuoteTerm i) = return $ C.QuoteTerm (getRange i)
toConcrete (A.Unquote i) = return $ C.Unquote (getRange i)
toConcrete (A.Tactic i e xs ys) = do
e' <- toConcrete e
xs' <- toConcrete xs
ys' <- toConcrete ys
let r = getRange i
rawtac = foldl (C.App r) e' xs'
return $ C.Tactic (getRange i) rawtac (map namedArg ys')
toConcrete (A.DontCare e) = C.Dot r . C.Paren r <$> toConcrete e
where r = getRange e
toConcrete (A.PatternSyn n) = C.Ident <$> toConcrete (headAmbQ n)
makeDomainFree :: A.LamBinding -> A.LamBinding
makeDomainFree b@(A.DomainFull (A.TBind _ [x] t)) =
case unScope t of
A.Underscore A.MetaInfo{metaNumber = Nothing} ->
A.DomainFree x
_ -> b
makeDomainFree b = b
instance ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) where
toConcrete = traverse toConcrete
bindToConcrete (FieldAssignment name a) ret =
bindToConcrete a $ ret . FieldAssignment name
forceNameIfHidden :: NamedArg A.BindName -> NamedArg A.BindName
forceNameIfHidden x
| isJust $ nameOf $ unArg x = x
| visible x = x
| otherwise = x <&> \ y -> y { nameOf = Just name }
where
name = Ranged (getRange x) $ C.nameToRawName $ nameConcrete $ unBind $ namedArg x
instance ToConcrete A.LamBinding C.LamBinding where
bindToConcrete (A.DomainFree x) ret =
bindToConcrete (forceNameIfHidden x) $ ret . C.DomainFree
bindToConcrete (A.DomainFull b) ret = bindToConcrete b $ ret . C.DomainFull
instance ToConcrete A.TypedBinding C.TypedBinding where
bindToConcrete (A.TBind r xs e) ret =
bindToConcrete (map forceNameIfHidden xs) $ \ xs -> do
e <- toConcreteTop e
ret $ C.TBind r xs e
bindToConcrete (A.TLet r lbs) ret =
bindToConcrete lbs $ \ ds -> do
ret $ C.TLet r $ concat ds
instance ToConcrete LetBinding [C.Declaration] where
bindToConcrete (LetBind i info x t e) ret =
bindToConcrete x $ \ x ->
do (t, (e, [], [], [])) <- toConcrete (t, A.RHS e Nothing)
ret $ addInstanceB (isInstance info) $
[ C.TypeSig info (C.boundName x) t
, C.FunClause (C.LHS (C.IdentP $ C.QName $ C.boundName x) [] [])
e C.NoWhere False
]
bindToConcrete (LetPatBind i p e) ret = do
p <- toConcrete p
e <- toConcrete e
ret [ C.FunClause (C.LHS p [] []) (C.RHS e) NoWhere False ]
bindToConcrete (LetApply i x modapp _ _) ret = do
x' <- unqualify <$> toConcrete x
modapp <- toConcrete modapp
let r = getRange modapp
open = fromMaybe DontOpen $ minfoOpenShort i
dir = fromMaybe defaultImportDir{ importDirRange = r } $ minfoDirective i
local (openModule' x dir id) $
ret [ C.ModuleMacro (getRange i) x' modapp open dir ]
bindToConcrete (LetOpen i x _) ret = do
x' <- toConcrete x
let dir = fromMaybe defaultImportDir $ minfoDirective i
local (openModule' x dir restrictPrivate) $
ret [ C.Open (getRange i) x' dir ]
bindToConcrete (LetDeclaredVariable _) ret =
ret []
instance ToConcrete A.WhereDeclarations WhereClause where
bindToConcrete (A.WhereDecls _ []) ret = ret C.NoWhere
bindToConcrete (A.WhereDecls (Just am) [A.Section _ _ _ ds]) ret = do
ds' <- declsToConcrete ds
cm <- unqualify <$> lookupModule am
let wh' = (if isNoName cm then AnyWhere else SomeWhere cm PublicAccess) $ ds'
local (openModule' am defaultImportDir id) $ ret wh'
bindToConcrete (A.WhereDecls _ ds) ret =
ret . AnyWhere =<< declsToConcrete ds
mergeSigAndDef :: [C.Declaration] -> [C.Declaration]
mergeSigAndDef (C.RecordSig _ x bs e : C.RecordDef r y ind eta c _ fs : ds)
| x == y = C.Record r y ind eta c bs e fs : mergeSigAndDef ds
mergeSigAndDef (C.DataSig _ _ x bs e : C.DataDef r i y _ cs : ds)
| x == y = C.Data r i y bs e cs : mergeSigAndDef ds
mergeSigAndDef (d : ds) = d : mergeSigAndDef ds
mergeSigAndDef [] = []
openModule' :: A.ModuleName -> C.ImportDirective -> (Scope -> Scope) -> Env -> Env
openModule' x dir restrict env = env{currentScope = sInfo{scopeModules = mods'}}
where sInfo = currentScope env
amod = scopeCurrent sInfo
mods = scopeModules sInfo
news = setScopeAccess PrivateNS
$ applyImportDirective dir
$ maybe emptyScope restrict
$ Map.lookup x mods
mods' = Map.update (Just . (`mergeScope` news)) amod mods
declsToConcrete :: [A.Declaration] -> AbsToCon [C.Declaration]
declsToConcrete ds = mergeSigAndDef . concat <$> toConcrete ds
instance ToConcrete A.RHS (C.RHS, [C.Expr], [C.Expr], [C.Declaration]) where
toConcrete (A.RHS e (Just c)) = return (C.RHS c, [], [], [])
toConcrete (A.RHS e Nothing) = do
e <- toConcrete e
return (C.RHS e, [], [], [])
toConcrete A.AbsurdRHS = return (C.AbsurdRHS, [], [], [])
toConcrete (A.WithRHS _ es cs) = do
es <- toConcrete es
cs <- noTakenNames $ concat <$> toConcrete cs
return (C.AbsurdRHS, [], es, cs)
toConcrete (A.RewriteRHS xeqs _spats rhs wh) = do
wh <- declsToConcrete (A.whereDecls wh)
(rhs, eqs', es, whs) <- toConcrete rhs
unless (null eqs')
__IMPOSSIBLE__
eqs <- toConcrete $ map snd xeqs
return (rhs, eqs, es, wh ++ whs)
instance ToConcrete (Maybe A.QName) (Maybe C.Name) where
toConcrete Nothing = return Nothing
toConcrete (Just x) = do
x' <- toConcrete (qnameName x)
return $ Just x'
instance ToConcrete (Constr A.Constructor) C.Declaration where
toConcrete (Constr (A.ScopedDecl scope [d])) =
withScope scope $ toConcrete (Constr d)
toConcrete (Constr (A.Axiom _ i info Nothing x t)) = do
x' <- unsafeQNameToName <$> toConcrete x
t' <- toConcreteTop t
return $ C.TypeSig info x' t'
toConcrete (Constr (A.Axiom _ _ _ (Just _) _ _)) = __IMPOSSIBLE__
toConcrete (Constr d) = head <$> toConcrete d
instance ToConcrete a C.LHS => ToConcrete (A.Clause' a) [C.Declaration] where
toConcrete (A.Clause lhs _ rhs wh catchall) =
bindToConcrete lhs $ \case
C.LHS p _ _ -> do
bindToConcrete wh $ \ wh' -> do
(rhs', eqs, with, wcs) <- toConcreteTop rhs
return $ FunClause (C.LHS p eqs with) rhs' wh' catchall : wcs
instance ToConcrete A.ModuleApplication C.ModuleApplication where
toConcrete (A.SectionApp tel y es) = do
y <- toConcreteCtx FunctionCtx y
bindToConcrete tel $ \ tel -> do
es <- toConcreteCtx argumentCtx_ es
let r = fuseRange y es
return $ C.SectionApp r tel (foldl (C.App r) (C.Ident y) es)
toConcrete (A.RecordModuleInstance recm) = do
recm <- toConcrete recm
return $ C.RecordModuleInstance (getRange recm) recm
instance ToConcrete A.Declaration [C.Declaration] where
toConcrete (ScopedDecl scope ds) =
withScope scope (declsToConcrete ds)
toConcrete (A.Axiom _ i info mp x t) = do
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
t' <- toConcreteTop t
return $
(case mp of
Nothing -> []
Just occs -> [C.Pragma (PolarityPragma noRange x' occs)]) ++
[C.Postulate (getRange i) [C.TypeSig info x' t']]
toConcrete (A.Generalize s i j x t) = do
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
t' <- toConcreteTop t
return [C.Generalize (getRange i) [C.TypeSig j x' $ C.Generalized t']]
toConcrete (A.Field i x t) = do
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
t' <- toConcreteTop t
return [C.Field (A.defInstance i) x' t']
toConcrete (A.Primitive i x t) = do
x' <- unsafeQNameToName <$> toConcrete x
withAbstractPrivate i $
withInfixDecl i x' $ do
t' <- toConcreteTop t
return [C.Primitive (getRange i) [C.TypeSig defaultArgInfo x' t']]
toConcrete (A.FunDef i _ _ cs) =
withAbstractPrivate i $ concat <$> toConcrete cs
toConcrete (A.DataSig i x bs t) =
withAbstractPrivate i $
bindToConcrete (A.generalizeTel bs) $ \ tel' -> do
x' <- unsafeQNameToName <$> toConcrete x
t' <- toConcreteTop t
return [ C.DataSig (getRange i) Inductive x' (map C.DomainFull tel') t' ]
toConcrete (A.DataDef i x uc bs cs) =
withAbstractPrivate i $
bindToConcrete (map makeDomainFree $ dataDefParams bs) $ \ tel' -> do
(x',cs') <- (unsafeQNameToName -*- id) <$> toConcrete (x, map Constr cs)
return [ C.DataDef (getRange i) Inductive x' tel' cs' ]
toConcrete (A.RecSig i x bs t) =
withAbstractPrivate i $
bindToConcrete (A.generalizeTel bs) $ \ tel' -> do
x' <- unsafeQNameToName <$> toConcrete x
t' <- toConcreteTop t
return [ C.RecordSig (getRange i) x' (map C.DomainFull tel') t' ]
toConcrete (A.RecDef i x uc ind eta c bs t cs) =
withAbstractPrivate i $
bindToConcrete (map makeDomainFree $ dataDefParams bs) $ \ tel' -> do
(x',cs') <- (unsafeQNameToName -*- id) <$> toConcrete (x, map Constr cs)
return [ C.RecordDef (getRange i) x' ind eta Nothing tel' cs' ]
toConcrete (A.Mutual i ds) = declsToConcrete ds
toConcrete (A.Section i x (A.GeneralizeTel _ tel) ds) = do
x <- toConcrete x
bindToConcrete tel $ \ tel -> do
ds <- declsToConcrete ds
return [ C.Module (getRange i) x tel ds ]
toConcrete (A.Apply i x modapp _ _) = do
x <- unsafeQNameToName <$> toConcrete x
modapp <- toConcrete modapp
let r = getRange modapp
open = fromMaybe DontOpen $ minfoOpenShort i
dir = fromMaybe defaultImportDir{ importDirRange = r } $ minfoDirective i
return [ C.ModuleMacro (getRange i) x modapp open dir ]
toConcrete (A.Import i x _) = do
x <- toConcrete x
let open = fromMaybe DontOpen $ minfoOpenShort i
dir = fromMaybe defaultImportDir $ minfoDirective i
return [ C.Import (getRange i) x Nothing open dir]
toConcrete (A.Pragma i p) = do
p <- toConcrete $ RangeAndPragma (getRange i) p
return [C.Pragma p]
toConcrete (A.Open i x _) = do
x <- toConcrete x
return [C.Open (getRange i) x defaultImportDir]
toConcrete (A.PatternSynDef x xs p) = do
C.QName x <- toConcrete x
bindToConcrete xs $ \xs -> (:[]) . C.PatternSyn (getRange x) x xs <$> dontFoldPatternSynonyms (toConcrete (vacuous p :: A.Pattern))
toConcrete (A.UnquoteDecl _ i xs e) = do
let unqual (C.QName x) = return x
unqual _ = __IMPOSSIBLE__
xs <- mapM (unqual <=< toConcrete) xs
(:[]) . C.UnquoteDecl (getRange i) xs <$> toConcrete e
toConcrete (A.UnquoteDef i xs e) = do
let unqual (C.QName x) = return x
unqual _ = __IMPOSSIBLE__
xs <- mapM (unqual <=< toConcrete) xs
(:[]) . C.UnquoteDef (getRange i) xs <$> toConcrete e
data RangeAndPragma = RangeAndPragma Range A.Pragma
instance ToConcrete RangeAndPragma C.Pragma where
toConcrete (RangeAndPragma r p) = case p of
A.OptionsPragma xs -> return $ C.OptionsPragma r xs
A.BuiltinPragma b x -> C.BuiltinPragma r b <$> toConcrete x
A.BuiltinNoDefPragma b x -> C.BuiltinPragma r b <$> toConcrete x
A.RewritePragma x -> C.RewritePragma r . singleton <$> toConcrete x
A.CompilePragma b x s -> do
x <- toConcrete x
return $ C.CompilePragma r b x s
A.StaticPragma x -> C.StaticPragma r <$> toConcrete x
A.InjectivePragma x -> C.InjectivePragma r <$> toConcrete x
A.InlinePragma b x -> C.InlinePragma r b <$> toConcrete x
A.EtaPragma x -> C.EtaPragma r <$> toConcrete x
A.DisplayPragma f ps rhs ->
C.DisplayPragma r <$> toConcrete (A.DefP (PatRange noRange) (unambiguous f) ps) <*> toConcrete rhs
instance ToConcrete A.SpineLHS C.LHS where
bindToConcrete lhs = bindToConcrete (A.spineToLhs lhs :: A.LHS)
instance ToConcrete A.LHS C.LHS where
bindToConcrete (A.LHS i lhscore) ret = do
bindToConcreteCtx TopCtx lhscore $ \ lhs ->
ret $ C.LHS lhs [] []
instance ToConcrete A.LHSCore C.Pattern where
bindToConcrete = bindToConcrete . lhsCoreToPattern
appBracketsArgs :: [arg] -> PrecedenceStack -> Bool
appBracketsArgs [] _ = False
appBracketsArgs (_:_) ctx = appBrackets ctx
newtype UserPattern a = UserPattern a
newtype SplitPattern a = SplitPattern a
newtype BindingPattern = BindingPat A.Pattern
newtype FreshenName = FreshenName BindName
instance ToConcrete FreshenName A.Name where
bindToConcrete (FreshenName (BindName x)) ret = bindToConcrete x $ \ y -> ret x { nameConcrete = y }
instance ToConcrete (UserPattern A.Pattern) A.Pattern where
bindToConcrete (UserPattern p) ret = do
reportSLn "toConcrete.pat" 100 $ "binding pattern (pass 1)" ++ show p
case p of
A.VarP bx -> do
let x = unBind bx
case isInScope x of
InScope -> bindName' x $ ret $ A.VarP bx
C.NotInScope -> bindName x $ \y ->
ret $ A.VarP $ BindName $ x { nameConcrete = y }
A.WildP{} -> ret p
A.ProjP{} -> ret p
A.AbsurdP{} -> ret p
A.LitP{} -> ret p
A.DotP{} -> ret p
A.EqualP{} -> ret p
A.ConP i c args
| patOrigin i == ConOSplit -> ret p
| otherwise -> bindToConcrete (map UserPattern args) $ ret . A.ConP i c
A.DefP i f args -> bindToConcrete (map UserPattern args) $ ret . A.DefP i f
A.PatternSynP i f args -> bindToConcrete (map UserPattern args) $ ret . A.PatternSynP i f
A.RecP i args -> bindToConcrete ((map . fmap) UserPattern args) $ ret . A.RecP i
A.AsP i x p -> bindName' (unBind x) $
bindToConcrete (UserPattern p) $ \ p ->
ret (A.AsP i x p)
A.WithP i p -> bindToConcrete (UserPattern p) $ ret . A.WithP i
instance ToConcrete (UserPattern (NamedArg A.Pattern)) (NamedArg A.Pattern) where
bindToConcrete (UserPattern np) ret =
case getOrigin np of
CaseSplit -> ret np
_ -> bindToConcrete (fmap (fmap UserPattern) np) ret
instance ToConcrete (SplitPattern A.Pattern) A.Pattern where
bindToConcrete (SplitPattern p) ret = do
reportSLn "toConcrete.pat" 100 $ "binding pattern (pass 2a)" ++ show p
case p of
A.VarP x -> ret p
A.WildP{} -> ret p
A.ProjP{} -> ret p
A.AbsurdP{} -> ret p
A.LitP{} -> ret p
A.DotP{} -> ret p
A.EqualP{} -> ret p
A.ConP i c args
| patOrigin i == ConOSplit
-> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.ConP i c
| otherwise -> bindToConcrete (map SplitPattern args) $ ret . A.ConP i c
A.DefP i f args -> bindToConcrete (map SplitPattern args) $ ret . A.DefP i f
A.PatternSynP i f args -> bindToConcrete (map SplitPattern args) $ ret . A.PatternSynP i f
A.RecP i args -> bindToConcrete ((map . fmap) SplitPattern args) $ ret . A.RecP i
A.AsP i x p -> bindToConcrete (SplitPattern p) $ \ p ->
ret (A.AsP i x p)
A.WithP i p -> bindToConcrete (SplitPattern p) $ ret . A.WithP i
instance ToConcrete (SplitPattern (NamedArg A.Pattern)) (NamedArg A.Pattern) where
bindToConcrete (SplitPattern np) ret =
case getOrigin np of
CaseSplit -> bindToConcrete (fmap (fmap BindingPat ) np) ret
_ -> bindToConcrete (fmap (fmap SplitPattern) np) ret
instance ToConcrete BindingPattern A.Pattern where
bindToConcrete (BindingPat p) ret = do
reportSLn "toConcrete.pat" 100 $ "binding pattern (pass 2b)" ++ show p
case p of
A.VarP x -> bindToConcrete (FreshenName x) $ ret . A.VarP . BindName
A.WildP{} -> ret p
A.ProjP{} -> ret p
A.AbsurdP{} -> ret p
A.LitP{} -> ret p
A.DotP{} -> ret p
A.EqualP{} -> ret p
A.ConP i c args -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.ConP i c
A.DefP i f args -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.DefP i f
A.PatternSynP i f args -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.PatternSynP i f
A.RecP i args -> bindToConcrete ((map . fmap) BindingPat args) $ ret . A.RecP i
A.AsP i x p -> bindToConcrete (FreshenName x) $ \ x ->
bindToConcrete (BindingPat p) $ \ p ->
ret (A.AsP i (BindName x) p)
A.WithP i p -> bindToConcrete (BindingPat p) $ ret . A.WithP i
instance ToConcrete A.Pattern C.Pattern where
bindToConcrete p ret = do
prec <- currentPrecedence
bindToConcrete (UserPattern p) $ \ p -> do
bindToConcrete (SplitPattern p) $ \ p -> do
ret =<< do withPrecedence' prec $ toConcrete p
toConcrete p =
case p of
A.VarP x ->
C.IdentP . C.QName . C.boundName <$> toConcrete x
A.WildP i ->
return $ C.WildP (getRange i)
A.ConP i c args -> tryOp (headAmbQ c) (A.ConP i c) args
A.ProjP i ProjPrefix p -> C.IdentP <$> toConcrete (headAmbQ p)
A.ProjP i _ p -> C.DotP noRange . C.Ident <$> toConcrete (headAmbQ p)
A.DefP i x args -> tryOp (headAmbQ x) (A.DefP i x) args
A.AsP i x p -> do
(x, p) <- toConcreteCtx argumentCtx_ (x, p)
return $ C.AsP (getRange i) (C.boundName x) p
A.AbsurdP i ->
return $ C.AbsurdP (getRange i)
A.LitP (LitQName r x) -> do
x <- lookupQName AmbiguousNothing x
bracketP_ appBrackets $ return $ C.AppP (C.QuoteP r) (defaultNamedArg (C.IdentP x))
A.LitP l ->
return $ C.LitP l
A.DotP i e@A.Proj{} -> C.DotP r . C.Paren r <$> toConcreteCtx TopCtx e
where r = getRange i
A.DotP i e@(A.Var v) -> do
let r = getRange i
cn <- toConcreteName v
liftTCM (resolveName' [FldName] Nothing (C.QName cn)) >>= \case
FieldName{} -> do
reportSLn "print.dotted" 50 $ "Wrapping ambiguous name " ++ show (nameConcrete v)
C.DotP r . C.Paren r <$> toConcrete (A.Var v)
_ -> printDotDefault i e
A.DotP i e -> printDotDefault i e
A.EqualP i es -> do
C.EqualP (getRange i) <$> toConcrete es
A.PatternSynP i n args -> tryOp (headAmbQ n) (A.PatternSynP i n) args
A.RecP i as ->
C.RecP (getRange i) <$> mapM (traverse toConcrete) as
A.WithP i p -> C.WithP (getRange i) <$> toConcreteCtx WithArgCtx p
where
printDotDefault :: PatInfo -> A.Expr -> AbsToCon C.Pattern
printDotDefault i e = do
c <- toConcreteCtx DotPatternCtx e
let r = getRange i
case c of
C.Underscore{} -> return $ C.WildP r
_ -> return $ C.DotP r c
tryOp :: A.QName -> (A.Patterns -> A.Pattern) -> A.Patterns -> AbsToCon C.Pattern
tryOp x f args = do
let (args1, args2) = splitAt (numHoles x) args
let funCtx = if null args2 then id else withPrecedence FunctionCtx
tryToRecoverPatternSynP (f args) $ funCtx (tryToRecoverOpAppP $ f args1) >>= \case
Just c -> applyTo args2 c
Nothing -> applyTo args . C.IdentP =<< toConcrete x
applyTo args c = bracketP_ (appBracketsArgs args) $ do
foldl C.AppP c <$> toConcreteCtx argumentCtx_ args
tryToRecoverNatural :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverNatural e def = do
is <- isBuiltinFun
caseMaybe (recoverNatural is e) def $ return . C.Lit . LitNat noRange
recoverNatural :: (A.QName -> String -> Bool) -> A.Expr -> Maybe Integer
recoverNatural is e = explore (`is` builtinZero) (`is` builtinSuc) 0 e
where
explore :: (A.QName -> Bool) -> (A.QName -> Bool) -> Integer -> A.Expr -> Maybe Integer
explore isZero isSuc k (A.App _ (A.Con c) t) | Just f <- getUnambiguous c, isSuc f
= (explore isZero isSuc $! k + 1) (namedArg t)
explore isZero isSuc k (A.Con c) | Just x <- getUnambiguous c, isZero x = Just k
explore isZero isSuc k (A.Lit (LitNat _ l)) = Just (k + l)
explore _ _ _ _ = Nothing
data Hd = HdVar A.Name | HdCon A.QName | HdDef A.QName | HdSyn A.QName
data MaybeSection a
= YesSection
| NoSection a
deriving (Eq, Show, Functor, Foldable, Traversable)
fromNoSection :: a -> MaybeSection a -> a
fromNoSection fallback = \case
YesSection -> fallback
NoSection x -> x
instance HasRange a => HasRange (MaybeSection a) where
getRange = \case
YesSection -> noRange
NoSection a -> getRange a
getHead :: A.Expr -> Maybe Hd
getHead (Var x) = Just (HdVar x)
getHead (Def f) = Just (HdDef f)
getHead (Proj o f) = Just (HdDef $ headAmbQ f)
getHead (Con c) = Just (HdCon $ headAmbQ c)
getHead (A.PatternSyn n) = Just (HdSyn $ headAmbQ n)
getHead _ = Nothing
cOpApp :: Range -> C.QName -> A.Name -> [MaybeSection C.Expr] -> C.Expr
cOpApp r x n es =
C.OpApp r x (Set.singleton n)
(map (defaultNamedArg . placeholder) eps)
where
x0 = C.unqualify x
positions | isPrefix x0 = [ Middle | _ <- drop 1 es ] ++ [End]
| isPostfix x0 = [Beginning] ++ [ Middle | _ <- drop 1 es ]
| isInfix x0 = [Beginning] ++ [ Middle | _ <- drop 2 es ] ++ [End]
| otherwise = [ Middle | _ <- es ]
eps = zip es positions
placeholder (YesSection , pos ) = Placeholder pos
placeholder (NoSection e, _pos) = noPlaceholder (Ordinary e)
tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverOpApp e def = fromMaybeM def $
recoverOpApp bracket (isLambda . defaultNamedArg) cOpApp view e
where
view :: A.Expr -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, A.Expr))])
view e
| Just xs@(_:_) <- traverse insertedName bs =
(,) <$> getHead hd <*> sectionArgs (map unBind xs) args
where
LamView bs body = A.lamView e
Application hd args = A.appView' body
insertedName (A.DomainFree x)
| getOrigin x == Inserted && visible x = Just $ namedArg x
insertedName _ = Nothing
sectionArgs :: [A.Name] -> [NamedArg (AppInfo, A.Expr)] -> Maybe [NamedArg (MaybeSection (AppInfo, A.Expr))]
sectionArgs xs = go xs
where
noXs = getAll . foldExpr (\ case A.Var x -> All (notElem x xs)
_ -> All True) . snd . namedArg
go [] [] = return []
go (y : ys) (arg : args)
| visible arg
, A.Var y' <- snd $ namedArg arg
, y == y' = (fmap (YesSection <$) arg :) <$> go ys args
go ys (arg : args)
| visible arg, noXs arg = ((fmap . fmap) NoSection arg :) <$> go ys args
go _ _ = Nothing
view e = (, (map . fmap . fmap) NoSection args) <$> getHead hd
where Application hd args = A.appView' e
tryToRecoverOpAppP :: A.Pattern -> AbsToCon (Maybe C.Pattern)
tryToRecoverOpAppP p = do
res <- recoverOpApp bracketP_ (const False) opApp view p
lift $ reportSLn "print.op" 90 $ unlines
[ "tryToRecoverOpApp"
, "in: " ++ show p
, "out: " ++ show res
]
return res
where
opApp r x n ps = C.OpAppP r x (Set.singleton n) $
map (defaultNamedArg . fromNoSection __IMPOSSIBLE__) ps
appInfo = defaultAppInfo_
view :: A.Pattern -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, A.Pattern))])
view p = case p of
ConP _ cs ps -> Just (HdCon (headAmbQ cs), (map . fmap . fmap) (NoSection . (appInfo,)) ps)
DefP _ fs ps -> Just (HdDef (headAmbQ fs), (map . fmap . fmap) (NoSection . (appInfo,)) ps)
PatternSynP _ ns ps -> Just (HdSyn (headAmbQ ns), (map . fmap . fmap) (NoSection . (appInfo,)) ps)
_ -> Nothing
recoverOpApp :: forall a c . (ToConcrete a c, HasRange c)
=> ((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)
-> (a -> Bool)
-> (Range -> C.QName -> A.Name -> [MaybeSection c] -> c)
-> (a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))]))
-> a
-> AbsToCon (Maybe c)
recoverOpApp bracket isLam opApp view e = case view e of
Nothing -> mDefault
Just (hd, args)
| all visible args -> do
let args' = map namedArg args
case hd of
HdVar n
| isNoName n -> mDefault
| otherwise -> doQNameHelper (Left n) args'
HdDef qn
| isExtendedLambdaName qn
-> mDefault
| otherwise -> doQNameHelper (Right qn) args'
HdCon qn -> doQNameHelper (Right qn) args'
HdSyn qn -> doQNameHelper (Right qn) args'
| otherwise -> mDefault
where
mDefault = return Nothing
skipParens :: MaybeSection (AppInfo, a) -> Bool
skipParens = \case
YesSection -> False
NoSection (i, e) -> isLam e && preferParenless (appParens i)
doQNameHelper :: Either A.Name A.QName -> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
doQNameHelper n args = do
x <- either (C.QName <.> toConcrete) toConcrete n
let n' = either id A.qnameName n
doQName (theFixity $ nameFixity n') x n' args (C.nameParts $ C.unqualify x)
doQName :: Fixity -> C.QName -> A.Name -> [MaybeSection (AppInfo, a)] -> [NamePart] -> AbsToCon (Maybe c)
doQName _ x _ es xs
| null es = mDefault
| length es /= numHoles x = mDefault
doQName fixity x n as xs
| Hole <- head xs
, Hole <- last xs = do
let a1 = head as
an = last as
as' = case as of
as@(_ : _ : _) -> init $ tail as
_ -> __IMPOSSIBLE__
Just <$> do
bracket (opBrackets' (skipParens an) fixity) $ do
e1 <- traverse (toConcreteCtx (LeftOperandCtx fixity) . snd) a1
es <- (mapM . traverse) (toConcreteCtx InsideOperandCtx . snd) as'
en <- traverse (uncurry $ toConcreteCtx . RightOperandCtx fixity . appParens) an
return $ opApp (getRange (e1, en)) x n ([e1] ++ es ++ [en])
doQName fixity x n as xs
| Hole <- last xs = do
let an = last as
as' = case as of
as@(_ : _) -> init as
_ -> __IMPOSSIBLE__
Just <$> do
bracket (opBrackets' (skipParens an) fixity) $ do
es <- (mapM . traverse) (toConcreteCtx InsideOperandCtx . snd) as'
en <- traverse (\ (i, e) -> toConcreteCtx (RightOperandCtx fixity $ appParens i) e) an
return $ opApp (getRange (n, en)) x n (es ++ [en])
doQName fixity x n as xs
| Hole <- head xs = do
let a1 = head as
as' = tail as
e1 <- traverse (toConcreteCtx (LeftOperandCtx fixity) . snd) a1
es <- (mapM . traverse) (toConcreteCtx InsideOperandCtx . snd) as'
Just <$> do
bracket (opBrackets fixity) $
return $ opApp (getRange (e1, n)) x n ([e1] ++ es)
doQName _ x n as xs = do
es <- (mapM . traverse) (toConcreteCtx InsideOperandCtx . snd) as
Just <$> do
bracket roundFixBrackets $
return $ opApp (getRange x) x n es
tryToRecoverPatternSyn :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverPatternSyn e fallback
| userWritten e = fallback
| litOrCon e = recoverPatternSyn apply matchPatternSyn e fallback
| otherwise = fallback
where
userWritten (A.App info _ _) = getOrigin info == UserWritten
userWritten _ = False
litOrCon e =
case A.appView e of
Application Con{} _ -> True
Application A.Lit{} _ -> True
_ -> False
apply c args = A.unAppView $ Application (A.PatternSyn $ unambiguous c) args
tryToRecoverPatternSynP :: A.Pattern -> AbsToCon C.Pattern -> AbsToCon C.Pattern
tryToRecoverPatternSynP = recoverPatternSyn apply matchPatternSynP
where apply c args = PatternSynP patNoRange (unambiguous c) args
recoverPatternSyn :: ToConcrete a c =>
(A.QName -> [NamedArg a] -> a) ->
(PatternSynDefn -> a -> Maybe [Arg a]) ->
a -> AbsToCon c -> AbsToCon c
recoverPatternSyn applySyn match e fallback = do
doFold <- asks foldPatternSynonyms
if not doFold then fallback else do
psyns <- lift getAllPatternSyns
scope <- lift getScope
let isConP ConP{} = True
isConP _ = False
cands = [ (q, args, score rhs) | (q, psyndef@(_, rhs)) <- reverse $ Map.toList psyns,
isConP rhs, Just args <- [match psyndef e],
isNameInScope q scope ]
cmp (_, _, x) (_, _, y) = flip compare x y
case sortBy cmp cands of
(q, args, _) : _ -> toConcrete $ applySyn q $ (map . fmap) unnamed args
[] -> fallback
where
score :: Pattern' Void -> Int
score = getSum . foldAPattern con
where con ConP{} = 1
con _ = 0
instance ToConcrete InteractionId C.Expr where
toConcrete (InteractionId i) = return $ C.QuestionMark noRange (Just i)
instance ToConcrete NamedMeta C.Expr where
toConcrete i = do
return $ C.Underscore noRange (Just $ prettyShow i)