git.iko.soy/Idris-dev
on master help sign in
Add basic elaboration context tracking to unification
b38bc03David Raymond Christiansen
src/Idris/Core/Elaborate.hs+3−3
compare with master
unifiedsplit
@@ -627,7 +627,7 @@ no_errors tac err
627 ps' <- get_probs
627 ps' <- get_probs
628 if (length ps' > length ps) then
628 if (length ps' > length ps) then
629 case reverse ps' of
629 case reverse ps' of
630− ((x,y,env,inerr,_) : _) ->
630+ ((x, y, env, inerr, while, _) : _) ->
631 let env' = map (\(x, b) -> (x, binderTy b)) env in
631 let env' = map (\(x, b) -> (x, binderTy b)) env in
632 lift $ tfail $
632 lift $ tfail $
633 case err of
633 case err of
@@ -721,12 +721,12 @@ prunStateT pmax zok ps x s
721 newpmax = if newps < 0 then 0 else newps in
721 newpmax = if newps < 0 then 0 else newps in
722 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
722 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
723 then case reverse (problems p) of
723 then case reverse (problems p) of
724− ((_,_,_,e,_):_) -> Error e
724+ ((_,_,_,e,_,_):_) -> Error e
725 else OK ((v, newpmax, problems p), s')
725 else OK ((v, newpmax, problems p), s')
726 Error e -> Error e
726 Error e -> Error e
727
727
728qshow :: Fails -> String
728qshow :: Fails -> String
729−qshow fs = show (map (\ (x, y, _, _, _) -> (x, y)) fs)
729+qshow fs = show (map (\ (x, y, _, _, _, _) -> (x, y)) fs)
730
730
731dumpprobs [] = ""
731dumpprobs [] = ""
732dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es
732dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es
src/Idris/Core/ProofState.hs+40−20
@@ -5,7 +5,7 @@
5 evaluation/checking inside the proof system, etc. --}
5 evaluation/checking inside the proof system, etc. --}
6
6
7module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
7module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8− Tactic(..), Goal(..), processTactic,
8+ Tactic(..), Goal(..), processTactic, now_elaborating, done_elaborating,
9 dropGiven, keepGiven) where
9 dropGiven, keepGiven) where
10
10
11import Idris.Core.Typecheck
11import Idris.Core.Typecheck
@@ -39,7 +39,8 @@ data ProofState = PS { thname :: Name,
39 context :: Context,
39 context :: Context,
40 plog :: String,
40 plog :: String,
41 unifylog :: Bool,
41 unifylog :: Bool,
42− done :: Bool
42+ done :: Bool,
43+ while_elaborating :: [FailContext]
43 }
44 }
44
45
45data Goal = GD { premises :: Env,
46data Goal = GD { premises :: Env,
@@ -90,9 +91,9 @@ data Tactic = Attack
90-- Some utilites on proof and tactic states
91-- Some utilites on proof and tactic states
91
92
92instance Show ProofState where
93instance Show ProofState where
93− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _)
94+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
94 = show nm ++ ": no more goals"
95 = show nm ++ ": no more goals"
95− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _)
96+ show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _ _)
96 = let OK g = goal (Just h) tm
97 = let OK g = goal (Just h) tm
97 wkenv = premises g in
98 wkenv = premises g in
98 "Other goals: " ++ show hs ++ "\n" ++
99 "Other goals: " ++ show hs ++ "\n" ++
@@ -115,9 +116,9 @@ instance Show ProofState where
115 showG ps b = showEnv ps (binderTy b)
116 showG ps b = showEnv ps (binderTy b)
116
117
117instance Pretty ProofState OutputAnnotation where
118instance Pretty ProofState OutputAnnotation where
118− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
119+ pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
119 pretty nm <+> colon <+> text " no more goals."
120 pretty nm <+> colon <+> text " no more goals."
120− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =
121+ pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _ _) =
121 let OK g = goal (Just h) tm in
122 let OK g = goal (Just h) tm in
122 let wkEnv = premises g in
123 let wkEnv = premises g in
123 text "Other goals" <+> colon <+> pretty hs <+>
124 text "Other goals" <+> colon <+> pretty hs <+>
@@ -148,12 +149,13 @@ hole _ = False
148holeName i = sMN i "hole"
149holeName i = sMN i "hole"
149
150
150qshow :: Fails -> String
151qshow :: Fails -> String
151−qshow fs = show (map (\ (x, y, _, _, t) -> (t, x, y)) fs)
152+qshow fs = show (map (\ (x, y, _, _, _, t) -> (t, x, y)) fs)
152
153
153match_unify' :: Context -> Env -> TT Name -> TT Name ->
154match_unify' :: Context -> Env -> TT Name -> TT Name ->
154 StateT TState TC [(Name, TT Name)]
155 StateT TState TC [(Name, TT Name)]
155match_unify' ctxt env topx topy =
156match_unify' ctxt env topx topy =
156 do ps <- get
157 do ps <- get
158+ let while = while_elaborating ps
157 let dont = dontunify ps
159 let dont = dontunify ps
158 let inj = injective ps
160 let inj = injective ps
159 traceWhen (unifylog ps)
161 traceWhen (unifylog ps)
@@ -163,11 +165,11 @@ match_unify' ctxt env topx topy =
163 ++ "\n"
165 ++ "\n"
164 ++ "\n" ++ show (pterm ps) ++ "\n\n"
166 ++ "\n" ++ show (pterm ps) ++ "\n\n"
165 ) $
167 ) $
166− case match_unify ctxt env topx topy inj (holes ps) of
168+ case match_unify ctxt env topx topy inj (holes ps) while of
167 OK u -> do let (h, ns) = unified ps
169 OK u -> do let (h, ns) = unified ps
168 put (ps { unified = (h, u ++ ns) })
170 put (ps { unified = (h, u ++ ns) })
169 return u
171 return u
170− Error e -> do put (ps { problems = (topx, topy, env, e, Match) :
172+ Error e -> do put (ps { problems = (topx, topy, env, e, while, Match) :
171 problems ps })
173 problems ps })
172 return []
174 return []
173-- traceWhen (unifylog ps)
175-- traceWhen (unifylog ps)
@@ -181,24 +183,25 @@ unify' :: Context -> Env -> TT Name -> TT Name ->
181 StateT TState TC [(Name, TT Name)]
183 StateT TState TC [(Name, TT Name)]
182unify' ctxt env topx topy =
184unify' ctxt env topx topy =
183 do ps <- get
185 do ps <- get
186+ let while = while_elaborating ps
184 let dont = dontunify ps
187 let dont = dontunify ps
185 let inj = injective ps
188 let inj = injective ps
186 (u, fails) <- traceWhen (unifylog ps)
189 (u, fails) <- traceWhen (unifylog ps)
187 ("Trying " ++ show (topx, topy) ++
190 ("Trying " ++ show (topx, topy) ++
188 "\nNormalised " ++ show (normalise ctxt env topx,
191 "\nNormalised " ++ show (normalise ctxt env topx,
189− normalise ctxt env topy) ++
192+ normalise ctxt env topy) ++
190 " in " ++ show env ++
193 " in " ++ show env ++
191 "\nHoles: " ++ show (holes ps)
194 "\nHoles: " ++ show (holes ps)
192− ++ "\nInjective: " ++ show (injective ps)
195+ ++ "\nInjective: " ++ show (injective ps)
193 ++ "\n") $
196 ++ "\n") $
194− lift $ unify ctxt env topx topy inj (holes ps)
197+ lift $ unify ctxt env topx topy inj (holes ps) while
195 let notu = filter (\ (n, t) -> case t of
198 let notu = filter (\ (n, t) -> case t of
196 P _ _ _ -> False
199 P _ _ _ -> False
197 _ -> n `elem` dont) u
200 _ -> n `elem` dont) u
198 traceWhen (unifylog ps)
201 traceWhen (unifylog ps)
199 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
202 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
200 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
203 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
201− ++ "\nNot unified:\n" ++ show (notunified ps)
204+ ++ "\nNot unified:\n" ++ show (notunified ps)
202 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
205 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
203-- ++ show (pterm ps)
206-- ++ show (pterm ps)
204 ++ "\n----------") $
207 ++ "\n----------") $
@@ -221,6 +224,21 @@ unify' ctxt env topx topy =
221 updateInj (_ : us) inj = updateInj us inj
224 updateInj (_ : us) inj = updateInj us inj
222 updateInj [] inj = inj
225 updateInj [] inj = inj
223
226
227+now_elaborating :: Monad m => FC -> Name -> Name -> StateT TState m ()
228+now_elaborating fc f arg = do ps <- get
229+ put ps {
230+ while_elaborating = FailContext fc f arg : while_elaborating ps
231+ }
232+
233+done_elaborating :: Monad m => Name -> Name -> StateT TState m ()
234+done_elaborating f x = do ps <- get
235+ let while = while_elaborating ps
236+ let while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
237+ put ps { while_elaborating = while' }
238+ where dropUntil p [] = []
239+ dropUntil p (x:xs) | p x = xs
240+ | otherwise = dropUntil p xs
241+
224getName :: Monad m => String -> StateT TState m Name
242getName :: Monad m => String -> StateT TState m Name
225getName tag = do ps <- get
243getName tag = do ps <- get
226 let n = nextname ps
244 let n = nextname ps
@@ -245,7 +263,7 @@ newProof n ctxt ty = let h = holeName 0
245 (P Bound h ty')) ty [] (h, []) []
263 (P Bound h ty')) ty [] (h, []) []
246 Nothing [] []
264 Nothing [] []
247 [] []
265 [] []
248− Nothing ctxt "" False False
266+ Nothing ctxt "" False False []
249
267
250type TState = ProofState -- [TacticAction])
268type TState = ProofState -- [TacticAction])
251type RunTactic = Context -> Env -> Term -> StateT TState TC Term
269type RunTactic = Context -> Env -> Term -> StateT TState TC Term
@@ -795,36 +813,38 @@ updateNotunified ns nu = up nu where
795 up ((n, t) : nus) = let t' = updateSolved ns t in
813 up ((n, t) : nus) = let t' = updateSolved ns t in
796 ((n, t') : up nus)
814 ((n, t') : up nus)
797
815
816+updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name]
817+ -> ([(Name, TT Name)], Fails)
798updateProblems ctxt [] ps inj holes = ([], ps)
818updateProblems ctxt [] ps inj holes = ([], ps)
799updateProblems ctxt ns ps inj holes = up ns ps where
819updateProblems ctxt ns ps inj holes = up ns ps where
800 up ns [] = (ns, [])
820 up ns [] = (ns, [])
801− up ns ((x, y, env, err, um) : ps) =
821+ up ns ((x, y, env, err, while, um) : ps) =
802 let x' = updateSolved ns x
822 let x' = updateSolved ns x
803 y' = updateSolved ns y
823 y' = updateSolved ns y
804 err' = updateError ns err
824 err' = updateError ns err
805 env' = updateEnv ns env in
825 env' = updateEnv ns env in
806-- trace ("Updating " ++ show (x',y')) $
826-- trace ("Updating " ++ show (x',y')) $
807− case unify ctxt env' x' y' inj holes of
827+ case unify ctxt env' x' y' inj holes while of
808 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
828 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
809 up (ns ++ v) ps
829 up (ns ++ v) ps
810 e -> -- trace ("Failed " ++ show e) $
830 e -> -- trace ("Failed " ++ show e) $
811 let (ns', ps') = up ns ps in
831 let (ns', ps') = up ns ps in
812− (ns', (x',y',env',err', um) : ps')
832+ (ns', (x',y',env',err', while, um) : ps')
813
833
814-- attempt to solve remaining problems with match_unify
834-- attempt to solve remaining problems with match_unify
815matchProblems all ns ctxt ps inj holes = up ns ps where
835matchProblems all ns ctxt ps inj holes = up ns ps where
816 up ns [] = (ns, [])
836 up ns [] = (ns, [])
817− up ns ((x, y, env, err, um) : ps)
837+ up ns ((x, y, env, err, while, um) : ps)
818 | all || um == Match =
838 | all || um == Match =
819 let x' = updateSolved ns x
839 let x' = updateSolved ns x
820 y' = updateSolved ns y
840 y' = updateSolved ns y
821 err' = updateError ns err
841 err' = updateError ns err
822 env' = updateEnv ns env in
842 env' = updateEnv ns env in
823− case match_unify ctxt env' x' y' inj holes of
843+ case match_unify ctxt env' x' y' inj holes while of
824 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
844 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
825 up (ns ++ v) ps
845 up (ns ++ v) ps
826 _ -> let (ns', ps') = up ns ps in
846 _ -> let (ns', ps') = up ns ps in
827− (ns', (x',y',env',err',um) : ps')
847+ (ns', (x', y', env', err', while, um) : ps')
828 up ns (p : ps) = let (ns', ps') = up ns ps in
848 up ns (p : ps) = let (ns', ps') = up ns ps in
829 (ns', p : ps')
849 (ns', p : ps')
830
850
src/Idris/Core/Unify.hs+20−14
@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2
2
3−module Idris.Core.Unify(match_unify, unify, Fails, FailAt(..)) where
3+module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..)) where
4
4
5import Idris.Core.TT
5import Idris.Core.TT
6import Idris.Core.Evaluate
6import Idris.Core.Evaluate
@@ -21,8 +21,14 @@ import Debug.Trace
21data FailAt = Match | Unify
21data FailAt = Match | Unify
22 deriving (Show, Eq)
22 deriving (Show, Eq)
23
23
24+data FailContext = FailContext { fail_sourceloc :: FC,
25+ fail_fn :: Name,
26+ fail_param :: Name
27+ }
28+ deriving (Eq, Show)
29+
24type Injs = [(TT Name, TT Name, TT Name)]
30type Injs = [(TT Name, TT Name, TT Name)]
25−type Fails = [(TT Name, TT Name, Env, Err, FailAt)]
31+type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]
26
32
27data UInfo = UI Int Fails
33data UInfo = UI Int Fails
28 deriving Show
34 deriving Show
@@ -34,10 +40,10 @@ data UResult a = UOK a
34-- Solve metavariables by matching terms against each other
40-- Solve metavariables by matching terms against each other
35-- Not really unification, of course!
41-- Not really unification, of course!
36
42
37−match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
43+match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->
38 TC [(Name, TT Name)]
44 TC [(Name, TT Name)]
39−match_unify ctxt env topx topy inj holes =
45+match_unify ctxt env topx topy inj holes from =
40− case runStateT (un [] (renameBindersTm env topx)
46+ case runStateT (un [] (renameBindersTm env topx)
41 (renameBindersTm env topy)) (UI 0 []) of
47 (renameBindersTm env topy)) (UI 0 []) of
42 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
48 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
43 res ->
49 res ->
@@ -86,7 +92,7 @@ match_unify ctxt env topx topy inj holes =
86 let err = CantUnify r
92 let err = CantUnify r
87 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
93 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
88 if (not r) then lift $ tfail err
94 if (not r) then lift $ tfail err
89− else do put (UI s ((x, y, env, err, Match) : f))
95+ else do put (UI s ((x, y, env, err, from, Match) : f))
90 lift $ tfail err
96 lift $ tfail err
91
97
92
98
@@ -100,7 +106,7 @@ match_unify ctxt env topx topy inj holes =
100 let err = CantUnify r topx topy
106 let err = CantUnify r topx topy
101 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
107 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
102 (errEnv env) s
108 (errEnv env) s
103− put (UI s ((binderTy x, binderTy y, env, err, Match) : f))
109+ put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))
104 return []
110 return []
105
111
106 -- TODO: there's an annoying amount of repetition between this and the
112 -- TODO: there's an annoying amount of repetition between this and the
@@ -113,7 +119,7 @@ match_unify ctxt env topx topy inj holes =
113 let r = recoverable x y
119 let r = recoverable x y
114 let err = CantUnify r
120 let err = CantUnify r
115 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
121 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
116− put (UI s ((x, y, env, err, Match) : f))
122+ put (UI s ((x, y, env, err, from, Match) : f))
117 lift $ tfail err
123 lift $ tfail err
118 combine bnames as [] = return as
124 combine bnames as [] = return as
119 combine bnames as ((n, t) : bs)
125 combine bnames as ((n, t) : bs)
@@ -188,9 +194,9 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)
188 = doSubst env tm
194 = doSubst env tm
189
195
190
196
191−unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->
197+unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->
192 TC ([(Name, TT Name)], Fails)
198 TC ([(Name, TT Name)], Fails)
193−unify ctxt env topx topy inj holes =
199+unify ctxt env topx topy inj holes from =
194-- trace ("Unifying " ++ show (topx, topy)) $
200-- trace ("Unifying " ++ show (topx, topy)) $
195 -- don't bother if topx and topy are different at the head
201 -- don't bother if topx and topy are different at the head
196 case runStateT (un False [] (renameBindersTm env topx)
202 case runStateT (un False [] (renameBindersTm env topx)
@@ -367,7 +373,7 @@ unify ctxt env topx topy inj holes =
367 let err = CantUnify r
373 let err = CantUnify r
368 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
374 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
369 if (not r) then lift $ tfail err
375 if (not r) then lift $ tfail err
370− else do put (UI s ((x, y, env, err, Unify) : f))
376+ else do put (UI s ((x, y, env, err, from, Unify) : f))
371 return [] -- lift $ tfail err
377 return [] -- lift $ tfail err
372
378
373 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
379 unApp fn bnames appx@(App fx ax) appy@(App fy ay)
@@ -466,7 +472,7 @@ unify ctxt env topx topy inj holes =
466 let r = recoverable x y
472 let r = recoverable x y
467 let err = CantUnify r
473 let err = CantUnify r
468 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
474 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
469− put (UI s ((topx, topy, env, err, Unify) : f))
475+ put (UI s ((topx, topy, env, err, from, Unify) : f))
470 return []
476 return []
471
477
472 -- shortcut failure, if we *know* nothing can fix it
478 -- shortcut failure, if we *know* nothing can fix it
@@ -474,7 +480,7 @@ unify ctxt env topx topy inj holes =
474 let r = recoverable x y
480 let r = recoverable x y
475 let err = CantUnify r
481 let err = CantUnify r
476 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
482 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
477− put (UI s ((topx, topy, env, err, Unify) : f))
483+ put (UI s ((topx, topy, env, err, from, Unify) : f))
478 lift $ tfail err
484 lift $ tfail err
479
485
480
486
@@ -497,7 +503,7 @@ unify ctxt env topx topy inj holes =
497 let err = CantUnify r topx topy
503 let err = CantUnify r topx topy
498 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
504 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
499 (errEnv env) s
505 (errEnv env) s
500− put (UI s ((binderTy x, binderTy y, env, err, Unify) : f))
506+ put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))
501 return [] -- lift $ tfail err
507 return [] -- lift $ tfail err
502
508
503 checkCycle ns p@(x, P _ _ _) = return [p]
509 checkCycle ns p@(x, P _ _ _) = return [p]
src/Idris/ElabDecls.hs+2−2
@@ -1389,7 +1389,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1389 inj <- get_inj
1389 inj <- get_inj
1390 return (res, probs, inj))
1390 return (res, probs, inj))
1391
1391
1392− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1392+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1393
1393
1394 let lhs_tm = orderPats (getInferTerm lhs')
1394 let lhs_tm = orderPats (getInferTerm lhs')
1395 let lhs_ty = getInferType lhs'
1395 let lhs_ty = getInferType lhs'
@@ -1453,7 +1453,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1453 probs <- get_probs
1453 probs <- get_probs
1454 return (tm, ds, is, probs))
1454 return (tm, ds, is, probs))
1455
1455
1456− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)
1456+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)
1457
1457
1458 logLvl 5 "DONE CHECK"
1458 logLvl 5 "DONE CHECK"
1459 logLvl 2 $ "---> " ++ show rhs'
1459 logLvl 2 $ "---> " ++ show rhs'
src/Idris/ElabTerm.hs+4−4
@@ -81,8 +81,8 @@ build ist info pattern opts fn tm
81 probs <- get_probs
81 probs <- get_probs
82 case probs of
82 case probs of
83 [] -> return ()
83 [] -> return ()
84− ((_,_,_,e,_):es) -> if inf then return ()
84+ ((_,_,_,e,_,_):es) -> if inf then return ()
85− else lift (Error e)
85+ else lift (Error e)
86 is <- getAux
86 is <- getAux
87 tt <- get_term
87 tt <- get_term
88 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
88 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
@@ -109,8 +109,8 @@ buildTC ist info pattern opts fn tm
109 tm <- get_term
109 tm <- get_term
110 case probs of
110 case probs of
111 [] -> return ()
111 [] -> return ()
112− ((_,_,_,e,_):es) -> if inf then return ()
112+ ((_,_,_,e,_,_):es) -> if inf then return ()
113− else lift (Error e)
113+ else lift (Error e)
114 is <- getAux
114 is <- getAux
115 tt <- get_term
115 tt <- get_term
116 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
116 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
src/Idris/Prover.hs+2−2
@@ -89,10 +89,10 @@ elabStep st e = do case runStateT e st of
89 Error a -> ierror a
89 Error a -> ierror a
90
90
91dumpState :: IState -> ProofState -> Idris ()
91dumpState :: IState -> ProofState -> Idris ()
92−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
92+dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
93 do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."
93 do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."
94 iputGoal rendered
94 iputGoal rendered
95−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
95+dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) = do
96 let OK ty = goalAtFocus ps
96 let OK ty = goalAtFocus ps
97 let OK env = envAtFocus ps
97 let OK env = envAtFocus ps
98 let state = prettyOtherGoals hs <> line <>
98 let state = prettyOtherGoals hs <> line <>