{-|
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
import Control.Monad.State.Strict
import Data.List

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

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

-- Some utilites on proof and tactic states

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

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

      prettyPs :: Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [] = Doc OutputAnnotation
forall a. Doc a
empty
      prettyPs Env
env ((a
n, b
_, Let RigCount
_ Term
t Term
v):[(a, b, Binder Term)]
bs) =
        Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (a -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty a
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
        Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env Term
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env Term
v Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
        Int -> Doc OutputAnnotation -> Doc OutputAnnotation
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) =
        Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (a -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty a
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
        Int -> Doc OutputAnnotation -> Doc OutputAnnotation
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 = [(FailAt, [Name], Term, Term, Bool)] -> String
forall a. Show a => a -> String
show (((Term, Term, Bool, Env, Err, [FailContext], FailAt)
 -> (FailAt, [Name], Term, Term, Bool))
-> Fails -> [(FailAt, [Name], Term, Term, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Term
x, Term
y, Bool
hs, Env
env, Err
_, [FailContext]
_, FailAt
t) -> (FailAt
t, ((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
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 TState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) =
   do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
      let while :: [FailContext]
while = TState -> [FailContext]
while_elaborating TState
ps
      let inj :: [Name]
inj = TState -> [Name]
injective TState
ps
      Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
                (String
"Matching " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
topx, Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
forall a. Show a => a -> String
show Env
env String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 String
"\nHoles: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
holes TState
ps)
                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
                 ) (StateT TState TC [(Name, Term)]
 -> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
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 (TState -> [Name]
holes TState
ps) [FailContext]
while of
            OK [(Name, Term)]
u -> Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
                        (String
"Matched " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show [(Name, Term)]
u) (StateT TState TC [(Name, Term)]
 -> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
                     do let (Name
h, [(Name, Term)]
ns) = TState -> (Name, [(Name, Term)])
unified TState
ps
                        TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { unified = (h, u ++ ns) })
                        [(Name, Term)] -> StateT TState TC [(Name, Term)]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Term)]
u
            Error Err
e -> Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
                         (String
"No match " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e) (StateT TState TC [(Name, Term)]
 -> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
                        do TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { problems = (topx, topy, True,
                                                 env, e, while, Match) :
                                                 problems ps })
                           [(Name, Term)] -> StateT TState TC [(Name, Term)]
forall a. a -> StateT TState TC a
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 TState TC [(Name, Term)]
mergeSolutions Env
env [(Name, Term)]
ns = [(Name, Term)] -> [(Name, Term)] -> StateT TState TC [(Name, Term)]
forall {m :: * -> *} {a}.
(Eq a, MonadState TState 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 [] = [(a, Term)] -> m [(a, Term)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, Term)] -> [(a, Term)]
forall a. [a] -> [a]
reverse [(a, Term)]
acc)
    merge [(a, Term)]
acc ((a
n, Term
t) : [(a, Term)]
ns)
          | Just Term
t' <- a -> [(a, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Term)]
ns
              = do TState
ps <- m TState
forall s (m :: * -> *). MonadState s m => m s
get
                   let probs :: Fails
probs = TState -> Fails
problems TState
ps
                   TState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { problems = probs ++ [(t,t',True,env,
                                                    CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
                                                     [], 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)(a, Term) -> [(a, Term)] -> [(a, Term)]
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) | Name -> Name -> [(Name, Term)] -> Bool
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 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y' Bool -> Bool -> Bool
&& t
x t -> t -> Bool
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 (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) =
   do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
      let while :: [FailContext]
while = TState -> [FailContext]
while_elaborating TState
ps
      let dont :: [Name]
dont = TState -> [Name]
dontunify TState
ps
      let inj :: [Name]
inj = TState -> [Name]
injective TState
ps
      ([(Name, Term)]
u, Fails
fails) <- Bool
-> String
-> StateT TState TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
                        (String
"Trying " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
topx, Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                         String
"\nNormalised " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
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) String -> ShowS
forall a. [a] -> [a] -> [a]
++
                         String
" in\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
forall a. Show a => a -> String
show Env
env String -> ShowS
forall a. [a] -> [a] -> [a]
++
                         String
"\nHoles: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
holes TState
ps)
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nInjective: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
injective TState
ps)
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") (StateT TState TC ([(Name, Term)], Fails)
 -> StateT TState TC ([(Name, Term)], Fails))
-> StateT TState TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall a b. (a -> b) -> a -> b
$
                     TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC ([(Name, Term)], Fails)
 -> StateT TState TC ([(Name, Term)], Fails))
-> TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
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 (TState -> [Name]
holes TState
ps)
                                  (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst (TState -> [(Name, Term)]
notunified TState
ps)) [FailContext]
while
      let notu :: [(Name, Term)]
notu = ((Name, Term) -> Bool) -> [(Name, Term)] -> [(Name, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n, Term
t) -> case Term
t of
--                                         P _ _ _ -> False
                                        Term
_ -> Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
dont) [(Name, Term)]
u
      Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
            (String
"Unified " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
topx, Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" without " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
dont String -> ShowS
forall a. [a] -> [a] -> [a]
++
             String
"\nSolved: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show [(Name, Term)]
u String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nNew problems: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow Fails
fails
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nNot unified:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show (TState -> [(Name, Term)]
notunified TState
ps)
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nCurrent problems:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow (TState -> Fails
problems TState
ps)
--              ++ show (pterm ps)
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n----------") (StateT TState TC [(Name, Term)]
 -> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
        do let (Name
h, [(Name, Term)]
ns) = TState -> (Name, [(Name, Term)])
unified TState
ps
           -- solve in results (maybe unify should do this itself...)
           let u' :: [(Name, Term)]
u' = ((Name, Term) -> (Name, Term)) -> [(Name, Term)] -> [(Name, Term)]
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 TState TC [(Name, Term)]
mergeSolutions Env
env ([(Name, Term)]
u' [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
ns)
           TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
           let ([(Name, Term)]
ns_p, Fails
probs') = TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps [(Name, Term)]
uns (Fails
fails Fails -> Fails -> Fails
forall a. [a] -> [a] -> [a]
++ TState -> Fails
problems TState
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 (TState -> [Name]
holes TState
ps) ([(Name, Term)]
notu [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ TState -> [(Name, Term)]
notunified TState
ps)
           Bool -> String -> StateT TState TC () -> StateT TState TC ()
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
            (String
"Now solved: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show [(Name, Term)]
ns' String -> ShowS
forall a. [a] -> [a] -> [a]
++
             String
"\nNow problems: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow (Fails
probs' Fails -> Fails -> Fails
forall a. [a] -> [a] -> [a]
++ Fails
probs_notu) String -> ShowS
forall a. [a] -> [a] -> [a]
++
             String
"\nNow injective: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show ([(Name, Term)] -> [Name] -> [Name]
forall {a}. Eq a => [(a, TT a)] -> [a] -> [a]
updateInj [(Name, Term)]
u (TState -> [Name]
injective TState
ps))) (StateT TState TC () -> StateT TState TC ())
-> StateT TState TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$
             TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { problems = probs' ++ probs_notu,
                       unified = (h, ns'),
                       injective = updateInj u (injective ps),
                       notunified = notu' })
           [(Name, Term)] -> StateT TState TC [(Name, Term)]
forall a. a -> StateT TState TC a
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]
_) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
a,
                a
n a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
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'a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
inj)
              | (P NameType
_ a
n' TT a
_, [TT a]
_) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
a,
                a
n' a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
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
na -> [a] -> [a]
forall 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 -> TState -> TState
nowElaboratingPS FC
fc Name
f Name
arg TState
ps = TState
ps { while_elaborating = FailContext fc f arg : while_elaborating 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 = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
p [a]
xs

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

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

getName :: Monad m => String -> StateT TState m Name
getName :: forall (m :: * -> *). Monad m => String -> StateT TState m Name
getName String
tag = do TState
ps <- StateT TState m TState
forall s (m :: * -> *). MonadState s m => m s
get
                 let n :: Int
n = TState -> Int
nextname TState
ps
                 TState -> StateT TState m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { nextname = n+1 })
                 Name -> StateT TState m Name
forall a. a -> StateT TState m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> StateT TState m Name) -> Name -> StateT TState m Name
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 =>
(TState -> TState) -> StateT TState m ()
action TState -> TState
a = do TState
ps <- StateT TState m TState
forall s (m :: * -> *). MonadState s m => m s
get
              TState -> StateT TState m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState -> TState
