various stdlib updates

libs/base/Data/Bool.idr

@@ -0,0 +1,99 @@
+module Data.Bool
+
+%default total
+
+export
+notInvolutive : (x : Bool) -> not (not x) = x
+notInvolutive True  = Refl
+notInvolutive False = Refl
+
+-- AND
+
+export
+andSameNeutral : (x : Bool) -> x && x = x
+andSameNeutral False = Refl
+andSameNeutral True = Refl
+
+export
+andFalseFalse : (x : Bool) -> x && False = False
+andFalseFalse False = Refl
+andFalseFalse True = Refl
+
+export
+andTrueNeutral : (x : Bool) -> x && True = x
+andTrueNeutral False = Refl
+andTrueNeutral True = Refl
+
+export
+andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
+andAssociative True  _ _ = Refl
+andAssociative False _ _ = Refl
+
+export
+andCommutative : (x, y : Bool) -> x && y = y && x
+andCommutative x True  = andTrueNeutral x
+andCommutative x False = andFalseFalse x
+
+export
+andNotFalse : (x : Bool) -> x && not x = False
+andNotFalse False = Refl
+andNotFalse True = Refl
+
+-- OR
+
+export
+orSameNeutral : (x : Bool) -> x || x = x
+orSameNeutral False = Refl
+orSameNeutral True = Refl
+
+export
+orFalseNeutral : (x : Bool) -> x || False = x
+orFalseNeutral False = Refl
+orFalseNeutral True = Refl
+
+export
+orTrueTrue : (x : Bool) -> x || True = True
+orTrueTrue False = Refl
+orTrueTrue True = Refl
+
+export
+orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
+orAssociative True  _ _ = Refl
+orAssociative False _ _ = Refl
+
+export
+orCommutative : (x, y : Bool) -> x || y = y || x
+orCommutative x True  = orTrueTrue x
+orCommutative x False = orFalseNeutral x
+
+export
+orNotTrue : (x : Bool) -> x || not x = True
+orNotTrue False = Refl
+orNotTrue True = Refl
+
+-- interaction & De Morgan's laws
+
+export
+orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
+orSameAndRightNeutral False _ = Refl
+orSameAndRightNeutral True  _ = Refl
+
+export
+andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
+andDistribOrR False _ _ = Refl
+andDistribOrR True  _ _ = Refl
+
+export
+orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
+orDistribAndR False _ _ = Refl
+orDistribAndR True  _ _ = Refl
+
+export
+notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
+notAndIsOr False _ = Refl
+notAndIsOr True  _ = Refl
+
+export
+notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
+notOrIsAnd False _ = Refl
+notOrIsAnd True  _ = Refl

libs/base/Data/Bool/Xor.idr

@@ -0,0 +1,64 @@
+module Data.Bool.Xor
+
+import Data.Bool
+
+%default total
+
+public export
+xor : Bool -> Bool -> Bool
+xor True True = False
+xor False False = False
+xor _ _ = True
+
+export
+xorSameFalse : (b : Bool) -> xor b b = False
+xorSameFalse False = Refl
+xorSameFalse True = Refl
+
+export
+xorFalseNeutral : (b : Bool) -> xor False b = b
+xorFalseNeutral False = Refl
+xorFalseNeutral True = Refl
+
+export
+xorTrueNot : (b : Bool) -> xor True b = not b
+xorTrueNot False = Refl
+xorTrueNot True  = Refl
+
+export
+notXor : (a, b : Bool) -> not (xor a b) = xor (not a) b
+notXor True  b = rewrite xorFalseNeutral b in
+                 rewrite xorTrueNot b in
+                 notInvolutive b
+notXor False b = rewrite xorFalseNeutral b in
+                 sym $ xorTrueNot b
+
+export
+notXorCancel : (a, b : Bool) -> xor (not a) (not b) = xor a b
+notXorCancel True  b = rewrite xorFalseNeutral (not b) in
+                       sym $ xorTrueNot b
+notXorCancel False b = rewrite xorFalseNeutral b in
+                       rewrite xorTrueNot (not b) in
+                       notInvolutive b
+
+export
+xorAssociative : (a, b, c : Bool) -> xor (xor a b) c = xor a (xor b c)
+xorAssociative False b c =
+  rewrite xorFalseNeutral b in
+  sym $ xorFalseNeutral (xor b c)
+xorAssociative True  b c =
+  rewrite xorTrueNot b in
+  rewrite xorTrueNot (xor b c) in
+  sym $ notXor b c
+
+export
+xorCommutative : (a, b : Bool) -> xor a b = xor b a
+xorCommutative False False = Refl
+xorCommutative False True  = Refl
+xorCommutative True  False = Refl
+xorCommutative True  True  = Refl
+
+export
+xorNotTrue : (a : Bool) -> a `xor` (not a) = True
+xorNotTrue False = Refl
+xorNotTrue True  = Refl

