2cff556 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Another unification fix

Removes 'matching' hack, which would sometimes cause function applications in patterns to be unified when they shouldn't have been. Fixes #898.

commit2cff5569e245d5f0fb17967cacd72ccd7834f43f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 17 Feb 2014, 02:01 (13 years ago) parentc959fb0

7 files changed+99−58

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2 src/Idris/Core/Elaborate.hs+5−5 src/Idris/Core/ProofState.hs+54−33 src/Idris/Core/Unify.hs+12−9 src/Idris/ElabDecls.hs+4−3 src/Idris/ElabTerm.hs+22−7 test/basic002/test006.idr−1

src/Idris/AbsSyntax.hs+2

@@ -1522,6 +1522,8 @@ stripLinear i tm = evalState (sl tm) [] where

15221522 then return Placeholder

15231523 else do put (f : ns)

15241524 return (PPatvar fc f)

1525+ sl t@(PAlternative _ (a : as)) = do sl a

1526+ return t

15251527 sl (PApp fc fn args) = do fn' <- sl fn

15261528 args' <- mapM slA args

15271529 return $ PApp fc fn' args'

src/Idris/Core/Elaborate.hs+5−5

@@ -372,8 +372,8 @@ focus n = processTactic' (Focus n)

372372movelast :: Name -> Elab' aux ()

373373movelast n = processTactic' (MoveLast n)

374374

375−matchProblems :: Elab' aux ()

376−matchProblems = processTactic' MatchProblems

375+matchProblems :: Bool -> Elab' aux ()

376+matchProblems all = processTactic' (MatchProblems all)

377377

378378unifyProblems :: Elab' aux ()

379379unifyProblems = processTactic' UnifyProblems

@@ -625,7 +625,7 @@ no_errors tac err

625625 ps' <- get_probs

626626 if (length ps' > length ps) then

627627 case reverse ps' of

628− ((x,y,env,err) : _) ->

628+ ((x,y,env,err,_) : _) ->

629629 let env' = map (\(x, b) -> (x, binderTy b)) env in

630630 lift $ tfail $ CantUnify False x y err env' 0

631631 else return $! ()

@@ -716,12 +716,12 @@ prunStateT pmax zok ps x s

716716 newpmax = if newps < 0 then 0 else newps in

717717 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

718718 then case reverse (problems p) of

719− ((_,_,_,e):_) -> Error e

719+ ((_,_,_,e,_):_) -> Error e

720720 else OK ((v, newpmax, problems p), s')

721721 Error e -> Error e

722722

723723qshow :: Fails -> String

724−qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

724+qshow fs = show (map (\ (x, y, _, _, _) -> (x, y)) fs)

725725

726726dumpprobs [] = ""

727727dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Idris/Core/ProofState.hs+54−33

@@ -79,7 +79,7 @@ data Tactic = Attack

7979 | Instance Name

8080 | SetInjective Name

8181 | MoveLast Name

82− | MatchProblems

82+ | MatchProblems Bool

8383 | UnifyProblems

8484 | ProofState

8585 | Undo

@@ -147,7 +147,7 @@ hole _ = False

147147holeName i = sMN i "hole"

148148

149149qshow :: Fails -> String

150−qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

150+qshow fs = show (map (\ (x, y, _, _, t) -> (t, x, y)) fs)

151151

152152match_unify' :: Context -> Env -> TT Name -> TT Name ->

153153 StateT TState TC [(Name, TT Name)]

@@ -155,10 +155,26 @@ match_unify' ctxt env topx topy =

155155 do ps <- get

156156 let dont = dontunify ps

157157 let inj = injective ps

158− u <- lift $ match_unify ctxt env topx topy inj (holes ps)

159− let (h, ns) = unified ps

160− put (ps { unified = (h, u ++ ns) })

161− return u

158+ traceWhen (unifylog ps)

159+ ("Matching " ++ show (topx, topy) ++

160+ " in " ++ show env ++

161+ "\nHoles: " ++ show (holes ps)

162+ ++ "\n"

163+ ++ "\n" ++ show (pterm ps) ++ "\n\n"

164+ ) $

165+ case match_unify ctxt env topx topy inj (holes ps) of

166+ OK u -> do let (h, ns) = unified ps

167+ put (ps { unified = (h, u ++ ns) })

168+ return u

169+ Error e -> do put (ps { problems = (topx, topy, env, e, Match) :

170+ problems ps })

171+ return []

172+-- traceWhen (unifylog ps)

173+-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++

174+-- "\nSolved: " ++ show u

175+-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)

176+-- -- ++ show (pterm ps)

177+-- ++ "\n----------") $

