40c7c45 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commit40c7c4522de27144e1cbe795c357088d0d1f7ab0 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateMon 20 Jan 2014, 11:09 (13 years ago) parent0c9e3a3 1dfc8fd

3 files changed+20−28

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+4 src/Idris/Core/ProofState.hs+7−14 src/Idris/ElabTerm.hs+9−14

src/Idris/Core/Elaborate.hs+4

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

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

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

145145

146+getUnifyLog :: Elab' aux Bool

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

148+ return (unifylog ps)

149+

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

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

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

476476 | True = do ps <- get

477477 let (uh, uns) = unified ps

478478 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

482480 _ -> return []

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

484482 solved = Just (x, val),

485−-- problems = solveInProblems

486−-- x val (problems ps),

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

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

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

490484 let tm' = subst x val sc in

491485 return tm'

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

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

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

741735

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

743− updateSolved' xs x

736+updateSolved xs x = updateSolved' xs x

744737updateSolved' [] x = x

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

746739 | Just v <- lookup n xs

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

772765updateNotunified [] nu = nu

773766updateNotunified ns nu = up nu where

774767 up [] = []

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

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

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

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

777770

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

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

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

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

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

822815 (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

825817 return (ps { pterm = tm',

826818 unified = (h, []),

827819 problems = probs',

828− notunified = updateNotunified ns (notunified ps),

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

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

830822processTactic (Reorder n) ps

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

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

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

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

852844 previous = Just ps, plog = "",

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

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

854847processTactic t ps

855848 = case holes ps of

src/Idris/ElabTerm.hs+9−14

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

708708 = do hnf_compute

709709 g <- goal

710710 ptm <- get_term

711+ ulog <- getUnifyLog

711712 hs <- get_holes

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

713− then try' (trivial' ist)

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

714+ try' (trivial' ist)

714715 (do t <- goal

715716 let (tc, ttypes) = unApply t

716717 scopeOnly <- needsDefault t tc ttypes

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

718719 let insts = if scopeOnly then filter chaser insts_in

719720 else insts_in

720721 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

724722 let depth' = if scopeOnly then 2 else depth

725723 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

731724 where

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

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

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

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

776769 ps <- get_probs

777770 tm <- get_term

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

779− (apply (Var n) imps) True

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

772+ (match_apply (Var n) imps) True

780773 ps' <- get_probs

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

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

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

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

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

790783 hs <- get_holes

791− solve

784+ ulog <- getUnifyLog

785+ solve

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

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

793788 isImp arg = (False, priority arg)

794789

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

10261021 else fail "Wrong goal type"

10271022 _ -> fail "Wrong goal type"

10281023 runT ProofState = do g <- goal

1029− trace (show g) $ return ()

1024+ return ()

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

10311026

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