libs/base/Data/Fin.idr

@@ -79,6 +79,14 @@ weakenN : (n : Nat) -> Fin m -> Fin (m + n)
 weakenN n FZ = FZ
 weakenN n (FS f) = FS (weakenN n f)
 
+||| Weaken the bound on a Fin using a constructive comparison
+public export
+weakenLTE : Fin n -> LTE n m -> Fin m
+weakenLTE  FZ     LTEZero impossible
+weakenLTE (FS _)  LTEZero impossible
+weakenLTE  FZ    (LTESucc y) = FZ
+weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y
+
 ||| Attempt to tighten the bound on a Fin.
 ||| Return `Left` if the bound could not be tightened, or `Right` if it could.
 export

libs/base/Data/Nat.idr

@@ -319,6 +319,11 @@ plusLeftLeftRightZero left right p =
     rewrite plusZeroRightNeutral left in
       p
 
+plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
+plusLteMonotoneRight p  Z     r     LTEZero    = rewrite plusCommutative r p in
+                                                 lteAddRight p
+plusLteMonotoneRight p (S q) (S r) (LTESucc l) = LTESucc $ plusLteMonotoneRight p q r l
+
 -- Proofs on *
 
 export
@@ -426,6 +431,14 @@ minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
 minusPlusZero Z     _ = Refl
 minusPlusZero (S n) m = minusPlusZero n m
 
+export
+plusMinusLte : (n, m : Nat) -> LTE n m -> (minus m n) + n = m
+plusMinusLte  Z     m    _   = rewrite minusZeroRight m in
+                               plusZeroRightNeutral m
+plusMinusLte (S _)  Z    lte = absurd lte
+plusMinusLte (S n) (S m) lte = rewrite sym $ plusSuccRightSucc (minus m n) n in
+                               cong S $ plusMinusLte n m (fromLteSucc lte)
+
 export
 minusMinusMinusPlus : (left, centre, right : Nat) ->
   minus (minus left centre) right = minus left (centre + right)

libs/base/Data/So.idr

@@ -1,5 +1,9 @@
 module Data.So
 
+import Data.Bool
+
+%default total
+
 ||| Ensure that some run-time Boolean test has been performed.
 |||
 ||| This lifts a Boolean predicate to the type level. See the function `choose`
@@ -14,7 +18,7 @@ data So : Bool -> Type where
   Oh : So True
 
 export
-implementation Uninhabited (So False) where
+Uninhabited (So False) where
   uninhabited Oh impossible
 
 ||| Perform a case analysis on a Boolean, providing clients with a `So` proof
@@ -23,3 +27,45 @@ choose : (b : Bool) -> Either (So b) (So (not b))
 choose True  = Left Oh
 choose False = Right Oh
 
+export
+eqToSo : b = True -> So b
+eqToSo Refl = Oh
+
+export
+soToEq : So b -> b = True
+soToEq Oh = Refl
+
+||| If `b` is True, `not b` can't be True
+export
+soToNotSoNot : So b -> Not (So (not b))
+soToNotSoNot Oh = uninhabited
+
+||| If `not b` is True, `b` can't be True
+export
+soNotToNotSo : So (not b) -> Not (So b)
+soNotToNotSo = flip soToNotSoNot
+
+export
+soAnd : {a : Bool} -> So (a && b) -> (So a, So b)
+soAnd soab with (choose a)
+  soAnd {a=True}  soab | Left Oh = (Oh, soab)
+  soAnd {a=True}  soab | Right prf = absurd prf
+  soAnd {a=False} soab | Right prf = absurd soab
+
+export
+andSo : (So a, So b) -> So (a && b)
+andSo (Oh, Oh) = Oh
+
+export
+soOr : {a : Bool} -> So (a || b) -> Either (So a) (So b)
+soOr soab with (choose a)
+  soOr {a=True}  _    | Left Oh = Left Oh
+  soOr {a=False} _    | Left Oh impossible
+  soOr {a=False} soab | Right Oh = Right soab
+  soOr {a=True}  _    | Right Oh impossible
+
+export
+orSo : Either (So a) (So b) -> So (a || b)
+orSo (Left Oh)  = Oh
+orSo (Right Oh) = rewrite orTrueTrue a in
+                  Oh

libs/base/base.ipkg

@@ -9,6 +9,8 @@ modules = Control.App,
           Control.Monad.Trans,
           Control.WellFounded,
 
+          Data.Bool,
+          Data.Bool.Xor,
           Data.Buffer,
           Data.Either,
           Data.Fin,

libs/contrib/Data/Bool/Extra.idr

