ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

More efficiency improvements

Browse Source 
More efforts to avoid allocation where no updates happen.
This commit is contained in:
Edwin Brady 2014-08-06 18:25:01 +01:00
parent 02f7c649ac
commit 42c694ced4
7 changed files with 91 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
CHANGELOG
View File

@ -1,9 +1,16 @@
New in 0.9.15:
--------------
* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.
* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.
* Stop showing irrelevant and inaccessible internal names in the interactive prover
* The proof arguments in the List library functions are now implicit and solved automatically
* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
as an argument and produces it as an error.
* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list
of ErrorReportParts as an argument, like error handlers produce, allowing
access to the pretty-printer.
* Stop showing irrelevant and inaccessible internal names in the interactive
prover.
* The proof arguments in the List library functions are now implicit and
solved automatically.
* More efficient representation of proof state, leading to faster elaboration
of large expressions.
New in 0.9.14:
--------------

3
libs/prelude/Prelude/Fin.idr
View File

@ -133,11 +133,12 @@ natToFin (S k) (S j) with (natToFin k j)
natToFin _ _ = Nothing
integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
||| Proof that some `Maybe` is actually `Just`
data IsJust : Maybe a -> Type where
ItIsJust : IsJust {a} (Just x)
ItIsJust : IsJust (Just x)
||| Allow overloading of Integer literals for Fin.
||| @ x the Integer that the user typed

16
src/Idris/Core/Elaborate.hs
View File

@ -498,10 +498,9 @@ apply' fillt fn imps =
-- (remove from unified list before calling end_unify)
hs <- get_holes
ES (p, a) s prev <- get
let dont = head hs : dontunify p ++
if null imps then [] -- do all we can
else
map fst (filter (not . snd) (zip (map snd args) (map fst imps)))
let dont = if null imps
then head hs : dontunify p
else getNonUnify (head hs : dontunify p) imps args
let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $
unified p
let unify = -- trace ("Not done " ++ show hs) $
@ -520,6 +519,15 @@ apply' fillt fn imps =
Just (P _ t _) -> t
_ -> n
getNonUnify acc [] _ = acc
getNonUnify acc _ [] = acc
getNonUnify acc ((i,_):is) ((a, t):as)
| i = getNonUnify acc is as
| otherwise = getNonUnify (t : acc) is as
-- getNonUnify imps args = map fst (filter (not . snd) (zip (map snd args) (map fst imps)))
apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
apply2 fn elabs =
do args <- prepare_apply fn (map isJust elabs)

49
src/Idris/Core/ProofTerm.hs
View File

@ -125,25 +125,42 @@ updateSolvedTerm :: [(Name, Term)] -> Term -> Term
updateSolvedTerm [] x = x
updateSolvedTerm xs x = -- updateSolved' xs x where
-- This version below saves allocations, because it doesn't need to reallocate
-- the term if there are no updates to do, but costs an extra pass. Below
-- version works better on larger terms...
if noneOf (map fst xs) x
then x
else updateSolved' xs x where
updateSolved' [] x = x
-- the term if there are no updates to do.
-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
fst $ updateSolved' xs x where
updateSolved' [] x = (x, False)
updateSolved' xs (Bind n (Hole ty) t)
| Just v <- lookup n xs
= case xs of
[_] -> substV v $ psubst n v t -- some may be Vs! Can't assume
-- explicit names
_ -> substV v $ psubst n v (updateSolved' xs t)
updateSolved' xs (Bind n b t)
| otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
updateSolved' xs (App f a)
= App (updateSolved' xs f) (updateSolved' xs a)
updateSolved' xs (P _ n@(MN _ _) _)
| Just v <- lookup n xs = v
updateSolved' xs t = t
[_] -> (substV v $ psubst n v t, True) -- some may be Vs! Can't assume
-- explicit names
_ -> let (t', _) = updateSolved' xs t in
(substV v $ psubst n v t', True)
updateSolved' xs tm@(Bind n b t)
| otherwise = let (t', ut) = updateSolved' xs t
(b', ub) = updateSolvedB' xs b in
if ut || ub then (Bind n b' t', True)
else (tm, False)
updateSolved' xs t@(App f a)
= let (f', uf) = updateSolved' xs f
(a', ua) = updateSolved' xs a in
if uf || ua then (App f' a', True)
else (t, False)
updateSolved' xs t@(P _ n@(MN _ _) _)
| Just v <- lookup n xs = (v, True)
updateSolved' xs t = (t, False)
updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t
(v', uv) = updateSolved' xs v in
if ut || uv then (Let t' v', True)
else (b, False)
updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t
(v', uv) = updateSolved' xs v in
if ut || uv then (Guess t' v', True)
else (b, False)
updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
if u then (b { binderTy = ty' }, u) else (b, False)
noneOf ns (P _ n _) | n `elem` ns = False
noneOf ns (App f a) = noneOf ns a && noneOf ns f

32
src/Idris/Core/TT.hs
View File

@ -935,7 +935,37 @@ subst :: Eq n => n {-^ The id to replace -} ->
TT n {-^ The replacement term -} ->
TT n {-^ The term to replace in -} ->
TT n
subst n v tm = instantiate v (pToV n tm)
-- subst n v tm = instantiate v (pToV n tm)
subst n v tm = fst $ subst' 0 tm
where
-- keep track of updates to save allocations - this is a big win on
-- large terms in particular
-- ('Maybe' would be neater here, but >>= is not the right combinator.
-- Feel free to tidy up, as long as it still saves allocating when no
-- substitution happens...)
subst' i (V x) | i == x = (v, True)
subst' i (P _ x _) | n == x = (v, True)
subst' i t@(Bind x b sc) | x /= n
= let (b', ub) = substB' i b
(sc', usc) = subst' (i+1) sc in
if ub || usc then (Bind x b' sc', True) else (t, False)
subst' i t@(App f a) = let (f', uf) = subst' i f
(a', ua) = subst' i a in
if uf || ua then (App f' a', True) else (t, False)
subst' i t@(Proj x idx) = let (x', u) = subst' i x in
if u then (Proj x' idx, u) else (t, False)
subst' i t = (t, False)
substB' i b@(Let t v) = let (t', ut) = subst' i t
(v', uv) = subst' i v in
if ut || uv then (Let t' v', True)
else (b, False)
substB' i b@(Guess t v) = let (t', ut) = subst' i t
(v', uv) = subst' i v in
if ut || uv then (Guess t' v', True)
else (b, False)
substB' i b = let (ty', u) = subst' i (binderTy b) in
if u then (b { binderTy = ty' }, u) else (b, False)
-- If there are no Vs in the term (i.e. in proof state)
psubst :: Eq n => n -> TT n -> TT n -> TT n

2
src/Idris/ElabTerm.hs
View File

@ -244,7 +244,7 @@ elab ist info emode opts fn tm
elab' ina (PConstant c) = do apply (RConstant c) []; solve
elab' ina (PQuote r) = do fill r; solve
elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
(elab' ina (PRef fc unitTy))
(elab' ina (PRef fc unitTy))
elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
= do g <- goal; resolveTC False 5 g fn ist

2
test/proof002/expected
View File

@ -1,7 +1,7 @@
Reflect.idr:207:38:When elaborating right hand side of testReflect1:
When elaborating an application of function Reflect.getJust:
Can't unify
IsJust (Just x2)
IsJust (Just x1)
with
IsJust (prove (getProof x))