module Agda.Compiler.Treeless.AsPatterns (recoverAsPatterns) where

import Control.Monad.Reader

import Agda.Syntax.Treeless

data AsPat = AsPat Int QName [Int]  -- x@(c ys)
  deriving (Int -> AsPat -> ShowS
[AsPat] -> ShowS
AsPat -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AsPat] -> ShowS
$cshowList :: [AsPat] -> ShowS
show :: AsPat -> String
$cshow :: AsPat -> String
showsPrec :: Int -> AsPat -> ShowS
$cshowsPrec :: Int -> AsPat -> ShowS
Show)

wk :: Int -> AsPat -> AsPat
wk :: Int -> AsPat -> AsPat
wk Int
n (AsPat Int
x QName
c [Int]
ys) = Int -> QName -> [Int] -> AsPat
AsPat (Int
n forall a. Num a => a -> a -> a
+ Int
x) QName
c (forall a b. (a -> b) -> [a] -> [b]
map (Int
n forall a. Num a => a -> a -> a
+) [Int]
ys)

type S = Reader [AsPat]

runS :: S a -> a
runS :: forall a. S a -> a
runS S a
m = forall r a. Reader r a -> r -> a
runReader S a
m []

underBinds :: Int -> S a -> S a
underBinds :: forall a. Int -> S a -> S a
underBinds Int
0 = forall a. a -> a
id
underBinds Int
n = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ Int -> AsPat -> AsPat
wk Int
n)

bindAsPattern :: AsPat -> S a -> S a
bindAsPattern :: forall a. AsPat -> S a -> S a
bindAsPattern AsPat
p = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (AsPat
p forall a. a -> [a] -> [a]
:)

lookupAsPattern :: QName -> [TTerm] -> S TTerm
lookupAsPattern :: QName -> [TTerm] -> S TTerm
lookupAsPattern QName
c [TTerm]
vs
  | Just [Int]
xs <- [TTerm] -> Maybe [Int]
allVars [TTerm]
vs = do
    [AsPat]
ps <- forall r (m :: * -> *). MonadReader r m => m r
ask
    case [ Int
x | AsPat Int
x QName
c' [Int]
ys <- [AsPat]
ps, QName
c forall a. Eq a => a -> a -> Bool
== QName
c', [Int]
xs forall a. Eq a => a -> a -> Bool
== [Int]
ys ] of
      Int
x : [Int]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> TTerm
TVar Int
x
      [Int]
_     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
mkTApp (QName -> TTerm
TCon QName
c) [TTerm]
vs
  | Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
mkTApp (QName -> TTerm
TCon QName
c) [TTerm]
vs
  where
    allVars :: [TTerm] -> Maybe [Int]
allVars = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TTerm -> Maybe Int
getVar
    getVar :: TTerm -> Maybe Int
getVar (TVar Int
x) = forall a. a -> Maybe a
Just Int
x
    getVar TTerm
_        = forall a. Maybe a
Nothing   -- what about erased?

-- | We lose track of @-patterns in the internal syntax. This pass puts them
--   back.
recoverAsPatterns :: Monad m => TTerm -> m TTerm
recoverAsPatterns :: forall (m :: * -> *). Monad m => TTerm -> m TTerm
recoverAsPatterns TTerm
t = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. S a -> a
runS (TTerm -> S TTerm
recover TTerm
t)

recover :: TTerm -> S TTerm
recover :: TTerm -> S TTerm
recover TTerm
t =
  case TTerm
t of
    TApp TTerm
f [TTerm]
vs -> do
      TTerm
f  <- TTerm -> S TTerm
recover TTerm
f
      [TTerm]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TTerm -> S TTerm
recover [TTerm]
vs
      TTerm -> [TTerm] -> S TTerm
tApp TTerm
f [TTerm]
vs
    TLam TTerm
b -> TTerm -> TTerm
TLam forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> S a -> S a
underBinds Int
1 (TTerm -> S TTerm
recover TTerm
b)
    TCon{} -> TTerm -> [TTerm] -> S TTerm
tApp TTerm
t []   -- need to recover nullary constructors as well (to make deep @-patterns work)
    TLet TTerm
v TTerm
b -> TTerm -> TTerm -> TTerm
TLet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
recover TTerm
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Int -> S a -> S a
underBinds Int
1 (TTerm -> S TTerm
recover TTerm
b)
    TCase Int
x CaseInfo
ct TTerm
d [TAlt]
bs -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
x CaseInfo
ct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
recover TTerm
d forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> TAlt -> S TAlt
recoverAlt Int
x) [TAlt]
bs
    TCoerce TTerm
t -> TTerm -> TTerm
TCoerce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
recover TTerm
t
    TLit{}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TVar{}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TPrim{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TDef{}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TUnit{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TSort{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TErased{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
    TError{}  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t

recoverAlt :: Int -> TAlt -> S TAlt
recoverAlt :: Int -> TAlt -> S TAlt
recoverAlt Int
x TAlt
b =
  case TAlt
b of
    TACon QName
c Int
n TTerm
b -> QName -> Int -> TTerm -> TAlt
TACon QName
c Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> S a -> S a
underBinds Int
n (forall a. AsPat -> S a -> S a
bindAsPattern (Int -> QName -> [Int] -> AsPat
AsPat (Int
x forall a. Num a => a -> a -> a
+ Int
n) QName
c [Int
n forall a. Num a => a -> a -> a
- Int
1, Int
n forall a. Num a => a -> a -> a
- Int
2..Int
0]) forall a b. (a -> b) -> a -> b
$ TTerm -> S TTerm
recover TTerm
b)
    TAGuard TTerm
g TTerm
b -> TTerm -> TTerm -> TAlt
TAGuard forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
recover TTerm
g forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> S TTerm
recover TTerm
b
    TALit Literal
l TTerm
b   -> Literal -> TTerm -> TAlt
TALit Literal
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
recover TTerm
b

tApp :: TTerm -> [TTerm] -> S TTerm
tApp :: TTerm -> [TTerm] -> S TTerm
tApp (TCon QName
c) [TTerm]
vs = QName -> [TTerm] -> S TTerm
lookupAsPattern QName
c [TTerm]
vs
tApp TTerm
f [TTerm]
vs        = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
mkTApp TTerm
f [TTerm]
vs