@@ -1,36 +0,0 @@
-module Data.Bool.Extra
-
-public export
-andSameNeutral : (x : Bool) -> x && x = x
-andSameNeutral False = Refl
-andSameNeutral True = Refl
-
-public export
-andFalseFalse : (x : Bool) -> x && False = False
-andFalseFalse False = Refl
-andFalseFalse True = Refl
-
-public export
-andTrueNeutral : (x : Bool) -> x && True = x
-andTrueNeutral False = Refl
-andTrueNeutral True = Refl
-
-public export
-orSameNeutral : (x : Bool) -> x || x = x
-orSameNeutral False = Refl
-orSameNeutral True = Refl
-
-public export
-orFalseNeutral : (x : Bool) -> x || False = x
-orFalseNeutral False = Refl
-orFalseNeutral True = Refl
-
-public export
-orTrueTrue : (x : Bool) -> x || True = True
-orTrueTrue False = Refl
-orTrueTrue True = Refl
-
-public export
-orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
-orSameAndRightNeutral False _ = Refl
-orSameAndRightNeutral True _ = Refl

libs/contrib/Data/Fin/Extra.idr

@@ -5,7 +5,6 @@ import Data.Nat
 
 %default total
 
-
 ||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
 export
 elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m

libs/contrib/Data/SortedMap.idr

@@ -215,6 +215,10 @@ insert k v (M _ t) =
     Left t' => (M _ t')
     Right t' => (M _ t')
 
+export
+singleton : Ord k => k -> v -> SortedMap k v
+singleton k v = insert k v empty
+
 export
 insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
 insertFrom = flip $ foldl $ flip $ uncurry insert

libs/contrib/Text/Lexer.idr

@@ -1,6 +1,6 @@
 module Text.Lexer
 
-import Data.Bool.Extra
+import Data.Bool
 import Data.List
 import Data.Nat
 

libs/contrib/Text/Lexer/Core.idr

@@ -1,7 +1,7 @@
 module Text.Lexer.Core
 
 import public Control.Delayed
-import Data.Bool.Extra
+import Data.Bool
 import Data.List
 import Data.Nat
 import Data.Strings
@@ -76,10 +76,10 @@ reject = Lookahead False
 ||| of a list. The resulting recogniser will consume input if the produced
 ||| recognisers consume and the list is non-empty.
 export
-concatMap : (a -> Recognise c) -> (xs : List a) -> 
+concatMap : (a -> Recognise c) -> (xs : List a) ->
             Recognise (c && (isCons xs))
 concatMap {c} _ [] = rewrite andFalseFalse c in Empty
-concatMap {c} f (x :: xs) 
+concatMap {c} f (x :: xs)
    = rewrite andTrueNeutral c in
      rewrite sym (orSameAndRightNeutral c (isCons xs)) in
              SeqEmpty (f x) (Core.concatMap f xs)
@@ -111,7 +111,7 @@ isJust (Just x) = True
 
 export
 unpack' : String -> List Char
-unpack' str 
+unpack' str
     = case strUncons str of
            Nothing => []
            Just (x, xs) => x :: unpack' xs
@@ -182,12 +182,12 @@ tokenise pred line col acc tmap str
                 (incol, []) => c + cast (length incol)
                 (incol, _) => cast (length incol)
 
-    getFirstToken : TokenMap a -> List Char -> 
+    getFirstToken : TokenMap a -> List Char ->
                     Maybe (TokenData a, Int, Int, List Char)
     getFirstToken [] str = Nothing
     getFirstToken ((lex, fn) :: ts) str
         = case scan lex [] str of
-               Just (tok, rest) => Just (MkToken line col (fn (pack (reverse tok))), 
+               Just (tok, rest) => Just (MkToken line col (fn (pack (reverse tok))),
                                          line + cast (countNLs tok),
                                          getCols tok col, rest)
                Nothing => getFirstToken ts str

libs/contrib/Text/Parser.idr

@@ -1,6 +1,6 @@
 module Text.Parser
 
-import Data.Bool.Extra
+import Data.Bool
 import Data.List
 import Data.Nat
 

libs/contrib/contrib.ipkg

@@ -8,7 +8,6 @@ modules = Control.Delayed,
           Data.List.Views.Extra,
           Data.List.Palindrome,
 
-          Data.Bool.Extra,
           Data.Fin.Extra,
           Data.Nat.Equational,
           Data.Nat.Factor,

tests/idris2/coverage010/expected

@@ -1,3 +1,3 @@
 1/1: Building casetot (casetot.idr)
 casetot.idr:12:1--13:1:main is not covering:
-	Calls non covering function Main.case block in 2071(287)
+	Calls non covering function Main.case block in 2097(578)

tests/idris2/reflection003/expected

@@ -12,4 +12,4 @@ Error during reflection: Still not trying
 refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
 Error during reflection: Undefined name
 refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
-Error during reflection: failed after generating Main.{plus:6078}
+Error during reflection: failed after generating Main.{plus:6151}