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