@@ -112,7 +112,8 @@ elab ist info pattern tcgen fn tm
112112 elab' ina (PResolveTC fc)
113113 | pattern = do c <- unique_hole (MN 0 "c")
114114 instanceArg c
115− | otherwise = try (resolveTC 2 fn ist)
115+ | otherwise = do g <- goal
116+ try (resolveTC 2 fn ist)
116117 (do c <- unique_hole (MN 0 "c")
117118 instanceArg c)
118119 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -147,9 +148,7 @@ elab ist info pattern tcgen fn tm
147148 ctxt <- get_context
148149 let (tc, _) = unApply ty
149150 let as' = pruneByType tc ctxt as
150− let as'' = as' -- pruneAlt as'
151− try (tryAll (zip (map (elab' ina) as'') (map showHd as'')))
152− (tryAll (zip (map (elab' ina) as') (map showHd as')))
151+ tryAll (zip (map (elab' ina) as') (map showHd as'))
153152 where showHd (PApp _ h _) = show h
154153 showHd x = show x
155154 elab' ina (PAlternative False as)
@@ -290,24 +289,26 @@ elab ist info pattern tcgen fn tm
290289 ctxt <- get_context
291290 let guarded = isConName Nothing f ctxt
292291-- when True
293− tryWhen True
292+ (ns, committed) <- tryWhen True
294293 (do ns <- apply (Var f) (map isph args)
295− let (ns', eargs)
296− = unzip $
294+ return (ns, True)) -- commit to this branch here
295+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
296+ mkSpecialised ist fc f (map getTm args') tm
297+ solve
298+ return ([], False))
299+ when committed $
300+ do let (ns', eargs) = unzip $
297301 sortBy (\(_,x) (_,y) ->
298302 compare (priority x) (priority y))
299303 (zip ns args)
300− try
301− (elabArgs (ina || not isinf, guarded)
302− [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
303− (elabArgs (ina || not isinf, guarded)
304− [] False (reverse ns')
305− (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))
306− mkSpecialised ist fc f (map getTm args') tm
307− solve)
308− (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
309− mkSpecialised ist fc f (map getTm args') tm
310− solve)
304+ tryWhen True
305+ (elabArgs (ina || not isinf, guarded)
306+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
307+ (elabArgs (ina || not isinf, guarded)
308+ [] False (reverse ns')
309+ (map (\x -> (lazyarg x, getTm x)) (reverse eargs)))
310+ mkSpecialised ist fc f (map getTm args') tm
311+ solve
311312-- ptm <- get_term
312313-- elog (show ptm)
313314 ivs' <- get_instances
@@ -405,10 +406,10 @@ elab ist info pattern tcgen fn tm
405406 failed' <- -- trace (show (n, t, hs, tm)) $
406407 case n `elem` hs of
407408 True ->
408− if r
409− then try (do focus n; elabE ina t; return failed)
410− (return ((n,(lazy, t)):failed))
411− else do focus n; elabE ina t; return failed
409+-- if r
410+-- then try (do focus n; elabE ina t; return failed)
411+-- (return ((n,(lazy, t)):failed))
412+ do focus n; elabE ina t; return failed
412413 False -> return failed
413414 elabArgs ina failed r ns args
414415
@@ -459,17 +460,17 @@ pruneByType (P _ n _) c as
459460pruneByType t _ as = as
460461
461462trivial :: IState -> ElabD ()
462−trivial ist = try (do elab ist toplevel False False (MN 0 "tac")
463+trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")
463464 (PRefl (FC "prf" 0) Placeholder)
464− return ())
465− (do env <- get_env
466− tryAll (map fst env)
467− return ())
465+ return ())
466+ (do env <- get_env
467+ tryAll (map fst env)
468+ return ()) True
468469 where
469470 tryAll [] = fail "No trivial solution"
470− tryAll (x:xs) = try (elab ist toplevel False False
471+ tryAll (x:xs) = try' (elab ist toplevel False False
471472 (MN 0 "tac") (PRef (FC "prf" 0) x))
472− (tryAll xs)
473+ (tryAll xs) True
473474
474475findInstances :: IState -> Term -> [Name]
475476findInstances ist t
@@ -481,19 +482,19 @@ findInstances ist t
481482
482483resolveTC :: Int -> Name -> IState -> ElabD ()
483484resolveTC 0 fn ist = fail $ "Can't resolve type class"
484−resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)
485+resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True
485486resolveTC depth fn ist
486487 = do hnf_compute
487− try (trivial ist)
488− (do t <- goal
489− let insts = findInstances ist t
490− let (tc, ttypes) = unApply t
491− scopeOnly <- needsDefault t tc ttypes
492− tm <- get_term
488+ try' (trivial ist)
489+ (do t <- goal
490+ let insts = findInstances ist t
491+ let (tc, ttypes) = unApply t
492+ scopeOnly <- needsDefault t tc ttypes
493+ tm <- get_term
493494-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
494495-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
495− let depth' = if scopeOnly then 2 else depth
496− blunderbuss t depth' insts)
496+ let depth' = if scopeOnly then 2 else depth
497+ blunderbuss t depth' insts) True
497498 where
498499 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
499500 | otherwise = (fail "Can't resolve", show n)
@@ -512,8 +513,8 @@ resolveTC depth fn ist
512513
513514 blunderbuss t d [] = lift $ tfail $ CantResolve t
514515 blunderbuss t d (n:ns)
515− | n /= fn && tcname n = try (resolve n d)
516− (blunderbuss t d ns)
516+ | n /= fn && tcname n = try' (resolve n d)
517+ (blunderbuss t d ns) True
517518 | otherwise = blunderbuss t d ns
518519
519520 resolve n depth
@@ -570,8 +571,8 @@ runTac autoSolve ist tac = do env <- get_env
570571 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
571572 runT Intros = do g <- goal
572573 attack; intro (bname g)
573− try (runT Intros)
574− (return ())
574+ try' (runT Intros)
575+ (return ()) True
575576 where
576577 bname (Bind n _ _) = Just n
577578 bname _ = Nothing
@@ -653,6 +654,13 @@ runTac autoSolve ist tac = do env <- get_env
653654-- trace (show p ++ "\n\n") $
654655 return ()
655656 where tacticTy = tacm "Tactic"
657+ runT (GoalType n tac) = do g <- goal
658+ case unApply g of
659+ (P _ n' _, _) ->
660+ if nsroot n' == UN n
661+ then runT tac
662+ else fail "Wrong goal type"
663+ _ -> fail "Wrong goal type"
656664 runT x = fail $ "Not implemented " ++ show x
657665
658666 runReflected t = do t' <- reify t
@@ -670,6 +678,8 @@ runTac autoSolve ist tac = do env <- get_env
670678 reifyAp t [Constant (Str x)]
671679 | t == tacm "Refine" = return $ Refine (UN x) []
672680 reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)
681+ reifyAp t [Constant (Str n), x]
682+ | t == tacm "GoalType" = liftM (GoalType n) (reify x)
673683 reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
674684
675685solveAll = try (do solve; solveAll) (return ())