88f88eb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unification tweak; better disambiguation

Fixes #963. Do alternatives after normal arguments so that more type information is available. (Ideally, order shouldn't matter - would be better to retry alternative resolution if there were still ambiguities at the end, but this will be fiddly to set up as things currently are.)

commit88f88ebcfb685324feace25bcebc0c1f9e791fcc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 10 Mar 2014, 16:29 (13 years ago) parenta7e6550

3 files changed+22−5

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+2−1 src/Idris/Core/Unify.hs+4−2 src/Idris/ElabTerm.hs+16−2

src/Idris/Core/ProofState.hs+2−1

@@ -491,7 +491,8 @@ solve ctxt env (Bind x (Guess ty val) sc)

491491 = do ps <- get

492492 let (uh, uns) = unified ps

493493 case lookup x (notunified ps) of

494− Just tm -> match_unify' ctxt env tm val

494+ Just tm -> -- trace ("NEED MATCH: " ++ show (tm, val)) $

495+ match_unify' ctxt env tm val

495496 _ -> return []

496497 action (\ps -> ps { holes = holes ps \\ [x],

497498 solved = Just (x, val),

src/Idris/Core/Unify.hs+4−2

@@ -372,8 +372,8 @@ unify ctxt env topx topy inj holes =

372372

373373 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

374374 | (injectiveApp fx && injectiveApp fy)

375− || (injectiveApp fx && rigid appx && metavarApp appy)

376− || (injectiveApp fy && rigid appy && metavarApp appx)

375+ || (injectiveApp fx && rigid appx && metavarApp appy && numArgs appx == numArgs appy)

376+ || (injectiveApp fy && rigid appy && metavarApp appx && numArgs appx == numArgs appy)

377377 || (injectiveApp fx && metavarApp fy && ax == ay)

378378 || (injectiveApp fy && metavarApp fx && ax == ay)

379379 = do let (headx, _) = unApply fx

@@ -418,6 +418,8 @@ unify ctxt env topx topy inj holes =

418418 vs <- combine bnames as as'

419419 unArgs vs xs ys

420420

421+ numArgs tm = let (f, args) = unApply tm in length args

422+

421423 metavarApp tm = let (f, args) = unApply tm in

422424 (metavar f &&

423425 all (\x -> metavarApp x) args

src/Idris/ElabTerm.hs+16−2

@@ -72,8 +72,11 @@ build ist info pattern opts fn tm

7272 tm <- get_term

7373 ctxt <- get_context

7474 probs <- get_probs

75+ u <- getUnifyLog

7576

76− when (not pattern) $ do matchProblems True; unifyProblems

77+ when (not pattern) $

78+ traceWhen u ("Remaining problems:\n" ++ show probs) $

79+ do matchProblems True; unifyProblems

7780 probs <- get_probs

7881 case probs of

7982 [] -> return ()

@@ -458,6 +461,8 @@ elab ist info pattern opts fn tm

458461-- trace ("ns is " ++ show ns) $ return ()

459462 -- mark any type class arguments as injective

460463 mapM_ checkIfInjective (map snd ns)

464+ unifyProblems -- try again with the new information,

465+ -- to help with disambiguation

461466 -- Sort so that the implicit tactics and alternatives go last

462467 let (ns', eargs) = unzip $

463468 sortBy cmpArg (zip ns args)

@@ -480,12 +485,21 @@ elab ist info pattern opts fn tm

480485 (movelast n)

481486 else movelast n)

482487 (ivs' \\ ivs)

483− where -- normal < tactic < default tactic

488+ where -- normal < alternatives < lambdas < rewrites < tactic < default tactic

489+ -- reason for lambdas after alternatives is that having

490+ -- the alternative resolved can help with typechecking the lambda

491+ -- or the rewrite. Rewrites/tactics need as much information

492+ -- as possible about the type.

493+ -- FIXME: Better would be to allow alternative resolution to be

494+ -- retried after more information is in.

484495 cmpArg (_, x) (_, y)

485496 = compare (conDepth 0 (getTm x) + priority x + alt x)

486497 (conDepth 0 (getTm y) + priority y + alt y)

487498 where alt t = case getTm t of

488499 PAlternative False _ -> 5

500+ PAlternative True _ -> 1

501+ PLam _ _ _ -> 2

502+ PRewrite _ _ _ _ -> 3

489503 _ -> 0

490504

491505 -- Score a point for every level where there is a non-constructor