162178

163179unify' :: Context -> Env -> TT Name -> TT Name ->

164180 StateT TState TC [(Name, TT Name)]

@@ -403,7 +419,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

403419 Nothing -> error ("deferType can't find " ++ show n)

404420

405421regret :: RunTactic

406−regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

422+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

407423 do action (\ps -> let hs = holes ps in

408424 ps { holes = hs \\ [x] })

409425 return sc

@@ -470,22 +486,23 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

470486

471487solve :: RunTactic

472488solve ctxt env (Bind x (Guess ty val) sc)

473− | True = do ps <- get

474− let (uh, uns) = unified ps

475− case lookup x (notunified ps) of

476− Just tm -> unify' ctxt env tm val

477− _ -> return []

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

479− solved = Just (x, val),

480− instances = instances ps \\ [x] })

481− let tm' = subst x val sc in

482− return tm'

483− | otherwise = lift $ tfail $ IncompleteTerm val

489+ = do ps <- get

490+ let (uh, uns) = unified ps

491+ case lookup x (notunified ps) of

492+ Just tm -> match_unify' ctxt env tm val

493+ _ -> return []

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

495+ solved = Just (x, val),

496+ notunified = updateNotunified [(x,val)]

497+ (notunified ps),

498+ instances = instances ps \\ [x] })

499+ let tm' = subst x val sc in

500+ return tm'

484501solve _ _ h@(Bind x t sc)

485− = do ps <- get

486− case findType x sc of

487− Just t -> lift $ tfail (CantInferType (show t))

488− _ -> fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

502+ = do ps <- get

503+ case findType x sc of

504+ Just t -> lift $ tfail (CantInferType (show t))

505+ _ -> fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

489506 where findType x (Bind n (Let t v) sc)

490507 = findType x v `mplus` findType x sc

491508 findType x (Bind n t sc)

@@ -539,6 +556,8 @@ forall n ty ctxt env _ = fail "Can't pi bind here"

539556patvar :: Name -> RunTactic

540557patvar n ctxt env (Bind x (Hole t) sc) =

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

559+ notunified = updateNotunified [(x,P Bound n t)]

560+ (notunified ps),

542561 injective = addInj n x (injective ps) })

543562 return $ Bind n (PVar t) (subst x (P Bound n t) sc)

544563 where addInj n x ps | x `elem` ps = n : ps

@@ -712,7 +731,6 @@ solve_unified ctxt env tm =

712731 action (\ps -> ps { holes = holes ps \\ map fst unify })

713732 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

714733 return (updateSolved unify tm)

715− where

716734

717735dropGiven du [] hs = []

718736dropGiven du ((n, P Bound t ty) : us) hs

@@ -771,7 +789,7 @@ updateNotunified ns nu = up nu where

771789updateProblems ctxt [] ps inj holes = ([], ps)

772790updateProblems ctxt ns ps inj holes = up ns ps where

773791 up ns [] = (ns, [])

774− up ns ((x, y, env, err) : ps) =

792+ up ns ((x, y, env, err, um) : ps) =

775793 let x' = updateSolved ns x

776794 y' = updateSolved ns y

777795 err' = updateError ns err

@@ -780,12 +798,13 @@ updateProblems ctxt ns ps inj holes = up ns ps where

780798 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

781799 up (ns ++ v) ps

782800 _ -> let (ns', ps') = up ns ps in

783− (ns', (x',y',env',err') : ps')

801+ (ns', (x',y',env',err', um) : ps')

784802

785803-- attempt to solve remaining problems with match_unify

786−matchProblems ctxt ps inj holes = up [] ps where

804+matchProblems all ctxt ps inj holes = up [] ps where

787805 up ns [] = (ns, [])

788− up ns ((x, y, env, err) : ps) =

806+ up ns ((x, y, env, err, um) : ps)

807+ | all || um == Match =

789808 let x' = updateSolved ns x

790809 y' = updateSolved ns y

