git.iko.soy/Idris-dev
on master help sign in
Don't reset totality for non-total things
e803aeaEdwin Brady
libs/base/Data/Vect/Quantifiers.idr+2−2
compare with master
unifiedsplit
@@ -5,8 +5,8 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
6
6
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8−anyNilAbsurd Here impossible
8+anyNilAbsurd (Here _) impossible
9−anyNilAbsurd There impossible
9+anyNilAbsurd (There _) impossible
10
10
11anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
11anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
12anyElim _ f (Here p) = f p
12anyElim _ f (Here p) = f p
src/Idris/Parser.hs+4−1
@@ -1054,7 +1054,10 @@ loadSource h lidr f
1054 -- Redo totality check for deferred names
1054 -- Redo totality check for deferred names
1055 let deftots = idris_defertotcheck i
1055 let deftots = idris_defertotcheck i
1056 iLOG $ "Totality checking " ++ show deftots
1056 iLOG $ "Totality checking " ++ show deftots
1057+ mapM_ (\x -> do tot <- getTotality x
1058+ case tot of
1057− mapM_ (\x -> setTotality x Unchecked) (map snd deftots)
1059+ Total _ -> setTotality x Unchecked
1060+ _ -> return ()) (map snd deftots)
1058 mapM_ buildSCG deftots
1061 mapM_ buildSCG deftots
1059 mapM_ checkDeclTotality deftots
1062 mapM_ checkDeclTotality deftots
1060
1063