f54c665 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

EXPERIMENTAL: Solve more implicits by matching

f54c665Edwin Brady13 years ago

src/Core/Elaborate.hs+3

compare with master

unifiedsplit

@@ -326,6 +326,9 @@ focus n = processTactic' (Focus n)

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

327movelast n = processTactic' (MoveLast n)

328

329+matchProblems :: Elab' aux ()

330+matchProblems = processTactic' MatchProblems

331+

329defer :: Name -> Elab' aux ()

332defer :: Name -> Elab' aux ()

330defer n = do n' <- unique_hole n

333defer n = do n' <- unique_hole n

331 processTactic' (Defer n')

334 processTactic' (Defer n')

src/Core/ProofState.hs+24−1

@@ -78,6 +78,7 @@ data Tactic = Attack

78 | Instance Name

79 | SetInjective Name

80 | MoveLast Name

81+ | MatchProblems

81 | ProofState

82 | ProofState

82 | Undo

83 | Undo

83 | QED

84 | QED

@@ -711,6 +712,20 @@ updateProblems ctxt ns ps inj holes = up ns ps where

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

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

712 (ns', (x',y',env',err') : ps')

713 (ns', (x',y',env',err') : ps')

713

714

715+-- attempt to solve remaining problems with match_unify

716+matchProblems ctxt ps inj holes = up [] ps where

717+ up ns [] = (ns, [])

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

719+ let x' = updateSolved ns x

720+ y' = updateSolved ns y

721+ err' = updateError ns err

722+ env' = updateEnv ns env in

723+ case match_unify ctxt env' x' y' inj holes of

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

725+ up (ns ++ v) ps

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

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

728+

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

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

715processTactic QED ps = case holes ps of

730processTactic QED ps = case holes ps of

716 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

731 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

@@ -739,6 +754,15 @@ processTactic (Reorder n) ps

739 return (ps' { previous = Just ps, plog = "" }, plog ps')

754 return (ps' { previous = Just ps, plog = "" }, plog ps')

740processTactic (ComputeLet n) ps

755processTactic (ComputeLet n) ps

741 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")

756 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")

757+processTactic MatchProblems ps

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

759+ (problems ps)

760+ (injective ps)

761+ (holes ps)

762+ pterm' = updateSolved ns' (pterm ps) in

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

764+ previous = Just ps, plog = "",

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

742processTactic t ps

766processTactic t ps

743 = case holes ps of

767 = case holes ps of

744 [] -> fail "Nothing to fill in."

768 [] -> fail "Nothing to fill in."

@@ -795,4 +819,3 @@ process t h = tactic (Just h) (mktac t)

795 mktac (Instance n) = instanceArg n

819 mktac (Instance n) = instanceArg n

796 mktac (SetInjective n) = setinj n

820 mktac (SetInjective n) = setinj n

797 mktac (MoveLast n) = movelast n

821 mktac (MoveLast n) = movelast n

798−

src/Idris/ElabTerm.hs+2−1

@@ -56,9 +56,10 @@ build ist info pattern fn tm

56 mapM_ (\n -> when (n `elem` hs) $

57 do focus n

58 resolveTC 7 fn ist) ivs

59− probs <- get_probs

60 tm <- get_term

59 tm <- get_term

61 ctxt <- get_context

60 ctxt <- get_context

61+ when (not pattern) matchProblems

62+ probs <- get_probs

62 case probs of

63 case probs of

63 [] -> return ()

64 [] -> return ()

64 ((_,_,_,e):es) -> lift (Error e)

65 ((_,_,_,e):es) -> lift (Error e)