git.iko.soy/Idris-dev
on master help sign in
Another minor efficiency gain in elaborator

Call updateSolved less often. Also cut down search in Effects to depth of 20 (this still needs to be done better, but it seems to have a large effect on typechecking time for effects programs).

commit70a041f91bfd2d59ab42a5f114061831509f6c66 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 28 Sep 2013, 12:16 (13 years ago) parent2c588b9
2 files changed+3−6
compare with master
unifiedsplit
effects/Effects.idr+2−2 src/Core/ProofState.hs+1−4
effects/Effects.idr+2−2
@@ -119,14 +119,14 @@ data EffM : (m : Type -> Type) ->
119119-- Eff : List (EFFECT m) -> Type -> Type
120120
121121implicit
122−lift' : {default tactics { applyTactic findSubList 100; solve; }
122+lift' : {default tactics { applyTactic findSubList 20; solve; }
123123 prf : SubList ys xs} ->
124124 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
125125lift' {prf} e = lift prf e
126126
127127implicit
128128effect' : {a, b: _} -> {e : Effect} ->
129− {default tactics { applyTactic findEffElem 100; solve; }
129+ {default tactics { applyTactic findEffElem 20; solve; }
130130 prf : EffElem e a xs} ->
131131 (eff : e a b t) ->
132132 EffM m xs (updateResTy xs prf eff) t
src/Core/ProofState.hs+1−4
@@ -741,9 +741,6 @@ processTactic t ps
741741 = case holes ps of
742742 [] -> fail "Nothing to fill in."
743743 (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'
747744 let (ns', probs')
748745 = case solved ps' of
749746 Just s -> updateProblems (context ps')
@@ -753,7 +750,7 @@ processTactic t ps
753750 _ -> ([], problems ps')
754751 -- rechecking problems may find more solutions, so
755752 -- apply them here
756− let pterm'' = updateSolved ns' pterm'
753+ let pterm'' = updateSolved ns' (pterm ps')
757754 return (ps' { pterm = pterm'',
758755 solved = Nothing,
759756 problems = probs',