{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
PatternGuards #-}
module Idris.Core.ProofState(
ProofState(..), newProof, envAtFocus, goalAtFocus
, Tactic(..), Goal(..), processTactic, nowElaboratingPS
, doneElaboratingAppPS, doneElaboratingArgPS, dropGiven
, keepGiven, getProvenance
) where
import Idris.Core.Evaluate
import Idris.Core.ProofTerm
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Unify
import Idris.Core.WHNF
import Util.Pretty hiding (fill)
import Control.Monad
import Control.Monad.State.Strict
import Data.List
#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<>))
#endif
data ProofState = PS { TState -> Name
thname :: Name,
TState -> [Name]
holes :: [Name],
TState -> [Name]
usedns :: [Name],
TState -> Int
nextname :: Int,
TState -> Int
global_nextname :: Int,
TState -> ProofTerm
pterm :: ProofTerm,
TState -> Term
ptype :: Type,
TState -> [Name]
dontunify :: [Name],
TState -> (Name, [(Name, Term)])
unified :: (Name, [(Name, Term)]),
TState -> [(Name, Term)]
notunified :: [(Name, Term)],
TState -> [(Name, [Name])]
dotted :: [(Name, [Name])],
TState -> Maybe (Name, Term)
solved :: Maybe (Name, Term),
TState -> Fails
problems :: Fails,
TState -> [Name]
injective :: [Name],
TState -> [Name]
deferred :: [Name],
TState -> [Name]
implementations :: [Name],
TState -> [(Name, ([FailContext], [Name]))]
autos :: [(Name, ([FailContext], [Name]))],
TState -> [Name]
psnames :: [Name],
TState -> Maybe TState
previous :: Maybe ProofState,
TState -> Context
context :: Context,
TState -> Ctxt TypeInfo
datatypes :: Ctxt TypeInfo,
TState -> String
plog :: String,
TState -> Bool
unifylog :: Bool,
TState -> Bool
done :: Bool,
TState -> [Name]
recents :: [Name],
TState -> [FailContext]
while_elaborating :: [FailContext],
TState -> String
constraint_ns :: String
}
data Tactic = Attack
| Claim Name Raw
| ClaimFn Name Name Raw
| Reorder Name
| Exact Raw
| Fill Raw
| MatchFill Raw
| PrepFill Name [Name]
| CompleteFill
| Regret
| Solve
| StartUnify Name
| EndUnify
| UnifyAll
| Compute
| ComputeLet Name
| Simplify
| WHNF_Compute
| WHNF_ComputeArgs
| EvalIn Raw
| CheckIn Raw
| Intro (Maybe Name)
| IntroTy Raw (Maybe Name)
| Forall Name RigCount (Maybe ImplicitInfo) Raw
| LetBind Name RigCount Raw Raw
| ExpandLet Name Term
| Rewrite Raw
| Equiv Raw
| PatVar Name
| PatBind Name RigCount
| Focus Name
| Defer [Name] [Name] Name
| DeferType Name Raw [Name]
| Implementation Name
| AutoArg Name
| SetInjective Name
| MoveLast Name
| MatchProblems Bool
| UnifyProblems
| UnifyGoal Raw
| UnifyTerms Raw Raw
| ProofState
| Undo
| QED
deriving Int -> Tactic -> ShowS
[Tactic] -> ShowS
Tactic -> String
(Int -> Tactic -> ShowS)
-> (Tactic -> String) -> ([Tactic] -> ShowS) -> Show Tactic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Tactic -> ShowS
showsPrec :: Int -> Tactic -> ShowS
$cshow :: Tactic -> String
show :: Tactic -> String
$cshowList :: [Tactic] -> ShowS
showList :: [Tactic] -> ShowS
Show
instance Show ProofState where
show :: TState -> String
show TState
ps | [] <- TState -> [Name]
holes TState
ps
= Name -> String
forall a. Show a => a -> String
show (TState -> Name
thname TState
ps) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": no more goals"
show TState
ps | (Name
h : [Name]
hs) <- TState -> [Name]
holes TState
ps
= let tm :: ProofTerm
tm = TState -> ProofTerm
pterm TState
ps
nm :: Name
nm = TState -> Name
thname TState
ps
OK Goal
g = Maybe Name -> ProofTerm -> TC Goal
goal (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
h) ProofTerm
tm
wkenv :: Env
wkenv = Goal -> Env
premises Goal
g in
String
"Other goals: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
hs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
Env -> Env -> String
forall {n} {a} {b}.
(Eq n, Show a, Show n) =>
EnvTT n -> [(a, b, Binder (TT n))] -> String
showPs Env
wkenv (Env -> Env
forall a. [a] -> [a]
reverse Env
wkenv) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"-------------------------------- (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
") -------\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Name -> String
forall a. Show a => a -> String
show Name
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> Binder Term -> String
forall {n}. (Eq n, Show n) => EnvTT n -> Binder (TT n) -> String
showG Env
wkenv (Goal -> Binder Term
goalType Goal
g) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
where showPs :: EnvTT n -> [(a, b, Binder (TT n))] -> String
showPs EnvTT n
env [] = String
""
showPs EnvTT n
env ((a
n, b
_, Let RigCount
_ TT n
t TT n
v):[(a, b, Binder (TT n))]
bs)
= String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++
EnvTT n -> TT n -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
env ( 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 ( 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 ( (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 ( TT n
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
" =?= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ EnvTT n -> TT n -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
ps TT n
v
showG EnvTT n
ps Binder (TT n)
b = EnvTT n -> TT n -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv EnvTT n
ps (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
b)
instance Pretty ProofState OutputAnnotation where
pretty :: TState -> Doc OutputAnnotation
pretty TState
ps | [] <- TState -> [Name]
holes TState
ps =
Name -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty (TState -> Name
thname TState
ps) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" no more goals."
pretty TState
ps | (Name
h : [Name]
hs) <- TState -> [Name]
holes TState
ps =
let tm :: ProofTerm
tm = TState -> ProofTerm
pterm TState
ps
OK Goal
g = Maybe Name -> ProofTerm -> TC Goal
goal (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
h) ProofTerm
tm
nm :: Name
nm = TState -> Name
thname TState
ps in
let wkEnv :: Env
wkEnv = Goal -> Env
premises Goal
g in
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Other goals" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Name] -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty [Name]
hs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Env -> Env -> Doc OutputAnnotation
forall {a} {b}.
Pretty a OutputAnnotation =>
Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
wkEnv (Env -> Env
forall a. [a] -> [a]
reverse Env
wkEnv) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"---------- " Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"Focussing on" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty Name
nm Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
" ----------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Name -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty Name
h Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Env -> Binder Term -> Doc OutputAnnotation
prettyGoal Env
wkEnv (Goal -> Binder Term
goalType Goal
g)
where
prettyGoal :: Env -> Binder Term -> Doc OutputAnnotation
prettyGoal Env
ps (Guess Term
t Term
v) =
Env -> Term -> Doc OutputAnnotation
prettyEnv Env
ps Term
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"=?=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
ps Term
v
prettyGoal Env
ps Binder Term
b = Env -> Term -> Doc OutputAnnotation
prettyEnv Env
ps (Term -> Doc OutputAnnotation) -> Term -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b
prettyPs :: Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [] = Doc OutputAnnotation
forall a. Doc a
empty
prettyPs Env
env ((a
n, b
_, Let RigCount
_ Term
t Term
v):[(a, b, Binder Term)]
bs) =
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (a -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty a
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env Term
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text String
"=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env Term
v Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [(a, b, Binder Term)]
bs))
prettyPs Env
env ((a
n, b
_, Binder Term
b):[(a, b, Binder Term)]
bs) =
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (a -> Doc OutputAnnotation
forall a ty. Pretty a ty => a -> Doc ty
pretty a
n Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Env -> Term -> Doc OutputAnnotation
prettyEnv Env
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Env -> [(a, b, Binder Term)] -> Doc OutputAnnotation
prettyPs Env
env [(a, b, Binder Term)]
bs))
holeName :: Int -> Name
holeName Int
i = Int -> String -> Name
sMN Int
i String
"hole"
qshow :: Fails -> String
qshow :: Fails -> String
qshow Fails
fs = [(FailAt, [Name], Term, Term, Bool)] -> String
forall a. Show a => a -> String
show (((Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> (FailAt, [Name], Term, Term, Bool))
-> Fails -> [(FailAt, [Name], Term, Term, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Term
x, Term
y, Bool
hs, Env
env, Err
_, [FailContext]
_, FailAt
t) -> (FailAt
t, ((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env, Term
x, Term
y, Bool
hs)) Fails
fs)
match_unify' :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) ->
StateT TState TC [(Name, TT Name)]
match_unify' :: Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) =
do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
let while :: [FailContext]
while = TState -> [FailContext]
while_elaborating TState
ps
let inj :: [Name]
inj = TState -> [Name]
injective TState
ps
Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"Matching " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
topx, Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
" in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
forall a. Show a => a -> String
show Env
env String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nHoles: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
holes TState
ps)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
) (StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
case Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Term)]
match_unify Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) [Name]
inj (TState -> [Name]
holes TState
ps) [FailContext]
while of
OK [(Name, Term)]
u -> Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"Matched " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show [(Name, Term)]
u) (StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
do let (Name
h, [(Name, Term)]
ns) = TState -> (Name, [(Name, Term)])
unified TState
ps
TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { unified = (h, u ++ ns) })
[(Name, Term)] -> StateT TState TC [(Name, Term)]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Term)]
u
Error Err
e -> Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"No match " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e) (StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
do TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { problems = (topx, topy, True,
env, e, while, Match) :
problems ps })
[(Name, Term)] -> StateT TState TC [(Name, Term)]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
mergeSolutions :: Env -> [(Name, Term)] -> StateT TState TC [(Name, Term)]
mergeSolutions Env
env [(Name, Term)]
ns = [(Name, Term)] -> [(Name, Term)] -> StateT TState TC [(Name, Term)]
forall {m :: * -> *} {a}.
(Eq a, MonadState TState m) =>
[(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge [] [(Name, Term)]
ns
where
merge :: [(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge [(a, Term)]
acc [] = [(a, Term)] -> m [(a, Term)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, Term)] -> [(a, Term)]
forall a. [a] -> [a]
reverse [(a, Term)]
acc)
merge [(a, Term)]
acc ((a
n, Term
t) : [(a, Term)]
ns)
| Just Term
t' <- a -> [(a, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Term)]
ns
= do TState
ps <- m TState
forall s (m :: * -> *). MonadState s m => m s
get
let probs :: Fails
probs = TState -> Fails
problems TState
ps
TState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { problems = probs ++ [(t,t',True,env,
CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
[], Unify)] })
[(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge [(a, Term)]
acc [(a, Term)]
ns
| Bool
otherwise = [(a, Term)] -> [(a, Term)] -> m [(a, Term)]
merge ((a
n, Term
t)(a, Term) -> [(a, Term)] -> [(a, Term)]
forall a. a -> [a] -> [a]
: [(a, Term)]
acc) [(a, Term)]
ns
dropSwaps :: [(Name, TT Name)] -> [(Name, TT Name)]
dropSwaps :: [(Name, Term)] -> [(Name, Term)]
dropSwaps [] = []
dropSwaps (p :: (Name, Term)
p@(Name
x, P NameType
_ Name
y Term
_) : [(Name, Term)]
xs) | Name -> Name -> [(Name, Term)] -> Bool
forall {t} {t}. (Eq t, Eq t) => t -> t -> [(t, TT t)] -> Bool
solvedIn Name
y Name
x [(Name, Term)]
xs = [(Name, Term)] -> [(Name, Term)]
dropSwaps [(Name, Term)]
xs
where solvedIn :: t -> t -> [(t, TT t)] -> Bool
solvedIn t
_ t
_ [] = Bool
False
solvedIn t
y t
x ((t
y', P NameType
_ t
x' TT t
_) : [(t, TT t)]
xs) | t
y t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y' Bool -> Bool -> Bool
&& t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x' = Bool
True
solvedIn t
y t
x ((t, TT t)
_ : [(t, TT t)]
xs) = t -> t -> [(t, TT t)] -> Bool
solvedIn t
y t
x [(t, TT t)]
xs
dropSwaps ((Name, Term)
p : [(Name, Term)]
xs) = (Name, Term)
p (Name, Term) -> [(Name, Term)] -> [(Name, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(Name, Term)]
dropSwaps [(Name, Term)]
xs
unify' :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) ->
StateT TState TC [(Name, TT Name)]
unify' :: Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) =
do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
let while :: [FailContext]
while = TState -> [FailContext]
while_elaborating TState
ps
let dont :: [Name]
dont = TState -> [Name]
dontunify TState
ps
let inj :: [Name]
inj = TState -> [Name]
injective TState
ps
([(Name, Term)]
u, Fails
fails) <- Bool
-> String
-> StateT TState TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"Trying " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
topx, Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nNormalised " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
topx,
Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
" in\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> String
forall a. Show a => a -> String
show Env
env String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nHoles: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
holes TState
ps)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nInjective: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
injective TState
ps)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") (StateT TState TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails))
-> StateT TState TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall a b. (a -> b) -> a -> b
$
TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails))
-> TC ([(Name, Term)], Fails)
-> StateT TState TC ([(Name, Term)], Fails)
forall a b. (a -> b) -> a -> b
$ Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, Term)], Fails)
unify Context
ctxt Env
env (Term
topx, Maybe Provenance
xfrom) (Term
topy, Maybe Provenance
yfrom) [Name]
inj (TState -> [Name]
holes TState
ps)
(((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst (TState -> [(Name, Term)]
notunified TState
ps)) [FailContext]
while
let notu :: [(Name, Term)]
notu = ((Name, Term) -> Bool) -> [(Name, Term)] -> [(Name, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Name
n, Term
t) -> case Term
t of
Term
_ -> Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
dont) [(Name, Term)]
u
Bool
-> String
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"Unified " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term) -> String
forall a. Show a => a -> String
show (Term
topx, Term
topy) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" without " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
dont String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nSolved: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show [(Name, Term)]
u String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nNew problems: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow Fails
fails
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nNot unified:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show (TState -> [(Name, Term)]
notunified TState
ps)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\nCurrent problems:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow (TState -> Fails
problems TState
ps)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n----------") (StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)])
-> StateT TState TC [(Name, Term)]
-> StateT TState TC [(Name, Term)]
forall a b. (a -> b) -> a -> b
$
do let (Name
h, [(Name, Term)]
ns) = TState -> (Name, [(Name, Term)])
unified TState
ps
let u' :: [(Name, Term)]
u' = ((Name, Term) -> (Name, Term)) -> [(Name, Term)] -> [(Name, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, Term
sol) -> (Name
n, [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
u Term
sol)) [(Name, Term)]
u
[(Name, Term)]
uns <- Env -> [(Name, Term)] -> StateT TState TC [(Name, Term)]
mergeSolutions Env
env ([(Name, Term)]
u' [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
ns)
TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
let ([(Name, Term)]
ns_p, Fails
probs') = TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps [(Name, Term)]
uns (Fails
fails Fails -> Fails -> Fails
forall a. [a] -> [a] -> [a]
++ TState -> Fails
problems TState
ps)
let ns' :: [(Name, Term)]
ns' = [(Name, Term)] -> [(Name, Term)]
dropSwaps [(Name, Term)]
ns_p
let ([(Name, Term)]
notu', Fails
probs_notu) = Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified Env
env (TState -> [Name]
holes TState
ps) ([(Name, Term)]
notu [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ TState -> [(Name, Term)]
notunified TState
ps)
Bool -> String -> StateT TState TC () -> StateT TState TC ()
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"Now solved: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
forall a. Show a => a -> String
show [(Name, Term)]
ns' String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nNow problems: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow (Fails
probs' Fails -> Fails -> Fails
forall a. [a] -> [a] -> [a]
++ Fails
probs_notu) String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nNow injective: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show ([(Name, Term)] -> [Name] -> [Name]
forall {a}. Eq a => [(a, TT a)] -> [a] -> [a]
updateInj [(Name, Term)]
u (TState -> [Name]
injective TState
ps))) (StateT TState TC () -> StateT TState TC ())
-> StateT TState TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$
TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { problems = probs' ++ probs_notu,
unified = (h, ns'),
injective = updateInj u (injective ps),
notunified = notu' })
[(Name, Term)] -> StateT TState TC [(Name, Term)]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, Term)]
u
where updateInj :: [(a, TT a)] -> [a] -> [a]
updateInj ((a
n, TT a
a) : [(a, TT a)]
us) [a]
inj
| (P NameType
_ a
n' TT a
_, [TT a]
_) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
a,
a
n a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
inj = [(a, TT a)] -> [a] -> [a]
updateInj [(a, TT a)]
us (a
n'a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
inj)
| (P NameType
_ a
n' TT a
_, [TT a]
_) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
a,
a
n' a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
inj = [(a, TT a)] -> [a] -> [a]
updateInj [(a, TT a)]
us (a
na -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
inj)
updateInj ((a, TT a)
_ : [(a, TT a)]
us) [a]
inj = [(a, TT a)] -> [a] -> [a]
updateInj [(a, TT a)]
us [a]
inj
updateInj [] [a]
inj = [a]
inj
nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
nowElaboratingPS :: FC -> Name -> Name -> TState -> TState
nowElaboratingPS FC
fc Name
f Name
arg TState
ps = TState
ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
dropUntil :: (a -> Bool) -> [a] -> [a]
dropUntil :: forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
p [] = []
dropUntil a -> Bool
p (a
x:[a]
xs) | a -> Bool
p a
x = [a]
xs
| Bool
otherwise = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
p [a]
xs
doneElaboratingAppPS :: Name -> ProofState -> ProofState
doneElaboratingAppPS :: Name -> TState -> TState
doneElaboratingAppPS Name
f TState
ps = let while :: [FailContext]
while = TState -> [FailContext]
while_elaborating TState
ps
while' :: [FailContext]
while' = (FailContext -> Bool) -> [FailContext] -> [FailContext]
forall a. (a -> Bool) -> [a] -> [a]
dropUntil (\ (FailContext FC
_ Name
f' Name
_) -> Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
f') [FailContext]
while
in TState
ps { while_elaborating = while' }
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS :: Name -> Name -> TState -> TState
doneElaboratingArgPS Name
f Name
x TState
ps = let while :: [FailContext]
while = TState -> [FailContext]
while_elaborating TState
ps
while' :: [FailContext]
while' = (FailContext -> Bool) -> [FailContext] -> [FailContext]
forall a. (a -> Bool) -> [a] -> [a]
dropUntil (\ (FailContext FC
_ Name
f' Name
x') -> Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
f' Bool -> Bool -> Bool
&& Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x') [FailContext]
while
in TState
ps { while_elaborating = while' }
getName :: Monad m => String -> StateT TState m Name
getName :: forall (m :: * -> *). Monad m => String -> StateT TState m Name
getName String
tag = do TState
ps <- StateT TState m TState
forall s (m :: * -> *). MonadState s m => m s
get
let n :: Int
n = TState -> Int
nextname TState
ps
TState -> StateT TState m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { nextname = n+1 })
Name -> StateT TState m Name
forall a. a -> StateT TState m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> StateT TState m Name) -> Name -> StateT TState m Name
forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
n String
tag
action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
action :: forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action TState -> TState
a = do TState
ps <- StateT TState m TState
forall s (m :: * -> *). MonadState s m => m s
get
TState -> StateT TState m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState -> TState
a TState
ps)
query :: Monad m => (ProofState -> r) -> StateT TState m r
query :: forall (m :: * -> *) r.
Monad m =>
(TState -> r) -> StateT TState m r
query TState -> r
q = do TState
ps <- StateT TState m TState
forall s (m :: * -> *). MonadState s m => m s
get
r -> StateT TState m r
forall a. a -> StateT TState m a
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> StateT TState m r) -> r -> StateT TState m r
forall a b. (a -> b) -> a -> b
$ TState -> r
q TState
ps
addLog :: Monad m => String -> StateT TState m ()
addLog :: forall (m :: * -> *). Monad m => String -> StateT TState m ()
addLog String
str = (TState -> TState) -> StateT TState m ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { plog = plog ps ++ str ++ "\n" })
newProof :: Name
-> String
-> Context
-> Ctxt TypeInfo
-> Int
-> Type
-> ProofState
newProof :: Name -> String -> Context -> Ctxt TypeInfo -> Int -> Term -> TState
newProof Name
n String
tcns Context
ctxt Ctxt TypeInfo
datatypes Int
globalNames Term
ty =
let h :: Name
h = Int -> Name
holeName Int
0
ty' :: Term
ty' = Term -> Term
forall n. TT n -> TT n
vToP Term
ty
in Name
-> [Name]
-> [Name]
-> Int
-> Int
-> ProofTerm
-> Term
-> [Name]
-> (Name, [(Name, Term)])
-> [(Name, Term)]
-> [(Name, [Name])]
-> Maybe (Name, Term)
-> Fails
-> [Name]
-> [Name]
-> [Name]
-> [(Name, ([FailContext], [Name]))]
-> [Name]
-> Maybe TState
-> Context
-> Ctxt TypeInfo
-> String
-> Bool
-> Bool
-> [Name]
-> [FailContext]
-> String
-> TState
PS Name
n [Name
h] [] Int
1 Int
globalNames (Term -> ProofTerm
mkProofTerm (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (Term -> Binder Term
forall b. b -> Binder b
Hole Term
ty')
(NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Term
ty'))) Term
ty [] (Name
h, []) [] []
Maybe (Name, Term)
forall a. Maybe a
Nothing [] []
[] [] [] []
Maybe TState
forall a. Maybe a
Nothing Context
ctxt Ctxt TypeInfo
datatypes String
"" Bool
False Bool
False [] [] String
tcns
type TState = ProofState
type RunTactic = RunTactic' TState
envAtFocus :: ProofState -> TC Env
envAtFocus :: TState -> TC Env
envAtFocus TState
ps
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TState -> [Name]
holes TState
ps) = do Goal
g <- Maybe Name -> ProofTerm -> TC Goal
goal (Name -> Maybe Name
forall a. a -> Maybe a
Just ([Name] -> Name
forall a. HasCallStack => [a] -> a
head (TState -> [Name]
holes TState
ps))) (TState -> ProofTerm
pterm TState
ps)
Env -> TC Env
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Env
premises Goal
g)
| Bool
otherwise = String -> TC Env
forall a. String -> TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> TC Env) -> String -> TC Env
forall a b. (a -> b) -> a -> b
$ String
"No holes in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps))
goalAtFocus :: ProofState -> TC (Binder Type)
goalAtFocus :: TState -> TC (Binder Term)
goalAtFocus TState
ps
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TState -> [Name]
holes TState
ps) = do Goal
g <- Maybe Name -> ProofTerm -> TC Goal
goal (Name -> Maybe Name
forall a. a -> Maybe a
Just ([Name] -> Name
forall a. HasCallStack => [a] -> a
head (TState -> [Name]
holes TState
ps))) (TState -> ProofTerm
pterm TState
ps)
Binder Term -> TC (Binder Term)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Binder Term
goalType Goal
g)
| Bool
otherwise = Err -> TC (Binder Term)
forall a. Err -> TC a
Error (Err -> TC (Binder Term))
-> (String -> Err) -> String -> TC (Binder Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> TC (Binder Term)) -> String -> TC (Binder Term)
forall a b. (a -> b) -> a -> b
$ String
"No goal in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
holes TState
ps) String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps))
tactic :: Hole -> RunTactic -> StateT TState TC ()
tactic :: Maybe Name -> RunTactic -> StateT TState TC ()
tactic Maybe Name
h RunTactic
f = do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
(ProofTerm
tm', Bool
_) <- Maybe Name
-> RunTactic
-> Context
-> Env
-> ProofTerm
-> StateT TState TC (ProofTerm, Bool)
forall a.
Maybe Name
-> RunTactic' a
-> Context
-> Env
-> ProofTerm
-> StateT a TC (ProofTerm, Bool)
atHole Maybe Name
h RunTactic
f (TState -> Context
context TState
ps) [] (TState -> ProofTerm
pterm TState
ps)
TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
TState -> StateT TState TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (TState
ps { pterm = tm' })
computeLet :: Context -> Name -> Term -> Term
computeLet :: Context -> Name -> Term -> Term
computeLet Context
ctxt Name
n Term
tm = Env -> Term -> Term
cl [] Term
tm where
cl :: Env -> Term -> Term
cl Env
env (Bind Name
n' (Let RigCount
r Term
t Term
v) Term
sc)
| Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = let v' :: Term
v' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
v in
Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
r Term
t Term
v') Term
sc
cl Env
env (Bind Name
n' Binder Term
b Term
sc) = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((Term -> Term) -> Binder Term -> Binder Term
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> Term -> Term
cl Env
env) Binder Term
b) (Env -> Term -> Term
cl ((Name
n, RigCount
Rig0, Binder Term
b)(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
sc)
cl Env
env (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Env -> Term -> Term
cl Env
env Term
f) (Env -> Term -> Term
cl Env
env Term
a)
cl Env
env Term
t = Term
t
attack :: RunTactic
attack :: RunTactic
attack Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc)
= do Name
h <- String -> StateT TState TC Name
forall (m :: * -> *). Monad m => String -> StateT TState m Name
getName String
"hole"
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = h : holes ps })
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
t (Name -> Term
newtm Name
h)) Term
sc
where
newtm :: Name -> Term
newtm Name
h = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
h (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
h Term
t)
attack Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not an attackable hole"
claim :: Name -> Raw -> RunTactic
claim :: Name -> Raw -> RunTactic
claim Name
n Raw
ty Context
ctxt Env
env Term
t =
do (Term
tyv, Term
tyt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let (Name
g:[Name]
gs) = TState -> [Name]
holes TState
ps in
TState
ps { holes = g : n : gs } )
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Term -> Binder Term
forall b. b -> Binder b
Hole Term
tyv) Term
t
claimFn :: Name -> Name -> Raw -> RunTactic
claimFn :: Name -> Name -> Raw -> RunTactic
claimFn Name
n Name
bn Raw
argty Context
ctxt Env
env t :: Term
t@(Bind Name
x (Hole Term
retty) Term
sc) =
do (Term
tyv, Term
tyt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
argty
TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let (Name
g:[Name]
gs) = TState -> [Name]
holes TState
ps in
TState
ps { holes = g : n : gs } )
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Term -> Binder Term
forall b. b -> Binder b
Hole (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
bn (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing Term
tyv Term
tyt) Term
retty)) Term
t
claimFn Name
_ Name
_ Raw
_ Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't make function type here"
reorder_claims :: RunTactic
reorder_claims :: RunTactic
reorder_claims Context
ctxt Env
env Term
t
=
let ([(Name, Binder Term)]
bs, Term
sc) = Term -> [(Name, Binder Term)] -> ([(Name, Binder Term)], Term)
forall {a}.
TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs Term
t []
newbs :: [(Name, Binder Term)]
newbs = [(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse ([(Name, Binder Term)] -> [(Name, Binder Term)]
sortB ([(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. [a] -> [a]
reverse [(Name, Binder Term)]
bs)) in
Bool -> String -> StateT TState TC Term -> StateT TState TC Term
forall {a}. Bool -> String -> a -> a
traceWhen ([(Name, Binder Term)]
bs [(Name, Binder Term)] -> [(Name, Binder Term)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [(Name, Binder Term)]
newbs) ([(Name, Binder Term)] -> String
forall a. Show a => a -> String
show [(Name, Binder Term)]
bs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n ==> \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Binder Term)] -> String
forall a. Show a => a -> String
show [(Name, Binder Term)]
newbs) (StateT TState TC Term -> StateT TState TC Term)
-> StateT TState TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Binder Term)] -> Term -> Term
forall n. [(n, Binder (TT n))] -> TT n -> TT n
bindAll [(Name, Binder Term)]
newbs Term
sc)
where scvs :: TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs (Bind a
n b :: Binder (TT a)
b@(Hole TT a
_) TT a
sc) [(a, Binder (TT a))]
acc = TT a -> [(a, Binder (TT a))] -> ([(a, Binder (TT a))], TT a)
scvs TT a
sc ((a
n, Binder (TT a)
b)(a, Binder (TT a)) -> [(a, Binder (TT a))] -> [(a, Binder (TT a))]
forall a. a -> [a] -> [a]
:[(a, Binder (TT a))]
acc)
scvs TT a
sc [(a, Binder (TT a))]
acc = ([(a, Binder (TT a))] -> [(a, Binder (TT a))]
forall a. [a] -> [a]
reverse [(a, Binder (TT a))]
acc, TT a
sc)
sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
sortB :: [(Name, Binder Term)] -> [(Name, Binder Term)]
sortB [] = []
sortB ((Name, Binder Term)
x:[(Name, Binder Term)]
xs) | ((Name, Binder Term) -> Bool) -> [(Name, Binder Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Name, Binder Term) -> (Name, Binder Term) -> Bool
forall {n} {b} {a}. Eq n => (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (Name, Binder Term)
x) [(Name, Binder Term)]
xs = (Name, Binder Term)
x (Name, Binder Term)
-> [(Name, Binder Term)] -> [(Name, Binder Term)]
forall a. a -> [a] -> [a]
: [(Name, Binder Term)] -> [(Name, Binder Term)]
sortB [(Name, Binder Term)]
xs
| Bool
otherwise = [(Name, Binder Term)] -> [(Name, Binder Term)]
sortB ((Name, Binder Term)
-> [(Name, Binder Term)] -> [(Name, Binder Term)]
forall {n}.
Eq n =>
(n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (Name, Binder Term)
x [(Name, Binder Term)]
xs)
insertB :: (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (n, Binder (TT n))
x [] = [(n, Binder (TT n))
x]
insertB (n, Binder (TT n))
x ((n, Binder (TT n))
y:[(n, Binder (TT n))]
ys) | ((n, Binder (TT n)) -> Bool) -> [(n, Binder (TT n))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((n, Binder (TT n)) -> (n, Binder (TT n)) -> Bool
forall {n} {b} {a}. Eq n => (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (n, Binder (TT n))
x) ((n, Binder (TT n))
y(n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
:[(n, Binder (TT n))]
ys) = (n, Binder (TT n))
x (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
: (n, Binder (TT n))
y (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
: [(n, Binder (TT n))]
ys
| Bool
otherwise = (n, Binder (TT n))
y (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
forall a. a -> [a] -> [a]
: (n, Binder (TT n)) -> [(n, Binder (TT n))] -> [(n, Binder (TT n))]
insertB (n, Binder (TT n))
x [(n, Binder (TT n))]
ys
noOcc :: (n, b) -> (a, Binder (TT n)) -> Bool
noOcc (n
n, b
_) (a
_, Let RigCount
_ TT n
t TT n
v) = n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
t Bool -> Bool -> Bool
&& n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
v
noOcc (n
n, b
_) (a
_, Guess TT n
t TT n
v) = n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
t Bool -> Bool -> Bool
&& n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n TT n
v
noOcc (n
n, b
_) (a
_, Binder (TT n)
b) = n -> TT n -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence n
n (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
b)
focus :: Name -> RunTactic
focus :: Name -> RunTactic
focus Name
n Context
ctxt Env
env Term
t = do (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
then TState
ps { holes = n : (hs \\ [n]) }
else TState
ps)
TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
movelast :: Name -> RunTactic
movelast :: Name -> RunTactic
movelast Name
n Context
ctxt Env
env Term
t = do (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs
then TState
ps { holes = (hs \\ [n]) ++ [n] }
else TState
ps)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
implementationArg :: Name -> RunTactic
implementationArg :: Name -> RunTactic
implementationArg Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc)
= do (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps
is :: [Name]
is = TState -> [Name]
implementations TState
ps in
TState
ps { holes = (hs \\ [x]) ++ [x],
implementations = x:is })
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) Term
sc)
implementationArg Name
n Context
ctxt Env
env Term
_
= String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The current focus is not a hole."
autoArg :: Name -> RunTactic
autoArg :: Name -> RunTactic
autoArg Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc)
= do (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> case Name
-> [(Name, ([FailContext], [Name]))]
-> Maybe ([FailContext], [Name])
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (TState -> [(Name, ([FailContext], [Name]))]
autos TState
ps) of
Maybe ([FailContext], [Name])
Nothing ->
let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
TState
ps { holes = (hs \\ [x]) ++ [x],
autos = (x, (while_elaborating ps, refsIn t)) : autos ps }
Just ([FailContext], [Name])
_ -> TState
ps)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) Term
sc)
autoArg Name
n Context
ctxt Env
env Term
_
= String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The current focus not a hole."
setinj :: Name -> RunTactic
setinj :: Name -> RunTactic
setinj Name
n Context
ctxt Env
env (Bind Name
x Binder Term
b Term
sc)
= do (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let is :: [Name]
is = TState -> [Name]
injective TState
ps in
TState
ps { injective = n : is })
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x Binder Term
b Term
sc)
defer :: [Name] -> [Name] -> Name -> RunTactic
defer :: [Name] -> [Name] -> Name -> RunTactic
defer [Name]
dropped [Name]
linused Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
nt Name
x' Term
ty)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do let env' :: Env
env' = ((Name, RigCount, Binder Term) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, RigCount
_, Binder Term
t) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
dropped) Env
env
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps in
TState
ps { usedns = n : usedns ps,
holes = hs \\ [x] })
TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Int -> [Name] -> Term -> Binder Term
forall b. Int -> [Name] -> b -> Binder b
GHole (Env -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
env') (TState -> [Name]
psnames TState
ps) (Env -> Term -> Term
mkTy (Env -> Env
forall a. [a] -> [a]
reverse Env
env') Term
t))
(Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty) (((Name, RigCount, Binder Term) -> Term) -> Env -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Term
forall {n} {b}. (n, b, Binder (TT n)) -> TT n
getP (Env -> Env
forall a. [a] -> [a]
reverse Env
env'))))
where
mkTy :: Env -> Term -> Term
mkTy [] Term
t = Term
t
mkTy ((Name
n,RigCount
rig,Binder Term
b) : Env
bs) Term
t = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi (RigCount -> Name -> RigCount
setRig RigCount
rig Name
n) Maybe ImplicitInfo
forall a. Maybe a
Nothing (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (Env -> Term -> Term
mkTy Env
bs Term
t)
setRig :: RigCount -> Name -> RigCount
setRig RigCount
Rig1 Name
n | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
linused = RigCount
Rig0
setRig RigCount
rig Name
n = RigCount
rig
getP :: (n, b, Binder (TT n)) -> TT n
getP (n
n, b
rig, Binder (TT n)
b) = NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
b)
defer [Name]
dropped [Name]
linused Name
n Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't defer a non-hole focus."
deferType :: Name -> Raw -> [Name] -> RunTactic
deferType :: Name -> Raw -> [Name] -> RunTactic
deferType Name
n Raw
fty_in [Name]
args Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
nt Name
x' Term
ty)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do (Term
fty, Term
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
fty_in
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> let hs :: [Name]
hs = TState -> [Name]
holes TState
ps
ds :: [Name]
ds = TState -> [Name]
deferred TState
ps in
TState
ps { holes = hs \\ [x],
deferred = n : ds })
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Int -> [Name] -> Term -> Binder Term
forall b. Int -> [Name] -> b -> Binder b
GHole Int
0 [] Term
fty)
(Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty) ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Term
getP [Name]
args)))
where
getP :: Name -> Term
getP Name
n = case Name -> Env -> Maybe (Binder Term)
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
env of
Just Binder Term
b -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
Maybe (Binder Term)
Nothing -> String -> Term
forall a. HasCallStack => String -> a
error (String
"deferType can't find " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n)
deferType Name
_ Raw
_ [Name]
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't defer a non-hole focus."
unifyGoal :: Raw -> RunTactic
unifyGoal :: Raw -> RunTactic
unifyGoal Raw
tm Context
ctxt Env
env h :: Term
h@(Bind Name
x Binder Term
b Term
sc) =
do (Term
tmv, Term
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
[(Name, Term)]
ns' <- Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b, Maybe Provenance
forall a. Maybe a
Nothing) (Term
tmv, Maybe Provenance
forall a. Maybe a
Nothing)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
h
unifyGoal Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"The focus is not a binder."
unifyTerms :: Raw -> Raw -> RunTactic
unifyTerms :: Raw -> Raw -> RunTactic
unifyTerms Raw
tm1 Raw
tm2 Context
ctxt Env
env Term
h =
do (Term
tm1v, Term
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm1
(Term
tm2v, Term
_) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm2
[(Name, Term)]
ns' <- Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
tm1v, Maybe Provenance
forall a. Maybe a
Nothing) (Term
tm2v, Maybe Provenance
forall a. Maybe a
Nothing)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
h
exact :: Raw -> RunTactic
exact :: Raw -> RunTactic
exact Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do (Term
val, Term
valty) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
valty Term
ty
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
exact Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't fill here."
fill :: Raw -> RunTactic
fill :: Raw -> RunTactic
fill Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do (Term
val, Term
valty) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val)
(Term
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Term -> Term -> Provenance
chkPurpose Term
val Term
ty))
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
where
chkPurpose :: Term -> Term -> Provenance
chkPurpose Term
val (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ (P NameType
_ (MN Int
_ Text
_) Term
_) Term
_) (P NameType
_ (MN Int
_ Text
_) Term
_))
= Term -> Provenance
TooManyArgs Term
val
chkPurpose Term
_ Term
_ = Provenance
ExpectedType
fill Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't fill here."
match_fill :: Raw -> RunTactic
match_fill :: Raw -> RunTactic
match_fill Raw
guess Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do (Term
val, Term
valty) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val)
(Term
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
ExpectedType)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
match_fill Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't fill here."
prep_fill :: Name -> [Name] -> RunTactic
prep_fill :: Name -> [Name] -> RunTactic
prep_fill Name
f [Name]
as Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do let val :: Term
val = Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
f Term
forall n. TT n
Erased) ((Name -> Term) -> [Name] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
forall n. TT n
Erased) [Name]
as)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
prep_fill Name
f [Name]
as Context
ctxt Env
env Term
t = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT TState TC Term)
-> String -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ String
"Can't prepare fill at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t
complete_fill :: RunTactic
complete_fill :: RunTactic
complete_fill Context
ctxt Env
env (Bind Name
x (Guess Term
ty Term
val) Term
sc) =
do let guess :: Raw
guess = Term -> Raw
forget Term
val
(Term
val', Term
valty) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
guess
Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
valty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just (Provenance -> Maybe Provenance) -> Provenance -> Maybe Provenance
forall a b. (a -> b) -> a -> b
$ Term -> Provenance
SourceTerm Term
val')
(Term
ty, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
ExpectedType)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
ty Term
val) Term
sc
complete_fill Context
ctxt Env
env Term
t = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT TState TC Term)
-> String -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ String
"Can't complete fill at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t
solve :: RunTactic
solve :: RunTactic
solve Context
ctxt Env
env (Bind Name
x (Guess Term
ty Term
val) Term
sc)
= do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
[Name]
dropdots <-
case Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
x (TState -> [(Name, Term)]
notunified TState
ps) of
Just (P NameType
_ Name
h Term
_)
| Name
h Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x -> [Name] -> StateT TState TC [Name]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Just Term
tm ->
do Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
match_unify' Context
ctxt Env
env (Term
tm, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
InferredVal)
(Term
val, Provenance -> Maybe Provenance
forall a. a -> Maybe a
Just Provenance
GivenVal)
[Name] -> StateT TState TC [Name]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name
x]
Maybe Term
_ -> [Name] -> StateT TState TC [Name]
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
holes ps \\ [x],
solved = Just (x, val),
dontunify = filter (/= x) (dontunify ps),
notunified = updateNotunified [(x,val)]
(notunified ps),
recents = x : recents ps,
implementations = implementations ps \\ [x],
dotted = dropUnified dropdots (dotted ps) })
let (Term
locked, Bool
_) = [Name] -> Term -> (Term, Bool)
tryLock (TState -> [Name]
holes TState
ps [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
x]) (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x Term
val Term
sc) in
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
locked
where dropUnified :: t a -> [(a, t a)] -> [(a, t a)]
dropUnified t a
ddots [] = []
dropUnified t a
ddots ((a
x, t a
es) : [(a, t a)]
ds)
| a
x a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ddots Bool -> Bool -> Bool
|| (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\a
e -> a
e a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ddots) t a
es
= t a -> [(a, t a)] -> [(a, t a)]
dropUnified t a
ddots [(a, t a)]
ds
| Bool
otherwise = (a
x, t a
es) (a, t a) -> [(a, t a)] -> [(a, t a)]
forall a. a -> [a] -> [a]
: t a -> [(a, t a)] -> [(a, t a)]
dropUnified t a
ddots [(a, t a)]
ds
tryLock :: [Name] -> Term -> (Term, Bool)
tryLock :: [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs tm :: Term
tm@(App AppStatus Name
Complete Term
_ Term
_) = (Term
tm, Bool
True)
tryLock [Name]
hs tm :: Term
tm@(App AppStatus Name
s Term
f Term
a) =
let (Term
f', Bool
fl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
f
(Term
a', Bool
al) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
a in
if Bool
fl Bool -> Bool -> Bool
&& Bool
al then (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Term
f' Term
a', Bool
True)
else (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Term
f' Term
a', Bool
False)
tryLock [Name]
hs t :: Term
t@(P NameType
_ Name
n Term
_) = (Term
t, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs)
tryLock [Name]
hs t :: Term
t@(Bind Name
n (Hole Term
_) Term
sc) = (Term
t, Bool
False)
tryLock [Name]
hs t :: Term
t@(Bind Name
n (Guess Term
_ Term
_) Term
sc) = (Term
t, Bool
False)
tryLock [Name]
hs t :: Term
t@(Bind Name
n (Let RigCount
r Term
ty Term
val) Term
sc)
= let (Term
ty', Bool
tyl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
ty
(Term
val', Bool
vall) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
val
(Term
sc', Bool
scl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
sc in
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
r Term
ty' Term
val') Term
sc', Bool
tyl Bool -> Bool -> Bool
&& Bool
vall Bool -> Bool -> Bool
&& Bool
scl)
tryLock [Name]
hs t :: Term
t@(Bind Name
n Binder Term
b Term
sc)
= let (Term
bt', Bool
btl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
(Term
sc', Bool
scl) = [Name] -> Term -> (Term, Bool)
tryLock [Name]
hs Term
sc in
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Binder Term
b { binderTy = bt' }) Term
sc', Bool
btl Bool -> Bool -> Bool
&& Bool
scl)
tryLock [Name]
hs Term
t = (Term
t, Bool
True)
solve Context
_ Env
_ h :: Term
h@(Bind Name
x Binder Term
t Term
sc)
= do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
case Name -> Term -> Maybe Name
forall {a}. Eq a => a -> TT a -> Maybe a
findType Name
x Term
sc of
Just Name
t -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
CantInferType (Name -> String
forall a. Show a => a -> String
show Name
t))
Maybe Name
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Term -> Err
forall t. t -> Err' t
IncompleteTerm Term
h)
where findType :: a -> TT a -> Maybe a
findType a
x (Bind a
n (Let RigCount
r TT a
t TT a
v) TT a
sc)
= a -> TT a -> Maybe a
findType a
x TT a
v Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` a -> TT a -> Maybe a
findType a
x TT a
sc
findType a
x (Bind a
n Binder (TT a)
t TT a
sc)
| P NameType
_ a
x' TT a
_ <- Binder (TT a) -> TT a
forall b. Binder b -> b
binderTy Binder (TT a)
t, a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' = a -> Maybe a
forall a. a -> Maybe a
Just a
n
| Bool
otherwise = a -> TT a -> Maybe a
findType a
x TT a
sc
findType a
x TT a
_ = Maybe a
forall a. Maybe a
Nothing
introTy :: Raw -> Maybe Name -> RunTactic
introTy :: Raw -> Maybe Name -> RunTactic
introTy Raw
ty Maybe Name
mn Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do let n :: Name
n = case Maybe Name
mn of
Just Name
name -> Name
name
Maybe Name
Nothing -> Name
x
let t' :: Term
t' = case Term
t of
x :: Term
x@(Bind Name
y (Pi RigCount
_ Maybe ImplicitInfo
_ Term
s Term
_) Term
_) -> Term
x
Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
t
(Term
tyv, Term
tyt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
case Term
t' of
Bind Name
y (Pi RigCount
rig Maybe ImplicitInfo
_ Term
s Term
_) Term
t -> let t' :: Term
t' = Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t in
do Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
s, Maybe Provenance
forall a. Maybe a
Nothing) (Term
tyv, Maybe Provenance
forall a. Maybe a
Nothing)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
tyv) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t') (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
Term
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Err -> TC Term) -> Err -> TC Term
forall a b. (a -> b) -> a -> b
$ Term -> Err
forall t. t -> Err' t
CantIntroduce Term
t'
introTy Raw
ty Maybe Name
n Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't introduce here."
intro :: Maybe Name -> RunTactic
intro :: Maybe Name -> RunTactic
intro Maybe Name
mn Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do let t' :: Term
t' = case Term
t of
x :: Term
x@(Bind Name
y (Pi RigCount
_ Maybe ImplicitInfo
_ Term
s Term
_) Term
_) -> Term
x
Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
t
case Term
t' of
Bind Name
y (Pi RigCount
rig Maybe ImplicitInfo
_ Term
s Term
_) Term
t ->
let n :: Name
n = case Maybe Name
mn of
Just Name
name -> Name
name
Maybe Name
Nothing -> Name
y
t' :: Term
t' = Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
y (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t
in Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
s) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t') (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
Term
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Err -> TC Term) -> Err -> TC Term
forall a b. (a -> b) -> a -> b
$ Term -> Err
forall t. t -> Err' t
CantIntroduce Term
t'
intro Maybe Name
n Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't introduce here."
forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
forAll Name
n RigCount
rig Maybe ImplicitInfo
impl Raw
ty Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do (Term
tyv, Term
tyt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
tyt, Maybe Provenance
forall a. Maybe a
Nothing) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), Maybe Provenance
forall a. Maybe a
Nothing)
Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> StateT TState TC [(Name, Term)]
unify' Context
ctxt Env
env (Term
t, Maybe Provenance
forall a. Maybe a
Nothing) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0), Maybe Provenance
forall a. Maybe a
Nothing)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
impl Term
tyv (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t))
forAll Name
n RigCount
rig Maybe ImplicitInfo
impl Raw
ty Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't pi bind here"
patvar :: Name -> RunTactic
patvar :: Name -> RunTactic
patvar Name
n Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc) =
do (TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
holes ps \\ [x],
solved = Just (x, P Bound n t),
dontunify = filter (/=x) (dontunify ps),
notunified = updateNotunified [(x,P Bound n t)]
(notunified ps),
injective = addInj n x (injective ps)
})
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
PVar RigCount
RigW Term
t) (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
x (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
t) Term
sc)
where addInj :: a -> a -> [a] -> [a]
addInj a
n a
x [a]
ps | a
x a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ps = a
n a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ps
| Bool
otherwise = [a]
ps
patvar Name
n Context
ctxt Env
env Term
tm = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT TState TC Term)
-> String -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ String
"Can't add pattern var at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm
letbind :: Name -> RigCount -> Raw -> Raw -> RunTactic
letbind :: Name -> RigCount -> Raw -> Raw -> RunTactic
letbind Name
n RigCount
rig Raw
ty Raw
val Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do (Term
tyv, Term
tyt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
ty
(Term
valv, Term
valt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
val
TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tyt
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Term
tyv Term
valv) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t) (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t))
letbind Name
n RigCount
rig Raw
ty Raw
val Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't let bind here"
expandLet :: Name -> Term -> RunTactic
expandLet :: Name -> Term -> RunTactic
expandLet Name
n Term
v Context
ctxt Env
env Term
tm =
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
n Term
v Term
tm
rewrite :: Raw -> RunTactic
rewrite :: Raw -> RunTactic
rewrite Raw
tm Context
ctxt Env
env (Bind Name
x (Hole Term
t) xp :: Term
xp@(P NameType
_ Name
x' Term
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do (Term
tmv, Term
tmt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
let tmt' :: Term
tmt' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
tmt
case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tmt' of
(P NameType
_ (UN Text
q) Term
_, [Term
lt,Term
rt,Term
l,Term
r]) | Text
q Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"=" ->
do let p :: Term
p = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
rname (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW Term
lt) (Term -> Term -> Term -> Term -> Term
mkP (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
rname Term
lt) Term
r Term
l Term
t)
let newt :: Term
newt = Term -> Term -> Term -> Term -> Term
mkP Term
l Term
r Term
l Term
t
let sc :: Raw
sc = Term -> Raw
forget (Term -> Raw) -> Term -> Raw
forall a b. (a -> b) -> a -> b
$ (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
newt)
(Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"replace") (UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)))
[Term
lt, Term
l, Term
r, Term
p, Term
tmv, Term
xp]))
(Term
scv, Term
sct) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
sc
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
scv
(Term, [Term])
_ -> TC Term -> StateT TState TC Term
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Term -> StateT TState TC Term)
-> TC Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Err -> TC Term
forall a. Err -> TC a
tfail (Term -> Term -> Err
forall t. t -> t -> Err' t
NotEquality Term
tmv Term
tmt')
where rname :: Name
rname = Int -> String -> Name
sMN Int
0 String
"replaced"
rewrite Raw
_ Context
_ Env
_ Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't rewrite here"
mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
mkP :: Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
ty | Term
l Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
ty = Term
lt
mkP Term
lt Term
l Term
r (App AppStatus Name
s Term
f Term
a) = let f' :: Term
f' = if (Term
r Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
f) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
f else Term
f
a' :: Term
a' = if (Term
r Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
a) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
a else Term
a in
AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Term
f' Term
a'
mkP Term
lt Term
l Term
r (Bind Name
n Binder Term
b Term
sc)
= let b' :: Binder Term
b' = Binder Term -> Binder Term
mkPB Binder Term
b
sc' :: Term
sc' = if (Term
r Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
sc) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
sc else Term
sc in
Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b' Term
sc'
where mkPB :: Binder Term -> Binder Term
mkPB (Let RigCount
c Term
t Term
v) = let t' :: Term
t' = if (Term
r Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
t) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
t else Term
t
v' :: Term
v' = if (Term
r Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
v) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
v else Term
v in
RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
c Term
t' Term
v'
mkPB Binder Term
b = let ty :: Term
ty = Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b
ty' :: Term
ty' = if (Term
r Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Term
ty) then Term -> Term -> Term -> Term -> Term
mkP Term
lt Term
l Term
r Term
ty else Term
ty in
Binder Term
b { binderTy = ty' }
mkP Term
lt Term
l Term
r Term
x = Term
x
equiv :: Raw -> RunTactic
equiv :: Raw -> RunTactic
equiv Raw
tm Context
ctxt Env
env (Bind Name
x (Hole Term
t) Term
sc) =
do (Term
tmv, Term
tmt) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
TC () -> StateT TState TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT TState TC ()) -> TC () -> StateT TState TC ()
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
tmv Term
t
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
tmv) Term
sc
equiv Raw
tm Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't equiv here"
patbind :: Name -> RigCount -> RunTactic
patbind :: Name -> RigCount -> RunTactic
patbind Name
n RigCount
rig Context
ctxt Env
env (Bind Name
x (Hole Term
t) (P NameType
_ Name
x' Term
_)) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' =
do let t' :: Term
t' = case Term
t of
x :: Term
x@(Bind Name
y (PVTy Term
s) Term
t) -> Term
x
Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
t
case Term
t' of
Bind Name
y (PVTy Term
s) Term
t -> let t' :: Term
t' = Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
updsubst Name
y (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
s) Term
t in
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
PVar RigCount
rig Term
s) (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
t') (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
x Term
t'))
Term
_ -> String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Nothing to pattern bind"
patbind Name
n RigCount
_ Context
ctxt Env
env Term
_ = String -> StateT TState TC Term
forall a. String -> StateT TState TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't pattern bind here"
compute :: RunTactic
compute :: RunTactic
compute Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
ty)) Term
sc
compute Context
ctxt Env
env Term
t = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
whnf_compute :: RunTactic
whnf_compute :: RunTactic
whnf_compute Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do let ty' :: Term
ty' = Context -> Env -> Term -> Term
whnf Context
ctxt Env
env Term
ty in
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
ty') Term
sc
whnf_compute Context
ctxt Env
env Term
t = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
whnf_compute_args :: RunTactic
whnf_compute_args :: RunTactic
whnf_compute_args Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do let ty' :: Term
ty' = Context -> Env -> Term -> Term
whnfArgs Context
ctxt Env
env Term
ty in
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole Term
ty') Term
sc
whnf_compute_args Context
ctxt Env
env Term
t = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
simplify :: RunTactic
simplify :: RunTactic
simplify Context
ctxt Env
env (Bind Name
x (Hole Term
ty) Term
sc) =
do Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT TState TC Term) -> Term -> StateT TState TC Term
forall a b. (a -> b) -> a -> b
$ Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (Term -> Binder Term
forall b. b -> Binder b
Hole ((Term, [(Name, Int)]) -> Term
forall a b. (a, b) -> a
fst (Context -> Env -> [(Name, Int)] -> Term -> (Term, [(Name, Int)])
specialise Context
ctxt Env
env [] Term
ty))) Term
sc
simplify Context
ctxt Env
env Term
t = Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
check_in :: Raw -> RunTactic
check_in :: Raw -> RunTactic
check_in Raw
t Context
ctxt Env
env Term
tm =
do (Term
val, Term
valty) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
t
String -> StateT TState TC ()
forall (m :: * -> *). Monad m => String -> StateT TState m ()
addLog (Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty)
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm
eval_in :: Raw -> RunTactic
eval_in :: Raw -> RunTactic
eval_in Raw
t Context
ctxt Env
env Term
tm =
do (Term
val, Term
valty) <- TC (Term, Term) -> StateT TState TC (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT TState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT TState TC (Term, Term))
-> TC (Term, Term) -> StateT TState TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
t
let val' :: Term
val' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
val
let valty' :: Term
valty' = Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
valty
String -> StateT TState TC ()
forall (m :: * -> *). Monad m => String -> StateT TState m ()
addLog (Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
" ==>\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
val' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
valty')
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm
start_unify :: Name -> RunTactic
start_unify :: Name -> RunTactic
start_unify Name
n Context
ctxt Env
env Term
tm = do
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm
solve_unified :: RunTactic
solve_unified :: RunTactic
solve_unified Context
ctxt Env
env Term
tm =
do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
let (Name
_, [(Name, Term)]
ns) = TState -> (Name, [(Name, Term)])
unified TState
ps
let unify :: [(Name, Term)]
unify = [Name] -> [(Name, Term)] -> [Name] -> [(Name, Term)]
forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (TState -> [Name]
dontunify TState
ps) [(Name, Term)]
ns (TState -> [Name]
holes TState
ps)
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
holes ps \\ map fst unify,
recents = recents ps ++ map fst unify })
(TState -> TState) -> StateT TState TC ()
forall (m :: * -> *).
Monad m =>
(TState -> TState) -> StateT TState m ()
action (\TState
ps -> TState
ps { pterm = updateSolved unify (pterm ps) })
Term -> StateT TState TC Term
forall a. a -> StateT TState TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
unify Term
tm)
dropGiven :: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [] t a
hs = []
dropGiven t a
du ((a
n, P NameType
Bound a
t TT a
ty) : [(a, TT a)]
us) t a
hs
| a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du Bool -> Bool -> Bool
&& Bool -> Bool
not (a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
Bool -> Bool -> Bool
&& a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs
= (a
t, NameType -> a -> TT a -> TT a
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound a
n TT a
ty) (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [(a, TT a)]
us t a
hs
dropGiven t a
du (u :: (a, TT a)
u@(a
n, TT a
_) : [(a, TT a)]
us) t a
hs
| a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du = t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [(a, TT a)]
us t a
hs
dropGiven t a
du ((a, TT a)
u : [(a, TT a)]
us) t a
hs = (a, TT a)
u (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven t a
du [(a, TT a)]
us t a
hs
keepGiven :: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [] t a
hs = []
keepGiven t a
du ((a
n, P NameType
Bound a
t TT a
ty) : [(a, TT a)]
us) t a
hs
| a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du Bool -> Bool -> Bool
&& Bool -> Bool
not (a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du)
Bool -> Bool -> Bool
&& a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& a
t a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs
= t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [(a, TT a)]
us t a
hs
keepGiven t a
du (u :: (a, TT a)
u@(a
n, TT a
_) : [(a, TT a)]
us) t a
hs
| a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
du = (a, TT a)
u (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [(a, TT a)]
us t a
hs
keepGiven t a
du ((a, TT a)
u : [(a, TT a)]
us) t a
hs = t a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven t a
du [(a, TT a)]
us t a
hs
updateEnv :: [(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [] [(a, b, f Term)]
e = [(a, b, f Term)]
e
updateEnv [(Name, Term)]
ns [] = []
updateEnv [(Name, Term)]
ns ((a
n, b
rig, f Term
b) : [(a, b, f Term)]
env)
= (a
n, b
rig, (Term -> Term) -> f Term -> f Term
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns) f Term
b) (a, b, f Term) -> [(a, b, f Term)] -> [(a, b, f Term)]
forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns [(a, b, f Term)]
env
updateProv :: [(Name, Term)] -> Provenance -> Provenance
updateProv [(Name, Term)]
ns (SourceTerm Term
t) = Term -> Provenance
SourceTerm (Term -> Provenance) -> Term -> Provenance
forall a b. (a -> b) -> a -> b
$ [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
t
updateProv [(Name, Term)]
ns Provenance
p = Provenance
p
updateError :: [(Name, Term)] -> Err -> Err
updateError [] Err
err = Err
err
updateError [(Name, Term)]
ns (At FC
f Err
e) = FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
f ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e)
updateError [(Name, Term)]
ns (Elaborating String
s Name
n Maybe Term
ty Err
e) = String -> Name -> Maybe Term -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
s Name
n Maybe Term
ty ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e)
updateError [(Name, Term)]
ns (ElaboratingArg Name
f Name
a [(Name, Name)]
env Err
e)
= Name -> Name -> [(Name, Name)] -> Err -> Err
forall t. Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
ElaboratingArg Name
f Name
a [(Name, Name)]
env ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e)
updateError [(Name, Term)]
ns (CantUnify Bool
b (Term
l,Maybe Provenance
lp) (Term
r,Maybe Provenance
rp) Err
e [(Name, Term)]
xs Int
sc)
= Bool
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> Err
-> [(Name, Term)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
b ([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
l, (Provenance -> Provenance) -> Maybe Provenance -> Maybe Provenance
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Provenance -> Provenance
updateProv [(Name, Term)]
ns) Maybe Provenance
lp)
([(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
r, (Provenance -> Provenance) -> Maybe Provenance -> Maybe Provenance
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, Term)] -> Provenance -> Provenance
updateProv [(Name, Term)]
ns) Maybe Provenance
rp) ([(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
e) [(Name, Term)]
xs Int
sc
updateError [(Name, Term)]
ns Err
e = Err
e
mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified Env
env [Name]
holes [(Name, Term)]
ns = [(Name, Term)]
-> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
forall {a} {t} {a}.
(Eq a, Eq t) =>
[(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [(Name, Term)]
ns [] [] where
mnu :: [(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [] [(a, t)]
ns_acc [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc = ([(a, t)] -> [(a, t)]
forall a. [a] -> [a]
reverse [(a, t)]
ns_acc, [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
forall a. [a] -> [a]
reverse [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc)
mnu ((a
n, t
t):[(a, t)]
ns) [(a, t)]
ns_acc [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc
| Just t
t' <- a -> [(a, t)] -> Maybe t
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, t)]
ns, t
t t -> t -> Bool
forall a. Eq a => a -> a -> Bool
/= t
t'
= [(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [(a, t)]
ns ((a
n,t
t') (a, t) -> [(a, t)] -> [(a, t)]
forall a. a -> [a] -> [a]
: [(a, t)]
ns_acc)
((t
t,t
t',Bool
True, Env
env,Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
True (t
t, Maybe Provenance
forall a. Maybe a
Nothing) (t
t', Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' t
forall t. String -> Err' t
Msg String
"") [] Int
0, [],FailAt
Match) (t, t, Bool, Env, Err' t, [a], FailAt)
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
forall a. a -> [a] -> [a]
: [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc)
| Bool
otherwise = [(a, t)]
-> [(a, t)]
-> [(t, t, Bool, Env, Err' t, [a], FailAt)]
-> ([(a, t)], [(t, t, Bool, Env, Err' t, [a], FailAt)])
mnu [(a, t)]
ns ((a
n,t
t) (a, t) -> [(a, t)] -> [(a, t)]
forall a. a -> [a] -> [a]
: [(a, t)]
ns_acc) [(t, t, Bool, Env, Err' t, [a], FailAt)]
ps_acc
updateNotunified :: [(Name, Term)] -> [(a, Term)] -> [(a, Term)]
updateNotunified [] [(a, Term)]
nu = [(a, Term)]
nu
updateNotunified [(Name, Term)]
ns [(a, Term)]
nu = [(a, Term)] -> [(a, Term)]
forall {a}. [(a, Term)] -> [(a, Term)]
up [(a, Term)]
nu where
up :: [(a, Term)] -> [(a, Term)]
up [] = []
up ((a
n, Term
t) : [(a, Term)]
nus) = let t' :: Term
t' = [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
t in
((a
n, Term
t') (a, Term) -> [(a, Term)] -> [(a, Term)]
forall a. a -> [a] -> [a]
: [(a, Term)] -> [(a, Term)]
up [(a, Term)]
nus)
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance (CantUnify Bool
_ (Term
_, Maybe Provenance
lp) (Term
_, Maybe Provenance
rp) Err
_ [(Name, Term)]
_ Int
_) = (Maybe Provenance
lp, Maybe Provenance
rp)
getProvenance Err
_ = (Maybe Provenance
forall a. Maybe a
Nothing, Maybe Provenance
forall a. Maybe a
Nothing)
setReady :: (a, b, c, d, e, f, g) -> (a, b, Bool, d, e, f, g)
setReady (a
x, b
y, c
_, d
env, e
err, f
c, g
at) = (a
x, b
y, Bool
True, d
env, e
err, f
c, g
at)
updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
-> ([(Name, TT Name)], Fails)
updateProblems :: TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps [(Name, Term)]
updates Fails
probs = Integer -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
forall {t} {g}.
(Eq t, Num t) =>
t
-> [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
rec Integer
10 [(Name, Term)]
updates Fails
probs
where
rec :: t
-> [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
rec t
0 [(Name, Term)]
us [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs = ([(Name, Term)]
us, [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs)
rec t
n [(Name, Term)]
us [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs = case [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
forall {g}.
[(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
us [] [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs of
res :: ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res@([(Name, Term)]
_, []) -> ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res
res :: ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res@([(Name, Term)]
us', [(Term, Term, Bool, Env, Err, [FailContext], g)]
_) | [(Name, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Term)]
us' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Name, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Term)]
us -> ([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
res
([(Name, Term)]
us', [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs') -> t
-> [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
rec (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) [(Name, Term)]
us' [(Term, Term, Bool, Env, Err, [FailContext], g)]
fs'
hs :: [Name]
hs = TState -> [Name]
holes TState
ps
inj :: [Name]
inj = TState -> [Name]
injective TState
ps
ctxt :: Context
ctxt = TState -> Context
context TState
ps
ulog :: Bool
ulog = TState -> Bool
unifylog TState
ps
usupp :: [Name]
usupp = ((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst (TState -> [(Name, Term)]
notunified TState
ps)
dont :: [Name]
dont = TState -> [Name]
dontunify TState
ps
up :: [(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
ns [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc [] = ([(Name, Term)]
ns, ((Term, Term, Bool, Env, Err, [FailContext], g)
-> (Term, Term, Bool, Env, Err, [FailContext], g))
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Term)]
-> (Term, Term, Bool, Env, Err, [FailContext], g)
-> (Term, Term, Bool, Env, Err, [FailContext], g)
forall {f :: * -> *} {c} {a} {b} {f} {g}.
Functor f =>
[(Name, Term)]
-> (Term, Term, c, [(a, b, f Term)], Err, f, g)
-> (Term, Term, Bool, [(a, b, f Term)], Err, f, g)
updateNs [(Name, Term)]
ns) ([(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
forall a. [a] -> [a]
reverse [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc))
up [(Name, Term)]
ns [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc (prob :: (Term, Term, Bool, Env, Err, [FailContext], g)
prob@(Term
x, Term
y, Bool
ready, Env
env, Err
err, [FailContext]
while, g
um) : [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps) =
let (Term
x', Bool
newx) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
x
(Term
y', Bool
newy) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
y
(Maybe Provenance
lp, Maybe Provenance
rp) = Err -> (Maybe Provenance, Maybe Provenance)
getProvenance Err
err
err' :: Err
err' = [(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
err
env' :: Env
env' = [(Name, Term)] -> Env -> Env
forall {f :: * -> *} {a} {b}.
Functor f =>
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns Env
env in
if Bool
newx Bool -> Bool -> Bool
|| Bool
newy Bool -> Bool -> Bool
|| Bool
ready Bool -> Bool -> Bool
||
(Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
n -> Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj) (Term -> [Name]
refsIn Term
x [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Term -> [Name]
refsIn Term
y) then
case Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, Term)], Fails)
unify Context
ctxt Env
env' (Term
x', Maybe Provenance
lp) (Term
y', Maybe Provenance
rp) [Name]
inj [Name]
hs [Name]
usupp [FailContext]
while of
OK ([(Name, Term)]
v, []) -> Bool
-> String
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"DID " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Term, Term, Bool, [(Name, Term)], [Name]) -> String
forall a. Show a => a -> String
show (Term
x',Term
y',Bool
ready,[(Name, Term)]
v,[Name]
dont)) (([(Name, Term)], [(Term, Term, Bool, Env, Err, [FailContext], g)])
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)]))
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
forall a b. (a -> b) -> a -> b
$
let v' :: [(Name, Term)]
v' = ((Name, Term) -> Bool) -> [(Name, Term)] -> [(Name, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, Term
_) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
dont) [(Name, Term)]
v in
[(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
up ([(Name, Term)]
ns [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
v') [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps
TC ([(Name, Term)], Fails)
e ->
[(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
ns ((Term
x',Term
y',Bool
False,Env
env',Err
err',[FailContext]
while,g
um) (Term, Term, Bool, Env, Err, [FailContext], g)
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
forall a. a -> [a] -> [a]
: [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc) [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps
else
[(Name, Term)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> ([(Name, Term)],
[(Term, Term, Bool, Env, Err, [FailContext], g)])
up [(Name, Term)]
ns ((Term
x',Term
y', Bool
False, Env
env',Err
err', [FailContext]
while, g
um) (Term, Term, Bool, Env, Err, [FailContext], g)
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
-> [(Term, Term, Bool, Env, Err, [FailContext], g)]
forall a. a -> [a] -> [a]
: [(Term, Term, Bool, Env, Err, [FailContext], g)]
acc) [(Term, Term, Bool, Env, Err, [FailContext], g)]
ps
updateNs :: [(Name, Term)]
-> (Term, Term, c, [(a, b, f Term)], Err, f, g)
-> (Term, Term, Bool, [(a, b, f Term)], Err, f, g)
updateNs [(Name, Term)]
ns (Term
x, Term
y, c
t, [(a, b, f Term)]
env, Err
err, f
fc, g
fa)
= let (Term
x', Bool
newx) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
x
(Term
y', Bool
newy) = [(Name, Term)] -> Term -> (Term, Bool)
updateSolvedTerm' [(Name, Term)]
ns Term
y in
(Term
x', Term
y', Bool
newx Bool -> Bool -> Bool
|| Bool
newy,
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
forall {f :: * -> *} {a} {b}.
Functor f =>
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns [(a, b, f Term)]
env, [(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
err, f
fc, g
fa)
orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved :: [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved [(Name, Term)]
ns ProofTerm
tm = [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update [] [(Name, Term)]
ns ProofTerm
tm
where
update :: [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update [Name]
done [] ProofTerm
t = (ProofTerm
t, [Name]
done)
update [Name]
done ((Name
n, P NameType
_ Name
n' Term
_) : [(Name, Term)]
ns) ProofTerm
t | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update [Name]
done [(Name, Term)]
ns ProofTerm
t
update [Name]
done ((Name, Term)
n : [(Name, Term)]
ns) ProofTerm
t = [Name] -> [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
update ((Name, Term) -> Name
forall a b. (a, b) -> a
fst (Name, Term)
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
done)
(((Name, Term) -> (Name, Term)) -> [(Name, Term)] -> [(Name, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Term) -> (Name, Term) -> (Name, Term)
forall {a}. (Name, Term) -> (a, Term) -> (a, Term)
updateMatch (Name, Term)
n) [(Name, Term)]
ns)
([(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)
n] ProofTerm
t)
updateMatch :: (Name, Term) -> (a, Term) -> (a, Term)
updateMatch (Name, Term)
n (a
x, Term
tm) = (a
x, [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)
n] Term
tm)
matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
-> ([(Name, TT Name)], Fails)
matchProblems :: Bool
-> TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all TState
ps [(Name, Term)]
updates Fails
probs = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
updates Fails
probs where
hs :: [Name]
hs = TState -> [Name]
holes TState
ps
inj :: [Name]
inj = TState -> [Name]
injective TState
ps
ctxt :: Context
ctxt = TState -> Context
context TState
ps
up :: [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
ns [] = ([(Name, Term)]
ns, [])
up [(Name, Term)]
ns ((Term
x, Term
y, Bool
ready, Env
env, Err
err, [FailContext]
while, FailAt
um) : Fails
ps)
| Bool
all Bool -> Bool -> Bool
|| FailAt
um FailAt -> FailAt -> Bool
forall a. Eq a => a -> a -> Bool
== FailAt
Match =
let x' :: Term
x' = [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
x
y' :: Term
y' = [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
y
(Maybe Provenance
lp, Maybe Provenance
rp) = Err -> (Maybe Provenance, Maybe Provenance)
getProvenance Err
err
err' :: Err
err' = [(Name, Term)] -> Err -> Err
updateError [(Name, Term)]
ns Err
err
env' :: Env
env' = [(Name, Term)] -> Env -> Env
forall {f :: * -> *} {a} {b}.
Functor f =>
[(Name, Term)] -> [(a, b, f Term)] -> [(a, b, f Term)]
updateEnv [(Name, Term)]
ns Env
env in
case Context
-> Env
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, Term)]
match_unify Context
ctxt Env
env' (Term
x', Maybe Provenance
lp) (Term
y', Maybe Provenance
rp) [Name]
inj [Name]
hs [FailContext]
while of
OK [(Name, Term)]
v ->
[(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up ([(Name, Term)]
ns [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
forall a. [a] -> [a] -> [a]
++ [(Name, Term)]
v) Fails
ps
TC [(Name, Term)]
_ -> let ([(Name, Term)]
ns', Fails
ps') = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
ns Fails
ps in
([(Name, Term)]
ns', (Term
x', Term
y', Bool
True, Env
env', Err
err', [FailContext]
while, FailAt
um) (Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
ps')
up [(Name, Term)]
ns ((Term, Term, Bool, Env, Err, [FailContext], FailAt)
p : Fails
ps) = let ([(Name, Term)]
ns', Fails
ps') = [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
up [(Name, Term)]
ns Fails
ps in
([(Name, Term)]
ns', (Term, Term, Bool, Env, Err, [FailContext], FailAt)
p (Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
ps')
processTactic :: Tactic -> ProofState -> TC (ProofState, String)
processTactic :: Tactic -> TState -> TC (TState, String)
processTactic Tactic
QED TState
ps = case TState -> [Name]
holes TState
ps of
[] -> do let tm :: Term
tm = ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps)
(Term
tm', Term
ty', UCs
_) <- String -> Context -> Env -> Raw -> Term -> TC (Term, Term, UCs)
recheck (TState -> String
constraint_ns TState
ps) (TState -> Context
context TState
ps) [] (Term -> Raw
forget Term
tm) Term
tm
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps { done = True, pterm = mkProofTerm tm' },
String
"Proof complete: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv [] Term
tm')
[Name]
_ -> String -> TC (TState, String)
forall a. String -> TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Still holes to fill."
processTactic Tactic
ProofState TState
ps = (TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps, Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv [] (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps)))
processTactic Tactic
Undo TState
ps = case TState -> Maybe TState
previous TState
ps of
Maybe TState
Nothing -> Err -> TC (TState, String)
forall a. Err -> TC a
Error (Err -> TC (TState, String))
-> (String -> Err) -> String -> TC (TState, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> TC (TState, String)) -> String -> TC (TState, String)
forall a b. (a -> b) -> a -> b
$ String
"Nothing to undo."
Just TState
pold -> (TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
pold, String
"")
processTactic Tactic
EndUnify TState
ps
= let (Name
h, [(Name, Term)]
ns_in) = TState -> (Name, [(Name, Term)])
unified TState
ps
ns :: [(Name, Term)]
ns = [Name] -> [(Name, Term)] -> [Name] -> [(Name, Term)]
forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (TState -> [Name]
dontunify TState
ps) [(Name, Term)]
ns_in (TState -> [Name]
holes TState
ps)
ns' :: [(Name, Term)]
ns' = ((Name, Term) -> (Name, Term)) -> [(Name, Term)] -> [(Name, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
n, Term
t) -> (Name
n, [(Name, Term)] -> Term -> Term
updateSolvedTerm [(Name, Term)]
ns Term
t)) [(Name, Term)]
ns
([(Name, Term)]
ns'', Fails
probs') = TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps [(Name, Term)]
ns' (TState -> Fails
problems TState
ps)
tm' :: ProofTerm
tm' = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)]
ns'' (TState -> ProofTerm
pterm TState
ps) in
Bool -> String -> TC (TState, String) -> TC (TState, String)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps) (String
"(EndUnify) Dropping holes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
ns'')) (TC (TState, String) -> TC (TState, String))
-> TC (TState, String) -> TC (TState, String)
forall a b. (a -> b) -> a -> b
$
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps { pterm = tm',
unified = (h, []),
problems = probs',
notunified = updateNotunified ns'' (notunified ps),
recents = recents ps ++ map fst ns'',
holes = holes ps \\ map fst ns'' }, String
"")
processTactic Tactic
UnifyAll TState
ps
= let tm' :: ProofTerm
tm' = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved (TState -> [(Name, Term)]
notunified TState
ps) (TState -> ProofTerm
pterm TState
ps) in
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps { pterm = tm',
notunified = [],
recents = recents ps ++ map fst (notunified ps),
holes = holes ps \\ map fst (notunified ps) }, String
"")
processTactic (Reorder Name
n) TState
ps
= do TState
ps' <- StateT TState TC () -> TState -> TC TState
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Maybe Name -> RunTactic -> StateT TState TC ()
tactic (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n) RunTactic
reorder_claims) TState
ps
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps' { previous = Just ps, plog = "" }, TState -> String
plog TState
ps')
processTactic (ComputeLet Name
n) TState
ps
= (TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps { pterm = mkProofTerm $
computeLet (context ps) n
(getProofTerm (pterm ps)) }, String
"")
processTactic Tactic
UnifyProblems TState
ps
= do let ([(Name, Term)]
ns', Fails
probs') = TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps [] (((Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> (Term, Term, Bool, Env, Err, [FailContext], FailAt))
-> Fails -> Fails
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> (Term, Term, Bool, Env, Err, [FailContext], FailAt)
forall {a} {b} {c} {d} {e} {f} {g}.
(a, b, c, d, e, f, g) -> (a, b, Bool, d, e, f, g)
setReady (TState -> Fails
problems TState
ps))
(ProofTerm
pterm', [Name]
dropped) = [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved [(Name, Term)]
ns' (TState -> ProofTerm
pterm TState
ps)
Bool -> String -> TC (TState, String) -> TC (TState, String)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps) (String
"(UnifyProblems) Dropping holes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
dropped) (TC (TState, String) -> TC (TState, String))
-> TC (TState, String) -> TC (TState, String)
forall a b. (a -> b) -> a -> b
$
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps { pterm = pterm', solved = Nothing, problems = probs',
previous = Just ps, plog = "",
notunified = updateNotunified ns' (notunified ps),
recents = recents ps ++ dropped,
dotted = filter (notIn ns') (dotted ps),
holes = holes ps \\ dropped }, TState -> String
plog TState
ps)
where notIn :: [(a, b)] -> (a, b) -> Bool
notIn [(a, b)]
ns (a
h, b
_) = a
h a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst [(a, b)]
ns
processTactic (MatchProblems Bool
all) TState
ps
= do let ([(Name, Term)]
ns', Fails
probs') = Bool
-> TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all TState
ps [] (((Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> (Term, Term, Bool, Env, Err, [FailContext], FailAt))
-> Fails -> Fails
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term, Bool, Env, Err, [FailContext], FailAt)
-> (Term, Term, Bool, Env, Err, [FailContext], FailAt)
forall {a} {b} {c} {d} {e} {f} {g}.
(a, b, c, d, e, f, g) -> (a, b, Bool, d, e, f, g)
setReady (TState -> Fails
problems TState
ps))
([(Name, Term)]
ns'', Fails
probs'') = Bool
-> TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
matchProblems Bool
all TState
ps [(Name, Term)]
ns' Fails
probs'
(ProofTerm
pterm', [Name]
dropped) = [(Name, Term)] -> ProofTerm -> (ProofTerm, [Name])
orderUpdateSolved [(Name, Term)]
ns'' (ProofTerm -> ProofTerm
resetProofTerm (TState -> ProofTerm
pterm TState
ps))
Bool -> String -> TC (TState, String) -> TC (TState, String)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps) (String
"(MatchProblems) Dropping holes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
dropped) (TC (TState, String) -> TC (TState, String))
-> TC (TState, String) -> TC (TState, String)
forall a b. (a -> b) -> a -> b
$
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps { pterm = pterm', solved = Nothing, problems = probs'',
previous = Just ps, plog = "",
notunified = updateNotunified ns'' (notunified ps),
recents = recents ps ++ dropped,
holes = holes ps \\ dropped }, TState -> String
plog TState
ps)
processTactic Tactic
t TState
ps
= case TState -> [Name]
holes TState
ps of
[] -> case Tactic
t of
Focus Name
_ -> (TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps, String
"")
Tactic
_ -> String -> TC (TState, String)
forall a. String -> TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> TC (TState, String)) -> String -> TC (TState, String)
forall a b. (a -> b) -> a -> b
$ String
"Proof done, nothing to run tactic on: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Tactic -> String
forall a. Show a => a -> String
show Tactic
t String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (ProofTerm -> Term
getProofTerm (TState -> ProofTerm
pterm TState
ps))
(Name
h:[Name]
_) -> do TState
ps' <- StateT TState TC () -> TState -> TC TState
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Tactic -> Name -> StateT TState TC ()
process Tactic
t Name
h) TState
ps
let ([(Name, Term)]
ns_in, Fails
probs')
= case TState -> Maybe (Name, Term)
solved TState
ps' of
Just (Name, Term)
s -> Bool
-> String -> ([(Name, Term)], Fails) -> ([(Name, Term)], Fails)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"SOLVED " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Name, Term) -> String
forall a. Show a => a -> String
show (Name, Term)
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
dontunify TState
ps')) (([(Name, Term)], Fails) -> ([(Name, Term)], Fails))
-> ([(Name, Term)], Fails) -> ([(Name, Term)], Fails)
forall a b. (a -> b) -> a -> b
$
TState -> [(Name, Term)] -> Fails -> ([(Name, Term)], Fails)
updateProblems TState
ps' [(Name, Term)
s] (TState -> Fails
problems TState
ps')
Maybe (Name, Term)
_ -> ([], TState -> Fails
problems TState
ps')
let ns' :: [(Name, Term)]
ns' = [Name] -> [(Name, Term)] -> [Name] -> [(Name, Term)]
forall {a} {t :: * -> *} {t :: * -> *}.
(Eq a, Foldable t, Foldable t) =>
t a -> [(a, TT a)] -> t a -> [(a, TT a)]
dropGiven (TState -> [Name]
dontunify TState
ps') [(Name, Term)]
ns_in (TState -> [Name]
holes TState
ps')
let pterm'' :: ProofTerm
pterm'' = [(Name, Term)] -> ProofTerm -> ProofTerm
updateSolved [(Name, Term)]
ns' (TState -> ProofTerm
pterm TState
ps')
Bool -> String -> TC (TState, String) -> TC (TState, String)
forall {a}. Bool -> String -> a -> a
traceWhen (TState -> Bool
unifylog TState
ps)
(String
"Updated problems after solve " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fails -> String
qshow Fails
probs' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"(Toplevel) Dropping holes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
forall a b. (a, b) -> a
fst [(Name, Term)]
ns') String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"Holes were: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (TState -> [Name]
holes TState
ps')) (TC (TState, String) -> TC (TState, String))
-> TC (TState, String) -> TC (TState, String)
forall a b. (a -> b) -> a -> b
$
(TState, String) -> TC (TState, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TState
ps' { pterm = pterm'',
solved = Nothing,
problems = probs',
notunified = updateNotunified ns' (notunified ps'),
previous = Just ps, plog = "",
recents = recents ps' ++ map fst ns',
holes = holes ps' \\ (map fst ns')
}, TState -> String
plog TState
ps')
process :: Tactic -> Name -> StateT TState TC ()
process :: Tactic -> Name -> StateT TState TC ()
process Tactic
EndUnify Name
_
= do TState
ps <- StateT TState TC TState
forall s (m :: * -> *). MonadState s m => m s
get
let (Name
h, [(Name, Term)]
_) = TState -> (Name, [(Name, Term)])
unified TState
ps
Maybe Name -> RunTactic -> StateT TState TC ()
tactic (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
h) RunTactic
solve_unified
process Tactic
t Name
h = Maybe Name -> RunTactic -> StateT TState TC ()
tactic (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
h) (Tactic -> RunTactic
mktac Tactic
t)
where mktac :: Tactic -> RunTactic
mktac Tactic
Attack = RunTactic
attack
mktac (Claim Name
n Raw
r) = Name -> Raw -> RunTactic
claim Name
n Raw
r
mktac (ClaimFn Name
n Name
bn Raw
r) = Name -> Name -> Raw -> RunTactic
claimFn Name
n Name
bn Raw
r
mktac (Exact Raw
r) = Raw -> RunTactic
exact Raw
r
mktac (Fill Raw
r) = Raw -> RunTactic
fill Raw
r
mktac (MatchFill Raw
r) = Raw -> RunTactic
match_fill Raw
r
mktac (PrepFill Name
n [Name]
ns) = Name -> [Name] -> RunTactic
prep_fill Name
n [Name]
ns
mktac Tactic
CompleteFill = RunTactic
complete_fill
mktac Tactic
Solve = RunTactic
solve
mktac (StartUnify Name
n) = Name -> RunTactic
start_unify Name
n
mktac Tactic
Compute = RunTactic
compute
mktac Tactic
Simplify = RunTactic
Idris.Core.ProofState.simplify
mktac Tactic
WHNF_Compute = RunTactic
whnf_compute
mktac Tactic
WHNF_ComputeArgs = RunTactic
whnf_compute_args
mktac (Intro Maybe Name
n) = Maybe Name -> RunTactic
intro Maybe Name
n
mktac (IntroTy Raw
ty Maybe Name
n) = Raw -> Maybe Name -> RunTactic
introTy Raw
ty Maybe Name
n
mktac (Forall Name
n RigCount
r Maybe ImplicitInfo
i Raw
t) = Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic
forAll Name
n RigCount
r Maybe ImplicitInfo
i Raw
t
mktac (LetBind Name
n RigCount
r Raw
t Raw
v) = Name -> RigCount -> Raw -> Raw -> RunTactic
letbind Name
n RigCount
r Raw
t Raw
v
mktac (ExpandLet Name
n Term
b) = Name -> Term -> RunTactic
expandLet Name
n Term
b
mktac (Rewrite Raw
t) = Raw -> RunTactic
rewrite Raw
t
mktac (Equiv Raw
t) = Raw -> RunTactic
equiv Raw
t
mktac (PatVar Name
n) = Name -> RunTactic
patvar Name
n
mktac (PatBind Name
n RigCount
rig) = Name -> RigCount -> RunTactic
patbind Name
n RigCount
rig
mktac (CheckIn Raw
r) = Raw -> RunTactic
check_in Raw
r
mktac (EvalIn Raw
r) = Raw -> RunTactic
eval_in Raw
r
mktac (Focus Name
n) = Name -> RunTactic
focus Name
n
mktac (Defer [Name]
ns [Name]
ls Name
n) = [Name] -> [Name] -> Name -> RunTactic
defer [Name]
ns [Name]
ls Name
n
mktac (DeferType Name
n Raw
t [Name]
a) = Name -> Raw -> [Name] -> RunTactic
deferType Name
n Raw
t [Name]
a
mktac (Implementation Name
n)= Name -> RunTactic
implementationArg Name
n
mktac (AutoArg Name
n) = Name -> RunTactic
autoArg Name
n
mktac (SetInjective Name
n) = Name -> RunTactic
setinj Name
n
mktac (MoveLast Name
n) = Name -> RunTactic
movelast Name
n
mktac (UnifyGoal Raw
r) = Raw -> RunTactic
unifyGoal Raw
r
mktac (UnifyTerms Raw
x Raw
y) = Raw -> Raw -> RunTactic
unifyTerms Raw
x Raw
y