1dfc8fd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix typo that led to unification bug

1dfc8fdEdwin Brady13 years ago

src/Idris/Core/Elaborate.hs+4

compare with master

unifiedsplit

@@ -143,6 +143,10 @@ unifyLog :: Bool -> Elab' aux ()

143unifyLog log = do ES (ps, a) l p <- get

144 put (ES (ps { unifylog = log }, a) l p)

145

146+getUnifyLog :: Elab' aux Bool

147+getUnifyLog = do ES (ps, a) l p <- get

148+ return (unifylog ps)

149+

146processTactic' t = do ES (p, a) logs prev <- get

150processTactic' t = do ES (p, a) logs prev <- get

147 (p', log) <- lift $ processTactic t p

151 (p', log) <- lift $ processTactic t p

148 put (ES (p', a) (logs ++ log) prev)

152 put (ES (p', a) (logs ++ log) prev)

src/Idris/Core/ProofState.hs+7−14

@@ -476,16 +476,10 @@ solve ctxt env (Bind x (Guess ty val) sc)

476 | True = do ps <- get

477 let (uh, uns) = unified ps

478 case lookup x (notunified ps) of

479− Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $

480− -- return []

481− unify' ctxt env tm val

479+ Just tm -> unify' ctxt env tm val

482 _ -> return []

480 _ -> return []

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

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

484 solved = Just (x, val),

482 solved = Just (x, val),

485−-- problems = solveInProblems

486−-- x val (problems ps),

487− -- dontunify = dontunify ps \\ [x],

488− -- unified = (uh, uns ++ [(x, val)]),

489 instances = instances ps \\ [x] })

483 instances = instances ps \\ [x] })

490 let tm' = subst x val sc in

484 let tm' = subst x val sc in

491 return tm'

485 return tm'

@@ -739,8 +733,7 @@ keepGiven du (u@(n, _) : us) hs

739 | n `elem` du = u : keepGiven du us hs

733 | n `elem` du = u : keepGiven du us hs

740keepGiven du (u : us) hs = keepGiven du us hs

734keepGiven du (u : us) hs = keepGiven du us hs

741

735

742−updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

743− updateSolved' xs x

736+updateSolved xs x = updateSolved' xs x

744updateSolved' [] x = x

737updateSolved' [] x = x

745updateSolved' xs (Bind n (Hole ty) t)

738updateSolved' xs (Bind n (Hole ty) t)

746 | Just v <- lookup n xs

739 | Just v <- lookup n xs

@@ -772,8 +765,8 @@ solveInProblems x val ((l, r, env, err) : ps)

772updateNotunified [] nu = nu

765updateNotunified [] nu = nu

773updateNotunified ns nu = up nu where

766updateNotunified ns nu = up nu where

774 up [] = []

767 up [] = []

775− up ((n, t) : ns) = let t' = updateSolved ns t in

768+ up ((n, t) : nus) = let t' = updateSolved ns t in

776− ((n, t') : up ns)

769+ ((n, t') : up nus)

777

770

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

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

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

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

@@ -820,12 +813,11 @@ processTactic EndUnify ps

820 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

813 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

821 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

814 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

822 (injective ps) (holes ps)

815 (injective ps) (holes ps)

823− tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $

824− updateSolved ns'' (pterm ps) in

816+ tm' = updateSolved ns'' (pterm ps) in

825 return (ps { pterm = tm',

817 return (ps { pterm = tm',

826 unified = (h, []),

818 unified = (h, []),

827 problems = probs',

819 problems = probs',

828− notunified = updateNotunified ns (notunified ps),

820+ notunified = updateNotunified ns'' (notunified ps),

829 holes = holes ps \\ map fst ns'' }, "")

821 holes = holes ps \\ map fst ns'' }, "")

830processTactic (Reorder n) ps

822processTactic (Reorder n) ps

831 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

823 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

@@ -850,6 +842,7 @@ processTactic MatchProblems ps

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

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

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

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

852 previous = Just ps, plog = "",

844 previous = Just ps, plog = "",

845+ notunified = updateNotunified ns' (notunified ps),

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

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

854processTactic t ps

847processTactic t ps

855 = case holes ps of

848 = case holes ps of

src/Idris/ElabTerm.hs+9−14

@@ -708,9 +708,10 @@ resolveTC depth topg fn ist

708 = do hnf_compute

709 g <- goal

710 ptm <- get_term

711+ ulog <- getUnifyLog

711 hs <- get_holes

712 hs <- get_holes

712− if True -- all (\n -> not (n `elem` hs)) (freeNames g)

713+ traceWhen ulog ("Resolving class " ++ show g) $

713− then try' (trivial' ist)

714+ try' (trivial' ist)

714 (do t <- goal

715 (do t <- goal

715 let (tc, ttypes) = unApply t

716 let (tc, ttypes) = unApply t

716 scopeOnly <- needsDefault t tc ttypes

717 scopeOnly <- needsDefault t tc ttypes

@@ -718,16 +719,8 @@ resolveTC depth topg fn ist

718 let insts = if scopeOnly then filter chaser insts_in

719 let insts = if scopeOnly then filter chaser insts_in

719 else insts_in

720 else insts_in

720 tm <- get_term

721 tm <- get_term

721−-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

722−-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

723−-- if scopeOnly then fail "Can't resolve" else

724 let depth' = if scopeOnly then 2 else depth

722 let depth' = if scopeOnly then 2 else depth

725 blunderbuss t depth' insts) True

723 blunderbuss t depth' insts) True

726− else do try' (trivial' ist)

727− (do g <- goal

728− fail $ "Can't resolve " ++ show g) True

729−-- tm <- get_term

730−-- fail $ "Can't resolve yet in " ++ show tm

731 where

724 where

732 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

725 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

733 | otherwise = (fail "Can't resolve", show n)

726 | otherwise = (fail "Can't resolve", show n)

@@ -775,8 +768,8 @@ resolveTC depth topg fn ist

775 [args] -> map isImp (snd args) -- won't be overloaded!

768 [args] -> map isImp (snd args) -- won't be overloaded!

776 ps <- get_probs

769 ps <- get_probs

777 tm <- get_term

770 tm <- get_term

778− args <- try' (match_apply (Var n) imps)

771+ args <- try' (apply (Var n) imps)

779− (apply (Var n) imps) True

772+ (match_apply (Var n) imps) True

780 ps' <- get_probs

773 ps' <- get_probs

781 when (length ps < length ps') $ fail "Can't apply type class"

774 when (length ps < length ps') $ fail "Can't apply type class"

782-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

775-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

@@ -788,7 +781,9 @@ resolveTC depth topg fn ist

788 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

781 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

789 -- if there's any arguments left, we've failed to resolve

782 -- if there's any arguments left, we've failed to resolve

790 hs <- get_holes

783 hs <- get_holes

784+ ulog <- getUnifyLog

791− solve

785+ solve

786+ traceWhen ulog ("Got " ++ show n) $ return ()

792 where isImp (PImp p _ _ _ _ _) = (True, p)

787 where isImp (PImp p _ _ _ _ _) = (True, p)

793 isImp arg = (False, priority arg)

788 isImp arg = (False, priority arg)

794

789

@@ -1026,7 +1021,7 @@ runTac autoSolve ist tac

1026 else fail "Wrong goal type"

1021 else fail "Wrong goal type"

1027 _ -> fail "Wrong goal type"

1022 _ -> fail "Wrong goal type"

1028 runT ProofState = do g <- goal

1023 runT ProofState = do g <- goal

1029− trace (show g) $ return ()

1024+ return ()

1030 runT x = fail $ "Not implemented " ++ show x

1025 runT x = fail $ "Not implemented " ++ show x

1031

1026

1032 runReflected t = do t' <- reify ist t

1027 runReflected t = do t' <- reify ist t