{-|
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 :: Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
extract1 n :: Int
n c :: PTerm -> a
c tm :: PTerm
tm = do (tm' :: PTerm
tm', ex :: [(Name, PTerm)]
ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
                     (a, [(Name, PTerm)]) -> Elab' aux (a, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> a
c PTerm
tm', [(Name, PTerm)]
ex)

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

extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes n :: Int
n (Rewrite t :: 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 n :: Int
n (LetTac name :: Name
name t :: 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 n :: Int
n (LetTacTy name :: Name
name t1 :: PTerm
t1 t2 :: 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 n :: Int
n (Exact tm :: 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 n :: Int
n (Try tac1 :: PTactic
tac1 tac2 :: PTactic
tac2)
  = do (tac1' :: PTactic
tac1', ex1 :: [(Name, PTerm)]
ex1) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac1
       (tac2' :: PTactic
tac2', ex2 :: [(Name, PTerm)]
ex2) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac2
       (PTactic, [(Name, PTerm)]) -> Elab' aux (PTactic, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
Try PTactic
tac1' PTactic
tac2', [(Name, PTerm)]
ex1 [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ex2)
extractTUnquotes n :: Int
n (TSeq tac1 :: PTactic
tac1 tac2 :: PTactic
tac2)
  = do (tac1' :: PTactic
tac1', ex1 :: [(Name, PTerm)]
ex1) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac1
       (tac2' :: PTactic
tac2', ex2 :: [(Name, PTerm)]
ex2) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac2
       (PTactic, [(Name, PTerm)]) -> Elab' aux (PTactic, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq PTactic
tac1' PTactic
tac2', [(Name, PTerm)]
ex1 [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ex2)
extractTUnquotes n :: Int
n (ApplyTactic t :: 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 n :: Int
n (ByReflection t :: 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 n :: Int
n (Reflect t :: 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 n :: Int
n (GoalType s :: String
s tac :: PTactic
tac)
  = do (tac' :: PTactic
tac', ex :: [(Name, PTerm)]
ex) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac
       (PTactic, [(Name, PTerm)]) -> Elab' aux (PTactic, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> PTactic -> PTactic
forall t. String -> PTactic' t -> PTactic' t
GoalType String
s PTactic
tac', [(Name, PTerm)]
ex)
extractTUnquotes n :: Int
n (TCheck t :: 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 n :: Int
n (TEval t :: 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 n :: Int
n (Claim name :: Name
name t :: 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 n :: Int
n tac :: PTactic
tac = (PTactic, [(Name, PTerm)]) -> Elab' aux (PTactic, [(Name, PTerm)])
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 :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
extractPArgUnquotes d :: Int
d (PImp p :: Int
p m :: Bool
m opts :: [ArgOpt]
opts n :: Name
n t :: PTerm
t) =
  do (t' :: PTerm
t', ex :: [(Name, PTerm)]
ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     (PArg, [(Name, PTerm)]) -> Elab' aux (PArg, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Bool -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
PImp Int
p Bool
m [ArgOpt]
opts Name
n PTerm
t', [(Name, PTerm)]
ex)
extractPArgUnquotes d :: Int
d (PExp p :: Int
p opts :: [ArgOpt]
opts n :: Name
n t :: PTerm
t) =
  do (t' :: PTerm
t', ex :: [(Name, PTerm)]
ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     (PArg, [(Name, PTerm)]) -> Elab' aux (PArg, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
p [ArgOpt]
opts Name
n PTerm
t', [(Name, PTerm)]
ex)
extractPArgUnquotes d :: Int
d (PConstraint p :: Int
p opts :: [ArgOpt]
opts n :: Name
n t :: PTerm
t) =
  do (t' :: PTerm
t', ex :: [(Name, PTerm)]
ex) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     (PArg, [(Name, PTerm)]) -> Elab' aux (PArg, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [ArgOpt] -> Name -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PConstraint Int
p [ArgOpt]
opts Name
n PTerm
t', [(Name, PTerm)]
ex)
extractPArgUnquotes d :: Int
d (PTacImplicit p :: Int
p opts :: [ArgOpt]
opts n :: Name
n scpt :: PTerm
scpt t :: PTerm
t) =
  do (scpt' :: PTerm
scpt', ex1 :: [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
scpt
     (t' :: PTerm
t', ex2 :: [(Name, PTerm)]
ex2) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
t
     (PArg, [(Name, PTerm)]) -> Elab' aux (PArg, [(Name, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [ArgOpt] -> Name -> PTerm -> PTerm -> PArg
forall t. Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
PTacImplicit Int
p [ArgOpt]
opts Name
n PTerm
scpt' PTerm
t', [(Name, PTerm)]
ex1 [(Name, PTerm)] -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ex2)

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


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