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

git.iko.soy/Idris-dev

on master help sign in

Unification tweak; better disambiguation

88f88ebEdwin Brady13 years ago

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

compare with master

unifiedsplit

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

491 = do ps <- get

492 let (uh, uns) = unified ps

493 case lookup x (notunified ps) of

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

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

495+ match_unify' ctxt env tm val

495 _ -> return []

496 _ -> return []

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

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

497 solved = Just (x, val),

498 solved = Just (x, val),

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

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

372

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

374 | (injectiveApp fx && injectiveApp fy)

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

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

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

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

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

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

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

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

418 vs <- combine bnames as as'

419 unArgs vs xs ys

420

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

422+

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

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

422 (metavar f &&

424 (metavar f &&

423 all (\x -> metavarApp x) args

425 all (\x -> metavarApp x) args

src/Idris/ElabTerm.hs+16−2

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

72 tm <- get_term

73 ctxt <- get_context

74 probs <- get_probs

75+ u <- getUnifyLog

77+ when (not pattern) $

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

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

79+ do matchProblems True; unifyProblems

77 probs <- get_probs

80 probs <- get_probs

78 case probs of

81 case probs of

79 [] -> return ()

82 [] -> return ()

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

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

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

459 -- mark any type class arguments as injective

462 -- mark any type class arguments as injective

460 mapM_ checkIfInjective (map snd ns)

463 mapM_ checkIfInjective (map snd ns)

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

465+ -- to help with disambiguation

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

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

462 let (ns', eargs) = unzip $

467 let (ns', eargs) = unzip $

463 sortBy cmpArg (zip ns args)

468 sortBy cmpArg (zip ns args)

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

480 (movelast n)

485 (movelast n)

481 else movelast n)

486 else movelast n)

482 (ivs' \\ ivs)

487 (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.

484 cmpArg (_, x) (_, y)

495 cmpArg (_, x) (_, y)

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

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

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

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

487 where alt t = case getTm t of

498 where alt t = case getTm t of

488 PAlternative False _ -> 5

499 PAlternative False _ -> 5

500+ PAlternative True _ -> 1

501+ PLam _ _ _ -> 2

502+ PRewrite _ _ _ _ -> 3

489 _ -> 0

503 _ -> 0

490

504

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

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