{-# LANGUAGE CPP          #-}

-- {-# OPTIONS -fwarn-unused-binds #-}

{-| The translation of abstract syntax to concrete syntax has two purposes.
    First it allows us to pretty print abstract syntax values without having to
    write a dedicated pretty printer, and second it serves as a sanity check
    for the concrete to abstract translation: translating from concrete to
    abstract and then back again should be (more or less) the identity.
-}
module Agda.Syntax.Translation.AbstractToConcrete
    ( ToConcrete(..)
    , toConcreteCtx
    , abstractToConcrete_
    , abstractToConcreteScope
    , abstractToConcreteHiding
    , runAbsToCon
    , RangeAndPragma(..)
    , abstractToConcreteCtx
    , withScope
    , preserveInteractionIds
    , MonadAbsToCon, AbsToCon, Env
    , noTakenNames
    , lookupQName
    ) where

import Prelude hiding (null)

import Control.Arrow        ( (&&&), first )
import Control.Monad        ( (<=<), forM, forM_, guard, liftM2 )
import Control.Monad.Except ( runExceptT )
import Control.Monad.Reader ( MonadReader(..), asks, runReaderT )
import Control.Monad.State  ( StateT(..), runStateT )

import qualified Control.Monad.Fail as Fail

import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid hiding ((<>))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Foldable as Fold
import Data.Void
import Data.List (sortBy)
import Data.Semigroup (Semigroup, (<>))
import Data.String

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Info as A
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Fixity
import Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pattern as C
import Agda.Syntax.Concrete.Glyph
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 ( tryResolveName )

import Agda.TypeChecking.Monad.State (getScope, getAllPatternSyns)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Pure
import Agda.TypeChecking.Monad.Signature
import {-# SOURCE #-} Agda.TypeChecking.Pretty (prettyTCM)
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.Lens
import Agda.Utils.List1 (List1, pattern (:|), (<|) )
import Agda.Utils.List2 (List2, pattern List2)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Singleton
import Agda.Utils.Suffix

import Agda.Utils.Impossible

-- Environment ------------------------------------------------------------

data Env = Env { Env -> Set Name
takenVarNames :: Set A.Name
                  -- ^ Abstract names currently in scope. Unlike the
                  --   ScopeInfo, this includes names for hidden
                  --   arguments inserted by the system.
               , Env -> Set NameParts
takenDefNames :: Set C.NameParts
                  -- ^ Concrete names of all definitions in scope
               , Env -> ScopeInfo
currentScope :: ScopeInfo
               , Env -> Map RawName QName
builtins     :: Map String A.QName
                  -- ^ Certain builtins (like `fromNat`) have special printing
               , Env -> Bool
preserveIIds :: Bool
                  -- ^ Preserve interaction point ids
               , Env -> Bool
foldPatternSynonyms :: Bool
               }

makeEnv :: MonadAbsToCon m => ScopeInfo -> m Env
makeEnv :: forall (m :: * -> *). MonadAbsToCon m => ScopeInfo -> m Env
makeEnv ScopeInfo
scope = do
      -- zero and suc doesn't have to be in scope for natural number literals to work
  let noScopeCheck :: RawName -> Bool
noScopeCheck RawName
b = RawName
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RawName
builtinZero, RawName
builtinSuc]
      name :: Term -> Maybe QName
name (I.Def QName
q Elims
_)   = forall a. a -> Maybe a
Just QName
q
      name (I.Con ConHead
q ConInfo
_ Elims
_) = forall a. a -> Maybe a
Just (ConHead -> QName
I.conName ConHead
q)
      name Term
_             = forall a. Maybe a
Nothing
      builtin :: RawName -> m [(RawName, QName)]
builtin RawName
b = forall (m :: * -> *). HasBuiltins m => RawName -> m (Maybe Term)
getBuiltin' RawName
b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
        Just Term
v | Just QName
q <- Term -> Maybe QName
name Term
v,
                 RawName -> Bool
noScopeCheck RawName
b Bool -> Bool -> Bool
|| QName -> ScopeInfo -> Bool
isNameInScope QName
q ScopeInfo
scope -> forall (m :: * -> *) a. Monad m => a -> m a
return [(RawName
b, QName
q)]
        Maybe Term
_                                                -> forall (m :: * -> *) a. Monad m => a -> m a
return []
  [Name]
ctxVars <- forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
I.unDom) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext
  [Name]
letVars <- forall k a. Map k a -> [k]
Map.keys forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
  let vars :: [Name]
vars = [Name]
ctxVars forall a. [a] -> [a] -> [a]
++ [Name]
letVars

  -- pick concrete names for in-scope names now so we don't
  -- accidentally shadow them
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' [(Name, LocalVar)] ScopeInfo
scopeLocals) forall a b. (a -> b) -> a -> b
$ \(Name
y , LocalVar
x) -> do
    forall (m :: * -> *).
MonadStConcreteNames m =>
Name -> Name -> m ()
pickConcreteName (LocalVar -> Name
localVar LocalVar
x) Name
y

  [(RawName, QName)]
builtinList <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RawName -> m [(RawName, QName)]
builtin [ RawName
builtinFromNat, RawName
builtinFromString, RawName
builtinFromNeg, RawName
builtinZero, RawName
builtinSuc ]
  Bool
foldPatSyns <- PragmaOptions -> Bool
optPrintPatternSynonyms forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Env { takenVarNames :: Set Name
takenVarNames = forall a. Ord a => [a] -> Set a
Set.fromList [Name]
vars
        , takenDefNames :: Set NameParts
takenDefNames = Set NameParts
defs
        , currentScope :: ScopeInfo
currentScope = ScopeInfo
scope
        , builtins :: Map RawName QName
builtins     = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ [(RawName, QName)]
builtinList
        , preserveIIds :: Bool
preserveIIds = Bool
False
        , foldPatternSynonyms :: Bool
foldPatternSynonyms = Bool
foldPatSyns
        }
  where
    defs :: Set NameParts
defs = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Name -> NameParts
nameParts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$
        forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey forall {t :: * -> *}. Foldable t => Name -> t AbstractName -> Bool
usefulDef forall a b. (a -> b) -> a -> b
$
        NameSpace -> Map Name [AbstractName]
nsNames forall a b. (a -> b) -> a -> b
$ ScopeInfo -> NameSpace
everythingInScope ScopeInfo
scope

    -- Jesper, 2018-12-10: It's fine to shadow generalizable names as
    -- they will never show up directly in printed terms.
    notGeneralizeName :: AbstractName -> Bool
notGeneralizeName AbsName{ anameKind :: AbstractName -> KindOfName
anameKind = KindOfName
k }  =
      Bool -> Bool
not (KindOfName
k forall a. Eq a => a -> a -> Bool
== KindOfName
GeneralizeName Bool -> Bool -> Bool
|| KindOfName
k forall a. Eq a => a -> a -> Bool
== KindOfName
DisallowedGeneralizeName)

    usefulDef :: Name -> t AbstractName -> Bool
usefulDef C.NoName{} t AbstractName
_ = Bool
False
    usefulDef C.Name{} t AbstractName
names = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all AbstractName -> Bool
notGeneralizeName t AbstractName
names

    nameParts :: Name -> NameParts
nameParts (C.NoName {}) = forall a. HasCallStack => a
__IMPOSSIBLE__
    nameParts (C.Name { NameParts
nameNameParts :: Name -> NameParts
nameNameParts :: NameParts
nameNameParts }) = NameParts
nameNameParts

currentPrecedence :: AbsToCon PrecedenceStack
currentPrecedence :: AbsToCon PrecedenceStack
currentPrecedence = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ (forall o i. o -> Lens' i o -> i
^. Lens' PrecedenceStack ScopeInfo
scopePrecedence) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ScopeInfo
currentScope

preserveInteractionIds :: AbsToCon a -> AbsToCon a
preserveInteractionIds :: forall a. AbsToCon a -> AbsToCon a
preserveInteractionIds = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \ Env
e -> Env
e { preserveIIds :: Bool
preserveIIds = Bool
True }

withPrecedence' :: PrecedenceStack -> AbsToCon a -> AbsToCon a
withPrecedence' :: forall a. PrecedenceStack -> AbsToCon a -> AbsToCon a
withPrecedence' PrecedenceStack
ps = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \Env
e ->
  Env
e { currentScope :: ScopeInfo
currentScope = forall i o. Lens' i o -> LensSet i o
set Lens' PrecedenceStack ScopeInfo
scopePrecedence PrecedenceStack
ps (Env -> ScopeInfo
currentScope Env
e) }

withPrecedence :: Precedence -> AbsToCon a -> AbsToCon a
withPrecedence :: forall a. Precedence -> AbsToCon a -> AbsToCon a
withPrecedence Precedence
p AbsToCon a
ret = do
  PrecedenceStack
ps <- AbsToCon PrecedenceStack
currentPrecedence
  forall a. PrecedenceStack -> AbsToCon a -> AbsToCon a
withPrecedence' (Precedence -> PrecedenceStack -> PrecedenceStack
pushPrecedence Precedence
p PrecedenceStack
ps) AbsToCon a
ret

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a
withScope :: forall a. ScopeInfo -> AbsToCon a -> AbsToCon a
withScope ScopeInfo
scope = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \Env
e -> Env
e { currentScope :: ScopeInfo
currentScope = ScopeInfo
scope }

noTakenNames :: AbsToCon a -> AbsToCon a
noTakenNames :: forall a. AbsToCon a -> AbsToCon a
noTakenNames = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \Env
e -> Env
e { takenVarNames :: Set Name
takenVarNames = forall a. Set a
Set.empty }

dontFoldPatternSynonyms :: AbsToCon a -> AbsToCon a
dontFoldPatternSynonyms :: forall a. AbsToCon a -> AbsToCon a
dontFoldPatternSynonyms = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ \ Env
e -> Env
e { foldPatternSynonyms :: Bool
foldPatternSynonyms = Bool
False }

-- | Bind a concrete name to an abstract in the translation environment.
addBinding :: C.Name -> A.Name -> Env -> Env
addBinding :: Name -> Name -> Env -> Env
addBinding Name
y Name
x Env
e =
  Env
e { takenVarNames :: Set Name
takenVarNames = forall a. Ord a => a -> Set a -> Set a
Set.insert Name
x forall a b. (a -> b) -> a -> b
$ Env -> Set Name
takenVarNames Env
e
    , currentScope :: ScopeInfo
currentScope = (([(Name, LocalVar)] -> [(Name, LocalVar)])
-> ScopeInfo -> ScopeInfo
`updateScopeLocals` Env -> ScopeInfo
currentScope Env
e) forall a b. (a -> b) -> a -> b
$
        forall k v. k -> v -> AssocList k v -> AssocList k v
AssocList.insert Name
y (Name -> BindingSource -> [AbstractName] -> LocalVar
LocalVar Name
x forall a. HasCallStack => a
__IMPOSSIBLE__ [])
    }

-- | Get a function to check if a name refers to a particular builtin function.
isBuiltinFun :: AbsToCon (A.QName -> String -> Bool)
isBuiltinFun :: AbsToCon (QName -> RawName -> Bool)
isBuiltinFun = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ forall {k} {a}. (Ord k, Eq a) => Map k a -> a -> k -> Bool
is forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Map RawName QName
builtins
  where is :: Map k a -> a -> k -> Bool
is Map k a
m a
q k
b = forall a. a -> Maybe a
Just a
q forall a. Eq a => a -> a -> Bool
== forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
b Map k a
m

-- | Resolve a concrete name. If illegally ambiguous fail with the ambiguous names.
resolveName :: KindsOfNames -> Maybe (Set A.Name) -> C.QName -> AbsToCon (Either AmbiguousNameReason ResolvedName)
resolveName :: KindsOfNames
-> Maybe (Set Name)
-> QName
-> AbsToCon (Either AmbiguousNameReason ResolvedName)
resolveName KindsOfNames
kinds Maybe (Set Name)
candidates QName
q = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(ReadTCState m, HasBuiltins m, MonadError AmbiguousNameReason m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
candidates QName
q

-- | Treat illegally ambiguous names as UnknownNames.
resolveName_ :: C.QName -> [A.Name] -> AbsToCon ResolvedName
resolveName_ :: QName -> [Name] -> AbsToCon ResolvedName
resolveName_ QName
q [Name]
cands = forall a b. (a -> b) -> Either a b -> b
fromRight (forall a b. a -> b -> a
const ResolvedName
UnknownName) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KindsOfNames
-> Maybe (Set Name)
-> QName
-> AbsToCon (Either AmbiguousNameReason ResolvedName)
resolveName KindsOfNames
allKindsOfNames (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [Name]
cands) QName
q

-- The Monad --------------------------------------------------------------

-- | The function 'runAbsToCon' can target any monad that satisfies
-- the constraints of 'MonadAbsToCon'.
type MonadAbsToCon m =
  ( MonadFresh NameId m
  , MonadInteractionPoints m
  , MonadStConcreteNames m
  , HasOptions m
  , PureTCM m
  , IsString (m Doc)
  , Null (m Doc)
  , Semigroup (m Doc)
  )

newtype AbsToCon a = AbsToCon
  { forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon :: forall m.
      ( MonadReader Env m
      , MonadAbsToCon m
      ) => m a
  }

-- TODO: Is there some way to automatically derive these boilerplate
-- instances?  GeneralizedNewtypeDeriving fails us here.
instance Functor AbsToCon where
  fmap :: forall a b. (a -> b) -> AbsToCon a -> AbsToCon b
fmap a -> b
f AbsToCon a
x = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
x

instance Applicative AbsToCon where
  pure :: forall a. a -> AbsToCon a
pure a
x = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
  AbsToCon (a -> b)
f <*> :: forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
<*> AbsToCon a
m = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon (a -> b)
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
m

instance Monad AbsToCon where
  -- ASR (2021-02-07). The eta-expansion @\m' -> unAbsToCon m'@ is
  -- required by GHC >= 9.0.1 (see Issue #4955).
  AbsToCon a
m >>= :: forall a b. AbsToCon a -> (a -> AbsToCon b) -> AbsToCon b
>>= a -> AbsToCon b
f = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\AbsToCon b
m' -> forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon b
m')forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AbsToCon b
f
#if __GLASGOW_HASKELL__ < 808
  fail = Fail.fail
#endif

instance Fail.MonadFail AbsToCon where
  fail :: forall a. RawName -> AbsToCon a
fail = forall a. HasCallStack => RawName -> a
error

instance MonadReader Env AbsToCon where
  ask :: AbsToCon Env
ask = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: forall a. (Env -> Env) -> AbsToCon a -> AbsToCon a
local Env -> Env
f AbsToCon a
m = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Env -> Env
f forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
m

instance MonadTCEnv AbsToCon where
  askTC :: AbsToCon TCEnv
askTC = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
  localTC :: forall a. (TCEnv -> TCEnv) -> AbsToCon a -> AbsToCon a
localTC TCEnv -> TCEnv
f AbsToCon a
m = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC TCEnv -> TCEnv
f forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
m

instance ReadTCState AbsToCon where
  getTCState :: AbsToCon TCState
getTCState = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> AbsToCon b -> AbsToCon b
locallyTCState Lens' a TCState
l a -> a
f AbsToCon b
m = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' a TCState
l a -> a
f forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon b
m

instance MonadStConcreteNames AbsToCon where
  -- ASR (2021-02-07). The eta-expansion @\m' -> unAbsToCon m'@ is
  -- required by GHC >= 9.0.1 (see Issue #4955).
  runStConcreteNames :: forall a. StateT ConcreteNames AbsToCon a -> AbsToCon a
runStConcreteNames StateT ConcreteNames AbsToCon a
m =
    forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall a b. (a -> b) -> a -> b
$ (\AbsToCon (a, ConcreteNames)
m' -> forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon (a, ConcreteNames)
m') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames AbsToCon a
m

instance HasBuiltins AbsToCon where
  getBuiltinThing :: RawName -> AbsToCon (Maybe (Builtin PrimFun))
getBuiltinThing RawName
x = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasBuiltins m =>
RawName -> m (Maybe (Builtin PrimFun))
getBuiltinThing RawName
x

instance HasOptions AbsToCon where
  pragmaOptions :: AbsToCon PragmaOptions
pragmaOptions = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  commandLineOptions :: AbsToCon CommandLineOptions
commandLineOptions = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions

instance MonadDebug AbsToCon where
  formatDebugMessage :: RawName -> VerboseLevel -> TCM Doc -> AbsToCon RawName
formatDebugMessage RawName
k VerboseLevel
n TCM Doc
s      = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> TCM Doc -> m RawName
formatDebugMessage RawName
k VerboseLevel
n TCM Doc
s
  traceDebugMessage :: forall a.
RawName -> VerboseLevel -> RawName -> AbsToCon a -> AbsToCon a
traceDebugMessage  RawName
k VerboseLevel
n RawName
s AbsToCon a
cont = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m a -> m a
traceDebugMessage  RawName
k VerboseLevel
n RawName
s forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
cont  -- can't eta-reduce!
  verboseBracket :: forall a.
RawName -> VerboseLevel -> RawName -> AbsToCon a -> AbsToCon a
verboseBracket     RawName
k VerboseLevel
n RawName
s AbsToCon a
cont = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m a -> m a
verboseBracket     RawName
k VerboseLevel
n RawName
s forall a b. (a -> b) -> a -> b
$ forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
cont  -- because of GHC-9.0

  getVerbosity :: AbsToCon Verbosity
getVerbosity      = forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  getProfileOptions :: AbsToCon ProfileOptions
getProfileOptions = forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions
  isDebugPrinting :: AbsToCon Bool
isDebugPrinting   = forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. AbsToCon a -> AbsToCon a
nowDebugPrinting  = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting

instance HasConstInfo AbsToCon where
  getConstInfo' :: QName -> AbsToCon (Either SigError Definition)
getConstInfo' QName
a      = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
a)
  getRewriteRulesFor :: QName -> AbsToCon RewriteRules
getRewriteRulesFor QName
a = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
getRewriteRulesFor QName
a)

instance MonadAddContext AbsToCon where
  addCtx :: forall a. Name -> Dom Type -> AbsToCon a -> AbsToCon a
addCtx Name
a Dom Type
b AbsToCon a
c = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
addCtx Name
a Dom Type
b (forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
c))

  addLetBinding' :: forall a. Name -> Term -> Dom Type -> AbsToCon a -> AbsToCon a
addLetBinding' Name
a Term
b Dom Type
c AbsToCon a
d =
    forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Term -> Dom Type -> m a -> m a
addLetBinding' Name
a Term
b Dom Type
c (forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
d))

  updateContext :: forall a.
Substitution -> (Context -> Context) -> AbsToCon a -> AbsToCon a
updateContext Substitution
a Context -> Context
b AbsToCon a
c = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
a Context -> Context
b (forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon a
c))

  withFreshName :: forall a. Range -> RawName -> (Name -> AbsToCon a) -> AbsToCon a
withFreshName Range
a RawName
b Name -> AbsToCon a
c =
    forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *) a.
MonadAddContext m =>
Range -> RawName -> (Name -> m a) -> m a
withFreshName Range
a RawName
b (\Name
x -> forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon (Name -> AbsToCon a
c Name
x)))

instance MonadReduce AbsToCon where
  liftReduce :: forall a. ReduceM a -> AbsToCon a
liftReduce ReduceM a
a = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce ReduceM a
a)

instance PureTCM AbsToCon where

instance MonadFresh NameId AbsToCon where
  fresh :: AbsToCon NameId
fresh = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall i (m :: * -> *). MonadFresh i m => m i
fresh

instance MonadInteractionPoints AbsToCon where
  freshInteractionId :: AbsToCon InteractionId
freshInteractionId        = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> AbsToCon ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
a = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
a)

instance IsString (AbsToCon Doc) where
  fromString :: RawName -> AbsToCon Doc
fromString RawName
a = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall a. IsString a => RawName -> a
fromString RawName
a)

instance Null (AbsToCon Doc) where
  empty :: AbsToCon Doc
empty = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon forall a. Null a => a
empty
  null :: AbsToCon Doc -> Bool
null  = forall a. HasCallStack => a
__IMPOSSIBLE__

instance Semigroup (AbsToCon Doc) where
  AbsToCon Doc
a <> :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc
<> AbsToCon Doc
b = forall a.
(forall (m :: * -> *). (MonadReader Env m, MonadAbsToCon m) => m a)
-> AbsToCon a
AbsToCon (forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon Doc
a forall a. Semigroup a => a -> a -> a
<> forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon Doc
b)

runAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon :: forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon AbsToCon c
m = do
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  forall (m :: * -> *) a.
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m a -> m a
verboseBracket RawName
"toConcrete" VerboseLevel
50 RawName
"runAbsToCon" forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ Doc -> RawName
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$
      [ Doc
"entering AbsToCon with scope:"
      , forall a. Pretty a => [a] -> Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (RawName -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RawName
C.nameToRawName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' [(Name, LocalVar)] ScopeInfo
scopeLocals)
      ]
    c
x <- forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon AbsToCon c
m) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadAbsToCon m => ScopeInfo -> m Env
makeEnv ScopeInfo
scope
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ RawName
"leaving AbsToCon"
    forall (m :: * -> *) a. Monad m => a -> m a
return c
x

abstractToConcreteScope :: (ToConcrete a, MonadAbsToCon m)
                        => ScopeInfo -> a -> m (ConOfAbs a)
abstractToConcreteScope :: forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
ScopeInfo -> a -> m (ConOfAbs a)
abstractToConcreteScope ScopeInfo
scope a
a = forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (forall a.
AbsToCon a
-> forall (m :: * -> *).
   (MonadReader Env m, MonadAbsToCon m) =>
   m a
unAbsToCon forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
a) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadAbsToCon m => ScopeInfo -> m Env
makeEnv ScopeInfo
scope

abstractToConcreteCtx :: (ToConcrete a, MonadAbsToCon m)
                      => Precedence -> a -> m (ConOfAbs a)
abstractToConcreteCtx :: forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
Precedence -> a -> m (ConOfAbs a)
abstractToConcreteCtx Precedence
ctx a
x = forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon forall a b. (a -> b) -> a -> b
$ forall a. Precedence -> AbsToCon a -> AbsToCon a
withPrecedence Precedence
ctx (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
x)

