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