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

git.iko.soy/Idris-dev

on master help sign in

Another unification fix

2cff556Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+2

compare with master

unifiedsplit

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

1522 then return Placeholder

1523 else do put (f : ns)

1524 return (PPatvar fc f)

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

1526+ return t

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

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

1526 args' <- mapM slA args

1528 args' <- mapM slA args

1527 return $ PApp fc fn' args'

1529 return $ PApp fc fn' args'

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

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

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

373movelast n = processTactic' (MoveLast n)

374

375−matchProblems :: Elab' aux ()

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

376−matchProblems = processTactic' MatchProblems

376+matchProblems all = processTactic' (MatchProblems all)

377

378unifyProblems :: Elab' aux ()

379unifyProblems = processTactic' UnifyProblems

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

625 ps' <- get_probs

626 if (length ps' > length ps) then

627 case reverse ps' of

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

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

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

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

631 else return $! ()

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

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

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

718 then case reverse (problems p) of

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

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

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

721 Error e -> Error e

722

723qshow :: Fails -> String

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

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

725

726dumpprobs [] = ""

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

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

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

79 | Instance Name

80 | SetInjective Name

81 | MoveLast Name

82− | MatchProblems

82+ | MatchProblems Bool

83 | UnifyProblems

84 | ProofState

85 | Undo

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

147holeName i = sMN i "hole"

148

149qshow :: Fails -> String

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

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

151

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

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

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

155 do ps <- get

156 let dont = dontunify ps

157 let inj = injective ps

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+ ) $

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

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

159− let (h, ns) = unified ps

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

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

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 })

161− return u

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----------") $

162

178

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

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

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

180 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' =

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

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

404

420

405regret :: RunTactic

421regret :: 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 =

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

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

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

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

409 return sc

425 return sc

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

470

486

471solve :: RunTactic

487solve :: RunTactic

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

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

473− | True = do ps <- get

489+ = do ps <- get

474− let (uh, uns) = unified ps

490+ let (uh, uns) = unified ps

475− case lookup x (notunified ps) of

491+ case lookup x (notunified ps) of

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

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

477− _ -> return []

493+ _ -> return []

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

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

479− solved = Just (x, val),

495+ solved = Just (x, val),

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

497+ (notunified ps),

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

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

481− let tm' = subst x val sc in

499+ let tm' = subst x val sc in

482− return tm'

500+ return tm'

483− | otherwise = lift $ tfail $ IncompleteTerm val

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

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

485− = do ps <- get

502+ = do ps <- get

486− case findType x sc of

503+ case findType x sc of

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

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

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

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

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

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

490 = findType x v `mplus` findType x sc

507 = findType x v `mplus` findType x sc

491 findType x (Bind n t sc)

508 findType x (Bind n t sc)

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

539patvar :: Name -> RunTactic

556patvar :: Name -> RunTactic

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

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

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

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

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

560+ (notunified ps),

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

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

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

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

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

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

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

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

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

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

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

714 return (updateSolved unify tm)

733 return (updateSolved unify tm)

715− where

716

734

717dropGiven du [] hs = []

735dropGiven du [] hs = []

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

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

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

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

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

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

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

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

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

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

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

775 let x' = updateSolved ns x

793 let x' = updateSolved ns x

776 y' = updateSolved ns y

794 y' = updateSolved ns y

777 err' = updateError ns err

795 err' = updateError ns err

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

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

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

781 up (ns ++ v) ps

799 up (ns ++ v) ps

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

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

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

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

784

802

785-- attempt to solve remaining problems with match_unify

803-- 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

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

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

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

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

807+ | all || um == Match =

789 let x' = updateSolved ns x

808 let x' = updateSolved ns x

790 y' = updateSolved ns y

809 y' = updateSolved ns y

791 err' = updateError ns err

810 err' = updateError ns err

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

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

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

795 up (ns ++ v) ps

814 up (ns ++ v) ps

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

815 _ -> 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')

798

819

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

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

800processTactic QED ps = case holes ps of

821processTactic QED ps = case holes ps of

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

834 previous = Just ps, plog = "",

855 previous = Just ps, plog = "",

835 notunified = updateNotunified ns' (notunified ps),

856 notunified = updateNotunified ns' (notunified ps),

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

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

837−processTactic MatchProblems ps

858+processTactic (MatchProblems all) ps

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

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

839− (problems ps)

860+ (problems ps)

840− (injective ps)

861+ (injective ps)

841− (holes ps)

862+ (holes ps)

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

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

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

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

