558d226 · Idris-dev · git.iko.soy

src/Core/ProofState.hs+5−4

compare with master

unifiedsplit

@@ -460,14 +460,15 @@ processTactic Undo ps = case previous ps of

460 Just pold -> return (pold, "")

461processTactic EndUnify ps

462 = let (h, ns) = unified ps

463+ ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

463− tm' = updateSolved ns (pterm ps)

464+ tm' = updateSolved ns' (pterm ps)

464− probs' = updateProblems ns (problems ps) in

465+ probs' = updateProblems ns' (problems ps) in

465 case probs' of

466 case probs' of

466 [] -> return (ps { pterm = tm',

467 [] -> return (ps { pterm = tm',

467 unified = (h, []),

468 unified = (h, []),

468− injective = map (tmap (updateSolved ns))

469+ injective = map (tmap (updateSolved ns'))

469 (injective ps),

470 (injective ps),

470− holes = holes ps \\ map fst ns }, "")

471+ holes = holes ps \\ map fst ns' }, "")

471 errs@((_,_,_,err):_) -> tfail err

472 errs@((_,_,_,err):_) -> tfail err

472processTactic (Reorder n) ps

473processTactic (Reorder n) ps

473 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

474 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

src/Idris/AbsSyntax.hs+1−1

@@ -1105,7 +1105,7 @@ aiFn ist fc f as

1105 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1106 [] -> if f `elem` idris_metavars ist

1107 then PApp fc (PRef fc f) as

1108− else mkPApp fc 1 (PRef fc f) as

1108+ else mkPApp fc (length as) (PRef fc f) as

1109 alts -> PAlternative $

1110 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1111 (insertImpl ns as)) alts

src/Idris/ElabTerm.hs+3−1

@@ -279,7 +279,9 @@ elab ist info pattern tcgen fn tm

279 | otherwise = elabArg n t

280 where elabArg n t

281 = do hs <- get_holes

282+ tm <- get_term

283+ failed' <- -- trace (show (n, t, hs, tm)) $

282− failed' <- case n `elem` hs of

284+ case n `elem` hs of

283 True ->

285 True ->

284 if r

286 if r

285 then try (do focus n; elabE ina t; return failed)

287 then try (do focus n; elabE ina t; return failed)