42c694c · Idris-dev · git.iko.soy

CHANGELOG+11−4

@@ -1,9 +1,16 @@

1New in 0.9.15:

2--------------

3−* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.

3+* Two new tactics: skip and fail. Skip does nothing, and fail takes a string

4+ as an argument and produces it as an error.

4−* 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.

5+* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list

6+ of ErrorReportParts as an argument, like error handlers produce, allowing

7+ access to the pretty-printer.

5−* Stop showing irrelevant and inaccessible internal names in the interactive prover

8+* Stop showing irrelevant and inaccessible internal names in the interactive

9+ prover.

6−* The proof arguments in the List library functions are now implicit and solved automatically

10+* The proof arguments in the List library functions are now implicit and

11+ solved automatically.

12+* More efficient representation of proof state, leading to faster elaboration

13+ of large expressions.

7

14

8New in 0.9.14:

15New in 0.9.14:

9--------------

16--------------

libs/prelude/Prelude/Fin.idr+2−1

@@ -133,11 +133,12 @@ natToFin (S k) (S j) with (natToFin k j)

133natToFin _ _ = Nothing

134

135integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)

136+integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!

136integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing

137integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing

137

138

138||| Proof that some `Maybe` is actually `Just`

139||| Proof that some `Maybe` is actually `Just`

139data IsJust : Maybe a -> Type where

140data IsJust : Maybe a -> Type where

140− ItIsJust : IsJust {a} (Just x)

141+ ItIsJust : IsJust (Just x)

141

142

142||| Allow overloading of Integer literals for Fin.

143||| Allow overloading of Integer literals for Fin.

143||| @ x the Integer that the user typed

144||| @ x the Integer that the user typed

src/Idris/Core/Elaborate.hs+12−4

@@ -498,10 +498,9 @@ apply' fillt fn imps =

498 -- (remove from unified list before calling end_unify)

499 hs <- get_holes

500 ES (p, a) s prev <- get

501− let dont = head hs : dontunify p ++

502− if null imps then [] -- do all we can

501+ let dont = if null imps

503− else

502+ then head hs : dontunify p

504− map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

503+ else getNonUnify (head hs : dontunify p) imps args

505 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

504 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

506 unified p

505 unified p

507 let unify = -- trace ("Not done " ++ show hs) $

506 let unify = -- trace ("Not done " ++ show hs) $

@@ -520,6 +519,15 @@ apply' fillt fn imps =

520 Just (P _ t _) -> t

519 Just (P _ t _) -> t

521 _ -> n

520 _ -> n

522

521

522+ getNonUnify acc [] _ = acc

523+ getNonUnify acc _ [] = acc

524+ getNonUnify acc ((i,_):is) ((a, t):as)

525+ | i = getNonUnify acc is as

526+ | otherwise = getNonUnify (t : acc) is as

527+

528+-- getNonUnify imps args = map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

529+

530+

523apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

531apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

524apply2 fn elabs =

532apply2 fn elabs =

525 do args <- prepare_apply fn (map isJust elabs)

533 do args <- prepare_apply fn (map isJust elabs)

src/Idris/Core/ProofTerm.hs+33−16

@@ -125,25 +125,42 @@ updateSolvedTerm :: [(Name, Term)] -> Term -> Term

125updateSolvedTerm [] x = x

126updateSolvedTerm xs x = -- updateSolved' xs x where

127-- This version below saves allocations, because it doesn't need to reallocate

128−-- the term if there are no updates to do, but costs an extra pass. Below

128+-- the term if there are no updates to do.

129−-- version works better on larger terms...

129+-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is

130− if noneOf (map fst xs) x

130+-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).

131− then x

132− else updateSolved' xs x where

131+ fst $ updateSolved' xs x where

133− updateSolved' [] x = x

132+ updateSolved' [] x = (x, False)

134 updateSolved' xs (Bind n (Hole ty) t)

133 updateSolved' xs (Bind n (Hole ty) t)

135 | Just v <- lookup n xs

134 | Just v <- lookup n xs

136 = case xs of

135 = case xs of

