{-|
Module      : Idris.Elab.Quasiquote
Description : Code to elaborate quasiquotations.

License     : BSD3
Maintainer  : The Idris Community.
-}
module Idris.Elab.Quasiquote (extractUnquotes) where

import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.TT


extract1 :: Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 :: forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> a
c PTerm
tm = do (tm', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
                     return (c tm', ex)

extract2 :: Int -> (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract2 :: forall a aux.
Int
-> (PTerm -> PTerm -> a)
-> PTerm
-> PTerm
-> Elab' aux (a, [(Name, PTerm)])
extract2 Int
n PTerm -> PTerm -> a
c PTerm
a PTerm
b = do (a', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
a
                      (b', ex2) <- extractUnquotes n b
                      return (c a' b', ex1 ++ ex2)

extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes :: forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n (Rewrite PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
Rewrite PTerm
t
extractTUnquotes Int
n (LetTac Name
name PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n (Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
LetTac Name
name) PTerm
t
extractTUnquotes Int
n (LetTacTy Name
name PTerm
t1 PTerm
t2) = Int
-> (PTerm -> PTerm -> PTactic)
-> PTerm
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int
-> (PTerm -> PTerm -> a)
-> PTerm
-> PTerm
-> Elab' aux (a, [(Name, PTerm)])
extract2 Int
n (Name -> PTerm -> PTerm -> PTactic
forall t. Name -> t -> t -> PTactic' t
LetTacTy Name
name) PTerm
t1 PTerm
t2
extractTUnquotes Int
n (Exact PTerm
tm) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
Exact PTerm
tm
extractTUnquotes Int
n (Try PTactic
tac1 PTactic
tac2)
  = do (tac1', ex1) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac1
       (tac2', ex2) <- extractTUnquotes n tac2
       return (Try tac1' tac2', ex1 ++ ex2)
extractTUnquotes Int
n (TSeq PTactic
tac1 PTactic
tac2)
  = do (tac1', ex1) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac1
       (tac2', ex2) <- extractTUnquotes n tac2
       return (TSeq tac1' tac2', ex1 ++ ex2)
extractTUnquotes Int
n (ApplyTactic PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
ApplyTactic PTerm
t
extractTUnquotes Int
n (ByReflection PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
ByReflection PTerm
t
extractTUnquotes Int
n (Reflect PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
Reflect PTerm
t
extractTUnquotes Int
n (GoalType String
s PTactic
tac)
  = do (tac', ex) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac
       return (GoalType s tac', ex)
extractTUnquotes Int
n (TCheck PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
TCheck PTerm
t
extractTUnquotes Int
n (TEval PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n PTerm -> PTactic
forall t. t -> PTactic' t
TEval PTerm
t
extractTUnquotes Int
n (Claim Name
name PTerm
t) = Int
-> (PTerm -> PTactic)
-> PTerm
-> Elab' aux (PTactic, [(Name, PTerm)])
forall a aux.
Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 Int
n (Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
Claim Name
name) PTerm
t
extractTUnquotes Int
n PTactic
tac = (PTactic, [(Name, PTerm)]) -> Elab' aux (PTactic, [(Name, PTerm)])
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic
tac, []) -- the rest don't contain PTerms, or have been desugared away

extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
extractPArgUnquotes :: forall aux. Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
extractPArgUnquotes Int
d (PImp Int
p Bool
m [ArgOpt]
opts Name
n PTerm
t) =
  do (t', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     return (PImp p m opts n t', ex)
extractPArgUnquotes Int
d (PExp Int
p [ArgOpt]
opts Name
n PTerm
t) =
  do (t', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     return (PExp p opts n t', ex)
extractPArgUnquotes Int
d (PConstraint Int
p [ArgOpt]
opts Name
n PTerm
t) =
  do (t', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     return (PConstraint p opts n t', ex)
extractPArgUnquotes Int
d (PTacImplicit Int
p [ArgOpt]
opts Name
n PTerm
scpt PTerm
t) =
  do (scpt', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
scpt
     (t', ex2) <- extractUnquotes d t
     return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)

extractDoUnquotes :: Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])
extractDoUnquotes :: forall aux. Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])
extractDoUnquotes Int
d (DoExp FC
fc PTerm
tm)
  = do (tm', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
tm
       return (DoExp fc tm', ex)
extractDoUnquotes Int
d (DoBind FC
fc Name
n FC
nfc PTerm
tm)
  = do (tm', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
tm
       return (DoBind fc n nfc tm', ex)
extractDoUnquotes Int
d (DoBindP FC
fc PTerm
t PTerm
t' [(PTerm, PTerm)]
alts)
  = String -> StateT (ElabState aux) TC (PDo, [(Name, PTerm)])
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Pattern-matching binds cannot be quasiquoted"
extractDoUnquotes Int
d (DoLet  FC
fc RigCount
rc Name
n FC
nfc PTerm
v PTerm
b)
  = do (v', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
v
       (b', ex2) <- extractUnquotes d b
       return (DoLet fc rc n nfc v' b', ex1 ++ ex2)
extractDoUnquotes Int
d (DoLetP FC
fc PTerm
t PTerm
t' [(PTerm, PTerm)]
alts) = String -> StateT (ElabState aux) TC (PDo, [(Name, PTerm)])
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Pattern-matching lets cannot be quasiquoted"
extractDoUnquotes Int
d (DoRewrite FC
fc PTerm
h) = String -> StateT (ElabState aux) TC (PDo, [(Name, PTerm)])
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Rewrites in Do block cannot be quasiquoted"


extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes :: forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n (PLam FC
fc Name
name FC
nfc PTerm
ty PTerm
body)
  = do (ty', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
ty
       (body', ex2) <- extractUnquotes n body
       return (PLam fc name nfc ty' body', ex1 ++ ex2)
extractUnquotes Int
n (PPi Plicity
plicity Name
name FC
fc PTerm
ty PTerm
body)
  = do (ty', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
ty
       (body', ex2) <- extractUnquotes n body
       return (PPi plicity name fc ty' body', ex1 ++ ex2)
extractUnquotes Int
n (PLet FC
fc RigCount
rc Name
name FC
nfc PTerm
ty PTerm
val PTerm
body)
  = do (ty', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
ty
       (val', ex2) <- extractUnquotes n val
       (body', ex3) <- extractUnquotes n body
       return (PLet fc rc name nfc ty' val' body', ex1 ++ ex2 ++ ex3)
extractUnquotes Int
n (PTyped PTerm
tm PTerm
ty)
  = do (tm', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
       (ty', ex2) <- extractUnquotes n ty
       return (PTyped tm' ty', ex1 ++ ex2)
extractUnquotes Int
n (PApp FC
fc PTerm
f [PArg]
args)
  = do (f', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
f
       args' <- mapM (extractPArgUnquotes n) args
       let (args'', exs) = unzip args'
       return (PApp fc f' args'', ex1 ++ concat exs)
extractUnquotes Int
n (PAppBind FC
fc PTerm
f [PArg]
args)
  = do (f', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
f
       args' <- mapM (extractPArgUnquotes n) args
       let (args'', exs) = unzip args'
       return (PAppBind fc f' args'', ex1 ++ concat exs)
extractUnquotes Int
n (PCase FC
fc PTerm
expr [(PTerm, PTerm)]
cases)
  = do (expr', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
expr
       let (pats, rhss) = unzip cases
       (pats', exs1) <- fmap unzip $ mapM (extractUnquotes n) pats
       (rhss', exs2) <- fmap unzip $ mapM (extractUnquotes n) rhss
       return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
extractUnquotes Int
n (PIfThenElse FC
fc PTerm
c PTerm
t PTerm
f)
  = do (c', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
c
       (t', ex2) <- extractUnquotes n t
       (f', ex3) <- extractUnquotes n f
       return (PIfThenElse fc c' t' f', ex1 ++ ex2 ++ ex3)
extractUnquotes Int
n (PRewrite FC
fc Maybe Name
by PTerm
x PTerm
y Maybe PTerm
z)
  = do (x', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
x
       (y', ex2) <- extractUnquotes n y
       case z of
         Just PTerm
zz -> do (z', ex3) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
zz
                       return (PRewrite fc by x' y' (Just z'), ex1 ++ ex2 ++ ex3)
         Maybe PTerm
Nothing -> (PTerm, [(Name, PTerm)]) -> Elab' aux (PTerm, [(Name, PTerm)])
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
by PTerm
x' PTerm
y' Maybe PTerm
forall a. Maybe a
Nothing, [(Name, PTerm)]
ex1 [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ex2)
extractUnquotes Int
n (PPair FC
fc [FC]
hls PunInfo
info PTerm
l PTerm
r)
  = do (l', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
l
       (r', ex2) <- extractUnquotes n r
       return (PPair fc hls info l' r', ex1 ++ ex2)
extractUnquotes Int
n (PDPair FC
fc [FC]
hls PunInfo
info PTerm
a PTerm
b PTerm
c)
  = do (a', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
a
       (b', ex2) <- extractUnquotes n b
       (c', ex3) <- extractUnquotes n c
       return (PDPair fc hls info a' b' c', ex1 ++ ex2 ++ ex3)
extractUnquotes Int
n (PAlternative [(Name, Name)]
ms PAltType
b [PTerm]
alts)
  = do alts' <- (PTerm -> Elab' aux (PTerm, [(Name, PTerm)]))
-> [PTerm] -> StateT (ElabState aux) TC [(PTerm, [(Name, 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 (Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n) [PTerm]
alts
       let (alts'', exs) = unzip alts'
       return (PAlternative ms b alts'', concat exs)
extractUnquotes Int
n (PHidden PTerm
tm)
  = do (tm', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
       return (PHidden tm', ex)
extractUnquotes Int
n (PGoal FC
fc PTerm
a Name
name PTerm
b)
  = do (a', ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
a
       (b', ex2) <- extractUnquotes n b
       return (PGoal fc a' name b', ex1 ++ ex2)
extractUnquotes Int
n (PDoBlock [PDo]
steps)
  = do steps' <- (PDo -> StateT (ElabState aux) TC (PDo, [(Name, PTerm)]))
-> [PDo] -> StateT (ElabState aux) TC [(PDo, [(Name, 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 (Int -> PDo -> StateT (ElabState aux) TC (PDo, [(Name, PTerm)])
forall aux. Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])
extractDoUnquotes Int
n) [PDo]
steps
       let (steps'', exs) = unzip steps'
       return (PDoBlock steps'', concat exs)
extractUnquotes Int
n (PIdiom FC
fc PTerm
tm)
  = ((PTerm, [(Name, PTerm)]) -> (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(PTerm
tm', [(Name, PTerm)]
ex) -> (FC -> PTerm -> PTerm
PIdiom FC
fc PTerm
tm', [(Name, PTerm)]
ex)) (Elab' aux (PTerm, [(Name, PTerm)])
 -> Elab' aux (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b. (a -> b) -> a -> b
$ Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
extractUnquotes Int
n (PProof [PTactic]
tacs)
  = do (tacs', exs) <- ([(PTactic, [(Name, PTerm)])] -> ([PTactic], [[(Name, PTerm)]]))
-> StateT (ElabState aux) TC [(PTactic, [(Name, PTerm)])]
-> StateT (ElabState aux) TC ([PTactic], [[(Name, PTerm)]])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(PTactic, [(Name, PTerm)])] -> ([PTactic], [[(Name, PTerm)]])
forall a b. [(a, b)] -> ([a], [b])
unzip (StateT (ElabState aux) TC [(PTactic, [(Name, PTerm)])]
 -> StateT (ElabState aux) TC ([PTactic], [[(Name, PTerm)]]))
-> StateT (ElabState aux) TC [(PTactic, [(Name, PTerm)])]
-> StateT (ElabState aux) TC ([PTactic], [[(Name, PTerm)]])
forall a b. (a -> b) -> a -> b
$ (PTactic -> StateT (ElabState aux) TC (PTactic, [(Name, PTerm)]))
-> [PTactic]
-> StateT (ElabState aux) TC [(PTactic, [(Name, 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 (Int
-> PTactic -> StateT (ElabState aux) TC (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n) [PTactic]
tacs
       return (PProof tacs', concat exs)
extractUnquotes Int
n (PTactics [PTactic]
tacs)
  = do (tacs', exs) <- ([(PTactic, [(Name, PTerm)])] -> ([PTactic], [[(Name, PTerm)]]))
-> StateT (ElabState aux) TC [(PTactic, [(Name, PTerm)])]
-> StateT (ElabState aux) TC ([PTactic], [[(Name, PTerm)]])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(PTactic, [(Name, PTerm)])] -> ([PTactic], [[(Name, PTerm)]])
forall a b. [(a, b)] -> ([a], [b])
unzip (StateT (ElabState aux) TC [(PTactic, [(Name, PTerm)])]
 -> StateT (ElabState aux) TC ([PTactic], [[(Name, PTerm)]]))
-> StateT (ElabState aux) TC [(PTactic, [(Name, PTerm)])]
-> StateT (ElabState aux) TC ([PTactic], [[(Name, PTerm)]])
forall a b. (a -> b) -> a -> b
$ (PTactic -> StateT (ElabState aux) TC (PTactic, [(Name, PTerm)]))
-> [PTactic]
-> StateT (ElabState aux) TC [(PTactic, [(Name, 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 (Int
-> PTactic -> StateT (ElabState aux) TC (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n) [PTactic]
tacs
       return (PTactics tacs', concat exs)
extractUnquotes Int
n (PElabError Err
err) = String -> Elab' aux (PTerm, [(Name, PTerm)])
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't quasiquote an error"
extractUnquotes Int
n (PCoerced PTerm
tm)
  = do (tm', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
       return (PCoerced tm', ex)
extractUnquotes Int
n (PDisamb [[Text]]
ns PTerm
tm)
  = do (tm', ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
       return (PDisamb ns tm', ex)
extractUnquotes Int
n (PUnifyLog PTerm
tm)
  = ((PTerm, [(Name, PTerm)]) -> (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(PTerm
tm', [(Name, PTerm)]
ex) -> (PTerm -> PTerm
PUnifyLog PTerm
tm', [(Name, PTerm)]
ex)) (Elab' aux (PTerm, [(Name, PTerm)])
 -> Elab' aux (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b. (a -> b) -> a -> b
$ Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
extractUnquotes Int
n (PNoImplicits PTerm
tm)
  = ((PTerm, [(Name, PTerm)]) -> (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(PTerm
tm', [(Name, PTerm)]
ex) -> (PTerm -> PTerm
PNoImplicits PTerm
tm', [(Name, PTerm)]
ex)) (Elab' aux (PTerm, [(Name, PTerm)])
 -> Elab' aux (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b. (a -> b) -> a -> b
$ Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
extractUnquotes Int
n (PQuasiquote PTerm
tm Maybe PTerm
goal)
  = ((PTerm, [(Name, PTerm)]) -> (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(PTerm
tm', [(Name, PTerm)]
ex) -> (PTerm -> Maybe PTerm -> PTerm
PQuasiquote PTerm
tm' Maybe PTerm
goal, [(Name, PTerm)]
ex)) (Elab' aux (PTerm, [(Name, PTerm)])
 -> Elab' aux (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b. (a -> b) -> a -> b
$ Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) PTerm
tm
extractUnquotes Int
n (PUnquote PTerm
tm)
  | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = do n <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"unquotation")
                return (PRef (fileFC "(unquote)") [] n, [(n, tm)])
  | Bool
otherwise = ((PTerm, [(Name, PTerm)]) -> (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(PTerm
tm', [(Name, PTerm)]
ex) -> (PTerm -> PTerm
PUnquote PTerm
tm', [(Name, PTerm)]
ex)) (Elab' aux (PTerm, [(Name, PTerm)])
 -> Elab' aux (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b. (a -> b) -> a -> b
$
                Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) PTerm
tm
extractUnquotes Int
n (PRunElab FC
fc PTerm
tm [String]
ns)
  = ((PTerm, [(Name, PTerm)]) -> (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(PTerm
tm', [(Name, PTerm)]
ex) -> (FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc PTerm
tm' [String]
ns, [(Name, PTerm)]
ex)) (Elab' aux (PTerm, [(Name, PTerm)])
 -> Elab' aux (PTerm, [(Name, PTerm)]))
-> Elab' aux (PTerm, [(Name, PTerm)])
-> Elab' aux (PTerm, [(Name, PTerm)])
forall a b. (a -> b) -> a -> b
$ Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
extractUnquotes Int
n (PConstSugar FC
fc PTerm
tm)
  = Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
extractUnquotes Int
n PTerm
x = (PTerm, [(Name, PTerm)]) -> Elab' aux (PTerm, [(Name, PTerm)])
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
x, []) -- no subterms!