{-# LANGUAGE NondecreasingIndentation #-}
module Agda.Syntax.Translation.InternalToAbstract
( Reify(..)
, MonadReify
, NamedClause(..)
, reifyPatterns
, reifyUnblocked
, blankNotInScope
, reifyDisplayFormP
) where
import Prelude hiding (null)
import Control.Applicative ( liftA2 )
import Control.Arrow ( (&&&) )
import Control.Monad ( filterM, forM )
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe
import Data.Semigroup ( Semigroup, (<>) )
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Traversable (mapM)
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A hiding (Binder)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Scope.Base (inverseScopeLookupName)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses'(Fail))
import Agda.TypeChecking.DisplayForm
import Agda.TypeChecking.Level
import {-# SOURCE #-} Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked :: forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked i
t = forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
stInstantiateBlocking (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i
t
apps :: MonadReify m => Expr -> [Arg Expr] -> m Expr
apps :: forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
e = forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
e forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
I.Apply
nelims :: MonadReify m => Expr -> [I.Elim' (Named_ Expr)] -> m Expr
nelims :: forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
e [] = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
nelims Expr
e (I.IApply Named_ Expr
x Named_ Expr
y Named_ Expr
r : [Elim' (Named_ Expr)]
es) =
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Named_ Expr
r) [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Apply Arg (Named_ Expr)
arg : [Elim' (Named_ Expr)]
es) = do
Arg (Named_ Expr)
arg <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Arg (Named_ Expr)
arg
Bool
dontShowImp <- Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
let hd :: Expr
hd | forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ Expr)
arg Bool -> Bool -> Bool
&& Bool
dontShowImp = Expr
e
| Bool
otherwise = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e Arg (Named_ Expr)
arg
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
hd [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Proj ProjOrigin
ProjPrefix QName
d : [Elim' (Named_ Expr)]
es) = forall (m :: * -> *).
MonadReify m =>
Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix Expr
e QName
d [Elim' (Named_ Expr)]
es
nelims Expr
e (I.Proj ProjOrigin
o QName
d : [Elim' (Named_ Expr)]
es) | Expr -> Bool
isSelf Expr
e = forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) [Elim' (Named_ Expr)]
es
| Bool
otherwise =
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
e (forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
o forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d)) [Elim' (Named_ Expr)]
es
nelimsProjPrefix :: MonadReify m => Expr -> QName -> [I.Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix :: forall (m :: * -> *).
MonadReify m =>
Expr -> QName -> [Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix Expr
e QName
d [Elim' (Named_ Expr)]
es =
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg Expr
e) [Elim' (Named_ Expr)]
es
isSelf :: Expr -> Bool
isSelf :: Expr -> Bool
isSelf = \case
A.Var Name
n -> Name -> Bool
nameIsRecordName Name
n
Expr
_ -> Bool
False
elims :: MonadReify m => Expr -> [I.Elim' Expr] -> m Expr
elims :: forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
e = forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
e 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 forall a name. a -> Named name a
unnamed)
noExprInfo :: ExprInfo
noExprInfo :: ExprInfo
noExprInfo = Range -> ExprInfo
ExprRange forall a. Range' a
noRange
reifyWhenE :: (Reify i, MonadReify m, Underscore (ReifiesTo i)) => Bool -> i -> m (ReifiesTo i)
reifyWhenE :: forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE Bool
True i
i = forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i
i
reifyWhenE Bool
False i
t = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Underscore a => a
underscore
type MonadReify m =
( PureTCM m
, MonadInteractionPoints m
, MonadFresh NameId m
)
class Reify i where
type ReifiesTo i
reify :: MonadReify m => i -> m (ReifiesTo i)
reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
_ = forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
instance Reify Bool where
type ReifiesTo Bool = Bool
reify :: forall (m :: * -> *). MonadReify m => Bool -> m (ReifiesTo Bool)
reify = forall (m :: * -> *) a. Monad m => a -> m a
return
instance Reify Name where
type ReifiesTo Name = Name
reify :: forall (m :: * -> *). MonadReify m => Name -> m (ReifiesTo Name)
reify = forall (m :: * -> *) a. Monad m => a -> m a
return
instance Reify Expr where
type ReifiesTo Expr = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Expr -> m (ReifiesTo Expr)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *). MonadReify m => Expr -> m (ReifiesTo Expr)
reify = forall (m :: * -> *) a. Monad m => a -> m a
return
instance Reify MetaId where
type ReifiesTo MetaId = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> MetaId -> m (ReifiesTo MetaId)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *).
MonadReify m =>
MetaId -> m (ReifiesTo MetaId)
reify MetaId
x = do
Bool
b <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
MetaInfo
mi <- MetaVariable -> MetaInfo
mvInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
let mi' :: MetaInfo
mi' = Info.MetaInfo
{ metaRange :: Range
metaRange = forall a. HasRange a => a -> Range
getRange forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange MetaInfo
mi
, metaScope :: ScopeInfo
metaScope = forall a. Closure a -> ScopeInfo
clScope forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange MetaInfo
mi
, metaNumber :: Maybe MetaId
metaNumber = if Bool
b then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just MetaId
x
, metaNameSuggestion :: String
metaNameSuggestion = if Bool
b then String
"" else MetaInfo -> String
miNameSuggestion MetaInfo
mi
}
underscore :: m Expr
underscore = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
A.Underscore MetaInfo
mi'
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe InteractionId
Nothing | Bool
b -> do
InteractionId
ii <- forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Nat -> m InteractionId
registerInteractionPoint Bool
False forall a. Range' a
noRange forall a. Maybe a
Nothing
forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaInfo -> InteractionId -> Expr
A.QuestionMark MetaInfo
mi' InteractionId
ii
Just InteractionId
ii | Bool
b -> m Expr
underscore
Maybe InteractionId
Nothing -> m Expr
underscore
Just InteractionId
ii -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaInfo -> InteractionId -> Expr
A.QuestionMark MetaInfo
mi' InteractionId
ii
instance Reify DisplayTerm where
type ReifiesTo DisplayTerm = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (ReifiesTo DisplayTerm)
reify = \case
DTerm Term
v -> forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
False Term
v
DDot Term
v -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs -> forall (m :: * -> *).
MonadReify m =>
QName -> ConInfo -> [Arg Expr] -> m Expr
recOrCon (ConHead -> QName
conName ConHead
c) ConInfo
ci forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify [Arg DisplayTerm]
vs
DDef QName
f [Elim' DisplayTerm]
es -> forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (QName -> Expr
A.Def QName
f) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify [Elim' DisplayTerm]
es
DWithApp DisplayTerm
u [DisplayTerm]
us Elims
es0 -> do
(Expr
e, [Expr]
es) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (DisplayTerm
u, [DisplayTerm]
us)
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (if forall a. Null a => a -> Bool
null [Expr]
es then Expr
e else ExprInfo -> Expr -> [Expr] -> Expr
A.WithApp ExprInfo
noExprInfo Expr
e [Expr]
es) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es0
reifyDisplayForm :: MonadReify m => QName -> I.Elims -> m A.Expr -> m A.Expr
reifyDisplayForm :: forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
f Elims
es m Expr
fallback =
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled m Expr
fallback forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
MonadDisplayForm m =>
QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
f Elims
es) m Expr
fallback forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
reifyDisplayFormP
:: MonadReify m
=> QName
-> A.Patterns
-> A.Patterns
-> m (QName, A.Patterns)
reifyDisplayFormP :: forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
ps Patterns
wps = do
let fallback :: m (QName, Patterns)
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Patterns
ps forall a. [a] -> [a] -> [a]
++ Patterns
wps)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled m (QName, Patterns)
fallback forall a b. (a -> b) -> a -> b
$ do
Maybe DisplayTerm
md <-
forall (m :: * -> *).
MonadDisplayForm m =>
QName -> Elims -> m (Maybe DisplayTerm)
displayForm QName
f forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Arg (Named_ Pattern)
p Nat
i -> forall a. Arg a -> Elim' a
I.Apply forall a b. (a -> b) -> a -> b
$ Arg (Named_ Pattern)
p forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Nat -> Term
I.var Nat
i) Patterns
ps [Nat
0..]
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
60 forall a b. (a -> b) -> a -> b
$
String
"display form of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Patterns
ps forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Patterns
wps forall a. [a] -> [a] -> [a]
++ String
":\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Maybe DisplayTerm
md
case Maybe DisplayTerm
md of
Just DisplayTerm
d | DisplayTerm -> Bool
okDisplayForm DisplayTerm
d -> do
(QName
f', Patterns
ps', Patterns
wps') <- forall (m :: * -> *).
MonadReify m =>
Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
displayLHS Patterns
ps DisplayTerm
d
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.display" Nat
70 forall a b. (a -> b) -> a -> b
$ do
Doc
doc <- forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall a b. (a -> b) -> a -> b
$ LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS forall a. Null a => a
empty QName
f' (Patterns
ps' forall a. [a] -> [a] -> [a]
++ Patterns
wps' forall a. [a] -> [a] -> [a]
++ Patterns
wps)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"rewritten lhs to"
, Doc
" lhs' = " Doc -> Doc -> Doc
<+> Doc
doc
]
forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f' Patterns
ps' (Patterns
wps' forall a. [a] -> [a] -> [a]
++ Patterns
wps)
Maybe DisplayTerm
_ -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
70 forall a b. (a -> b) -> a -> b
$ String
"display form absent or not valid as lhs"
m (QName, Patterns)
fallback
where
okDisplayForm :: DisplayTerm -> Bool
okDisplayForm :: DisplayTerm -> Bool
okDisplayForm (DWithApp DisplayTerm
d [DisplayTerm]
ds Elims
es) =
DisplayTerm -> Bool
okDisplayForm DisplayTerm
d Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DisplayTerm -> Bool
okDisplayTerm [DisplayTerm]
ds Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okToDropE Elims
es
okDisplayForm (DTerm (I.Def QName
f Elims
vs)) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
okDisplayForm (DDef QName
f [Elim' DisplayTerm]
es) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' DisplayTerm -> Bool
okDElim [Elim' DisplayTerm]
es
okDisplayForm DDot{} = Bool
False
okDisplayForm DCon{} = Bool
False
okDisplayForm DTerm{} = Bool
False
okDisplayTerm :: DisplayTerm -> Bool
okDisplayTerm :: DisplayTerm -> Bool
okDisplayTerm (DTerm Term
v) = Term -> Bool
okTerm Term
v
okDisplayTerm DDot{} = Bool
True
okDisplayTerm DCon{} = Bool
True
okDisplayTerm DDef{} = Bool
False
okDisplayTerm DisplayTerm
_ = Bool
False
okDElim :: Elim' DisplayTerm -> Bool
okDElim :: Elim' DisplayTerm -> Bool
okDElim (I.IApply DisplayTerm
x DisplayTerm
y DisplayTerm
r) = DisplayTerm -> Bool
okDisplayTerm DisplayTerm
r
okDElim (I.Apply Arg DisplayTerm
v) = DisplayTerm -> Bool
okDisplayTerm forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg DisplayTerm
v
okDElim I.Proj{} = Bool
True
okToDropE :: Elim' Term -> Bool
okToDropE :: Elim' Term -> Bool
okToDropE (I.Apply Arg Term
v) = Arg Term -> Bool
okToDrop Arg Term
v
okToDropE I.Proj{} = Bool
False
okToDropE (I.IApply Term
x Term
y Term
r) = Bool
False
okToDrop :: Arg I.Term -> Bool
okToDrop :: Arg Term -> Bool
okToDrop Arg Term
arg = forall a. LensHiding a => a -> Bool
notVisible Arg Term
arg Bool -> Bool -> Bool
&& case forall e. Arg e -> e
unArg Arg Term
arg of
I.Var Nat
_ [] -> Bool
True
I.DontCare{} -> Bool
True
I.Level{} -> Bool
True
Term
_ -> Bool
False
okArg :: Arg I.Term -> Bool
okArg :: Arg Term -> Bool
okArg = Term -> Bool
okTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg
okElim :: Elim' I.Term -> Bool
okElim :: Elim' Term -> Bool
okElim (I.IApply Term
x Term
y Term
r) = Term -> Bool
okTerm Term
r
okElim (I.Apply Arg Term
a) = Arg Term -> Bool
okArg Arg Term
a
okElim I.Proj{} = Bool
True
okTerm :: I.Term -> Bool
okTerm :: Term -> Bool
okTerm (I.Var Nat
_ []) = Bool
True
okTerm (I.Con ConHead
c ConInfo
ci Elims
vs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Elim' Term -> Bool
okElim Elims
vs
okTerm (I.Def QName
x []) = forall a. IsNoName a => a -> Bool
isNoName forall a b. (a -> b) -> a -> b
$ QName -> QName
qnameToConcrete QName
x
okTerm Term
_ = Bool
False
flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm])
flattenWith :: DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith (DWithApp DisplayTerm
d [DisplayTerm]
ds1 Elims
es2) =
let (QName
f, [Elim' DisplayTerm]
es, [Elim' DisplayTerm]
ds0) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith DisplayTerm
d
in (QName
f, [Elim' DisplayTerm]
es, [Elim' DisplayTerm]
ds0 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Arg a -> Elim' a
I.Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Arg a
defaultArg) [DisplayTerm]
ds1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es2)
flattenWith (DDef QName
f [Elim' DisplayTerm]
es) = (QName
f, [Elim' DisplayTerm]
es, [])
flattenWith (DTerm (I.Def QName
f Elims
es)) = (QName
f, forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
es, [])
flattenWith DisplayTerm
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
displayLHS
:: MonadReify m
=> A.Patterns
-> DisplayTerm
-> m (QName, A.Patterns, A.Patterns)
displayLHS :: forall (m :: * -> *).
MonadReify m =>
Patterns -> DisplayTerm -> m (QName, Patterns, Patterns)
displayLHS Patterns
ps DisplayTerm
d = do
let (QName
f, [Elim' DisplayTerm]
vs, [Elim' DisplayTerm]
es) = DisplayTerm -> (QName, [Elim' DisplayTerm], [Elim' DisplayTerm])
flattenWith DisplayTerm
d
Patterns
ps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
MonadReify m =>
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat [Elim' DisplayTerm]
vs
Patterns
wps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP forall a. Null a => a
empty) forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
MonadReify m =>
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat) [Elim' DisplayTerm]
es
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Patterns
ps, Patterns
wps)
where
argToPat :: MonadReify m => Arg DisplayTerm -> m (NamedArg A.Pattern)
argToPat :: forall (m :: * -> *).
MonadReify m =>
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat Arg DisplayTerm
arg = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (Named_ Pattern)
termToPat Arg DisplayTerm
arg
elimToPat :: MonadReify m => I.Elim' DisplayTerm -> m (NamedArg A.Pattern)
elimToPat :: forall (m :: * -> *).
MonadReify m =>
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat (I.IApply DisplayTerm
_ DisplayTerm
_ DisplayTerm
r) = forall (m :: * -> *).
MonadReify m =>
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo DisplayTerm
r)
elimToPat (I.Apply Arg DisplayTerm
arg) = forall (m :: * -> *).
MonadReify m =>
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat Arg DisplayTerm
arg
elimToPat (I.Proj ProjOrigin
o QName
d) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
o forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d
termToPat :: MonadReify m => DisplayTerm -> m (Named_ A.Pattern)
termToPat :: forall (m :: * -> *).
MonadReify m =>
DisplayTerm -> m (Named_ Pattern)
termToPat (DTerm (I.Var Nat
n [])) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Patterns
ps forall a. [a] -> Nat -> Maybe a
!!! Nat
n
termToPat (DCon ConHead
c ConInfo
ci [Arg DisplayTerm]
vs) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ci PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) 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 :: * -> *).
MonadReify m =>
Arg DisplayTerm -> m (Arg (Named_ Pattern))
argToPat [Arg DisplayTerm]
vs
termToPat (DTerm (I.Con ConHead
c ConInfo
ci Elims
vs)) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP (ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ci PatInfo
patNoRange ConPatLazy
ConPatEager) (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) 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 :: * -> *).
MonadReify m =>
Elim' DisplayTerm -> m (Arg (Named_ Pattern))
elimToPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Elims
vs
termToPat (DTerm (I.Def QName
_ [])) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
termToPat (DDef QName
_ []) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
termToPat (DTerm (I.Lit Literal
l)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Literal -> Pattern' e
A.LitP PatInfo
patNoRange Literal
l
termToPat (DDot Term
v) = forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadReify m => Term -> m Expr
termToExpr Term
v
termToPat DisplayTerm
v = forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify DisplayTerm
v
len :: Nat
len = forall (t :: * -> *) a. Foldable t => t a -> Nat
length Patterns
ps
argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr]
argsToExpr :: forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr = 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 (m :: * -> *). MonadReify m => Term -> m Expr
termToExpr)
termToExpr :: MonadReify m => Term -> m A.Expr
termToExpr :: forall (m :: * -> *). MonadReify m => Term -> m Expr
termToExpr Term
v = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.display" Nat
60 forall a b. (a -> b) -> a -> b
$ String
"termToExpr " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
v
case Term -> Term
unSpine Term
v of
I.Con ConHead
c ConInfo
ci Elims
es -> do
let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c))) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
I.Def QName
f Elims
es -> do
let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (QName -> Expr
A.Def QName
f) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
I.Var Nat
n Elims
es -> do
let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. Elim' a -> Maybe (Arg a)
isApplyElim Elims
es
Expr
e <- if Nat
n forall a. Ord a => a -> a -> Bool
< Nat
len
then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pattern -> Expr
A.patternToExpr forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Nat -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Patterns
ps Nat
n
else forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Nat -> Term
I.var (Nat
n forall a. Num a => a -> a -> a
- Nat
len))
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadReify m => Args -> m [Arg Expr]
argsToExpr Args
vs
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Underscore a => a
underscore
instance Reify Literal where
type ReifiesTo Literal = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Literal -> m (ReifiesTo Literal)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *).
MonadReify m =>
Literal -> m (ReifiesTo Literal)
reify Literal
l = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit forall a. Null a => a
empty Literal
l
instance Reify Term where
type ReifiesTo Term = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Term -> m (ReifiesTo Term)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v = forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
True Term
v
reifyPathPConstAsPath :: MonadReify m => QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath :: forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x es :: Elims
es@[I.Apply Arg Term
l, I.Apply Arg Term
t, I.Apply Arg Term
lhs, I.Apply Arg Term
rhs] = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
100 forall a b. (a -> b) -> a -> b
$ String
"reifying def path " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (QName
x,Elims
es)
Maybe QName
mpath <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinPath
Maybe QName
mpathp <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinPathP
let fallback :: m (QName, Elims)
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x,Elims
es)
case (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe QName
mpath forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe QName
mpathp of
Just (QName
path,QName
pathp) | QName
x forall a. Eq a => a -> a -> Bool
== QName
pathp -> do
let a :: Maybe Term
a = case forall e. Arg e -> e
unArg Arg Term
t of
I.Lam ArgInfo
_ (NoAbs String
_ Term
b) -> forall a. a -> Maybe a
Just Term
b
I.Lam ArgInfo
_ (Abs String
_ Term
b)
| Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Nat
0 forall a. Free a => Nat -> a -> Bool
`freeIn` Term
b -> forall a. a -> Maybe a
Just (forall a. Subst a => Impossible -> a -> a
strengthen HasCallStack => Impossible
impossible Term
b)
Term
_ -> forall a. Maybe a
Nothing
case Maybe Term
a of
Just Term
a -> forall (m :: * -> *) a. Monad m => a -> m a
return (QName
path, [forall a. Arg a -> Elim' a
I.Apply Arg Term
l, forall a. Arg a -> Elim' a
I.Apply (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Term
a), forall a. Arg a -> Elim' a
I.Apply Arg Term
lhs, forall a. Arg a -> Elim' a
I.Apply Arg Term
rhs])
Maybe Term
Nothing -> m (QName, Elims)
fallback
Maybe (QName, QName)
_ -> m (QName, Elims)
fallback
reifyPathPConstAsPath QName
x Elims
es = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
x,Elims
es)
reifyTerm :: MonadReify m => Bool -> Term -> m Expr
reifyTerm :: forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
expandAnonDefs0 Term
v0 = do
Bool
metasBare <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintMetasBare
Term
v <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
I.MetaV MetaId
x Elims
_ | Bool
metasBare -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x []
Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
Bool
expandAnonDefs <- forall (m :: * -> *) a. Monad m => a -> m a
return Bool
expandAnonDefs0 forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled
Bool
havePfp <- PragmaOptions -> Bool
optPostfixProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
let pred :: ProjOrigin -> Bool
pred = if Bool
havePfp then (forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPrefix) else (forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPostfix)
case (ProjOrigin -> Bool) -> Term -> Term
unSpine' ProjOrigin -> Bool
pred Term
v of
Term
_ | I.Var Nat
n (I.Proj ProjOrigin
_ QName
p : Elims
es) <- Term
v,
Just String
name <- QName -> Maybe String
getGeneralizedFieldName QName
p -> do
let fakeName :: Name
fakeName = (QName -> Name
qnameName QName
p) {nameConcrete :: Name
nameConcrete = String -> Name
C.simpleName String
name}
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
fakeName) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
I.Var Nat
n Elims
es -> do
Name
x <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ forall a b. (a -> b) -> a -> b
$ String
"@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Nat
n) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m (Maybe Name)
nameOfBV' Nat
n
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (Name -> Expr
A.Var Name
x) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
I.Def QName
x Elims
es -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.def" Nat
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"reifying def" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
x
(QName
x, Elims
es) <- forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath QName
x Elims
es
forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
es forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadReify m =>
Bool -> QName -> Elims -> m Expr
reifyDef Bool
expandAnonDefs QName
x Elims
es
I.Con ConHead
c ConInfo
ci Elims
vs -> do
let x :: QName
x = ConHead -> QName
conName ConHead
c
Bool
isR <- forall (m :: * -> *).
(MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
isGeneratedRecordConstructor QName
x
if Bool
isR Bool -> Bool -> Bool
|| ConInfo
ci forall a. Eq a => a -> a -> Bool
== ConInfo
ConORec
then do
Bool
showImp <- forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
let keep :: (Dom' Term Name, Expr) -> Bool
keep (Dom' Term Name
a, Expr
v) = Bool
showImp Bool -> Bool -> Bool
|| forall a. LensHiding a => a -> Bool
visible Dom' Term Name
a
QName
r <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
x
[Dom' Term Name]
xs <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom' Term Name])
getRecordFieldNames_ QName
r
[Expr]
vs <- forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
vs)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
noExprInfo forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Name -> a -> FieldAssignment' a
FieldAssignment forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall t e. Dom' t e -> e
unDom) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Dom' Term Name, Expr) -> Bool
keep forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Dom' Term Name]
xs [Expr]
vs
else forall (m :: * -> *).
MonadReify m =>
QName -> Elims -> m Expr -> m Expr
reifyDisplayForm QName
x Elims
vs forall a b. (a -> b) -> a -> b
$ do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
let Constructor {conPars :: Defn -> Nat
conPars = Nat
np} = Definition -> Defn
theDef Definition
def
Nat
n <- forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Nat
getDefFreeVars QName
x
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Nat
n forall a. Ord a => a -> a -> Bool
> Nat
np) forall a. HasCallStack => a
__IMPOSSIBLE__
let h :: Expr
h = AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
x)
if forall a. Null a => a -> Bool
null Elims
vs
then forall (m :: * -> *) a. Monad m => a -> m a
return Expr
h
else do
[Arg Expr]
es <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Elim' a -> Maybe (Arg a)
isApplyElim) Elims
vs)
if Nat
np forall a. Eq a => a -> a -> Bool
== Nat
0
then forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
es
else do
TelV Telescope
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Definition -> Type
defType Definition
def)
let ([Dom (String, Type)]
pars, [Dom (String, Type)]
rest) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
np forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
case [Dom (String, Type)]
rest of
(Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} : [Dom (String, Type)]
_) | forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info -> do
let us :: [Arg Expr]
us = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall a. Nat -> [a] -> [a]
drop Nat
n [Dom (String, Type)]
pars) forall a b. (a -> b) -> a -> b
$ \(Dom {domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai}) ->
forall a. LensHiding a => a -> a
hideOrKeepInstance forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a. Underscore a => a
underscore
forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h forall a b. (a -> b) -> a -> b
$ [Arg Expr]
us forall a. [a] -> [a] -> [a]
++ [Arg Expr]
es
[Dom (String, Type)]
_ -> forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps Expr
h [Arg Expr]
es
I.Lam ArgInfo
info Abs Term
b -> do
(Name
x,Expr
e) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Term
b
ArgInfo
info <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
UserWritten ArgInfo
info) (forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
mkDomainFree forall a b. (a -> b) -> a -> b
$ forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x) Expr
e
I.Lit Literal
l -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Literal
l
I.Level Level
l -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
l
I.Pi Dom Type
a Abs Type
b -> case Abs Type
b of
NoAbs String
_ Type
b'
| forall a. LensHiding a => a -> Bool
visible Dom Type
a, Bool -> Bool
not (forall t e. Dom' t e -> Bool
domIsFinite Dom Type
a) -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun forall a b. (a -> b) -> a -> b
$ ExprInfo
noExprInfo) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Dom Type
a, Type
b')
| Bool
otherwise -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Dom Type
a
Abs Type
b -> Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall {m :: * -> *} {a} {t}.
(MonadTCEnv m, Free a, Free t) =>
t -> a -> m Bool
domainFree Dom Type
a (forall a. Subst a => Abs a -> a
absBody Abs Type
b))
(forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) forall a. Underscore a => a
underscore)
(forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Dom Type
a)
where
mkPi :: Abs Type -> Arg Expr -> m Expr
mkPi Abs Type
b (Arg ArgInfo
info Expr
a') = do
Maybe Expr
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> Maybe t
domTactic Dom Type
a
(Name
x, Expr
b) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Type
b
let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named (forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
domName Dom Type
a) forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
noExprInfo
(forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind forall a. Range' a
noRange (Maybe Expr -> Bool -> TypedBindingInfo
TypedBindingInfo Maybe Expr
tac (forall t e. Dom' t e -> Bool
domIsFinite Dom Type
a)) List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
a')
Expr
b
domainFree :: t -> a -> m Bool
domainFree t
a a
b = do
Bool
df <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envPrintDomainFreePi
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
df Bool -> Bool -> Bool
&& forall a. Free a => Nat -> a -> Bool
freeIn Nat
0 a
b Bool -> Bool -> Bool
&& forall t. Free t => t -> Bool
closed t
a
I.Sort Sort
s -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
s
I.MetaV MetaId
x Elims
es -> do
Expr
x' <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify MetaId
x
[Elim' Expr]
es' <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
(Maybe (Substitution' Term)
msub1,Telescope
meta_tel,Maybe (Substitution' Term)
msub2) <- do
CheckpointId
local_chkpt <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
(CheckpointId
chkpt, Telescope
tel, Maybe (Substitution' Term)
msub2) <- forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure MetaVariable
mv forall a b. (a -> b) -> a -> b
$ \ Range
_ ->
(,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC (Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
local_chkpt)
(,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC (Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
chkpt) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope
tel forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Substitution' Term)
msub2
Bool
opt_show_ids <- forall (m :: * -> *). HasOptions m => m Bool
showIdentitySubstitutions
let
addNames :: [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [] [Elim' a]
es = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) [Elim' a]
es
addNames [name]
_ [] = []
addNames [name]
xs (I.Proj{} : [Elim' a]
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
addNames [name]
xs (I.IApply a
x a
y a
r : [Elim' a]
es) =
[name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [name]
xs (forall a. Arg a -> Elim' a
I.Apply (forall a. a -> Arg a
defaultArg a
r) forall a. a -> [a] -> [a]
: [Elim' a]
es)
addNames (name
x:[name]
xs) (I.Apply Arg a
arg : [Elim' a]
es) =
forall a. Arg a -> Elim' a
I.Apply (forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just name
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Substitution Arg a
arg)) forall a. a -> [a] -> [a]
: [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [name]
xs [Elim' a]
es
p :: Permutation
p = MetaVariable -> Permutation
mvPermutation MetaVariable
mv
applyPerm :: Permutation -> [a] -> [a]
applyPerm Permutation
p [a]
vs = forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
takeP (forall a. Sized a => a -> Nat
size [a]
vs) Permutation
p) [a]
vs
names :: [WithOrigin (Ranged String)]
names = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Ranged a
unranged) forall a b. (a -> b) -> a -> b
$ Permutation
p forall a. Permutation -> [a] -> [a]
`applyPerm` Telescope -> [String]
teleNames Telescope
meta_tel
named_es' :: [Elim' (Named_ Expr)]
named_es' = forall {name} {a}. [name] -> [Elim' a] -> [Elim' (Named name a)]
addNames [WithOrigin (Ranged String)]
names [Elim' Expr]
es'
dropIdentitySubs :: Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
dropIdentitySubs Substitution' Term
sub_local2G Substitution' Term
sub_tel2G =
let
args_G :: Args
args_G = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sub_tel2G forall a b. (a -> b) -> a -> b
$ Permutation
p forall a. Permutation -> [a] -> [a]
`applyPerm` (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
meta_tel :: [Arg Term])
es_G :: Elims
es_G = Substitution' Term
sub_local2G forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Elims
es
sameVar :: Arg a -> Elim' a -> Bool
sameVar Arg a
x (I.Apply Arg a
y) = forall a. Maybe a -> Bool
isJust Maybe Nat
xv Bool -> Bool -> Bool
&& Maybe Nat
xv forall a. Eq a => a -> a -> Bool
== forall a. DeBruijn a => a -> Maybe Nat
deBruijnView (forall e. Arg e -> e
unArg Arg a
y)
where
xv :: Maybe Nat
xv = forall a. DeBruijn a => a -> Maybe Nat
deBruijnView forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg a
x
sameVar Arg a
_ Elim' a
_ = Bool
False
dropArg :: [Bool]
dropArg = forall a. Nat -> [a] -> [a]
take (forall a. Sized a => a -> Nat
size [WithOrigin (Ranged String)]
names) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a} {a}.
(DeBruijn a, DeBruijn a) =>
Arg a -> Elim' a -> Bool
sameVar Args
args_G Elims
es_G
doDrop :: [Bool] -> [a] -> [a]
doDrop (Bool
b : [Bool]
xs) (a
e : [a]
es) = (if Bool
b then forall a. a -> a
id else (a
e forall a. a -> [a] -> [a]
:)) forall a b. (a -> b) -> a -> b
$ [Bool] -> [a] -> [a]
doDrop [Bool]
xs [a]
es
doDrop [] [a]
es = [a]
es
doDrop [Bool]
_ [] = []
in forall {a}. [Bool] -> [a] -> [a]
doDrop [Bool]
dropArg forall a b. (a -> b) -> a -> b
$ [Elim' (Named_ Expr)]
named_es'
simpl_named_es' :: [Elim' (Named_ Expr)]
simpl_named_es' | Bool
opt_show_ids = [Elim' (Named_ Expr)]
named_es'
| Just Substitution' Term
sub_mtel2local <- Maybe (Substitution' Term)
msub1 = Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
dropIdentitySubs forall a. Substitution' a
IdS Substitution' Term
sub_mtel2local
| Just Substitution' Term
sub_local2mtel <- Maybe (Substitution' Term)
msub2 = Substitution' Term -> Substitution' Term -> [Elim' (Named_ Expr)]
dropIdentitySubs Substitution' Term
sub_local2mtel forall a. Substitution' a
IdS
| Bool
otherwise = [Elim' (Named_ Expr)]
named_es'
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
x' [Elim' (Named_ Expr)]
simpl_named_es'
I.DontCare Term
v -> do
Bool
showIrr <- PragmaOptions -> Bool
optShowIrrelevant forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
if | Bool
showIrr -> forall (m :: * -> *). MonadReify m => Bool -> Term -> m Expr
reifyTerm Bool
expandAnonDefs Term
v
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Underscore a => a
underscore
I.Dummy String
s [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ Text -> Literal
LitString (String -> Text
T.pack String
s)
I.Dummy String
"applyE" Elims
es | I.Apply (Arg ArgInfo
_ Term
h) : Elims
es' <- Elims
es -> do
Expr
h <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
h
[Elim' Expr]
es' <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es'
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
h [Elim' Expr]
es'
| Bool
otherwise -> forall a. HasCallStack => a
__IMPOSSIBLE__
I.Dummy String
s Elims
es -> do
Expr
s <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (String -> Elims -> Term
I.Dummy String
s [])
[Elim' Expr]
es <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
es
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
s [Elim' Expr]
es
where
reifyDef :: MonadReify m => Bool -> QName -> I.Elims -> m Expr
reifyDef :: forall (m :: * -> *).
MonadReify m =>
Bool -> QName -> Elims -> m Expr
reifyDef Bool
True QName
x Elims
es =
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ScopeInfo -> [QName]
inverseScopeLookupName QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope) (forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es) forall a b. (a -> b) -> a -> b
$ do
Reduced () Term
r <- forall (m :: * -> *).
PureTCM m =>
QName -> Elims -> m (Reduced () Term)
reduceDefCopy QName
x Elims
es
case Reduced () Term
r of
YesReduction Simplification
_ Term
v -> do
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS String
"reify.anon" Nat
60
[ String
"reduction on defined ident. in anonymous module"
, String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
x
, String
"v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
v
]
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
NoReduction () -> do
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS String
"reify.anon" Nat
60
[ String
"no reduction on defined ident. in anonymous module"
, String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
x
, String
"es = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Elims
es
]
forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es
reifyDef Bool
_ QName
x Elims
es = forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es
reifyDef' :: MonadReify m => QName -> I.Elims -> m Expr
reifyDef' :: forall (m :: * -> *). MonadReify m => QName -> Elims -> m Expr
reifyDef' QName
x Elims
es = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
60 forall a b. (a -> b) -> a -> b
$ String
"reifying call to " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
x
Nat
n <- forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Nat
getDefFreeVars QName
x
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
70 forall a b. (a -> b) -> a -> b
$ String
"freeVars for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Nat
n
let fallback :: SigError -> m Expr
fallback SigError
_ = forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims (QName -> Expr
A.Def QName
x) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x) SigError -> m Expr
fallback forall a b. (a -> b) -> a -> b
$ \ Definition
defn -> do
let def :: Defn
def = Definition -> Defn
theDef Definition
defn
case Defn
def of
Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Just Fail{}, funClauses :: Defn -> [Clause]
funClauses = [Clause
cl] }
| QName -> Bool
isAbsurdLambdaName QName
x -> do
let ([NamedArg DeBruijnPattern]
ps, NamedArg DeBruijnPattern
p) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe ([a], a)
initLast forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
let h :: Hiding
h = forall a. LensHiding a => a -> Hiding
getHiding NamedArg DeBruijnPattern
p
n :: Nat
n = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [NamedArg DeBruijnPattern]
ps
absLam :: Expr
absLam = ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
h
if | Nat
n forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es -> do
let name :: DeBruijnPattern -> String
name (I.VarP PatternInfo
_ DBPatVar
x) = String -> String
patVarNameToString forall a b. (a -> b) -> a -> b
$ DBPatVar -> String
dbPatVarName DBPatVar
x
name DeBruijnPattern
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
vars :: [(ArgInfo, String)]
vars = forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& DeBruijnPattern -> String
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es) [NamedArg DeBruijnPattern]
ps
lam :: (ArgInfo, a) -> m (Expr -> Expr)
lam (ArgInfo
i, a
s) = do
Name
x <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ a
s
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
exprNoRange (Arg (Named (WithOrigin (Ranged String)) Binder) -> LamBinding
A.mkDomainFree forall a b. (a -> b) -> a -> b
$ forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
i forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
($) Expr
absLam 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 :: * -> *} {a}.
(FreshName a, MonadFresh NameId m) =>
(ArgInfo, a) -> m (Expr -> Expr)
lam [(ArgInfo, String)]
vars
| Bool
otherwise -> forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
absLam forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)
Defn
_ -> do
Bool
df <- forall (m :: * -> *). MonadTCEnv m => m Bool
displayFormsEnabled
[QName]
alreadyPrinting <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' [QName] TCEnv
ePrintingPatternLambdas
Maybe (Nat, Maybe System)
extLam <- case Defn
def of
Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just{}, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right{} } -> forall a. HasCallStack => a
__IMPOSSIBLE__
Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
m Bool
b Maybe System
sys) } ->
forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy Maybe System
sys) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sized a => a -> Nat
size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
case Maybe (Nat, Maybe System)
extLam of
Just (Nat
pars, Maybe System
sys) | Bool
df, QName
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [QName]
alreadyPrinting ->
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' [QName] TCEnv
ePrintingPatternLambdas (QName
x forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x (Definition -> ArgInfo
defArgInfo Definition
defn) Nat
pars Maybe System
sys
(Definition -> [Clause]
defClauses Definition
defn) Elims
es
Maybe (Nat, Maybe System)
_ -> do
([Arg (Named_ Expr)]
pad, [Elim' (Named_ Term)]
nes :: [Elim' (Named_ Term)]) <- case Defn
def of
Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projIndex :: Projection -> Nat
projIndex = Nat
np } } | Nat
np forall a. Ord a => a -> a -> Bool
> Nat
0 -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
70 forall a b. (a -> b) -> a -> b
$ String
" def. is a projection with projIndex = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Nat
np
TelV Telescope
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> Type -> m (TelV Type)
telViewUpTo Nat
np (Definition -> Type
defType Definition
defn)
let ([Dom (String, Type)]
as, [Dom (String, Type)]
rest) = forall a. Nat -> [a] -> ([a], [a])
splitAt (Nat
np forall a. Num a => a -> a -> a
- Nat
1) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
dom :: Dom (String, Type)
dom = forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Dom (String, Type)]
rest
ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
let underscore :: Expr
underscore = MetaInfo -> Expr
A.Underscore forall a b. (a -> b) -> a -> b
$ MetaInfo
Info.emptyMetaInfo { metaScope :: ScopeInfo
metaScope = ScopeInfo
scope }
let pad :: [NamedArg Expr]
pad :: [Arg (Named_ Expr)]
pad = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom (String, Type)]
as forall a b. (a -> b) -> a -> b
$ \ (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (String
x, Type
_)}) ->
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged String
x) Expr
underscore
let pad' :: [Arg (Named_ Expr)]
pad' = forall a. Nat -> [a] -> [a]
drop Nat
n [Arg (Named_ Expr)]
pad
es' :: Elims
es' = forall a. Nat -> [a] -> [a]
drop (forall a. Ord a => a -> a -> a
max Nat
0 (Nat
n forall a. Num a => a -> a -> a
- forall a. Sized a => a -> Nat
size [Arg (Named_ Expr)]
pad)) Elims
es
Bool
showImp <- forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
let ([Arg (Named_ Expr)]
padVisNamed, [Arg (Named_ Expr)]
padRest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
filterAndRest forall a. LensHiding a => a -> Bool
visible [Arg (Named_ Expr)]
pad'
let padVis :: [Arg (Named_ Expr)]
padVis = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing) [Arg (Named_ Expr)]
padVisNamed
let padTail :: [Arg (Named_ Expr)]
padTail = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom (String, Type)
dom) [Arg (Named_ Expr)]
padRest
let padSame :: [Arg (Named_ Expr)]
padSame = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. a -> Maybe a
Just (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom (String, Type)
dom) forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged String)) =>
a -> Maybe String
bareNameOf) [Arg (Named_ Expr)]
padTail
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null [Arg (Named_ Expr)]
padTail Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
showImp
then ([Arg (Named_ Expr)]
padVis , forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) Elims
es')
else ([Arg (Named_ Expr)]
padVis forall a. [a] -> [a] -> [a]
++ [Arg (Named_ Expr)]
padSame, forall t a. Dom (String, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden Dom (String, Type)
dom Elims
es')
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ([], forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
drop Nat
n Elims
es)
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.def" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
" pad =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow [Arg (Named_ Expr)]
pad
, Doc
" nes =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow [Elim' (Named_ Term)]
nes
]
let hd0 :: Expr
hd0 | Defn -> Bool
isProperProjection Defn
def = ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix forall a b. (a -> b) -> a -> b
$ List1 QName -> AmbiguousQName
AmbQ forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton QName
x
| Bool
otherwise = QName -> Expr
A.Def QName
x
let hd :: Expr
hd = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_) Expr
hd0 [Arg (Named_ Expr)]
pad
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' (Named_ Expr)] -> m Expr
nelims Expr
hd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify [Elim' (Named_ Term)]
nes
reifyExtLam
:: MonadReify m
=> QName -> ArgInfo -> Int -> Maybe System -> [I.Clause]
-> I.Elims -> m Expr
reifyExtLam :: forall (m :: * -> *).
MonadReify m =>
QName
-> ArgInfo -> Nat -> Maybe System -> [Clause] -> Elims -> m Expr
reifyExtLam QName
x ArgInfo
ai Nat
npars Maybe System
msys [Clause]
cls Elims
es = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
10 forall a b. (a -> b) -> a -> b
$ String
"reifying extended lambda " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
x
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.def" Nat
50 forall a b. (a -> b) -> a -> b
$ Doc -> String
render forall a b. (a -> b) -> a -> b
$ Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"npars =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Nat
npars
, Doc
"es =" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Pretty a => Nat -> a -> Doc
prettyPrec Nat
10) Elims
es)
, Doc
"def =" Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> Doc
pretty [Clause]
cls) ]
let (Elims
pares, Elims
rest) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
npars Elims
es
let pars :: Args
pars = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
pares
[Clause]
cls <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe System
msys
(forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
x Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cls)
(forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. QName -> a -> QNamed a
QNamed QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall t. Apply t => t -> Args -> t
`apply` Args
pars))
let cx :: Name
cx = Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
dInfo :: DefInfo' Expr
dInfo = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
cx Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef
(forall a. HasRange a => a -> Range
getRange QName
x)
erased :: Erased
erased = case forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai of
Quantity0 Q0Origin
o -> Q0Origin -> Erased
Erased Q0Origin
o
Quantityω QωOrigin
o -> QωOrigin -> Erased
NotErased QωOrigin
o
Quantity1 Q1Origin
o -> forall a. HasCallStack => a
__IMPOSSIBLE__
lam :: Expr
lam = case [Clause]
cls of
[] -> ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
exprNoRange Hiding
NotHidden
(Clause
cl:[Clause]
cls) -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
exprNoRange DefInfo' Expr
dInfo Erased
erased QName
x (Clause
cl forall a. a -> [a] -> NonEmpty a
:| [Clause]
cls)
forall (m :: * -> *).
MonadReify m =>
Expr -> [Elim' Expr] -> m Expr
elims Expr
lam forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Elims
rest
nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden :: forall t a. Dom (String, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden Dom (String, t)
dom (I.Apply (Arg ArgInfo
info a
e) : [Elim' a]
es) | forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info =
forall a. Arg a -> Elim' a
I.Apply (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom (String, t)
dom) a
e)) forall a. a -> [a] -> [a]
:
forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) [Elim' a]
es
nameFirstIfHidden Dom (String, t)
_ [Elim' a]
es =
forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) [Elim' a]
es
instance Reify i => Reify (Named n i) where
type ReifiesTo (Named n i) = Named n (ReifiesTo i)
reify :: forall (m :: * -> *).
MonadReify m =>
Named n i -> m (ReifiesTo (Named n i))
reify = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Named n i -> m (ReifiesTo (Named n i))
reifyWhen Bool
b = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)
instance Reify i => Reify (Arg i) where
type ReifiesTo (Arg i) = Arg (ReifiesTo i)
reify :: forall (m :: * -> *).
MonadReify m =>
Arg i -> m (ReifiesTo (Arg i))
reify (Arg ArgInfo
info i
i) = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
reifyWhen i
i forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Bool
condition)
where condition :: m Bool
condition = (forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> Hiding
argInfoHiding ArgInfo
info forall a. Eq a => a -> a -> Bool
/= Hiding
Hidden) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments)
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` forall (m :: * -> *). HasOptions m => m Bool
showIrrelevantArguments)
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Arg i -> m (ReifiesTo (Arg i))
reifyWhen Bool
b Arg i
i = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b) Arg i
i
data NamedClause = NamedClause QName Bool I.Clause
newtype MonoidMap k v = MonoidMap { forall k v. MonoidMap k v -> Map k v
_unMonoidMap :: Map.Map k v }
instance (Ord k, Monoid v) => Semigroup (MonoidMap k v) where
MonoidMap Map k v
m1 <> :: MonoidMap k v -> MonoidMap k v -> MonoidMap k v
<> MonoidMap Map k v
m2 = forall k v. Map k v -> MonoidMap k v
MonoidMap (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Monoid a => a -> a -> a
mappend Map k v
m1 Map k v
m2)
instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where
mempty :: MonoidMap k v
mempty = forall k v. Map k v -> MonoidMap k v
MonoidMap forall k a. Map k a
Map.empty
mappend :: MonoidMap k v -> MonoidMap k v -> MonoidMap k v
mappend = forall a. Semigroup a => a -> a -> a
(<>)
removeNameUnlessUserWritten :: (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten :: forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten a
a
| (forall a. LensOrigin a => a -> Origin
getOrigin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf a
a) forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Origin
UserWritten = a
a
| Bool
otherwise = forall a. LensNamed a => Maybe (NameOf a) -> a -> a
setNameOf forall a. Maybe a
Nothing a
a
stripImplicits :: MonadReify m => A.Patterns -> A.Patterns -> m A.Patterns
stripImplicits :: forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits Patterns
params Patterns
ps = do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten) Patterns
ps) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.implicit" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"stripping implicits"
, Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"ps =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow Patterns
ps
]
let ps' :: Patterns
ps' = Patterns -> Patterns
blankDots forall a b. (a -> b) -> a -> b
$ forall {e}. [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip Patterns
ps
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.implicit" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Nat -> Doc -> Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ Doc
"ps' =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow Patterns
ps'
]
forall (m :: * -> *) a. Monad m => a -> m a
return Patterns
ps'
where
blankDots :: Patterns -> Patterns
blankDots Patterns
ps = forall a. BlankVars a => Set Name -> a -> a
blank (forall a. Binder a => a -> Set Name
varsBoundIn forall a b. (a -> b) -> a -> b
$ Patterns
params forall a. [a] -> [a] -> [a]
++ Patterns
ps) Patterns
ps
strip :: [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
strip [NamedArg (Pattern' e)]
ps = forall {e}.
Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
ps
where
stripArgs :: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
_ [] = []
stripArgs Bool
fixedPos (NamedArg (Pattern' e)
a : [NamedArg (Pattern' e)]
as)
| forall {e}. Arg (Named_ (Pattern' e)) -> Bool
canStrip NamedArg (Pattern' e)
a =
if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {e}. Arg (Named_ (Pattern' e)) -> Bool
canStrip forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall {a}. (LensHiding a, LensNamed a, IsProjP a) => a -> Bool
isUnnamedHidden [NamedArg (Pattern' e)]
as
then Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
False [NamedArg (Pattern' e)]
as
else [NamedArg (Pattern' e)]
goWild
| Bool
otherwise = forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos (NamedArg (Pattern' e) -> NamedArg (Pattern' e)
stripArg NamedArg (Pattern' e)
a) forall a. a -> [a] -> [a]
: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
as
where
a' :: NamedArg (Pattern' e)
a' = forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg (Pattern' e)
a forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP forall a b. (a -> b) -> a -> b
$ Range -> PatInfo
Info.PatRange forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange NamedArg (Pattern' e)
a
goWild :: [NamedArg (Pattern' e)]
goWild = forall {f :: * -> *} {b}.
(Functor f, LensNamed b, LensOrigin (NameOf b)) =>
Bool -> f b -> f b
stripName Bool
fixedPos NamedArg (Pattern' e)
a' forall a. a -> [a] -> [a]
: Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
as
stripName :: Bool -> f b -> f b
stripName Bool
True = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (LensNamed a, LensOrigin (NameOf a)) => a -> a
removeNameUnlessUserWritten
stripName Bool
False = forall a. a -> a
id
canStrip :: Arg (Named_ (Pattern' e)) -> Bool
canStrip Arg (Named_ (Pattern' e))
a = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ forall a. LensHiding a => a -> Bool
notVisible Arg (Named_ (Pattern' e))
a
, forall a. LensOrigin a => a -> Origin
getOrigin Arg (Named_ (Pattern' e))
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [ Origin
UserWritten , Origin
CaseSplit ]
, (forall a. LensOrigin a => a -> Origin
getOrigin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf Arg (Named_ (Pattern' e))
a) forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Origin
UserWritten
, forall {e}. Pattern' e -> Bool
varOrDot (forall a. NamedArg a -> a
namedArg Arg (Named_ (Pattern' e))
a)
]
isUnnamedHidden :: a -> Bool
isUnnamedHidden a
x = forall a. LensHiding a => a -> Bool
notVisible a
x Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf a
x) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP a
x)
stripArg :: NamedArg (Pattern' e) -> NamedArg (Pattern' e)
stripArg NamedArg (Pattern' e)
a = 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' e -> Pattern' e
stripPat) NamedArg (Pattern' e)
a
stripPat :: Pattern' e -> Pattern' e
stripPat = \case
p :: Pattern' e
p@(A.VarP BindName
_) -> Pattern' e
p
A.ConP ConPatInfo
i AmbiguousQName
c [NamedArg (Pattern' e)]
ps -> forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
i AmbiguousQName
c forall a b. (a -> b) -> a -> b
$ Bool -> [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
stripArgs Bool
True [NamedArg (Pattern' e)]
ps
p :: Pattern' e
p@A.ProjP{} -> Pattern' e
p
p :: Pattern' e
p@(A.DefP PatInfo
_ AmbiguousQName
_ [NamedArg (Pattern' e)]
_) -> Pattern' e
p
p :: Pattern' e
p@(A.DotP PatInfo
_ e
_e) -> Pattern' e
p
p :: Pattern' e
p@(A.WildP PatInfo
_) -> Pattern' e
p
p :: Pattern' e
p@(A.AbsurdP PatInfo
_) -> Pattern' e
p
p :: Pattern' e
p@(A.LitP PatInfo
_ Literal
_) -> Pattern' e
p
A.AsP PatInfo
i BindName
x Pattern' e
p -> forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
x forall a b. (a -> b) -> a -> b
$ Pattern' e -> Pattern' e
stripPat Pattern' e
p
A.PatternSynP PatInfo
_ AmbiguousQName
_ [NamedArg (Pattern' e)]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.RecP PatInfo
i [FieldAssignment' (Pattern' e)]
fs -> forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
i forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' e -> Pattern' e
stripPat) [FieldAssignment' (Pattern' e)]
fs
p :: Pattern' e
p@A.EqualP{} -> Pattern' e
p
A.WithP PatInfo
i Pattern' e
p -> forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i forall a b. (a -> b) -> a -> b
$ Pattern' e -> Pattern' e
stripPat Pattern' e
p
A.AnnP PatInfo
i e
a Pattern' e
p -> forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
i e
a forall a b. (a -> b) -> a -> b
$ Pattern' e -> Pattern' e
stripPat Pattern' e
p
varOrDot :: Pattern' e -> Bool
varOrDot A.VarP{} = Bool
True
varOrDot A.WildP{} = Bool
True
varOrDot A.DotP{} = Bool
True
varOrDot (A.ConP ConPatInfo
cpi AmbiguousQName
_ NAPs e
ps) | ConPatInfo -> ConInfo
conPatOrigin ConPatInfo
cpi forall a. Eq a => a -> a -> Bool
== ConInfo
ConOSystem
= ConPatInfo -> ConPatLazy
conPatLazy ConPatInfo
cpi forall a. Eq a => a -> a -> Bool
== ConPatLazy
ConPatLazy Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' e -> Bool
varOrDot forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) NAPs e
ps
varOrDot Pattern' e
_ = Bool
False
blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope :: forall (m :: * -> *) a. (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope a
e = do
Set Name
names <- forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
== NameInScope
C.InScope) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensInScope a => a -> NameInScope
C.isInScope) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
names a
e
class BlankVars a where
blank :: Set Name -> a -> a
default blank :: (Functor f, BlankVars b, f b ~ a) => Set Name -> a -> a
blank = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. BlankVars a => Set Name -> a -> a
blank
instance BlankVars a => BlankVars (Arg a)
instance BlankVars a => BlankVars (Named s a)
instance BlankVars a => BlankVars [a]
instance BlankVars a => BlankVars (List1 a)
instance BlankVars a => BlankVars (FieldAssignment' a)
instance (BlankVars a, BlankVars b) => BlankVars (a, b) where
blank :: Set Name -> (a, b) -> (a, b)
blank Set Name
bound (a
x, b
y) = (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound a
x, forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound b
y)
instance (BlankVars a, BlankVars b) => BlankVars (Either a b) where
blank :: Set Name -> Either a b -> Either a b
blank Set Name
bound (Left a
x) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound a
x
blank Set Name
bound (Right b
y) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound b
y
instance BlankVars A.ProblemEq where
blank :: Set Name -> ProblemEq -> ProblemEq
blank Set Name
bound = forall a. a -> a
id
instance BlankVars A.Clause where
blank :: Set Name -> Clause -> Clause
blank Set Name
bound (A.Clause LHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Bool
ca)
| forall a. Null a => a -> Bool
null WhereDeclarations
wh =
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' LHS
lhs)
(forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' [ProblemEq]
strippedPats)
(forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' RHS
rhs) WhereDeclarations
noWhereDecls Bool
ca
| Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__
where bound' :: Set Name
bound' = forall a. Binder a => a -> Set Name
varsBoundIn LHS
lhs forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
instance BlankVars A.LHS where
blank :: Set Name -> LHS -> LHS
blank Set Name
bound (A.LHS LHSInfo
i LHSCore
core) = LHSInfo -> LHSCore -> LHS
A.LHS LHSInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound LHSCore
core
instance BlankVars A.LHSCore where
blank :: Set Name -> LHSCore -> LHSCore
blank Set Name
bound (A.LHSHead QName
f Patterns
ps) = forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
f forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
blank Set Name
bound (A.LHSProj AmbiguousQName
p NamedArg LHSCore
b Patterns
ps) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSProj AmbiguousQName
p) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (NamedArg LHSCore
b, Patterns
ps)
blank Set Name
bound (A.LHSWith LHSCore
h [Arg Pattern]
wps Patterns
ps) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound ((LHSCore
h, [Arg Pattern]
wps), Patterns
ps)
instance BlankVars A.Pattern where
blank :: Set Name -> Pattern -> Pattern
blank Set Name
bound Pattern
p = case Pattern
p of
A.VarP BindName
_ -> Pattern
p
A.ConP ConPatInfo
c AmbiguousQName
i Patterns
ps -> forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
c AmbiguousQName
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
A.ProjP{} -> Pattern
p
A.DefP PatInfo
i AmbiguousQName
f Patterns
ps -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
i AmbiguousQName
f forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Patterns
ps
A.DotP PatInfo
i Expr
e -> forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
A.WildP PatInfo
_ -> Pattern
p
A.AbsurdP PatInfo
_ -> Pattern
p
A.LitP PatInfo
_ Literal
_ -> Pattern
p
A.AsP PatInfo
i BindName
n Pattern
p -> forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
A.AsP PatInfo
i BindName
n forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p
A.PatternSynP PatInfo
_ AmbiguousQName
_ Patterns
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.RecP PatInfo
i [FieldAssignment' Pattern]
fs -> forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound [FieldAssignment' Pattern]
fs
A.EqualP{} -> Pattern
p
A.WithP PatInfo
i Pattern
p -> forall e. PatInfo -> Pattern' e -> Pattern' e
A.WithP PatInfo
i (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p)
A.AnnP PatInfo
i Expr
a Pattern
p -> forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
i (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
a) (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Pattern
p)
instance BlankVars A.Expr where
blank :: Set Name -> Expr -> Expr
blank Set Name
bound Expr
e = case Expr
e of
A.ScopedExpr ScopeInfo
i Expr
e -> ScopeInfo -> Expr -> Expr
A.ScopedExpr ScopeInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
A.Var Name
x -> if Name
x forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
bound then Expr
e
else MetaInfo -> Expr
A.Underscore MetaInfo
emptyMetaInfo
A.Def' QName
_ Suffix
_ -> Expr
e
A.Proj{} -> Expr
e
A.Con AmbiguousQName
_ -> Expr
e
A.Lit ExprInfo
_ Literal
_ -> Expr
e
A.QuestionMark{} -> Expr
e
A.Underscore MetaInfo
_ -> Expr
e
A.Dot ExprInfo
i Expr
e -> ExprInfo -> Expr -> Expr
A.Dot ExprInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
A.App AppInfo
i Expr
e1 Arg (Named_ Expr)
e2 -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e1, Arg (Named_ Expr)
e2)
A.WithApp ExprInfo
i Expr
e [Expr]
es -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Expr -> [Expr] -> Expr
A.WithApp ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, [Expr]
es)
A.Lam ExprInfo
i LamBinding
b Expr
e -> let bound' :: Set Name
bound' = forall a. Binder a => a -> Set Name
varsBoundIn LamBinding
b forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
in ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound LamBinding
b) (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' Expr
e)
A.AbsurdLam ExprInfo
_ Hiding
_ -> Expr
e
A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f List1 Clause
cs -> ExprInfo
-> DefInfo' Expr -> Erased -> QName -> List1 Clause -> Expr
A.ExtendedLam ExprInfo
i DefInfo' Expr
d Erased
e QName
f forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound List1 Clause
cs
A.Pi ExprInfo
i Telescope1
tel Expr
e -> let bound' :: Set Name
bound' = forall a. Binder a => a -> Set Name
varsBoundIn Telescope1
tel forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name
bound
in forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Telescope1 -> Expr -> Expr
A.Pi ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound' (Telescope1
tel, Expr
e)
A.Generalized {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.Fun ExprInfo
i Arg Expr
a Expr
b -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Arg Expr -> Expr -> Expr
A.Fun ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Arg Expr
a, Expr
b)
A.Let ExprInfo
_ List1 LetBinding
_ Expr
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.Rec ExprInfo
i RecordAssigns
es -> ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
i forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound RecordAssigns
es
A.RecUpdate ExprInfo
i Expr
e Assigns
es -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ExprInfo -> Expr -> Assigns -> Expr
A.RecUpdate ExprInfo
i) forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound (Expr
e, Assigns
es)
A.Quote {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.QuoteTerm {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.Unquote {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
A.DontCare Expr
v -> Expr -> Expr
A.DontCare forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
v
A.PatternSyn {} -> Expr
e
A.Macro {} -> Expr
e
instance BlankVars A.ModuleName where
blank :: Set Name -> ModuleName -> ModuleName
blank Set Name
bound = forall a. a -> a
id
instance BlankVars RHS where
blank :: Set Name -> RHS -> RHS
blank Set Name
bound (RHS Expr
e Maybe Expr
mc) = Expr -> Maybe Expr -> RHS
RHS (forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e) Maybe Expr
mc
blank Set Name
bound RHS
AbsurdRHS = RHS
AbsurdRHS
blank Set Name
bound (WithRHS QName
_ [WithExpr]
es [Clause]
clauses) = forall a. HasCallStack => a
__IMPOSSIBLE__
blank Set Name
bound (RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
instance BlankVars A.LamBinding where
blank :: Set Name -> LamBinding -> LamBinding
blank Set Name
bound b :: LamBinding
b@A.DomainFree{} = LamBinding
b
blank Set Name
bound (A.DomainFull TypedBinding
bs) = TypedBinding -> LamBinding
A.DomainFull forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound TypedBinding
bs
instance BlankVars TypedBinding where
blank :: Set Name -> TypedBinding -> TypedBinding
blank Set Name
bound (TBind Range
r TypedBindingInfo
t List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
n Expr
e) = Range
-> TypedBindingInfo
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
n forall a b. (a -> b) -> a -> b
$ forall a. BlankVars a => Set Name -> a -> a
blank Set Name
bound Expr
e
blank Set Name
bound (TLet Range
_ List1 LetBinding
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
class Binder a where
varsBoundIn :: a -> Set Name
default varsBoundIn :: (Foldable f, Binder b, f b ~ a) => a -> Set Name
varsBoundIn = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. Binder a => a -> Set Name
varsBoundIn
instance Binder A.LHS where
varsBoundIn :: LHS -> Set Name
varsBoundIn (A.LHS LHSInfo
_ LHSCore
core) = forall a. Binder a => a -> Set Name
varsBoundIn LHSCore
core
instance Binder A.LHSCore where
varsBoundIn :: LHSCore -> Set Name
varsBoundIn (A.LHSHead QName
_ Patterns
ps) = forall a. Binder a => a -> Set Name
varsBoundIn Patterns
ps
varsBoundIn (A.LHSProj AmbiguousQName
_ NamedArg LHSCore
b Patterns
ps) = forall a. Binder a => a -> Set Name
varsBoundIn (NamedArg LHSCore
b, Patterns
ps)
varsBoundIn (A.LHSWith LHSCore
h [Arg Pattern]
wps Patterns
ps) = forall a. Binder a => a -> Set Name
varsBoundIn ((LHSCore
h, [Arg Pattern]
wps), Patterns
ps)
instance Binder A.Pattern where
varsBoundIn :: Pattern -> Set Name
varsBoundIn = forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m) -> p -> m
foldAPattern forall a b. (a -> b) -> a -> b
$ \case
A.VarP BindName
x -> forall a. Binder a => a -> Set Name
varsBoundIn BindName
x
A.AsP PatInfo
_ BindName
x Pattern' (ADotT Pattern)
_ -> forall a. Null a => a
empty
A.ConP ConPatInfo
_ AmbiguousQName
_ NAPs (ADotT Pattern)
_ -> forall a. Null a => a
empty
A.ProjP{} -> forall a. Null a => a
empty
A.DefP PatInfo
_ AmbiguousQName
_ NAPs (ADotT Pattern)
_ -> forall a. Null a => a
empty
A.WildP{} -> forall a. Null a => a
empty
A.DotP{} -> forall a. Null a => a
empty
A.AbsurdP{} -> forall a. Null a => a
empty
A.LitP{} -> forall a. Null a => a
empty
A.PatternSynP PatInfo
_ AmbiguousQName
_ NAPs (ADotT Pattern)
_ -> forall a. Null a => a
empty
A.RecP PatInfo
_ [FieldAssignment' (Pattern' (ADotT Pattern))]
_ -> forall a. Null a => a
empty
A.EqualP{} -> forall a. Null a => a
empty
A.WithP PatInfo
_ Pattern' (ADotT Pattern)
_ -> forall a. Null a => a
empty
A.AnnP{} -> forall a. Null a => a
empty
instance Binder a => Binder (A.Binder' a) where
varsBoundIn :: Binder' a -> Set Name
varsBoundIn (A.Binder Maybe Pattern
p a
n) = forall a. Binder a => a -> Set Name
varsBoundIn (Maybe Pattern
p, a
n)
instance Binder A.LamBinding where
varsBoundIn :: LamBinding -> Set Name
varsBoundIn (A.DomainFree Maybe Expr
_ Arg (Named (WithOrigin (Ranged String)) Binder)
x) = forall a. Binder a => a -> Set Name
varsBoundIn Arg (Named (WithOrigin (Ranged String)) Binder)
x
varsBoundIn (A.DomainFull TypedBinding
b) = forall a. Binder a => a -> Set Name
varsBoundIn TypedBinding
b
instance Binder TypedBinding where
varsBoundIn :: TypedBinding -> Set Name
varsBoundIn (TBind Range
_ TypedBindingInfo
_ List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
_) = forall a. Binder a => a -> Set Name
varsBoundIn List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs
varsBoundIn (TLet Range
_ List1 LetBinding
bs) = forall a. Binder a => a -> Set Name
varsBoundIn List1 LetBinding
bs
instance Binder BindName where
varsBoundIn :: BindName -> Set Name
varsBoundIn BindName
x = forall el coll. Singleton el coll => el -> coll
singleton (BindName -> Name
unBind BindName
x)
instance Binder LetBinding where
varsBoundIn :: LetBinding -> Set Name
varsBoundIn (LetBind LetInfo
_ ArgInfo
_ BindName
x Expr
_ Expr
_) = forall a. Binder a => a -> Set Name
varsBoundIn BindName
x
varsBoundIn (LetPatBind LetInfo
_ Pattern
p Expr
_) = forall a. Binder a => a -> Set Name
varsBoundIn Pattern
p
varsBoundIn LetApply{} = forall a. Null a => a
empty
varsBoundIn LetOpen{} = forall a. Null a => a
empty
varsBoundIn LetDeclaredVariable{} = forall a. Null a => a
empty
instance Binder a => Binder (FieldAssignment' a)
instance Binder a => Binder (Arg a)
instance Binder a => Binder (Named x a)
instance Binder a => Binder [a]
instance Binder a => Binder (List1 a)
instance Binder a => Binder (Maybe a)
instance (Binder a, Binder b) => Binder (a, b) where
varsBoundIn :: (a, b) -> Set Name
varsBoundIn (a
x, b
y) = forall a. Binder a => a -> Set Name
varsBoundIn a
x forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Binder a => a -> Set Name
varsBoundIn b
y
reifyPatterns :: MonadReify m => [NamedArg I.DeBruijnPattern] -> m [NamedArg A.Pattern]
reifyPatterns :: forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a b. (a -> b) -> a -> b
$ (forall p. NamedArg p -> NamedArg p
stripNameFromExplicit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj) forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.>
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *). MonadReify m => DeBruijnPattern -> m Pattern
reifyPat)
where
stripNameFromExplicit :: NamedArg p -> NamedArg p
stripNameFromExplicit :: forall p. NamedArg p -> NamedArg p
stripNameFromExplicit NamedArg p
a
| forall a. LensHiding a => a -> Bool
visible NamedArg p
a Bool -> Bool -> Bool
|| forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) forall a. Null a => a -> Bool
null forall a. IsNoName a => a -> Bool
isNoName) (forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged String)) =>
a -> Maybe String
bareNameOf NamedArg p
a) =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing) NamedArg p
a
| Bool
otherwise = NamedArg p
a
stripHidingFromPostfixProj :: IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj :: forall p. IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj NamedArg p
a = case forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg p
a of
Just (ProjOrigin
o, AmbiguousQName
_) | ProjOrigin
o forall a. Eq a => a -> a -> Bool
/= ProjOrigin
ProjPrefix -> forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden NamedArg p
a
Maybe (ProjOrigin, AmbiguousQName)
_ -> NamedArg p
a
reifyPat :: MonadReify m => I.DeBruijnPattern -> m A.Pattern
reifyPat :: forall (m :: * -> *). MonadReify m => DeBruijnPattern -> m Pattern
reifyPat DeBruijnPattern
p = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.pat" Nat
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"reifying pattern" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty DeBruijnPattern
p
Bool
keepVars <- PragmaOptions -> Bool
optKeepPatternVariables forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
case DeBruijnPattern
p of
DeBruijnPattern
p | Just (PatternInfo PatOrigin
PatOLit [Name]
asB) <- forall x. Pattern' x -> Maybe PatternInfo
patternInfo DeBruijnPattern
p -> do
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (DeBruijnPattern -> Term
I.patternToTerm DeBruijnPattern
p) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
I.Lit Literal
l -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings [Name]
asB forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Literal -> Pattern' e
A.LitP forall a. Null a => a
empty Literal
l
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
I.VarP PatternInfo
i DBPatVar
x -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
o :: PatOrigin
o@PatOrigin
PatODot -> forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o forall a b. (a -> b) -> a -> b
$ Nat -> Term
var forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
PatOrigin
PatOWild -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
PatOrigin
PatOAbsurd -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
PatOrigin
_ -> forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x
I.DotP PatternInfo
i Term
v -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
PatOrigin
PatOWild -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
PatOrigin
PatOAbsurd -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
o :: PatOrigin
o@(PatOVar Name
x) | I.Var Nat
i [] <- Term
v -> do
Name
x' <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV Nat
i
if Name -> Name
nameConcrete Name
x forall a. Eq a => a -> a -> Bool
== Name -> Name
nameConcrete Name
x' then
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x'
else
forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o Term
v
PatOrigin
o -> forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o Term
v
I.LitP PatternInfo
i Literal
l -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Literal -> Pattern' e
A.LitP forall a. Null a => a
empty Literal
l
I.ProjP ProjOrigin
o QName
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
A.ProjP PatInfo
patNoRange ProjOrigin
o forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d
I.ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps | ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) forall a b. (a -> b) -> a -> b
$
case PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) of
PatOrigin
PatOWild -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
PatOrigin
PatOAbsurd -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
PatOVar Name
x | Bool
keepVars -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
PatOrigin
_ -> forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
reifyConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps
I.ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
reifyConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps
I.DefP PatternInfo
i QName
f [NamedArg DeBruijnPattern]
ps -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
PatOrigin
PatOWild -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
PatOrigin
PatOAbsurd -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
PatOVar Name
x | Bool
keepVars -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
PatOrigin
_ -> forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.DefP PatInfo
patNoRange (QName -> AmbiguousQName
unambiguous QName
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns [NamedArg DeBruijnPattern]
ps
I.IApplyP PatternInfo
i Term
_ Term
_ DBPatVar
x -> forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings (PatternInfo -> [Name]
patAsNames PatternInfo
i) forall a b. (a -> b) -> a -> b
$ case PatternInfo -> PatOrigin
patOrigin PatternInfo
i of
o :: PatOrigin
o@PatOrigin
PatODot -> forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o forall a b. (a -> b) -> a -> b
$ Nat -> Term
var forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
PatOrigin
PatOWild -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
PatOrigin
PatOAbsurd -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.AbsurdP PatInfo
patNoRange
PatOrigin
_ -> forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x
reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
reifyVarP :: forall (m :: * -> *). MonadReify m => DBPatVar -> m Pattern
reifyVarP DBPatVar
x = do
Name
n <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Nat -> m Name
nameOfBV forall a b. (a -> b) -> a -> b
$ DBPatVar -> Nat
dbPatVarIndex DBPatVar
x
let y :: String
y = DBPatVar -> String
dbPatVarName DBPatVar
x
if | String
y forall a. Eq a => a -> a -> Bool
== String
"_" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
n
| forall a. Pretty a => a -> String
prettyShow (Name -> Name
nameConcrete Name
n) forall a. Eq a => a -> a -> Bool
== String
"()" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP (Name -> BindName
mkBindName Name
n)
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$
Name -> BindName
mkBindName Name
n { nameConcrete :: Name
nameConcrete = String -> Name
C.simpleName String
y }
reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
reifyDotP :: forall (m :: * -> *).
MonadReify m =>
PatOrigin -> Term -> m Pattern
reifyDotP PatOrigin
o Term
v = do
Bool
keepVars <- PragmaOptions -> Bool
optKeepPatternVariables forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
if | PatOVar Name
x <- PatOrigin
o , Bool
keepVars -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. BindName -> Pattern' e
A.VarP forall a b. (a -> b) -> a -> b
$ Name -> BindName
mkBindName Name
x
| Bool
otherwise -> forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
patNoRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
reifyConP :: MonadReify m
=> ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
-> m A.Pattern
reifyConP :: forall (m :: * -> *).
MonadReify m =>
ConHead
-> ConPatternInfo -> [NamedArg DeBruijnPattern] -> m Pattern
reifyConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps = do
forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
A.ConP ConPatInfo
ci (QName -> AmbiguousQName
unambiguous (ConHead -> QName
conName ConHead
c)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns [NamedArg DeBruijnPattern]
ps
where
ci :: ConPatInfo
ci = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
origin PatInfo
patNoRange ConPatLazy
lazy
lazy :: ConPatLazy
lazy | ConPatternInfo -> Bool
conPLazy ConPatternInfo
cpi = ConPatLazy
ConPatLazy
| Bool
otherwise = ConPatLazy
ConPatEager
origin :: ConInfo
origin = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi
addAsBindings :: Functor m => [A.Name] -> m A.Pattern -> m A.Pattern
addAsBindings :: forall (m :: * -> *). Functor m => [Name] -> m Pattern -> m Pattern
addAsBindings [Name]
xs m Pattern
p = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
patNoRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName) m Pattern
p [Name]
xs
tryRecPFromConP :: MonadReify m => A.Pattern -> m A.Pattern
tryRecPFromConP :: forall (m :: * -> *). MonadReify m => Pattern -> m Pattern
tryRecPFromConP Pattern
p = do
let fallback :: m Pattern
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
case Pattern
p of
A.ConP ConPatInfo
ci AmbiguousQName
c Patterns
ps -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.pat" Nat
60 forall a b. (a -> b) -> a -> b
$ String
"tryRecPFromConP " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow AmbiguousQName
c
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
c) m Pattern
fallback forall a b. (a -> b) -> a -> b
$ \ (QName
r, Defn
def) -> do
if Defn -> Bool
recNamedCon Defn
def Bool -> Bool -> Bool
&& ConPatInfo -> ConInfo
conPatOrigin ConPatInfo
ci forall a. Eq a => a -> a -> Bool
/= ConInfo
ConORec then m Pattern
fallback else do
[Dom' Term Name]
fs <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom' Term Name])
getRecordFieldNames_ QName
r
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom' Term Name]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length Patterns
ps) forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
A.RecP PatInfo
patNoRange forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {t} {a}. Dom' t Name -> NamedArg a -> FieldAssignment' a
mkFA [Dom' Term Name]
fs Patterns
ps
where
mkFA :: Dom' t Name -> NamedArg a -> FieldAssignment' a
mkFA Dom' t Name
ax NamedArg a
nap = forall a. Name -> a -> FieldAssignment' a
FieldAssignment (forall t e. Dom' t e -> e
unDom Dom' t Name
ax) (forall a. NamedArg a -> a
namedArg NamedArg a
nap)
Pattern
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
recOrCon :: MonadReify m => QName -> ConOrigin -> [Arg Expr] -> m A.Expr
recOrCon :: forall (m :: * -> *).
MonadReify m =>
QName -> ConInfo -> [Arg Expr] -> m Expr
recOrCon QName
c ConInfo
co [Arg Expr]
es = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> String -> m ()
reportSLn String
"reify.expr" Nat
60 forall a b. (a -> b) -> a -> b
$ String
"recOrCon " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow QName
c
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) m Expr
fallback forall a b. (a -> b) -> a -> b
$ \ (QName
r, Defn
def) -> do
if Defn -> Bool
recNamedCon Defn
def Bool -> Bool -> Bool
&& ConInfo
co forall a. Eq a => a -> a -> Bool
/= ConInfo
ConORec then m Expr
fallback else do
[Dom' Term Name]
fs <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Maybe [Dom' Term Name])
getRecordFieldNames_ QName
r
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom' Term Name]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg Expr]
es) forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> RecordAssigns -> Expr
A.Rec forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {t} {b} {b}.
Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
mkFA [Dom' Term Name]
fs [Arg Expr]
es
where
fallback :: m Expr
fallback = forall (m :: * -> *). MonadReify m => Expr -> [Arg Expr] -> m Expr
apps (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous QName
c)) [Arg Expr]
es
mkFA :: Dom' t Name -> Arg b -> Either (FieldAssignment' b) b
mkFA Dom' t Name
ax = forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Name -> a -> FieldAssignment' a
FieldAssignment (forall t e. Dom' t e -> e
unDom Dom' t Name
ax) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg
instance Reify (QNamed I.Clause) where
type ReifiesTo (QNamed I.Clause) = A.Clause
reify :: forall (m :: * -> *).
MonadReify m =>
QNamed Clause -> m (ReifiesTo (QNamed Clause))
reify (QNamed QName
f Clause
cl) = forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True Clause
cl)
instance Reify NamedClause where
type ReifiesTo NamedClause = A.Clause
reify :: forall (m :: * -> *).
MonadReify m =>
NamedClause -> m (ReifiesTo NamedClause)
reify (NamedClause QName
f Bool
toDrop Clause
cl) = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
cl) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.clause" Nat
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"reifying NamedClause"
, Doc
" f =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty QName
f
, Doc
" toDrop =" Doc -> Doc -> Doc
<+> forall a. Show a => a -> Doc
pshow Bool
toDrop
, Doc
" cl =" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty Clause
cl
]
let ell :: ExpandedEllipsis
ell = Clause -> ExpandedEllipsis
clauseEllipsis Clause
cl
Patterns
ps <- forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
SpineLHS
lhs <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS forall a b. (a -> b) -> a -> b
$ forall a. Null a => a
empty { lhsEllipsis :: ExpandedEllipsis
lhsEllipsis = ExpandedEllipsis
ell }) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
ps []
(Patterns
params , SpineLHS
lhs) <- if Bool -> Bool
not Bool
toDrop then forall (m :: * -> *) a. Monad m => a -> m a
return ([] , SpineLHS
lhs) else do
Nat
nfv <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ModuleName)
getDefModule QName
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left SigError
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Nat
0
Right ModuleName
m -> forall a. Sized a => a -> Nat
size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Nat -> SpineLHS -> (Patterns, SpineLHS)
splitParams Nat
nfv SpineLHS
lhs
SpineLHS
lhs <- forall (m :: * -> *).
MonadReify m =>
Patterns -> SpineLHS -> m SpineLHS
stripImps Patterns
params SpineLHS
lhs
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.clause" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"reifying NamedClause, lhs =" Doc -> Doc -> Doc
<?> forall a. Show a => a -> Doc
pshow SpineLHS
lhs
RHS
rhs <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Clause -> Maybe Term
clauseBody Clause
cl) (forall (m :: * -> *) a. Monad m => a -> m a
return RHS
AbsurdRHS) forall a b. (a -> b) -> a -> b
$ \ Term
e ->
Expr -> Maybe Expr -> RHS
RHS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.clause" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"reifying NamedClause, rhs =" Doc -> Doc -> Doc
<?> forall a. Show a => a -> Doc
pshow RHS
rhs
let result :: Clause
result = forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls (Clause -> Bool
I.clauseCatchall Clause
cl)
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"reify.clause" Nat
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Doc
"reified NamedClause, result =" Doc -> Doc -> Doc
<?> forall a. Show a => a -> Doc
pshow Clause
result
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
result
where
splitParams :: Nat -> SpineLHS -> (Patterns, SpineLHS)
splitParams Nat
n (SpineLHS LHSInfo
i QName
f Patterns
ps) =
let (Patterns
params , Patterns
pats) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n Patterns
ps
in (Patterns
params , LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
i QName
f Patterns
pats)
stripImps :: MonadReify m => [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
stripImps :: forall (m :: * -> *).
MonadReify m =>
Patterns -> SpineLHS -> m SpineLHS
stripImps Patterns
params (SpineLHS LHSInfo
i QName
f Patterns
ps) = LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS LHSInfo
i QName
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits Patterns
params Patterns
ps
instance Reify (QNamed System) where
type ReifiesTo (QNamed System) = [A.Clause]
reify :: forall (m :: * -> *).
MonadReify m =>
QNamed System -> m (ReifiesTo (QNamed System))
reify (QNamed QName
f (System Telescope
tel [(Face, Term)]
sys)) = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Nat -> a -> m ()
reportS String
"reify.system" Nat
40 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Telescope
tel forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [(Face, Term)]
sys
Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
[(Face, Term)]
sys <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [(Face, Term)]
sys forall a b. (a -> b) -> a -> b
$ \ (Face
phi,Term
t) -> do
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM Face
phi forall a b. (a -> b) -> a -> b
$ \ (Term
u,Bool
b) -> do
Term
u <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case (Term -> IntervalView
view Term
u, Bool
b) of
(IntervalView
IZero, Bool
True) -> Bool
False
(IntervalView
IOne, Bool
False) -> Bool
False
(IntervalView, Bool)
_ -> Bool
True
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Face, Term)]
sys forall a b. (a -> b) -> a -> b
$ \ (Face
alpha,Term
u) -> do
RHS
rhs <- Expr -> Maybe Expr -> RHS
RHS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
Pattern
ep <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall e. PatInfo -> [(e, e)] -> Pattern' e
A.EqualP PatInfo
patNoRange) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Face
alpha forall a b. (a -> b) -> a -> b
$ \ (Term
phi,Bool
b) -> do
let
d :: Bool -> Term
d Bool
True = IntervalView -> Term
unview IntervalView
IOne
d Bool
False = IntervalView -> Term
unview IntervalView
IZero
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Term
phi, Bool -> Term
d Bool
b)
Patterns
ps <- forall (m :: * -> *).
MonadReify m =>
[NamedArg DeBruijnPattern] -> m Patterns
reifyPatterns forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
tel
Patterns
ps <- forall (m :: * -> *).
MonadReify m =>
Patterns -> Patterns -> m Patterns
stripImplicits [] forall a b. (a -> b) -> a -> b
$ Patterns
ps forall a. [a] -> [a] -> [a]
++ [forall a. a -> NamedArg a
defaultNamedArg Pattern
ep]
let
lhs :: SpineLHS
lhs = LHSInfo -> QName -> Patterns -> SpineLHS
SpineLHS forall a. Null a => a
empty QName
f Patterns
ps
result :: Clause
result = forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (forall a b. LHSToSpine a b => b -> a
spineToLhs SpineLHS
lhs) [] RHS
rhs WhereDeclarations
A.noWhereDecls Bool
False
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
result
instance Reify I.Type where
type ReifiesTo I.Type = A.Type
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Type -> m (ReifiesTo Type)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (I.El Sort
_ Term
t) = forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
t
instance Reify Sort where
type ReifiesTo Sort = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Sort -> m (ReifiesTo Sort)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s = do
Sort
s <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Sort
s
SortKit{QName
IsFibrant -> QName
nameOfSetOmega :: SortKit -> IsFibrant -> QName
nameOfSSet :: SortKit -> QName
nameOfProp :: SortKit -> QName
nameOfSet :: SortKit -> QName
nameOfSetOmega :: IsFibrant -> QName
nameOfSSet :: QName
nameOfProp :: QName
nameOfSet :: QName
..} <- forall (m :: * -> *). HasBuiltins m => m SortKit
infallibleSortKit
case Sort
s of
I.Type (I.ClosedLevel Integer
0) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
nameOfSet Suffix
A.NoSuffix
I.Type (I.ClosedLevel Integer
n) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
nameOfSet (Integer -> Suffix
A.Suffix Integer
n)
I.Type Level
a -> do
Expr
a <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
a
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (QName -> Expr
A.Def QName
nameOfSet) (forall a. a -> NamedArg a
defaultNamedArg Expr
a)
I.Prop (I.ClosedLevel Integer
0) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
nameOfProp Suffix
A.NoSuffix
I.Prop (I.ClosedLevel Integer
n) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' QName
nameOfProp (Integer -> Suffix
A.Suffix Integer
n)
I.Prop Level
a -> do
Expr
a <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
a
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (QName -> Expr
A.Def QName
nameOfProp) (forall a. a -> NamedArg a
defaultNamedArg Expr
a)
I.Inf IsFibrant
f Integer
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' (IsFibrant -> QName
nameOfSetOmega IsFibrant
f) Suffix
A.NoSuffix
I.Inf IsFibrant
f Integer
n -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Suffix -> Expr
A.Def' (IsFibrant -> QName
nameOfSetOmega IsFibrant
f) (Integer -> Suffix
A.Suffix Integer
n)
I.SSet Level
a -> do
I.Def QName
sset [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinStrictSet
Expr
a <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
a
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (QName -> Expr
A.Def QName
sset) (forall a. a -> NamedArg a
defaultNamedArg Expr
a)
Sort
I.SizeUniv -> do
I.Def QName
sizeU [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSizeUniv
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
sizeU
Sort
I.LockUniv -> do
QName
lockU <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
builtinLockUniv
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
lockU
Sort
I.IntervalUniv -> do
QName
intervalU <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
builtinIntervalUniv
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Expr
A.Def QName
intervalU
I.PiSort Dom' Term Term
a Sort
s1 Abs Sort
s2 -> do
Name
pis <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"piSort" :: String)
(Expr
e1,Expr
e2) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Sort
s1, ArgInfo -> Abs Term -> Term
I.Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sort -> Term
Sort Abs Sort
s2)
let app :: Expr -> Expr -> Expr
app Expr
x Expr
y = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (forall a. a -> NamedArg a
defaultNamedArg Expr
y)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
pis Expr -> Expr -> Expr
`app` Expr
e1 Expr -> Expr -> Expr
`app` Expr
e2
I.FunSort Sort
s1 Sort
s2 -> do
Name
funs <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"funSort" :: String)
(Expr
e1,Expr
e2) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Sort
s1 , Sort
s2)
let app :: Expr -> Expr -> Expr
app Expr
x Expr
y = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ Expr
x (forall a. a -> NamedArg a
defaultNamedArg Expr
y)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
funs Expr -> Expr -> Expr
`app` Expr
e1 Expr -> Expr -> Expr
`app` Expr
e2
I.UnivSort Sort
s -> do
Name
univs <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"univSort" :: String)
Expr
e <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
s
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
defaultAppInfo_ (Name -> Expr
A.Var Name
univs) forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg Expr
e
I.MetaS MetaId
x Elims
es -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
x Elims
es
I.DefS QName
d Elims
es -> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
d Elims
es
I.DummyS String
s -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprInfo -> Literal -> Expr
A.Lit forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ Text -> Literal
LitString forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
s
instance Reify Level where
type ReifiesTo Level = Expr
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Level -> m (ReifiesTo Level)
reifyWhen = forall i (m :: * -> *).
(Reify i, MonadReify m, Underscore (ReifiesTo i)) =>
Bool -> i -> m (ReifiesTo i)
reifyWhenE
reify :: forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
l = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasBuiltins m => m Bool
haveLevels (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l) forall a b. (a -> b) -> a -> b
$ do
Name
name <- forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
".#Lacking_Level_Builtins#" :: String)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
name
instance (Free i, Reify i) => Reify (Abs i) where
type ReifiesTo (Abs i) = (Name, ReifiesTo i)
reify :: forall (m :: * -> *).
MonadReify m =>
Abs i -> m (ReifiesTo (Abs i))
reify (NoAbs String
x i
v) = forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Name
name -> (Name
name,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i
v
reify (Abs String
s i
v) = do
String
s <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall a. Underscore a => a -> Bool
isUnderscore String
s Bool -> Bool -> Bool
&& Nat
0 forall a. Free a => Nat -> a -> Bool
`freeIn` i
v then String
"z" else String
s
Name
x <- forall a. LensInScope a => a -> a
C.setNotInScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ String
s
ReifiesTo i
e <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Name
x
forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i
v
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x,ReifiesTo i
e)
instance Reify I.Telescope where
type ReifiesTo I.Telescope = A.Telescope
reify :: forall (m :: * -> *).
MonadReify m =>
Telescope -> m (ReifiesTo Telescope)
reify Telescope
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return []
reify (ExtendTel Dom Type
arg Abs Telescope
tel) = do
Arg ArgInfo
info Expr
e <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Dom Type
arg
(Name
x, [TypedBinding]
bs) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Abs Telescope
tel
let r :: Range
r = forall a. HasRange a => a -> Range
getRange Expr
e
name :: Maybe (WithOrigin (Ranged String))
name = forall t e. Dom' t e -> Maybe (WithOrigin (Ranged String))
domName Dom Type
arg
Maybe Expr
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> Maybe t
domTactic Dom Type
arg
let xs :: List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged String))
name forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
-> Expr
-> TypedBinding
TBind Range
r (Maybe Expr -> Bool -> TypedBindingInfo
TypedBindingInfo Maybe Expr
tac (forall t e. Dom' t e -> Bool
domIsFinite Dom Type
arg)) List1 (Arg (Named (WithOrigin (Ranged String)) Binder))
xs Expr
e forall a. a -> [a] -> [a]
: [TypedBinding]
bs
instance Reify i => Reify (Dom i) where
type ReifiesTo (Dom i) = Arg (ReifiesTo i)
reify :: forall (m :: * -> *).
MonadReify m =>
Dom i -> m (ReifiesTo (Dom i))
reify (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = i
i}) = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i
i
instance Reify i => Reify (I.Elim' i) where
type ReifiesTo (I.Elim' i) = I.Elim' (ReifiesTo i)
reify :: forall (m :: * -> *).
MonadReify m =>
Elim' i -> m (ReifiesTo (Elim' i))
reify = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> Elim' i -> m (ReifiesTo (Elim' i))
reifyWhen Bool
b = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)
instance Reify i => Reify [i] where
type ReifiesTo [i] = [ReifiesTo i]
reify :: forall (m :: * -> *). MonadReify m => [i] -> m (ReifiesTo [i])
reify = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify
reifyWhen :: forall (m :: * -> *).
MonadReify m =>
Bool -> [i] -> m (ReifiesTo [i])
reifyWhen Bool
b = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
Bool -> i -> m (ReifiesTo i)
reifyWhen Bool
b)
instance (Reify i1, Reify i2) => Reify (i1, i2) where
type ReifiesTo (i1, i2) = (ReifiesTo i1, ReifiesTo i2)
reify :: forall (m :: * -> *).
MonadReify m =>
(i1, i2) -> m (ReifiesTo (i1, i2))
reify (i1
x,i2
y) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i1
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i2
y
instance (Reify i1, Reify i2, Reify i3) => Reify (i1,i2,i3) where
type ReifiesTo (i1, i2, i3) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)
reify :: forall (m :: * -> *).
MonadReify m =>
(i1, i2, i3) -> m (ReifiesTo (i1, i2, i3))
reify (i1
x,i2
y,i3
z) = (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i1
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i2
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i3
z
instance (Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1,i2,i3,i4) where
type ReifiesTo (i1, i2, i3, i4) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4)
reify :: forall (m :: * -> *).
MonadReify m =>
(i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4))
reify (i1
x,i2
y,i3
z,i4
w) = (,,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i1
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i2
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i3
z forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify i4
w