137− [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume

136+ [_] -> (substV v $ psubst n v t, True) -- some may be Vs! Can't assume

138− -- explicit names

137+ -- explicit names

138+ _ -> let (t', _) = updateSolved' xs t in

139− _ -> substV v $ psubst n v (updateSolved' xs t)

139+ (substV v $ psubst n v t', True)

140− updateSolved' xs (Bind n b t)

140+ updateSolved' xs tm@(Bind n b t)

141− | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

141+ | otherwise = let (t', ut) = updateSolved' xs t

142+ (b', ub) = updateSolvedB' xs b in

143+ if ut || ub then (Bind n b' t', True)

144+ else (tm, False)

142− updateSolved' xs (App f a)

145+ updateSolved' xs t@(App f a)

146+ = let (f', uf) = updateSolved' xs f

143− = App (updateSolved' xs f) (updateSolved' xs a)

147+ (a', ua) = updateSolved' xs a in

148+ if uf || ua then (App f' a', True)

149+ else (t, False)

144− updateSolved' xs (P _ n@(MN _ _) _)

150+ updateSolved' xs t@(P _ n@(MN _ _) _)

145− | Just v <- lookup n xs = v

151+ | Just v <- lookup n xs = (v, True)

152+ updateSolved' xs t = (t, False)

153+

154+ updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

155+ (v', uv) = updateSolved' xs v in

156+ if ut || uv then (Let t' v', True)

157+ else (b, False)

146− updateSolved' xs t = t

158+ updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t

159+ (v', uv) = updateSolved' xs v in

160+ if ut || uv then (Guess t' v', True)

161+ else (b, False)

162+ updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in

163+ if u then (b { binderTy = ty' }, u) else (b, False)

147

164

148 noneOf ns (P _ n _) | n `elem` ns = False

165 noneOf ns (P _ n _) | n `elem` ns = False

149 noneOf ns (App f a) = noneOf ns a && noneOf ns f

166 noneOf ns (App f a) = noneOf ns a && noneOf ns f

src/Idris/Core/TT.hs+31−1

@@ -935,7 +935,37 @@ subst :: Eq n => n {-^ The id to replace -} ->

935 TT n {-^ The replacement term -} ->

936 TT n {-^ The term to replace in -} ->

937 TT n

938−subst n v tm = instantiate v (pToV n tm)

938+-- subst n v tm = instantiate v (pToV n tm)

939+subst n v tm = fst $ subst' 0 tm

940+ where

941+ -- keep track of updates to save allocations - this is a big win on

942+ -- large terms in particular

943+ -- ('Maybe' would be neater here, but >>= is not the right combinator.

944+ -- Feel free to tidy up, as long as it still saves allocating when no

945+ -- substitution happens...)

946+ subst' i (V x) | i == x = (v, True)

947+ subst' i (P _ x _) | n == x = (v, True)

948+ subst' i t@(Bind x b sc) | x /= n

949+ = let (b', ub) = substB' i b

950+ (sc', usc) = subst' (i+1) sc in

951+ if ub || usc then (Bind x b' sc', True) else (t, False)

952+ subst' i t@(App f a) = let (f', uf) = subst' i f

953+ (a', ua) = subst' i a in

954+ if uf || ua then (App f' a', True) else (t, False)

955+ subst' i t@(Proj x idx) = let (x', u) = subst' i x in

956+ if u then (Proj x' idx, u) else (t, False)

957+ subst' i t = (t, False)

958+

959+ substB' i b@(Let t v) = let (t', ut) = subst' i t

960+ (v', uv) = subst' i v in

961+ if ut || uv then (Let t' v', True)

962+ else (b, False)

963+ substB' i b@(Guess t v) = let (t', ut) = subst' i t

964+ (v', uv) = subst' i v in

965+ if ut || uv then (Guess t' v', True)

966+ else (b, False)

967+ substB' i b = let (ty', u) = subst' i (binderTy b) in

968+ if u then (b { binderTy = ty' }, u) else (b, False)

939

969

940-- If there are no Vs in the term (i.e. in proof state)

970-- If there are no Vs in the term (i.e. in proof state)

941psubst :: Eq n => n -> TT n -> TT n -> TT n

971psubst :: Eq n => n -> TT n -> TT n -> TT n

src/Idris/ElabTerm.hs+1−1

@@ -244,7 +244,7 @@ elab ist info emode opts fn tm

244 elab' ina (PConstant c) = do apply (RConstant c) []; solve

245 elab' ina (PQuote r) = do fill r; solve

246 elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))

247− (elab' ina (PRef fc unitTy))

247+ (elab' ina (PRef fc unitTy))

248 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

249 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

250 = do g <- goal; resolveTC False 5 g fn ist

test/proof002/expected+1−1

@@ -1,7 +1,7 @@

1Reflect.idr:207:38:When elaborating right hand side of testReflect1:

2When elaborating an application of function Reflect.getJust:

3 Can't unify

4− IsJust (Just x2)

4+ IsJust (Just x1)

5 with

6 IsJust (prove (getProof x))

7