{-|
Module      : Idris.Core.ProofTerm
Description : Proof term. implementation and utilities.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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.State.Strict

-- | A zipper over terms, in order to efficiently update proof terms.
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
showList :: [TermPath] -> ShowS
$cshowList :: [TermPath] -> ShowS
show :: TermPath -> String
$cshow :: TermPath -> String
showsPrec :: Int -> TermPath -> ShowS
$cshowsPrec :: Int -> TermPath -> ShowS
Show

-- | A zipper over binders, because terms and binders are mutually defined.
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
showList :: [BinderPath] -> ShowS
$cshowList :: [BinderPath] -> ShowS
show :: BinderPath -> String
$cshow :: BinderPath -> String
showsPrec :: Int -> BinderPath -> ShowS
$cshowsPrec :: Int -> BinderPath -> ShowS
Show

-- | Replace the top of a term path with another term path. In other
-- words, "graft" one term path into another.
replaceTop :: TermPath -> TermPath -> TermPath
replaceTop :: TermPath -> TermPath -> TermPath
replaceTop p :: TermPath
p Top = TermPath
p
replaceTop p :: TermPath
p (AppL s :: AppStatus Name
s l :: TermPath
l t :: Term
t) = AppStatus Name -> TermPath -> Term -> TermPath
AppL AppStatus Name
s (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
l) Term
t
replaceTop p :: TermPath
p (AppR s :: AppStatus Name
s t :: Term
t r :: TermPath
r) = AppStatus Name -> Term -> TermPath -> TermPath
AppR AppStatus Name
s Term
t (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
r)
replaceTop p :: TermPath
p (InBind n :: Name
n bp :: BinderPath
bp sc :: 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 p :: TermPath
p (Binder b :: Binder TermPath
b) = Binder TermPath -> BinderPath
Binder ((TermPath -> TermPath) -> Binder TermPath -> Binder TermPath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TermPath -> TermPath -> TermPath
replaceTop TermPath
p) Binder TermPath
b)
    replaceTopB p :: TermPath
p (LetT c :: RigCount
c t :: TermPath
t v :: Term
v) = RigCount -> TermPath -> Term -> BinderPath
LetT RigCount
c (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
t) Term
v
    replaceTopB p :: TermPath
p (LetV c :: RigCount
c t :: Term
t v :: TermPath
v) = RigCount -> Term -> TermPath -> BinderPath
LetV RigCount
c Term
t (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
v)
    replaceTopB p :: TermPath
p (GuessT t :: TermPath
t v :: Term
v) = TermPath -> Term -> BinderPath
GuessT (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
t) Term
v
    replaceTopB p :: TermPath
p (GuessV t :: Term
t v :: TermPath
v) = Term -> TermPath -> BinderPath
GuessV Term
t (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
v)
replaceTop p :: TermPath
p (InScope n :: Name
n b :: Binder Term
b sc :: TermPath
sc) = Name -> Binder Term -> TermPath -> TermPath
InScope Name
n Binder Term
b (TermPath -> TermPath -> TermPath
replaceTop TermPath
p TermPath
sc)

-- | Build a term from a zipper, given something to put in the hole.
rebuildTerm :: Term -> TermPath -> Term
rebuildTerm :: Term -> TermPath -> Term
rebuildTerm tm :: Term
tm Top = Term
tm
rebuildTerm tm :: Term
tm (AppL s :: AppStatus Name
s p :: TermPath
p a :: 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 tm :: Term
tm (AppR s :: AppStatus Name
s f :: Term
f p :: 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 tm :: Term
tm (InScope n :: Name
n b :: Binder Term
b p :: 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 tm :: Term
tm (InBind n :: Name
n bp :: BinderPath
bp sc :: 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

-- | Build a binder from a zipper, given something to put in the hole.
rebuildBinder :: Term -> BinderPath -> Binder Term
rebuildBinder :: Term -> BinderPath -> Binder Term
rebuildBinder tm :: Term
tm (Binder p :: Binder TermPath
p) = (TermPath -> Term) -> Binder TermPath -> Binder Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> TermPath -> Term
rebuildTerm Term
tm) Binder TermPath
p
rebuildBinder tm :: Term
tm (LetT c :: RigCount
c p :: TermPath
p t :: 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 tm :: Term
tm (LetV c :: RigCount
c v :: Term
v p :: 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 tm :: Term
tm (GuessT p :: TermPath
p t :: Term
t) = Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p) Term
t
rebuildBinder tm :: Term
tm (GuessV v :: Term
v p :: TermPath
p) = Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
v (Term -> TermPath -> Term
rebuildTerm Term
tm TermPath
p)

-- | Find the binding of a hole in a term. If present, return the path
-- to the hole's binding, the environment extended by the binders that
-- are crossed, and the actual binding term.
findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
findHole n :: Name
n env :: Env
env t :: 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
env path :: TermPath
path tm :: Term
tm@(Bind x :: Name
x h :: Binder Term
h sc :: 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
env path :: TermPath
path (App Complete _ _) = Maybe (TermPath, Env, Term)
forall a. Maybe a
Nothing
  fh' env :: Env
env path :: TermPath
path (App s :: AppStatus Name
s f :: Term
f a :: Term
a)
      | Just (p :: TermPath
p, env' :: Env
env', tm :: 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 (p :: TermPath
p, env' :: Env
env', tm :: 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
env path :: TermPath
path (Bind x :: Name
x b :: Binder Term
b sc :: Term
sc)
      | Just (bp :: BinderPath
bp, env' :: Env
env', tm :: 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 (p :: TermPath
p, env' :: Env
env', tm :: 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' _ _ _ = Maybe (TermPath, Env, Term)
forall a. Maybe a
Nothing

  fhB :: Env -> TermPath -> Binder Term -> Maybe (BinderPath, Env, Term)
fhB env :: Env
env path :: TermPath
path (Let c :: RigCount
c t :: Term
t v :: Term
v)
      | Just (p :: TermPath
p, env' :: Env
env', tm :: 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 (p :: TermPath
p, env' :: Env
env', tm :: 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
env path :: TermPath
path (Guess t :: Term
t v :: Term
v)
      | Just (p :: TermPath
p, env' :: Env
env', tm :: 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 (p :: TermPath
p, env' :: Env
env', tm :: 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
env path :: TermPath
path b :: Binder Term
b
      | Just (p :: TermPath
p, env' :: Env
env', tm :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\_ -> TermPath
p) Binder Term
b), Env
env', Term
tm)
  fhB _ _ _ = Maybe (BinderPath, Env, Term)
forall a. Maybe a
Nothing

data ProofTerm = PT { -- wholeterm :: Term,
                      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
showList :: [ProofTerm] -> ShowS
$cshowList :: [ProofTerm] -> ShowS
show :: ProofTerm -> String
$cshow :: ProofTerm -> String
showsPrec :: Int -> ProofTerm -> ShowS
$cshowsPrec :: Int -> ProofTerm -> ShowS
Show

type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

-- | Refocus the proof term zipper on a particular hole, if it
-- exists. If not, return the original proof term.
refocus :: Hole -> ProofTerm -> ProofTerm
refocus :: Hole -> ProofTerm -> ProofTerm
refocus h :: Hole
h t :: ProofTerm
t = let res :: ProofTerm
res = Hole -> ProofTerm -> ProofTerm
refocus' Hole
h ProofTerm
t in ProofTerm
res
--                   trace ("OLD: " ++ show t ++ "\n" ++
--                          "REFOCUSSED " ++ show h ++ ": " ++ show res) res
refocus' :: Hole -> ProofTerm -> ProofTerm
refocus' (Just n :: Name
n) pt :: ProofTerm
pt@(PT path :: TermPath
path env :: Env
env tm :: Term
tm ups :: [(Name, Term)]
ups)
      -- First look for the hole in the proof term as-is
      | Just (p' :: TermPath
p', env' :: Env
env', tm' :: 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
      -- If it's not there, rebuild and look from the top
      | Just (p' :: TermPath
p', env' :: Env
env', tm' :: 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' _ pt :: ProofTerm
pt = ProofTerm
pt

data Goal = GD { Goal -> Env
premises :: Env,
                 Goal -> Binder Term
goalType :: Binder Term
               }

mkProofTerm :: Term -> ProofTerm
mkProofTerm :: Term -> ProofTerm
mkProofTerm tm :: Term
tm = TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT TermPath
Top [] Term
tm []

getProofTerm :: ProofTerm -> Term
getProofTerm :: ProofTerm -> Term
getProofTerm (PT path :: TermPath
path _ sub :: Term
sub ups :: [(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 :: Maybe a -> a -> Bool
same Nothing n :: a
n  = Bool
True
same (Just x :: a
x) n :: a
n = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n

-- | Is a particular binder a hole or a guess?
hole :: Binder b -> Bool
hole :: Binder b -> Bool
hole (Hole _)    = Bool
True
hole (Guess _ _) = Bool
True
hole _           = Bool
False

-- | Given a list of solved holes, fill out the solutions in a term
updateSolvedTerm :: [(Name, Term)] -> Term -> Term
updateSolvedTerm :: [(Name, Term)] -> Term -> Term
updateSolvedTerm xs :: [(Name, Term)]
xs x :: 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

-- | Given a list of solved holes, fill out the solutions in a
-- term. Return whether updates were performed, to facilitate sharing
-- when there are no updates.
updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [] x :: Term
x = (Term
x, Bool
False)
updateSolvedTerm' xs :: [(Name, Term)]
xs x :: Term
x = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
x where
    -- This version below saves allocations, because it doesn't need to reallocate
    -- the term if there are no updates to do.
    -- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
    -- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
    updateSolved' :: [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [] x :: Term
x = (Term
x, Bool
False)
    updateSolved' xs :: [(Name, Term)]
xs (Bind n :: Name
n (Hole ty :: Term
ty) t :: Term
t)
        | Just v :: 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 -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
n Term
v Term
t, Bool
True) -- some may be Vs! Can't assume
                                              -- explicit names
                   _ -> let (t' :: Term
t', _) = [(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' xs :: [(Name, Term)]
xs tm :: Term
tm@(Bind n :: Name
n b :: Binder Term
b t :: Term
t)
        = let (t' :: Term
t', ut :: Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t
              (b' :: Binder Term
b', ub :: 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' xs :: [(Name, Term)]
xs t :: Term
t@(App Complete f :: Term
f a :: Term
a) = (Term
t, Bool
False)
    updateSolved' xs :: [(Name, Term)]
xs t :: Term
t@(App s :: AppStatus Name
s f :: Term
f a :: Term
a)
        = let (f' :: Term
f', uf :: Bool
uf) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
f
              (a' :: Term
a', ua :: 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' xs :: [(Name, Term)]
xs t :: Term
t@(P _ n :: Name
n@(MN _ _) _)
        | Just v :: 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' xs :: [(Name, Term)]
xs t :: Term
t@(P nt :: NameType
nt n :: Name
n ty :: Term
ty)
        = let (ty' :: Term
ty', ut :: 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' xs :: [(Name, Term)]
xs t :: Term
t = (Term
t, Bool
False)

    updateSolvedB' :: [(Name, Term)] -> Binder Term -> (Binder Term, Bool)
updateSolvedB' xs :: [(Name, Term)]
xs b :: Binder Term
b@(Let c :: RigCount
c t :: Term
t v :: Term
v) = let (t' :: Term
t', ut :: Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t
                                          (v' :: Term
v', uv :: 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' xs :: [(Name, Term)]
xs b :: Binder Term
b@(Guess t :: Term
t v :: Term
v) = let (t' :: Term
t', ut :: Bool
ut) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolved' [(Name, Term)]
xs Term
t
                                          (v' :: Term
v', uv :: 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' xs :: [(Name, Term)]
xs b :: Binder Term
b = let (ty' :: Term
ty', u :: 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 :: Term
binderTy = Term
ty' }, Bool
u) else (Binder Term
b, Bool
False)

-- | As 'subst', in TT, but takes advantage of knowing not to substitute
-- under Complete applications.
updsubst :: Eq n => n {-^ The id to replace -} ->
            TT n {-^ The replacement term -} ->
            TT n {-^ The term to replace in -} ->
            TT n
-- subst n v tm = instantiate v (pToV n tm)
updsubst :: n -> TT n -> TT n -> TT n
updsubst n :: n
n v :: TT n
v tm :: 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' 0 TT n
tm
  where
    -- keep track of updates to save allocations - this is a big win on
    -- large terms in particular
    -- ('Maybe' would be neater here, but >>= is not the right combinator.
    -- Feel free to tidy up, as long as it still saves allocating when no
    -- substitution happens...)
    subst' :: Int -> TT n -> (TT n, Bool)
subst' i :: Int
i (V x :: Int
x) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x = (TT n
v, Bool
True)
    subst' i :: Int
i (P _ x :: n
x _) | n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
x = (TT n
v, Bool
True)
    subst' i :: Int
i t :: TT n
t@(P nt :: NameType
nt x :: n
x ty :: TT n
ty)
         = let (ty' :: TT n
ty', ut :: 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' i :: Int
i t :: TT n
t@(Bind x :: n
x b :: Binder (TT n)
b sc :: TT n
sc) | n
x n -> n -> Bool
forall a. Eq a => a -> a -> Bool
/= n
n
         = let (b' :: Binder (TT n)
b', ub :: Bool
ub) = Int -> Binder (TT n) -> (Binder (TT n), Bool)
substB' Int
i Binder (TT n)
b
               (sc' :: TT n
sc', usc :: Bool
usc) = Int -> TT n -> (TT n, Bool)
subst' (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+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' i :: Int
i t :: TT n
t@(App Complete f :: TT n
f a :: TT n
a) = (TT n
t, Bool
False)
    subst' i :: Int
i t :: TT n
t@(App s :: AppStatus n
s f :: TT n
f a :: TT n
a) = let (f' :: TT n
f', uf :: Bool
uf) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
f
                                 (a' :: TT n
a', ua :: 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' i :: Int
i t :: TT n
t@(Proj x :: TT n
x idx :: Int
idx) = let (x' :: TT n
x', u :: 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' i :: Int
i t :: TT n
t = (TT n
t, Bool
False)

    substB' :: Int -> Binder (TT n) -> (Binder (TT n), Bool)
substB' i :: Int
i b :: Binder (TT n)
b@(Let c :: RigCount
c t :: TT n
t v :: TT n
v) = let (t' :: TT n
t', ut :: Bool
ut) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
t
                                  (v' :: TT n
v', uv :: 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' i :: Int
i b :: Binder (TT n)
b@(Guess t :: TT n
t v :: TT n
v) = let (t' :: TT n
t', ut :: Bool
ut) = Int -> TT n -> (TT n, Bool)
subst' Int
i TT n
t
                                  (v' :: TT n
v', uv :: 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' i :: Int
i b :: Binder (TT n)
b = let (ty' :: TT n
ty', u :: 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 :: TT n
binderTy = TT n
ty' }, Bool
u) else (Binder (TT n)
b, Bool
False)


-- | Apply solutions to an environment.
updateEnv :: [(Name, Term)] -> Env -> Env
updateEnv :: [(Name, Term)] -> Env -> Env
updateEnv [] e :: Env
e = Env
e
updateEnv ns :: [(Name, Term)]
ns [] = []
updateEnv ns :: [(Name, Term)]
ns ((n :: Name
n, r :: RigCount
r, b :: Binder Term
b) : env :: Env
env) = (Name
n, RigCount
r, (Term -> Term) -> Binder Term -> Binder Term
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

-- | Fill out solved holes in a term zipper.
updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
updateSolvedPath [] t :: TermPath
t = TermPath
t
updateSolvedPath ns :: [(Name, Term)]
ns Top = TermPath
Top
updateSolvedPath ns :: [(Name, Term)]
ns t :: TermPath
t@(AppL Complete _ _) = TermPath
t
updateSolvedPath ns :: [(Name, Term)]
ns t :: TermPath
t@(AppR Complete _ _) = TermPath
t
updateSolvedPath ns :: [(Name, Term)]
ns (AppL s :: AppStatus Name
s p :: TermPath
p r :: 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 ns :: [(Name, Term)]
ns (AppR s :: AppStatus Name
s l :: Term
l p :: 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 ns :: [(Name, Term)]
ns (InBind n :: Name
n b :: BinderPath
b sc :: 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 b :: Binder TermPath
b) = Binder TermPath -> BinderPath
Binder ((TermPath -> TermPath) -> Binder TermPath -> Binder TermPath
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 c :: RigCount
c p :: TermPath
p v :: 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 c :: RigCount
c v :: Term
v p :: 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 p :: TermPath
p v :: 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 v :: Term
v p :: 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 ns :: [(Name, Term)]
ns (InScope n :: Name
n (Hole ty :: Term
ty) t :: TermPath
t)
    | Just v :: 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)] -> TermPath -> TermPath
updateSolvedPath [(Name
n,Term
v)] TermPath
t
                                  _ -> [(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 ns :: [(Name, Term)]
ns (InScope n :: Name
n b :: Binder Term
b sc :: TermPath
sc)
    = Name -> Binder Term -> TermPath -> TermPath
InScope Name
n ((Term -> Term) -> Binder Term -> Binder Term
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 xs :: [(Name, Term)]
xs pt :: ProofTerm
pt@(PT path :: TermPath
path env :: Env
env sub :: Term
sub ups :: [(Name, Term)]
ups)
     = TermPath -> Env -> Term -> [(Name, Term)] -> ProofTerm
PT TermPath
path -- (updateSolvedPath xs path)
          ([(Name, Term)] -> Env -> Env
updateEnv [(Name, Term)]
xs (((Name, RigCount, Binder Term) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: Name
n, r :: RigCount
r, t :: 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 rig :: RigCount
rig _ _ _) = RigCount
rig
getRig (PVar rig :: RigCount
rig _) = RigCount
rig
getRig (Lam rig :: RigCount
rig _) = RigCount
rig
getRig (Let rig :: RigCount
rig _ _) = RigCount
rig
getRig _ = RigCount
RigW

goal :: Hole -> ProofTerm -> TC Goal
goal :: Hole -> ProofTerm -> TC Goal
goal h :: Hole
h pt :: ProofTerm
pt@(PT path :: TermPath
path env :: Env
env sub :: Term
sub ups :: [(Name, Term)]
ups)
--      | OK ginf <- g env sub = return ginf
     | 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
env (Bind n :: Name
n b :: Binder Term
b@(Guess _ _) sc :: Term
sc)
                        | Hole -> Name -> Bool
forall a. Eq a => Maybe a -> a -> Bool
same Hole
h Name
n = Goal -> TC Goal
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 (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
env (Bind n :: Name
n b :: Binder Term
b sc :: 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 (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 (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
env (App Complete f :: Term
f a :: Term
a) = String -> TC Goal
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't find hole"
    g env :: Env
env (App _ f :: Term
f a :: Term
a) = Env -> Term -> TC Goal
g Env
env Term
a TC Goal -> TC Goal -> TC Goal
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g Env
env Term
f
    g env :: Env
env t :: Term
t           = String -> TC Goal
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't find hole"

    gb :: Env -> Binder Term -> TC Goal
gb env :: Env
env (Let c :: RigCount
c t :: Term
t v :: Term
v) = Env -> Term -> TC Goal
g Env
env Term
v TC Goal -> TC Goal -> TC Goal
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g Env
env Term
t
    gb env :: Env
env (Guess t :: Term
t v :: Term
v) = Env -> Term -> TC Goal
g Env
env Term
v TC Goal -> TC Goal -> TC Goal
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Env -> Term -> TC Goal
g Env
env Term
t
    gb env :: Env
env t :: 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 :: Hole
-> RunTactic' a
-> Context
-> Env
-> ProofTerm
-> StateT a TC (ProofTerm, Bool)
atHole h :: Hole
h f :: RunTactic' a
f c :: Context
c e :: Env
e pt :: ProofTerm
pt -- @(PT path env sub)
     = do let PT path :: TermPath
path env :: Env
env sub :: Term
sub ups :: [(Name, Term)]
ups = Hole -> ProofTerm -> ProofTerm
refocus Hole
h ProofTerm
pt
          (tm :: Term
tm, u :: 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 (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)
--           if u then return (PT path env tm ups, u)
--                else do let PT path env sub ups = refocus h pt
--                        (tm, u) <- atH f c env sub
--                        return (PT path env tm ups, u)
  where
    updated :: m a -> m (a, Bool)
updated o :: m a
o = do a
o' <- m a
o
                   (a, Bool) -> m (a, Bool)
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 f :: RunTactic' a
f c :: Context
c env :: Env
env op :: Term -> Term -> a
op a :: Term
a b :: Term
b
                  = do (b' :: Term
b', u :: 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 (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> a
op Term
a Term
b', Bool
True)
                            else do (a' :: Term
a', u :: 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 (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> a
op Term
a' Term
b', Bool
u)

    -- Search the things most likely to contain the binding first!

    atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
    atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
atH f :: RunTactic' a
f c :: Context
c env :: Env
env binder :: Term
binder@(Bind n :: Name
n b :: Binder Term
b@(Guess t :: Term
t v :: Term
v) sc :: 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 first
                 (b' :: Binder Term
b', u :: 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 (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 (sc' :: Term
sc', u :: 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 (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 f :: RunTactic' a
f c :: Context
c env :: Env
env binder :: Term
binder@(Bind n :: Name
n b :: Binder Term
b sc :: 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 -- scope first
            = do (sc' :: Term
sc', u :: 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 (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 (b' :: Binder Term
b', u :: 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 (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 tac :: RunTactic' a
tac c :: Context
c env :: Env
env (App s :: AppStatus Name
s f :: Term
f a :: 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 tac :: RunTactic' a
tac c :: Context
c env :: Env
env t :: Term
t            = (Term, Bool) -> StateT a TC (Term, Bool)
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 f :: RunTactic' a
f c :: Context
c env :: Env
env (Let rc :: RigCount
rc t :: Term
t v :: 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 f :: RunTactic' a
f c :: Context
c env :: Env
env (Guess t :: Term
t v :: 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 f :: RunTactic' a
f c :: Context
c env :: Env
env t :: Binder Term
t           = do (ty' :: Term
ty', u :: 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 (m :: * -> *) a. Monad m => a -> m a
return (Binder Term
t { binderTy :: Term
binderTy = Term
ty' }, Bool
u)

bound_in :: ProofTerm -> [Name]
bound_in :: ProofTerm -> [Name]
bound_in (PT path :: TermPath
path _ tm :: Term
tm ups :: [(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 n :: Name
n b :: Binder Term
b sc :: 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 c :: RigCount
c t :: Term
t v :: 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 t :: Term
t v :: 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 b :: Binder Term
b = Term -> [Name]
bound_in_term (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
bound_in_term (App _ f :: Term
f a :: 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 _ = []