git.iko.soy/Idris-dev
on master help sign in
Another minor efficiency gain in elaborator
70a041fEdwin Brady
effects/Effects.idr+2−2
compare with master
unifiedsplit
@@ -119,14 +119,14 @@ data EffM : (m : Type -> Type) ->
119-- Eff : List (EFFECT m) -> Type -> Type
119-- Eff : List (EFFECT m) -> Type -> Type
120
120
121implicit
121implicit
122−lift' : {default tactics { applyTactic findSubList 100; solve; }
122+lift' : {default tactics { applyTactic findSubList 20; solve; }
123 prf : SubList ys xs} ->
123 prf : SubList ys xs} ->
124 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
124 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
125lift' {prf} e = lift prf e
125lift' {prf} e = lift prf e
126
126
127implicit
127implicit
128effect' : {a, b: _} -> {e : Effect} ->
128effect' : {a, b: _} -> {e : Effect} ->
129− {default tactics { applyTactic findEffElem 100; solve; }
129+ {default tactics { applyTactic findEffElem 20; solve; }
130 prf : EffElem e a xs} ->
130 prf : EffElem e a xs} ->
131 (eff : e a b t) ->
131 (eff : e a b t) ->
132 EffM m xs (updateResTy xs prf eff) t
132 EffM m xs (updateResTy xs prf eff) t
src/Core/ProofState.hs+1−4
@@ -741,9 +741,6 @@ processTactic t ps
741 = case holes ps of
741 = case holes ps of
742 [] -> fail "Nothing to fill in."
742 [] -> fail "Nothing to fill in."
743 (h:_) -> do ps' <- execStateT (process t h) ps
743 (h:_) -> do ps' <- execStateT (process t h) ps
744− let pterm' = case solved ps' of
745− Just s -> updateSolved [s] (pterm ps')
746− _ -> pterm ps'
747 let (ns', probs')
744 let (ns', probs')
748 = case solved ps' of
745 = case solved ps' of
749 Just s -> updateProblems (context ps')
746 Just s -> updateProblems (context ps')
@@ -753,7 +750,7 @@ processTactic t ps
753 _ -> ([], problems ps')
750 _ -> ([], problems ps')
754 -- rechecking problems may find more solutions, so
751 -- rechecking problems may find more solutions, so
755 -- apply them here
752 -- apply them here
756− let pterm'' = updateSolved ns' pterm'
753+ let pterm'' = updateSolved ns' (pterm ps')
757 return (ps' { pterm = pterm'',
754 return (ps' { pterm = pterm'',
758 solved = Nothing,
755 solved = Nothing,
759 problems = probs',
756 problems = probs',