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)])
Int
n PTerm -> a
c PTerm
tm = do (PTerm
tm', [(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 a. a -> StateT (ElabState aux) TC a
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)])
Int
n PTerm -> PTerm -> a
c PTerm
a PTerm
b = do (PTerm
a', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
a
(PTerm
b', [(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 a. a -> StateT (ElabState aux) TC a
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)])
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 (PTactic
tac1', [(Name, PTerm)]
ex1) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac1
(PTactic
tac2', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (TSeq PTactic
tac1 PTactic
tac2)
= do (PTactic
tac1', [(Name, PTerm)]
ex1) <- Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
forall aux. Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
extractTUnquotes Int
n PTactic
tac1
(PTactic
tac2', [(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 a. a -> StateT (ElabState aux) TC a
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 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 (PTactic
tac', [(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 a. a -> StateT (ElabState aux) TC a
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 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, [])
extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
Int
d (PImp Int
p Bool
m [ArgOpt]
opts Name
n PTerm
t) =
do (PTerm
t', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
d (PExp Int
p [ArgOpt]
opts Name
n PTerm
t) =
do (PTerm
t', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
d (PConstraint Int
p [ArgOpt]
opts Name
n PTerm
t) =
do (PTerm
t', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
d (PTacImplicit Int
p [ArgOpt]
opts Name
n PTerm
scpt PTerm
t) =
do (PTerm
scpt', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
scpt
(PTerm
t', [(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 a. a -> StateT (ElabState aux) TC a
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)])
Int
d (DoExp FC
fc PTerm
tm)
= do (PTerm
tm', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
d (DoBind FC
fc Name
n FC
nfc PTerm
tm)
= do (PTerm
tm', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
d (DoBindP FC
fc PTerm
t PTerm
t' [(PTerm, PTerm)]
alts)
= String -> Elab' aux (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 (PTerm
v', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
d PTerm
v
(PTerm
b', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
d (DoLetP FC
fc PTerm
t PTerm
t' [(PTerm, PTerm)]
alts) = String -> Elab' aux (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 -> Elab' aux (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)])
Int
n (PLam FC
fc Name
name FC
nfc PTerm
ty PTerm
body)
= do (PTerm
ty', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
ty
(PTerm
body', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PPi Plicity
plicity Name
name FC
fc PTerm
ty PTerm
body)
= do (PTerm
ty', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
ty
(PTerm
body', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PLet FC
fc RigCount
rc Name
name FC
nfc PTerm
ty PTerm
val PTerm
body)
= do (PTerm
ty', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
ty
(PTerm
val', [(Name, PTerm)]
ex2) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
val
(PTerm
body', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PTyped PTerm
tm PTerm
ty)
= do (PTerm
tm', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
tm
(PTerm
ty', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PApp FC
fc PTerm
f [PArg]
args)
= do (PTerm
f', [(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 ([PArg]
args'', [[(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PAppBind FC
fc PTerm
f [PArg]
args)
= do (PTerm
f', [(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 ([PArg]
args'', [[(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PCase FC
fc PTerm
expr [(PTerm, PTerm)]
cases)
= do (PTerm
expr', [(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 ([PTerm]
pats, [PTerm]
rhss) = [(PTerm, PTerm)] -> ([PTerm], [PTerm])
forall a b. [(a, b)] -> ([a], [b])
unzip [(PTerm, PTerm)]
cases
([PTerm]
pats', [[(Name, PTerm)]]
exs1) <- ([(PTerm, [(Name, PTerm)])] -> ([PTerm], [[(Name, PTerm)]]))
-> StateT (ElabState aux) TC [(PTerm, [(Name, PTerm)])]
-> StateT (ElabState aux) TC ([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, [(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)
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]
pats
([PTerm]
rhss', [[(Name, PTerm)]]
exs2) <- ([(PTerm, [(Name, PTerm)])] -> ([PTerm], [[(Name, PTerm)]]))
-> StateT (ElabState aux) TC [(PTerm, [(Name, PTerm)])]
-> StateT (ElabState aux) TC ([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, [(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)
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]
rhss
(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 -> 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 Int
n (PIfThenElse FC
fc PTerm
c PTerm
t PTerm
f)
= do (PTerm
c', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
c
(PTerm
t', [(Name, PTerm)]
ex2) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
t
(PTerm
f', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PRewrite FC
fc Maybe Name
by PTerm
x PTerm
y Maybe PTerm
z)
= do (PTerm
x', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
x
(PTerm
y', [(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 PTerm
zz -> do (PTerm
z', [(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 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' (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)
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 (PTerm
l', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
l
(PTerm
r', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PDPair FC
fc [FC]
hls PunInfo
info PTerm
a PTerm
b PTerm
c)
= do (PTerm
a', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
a
(PTerm
b', [(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
c', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PAlternative [(Name, Name)]
ms PAltType
b [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)
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 ([PTerm]
alts'', [[(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PHidden PTerm
tm)
= do (PTerm
tm', [(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 a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
PHidden PTerm
tm', [(Name, PTerm)]
ex)
extractUnquotes Int
n (PGoal FC
fc PTerm
a Name
name PTerm
b)
= do (PTerm
a', [(Name, PTerm)]
ex1) <- Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
forall aux. Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
extractUnquotes Int
n PTerm
a
(PTerm
b', [(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 a. a -> StateT (ElabState aux) TC a
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 Int
n (PDoBlock [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)
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 ([PDo]
steps'', [[(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 a. a -> StateT (ElabState aux) TC a
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 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 ([PTactic]
tacs', [[(Name, PTerm)]]
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
(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 ([PTactic] -> PTerm
PProof [PTactic]
tacs', [[(Name, PTerm)]] -> [(Name, PTerm)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, PTerm)]]
exs)
extractUnquotes Int
n (PTactics [PTactic]
tacs)
= do ([PTactic]
tacs', [[(Name, PTerm)]]
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
(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 ([PTactic] -> PTerm
PTactics [PTactic]
tacs', [[(Name, PTerm)]] -> [(Name, PTerm)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Name, PTerm)]]
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 (PTerm
tm', [(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 a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
PCoerced PTerm
tm', [(Name, PTerm)]
ex)
extractUnquotes Int
n (PDisamb [[Text]]
ns PTerm
tm)
= do (PTerm
tm', [(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 a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Text]] -> PTerm -> PTerm
PDisamb [[Text]]
ns PTerm
tm', [(Name, PTerm)]
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 Name
n <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"unquotation")
(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 -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC String
"(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 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, [])