cb92598 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification tweak

cb92598Edwin Brady14 years ago

lib/prelude/nat.idr+1−2

compare with master

unifiedsplit

@@ -813,7 +813,7 @@ plusLeftLeftRightZeroStepCase = proof {

813plusRightCancelStepCase = proof {

814 intros;

815 refine inductiveHypothesis;

816− refine succInjective;

816+ refine succInjective _ _ ?;

817 rewrite sym (plusSuccRightSucc left right);

818 rewrite sym (plusSuccRightSucc left' right);

819 rewrite p;

@@ -840,4 +840,3 @@ plusLeftCancelBaseCase = proof {

840 rewrite p;

841 trivial;

842}

843−

src/Core/Elaborate.hs+13−5

@@ -317,16 +317,24 @@ apply fn imps =

317 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

318 -- so do nothing

319 ptm <- get_term

320+ let dontunify = if null imps then [] -- do all we can

321+ else

320− let dontunify = [] -- map fst (filter (not.snd) (zip args (map fst imps)))

322+ map fst (filter (not.snd) (zip args (map fst imps)))

321 ES (p, a) s prev <- get

323 ES (p, a) s prev <- get

322− let (n, hs) = unified p

324+ let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dontunify)) $

323− let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

325+ unified p

326+ let unify = dropGiven dontunify hs

324− put (ES (p { unified = unify }, a) s prev)

327+ put (ES (p { unified = (n, unify) }, a) s prev)

325 end_unify

328 end_unify

326− return (map (updateUnify hs) args)

329+ return (map (updateUnify unify) args)

327 where updateUnify hs n = case lookup n hs of

330 where updateUnify hs n = case lookup n hs of

328 Just (P _ t _) -> t

331 Just (P _ t _) -> t

329 _ -> n

332 _ -> n

333+ dropGiven du [] = []

334+ dropGiven du ((n, P a t ty) : us) | n `elem` du && not (t `elem` du)

335+ = (t, P a n ty) : dropGiven du us

336+ dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us

337+ dropGiven du (u : us) = u : dropGiven du us

330

338

331apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

339apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

332apply2 fn elabs =

340apply2 fn elabs =

src/Idris/ElabTerm.hs+1−1

@@ -504,7 +504,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

504 return (fn, a)

505 -- FIXME: resolve ambiguities

506 [(n, args)] -> return $ (n, map isImp args)

507− ns <- apply (Var fn') (map (\x -> (x,0)) imps)

507+ ns <- apply (Var fn') (map (\x -> (x, 0)) imps)

508 when autoSolve solveAll

509 where isImp (PImp _ _ _ _) = True

510 isImp _ = False