{-|
Module      : Idris.Core.ProofState
Description : Proof state implementation.

License     : BSD3
Maintainer  : The Idris Community.

Implements a proof state, some primitive tactics for manipulating
proofs, and some high level commands for introducing new theorems,
evaluation/checking inside the proof system, etc.
-}

{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
             PatternGuards #-}
module Idris.Core.ProofState(
    ProofState(..), newProof, envAtFocus, goalAtFocus
  , Tactic(..), Goal(..), processTactic, nowElaboratingPS
  , doneElaboratingAppPS, doneElaboratingArgPS, dropGiven
  , keepGiven, getProvenance
  ) where

import Idris.Core.Evaluate
import Idris.Core.ProofTerm
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Unify
import Idris.Core.WHNF

import Util.Pretty hiding (fill)

import Control.Monad.State.Strict
import Data.List

#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<>))
#endif

data ProofState = PS { ProofState -> Name
thname            :: Name,
                       ProofState -> [Name]
holes             :: [Name], -- ^ holes still to be solved
                       ProofState -> [Name]
usedns            :: [Name], -- ^ used names, don't use again
                       ProofState -> Int
nextname          :: Int,    -- ^ name supply, for locally unique names
                       ProofState -> Int
global_nextname   :: Int, -- ^ a mirror of the global name supply,
                                                 --   for generating things like type tags
                                                 --   in reflection
                       ProofState -> ProofTerm
pterm             :: ProofTerm, -- ^ current proof term
                       ProofState -> Term
ptype             :: Type,   -- ^ original goal
                       ProofState -> [Name]
dontunify         :: [Name], -- ^ explicitly given by programmer, leave it
                       ProofState -> (Name, [(Name, Term)])
unified           :: (Name, [(Name, Term)]),
                       ProofState -> [(Name, Term)]
notunified        :: [(Name, Term)],
                       ProofState -> [(Name, [Name])]
dotted            :: [(Name, [Name])], -- ^ dot pattern holes + environment
                                                              -- either hole or something in env must turn up in the 'notunified' list during elaboration
                       ProofState -> Maybe (Name, Term)
solved            :: Maybe (Name, Term),
                       ProofState -> Fails
problems          :: Fails,
                       ProofState -> [Name]
injective         :: [Name],
                       ProofState -> [Name]
deferred          :: [Name], -- ^ names we'll need to define
                       ProofState -> [Name]
implementations   :: [Name], -- ^ implementation arguments (for interfaces)
                       ProofState -> [(Name, ([FailContext], [Name]))]
autos             :: [(Name, ([FailContext], [Name]))], -- ^ unsolved 'auto' implicits with their holes
                       ProofState -> [Name]
psnames           :: [Name], -- ^ Local names okay to use in proof search
                       ProofState -> Maybe ProofState
previous          :: Maybe ProofState, -- ^ for undo
                       ProofState -> Context
context           :: Context,
                       ProofState -> Ctxt TypeInfo
datatypes         :: Ctxt TypeInfo,
                       ProofState -> String
plog              :: String,
                       ProofState -> Bool
unifylog          :: Bool,
                       ProofState -> Bool
done              :: Bool,
                       ProofState -> [Name]
recents           :: [Name],
                       ProofState -> [FailContext]
while_elaborating :: [FailContext],
                       ProofState -> String
constraint_ns     :: String
                     }

data Tactic = Attack
            | Claim Name Raw
            | ClaimFn Name Name Raw
            | Reorder Name
            | Exact Raw
            | Fill Raw
            | MatchFill Raw
            | PrepFill Name [Name]
            | CompleteFill
            | Regret
            | Solve
            | StartUnify Name
            | EndUnify
            | UnifyAll
            | Compute
            | ComputeLet Name
            | Simplify
            | WHNF_Compute
            | WHNF_ComputeArgs
            | EvalIn Raw
            | CheckIn Raw
            | Intro (Maybe Name)
            | IntroTy Raw (Maybe Name)
            | Forall Name RigCount (Maybe ImplicitInfo) Raw
            | LetBind Name RigCount Raw Raw
            | ExpandLet Name Term
            | Rewrite Raw
            | Equiv Raw
            | PatVar Name
            | PatBind Name RigCount
            | Focus Name
            | Defer [Name] [Name] Name
            | DeferType Name Raw [Name]
            | Implementation Name
            | AutoArg Name
            | SetInjective Name
            | MoveLast Name
            | MatchProblems Bool
            | UnifyProblems
            | UnifyGoal Raw
            | UnifyTerms Raw Raw
            | ProofState
            | Undo
            | QED
    deriving Int -> Tactic -> ShowS
[Tactic] -> ShowS
Tactic -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tactic] -> ShowS
$cshowList :: [Tactic] -> ShowS
show :: Tactic -> String
$cshow :: Tactic -> String
showsPrec :: Int -> Tactic -> ShowS
$cshowsPrec :: Int -> Tactic -> ShowS
Show

-- Some utilites on proof and tactic states

instance Show ProofState where
    show :: ProofState -> String
show ProofState
ps | [] <- ProofState -> [Name]
holes ProofState
ps
          = forall a. Show a => a -> String
show (ProofState -> Name
thname ProofState
ps) forall a. [a] -> [a] -> [a]
++ String
": no more goals"
    show ProofState
ps | (Name
h : [Name]
hs) <- ProofState -> [Name]
holes ProofState
ps
          = let tm :: ProofTerm
tm = ProofState -> ProofTerm
pterm ProofState
ps
                nm :: Name
nm = ProofState -> Name
thname ProofState
ps
                OK Goal
g = Maybe Name -> ProofTerm -> TC Goal
goal (forall a. a -> Maybe a
Just Name
h) ProofTerm
tm
                wkenv :: Env
wkenv = Goal -> Env
premises Goal
g in
                String
"Other goals: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
hs forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
                forall {n} {a} {b}.
(Eq n, Show a, Show n) =>
EnvTT n -> [(a, b, Binder (TT n))] -> String
showPs Env
wkenv (forall a. [a] -> [a]
reverse Env
wkenv) forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
                String
"-------------------------------- (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
nm forall a. [a] -> [a] -> [a]
++
                String
") -------\n  " forall a. [a] -> [a] -> [a]
++
                forall a. Show a => a -> String
show Name
h forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall {n}. (Eq n, Show n) => EnvTT n -> Binder (TT n) -> String
showG Env
wkenv (Goal -> Binder Term
goalType Goal
g) forall a. [a] -> [a] -> [a]
++ String
"\n"
         where showPs :: EnvTT n -> [(a, b, Binder (TT n))] -> String
showPs EnvTT n
env [] = String
""
               showPs EnvTT n
env ((a
n, b
_, Let RigCount
_ TT n
t TT n
v):[(a, b, Binder (TT n))]
bs)
                   = String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++
                     forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
env ({- normalise ctxt env -} TT n
t) forall a. [a] -> [a] -> [a]
++ String
"   =   " forall a. [a] -> [a] -> [a]
++
                     forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
env ({- normalise ctxt env -} TT n
v) forall a. [a] -> [a] -> [a]
++
                     String
"\n" forall a. [a] -> [a] -> [a]
++ EnvTT n -> [(a, b, Binder (TT n))] -> String
showPs EnvTT n
env [(a, b, Binder (TT n))]
bs
               showPs EnvTT n
env ((a
n, b
_, Binder (TT n)
b):[(a, b, Binder (TT n))]
bs)
                   = String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++
                     forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
env ({- normalise ctxt env -} (forall b. Binder b -> b
binderTy Binder (TT n)
b)) forall a. [a] -> [a] -> [a]
++
                     String
"\n" forall a. [a] -> [a] -> [a]
++ EnvTT n -> [(a, b, Binder (TT n))] -> String
showPs EnvTT n
env [(a, b, Binder (TT n))]
bs
               showG :: EnvTT n -> Binder (TT n) -> String
showG EnvTT n
ps (Guess TT n
t TT n
v) = forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
ps ({- normalise ctxt ps -} TT n
t) forall a. [a] -> [a] -> [a]
++
                                         String
" =?= " forall a. [a] -> [a] -> [a]
++ forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
ps TT n
v
               showG EnvTT n
ps Binder (TT n)
b = forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
ps (forall b. Binder b -> b
binderTy Binder (TT n)
b)

instance Pretty ProofState OutputAnnotation where
  pretty :: ProofState -> Doc OutputAnnotation
pretty ProofState
ps | [] <- ProofState -> [Name]
holes ProofState
ps =
    forall a ty. Pretty a ty => a -> Doc ty
pretty (ProofState -> Name
thname ProofState
ps) forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
" no more goals."
  pretty ProofState
ps | (Name
h : [Name]
hs) <- ProofState -> [Name]
holes ProofState
ps =
    let tm :: ProofTerm
tm = ProofState -> ProofTerm
pterm ProofState
ps
        OK Goal
g = Maybe Name -> ProofTerm -> TC Goal
goal (forall a. a -> Maybe a
Just Name
h) ProofTerm
tm
        nm :: Name
nm = ProofState -> Name
thname ProofState
ps in
    let wkEnv :: Env
wkEnv = Goal -> Env
premises Goal
g in
      forall a. String -> Doc a
text String
"Other goals" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> forall a ty. Pretty a ty => a -> Doc ty
pretty [Name]
hs forall a. Doc a -> Doc a -> Doc a
<+>
      forall {a} {b}.
Pretty a OutputAnnotation =>
Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
wkEnv (forall a. [a] -> [a]
reverse Env
wkEnv) forall a. Doc a -> Doc a -> Doc a
<+>
      forall a. String -> Doc a
text String
"---------- " forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"Focussing on" forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> forall a ty. Pretty a ty => a -> Doc ty
pretty Name
nm forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
" ----------" forall a. Doc a -> Doc a -> Doc a
<+>
      forall a ty. Pretty a ty => a -> Doc ty
pretty Name
h forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> Env -> Binder Term -> Doc OutputAnnotation
prettyGoal Env
wkEnv (Goal -> Binder Term
goalType Goal
g)
    where
      prettyGoal :: Env -> Binder Term -> Doc OutputAnnotation
prettyGoal Env
ps (Guess Term
t Term
v) =
        Env -> Term -> Doc OutputAnnotation
prettyEnv Env
ps Term
t forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"=?=" forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
ps Term
v
      prettyGoal Env
ps Binder Term
b = Env -> Term -> Doc OutputAnnotation
prettyEnv Env
ps forall a b. (a -> b) -> a -> b
$ forall b. Binder b -> b
binderTy Binder Term
b

      prettyPs :: Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [] = forall a. Doc a
empty
      prettyPs Env
env ((a
n, b
_, Let RigCount
_ Term
t Term
v):[(a, b, Binder Term)]
bs) =
        forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (forall a ty. Pretty a ty => a -> Doc ty
pretty a
n forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+>
        Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env Term
t forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"=" forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env Term
v forall a. Doc a -> Doc a -> Doc a
<+>
        forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [(a, b, Binder Term)]
bs))
      prettyPs Env
env ((a
n, b
_, Binder Term
b):[(a, b, Binder Term)]
bs) =
        forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (forall a ty. Pretty a ty => a -> Doc ty
pretty a
n forall a. Doc a -> Doc a -> Doc a
<+> forall a. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env (forall b. Binder b -> b
binderTy Binder Term
b) forall a. Doc a -> Doc a -> Doc a
<+>
        forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [(a, b, Binder Term)]
bs))