a TState
ps)

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

addLog :: Monad m => String -> StateT TState m ()
addLog :: forall (m :: * -> *). Monad m => String -> StateT TState m ()
addLog String
str = (TState -> TState) -> StateT TState m ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { plog = plog ps ++ str ++ "\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 -> TState
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' = Term -> Term
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 TState
-> Context
-> Ctxt TypeInfo
-> String
-> Bool
-> Bool
-> [Name]
-> [FailContext]
-> String
-> TState
PS Name
n [Name
h] [] Int
1 Int
globalNames (Term -> ProofTerm
mkProofTerm (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (Term -> Binder Term
forall b. b -> Binder b
Hole Term
ty')
        (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Term
ty'))) Term
ty [] (Name
h, []) [] []
        Maybe (Name, Term)
forall a. Maybe a
Nothing [] []
        [] [] [] []
        Maybe TState
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 :: TState -> TC Env
envAtFocus TState
ps
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TState -> [Name]
holes TState
ps) = do Goal
g <- Maybe Name -> ProofTerm -> TC Goal
goal (Name -> Maybe Name
forall a. a -> Maybe a
Just ([Name] -> Name
forall a. HasCallStack => [a] -> a
head (TState -> [Name]
holes TState
ps))) (TState -> ProofTerm
pterm TState
ps)
                                 Env -> TC Env
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Env
premises Goal
g)
    | Bool
otherwise = String -> TC Env
forall a. String -> TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> TC Env) -> String -> TC Env
forall a b. (a -> b) -> a -> b
$ String
"No holes in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps))

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

tactic :: Hole -> RunTactic -> StateT TState TC ()
tactic :: Maybe Name -> RunTactic -> StateT TState TC ()
tactic Maybe Name
h RunTactic
f = do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
                (ProofTerm
tm', Bool
_) <- Maybe Name
-> RunTactic
-> Context
-> Env
-> ProofTerm
-> StateT TState TC (ProofTerm, Bool)
forall a.
Maybe Name
-> RunTactic' a
-> Context
-> Env
-> ProofTerm
-> StateT a TC (ProofTerm, Bool)
atHole Maybe Name
h RunTactic
f (TState -> Context
context TState
ps) [] (TState -> ProofTerm
pterm TState
ps)
                TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get -- might have changed while processing
                TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { pterm = 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' Name -> Name -> Bool
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
                       Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' (RigCount -> Term -> Term -> Binder Term
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) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> Term -> Term
cl Env
env) Binder Term
b) (Env -> Term -> Term
cl ((Name
n, RigCount
Rig0, Binder Term
b)(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
sc)
   cl Env
env (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
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 <- String -> StateT TState TC Name
forall (m :: * -> *). Monad m => String -> StateT TState m Name
getName String
"hole"
         (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = h : holes ps })
         Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
t (Name -> Term
newtm Name
h)) Term
sc
  where
    newtm :: Name -> Term
newtm Name
h = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Term
t)
attack Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
       TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
       (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let (Name
g:[Name]
gs) = TState -> [Name]
holes TState
ps in
                          TState
ps { holes = g : n : gs } )
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Term -> Binder Term
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
argty
       TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
       (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let (Name
g:[Name]
gs) = TState -> [Name]
holes TState
ps in
                          TState
ps { holes = g : n : gs } )
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Term -> Binder Term
forall b. b -> Binder b
Hole (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
bn (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing Term
tyv Term
tyt) Term
retty)) Term
t
claimFn Name
_ Name
_ Raw
_ Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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) = Term -> [(Name, Binder Term)] -> ([(Name, Binder Term)], Term)
forall {a}.
TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs Term
t []
          newbs :: [(Name, Binder Term)]
newbs = [(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse ([(Name, Binder Term)] -> [(Name, Binder Term)]
sortB ([(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse [(Name, Binder Term)]
bs)) in
          Bool -> String -> StateT TState TC Term -> StateT TState TC Term
forall {a}. Bool -> String -> a -> a
traceWhen ([(Name, Binder Term)]
bs [(Name, Binder Term)] -> [(Name, Binder Term)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [(Name, Binder Term)]
newbs) ([(Name, Binder Term)] -> String
forall a. Show a => a -> String
show [(Name, Binder Term)]
bs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n ==> \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Binder Term)] -> String
forall a. Show a => a -> String
show [(Name, Binder Term)]
newbs) (StateT TState TC Term -> StateT TState TC Term)
-> StateT TState TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$
            Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Binder Term)] -> Term -> Term
forall n. [(n, Binder (TT n))] -> TT n -> TT n
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)(a, Binder (TT a)) -> [(a, Binder (TT a))] -> [(a, Binder (TT a))]
forall a. a -> [a] -> [a]
:[(a, Binder (TT a))]
acc)
        scvs TT a
sc [(a, Binder (TT a))]
acc = ([(a, Binder (TT a))] -> [(a, Binder (TT a))]
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) | ((Name, Binder Term) -> Bool) -> [(Name, Binder Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Name, Binder Term) -> (Name, Binder Term) -> Bool
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 (Name, Binder Term)
-> [(Name, Binder Term)] -> [(Name, Binder Term)]
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 ((Name, Binder Term)
-> [(Name, Binder Term)] -> [(Name, Binder Term)]
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) | ((n, Binder (TT n)) -> Bool) -> [(n, Binder (TT n))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((n, Binder (TT n)) -> (n, Binder (TT n)) -> Bool
forall {n} {b} {a}. Eq n => (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (n, Binder (TT n))
x) ((n, Binder (TT n))
y(n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
:[(n, Binder (TT n))]
ys) = (n, Binder (TT n))
x (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
: (n, Binder (TT n))
y (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
: [(n, Binder (TT n))]
ys
                         | Bool
otherwise = (n, Binder (TT n))
y (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
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) = n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
t Bool -> Bool -> Bool
&& n -> TT n -> 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) = n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
t Bool -> Bool -> Bool
&& n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
v
        noOcc (n
n, b
_) (a
_, Binder (TT n)
b) = n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n (Binder (TT n) -> TT 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 (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
                                            if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
                                               then TState
ps { holes = n : (hs \\ [n]) }
                                               else TState
ps)
                        TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
                        Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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 (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
                                              if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
                                                  then TState
ps { holes = (hs \\ [n]) ++ [n] }
                                                  else TState
ps)
                           Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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 (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps
                            is :: [Name]
is = TState -> [Name]
implementations TState
ps in
                            TState
ps { holes = (hs \\ [x]) ++ [x],
                                 implementations = x:is })
         Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) Term
sc)
implementationArg Name
n Context
ctxt Env
env Term
_
    = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> case Name
-> [(Name, ([FailContext], [Name]))]
-> Maybe ([FailContext], [Name])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (TState -> [(Name, ([FailContext], [Name]))]
autos TState
ps) of
                             Maybe ([FailContext], [Name])
Nothing ->
                               let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
                               TState
ps { holes = (hs \\ [x]) ++ [x],
                                    autos = (x, (while_elaborating ps, refsIn t)) : autos ps }
                             Just ([FailContext], [Name])
_ -> TState
ps)
         Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) Term
sc)
autoArg Name
n Context
ctxt Env
env Term
_
    = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let is :: [Name]
is = TState -> [Name]
injective TState
ps in
                            TState
ps { injective = n : is })
         Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let env' :: Env
env' = ((Name, RigCount, Binder Term) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, RigCount
_, Binder Term
t) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
dropped) Env
env
       (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
                          TState
ps { usedns = n : usedns ps,
                               holes = hs \\ [x] })
       TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Int -> [Name] -> Term -> Binder Term
forall b. Int -> [Name] -> b -> Binder b
GHole (Env -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
env') (TState -> [Name]
psnames TState
ps) (Env -> Term -> Term
mkTy (Env -> Env
forall a. [a] -> [a]
reverse Env
env') Term
t))
                      (Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty) (((Name, RigCount, Binder Term) -> Term) -> Env -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Term
forall {n} {b}. (n, b, Binder (TT n)) -> TT n
getP (Env -> Env
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 = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi (RigCount -> Name -> RigCount
setRig RigCount
rig Name
n) Maybe ImplicitInfo
forall a. Maybe a
Nothing (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) (UExp -> Term
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
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) = NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
b)
defer [Name]
dropped [Name]
linused Name
n Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
fty, Term
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
fty_in
       (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps
                          ds :: [Name]
ds = TState -> [Name]
deferred TState
ps in
                          TState
ps { holes = hs \\ [x],
                               deferred = n : ds })
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Int -> [Name] -> Term -> Binder Term
forall b. Int -> [Name] -> b -> Binder b
GHole Int
0 [] Term
fty)
                      (Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty) ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Term
getP [Name]
args)))
  where
    getP :: Name -> Term
getP Name
n = case Name -> Env -> Maybe (Binder Term)
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
env of
                  Just Binder Term
b -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
                  Maybe (Binder Term)
Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String
"deferType can't find " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n)
deferType Name
_ Raw
_ [Name]
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b, Maybe Provenance
forall a. Maybe a
Nothing) (Term
tmv, Maybe Provenance
forall a. Maybe a
Nothing)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
h
unifyGoal Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm1
       (Term
tm2v, Term
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
tm1v, Maybe Provenance
forall a. Maybe a
Nothing) (Term
tm2v, Maybe Provenance
forall a. Maybe a
Nothing)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
       TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
valty Term
ty
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
exact Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val)
                       (Term
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Term -> Term -> Provenance
chkPurpose Term
val Term
ty))
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
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
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 TState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val)
                             (Term
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
ExpectedType)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
match_fill Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
f Term
forall n. TT n
Erased) ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
as)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
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 = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT TState TC Term)
-> String -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ String
"Can't prepare fill at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val')
                       (Term
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
ExpectedType)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
complete_fill Context
ctxt Env
env Term
t = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT TState TC Term)
-> String -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ String
"Can't complete fill at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
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 TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
        [Name]
dropdots <-
             case Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (TState -> [(Name, Term)]
notunified TState
ps) of
                Just (P NameType
_ Name
h Term
_)
                     | Name
h Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x -> [Name] -> StateT TState TC [Name]
forall a. a -> StateT TState TC a
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 TState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
tm, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
InferredVal)
                                                     (Term
val, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
GivenVal)
                               [Name] -> StateT TState TC [Name]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name
x]
                Maybe Term
_ -> [Name] -> StateT TState TC [Name]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
                                       holes ps \\ [x],
                            solved = Just (x, val),
                            dontunify = filter (/= x) (dontunify ps),
                            notunified = updateNotunified [(x,val)]
                                           (notunified ps),
                            recents = x : recents ps,
                            implementations = implementations ps \\ [x],
                            dotted = dropUnified dropdots (dotted ps) })
        let (Term
locked, Bool
_) = [Name] -> Term -> (Term, Bool)
tryLock (TState -> [Name]
holes TState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x Term
val Term
sc) in
            Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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 a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ddots Bool -> Bool -> Bool
|| (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\a
e -> a
e a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
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) (a, t a) -> [(a, t a)] -> [(a, t a)]
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 (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Term
f' Term
a', Bool
True)
                             else (AppStatus Name -> Term -> Term -> Term
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
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
                  (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Term -> Binder Term
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 (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
                  (Term
sc', Bool
scl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
sc in
                  (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Binder Term
b { binderTy = 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 TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
        case Name -> Term -> Maybe Name
forall {a}. Eq a => a -> TT a -> Maybe a
findType Name
x Term
sc of
             Just Name
t -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
CantInferType (Name -> String
forall a. Show a => a -> String
show Name
t))
             Maybe Name
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Term -> Err
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 Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
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
_ <- Binder (TT a) -> TT a
forall b. Binder b -> b
binderTy Binder (TT a)
t, a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' = a -> Maybe a
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
_ = Maybe 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 Name -> Name -> Bool
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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' = Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (NameType -> Name -> Term -> Term
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
s, Maybe Provenance
forall a. Maybe a
Nothing) (Term
tyv, Maybe Provenance
forall a. Maybe a
Nothing)
                                           Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
tyv) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t') (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
           Term
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Err -> TC Term) -> Err -> TC Term
forall a b. (a -> b) -> a -> b
$ Term -> Err
forall t. t -> Err' t
CantIntroduce Term
t'
introTy Raw
ty Maybe Name
n Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 Name -> Name -> Bool
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' = Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
y (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t
               in Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
s) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t') (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
           Term
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Err -> TC Term) -> Err -> TC Term
forall a b. (a -> b) -> a -> b
$ Term -> Err
forall t. t -> Err' t
CantIntroduce Term
t'
intro Maybe Name
n Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
tyv, Term
tyt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
tyt, Maybe Provenance
forall a. Maybe a
Nothing) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), Maybe Provenance
forall a. Maybe a
Nothing)
       Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
t, Maybe Provenance
forall a. Maybe a
Nothing) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), Maybe Provenance
forall a. Maybe a
Nothing)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
impl Term
tyv (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) (NameType -> Name -> Term -> Term
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
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
                                     holes ps \\ [x],
                           solved = Just (x, P Bound n t),
                           dontunify = filter (/=x) (dontunify ps),
                           notunified = updateNotunified [(x,P Bound n t)]
                                          (notunified ps),
                           injective = addInj n x (injective ps)
                         })
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
PVar RigCount
RigW Term
t) (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x (NameType -> Name -> Term -> Term
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 a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ps = a
n a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ps
                      | Bool
otherwise = [a]
ps
patvar Name
n Context
ctxt Env
env Term
tm = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT TState TC Term)
-> String -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ String
"Can't add pattern var at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
tyv,  Term
tyt)  <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
       (Term
valv, Term
valt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
val
       TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Term
tyv Term
valv) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) (NameType -> Name -> Term -> Term
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
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 =
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Term -> Term
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Term
tmv, Term
tmt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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 Term -> (Term, [Term])
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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"=" ->
            do let p :: Term
p = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
rname (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW Term
lt) (Term -> Term -> Term -> Term -> Term
mkP (NameType -> Name -> Term -> Term
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 (Term -> Raw) -> Term -> Raw
forall a b. (a -> b) -> a -> b
$ (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
newt)
                                       (Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"replace") (UExp -> Term
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
sc
               Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
scv
         (Term, [Term])
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Term -> Term -> Err
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
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 Term -> Term -> Bool
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 Term -> Term -> Bool
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 Term -> Term -> Bool
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
                             AppStatus Name -> Term -> Term -> Term
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 Term -> Term -> Bool
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
                           Name -> Binder Term -> Term -> Term
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 Term -> Term -> Bool
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 Term -> Term -> Bool
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
                                 RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c Term
t' Term
v'
          mkPB Binder Term
b = let ty :: Term
ty = Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b
                       ty' :: Term
ty' = if (Term
r Term -> Term -> Bool
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 = 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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
       TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
tmv Term
t
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
tmv) Term
sc
equiv Raw
tm Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 Name -> Name -> Bool
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' = Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t in
                                    Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
PVar RigCount
rig Term
s) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t') (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
           Term
_ -> String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Nothing to pattern bind"
patbind Name
n RigCount
_ Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
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 Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
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 = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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
           Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
ty') Term
sc
whnf_compute Context
ctxt Env
env Term
t = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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
           Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
ty') Term
sc
whnf_compute_args Context
ctxt Env
env Term
t = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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 Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole ((Term, [(Name, Int)]) -> Term
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 = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
t
       String -> StateT TState TC ()
forall (m :: * -> *). Monad m => String -> StateT TState m ()
addLog (Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty)
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
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
       String -> StateT TState TC ()
forall (m :: * -> *). Monad m => String -> StateT TState m ()
addLog (Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++
               Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty String -> ShowS
forall a. [a] -> [a] -> [a]
++
--                     " in " ++ show env ++
               String
" ==>\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++
               Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++
               Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty')
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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, []) })
                               Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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 TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
       let (Name
_, [(Name, Term)]
ns) = TState -> (Name, [(Name, Term)])
unified TState
ps
       let unify :: [(Name, Term)]
unify = [Name] -> [(Name, Term)] -> [Name] -> [(Name, Term)]
forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (TState -> [Name]
dontunify TState
ps) [(Name, Term)]
ns (TState -> [Name]
holes TState
ps)
       (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
                                     holes ps \\ map fst unify,
                           recents = recents ps ++ map fst unify })
       (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { pterm = updateSolved unify (pterm ps) })
       Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
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 a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du Bool -> Bool -> Bool
&& Bool -> Bool
not (a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
     Bool -> Bool -> Bool
&& a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs
            = (a
t, NameType -> a -> TT a -> TT a
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound a
n TT a
ty) (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
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 a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
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 (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
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 a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du Bool -> Bool -> Bool
&& Bool -> Bool
not (a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
     Bool -> Bool -> Bool
&& a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
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 a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du = (a, TT a)
u (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
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, (Term -> Term) -> f Term -> f Term
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns) f Term
b) (a, b, f Term) -> [(a, b, f Term)] -> [(a, b, f Term)]
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 (Term -> Provenance) -> Term -> Provenance
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) = FC -> Err -> Err
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) = String -> Name -> Maybe Term -> Err -> Err
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)
 = Name -> Name -> [(Name, Name)] -> Err -> Err
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)
 = Bool
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> Err
-> [(Name, Term)]
-> Int
-> Err
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, (Provenance -> Provenance) -> Maybe Provenance -> Maybe Provenance
forall a b. (a -> b) -> Maybe a -> Maybe b
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, (Provenance -> Provenance) -> Maybe Provenance -> Maybe Provenance
forall a b. (a -> b) -> Maybe a -> Maybe b
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 = [(Name, Term)]
-> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
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 = ([(a, t)] -> [(a, t)]
forall a. [a] -> [a]
reverse [(a, t)]
ns_acc, [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
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' <- a -> [(a, t)] -> Maybe t
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, t)]
ns, t
t t -> t -> Bool
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') (a, t) -> [(a, t)] -> [(a, t)]
forall a. a -> [a] -> [a]
: [(a, t)]
ns_acc)
                      ((t
t,t
t',Bool
True, Env
env,Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
True (t
t, Maybe Provenance
forall a. Maybe a
Nothing) (t
t', Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' t
forall t. String -> Err' t
Msg String
"") [] Int
0, [],FailAt
Match) (t, t, Bool, Env, Err' t, [a], FailAt)
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
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) (a, t) -> [(a, t)] -> [(a, 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 = [(a, Term)] -> [(a, Term)]
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') (a, Term) -> [(a, Term)] -> [(a, Term)]
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
_ = (Maybe Provenance
forall a. Maybe a
Nothing, Maybe Provenance
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 :: TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps [(Name, Term)]
updates Fails
probs = Integer -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
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 [(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)])
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)]
_) | [(Name, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Term)]
us' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Name, Term)] -> Int
forall a. [a] -> Int
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 t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [(Name, Term)]
us' [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs'

  hs :: [Name]