abstractToConcrete_ :: (ToConcrete a, MonadAbsToCon m)
                    => a -> m (ConOfAbs a)
abstractToConcrete_ :: forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ = forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete

abstractToConcreteHiding :: (LensHiding i, ToConcrete a, MonadAbsToCon m)
                         => i -> a -> m (ConOfAbs a)
abstractToConcreteHiding :: forall i a (m :: * -> *).
(LensHiding i, ToConcrete a, MonadAbsToCon m) =>
i -> a -> m (ConOfAbs a)
abstractToConcreteHiding i
i = forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall h a.
(LensHiding h, ToConcrete a) =>
h -> a -> AbsToCon (ConOfAbs a)
toConcreteHiding i
i

-- Dealing with names -----------------------------------------------------

-- | Names in abstract syntax are fully qualified, but the concrete syntax
--   requires non-qualified names in places. In theory (if all scopes are
--   correct), we should get a non-qualified name when translating back to a
--   concrete name, but I suspect the scope isn't always perfect. In these
--   cases we just throw away the qualified part. It's just for pretty printing
--   anyway...
unsafeQNameToName :: C.QName -> C.Name
unsafeQNameToName :: QName -> Name
unsafeQNameToName = QName -> Name
C.unqualify

lookupQName :: AllowAmbiguousNames -> A.QName -> AbsToCon C.QName
lookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName
lookupQName AllowAmbiguousNames
ambCon QName
x | Just RawName
s <- QName -> Maybe RawName
getGeneralizedFieldName QName
x =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> NameParts -> Name
C.Name forall a. Range' a
noRange NameInScope
C.InScope forall a b. (a -> b) -> a -> b
$ RawName -> NameParts
C.stringNameParts RawName
s)
lookupQName AllowAmbiguousNames
ambCon QName
x = do
  [QName]
ys <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (AllowAmbiguousNames -> QName -> ScopeInfo -> [QName]
inverseScopeLookupName' AllowAmbiguousNames
ambCon QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ScopeInfo
currentScope)
  forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"scope.inverse" VerboseLevel
100 forall a b. (a -> b) -> a -> b
$
    RawName
"inverse looking up abstract name " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> RawName
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ RawName
" yields " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> RawName
prettyShow [QName]
ys
  [QName] -> AbsToCon QName
loop [QName]
ys

  where
    -- Found concrete name: check that it is not shadowed by a local
    loop :: [QName] -> AbsToCon QName
loop (qy :: QName
qy@Qual{}      : [QName]
_ ) = forall (m :: * -> *) a. Monad m => a -> m a
return QName
qy -- local names cannot be qualified
    loop (qy :: QName
qy@(C.QName Name
y) : [QName]
ys) = Name -> AbsToCon (Maybe Name)
lookupNameInScope Name
y forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just Name
x' | Name
x' forall a. Eq a => a -> a -> Bool
/= QName -> Name
qnameName QName
x -> [QName] -> AbsToCon QName
loop [QName]
ys
      Maybe Name
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
qy
    -- Found no concrete name: make up a new one
    loop [] = case QName -> QName
qnameToConcrete QName
x of
      qy :: QName
qy@Qual{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensInScope a => a -> a
setNotInScope QName
qy
      qy :: QName
qy@C.QName{} -> Name -> QName
C.QName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> AbsToCon Name
chooseName (QName -> Name
qnameName QName
x)

lookupModule :: A.ModuleName -> AbsToCon C.QName
lookupModule :: ModuleName -> AbsToCon QName
lookupModule (A.MName []) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ RawName -> Name
C.simpleName RawName
"-1"
  -- Andreas, 2016-10-10 it can happen that we have an empty module name
  -- for instance when we query the current module inside the
  -- frontmatter or module telescope of the top level module.
  -- In this case, we print it as an invalid module name.
  -- (Should only affect debug printing.)
lookupModule ModuleName
x =
    do  ScopeInfo
scope <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> ScopeInfo
currentScope
        case ModuleName -> ScopeInfo -> [QName]
inverseScopeLookupModule ModuleName
x ScopeInfo
scope of
            (QName
y : [QName]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
y
            []      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
mnameToConcrete ModuleName
x
                -- this is what happens for names that are not in scope (private names)

-- | Is this concrete name currently in use by a particular abstract
--   name in the current scope?
lookupNameInScope :: C.Name -> AbsToCon (Maybe A.Name)
lookupNameInScope :: Name -> AbsToCon (Maybe Name)
lookupNameInScope Name
y =
  forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocalVar -> Name
localVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
y) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((forall o i. o -> Lens' i o -> i
^. Lens' [(Name, LocalVar)] ScopeInfo
scopeLocals) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ScopeInfo
currentScope))

-- | Have we already committed to a specific concrete name for this
--   abstract name? If yes, return the concrete name(s).
hasConcreteNames :: (MonadStConcreteNames m) => A.Name -> m [C.Name]
hasConcreteNames :: forall (m :: * -> *). MonadStConcreteNames m => Name -> m [Name]
hasConcreteNames Name
x = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadStConcreteNames m => m ConcreteNames
useConcreteNames

-- | Commit to a specific concrete name for printing the given
--   abstract name. If the abstract name already has associated
---  concrete name(s), the new name is only used when all previous
---  names are shadowed. Precondition: the abstract name should be in
--   scope.
pickConcreteName :: (MonadStConcreteNames m) => A.Name -> C.Name -> m ()
pickConcreteName :: forall (m :: * -> *).
MonadStConcreteNames m =>
Name -> Name -> m ()
pickConcreteName Name
x Name
y = forall (m :: * -> *).
MonadStConcreteNames m =>
(ConcreteNames -> ConcreteNames) -> m ()
modifyConcreteNames forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter Name
x forall a b. (a -> b) -> a -> b
$ \case
    Maybe [Name]
Nothing   -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Name
y]
    (Just [Name]
ys) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Name]
ys forall a. [a] -> [a] -> [a]
++ [Name
y]

-- | For the given abstract name, return the names that could shadow it.
shadowingNames :: (ReadTCState m, MonadStConcreteNames m)
               => A.Name -> m (Set RawName)
shadowingNames :: forall (m :: * -> *).
(ReadTCState m, MonadStConcreteNames m) =>
Name -> m (Set RawName)
shadowingNames Name
x =
  forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. Monoid a => a
mempty Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' (Map Name (DList RawName)) TCState
stShadowingNames

toConcreteName :: A.Name -> AbsToCon C.Name
toConcreteName :: Name -> AbsToCon Name
toConcreteName Name
x | Name
y <- Name -> Name
nameConcrete Name
x , forall a. IsNoName a => a -> Bool
isNoName Name
y = forall (m :: * -> *) a. Monad m => a -> m a
return Name
y
toConcreteName Name
x = (forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Name
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadStConcreteNames m => m ConcreteNames
useConcreteNames) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Name] -> AbsToCon Name
loop
  where
    -- case: we already have picked some name(s) for x
    loop :: [Name] -> AbsToCon Name
loop (Name
y:[Name]
ys) = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Name -> Name -> AbsToCon Bool
isGoodName Name
x Name
y) (forall (m :: * -> *) a. Monad m => a -> m a
return Name
y) ([Name] -> AbsToCon Name
loop [Name]
ys)

    -- case: we haven't picked a concrete name yet, or all previously
    -- picked names are shadowed, so we pick a new name now
    loop [] = do
      Name
y <- Name -> AbsToCon Name
chooseName Name
x
      forall (m :: * -> *).
MonadStConcreteNames m =>
Name -> Name -> m ()
pickConcreteName Name
x Name
y
      forall (m :: * -> *) a. Monad m => a -> m a
return Name
y

    -- Is 'y' a good concrete name for abstract name 'x'?
    isGoodName :: A.Name -> C.Name -> AbsToCon Bool
    isGoodName :: Name -> Name -> AbsToCon Bool
isGoodName Name
x Name
y = do
      [Name]
zs <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Set Name
takenVarNames)
      forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM [Name]
zs forall a b. (a -> b) -> a -> b
$ \Name
z -> if Name
x forall a. Eq a => a -> a -> Bool
== Name
z then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else do
        [Name]
czs <- forall (m :: * -> *). MonadStConcreteNames m => Name -> m [Name]
hasConcreteNames Name
z
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Name
y [Name]
czs


-- | Choose a new unshadowed name for the given abstract name
-- | NOTE: See @withName@ in @Agda.Syntax.Translation.ReflectedToAbstract@ for similar logic.
-- | NOTE: See @freshConcreteName@ in @Agda.Syntax.Scope.Monad@ also for similar logic.
chooseName :: A.Name -> AbsToCon C.Name
chooseName :: Name -> AbsToCon Name
chooseName Name
x = Name -> AbsToCon (Maybe Name)
lookupNameInScope (Name -> Name
nameConcrete Name
x) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  -- If the name is currently in scope, we do not rename it
  Just Name
x' | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' -> do
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.bindName" VerboseLevel
80 forall a b. (a -> b) -> a -> b
$
      RawName
"name " forall a. [a] -> [a] -> [a]
++ Name -> RawName
C.nameToRawName (Name -> Name
nameConcrete Name
x) forall a. [a] -> [a] -> [a]
++ RawName
" already in scope, so not renaming"
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x
  -- Otherwise we pick a name that does not shadow other names
  Maybe Name
_ -> do
    Set NameParts
takenDefs <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Set NameParts
takenDefNames
    Set RawName
taken   <- AbsToCon (Set RawName)
takenNames
    Set RawName
toAvoid <- forall (m :: * -> *).
(ReadTCState m, MonadStConcreteNames m) =>
Name -> m (Set RawName)
shadowingNames Name
x
    UnicodeOrAscii
glyphMode <- PragmaOptions -> UnicodeOrAscii
optUseUnicode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    let freshNameMode :: FreshNameMode
freshNameMode = case UnicodeOrAscii
glyphMode of
          UnicodeOrAscii
UnicodeOk -> FreshNameMode
A.UnicodeSubscript
          UnicodeOrAscii
AsciiOnly -> FreshNameMode
A.AsciiCounter

        shouldAvoid :: Name -> Bool
shouldAvoid C.NoName {} = Bool
False
        shouldAvoid name :: Name
name@C.Name { NameParts
nameNameParts :: NameParts
nameNameParts :: Name -> NameParts
nameNameParts } =
          let raw :: RawName
raw = Name -> RawName
C.nameToRawName Name
name in
          NameParts
nameNameParts forall a. Ord a => a -> Set a -> Bool
`Set.member` Set NameParts
takenDefs Bool -> Bool -> Bool
||
          RawName
raw forall a. Ord a => a -> Set a -> Bool
`Set.member` Set RawName
taken Bool -> Bool -> Bool
||
          RawName
raw forall a. Ord a => a -> Set a -> Bool
`Set.member` Set RawName
toAvoid

        y :: Name
y = FreshNameMode -> (Name -> Bool) -> Name -> Name
firstNonTakenName FreshNameMode
freshNameMode Name -> Bool
shouldAvoid forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.bindName" VerboseLevel
80 forall a b. (a -> b) -> a -> b
$ Doc -> RawName
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"picking concrete name for:" Doc -> Doc -> Doc
<+> RawName -> Doc
text (Name -> RawName
C.nameToRawName forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete Name
x)
      , Doc
"names already taken:      " Doc -> Doc -> Doc
<+> forall a. Pretty a => [a] -> Doc
prettyList_ (forall a. Set a -> [a]
Set.toList Set RawName
taken)
      , Doc
"names to avoid:           " Doc -> Doc -> Doc
<+> forall a. Pretty a => [a] -> Doc
prettyList_ (forall a. Set a -> [a]
Set.toList Set RawName
toAvoid)
      , Doc
"concrete name chosen:     " Doc -> Doc -> Doc
<+> RawName -> Doc
text (Name -> RawName
C.nameToRawName Name
y)
      ]
    forall (m :: * -> *) a. Monad m => a -> m a
return Name
y

  where
    takenNames :: AbsToCon (Set RawName)
    takenNames :: AbsToCon (Set RawName)
takenNames = do
      Set Name
ys0 <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Set Name
takenVarNames
      forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.bindName" VerboseLevel
90 forall a b. (a -> b) -> a -> b
$ Doc -> RawName
render forall a b. (a -> b) -> a -> b
$ Doc
"abstract names of local vars: " Doc -> Doc -> Doc
<+> forall a. Pretty a => [a] -> Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map (Name -> RawName
C.nameToRawName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nameConcrete) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Name
ys0)
      Set Name
ys <- forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadStConcreteNames m => Name -> m [Name]
hasConcreteNames (forall a. Set a -> [a]
Set.toList Set Name
ys0)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Name -> RawName
C.nameToRawName Set Name
ys


-- | Add a abstract name to the scope and produce an available concrete version of it.
bindName :: A.Name -> (C.Name -> AbsToCon a) -> AbsToCon a
bindName :: forall a. Name -> (Name -> AbsToCon a) -> AbsToCon a
bindName Name
x Name -> AbsToCon a
ret = do
  Name
y <- Name -> AbsToCon Name
toConcreteName Name
x
  forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.bindName" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ RawName
"adding " forall a. [a] -> [a] -> [a]
++ Name -> RawName
C.nameToRawName (Name -> Name
nameConcrete Name
x) forall a. [a] -> [a] -> [a]
++ RawName
" to the scope under concrete name " forall a. [a] -> [a] -> [a]
++ Name -> RawName
C.nameToRawName Name
y
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Name -> Name -> Env -> Env
addBinding Name
y Name
x) forall a b. (a -> b) -> a -> b
$ Name -> AbsToCon a
ret Name
y

-- | Like 'bindName', but do not care whether name is already taken.
bindName' :: A.Name -> AbsToCon a -> AbsToCon a
bindName' :: forall a. Name -> AbsToCon a -> AbsToCon a
bindName' Name
x AbsToCon a
ret = do
  forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.bindName" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ RawName
"adding " forall a. [a] -> [a] -> [a]
++ Name -> RawName
C.nameToRawName (Name -> Name
nameConcrete Name
x) forall a. [a] -> [a] -> [a]
++ RawName
" to the scope with forced name"
  forall (m :: * -> *).
MonadStConcreteNames m =>
Name -> Name -> m ()
pickConcreteName Name
x Name
y
  forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. IsNoName a => a -> Bool
isNoName Name
y) (forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall a b. (a -> b) -> a -> b
$ Name -> Name -> Env -> Env
addBinding Name
y Name
x) AbsToCon a
ret
  where y :: Name
y = Name -> Name
nameConcrete Name
x

-- Dealing with precedences -----------------------------------------------

-- | General bracketing function.
bracket' ::    (e -> e)             -- ^ the bracketing function
            -> (PrecedenceStack -> Bool) -- ^ Should we bracket things
                                    --   which have the given
                                    --   precedence?
            -> e -> AbsToCon e
bracket' :: forall e. (e -> e) -> (PrecedenceStack -> Bool) -> e -> AbsToCon e
bracket' e -> e
paren PrecedenceStack -> Bool
needParen e
e =
    do  PrecedenceStack
p <- AbsToCon PrecedenceStack
currentPrecedence
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if PrecedenceStack -> Bool
needParen PrecedenceStack
p then e -> e
paren e
e else e
e

-- | Expression bracketing
bracket :: (PrecedenceStack -> Bool) -> AbsToCon C.Expr -> AbsToCon C.Expr
bracket :: (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
par AbsToCon Expr
m =
    do  Expr
e <- AbsToCon Expr
m
        forall e. (e -> e) -> (PrecedenceStack -> Bool) -> e -> AbsToCon e
bracket' (Range -> Expr -> Expr
Paren (forall a. HasRange a => a -> Range
getRange Expr
e)) PrecedenceStack -> Bool
par Expr
e

-- | Pattern bracketing
bracketP_ :: (PrecedenceStack -> Bool) -> AbsToCon C.Pattern -> AbsToCon C.Pattern
bracketP_ :: (PrecedenceStack -> Bool) -> AbsToCon Pattern -> AbsToCon Pattern
bracketP_ PrecedenceStack -> Bool
par AbsToCon Pattern
m =
    do  Pattern
e <- AbsToCon Pattern
m
        forall e. (e -> e) -> (PrecedenceStack -> Bool) -> e -> AbsToCon e
bracket' (Range -> Pattern -> Pattern
ParenP (forall a. HasRange a => a -> Range
getRange Pattern
e)) PrecedenceStack -> Bool
par Pattern
e

{- UNUSED
-- | Pattern bracketing
bracketP :: (PrecedenceStack -> Bool) -> (C.Pattern -> AbsToCon a)
                                 -> ((C.Pattern -> AbsToCon a) -> AbsToCon a)
                                 -> AbsToCon a
bracketP par ret m = m $ \p -> do
    p <- bracket' (ParenP $ getRange p) par p
    ret p
-}

-- | Applications where the argument is a lambda without parentheses need
--   parens more often than other applications.
isLambda :: NamedArg A.Expr -> Bool
isLambda :: NamedArg Expr -> Bool
isLambda NamedArg Expr
e | forall a. LensHiding a => a -> Bool
notVisible NamedArg Expr
e = Bool
False
isLambda NamedArg Expr
e =
  case Expr -> Expr
unScope forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Expr
e of
    A.Lam{}         -> Bool
True
    A.AbsurdLam{}   -> Bool
True
    A.ExtendedLam{} -> Bool
True
    Expr
_               -> Bool
False

-- Dealing with infix declarations ----------------------------------------