holeName :: Int -> Name
holeName Int
i = Int -> String -> Name
sMN Int
i String
"hole"

qshow :: Fails -> String
qshow :: Fails -> String
qshow Fails
fs = forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map (\ (Term
x, Term
y, Bool
hs, Env
env, Err
_, [FailContext]
_, FailAt
t) -> (FailAt
t, forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env, Term
x, Term
y, Bool
hs)) Fails
fs)

match_unify' :: Context -> Env ->
                (TT Name, Maybe Provenance) ->
                (TT Name, Maybe Provenance) ->
                StateT TState TC [(Name, TT Name)]
match_unify' :: Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) =
   do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
      let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
ps
      let inj :: [Name]
inj = ProofState -> [Name]
injective ProofState
ps
      forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                (String
"Matching " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term
topx, Term
topy) forall a. [a] -> [a] -> [a]
++
                 String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Env
env forall a. [a] -> [a] -> [a]
++
                 String
"\nHoles: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [Name]
holes ProofState
ps)
                  forall a. [a] -> [a] -> [a]
++ String
"\n"
                  forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps)) forall a. [a] -> [a] -> [a]
++ String
"\n\n"
                 ) forall a b. (a -> b) -> a -> b
$
       case Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Term)]
match_unify Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) [Name]
inj (ProofState -> [Name]
holes ProofState
ps) [FailContext]
while of
            OK [(Name, Term)]
u -> forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                        (String
"Matched " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Term)]
u) forall a b. (a -> b) -> a -> b
$
                     do let (Name
h, [(Name, Term)]
ns) = ProofState -> (Name, [(Name, Term)])
unified ProofState
ps
                        forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { unified :: (Name, [(Name, Term)])
unified = (Name
h, [(Name, Term)]
u forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
ns) })
                        forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Term)]
u
            Error Err
e -> forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                         (String
"No match " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
e) forall a b. (a -> b) -> a -> b
$
                        do forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { problems :: Fails
problems = (Term
topx, Term
topy, Bool
True,
                                                 Env
env, Err
e, [FailContext]
while, FailAt
Match) forall a. a -> [a] -> [a]
:
                                                 ProofState -> Fails
problems ProofState
ps })
                           forall (m :: * -> *) a. Monad m => a -> m a
return []
--       traceWhen (unifylog ps)
--             ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++
--              "\nSolved: " ++ show u
--              ++ "\nCurrent problems:\n" ++ qshow (problems ps)
-- --              ++ show (pterm ps)
--              ++ "\n----------") $

mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
mergeSolutions :: Env -> [(Name, Term)] -> StateT ProofState TC [(Name, Term)]
mergeSolutions Env
env [(Name, Term)]
ns = forall {m :: * -> *} {a}.
(Eq a, MonadState ProofState m) =>
[(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge [] [(Name, Term)]
ns
  where
    merge :: [(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge [(a, Term)]
acc [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [(a, Term)]
acc)
    merge [(a, Term)]
acc ((a
n, Term
t) : [(a, Term)]
ns)
          | Just Term
t' <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Term)]
ns
              = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
                   let probs :: Fails
probs = ProofState -> Fails
problems ProofState
ps
                   forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { problems :: Fails
problems = Fails
probs forall a. [a] -> [a] -> [a]
++ [(Term
t,Term
t',Bool
True,Env
env,
                                                    forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
True (Term
t, forall a. Maybe a
Nothing) (Term
t', forall a. Maybe a
Nothing) (forall t. String -> Err' t
Msg String
"") (forall {a} {b1} {b2}. [(a, b1, Binder b2)] -> [(a, b2)]
errEnv Env
env) Int
0,
                                                     [], FailAt
Unify)] })
                   [(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge [(a, Term)]
acc [(a, Term)]
ns
          | Bool
otherwise = [(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge ((a
n, Term
t)forall a. a -> [a] -> [a]
: [(a, Term)]
acc) [(a, Term)]
ns

dropSwaps :: [(Name, TT Name)] -> [(Name, TT Name)]
dropSwaps :: [(Name, Term)] -> [(Name, Term)]
dropSwaps [] = []
dropSwaps (p :: (Name, Term)
p@(Name
x, P NameType
_ Name
y Term
_) : [(Name, Term)]
xs) | forall {t} {t}. (Eq t, Eq t) => t -> t -> [(t, TT t)] -> Bool
solvedIn Name
y Name
x [(Name, Term)]
xs = [(Name, Term)] -> [(Name, Term)]
dropSwaps [(Name, Term)]
xs
  where solvedIn :: t -> t -> [(t, TT t)] -> Bool
solvedIn t
_ t
_ [] = Bool
False
        solvedIn t
y t
x ((t
y', P NameType
_ t
x' TT t
_) : [(t, TT t)]
xs) | t
y forall a. Eq a => a -> a -> Bool
== t
y' Bool -> Bool -> Bool
&& t
x forall a. Eq a => a -> a -> Bool
== t
x' = Bool
True
        solvedIn t
y t
x ((t, TT t)
_ : [(t, TT t)]
xs) = t -> t -> [(t, TT t)] -> Bool
solvedIn t
y t
x [(t, TT t)]
xs
dropSwaps ((Name, Term)
p : [(Name, Term)]
xs) = (Name, Term)
p forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(Name, Term)]
dropSwaps [(Name, Term)]
xs

unify' :: Context -> Env ->
          (TT Name, Maybe Provenance) ->
          (TT Name, Maybe Provenance) ->
          StateT TState TC [(Name, TT Name)]
unify' :: Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) =
   do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
      let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
ps
      let dont :: [Name]
dont = ProofState -> [Name]
dontunify ProofState
ps
      let inj :: [Name]
inj = ProofState -> [Name]
injective ProofState
ps
      ([(Name, Term)]
u, Fails
fails) <- forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                        (String
"Trying " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term
topx, Term
topy) forall a. [a] -> [a] -> [a]
++
                         String
"\nNormalised " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
topx,
                                                  Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
topy) forall a. [a] -> [a] -> [a]
++
                         String
" in\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Env
env forall a. [a] -> [a] -> [a]
++
                         String
"\nHoles: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [Name]
holes ProofState
ps)
                         forall a. [a] -> [a] -> [a]
++ String
"\nInjective: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [Name]
injective ProofState
ps)
                         forall a. [a] -> [a] -> [a]
++ String
"\n") forall a b. (a -> b) -> a -> b
$
                     forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, Term)], Fails)
unify Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) [Name]
inj (ProofState -> [Name]
holes ProofState
ps)
                                  (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (ProofState -> [(Name, Term)]
notunified ProofState
ps)) [FailContext]
while
      let notu :: [(Name, Term)]
notu = forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n, Term
t) -> case Term
t of
--                                         P _ _ _ -> False
                                        Term
_ -> Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
dont) [(Name, Term)]
u
      forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
            (String
"Unified " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term
topx, Term
topy) forall a. [a] -> [a] -> [a]
++ String
" without " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
dont forall a. [a] -> [a] -> [a]
++
             String
"\nSolved: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Term)]
u forall a. [a] -> [a] -> [a]
++ String
"\nNew problems: " forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow Fails
fails
             forall a. [a] -> [a] -> [a]
++ String
"\nNot unified:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [(Name, Term)]
notunified ProofState
ps)
             forall a. [a] -> [a] -> [a]
++ String
"\nCurrent problems:\n" forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow (ProofState -> Fails
problems ProofState
ps)
--              ++ show (pterm ps)
             forall a. [a] -> [a] -> [a]
++ String
"\n----------") forall a b. (a -> b) -> a -> b
$
        do let (Name
h, [(Name, Term)]
ns) = ProofState -> (Name, [(Name, Term)])
unified ProofState
ps
           -- solve in results (maybe unify should do this itself...)
           let u' :: [(Name, Term)]
u' = forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Term
sol) -> (Name
n, [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
u Term
sol)) [(Name, Term)]
u
           -- if a metavar has multiple solutions, make a new unification
           -- problem for each.
           [(Name, Term)]
uns <- Env -> [(Name, Term)] -> StateT ProofState TC [(Name, Term)]
mergeSolutions Env
env ([(Name, Term)]
u' forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
ns)
           ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
           let ([(Name, Term)]
ns_p, Fails
probs') = ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems ProofState
ps [(Name, Term)]
uns (Fails
fails forall a. [a] -> [a] -> [a]
++ ProofState -> Fails
problems ProofState
ps)
           let ns' :: [(Name, Term)]
ns' = [(Name, Term)] -> [(Name, Term)]
dropSwaps [(Name, Term)]
ns_p
           let ([(Name, Term)]
notu', Fails
probs_notu) = Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified Env
env (ProofState -> [Name]
holes ProofState
ps) ([(Name, Term)]
notu forall a. [a] -> [a] -> [a]
++ ProofState -> [(Name, Term)]
notunified ProofState
ps)
           forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
            (String
"Now solved: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Term)]
ns' forall a. [a] -> [a] -> [a]
++
             String
"\nNow problems: " forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow (Fails
probs' forall a. [a] -> [a] -> [a]
++ Fails
probs_notu) forall a. [a] -> [a] -> [a]
++
             String
"\nNow injective: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {a}. Eq a => [(a, TT a)] -> [a] -> [a]
updateInj [(Name, Term)]
u (ProofState -> [Name]
injective ProofState
ps))) forall a b. (a -> b) -> a -> b
$
             forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { problems :: Fails
problems = Fails
probs' forall a. [a] -> [a] -> [a]
++ Fails
probs_notu,
                       unified :: (Name, [(Name, Term)])
unified = (Name
h, [(Name, Term)]
ns'),
                       injective :: [Name]
injective = forall {a}. Eq a => [(a, TT a)] -> [a] -> [a]
updateInj [(Name, Term)]
u (ProofState -> [Name]
injective ProofState
ps),
                       notunified :: [(Name, Term)]
notunified = [(Name, Term)]
notu' })
           forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Term)]
u
  where updateInj :: [(a, TT a)] -> [a] -> [a]
