{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
module Idris.Core.ProofTerm(
ProofTerm, Goal(..), mkProofTerm, getProofTerm
, resetProofTerm
, updateSolved, updateSolvedTerm, updateSolvedTerm'
, bound_in, bound_in_term, refocus, updsubst
, Hole, RunTactic'
, goal, atHole
) where
import Idris.Core.Evaluate
import Idris.Core.TT
import Control.Monad
import Control.Monad.State.Strict
data TermPath = Top
| AppL (AppStatus Name) TermPath Term
| AppR (AppStatus Name) Term TermPath
| InBind Name BinderPath Term
| InScope Name (Binder Term) TermPath
deriving Int -> TermPath -> ShowS
[TermPath] -> ShowS
TermPath -> String
(Int -> TermPath -> ShowS)
-> (TermPath -> String) -> ([TermPath] -> ShowS) -> Show TermPath
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TermPath -> ShowS
showsPrec :: Int -> TermPath -> ShowS
$cshow :: TermPath -> String
show :: TermPath -> String
$cshowList :: [TermPath] -> ShowS
showList :: [TermPath] -> ShowS
Show
data BinderPath = Binder (Binder TermPath)
| LetT RigCount TermPath Term
| LetV RigCount Term TermPath
| GuessT TermPath Term
| GuessV Term TermPath
deriving Int -> BinderPath -> ShowS
[BinderPath] -> ShowS
BinderPath -> String
(Int -> BinderPath -> ShowS)
-> (BinderPath -> String)
-> ([BinderPath] -> ShowS)
-> Show BinderPath
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BinderPath -> ShowS
showsPrec :: Int -> BinderPath -> ShowS
$cshow :: BinderPath -> String
show :: BinderPath -> String
$cshowList :: [BinderPath] -> ShowS
showList :: [BinderPath] -> ShowS
Show
replaceTop :: TermPath -> TermPath -> TermPath
replaceTop :: TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
Top = TermPath
p
replaceTop TermPath
p (AppL AppStatus Name
s TermPath
l Term
t) = AppStatus Name -> TermPath -> Term -> TermPath
AppL AppStatus Name
s (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
l) Term
t
replaceTop TermPath
p (AppR AppStatus Name
s Term
t TermPath
r) = AppStatus Name -> Term -> TermPath -> TermPath
AppR AppStatus Name
s Term
t (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
r)
replaceTop TermPath
p (InBind Name
n BinderPath
bp Term
sc) = Name -> BinderPath -> Term -> TermPath
InBind Name
n (TermPath -> BinderPath -> BinderPath
replaceTopB TermPath
p BinderPath
bp) Term
sc
where
replaceTopB :: TermPath -> BinderPath -> BinderPath
replaceTopB TermPath
p (Binder Binder TermPath
b) = Binder TermPath -> BinderPath
Binder ((TermPath -> TermPath) -> Binder TermPath -> Binder TermPath
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TermPath -> TermPath -> TermPath
replaceTop TermPath
p) Binder TermPath
b)
replaceTopB TermPath
p (LetT RigCount
c TermPath
t Term
v) = RigCount -> TermPath -> Term -> BinderPath
LetT RigCount
c (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
t) Term
v
replaceTopB TermPath
p (LetV RigCount
c Term
t TermPath
v) = RigCount -> Term -> TermPath -> BinderPath
LetV RigCount
c Term
t (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
v)
replaceTopB TermPath
p (GuessT TermPath
t Term
v) = TermPath -> Term -> BinderPath
GuessT (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
t) Term
v
replaceTopB TermPath
p (GuessV Term
t TermPath
v) = Term -> TermPath -> BinderPath
GuessV Term
t (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
v)
replaceTop TermPath
p (InScope Name
n Binder Term
b TermPath
sc) = Name -> Binder Term -> TermPath -> TermPath
InScope Name
n Binder Term
b (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
sc)
rebuildTerm :: Term -> TermPath -> Term
rebuildTerm :: Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
Top = Term
tm
rebuildTerm Term
tm (AppL AppStatus Name
s TermPath
p Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p) Term
a
rebuildTerm Term
tm (AppR AppStatus Name
s Term
f TermPath
p) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Term
f (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p)
rebuildTerm Term
tm (InScope Name
n Binder Term
b TermPath
p) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p)
rebuildTerm Term
tm (InBind Name
n BinderPath
bp Term
sc) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Term -> BinderPath -> Binder Term
rebuildBinder Term
tm BinderPath
bp) Term
sc
rebuildBinder :: Term -> BinderPath -> Binder Term
rebuildBinder :: Term -> BinderPath -> Binder Term
rebuildBinder Term
tm (Binder Binder TermPath
p) = (TermPath -> Term) -> Binder TermPath -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> TermPath -> Term
rebuildTerm Term
tm) Binder TermPath
p
rebuildBinder Term
tm (LetT RigCount
c TermPath
p Term
t) = RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p) Term
t
rebuildBinder Term
tm (LetV RigCount
c Term
v TermPath
p) = RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c Term
v (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p)
rebuildBinder Term
tm (GuessT TermPath
p Term
t) = Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p) Term
t
rebuildBinder Term
tm (GuessV Term
v TermPath
p) = Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
v (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p)
findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
findHole Name
n Env
env Term
t = Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
Top Term
t where
fh' :: Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path tm :: Term
tm@(Bind Name
x Binder Term
h Term
sc)
| Binder Term -> Bool
forall b. Binder b -> Bool
hole Binder Term
h Bool -> Bool -> Bool
&& Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = (TermPath, Env, Term) -> Maybe (TermPath, Env, Term)
forall a. a -> Maybe a
Just (TermPath
path, Env
env, Term
tm)
fh' Env
env TermPath
path (App AppStatus Name
Complete Term
_ Term
_) = Maybe (TermPath, Env, Term)
forall a. Maybe a
Nothing
fh' Env
env TermPath
path (App AppStatus Name
s Term
f Term
a)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path Term
a = (TermPath, Env, Term) -> Maybe (TermPath, Env, Term)
forall a. a -> Maybe a
Just (AppStatus Name -> Term -> TermPath -> TermPath
AppR AppStatus Name
s Term
f TermPath
p, Env
env', Term
tm)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path Term
f = (TermPath, Env, Term) -> Maybe (TermPath, Env, Term)
forall a. a -> Maybe a
Just (AppStatus Name -> TermPath -> Term -> TermPath
AppL AppStatus Name
s TermPath
p Term
a, Env
env', Term
tm)
fh' Env
env TermPath
path (Bind Name
x Binder Term
b Term
sc)
| Just (BinderPath
bp, Env
env', Term
tm) <- Env -> TermPath -> Binder Term -> Maybe (BinderPath, Env, Term)
fhB Env
env TermPath
path Binder Term
b = (TermPath, Env, Term) -> Maybe (TermPath, Env, Term)
forall a. a -> Maybe a
Just (Name -> BinderPath -> Term -> TermPath
InBind Name
x BinderPath
bp Term
sc, Env
env', Term
tm)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' ((Name
x,Binder Term -> RigCount
getRig Binder Term
b,Binder Term
b)(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) TermPath
path Term
sc = (TermPath, Env, Term) -> Maybe (TermPath, Env, Term)
forall a. a -> Maybe a
Just (Name -> Binder Term -> TermPath -> TermPath
InScope Name
x Binder Term
b TermPath
p, Env
env', Term
tm)
fh' Env
_ TermPath
_ Term
_ = Maybe (TermPath, Env, Term)
forall a. Maybe a
Nothing
fhB :: Env -> TermPath -> Binder Term -> Maybe (BinderPath, Env, Term)
fhB Env
env TermPath
path (Let RigCount
c Term
t Term
v)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path Term
t = (BinderPath, Env, Term) -> Maybe (BinderPath, Env, Term)
forall a. a -> Maybe a
Just (RigCount -> TermPath -> Term -> BinderPath
LetT RigCount
c TermPath
p Term
v, Env
env', Term
tm)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path Term
v = (BinderPath, Env, Term) -> Maybe (BinderPath, Env, Term)
forall a. a -> Maybe a
Just (RigCount -> Term -> TermPath -> BinderPath
LetV RigCount
c Term
t TermPath
p, Env
env', Term
tm)
fhB Env
env TermPath
path (Guess Term
t Term
v)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path Term
t = (BinderPath, Env, Term) -> Maybe (BinderPath, Env, Term)
forall a. a -> Maybe a
Just (TermPath -> Term -> BinderPath
GuessT TermPath
p Term
v, Env
env', Term
tm)
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path Term
v = (BinderPath, Env, Term) -> Maybe (BinderPath, Env, Term)
forall a. a -> Maybe a
Just (Term -> TermPath -> BinderPath
GuessV Term
t TermPath
p, Env
env', Term
tm)
fhB Env
env TermPath
path Binder Term
b
| Just (TermPath
p, Env
env', Term
tm) <- Env -> TermPath -> Term -> Maybe (TermPath, Env, Term)
fh' Env
env TermPath
path (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
= (BinderPath, Env, Term) -> Maybe (BinderPath, Env, Term)
forall a. a -> Maybe a
Just (Binder TermPath -> BinderPath
Binder ((Term -> TermPath) -> Binder Term -> Binder TermPath
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Term
_ -> TermPath
p) Binder Term
b), Env
env', Term
tm)
fhB Env
_ TermPath
_ Binder Term
_ = Maybe (BinderPath, Env, Term)
forall a. Maybe a
Nothing
data ProofTerm = PT {
ProofTerm -> TermPath
path :: TermPath,
ProofTerm -> Env
subterm_env :: Env,
ProofTerm -> Term
subterm :: Term,
ProofTerm -> [(Name, Term)]
updates :: [(Name, Term)] }
deriving Int -> ProofTerm -> ShowS
[ProofTerm] -> ShowS
ProofTerm -> String
(Int -> ProofTerm -> ShowS)
-> (ProofTerm -> String)
-> ([ProofTerm] -> ShowS)
-> Show ProofTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProofTerm -> ShowS
showsPrec :: Int -> ProofTerm -> ShowS
$cshow :: ProofTerm -> String
show :: ProofTerm -> String
$cshowList :: [ProofTerm] -> ShowS
showList :: [ProofTerm] -> ShowS
Show
type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
type Hole = Maybe Name
refocus :: Hole -> ProofTerm -> ProofTerm
refocus :: Hole -> ProofTerm -> ProofTerm
refocus Hole
h ProofTerm
t = let res :: ProofTerm
res = Hole -> ProofTerm -> ProofTerm
refocus' Hole
h ProofTerm
t in ProofTerm
res
refocus' :: Hole -> ProofTerm -> ProofTerm
refocus' (Just Name
n) pt :: ProofTerm
pt@(PT TermPath
path Env
env Term
tm [(Name, Term)]
ups)
| Just (TermPath
p', Env
env', Term
tm') <- Name -> Env -> Term -> Maybe (TermPath, Env, Term)
findHole Name
n Env
env Term
tm
= TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT (TermPath -> TermPath -> TermPath
replaceTop TermPath
p' TermPath
path) Env
env' Term
tm' [(Name, Term)]
ups
| Just (TermPath
p', Env
env', Term
tm') <- Name -> Env -> Term -> Maybe (TermPath, Env, Term)
findHole Name
n [] (Term -> TermPath -> Term
rebuildTerm Term
tm ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ups TermPath
path))
= TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT TermPath
p' Env
env' Term
tm' []
| Bool
otherwise = ProofTerm
pt
refocus' Hole
_ ProofTerm
pt = ProofTerm
pt
data Goal = GD { Goal -> Env
premises :: Env,
Goal -> Binder Term
goalType :: Binder Term
}
mkProofTerm :: Term -> ProofTerm
mkProofTerm :: Term -> ProofTerm
mkProofTerm Term
tm = TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT TermPath
Top [] Term
tm []
getProofTerm :: ProofTerm -> Term
getProofTerm :: ProofTerm -> Term
getProofTerm (PT TermPath
path Env
_ Term
sub [(Name, Term)]
ups) = Term -> TermPath -> Term
rebuildTerm Term
sub ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ups TermPath
path)
resetProofTerm :: ProofTerm -> ProofTerm
resetProofTerm :: ProofTerm -> ProofTerm
resetProofTerm = Term -> ProofTerm
mkProofTerm (Term -> ProofTerm)
-> (ProofTerm -> Term) -> ProofTerm -> ProofTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofTerm -> Term
getProofTerm
same :: Eq a => Maybe a -> a -> Bool
same :: forall a. Eq a => Maybe a -> a -> Bool
same Maybe a
Nothing a
n = Bool
True
same (Just a
x) a
n = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n
hole :: Binder b -> Bool
hole :: forall b. Binder b -> Bool
hole (Hole b
_) = Bool
True
hole (Guess b
_ b
_) = Bool
True
hole Binder b
_ = Bool
False
updateSolvedTerm :: [(Name, Term)] -> Term -> Term
updateSolvedTerm :: [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
xs Term
x = (Term, Bool) -> Term
forall a b. (a, b) -> a
fst ((Term, Bool) -> Term) -> (Term, Bool) -> Term
forall a b. (a -> b) -> a -> b
$ [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
xs Term
x
updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [] Term
x = (Term
x, Bool
False)
updateSolvedTerm' [(Name, Term)]
xs Term
x = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
x where
updateSolved' :: [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [] Term
x = (Term
x, Bool
False)
updateSolved' [(Name, Term)]
xs (Bind Name
n (Hole Term
ty) Term
t)
| Just Term
v <- Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
xs
= case [(Name, Term)]
xs of
[(Name, Term)
_] -> (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
n Term
v Term
t, Bool
True)
[(Name, Term)]
_ -> let (Term
t', Bool
_) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t in
(Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
n Term
v Term
t', Bool
True)
updateSolved' [(Name, Term)]
xs tm :: Term
tm@(Bind Name
n Binder Term
b Term
t)
= let (Term
t', Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t
(Binder Term
b', Bool
ub) = [(Name, Term)] -> Binder Term -> (Binder Term, Bool)
updateSolvedB' [(Name, Term)]
xs Binder Term
b in
if Bool
ut Bool -> Bool -> Bool
|| Bool
ub then (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
t', Bool
True)
else (Term
tm, Bool
False)
updateSolved' [(Name, Term)]
xs t :: Term
t@(App AppStatus Name
Complete Term
f Term
a) = (Term
t, Bool
False)
updateSolved' [(Name, Term)]
xs t :: Term
t@(App AppStatus Name
s Term
f Term
a)
= let (Term
f', Bool
uf) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
f
(Term
a', Bool
ua) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
a in
if Bool
uf Bool -> Bool -> Bool
|| Bool
ua then (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Term
f' Term
a', Bool
True)
else (Term
t, Bool
False)
updateSolved' [(Name, Term)]
xs t :: Term
t@(P NameType
_ n :: Name
n@(MN Int
_ Text
_) Term
_)
| Just Term
v <- Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
xs = (Term
v, Bool
True)
updateSolved' [(Name, Term)]
xs t :: Term
t@(P NameType
nt Name
n Term
ty)
= let (Term
ty', Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
ty in
if Bool
ut then (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n Term
ty', Bool
True) else (Term
t, Bool
False)
updateSolved' [(Name, Term)]
xs Term
t = (Term
t, Bool
False)
updateSolvedB' :: [(Name, Term)] -> Binder Term -> (Binder Term, Bool)
updateSolvedB' [(Name, Term)]
xs b :: Binder Term
b@(Let RigCount
c Term
t Term
v) = let (Term
t', Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t
(Term
v', Bool
uv) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
v in
if Bool
ut Bool -> Bool -> Bool
|| Bool
uv then (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c Term
t' Term
v', Bool
True)
else (Binder Term
b, Bool
False)
updateSolvedB' [(Name, Term)]
xs b :: Binder Term
b@(Guess Term
t Term
v) = let (Term
t', Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t
(Term
v', Bool
uv) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
v in
if Bool
ut Bool -> Bool -> Bool
|| Bool
uv then (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
t' Term
v', Bool
True)
else (Binder Term
b, Bool
False)
updateSolvedB' [(Name, Term)]
xs Binder Term
b = let (Term
ty', Bool
u) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) in
if Bool
u then (Binder Term
b { binderTy = ty' }, Bool
u) else (Binder Term
b, Bool
False)
updsubst :: Eq n => n ->
TT n ->
TT n ->
TT n
updsubst :: forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst n
n TT n
v TT n
tm = (TT n, Bool) -> TT n
forall a b. (a, b) -> a
fst ((TT n, Bool) -> TT n) -> (TT n, Bool) -> TT n
forall a b. (a -> b) -> a -> b
$ Int -> TT n -> (TT n, Bool)
subst' Int
0 TT n
tm
where
subst' :: Int -> TT n -> (TT n, Bool)
subst' Int
i (V Int
x) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x = (TT n
v, Bool
True)
subst' Int
i (P NameType
_ n
x TT n
_) | n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
x = (TT n
v, Bool
True)
subst' Int
i t :: TT n
t@(P NameType
nt n
x TT n
ty)
= let (TT n
ty', Bool
ut) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
ty in
if Bool
ut then (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
nt n
x TT n
ty', Bool
True) else (TT n
t, Bool
False)
subst' Int
i t :: TT n
t@(Bind n
x Binder (TT n)
b TT n
sc) | n
x n -> n -> Bool
forall a. Eq a => a -> a -> Bool
/= n
n
= let (Binder (TT n)
b', Bool
ub) = Int -> Binder (TT n) -> (Binder (TT n), Bool)
substB' Int
i Binder (TT n)
b
(TT n
sc', Bool
usc) = Int -> TT n -> (TT n, Bool)
subst' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TT n
sc in
if Bool
ub Bool -> Bool -> Bool
|| Bool
usc then (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
x Binder (TT n)
b' TT n
sc', Bool
True) else (TT n
t, Bool
False)
subst' Int
i t :: TT n
t@(App AppStatus n
Complete TT n
f TT n
a) = (TT n
t, Bool
False)
subst' Int
i t :: TT n
t@(App AppStatus n
s TT n
f TT n
a) = let (TT n
f', Bool
uf) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
f
(TT n
a', Bool
ua) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
a in
if Bool
uf Bool -> Bool -> Bool
|| Bool
ua then (AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
s TT n
f' TT n
a', Bool
True) else (TT n
t, Bool
False)
subst' Int
i t :: TT n
t@(Proj TT n
x Int
idx) = let (TT n
x', Bool
u) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
x in
if Bool
u then (TT n -> Int -> TT n
forall n. TT n -> Int -> TT n
Proj TT n
x' Int
idx, Bool
u) else (TT n
t, Bool
False)
subst' Int
i TT n
t = (TT n
t, Bool
False)
substB' :: Int -> Binder (TT n) -> (Binder (TT n), Bool)
substB' Int
i b :: Binder (TT n)
b@(Let RigCount
c TT n
t TT n
v) = let (TT n
t', Bool
ut) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
t
(TT n
v', Bool
uv) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
v in
if Bool
ut Bool -> Bool -> Bool
|| Bool
uv then (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c TT n
t' TT n
v', Bool
True)
else (Binder (TT n)
b, Bool
False)
substB' Int
i b :: Binder (TT n)
b@(Guess TT n
t TT n
v) = let (TT n
t', Bool
ut) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
t
(TT n
v', Bool
uv) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
v in
if Bool
ut Bool -> Bool -> Bool
|| Bool
uv then (TT n -> TT n -> Binder (TT n)
forall b. b -> b -> Binder b
Guess TT n
t' TT n
v', Bool
True)
else (Binder (TT n)
b, Bool
False)
substB' Int
i Binder (TT n)
b = let (TT n
ty', Bool
u) = Int -> TT n -> (TT n, Bool)
subst' Int
i (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
b) in
if Bool
u then (Binder (TT n)
b { binderTy = ty' }, Bool
u) else (Binder (TT n)
b, Bool
False)
updateEnv :: [(Name, Term)] -> Env -> Env
updateEnv :: [(Name, Term)] -> Env -> Env
updateEnv [] Env
e = Env
e
updateEnv [(Name, Term)]
ns [] = []
updateEnv [(Name, Term)]
ns ((Name
n, RigCount
r, Binder Term
b) : Env
env) = (Name
n, RigCount
r, (Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns) Binder Term
b) (Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
: [(Name, Term)] -> Env -> Env
updateEnv [(Name, Term)]
ns Env
env
updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [] TermPath
t = TermPath
t
updateSolvedPath [(Name, Term)]
ns TermPath
Top = TermPath
Top
updateSolvedPath [(Name, Term)]
ns t :: TermPath
t@(AppL AppStatus Name
Complete TermPath
_ Term
_) = TermPath
t
updateSolvedPath [(Name, Term)]
ns t :: TermPath
t@(AppR AppStatus Name
Complete Term
_ TermPath
_) = TermPath
t
updateSolvedPath [(Name, Term)]
ns (AppL AppStatus Name
s TermPath
p Term
r) = AppStatus Name -> TermPath -> Term -> TermPath
AppL AppStatus Name
s ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
p) ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
r)
updateSolvedPath [(Name, Term)]
ns (AppR AppStatus Name
s Term
l TermPath
p) = AppStatus Name -> Term -> TermPath -> TermPath
AppR AppStatus Name
s ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
l) ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
p)
updateSolvedPath [(Name, Term)]
ns (InBind Name
n BinderPath
b Term
sc)
= Name -> BinderPath -> Term -> TermPath
InBind Name
n (BinderPath -> BinderPath
updateSolvedPathB BinderPath
b) ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
sc)
where
updateSolvedPathB :: BinderPath -> BinderPath
updateSolvedPathB (Binder Binder TermPath
b) = Binder TermPath -> BinderPath
Binder ((TermPath -> TermPath) -> Binder TermPath -> Binder TermPath
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns) Binder TermPath
b)
updateSolvedPathB (LetT RigCount
c TermPath
p Term
v) = RigCount -> TermPath -> Term -> BinderPath
LetT RigCount
c ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
p) ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
v)
updateSolvedPathB (LetV RigCount
c Term
v TermPath
p) = RigCount -> Term -> TermPath -> BinderPath
LetV RigCount
c ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
v) ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
p)
updateSolvedPathB (GuessT TermPath
p Term
v) = TermPath -> Term -> BinderPath
GuessT ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
p) ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
v)
updateSolvedPathB (GuessV Term
v TermPath
p) = Term -> TermPath -> BinderPath
GuessV ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
v) ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
p)
updateSolvedPath [(Name, Term)]
ns (InScope Name
n (Hole Term
ty) TermPath
t)
| Just Term
v <- Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
ns = case [(Name, Term)]
ns of
[(Name, Term)
_] -> [(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name
n,Term
v)] TermPath
t
[(Name, Term)]
_ -> [(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns (TermPath -> TermPath) -> TermPath -> TermPath
forall a b. (a -> b) -> a -> b
$
[(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name
n,Term
v)] TermPath
t
updateSolvedPath [(Name, Term)]
ns (InScope Name
n Binder Term
b TermPath
sc)
= Name -> Binder Term -> TermPath -> TermPath
InScope Name
n ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns) Binder Term
b) ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ns TermPath
sc)
updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)]
xs pt :: ProofTerm
pt@(PT TermPath
path Env
env Term
sub [(Name, Term)]
ups)
= TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT TermPath
path
([(Name, Term)] -> Env -> Env
updateEnv [(Name, Term)]
xs (((Name, RigCount, Binder Term) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, RigCount
r, Binder Term
t) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
xs) Env
env))
([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
xs Term
sub)
([(Name, Term)]
ups [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
xs)
getRig :: Binder Term -> RigCount
getRig :: Binder Term -> RigCount
getRig (Pi RigCount
rig Maybe ImplicitInfo
_ Term
_ Term
_) = RigCount
rig
getRig (PVar RigCount
rig Term
_) = RigCount
rig
getRig (Lam RigCount
rig Term
_) = RigCount
rig
getRig (Let RigCount
rig Term
_ Term
_) = RigCount
rig
getRig Binder Term
_ = RigCount
RigW
goal :: Hole -> ProofTerm -> TC Goal
goal :: Hole -> ProofTerm -> TC Goal
goal Hole
h pt :: ProofTerm
pt@(PT TermPath
path Env
env Term
sub [(Name, Term)]
ups)
| Bool
otherwise = Env -> Term -> TC Goal
g [] (Term -> TermPath -> Term
rebuildTerm Term
sub ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ups TermPath
path))
where
g :: Env -> Term -> TC Goal
g :: Env -> Term -> TC Goal
g Env
env (Bind Name
n b :: Binder Term
b@(Guess Term
_ Term
_) Term
sc)
| Hole -> Name -> Bool
forall a. Eq a => Maybe a -> a -> Bool
same Hole
h Name
n = Goal -> TC Goal
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> TC Goal) -> Goal -> TC Goal
forall a b. (a -> b) -> a -> b
$ Env -> Binder Term -> Goal
GD Env
env Binder Term
b
| Bool
otherwise
= Env -> Binder Term -> TC Goal
gb Env
env Binder Term
b TC Goal -> TC Goal -> TC Goal
forall a. TC a -> TC a -> TC a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g ((Name
n, RigCount
RigW, Binder Term
b)(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
sc
g Env
env (Bind Name
n Binder Term
b Term
sc) | Binder Term -> Bool
forall b. Binder b -> Bool
hole Binder Term
b Bool -> Bool -> Bool
&& Hole -> Name -> Bool
forall a. Eq a => Maybe a -> a -> Bool
same Hole
h Name
n = Goal -> TC Goal
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> TC Goal) -> Goal -> TC Goal
forall a b. (a -> b) -> a -> b
$ Env -> Binder Term -> Goal
GD Env
env Binder Term
b
| Bool
otherwise
= Env -> Term -> TC Goal
g ((Name
n, Binder Term -> RigCount
getRig Binder Term
b, Binder Term
b)(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
sc TC Goal -> TC Goal -> TC Goal
forall a. TC a -> TC a -> TC a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Binder Term -> TC Goal
gb Env
env Binder Term
b
g Env
env (App AppStatus Name
Complete Term
f Term
a) = String -> TC Goal
forall a. String -> TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't find hole"
g Env
env (App AppStatus Name
_ Term
f Term
a) = Env -> Term -> TC Goal
g Env
env Term
a TC Goal -> TC Goal -> TC Goal
forall a. TC a -> TC a -> TC a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g Env
env Term
f
g Env
env Term
t = String -> TC Goal
forall a. String -> TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't find hole"
gb :: Env -> Binder Term -> TC Goal
gb Env
env (Let RigCount
c Term
t Term
v) = Env -> Term -> TC Goal
g Env
env Term
v TC Goal -> TC Goal -> TC Goal
forall a. TC a -> TC a -> TC a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g Env
env Term
t
gb Env
env (Guess Term
t Term
v) = Env -> Term -> TC Goal
g Env
env Term
v TC Goal -> TC Goal -> TC Goal
forall a. TC a -> TC a -> TC a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g Env
env Term
t
gb Env
env Binder Term
t = Env -> Term -> TC Goal
g Env
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
t)
atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
StateT a TC (ProofTerm, Bool)
atHole :: forall a.
Hole
-> RunTactic' a
-> Context
-> Env
-> ProofTerm
-> StateT a TC (ProofTerm, Bool)
atHole Hole
h RunTactic' a
f Context
c Env
e ProofTerm
pt
= do let PT TermPath
path Env
env Term
sub [(Name, Term)]
ups = Hole -> ProofTerm -> ProofTerm
refocus Hole
h ProofTerm
pt
(Term
tm, Bool
u) <- RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c Env
env Term
sub
(ProofTerm, Bool) -> StateT a TC (ProofTerm, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT TermPath
path Env
env Term
tm [(Name, Term)]
ups, Bool
u)
where
updated :: m a -> m (a, Bool)
updated m a
o = do a
o' <- m a
o
(a, Bool) -> m (a, Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
o', Bool
True)
ulift2 :: RunTactic' a
-> Context
-> Env
-> (Term -> Term -> a)
-> Term
-> Term
-> StateT a TC (a, Bool)
ulift2 RunTactic' a
f Context
c Env
env Term -> Term -> a
op Term
a Term
b
= do (Term
b', Bool
u) <- RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c Env
env Term
b
if Bool
u then (a, Bool) -> StateT a TC (a, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> a
op Term
a Term
b', Bool
True)
else do (Term
a', Bool
u) <- RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c Env
env Term
a
(a, Bool) -> StateT a TC (a, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> a
op Term
a' Term
b', Bool
u)
atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH :: forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c Env
env binder :: Term
binder@(Bind Name
n b :: Binder Term
b@(Guess Term
t Term
v) Term
sc)
| Hole -> Name -> Bool
forall a. Eq a => Maybe a -> a -> Bool
same Hole
h Name
n = StateT a TC Term -> StateT a TC (Term, Bool)
forall {m :: * -> *} {a}. Monad m => m a -> m (a, Bool)
updated (RunTactic' a
f Context
c Env
env Term
binder)
| Bool
otherwise
= do
(Binder Term
b', Bool
u) <- RunTactic' a
-> Context
-> Env
-> (Term -> Term -> Binder Term)
-> Term
-> Term
-> StateT a TC (Binder Term, Bool)
forall {a} {a}.
RunTactic' a
-> Context
-> Env
-> (Term -> Term -> a)
-> Term
-> Term
-> StateT a TC (a, Bool)
ulift2 RunTactic' a
f Context
c Env
env Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
t Term
v
if Bool
u then (Term, Bool) -> StateT a TC (Term, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
sc, Bool
True)
else do (Term
sc', Bool
u) <- RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c ((Name
n, RigCount
RigW, Binder Term
b) (Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Term
sc
(Term, Bool) -> StateT a TC (Term, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
sc', Bool
u)
atH RunTactic' a
f Context
c Env
env binder :: Term
binder@(Bind Name
n Binder Term
b Term
sc)
| Binder Term -> Bool
forall b. Binder b -> Bool
hole Binder Term
b Bool -> Bool -> Bool
&& Hole -> Name -> Bool
forall a. Eq a => Maybe a -> a -> Bool
same Hole
h Name
n = StateT a TC Term -> StateT a TC (Term, Bool)
forall {m :: * -> *} {a}. Monad m => m a -> m (a, Bool)
updated (RunTactic' a
f Context
c Env
env Term
binder)
| Bool
otherwise
= do (Term
sc', Bool
u) <- RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c ((Name
n, Binder Term -> RigCount
getRig Binder Term
b, Binder Term
b) (Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Term
sc
if Bool
u then (Term, Bool) -> StateT a TC (Term, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b Term
sc', Bool
True)
else do (Binder Term
b', Bool
u) <- RunTactic' a
-> Context -> Env -> Binder Term -> StateT a TC (Binder Term, Bool)
forall {a}.
RunTactic' a
-> Context -> Env -> Binder Term -> StateT a TC (Binder Term, Bool)
atHb RunTactic' a
f Context
c Env
env Binder Term
b
(Term, Bool) -> StateT a TC (Term, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
sc', Bool
u)
atH RunTactic' a
tac Context
c Env
env (App AppStatus Name
s Term
f Term
a) = RunTactic' a
-> Context
-> Env
-> (Term -> Term -> Term)
-> Term
-> Term
-> StateT a TC (Term, Bool)
forall {a} {a}.
RunTactic' a
-> Context
-> Env
-> (Term -> Term -> a)
-> Term
-> Term
-> StateT a TC (a, Bool)
ulift2 RunTactic' a
tac Context
c Env
env (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s) Term
f Term
a
atH RunTactic' a
tac Context
c Env
env Term
t = (Term, Bool) -> StateT a TC (Term, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t, Bool
False)
atHb :: RunTactic' a
-> Context -> Env -> Binder Term -> StateT a TC (Binder Term, Bool)
atHb RunTactic' a
f Context
c Env
env (Let RigCount
rc Term
t Term
v) = RunTactic' a
-> Context
-> Env
-> (Term -> Term -> Binder Term)
-> Term
-> Term
-> StateT a TC (Binder Term, Bool)
forall {a} {a}.
RunTactic' a
-> Context
-> Env
-> (Term -> Term -> a)
-> Term
-> Term
-> StateT a TC (a, Bool)
ulift2 RunTactic' a
f Context
c Env
env (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc) Term
t Term
v
atHb RunTactic' a
f Context
c Env
env (Guess Term
t Term
v) = RunTactic' a
-> Context
-> Env
-> (Term -> Term -> Binder Term)
-> Term
-> Term
-> StateT a TC (Binder Term, Bool)
forall {a} {a}.
RunTactic' a
-> Context
-> Env
-> (Term -> Term -> a)
-> Term
-> Term
-> StateT a TC (a, Bool)
ulift2 RunTactic' a
f Context
c Env
env Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
t Term
v
atHb RunTactic' a
f Context
c Env
env Binder Term
t = do (Term
ty', Bool
u) <- RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
forall a.
RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH RunTactic' a
f Context
c Env
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
t)
(Binder Term, Bool) -> StateT a TC (Binder Term, Bool)
forall a. a -> StateT a TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Binder Term
t { binderTy = ty' }, Bool
u)
bound_in :: ProofTerm -> [Name]
bound_in :: ProofTerm -> [Name]
bound_in (PT TermPath
path Env
_ Term
tm [(Name, Term)]
ups) = Term -> [Name]
bound_in_term (Term -> TermPath -> Term
rebuildTerm Term
tm ([(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [(Name, Term)]
ups TermPath
path))
bound_in_term :: Term -> [Name]
bound_in_term :: Term -> [Name]
bound_in_term (Bind Name
n Binder Term
b Term
sc) = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Binder Term -> [Name]
bi Binder Term
b [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
bound_in_term Term
sc
where
bi :: Binder Term -> [Name]
bi (Let RigCount
c Term
t Term
v) = Term -> [Name]
bound_in_term Term
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
bound_in_term Term
v
bi (Guess Term
t Term
v) = Term -> [Name]
bound_in_term Term
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
bound_in_term Term
v
bi Binder Term
b = Term -> [Name]
bound_in_term (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
bound_in_term (App AppStatus Name
_ Term
f Term
a) = Term -> [Name]
bound_in_term Term
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
bound_in_term Term
a
bound_in_term Term
_ = []