-- | If a name is defined with a fixity that differs from the default, we have
--   to generate a fixity declaration for that name.
withInfixDecl :: DefInfo -> C.Name -> AbsToCon [C.Declaration] -> AbsToCon [C.Declaration]
withInfixDecl :: DefInfo -> Name -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withInfixDecl DefInfo
i Name
x AbsToCon [Declaration]
m = (([Declaration]
fixDecl forall a. [a] -> [a] -> [a]
++ [Declaration]
synDecl) forall a. [a] -> [a] -> [a]
++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsToCon [Declaration]
m
  where
  fixDecl :: [Declaration]
fixDecl = [ Fixity -> List1 Name -> Declaration
C.Infix (Fixity' -> Fixity
theFixity forall a b. (a -> b) -> a -> b
$ forall t. DefInfo' t -> Fixity'
defFixity DefInfo
i) forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton Name
x
            | Fixity' -> Fixity
theFixity (forall t. DefInfo' t -> Fixity'
defFixity DefInfo
i) forall a. Eq a => a -> a -> Bool
/= Fixity
noFixity
            ]
  synDecl :: [Declaration]
synDecl = [ Name -> Notation -> Declaration
C.Syntax Name
x forall a b. (a -> b) -> a -> b
$ Fixity' -> Notation
theNotation forall a b. (a -> b) -> a -> b
$ forall t. DefInfo' t -> Fixity'
defFixity DefInfo
i ]

-- Dealing with private definitions ---------------------------------------

-- | Add @abstract@, @private@, @instance@ modifiers.
withAbstractPrivate :: DefInfo -> AbsToCon [C.Declaration] -> AbsToCon [C.Declaration]
withAbstractPrivate :: DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i AbsToCon [Declaration]
m =
    Access -> [Declaration] -> [Declaration]
priv (forall t. DefInfo' t -> Access
defAccess DefInfo
i)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> [Declaration] -> [Declaration]
abst (forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
i)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Range -> [Declaration] -> [Declaration]
addInstanceB (case forall t. DefInfo' t -> IsInstance
A.defInstance DefInfo
i of InstanceDef Range
r -> forall a. a -> Maybe a
Just Range
r; IsInstance
NotInstanceDef -> forall a. Maybe a
Nothing)
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsToCon [Declaration]
m
    where
        priv :: Access -> [Declaration] -> [Declaration]
priv (PrivateAccess Origin
UserWritten)
                         [Declaration]
ds = [ Range -> Origin -> [Declaration] -> Declaration
C.Private  (forall a. HasRange a => a -> Range
getRange [Declaration]
ds) Origin
UserWritten [Declaration]
ds ]
        priv Access
_           [Declaration]
ds = [Declaration]
ds
        abst :: IsAbstract -> [Declaration] -> [Declaration]
abst IsAbstract
AbstractDef [Declaration]
ds = [ Range -> [Declaration] -> Declaration
C.Abstract (forall a. HasRange a => a -> Range
getRange [Declaration]
ds) [Declaration]
ds ]
        abst IsAbstract
ConcreteDef [Declaration]
ds = [Declaration]
ds

addInstanceB :: Maybe Range -> [C.Declaration] -> [C.Declaration]
addInstanceB :: Maybe Range -> [Declaration] -> [Declaration]
addInstanceB (Just Range
r) [Declaration]
ds = [ Range -> [Declaration] -> Declaration
C.InstanceB Range
r [Declaration]
ds ]
addInstanceB Maybe Range
Nothing  [Declaration]
ds = [Declaration]
ds

-- The To Concrete Class --------------------------------------------------

class ToConcrete a where
    type ConOfAbs a
    toConcrete :: a -> AbsToCon (ConOfAbs a)
    bindToConcrete :: a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b

    -- Christian Sattler, 2017-08-05:
    -- These default implementations are not valid semantically (at least
    -- the second one). Perhaps they (it) should be removed.
    toConcrete     a
x     = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
x forall (m :: * -> *) a. Monad m => a -> m a
return
    bindToConcrete a
x ConOfAbs a -> AbsToCon b
ret = ConOfAbs a -> AbsToCon b
ret forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
x

-- | Translate something in a context of the given precedence.
toConcreteCtx :: ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx :: forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
p a
x = forall a. Precedence -> AbsToCon a -> AbsToCon a
withPrecedence Precedence
p forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
x

-- | Translate something in a context of the given precedence.
bindToConcreteCtx :: ToConcrete a => Precedence -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteCtx :: forall a b.
ToConcrete a =>
Precedence -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteCtx Precedence
p a
x ConOfAbs a -> AbsToCon b
ret = forall a. Precedence -> AbsToCon a -> AbsToCon a
withPrecedence Precedence
p forall a b. (a -> b) -> a -> b
$ forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
x ConOfAbs a -> AbsToCon b
ret

-- | Translate something in the top context.
toConcreteTop :: ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop :: forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop = forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx

-- | Translate something in the top context.
bindToConcreteTop :: ToConcrete a => a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteTop :: forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteTop = forall a b.
ToConcrete a =>
Precedence -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteCtx Precedence
TopCtx

-- | Translate something in a context indicated by 'Hiding' info.
toConcreteHiding :: (LensHiding h, ToConcrete a) => h -> a -> AbsToCon (ConOfAbs a)
toConcreteHiding :: forall h a.
(LensHiding h, ToConcrete a) =>
h -> a -> AbsToCon (ConOfAbs a)
toConcreteHiding h
h =
  case forall a. LensHiding a => a -> Hiding
getHiding h
h of
    Hiding
NotHidden  -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete
    Hiding
Hidden     -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop
    Instance{} -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop

-- | Translate something in a context indicated by 'Hiding' info.
bindToConcreteHiding :: (LensHiding h, ToConcrete a) => h -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteHiding :: forall h a b.
(LensHiding h, ToConcrete a) =>
h -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteHiding h
h =
  case forall a. LensHiding a => a -> Hiding
getHiding h
h of
    Hiding
NotHidden  -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete
    Hiding
Hidden     -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteTop
    Instance{} -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteTop

-- General instances ------------------------------------------------------

instance ToConcrete () where
  type ConOfAbs () = ()
  toConcrete :: () -> AbsToCon (ConOfAbs ())
toConcrete = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance ToConcrete Bool where
  type ConOfAbs Bool = Bool
  toConcrete :: Bool -> AbsToCon (ConOfAbs Bool)
toConcrete = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance ToConcrete a => ToConcrete [a] where
    type ConOfAbs [a] = [ConOfAbs a]

    toConcrete :: [a] -> AbsToCon (ConOfAbs [a])
toConcrete     = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete
    bindToConcrete :: forall b. [a] -> (ConOfAbs [a] -> AbsToCon b) -> AbsToCon b
bindToConcrete []     ConOfAbs [a] -> AbsToCon b
ret = ConOfAbs [a] -> AbsToCon b
ret []
    bindToConcrete (a
a:[a]
as) ConOfAbs [a] -> AbsToCon b
ret = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (a
aforall a. a -> [a] -> NonEmpty a
:|[a]
as) forall a b. (a -> b) -> a -> b
$ \ (ConOfAbs a
c:|[ConOfAbs a]
cs) -> ConOfAbs [a] -> AbsToCon b
ret (ConOfAbs a
cforall a. a -> [a] -> [a]
:[ConOfAbs a]
cs)

instance ToConcrete a => ToConcrete (List1 a) where
    type ConOfAbs (List1 a) = List1 (ConOfAbs a)

    toConcrete :: List1 a -> AbsToCon (ConOfAbs (List1 a))
toConcrete     = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete
    -- Andreas, 2017-04-11, Issue #2543
    -- The naive `thread'ing does not work as we have to undo
    -- changes to the Precedence.
    -- bindToConcrete = thread bindToConcrete
    bindToConcrete :: forall b.
List1 a -> (ConOfAbs (List1 a) -> AbsToCon b) -> AbsToCon b
bindToConcrete (a
a :| [a]
as) ConOfAbs (List1 a) -> AbsToCon b
ret = do
      PrecedenceStack
p <- AbsToCon PrecedenceStack
currentPrecedence  -- save precedence
      forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
a forall a b. (a -> b) -> a -> b
$ \ ConOfAbs a
c ->
        forall a. PrecedenceStack -> AbsToCon a -> AbsToCon a
withPrecedence' PrecedenceStack
p forall a b. (a -> b) -> a -> b
$ -- reset precedence
          forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete [a]
as forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [a]
cs ->
            ConOfAbs (List1 a) -> AbsToCon b
ret (ConOfAbs a
c forall a. a -> [a] -> NonEmpty a
:| ConOfAbs [a]
cs)

instance (ToConcrete a1, ToConcrete a2) => ToConcrete (Either a1 a2) where
    type ConOfAbs (Either a1 a2) = Either (ConOfAbs a1) (ConOfAbs a2)

    toConcrete :: Either a1 a2 -> AbsToCon (ConOfAbs (Either a1 a2))
toConcrete = forall (f :: * -> *) a c b d.
Functor f =>
(a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
traverseEither forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete
    bindToConcrete :: forall b.
Either a1 a2
-> (ConOfAbs (Either a1 a2) -> AbsToCon b) -> AbsToCon b
bindToConcrete (Left a1
x) ConOfAbs (Either a1 a2) -> AbsToCon b
ret =
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a1
x forall a b. (a -> b) -> a -> b
$ \ConOfAbs a1
x ->
        ConOfAbs (Either a1 a2) -> AbsToCon b
ret (forall a b. a -> Either a b
Left ConOfAbs a1
x)
    bindToConcrete (Right a2
y) ConOfAbs (Either a1 a2) -> AbsToCon b
ret =
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a2
y forall a b. (a -> b) -> a -> b
$ \ConOfAbs a2
y ->
        ConOfAbs (Either a1 a2) -> AbsToCon b
ret (forall a b. b -> Either a b
Right ConOfAbs a2
y)

instance (ToConcrete a1, ToConcrete a2) => ToConcrete (a1, a2) where
    type ConOfAbs (a1, a2) = (ConOfAbs a1, ConOfAbs a2)

    toConcrete :: (a1, a2) -> AbsToCon (ConOfAbs (a1, a2))
toConcrete (a1
x,a2
y) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a1
x) (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a2
y)
    bindToConcrete :: forall b.
(a1, a2) -> (ConOfAbs (a1, a2) -> AbsToCon b) -> AbsToCon b
bindToConcrete (a1
x,a2
y) ConOfAbs (a1, a2) -> AbsToCon b
ret =
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a1
x forall a b. (a -> b) -> a -> b
$ \ConOfAbs a1
x ->
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a2
y forall a b. (a -> b) -> a -> b
$ \ConOfAbs a2
y ->
        ConOfAbs (a1, a2) -> AbsToCon b
ret (ConOfAbs a1
x,ConOfAbs a2
y)

instance (ToConcrete a1, ToConcrete a2, ToConcrete a3) => ToConcrete (a1,a2,a3) where
    type ConOfAbs (a1, a2, a3) = (ConOfAbs a1, ConOfAbs a2, ConOfAbs a3)

    toConcrete :: (a1, a2, a3) -> AbsToCon (ConOfAbs (a1, a2, a3))
toConcrete (a1
x,a2
y,a3
z) = forall {a} {b} {c}. (a, (b, c)) -> (a, b, c)
reorder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (a1
x,(a2
y,a3
z))
        where
            reorder :: (a, (b, c)) -> (a, b, c)
reorder (a
x,(b
y,c
z)) = (a
x,b
y,c
z)

    bindToConcrete :: forall b.
(a1, a2, a3) -> (ConOfAbs (a1, a2, a3) -> AbsToCon b) -> AbsToCon b
bindToConcrete (a1
x,a2
y,a3
z) ConOfAbs (a1, a2, a3) -> AbsToCon b
ret = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (a1
x,(a2
y,a3
z)) forall a b. (a -> b) -> a -> b
$ ConOfAbs (a1, a2, a3) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {b} {c}. (a, (b, c)) -> (a, b, c)
reorder
        where
            reorder :: (a, (b, c)) -> (a, b, c)
reorder (a
x,(b
y,c
z)) = (a
x,b
y,c
z)

instance ToConcrete a => ToConcrete (Arg a) where
    type ConOfAbs (Arg a) = Arg (ConOfAbs a)

    toConcrete :: Arg a -> AbsToCon (ConOfAbs (Arg a))
toConcrete (Arg ArgInfo
i a
a) = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall h a.
(LensHiding h, ToConcrete a) =>
h -> a -> AbsToCon (ConOfAbs a)
toConcreteHiding ArgInfo
i a
a

    bindToConcrete :: forall b. Arg a -> (ConOfAbs (Arg a) -> AbsToCon b) -> AbsToCon b
bindToConcrete (Arg ArgInfo
info a
x) ConOfAbs (Arg a) -> AbsToCon b
ret =
      forall h a b.
(LensHiding h, ToConcrete a) =>
h -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteHiding ArgInfo
info a
x forall a b. (a -> b) -> a -> b
$ ConOfAbs (Arg a) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info

instance ToConcrete a => ToConcrete (WithHiding a) where
  type ConOfAbs (WithHiding a) = WithHiding (ConOfAbs a)

  toConcrete :: WithHiding a -> AbsToCon (ConOfAbs (WithHiding a))
toConcrete     (WithHiding Hiding
h a
a) = forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
h forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall h a.
(LensHiding h, ToConcrete a) =>
h -> a -> AbsToCon (ConOfAbs a)
toConcreteHiding Hiding
h a
a
  bindToConcrete :: forall b.
WithHiding a
-> (ConOfAbs (WithHiding a) -> AbsToCon b) -> AbsToCon b
bindToConcrete (WithHiding Hiding
h a
a) ConOfAbs (WithHiding a) -> AbsToCon b
ret = forall h a b.
(LensHiding h, ToConcrete a) =>
h -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteHiding Hiding
h a
a forall a b. (a -> b) -> a -> b
$ \ ConOfAbs a
a ->
    ConOfAbs (WithHiding a) -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
h ConOfAbs a
a

instance ToConcrete a => ToConcrete (Named name a)  where
    type ConOfAbs (Named name a) = Named name (ConOfAbs a)

    toConcrete :: Named name a -> AbsToCon (ConOfAbs (Named name a))
toConcrete (Named Maybe name
n a
x) = forall name a. Maybe name -> a -> Named name a
Named Maybe name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
x
    bindToConcrete :: forall b.
Named name a
-> (ConOfAbs (Named name a) -> AbsToCon b) -> AbsToCon b
bindToConcrete (Named Maybe name
n a
x) ConOfAbs (Named name a) -> AbsToCon b
ret = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
x forall a b. (a -> b) -> a -> b
$ ConOfAbs (Named name a) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Maybe name -> a -> Named name a
Named Maybe name
n

-- Names ------------------------------------------------------------------

instance ToConcrete A.Name where
  type ConOfAbs A.Name = C.Name

  toConcrete :: Name -> AbsToCon (ConOfAbs Name)
toConcrete       = Name -> AbsToCon Name
toConcreteName
  bindToConcrete :: forall b. Name -> (ConOfAbs Name -> AbsToCon b) -> AbsToCon b
bindToConcrete Name
x = forall a. Name -> (Name -> AbsToCon a) -> AbsToCon a
bindName Name
x

instance ToConcrete BindName where
  type ConOfAbs BindName = C.BoundName

  toConcrete :: BindName -> AbsToCon (ConOfAbs BindName)
toConcrete       = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BoundName
C.mkBoundName_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> AbsToCon Name
toConcreteName forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindName -> Name
unBind
  bindToConcrete :: forall b.
BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b
bindToConcrete BindName
x = forall a. Name -> (Name -> AbsToCon a) -> AbsToCon a
bindName (BindName -> Name
unBind BindName
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BoundName
C.mkBoundName_)

instance ToConcrete A.QName where
  type ConOfAbs A.QName = C.QName

  toConcrete :: QName -> AbsToCon (ConOfAbs QName)
toConcrete = AllowAmbiguousNames -> QName -> AbsToCon QName
lookupQName AllowAmbiguousNames
AmbiguousConProjs

instance ToConcrete A.ModuleName where
  type ConOfAbs A.ModuleName = C.QName
  toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName)
toConcrete = ModuleName -> AbsToCon QName
lookupModule

instance ToConcrete AbstractName where
  type ConOfAbs AbstractName = C.QName
  toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName)
toConcrete = forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName

-- | Assumes name is not 'UnknownName'.
instance ToConcrete ResolvedName where
  type ConOfAbs ResolvedName = C.QName

  toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName)
toConcrete = \case
    VarName Name
x BindingSource
_          -> Name -> QName
C.QName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Name
x
    DefinedName Access
_ AbstractName
x Suffix
s    -> forall (m :: * -> *). HasOptions m => Suffix -> m QName -> m QName
addSuffixConcrete Suffix
s forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete AbstractName
x
    FieldName List1 AbstractName
xs         -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall a. NonEmpty a -> a
List1.head List1 AbstractName
xs)
    ConstructorName Set Induction
_ List1 AbstractName
xs -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall a. NonEmpty a -> a
List1.head List1 AbstractName
xs)
    PatternSynResName List1 AbstractName
xs -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall a. NonEmpty a -> a
List1.head List1 AbstractName
xs)
    ResolvedName
UnknownName          -> forall a. HasCallStack => a
__IMPOSSIBLE__

addSuffixConcrete :: HasOptions m => A.Suffix -> m C.QName -> m C.QName
addSuffixConcrete :: forall (m :: * -> *). HasOptions m => Suffix -> m QName -> m QName
addSuffixConcrete Suffix
A.NoSuffix m QName
x = m QName
x
addSuffixConcrete (A.Suffix Integer
i) m QName
x = do
  UnicodeOrAscii
glyphMode <- PragmaOptions -> UnicodeOrAscii
optUseUnicode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  UnicodeOrAscii -> Integer -> QName -> QName
addSuffixConcrete' UnicodeOrAscii
glyphMode Integer
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m QName
x

addSuffixConcrete' :: UnicodeOrAscii -> Integer -> C.QName -> C.QName
addSuffixConcrete' :: UnicodeOrAscii -> Integer -> QName -> QName
addSuffixConcrete' UnicodeOrAscii
glyphMode Integer
i = forall i o. Lens' i o -> LensSet i o
set (Lens' Name QName
C.lensQNameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' (Maybe Suffix) Name
nameSuffix) Maybe Suffix
suffix
  where
    suffix :: Maybe Suffix
suffix = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ case UnicodeOrAscii
glyphMode of
      UnicodeOrAscii
UnicodeOk -> Integer -> Suffix
Subscript forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
i
      UnicodeOrAscii
AsciiOnly -> Integer -> Suffix
Index forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
i

-- Expression instance ----------------------------------------------------

instance ToConcrete A.Expr where
    type ConOfAbs A.Expr = C.Expr

    toConcrete :: Expr -> AbsToCon (ConOfAbs Expr)
toConcrete (Var Name
x)             = QName -> Expr
Ident forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
C.QName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Name
x
    toConcrete (Def' QName
x Suffix
suffix)     = QName -> Expr
Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => Suffix -> m QName -> m QName
addSuffixConcrete Suffix
suffix (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x)
    toConcrete (Proj ProjOrigin
ProjPrefix AmbiguousQName
p) = QName -> Expr
Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (AmbiguousQName -> QName
headAmbQ AmbiguousQName
p)
    toConcrete (Proj ProjOrigin
_          AmbiguousQName
p) = Range -> Expr -> Expr
C.Dot forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Expr
Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (AmbiguousQName -> QName
headAmbQ AmbiguousQName
p)
    toConcrete (A.Macro QName
x)         = QName -> Expr
Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    toConcrete e :: Expr
e@(Con AmbiguousQName
c)           = Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverPatternSyn Expr
e forall a b. (a -> b) -> a -> b
$ QName -> Expr
Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (AmbiguousQName -> QName
headAmbQ AmbiguousQName
c)
        -- for names we have to use the name from the info, since the abstract
        -- name has been resolved to a fully qualified name (except for
        -- variables)
    toConcrete e :: Expr
e@(A.Lit ExprInfo
i (LitQName QName
x)) = Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverPatternSyn Expr
e forall a b. (a -> b) -> a -> b
$ do
      QName
x <- AllowAmbiguousNames -> QName -> AbsToCon QName
lookupQName AllowAmbiguousNames
AmbiguousNothing QName
x
      let r :: Range
r = forall a. HasRange a => a -> Range
getRange ExprInfo
i
      (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
appBrackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        Range -> Expr -> NamedArg Expr -> Expr
C.App Range
r (Range -> Expr
C.Quote Range
r) (forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ QName -> Expr
C.Ident QName
x)
    toConcrete e :: Expr
e@(A.Lit ExprInfo
i Literal
l) = Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverPatternSyn Expr
e forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Literal -> Expr
C.Lit (forall a. HasRange a => a -> Range
getRange ExprInfo
i) Literal
l

    -- Andreas, 2014-05-17  We print question marks with their
    -- interaction id, in case @metaNumber /= Nothing@
    -- Ulf, 2017-09-20  ... or @preserveIIds == True@.
    toConcrete (A.QuestionMark MetaInfo
i InteractionId
ii) = do
      Bool
preserve <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Bool
preserveIIds
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Maybe VerboseLevel -> Expr
C.QuestionMark (forall a. HasRange a => a -> Range
getRange MetaInfo
i) forall a b. (a -> b) -> a -> b
$
                 InteractionId -> VerboseLevel
interactionId InteractionId
ii forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
preserve Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust (MetaInfo -> Maybe MetaId
metaNumber MetaInfo
i))

    toConcrete (A.Underscore MetaInfo
i) =
      Range -> Maybe RawName -> Expr
C.Underscore (forall a. HasRange a => a -> Range
getRange MetaInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Doc -> RawName
render forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM)
        (RawName -> MetaId -> NamedMeta
NamedMeta (MetaInfo -> RawName
metaNameSuggestion MetaInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaInfo -> Maybe MetaId
metaNumber MetaInfo
i)

    toConcrete (A.Dot ExprInfo
i Expr
e) =
      Range -> Expr -> Expr
C.Dot (forall a. HasRange a => a -> Range
getRange ExprInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e

    toConcrete e :: Expr
e@(A.App AppInfo
i Expr
e1 NamedArg Expr
e2) = do
      QName -> RawName -> Bool
is <- AbsToCon (QName -> RawName -> Bool)
isBuiltinFun
      -- Special printing of desugared overloaded literals:
      --  fromNat 4        --> 4
      --  fromNeg 4        --> -4
      --  fromString "foo" --> "foo"
      -- Only when the corresponding conversion function is in scope and was
      -- inserted by the system.
      case (Expr -> Maybe Hd
getHead Expr
e1, forall a. NamedArg a -> a
namedArg NamedArg Expr
e2) of
        (Just (HdDef QName
q), l :: Expr
l@A.Lit{})
          | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (QName -> RawName -> Bool
is QName
q) [RawName
builtinFromNat, RawName
builtinFromString], forall a. LensHiding a => a -> Bool
visible NamedArg Expr
e2,
            forall a. LensOrigin a => a -> Origin
getOrigin AppInfo
i forall a. Eq a => a -> a -> Bool
== Origin
Inserted -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
l
        (Just (HdDef QName
q), A.Lit ExprInfo
r (LitNat Integer
n))
          | QName
q QName -> RawName -> Bool
`is` RawName
builtinFromNeg, forall a. LensHiding a => a -> Bool
visible NamedArg Expr
e2,
            forall a. LensOrigin a => a -> Origin
getOrigin AppInfo
i forall a. Eq a => a -> a -> Bool
== Origin
Inserted -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (ExprInfo -> Literal -> Expr
A.Lit ExprInfo
r (Integer -> Literal
LitNat (-Integer
n)))
        (Maybe Hd, Expr)
_ ->
          Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverPatternSyn Expr
e
          forall a b. (a -> b) -> a -> b
$ Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverOpApp Expr
e
          forall a b. (a -> b) -> a -> b
$ Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverNatural Expr
e
          -- or fallback to App
          forall a b. (a -> b) -> a -> b
$ (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket (Bool -> PrecedenceStack -> Bool
appBrackets' forall a b. (a -> b) -> a -> b
$ ParenPreference -> Bool
preferParenless (AppInfo -> ParenPreference
appParens AppInfo
i) Bool -> Bool -> Bool
&& NamedArg Expr -> Bool
isLambda NamedArg Expr
e2)
          forall a b. (a -> b) -> a -> b
$ do Expr
e1' <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
FunctionCtx Expr
e1
               NamedArg Expr
e2' <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx (ParenPreference -> Precedence
ArgumentCtx forall a b. (a -> b) -> a -> b
$ AppInfo -> ParenPreference
appParens AppInfo
i) NamedArg Expr
e2
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Expr -> NamedArg Expr -> Expr
C.App (forall a. HasRange a => a -> Range
getRange AppInfo
i) Expr
e1' NamedArg Expr
e2'

    toConcrete (A.WithApp ExprInfo
i Expr
e [Expr]
es) =
      (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
withAppBrackets forall a b. (a -> b) -> a -> b
$ do
        Expr
e <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
WithFunCtx Expr
e
        [Expr]
es <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
WithArgCtx) [Expr]
es
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Expr -> [Expr] -> Expr
C.WithApp (forall a. HasRange a => a -> Range
getRange ExprInfo
i) Expr
e [Expr]
es

    toConcrete (A.AbsurdLam ExprInfo
i Hiding
h) =
      (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
lamBrackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Hiding -> Expr
C.AbsurdLam (forall a. HasRange a => a -> Range
getRange ExprInfo
i) Hiding
h
    toConcrete e :: Expr
e@(A.Lam ExprInfo
i LamBinding
_ Expr
_) =
      Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverOpApp Expr
e forall a b. (a -> b) -> a -> b
$   -- recover sections
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> LamBinding
makeDomainFree [LamBinding]
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [LamBinding]
bs' -> do
          forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull (forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [LamBinding]
bs')
            {-then-} (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e')
            {-else-} forall a b. (a -> b) -> a -> b
$ \ List1 LamBinding
bs -> (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
lamBrackets forall a b. (a -> b) -> a -> b
$
              Range -> List1 LamBinding -> Expr -> Expr
C.Lam (forall a. HasRange a => a -> Range
getRange ExprInfo
i) List1 LamBinding
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
e'
      where
          ([LamBinding]
bs, Expr
e') = Expr -> ([LamBinding], Expr)
lamView Expr
e
          -- #3238 GA: We drop the hidden lambda abstractions which have
          -- been inserted by the machine rather than the user. This means
          -- that the result of lamView may actually be an empty list of
          -- binders.
          lamView :: A.Expr -> ([A.LamBinding], A.Expr)
          lamView :: Expr -> ([LamBinding], Expr)
lamView (A.Lam ExprInfo
_ b :: LamBinding
b@(A.DomainFree TacticAttr
_ NamedArg Binder
x) Expr
e)
            | forall a. (LensHiding a, LensOrigin a) => a -> Bool
isInsertedHidden NamedArg Binder
x = Expr -> ([LamBinding], Expr)
lamView Expr
e
            | Bool
otherwise = case Expr -> ([LamBinding], Expr)
lamView Expr
e of
              (bs :: [LamBinding]
bs@(A.DomainFree{} : [LamBinding]
_), Expr
e) -> (LamBinding
bforall a. a -> [a] -> [a]
:[LamBinding]
bs, Expr
e)
              ([LamBinding], Expr)
_                            -> ([LamBinding
b] , Expr
e)
          lamView (A.Lam ExprInfo
_ b :: LamBinding
b@(A.DomainFull A.TLet{}) Expr
e) = case Expr -> ([LamBinding], Expr)
lamView Expr
e of
            (bs :: [LamBinding]
bs@(A.DomainFull TypedBinding
_ : [LamBinding]
_), Expr
e) -> (LamBinding
bforall a. a -> [a] -> [a]
:[LamBinding]
bs, Expr
e)
            ([LamBinding], Expr)
_                            -> ([LamBinding
b], Expr
e)
          lamView (A.Lam ExprInfo
_ (A.DomainFull (A.TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
ty)) Expr
e) =
            case forall a. (a -> Bool) -> NonEmpty a -> [a]
List1.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (LensHiding a, LensOrigin a) => a -> Bool
isInsertedHidden) List1 (NamedArg Binder)
xs of
              []    -> Expr -> ([LamBinding], Expr)
lamView Expr
e
              NamedArg Binder
x:[NamedArg Binder]
xs' -> let b :: LamBinding
b = TypedBinding -> LamBinding
A.DomainFull (Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
A.TBind Range
r TypedBindingInfo
t (NamedArg Binder
x forall a. a -> [a] -> NonEmpty a
:| [NamedArg Binder]
xs') Expr
ty) in
                case Expr -> ([LamBinding], Expr)
lamView Expr
e of
                  (bs :: [LamBinding]
bs@(A.DomainFull TypedBinding
_ : [LamBinding]
_), Expr
e) -> (LamBinding
bforall a. a -> [a] -> [a]
:[LamBinding]
bs, Expr
e)
                  ([LamBinding], Expr)
_                            -> ([LamBinding
b], Expr
e)
          lamView Expr
e = ([], Expr
e)
    toConcrete (A.ExtendedLam ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs) =
        (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
lamBrackets forall a b. (a -> b) -> a -> b
$ do
          [Declaration]
decls <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete List1 Clause
cs
          let namedPat :: Arg (Named_ Pattern) -> Pattern
namedPat Arg (Named_ Pattern)
np = case forall a. LensHiding a => a -> Hiding
getHiding Arg (Named_ Pattern)
np of
                 Hiding
NotHidden  -> forall a. NamedArg a -> a
namedArg Arg (Named_ Pattern)
np
                 Hiding
Hidden     -> Range -> Named_ Pattern -> Pattern
C.HiddenP forall a. Range' a
noRange (forall e. Arg e -> e
unArg Arg (Named_ Pattern)
np)
                 Instance{} -> Range -> Named_ Pattern -> Pattern
C.InstanceP forall a. Range' a
noRange (forall e. Arg e -> e
unArg Arg (Named_ Pattern)
np)
              -- we know all lhs are of the form `.extlam p1 p2 ... pn`,
              -- with the name .extlam leftmost. It is our mission to remove it.
          let removeApp :: C.Pattern -> AbsToCon [C.Pattern]
              removeApp :: Pattern -> AbsToCon [Pattern]
removeApp (C.RawAppP Range
_ (List2 Pattern
_ Pattern
p [Pattern]
ps)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pattern
pforall a. a -> [a] -> [a]
:[Pattern]
ps
              removeApp (C.AppP (C.IdentP QName
_) Arg (Named_ Pattern)
np) = forall (m :: * -> *) a. Monad m => a -> m a
return [Arg (Named_ Pattern) -> Pattern
namedPat Arg (Named_ Pattern)
np]
              removeApp (C.AppP Pattern
p Arg (Named_ Pattern)
np)            = Pattern -> AbsToCon [Pattern]
removeApp Pattern
p forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Pattern) -> Pattern
namedPat Arg (Named_ Pattern)
np])
              -- Andreas, 2018-06-18, issue #3136
              -- Empty pattern list also allowed in extended lambda,
              -- thus, we might face the unapplied .extendedlambda identifier.
              removeApp x :: Pattern
x@C.IdentP{} = forall (m :: * -> *) a. Monad m => a -> m a
return []

              removeApp Pattern
p = do
                forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"extendedlambda" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ RawName
"abstractToConcrete removeApp p = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Pattern
p
                forall (m :: * -> *) a. Monad m => a -> m a
return [Pattern
p] -- __IMPOSSIBLE__
                  -- Andreas, this is actually not impossible,
                  -- my strictification exposed this sleeping bug
          let decl2clause :: Declaration -> AbsToCon LamClause
decl2clause (C.FunClause (C.LHS Pattern
p [] []) RHS
rhs WhereClause' [Declaration]
C.NoWhere Bool
ca) = do
                forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"extendedlambda" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ RawName
"abstractToConcrete extended lambda pattern p = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Pattern
p
                [Pattern]
ps <- Pattern -> AbsToCon [Pattern]
removeApp Pattern
p
                forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"extendedlambda" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ RawName
"abstractToConcrete extended lambda patterns ps = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> RawName
prettyShow [Pattern]
ps
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Pattern] -> RHS -> Bool -> LamClause
LamClause [Pattern]
ps RHS
rhs Bool
ca
              decl2clause Declaration
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
          Range -> Erased -> List1 LamClause -> Expr
C.ExtendedLam (forall a. HasRange a => a -> Range
getRange ExprInfo
i) Erased
erased forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. List1 a -> [a] -> List1 a
List1.fromListSafe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Declaration -> AbsToCon LamClause
decl2clause [Declaration]
decls
            -- TODO List1: can we demonstrate non-emptiness?

    toConcrete (A.Pi ExprInfo
_ NonEmpty TypedBinding
tel1 Expr
e0) = do
      let (NonEmpty TypedBinding
tel, Expr
e) = NonEmpty TypedBinding -> Expr -> (NonEmpty TypedBinding, Expr)
piTel1 NonEmpty TypedBinding
tel1 Expr
e0
      (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
piBrackets forall a b. (a -> b) -> a -> b
$
         forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete NonEmpty TypedBinding
tel forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (NonEmpty TypedBinding)
tel' ->
           Telescope -> Expr -> Expr
C.makePi (forall a. List1 (Maybe a) -> [a]
List1.catMaybes ConOfAbs (NonEmpty TypedBinding)
tel') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
e
      where
        piTel1 :: NonEmpty TypedBinding -> Expr -> (NonEmpty TypedBinding, Expr)
piTel1 NonEmpty TypedBinding
tel Expr
e         = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a. List1 a -> [a] -> List1 a
List1.appendList NonEmpty TypedBinding
tel) forall a b. (a -> b) -> a -> b
$ Expr -> ([TypedBinding], Expr)
piTel Expr
e
        piTel :: Expr -> ([TypedBinding], Expr)
piTel (A.Pi ExprInfo
_ NonEmpty TypedBinding
tel Expr
e) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ NonEmpty TypedBinding -> Expr -> (NonEmpty TypedBinding, Expr)
piTel1 NonEmpty TypedBinding
tel Expr
e
        piTel Expr
e              = ([], Expr
e)

    toConcrete (A.Generalized Set QName
_ Expr
e) = Expr -> Expr
C.Generalized forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e

    toConcrete (A.Fun ExprInfo
i Arg Expr
a Expr
b) =
        (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
piBrackets
        forall a b. (a -> b) -> a -> b
$ do Arg Expr
a' <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
ctx Arg Expr
a
             Expr
b' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
b
             let dom :: Arg Expr
dom = forall a. LensQuantity a => Quantity -> a -> a
setQuantity (forall a. LensQuantity a => a -> Quantity
getQuantity Arg Expr
a') forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall {a}. (LensRelevance a, HasRange a) => a -> Expr -> Expr
addRel Arg Expr
a' forall a b. (a -> b) -> a -> b
$ Arg Expr -> Expr
mkArg Arg Expr
a'
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Arg Expr -> Expr -> Expr
C.Fun (forall a. HasRange a => a -> Range
getRange ExprInfo
i) Arg Expr
dom Expr
b'
             -- Andreas, 2018-06-14, issue #2513
             -- TODO: print attributes
        where
            ctx :: Precedence
ctx = if forall a. LensRelevance a => a -> Bool
isRelevant Arg Expr
a then Precedence
FunctionSpaceDomainCtx else Precedence
DotPatternCtx
            addRel :: a -> Expr -> Expr
addRel a
a Expr
e = case forall a. LensRelevance a => a -> Relevance
getRelevance a
a of
                           Relevance
Irrelevant -> Range -> Expr -> Expr
C.Dot (forall a. HasRange a => a -> Range
getRange a
a) Expr
e
                           Relevance
NonStrict  -> Range -> Expr -> Expr
C.DoubleDot (forall a. HasRange a => a -> Range
getRange a
a) Expr
e
                           Relevance
_          -> Expr
e
            mkArg :: Arg Expr -> Expr
mkArg (Arg ArgInfo
info Expr
e) = case forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info of
                                          Hiding
Hidden     -> Range -> Named_ Expr -> Expr
HiddenArg   (forall a. HasRange a => a -> Range
getRange Expr
e) (forall a name. a -> Named name a
unnamed Expr
e)
                                          Instance{} -> Range -> Named_ Expr -> Expr
InstanceArg (forall a. HasRange a => a -> Range
getRange Expr
e) (forall a name. a -> Named name a
unnamed Expr
e)
                                          Hiding
NotHidden  -> Expr
e

    toConcrete (A.Let ExprInfo
i List1 LetBinding
ds Expr
e) =
        (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
lamBrackets
        forall a b. (a -> b) -> a -> b
$ forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete List1 LetBinding
ds forall a b. (a -> b) -> a -> b
$ \ConOfAbs (List1 LetBinding)
ds' -> do
             Expr
e'  <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
e
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> [Declaration] -> Expr -> Expr
C.mkLet (forall a. HasRange a => a -> Range
getRange ExprInfo
i) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ConOfAbs (List1 LetBinding)
ds') Expr
e'

    toConcrete (A.Rec ExprInfo
i RecordAssigns
fs) =
      (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
appBrackets forall a b. (a -> b) -> a -> b
$ do
        Range -> RecordAssignments -> Expr
C.Rec (forall a. HasRange a => a -> Range
getRange ExprInfo
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\QName
x -> QName -> [Expr] -> ImportDirective -> ModuleAssignment
ModuleAssignment QName
x [] forall n m. ImportDirective' n m
defaultImportDir)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop RecordAssigns
fs

    toConcrete (A.RecUpdate ExprInfo
i Expr
e Assigns
fs) =
      (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket PrecedenceStack -> Bool
appBrackets forall a b. (a -> b) -> a -> b
$ do
        Range -> Expr -> [FieldAssignment] -> Expr
C.RecUpdate (forall a. HasRange a => a -> Range
getRange ExprInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Assigns
fs

    toConcrete (A.ScopedExpr ScopeInfo
_ Expr
e) = forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e
    toConcrete (A.Quote ExprInfo
i) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Expr
C.Quote (forall a. HasRange a => a -> Range
getRange ExprInfo
i)
    toConcrete (A.QuoteTerm ExprInfo
i) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Expr
C.QuoteTerm (forall a. HasRange a => a -> Range
getRange ExprInfo
i)
    toConcrete (A.Unquote ExprInfo
i) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Expr
C.Unquote (forall a. HasRange a => a -> Range
getRange ExprInfo
i)

    -- Andreas, 2012-04-02: TODO!  print DontCare as irrAxiom
    -- Andreas, 2010-10-05 print irrelevant things as ordinary things
    toConcrete (A.DontCare Expr
e) = Range -> Expr -> Expr
C.Dot Range
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Expr -> Expr
C.Paren Range
r  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e
       where r :: Range
r = forall a. HasRange a => a -> Range
getRange Expr
e
    toConcrete (A.PatternSyn AmbiguousQName
n) = QName -> Expr
C.Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (AmbiguousQName -> QName
headAmbQ AmbiguousQName
n)

makeDomainFree :: A.LamBinding -> A.LamBinding
makeDomainFree :: LamBinding -> LamBinding
makeDomainFree b :: LamBinding
b@(A.DomainFull (A.TBind Range
_ TypedBindingInfo
tac (NamedArg Binder
x :| []) Expr
t)) =
  case Expr -> Expr
unScope Expr
t of
    A.Underscore A.MetaInfo{metaNumber :: MetaInfo -> Maybe MetaId
metaNumber = Maybe MetaId
Nothing} ->
      TacticAttr -> NamedArg Binder -> LamBinding
A.DomainFree (TypedBindingInfo -> TacticAttr
tbTacticAttr TypedBindingInfo
tac) NamedArg Binder
x
    Expr
_ -> LamBinding
b
makeDomainFree LamBinding
b = LamBinding
b

-- Christian Sattler, 2017-08-05, fixing #2669
-- Both methods of ToConcrete (FieldAssignment' a) (FieldAssignment' c) need
-- to be implemented, each in terms of the corresponding one of ToConcrete a c.
-- This mirrors the instance ToConcrete (Arg a) (Arg c).
-- The default implementations of ToConcrete are not valid semantically.
instance ToConcrete a => ToConcrete (FieldAssignment' a) where
    type ConOfAbs (FieldAssignment' a) = FieldAssignment' (ConOfAbs a)
    toConcrete :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a))
toConcrete = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete

    bindToConcrete :: forall b.
FieldAssignment' a
-> (ConOfAbs (FieldAssignment' a) -> AbsToCon b) -> AbsToCon b
bindToConcrete (FieldAssignment Name
name a
a) ConOfAbs (FieldAssignment' a) -> AbsToCon b
ret =
      forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
a forall a b. (a -> b) -> a -> b
$ ConOfAbs (FieldAssignment' a) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
name


-- Binder instances -------------------------------------------------------

-- If there is no label we set it to the bound name, to make renaming the bound
-- name safe.
forceNameIfHidden :: NamedArg A.Binder -> NamedArg A.Binder
forceNameIfHidden :: NamedArg Binder -> NamedArg Binder
forceNameIfHidden NamedArg Binder
x
  | forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf  NamedArg Binder
x = NamedArg Binder
x
  | forall a. LensHiding a => a -> Bool
visible NamedArg Binder
x             = NamedArg Binder
x
  | Bool
otherwise             = forall a. LensNamed a => Maybe (NameOf a) -> a -> a
setNameOf (forall a. a -> Maybe a
Just NamedName
name) NamedArg Binder
x
  where
    name :: NamedName
name = forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted
         forall a b. (a -> b) -> a -> b
$ forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange NamedArg Binder
x)
         forall a b. (a -> b) -> a -> b
$ Name -> RawName
C.nameToRawName forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete
         forall a b. (a -> b) -> a -> b
$ BindName -> Name
unBind forall a b. (a -> b) -> a -> b
$ forall a. Binder' a -> a
A.binderName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
x

instance ToConcrete a => ToConcrete (A.Binder' a) where
  type ConOfAbs (A.Binder' a) = C.Binder' (ConOfAbs a)

  bindToConcrete :: forall b.
Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b
bindToConcrete (A.Binder Maybe Pattern
p a
a) ConOfAbs (Binder' a) -> AbsToCon b
ret =
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
a forall a b. (a -> b) -> a -> b
$ \ ConOfAbs a
a ->
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete Maybe Pattern
p forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (Maybe Pattern)
p ->
    ConOfAbs (Binder' a) -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ forall a. Maybe Pattern -> a -> Binder' a
C.Binder ConOfAbs (Maybe Pattern)
p ConOfAbs a
a

instance ToConcrete A.LamBinding where
    type ConOfAbs A.LamBinding = Maybe C.LamBinding

    bindToConcrete :: forall b.
LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b
bindToConcrete (A.DomainFree TacticAttr
t NamedArg Binder
x) ConOfAbs LamBinding -> AbsToCon b
ret = do
      Maybe Expr
t <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete TacticAttr
t
      let setTac :: BoundName -> BoundName
setTac BoundName
x = BoundName
x { bnameTactic :: Maybe Expr
bnameTactic = Maybe Expr
t }
      forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (NamedArg Binder -> NamedArg Binder
forceNameIfHidden NamedArg Binder
x) forall a b. (a -> b) -> a -> b
$
        ConOfAbs LamBinding -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg (Binder' BoundName) -> LamBinding' a
C.DomainFree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BoundName -> BoundName
setTac)
    bindToConcrete (A.DomainFull TypedBinding
b) ConOfAbs LamBinding -> AbsToCon b
ret = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete TypedBinding
b forall a b. (a -> b) -> a -> b
$ ConOfAbs LamBinding -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> LamBinding' a
C.DomainFull

instance ToConcrete A.TypedBinding where
    type ConOfAbs A.TypedBinding = Maybe C.TypedBinding

    bindToConcrete :: forall b.
TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b
bindToConcrete (A.TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e) ConOfAbs TypedBinding -> AbsToCon b
ret = do
        Maybe Expr
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (TypedBindingInfo -> TacticAttr
tbTacticAttr TypedBindingInfo
t)
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Binder -> NamedArg Binder
forceNameIfHidden List1 (NamedArg Binder)
xs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (List1 (NamedArg Binder))
xs -> do
          Expr
e <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
e
          let setTac :: BoundName -> BoundName
setTac BoundName
x = BoundName
x { bnameTactic :: Maybe Expr
bnameTactic = Maybe Expr
tac , bnameIsFinite :: Bool
C.bnameIsFinite = TypedBindingInfo -> Bool
tbFinite TypedBindingInfo
t }
          ConOfAbs TypedBinding -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e.
Range
-> List1 (NamedArg (Binder' BoundName)) -> e -> TypedBinding' e
C.TBind Range
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BoundName -> BoundName
setTac)) ConOfAbs (List1 (NamedArg Binder))
xs) Expr
e
    bindToConcrete (A.TLet Range
r List1 LetBinding
lbs) ConOfAbs TypedBinding -> AbsToCon b
ret =
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete List1 LetBinding
lbs forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (List1 LetBinding)
ds -> do
        ConOfAbs TypedBinding -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ forall e. Range -> [Declaration] -> Maybe (TypedBinding' e)
C.mkTLet Range
r forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ConOfAbs (List1 LetBinding)
ds

instance ToConcrete A.LetBinding where
    type ConOfAbs A.LetBinding = [C.Declaration]

    bindToConcrete :: forall b.
LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b
bindToConcrete (A.LetBind LetInfo
i ArgInfo
info BindName
x Expr
t Expr
e) ConOfAbs LetBinding -> AbsToCon b
ret =
        forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete BindName
x forall a b. (a -> b) -> a -> b
$ \ ConOfAbs BindName
x ->
        do (Expr
t, (RHS
e, [], [], [])) <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (Expr
t, Expr -> Maybe Expr -> RHS
A.RHS Expr
e forall a. Maybe a
Nothing)
           ConOfAbs LetBinding -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ Maybe Range -> [Declaration] -> [Declaration]
addInstanceB (if forall a. LensHiding a => a -> Bool
isInstance ArgInfo
info then forall a. a -> Maybe a
Just forall a. Range' a
noRange else forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
               [ ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
C.TypeSig ArgInfo
info forall a. Maybe a
Nothing (BoundName -> Name
C.boundName ConOfAbs BindName
x) Expr
t
               , LHS -> RHS -> WhereClause' [Declaration] -> Bool -> Declaration
C.FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
C.LHS (QName -> Pattern
C.IdentP forall a b. (a -> b) -> a -> b
$ Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ BoundName -> Name
C.boundName ConOfAbs BindName
x) [] [])
                             RHS
e forall decls. WhereClause' decls
C.NoWhere Bool
False
               ]
    -- TODO: bind variables
    bindToConcrete (LetPatBind LetInfo
i Pattern
p Expr
e) ConOfAbs LetBinding -> AbsToCon b
ret = do
        Pattern
p <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Pattern
p
        Expr
e <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e
        ConOfAbs LetBinding -> AbsToCon b
ret [ LHS -> RHS -> WhereClause' [Declaration] -> Bool -> Declaration
C.FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
C.LHS Pattern
p [] []) (forall e. e -> RHS' e
C.RHS Expr
e) forall decls. WhereClause' decls
NoWhere Bool
False ]
    bindToConcrete (LetApply ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
_ ImportDirective
_) ConOfAbs LetBinding -> AbsToCon b
ret = do
      Name
x' <- QName -> Name
unqualify forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
x
      ModuleApplication
modapp <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleApplication
modapp
      let r :: Range
r = forall a. HasRange a => a -> Range
getRange ModuleApplication
modapp
          open :: OpenShortHand
open = forall a. a -> Maybe a -> a
fromMaybe OpenShortHand
DontOpen forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe OpenShortHand
minfoOpenShort ModuleInfo
i
          dir :: ImportDirective
dir  = forall a. a -> Maybe a -> a
fromMaybe forall n m. ImportDirective' n m
defaultImportDir{ importDirRange :: Range
importDirRange = Range
r } forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe ImportDirective
minfoDirective ModuleInfo
i
      -- This is no use since toAbstract LetDefs is in localToAbstract.
      forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ModuleName -> ImportDirective -> (Scope -> Scope) -> Env -> Env
openModule' ModuleName
x ImportDirective
dir forall a. a -> a
id) forall a b. (a -> b) -> a -> b
$
        ConOfAbs LetBinding -> AbsToCon b
ret [ Range
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
C.ModuleMacro (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) Name
x' ModuleApplication
modapp OpenShortHand
open ImportDirective
dir ]
    bindToConcrete (LetOpen ModuleInfo
i ModuleName
x ImportDirective
_) ConOfAbs LetBinding -> AbsToCon b
ret = do
      QName
x' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
x
      let dir :: ImportDirective
dir = forall a. a -> Maybe a -> a
fromMaybe forall n m. ImportDirective' n m
defaultImportDir forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe ImportDirective
minfoDirective ModuleInfo
i
      forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ModuleName -> ImportDirective -> (Scope -> Scope) -> Env -> Env
openModule' ModuleName
x ImportDirective
dir Scope -> Scope
restrictPrivate) forall a b. (a -> b) -> a -> b
$
            ConOfAbs LetBinding -> AbsToCon b
ret [ Range -> QName -> ImportDirective -> Declaration
C.Open (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) QName
x' ImportDirective
dir ]
    bindToConcrete (LetDeclaredVariable BindName
_) ConOfAbs LetBinding -> AbsToCon b
ret =
      -- Note that the range of the declaration site is dropped.
      ConOfAbs LetBinding -> AbsToCon b
ret []

instance ToConcrete A.WhereDeclarations where
  type ConOfAbs A.WhereDeclarations = WhereClause

  bindToConcrete :: forall b.
WhereDeclarations
-> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b
bindToConcrete (A.WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
Nothing) ConOfAbs WhereDeclarations -> AbsToCon b
ret = ConOfAbs WhereDeclarations -> AbsToCon b
ret forall decls. WhereClause' decls
C.NoWhere
  bindToConcrete (A.WhereDecls (Just ModuleName
am) Bool
False (Just (A.Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds))) ConOfAbs WhereDeclarations -> AbsToCon b
ret = do
    [Declaration]
ds' <- [Declaration] -> AbsToCon [Declaration]
declsToConcrete [Declaration]
ds
    Name
cm  <- QName -> Name
unqualify forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> AbsToCon QName
lookupModule ModuleName
am
    -- Andreas, 2016-07-08 I put PublicAccess in the following SomeWhere
    -- Should not really matter for printing...
    let wh' :: WhereClause' [Declaration]
wh' = (if forall a. IsNoName a => a -> Bool
isNoName Name
cm then forall decls. Range -> decls -> WhereClause' decls
AnyWhere forall a. Range' a
noRange else forall decls.
Range -> Name -> Access -> decls -> WhereClause' decls
SomeWhere forall a. Range' a
noRange Name
cm Access
PublicAccess) forall a b. (a -> b) -> a -> b
$ [Declaration]
ds'
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ModuleName -> ImportDirective -> (Scope -> Scope) -> Env -> Env
openModule' ModuleName
am forall n m. ImportDirective' n m
defaultImportDir forall a. a -> a
id) forall a b. (a -> b) -> a -> b
$ ConOfAbs WhereDeclarations -> AbsToCon b
ret WhereClause' [Declaration]
wh'
  bindToConcrete (A.WhereDecls Maybe ModuleName
_ Bool
_ (Just Declaration
d)) ConOfAbs WhereDeclarations -> AbsToCon b
ret =
    ConOfAbs WhereDeclarations -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall decls. Range -> decls -> WhereClause' decls
AnyWhere forall a. Range' a
noRange forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Declaration
d

mergeSigAndDef :: [C.Declaration] -> [C.Declaration]
mergeSigAndDef :: [Declaration] -> [Declaration]
mergeSigAndDef (C.RecordSig Range
_ Name
x [LamBinding]
bs Expr
e : C.RecordDef Range
r Name
y RecordDirectives
dir [LamBinding]
_ [Declaration]
fs : [Declaration]
ds)
  | Name
x forall a. Eq a => a -> a -> Bool
== Name
y = Range
-> Name
-> RecordDirectives
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
C.Record Range
r Name
y RecordDirectives
dir [LamBinding]
bs Expr
e [Declaration]
fs forall a. a -> [a] -> [a]
: [Declaration] -> [Declaration]
mergeSigAndDef [Declaration]
ds
mergeSigAndDef (C.DataSig Range
_ Name
x [LamBinding]
bs Expr
e : C.DataDef Range
r Name
y [LamBinding]
_ [Declaration]
cs : [Declaration]
ds)
  | Name
x forall a. Eq a => a -> a -> Bool
== Name
y = Range
-> Name -> [LamBinding] -> Expr -> [Declaration] -> Declaration
C.Data Range
r Name
y [LamBinding]
bs Expr
e [Declaration]
cs forall a. a -> [a] -> [a]
: [Declaration] -> [Declaration]
mergeSigAndDef [Declaration]
ds
mergeSigAndDef (Declaration
d : [Declaration]
ds) = Declaration
d forall a. a -> [a] -> [a]
: [Declaration] -> [Declaration]
mergeSigAndDef [Declaration]
ds
mergeSigAndDef [] = []

openModule' :: A.ModuleName -> C.ImportDirective -> (Scope -> Scope) -> Env -> Env
openModule' :: ModuleName -> ImportDirective -> (Scope -> Scope) -> Env -> Env
openModule' ModuleName
x ImportDirective
dir Scope -> Scope
restrict Env
env = Env
env{currentScope :: ScopeInfo
currentScope = forall i o. Lens' i o -> LensSet i o
set Lens' (Map ModuleName Scope) ScopeInfo
scopeModules Map ModuleName Scope
mods' ScopeInfo
sInfo}
  where sInfo :: ScopeInfo
sInfo = Env -> ScopeInfo
currentScope Env
env
        amod :: ModuleName
amod  = ScopeInfo
sInfo forall o i. o -> Lens' i o -> i
^. Lens' ModuleName ScopeInfo
scopeCurrent
        mods :: Map ModuleName Scope
mods  = ScopeInfo
sInfo forall o i. o -> Lens' i o -> i
^. Lens' (Map ModuleName Scope) ScopeInfo
scopeModules
        news :: Scope
news  = NameSpaceId -> Scope -> Scope
setScopeAccess NameSpaceId
PrivateNS
                forall a b. (a -> b) -> a -> b
$ ImportDirective -> Scope -> Scope
applyImportDirective ImportDirective
dir
                forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe Scope
emptyScope Scope -> Scope
restrict
                forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
x Map ModuleName Scope
mods
        mods' :: Map ModuleName Scope
mods' = forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Scope -> Scope -> Scope
`mergeScope` Scope
news)) ModuleName
amod Map ModuleName Scope
mods


-- Declaration instances --------------------------------------------------

declsToConcrete :: [A.Declaration] -> AbsToCon [C.Declaration]
declsToConcrete :: [Declaration] -> AbsToCon [Declaration]
declsToConcrete [Declaration]
ds = [Declaration] -> [Declaration]
mergeSigAndDef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [Declaration]
ds

instance ToConcrete A.RHS where
    type ConOfAbs A.RHS = (C.RHS, [C.RewriteEqn], [C.WithExpr], [C.Declaration])

    toConcrete :: RHS -> AbsToCon (ConOfAbs RHS)
toConcrete (A.RHS Expr
e (Just Expr
c)) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. e -> RHS' e
C.RHS Expr
c, [], [], [])
    toConcrete (A.RHS Expr
e Maybe Expr
Nothing) = do
      Expr
e <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. e -> RHS' e
C.RHS Expr
e, [], [], [])
    toConcrete RHS
A.AbsurdRHS = forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. RHS' e
C.AbsurdRHS, [], [], [])
    toConcrete (A.WithRHS QName
_ [WithExpr]
es [Clause]
cs) = do
      [WithExpr]
es <- do [Named BindName (Arg Expr)]
es <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [WithExpr]
es
               forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Named BindName (Arg Expr)]
es forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
n Arg Expr
e) -> do
                 Maybe BoundName
n <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Maybe BindName
n
                 forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named (BoundName -> Name
C.boundName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe BoundName
n) Arg Expr
e
      [Declaration]
cs <- forall a. AbsToCon a -> AbsToCon a
noTakenNames forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [Clause]
cs
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. RHS' e
C.AbsurdRHS, [], [WithExpr]
es, [Declaration]
cs)
    toConcrete (A.RewriteRHS [RewriteEqn]
xeqs [ProblemEq]
_spats RHS
rhs WhereDeclarations
wh) = do
      [Declaration]
wh <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall a b. (a -> b) -> a -> b
$ WhereDeclarations -> Maybe Declaration
A.whereDecls WhereDeclarations
wh
      (RHS
rhs, [RewriteEqn]
eqs', [WithExpr]
es, [Declaration]
whs) <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete RHS
rhs
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [RewriteEqn]
eqs') forall a. HasCallStack => a
__IMPOSSIBLE__
      [RewriteEqn]
eqs <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [RewriteEqn]
xeqs
      forall (m :: * -> *) a. Monad m => a -> m a
return (RHS
rhs, [RewriteEqn]
eqs, [WithExpr]
es, [Declaration]
wh forall a. [a] -> [a] -> [a]
++ [Declaration]
whs)

instance (ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn A.BindName p a) where
  type ConOfAbs (RewriteEqn' qn A.BindName p a) = (RewriteEqn' () C.Name (ConOfAbs p) (ConOfAbs a))

  toConcrete :: RewriteEqn' qn BindName p a
-> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a))
toConcrete = \case
    Rewrite List1 (qn, a)
es    -> forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ (qn
_, a
e) -> ((),a
e))) List1 (qn, a)
es
    Invert qn
qn List1 (Named BindName (p, a))
pes -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall qn nm p e.
qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
Invert ()) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 (Named BindName (p, a))
pes forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
n (p, a)
pe) -> do
      (ConOfAbs p, ConOfAbs a)
pe <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (p, a)
pe
      Maybe Name
n  <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Maybe BindName
n
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named Maybe Name
n (ConOfAbs p, ConOfAbs a)
pe

instance ToConcrete (Maybe A.BindName) where
  type ConOfAbs (Maybe A.BindName) = Maybe C.Name
  toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName))
toConcrete = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (BoundName -> Name
C.boundName forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete)

instance ToConcrete (Maybe A.QName) where
  type ConOfAbs (Maybe A.QName) = Maybe C.Name

  toConcrete :: Maybe QName -> AbsToCon (ConOfAbs (Maybe QName))
toConcrete = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName)

instance ToConcrete (Constr A.Constructor) where
  type ConOfAbs (Constr A.Constructor) = C.Declaration

  toConcrete :: Constr Declaration -> AbsToCon (ConOfAbs (Constr Declaration))
toConcrete (Constr (A.ScopedDecl ScopeInfo
scope [Declaration
d])) =
    forall a. ScopeInfo -> AbsToCon a -> AbsToCon a
withScope ScopeInfo
scope forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall a. a -> Constr a
Constr Declaration
d)
  toConcrete (Constr (A.Axiom KindOfName
_ DefInfo
i ArgInfo
info Maybe [Occurrence]
Nothing QName
x Expr
t)) = do
    Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    Expr
t' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
t
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
C.TypeSig ArgInfo
info forall a. Maybe a
Nothing Name
x' Expr
t'
  toConcrete (Constr (A.Axiom KindOfName
_ DefInfo
_ ArgInfo
_ (Just [Occurrence]
_) QName
_ Expr
_)) = forall a. HasCallStack => a
__IMPOSSIBLE__
  toConcrete (Constr Declaration
d) = forall a. [a] -> a
head forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Declaration
d

instance (ToConcrete a, ConOfAbs a ~ C.LHS) => ToConcrete (A.Clause' a) where
  type ConOfAbs (A.Clause' a) = [C.Declaration]

  toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a))
toConcrete (A.Clause a
lhs [ProblemEq]
_ RHS
rhs WhereDeclarations
wh Bool
catchall) =
      forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete a
lhs forall a b. (a -> b) -> a -> b
$ \case
          C.LHS Pattern
p [RewriteEqn]
_ [WithExpr]
_ -> do
            forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete WhereDeclarations
wh forall a b. (a -> b) -> a -> b
$ \ ConOfAbs WhereDeclarations
wh' -> do
                (RHS
rhs', [RewriteEqn]
eqs, [WithExpr]
with, [Declaration]
wcs) <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop RHS
rhs
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LHS -> RHS -> WhereClause' [Declaration] -> Bool -> Declaration
FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
C.LHS Pattern
p [RewriteEqn]
eqs [WithExpr]
with) RHS
rhs' ConOfAbs WhereDeclarations
wh' Bool
catchall forall a. a -> [a] -> [a]
: [Declaration]
wcs

instance ToConcrete A.ModuleApplication where
  type ConOfAbs A.ModuleApplication = C.ModuleApplication

  toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication)
toConcrete (A.SectionApp [TypedBinding]
tel ModuleName
y [NamedArg Expr]
es) = do
    QName
y  <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
FunctionCtx ModuleName
y
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete [TypedBinding]
tel forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [TypedBinding]
tel -> do
      [NamedArg Expr]
es <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
argumentCtx_ [NamedArg Expr]
es
      let r :: Range
r = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
y [NamedArg Expr]
es
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Telescope -> Expr -> ModuleApplication
C.SectionApp Range
r (forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [TypedBinding]
tel) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Range -> Expr -> NamedArg Expr -> Expr
C.App Range
r) (QName -> Expr
C.Ident QName
y) [NamedArg Expr]
es)

  toConcrete (A.RecordModuleInstance ModuleName
recm) = do
    QName
recm <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
recm
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QName -> ModuleApplication
C.RecordModuleInstance (forall a. HasRange a => a -> Range
getRange QName
recm) QName
recm

instance ToConcrete A.Declaration where
  type ConOfAbs A.Declaration = [C.Declaration]

  toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration)
toConcrete (ScopedDecl ScopeInfo
scope [Declaration]
ds) =
    forall a. ScopeInfo -> AbsToCon a -> AbsToCon a
withScope ScopeInfo
scope ([Declaration] -> AbsToCon [Declaration]
declsToConcrete [Declaration]
ds)

  toConcrete (A.Axiom KindOfName
_ DefInfo
i ArgInfo
info Maybe [Occurrence]
mp QName
x Expr
t) = do
    Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
      DefInfo -> Name -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withInfixDecl DefInfo
i Name
x'  forall a b. (a -> b) -> a -> b
$ do
      Expr
t' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
t
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        (case Maybe [Occurrence]
mp of
           Maybe [Occurrence]
Nothing   -> []
           Just [Occurrence]
occs -> [Pragma -> Declaration
C.Pragma (Range -> Name -> [Occurrence] -> Pragma
PolarityPragma forall a. Range' a
noRange Name
x' [Occurrence]
occs)]) forall a. [a] -> [a] -> [a]
++
        [Range -> [Declaration] -> Declaration
C.Postulate (forall a. HasRange a => a -> Range
getRange DefInfo
i) [ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
C.TypeSig ArgInfo
info forall a. Maybe a
Nothing Name
x' Expr
t']]

  toConcrete (A.Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Expr
t) = do
    Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    Maybe Expr
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall t. DefInfo' t -> Maybe t
defTactic DefInfo
i)
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
      DefInfo -> Name -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withInfixDecl DefInfo
i Name
x'  forall a b. (a -> b) -> a -> b
$ do
      Expr
t' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
t
      forall (m :: * -> *) a. Monad m => a -> m a
return [Range -> [Declaration] -> Declaration
C.Generalize (forall a. HasRange a => a -> Range
getRange DefInfo
i) [ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
C.TypeSig ArgInfo
j Maybe Expr
tac Name
x' forall a b. (a -> b) -> a -> b
$ Expr -> Expr
C.Generalized Expr
t']]

  toConcrete (A.Field DefInfo
i QName
x Arg Expr
t) = do
    Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    Maybe Expr
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall t. DefInfo' t -> Maybe t
defTactic DefInfo
i)
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
      DefInfo -> Name -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withInfixDecl DefInfo
i Name
x'  forall a b. (a -> b) -> a -> b
$ do
      Arg Expr
t' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Arg Expr
t
      forall (m :: * -> *) a. Monad m => a -> m a
return [IsInstance -> Maybe Expr -> Name -> Arg Expr -> Declaration
C.FieldSig (forall t. DefInfo' t -> IsInstance
A.defInstance DefInfo
i) Maybe Expr
tac Name
x' Arg Expr
t']

  toConcrete (A.Primitive DefInfo
i QName
x Arg Expr
t) = do
    Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
      DefInfo -> Name -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withInfixDecl DefInfo
i Name
x'  forall a b. (a -> b) -> a -> b
$ do
      Arg Expr
t' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Arg Expr
t
      forall (m :: * -> *) a. Monad m => a -> m a
return [Range -> [Declaration] -> Declaration
C.Primitive (forall a. HasRange a => a -> Range
getRange DefInfo
i) [ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
C.TypeSig (forall e. Arg e -> ArgInfo
argInfo Arg Expr
t') forall a. Maybe a
Nothing Name
x' (forall e. Arg e -> e
unArg Arg Expr
t')]]
        -- Primitives are always relevant.

  toConcrete (A.FunDef DefInfo
i QName
_ Delayed
_ [Clause]
cs) =
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [Clause]
cs

  toConcrete (A.DataSig DefInfo
i QName
x GeneralizeTelescope
bs Expr
t) =
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (GeneralizeTelescope -> [TypedBinding]
A.generalizeTel GeneralizeTelescope
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [TypedBinding]
tel' -> do
      Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
      Expr
t' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
t
      forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Name -> [LamBinding] -> Expr -> Declaration
C.DataSig (forall a. HasRange a => a -> Range
getRange DefInfo
i) Name
x' (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> LamBinding' a
C.DomainFull forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [TypedBinding]
tel') Expr
t' ]

  toConcrete (A.DataDef DefInfo
i QName
x UniverseCheck
uc DataDefParams
bs [Declaration]
cs) =
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> LamBinding
makeDomainFree forall a b. (a -> b) -> a -> b
$ DataDefParams -> [LamBinding]
dataDefParams DataDefParams
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [LamBinding]
tel' -> do
      (Name
x',[Declaration]
cs') <- forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (QName
x, forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Constr a
Constr [Declaration]
cs)
      forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
C.DataDef (forall a. HasRange a => a -> Range
getRange DefInfo
i) Name
x' (forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [LamBinding]
tel') [Declaration]
cs' ]

  toConcrete (A.RecSig DefInfo
i QName
x GeneralizeTelescope
bs Expr
t) =
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (GeneralizeTelescope -> [TypedBinding]
A.generalizeTel GeneralizeTelescope
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [TypedBinding]
tel' -> do
      Name
x' <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
      Expr
t' <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcreteTop Expr
t
      forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> Name -> [LamBinding] -> Expr -> Declaration
C.RecordSig (forall a. HasRange a => a -> Range
getRange DefInfo
i) Name
x' (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> LamBinding' a
C.DomainFull forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [TypedBinding]
tel') Expr
t' ]

  toConcrete (A.RecDef  DefInfo
i QName
x UniverseCheck
uc RecordDirectives
dir DataDefParams
bs Expr
t [Declaration]
cs) =
    DefInfo -> AbsToCon [Declaration] -> AbsToCon [Declaration]
withAbstractPrivate DefInfo
i forall a b. (a -> b) -> a -> b
$
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map LamBinding -> LamBinding
makeDomainFree forall a b. (a -> b) -> a -> b
$ DataDefParams -> [LamBinding]
dataDefParams DataDefParams
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [LamBinding]
tel' -> do
      (Name
x',[Declaration]
cs') <- forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (QName
x, forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Constr a
Constr [Declaration]
cs)
      forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Name
-> RecordDirectives
-> [LamBinding]
-> [Declaration]
-> Declaration
C.RecordDef (forall a. HasRange a => a -> Range
getRange DefInfo
i) Name
x' (RecordDirectives
dir { recConstructor :: Maybe (Name, IsInstance)
recConstructor = forall a. Maybe a
Nothing }) (forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [LamBinding]
tel') [Declaration]
cs' ]

  toConcrete (A.Mutual MutualInfo
i [Declaration]
ds) = [Declaration] -> AbsToCon [Declaration]
declsToConcrete [Declaration]
ds

  toConcrete (A.Section Range
i ModuleName
x (A.GeneralizeTel Map QName Name
_ [TypedBinding]
tel) [Declaration]
ds) = do
    QName
x <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
x
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete [TypedBinding]
tel forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [TypedBinding]
tel -> do
      [Declaration]
ds <- [Declaration] -> AbsToCon [Declaration]
declsToConcrete [Declaration]
ds
      forall (m :: * -> *) a. Monad m => a -> m a
return [ Range -> QName -> Telescope -> [Declaration] -> Declaration
C.Module (forall a. HasRange a => a -> Range
getRange Range
i) QName
x (forall a. [Maybe a] -> [a]
catMaybes ConOfAbs [TypedBinding]
tel) [Declaration]
ds ]

  toConcrete (A.Apply ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
_ ImportDirective
_) = do
    Name
x  <- QName -> Name
unsafeQNameToName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
x
    ModuleApplication
modapp <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleApplication
modapp
    let r :: Range
r = forall a. HasRange a => a -> Range
getRange ModuleApplication
modapp
        open :: OpenShortHand
open = forall a. a -> Maybe a -> a
fromMaybe OpenShortHand
DontOpen forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe OpenShortHand
minfoOpenShort ModuleInfo
i
        dir :: ImportDirective
dir  = forall a. a -> Maybe a -> a
fromMaybe forall n m. ImportDirective' n m
defaultImportDir{ importDirRange :: Range
importDirRange = Range
r } forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe ImportDirective
minfoDirective ModuleInfo
i
    forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
C.ModuleMacro (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) Name
x ModuleApplication
modapp OpenShortHand
open ImportDirective
dir ]

  toConcrete (A.Import ModuleInfo
i ModuleName
x ImportDirective
_) = do
    QName
x <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
x
    let open :: OpenShortHand
open = forall a. a -> Maybe a -> a
fromMaybe OpenShortHand
DontOpen forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe OpenShortHand
minfoOpenShort ModuleInfo
i
        dir :: ImportDirective
dir  = forall a. a -> Maybe a -> a
fromMaybe forall n m. ImportDirective' n m
defaultImportDir forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Maybe ImportDirective
minfoDirective ModuleInfo
i
    forall (m :: * -> *) a. Monad m => a -> m a
return [ Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> Declaration
C.Import (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) QName
x forall a. Maybe a
Nothing OpenShortHand
open ImportDirective
dir]

  toConcrete (A.Pragma Range
i Pragma
p)     = do
    Pragma
p <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall a b. (a -> b) -> a -> b
$ Range -> Pragma -> RangeAndPragma
RangeAndPragma (forall a. HasRange a => a -> Range
getRange Range
i) Pragma
p
    forall (m :: * -> *) a. Monad m => a -> m a
return [Pragma -> Declaration
C.Pragma Pragma
p]

  toConcrete (A.Open ModuleInfo
i ModuleName
x ImportDirective
_) = do
    QName
x <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ModuleName
x
    forall (m :: * -> *) a. Monad m => a -> m a
return [Range -> QName -> ImportDirective -> Declaration
C.Open (forall a. HasRange a => a -> Range
getRange ModuleInfo
i) QName
x forall n m. ImportDirective' n m
defaultImportDir]

  toConcrete (A.PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p) = do
    C.QName Name
x <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindName -> Name
A.unBind) [Arg BindName]
xs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs [Arg Name]
xs ->
      forall el coll. Singleton el coll => el -> coll
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Name -> [Arg Name] -> Pattern -> Declaration
C.PatternSyn (forall a. HasRange a => a -> Range
getRange Name
x) Name
x ConOfAbs [Arg Name]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        forall a. AbsToCon a -> AbsToCon a
dontFoldPatternSynonyms forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall (f :: * -> *) a. Functor f => f Void -> f a
vacuous Pattern' Void
p :: A.Pattern)

  toConcrete (A.UnquoteDecl MutualInfo
_ [DefInfo]
i [QName]
xs Expr
e) = do
    let unqual :: QName -> m Name
unqual (C.QName Name
x) = forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
        unqual QName
_           = forall a. HasCallStack => a
__IMPOSSIBLE__
    [Name]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *}. Monad m => QName -> m Name
unqual forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete) [QName]
xs
    (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> [Name] -> Expr -> Declaration
C.UnquoteDecl (forall a. HasRange a => a -> Range
getRange [DefInfo]
i) [Name]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e

  toConcrete (A.UnquoteDef [DefInfo]
i [QName]
xs Expr
e) = do
    let unqual :: QName -> m Name
unqual (C.QName Name
x) = forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
        unqual QName
_           = forall a. HasCallStack => a
__IMPOSSIBLE__
    [Name]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *}. Monad m => QName -> m Name
unqual forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete) [QName]
xs
    (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> [Name] -> Expr -> Declaration
C.UnquoteDef (forall a. HasRange a => a -> Range
getRange [DefInfo]
i) [Name]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e

  toConcrete (A.UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e) = forall a. HasCallStack => a
__IMPOSSIBLE__


data RangeAndPragma = RangeAndPragma Range A.Pragma

instance ToConcrete RangeAndPragma where
  type ConOfAbs RangeAndPragma = C.Pragma

  toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma)
toConcrete (RangeAndPragma Range
r Pragma
p) = case Pragma
p of
    A.OptionsPragma [RawName]
xs  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> [RawName] -> Pragma
C.OptionsPragma Range
r [RawName]
xs
    A.BuiltinPragma Ranged RawName
b ResolvedName
x       -> Range -> Ranged RawName -> QName -> Pragma
C.BuiltinPragma Range
r Ranged RawName
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ResolvedName
x
    A.BuiltinNoDefPragma Ranged RawName
b KindOfName
_kind QName
x -> Range -> Ranged RawName -> QName -> Pragma
C.BuiltinPragma Range
r Ranged RawName
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    A.RewritePragma Range
r' [QName]
x      -> Range -> Range -> [QName] -> Pragma
C.RewritePragma Range
r Range
r' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [QName]
x
    A.CompilePragma Ranged RawName
b QName
x RawName
s -> do
      QName
x <- forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Ranged RawName -> QName -> RawName -> Pragma
C.CompilePragma Range
r Ranged RawName
b QName
x RawName
s
    A.StaticPragma QName
x -> Range -> QName -> Pragma
C.StaticPragma Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    A.InjectivePragma QName
x -> Range -> QName -> Pragma
C.InjectivePragma Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    A.InlinePragma Bool
b QName
x -> Range -> Bool -> QName -> Pragma
C.InlinePragma Range
r Bool
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    A.NotProjectionLikePragma QName
q -> Range -> QName -> Pragma
C.NotProjectionLikePragma Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
q
    A.EtaPragma QName
x    -> Range -> QName -> Pragma
C.EtaPragma    Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    A.DisplayPragma QName
f [NamedArg Pattern]
ps Expr
rhs ->
      Range -> Pattern -> Expr -> Pragma
C.DisplayPragma Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP (Range -> PatInfo
PatRange forall a. Range' a
noRange) (QName -> AmbiguousQName
unambiguous QName
f) [NamedArg Pattern]
ps) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
rhs

-- Left hand sides --------------------------------------------------------

instance ToConcrete A.SpineLHS where
  type ConOfAbs A.SpineLHS = C.LHS

  bindToConcrete :: forall b.
SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b
bindToConcrete SpineLHS
lhs = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. LHSToSpine a b => b -> a
A.spineToLhs SpineLHS
lhs :: A.LHS)

instance ToConcrete A.LHS where
    type ConOfAbs A.LHS = C.LHS

    bindToConcrete :: forall b. LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b
bindToConcrete (A.LHS LHSInfo
i LHSCore
lhscore) ConOfAbs LHS -> AbsToCon b
ret = do
      forall a b.
ToConcrete a =>
Precedence -> a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcreteCtx Precedence
TopCtx LHSCore
lhscore forall a b. (a -> b) -> a -> b
$ \ ConOfAbs LHSCore
lhs ->
          ConOfAbs LHS -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
C.LHS (ExpandedEllipsis -> Pattern -> Pattern
reintroduceEllipsis (LHSInfo -> ExpandedEllipsis
lhsEllipsis LHSInfo
i) ConOfAbs LHSCore
lhs) [] []

instance ToConcrete A.LHSCore where
  type ConOfAbs A.LHSCore = C.Pattern
  bindToConcrete :: forall b. LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b
bindToConcrete = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHSCore -> Pattern
lhsCoreToPattern

appBracketsArgs :: [arg] -> PrecedenceStack -> Bool
appBracketsArgs :: forall arg. [arg] -> PrecedenceStack -> Bool
appBracketsArgs []    PrecedenceStack
_   = Bool
False
appBracketsArgs (arg
_:[arg]
_) PrecedenceStack
ctx = PrecedenceStack -> Bool
appBrackets PrecedenceStack
ctx

-- Auxiliary wrappers for processing the bindings in patterns in the right order.
newtype UserPattern a  = UserPattern a
newtype SplitPattern a = SplitPattern a
newtype BindingPattern = BindingPat A.Pattern
newtype FreshenName = FreshenName BindName

instance ToConcrete FreshenName where
  type ConOfAbs FreshenName = A.Name
  bindToConcrete :: forall b.
FreshenName -> (ConOfAbs FreshenName -> AbsToCon b) -> AbsToCon b
bindToConcrete (FreshenName BindName{ unBind :: BindName -> Name
unBind = Name
x }) ConOfAbs FreshenName -> AbsToCon b
ret = forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete Name
x forall a b. (a -> b) -> a -> b
$ \ ConOfAbs Name
y -> ConOfAbs FreshenName -> AbsToCon b
ret Name
x { nameConcrete :: Name
nameConcrete = ConOfAbs Name
y }

-- Pass 1: (Issue #2729)
-- Takes care of binding the originally user-written pattern variables, but doesn't actually
-- translate anything to Concrete.
instance ToConcrete (UserPattern A.Pattern) where
  type ConOfAbs (UserPattern A.Pattern) = A.Pattern

  bindToConcrete :: forall b.
UserPattern Pattern
-> (ConOfAbs (UserPattern Pattern) -> AbsToCon b) -> AbsToCon b
bindToConcrete (UserPattern Pattern
p) ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret = do
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.pat" VerboseLevel
100 forall a b. (a -> b) -> a -> b
$ RawName
"binding pattern (pass 1)" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Pattern
p
    case Pattern
p of
      A.VarP BindName
bx -> do
        let x :: Name
x = BindName -> Name
unBind BindName
bx
        case forall a. LensInScope a => a -> NameInScope
isInScope Name
x of
          NameInScope
InScope            -> forall a. Name -> AbsToCon a -> AbsToCon a
bindName' Name
x forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP BindName
bx
          NameInScope
C.NotInScope       -> forall a. Name -> (Name -> AbsToCon a) -> AbsToCon a
bindName Name
x forall a b. (a -> b) -> a -> b
$ \Name
y ->
                                ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName forall a b. (a -> b) -> a -> b
$ Name
x { nameConcrete :: Name
nameConcrete = Name
y }
      A.WildP{}              -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.ProjP{}              -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.AbsurdP{}            -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.LitP{}               -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.DotP{}               -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.EqualP{}             -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
      -- Andreas, 2017-09-03, issue #2729:
      -- Do not go into patterns generated by case-split here!
      -- They are treated in a second pass.
      A.ConP ConPatInfo
i AmbiguousQName
c [NamedArg Pattern]
args
        | ConPatInfo -> ConInfo
conPatOrigin ConPatInfo
i forall a. Eq a => a -> a -> Bool
== ConInfo
ConOSplit -> ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret Pattern
p
        | Bool
otherwise          -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> UserPattern a
UserPattern [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c
      A.DefP PatInfo
i AmbiguousQName
f [NamedArg Pattern]
args        -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> UserPattern a
UserPattern [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f
      A.PatternSynP PatInfo
i AmbiguousQName
f [NamedArg Pattern]
args -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> UserPattern a
UserPattern [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
f
      A.RecP PatInfo
i [FieldAssignment' Pattern]
args          -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete ((forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a. a -> UserPattern a
UserPattern [FieldAssignment' Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
i
      A.AsP PatInfo
i BindName
x Pattern
p            -> forall a. Name -> AbsToCon a -> AbsToCon a
bindName' (BindName -> Name
unBind BindName
x) forall a b. (a -> b) -> a -> b
$
                                forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> UserPattern a
UserPattern Pattern
p) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (UserPattern Pattern)
p ->
                                ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret (forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
x ConOfAbs (UserPattern Pattern)
p)
      A.WithP PatInfo
i Pattern
p            -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> UserPattern a
UserPattern Pattern
p) forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i
      A.AnnP PatInfo
i Expr
a Pattern
p           -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> UserPattern a
UserPattern Pattern
p) forall a b. (a -> b) -> a -> b
$ ConOfAbs (UserPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
i Expr
a

instance ToConcrete (UserPattern (NamedArg A.Pattern)) where
  type ConOfAbs (UserPattern (NamedArg A.Pattern)) = NamedArg A.Pattern

  bindToConcrete :: forall b.
UserPattern (NamedArg Pattern)
-> (ConOfAbs (UserPattern (NamedArg Pattern)) -> AbsToCon b)
-> AbsToCon b
bindToConcrete (UserPattern NamedArg Pattern
np) ConOfAbs (UserPattern (NamedArg Pattern)) -> AbsToCon b
ret =
    case forall a. LensOrigin a => a -> Origin
getOrigin NamedArg Pattern
np of
      Origin
CaseSplit -> ConOfAbs (UserPattern (NamedArg Pattern)) -> AbsToCon b
ret NamedArg Pattern
np
      Origin
_         -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> UserPattern a
UserPattern) NamedArg Pattern
np) ConOfAbs (UserPattern (NamedArg Pattern)) -> AbsToCon b
ret

-- Pass 2a: locate case-split pattern.  Don't bind anything!
instance ToConcrete (SplitPattern A.Pattern) where
  type ConOfAbs (SplitPattern A.Pattern) = A.Pattern

  bindToConcrete :: forall b.
SplitPattern Pattern
-> (ConOfAbs (SplitPattern Pattern) -> AbsToCon b) -> AbsToCon b
bindToConcrete (SplitPattern Pattern
p) ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret = do
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.pat" VerboseLevel
100 forall a b. (a -> b) -> a -> b
$ RawName
"binding pattern (pass 2a)" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Pattern
p
    case Pattern
p of
      A.VarP BindName
x               -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.WildP{}              -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.ProjP{}              -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.AbsurdP{}            -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.LitP{}               -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.DotP{}               -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      A.EqualP{}             -> ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret Pattern
p
      -- Andreas, 2017-09-03, issue #2729:
      -- For patterns generated by case-split here, switch to freshening & binding.
      A.ConP ConPatInfo
i AmbiguousQName
c [NamedArg Pattern]
args
        | ConPatInfo -> ConInfo
conPatOrigin ConPatInfo
i forall a. Eq a => a -> a -> Bool
== ConInfo
ConOSplit
                             -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete ((forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> BindingPattern
BindingPat [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c
        | Bool
otherwise          -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> SplitPattern a
SplitPattern [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c
      A.DefP PatInfo
i AmbiguousQName
f [NamedArg Pattern]
args        -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> SplitPattern a
SplitPattern [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f
      A.PatternSynP PatInfo
i AmbiguousQName
f [NamedArg Pattern]
args -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> SplitPattern a
SplitPattern [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
f
      A.RecP PatInfo
i [FieldAssignment' Pattern]
args          -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete ((forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a. a -> SplitPattern a
SplitPattern [FieldAssignment' Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
i
      A.AsP PatInfo
i BindName
x Pattern
p            -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> SplitPattern a
SplitPattern Pattern
p)  forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (SplitPattern Pattern)
p ->
                                ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret (forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
x ConOfAbs (SplitPattern Pattern)
p)
      A.WithP PatInfo
i Pattern
p            -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> SplitPattern a
SplitPattern Pattern
p) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i
      A.AnnP PatInfo
i Expr
a Pattern
p           -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> SplitPattern a
SplitPattern Pattern
p) forall a b. (a -> b) -> a -> b
$ ConOfAbs (SplitPattern Pattern) -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
i Expr
a

instance ToConcrete (SplitPattern (NamedArg A.Pattern)) where
  type ConOfAbs (SplitPattern (NamedArg A.Pattern)) = NamedArg A.Pattern
  bindToConcrete :: forall b.
SplitPattern (NamedArg Pattern)
-> (ConOfAbs (SplitPattern (NamedArg Pattern)) -> AbsToCon b)
-> AbsToCon b
bindToConcrete (SplitPattern NamedArg Pattern
np) ConOfAbs (SplitPattern (NamedArg Pattern)) -> AbsToCon b
ret =
    case forall a. LensOrigin a => a -> Origin
getOrigin NamedArg Pattern
np of
      Origin
CaseSplit -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> BindingPattern
BindingPat  ) NamedArg Pattern
np) ConOfAbs (SplitPattern (NamedArg Pattern)) -> AbsToCon b
ret
      Origin
_         -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> SplitPattern a
SplitPattern) NamedArg Pattern
np) ConOfAbs (SplitPattern (NamedArg Pattern)) -> AbsToCon b
ret


-- Pass 2b:
-- Takes care of freshening and binding pattern variables introduced by case split.
-- Still does not translate anything to Concrete.
instance ToConcrete BindingPattern where
  type ConOfAbs BindingPattern = A.Pattern
  bindToConcrete :: forall b.
BindingPattern
-> (ConOfAbs BindingPattern -> AbsToCon b) -> AbsToCon b
bindToConcrete (BindingPat Pattern
p) ConOfAbs BindingPattern -> AbsToCon b
ret = do
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.pat" VerboseLevel
100 forall a b. (a -> b) -> a -> b
$ RawName
"binding pattern (pass 2b)" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Pattern
p
    case Pattern
p of
      A.VarP BindName
x               -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (BindName -> FreshenName
FreshenName BindName
x) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. BindName -> Pattern' e
A.VarP forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName
      A.WildP{}              -> ConOfAbs BindingPattern -> AbsToCon b
ret Pattern
p
      A.ProjP{}              -> ConOfAbs BindingPattern -> AbsToCon b
ret Pattern
p
      A.AbsurdP{}            -> ConOfAbs BindingPattern -> AbsToCon b
ret Pattern
p
      A.LitP{}               -> ConOfAbs BindingPattern -> AbsToCon b
ret Pattern
p
      A.DotP{}               -> ConOfAbs BindingPattern -> AbsToCon b
ret Pattern
p
      A.EqualP{}             -> ConOfAbs BindingPattern -> AbsToCon b
ret Pattern
p
      A.ConP ConPatInfo
i AmbiguousQName
c [NamedArg Pattern]
args        -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> BindingPattern
BindingPat) [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c
      A.DefP PatInfo
i AmbiguousQName
f [NamedArg Pattern]
args        -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> BindingPattern
BindingPat) [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f
      A.PatternSynP PatInfo
i AmbiguousQName
f [NamedArg Pattern]
args -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> BindingPattern
BindingPat) [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
f
      A.RecP PatInfo
i [FieldAssignment' Pattern]
args          -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete ((forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)        Pattern -> BindingPattern
BindingPat [FieldAssignment' Pattern]
args) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
i
      A.AsP PatInfo
i BindName
x Pattern
p            -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (BindName -> FreshenName
FreshenName BindName
x) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs FreshenName
x ->
                                forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (Pattern -> BindingPattern
BindingPat Pattern
p)  forall a b. (a -> b) -> a -> b
$ \ ConOfAbs BindingPattern
p ->
                                ConOfAbs BindingPattern -> AbsToCon b
ret (forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i (Name -> BindName
mkBindName ConOfAbs FreshenName
x) ConOfAbs BindingPattern
p)
      A.WithP PatInfo
i Pattern
p            -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (Pattern -> BindingPattern
BindingPat Pattern
p) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i
      A.AnnP PatInfo
i Expr
a Pattern
p           -> forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (Pattern -> BindingPattern
BindingPat Pattern
p) forall a b. (a -> b) -> a -> b
$ ConOfAbs BindingPattern -> AbsToCon b
ret forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
i Expr
a

instance ToConcrete A.Pattern where
  type ConOfAbs A.Pattern = C.Pattern

  bindToConcrete :: forall b. Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b
bindToConcrete Pattern
p ConOfAbs Pattern -> AbsToCon b
ret = do
    PrecedenceStack
prec <- AbsToCon PrecedenceStack
currentPrecedence
    forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> UserPattern a
UserPattern Pattern
p) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (UserPattern Pattern)
p -> do
      forall a b.
ToConcrete a =>
a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
bindToConcrete (forall a. a -> SplitPattern a
SplitPattern ConOfAbs (UserPattern Pattern)
p) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs (SplitPattern Pattern)
p -> do
        ConOfAbs Pattern -> AbsToCon b
ret forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall a. PrecedenceStack -> AbsToCon a -> AbsToCon a
withPrecedence' PrecedenceStack
prec forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete ConOfAbs (SplitPattern Pattern)
p
  toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern)
toConcrete Pattern
p =
    case Pattern
p of
      A.VarP BindName
x ->
        QName -> Pattern
C.IdentP forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
C.QName forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundName -> Name
C.boundName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete BindName
x

      A.WildP PatInfo
i ->
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Pattern
C.WildP (forall a. HasRange a => a -> Range
getRange PatInfo
i)

      A.ConP ConPatInfo
i AmbiguousQName
c [NamedArg Pattern]
args  -> QName
-> ([NamedArg Pattern] -> Pattern)
-> [NamedArg Pattern]
-> AbsToCon Pattern
tryOp (AmbiguousQName -> QName
headAmbQ AmbiguousQName
c) (forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c) [NamedArg Pattern]
args

      A.ProjP PatInfo
i ProjOrigin
ProjPrefix AmbiguousQName
p -> QName -> Pattern
C.IdentP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (AmbiguousQName -> QName
headAmbQ AmbiguousQName
p)
      A.ProjP PatInfo
i ProjOrigin
_          AmbiguousQName
p -> Range -> Expr -> Pattern
C.DotP forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Expr
C.Ident forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (AmbiguousQName -> QName
headAmbQ AmbiguousQName
p)

      A.DefP PatInfo
i AmbiguousQName
x [NamedArg Pattern]
args -> QName
-> ([NamedArg Pattern] -> Pattern)
-> [NamedArg Pattern]
-> AbsToCon Pattern
tryOp (AmbiguousQName -> QName
headAmbQ AmbiguousQName
x) (forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
x)  [NamedArg Pattern]
args

      A.AsP PatInfo
i BindName
x Pattern
p -> do
        (BoundName
x, Pattern
p) <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
argumentCtx_ (BindName
x, Pattern
p)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Name -> Pattern -> Pattern
C.AsP (forall a. HasRange a => a -> Range
getRange PatInfo
i) (BoundName -> Name
C.boundName BoundName
x) Pattern
p

      A.AbsurdP PatInfo
i ->
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Pattern
C.AbsurdP (forall a. HasRange a => a -> Range
getRange PatInfo
i)

      A.LitP PatInfo
i (LitQName QName
x) -> do
        QName
x <- AllowAmbiguousNames -> QName -> AbsToCon QName
lookupQName AllowAmbiguousNames
AmbiguousNothing QName
x
        (PrecedenceStack -> Bool) -> AbsToCon Pattern -> AbsToCon Pattern
bracketP_ PrecedenceStack -> Bool
appBrackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pattern -> Arg (Named_ Pattern) -> Pattern
C.AppP (Range -> Pattern
C.QuoteP (forall a. HasRange a => a -> Range
getRange PatInfo
i)) (forall a. a -> NamedArg a
defaultNamedArg (QName -> Pattern
C.IdentP QName
x))
      A.LitP PatInfo
i Literal
l ->
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Literal -> Pattern
C.LitP (forall a. HasRange a => a -> Range
getRange PatInfo
i) Literal
l

      -- Andreas, 2018-06-19, issue #3130
      -- Print .p as .(p) if p is a projection
      -- to avoid confusion with projection pattern.
      A.DotP PatInfo
i e :: Expr
e@A.Proj{} -> Range -> Expr -> Pattern
C.DotP Range
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Expr -> Expr
C.Paren Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx Expr
e
        where r :: Range
r = forall a. HasRange a => a -> Range
getRange PatInfo
i

      -- gallais, 2019-02-12, issue #3491
      -- Print p as .(p) if p is a variable but there is a projection of the
      -- same name in scope.
      A.DotP PatInfo
i e :: Expr
e@(A.Var Name
v) -> do
        let r :: Range
r = forall a. HasRange a => a -> Range
getRange PatInfo
i
        -- Erase @v@ to a concrete name and resolve it back to check whether
        -- we have a conflicting field name.
        Name
cn <- Name -> AbsToCon Name
toConcreteName Name
v
        KindsOfNames
-> Maybe (Set Name)
-> QName
-> AbsToCon (Either AmbiguousNameReason ResolvedName)
resolveName ([KindOfName] -> KindsOfNames
someKindsOfNames [KindOfName
FldName]) forall a. Maybe a
Nothing (Name -> QName
C.QName Name
cn) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
          -- If we do then we print .(v) rather than .v
          Right FieldName{} -> do
            forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"print.dotted" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ RawName
"Wrapping ambiguous name " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> RawName
prettyShow (Name -> Name
nameConcrete Name
v)
            Range -> Expr -> Pattern
C.DotP Range
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Expr -> Expr
C.Paren Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (Name -> Expr
A.Var Name
v)
          Right ResolvedName
_ -> PatInfo -> Expr -> AbsToCon Pattern
printDotDefault PatInfo
i Expr
e
          Left AmbiguousNameReason
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

      A.DotP PatInfo
i Expr
e -> PatInfo -> Expr -> AbsToCon Pattern
printDotDefault PatInfo
i Expr
e

      A.EqualP PatInfo
i [(Expr, Expr)]
es -> do
        Range -> [(Expr, Expr)] -> Pattern
C.EqualP (forall a. HasRange a => a -> Range
getRange PatInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [(Expr, Expr)]
es

      A.PatternSynP PatInfo
i AmbiguousQName
n [NamedArg Pattern]
args -> QName
-> ([NamedArg Pattern] -> Pattern)
-> [NamedArg Pattern]
-> AbsToCon Pattern
tryOp (AmbiguousQName -> QName
headAmbQ AmbiguousQName
n) (forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.PatternSynP PatInfo
i AmbiguousQName
n) [NamedArg Pattern]
args

      A.RecP PatInfo
i [FieldAssignment' Pattern]
as ->
        Range -> [FieldAssignment' Pattern] -> Pattern
C.RecP (forall a. HasRange a => a -> Range
getRange PatInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete) [FieldAssignment' Pattern]
as

      A.WithP PatInfo
i Pattern
p -> Range -> Pattern -> Pattern
C.WithP (forall a. HasRange a => a -> Range
getRange PatInfo
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
WithArgCtx Pattern
p

      A.AnnP PatInfo
i Expr
a Pattern
p -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Pattern
p -- TODO: print type annotation

    where

    printDotDefault :: PatInfo -> A.Expr -> AbsToCon C.Pattern
    printDotDefault :: PatInfo -> Expr -> AbsToCon Pattern
printDotDefault PatInfo
i Expr
e = do
      Expr
c <- forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
DotPatternCtx Expr
e
      let r :: Range
r = forall a. HasRange a => a -> Range
getRange PatInfo
i
      case Expr
c of
        -- Andreas, 2016-02-04 print ._ pattern as _ pattern,
        -- following the fusing of WildP and ImplicitP.
        C.Underscore{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Pattern
C.WildP Range
r
        Expr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Pattern
C.DotP Range
r Expr
c

    tryOp :: A.QName -> (A.Patterns -> A.Pattern) -> A.Patterns -> AbsToCon C.Pattern
    tryOp :: QName
-> ([NamedArg Pattern] -> Pattern)
-> [NamedArg Pattern]
-> AbsToCon Pattern
tryOp QName
x [NamedArg Pattern] -> Pattern
f [NamedArg Pattern]
args = do
      -- Andreas, 2016-02-04, Issue #1792
      -- To prevent failing of tryToRecoverOpAppP for overapplied operators,
      -- we take off the exceeding arguments first
      -- and apply them pointwise with C.AppP later.
      let ([NamedArg Pattern]
args1, [NamedArg Pattern]
args2) = forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt (forall a. NumHoles a => a -> VerboseLevel
numHoles QName
x) [NamedArg Pattern]
args
      let funCtx :: AbsToCon (Maybe Pattern) -> AbsToCon (Maybe Pattern)
funCtx = forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. Null a => a -> Bool
null [NamedArg Pattern]
args2) (forall a. Precedence -> AbsToCon a -> AbsToCon a
withPrecedence Precedence
FunctionCtx)
      Pattern -> AbsToCon Pattern -> AbsToCon Pattern
tryToRecoverPatternSynP ([NamedArg Pattern] -> Pattern
f [NamedArg Pattern]
args) forall a b. (a -> b) -> a -> b
$ AbsToCon (Maybe Pattern) -> AbsToCon (Maybe Pattern)
funCtx (Pattern -> AbsToCon (Maybe Pattern)
tryToRecoverOpAppP forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern] -> Pattern
f [NamedArg Pattern]
args1) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just Pattern
c  -> forall {arg}.
(ConOfAbs arg ~ Arg (Named_ Pattern), ToConcrete arg) =>
[arg] -> Pattern -> AbsToCon Pattern
applyTo [NamedArg Pattern]
args2 Pattern
c
        Maybe Pattern
Nothing -> forall {arg}.
(ConOfAbs arg ~ Arg (Named_ Pattern), ToConcrete arg) =>
[arg] -> Pattern -> AbsToCon Pattern
applyTo [NamedArg Pattern]
args forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Pattern
C.IdentP forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete QName
x
    -- Note: applyTo [] c = return c
    applyTo :: [arg] -> Pattern -> AbsToCon Pattern
applyTo [arg]
args Pattern
c = (PrecedenceStack -> Bool) -> AbsToCon Pattern -> AbsToCon Pattern
bracketP_ (forall arg. [arg] -> PrecedenceStack -> Bool
appBracketsArgs [arg]
args) forall a b. (a -> b) -> a -> b
$ do
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> Arg (Named_ Pattern) -> Pattern
C.AppP Pattern
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
argumentCtx_ [arg]
args

instance ToConcrete (Maybe A.Pattern) where
  type ConOfAbs (Maybe A.Pattern) = Maybe C.Pattern

  toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern))
toConcrete = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete

-- Helpers for recovering natural number literals

tryToRecoverNatural :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverNatural :: Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverNatural Expr
e AbsToCon Expr
def = do
  QName -> RawName -> Bool
is <- AbsToCon (QName -> RawName -> Bool)
isBuiltinFun
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((QName -> RawName -> Bool) -> Expr -> Maybe Integer
recoverNatural QName -> RawName -> Bool
is Expr
e) AbsToCon Expr
def forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Literal -> Expr
C.Lit forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
LitNat

recoverNatural :: (A.QName -> String -> Bool) -> A.Expr -> Maybe Integer
recoverNatural :: (QName -> RawName -> Bool) -> Expr -> Maybe Integer
recoverNatural QName -> RawName -> Bool
is Expr
e = (QName -> Bool)
-> (QName -> Bool) -> Integer -> Expr -> Maybe Integer
explore (QName -> RawName -> Bool
`is` RawName
builtinZero) (QName -> RawName -> Bool
`is` RawName
builtinSuc) Integer
0 Expr
e
  where
    explore :: (A.QName -> Bool) -> (A.QName -> Bool) -> Integer -> A.Expr -> Maybe Integer
    explore :: (QName -> Bool)
-> (QName -> Bool) -> Integer -> Expr -> Maybe Integer
explore QName -> Bool
isZero QName -> Bool
isSuc Integer
k (A.App AppInfo
_ (A.Con AmbiguousQName
c) NamedArg Expr
t) | Just QName
f <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
c, QName -> Bool
isSuc QName
f
                                                = ((QName -> Bool)
-> (QName -> Bool) -> Integer -> Expr -> Maybe Integer
explore QName -> Bool
isZero QName -> Bool
isSuc forall a b. (a -> b) -> a -> b
$! Integer
k forall a. Num a => a -> a -> a
+ Integer
1) (forall a. NamedArg a -> a
namedArg NamedArg Expr
t)
    explore QName -> Bool
isZero QName -> Bool
isSuc Integer
k (A.Con AmbiguousQName
c) | Just QName
x <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
c, QName -> Bool
isZero QName
x = forall a. a -> Maybe a
Just Integer
k
    explore QName -> Bool
isZero QName -> Bool
isSuc Integer
k (A.Lit ExprInfo
_ (LitNat Integer
l)) = forall a. a -> Maybe a
Just (Integer
k forall a. Num a => a -> a -> a
+ Integer
l)
    explore QName -> Bool
_ QName -> Bool
_ Integer
_ Expr
_                             = forall a. Maybe a
Nothing

-- Helpers for recovering C.OpApp ------------------------------------------

data Hd = HdVar A.Name | HdCon A.QName | HdDef A.QName | HdSyn A.QName

data MaybeSection a
  = YesSection
  | NoSection a
  deriving (MaybeSection a -> MaybeSection a -> Bool
forall a. Eq a => MaybeSection a -> MaybeSection a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MaybeSection a -> MaybeSection a -> Bool
$c/= :: forall a. Eq a => MaybeSection a -> MaybeSection a -> Bool
== :: MaybeSection a -> MaybeSection a -> Bool
$c== :: forall a. Eq a => MaybeSection a -> MaybeSection a -> Bool
Eq, VerboseLevel -> MaybeSection a -> ShowS
forall a. Show a => VerboseLevel -> MaybeSection a -> ShowS
forall a. Show a => [MaybeSection a] -> ShowS
forall a. Show a => MaybeSection a -> RawName
forall a.
(VerboseLevel -> a -> ShowS)
-> (a -> RawName) -> ([a] -> ShowS) -> Show a
showList :: [MaybeSection a] -> ShowS
$cshowList :: forall a. Show a => [MaybeSection a] -> ShowS
show :: MaybeSection a -> RawName
$cshow :: forall a. Show a => MaybeSection a -> RawName
showsPrec :: VerboseLevel -> MaybeSection a -> ShowS
$cshowsPrec :: forall a. Show a => VerboseLevel -> MaybeSection a -> ShowS
Show, forall a b. a -> MaybeSection b -> MaybeSection a
forall a b. (a -> b) -> MaybeSection a -> MaybeSection b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> MaybeSection b -> MaybeSection a
$c<$ :: forall a b. a -> MaybeSection b -> MaybeSection a
fmap :: forall a b. (a -> b) -> MaybeSection a -> MaybeSection b
$cfmap :: forall a b. (a -> b) -> MaybeSection a -> MaybeSection b
Functor, forall a. Eq a => a -> MaybeSection a -> Bool
forall a. Num a => MaybeSection a -> a
forall a. Ord a => MaybeSection a -> a
forall m. Monoid m => MaybeSection m -> m
forall a. MaybeSection a -> Bool
forall a. MaybeSection a -> VerboseLevel
forall a. MaybeSection a -> [a]
forall a. (a -> a -> a) -> MaybeSection a -> a
forall m a. Monoid m => (a -> m) -> MaybeSection a -> m
forall b a. (b -> a -> b) -> b -> MaybeSection a -> b
forall a b. (a -> b -> b) -> b -> MaybeSection a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> VerboseLevel)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => MaybeSection a -> a
$cproduct :: forall a. Num a => MaybeSection a -> a
sum :: forall a. Num a => MaybeSection a -> a
$csum :: forall a. Num a => MaybeSection a -> a
minimum :: forall a. Ord a => MaybeSection a -> a
$cminimum :: forall a. Ord a => MaybeSection a -> a
maximum :: forall a. Ord a => MaybeSection a -> a
$cmaximum :: forall a. Ord a => MaybeSection a -> a
elem :: forall a. Eq a => a -> MaybeSection a -> Bool
$celem :: forall a. Eq a => a -> MaybeSection a -> Bool
length :: forall a. MaybeSection a -> VerboseLevel
$clength :: forall a. MaybeSection a -> VerboseLevel
null :: forall a. MaybeSection a -> Bool
$cnull :: forall a. MaybeSection a -> Bool
toList :: forall a. MaybeSection a -> [a]
$ctoList :: forall a. MaybeSection a -> [a]
foldl1 :: forall a. (a -> a -> a) -> MaybeSection a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> MaybeSection a -> a
foldr1 :: forall a. (a -> a -> a) -> MaybeSection a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> MaybeSection a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> MaybeSection a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> MaybeSection a -> b
foldl :: forall b a. (b -> a -> b) -> b -> MaybeSection a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> MaybeSection a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> MaybeSection a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> MaybeSection a -> b
foldr :: forall a b. (a -> b -> b) -> b -> MaybeSection a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> MaybeSection a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> MaybeSection a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> MaybeSection a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> MaybeSection a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> MaybeSection a -> m
fold :: forall m. Monoid m => MaybeSection m -> m
$cfold :: forall m. Monoid m => MaybeSection m -> m
Foldable, Functor MaybeSection
Foldable MaybeSection
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
MaybeSection (m a) -> m (MaybeSection a)
forall (f :: * -> *) a.
Applicative f =>
MaybeSection (f a) -> f (MaybeSection a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeSection a -> m (MaybeSection b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeSection a -> f (MaybeSection b)
sequence :: forall (m :: * -> *) a.
Monad m =>
MaybeSection (m a) -> m (MaybeSection a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
MaybeSection (m a) -> m (MaybeSection a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeSection a -> m (MaybeSection b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeSection a -> m (MaybeSection b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
MaybeSection (f a) -> f (MaybeSection a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
MaybeSection (f a) -> f (MaybeSection a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeSection a -> f (MaybeSection b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeSection a -> f (MaybeSection b)
Traversable)

fromNoSection :: a -> MaybeSection a -> a
fromNoSection :: forall a. a -> MaybeSection a -> a
fromNoSection a
fallback = \case
  MaybeSection a
YesSection  -> a
fallback
  NoSection a
x -> a
x

instance HasRange a => HasRange (MaybeSection a) where
  getRange :: MaybeSection a -> Range
getRange = \case
    MaybeSection a
YesSection  -> forall a. Range' a
noRange
    NoSection a
a -> forall a. HasRange a => a -> Range
getRange a
a

getHead :: A.Expr -> Maybe Hd
getHead :: Expr -> Maybe Hd
getHead (Var Name
x)          = forall a. a -> Maybe a
Just (Name -> Hd
HdVar Name
x)
getHead (Def QName
f)          = forall a. a -> Maybe a
Just (QName -> Hd
HdDef QName
f)
getHead (Proj ProjOrigin
o AmbiguousQName
f)       = forall a. a -> Maybe a
Just (QName -> Hd
HdDef forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
f)
getHead (Con AmbiguousQName
c)          = forall a. a -> Maybe a
Just (QName -> Hd
HdCon forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
c)
getHead (A.PatternSyn AmbiguousQName
n) = forall a. a -> Maybe a
Just (QName -> Hd
HdSyn forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
n)
getHead Expr
_                = forall a. Maybe a
Nothing

cOpApp :: Range -> C.QName -> A.Name -> List1 (MaybeSection C.Expr) -> C.Expr
cOpApp :: Range -> QName -> Name -> List1 (MaybeSection Expr) -> Expr
cOpApp Range
r QName
x Name
n List1 (MaybeSection Expr)
es =
  Range -> QName -> Set Name -> OpAppArgs -> Expr
C.OpApp Range
r QName
x (forall a. a -> Set a
Set.singleton Name
n) forall a b. (a -> b) -> a -> b
$
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> NamedArg a
defaultNamedArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {e}.
(MaybeSection e, PositionInName) -> MaybePlaceholder (OpApp e)
placeholder) forall a b. (a -> b) -> a -> b
$
  forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (MaybeSection Expr, PositionInName)
eps
  where
    x0 :: Name
x0 = QName -> Name
C.unqualify QName
x
    positions :: List1 PositionInName
positions | Name -> Bool
isPrefix  Name
x0 =              (forall a b. a -> b -> a
const PositionInName
Middle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. VerboseLevel -> NonEmpty a -> [a]
List1.drop VerboseLevel
1 List1 (MaybeSection Expr)
es) forall a. [a] -> a -> List1 a
`List1.snoc` PositionInName
End
              | Name -> Bool
isPostfix Name
x0 = PositionInName
Beginning forall a. a -> [a] -> NonEmpty a
:| (forall a b. a -> b -> a
const PositionInName
Middle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. VerboseLevel -> NonEmpty a -> [a]
List1.drop VerboseLevel
1 List1 (MaybeSection Expr)
es)
              | Name -> Bool
isInfix Name
x0   = PositionInName
Beginning forall a. a -> [a] -> NonEmpty a
:| (forall a b. a -> b -> a
const PositionInName
Middle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. VerboseLevel -> NonEmpty a -> [a]
List1.drop VerboseLevel
2 List1 (MaybeSection Expr)
es) forall a. [a] -> [a] -> [a]
++ [ PositionInName
End ]
              | Bool
otherwise    =               forall a b. a -> b -> a
const PositionInName
Middle forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 (MaybeSection Expr)
es
    eps :: NonEmpty (MaybeSection Expr, PositionInName)
eps = forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
List1.zip List1 (MaybeSection Expr)
es List1 PositionInName
positions
    placeholder :: (MaybeSection e, PositionInName) -> MaybePlaceholder (OpApp e)
placeholder (MaybeSection e
YesSection , PositionInName
pos ) = forall e. PositionInName -> MaybePlaceholder e
Placeholder PositionInName
pos
    placeholder (NoSection e
e, PositionInName
_pos) = forall e. e -> MaybePlaceholder e
noPlaceholder (forall e. e -> OpApp e
Ordinary e
e)

tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverOpApp :: Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverOpApp Expr
e AbsToCon Expr
def = forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM AbsToCon Expr
def forall a b. (a -> b) -> a -> b
$
  forall a c.
(ToConcrete a, c ~ ConOfAbs a, HasRange c) =>
((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)
-> (a -> Bool)
-> (Range -> QName -> Name -> List1 (MaybeSection c) -> c)
-> (a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))]))
-> a
-> AbsToCon (Maybe c)
recoverOpApp (PrecedenceStack -> Bool) -> AbsToCon Expr -> AbsToCon Expr
bracket (NamedArg Expr -> Bool
isLambda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg) Range -> QName -> Name -> List1 (MaybeSection Expr) -> Expr
cOpApp Expr -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, Expr))])
view Expr
e
  where
    view :: A.Expr -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, A.Expr))])
    view :: Expr -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, Expr))])
view Expr
e
        -- Do we have a series of inserted lambdas?
      | Just xs :: [Binder]
xs@(Binder
_:[Binder]
_) <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse LamBinding -> Maybe Binder
insertedName [LamBinding]
bs =
        (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Hd
getHead Expr
hd forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Name]
-> [Arg (Named_ (AppInfo, Expr))]
-> Maybe [NamedArg (MaybeSection (AppInfo, Expr))]
sectionArgs (forall a b. (a -> b) -> [a] -> [b]
map (BindName -> Name
unBind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binder' a -> a
A.binderName) [Binder]
xs) [Arg (Named_ (AppInfo, Expr))]
args
      where
        LamView     [LamBinding]
bs Expr
body = Expr -> LamView
A.lamView Expr
e
        Application Expr
hd [Arg (Named_ (AppInfo, Expr))]
args = Expr -> AppView' (AppInfo, Expr)
A.appView' Expr
body

        -- Only inserted domain-free visible lambdas come from sections.
        insertedName :: LamBinding -> Maybe Binder
insertedName (A.DomainFree TacticAttr
_ NamedArg Binder
x)
          | forall a. LensOrigin a => a -> Origin
getOrigin NamedArg Binder
x forall a. Eq a => a -> a -> Bool
== Origin
Inserted Bool -> Bool -> Bool
&& forall a. LensHiding a => a -> Bool
visible NamedArg Binder
x = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
x
        insertedName LamBinding
_ = forall a. Maybe a
Nothing

        -- Build section arguments. Need to check that:
        -- lambda bound variables appear in the right order and only as
        -- top-level arguments.
        sectionArgs :: [A.Name] -> [NamedArg (AppInfo, A.Expr)] -> Maybe [NamedArg (MaybeSection (AppInfo, A.Expr))]
        sectionArgs :: [Name]
-> [Arg (Named_ (AppInfo, Expr))]
-> Maybe [NamedArg (MaybeSection (AppInfo, Expr))]
sectionArgs [Name]
xs = [Name]
-> [Arg (Named_ (AppInfo, Expr))]
-> Maybe [NamedArg (MaybeSection (AppInfo, Expr))]
go [Name]
xs
          where
            noXs :: Arg (Named_ (AppInfo, Expr)) -> Bool
noXs = All -> Bool
getAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a m. ExprLike a => FoldExprFn m a
foldExpr (\ case A.Var Name
x -> Bool -> All
All (Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
xs)
                                             Expr
_       -> Bool -> All
All Bool
True) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg
            go :: [Name]
-> [Arg (Named_ (AppInfo, Expr))]
-> Maybe [NamedArg (MaybeSection (AppInfo, Expr))]
go [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
            go (Name
y : [Name]
ys) (Arg (Named_ (AppInfo, Expr))
arg : [Arg (Named_ (AppInfo, Expr))]
args)
              | forall a. LensHiding a => a -> Bool
visible Arg (Named_ (AppInfo, Expr))
arg
              , A.Var Name
y' <- forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg Arg (Named_ (AppInfo, Expr))
arg
              , Name
y forall a. Eq a => a -> a -> Bool
== Name
y' = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. MaybeSection a
YesSection forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Arg (Named_ (AppInfo, Expr))
arg forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
-> [Arg (Named_ (AppInfo, Expr))]
-> Maybe [NamedArg (MaybeSection (AppInfo, Expr))]
go [Name]
ys [Arg (Named_ (AppInfo, Expr))]
args
            go [Name]
ys (Arg (Named_ (AppInfo, Expr))
arg : [Arg (Named_ (AppInfo, Expr))]
args)
              | forall a. LensHiding a => a -> Bool
visible Arg (Named_ (AppInfo, Expr))
arg, Arg (Named_ (AppInfo, Expr)) -> Bool
noXs Arg (Named_ (AppInfo, Expr))
arg = ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a. a -> MaybeSection a
NoSection Arg (Named_ (AppInfo, Expr))
arg forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
-> [Arg (Named_ (AppInfo, Expr))]
-> Maybe [NamedArg (MaybeSection (AppInfo, Expr))]
go [Name]
ys [Arg (Named_ (AppInfo, Expr))]
args
            go [Name]
_ [Arg (Named_ (AppInfo, Expr))]
_ = forall a. Maybe a
Nothing

    view Expr
e = (, (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a. a -> MaybeSection a
NoSection [Arg (Named_ (AppInfo, Expr))]
args) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Hd
getHead Expr
hd
      where Application Expr
hd [Arg (Named_ (AppInfo, Expr))]
args = Expr -> AppView' (AppInfo, Expr)
A.appView' Expr
e

tryToRecoverOpAppP :: A.Pattern -> AbsToCon (Maybe C.Pattern)
tryToRecoverOpAppP :: Pattern -> AbsToCon (Maybe Pattern)
tryToRecoverOpAppP Pattern
p = do
  Maybe Pattern
res <- forall a c.
(ToConcrete a, c ~ ConOfAbs a, HasRange c) =>
((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)
-> (a -> Bool)
-> (Range -> QName -> Name -> List1 (MaybeSection c) -> c)
-> (a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))]))
-> a
-> AbsToCon (Maybe c)
recoverOpApp (PrecedenceStack -> Bool) -> AbsToCon Pattern -> AbsToCon Pattern
bracketP_ (forall a b. a -> b -> a
const Bool
False) forall {l}.
(Item l ~ MaybeSection Pattern, IsList l) =>
Range -> QName -> Name -> l -> Pattern
opApp Pattern -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, Pattern))])
view Pattern
p
  forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
RawName -> VerboseLevel -> a -> m ()
reportS RawName
"print.op" VerboseLevel
90
    [ RawName
"tryToRecoverOpApp"
    , RawName
"in:  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Pattern
p
    , RawName
"out: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> RawName
show Maybe Pattern
res
    ]
  forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Pattern
res
  where
    opApp :: Range -> QName -> Name -> l -> Pattern
opApp Range
r QName
x Name
n l
ps = Range -> QName -> Set Name -> [Arg (Named_ Pattern)] -> Pattern
C.OpAppP Range
r QName
x (forall a. a -> Set a
Set.singleton Name
n) forall a b. (a -> b) -> a -> b
$
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> NamedArg a
defaultNamedArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> MaybeSection a -> a
fromNoSection forall a. HasCallStack => a
__IMPOSSIBLE__) forall a b. (a -> b) -> a -> b
$
      -- `view` does not generate any `Nothing`s
      forall l. IsList l => l -> [Item l]
List1.toList l
ps

    appInfo :: AppInfo
appInfo = AppInfo
defaultAppInfo_

    view :: A.Pattern -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, A.Pattern))])
    view :: Pattern -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, Pattern))])
view = \case
      ConP ConPatInfo
_        AmbiguousQName
cs [NamedArg Pattern]
ps -> forall a. a -> Maybe a
Just (QName -> Hd
HdCon (AmbiguousQName -> QName
headAmbQ AmbiguousQName
cs), (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a. a -> MaybeSection a
NoSection forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AppInfo
appInfo,)) [NamedArg Pattern]
ps)
      DefP PatInfo
_        AmbiguousQName
fs [NamedArg Pattern]
ps -> forall a. a -> Maybe a
Just (QName -> Hd
HdDef (AmbiguousQName -> QName
headAmbQ AmbiguousQName
fs), (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a. a -> MaybeSection a
NoSection forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AppInfo
appInfo,)) [NamedArg Pattern]
ps)
      PatternSynP PatInfo
_ AmbiguousQName
ns [NamedArg Pattern]
ps -> forall a. a -> Maybe a
Just (QName -> Hd
HdSyn (AmbiguousQName -> QName
headAmbQ AmbiguousQName
ns), (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall a. a -> MaybeSection a
NoSection forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AppInfo
appInfo,)) [NamedArg Pattern]
ps)
      Pattern
_                   -> forall a. Maybe a
Nothing
      -- ProjP _ _ d   -> Just (HdDef (headAmbQ d), [])   -- ? Andreas, 2016-04-21

recoverOpApp :: forall a c . (ToConcrete a, c ~ ConOfAbs a, HasRange c)
  => ((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)
  -> (a -> Bool)  -- ^ Check for lambdas
  -> (Range -> C.QName -> A.Name -> List1 (MaybeSection c) -> c)  -- ^ @opApp@
  -> (a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))]))
  -> a
  -> AbsToCon (Maybe c)
recoverOpApp :: forall a c.
(ToConcrete a, c ~ ConOfAbs a, HasRange c) =>
((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)
-> (a -> Bool)
-> (Range -> QName -> Name -> List1 (MaybeSection c) -> c)
-> (a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))]))
-> a
-> AbsToCon (Maybe c)
recoverOpApp (PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c
bracket a -> Bool
isLam Range -> QName -> Name -> List1 (MaybeSection c) -> c
opApp a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))])
view a
e = case a -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))])
view a
e of
  Maybe (Hd, [NamedArg (MaybeSection (AppInfo, a))])
Nothing -> forall {a}. AbsToCon (Maybe a)
mDefault
  Just (Hd
hd, [NamedArg (MaybeSection (AppInfo, a))]
args)
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. LensHiding a => a -> Bool
visible [NamedArg (MaybeSection (AppInfo, a))]
args    -> do
      let  args' :: [MaybeSection (AppInfo, a)]
args' = forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg (MaybeSection (AppInfo, a))]
args
      case Hd
hd of
        HdVar  Name
n
          | forall a. IsNoName a => a -> Bool
isNoName Name
n    -> forall {a}. AbsToCon (Maybe a)
mDefault
          | Bool
otherwise     -> Either Name QName
-> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
doQNameHelper (forall a b. a -> Either a b
Left Name
n) [MaybeSection (AppInfo, a)]
args'
        HdDef QName
qn
          | QName -> Bool
isExtendedLambdaName QName
qn
                          -> forall {a}. AbsToCon (Maybe a)
mDefault
          | Bool
otherwise     -> Either Name QName
-> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
doQNameHelper (forall a b. b -> Either a b
Right QName
qn) [MaybeSection (AppInfo, a)]
args'
        -- HdDef qn          -> doQNameHelper (Right qn) args'
        HdCon QName
qn          -> Either Name QName
-> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
doQNameHelper (forall a b. b -> Either a b
Right QName
qn) [MaybeSection (AppInfo, a)]
args'
        HdSyn QName
qn          -> Either Name QName
-> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
doQNameHelper (forall a b. b -> Either a b
Right QName
qn) [MaybeSection (AppInfo, a)]
args'
    | Bool
otherwise           -> forall {a}. AbsToCon (Maybe a)
mDefault
  where
  mDefault :: AbsToCon (Maybe a)
mDefault = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

  skipParens :: MaybeSection (AppInfo, a) -> Bool
  skipParens :: MaybeSection (AppInfo, a) -> Bool
skipParens = \case
     MaybeSection (AppInfo, a)
YesSection       -> Bool
False
     NoSection (AppInfo
i, a
e) -> a -> Bool
isLam a
e Bool -> Bool -> Bool
&& ParenPreference -> Bool
preferParenless (AppInfo -> ParenPreference
appParens AppInfo
i)

  doQNameHelper :: Either A.Name A.QName -> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
  doQNameHelper :: Either Name QName
-> [MaybeSection (AppInfo, a)] -> AbsToCon (Maybe c)
doQNameHelper Either Name QName
n [MaybeSection (AppInfo, a)]
args = do
    QName
x <- forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Name -> QName
C.QName forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete) forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Either Name QName
n
    let n' :: Name
n' = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id QName -> Name
A.qnameName Either Name QName
n
    -- #1346: The fixity of the abstract name is not necessarily correct, it depends on which
    -- concrete name we choose! Make sure to resolve ambiguities with n'.
    Fixity
fx <- QName -> [Name] -> AbsToCon ResolvedName
resolveName_ QName
x [Name
n'] forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ case
            VarName Name
y BindingSource
_                -> Name
y forall o i. o -> Lens' i o -> i
^. forall a. LensFixity a => Lens' Fixity a
lensFixity
            DefinedName Access
_ AbstractName
q Suffix
_          -> AbstractName
q forall o i. o -> Lens' i o -> i
^. forall a. LensFixity a => Lens' Fixity a
lensFixity
            FieldName (AbstractName
q :| [AbstractName]
_)         -> AbstractName
q forall o i. o -> Lens' i o -> i
^. forall a. LensFixity a => Lens' Fixity a
lensFixity
            ConstructorName Set Induction
_ (AbstractName
q :| [AbstractName]
_) -> AbstractName
q forall o i. o -> Lens' i o -> i
^. forall a. LensFixity a => Lens' Fixity a
lensFixity
            PatternSynResName (AbstractName
q :| [AbstractName]
_) -> AbstractName
q forall o i. o -> Lens' i o -> i
^. forall a. LensFixity a => Lens' Fixity a
lensFixity
            ResolvedName
UnknownName                -> Fixity
noFixity
    forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [MaybeSection (AppInfo, a)]
args {-then-} forall {a}. AbsToCon (Maybe a)
mDefault {-else-} forall a b. (a -> b) -> a -> b
$ \ List1 (MaybeSection (AppInfo, a))
as ->
      Fixity
-> QName
-> Name
-> List1 (MaybeSection (AppInfo, a))
-> NameParts
-> AbsToCon (Maybe c)
doQName Fixity
fx QName
x Name
n' List1 (MaybeSection (AppInfo, a))
as (Name -> NameParts
C.nameParts forall a b. (a -> b) -> a -> b
$ QName -> Name
C.unqualify QName
x)

  doQName :: Fixity -> C.QName -> A.Name -> List1 (MaybeSection (AppInfo, a)) -> NameParts -> AbsToCon (Maybe c)

  -- fall-back (wrong number of arguments or no holes)
  doQName :: Fixity
-> QName
-> Name
-> List1 (MaybeSection (AppInfo, a))
-> NameParts
-> AbsToCon (Maybe c)
doQName Fixity
_ QName
x Name
_ List1 (MaybeSection (AppInfo, a))
as NameParts
xs
    | forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length List1 (MaybeSection (AppInfo, a))
as forall a. Eq a => a -> a -> Bool
/= forall a. NumHoles a => a -> VerboseLevel
numHoles QName
x = forall {a}. AbsToCon (Maybe a)
mDefault

  -- binary case
  doQName Fixity
fixity QName
x Name
n (MaybeSection (AppInfo, a)
a1 :| [MaybeSection (AppInfo, a)]
as) NameParts
xs
    | NamePart
Hole <- forall a. NonEmpty a -> a
List1.head NameParts
xs
    , NamePart
Hole <- forall a. NonEmpty a -> a
List1.last NameParts
xs = do
        let ([MaybeSection (AppInfo, a)]
as', MaybeSection (AppInfo, a)
an) = forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [MaybeSection (AppInfo, a)]
as {-then-} forall a. HasCallStack => a
__IMPOSSIBLE__ {-else-} forall a. List1 a -> ([a], a)
List1.initLast
        forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          (PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c
bracket (Bool -> Fixity -> PrecedenceStack -> Bool
opBrackets' (MaybeSection (AppInfo, a) -> Bool
skipParens MaybeSection (AppInfo, a)
an) Fixity
fixity) forall a b. (a -> b) -> a -> b
$ do
            MaybeSection c
e1 <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx (Fixity -> Precedence
LeftOperandCtx Fixity
fixity) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) MaybeSection (AppInfo, a)
a1
            [MaybeSection c]
es <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
InsideOperandCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [MaybeSection (AppInfo, a)]
as'
            MaybeSection c
en <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fixity -> ParenPreference -> Precedence
RightOperandCtx Fixity
fixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. AppInfo -> ParenPreference
appParens) MaybeSection (AppInfo, a)
an
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QName -> Name -> List1 (MaybeSection c) -> c
opApp (forall a. HasRange a => a -> Range
getRange (MaybeSection c
e1, MaybeSection c
en)) QName
x Name
n (MaybeSection c
e1 forall a. a -> [a] -> NonEmpty a
:| [MaybeSection c]
es forall a. [a] -> [a] -> [a]
++ [MaybeSection c
en])

  -- prefix
  doQName Fixity
fixity QName
x Name
n List1 (MaybeSection (AppInfo, a))
as NameParts
xs
    | NamePart
Hole <- forall a. NonEmpty a -> a
List1.last NameParts
xs = do
        let ([MaybeSection (AppInfo, a)]
as', MaybeSection (AppInfo, a)
an) = forall a. List1 a -> ([a], a)
List1.initLast List1 (MaybeSection (AppInfo, a))
as
        forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          (PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c
bracket (Bool -> Fixity -> PrecedenceStack -> Bool
opBrackets' (MaybeSection (AppInfo, a) -> Bool
skipParens MaybeSection (AppInfo, a)
an) Fixity
fixity) forall a b. (a -> b) -> a -> b
$ do
            [MaybeSection c]
es <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
InsideOperandCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [MaybeSection (AppInfo, a)]
as'
            MaybeSection c
en <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\ (AppInfo
i, a
e) -> forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx (Fixity -> ParenPreference -> Precedence
RightOperandCtx Fixity
fixity forall a b. (a -> b) -> a -> b
$ AppInfo -> ParenPreference
appParens AppInfo
i) a
e) MaybeSection (AppInfo, a)
an
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QName -> Name -> List1 (MaybeSection c) -> c
opApp (forall a. HasRange a => a -> Range
getRange (Name
n, MaybeSection c
en)) QName
x Name
n (forall a. [a] -> a -> List1 a
List1.snoc [MaybeSection c]
es MaybeSection c
en)

  -- postfix
  doQName Fixity
fixity QName
x Name
n List1 (MaybeSection (AppInfo, a))
as NameParts
xs
    | NamePart
Hole <- forall a. NonEmpty a -> a
List1.head NameParts
xs = do
        let a1 :: MaybeSection (AppInfo, a)
a1  = forall a. NonEmpty a -> a
List1.head List1 (MaybeSection (AppInfo, a))
as
            as' :: [MaybeSection (AppInfo, a)]
as' = forall a. NonEmpty a -> [a]
List1.tail List1 (MaybeSection (AppInfo, a))
as
        MaybeSection c
e1 <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx (Fixity -> Precedence
LeftOperandCtx Fixity
fixity) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) MaybeSection (AppInfo, a)
a1
        [MaybeSection c]
es <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
InsideOperandCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [MaybeSection (AppInfo, a)]
as'
        forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          (PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c
bracket (Fixity -> PrecedenceStack -> Bool
opBrackets Fixity
fixity) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QName -> Name -> List1 (MaybeSection c) -> c
opApp (forall a. HasRange a => a -> Range
getRange (MaybeSection c
e1, Name
n)) QName
x Name
n (MaybeSection c
e1 forall a. a -> [a] -> NonEmpty a
:| [MaybeSection c]
es)

  -- roundfix
  doQName Fixity
_ QName
x Name
n List1 (MaybeSection (AppInfo, a))
as NameParts
_ = do
    List1 (MaybeSection c)
es <- (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
InsideOperandCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) List1 (MaybeSection (AppInfo, a))
as
    forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      (PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c
bracket PrecedenceStack -> Bool
roundFixBrackets forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QName -> Name -> List1 (MaybeSection c) -> c
opApp (forall a. HasRange a => a -> Range
getRange QName
x) QName
x Name
n List1 (MaybeSection c)
es

-- Recovering pattern synonyms --------------------------------------------

-- | Recover pattern synonyms for expressions.
tryToRecoverPatternSyn :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
tryToRecoverPatternSyn :: Expr -> AbsToCon Expr -> AbsToCon Expr
tryToRecoverPatternSyn Expr
e AbsToCon Expr
fallback
  | Expr -> Bool
userWritten Expr
e = AbsToCon Expr
fallback
  | Expr -> Bool
litOrCon Expr
e    = forall a.
ToConcrete a =>
(QName -> [NamedArg a] -> a)
-> (PatternSynDefn -> a -> Maybe [Arg a])
-> a
-> AbsToCon (ConOfAbs a)
-> AbsToCon (ConOfAbs a)
recoverPatternSyn QName -> [NamedArg Expr] -> Expr
apply PatternSynDefn -> Expr -> Maybe [Arg Expr]
matchPatternSyn Expr
e AbsToCon Expr
fallback
  | Bool
otherwise     = AbsToCon Expr
fallback
  where
    userWritten :: Expr -> Bool
userWritten (A.App AppInfo
info Expr
_ NamedArg Expr
_) = forall a. LensOrigin a => a -> Origin
getOrigin AppInfo
info forall a. Eq a => a -> a -> Bool
== Origin
UserWritten
    userWritten Expr
_                = Bool
False  -- this means we always use pattern synonyms for nullary constructors

    -- Only literals or constructors can head pattern synonym definitions
    litOrCon :: Expr -> Bool
litOrCon Expr
e =
      case Expr -> AppView
A.appView Expr
e of
        Application Con{}   [NamedArg Expr]
_ -> Bool
True
        Application A.Lit{} [NamedArg Expr]
_ -> Bool
True
        AppView
_                     -> Bool
False

    apply :: QName -> [NamedArg Expr] -> Expr
apply QName
c [NamedArg Expr]
args = AppView -> Expr
A.unAppView forall a b. (a -> b) -> a -> b
$ forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application (AmbiguousQName -> Expr
A.PatternSyn forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
c) [NamedArg Expr]
args

-- | Recover pattern synonyms in patterns.
tryToRecoverPatternSynP :: A.Pattern -> AbsToCon C.Pattern -> AbsToCon C.Pattern
tryToRecoverPatternSynP :: Pattern -> AbsToCon Pattern -> AbsToCon Pattern
tryToRecoverPatternSynP = forall a.
ToConcrete a =>
(QName -> [NamedArg a] -> a)
-> (PatternSynDefn -> a -> Maybe [Arg a])
-> a
-> AbsToCon (ConOfAbs a)
-> AbsToCon (ConOfAbs a)
recoverPatternSyn forall {e}. QName -> NAPs e -> Pattern' e
apply forall e. PatternSynDefn -> Pattern' e -> Maybe [Arg (Pattern' e)]
matchPatternSynP
  where apply :: QName -> NAPs e -> Pattern' e
apply QName
c NAPs e
args = forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP PatInfo
patNoRange (QName -> AmbiguousQName
unambiguous QName
c) NAPs e
args

-- | General pattern synonym recovery parameterised over expression type
recoverPatternSyn :: ToConcrete a =>
  (A.QName -> [NamedArg a] -> a)         -> -- applySyn
  (PatternSynDefn -> a -> Maybe [Arg a]) -> -- match
  a -> AbsToCon (ConOfAbs a) -> AbsToCon (ConOfAbs a)
recoverPatternSyn :: forall a.
ToConcrete a =>
(QName -> [NamedArg a] -> a)
-> (PatternSynDefn -> a -> Maybe [Arg a])
-> a
-> AbsToCon (ConOfAbs a)
-> AbsToCon (ConOfAbs a)
recoverPatternSyn QName -> [NamedArg a] -> a
applySyn PatternSynDefn -> a -> Maybe [Arg a]
match a
e AbsToCon (ConOfAbs a)
fallback = do
  Bool
doFold <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Bool
foldPatternSynonyms
  if Bool -> Bool
not Bool
doFold then AbsToCon (ConOfAbs a)
fallback else do
    PatternSynDefns
psyns  <- forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getAllPatternSyns
    ScopeInfo
scope  <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.patsyn" VerboseLevel
100 forall a b. (a -> b) -> a -> b
$ Doc -> RawName
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$
      [ Doc
"Scope when attempting to recover pattern synonyms:"
      , forall a. Pretty a => a -> Doc
pretty ScopeInfo
scope
      ]
    let isConP :: Pattern' e -> Bool
isConP ConP{} = Bool
True    -- #2828: only fold pattern synonyms with
        isConP Pattern' e
_      = Bool
False   --        constructor rhs
        cands :: [(QName, [Arg a], VerboseLevel)]
cands = [ (QName
q, [Arg a]
args, Pattern' Void -> VerboseLevel
score Pattern' Void
rhs)
                | (QName
q, psyndef :: PatternSynDefn
psyndef@([Arg Name]
_, Pattern' Void
rhs)) <- forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList PatternSynDefns
psyns
                , forall {e}. Pattern' e -> Bool
isConP Pattern' Void
rhs
                , Just [Arg a]
args <- [PatternSynDefn -> a -> Maybe [Arg a]
match PatternSynDefn
psyndef a
e]
                -- #3879: only fold pattern synonyms with an unqualified concrete name in scope
                -- Note that we only need to consider the head of the inverse lookup result: they
                -- are already sorted from shortest to longest!
                , C.QName{} <- forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ QName -> ScopeInfo -> [QName]
inverseScopeLookupName QName
q ScopeInfo
scope
                ]
        cmp :: (a, b, a) -> (a, b, a) -> Ordering
cmp (a
_, b
_, a
x) (a
_, b
_, a
y) = forall a. Ord a => a -> a -> Ordering
compare a
y a
x
    forall (m :: * -> *).
MonadDebug m =>
RawName -> VerboseLevel -> RawName -> m ()
reportSLn RawName
"toConcrete.patsyn" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ Doc -> RawName
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$
      [ Doc
"Found pattern synonym candidates:"
      , forall a. Pretty a => [a] -> Doc
prettyList_ forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ (QName
q,[Arg a]
_,VerboseLevel
_) -> QName
q) [(QName, [Arg a], VerboseLevel)]
cands
      ]
    case forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {a} {a} {b} {a} {b}.
Ord a =>
(a, b, a) -> (a, b, a) -> Ordering
cmp [(QName, [Arg a], VerboseLevel)]
cands of
      (QName
q, [Arg a]
args, VerboseLevel
_) : [(QName, [Arg a], VerboseLevel)]
_ -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg a] -> a
applySyn QName
q forall a b. (a -> b) -> a -> b
$ (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a name. a -> Named name a
unnamed [Arg a]
args
      []               -> AbsToCon (ConOfAbs a)
fallback
  where
    -- Heuristic to pick the best pattern synonym: the one that folds the most
    -- constructors.
    score :: Pattern' Void -> Int
    score :: Pattern' Void -> VerboseLevel
score = forall a. Sum a -> a
getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern forall {a} {e}. Num a => Pattern' e -> a
con
      where con :: Pattern' e -> a
con ConP{} = a
1
            con Pattern' e
_      = a
0

-- Some instances that are related to interaction with users -----------

instance ToConcrete InteractionId where
    type ConOfAbs InteractionId = C.Expr
    toConcrete :: InteractionId -> AbsToCon (ConOfAbs InteractionId)
toConcrete (InteractionId VerboseLevel
i) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Maybe VerboseLevel -> Expr
C.QuestionMark forall a. Range' a
noRange (forall a. a -> Maybe a
Just VerboseLevel
i)

instance ToConcrete NamedMeta where
    type ConOfAbs NamedMeta = C.Expr
    toConcrete :: NamedMeta -> AbsToCon (ConOfAbs NamedMeta)
toConcrete NamedMeta
i =
      Range -> Maybe RawName -> Expr
C.Underscore forall a. Range' a
noRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> RawName
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NamedMeta
i