updateInj ((a
n, TT a
a) : [(a, TT a)]
us) [a]
inj
              | (P NameType
_ a
n' TT a
_, [TT a]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT a
a,
                a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
inj = [(a, TT a)] -> [a] -> [a]
updateInj [(a, TT a)]
us (a
n'forall a. a -> [a] -> [a]
:[a]
inj)
              | (P NameType
_ a
n' TT a
_, [TT a]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT a
a,
                a
n' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
inj = [(a, TT a)] -> [a] -> [a]
updateInj [(a, TT a)]
us (a
nforall a. a -> [a] -> [a]
:[a]
inj)
        updateInj ((a, TT a)
_ : [(a, TT a)]
us) [a]
inj = [(a, TT a)] -> [a] -> [a]
updateInj [(a, TT a)]
us [a]
inj
        updateInj [] [a]
inj = [a]
inj

nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
nowElaboratingPS FC
fc Name
f Name
arg ProofState
ps = ProofState
ps { while_elaborating :: [FailContext]
while_elaborating = FC -> Name -> Name -> FailContext
FailContext FC
fc Name
f Name
arg forall a. a -> [a] -> [a]
: ProofState -> [FailContext]
while_elaborating ProofState
ps }

dropUntil :: (a -> Bool) -> [a] -> [a]
dropUntil :: forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
p [] = []
dropUntil a -> Bool
p (a
x:[a]
xs) | a -> Bool
p a
x       = [a]
xs
                   | Bool
otherwise = forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
p [a]
xs

doneElaboratingAppPS :: Name -> ProofState -> ProofState
doneElaboratingAppPS :: Name -> ProofState -> ProofState
doneElaboratingAppPS Name
f ProofState
ps = let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
ps
                                while' :: [FailContext]
while' = forall a. (a -> Bool) -> [a] -> [a]
dropUntil (\ (FailContext FC
_ Name
f' Name
_) -> Name
f forall a. Eq a => a -> a -> Bool
== Name
f') [FailContext]
while
                            in ProofState
ps { while_elaborating :: [FailContext]
while_elaborating = [FailContext]
while' }

doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS Name
f Name
x ProofState
ps = let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
ps
                                  while' :: [FailContext]
while' = forall a. (a -> Bool) -> [a] -> [a]
dropUntil (\ (FailContext FC
_ Name
f' Name
x') -> Name
f forall a. Eq a => a -> a -> Bool
== Name
f' Bool -> Bool -> Bool
&& Name
x forall a. Eq a => a -> a -> Bool
== Name
x') [FailContext]
while
                              in ProofState
ps { while_elaborating :: [FailContext]
while_elaborating = [FailContext]
while' }

getName :: Monad m => String -> StateT TState m Name
getName :: forall (m :: * -> *). Monad m => String -> StateT ProofState m Name
getName String
tag = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
                 let n :: Int
n = ProofState -> Int
nextname ProofState
ps
                 forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { nextname :: Int
nextname = Int
nforall a. Num a => a -> a -> a
+Int
1 })
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
n String
tag

action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
action :: forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action ProofState -> ProofState
a = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
              forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState -> ProofState
a ProofState
ps)

query :: Monad m => (ProofState -> r) -> StateT TState m r
query :: forall (m :: * -> *) r.
Monad m =>
(ProofState -> r) -> StateT ProofState m r
query ProofState -> r
q = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ProofState -> r
q ProofState
ps

addLog :: Monad m => String -> StateT TState m ()
addLog :: forall (m :: * -> *). Monad m => String -> StateT ProofState m ()
addLog String
str = forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { plog :: String
plog = ProofState -> String
plog ProofState
ps forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
"\n" })

newProof :: Name -- ^ the name of what's to be elaborated
         -> String -- ^ current source file
         -> Context -- ^ the current global context
         -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState
         -> Int -- ^ the value of the idris_name field of IState
         -> Type -- ^ the goal type
         -> ProofState
newProof :: Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Term -> ProofState
newProof Name
n String
tcns Context
ctxt Ctxt TypeInfo
datatypes Int
globalNames Term
ty =
  let h :: Name
h = Int -> Name
holeName Int
0
      ty' :: Term
ty' = forall n. TT n -> TT n
vToP Term
ty
  in Name
-> [Name]
-> [Name]
-> Int
-> Int
-> ProofTerm
-> Term
-> [Name]
-> (Name, [(Name, Term)])
-> [(Name, Term)]
-> [(Name, [Name])]
-> Maybe (Name, Term)
-> Fails
-> [Name]
-> [Name]
-> [Name]
-> [(Name, ([FailContext], [Name]))]
-> [Name]
-> Maybe ProofState
-> Context
-> Ctxt TypeInfo
-> String
-> Bool
-> Bool
-> [Name]
-> [FailContext]
-> String
-> ProofState
PS Name
n [Name
h] [] Int
1 Int
globalNames (Term -> ProofTerm
mkProofTerm (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (forall b. b -> Binder b
Hole Term
ty')
        (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Term
ty'))) Term
ty [] (Name
h, []) [] []
        forall a. Maybe a
Nothing [] []
        [] [] [] []
        forall a. Maybe a
Nothing Context
ctxt Ctxt TypeInfo
datatypes String
"" Bool
False Bool
False [] [] String
tcns

type TState = ProofState -- [TacticAction])
type RunTactic = RunTactic' TState

envAtFocus :: ProofState -> TC Env
envAtFocus :: ProofState -> TC Env
envAtFocus ProofState
ps
    | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ProofState -> [Name]
holes ProofState
ps) = do Goal
g <- Maybe Name -> ProofTerm -> TC Goal
goal (forall a. a -> Maybe a
Just (forall a. [a] -> a
head (ProofState -> [Name]
holes ProofState
ps))) (ProofState -> ProofTerm
pterm ProofState
ps)
                                 forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Env
premises Goal
g)
    | Bool
otherwise = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"No holes in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps))

goalAtFocus :: ProofState -> TC (Binder Type)
goalAtFocus :: ProofState -> TC (Binder Term)
goalAtFocus ProofState
ps
    | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ProofState -> [Name]
holes ProofState
ps) = do Goal
g <- Maybe Name -> ProofTerm -> TC Goal
goal (forall a. a -> Maybe a
Just (forall a. [a] -> a
head (ProofState -> [Name]
holes ProofState
ps))) (ProofState -> ProofTerm
pterm ProofState
ps)
                                 forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Binder Term
goalType Goal
g)
    | Bool
otherwise = forall a. Err -> TC a
Error forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"No goal in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [Name]
holes ProofState
ps) forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps))

tactic :: Hole -> RunTactic -> StateT TState TC ()
tactic :: Maybe Name -> RunTactic -> StateT ProofState TC ()
tactic Maybe Name
h RunTactic
f = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
                (ProofTerm
tm', Bool
_) <- forall a.
Maybe Name
-> RunTactic' a
-> Context
-> Env
-> ProofTerm
-> StateT a TC (ProofTerm, Bool)
atHole Maybe Name
h RunTactic
f (ProofState -> Context
context ProofState
ps) [] (ProofState -> ProofTerm
pterm ProofState
ps)
                ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get -- might have changed while processing
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { pterm :: ProofTerm
pterm = ProofTerm
tm' })

computeLet :: Context -> Name -> Term -> Term
computeLet :: Context -> Name -> Term -> Term
computeLet Context
ctxt Name
n Term
tm = Env -> Term -> Term
cl [] Term
tm where
   cl :: Env -> Term -> Term
cl Env
env (Bind Name
n' (Let RigCount
r Term
t Term
v) Term
sc)
       | Name
n' forall a. Eq a => a -> a -> Bool
== Name
n = let v' :: Term
v' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
v in
                       forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' (forall b. RigCount -> b -> b -> Binder b
Let RigCount
r Term
t Term
v') Term
sc
   cl Env
env (Bind Name
n' Binder Term
b Term
sc) = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> Term -> Term
cl Env
env) Binder Term
b) (Env -> Term -> Term
cl ((Name
n, RigCount
Rig0, Binder Term
b)forall a. a -> [a] -> [a]
:Env
env) Term
sc)
   cl Env
env (App AppStatus Name
s Term
f Term
a) = forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Env -> Term -> Term
cl Env
env Term
f) (Env -> Term -> Term
cl Env
env Term
a)
   cl Env
env Term
t = Term
t

attack :: RunTactic
attack :: RunTactic
attack Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc)
    = do Name
h <- forall (m :: * -> *). Monad m => String -> StateT ProofState m Name
getName String
"hole"
         forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = Name
h forall a. a -> [a] -> [a]
: ProofState -> [Name]
holes ProofState
ps })
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> b -> Binder b
Guess Term
t (Name -> Term
newtm Name
h)) Term
sc
  where
    newtm :: Name -> Term
newtm Name
h = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (forall b. b -> Binder b
Hole Term
t) (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Term
t)
attack Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not an attackable hole"

claim :: Name -> Raw -> RunTactic
claim :: Name -> Raw -> RunTactic
claim Name
n Raw
ty Context
ctxt Env
env Term
t =
    do (Term
tyv, Term
tyt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
       forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
       forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let (Name
g:[Name]
gs) = ProofState -> [Name]
holes ProofState
ps in
                          ProofState
ps { holes :: [Name]
holes = Name
g forall a. a -> [a] -> [a]
: Name
n forall a. a -> [a] -> [a]
: [Name]
gs } )
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. b -> Binder b
Hole Term
tyv) Term
t

-- If the current goal is 'retty', make a claim which is a function that
-- can compute a retty from argty (i.e a claim 'argty -> retty')
claimFn :: Name -> Name -> Raw -> RunTactic
claimFn :: Name -> Name -> Raw -> RunTactic
claimFn Name
n Name
bn Raw
argty Context
ctxt Env
env t :: Term
t@(Bind Name
x (Hole Term
retty) Term
sc) =
    do (Term
tyv, Term
tyt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
argty
       forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
       forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let (Name
g:[Name]
gs) = ProofState -> [Name]
holes ProofState
ps in
                          ProofState
ps { holes :: [Name]
holes = Name
g forall a. a -> [a] -> [a]
: Name
n forall a. a -> [a] -> [a]
: [Name]
gs } )
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. b -> Binder b
Hole (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
bn (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing Term
tyv Term
tyt) Term
retty)) Term
t
claimFn Name
_ Name
_ Raw
_ Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't make function type here"

reorder_claims :: RunTactic
reorder_claims :: RunTactic
reorder_claims Context
ctxt Env
env Term
t
    = -- trace (showSep "\n" (map show (scvs t))) $
      let ([(Name, Binder Term)]
bs, Term
sc) = forall {a}.
TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs Term
t []
          newbs :: [(Name, Binder Term)]
newbs = forall a. [a] -> [a]
reverse ([(Name, Binder Term)] -> [(Name, Binder Term)]
sortB (forall a. [a] -> [a]
reverse [(Name, Binder Term)]
bs)) in
          forall {a}. Bool -> String -> a -> a
traceWhen ([(Name, Binder Term)]
bs forall a. Eq a => a -> a -> Bool
/= [(Name, Binder Term)]
newbs) (forall a. Show a => a -> String
show [(Name, Binder Term)]
bs forall a. [a] -> [a] -> [a]
++ String
"\n ==> \n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Binder Term)]
newbs) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. [(n, Binder (TT n))] -> TT n -> TT n
bindAll [(Name, Binder Term)]
newbs Term
sc)
  where scvs :: TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs (Bind a
n b :: Binder (TT a)
b@(Hole TT a
_) TT a
sc) [(a, Binder (TT a))]
acc = TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs TT a
sc ((a
n, Binder (TT a)
b)forall a. a -> [a] -> [a]
:[(a, Binder (TT a))]
acc)
        scvs TT a
sc [(a, Binder (TT a))]
acc = (forall a. [a] -> [a]
reverse [(a, Binder (TT a))]
acc, TT a
sc)

        sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
        sortB :: [(Name, Binder Term)] -> [(Name, Binder Term)]
sortB [] = []
        sortB ((Name, Binder Term)
x:[(Name, Binder Term)]
xs) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall {n} {b} {a}. Eq n => (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (Name, Binder Term)
x) [(Name, Binder Term)]
xs = (Name, Binder Term)
x forall a. a -> [a] -> [a]
: [(Name, Binder Term)] -> [(Name, Binder Term)]
sortB [(Name, Binder Term)]
xs
                     | Bool
