{-# LANGUAGE CPP #-}
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
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.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
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.Debug
import Agda.TypeChecking.Monad.Builtin
import Agda.Interaction.Options
import qualified Agda.Utils.AssocList as AssocList
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.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
import Agda.Utils.Singleton
import Agda.Utils.Suffix
import Agda.Utils.Impossible
data Env = Env { Env -> Set Name
takenVarNames :: Set A.Name
, Env -> Set Name
takenDefNames :: Set C.Name
, Env -> ScopeInfo
currentScope :: ScopeInfo
, Env -> Map RawName QName
builtins :: Map String A.QName
, Env -> Bool
preserveIIds :: Bool
, Env -> Bool
foldPatternSynonyms :: Bool
}
makeEnv :: MonadAbsToCon m => ScopeInfo -> m Env
makeEnv :: forall (m :: * -> *). MonadAbsToCon m => ScopeInfo -> m Env
makeEnv ScopeInfo
scope = do
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
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 Name
takenDefNames = Set Name
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
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)
defs :: Set Name
defs = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all AbstractName -> Bool
notGeneralizeName) forall a b. (a -> b) -> a -> b
$
NameSpace -> Map Name [AbstractName]
nsNames forall a b. (a -> b) -> a -> b
$ ScopeInfo -> NameSpace
everythingInScope ScopeInfo
scope
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 }
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__ [])
}
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
resolveName :: KindsOfNames -> Maybe (Set A.Name) -> C.QName -> AbsToCon (Either (NonEmpty A.QName) ResolvedName)
resolveName :: KindsOfNames
-> Maybe (Set Name)
-> QName
-> AbsToCon (Either (NonEmpty QName) 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 (NonEmpty QName) m) =>
KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
tryResolveName KindsOfNames
kinds Maybe (Set Name)
candidates QName
q
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 (NonEmpty QName) 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
type MonadAbsToCon m =
( MonadTCEnv m
, ReadTCState m
, MonadStConcreteNames m
, HasOptions m
, HasBuiltins m
, MonadDebug m
)
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
}
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
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
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
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
getVerbosity :: AbsToCon Verbosity
getVerbosity = forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
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
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
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
loop :: [QName] -> AbsToCon QName
loop (qy :: QName
qy@Qual{} : [QName]
_ ) = forall (m :: * -> *) a. Monad m => a -> m a
return QName
qy
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
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"
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
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))
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
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]
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 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 :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' (Map Name [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
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)
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
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.
(Functor f, 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
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
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
Maybe Name
_ -> do
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
let shouldAvoid :: Name -> Bool
shouldAvoid = (forall a. Ord a => a -> Set a -> Bool
`Set.member` (Set RawName
taken forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set RawName
toAvoid)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> RawName
C.nameToRawName
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
xs <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> Set Name
takenDefNames
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 forall a b. (a -> b) -> a -> b
$ Set Name
xs forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
ys
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
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
bracket' :: (e -> e)
-> (PrecedenceStack -> Bool)
-> 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
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
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
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
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 ]
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
class ToConcrete a where
type ConOfAbs a
toConcrete :: a -> AbsToCon (ConOfAbs a)
bindToConcrete :: a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b
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
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
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
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
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
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
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
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
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
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
$
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
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
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
NonEmpty.head List1 AbstractName
xs)
ConstructorName Set Induction
_ List1 AbstractName
xs -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall a. NonEmpty a -> a
NonEmpty.head List1 AbstractName
xs)
PatternSynResName List1 AbstractName
xs -> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete (forall a. NonEmpty a -> a
NonEmpty.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
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)
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
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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
Range -> Maybe RawName -> Expr
C.Underscore (forall a. HasRange a => a -> Range
getRange MetaInfo
i) forall a b. (a -> b) -> a -> b
$
forall a. Pretty a => a -> RawName
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawName -> MetaId -> NamedMeta
NamedMeta (MetaInfo -> RawName
metaNameSuggestion MetaInfo
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> MetaId
MetaId forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> VerboseLevel
metaId 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
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
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
$
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')
(forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Expr
e')
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
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 TacticAttr
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
-> TacticAttr -> List1 (NamedArg Binder) -> Expr -> TypedBinding
A.TBind Range
r TacticAttr
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)
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])
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]
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. [a] -> NonEmpty a
List1.fromList 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
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. NonEmpty a -> [a] -> NonEmpty a
List1.appendList NonEmpty TypedBinding
tel) forall a b. (a -> b) -> a -> b
$ Expr -> (Telescope, Expr)
piTel Expr
e
piTel :: Expr -> (Telescope, 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 a. NonEmpty a -> [a]
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'
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.ETel Telescope
tel) = Telescope -> Expr
C.ETel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete Telescope
tel
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)
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
_ TacticAttr
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 TacticAttr
tac NamedArg Binder
x
Expr
_ -> LamBinding
b
makeDomainFree LamBinding
b = LamBinding
b
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
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 TacticAttr
t List1 (NamedArg Binder)
xs Expr
e) ConOfAbs TypedBinding -> 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
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
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
]
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
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 =
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
_ 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) (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
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
_ (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
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 Telescope
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 Telescope
tel forall a b. (a -> b) -> a -> b
$ \ ConOfAbs Telescope
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 Telescope
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')]]
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 -> Telescope
A.generalizeTel GeneralizeTelescope
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs Telescope
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 Telescope
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 -> Telescope
A.generalizeTel GeneralizeTelescope
bs) forall a b. (a -> b) -> a -> b
$ \ ConOfAbs Telescope
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 Telescope
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
_ Telescope
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 Telescope
tel forall a b. (a -> b) -> a -> b
$ \ ConOfAbs Telescope
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 Telescope
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
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.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
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
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 }
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
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
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
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
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
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
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
Name
cn <- Name -> AbsToCon Name
toConcreteName Name
v
KindsOfNames
-> Maybe (Set Name)
-> QName
-> AbsToCon (Either (NonEmpty QName) 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
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 NonEmpty QName
_ -> 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
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
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
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
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
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
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 a. NonEmpty a -> [a]
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
| 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
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
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) Range
-> QName -> Name -> NonEmpty (MaybeSection Pattern) -> 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 -> NonEmpty (MaybeSection Pattern) -> Pattern
opApp Range
r QName
x Name
n NonEmpty (MaybeSection Pattern)
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
$
forall a. NonEmpty a -> [a]
List1.toList NonEmpty (MaybeSection Pattern)
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
recoverOpApp :: forall a c . (ToConcrete a, c ~ ConOfAbs a, HasRange c)
=> ((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)
-> (a -> Bool)
-> (Range -> C.QName -> A.Name -> List1 (MaybeSection c) -> c)
-> (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'
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
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 forall {a}. AbsToCon (Maybe a)
mDefault 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)
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
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 forall a. HasCallStack => a
__IMPOSSIBLE__ 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])
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)
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)
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
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
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
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
recoverPatternSyn :: ToConcrete a =>
(A.QName -> [NamedArg a] -> a) ->
(PatternSynDefn -> a -> Maybe [Arg a]) ->
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
isConP Pattern' e
_ = Bool
False
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]
, 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
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
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 = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Maybe RawName -> Expr
C.Underscore forall a. Range' a
noRange (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> RawName
prettyShow NamedMeta
i)