844 previous = Just ps, plog = "",

865 previous = Just ps, plog = "",

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

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

1{-# LANGUAGE PatternGuards #-}

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

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

5import Idris.Core.TT

6import Idris.Core.Evaluate

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

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

19-- at the time

21+data FailAt = Match | Unify

22+ deriving (Show, Eq)

23+

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

24type 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)]

24data UInfo = UI Int Fails

27data UInfo = UI Int Fails

25 deriving Show

28 deriving Show

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

78 let err = CantUnify r

81 let err = CantUnify r

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

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

80 if (not r) then lift $ tfail err

83 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))

82 lift $ tfail err

85 lift $ tfail err

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

92 let err = CantUnify r topx topy

95 let err = CantUnify r topx topy

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

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

94 (errEnv env) s

97 (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))

96 return []

99 return []

100

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

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

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

105 let r = recoverable x y

108 let r = recoverable x y

106 let err = CantUnify r

109 let err = CantUnify r

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

110 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))

109 lift $ tfail err

112 lift $ tfail err

110 combine bnames as [] = return as

113 combine bnames as [] = return as

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

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

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

334 let err = CantUnify r

337 let err = CantUnify r

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

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

336 if (not r) then lift $ tfail err

339 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))

338 return [] -- lift $ tfail err

341 return [] -- lift $ tfail err

339

342

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

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

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

470 let r = recoverable x y

473 let r = recoverable x y

471 let err = CantUnify r

474 let err = CantUnify r

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

475 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))

474 return []

477 return []

475

478

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

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

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

478 let r = recoverable x y

481 let r = recoverable x y

479 let err = CantUnify r

482 let err = CantUnify r

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

483 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))

482 lift $ tfail err

485 lift $ tfail err

483

486

484

487

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

501 let err = CantUnify r topx topy

504 let err = CantUnify r topx topy

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

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

503 (errEnv env) s

506 (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))

505 return [] -- lift $ tfail err

508 return [] -- lift $ tfail err

506

509

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

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

src/Idris/ElabDecls.hs+4−3

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

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

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

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

1255+ Error err -> if tcgen then return False

1255− Error err -> return (impossibleError err)

1256+ else return (impossibleError err)

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

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

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

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

1258 impossibleError (CantConvert _ _ _) = False

1259 impossibleError (CantConvert _ _ _) = False

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

1304 inj <- get_inj

1305 inj <- get_inj

1305 return (res, probs, inj))

1306 return (res, probs, inj))

1306

1307

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

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

1308

1309

1309 let lhs_tm = orderPats (getInferTerm lhs')

1310 let lhs_tm = orderPats (getInferTerm lhs')

1310 let lhs_ty = getInferType lhs'

1311 let lhs_ty = getInferType lhs'

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

1368 probs <- get_probs

1369 probs <- get_probs

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

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

1370

1371

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

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

1372

1373

1373 logLvl 5 "DONE CHECK"

1374 logLvl 5 "DONE CHECK"

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

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

src/Idris/ElabTerm.hs+22−7

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

71 resolveTC 7 g fn ist) ivs

72 tm <- get_term

73 ctxt <- get_context

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

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

75 probs <- get_probs

76 case probs of

77 [] -> return ()

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

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

79− else lift (Error e)

79+ else lift (Error e)

80 is <- getAux

81 tt <- get_term

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

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

103 tm <- get_term

104 case probs of

105 [] -> return ()

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

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

107− else lift (Error e)

107+ else lift (Error e)

108 is <- getAux

109 tt <- get_term

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

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

125 end_unify

126 when pattern -- convert remaining holes to pattern vars

127 (do update_term orderPats

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

128− matchProblems; unifyProblems

129+ unifyProblems

129 mkPat)

130 mkPat)

130 where

131 where

131 tcgen = Dictionary `elem` opts

132 tcgen = Dictionary `elem` opts

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

480 (ivs' \\ ivs)

481 (ivs' \\ ivs)

481 where -- normal < tactic < default tactic

482 where -- normal < tactic < default tactic

482 cmpArg (_, x) (_, y)

483 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)

484 where alt t = case getTm t of

486 where alt t = case getTm t of

485 PAlternative False _ -> 5

487 PAlternative False _ -> 5

486 _ -> 0

488 _ -> 0

487

489

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+

488 checkIfInjective n = do

503 checkIfInjective n = do

489 env <- get_env

504 env <- get_env

490 case lookup n env of

505 case lookup n env of

test/basic002/test006.idr−1

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

36 trivial;

37};

39−