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, (PDecl -> PDecl) -> [PDecl] -> [PDecl]
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) = State [(Name, FC, PTerm)] PTerm
-> [(Name, FC, PTerm)] -> (PTerm, [(Name, FC, PTerm)])
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 = ((Name, FC, PTerm) -> PTerm -> PTerm)
-> PTerm -> [(Name, FC, PTerm)] -> PTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
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)
= FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
opts Name
n ([PClause' PTerm] -> PDecl) -> [PClause' PTerm] -> PDecl
forall a b. (a -> b) -> a -> b
$ (PClause' PTerm -> PClause' PTerm)
-> [PClause' PTerm] -> [PClause' PTerm]
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) <- PTerm -> [PTerm]
forall on. Uniplate on => on -> [on]
universe PTerm
lhs ]
pats' :: [(Name, FC, PTerm)]
pats' = ((Name, FC, PTerm) -> Bool)
-> [(Name, FC, PTerm)] -> [(Name, FC, PTerm)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Name, FC, PTerm) -> Bool) -> (Name, FC, PTerm) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
bound) (Name -> Bool)
-> ((Name, FC, PTerm) -> Name) -> (Name, FC, PTerm) -> Bool
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
FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
lhs [PTerm]
ws PTerm
rhs' ([PDecl] -> PClause' PTerm) -> [PDecl] -> PClause' PTerm
forall a b. (a -> b) -> a -> b
$ (PDecl -> PDecl) -> [PDecl] -> [PDecl]
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 <- StateT [(Name, FC, PTerm)] Identity [(Name, FC, PTerm)]
forall s (m :: * -> *). MonadState s m => m s
get
[(Name, FC, PTerm)] -> StateT [(Name, FC, PTerm)] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([(Name, FC, PTerm)]
pats [(Name, FC, PTerm)] -> [(Name, FC, PTerm)] -> [(Name, FC, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name
n, FC
fc, PTerm
tm')])
PTerm -> State [(Name, FC, PTerm)] PTerm
forall a. a -> StateT [(Name, FC, PTerm)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm'
collectAs (PApp FC
fc PTerm
t [PArg]
as)
= do [PTerm]
as_tm <- (PTerm -> State [(Name, FC, PTerm)] PTerm)
-> [PTerm] -> StateT [(Name, FC, PTerm)] Identity [PTerm]
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 PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs ((PArg -> PTerm) -> [PArg] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PTerm
forall t. PArg' t -> t
getTm [PArg]
as)
let as' :: [PArg]
as' = (PArg -> PTerm -> PArg) -> [PArg] -> [PTerm] -> [PArg]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\PArg
a PTerm
tm -> PArg
a { getTm = tm }) [PArg]
as [PTerm]
as_tm
PTerm -> State [(Name, FC, PTerm)] PTerm
forall a. a -> StateT [(Name, FC, PTerm)] Identity a
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 <- StateT [(Name, FC, PTerm)] Identity [(Name, FC, PTerm)]
forall s (m :: * -> *). MonadState s m => m s
get
[PTerm]
as' <- (PTerm -> State [(Name, FC, PTerm)] PTerm)
-> [PTerm] -> StateT [(Name, FC, PTerm)] Identity [PTerm]
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 PTerm -> State [(Name, FC, PTerm)] PTerm
collectAs [PTerm]
as
[(Name, FC, PTerm)] -> StateT [(Name, FC, PTerm)] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [(Name, FC, PTerm)]
pats
PTerm -> State [(Name, FC, PTerm)] PTerm
forall a. a -> StateT [(Name, FC, PTerm)] Identity a
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' PTerm -> [PTerm] -> [PTerm]
forall a. a -> [a] -> [a]
: [PTerm]
as'))
collectAs PTerm
x = PTerm -> State [(Name, FC, PTerm)] PTerm
forall a. a -> StateT [(Name, FC, PTerm)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x
replaceUnderscore :: PTerm -> PTerm
replaceUnderscore :: PTerm -> PTerm
replaceUnderscore PTerm
tm = State Int PTerm -> Int -> PTerm
forall s a. State s a -> s -> a
evalState ((PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
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 (PTerm -> PTerm) -> State Int PTerm -> State Int PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PTerm -> State Int PTerm) -> PTerm -> State Int PTerm
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 = PTerm -> State Int PTerm
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x
fresh :: State Int Name
fresh :: State Int Name
fresh = (Int -> Int) -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) StateT Int Identity () -> State Int Name -> State Int Name
forall a b.
StateT Int Identity a
-> StateT Int Identity b -> StateT Int Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Int -> String -> Name) -> String -> Int -> Name
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> String -> Name
sMN String
"underscorePatVar" (Int -> Name) -> StateT Int Identity Int -> State Int Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT Int Identity Int
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 [] (Name -> PTerm) -> State Int Name -> State Int PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State Int Name
fresh
replaceUnderscore' PTerm
tm = PTerm -> State Int PTerm
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm