module Idris.Elab.AsPat(desugarAs) where
import Idris.AbsSyntax
import Idris.Core.TT
import Control.Monad.State.Strict
import Data.Generics.Uniplate.Data (transformM, universe)
desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])
desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])
desugarAs PTerm
lhs PTerm
rhs [PDecl]
whereblock
= (PTerm
lhs', PTerm -> [(Name, FC, PTerm)] -> PTerm
bindOnRight PTerm
rhs [(Name, FC, PTerm)]
pats, forall a b. (a -> b) -> [a] -> [b]
map ([(Name, FC, PTerm)] -> PDecl -> PDecl
bindInWhereDecl [(Name, FC, PTerm)]
pats) [PDecl]
whereblock)
where
(PTerm
lhs', [(Name, FC, PTerm)]
pats) = forall s a. State s a -> s -> (a, s)
runState (PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs (PTerm -> PTerm
replaceUnderscore PTerm
lhs)) []
bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm
bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm
bindOnRight = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
n, FC
fc, PTerm
tm) -> FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
RigW Name
n FC
NoFC PTerm
Placeholder PTerm
tm)
bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl
bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl
bindInWhereDecl [(Name, FC, PTerm)]
pats (PClauses FC
fc FnOpts
opts Name
n [PClause' PTerm]
clauses)
= forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opts Name
n forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([(Name, FC, PTerm)] -> PClause' PTerm -> PClause' PTerm
bindInWhereClause [(Name, FC, PTerm)]
pats) [PClause' PTerm]
clauses
bindInWhereDecl [(Name, FC, PTerm)]
_ PDecl
d = PDecl
d
bindInWhereClause :: [(Name, FC, PTerm)] -> PClause -> PClause
bindInWhereClause :: [(Name, FC, PTerm)] -> PClause' PTerm -> PClause' PTerm
bindInWhereClause [(Name, FC, PTerm)]
pats (PClause FC
fc Name
n PTerm
lhs [PTerm]
ws PTerm
rhs [PDecl]
wb)
= let bound :: [Name]
bound = [ Name
n | (PRef FC
_ [FC]
_ Name
n) <- forall on. Uniplate on => on -> [on]
universe PTerm
lhs ]
pats' :: [(Name, FC, PTerm)]
pats' = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
bound) forall b c a. (b -> c) -> (a -> b) -> a -> c
. \(Name
n,FC
_,PTerm
_) -> Name
n) [(Name, FC, PTerm)]
pats
rhs' :: PTerm
rhs' = PTerm -> [(Name, FC, PTerm)] -> PTerm
bindOnRight PTerm
rhs [(Name, FC, PTerm)]
pats' in
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
lhs [PTerm]
ws PTerm
rhs' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([(Name, FC, PTerm)] -> PDecl -> PDecl
bindInWhereDecl [(Name, FC, PTerm)]
pats') [PDecl]
wb
bindInWhereClause [(Name, FC, PTerm)]
_ PClause' PTerm
c = PClause' PTerm
c
collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs (PAs FC
fc Name
n PTerm
tm) = do PTerm
tm' <- PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs PTerm
tm
[(Name, FC, PTerm)]
pats <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([(Name, FC, PTerm)]
pats forall a. [a] -> [a] -> [a]
++ [(Name
n, FC
fc, PTerm
tm')])
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm'
collectAs (PApp FC
fc PTerm
t [PArg]
as)
= do [PTerm]
as_tm <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs (forall a b. (a -> b) -> [a] -> [b]
map forall t. PArg' t -> t
getTm [PArg]
as)
let as' :: [PArg]
as' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\PArg
a PTerm
tm -> PArg
a { getTm :: PTerm
getTm = PTerm
tm }) [PArg]
as [PTerm]
as_tm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t [PArg]
as')
collectAs tm :: PTerm
tm@(PAlternative [(Name, Name)]
ns (ExactlyOne Bool
d) (PTerm
a : [PTerm]
as))
= do PTerm
a' <- PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs PTerm
a
[(Name, FC, PTerm)]
pats <- forall s (m :: * -> *). MonadState s m => m s
get
[PTerm]
as' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs [PTerm]
as
forall s (m :: * -> *). MonadState s m => s -> m ()
put [(Name, FC, PTerm)]
pats
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ns (Bool -> PAltType
ExactlyOne Bool
d) (PTerm
a' forall a. a -> [a] -> [a]
: [PTerm]
as'))
collectAs PTerm
x = forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x
replaceUnderscore :: PTerm -> PTerm
replaceUnderscore :: PTerm -> PTerm
replaceUnderscore PTerm
tm = forall s a. State s a -> s -> a
evalState (forall (m :: * -> *) on.
(Monad m, Applicative m, Uniplate on) =>
(on -> m on) -> on -> m on
transformM ((PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
underAs PTerm -> State Int PTerm
replaceUnderscore') PTerm
tm) Int
0
where
underAs :: (PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
underAs :: (PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
underAs PTerm -> State Int PTerm
f (PAs FC
fc Name
n PTerm
tm) = FC -> Name -> PTerm -> PTerm
PAs FC
fc Name
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) on.
(Monad m, Applicative m, Uniplate on) =>
(on -> m on) -> on -> m on
transformM PTerm -> State Int PTerm
f PTerm
tm
underAs PTerm -> State Int PTerm
f PTerm
x = forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x
fresh :: State Int Name
fresh :: State Int Name
fresh = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Num a => a -> a -> a
+Int
1) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> String -> Name
sMN String
"underscorePatVar" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
replaceUnderscore' :: PTerm -> State Int PTerm
replaceUnderscore' :: PTerm -> State Int PTerm
replaceUnderscore' PTerm
Placeholder = FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State Int Name
fresh
replaceUnderscore' PTerm
tm = forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm