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

License     : BSD3
Maintainer  : The Idris Community.

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

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

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

import Util.Pretty hiding (fill)

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

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

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

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

-- Some utilites on proof and tactic states

instance Show ProofState where
    show :: ProofState -> String
show ProofState
ps | [] <- ProofState -> [Name]
holes ProofState
ps
          = Name -> String
forall a. Show a => a -> String
show (ProofState -> Name
thname ProofState
ps) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": no more goals"
    show ProofState
ps | (Name
h : [Name]
hs) <- ProofState -> [Name]
holes ProofState
ps
          = let tm :: ProofTerm
tm = ProofState -> ProofTerm
pterm ProofState
ps
                nm :: Name
nm = ProofState -> Name
thname ProofState
ps
                OK Goal
g = Hole -> ProofTerm -> TC Goal
goal (Name -> Hole
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 Type -> String
forall n. (Eq n, Show n) => EnvTT n -> Binder (TT n) -> String
showG Env
wkenv (Goal -> Binder Type
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 :: ProofState -> Doc OutputAnnotation
pretty ProofState
ps | [] <- ProofState -> [Name]
holes ProofState
ps =
    Name -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty (ProofState -> Name
thname ProofState
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 ProofState
ps | (Name
h : [Name]
hs) <- ProofState -> [Name]
holes ProofState
ps =
    let tm :: ProofTerm
tm = ProofState -> ProofTerm
pterm ProofState
ps
        OK Goal
g = Hole -> ProofTerm -> TC Goal
goal (Name -> Hole
forall a. a -> Maybe a
Just Name
h) ProofTerm
tm
        nm :: Name
nm = ProofState -> Name
thname ProofState
ps in
    let wkEnv :: Env
wkEnv = Goal -> Env
premises Goal
g in
      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 Type)] -> 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 Type -> Doc OutputAnnotation
prettyGoal Env
wkEnv (Goal -> Binder Type
goalType Goal
g)
    where
      prettyGoal :: Env -> Binder Type -> Doc OutputAnnotation
prettyGoal Env
ps (Guess Type
t Type
v) =
        Env -> Type -> Doc OutputAnnotation
prettyEnv Env
ps Type
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 -> Type -> Doc OutputAnnotation
prettyEnv Env
ps Type
v
      prettyGoal Env
ps Binder Type
b = Env -> Type -> Doc OutputAnnotation
prettyEnv Env
ps (Type -> Doc OutputAnnotation) -> Type -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b

      prettyPs :: Env -> [(a, b, Binder Type)] -> Doc OutputAnnotation
prettyPs Env
env [] = Doc OutputAnnotation
forall a. Doc a
empty
      prettyPs Env
env ((a
n, b
_, Let RigCount
_ Type
t Type
v):[(a, b, Binder Type)]
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 -> Type -> Doc OutputAnnotation
prettyEnv Env
env Type
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 -> Type -> Doc OutputAnnotation
prettyEnv Env
env Type
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 Type)] -> Doc OutputAnnotation
prettyPs Env
env [(a, b, Binder Type)]
bs))
      prettyPs Env
env ((a
n, b
_, Binder Type
b):[(a, b, Binder Type)]
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 -> Type -> Doc OutputAnnotation
prettyEnv Env
env (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
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 Type)] -> Doc OutputAnnotation
prettyPs Env
env [(a, b, Binder Type)]
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], Type, Type, Bool)] -> String
forall a. Show a => a -> String
show (((Type, Type, Bool, Env, Err, [FailContext], FailAt)
 -> (FailAt, [Name], Type, Type, Bool))
-> Fails -> [(FailAt, [Name], Type, Type, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Type
x, Type
y, Bool
hs, Env
env, Err
_, [FailContext]
_, FailAt
t) -> (FailAt
t, ((Name, RigCount, Binder Type) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> Name
forall a b c. (a, b, c) -> a
fstEnv Env
env, Type
x, Type
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
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
match_unify' Context
ctxt Env
env (Type
topx, Maybe Provenance
xfrom) (Type
topy, Maybe Provenance
yfrom) =
   do ProofState
ps <- StateT ProofState TC ProofState
forall s (m :: * -> *). MonadState s m => m s
get
      let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
ps
      let inj :: [Name]
inj = ProofState -> [Name]
injective ProofState
ps
      Bool
-> String
-> StateT ProofState TC [(Name, Type)]
-> StateT ProofState TC [(Name, Type)]
forall p. Bool -> String -> p -> p
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                (String
"Matching " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Type, Type) -> String
forall a. Show a => a -> String
show (Type
topx, Type
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 (ProofState -> [Name]
holes ProofState
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]
++ Type -> String
forall a. Show a => a -> String
show (ProofTerm -> Type
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
                 ) (StateT ProofState TC [(Name, Type)]
 -> StateT ProofState TC [(Name, Type)])
-> StateT ProofState TC [(Name, Type)]
-> StateT ProofState TC [(Name, Type)]
forall a b. (a -> b) -> a -> b
$
       case Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Type)]
match_unify Context
ctxt Env
env (Type
topx, Maybe Provenance
xfrom) (Type
topy, Maybe Provenance
yfrom) [Name]
inj (ProofState -> [Name]
holes ProofState
ps) [FailContext]
while of
            OK [(Name, Type)]
u -> Bool
-> String
-> StateT ProofState TC [(Name, Type)]
-> StateT ProofState TC [(Name, Type)]
forall p. Bool -> String -> p -> p
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                        (String
"Matched " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Type)] -> String
forall a. Show a => a -> String
show [(Name, Type)]
u) (StateT ProofState TC [(Name, Type)]
 -> StateT ProofState TC [(Name, Type)])
-> StateT ProofState TC [(Name, Type)]
-> StateT ProofState TC [(Name, Type)]
forall a b. (a -> b) -> a -> b
$
                     do let (Name
h, [(Name, Type)]
ns) = ProofState -> (Name, [(Name, Type)])
unified ProofState
ps
                        ProofState -> StateT ProofState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { unified :: (Name, [(Name, Type)])
unified = (Name
h, [(Name, Type)]
u [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. [a] -> [a] -> [a]
++ [(Name, Type)]
ns) })
                        [(Name, Type)] -> StateT ProofState TC [(Name, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Type)]
u
            Error Err
e -> Bool
-> String
-> StateT ProofState TC [(Name, Type)]
-> StateT ProofState TC [(Name, Type)]
forall p. Bool -> String -> p -> p
traceWhen (ProofState -> Bool
unifylog ProofState
ps)
                         (String
"No match " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e) (StateT ProofState TC [(Name, Type)]
 -> StateT ProofState TC [(Name, Type)])
-> StateT ProofState TC [(Name, Type)]
-> StateT ProofState TC [(Name, Type)]
forall a b. (a -> b) -> a -> b
$
                        do ProofState -> StateT ProofState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { problems :: Fails
problems = (Type
topx, Type
topy, Bool
True,
                                                 Env
env, Err
e, [FailContext]
while, FailAt
Match) (Type, Type, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
:
                                                 ProofState -> Fails
problems ProofState
ps })
                           [(Name, Type)] -> StateT ProofState TC [(Name, Type)]
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, Type)] -> StateT ProofState TC [(Name, Type)]
mergeSolutions Env
env [(Name, Type)]
ns = [(Name, Type)]
-> [(Name, Type)] -> StateT ProofState TC [(Name, Type)]
forall (m :: * -> *) a.
(Eq a, MonadState ProofState m) =>
[(a, Type)] -> [(a, Type)] -> m [(a, Type)]
merge [] [(Name, Type)]
ns
  where
    merge :: [(a, Type)] -> [(a, Type)] -> m [(a, Type)]
merge [(a, Type)]
acc [] = [(a, Type)] -> m [(a, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, Type)] -> [(a, Type)]
forall a. [a] -> [a]
reverse [(a, Type)]
acc)
    merge [(a, Type)]
acc ((a
n, Type
t) : [(a, Type)]
ns)
          | Just Type
t' <- a -> [(a, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Type)]
ns
              = do ProofState
ps <- m ProofState
forall s (m :: * -> *). MonadState s m => m s
get
                   let probs :: Fails
probs = ProofState -> Fails
problems ProofState
ps
                   ProofState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ProofState
ps { problems :: Fails
problems = Fails
probs Fails -> Fails -> Fails
forall a. [a] -> [a] -> [a]
++ [(Type
t,Type
t',Bool
True,Env
env,
                                                    Bool
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> Err
-> [(Name, Type)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
True (Type
t, Maybe Provenance
forall a. Maybe a
Nothing) (Type
t', Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err
forall t. String -> Err' t
Msg String
"") (Env -> [(Name, Type)]
forall a b1 b2. [(a, b1, Binder b2)] -> [(a, b2)]
errEnv Env
env) Int
0,
                                                     [], FailAt
Unify)] })
                   [(a, Type)] -> [(a, Type)] -> m [(a, Type)]
merge [(a, Type)]
acc [(a, Type)]
ns
          | Bool
otherwise = [(a, Type)] -> [(a, Type)] -> m [(a, Type)]
merge ((a
n, Type
t)(a, Type) -> [(a, Type)] -> [(a, Type)]
forall a. a -> [a] -> [a]
: [(a, Type)]
acc) [(a, Type)]
ns

dropSwaps :: [(Name, TT Name)] -> [(Name, TT Name)]
dropSwaps :: [(Name, Type)] -> [(Name, Type)]
dropSwaps [] = []
dropSwaps (p :: (Name, Type)
p@(Name
x, P NameType
_ Name
y Type
_) : [(Name, Type)]
xs) | Name -> Name -> [(Name, Type)] -> Bool
forall t t. (Eq t, Eq t) => t -> t -> [(t, TT t)] -> Bool
solvedIn Name
y Name
x [(Name, Type)]
xs = [(Name, Type)] -> [(Name, Type)]
dropSwaps [(Name, Type)]
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, Type)
p : [(Name, Type)]
xs) = (Name, Type)
p (Name, Type) -> [(Name, Type)] -> [(Name, Type)]
forall a. a -> [a] -> [a]
: [(Name, Type)] -> [(Name, Type)]
dropSwaps [(Name, Type)]
xs

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

dropUntil :: (a -> Bool) -> [a] -> [a]
dropUntil :: (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 -> ProofState -> ProofState
doneElaboratingAppPS Name
f ProofState
ps = let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
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 ProofState
ps { while_elaborating :: [FailContext]
while_elaborating = [FailContext]
while' }

doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS Name
f Name
x ProofState
ps = let while :: [FailContext]
while = ProofState -> [FailContext]
while_elaborating ProofState
ps
                                  while' :: [FailContext]
while' = (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 ProofState
ps { while_elaborating :: [FailContext]
while_elaborating = [FailContext]
while' }

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

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

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

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

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

envAtFocus :: ProofState -> TC Env
envAtFocus :: ProofState -> TC Env
envAtFocus ProofState
ps
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ProofState -> [Name]
holes ProofState
ps) = do Goal
g <- Hole -> ProofTerm -> TC Goal
goal (Name -> Hole
forall a. a -> Maybe a
Just ([Name] -> Name
forall a. [a] -> a
head (ProofState -> [Name]
holes ProofState
ps))) (ProofState -> ProofTerm
pterm ProofState
ps)
                                 Env -> TC Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Env
premises Goal
g)
    | Bool
otherwise = String -> TC Env
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]
++ Type -> String
forall a. Show a => a -> String
show (ProofTerm -> Type
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps))

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

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

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

attack :: RunTactic
attack :: RunTactic
attack Context
ctxt Env
env (Bind Name
x (Hole Type
t) Type
sc)
    = do Name
h <- String -> StateT ProofState TC Name
forall (m :: * -> *). Monad m => String -> StateT ProofState m Name
getName String
"hole"
         (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = Name
h Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ProofState -> [Name]
holes ProofState
ps })
         Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Type -> Binder Type
forall b. b -> b -> Binder b
Guess Type
t (Name -> Type
newtm Name
h)) Type
sc
  where
    newtm :: Name -> Type
newtm Name
h = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t) (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Type
t)
attack Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
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 Type
t =
    do (Type
tyv, Type
tyt) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
ty
       TC () -> StateT ProofState TC ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT ProofState TC ())
-> TC () -> StateT ProofState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> TC ()
isType Context
ctxt Env
env Type
tyt
       (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let (Name
g:[Name]
gs) = ProofState -> [Name]
holes ProofState
ps in
                          ProofState
ps { holes :: [Name]
holes = Name
g Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
gs } )
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Type -> Binder Type
forall b. b -> Binder b
Hole Type
tyv) Type
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 :: Type
t@(Bind Name
x (Hole Type
retty) Type
sc) =
    do (Type
tyv, Type
tyt) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
argty
       TC () -> StateT ProofState TC ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT ProofState TC ())
-> TC () -> StateT ProofState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> TC ()
isType Context
ctxt Env
env Type
tyt
       (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let (Name
g:[Name]
gs) = ProofState -> [Name]
holes ProofState
ps in
                          ProofState
ps { holes :: [Name]
holes = Name
g Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
gs } )
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Type -> Binder Type
forall b. b -> Binder b
Hole (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
bn (RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing Type
tyv Type
tyt) Type
retty)) Type
t
claimFn Name
_ Name
_ Raw
_ Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
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 Type
t
    = -- trace (showSep "\n" (map show (scvs t))) $
      let ([(Name, Binder Type)]
bs, Type
sc) = Type -> [(Name, Binder Type)] -> ([(Name, Binder Type)], Type)
forall a.
TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs Type
t []
          newbs :: [(Name, Binder Type)]
newbs = [(Name, Binder Type)] -> [(Name, Binder Type)]
forall a. [a] -> [a]
reverse ([(Name, Binder Type)] -> [(Name, Binder Type)]
sortB ([(Name, Binder Type)] -> [(Name, Binder Type)]
forall a. [a] -> [a]
reverse [(Name, Binder Type)]
bs)) in
          Bool
-> String -> StateT ProofState TC Type -> StateT ProofState TC Type
forall p. Bool -> String -> p -> p
traceWhen ([(Name, Binder Type)]
bs [(Name, Binder Type)] -> [(Name, Binder Type)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [(Name, Binder Type)]
newbs) ([(Name, Binder Type)] -> String
forall a. Show a => a -> String
show [(Name, Binder Type)]
bs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n ==> \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Binder Type)] -> String
forall a. Show a => a -> String
show [(Name, Binder Type)]
newbs) (StateT ProofState TC Type -> StateT ProofState TC Type)
-> StateT ProofState TC Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$
            Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Binder Type)] -> Type -> Type
forall n. [(n, Binder (TT n))] -> TT n -> TT n
bindAll [(Name, Binder Type)]
newbs Type
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 Type)] -> [(Name, Binder Type)]
sortB [] = []
        sortB ((Name, Binder Type)
x:[(Name, Binder Type)]
xs) | ((Name, Binder Type) -> Bool) -> [(Name, Binder Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Name, Binder Type) -> (Name, Binder Type) -> Bool
forall n b a. Eq n => (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (Name, Binder Type)
x) [(Name, Binder Type)]
xs = (Name, Binder Type)
x (Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
forall a. a -> [a] -> [a]
: [(Name, Binder Type)] -> [(Name, Binder Type)]
sortB [(Name, Binder Type)]
xs
                     | Bool
otherwise = [(Name, Binder Type)] -> [(Name, Binder Type)]
sortB ((Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
forall n.
Eq n =>
(n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (Name, Binder Type)
x [(Name, Binder Type)]
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 Type
t = do (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                                            if Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
                                               then ProofState
ps { holes :: [Name]
holes = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ([Name]
hs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
n]) }
                                               else ProofState
ps)
                        ProofState
ps <- StateT ProofState TC ProofState
forall s (m :: * -> *). MonadState s m => m s
get
                        Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t

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

implementationArg :: Name -> RunTactic
implementationArg :: Name -> RunTactic
implementationArg Name
n Context
ctxt Env
env (Bind Name
x (Hole Type
t) Type
sc)
    = do (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps
                            is :: [Name]
is = ProofState -> [Name]
implementations ProofState
ps in
                            ProofState
ps { holes :: [Name]
holes = ([Name]
hs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
x],
                                 implementations :: [Name]
implementations = Name
xName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
is })
         Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t) Type
sc)
implementationArg Name
n Context
ctxt Env
env Type
_
    = String -> StateT ProofState TC Type
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 Type
t) Type
sc)
    = do (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> case Name
-> [(Name, ([FailContext], [Name]))]
-> Maybe ([FailContext], [Name])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (ProofState -> [(Name, ([FailContext], [Name]))]
autos ProofState
ps) of
                             Maybe ([FailContext], [Name])
Nothing ->
                               let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                               ProofState
ps { holes :: [Name]
holes = ([Name]
hs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
x],
                                    autos :: [(Name, ([FailContext], [Name]))]
autos = (Name
x, (ProofState -> [FailContext]
while_elaborating ProofState
ps, Type -> [Name]
refsIn Type
t)) (Name, ([FailContext], [Name]))
-> [(Name, ([FailContext], [Name]))]
-> [(Name, ([FailContext], [Name]))]
forall a. a -> [a] -> [a]
: ProofState -> [(Name, ([FailContext], [Name]))]
autos ProofState
ps }
                             Just ([FailContext], [Name])
_ -> ProofState
ps)
         Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t) Type
sc)
autoArg Name
n Context
ctxt Env
env Type
_
    = String -> StateT ProofState TC Type
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 Type
b Type
sc)
    = do (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let is :: [Name]
is = ProofState -> [Name]
injective ProofState
ps in
                            ProofState
ps { injective :: [Name]
injective = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
is })
         Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x Binder Type
b Type
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 Type
t) (P NameType
nt Name
x' Type
ty)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let env' :: Env
env' = ((Name, RigCount, Binder Type) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, RigCount
_, Binder Type
t) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
dropped) Env
env
       (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps in
                          ProofState
ps { usedns :: [Name]
usedns = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ProofState -> [Name]
usedns ProofState
ps,
                               holes :: [Name]
holes = [Name]
hs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x] })
       ProofState
ps <- StateT ProofState TC ProofState
forall s (m :: * -> *). MonadState s m => m s
get
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Int -> [Name] -> Type -> Binder Type
forall b. Int -> [Name] -> b -> Binder b
GHole (Env -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
env') (ProofState -> [Name]
psnames ProofState
ps) (Env -> Type -> Type
mkTy (Env -> Env
forall a. [a] -> [a]
reverse Env
env') Type
t))
                      (Type -> [Type] -> Type
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
ty) (((Name, RigCount, Binder Type) -> Type) -> Env -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> Type
forall n b. (n, b, Binder (TT n)) -> TT n
getP (Env -> Env
forall a. [a] -> [a]
reverse Env
env'))))
  where
    mkTy :: Env -> Type -> Type
mkTy []           Type
t = Type
t
    mkTy ((Name
n,RigCount
rig,Binder Type
b) : Env
bs) Type
t = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
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 Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b) (UExp -> Type
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (Env -> Type -> Type
mkTy Env
bs Type
t)

    setRig :: RigCount -> Name -> RigCount
setRig RigCount
Rig1 Name
n | Name
n Name -> [Name] -> 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 Type
_ = String -> StateT ProofState TC Type
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 Type
t) (P NameType
nt Name
x' Type
ty)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Type
fty, Type
_) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
fty_in
       (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> let hs :: [Name]
hs = ProofState -> [Name]
holes ProofState
ps
                          ds :: [Name]
ds = ProofState -> [Name]
deferred ProofState
ps in
                          ProofState
ps { holes :: [Name]
holes = [Name]
hs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                               deferred :: [Name]
deferred = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
ds })
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Int -> [Name] -> Type -> Binder Type
forall b. Int -> [Name] -> b -> Binder b
GHole Int
0 [] Type
fty)
                      (Type -> [Type] -> Type
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
ty) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
getP [Name]
args)))
  where
    getP :: Name -> Type
getP Name
n = case Name -> Env -> Maybe (Binder Type)
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
env of
                  Just Binder Type
b -> NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)
                  Maybe (Binder Type)
Nothing -> String -> Type
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
_ Type
_ = String -> StateT ProofState TC Type
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 :: Type
h@(Bind Name
x Binder Type
b Type
sc) =
    do (Type
tmv, Type
_) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
tm
       [(Name, Type)]
ns' <- Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
unify' Context
ctxt Env
env (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b, Maybe Provenance
forall a. Maybe a
Nothing) (Type
tmv, Maybe Provenance
forall a. Maybe a
Nothing)
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
h
unifyGoal Raw
_ Context
_ Env
_ Type
_ = String -> StateT ProofState TC Type
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 Type
h =
    do (Type
tm1v, Type
_) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
tm1
       (Type
tm2v, Type
_) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
tm2
       [(Name, Type)]
ns' <- Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
unify' Context
ctxt Env
env (Type
tm1v, Maybe Provenance
forall a. Maybe a
Nothing) (Type
tm2v, Maybe Provenance
forall a. Maybe a
Nothing)
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
h

exact :: Raw -> RunTactic
exact :: Raw -> RunTactic
exact Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Type
ty) Type
sc) =
    do (Type
val, Type
valty) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
guess
       TC () -> StateT ProofState TC ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT ProofState TC ())
-> TC () -> StateT ProofState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt Env
env Type
valty Type
ty
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Type -> Binder Type
forall b. b -> b -> Binder b
Guess Type
ty Type
val) Type
sc
exact Raw
_ Context
_ Env
_ Type
_ = String -> StateT ProofState TC Type
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 Type
ty) Type
sc) =
    do (Type
val, Type
valty) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
guess
       Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
unify' Context
ctxt Env
env (Type
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Type -> Provenance
SourceTerm Type
val)
                       (Type
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Type -> Type -> Provenance
chkPurpose Type
val Type
ty))
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Type -> Binder Type
forall b. b -> b -> Binder b
Guess Type
ty Type
val) Type
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 :: Type -> Type -> Provenance
chkPurpose Type
val (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ (P NameType
_ (MN Int
_ Text
_) Type
_) Type
_) (P NameType
_ (MN Int
_ Text
_) Type
_))
                   = Type -> Provenance
TooManyArgs Type
val
    chkPurpose Type
_ Type
_ = Provenance
ExpectedType
fill Raw
_ Context
_ Env
_ Type
_ = String -> StateT ProofState TC Type
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 Type
ty) Type
sc) =
    do (Type
val, Type
valty) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
guess
       Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
match_unify' Context
ctxt Env
env (Type
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Type -> Provenance
SourceTerm Type
val)
                             (Type
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
ExpectedType)
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Type -> Binder Type
forall b. b -> b -> Binder b
Guess Type
ty Type
val) Type
sc
match_fill Raw
_ Context
_ Env
_ Type
_ = String -> StateT ProofState TC Type
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 Type
ty) Type
sc) =
    do let val :: Type
val = Type -> [Type] -> Type
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
f Type
forall n. TT n
Erased) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
forall n. TT n
Erased) [Name]
as)
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Type -> Binder Type
forall b. b -> b -> Binder b
Guess Type
ty Type
val) Type
sc
prep_fill Name
f [Name]
as Context
ctxt Env
env Type
t = String -> StateT ProofState TC Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT ProofState TC Type)
-> String -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ String
"Can't prepare fill at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t

complete_fill :: RunTactic
complete_fill :: RunTactic
complete_fill Context
ctxt Env
env (Bind Name
x (Guess Type
ty Type
val) Type
sc) =
    do let guess :: Raw
guess = Type -> Raw
forget Type
val
       (Type
val', Type
valty) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
guess
       Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
unify' Context
ctxt Env
env (Type
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Type -> Provenance
SourceTerm Type
val')
                       (Type
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
ExpectedType)
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Type -> Binder Type
forall b. b -> b -> Binder b
Guess Type
ty Type
val) Type
sc
complete_fill Context
ctxt Env
env Type
t = String -> StateT ProofState TC Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT ProofState TC Type)
-> String -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ String
"Can't complete fill at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
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 Type
ty Type
val) Type
sc)
   = do ProofState
ps <- StateT ProofState TC ProofState
forall s (m :: * -> *). MonadState s m => m s
get
        [Name]
dropdots <-
             case Name -> [(Name, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (ProofState -> [(Name, Type)]
notunified ProofState
ps) of
                Just (P NameType
_ Name
h Type
_)
                     | Name
h Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x -> [Name] -> StateT ProofState TC [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- Can't solve itself!
                Just Type
tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
                            do Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
match_unify' Context
ctxt Env
env (Type
tm, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
InferredVal)
                                                     (Type
val, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
GivenVal)
                               [Name] -> StateT ProofState TC [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return [Name
x]
                Maybe Type
_ -> [Name] -> StateT ProofState TC [Name]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = Bool -> String -> [Name] -> [Name]
forall p. Bool -> String -> p -> p
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"Dropping hole " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x) ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$
                                       ProofState -> [Name]
holes ProofState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                            solved :: Maybe (Name, Type)
solved = (Name, Type) -> Maybe (Name, Type)
forall a. a -> Maybe a
Just (Name
x, Type
val),
                            dontunify :: [Name]
dontunify = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
x) (ProofState -> [Name]
dontunify ProofState
ps),
                            notunified :: [(Name, Type)]
notunified = [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. [(Name, Type)] -> [(a, Type)] -> [(a, Type)]
updateNotunified [(Name
x,Type
val)]
                                           (ProofState -> [(Name, Type)]
notunified ProofState
ps),
                            recents :: [Name]
recents = Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ProofState -> [Name]
recents ProofState
ps,
                            implementations :: [Name]
implementations = ProofState -> [Name]
implementations ProofState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                            dotted :: [(Name, [Name])]
dotted = [Name] -> [(Name, [Name])] -> [(Name, [Name])]
forall a (t :: * -> *) (t :: * -> *).
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, t a)] -> [(a, t a)]
dropUnified [Name]
dropdots (ProofState -> [(Name, [Name])]
dotted ProofState
ps) })
        let (Type
locked, Bool
_) = [Name] -> Type -> (Type, Bool)
tryLock (ProofState -> [Name]
holes ProofState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) (Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x Type
val Type
sc) in
            Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
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 (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 (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] -> Type -> (Type, Bool)
tryLock [Name]
hs tm :: Type
tm@(App AppStatus Name
Complete Type
_ Type
_) = (Type
tm, Bool
True)
        tryLock [Name]
hs tm :: Type
tm@(App AppStatus Name
s Type
f Type
a) =
             let (Type
f', Bool
fl) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs Type
f
                 (Type
a', Bool
al) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs Type
a in
                 if Bool
fl Bool -> Bool -> Bool
&& Bool
al then (AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Type
f' Type
a', Bool
True)
                             else (AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f' Type
a', Bool
False)
        tryLock [Name]
hs t :: Type
t@(P NameType
_ Name
n Type
_) = (Type
t, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs)
        tryLock [Name]
hs t :: Type
t@(Bind Name
n (Hole Type
_) Type
sc) = (Type
t, Bool
False)
        tryLock [Name]
hs t :: Type
t@(Bind Name
n (Guess Type
_ Type
_) Type
sc) = (Type
t, Bool
False)
        tryLock [Name]
hs t :: Type
t@(Bind Name
n (Let RigCount
r Type
ty Type
val) Type
sc)
            = let (Type
ty', Bool
tyl) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs Type
ty
                  (Type
val', Bool
vall) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs Type
val
                  (Type
sc', Bool
scl) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs Type
sc in
                  (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Type -> Binder Type
forall b. RigCount -> b -> b -> Binder b
Let RigCount
r Type
ty' Type
val') Type
sc', Bool
tyl Bool -> Bool -> Bool
&& Bool
vall Bool -> Bool -> Bool
&& Bool
scl)
        tryLock [Name]
hs t :: Type
t@(Bind Name
n Binder Type
b Type
sc)
            = let (Type
bt', Bool
btl) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)
                  (Type
sc', Bool
scl) = [Name] -> Type -> (Type, Bool)
tryLock [Name]
hs Type
sc in
                  (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Binder Type
b { binderTy :: Type
binderTy = Type
bt' }) Type
sc', Bool
btl Bool -> Bool -> Bool
&& Bool
scl)
        tryLock [Name]
hs Type
t = (Type
t, Bool
True)

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

intro :: Maybe Name -> RunTactic
intro :: Hole -> RunTactic
intro Hole
mn Context
ctxt Env
env (Bind Name
x (Hole Type
t) (P NameType
_ Name
x' Type
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let t' :: Type
t' = case Type
t of
                    x :: Type
x@(Bind Name
y (Pi RigCount
_ Maybe ImplicitInfo
_ Type
s Type
_) Type
_) -> Type
x
                    Type
_ -> Context -> Env -> Type -> Type
normalise Context
ctxt Env
env Type
t
       case Type
t' of
           Bind Name
y (Pi RigCount
rig Maybe ImplicitInfo
_ Type
s Type
_) Type
t ->
               let n :: Name
n = case Hole
mn of
                      Just Name
name -> Name
name
                      Hole
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' :: Type
t' = Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
y (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
s) Type
t
               in Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
Lam RigCount
rig Type
s) (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t') (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Type
t'))
           Type
_ -> TC Type -> StateT ProofState TC Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Type -> StateT ProofState TC Type)
-> TC Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Err -> TC Type
forall a. Err -> TC a
tfail (Err -> TC Type) -> Err -> TC Type
forall a b. (a -> b) -> a -> b
$ Type -> Err
forall t. t -> Err' t
CantIntroduce Type
t'
intro Hole
n Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
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 Type
t) (P NameType
_ Name
x' Type
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Type
tyv, Type
tyt) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
ty
       Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
unify' Context
ctxt Env
env (Type
tyt, Maybe Provenance
forall a. Maybe a
Nothing) (UExp -> Type
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), Maybe Provenance
forall a. Maybe a
Nothing)
       Context
-> Env
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> StateT ProofState TC [(Name, Type)]
unify' Context
ctxt Env
env (Type
t, Maybe Provenance
forall a. Maybe a
Nothing) (UExp -> Type
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), Maybe Provenance
forall a. Maybe a
Nothing)
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
impl Type
tyv (UExp -> Type
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t) (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Type
t))
forall Name
n RigCount
rig Maybe ImplicitInfo
impl Raw
ty Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
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 Type
t) Type
sc) =
    do (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = Bool -> String -> [Name] -> [Name]
forall p. Bool -> String -> p -> p
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"Dropping pattern hole " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x) ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$
                                     ProofState -> [Name]
holes ProofState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x],
                           solved :: Maybe (Name, Type)
solved = (Name, Type) -> Maybe (Name, Type)
forall a. a -> Maybe a
Just (Name
x, NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t),
                           dontunify :: [Name]
dontunify = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
x) (ProofState -> [Name]
dontunify ProofState
ps),
                           notunified :: [(Name, Type)]
notunified = [(Name, Type)] -> [(Name, Type)] -> [(Name, Type)]
forall a. [(Name, Type)] -> [(a, Type)] -> [(a, Type)]
updateNotunified [(Name
x,NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t)]
                                          (ProofState -> [(Name, Type)]
notunified ProofState
ps),
                           injective :: [Name]
injective = Name -> Name -> [Name] -> [Name]
forall a. Eq a => a -> a -> [a] -> [a]
addInj Name
n Name
x (ProofState -> [Name]
injective ProofState
ps)
                         })
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
PVar RigCount
RigW Type
t) (Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
  where addInj :: a -> a -> [a] -> [a]
addInj a
n a
x [a]
ps | a
x 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 Type
tm = String -> StateT ProofState TC Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT ProofState TC Type)
-> String -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ String
"Can't add pattern var at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
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 Type
t) (P NameType
_ Name
x' Type
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Type
tyv,  Type
tyt)  <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
ty
       (Type
valv, Type
valt) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
val
       TC () -> StateT ProofState TC ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT ProofState TC ())
-> TC () -> StateT ProofState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> TC ()
isType Context
ctxt Env
env Type
tyt
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Type -> Binder Type
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Type
tyv Type
valv) (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t) (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Type
t))
letbind Name
n RigCount
rig Raw
ty Raw
val Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't let bind here"

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

rewrite :: Raw -> RunTactic
rewrite :: Raw -> RunTactic
rewrite Raw
tm Context
ctxt Env
env (Bind Name
x (Hole Type
t) xp :: Type
xp@(P NameType
_ Name
x' Type
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do (Type
tmv, Type
tmt) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
tm
       let tmt' :: Type
tmt' = Context -> Env -> Type -> Type
normalise Context
ctxt Env
env Type
tmt
       case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
tmt' of
         (P NameType
_ (UN Text
q) Type
_, [Type
lt,Type
rt,Type
l,Type
r]) | Text
q Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"=" ->
            do let p :: Type
p = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
rname (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW Type
lt) (Type -> Type -> Type -> Type -> Type
mkP (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
rname Type
lt) Type
r Type
l Type
t)
               let newt :: Type
newt = Type -> Type -> Type -> Type -> Type
mkP Type
l Type
r Type
l Type
t
               let sc :: Raw
sc = Type -> Raw
forget (Type -> Raw) -> Type -> Raw
forall a b. (a -> b) -> a -> b
$ (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
newt)
                                       (Type -> [Type] -> Type
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"replace") (UExp -> Type
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)))
                                              [Type
lt, Type
l, Type
r, Type
p, Type
tmv, Type
xp]))
               (Type
scv, Type
sct) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
sc
               Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
scv
         (Type, [Type])
_ -> TC Type -> StateT ProofState TC Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Type -> StateT ProofState TC Type)
-> TC Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Err -> TC Type
forall a. Err -> TC a
tfail (Type -> Type -> Err
forall t. t -> t -> Err' t
NotEquality Type
tmv Type
tmt')
  where rname :: Name
rname = Int -> String -> Name
sMN Int
0 String
"replaced"
rewrite Raw
_ Context
_ Env
_ Type
_ = String -> StateT ProofState TC Type
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 :: Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
ty | Type
l Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty = Type
lt
mkP Type
lt Type
l Type
r (App AppStatus Name
s Type
f Type
a) = let f' :: Type
f' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
f) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
f else Type
f
                             a' :: Type
a' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
a) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
a else Type
a in
                             AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f' Type
a'
mkP Type
lt Type
l Type
r (Bind Name
n Binder Type
b Type
sc)
                     = let b' :: Binder Type
b' = Binder Type -> Binder Type
mkPB Binder Type
b
                           sc' :: Type
sc' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
sc) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
sc else Type
sc in
                           Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Type
b' Type
sc'
    where mkPB :: Binder Type -> Binder Type
mkPB (Let RigCount
c Type
t Type
v) = let t' :: Type
t' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
t) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
t else Type
t
                                 v' :: Type
v' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
v) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
v else Type
v in
                                 RigCount -> Type -> Type -> Binder Type
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c Type
t' Type
v'
          mkPB Binder Type
b = let ty :: Type
ty = Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b
                       ty' :: Type
ty' = if (Type
r Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
ty) then Type -> Type -> Type -> Type -> Type
mkP Type
lt Type
l Type
r Type
ty else Type
ty in
                             Binder Type
b { binderTy :: Type
binderTy = Type
ty' }
mkP Type
lt Type
l Type
r Type
x = Type
x

equiv :: Raw -> RunTactic
equiv :: Raw -> RunTactic
equiv Raw
tm Context
ctxt Env
env (Bind Name
x (Hole Type
t) Type
sc) =
    do (Type
tmv, Type
tmt) <- TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT ProofState TC (Type, Type))
-> TC (Type, Type) -> StateT ProofState TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env Raw
tm
       TC () -> StateT ProofState TC ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT ProofState TC ())
-> TC () -> StateT ProofState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt Env
env Type
tmv Type
t
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
tmv) Type
sc
equiv Raw
tm Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
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 Type
t) (P NameType
_ Name
x' Type
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
    do let t' :: Type
t' = case Type
t of
                    x :: Type
x@(Bind Name
y (PVTy Type
s) Type
t) -> Type
x
                    Type
_ -> Context -> Env -> Type -> Type
normalise Context
ctxt Env
env Type
t
       case Type
t' of
           Bind Name
y (PVTy Type
s) Type
t -> let t' :: Type
t' = Name -> Type -> Type -> Type
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
s) Type
t in
                                    Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
PVar RigCount
rig Type
s) (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole Type
t') (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Type
t'))
           Type
_ -> String -> StateT ProofState TC Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Nothing to pattern bind"
patbind Name
n RigCount
_ Context
ctxt Env
env Type
_ = String -> StateT ProofState TC Type
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 Type
ty) Type
sc) =
    do Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> StateT ProofState TC Type)
-> Type -> StateT ProofState TC Type
forall a b. (a -> b) -> a -> b
$ Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Type -> Binder Type
forall b. b -> Binder b
Hole (Context -> Env -> Type -> Type
normalise Context
ctxt Env
env Type
ty)) Type
sc
compute Context
ctxt Env
env Type
t = Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t

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

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

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

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

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

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

solve_unified :: RunTactic
solve_unified :: RunTactic
solve_unified Context
ctxt Env
env Type
tm =
    do ProofState
ps <- StateT ProofState TC ProofState
forall s (m :: * -> *). MonadState s m => m s
get
       let (Name
_, [(Name, Type)]
ns) = ProofState -> (Name, [(Name, Type)])
unified ProofState
ps
       let unify :: [(Name, Type)]
unify = [Name] -> [(Name, Type)] -> [Name] -> [(Name, Type)]
forall a (t :: * -> *) (t :: * -> *).
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (ProofState -> [Name]
dontunify ProofState
ps) [(Name, Type)]
ns (ProofState -> [Name]
holes ProofState
ps)
       (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { holes :: [Name]
holes = Bool -> String -> [Name] -> [Name]
forall p. Bool -> String -> p -> p
traceWhen (ProofState -> Bool
unifylog ProofState
ps) (String
"Dropping holes " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
unify)) ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$
                                     ProofState -> [Name]
holes ProofState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
unify,
                           recents :: [Name]
recents = ProofState -> [Name]
recents ProofState
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
unify })
       (ProofState -> ProofState) -> StateT ProofState TC ()
forall (m :: * -> *).
Monad m =>
(ProofState -> ProofState) -> StateT ProofState m ()
action (\ProofState
ps -> ProofState
ps { pterm :: ProofTerm
pterm = [(Name, Type)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Type)]
unify (ProofState -> ProofTerm
pterm ProofState
ps) })
       Type -> StateT ProofState TC Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Type)] -> Type -> Type
updateSolvedTerm [(Name, Type)]
unify Type
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 (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
     Bool -> Bool -> Bool
&& a
n 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 (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 (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 (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
     Bool -> Bool -> Bool
&& a
n 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 (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 (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, Type)] -> [(a, b, f Type)] -> [(a, b, f Type)]
updateEnv [] [(a, b, f Type)]
e = [(a, b, f Type)]
e
updateEnv [(Name, Type)]
ns [] = []
updateEnv [(Name, Type)]
ns ((a
n, b
rig, f Type
b) : [(a, b, f Type)]
env)
   = (a
n, b
rig, (Type -> Type) -> f Type -> f Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Type)] -> Type -> Type
updateSolvedTerm [(Name, Type)]
ns) f Type
b) (a, b, f Type) -> [(a, b, f Type)] -> [(a, b, f Type)]
forall a. a -> [a] -> [a]
: [(Name, Type)] -> [(a, b, f Type)] -> [(a, b, f Type)]
updateEnv [(Name, Type)]
ns [(a, b, f Type)]
env

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

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

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

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

getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance (CantUnify Bool
_ (Type
_, Maybe Provenance
lp) (Type
_, Maybe Provenance
rp) Err
_ [(Name, Type)]
_ 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 :: ProofState -> [(Name, Type)] -> Fails -> ([(Name, Type)], Fails)
updateProblems ProofState
ps [(Name, Type)]
updates Fails
probs = Integer -> [(Name, Type)] -> Fails -> ([(Name, Type)], Fails)
forall t g.
(Eq t, Num t) =>
t
-> [(Name, Type)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Type)],
    [(Type, Type, Bool, Env, Err, [FailContext], g)])
rec Integer
10 [(Name, Type)]
updates Fails
probs
 where
  -- keep trying if we make progress, but not too many times...
  rec :: t
-> [(Name, Type)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Type)],
    [(Type, Type, Bool, Env, Err, [FailContext], g)])
rec t
0 [(Name, Type)]
us [(Type, Type, Bool, Env, Err, [FailContext], g)]
fs = ([(Name, Type)]
us, [(Type, Type, Bool, Env, Err, [FailContext], g)]
fs)
  rec t
n [(Name, Type)]
us [(Type, Type, Bool, Env, Err, [FailContext], g)]
fs = case [(Name, Type)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Type)],
    [(Type, Type, Bool, Env, Err, [FailContext], g)])
forall g.
[(Name, Type)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Type)],
    [(Type, Type, Bool, Env, Err, [FailContext], g)])
up [(Name, Type)]
us [] [(Type, Type, Bool, Env, Err, [FailContext], g)]
fs of
                     res :: ([(Name, Type)], [(Type, Type, Bool, Env, Err, [FailContext], g)])
res@([(Name, Type)]
_, []) -> ([(Name, Type)], [(Type, Type, Bool, Env, Err, [FailContext], g)])
res
                     res :: ([(Name, Type)], [(Type, Type, Bool, Env, Err, [FailContext], g)])
res@([(Name, Type)]
us', [(Type, Type, Bool, Env, Err, [FailContext], g)]
_) | [(Name, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Type)]
us' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Name, Type)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Type)]
us -> ([(Name, Type)], [(Type, Type, Bool, Env, Err, [FailContext], g)])
res
                     ([(Name, Type)]
us', [(Type, Type, Bool, Env, Err, [FailContext], g)]
fs') -> t
-> [(Name, Type)]
-> [(Type, Type, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Type)],
    [(Type, Type, Bool, Env, Err, [FailContext], g)])
rec (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [(Name, Type)]
us' [(Type, Type, Bool, Env, Err, [FailContext], g)]
fs'

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

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

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

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

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

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

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

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

process :: Tactic -> Name -> StateT TState TC ()
process :: Tactic -> Name -> StateT ProofState TC ()
process Tactic
EndUnify Name
_
   = do ProofState
ps <- StateT ProofState TC ProofState
forall s (m :: * -> *). MonadState s m => m s
get
        let (Name
h, [(Name, Type)]
_) = ProofState -> (Name, [(Name, Type)])
unified ProofState
ps
        Hole -> RunTactic -> StateT ProofState TC ()
tactic (Name -> Hole
forall a. a -> Maybe a
Just Name
h) RunTactic
solve_unified
process Tactic
t Name
h = Hole -> RunTactic -> StateT ProofState TC ()
tactic (Name -> Hole
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 Hole
n)         = Hole -> RunTactic
intro Hole
n
         mktac (IntroTy Raw
ty Hole
n)    = Raw -> Hole -> RunTactic
introTy Raw
ty Hole
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 Type
b)   = Name -> Type -> RunTactic
expandLet Name
n Type
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