791810 err' = updateError ns err

@@ -794,7 +813,9 @@ matchProblems ctxt ps inj holes = up [] ps where

794813 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

795814 up (ns ++ v) ps

796815 _ -> let (ns', ps') = up ns ps in

797− (ns', (x',y',env',err') : ps')

816+ (ns', (x',y',env',err',um) : ps')

817+ up ns (p : ps) = let (ns', ps') = up ns ps in

818+ (ns', p : ps')

798819

799820processTactic :: Tactic -> ProofState -> TC (ProofState, String)

800821processTactic QED ps = case holes ps of

@@ -834,11 +855,11 @@ processTactic UnifyProblems ps

834855 previous = Just ps, plog = "",

835856 notunified = updateNotunified ns' (notunified ps),

836857 holes = holes ps \\ (map fst ns') }, plog ps)

837−processTactic MatchProblems ps

838− = let (ns', probs') = matchProblems (context ps)

839− (problems ps)

840− (injective ps)

841− (holes ps)

858+processTactic (MatchProblems all) ps

859+ = let (ns', probs') = matchProblems all (context ps)

860+ (problems ps)

861+ (injective ps)

862+ (holes ps)

842863 pterm' = updateSolved ns' (pterm ps) in

843864 return (ps { pterm = pterm', solved = Nothing, problems = probs',

844865 previous = Just ps, plog = "",

src/Idris/Core/Unify.hs+12−9

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.Core.Unify(match_unify, unify, Fails) where

3+module Idris.Core.Unify(match_unify, unify, Fails, FailAt(..)) where

55import Idris.Core.TT

66import Idris.Core.Evaluate

@@ -18,8 +18,11 @@ import Debug.Trace

1818-- terms which need to be injective, with the things we're trying to unify

1919-- at the time

2020

21+data FailAt = Match | Unify

22+ deriving (Show, Eq)

23+

2124type Injs = [(TT Name, TT Name, TT Name)]

22−type Fails = [(TT Name, TT Name, Env, Err)]

25+type Fails = [(TT Name, TT Name, Env, Err, FailAt)]

2326

2427data UInfo = UI Int Fails

2528 deriving Show

@@ -78,7 +81,7 @@ match_unify ctxt env topx topy inj holes =

7881 let err = CantUnify r

7982 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

8083 if (not r) then lift $ tfail err

81− else do put (UI s ((x, y, env, err) : f))

84+ else do put (UI s ((x, y, env, err, Match) : f))

8285 lift $ tfail err

8386

8487

@@ -92,7 +95,7 @@ match_unify ctxt env topx topy inj holes =

9295 let err = CantUnify r topx topy

9396 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

9497 (errEnv env) s

95− put (UI s ((binderTy x, binderTy y, env, err) : f))

98+ put (UI s ((binderTy x, binderTy y, env, err, Match) : f))

9699 return []

97100

98101 -- TODO: there's an annoying amount of repetition between this and the

@@ -105,7 +108,7 @@ match_unify ctxt env topx topy inj holes =

105108 let r = recoverable x y

106109 let err = CantUnify r

107110 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

108− put (UI s ((x, y, env, err) : f))

111+ put (UI s ((x, y, env, err, Match) : f))

109112 lift $ tfail err

110113 combine bnames as [] = return as

111114 combine bnames as ((n, t) : bs)

@@ -334,7 +337,7 @@ unify ctxt env topx topy inj holes =

334337 let err = CantUnify r

335338 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

336339 if (not r) then lift $ tfail err

337− else do put (UI s ((x, y, env, err) : f))

340+ else do put (UI s ((x, y, env, err, Unify) : f))

338341 return [] -- lift $ tfail err

339342

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

@@ -470,7 +473,7 @@ unify ctxt env topx topy inj holes =

470473 let r = recoverable x y

471474 let err = CantUnify r

472475 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

473− put (UI s ((topx, topy, env, err) : f))

476+ put (UI s ((topx, topy, env, err, Unify) : f))

474477 return []

475478

476479 -- shortcut failure, if we *know* nothing can fix it

@@ -478,7 +481,7 @@ unify ctxt env topx topy inj holes =

478481 let r = recoverable x y

479482 let err = CantUnify r

480483 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

481− put (UI s ((topx, topy, env, err) : f))

484+ put (UI s ((topx, topy, env, err, Unify) : f))

482485 lift $ tfail err

483486

484487

@@ -501,7 +504,7 @@ unify ctxt env topx topy inj holes =

501504 let err = CantUnify r topx topy

502505 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

503506 (errEnv env) s

504− put (UI s ((binderTy x, binderTy y, env, err) : f))

507+ put (UI s ((binderTy x, binderTy y, env, err, Unify) : f))

505508 return [] -- lift $ tfail err

506509

507510 checkCycle ns p@(x, P _ _ _) = return [p]

src/Idris/ElabDecls.hs+4−3

@@ -1252,7 +1252,8 @@ checkPossible info fc tcgen fname lhs_in

12521252-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

12531253-- return (not b) -- then return (Just lhs_tm) else return Nothing

12541254-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

1255− Error err -> return (impossibleError err)

1255+ Error err -> if tcgen then return False

1256+ else return (impossibleError err)

12561257 where impossibleError (CantUnify _ topx topy e _ _)

12571258 = not (sameFam topx topy || not (impossibleError e))

12581259 impossibleError (CantConvert _ _ _) = False

@@ -1304,7 +1305,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

13041305 inj <- get_inj

13051306 return (res, probs, inj))

13061307

1307− when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1308+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)

13081309

13091310 let lhs_tm = orderPats (getInferTerm lhs')

13101311 let lhs_ty = getInferType lhs'

@@ -1368,7 +1369,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

13681369 probs <- get_probs

13691370 return (tm, ds, is, probs))

13701371

1371− when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1372+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)

