@@ -29,7 +29,7 @@ data ProofState = PS { thname :: Name,
2929 unified :: (Name, [(Name, Term)]),
3030 solved :: Maybe (Name, Term),
3131 problems :: Fails,
32− injective :: [(Term, Term, Term)],
32+ injective :: [Name],
3333 deferred :: [Name], -- names we'll need to define
3434 instances :: [Name], -- instance arguments (for type classes)
3535 previous :: Maybe ProofState, -- for undo
@@ -68,6 +68,7 @@ data Tactic = Attack
6868 | Defer Name
6969 | DeferType Name Raw [Name]
7070 | Instance Name
71+ | SetInjective Name
7172 | MoveLast Name
7273 | ProofState
7374 | Undo
@@ -148,15 +149,28 @@ hole _ = False
148149
149150holeName i = MN i "hole"
150151
152+qshow :: Fails -> String
153+qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
154+
151155unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]
152−unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy
153− addInj inj
154− case fails of
155− [] -> return u
156− err ->
157− do ps <- get
158− put (ps { problems = err ++ problems ps })
159− return []
156+unify' ctxt env topx topy =
157+ do ps <- get
158+ (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)
159+-- trace ("Unified " ++ show (topx, topy) ++ show (injective ps) ++
160+-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
161+-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps)) $
162+ case fails of
163+-- [] -> return u
164+ err ->
165+ do ps <- get
166+ let (h, ns) = unified ps
167+ let (ns', probs') = updateProblems (context ps) (u ++ ns)
168+ (err ++ problems ps)
169+ (injective ps)
170+ (holes ps)
171+ put (ps { problems = probs',
172+ unified = (h, ns') })
173+ return u
160174
161175getName :: Monad m => String -> StateT TState m Name
162176getName tag = do ps <- get
@@ -194,6 +208,7 @@ goalAtFocus :: ProofState -> TC (Binder Type)
194208goalAtFocus ps
195209 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
196210 return (goalType g)
211+ | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
197212
198213goal :: Hole -> Term -> TC Goal
199214goal h tm = g [] tm where
@@ -288,6 +303,12 @@ instanceArg n ctxt env (Bind x (Hole t) sc)
288303 instances = x:is })
289304 return (Bind x (Hole t) sc)
290305
306+setinj :: Name -> RunTactic
307+setinj n ctxt env (Bind x (Hole t) sc)
308+ = do action (\ps -> let is = injective ps in
309+ ps { injective = n : is })
310+ return (Bind x (Hole t) sc)
311+
291312defer :: Name -> RunTactic
292313defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
293314 do action (\ps -> let hs = holes ps in
@@ -322,10 +343,6 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
322343 return sc
323344regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
324345
325−addInj :: [(Term, Term, Term)] -> StateT TState TC ()
326−addInj inj = do ps <- get
327− put (ps { injective = inj ++ injective ps })
328−
329346exact :: Raw -> RunTactic
330347exact guess ctxt env (Bind x (Hole ty) sc) =
331348 do (val, valty) <- lift $ check ctxt env guess
@@ -344,7 +361,7 @@ fill guess ctxt env (Bind x (Hole ty) sc) =
344361 ns <- unify' ctxt env valty ty
345362 ps <- get
346363 let (uh, uns) = unified ps
347− put (ps { unified = (uh, uns ++ ns) })
364+-- put (ps { unified = (uh, uns ++ ns) })
348365-- addLog (show (uh, uns ++ ns))
349366 return $ Bind x (Guess ty val) sc
350367fill _ _ _ _ = fail "Can't fill here."
@@ -362,22 +379,25 @@ complete_fill ctxt env (Bind x (Guess ty val) sc) =
362379 ns <- unify' ctxt env valty ty
363380 ps <- get
364381 let (uh, uns) = unified ps
365− put (ps { unified = (uh, uns ++ ns) })
382+-- put (ps { unified = (uh, uns ++ ns) })
366383 return $ Bind x (Guess ty val) sc
367384complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
368385
369386solve :: RunTactic
370387solve ctxt env (Bind x (Guess ty val) sc)
371− | pureTerm val = do ps <- get
388+ | True = do ps <- get
372389 let (uh, uns) = unified ps
373390 action (\ps -> ps { holes = holes ps \\ [x],
374391 solved = Just (x, val),
392+-- problems = solveInProblems
393+-- x val (problems ps),
375394 -- dontunify = dontunify ps \\ [x],
376395 -- unified = (uh, uns ++ [(x, val)]),
377396 instances = instances ps \\ [x] })
378397 return $ {- Bind x (Let ty val) sc -}
379398 instantiate val (pToV x sc)
380− | otherwise = lift $ tfail $ IncompleteTerm val
399+ | otherwise = do ps <- get
400+ lift $ tfail $ IncompleteTerm val
381401solve _ _ h = do ps <- get
382402 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
383403
@@ -396,7 +416,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
396416 do ns <- unify' ctxt env s tyv
397417 ps <- get
398418 let (uh, uns) = unified ps
399− put (ps { unified = (uh, uns ++ ns) })
419+-- put (ps { unified = (uh, uns ++ ns) })
400420 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
401421 _ -> fail "Nothing to introduce"
402422introTy ty n ctxt env _ = fail "Can't introduce here."
@@ -494,7 +514,8 @@ hnf_compute ctxt env (Bind x (Hole ty) sc) =
494514 do let ty' = hnf ctxt env ty in
495515-- trace ("HNF " ++ show (ty, ty')) $
496516 return $ Bind x (Hole ty') sc
497−
517+hnf_compute ctxt env t = return t
518+
498519check_in :: Raw -> RunTactic
499520check_in t ctxt env tm =
500521 do (val, valty) <- lift $ check ctxt env t
@@ -515,7 +536,7 @@ eval_in t ctxt env tm =
515536 return tm
516537
517538start_unify :: Name -> RunTactic
518−start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
539+start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
519540 return tm
520541
521542tmap f (a, b, c) = (f a, b, c)
@@ -524,22 +545,24 @@ solve_unified :: RunTactic
524545solve_unified ctxt env tm =
525546 do ps <- get
526547 let (_, ns) = unified ps
527− let unify = dropGiven (dontunify ps) ns
548+ let unify = dropGiven (dontunify ps) ns (holes ps)
528549 action (\ps -> ps { holes = holes ps \\ map fst unify })
529550 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
530− action (\ps -> ps { injective = map (tmap (updateSolved unify)) (injective ps) })
531551 return (updateSolved unify tm)
532552 where
533553
534−dropGiven du [] = []
535−dropGiven du ((n, P Bound t ty) : us) | n `elem` du && not (t `elem` du)
536− = (t, P Bound n ty) : dropGiven du us
537−dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us
554+dropGiven du [] hs = []
555+dropGiven du ((n, P Bound t ty) : us) hs
556+ | n `elem` du && not (t `elem` du)
557+ && n `elem` hs && t `elem` hs
558+ = (t, P Bound n ty) : dropGiven du us hs
559+dropGiven du (u@(n, _) : us) hs
560+ | n `elem` du = dropGiven du us hs
538561-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
539−dropGiven du (u : us) = u : dropGiven du us
562+dropGiven du (u : us) hs = u : dropGiven du us hs
540563
541564updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
542− updateSolved' xs x
565+ updateSolved' xs x
543566updateSolved' xs (Bind n (Hole ty) t)
544567 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
545568updateSolved' xs (Bind n b t)
@@ -549,11 +572,30 @@ updateSolved' xs (P _ n _)
549572 | Just v <- lookup n xs = v
550573updateSolved' xs t = t
551574
552−updateProblems ns [] = []
553−updateProblems ns ((x, y, env, err) : ps) =
575+updateEnv ns [] = []
576+updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
577+
578+updateError ns (CantUnify b l r e xs sc)
579+ = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
580+updateError ns e = e
581+
582+solveInProblems x val [] = []
583+solveInProblems x val ((l, r, env, err) : ps)
584+ = ((instantiate val (pToV x l), instantiate val (pToV x r),
585+ updateEnv [(x, val)] env, err) : solveInProblems x val ps)
586+
587+updateProblems ctxt ns ps inj holes = up ns ps where
588+ up ns [] = (ns, [])
589+ up ns ((x, y, env, err) : ps) =
554590 let x' = updateSolved ns x
555− y' = updateSolved ns y in
556− (x',y',env,err) : updateProblems ns ps
591+ y' = updateSolved ns y
592+ err' = updateError ns err
593+ env' = updateEnv ns env in
594+ case unify ctxt env' x' y' inj holes of
595+ OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
596+ up (ns ++ v) ps
597+ _ -> let (ns', ps') = up ns ps in
598+ (ns', (x',y',env',err') : ps')
557599
558600processTactic :: Tactic -> ProofState -> TC (ProofState, String)
559601processTactic QED ps = case holes ps of
@@ -568,18 +610,16 @@ processTactic Undo ps = case previous ps of
568610 Just pold -> return (pold, "")
569611processTactic EndUnify ps
570612 = let (h, ns_in) = unified ps
571− ns = dropGiven (dontunify ps) ns_in
613+ ns = dropGiven (dontunify ps) ns_in (holes ps)
572614 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
573− tm' = -- trace ("Updating " ++ show ns') $ -- ++ " in " ++ show (pterm ps)) $
574− updateSolved ns' (pterm ps)
575− probs' = updateProblems ns' (problems ps) in
576− case probs' of
577− [] -> return (ps { pterm = tm',
578− unified = (h, []),
579− injective = map (tmap (updateSolved ns'))
580− (injective ps),
581− holes = holes ps \\ map fst ns' }, "")
582− errs@((_,_,_,err):_) -> tfail err
615+ (ns'', probs') = updateProblems (context ps) ns' (problems ps)
616+ (injective ps) (holes ps)
617+ tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
618+ updateSolved ns'' (pterm ps) in
619+ return (ps { pterm = tm',
620+ unified = (h, []),
621+ problems = probs',
622+ holes = holes ps \\ map fst ns'' }, "")
583623processTactic (Reorder n) ps
584624 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
585625 return (ps' { previous = Just ps, plog = "" }, plog ps')
@@ -590,9 +630,21 @@ processTactic t ps
590630 let pterm' = case solved ps' of
591631 Just s -> updateSolved [s] (pterm ps')
592632 _ -> pterm ps'
593− return (ps' { pterm = pterm',
633+ let (ns', probs')
634+ = case solved ps' of
635+ Just s -> updateProblems (context ps')
636+ [s] (problems ps')
637+ (injective ps')
638+ (holes ps')
639+ _ -> ([], problems ps')
640+ -- rechecking problems may find more solutions, so
641+ -- apply them here
642+ let pterm'' = updateSolved ns' pterm'
643+ return (ps' { pterm = pterm'',
594644 solved = Nothing,
595− previous = Just ps, plog = "" }, plog ps')
645+ problems = probs',
646+ previous = Just ps, plog = "",
647+ holes = holes ps' \\ (map fst ns')}, plog ps')
596648
597649process :: Tactic -> Name -> StateT TState TC ()
598650process EndUnify _
@@ -624,5 +676,6 @@ process t h = tactic (Just h) (mktac t)
624676 mktac (Defer n) = defer n
625677 mktac (DeferType n t a) = deferType n t a
626678 mktac (Instance n) = instanceArg n
679+ mktac (SetInjective n) = setinj n
627680 mktac (MoveLast n) = movelast n
628681