packages feed

liquid-base 4.14.1.0 → 4.14.3.0

raw patch · 21 files changed

+68/−39 lines, 21 filesdep +integer-gmpdep ~basedep ~liquidhaskellnew-uploader

Dependencies added: integer-gmp

Dependency ranges changed: base, liquidhaskell

Files

liquid-base.cabal view
@@ -1,8 +1,8 @@ cabal-version:      1.24 name:               liquid-base-version:            4.14.1.0-synopsis:           Drop-in base replacement for LiquidHaskell-description:        Drop-in base replacement for LiquidHaskell.+version:            4.14.3.0+synopsis:           Drop-in base replacement for LH+description:        Superseded by liquidhaskell >= 9.2 license:            BSD3 license-file:       LICENSE copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.@@ -23,7 +23,7 @@                     src/Control/*.spec  custom-setup-  setup-depends: Cabal, base, liquidhaskell+  setup-depends: Cabal<4, base<5, liquidhaskell  library   exposed-modules:  Control.Applicative@@ -244,9 +244,11 @@                     Liquid.Prelude.Totality    hs-source-dirs:     src-  build-depends:      base                 == 4.14.1.0+  build-depends:      base                 == 4.14.3.0                     , liquid-ghc-prim-                    , liquidhaskell        >= 0.8.10.1+                    , liquidhaskell        >= 0.8.10.7.1 && < 0.9+  if impl(ghc < 9)+    build-depends:    integer-gmp < 1.0.4.0   default-language:   Haskell2010   default-extensions: PackageImports                       NoImplicitPrelude
src/Control/Exception.spec view
@@ -1,5 +1,5 @@ module spec Control.Exception where -// Useless as compiled into GHC primitive, which is ignored+//  Useless as compiled into GHC primitive, which is ignored assume assert :: {v:Bool | v } -> a -> a
src/Data/Bits.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE Trustworthy #-} module Data.Bits ( module Exports ) where  import "base" Data.Bits as Exports
src/Data/Bits.spec view
@@ -1,6 +1,6 @@ module spec Data.Bits where -// TODO: cannot use this because `Bits` is not a `Num`-// Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat -//                  -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }+//  TODO: cannot use this because `Bits` is not a `Num`+//  Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat +//                   -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
src/Data/Foldable.spec view
@@ -3,3 +3,4 @@ import GHC.Base  length :: Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}+null   :: Data.Foldable.Foldable f => v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)}
src/Data/Int.spec view
@@ -5,4 +5,4 @@ embed Data.Int.Int32 as int embed Data.Int.Int64 as int -// type Nat64 = {v:Data.Int.Int64 | v >= 0}+//  type Nat64 = {v:Data.Int.Int64 | v >= 0}
+ src/Data/Maybe.spec view
@@ -0,0 +1,7 @@+module spec Data.Maybe where++maybe :: v:b -> (a -> b) -> u:(Maybe a) -> {w:b | not (isJust u) => w == v}+isJust :: v:(Maybe a) -> {b:Bool | b == isJust v}+isNothing :: v:(Maybe a) -> {b:Bool | not (isJust v) == b}+fromJust :: {v:(Maybe a) | isJust v} -> a+fromMaybe :: v:a -> u:(Maybe a) -> {x:a | not (isJust u) => x == v}
src/Data/Typeable.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE Trustworthy #-} module Data.Typeable (module Exports) where  import "base" Data.Typeable as Exports
src/Data/Word.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE Trustworthy #-} module Data.Word ( module Exports) where  import "base" Data.Word as Exports
src/Foreign/C/String.spec view
@@ -5,8 +5,8 @@ type CStringLen    = ((GHC.Ptr.Ptr Foreign.C.Types.CChar), Nat)<{\p v -> (v <= (plen p))}> type CStringLenN N = ((GHC.Ptr.Ptr Foreign.C.Types.CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}> -//measure cStringLen :: Foreign.C.String.CStringLen -> GHC.Types.Int+// measure cStringLen :: Foreign.C.String.CStringLen -> GHC.Types.Int measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int -//measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int -//cStringLen (c, n) = n+// measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int +// cStringLen (c, n) = n
src/Foreign/ForeignPtr.spec view
@@ -12,5 +12,5 @@ Foreign.ForeignPtr.newForeignPtr ::  _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))  -// this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`-// Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)+//  this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`+//  Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
src/GHC/IO/Handle.hs view
@@ -1,4 +1,5 @@ module GHC.IO.Handle ( module Exports ) where  import GHC.Types+import GHC.Integer import "base" GHC.IO.Handle as Exports
src/GHC/IO/Handle.spec view
@@ -7,4 +7,4 @@                    -> (GHC.Types.IO {v:Nat | v <= n})  hFileSize :: GHC.IO.Handle.Handle-          -> (GHC.Types.IO {v:GHC.Integer.Type.Integer | v >= 0})+          -> (GHC.Types.IO {v:Integer | v >= 0})
src/GHC/List.spec view
@@ -46,7 +46,7 @@  reverse      :: xs:[a] -> {v: [a] | len(v) = len(xs)} -// Copy-pasted from len.hquals+//  Copy-pasted from len.hquals qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys])) qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))
src/GHC/Num.spec view
@@ -1,8 +1,9 @@ module spec GHC.Num where -embed GHC.Integer.Type.Integer as int +embed GHC.Integer.Type.Integer as int+embed GHC.Num.Integer as int -GHC.Num.fromInteger :: (GHC.Num.Num a) => x:GHC.Integer.Type.Integer -> {v:a | v = x }+GHC.Num.fromInteger :: (GHC.Num.Num a) => x:Integer -> {v:a | v = x }  GHC.Num.negate :: (GHC.Num.Num a)                => x:a
src/GHC/Real.hs view
@@ -3,5 +3,4 @@ import GHC.Types import GHC.Num import "base" GHC.Enum- import "base" GHC.Real as Exports
src/GHC/Real.spec view
@@ -33,7 +33,7 @@                                                          ((x >= 0 && y >= 1) => v <= x) }                                                 , {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}                                                 )-  GHC.Real.toInteger :: x:a -> {v:GHC.Integer.Type.Integer | v = x}+  GHC.Real.toInteger :: x:a -> {v:Integer | v = x} -// fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here-// mod :: x:a -> y:a -> {v:a | v = (x mod y) }+//  fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here+//  mod :: x:a -> y:a -> {v:a | v = (x mod y) }
src/Liquid/Prelude/Totality.hs view
@@ -1,3 +1,8 @@-module Liquid.Prelude.Totality where+module Liquid.Prelude.Totality (module Exports) where -import "base" Control.Exception.Base+import GHC.Types+import "base" Control.Exception.Base as Exports+++totalityError :: a -> Bool+totalityError _ = False
src/Liquid/Prelude/Totality.spec view
@@ -1,6 +1,15 @@ module spec Liquid.Prelude.Totality where -assume Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | 5 <4 } -> a-assume Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | 5 < 4 } -> a-assume Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | 5 < 4 } -> a-assume Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | 5 < 4 } -> a++measure totalityError :: a -> Bool+++assume Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a++assume Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | totalityError "Use of partial record field selector"} -> a++assume Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | totalityError "Guards are non-exhaustive"} -> a++assume Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | totalityError "Missing method(s) on instance declaration"} -> a++assume Control.Exception.Base.recConError :: {v:GHC.Prim.Addr# | totalityError "Missing field in record construction"} -> a
src/Prelude.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE Trustworthy #-} module Prelude (module Exports) where  import Data.Foldable
src/Prelude.spec view
@@ -14,11 +14,11 @@ import GHC.Err   -// GHC.Types.D# :: x:_ -> {v:_ | v = x}+//  GHC.Types.D# :: x:_ -> {v:_ | v = x}  GHC.Err.error :: {v:_ | false} -> a  -//assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) }+// assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) }  embed Integer           as int @@ -27,7 +27,7 @@  type IncrListD a  = [a]<{\x y -> (x+D) <= y}> -//BOT: Do not delete EVER!+// BOT: Do not delete EVER!  qualif Bot(v:@(0))    : (0 = 1) qualif Bot(v:obj)     : (0 = 1)@@ -53,16 +53,16 @@ qualif True1(v:GHC.Types.Bool)   : (v) qualif False1(v:GHC.Types.Bool)  : (~ v) -// REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])+//  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool]) qualif Papp(v:a, p:Pred a) : (papp1 p v) -// REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])+//  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool]) qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x) -// REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])+//  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool]) qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y) -// qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)-// REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])+//  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)+//  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool]) -// REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])+//  REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])