otherwise = [(Name, Binder Term)] -> [(Name, Binder Term)]
sortB (forall {n}.
Eq n =>
(n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (Name, Binder Term)
x [(Name, Binder Term)]
xs)

        insertB :: (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (n, Binder (TT n))
x [] = [(n, Binder (TT n))
x]
        insertB (n, Binder (TT n))
x ((n, Binder (TT n))
y:[(n, Binder (TT n))]
ys) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall {n} {b} {a}. Eq n => (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (n, Binder (TT n))
x) ((n, Binder (TT n))
yforall a. a -> [a] -> [a]
:[(n, Binder (TT n))]
ys) = (n, Binder (TT n))
x forall a. a -> [a] -> [a]
: (n, Binder (TT n))
y forall a. a -> [a] -> [a]
: [(n, Binder (TT n))]
ys
                         | Bool
otherwise = (n, Binder (TT n))
y forall a. a -> [a] -> [a]
: (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (n, Binder (TT n))
x [(n, Binder (TT n))]
ys

        noOcc :: (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (n
n, b
_) (a
_, Let RigCount
_ TT n
t TT n
v) = forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
t Bool -> Bool -> Bool
&& forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
v
        noOcc (n
n, b
_) (a
_, Guess TT n
t TT n
v) = forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
t Bool -> Bool -> Bool
&& forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
v
        noOcc (n
n, b
_) (a
_, Binder (TT n)
b) = forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n (forall b. Binder b -> b
binderTy Binder (TT n)
b)

focus :: Name -> RunTactic
focus :: Name -> RunTactic
focus Name
n Context
ctxt Env
env Term
t = do forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                                            if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
                                               then ProofState
ps { holes :: [Name]
holes = Name
n forall a. a -> [a] -> [a]
: ([Name]
hs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n]) }
                                               else ProofState
ps)
                        ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
                        forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

movelast :: Name -> RunTactic
movelast :: Name -> RunTactic
movelast Name
n Context
ctxt Env
env Term
t = do forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                                              if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
                                                  then ProofState
ps { holes :: [Name]
holes = ([Name]
hs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n]) forall a. [a] -> [a] -> [a]
++ [Name
n] }
                                                  else ProofState
ps)
                           forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

implementationArg :: Name -> RunTactic
implementationArg :: Name -> RunTactic
implementationArg Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc)
    = do forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps
                            is :: [Name]
is = ProofState -> [Name]
implementations ProofState
ps in
                            ProofState
ps { holes :: [Name]
holes = ([Name]
hs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) forall a. [a] -> [a] -> [a]
++ [Name
x],
                                 implementations :: [Name]
implementations = Name
xforall a. a -> [a] -> [a]
:[Name]
is })
         forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t) Term
sc)
implementationArg Name
n Context
ctxt Env
env Term
_
    = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The current focus is not a hole."

autoArg :: Name -> RunTactic
autoArg :: Name -> RunTactic
autoArg Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc)
    = do forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (ProofState -> [(Name, ([FailContext], [Name]))]
autos ProofState
ps) of
                             Maybe ([FailContext], [Name])
Nothing ->
                               let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                               ProofState
ps { holes :: [Name]
holes = ([Name]
hs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) forall a. [a] -> [a] -> [a]
++ [Name
x],
                                    autos :: [(Name, ([FailContext], [Name]))]
autos = (Name
x, (ProofState -> [FailContext]
while_elaborating ProofState
ps, Term -> [Name]
refsIn Term
t)) forall a. a -> [a] -> [a]
: ProofState -> [(Name, ([FailContext], [Name]))]
autos ProofState
ps }
                             Just ([FailContext], [Name])
_ -> ProofState
ps)
         forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t) Term
sc)
autoArg Name
n Context
ctxt Env
env Term
_
    = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The current focus not a hole."

setinj :: Name -> RunTactic
setinj :: Name -> RunTactic
setinj Name
n Context
ctxt Env
env (Bind Name
x Binder Term
b Term
sc)
    = do forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let is :: [Name]
is = ProofState -> [Name]
injective ProofState
ps in
                            ProofState
ps { injective :: [Name]
injective = Name
n forall a. a -> [a] -> [a]
: [Name]
is })
         forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x Binder Term
b Term
sc)

defer :: [Name] -> [Name] -> Name -> RunTactic
defer :: [Name] -> [Name] -> Name -> RunTactic
defer [Name]
dropped [Name]
linused Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
nt Name
x' Term
ty)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let env' :: Env
env' = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, RigCount
_, Binder Term
t) -> Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
dropped) Env
env
       forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                          ProofState
ps { usedns :: [Name]
usedns = Name
n forall a. a -> [a] -> [a]
: ProofState -> [Name]
usedns ProofState
ps,
                               holes :: [Name]
holes = [Name]
hs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x] })
       ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. Int -> [Name] -> b -> Binder b
GHole (forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
env') (ProofState -> [Name]
psnames ProofState
ps) (Env -> Term -> Term
mkTy (forall a. [a] -> [a]
reverse Env
env') Term
t))
                      (forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty) (forall a b. (a -> b) -> [a] -> [b]
map forall {n} {b}. (n, b, Binder (TT n)) -> TT n
getP (forall a. [a] -> [a]
reverse Env
env'))))
  where
    mkTy :: Env -> Term -> Term
mkTy []           Term
t = Term
t
    mkTy ((Name
n,RigCount
rig,Binder Term
b) : Env
bs) Term
t = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi (RigCount -> Name -> RigCount
setRig RigCount
rig Name
n) forall a. Maybe a
Nothing (forall b. Binder b -> b
binderTy Binder Term
b) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (Env -> Term -> Term
mkTy Env
bs Term
t)

    setRig :: RigCount -> Name -> RigCount
setRig RigCount
Rig1 Name
n | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
linused = RigCount
Rig0
    setRig RigCount
rig Name
n = RigCount
rig

    getP :: (n, b, Binder (TT n)) -> TT n
getP (n
n, b
rig, Binder (TT n)
b) = forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n (forall b. Binder b -> b
binderTy Binder (TT n)
b)
defer [Name]
dropped [Name]
linused Name
n Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't defer a non-hole focus."

-- as defer, but build the type and application explicitly
deferType :: Name -> Raw -> [Name] -> RunTactic
deferType :: Name -> Raw -> [Name] -> RunTactic
deferType Name
n Raw
fty_in [Name]
args Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
nt Name
x' Term
ty)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
fty, Term
_) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
fty_in
       forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps
                          ds :: [Name]
ds = ProofState -> [Name]
deferred ProofState
ps in
                          ProofState
ps { holes :: [Name]
holes = [Name]
hs forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                               deferred :: [Name]
deferred = Name
n forall a. a -> [a] -> [a]
: [Name]
ds })
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. Int -> [Name] -> b -> Binder b
GHole Int
0 [] Term
fty)
                      (forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty) (forall a b. (a -> b) -> [a] -> [b]
map Name -> Term
getP [Name]
args)))
  where
    getP :: Name -> Term
getP Name
n = case forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
env of
                  Just Binder Term
b -> forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n (forall b. Binder b -> b
binderTy Binder Term
b)
                  Maybe (Binder Term)
Nothing -> forall a. HasCallStack => String -> a
error (String
"deferType can't find " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n)
deferType Name
_ Raw
_ [Name]
_ Context
_ Env
_ Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't defer a non-hole focus."

unifyGoal :: Raw -> RunTactic
unifyGoal :: Raw -> RunTactic
unifyGoal Raw
tm Context
ctxt Env
env h :: Term
h@(Bind Name
x Binder Term
b Term
sc) =
    do (Term
tmv, Term
_) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
       [(Name, Term)]
ns' <- Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (forall b. Binder b -> b
binderTy Binder Term
b, forall a. Maybe a
Nothing) (Term
tmv, forall a. Maybe a
Nothing)
       forall (m :: * -> *) a. Monad m => a -> m a
return Term
h
unifyGoal Raw
_ Context
_ Env
_ Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The focus is not a binder."

unifyTerms :: Raw -> Raw -> RunTactic
unifyTerms :: Raw -> Raw -> RunTactic
unifyTerms Raw
tm1 Raw
tm2 Context
ctxt Env
env Term
h =
    do (Term
tm1v, Term
_) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm1
       (Term
tm2v, Term
_) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm2
       [(Name, Term)]
ns' <- Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
tm1v, forall a. Maybe a
Nothing) (Term
tm2v, forall a. Maybe a
Nothing)
       forall (m :: * -> *) a. Monad m => a -> m a
return Term
h

exact :: Raw -> RunTactic
exact :: Raw -> RunTactic
exact Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do (Term
val, Term
valty) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
       forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
valty Term
ty
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
exact Raw
_ Context
_ Env
_ Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't fill here."

-- As exact, but attempts to solve other goals by unification

fill :: Raw -> RunTactic
fill :: Raw -> RunTactic
fill Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do (Term
val, Term
valty) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
       Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
valty, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val)
                       (Term
ty, forall a. a -> Maybe a
Just (Term -> Term -> Provenance
chkPurpose Term
val Term
ty))
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
  where
    -- some expected types show up commonly in errors and indicate a
    -- specific problem.
    --   argTy -> retTy suggests a function applied to too many arguments
    chkPurpose :: Term -> Term -> Provenance
chkPurpose Term
val (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ (P NameType
_ (MN Int
_ Text
_) Term
_) Term
_) (P NameType
_ (MN Int
_ Text
_) Term
_))
                   = Term -> Provenance
TooManyArgs Term
val
    chkPurpose Term
_ Term
_ = Provenance
ExpectedType
fill Raw
_ Context
_ Env
_ Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't fill here."

-- As fill, but attempts to solve other goals by matching

match_fill :: Raw -> RunTactic
match_fill :: Raw -> RunTactic
match_fill Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do (Term
val, Term
valty) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
       Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
valty, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val)
                             (Term
ty, forall a. a -> Maybe a
Just Provenance
ExpectedType)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
match_fill Raw
_ Context
_ Env
_ Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't fill here."

prep_fill :: Name -> [Name] -> RunTactic
prep_fill :: Name -> [Name] -> RunTactic
prep_fill Name
f [Name]
as Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do let val :: Term
val = forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
f forall n. TT n
Erased) (forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n forall n. TT n
Erased) [Name]
as)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
prep_fill Name
f [Name]
as Context
ctxt Env
env Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Can't prepare fill at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t

complete_fill :: RunTactic
complete_fill :: RunTactic
complete_fill Context
ctxt Env
env (Bind Name
x (Guess Term
ty Term
val) Term
sc) =
    do let guess :: Raw
guess = Term -> Raw
forget Term
val
       (Term
val', Term
valty) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
       Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
valty, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val')
                       (Term
ty, forall a. a -> Maybe a
Just Provenance
ExpectedType)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
complete_fill Context
ctxt Env
env Term
t = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Can't complete fill at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
t

-- When solving something in the 'dont unify' set, we should check
-- that the guess we are solving it with unifies with the thing unification
-- found for it, if anything.

solve :: RunTactic
solve :: RunTactic
solve Context
ctxt Env
env (Bind Name
x (Guess Term
ty Term
val) Term
sc)
   = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
        [Name]
dropdots <-
             case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (ProofState -> [(Name, Term)]
notunified ProofState
ps) of
                Just (P NameType
_ Name
h Term
_)
                     | Name
h forall a. Eq a => a -> a -> Bool
== Name
x -> forall (m :: * -> *) a. Monad m => a -> m a
return [] -- Can't solve itself!
                Just Term
tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
                            do Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
tm, forall a. a -> Maybe a
Just Provenance
InferredVal)
                                                     (Term
val, forall a. a -> Maybe a
Just Provenance
GivenVal)
                               forall (m :: * -> *) a. Monad m => a -> m a
return [Name
x]
                Maybe Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
        forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"Dropping hole " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