13721373

13731374 logLvl 5 "DONE CHECK"

13741375 logLvl 2 $ "---> " ++ show rhs'

src/Idris/ElabTerm.hs+22−7

@@ -71,12 +71,12 @@ build ist info pattern opts fn tm

7171 resolveTC 7 g fn ist) ivs

7272 tm <- get_term

7373 ctxt <- get_context

74− when (not pattern) $ do matchProblems; unifyProblems

74+ when (not pattern) $ do matchProblems True; unifyProblems

7575 probs <- get_probs

7676 case probs of

7777 [] -> return ()

78− ((_,_,_,e):es) -> if inf then return ()

79− else lift (Error e)

78+ ((_,_,_,e,_):es) -> if inf then return ()

79+ else lift (Error e)

8080 is <- getAux

8181 tt <- get_term

8282 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -103,8 +103,8 @@ buildTC ist info pattern opts fn tm

103103 tm <- get_term

104104 case probs of

105105 [] -> return ()

106− ((_,_,_,e):es) -> if inf then return ()

107− else lift (Error e)

106+ ((_,_,_,e,_):es) -> if inf then return ()

107+ else lift (Error e)

108108 is <- getAux

109109 tt <- get_term

110110 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -125,7 +125,8 @@ elab ist info pattern opts fn tm

125125 end_unify

126126 when pattern -- convert remaining holes to pattern vars

127127 (do update_term orderPats

128− matchProblems; unifyProblems

128+ matchProblems False -- only the ones we matched earlier

129+ unifyProblems

129130 mkPat)

130131 where

131132 tcgen = Dictionary `elem` opts

@@ -480,11 +481,25 @@ elab ist info pattern opts fn tm

480481 (ivs' \\ ivs)

481482 where -- normal < tactic < default tactic

482483 cmpArg (_, x) (_, y)

483− = compare (priority x + alt x) (priority y + alt y)

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

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

484486 where alt t = case getTm t of

485487 PAlternative False _ -> 5

486488 _ -> 0

487489

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

491+ -- function (so higher score --> done later)

492+ -- Only relevant when on lhs

493+ conDepth d t | not pattern = 0

494+ conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0

495+ | otherwise = max (100 - d) 1

496+ conDepth d (PApp _ f as)

497+ = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))

498+ conDepth d (PPatvar _ _) = 0

499+ conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

500+ conDepth d Placeholder = 0

501+ conDepth d t = max (100 - d) 1

502+

488503 checkIfInjective n = do

489504 env <- get_env

490505 case lookup n env of

test/basic002/test006.idr−1

@@ -36,4 +36,3 @@ Main.parity_lemma_1 = proof {

3636 trivial;

3737};

3838

39−