hs = TState -> [Name]
holes TState
ps
  inj :: [Name]
inj = TState -> [Name]
injective TState
ps
  ctxt :: Context
ctxt = TState -> Context
context TState
ps
  ulog :: Bool
ulog = TState -> Bool
unifylog TState
ps
  usupp :: [Name]
usupp = ((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst (TState -> [(Name, Term)]
notunified TState
ps)
  dont :: [Name]
dont = TState -> [Name]
dontunify TState
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, ((Term, Term, Bool, Env, Err, [FailContext], g)
 -> (Term, Term, Bool, Env, Err, [FailContext], g))
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)]
-> (Term, Term, Bool, Env, Err, [FailContext], g)
-> (Term, Term, Bool, Env, Err, [FailContext], g)
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) ([(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
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' = [(Name, Term)] -> 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
||
             (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
n -> Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj) (Term -> [Name]
refsIn Term
x [Name] -> [Name] -> [Name]
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, []) -> Bool
-> String
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"DID " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term, Bool, [(Name, Term)], [Name]) -> String
forall a. Show a => a -> String
show (Term
x',Term
y',Bool
ready,[(Name, Term)]
v,[Name]
dont)) (([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
 -> ([(Name, Term)],
     [(Term, Term, Bool, Env, Err, [FailContext], g)]))
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
-> ([(Name, Term)],
    [(Term, Term, Bool, Env, Err, [FailContext], g)])
forall a b. (a -> b) -> a -> b
$
                                let v' :: [(Name, Term)]
v' = ((Name, Term) -> Bool) -> [(Name, Term)] -> [(Name, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, Term
_) -> Name
n Name -> [Name] -> Bool
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 [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
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) (Term, Term, Bool, Env, Err, [FailContext], g)
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
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) (Term, Term, Bool, Env, Err, [FailContext], g)
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
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,
                  [(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
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 Name -> Name -> Bool
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 ((Name, Term) -> Name
forall a b. (a, b) -> a
fst (Name, Term)
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
done)
                                    (((Name, Term) -> (Name, Term)) -> [(Name, Term)] -> [(Name, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Term) -> (Name, Term) -> (Name, Term)
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
-> TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all TState
ps [(Name, Term)]
updates Fails
probs = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
updates Fails
probs where
  hs :: [Name]
hs = TState -> [Name]
holes TState
ps
  inj :: [Name]
inj = TState -> [Name]
injective TState
ps
  ctxt :: Context
ctxt = TState -> Context
context TState
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 FailAt -> FailAt -> Bool
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' = [(Name, Term)] -> 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 [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
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) (Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
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 (Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
ps')

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

process :: Tactic -> Name -> StateT TState TC ()
process :: Tactic -> Name -> StateT TState TC ()
process Tactic
EndUnify Name
_
   = do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
        let (Name
h, [(Name, Term)]
_) = TState -> (Name, [(Name, Term)])
unified TState
ps
        Maybe Name -> RunTactic -> StateT TState TC ()
tactic (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
h) RunTactic
solve_unified
process Tactic
t Name
h = Maybe Name -> RunTactic -> StateT TState TC ()
tactic (Name -> Maybe Name
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