x) forall a b. (a -> b) -> a -> b
$
                                       ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                            solved :: Maybe (Name, Term)
solved = forall a. a -> Maybe a
Just (Name
x, Term
val),
                            dontunify :: [Name]
dontunify = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Name
x) (ProofState -> [Name]
dontunify ProofState
ps),
                            notunified :: [(Name, Term)]
notunified = forall {a}. [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [(Name
x,Term
val)]
                                           (ProofState -> [(Name, Term)]
notunified ProofState
ps),
                            recents :: [Name]
recents = Name
x forall a. a -> [a] -> [a]
: ProofState -> [Name]
recents ProofState
ps,
                            implementations :: [Name]
implementations = ProofState -> [Name]
implementations ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                            dotted :: [(Name, [Name])]
dotted = forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, t a)] -> [(a, t a)]
dropUnified [Name]
dropdots (ProofState -> [(Name, [Name])]
dotted ProofState
ps) })
        let (Term
locked, Bool
_) = [Name] -> Term -> (Term, Bool)
tryLock (ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) (forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x Term
val Term
sc) in
            forall (m :: * -> *) a. Monad m => a -> m a
return Term
locked
  where dropUnified :: t a -> [(a, t a)] -> [(a, t a)]
dropUnified t a
ddots [] = []
        dropUnified t a
ddots ((a
x, t a
es) : [(a, t a)]
ds)
             | a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ddots Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\a
e -> a
e forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ddots) t a
es
                  = t a -> [(a, t a)] -> [(a, t a)]
dropUnified t a
ddots [(a, t a)]
ds
             | Bool
otherwise = (a
x, t a
es) forall a. a -> [a] -> [a]
: t a -> [(a, t a)] -> [(a, t a)]
dropUnified t a
ddots [(a, t a)]
ds

        tryLock :: [Name] -> Term -> (Term, Bool)
        tryLock :: [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs tm :: Term
tm@(App AppStatus Name
Complete Term
_ Term
_) = (Term
tm, Bool
True)
        tryLock [Name]
hs tm :: Term
tm@(App AppStatus Name
s Term
f Term
a) =
             let (Term
f', Bool
fl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
f
                 (Term
a', Bool
al) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
a in
                 if Bool
fl Bool -> Bool -> Bool
&& Bool
al then (forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete Term
f' Term
a', Bool
True)
                             else (forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Term
f' Term
a', Bool
False)
        tryLock [Name]
hs t :: Term
t@(P NameType
_ Name
n Term
_) = (Term
t, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs)
        tryLock [Name]
hs t :: Term
t@(Bind Name
n (Hole Term
_) Term
sc) = (Term
t, Bool
False)
        tryLock [Name]
hs t :: Term
t@(Bind Name
n (Guess Term
_ Term
_) Term
sc) = (Term
t, Bool
False)
        tryLock [Name]
hs t :: Term
t@(Bind Name
n (Let RigCount
r Term
ty Term
val) Term
sc)
            = let (Term
ty', Bool
tyl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
ty
                  (Term
val', Bool
vall) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
val
                  (Term
sc', Bool
scl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
sc in
                  (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
r Term
ty' Term
val') Term
sc', Bool
tyl Bool -> Bool -> Bool
&& Bool
vall Bool -> Bool -> Bool
&& Bool
scl)
        tryLock [Name]
hs t :: Term
t@(Bind Name
n Binder Term
b Term
sc)
            = let (Term
bt', Bool
btl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs (forall b. Binder b -> b
binderTy Binder Term
b)
                  (Term
sc', Bool
scl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
sc in
                  (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Binder Term
b { binderTy :: Term
binderTy = Term
bt' }) Term
sc', Bool
btl Bool -> Bool -> Bool
&& Bool
scl)
        tryLock [Name]
hs Term
t = (Term
t, Bool
True)

solve Context
_ Env
_ h :: Term
h@(Bind Name
x Binder Term
t Term
sc)
   = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
        case forall {a}. Eq a => a -> TT a -> Maybe a
findType Name
x Term
sc of
             Just Name
t -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. String -> Err' t
CantInferType (forall a. Show a => a -> String
show Name
t))
             Maybe Name
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. t -> Err' t
IncompleteTerm Term
h)
   where findType :: a -> TT a -> Maybe a
findType a
x (Bind a
n (Let RigCount
r TT a
t TT a
v) TT a
sc)
              = a -> TT a -> Maybe a
findType a
x TT a
v forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` a -> TT a -> Maybe a
findType a
x TT a
sc
         findType a
x (Bind a
n Binder (TT a)
t TT a
sc)
              | P NameType
_ a
x' TT a
_ <- forall b. Binder b -> b
binderTy Binder (TT a)
t, a
x forall a. Eq a => a -> a -> Bool
== a
x' = forall a. a -> Maybe a
Just a
n
              | Bool
otherwise = a -> TT a -> Maybe a
findType a
x TT a
sc
         findType a
x TT a
_ = forall a. Maybe a
Nothing

introTy :: Raw -> Maybe Name -> RunTactic
introTy :: Raw -> Maybe Name -> RunTactic
introTy Raw
ty Maybe Name
mn Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let n :: Name
n = case Maybe Name
mn of
                  Just Name
name -> Name
name
                  Maybe Name
Nothing -> Name
x
       let t' :: Term
t' = case Term
t of
                    x :: Term
x@(Bind Name
y (Pi RigCount
_ Maybe ImplicitInfo
_ Term
s Term
_) Term
_) -> Term
x
                    Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
t
       (Term
tyv, Term
tyt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
       case Term
t' of
           Bind Name
y (Pi RigCount
rig Maybe ImplicitInfo
_ Term
s Term
_) Term
t -> let t' :: Term
t' = forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t in
                                        do Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
s, forall a. Maybe a
Nothing) (Term
tyv, forall a. Maybe a
Nothing)
                                           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
tyv) (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t') (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
           Term
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ forall t. t -> Err' t
CantIntroduce Term
t'
introTy Raw
ty Maybe Name
n Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't introduce here."

intro :: Maybe Name -> RunTactic
intro :: Maybe Name -> RunTactic
intro Maybe Name
mn Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let t' :: Term
t' = case Term
t of
                    x :: Term
x@(Bind Name
y (Pi RigCount
_ Maybe ImplicitInfo
_ Term
s Term
_) Term
_) -> Term
x
                    Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
t
       case Term
t' of
           Bind Name
y (Pi RigCount
rig Maybe ImplicitInfo
_ Term
s Term
_) Term
t ->
               let n :: Name
n = case Maybe Name
mn of
                      Just Name
name -> Name
name
                      Maybe Name
Nothing -> Name
y
               -- It's important that this be subst and not updsubst,
               -- because we want to substitute even in portions of
               -- terms that we know do not contain holes.
                   t' :: Term
t' = forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
y (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t
               in forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
s) (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t') (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
           Term
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ forall t. t -> Err' t
CantIntroduce Term
t'
intro Maybe Name
n Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't introduce here."

forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
forAll Name
n RigCount
rig Maybe ImplicitInfo
impl Raw
ty Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
tyv, Term
tyt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
       Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
tyt, forall a. Maybe a
Nothing) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), forall a. Maybe a
Nothing)
       Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT ProofState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
t, forall a. Maybe a
Nothing) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), forall a. Maybe a
Nothing)
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
impl Term
tyv (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t) (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t))
forAll Name
n RigCount
rig Maybe ImplicitInfo
impl Raw
ty Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't pi bind here"

patvar :: Name -> RunTactic
patvar :: Name -> RunTactic
patvar Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc) =
    do forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"Dropping pattern hole " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
x) forall a b. (a -> b) -> a -> b
$
                                     ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                           solved :: Maybe (Name, Term)
solved = forall a. a -> Maybe a
Just (Name
x, forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
t),
                           dontunify :: [Name]
dontunify = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/=Name
x) (ProofState -> [Name]
dontunify ProofState
ps),
                           notunified :: [(Name, Term)]
notunified = forall {a}. [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [(Name
x,forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
t)]
                                          (ProofState -> [(Name, Term)]
notunified ProofState
ps),
                           injective :: [Name]
injective = forall {a}. Eq a => a -> a -> [a] -> [a]
addInj Name
n Name
x (ProofState -> [Name]
injective ProofState
ps)
                         })
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
PVar RigCount
RigW Term
t) (forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
t) Term
sc)
  where addInj :: a -> a -> [a] -> [a]
addInj a
n a
x [a]
ps | a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ps = a
n forall a. a -> [a] -> [a]
: [a]
ps
                      | Bool
otherwise = [a]
ps
patvar Name
n Context
ctxt Env
env Term
tm = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Can't add pattern var at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm

letbind :: Name -> RigCount -> Raw -> Raw -> RunTactic
letbind :: Name -> RigCount -> Raw -> Raw -> RunTactic
letbind Name
n RigCount
rig Raw
ty Raw
val Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
tyv,  Term
tyt)  <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
       (Term
valv, Term
valt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
val
       forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Term
tyv Term
valv) (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t) (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t))
letbind Name
n RigCount
rig Raw
ty Raw
val Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't let bind here"

expandLet :: Name -> Term -> RunTactic
expandLet :: Name -> Term -> RunTactic
expandLet Name
n Term
v Context
ctxt Env
env Term
tm =
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
n Term
v Term
tm

rewrite :: Raw -> RunTactic
rewrite :: Raw -> RunTactic
rewrite Raw
tm Context
ctxt Env
env (Bind Name
x (Hole Term
t) xp :: Term
xp@(P NameType
_ Name
x' Term
_)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
tmv, Term
tmt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
       let tmt' :: Term
tmt' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
tmt
       case forall n. TT n -> (TT n, [TT n])
unApply Term
tmt' of
         (P NameType
_ (UN Text
q) Term
_, [Term
lt,Term
rt,Term
l,Term
r]) | Text
q forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"=" ->
            do let p :: Term
p = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
rname (forall b. RigCount -> b -> Binder b
Lam RigCount
RigW Term
lt) (Term -> Term -> Term -> Term -> Term
mkP (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
rname Term
lt) Term
r Term
l Term
t)
               let newt :: Term
newt = Term -> Term -> Term -> Term -> Term
mkP Term
l Term
r Term
l Term
t
               let sc :: Raw
sc = Term -> Raw
forget forall a b. (a -> b) -> a -> b
$ (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
newt)
                                       (forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"replace") (forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)))
                                              [Term
lt, Term
l, Term
r, Term
p, Term
tmv, Term
xp]))
               (Term
scv, Term
sct) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
sc
               forall (m :: * -> *) a. Monad m => a -> m a
return Term
scv
         (Term, [Term])
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. t -> t -> Err' t
NotEquality Term
tmv Term
tmt')
  where rname :: Name
rname = Int -> String -> Name
sMN Int
0 String
"replaced"
rewrite Raw
_ Context
_ Env
_ Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't rewrite here"

-- To make the P for rewrite, replace syntactic occurrences of l in ty with
-- an x, and put \x : lt in front
mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
mkP :: Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
ty | Term
l forall a. Eq a => a -> a -> Bool
== Term
ty = Term
lt
mkP Term
lt Term
l Term
r (App AppStatus Name
s Term
f Term
a) = let f' :: Term
f' = if (Term
r forall a. Eq a => a -> a -> Bool
/= Term
f) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
f else Term
f
                             a' :: Term
a' = if (Term
r forall a. Eq a => a -> a -> Bool
/= Term
a) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
a else Term
a in
                             forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Term
f' Term
a'
mkP Term
lt Term
l Term
r (Bind Name
n Binder Term
b Term
sc)
                     = let b' :: Binder Term
b' = Binder Term -> Binder Term
mkPB Binder Term
b
                           sc' :: Term
sc' = if (Term
r forall a. Eq a => a -> a -> Bool
/= Term
sc) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
sc else Term
sc in
                           forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
sc'
    where mkPB :: Binder Term -> Binder Term
mkPB (Let RigCount
c Term
t Term
v) = let t' :: Term
t' = if (Term
r forall a. Eq a => a -> a -> Bool
/= Term
t) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
t else Term
t
                                 v' :: Term
v' = if (Term
r forall a. Eq a => a -> a -> Bool
/= Term
v) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
v else Term
v in
                                 forall b. RigCount -> b -> b -> Binder b
Let RigCount
c Term
t' Term
v'
          mkPB Binder Term
b = let ty :: Term
ty = forall b. Binder b -> b
binderTy Binder Term
b
                       ty' :: Term
ty' = if (Term
r forall a. Eq a => a -> a -> Bool
/= Term
ty) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
ty else Term
ty in
                             Binder Term
b { binderTy :: Term
binderTy = Term
ty' }
mkP Term
lt Term
l Term
r Term
x = Term
x

equiv :: Raw -> RunTactic
equiv :: Raw -> RunTactic
equiv Raw
tm Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc) =
    do (Term
tmv, Term
tmt) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
       forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
tmv Term
t
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
tmv) Term
sc
equiv Raw
tm Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't equiv here"

patbind :: Name -> RigCount -> RunTactic
patbind :: Name -> RigCount -> RunTactic
patbind Name
n RigCount
rig Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let t' :: Term
t' = case Term
t of
                    x :: Term
x@(Bind Name
y (PVTy Term
s) Term
t) -> Term
x
                    Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
t
       case Term
t' of
           Bind Name
y (PVTy Term
s) Term
t -> let t' :: Term
t' = forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t in
                                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
PVar RigCount
rig Term
s) (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
t') (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
           Term
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Nothing to pattern bind"
patbind Name
n RigCount
_ Context
ctxt Env
env Term
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't pattern bind here"

compute :: RunTactic
compute :: RunTactic
compute Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
ty)) Term
sc
compute Context
ctxt Env
env Term
t = forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

whnf_compute :: RunTactic
whnf_compute :: RunTactic
whnf_compute Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do let ty' :: Term
ty' = Context -> Env -> Term -> Term
whnf Context
ctxt Env
env Term
ty in
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
ty') Term
sc
whnf_compute Context
ctxt Env
env Term
t = forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

whnf_compute_args :: RunTactic
whnf_compute_args :: RunTactic
whnf_compute_args Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do let ty' :: Term
ty' = Context -> Env -> Term -> Term
whnfArgs Context
ctxt Env
env Term
ty in
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole Term
ty') Term
sc
whnf_compute_args Context
ctxt Env
env Term
t = forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

-- reduce let bindings only
simplify :: RunTactic
simplify :: RunTactic
simplify Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
    do forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (forall b. b -> Binder b
Hole (forall a b. (a, b) -> a
fst (Context -> Env -> [(Name, Int)] -> Term -> (Term, [(Name, Int)])
specialise Context
ctxt Env
env [] Term
ty))) Term
sc
simplify Context
ctxt Env
env Term
t = forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

check_in :: Raw -> RunTactic
check_in :: Raw -> RunTactic
check_in Raw
t Context
ctxt Env
env Term
tm =
    do (Term
val, Term
valty) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
t
       forall (m :: * -> *). Monad m => String -> StateT ProofState m ()
addLog (forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty)
       forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm

eval_in :: Raw -> RunTactic
eval_in :: Raw -> RunTactic
eval_in Raw
t Context
ctxt Env
env Term
tm =
    do (Term
val, Term
valty) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
t
       let val' :: Term
val' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
val
       let valty' :: Term
valty' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
valty
       forall (m :: * -> *). Monad m => String -> StateT ProofState m ()
addLog (forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++
               forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty forall a. [a] -> [a] -> [a]
++
--                     " in " ++ show env ++
               String
" ==>\n " forall a. [a] -> [a] -> [a]
++
               forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val' forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++
               forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty')
       forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm

start_unify :: Name -> RunTactic
start_unify :: Name -> RunTactic
start_unify Name
n Context
ctxt Env
env Term
tm = do -- action (\ps -> ps { unified = (n, []) })
                               forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm

solve_unified :: RunTactic
solve_unified :: RunTactic
solve_unified Context
ctxt Env
env Term
tm =
    do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
       let (Name
_, [(Name, Term)]
ns) = ProofState -> (Name, [(Name, Term)])
unified ProofState
ps
       let unify :: [(Name, Term)]
unify = forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (ProofState -> [Name]
dontunify ProofState
ps) [(Name, Term)]
ns (ProofState -> [Name]
holes ProofState
ps)
       forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"Dropping holes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
unify)) forall a b. (a -> b) -> a -> b
$
                                     ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
unify,
                           recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
unify })
       forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { pterm :: ProofTerm
pterm = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)]
unify (ProofState -> ProofTerm
pterm ProofState
ps) })
       forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
unify Term
tm)

dropGiven :: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [] t a
hs = []
dropGiven t a
du ((a
n, P NameType
Bound a
t TT a
ty) : [(a, TT a)]
us) t a
hs
   | a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du Bool -> Bool -> Bool
&& Bool -> Bool
not (a
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
     Bool -> Bool -> Bool
&& a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& a
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs
            = (a
t, forall n. NameType -> n -> TT n -> TT n
P NameType
Bound a
n TT a
ty) forall a. a -> [a] -> [a]
: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [(a, TT a)]
us t a
hs
dropGiven t a
du (u :: (a, TT a)
u@(a
n, TT a
_) : [(a, TT a)]
us) t a
hs
   | a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du = t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [(a, TT a)]
us t a
hs
-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
dropGiven t a
du ((a, TT a)
u : [(a, TT a)]
us) t a
hs = (a, TT a)
u forall a. a -> [a] -> [a]
: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [(a, TT a)]
us t a
hs

keepGiven :: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [] t a
hs = []
keepGiven t a
du ((a
n, P NameType
Bound a
t TT a
ty) : [(a, TT a)]
us) t a
hs
   | a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du Bool -> Bool -> Bool
&& Bool -> Bool
not (a
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
     Bool -> Bool -> Bool
&& a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& a
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs
            = t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [(a, TT a)]
us t a
hs
keepGiven t a
du (u :: (a, TT a)
u@(a
n, TT a
_) : [(a, TT a)]
us) t a
hs
   | a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du = (a, TT a)
u forall a. a -> [a] -> [a]
: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [(a, TT a)]
us t a
hs
keepGiven t a
du ((a, TT a)
u : [(a, TT a)]
us) t a
hs = t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [(a, TT a)]
us t a
hs

updateEnv :: [(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [] [(a, b, f Term)]
e = [(a, b, f Term)]
e
updateEnv [(Name, Term)]
ns [] = []
updateEnv [(Name, Term)]
ns ((a
n, b
rig, f Term
b) : [(a, b, f Term)]
env)
   = (a
n, b
rig, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns) f Term
b) forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns [(a, b, f Term)]
env

updateProv :: [(Name, Term)] -> Provenance -> Provenance
updateProv [(Name, Term)]
ns (SourceTerm Term
t) = Term -> Provenance
SourceTerm forall a b. (a -> b) -> a -> b
$ [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
t
updateProv [(Name, Term)]
ns Provenance
p = Provenance
p

updateError :: [(Name, Term)] -> Err -> Err
updateError [] Err
err = Err
err
updateError [(Name, Term)]
ns (At FC
f Err
e) = forall t. FC -> Err' t -> Err' t
At FC
f ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e)
updateError [(Name, Term)]
ns (Elaborating String
s Name
n Maybe Term
ty Err
e) = forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
s Name
n Maybe Term
ty ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e)
updateError [(Name, Term)]
ns (ElaboratingArg Name
f Name
a [(Name, Name)]
env Err
e)
 = forall t. Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
ElaboratingArg Name
f Name
a [(Name, Name)]
env ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e)
updateError [(Name, Term)]
ns (CantUnify Bool
b (Term
l,Maybe Provenance
lp) (Term
r,Maybe Provenance
rp) Err
e [(Name, Term)]
xs Int
sc)
 = forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
b ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
l, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Provenance -> Provenance
updateProv [(Name, Term)]
ns) Maybe Provenance
lp)
               ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
r, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Provenance -> Provenance
updateProv [(Name, Term)]
ns) Maybe Provenance
rp) ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e) [(Name, Term)]
xs Int
sc
updateError [(Name, Term)]
ns Err
e = Err
e

mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified Env
env [Name]
holes [(Name, Term)]
ns = forall {a} {t} {a}.
(Eq a, Eq t) =>
[(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [(Name, Term)]
ns [] [] where
  mnu :: [(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [] [(a, t)]
ns_acc [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc = (forall a. [a] -> [a]
reverse [(a, t)]
ns_acc, forall a. [a] -> [a]
reverse [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc)
  mnu ((a
n, t
t):[(a, t)]
ns) [(a, t)]
ns_acc [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc
      | Just t
t' <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, t)]
ns, t
t forall a. Eq a => a -> a -> Bool
/= t
t'
             = [(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [(a, t)]
ns ((a
n,t
t') forall a. a -> [a] -> [a]
: [(a, t)]
ns_acc)
                      ((t
t,t
t',Bool
True, Env
env,forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
True (t
t, forall a. Maybe a
Nothing) (t
t', forall a. Maybe a
Nothing) (forall t. String -> Err' t
Msg String
"") [] Int
0, [],FailAt
Match) forall a. a -> [a] -> [a]
: [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc)
      | Bool
otherwise = [(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [(a, t)]
ns ((a
n,t
t) forall a. a -> [a] -> [a]
: [(a, t)]
ns_acc) [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc

updateNotunified :: [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [] [(a, Term)]
nu = [(a, Term)]
nu
updateNotunified [(Name, Term)]
ns [(a, Term)]
nu = forall {a}. [(a, Term)] -> [(a, Term)]
up [(a, Term)]
nu where
  up :: [(a, Term)] -> [(a, Term)]
up [] = []
  up ((a
n, Term
t) : [(a, Term)]
nus) = let t' :: Term
t' = [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
t in
                          ((a
n, Term
t') forall a. a -> [a] -> [a]
: [(a, Term)] -> [(a, Term)]
up [(a, Term)]
nus)

getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance (CantUnify Bool
_ (Term
_, Maybe Provenance
lp) (Term
_, Maybe Provenance
rp) Err
_ [(Name, Term)]
_ Int
_) = (Maybe Provenance
lp, Maybe Provenance
rp)
getProvenance Err
_ = (forall a. Maybe a
Nothing, forall a. Maybe a
Nothing)

setReady :: (a, b, c, d, e, f, g) -> (a, b, Bool, d, e, f, g)
setReady (a
x, b
y, c
_, d
env, e
err, f
c, g
at) = (a
x, b
y, Bool
True, d
env, e
err, f
c, g
at)

updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
                    -> ([(Name, TT Name)], Fails)
-- updateProblems ctxt [] ps inj holes = ([], ps)
updateProblems :: ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems ProofState
ps [(Name, Term)]
updates Fails
probs = forall {t} {g}.
(Eq t, Num t) =>
t
-> [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
rec Integer
10 [(Name, Term)]
updates Fails
probs
 where
  -- keep trying if we make progress, but not too many times...
  rec :: t
-> [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
rec t
0 [(Name, Term)]
us [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs = ([(Name, Term)]
us, [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs)
  rec t
n [(Name, Term)]
us [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs = case forall {g}.
[(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
us [] [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs of
                     res :: ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res@([(Name, Term)]
_, []) -> ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res
                     res :: ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res@([(Name, Term)]
us', [(Term, Term, Bool, Env, Err, [FailContext], g)]
_) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Term)]
us' forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Term)]
us -> ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res
                     ([(Name, Term)]
us', [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs') -> t
-> [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
rec (t
n forall a. Num a => a -> a -> a
- t
1) [(Name, Term)]
us' [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs'

  hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps
  inj :: [Name]
inj = ProofState -> [Name]
injective ProofState
ps
  ctxt :: Context
ctxt = ProofState -> Context
context ProofState
ps
  ulog :: Bool
ulog = ProofState -> Bool
unifylog ProofState
ps
  usupp :: [Name]
usupp = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (ProofState -> [(Name, Term)]
notunified ProofState
ps)
  dont :: [Name]
dont = ProofState -> [Name]
dontunify ProofState
ps

  up :: [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
ns [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc [] = ([(Name, Term)]
ns, forall a b. (a -> b) -> [a] -> [b]
map (forall {f :: * -> *} {c} {a} {b} {f} {g}.
Functor f =>
[(Name, Term)]
-> (Term, Term, c, [(a, b, f Term)], Err, f, g)
-> (Term, Term, Bool, [(a, b, f Term)], Err, f, g)
updateNs [(Name, Term)]
ns) (forall a. [a] -> [a]
reverse [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc))
  up [(Name, Term)]
ns [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc (prob :: (Term, Term, Bool, Env, Err, [FailContext], g)
prob@(Term
x, Term
y, Bool
ready, Env
env, Err
err, [FailContext]
while, g
um) : [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps) =
    let (Term
x', Bool
newx) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
x
        (Term
y', Bool
newy) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
y
        (Maybe Provenance
lp, Maybe Provenance
rp) = Err -> (Maybe Provenance, Maybe Provenance)
getProvenance Err
err
        err' :: Err
err' = [(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
err
        env' :: Env
env' = forall {f :: * -> *} {a} {b}.
Functor f =>
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns Env
env in
          if Bool
newx Bool -> Bool -> Bool
|| Bool
newy Bool -> Bool -> Bool
|| Bool
ready Bool -> Bool -> Bool
||
             forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
n -> Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj) (Term -> [Name]
refsIn Term
x forall a. [a] -> [a] -> [a]
++ Term -> [Name]
refsIn Term
y) then
            case Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, Term)], Fails)
unify Context
ctxt Env
env' (Term
x', Maybe Provenance
lp) (Term
y', Maybe Provenance
rp) [Name]
inj [Name]
hs [Name]
usupp [FailContext]
while of
                 OK ([(Name, Term)]
v, []) -> forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"DID " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term
x',Term
y',Bool
ready,[(Name, Term)]
v,[Name]
dont)) forall a b. (a -> b) -> a -> b
$
                                let v' :: [(Name, Term)]
v' = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, Term
_) -> Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
dont) [(Name, Term)]
v in
                                    [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
up ([(Name, Term)]
ns forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
v') [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps
                 TC ([(Name, Term)], Fails)
e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
                      [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
ns ((Term
x',Term
y',Bool
False,Env
env',Err
err',[FailContext]
while,g
um) forall a. a -> [a] -> [a]
: [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc) [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps
            else -- trace ("SKIPPING " ++ show (x,y,ready)) $
                 [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
ns ((Term
x',Term
y', Bool
False, Env
env',Err
err', [FailContext]
while, g
um) forall a. a -> [a] -> [a]
: [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc) [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps

  updateNs :: [(Name, Term)]
-> (Term, Term, c, [(a, b, f Term)], Err, f, g)
-> (Term, Term, Bool, [(a, b, f Term)], Err, f, g)
updateNs [(Name, Term)]
ns (Term
x, Term
y, c
t, [(a, b, f Term)]
env, Err
err, f
fc, g
fa)
       = let (Term
x', Bool
newx) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
x
             (Term
y', Bool
newy) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
y in
             (Term
x', Term
y', Bool
newx Bool -> Bool -> Bool
|| Bool
newy,
                  forall {f :: * -> *} {a} {b}.
Functor f =>
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns [(a, b, f Term)]
env, [(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
err, f
fc, g
fa)

orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved [(Name, Term)]
ns ProofTerm
tm = [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update [] [(Name, Term)]
ns ProofTerm
tm
  where
    update :: [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update [Name]
done [] ProofTerm
t = (ProofTerm
t, [Name]
done)
    update [Name]
done ((Name
n, P NameType
_ Name
n' Term
_) : [(Name, Term)]
ns) ProofTerm
t | Name
n forall a. Eq a => a -> a -> Bool
== Name
n' = [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update [Name]
done [(Name, Term)]
ns ProofTerm
t
    update [Name]
done ((Name, Term)
n : [(Name, Term)]
ns) ProofTerm
t = [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update (forall a b. (a, b) -> a
fst (Name, Term)
n forall a. a -> [a] -> [a]
: [Name]
done)
                                    (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. (Name, Term) -> (a, Term) -> (a, Term)
updateMatch (Name, Term)
n) [(Name, Term)]
ns)
                                    ([(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)
n] ProofTerm
t)

    -- Update the later solutions too
    updateMatch :: (Name, Term) -> (a, Term) -> (a, Term)
updateMatch (Name, Term)
n (a
x, Term
tm) = (a
x, [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)
n] Term
tm)

-- attempt to solve remaining problems with match_unify
matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
                    -> ([(Name, TT Name)], Fails)
matchProblems :: Bool
-> ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all ProofState
ps [(Name, Term)]
updates Fails
probs = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
updates Fails
probs where
  hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps
  inj :: [Name]
inj = ProofState -> [Name]
injective ProofState
ps
  ctxt :: Context
ctxt = ProofState -> Context
context ProofState
ps

  up :: [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
ns [] = ([(Name, Term)]
ns, [])
  up [(Name, Term)]
ns ((Term
x, Term
y, Bool
ready, Env
env, Err
err, [FailContext]
while, FailAt
um) : Fails
ps)
       | Bool
all Bool -> Bool -> Bool
|| FailAt
um forall a. Eq a => a -> a -> Bool
== FailAt
Match =
    let x' :: Term
x' = [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
x
        y' :: Term
y' = [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
y
        (Maybe Provenance
lp, Maybe Provenance
rp) = Err -> (Maybe Provenance, Maybe Provenance)
getProvenance Err
err
        err' :: Err
err' = [(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
err
        env' :: Env
env' = forall {f :: * -> *} {a} {b}.
Functor f =>
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns Env
env in
        case Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Term)]
match_unify Context
ctxt Env
env' (Term
x', Maybe Provenance
lp) (Term
y', Maybe Provenance
rp) [Name]
inj [Name]
hs [FailContext]
while of
            OK [(Name, Term)]
v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
                               [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up ([(Name, Term)]
ns forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
v) Fails
ps
            TC [(Name, Term)]
_ -> let ([(Name, Term)]
ns', Fails
ps') = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
ns Fails
ps in
                     ([(Name, Term)]
ns', (Term
x', Term
y', Bool
True, Env
env', Err
err', [FailContext]
while, FailAt
um) forall a. a -> [a] -> [a]
: Fails
ps')
  up [(Name, Term)]
ns ((Term, Term, Bool, Env, Err, [FailContext], FailAt)
p : Fails
ps) = let ([(Name, Term)]
ns', Fails
ps') = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
ns Fails
ps in
                       ([(Name, Term)]
ns', (Term, Term, Bool, Env, Err, [FailContext], FailAt)
p forall a. a -> [a] -> [a]
: Fails
ps')

processTactic :: Tactic -> ProofState -> TC (ProofState, String)
processTactic :: Tactic -> ProofState -> TC (ProofState, String)
processTactic Tactic
QED ProofState
ps = case ProofState -> [Name]
holes ProofState
ps of
                           [] -> do let tm :: Term
tm = {- normalise (context ps) [] -} ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps)
                                    (Term
tm', Term
ty', UCs
_) <- String -> Context -> Env -> Raw -> Term -> TC (Term, Term, UCs)
recheck (ProofState -> String
constraint_ns ProofState
ps) (ProofState -> Context
context ProofState
ps) [] (Term -> Raw
forget Term
tm) Term
tm
                                    forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps { done :: Bool
done = Bool
True, pterm :: ProofTerm
pterm = Term -> ProofTerm
mkProofTerm Term
tm' },
                                            String
"Proof complete: " forall a. [a] -> [a] -> [a]
++ forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv [] Term
tm')
                           [Name]
_  -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Still holes to fill."
processTactic Tactic
ProofState ProofState
ps = forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps, forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv [] (ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps)))
processTactic Tactic
Undo ProofState
ps = case ProofState -> Maybe ProofState
previous ProofState
ps of
                            Maybe ProofState
Nothing -> forall a. Err -> TC a
Error forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Nothing to undo."
                            Just ProofState
pold -> forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
pold, String
"")
processTactic Tactic
EndUnify ProofState
ps
    = let (Name
h, [(Name, Term)]
ns_in) = ProofState -> (Name, [(Name, Term)])
unified ProofState
ps
          ns :: [(Name, Term)]
ns = forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (ProofState -> [Name]
dontunify ProofState
ps) [(Name, Term)]
ns_in (ProofState -> [Name]
holes ProofState
ps)
          ns' :: [(Name, Term)]
ns' = forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
t) -> (Name
n, [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
t)) [(Name, Term)]
ns
          ([(Name, Term)]
ns'', Fails
probs') = ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems ProofState
ps [(Name, Term)]
ns' (ProofState -> Fails
problems ProofState
ps)
          tm' :: ProofTerm
tm' = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)]
ns'' (ProofState -> ProofTerm
pterm ProofState
ps) in
             forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"(EndUnify) Dropping holes: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns'')) forall a b. (a -> b) -> a -> b
$
              forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps { pterm :: ProofTerm
pterm = ProofTerm
tm',
                           unified :: (Name, [(Name, Term)])
unified = (Name
h, []),
                           problems :: Fails
problems = Fails
probs',
                           notunified :: [(Name, Term)]
notunified = forall {a}. [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [(Name, Term)]
ns'' (ProofState -> [(Name, Term)]
notunified ProofState
ps),
                           recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns'',
                           holes :: [Name]
holes = ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns'' }, String
"")
processTactic Tactic
UnifyAll ProofState
ps
    = let tm' :: ProofTerm
tm' = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved (ProofState -> [(Name, Term)]
notunified ProofState
ps) (ProofState -> ProofTerm
pterm ProofState
ps) in
          forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps { pterm :: ProofTerm
pterm = ProofTerm
tm',
                       notunified :: [(Name, Term)]
notunified = [],
                       recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (ProofState -> [(Name, Term)]
notunified ProofState
ps),
                       holes :: [Name]
holes = ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (ProofState -> [(Name, Term)]
notunified ProofState
ps) }, String
"")
processTactic (Reorder Name
n) ProofState
ps
    = do ProofState
ps' <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Maybe Name -> RunTactic -> StateT ProofState TC ()
tactic (forall a. a -> Maybe a
Just Name
n) RunTactic
reorder_claims) ProofState
ps
         forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps' { previous :: Maybe ProofState
previous = forall a. a -> Maybe a
Just ProofState
ps, plog :: String
plog = String
"" }, ProofState -> String
plog ProofState
ps')
processTactic (ComputeLet Name
n) ProofState
ps
    = forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps { pterm :: ProofTerm
pterm = Term -> ProofTerm
mkProofTerm forall a b. (a -> b) -> a -> b
$
                              Context -> Name -> Term -> Term
computeLet (ProofState -> Context
context ProofState
ps) Name
n
                                         (ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps)) }, String
"")
processTactic Tactic
UnifyProblems ProofState
ps
    = do let ([(Name, Term)]
ns', Fails
probs') = ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems ProofState
ps [] (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d} {e} {f} {g}.
(a, b, c, d, e, f, g) -> (a, b, Bool, d, e, f, g)
setReady (ProofState -> Fails
problems ProofState
ps))
             (ProofTerm
pterm', [Name]
dropped) = [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved [(Name, Term)]
ns' (ProofState -> ProofTerm
pterm ProofState
ps)
         forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"(UnifyProblems) Dropping holes: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
dropped) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps { pterm :: ProofTerm
pterm = ProofTerm
pterm', solved :: Maybe (Name, Term)
solved = forall a. Maybe a
Nothing, problems :: Fails
problems = Fails
probs',
                       previous :: Maybe ProofState
previous = forall a. a -> Maybe a
Just ProofState
ps, plog :: String
plog = String
"",
                       notunified :: [(Name, Term)]
notunified = forall {a}. [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [(Name, Term)]
ns' (ProofState -> [(Name, Term)]
notunified ProofState
ps),
                       recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps forall a. [a] -> [a] -> [a]
++ [Name]
dropped,
                       dotted :: [(Name, [Name])]
dotted = forall a. (a -> Bool) -> [a] -> [a]
filter (forall {a} {b} {b}. Eq a => [(a, b)] -> (a, b) -> Bool
notIn [(Name, Term)]
ns') (ProofState -> [(Name, [Name])]
dotted ProofState
ps),
                       holes :: [Name]
holes = ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
dropped }, ProofState -> String
plog ProofState
ps)
   where notIn :: [(a, b)] -> (a, b) -> Bool
notIn [(a, b)]
ns (a
h, b
_) = a
h forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(a, b)]
ns
processTactic (MatchProblems Bool
all) ProofState
ps
    = do let ([(Name, Term)]
ns', Fails
probs') = Bool
-> ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all ProofState
ps [] (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d} {e} {f} {g}.
(a, b, c, d, e, f, g) -> (a, b, Bool, d, e, f, g)
setReady (ProofState -> Fails
problems ProofState
ps))
             ([(Name, Term)]
ns'', Fails
probs'') = Bool
-> ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all ProofState
ps [(Name, Term)]
ns' Fails
probs'
             (ProofTerm
pterm', [Name]
dropped) = [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved [(Name, Term)]
ns'' (ProofTerm -> ProofTerm
resetProofTerm (ProofState -> ProofTerm
pterm ProofState
ps))
         forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"(MatchProblems) Dropping holes: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
dropped) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps { pterm :: ProofTerm
pterm = ProofTerm
pterm', solved :: Maybe (Name, Term)
solved = forall a. Maybe a
Nothing, problems :: Fails
problems = Fails
probs'',
                       previous :: Maybe ProofState
previous = forall a. a -> Maybe a
Just ProofState
ps, plog :: String
plog = String
"",
                       notunified :: [(Name, Term)]
notunified = forall {a}. [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [(Name, Term)]
ns'' (ProofState -> [(Name, Term)]
notunified ProofState
ps),
                       recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps forall a. [a] -> [a] -> [a]
++ [Name]
dropped,
                       holes :: [Name]
holes = ProofState -> [Name]
holes ProofState
ps forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
dropped }, ProofState -> String
plog ProofState
ps)
processTactic Tactic
t ProofState
ps
    = case ProofState -> [Name]
holes ProofState
ps of
        [] -> case Tactic
t of
                   Focus Name
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps, String
"") -- harmless to refocus when done, since
                                              -- 'focus' doesn't fail
                   Tactic
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Proof done, nothing to run tactic on: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Tactic
t forall a. [a] -> [a] -> [a]
++
                              String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps))
        (Name
h:[Name]
_)  -> do ProofState
ps' <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Tactic -> Name -> StateT ProofState TC ()
process Tactic
t Name
h) ProofState
ps
                     let ([(Name, Term)]
ns_in, Fails
probs')
                                = case ProofState -> Maybe (Name, Term)
solved ProofState
ps' of
                                    Just (Name, Term)
s -> forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                                                (String
"SOLVED " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name, Term)
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [Name]
dontunify ProofState
ps')) forall a b. (a -> b) -> a -> b
$
                                                ProofState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems ProofState
ps' [(Name, Term)
s] (ProofState -> Fails
problems ProofState
ps')
                                    Maybe (Name, Term)
_ -> ([], ProofState -> Fails
problems ProofState
ps')
                     -- rechecking problems may find more solutions, so
                     -- apply them here
                     let ns' :: [(Name, Term)]
ns' = forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (ProofState -> [Name]
dontunify ProofState
ps') [(Name, Term)]
ns_in (ProofState -> [Name]
holes ProofState
ps')
                     let pterm'' :: ProofTerm
pterm'' = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)]
ns' (ProofState -> ProofTerm
pterm ProofState
ps')
                     forall {a}. Bool -> String -> a -> a
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                                 (String
"Updated problems after solve " forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow Fails
probs' forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
                                  String
"(Toplevel) Dropping holes: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns') forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
                                  String
"Holes were: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ProofState -> [Name]
holes ProofState
ps')) forall a b. (a -> b) -> a -> b
$
                       forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState
ps' { pterm :: ProofTerm
pterm = ProofTerm
pterm'',
                                     solved :: Maybe (Name, Term)
solved = forall a. Maybe a
Nothing,
                                     problems :: Fails
problems = Fails
probs',
                                     notunified :: [(Name, Term)]
notunified = forall {a}. [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [(Name, Term)]
ns' (ProofState -> [(Name, Term)]
notunified ProofState
ps'),
                                     previous :: Maybe ProofState
previous = forall a. a -> Maybe a
Just ProofState
ps, plog :: String
plog = String
"",
                                     recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps' forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns',
                                     holes :: [Name]
holes = ProofState -> [Name]
holes ProofState
ps' forall a. Eq a => [a] -> [a] -> [a]
\\ (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns')
                                   }, ProofState -> String
plog ProofState
ps')

process :: Tactic -> Name -> StateT TState TC ()
process :: Tactic -> Name -> StateT ProofState TC ()
process Tactic
EndUnify Name
_
   = do ProofState
ps <- forall s (m :: * -> *). MonadState s m => m s
get
        let (Name
h, [(Name, Term)]
_) = ProofState -> (Name, [(Name, Term)])
unified ProofState
ps
        Maybe Name -> RunTactic -> StateT ProofState TC ()
tactic (forall a. a -> Maybe a
Just Name
h) RunTactic
solve_unified
process Tactic
t Name
h = Maybe Name -> RunTactic -> StateT ProofState TC ()
tactic (forall a. a -> Maybe a
Just Name
h) (Tactic -> RunTactic
mktac Tactic
t)
   where mktac :: Tactic -> RunTactic
mktac Tactic
Attack            = RunTactic
attack
         mktac (Claim Name
n Raw
r)       = Name -> Raw -> RunTactic
claim Name
n Raw
r
         mktac (ClaimFn Name
n Name
bn Raw
r)  = Name -> Name -> Raw -> RunTactic
claimFn Name
n Name
bn Raw
r
         mktac (Exact Raw
r)         = Raw -> RunTactic
exact Raw
r
         mktac (Fill Raw
r)          = Raw -> RunTactic
fill Raw
r
         mktac (MatchFill Raw
r)     = Raw -> RunTactic
match_fill Raw
r
         mktac (PrepFill Name
n [Name]
ns)   = Name -> [Name] -> RunTactic
prep_fill Name
n [Name]
ns
         mktac Tactic
CompleteFill      = RunTactic
complete_fill
         mktac Tactic
Solve             = RunTactic
solve
         mktac (StartUnify Name
n)    = Name -> RunTactic
start_unify Name
n
         mktac Tactic
Compute           = RunTactic
compute
         mktac Tactic
Simplify          = RunTactic
Idris.Core.ProofState.simplify
         mktac Tactic
WHNF_Compute      = RunTactic
whnf_compute
         mktac Tactic
WHNF_ComputeArgs  = RunTactic
whnf_compute_args
         mktac (Intro Maybe Name
n)         = Maybe Name -> RunTactic
intro Maybe Name
n
         mktac (IntroTy Raw
ty Maybe Name
n)    = Raw -> Maybe Name -> RunTactic
introTy Raw
ty Maybe Name
n
         mktac (Forall Name
n RigCount
r Maybe ImplicitInfo
i Raw
t)  = Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
forAll Name
n RigCount
r Maybe ImplicitInfo
i Raw
t
         mktac (LetBind Name
n RigCount
r Raw
t Raw
v) = Name -> RigCount -> Raw -> Raw -> RunTactic
letbind Name
n RigCount
r Raw
t Raw
v
         mktac (ExpandLet Name
n Term
b)   = Name -> Term -> RunTactic
expandLet Name
n Term
b
         mktac (Rewrite Raw
t)       = Raw -> RunTactic
rewrite Raw
t
         mktac (Equiv Raw
t)         = Raw -> RunTactic
equiv Raw
t
         mktac (PatVar Name
n)        = Name -> RunTactic
patvar Name
n
         mktac (PatBind Name
n RigCount
rig)   = Name -> RigCount -> RunTactic
patbind Name
n RigCount
rig
         mktac (CheckIn Raw
r)       = Raw -> RunTactic
check_in Raw
r
         mktac (EvalIn Raw
r)        = Raw -> RunTactic
eval_in Raw
r
         mktac (Focus Name
n)         = Name -> RunTactic
focus Name
n
         mktac (Defer [Name]
ns [Name]
ls Name
n)   = [Name] -> [Name] -> Name -> RunTactic
defer [Name]
ns [Name]
ls Name
n
         mktac (DeferType Name
n Raw
t [Name]
a) = Name -> Raw -> [Name] -> RunTactic
deferType Name
n Raw
t [Name]
a
         mktac (Implementation Name
n)= Name -> RunTactic
implementationArg Name
n
         mktac (AutoArg Name
n)       = Name -> RunTactic
autoArg Name
n
         mktac (SetInjective Name
n)  = Name -> RunTactic
setinj Name
n
         mktac (MoveLast Name
n)      = Name -> RunTactic
movelast Name
n
         mktac (UnifyGoal Raw
r)     = Raw -> RunTactic
unifyGoal Raw
r
         mktac (UnifyTerms Raw
x Raw
y)  = Raw -> Raw -> RunTactic
unifyTerms Raw
x Raw
y