packages feed

liquid-base (empty) → 4.14.0.0

raw patch · 245 files changed

+1474/−0 lines, 245 filesdep +basedep +liquid-ghc-primdep +liquidhaskellbuild-type:Customsetup-changed

Dependencies added: base, liquid-ghc-prim, liquidhaskell

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2013-2014, Ranjit Jhala++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Ranjit Jhala nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main where++import Language.Haskell.Liquid.Cabal (liquidHaskellMain)++main :: IO ()+main = liquidHaskellMain
+ liquid-base.cabal view
@@ -0,0 +1,254 @@+cabal-version:      1.24+name:               liquid-base+version:            4.14.0.0+synopsis:           Drop-in base replacement for LiquidHaskell+description:        Drop-in base replacement for LiquidHaskell.+license:            BSD3+license-file:       LICENSE+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.+author:             Ranjit Jhala, Niki Vazou, Eric Seidel+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>+category:           Language+homepage:           https://github.com/ucsd-progsys/liquidhaskell+build-type:         Custom++data-files:         src/Data/*.spec+                    src/System/*.spec+                    src/GHC/IO/Handle.spec+                    src/GHC/*.spec+                    src/Prelude.spec+                    src/Liquid/Prelude/*.spec+                    src/Foreign/C/*.spec+                    src/Foreign/*.spec+                    src/Control/*.spec++custom-setup+  setup-depends: Cabal, base, liquidhaskell++library+  exposed-modules:  Control.Applicative+                    Control.Arrow+                    Control.Category+                    Control.Concurrent+                    Control.Concurrent.Chan+                    Control.Concurrent.MVar+                    Control.Concurrent.QSem+                    Control.Concurrent.QSemN+                    Control.Exception+                    Control.Exception.Base+                    Control.Monad+                    Control.Monad.Fail+                    Control.Monad.Fix+                    Control.Monad.Instances+                    Control.Monad.IO.Class+                    Control.Monad.ST+                    Control.Monad.ST.Lazy+                    Control.Monad.ST.Lazy.Safe+                    Control.Monad.ST.Lazy.Unsafe+                    Control.Monad.ST.Safe+                    Control.Monad.ST.Strict+                    Control.Monad.ST.Unsafe+                    Control.Monad.Zip+                    Data.Bifoldable+                    Data.Bifunctor+                    Data.Bitraversable+                    Data.Bits+                    Data.Bool+                    Data.Char+                    Data.Coerce+                    Data.Complex+                    Data.Data+                    Data.Dynamic+                    Data.Either+                    Data.Eq+                    Data.Fixed+                    Data.Foldable+                    Data.Function+                    Data.Functor+                    Data.Functor.Classes+                    Data.Functor.Contravariant+                    Data.Functor.Compose+                    Data.Functor.Const+                    Data.Functor.Identity+                    Data.Functor.Product+                    Data.Functor.Sum+                    Data.IORef+                    Data.Int+                    Data.Ix+                    Data.Kind+                    Data.List+                    Data.List.NonEmpty+                    Data.Maybe+                    Data.Monoid+                    Data.Ord+                    Data.Proxy+                    Data.Ratio+                    Data.Semigroup+                    Data.STRef+                    Data.STRef.Lazy+                    Data.STRef.Strict+                    Data.String+                    Data.Traversable+                    Data.Tuple+                    Data.Type.Bool+                    Data.Type.Coercion+                    Data.Type.Equality+                    Data.Typeable+                    Data.Unique+                    Data.Version+                    Data.Void+                    Data.Word+                    Debug.Trace+                    Foreign+                    Foreign.C+                    Foreign.C.Error+                    Foreign.C.String+                    Foreign.C.Types+                    Foreign.Concurrent+                    Foreign.ForeignPtr+                    Foreign.ForeignPtr.Safe+                    Foreign.ForeignPtr.Unsafe+                    Foreign.Marshal+                    Foreign.Marshal.Alloc+                    Foreign.Marshal.Array+                    Foreign.Marshal.Error+                    Foreign.Marshal.Pool+                    Foreign.Marshal.Safe+                    Foreign.Marshal.Unsafe+                    Foreign.Marshal.Utils+                    Foreign.Ptr+                    Foreign.Safe+                    Foreign.StablePtr+                    Foreign.Storable+                    GHC.Arr+                    GHC.Base+                    GHC.ByteOrder+                    GHC.Char+                    GHC.Clock+                    GHC.Conc+                    GHC.Conc.IO+                    GHC.Conc.Signal+                    GHC.Conc.Sync+                    GHC.ConsoleHandler+                    GHC.Constants+                    GHC.Desugar+                    GHC.Enum+                    GHC.Environment+                    GHC.Err+                    GHC.Exception+                    GHC.Exception.Type+                    GHC.ExecutionStack+                    GHC.ExecutionStack.Internal+                    GHC.Exts+                    GHC.Fingerprint+                    GHC.Fingerprint.Type+                    GHC.Float+                    GHC.Float.ConversionUtils+                    GHC.Float.RealFracMethods+                    GHC.Foreign+                    GHC.ForeignPtr+                    GHC.GHCi+                    GHC.GHCi.Helpers+                    GHC.Generics+                    GHC.IO+                    GHC.IO.Buffer+                    GHC.IO.BufferedIO+                    GHC.IO.Device+                    GHC.IO.Encoding+                    GHC.IO.Encoding.CodePage+                    GHC.IO.Encoding.Failure+                    GHC.IO.Encoding.Iconv+                    GHC.IO.Encoding.Latin1+                    GHC.IO.Encoding.Types+                    GHC.IO.Encoding.UTF16+                    GHC.IO.Encoding.UTF32+                    GHC.IO.Encoding.UTF8+                    GHC.IO.Exception+                    GHC.IO.FD+                    GHC.IO.Handle+                    GHC.IO.Handle.FD+                    GHC.IO.Handle.Internals+                    GHC.IO.Handle.Lock+                    GHC.IO.Handle.Text+                    GHC.IO.Handle.Types+                    GHC.IO.IOMode+                    GHC.IO.Unsafe+                    GHC.IOArray+                    GHC.IORef+                    GHC.Int+                    GHC.Ix+                    GHC.List+                    GHC.Maybe+                    GHC.MVar+                    GHC.Natural+                    GHC.Num+                    GHC.OldList+                    GHC.OverloadedLabels+                    GHC.Pack+                    GHC.Profiling+                    GHC.Ptr+                    GHC.Read+                    GHC.Real+                    GHC.Records+                    GHC.ResponseFile+                    GHC.RTS.Flags+                    GHC.ST+                    GHC.StaticPtr+                    GHC.STRef+                    GHC.Show+                    GHC.Stable+                    GHC.StableName+                    GHC.Stack+                    GHC.Stack.CCS+                    GHC.Stack.Types+                    GHC.Stats+                    GHC.Storable+                    GHC.TopHandler+                    GHC.TypeLits+                    GHC.TypeNats+                    GHC.Unicode+                    GHC.Weak+                    GHC.Word+                    Numeric+                    Numeric.Natural+                    Prelude+                    System.CPUTime+                    System.Console.GetOpt+                    System.Environment+                    System.Environment.Blank+                    System.Exit+                    System.IO+                    System.IO.Error+                    System.IO.Unsafe+                    System.Info+                    System.Mem+                    System.Mem.StableName+                    System.Mem.Weak+                    System.Posix.Internals+                    System.Posix.Types+                    System.Timeout+                    Text.ParserCombinators.ReadP+                    Text.ParserCombinators.ReadPrec+                    Text.Printf+                    Text.Read+                    Text.Read.Lex+                    Text.Show+                    Text.Show.Functions+                    Type.Reflection+                    Type.Reflection.Unsafe+                    Unsafe.Coerce++                    -- Liquid special modules+                    Liquid.Prelude.Real+                    Liquid.Prelude.NotReal+                    Liquid.Prelude.Totality++  hs-source-dirs:     src+  build-depends:      base                 == 4.14.0.0+                    , liquid-ghc-prim+                    , liquidhaskell        >= 0.8.10.1+  default-language:   Haskell2010+  default-extensions: PackageImports+                      NoImplicitPrelude+  if impl(ghc >= 8.10)+    ghc-options: -fplugin=LiquidHaskell
+ src/Control/Applicative.hs view
@@ -0,0 +1,4 @@+module Control.Applicative ( module Exports ) where++import GHC.Base+import "base" Control.Applicative as Exports
+ src/Control/Arrow.hs view
@@ -0,0 +1,3 @@+module Control.Arrow (module Exports) where++import "base" Control.Arrow as Exports
+ src/Control/Category.hs view
@@ -0,0 +1,3 @@+module Control.Category (module Exports) where++import "base" Control.Category as Exports
+ src/Control/Concurrent.hs view
@@ -0,0 +1,3 @@+module Control.Concurrent (module Exports) where++import "base" Control.Concurrent as Exports
+ src/Control/Concurrent/Chan.hs view
@@ -0,0 +1,3 @@+module Control.Concurrent.Chan (module Exports) where++import "base" Control.Concurrent.Chan as Exports
+ src/Control/Concurrent/MVar.hs view
@@ -0,0 +1,3 @@+module Control.Concurrent.MVar (module Exports) where++import "base" Control.Concurrent.MVar as Exports
+ src/Control/Concurrent/QSem.hs view
@@ -0,0 +1,3 @@+module Control.Concurrent.QSem (module Exports) where++import "base" Control.Concurrent.QSem as Exports
+ src/Control/Concurrent/QSemN.hs view
@@ -0,0 +1,3 @@+module Control.Concurrent.QSemN (module Exports) where++import "base" Control.Concurrent.QSemN as Exports
+ src/Control/Exception.hs view
@@ -0,0 +1,6 @@+module Control.Exception ( module Exports ) where++import GHC.Base+import Control.Exception.Base++import "base" Control.Exception as Exports
+ src/Control/Exception.spec view
@@ -0,0 +1,5 @@+module spec Control.Exception where++// Useless as compiled into GHC primitive, which is ignored+assume assert :: {v:Bool | v } -> a -> a+
+ src/Control/Exception/Base.hs view
@@ -0,0 +1,4 @@+module Control.Exception.Base (module Exports) where++import GHC.Base+import "base" Control.Exception.Base as Exports
+ src/Control/Monad.hs view
@@ -0,0 +1,4 @@+module Control.Monad ( module Exports ) where++import GHC.Base+import "base" Control.Monad as Exports
+ src/Control/Monad/Fail.hs view
@@ -0,0 +1,3 @@+module Control.Monad.Fail (module Exports) where++import "base" Control.Monad.Fail as Exports
+ src/Control/Monad/Fix.hs view
@@ -0,0 +1,3 @@+module Control.Monad.Fix (module Exports) where++import "base" Control.Monad.Fix as Exports
+ src/Control/Monad/IO/Class.hs view
@@ -0,0 +1,3 @@+module Control.Monad.IO.Class (module Exports) where++import "base" Control.Monad.IO.Class as Exports
+ src/Control/Monad/Instances.hs view
@@ -0,0 +1,3 @@+module Control.Monad.Instances (module Exports) where++import "base" Control.Monad.Instances as Exports
+ src/Control/Monad/ST.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST (module Exports) where++import "base" Control.Monad.ST as Exports
+ src/Control/Monad/ST/Lazy.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST.Lazy (module Exports) where++import "base" Control.Monad.ST.Lazy as Exports
+ src/Control/Monad/ST/Lazy/Safe.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST.Lazy.Safe (module Exports) where++import "base" Control.Monad.ST.Lazy.Safe as Exports
+ src/Control/Monad/ST/Lazy/Unsafe.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST.Lazy.Unsafe (module Exports) where++import "base" Control.Monad.ST.Lazy.Unsafe as Exports
+ src/Control/Monad/ST/Safe.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST.Safe (module Exports) where++import "base" Control.Monad.ST.Safe as Exports
+ src/Control/Monad/ST/Strict.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST.Strict (module Exports) where++import "base" Control.Monad.ST.Strict as Exports
+ src/Control/Monad/ST/Unsafe.hs view
@@ -0,0 +1,3 @@+module Control.Monad.ST.Unsafe (module Exports) where++import "base" Control.Monad.ST.Unsafe as Exports
+ src/Control/Monad/Zip.hs view
@@ -0,0 +1,3 @@+module Control.Monad.Zip (module Exports) where++import "base" Control.Monad.Zip as Exports
+ src/Data/Bifoldable.hs view
@@ -0,0 +1,3 @@+module Data.Bifoldable (module Exports) where++import "base" Data.Bifoldable as Exports
+ src/Data/Bifunctor.hs view
@@ -0,0 +1,3 @@+module Data.Bifunctor (module Exports) where++import "base" Data.Bifunctor as Exports
+ src/Data/Bitraversable.hs view
@@ -0,0 +1,3 @@+module Data.Bitraversable (module Exports) where++import "base" Data.Bitraversable as Exports
+ src/Data/Bits.hs view
@@ -0,0 +1,3 @@+module Data.Bits ( module Exports ) where++import "base" Data.Bits as Exports
+ src/Data/Bits.spec view
@@ -0,0 +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)) }+
+ src/Data/Bool.hs view
@@ -0,0 +1,3 @@+module Data.Bool (module Exports) where++import "base" Data.Bool as Exports
+ src/Data/Char.hs view
@@ -0,0 +1,4 @@+module Data.Char ( module Exports ) where++import GHC.Base+import "base" Data.Char as Exports
+ src/Data/Coerce.hs view
@@ -0,0 +1,3 @@+module Data.Coerce (module Exports) where++import "base" Data.Coerce as Exports
+ src/Data/Complex.hs view
@@ -0,0 +1,3 @@+module Data.Complex (module Exports) where++import "base" Data.Complex as Exports
+ src/Data/Data.hs view
@@ -0,0 +1,3 @@+module Data.Data (module Exports) where++import "base" Data.Data as Exports
+ src/Data/Dynamic.hs view
@@ -0,0 +1,3 @@+module Data.Dynamic (module Exports) where++import "base" Data.Dynamic as Exports
+ src/Data/Either.hs view
@@ -0,0 +1,5 @@+module Data.Either ( module Exports ) where++import GHC.Base++import "base" Data.Either as Exports
+ src/Data/Either.spec view
@@ -0,0 +1,5 @@+module spec Data.Either where++measure isLeft :: Data.Either.Either a b -> Bool+  isLeft (Left x)  = true+  isLeft (Right x) = false
+ src/Data/Eq.hs view
@@ -0,0 +1,3 @@+module Data.Eq (module Exports) where++import "base" Data.Eq as Exports
+ src/Data/Fixed.hs view
@@ -0,0 +1,3 @@+module Data.Fixed (module Exports) where++import "base" Data.Fixed as Exports
+ src/Data/Foldable.hs view
@@ -0,0 +1,4 @@+module Data.Foldable (module Exports) where++import GHC.Types+import "base" Data.Foldable as Exports
+ src/Data/Foldable.spec view
@@ -0,0 +1,5 @@+module spec Data.Foldable where++import GHC.Base++length :: Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs}
+ src/Data/Function.hs view
@@ -0,0 +1,3 @@+module Data.Function ( module Exports) where++import "base" Data.Function as Exports
+ src/Data/Functor.hs view
@@ -0,0 +1,3 @@+module Data.Functor ( module Exports ) where++import "base" Data.Functor as Exports
+ src/Data/Functor/Classes.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Classes (module Exports) where++import "base" Data.Functor.Classes as Exports
+ src/Data/Functor/Compose.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Compose (module Exports) where++import "base" Data.Functor.Compose as Exports
+ src/Data/Functor/Const.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Const (module Exports) where++import "base" Data.Functor.Const as Exports
+ src/Data/Functor/Contravariant.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Contravariant (module Exports) where++import "base" Data.Functor.Contravariant as Exports
+ src/Data/Functor/Identity.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Identity (module Exports) where++import "base" Data.Functor.Identity as Exports
+ src/Data/Functor/Product.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Product (module Exports) where++import "base" Data.Functor.Product as Exports
+ src/Data/Functor/Sum.hs view
@@ -0,0 +1,3 @@+module Data.Functor.Sum (module Exports) where++import "base" Data.Functor.Sum as Exports
+ src/Data/IORef.hs view
@@ -0,0 +1,5 @@+module Data.IORef (module Exports ) where++import GHC.Base+import "base" Data.IORef as Exports+
+ src/Data/Int.hs view
@@ -0,0 +1,4 @@+module Data.Int ( module Exports ) where++import GHC.Int+import "base" Data.Int as Exports
+ src/Data/Int.spec view
@@ -0,0 +1,8 @@+module spec Data.Int where++embed Data.Int.Int8  as int+embed Data.Int.Int16 as int+embed Data.Int.Int32 as int+embed Data.Int.Int64 as int++// type Nat64 = {v:Data.Int.Int64 | v >= 0}
+ src/Data/Ix.hs view
@@ -0,0 +1,3 @@+module Data.Ix (module Exports) where++import "base" Data.Ix as Exports
+ src/Data/Kind.hs view
@@ -0,0 +1,3 @@+module Data.Kind (module Exports) where++import "base" Data.Kind as Exports
+ src/Data/List.hs view
@@ -0,0 +1,4 @@+module Data.List ( module Exports) where++import Data.Char+import "base" Data.List as Exports
+ src/Data/List/NonEmpty.hs view
@@ -0,0 +1,4 @@+module Data.List.NonEmpty ( module Exports ) where++import Data.List+import "base" Data.List.NonEmpty as Exports
+ src/Data/Maybe.hs view
@@ -0,0 +1,4 @@+module Data.Maybe ( module Exports ) where++import GHC.Base+import "base" Data.Maybe as Exports
+ src/Data/Monoid.hs view
@@ -0,0 +1,3 @@+module Data.Monoid (module Exports) where++import "base" Data.Monoid as Exports
+ src/Data/Ord.hs view
@@ -0,0 +1,3 @@+module Data.Ord ( module Exports) where++import "base" Data.Ord as Exports
+ src/Data/Proxy.hs view
@@ -0,0 +1,3 @@+module Data.Proxy (module Exports) where++import "base" Data.Proxy as Exports
+ src/Data/Ratio.hs view
@@ -0,0 +1,4 @@+module Data.Ratio ( module Exports ) where++import GHC.Base+import "base" Data.Ratio as Exports
+ src/Data/STRef.hs view
@@ -0,0 +1,3 @@+module Data.STRef (module Exports) where++import "base" Data.STRef as Exports
+ src/Data/STRef/Lazy.hs view
@@ -0,0 +1,3 @@+module Data.STRef.Lazy (module Exports) where++import "base" Data.STRef.Lazy as Exports
+ src/Data/STRef/Strict.hs view
@@ -0,0 +1,3 @@+module Data.STRef.Strict (module Exports) where++import "base" Data.STRef.Strict as Exports
+ src/Data/Semigroup.hs view
@@ -0,0 +1,3 @@+module Data.Semigroup (module Exports) where++import "base" Data.Semigroup as Exports
+ src/Data/String.hs view
@@ -0,0 +1,5 @@+module Data.String ( module Exports ) where++import GHC.Base+import "base" Data.String as Exports+
+ src/Data/String.spec view
@@ -0,0 +1,8 @@+module spec Data.String where++measure stringlen :: a -> GHC.Types.Int++Data.String.fromString+    ::  forall a. Data.String.IsString a+    =>  i : [GHC.Types.Char]+    ->  { o : a | i ~~ o && len i == stringlen o }
+ src/Data/Traversable.hs view
@@ -0,0 +1,3 @@+module Data.Traversable (module Exports) where++import "base" Data.Traversable as Exports
+ src/Data/Tuple.hs view
@@ -0,0 +1,5 @@+module Data.Tuple (module Exports) where++import GHC.Base++import "base" Data.Tuple as Exports
+ src/Data/Tuple.spec view
@@ -0,0 +1,4 @@+module spec Data.Tuple where++fst :: {f:(x:(a,b) -> {v:a | v = (fst x)}) | f == fst }+snd :: {f:(x:(a,b) -> {v:b | v = (snd x)}) | f == snd }
+ src/Data/Type/Bool.hs view
@@ -0,0 +1,3 @@+module Data.Type.Bool (module Exports) where++import "base" Data.Type.Bool as Exports
+ src/Data/Type/Coercion.hs view
@@ -0,0 +1,3 @@+module Data.Type.Coercion (module Exports) where++import "base" Data.Type.Coercion as Exports
+ src/Data/Type/Equality.hs view
@@ -0,0 +1,3 @@+module Data.Type.Equality (module Exports) where++import "base" Data.Type.Equality as Exports
+ src/Data/Typeable.hs view
@@ -0,0 +1,3 @@+module Data.Typeable (module Exports) where++import "base" Data.Typeable as Exports
+ src/Data/Unique.hs view
@@ -0,0 +1,3 @@+module Data.Unique (module Exports) where++import "base" Data.Unique as Exports
+ src/Data/Version.hs view
@@ -0,0 +1,3 @@+module Data.Version (module Exports) where++import "base" Data.Version as Exports
+ src/Data/Void.hs view
@@ -0,0 +1,3 @@+module Data.Void (module Exports) where++import "base" Data.Void as Exports
+ src/Data/Word.hs view
@@ -0,0 +1,3 @@+module Data.Word ( module Exports) where++import "base" Data.Word as Exports
+ src/Data/Word.spec view
@@ -0,0 +1,10 @@+module spec Data.Word where++embed Data.Word.Word   as int+embed Data.Word.Word8  as int+embed Data.Word.Word16 as int+embed Data.Word.Word32 as int+embed Data.Word.Word64 as int++invariant {v : Data.Word.Word32 | 0 <= v }+invariant {v : Data.Word.Word16 | 0 <= v }
+ src/Debug/Trace.hs view
@@ -0,0 +1,3 @@+module Debug.Trace (module Exports) where++import "base" Debug.Trace as Exports
+ src/Foreign.hs view
@@ -0,0 +1,12 @@+module Foreign ( module Exports ) where++import Data.Bits+import Data.Int+import Data.Word+import Foreign.Ptr+import Foreign.ForeignPtr+import Foreign.StablePtr+import Foreign.Storable+import Foreign.Marshal++import "base" Foreign as Exports
+ src/Foreign/C.hs view
@@ -0,0 +1,3 @@+module Foreign.C (module Exports) where++import "base" Foreign.C as Exports
+ src/Foreign/C/Error.hs view
@@ -0,0 +1,3 @@+module Foreign.C.Error (module Exports) where++import "base" Foreign.C.Error as Exports
+ src/Foreign/C/String.hs view
@@ -0,0 +1,4 @@+module Foreign.C.String (module Exports) where++import Foreign.Ptr+import "base" Foreign.C.String as Exports
+ src/Foreign/C/String.spec view
@@ -0,0 +1,12 @@+module spec Foreign.C.String where++import Foreign.Ptr++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 :: ((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
+ src/Foreign/C/Types.hs view
@@ -0,0 +1,5 @@+module Foreign.C.Types (module Exports) where++import GHC.Base+import GHC.Word+import "base" Foreign.C.Types as Exports
+ src/Foreign/C/Types.spec view
@@ -0,0 +1,7 @@+module spec Foreign.C.Types where++import GHC.Word++embed Foreign.C.Types.CInt   as int+embed Foreign.C.Types.CSize  as int+embed Foreign.C.Types.CULong as int
+ src/Foreign/Concurrent.hs view
@@ -0,0 +1,7 @@+module Foreign.Concurrent (module Exports) where++import GHC.IO+import GHC.Ptr+import GHC.ForeignPtr++import "base" Foreign.Concurrent as Exports
+ src/Foreign/Concurrent.spec view
@@ -0,0 +1,3 @@+module spec Foreign.Concurrent where++Foreign.Concurrent.newForeignPtr  :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types.IO (ForeignPtrN a (plen p)))
+ src/Foreign/ForeignPtr.hs view
@@ -0,0 +1,7 @@+module Foreign.ForeignPtr (module Exports) where++import GHC.Ptr+import GHC.ForeignPtr+import Foreign.Concurrent+import Foreign.Ptr+import "base" Foreign.ForeignPtr as Exports
+ src/Foreign/ForeignPtr.spec view
@@ -0,0 +1,16 @@+module spec Foreign.ForeignPtr where++import GHC.ForeignPtr+import Foreign.Ptr++Foreign.ForeignPtr.withForeignPtr :: forall a b. fp:(GHC.ForeignPtr.ForeignPtr a) +  -> ((PtrN a (fplen fp)) -> GHC.Types.IO b) +  -> (GHC.Types.IO b)++GHC.ForeignPtr.newForeignPtr_     :: p:(GHC.Ptr.Ptr a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))+Foreign.Concurrent.newForeignPtr  :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types.IO (ForeignPtrN a (plen p)))+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)
+ src/Foreign/ForeignPtr/Safe.hs view
@@ -0,0 +1,3 @@+module Foreign.ForeignPtr.Safe (module Exports) where++import "base" Foreign.ForeignPtr.Safe as Exports
+ src/Foreign/ForeignPtr/Unsafe.hs view
@@ -0,0 +1,3 @@+module Foreign.ForeignPtr.Unsafe (module Exports) where++import "base" Foreign.ForeignPtr.Unsafe as Exports
+ src/Foreign/Marshal.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal (module Exports) where++import "base" Foreign.Marshal as Exports
+ src/Foreign/Marshal/Alloc.hs view
@@ -0,0 +1,7 @@+module Foreign.Marshal.Alloc (module Exports) where++import GHC.Types+import GHC.Ptr++import "base" Foreign.Marshal.Alloc as Exports+
+ src/Foreign/Marshal/Array.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal.Array (module Exports) where++import "base" Foreign.Marshal.Array as Exports
+ src/Foreign/Marshal/Error.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal.Error (module Exports) where++import "base" Foreign.Marshal.Error as Exports
+ src/Foreign/Marshal/Pool.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal.Pool (module Exports) where++import "base" Foreign.Marshal.Pool as Exports
+ src/Foreign/Marshal/Safe.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal.Safe (module Exports) where++import "base" Foreign.Marshal.Safe as Exports
+ src/Foreign/Marshal/Unsafe.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal.Unsafe (module Exports) where++import "base" Foreign.Marshal.Unsafe as Exports
+ src/Foreign/Marshal/Utils.hs view
@@ -0,0 +1,3 @@+module Foreign.Marshal.Utils (module Exports) where++import "base" Foreign.Marshal.Utils as Exports
+ src/Foreign/Ptr.hs view
@@ -0,0 +1,4 @@+module Foreign.Ptr (module Exports) where++import GHC.Ptr+import "base" Foreign.Ptr as Exports
+ src/Foreign/Ptr.spec view
@@ -0,0 +1,7 @@+module spec Foreign.Ptr where++import GHC.Ptr++invariant {v:Foreign.Ptr.Ptr a | 0 <= plen  v }+invariant {v:Foreign.Ptr.Ptr a | 0 <= pbase v }+
+ src/Foreign/Safe.hs view
@@ -0,0 +1,3 @@+module Foreign.Safe (module Exports) where++import "base" Foreign.Safe as Exports
+ src/Foreign/StablePtr.hs view
@@ -0,0 +1,3 @@+module Foreign.StablePtr (module Exports) where++import "base" Foreign.StablePtr as Exports
+ src/Foreign/Storable.hs view
@@ -0,0 +1,6 @@+module Foreign.Storable (module Exports) where++import GHC.Base+import GHC.Ptr+import Foreign.Ptr+import "base" Foreign.Storable as Exports
+ src/Foreign/Storable.spec view
@@ -0,0 +1,25 @@+module spec Foreign.Storable where++import Foreign.Ptr++predicate PValid P N         = ((0 <= N) && (N < (plen P)))   ++Foreign.Storable.poke        :: (Foreign.Storable.Storable a)+                             => {v: (GHC.Ptr.Ptr a) | 0 < (plen v)}+                             -> a+                             -> (GHC.Types.IO ())++Foreign.Storable.peek        :: (Foreign.Storable.Storable a)+                             => p:{v: (GHC.Ptr.Ptr a) | 0 < (plen v)}+                             -> (GHC.Types.IO {v:a | v = (deref p)})++Foreign.Storable.peekByteOff :: (Foreign.Storable.Storable a)+                             => forall b. p:(GHC.Ptr.Ptr b)+                             -> {v:GHC.Types.Int | (PValid p v)}+                             -> (GHC.Types.IO a)++Foreign.Storable.pokeByteOff :: (Foreign.Storable.Storable a)+                             => forall b. p:(GHC.Ptr.Ptr b)+                             -> {v:GHC.Types.Int | (PValid p v)}+                             -> a+                             -> GHC.Types.IO ()
+ src/GHC/Arr.hs view
@@ -0,0 +1,3 @@+module GHC.Arr (module Exports) where++import "base" GHC.Arr as Exports
+ src/GHC/Base.hs view
@@ -0,0 +1,8 @@+module GHC.Base (module Exports) where++import GHC.Types+import GHC.CString+import GHC.Classes+import GHC.Tuple++import "base" GHC.Base as Exports
+ src/GHC/Base.spec view
@@ -0,0 +1,61 @@+module spec GHC.Base where++import GHC.CString+import GHC.Classes+import GHC.Types+import GHC.Tuple++GHC.Base.. :: forall <p :: b -> c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. +                   {xcmp::a, wcmp::b<q xcmp> |- c<p wcmp> <: c<r xcmp>}+                   (ycmp:b -> c<p ycmp>)+                -> (zcmp:a -> b<q zcmp>)+                ->  xcmp:a -> c<r xcmp>++measure autolen :: forall a. a -> GHC.Types.Int++instance measure len :: forall a. [a] -> GHC.Types.Int+  len []     = 0+  len (y:ys) = 1 + len ys++measure fst :: (a, b) -> a+  fst (a, b) = a++measure snd :: (a, b) -> b+  snd (a, b) = b++qualif Fst(__v:a, __y:b): (__v = (fst __y))+qualif Snd(__v:a, __y:b): (__v = (snd __y))++measure isJust :: Maybe a -> Bool+  isJust (Just x)  = true+  isJust (Nothing) = false++measure fromJust :: Maybe a -> a+  fromJust (Just x) = x++invariant {v: [a] | len v >= 0 }+map       :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}+(++)      :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}++($)       :: (a -> b) -> a -> b+id        :: x:a -> {v:a | v = x}++qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0))+qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0))++qualif ListZ(v: [a])          : (len v =  0) +qualif ListZ(v: [a])          : (len v >= 0) +qualif ListZ(v: [a])          : (len v >  0) ++qualif CmpLen(v:[a], xs:[b])  : (len v  =  len xs ) +qualif CmpLen(v:[a], xs:[b])  : (len v  >= len xs ) +qualif CmpLen(v:[a], xs:[b])  : (len v  >  len xs ) +qualif CmpLen(v:[a], xs:[b])  : (len v  <= len xs ) +qualif CmpLen(v:[a], xs:[b])  : (len v  <  len xs ) ++qualif EqLen(v:int, xs: [a])  : (v = len xs ) +qualif LenEq(v:[a], x: int)   : (x = len v ) ++qualif LenDiff(v:[a], x:int)  : (len v  = x + 1)+qualif LenDiff(v:[a], x:int)  : (len v  = x - 1)+qualif LenAcc(v:int, xs:[a], n: int): (v = len xs  + n)
+ src/GHC/ByteOrder.hs view
@@ -0,0 +1,3 @@+module GHC.ByteOrder (module Exports) where++import "base" GHC.ByteOrder as Exports
+ src/GHC/Char.hs view
@@ -0,0 +1,3 @@+module GHC.Char (module Exports) where++import "base" GHC.Char as Exports
+ src/GHC/Clock.hs view
@@ -0,0 +1,3 @@+module GHC.Clock (module Exports) where++import "base" GHC.Clock as Exports
+ src/GHC/Conc.hs view
@@ -0,0 +1,3 @@+module GHC.Conc (module Exports) where++import "base" GHC.Conc as Exports
+ src/GHC/Conc/IO.hs view
@@ -0,0 +1,3 @@+module GHC.Conc.IO (module Exports) where++import "base" GHC.Conc.IO as Exports
+ src/GHC/Conc/Signal.hs view
@@ -0,0 +1,3 @@+module GHC.Conc.Signal (module Exports) where++import "base" GHC.Conc.Signal as Exports
+ src/GHC/Conc/Sync.hs view
@@ -0,0 +1,3 @@+module GHC.Conc.Sync (module Exports) where++import "base" GHC.Conc.Sync as Exports
+ src/GHC/ConsoleHandler.hs view
@@ -0,0 +1,3 @@+module GHC.ConsoleHandler (module Exports) where++import "base" GHC.ConsoleHandler as Exports
+ src/GHC/Constants.hs view
@@ -0,0 +1,3 @@+module GHC.Constants (module Exports) where++import "base" GHC.Constants as Exports
+ src/GHC/Desugar.hs view
@@ -0,0 +1,3 @@+module GHC.Desugar (module Exports) where++import "base" GHC.Desugar as Exports
+ src/GHC/Enum.hs view
@@ -0,0 +1,3 @@+module GHC.Enum (module Exports) where++import "base" GHC.Enum as Exports
+ src/GHC/Environment.hs view
@@ -0,0 +1,3 @@+module GHC.Environment (module Exports) where++import "base" GHC.Environment as Exports
+ src/GHC/Err.hs view
@@ -0,0 +1,3 @@+module GHC.Err (module Exports) where++import "base" GHC.Err as Exports
+ src/GHC/Exception.hs view
@@ -0,0 +1,3 @@+module GHC.Exception (module Exports) where++import "base" GHC.Exception as Exports
+ src/GHC/Exception/Type.hs view
@@ -0,0 +1,3 @@+module GHC.Exception.Type (module Exports) where++import "base" GHC.Exception.Type as Exports
+ src/GHC/ExecutionStack.hs view
@@ -0,0 +1,3 @@+module GHC.ExecutionStack (module Exports) where++import "base" GHC.ExecutionStack as Exports
+ src/GHC/ExecutionStack/Internal.hs view
@@ -0,0 +1,3 @@+module GHC.ExecutionStack.Internal (module Exports) where++import "base" GHC.ExecutionStack.Internal as Exports
+ src/GHC/Exts.hs view
@@ -0,0 +1,12 @@+module GHC.Exts ( module Exports ) where++import GHC.Base+import "base" GHC.Exts as Exports++{-@ GHC.Prim.+#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x + y} @-}+{-@ GHC.Prim.-#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x - y} @-}+{-@ GHC.Prim.==# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x = y} @-}+{-@ GHC.Prim.>=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x >= y} @-}+{-@ GHC.Prim.<=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x <= y} @-}+{-@ GHC.Prim.<#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x < y}  @-}+{-@ GHC.Prim.>#  :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x > y}  @-}
+ src/GHC/Fingerprint.hs view
@@ -0,0 +1,3 @@+module GHC.Fingerprint (module Exports) where++import "base" GHC.Fingerprint as Exports
+ src/GHC/Fingerprint/Type.hs view
@@ -0,0 +1,3 @@+module GHC.Fingerprint.Type (module Exports) where++import "base" GHC.Fingerprint.Type as Exports
+ src/GHC/Float.hs view
@@ -0,0 +1,3 @@+module GHC.Float (module Exports) where++import "base" GHC.Float as Exports
+ src/GHC/Float/ConversionUtils.hs view
@@ -0,0 +1,3 @@+module GHC.Float.ConversionUtils (module Exports) where++import "base" GHC.Float.ConversionUtils as Exports
+ src/GHC/Float/RealFracMethods.hs view
@@ -0,0 +1,3 @@+module GHC.Float.RealFracMethods (module Exports) where++import "base" GHC.Float.RealFracMethods as Exports
+ src/GHC/Foreign.hs view
@@ -0,0 +1,3 @@+module GHC.Foreign (module Exports) where++import "base" GHC.Foreign as Exports
+ src/GHC/ForeignPtr.hs view
@@ -0,0 +1,4 @@+module GHC.ForeignPtr ( module Exports ) where++import GHC.Base+import "base" GHC.ForeignPtr as Exports
+ src/GHC/ForeignPtr.spec view
@@ -0,0 +1,8 @@+module spec GHC.ForeignPtr where++measure fplen :: GHC.ForeignPtr.ForeignPtr a -> GHC.Types.Int++type ForeignPtrV a   = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v}+type ForeignPtrN a N = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v && fplen v == N }++mallocPlainForeignPtrBytes :: n:{v:GHC.Types.Int  | v >= 0 } -> (GHC.Types.IO (ForeignPtrN a n))
+ src/GHC/GHCi.hs view
@@ -0,0 +1,3 @@+module GHC.GHCi (module Exports) where++import "base" GHC.GHCi as Exports
+ src/GHC/GHCi/Helpers.hs view
@@ -0,0 +1,3 @@+module GHC.GHCi.Helpers (module Exports) where++import "base" GHC.GHCi.Helpers as Exports
+ src/GHC/Generics.hs view
@@ -0,0 +1,4 @@+module GHC.Generics ( module Exports ) where++import GHC.Base+import "base" GHC.Generics as Exports
+ src/GHC/IO.hs view
@@ -0,0 +1,4 @@+module GHC.IO ( module Exports ) where++import GHC.Base+import "base" GHC.IO as Exports
+ src/GHC/IO/Buffer.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Buffer (module Exports) where++import "base" GHC.IO.Buffer as Exports
+ src/GHC/IO/BufferedIO.hs view
@@ -0,0 +1,3 @@+module GHC.IO.BufferedIO (module Exports) where++import "base" GHC.IO.BufferedIO as Exports
+ src/GHC/IO/Device.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Device (module Exports) where++import "base" GHC.IO.Device as Exports
+ src/GHC/IO/Encoding.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding (module Exports) where++import "base" GHC.IO.Encoding as Exports
+ src/GHC/IO/Encoding/CodePage.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.CodePage (module Exports) where++import "base" GHC.IO.Encoding.CodePage as Exports
+ src/GHC/IO/Encoding/Failure.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.Failure (module Exports) where++import "base" GHC.IO.Encoding.Failure as Exports
+ src/GHC/IO/Encoding/Iconv.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.Iconv (module Exports) where++import "base" GHC.IO.Encoding.Iconv as Exports
+ src/GHC/IO/Encoding/Latin1.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.Latin1 (module Exports) where++import "base" GHC.IO.Encoding.Latin1 as Exports
+ src/GHC/IO/Encoding/Types.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.Types (module Exports) where++import "base" GHC.IO.Encoding.Types as Exports
+ src/GHC/IO/Encoding/UTF16.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.UTF16 (module Exports) where++import "base" GHC.IO.Encoding.UTF16 as Exports
+ src/GHC/IO/Encoding/UTF32.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.UTF32 (module Exports) where++import "base" GHC.IO.Encoding.UTF32 as Exports
+ src/GHC/IO/Encoding/UTF8.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Encoding.UTF8 (module Exports) where++import "base" GHC.IO.Encoding.UTF8 as Exports
+ src/GHC/IO/Exception.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Exception (module Exports) where++import "base" GHC.IO.Exception as Exports
+ src/GHC/IO/FD.hs view
@@ -0,0 +1,3 @@+module GHC.IO.FD (module Exports) where++import "base" GHC.IO.FD as Exports
+ src/GHC/IO/Handle.hs view
@@ -0,0 +1,4 @@+module GHC.IO.Handle ( module Exports ) where++import GHC.Types+import "base" GHC.IO.Handle as Exports
+ src/GHC/IO/Handle.spec view
@@ -0,0 +1,10 @@+module spec GHC.IO.Handle where++hGetBuf :: GHC.IO.Handle.Handle -> GHC.Ptr.Ptr a -> n:Nat+        -> (GHC.Types.IO {v:Nat | v <= n})++hGetBufNonBlocking :: GHC.IO.Handle.Handle -> GHC.Ptr.Ptr a -> n:Nat+                   -> (GHC.Types.IO {v:Nat | v <= n})++hFileSize :: GHC.IO.Handle.Handle+          -> (GHC.Types.IO {v:GHC.Integer.Type.Integer | v >= 0})
+ src/GHC/IO/Handle/FD.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Handle.FD (module Exports) where++import "base" GHC.IO.Handle.FD as Exports
+ src/GHC/IO/Handle/Internals.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Handle.Internals (module Exports) where++import "base" GHC.IO.Handle.Internals as Exports
+ src/GHC/IO/Handle/Lock.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Handle.Lock (module Exports) where++import "base" GHC.IO.Handle.Lock as Exports
+ src/GHC/IO/Handle/Text.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Handle.Text (module Exports) where++import "base" GHC.IO.Handle.Text as Exports
+ src/GHC/IO/Handle/Types.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Handle.Types (module Exports) where++import "base" GHC.IO.Handle.Types as Exports
+ src/GHC/IO/IOMode.hs view
@@ -0,0 +1,3 @@+module GHC.IO.IOMode (module Exports) where++import "base" GHC.IO.IOMode as Exports
+ src/GHC/IO/Unsafe.hs view
@@ -0,0 +1,3 @@+module GHC.IO.Unsafe (module Exports) where++import "base" GHC.IO.Unsafe as Exports
+ src/GHC/IOArray.hs view
@@ -0,0 +1,3 @@+module GHC.IOArray (module Exports) where++import "base" GHC.IOArray as Exports
+ src/GHC/IORef.hs view
@@ -0,0 +1,3 @@+module GHC.IORef (module Exports) where++import "base" GHC.IORef as Exports
+ src/GHC/Int.hs view
@@ -0,0 +1,4 @@+module GHC.Int (module Exports) where++import GHC.Base+import "base" GHC.Int as Exports
+ src/GHC/Int.spec view
@@ -0,0 +1,8 @@+module spec GHC.Int where++embed GHC.Int.Int8  as int+embed GHC.Int.Int16 as int+embed GHC.Int.Int32 as int+embed GHC.Int.Int64 as int++type Nat64 = {v:GHC.Int.Int64 | v >= 0}
+ src/GHC/Ix.hs view
@@ -0,0 +1,3 @@+module GHC.Ix (module Exports) where++import "base" GHC.Ix as Exports
+ src/GHC/List.hs view
@@ -0,0 +1,4 @@+module GHC.List (module Exports) where++import GHC.Base+import "base" GHC.List as Exports
+ src/GHC/List.spec view
@@ -0,0 +1,64 @@+module spec GHC.List where ++import GHC.Base++head         :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}+tail         :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}++last         :: xs:{v: [a] | len v > 0} -> a+init         :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1}+null         :: xs:[a] -> {v: GHC.Types.Bool | ((v) <=> len(xs) = 0) }+length       :: xs:[a] -> {v: GHC.Types.Int | v = len(xs)}+filter       :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}+scanl        :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) }+scanl1       :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }+foldr1       :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a+scanr        :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }+scanr1       :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }++lazy GHC.List.iterate+iterate :: (a -> a) -> a -> [a]++repeat :: a -> [a]+lazy GHC.List.repeat++replicate    :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}++cycle        :: {v: [a] | len(v) > 0 } -> [a]+lazy cycle++takeWhile    :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}+dropWhile    :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}++take :: n:GHC.Types.Int+     -> xs:[a]+     -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)}+drop :: n:GHC.Types.Int+     -> xs:[a]+     -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))}++splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}>+span    :: (a -> GHC.Types.Bool) +        -> xs:[a] +        -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))})++break :: (a -> GHC.Types.Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}>++reverse      :: xs:[a] -> {v: [a] | len(v) = len(xs)}++// 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]))++GHC.List.!!         :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a+++zip :: xs : [a] -> ys:[b] +            -> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys)))+            && (((len xs) = (len ys)) => ((len v) = (len xs))) )}++zipWith :: (a -> b -> c) +        -> xs : [a] -> ys:[b] +        -> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))}++errorEmptyList :: {v: _ | false} -> a
+ src/GHC/MVar.hs view
@@ -0,0 +1,3 @@+module GHC.MVar (module Exports) where++import "base" GHC.MVar as Exports
+ src/GHC/Maybe.hs view
@@ -0,0 +1,3 @@+module GHC.Maybe (module Exports) where++import "base" GHC.Maybe as Exports
+ src/GHC/Natural.hs view
@@ -0,0 +1,3 @@+module GHC.Natural (module Exports) where++import "base" GHC.Natural as Exports
+ src/GHC/Num.hs view
@@ -0,0 +1,4 @@+module GHC.Num (module Exports) where++import GHC.Base+import "base" GHC.Num as Exports
+ src/GHC/Num.spec view
@@ -0,0 +1,12 @@+module spec GHC.Num where++embed GHC.Integer.Type.Integer as int ++GHC.Num.fromInteger :: (GHC.Num.Num a) => x:GHC.Integer.Type.Integer -> {v:a | v = x }++GHC.Num.negate :: (GHC.Num.Num a)+               => x:a+               -> {v:a | v = -x}++GHC.Num.+ :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x + y }+GHC.Num.- :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x - y }
+ src/GHC/OldList.hs view
@@ -0,0 +1,3 @@+module GHC.OldList (module Exports) where++import "base" GHC.OldList as Exports
+ src/GHC/OverloadedLabels.hs view
@@ -0,0 +1,3 @@+module GHC.OverloadedLabels (module Exports) where++import "base" GHC.OverloadedLabels as Exports
+ src/GHC/Pack.hs view
@@ -0,0 +1,3 @@+module GHC.Pack (module Exports) where++import "base" GHC.Pack as Exports
+ src/GHC/Profiling.hs view
@@ -0,0 +1,3 @@+module GHC.Profiling (module Exports) where++import "base" GHC.Profiling as Exports
+ src/GHC/Ptr.hs view
@@ -0,0 +1,4 @@+module GHC.Ptr ( module Exports ) where++import GHC.Types+import "base" GHC.Ptr as Exports
+ src/GHC/Ptr.spec view
@@ -0,0 +1,21 @@+module spec GHC.Ptr where++measure pbase     :: GHC.Ptr.Ptr a -> GHC.Types.Int+measure plen      :: GHC.Ptr.Ptr a -> GHC.Types.Int+measure isNullPtr :: GHC.Ptr.Ptr a -> Bool ++type PtrN a N = {v: PtrV a        | plen v == N }+type PtrV a   = {v: GHC.Ptr.Ptr a | 0 <= plen v }++GHC.Ptr.castPtr :: p:(PtrV a) -> (PtrN b (plen p))++GHC.Ptr.plusPtr :: base:(PtrV a)+                -> off:{v:GHC.Types.Int | v <= plen base }+                -> {v:(PtrV b) | pbase v = pbase base && plen v = plen base - off}++GHC.Ptr.minusPtr :: q:(PtrV a)+                 -> p:{v:(PtrV b) | pbase v == pbase q && plen v >= plen q}+                 -> {v:Nat | v == plen p - plen q}++measure deref     :: GHC.Ptr.Ptr a -> a+
+ src/GHC/RTS/Flags.hs view
@@ -0,0 +1,3 @@+module GHC.RTS.Flags (module Exports) where++import "base" GHC.RTS.Flags as Exports
+ src/GHC/Read.hs view
@@ -0,0 +1,3 @@+module GHC.Read (module Exports) where++import "base" GHC.Read as Exports
+ src/GHC/Real.hs view
@@ -0,0 +1,7 @@+module GHC.Real (module Exports) where++import GHC.Types+import GHC.Num+import "base" GHC.Enum++import "base" GHC.Real as Exports
+ src/GHC/Real.spec view
@@ -0,0 +1,39 @@+module spec GHC.Real where++import GHC.Types++(GHC.Real.^) :: (GHC.Num.Num a, GHC.Real.Integral b) => a:a -> n:b -> {v:a | v == 0 <=> a == 0 }++GHC.Real.fromIntegral    :: (GHC.Real.Integral a, GHC.Num.Num b) => x:a -> {v:b|v=x}++class (GHC.Num.Num a) => GHC.Real.Fractional a where+  (GHC.Real./)   :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y}+  GHC.Real.recip :: a -> a+  GHC.Real.fromRational :: GHC.Real.Ratio Integer -> a++class (GHC.Real.Real a, GHC.Enum.Enum a) => GHC.Real.Integral a where+  GHC.Real.quot :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) &&+                                                     ((x >= 0 && y >= 0) => v >= 0) &&+                                                     ((x >= 0 && y >= 1) => v <= x) }+  GHC.Real.rem :: x:a -> y:{v:a | v /= 0} -> {v:a | ((v >= 0) && (v < y))}+  GHC.Real.mod :: x:a -> y:{v:a | v /= 0} -> {v:a | v = x mod y && ((0 <= x && 0 < y) => (0 <= v && v < y))}++  GHC.Real.div :: x:a -> y:{v:a | v /= 0} -> {v:a | (v = (x / y)) &&+                                                    ((x >= 0 && y >= 0) => v >= 0) &&+                                                    ((x >= 0 && y >= 1) => v <= x) && +                                                    ((1 < y)            => v < x ) && +                                                    ((y >= 1)           => v <= x)  +                                                    }+  GHC.Real.quotRem :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) &&+                                                          ((x >= 0 && y >= 0) => v >= 0) &&+                                                          ((x >= 0 && y >= 1) => v <= x)}+                                                 , {v:a | ((v >= 0) && (v < y))})+  GHC.Real.divMod :: x:a -> y:{v:a | v /= 0} -> ( {v:a | (v = (x / y)) &&+                                                         ((x >= 0 && y >= 0) => v >= 0) &&+                                                         ((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}++// 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/GHC/Records.hs view
@@ -0,0 +1,3 @@+module GHC.Records (module Exports) where++import "base" GHC.Records as Exports
+ src/GHC/ResponseFile.hs view
@@ -0,0 +1,3 @@+module GHC.ResponseFile (module Exports) where++import "base" GHC.ResponseFile as Exports
+ src/GHC/ST.hs view
@@ -0,0 +1,3 @@+module GHC.ST (module Exports) where++import "base" GHC.ST as Exports
+ src/GHC/STRef.hs view
@@ -0,0 +1,3 @@+module GHC.STRef (module Exports) where++import "base" GHC.STRef as Exports
+ src/GHC/Show.hs view
@@ -0,0 +1,3 @@+module GHC.Show (module Exports) where++import "base" GHC.Show as Exports
+ src/GHC/Stable.hs view
@@ -0,0 +1,3 @@+module GHC.Stable (module Exports) where++import "base" GHC.Stable as Exports
+ src/GHC/StableName.hs view
@@ -0,0 +1,3 @@+module GHC.StableName (module Exports) where++import "base" GHC.StableName as Exports
+ src/GHC/Stack.hs view
@@ -0,0 +1,3 @@+module GHC.Stack (module Exports) where++import "base" GHC.Stack as Exports
+ src/GHC/Stack/CCS.hs view
@@ -0,0 +1,3 @@+module GHC.Stack.CCS (module Exports) where++import "base" GHC.Stack.CCS as Exports
+ src/GHC/Stack/Types.hs view
@@ -0,0 +1,3 @@+module GHC.Stack.Types (module Exports) where++import "base" GHC.Stack.Types as Exports
+ src/GHC/StaticPtr.hs view
@@ -0,0 +1,3 @@+module GHC.StaticPtr (module Exports) where++import "base" GHC.StaticPtr as Exports
+ src/GHC/Stats.hs view
@@ -0,0 +1,3 @@+module GHC.Stats (module Exports) where++import "base" GHC.Stats as Exports
+ src/GHC/Storable.hs view
@@ -0,0 +1,3 @@+module GHC.Storable (module Exports) where++import "base" GHC.Storable as Exports
+ src/GHC/TopHandler.hs view
@@ -0,0 +1,3 @@+module GHC.TopHandler (module Exports) where++import "base" GHC.TopHandler as Exports
+ src/GHC/TypeLits.hs view
@@ -0,0 +1,4 @@+module GHC.TypeLits ( module Exports ) where++import GHC.Base+import "base" GHC.TypeLits as Exports
+ src/GHC/TypeNats.hs view
@@ -0,0 +1,3 @@+module GHC.TypeNats (module Exports) where++import "base" GHC.TypeNats as Exports
+ src/GHC/Unicode.hs view
@@ -0,0 +1,3 @@+module GHC.Unicode (module Exports) where++import "base" GHC.Unicode as Exports
+ src/GHC/Weak.hs view
@@ -0,0 +1,3 @@+module GHC.Weak (module Exports) where++import "base" GHC.Weak as Exports
+ src/GHC/Word.hs view
@@ -0,0 +1,4 @@+module GHC.Word (module Exports) where++import GHC.Base+import "base" GHC.Word as Exports
+ src/GHC/Word.spec view
@@ -0,0 +1,7 @@+module spec GHC.Word where++embed GHC.Word.Word   as int+embed GHC.Word.Word8  as int+embed GHC.Word.Word16 as int+embed GHC.Word.Word32 as int+embed GHC.Word.Word64 as int
+ src/Liquid/Prelude/NotReal.hs view
@@ -0,0 +1,4 @@+module Liquid.Prelude.NotReal where++import GHC.Num+import GHC.Real
+ src/Liquid/Prelude/NotReal.spec view
@@ -0,0 +1,13 @@+module spec Liquid.Prelude.NotReal where++import GHC.Num+import GHC.Real++assume GHC.Num.* :: (GHC.Num.Num a) => x:a -> y:a +                 -> {v:a | ((((((x = 0) || (y = 0)) => (v = 0))) +                         && (((x > 0) && (y > 0)) => ((v >= x) && (v >= y))))+                         && (((x > 1) && (y > 1)) => ((v > x) && (v > y))))+                    }+++GHC.Real./       :: (GHC.Real.Fractional a) => x:a -> y:{v:a | v != 0.0} -> a
+ src/Liquid/Prelude/Real.hs view
@@ -0,0 +1,3 @@+module Liquid.Prelude.Real where++import GHC.Num
+ src/Liquid/Prelude/Real.spec view
@@ -0,0 +1,5 @@+module spec Liquid.Prelude.Real where++import GHC.Num++assume GHC.Num.* :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x * y}
+ src/Liquid/Prelude/Totality.hs view
@@ -0,0 +1,3 @@+module Liquid.Prelude.Totality where++import "base" Control.Exception.Base
+ src/Liquid/Prelude/Totality.spec view
@@ -0,0 +1,6 @@+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
+ src/Numeric.hs view
@@ -0,0 +1,3 @@+module Numeric (module Exports) where++import "base" Numeric as Exports
+ src/Numeric/Natural.hs view
@@ -0,0 +1,3 @@+module Numeric.Natural (module Exports) where++import "base" Numeric.Natural as Exports
+ src/Prelude.hs view
@@ -0,0 +1,20 @@+module Prelude (module Exports) where++import Data.Foldable+import Data.Tuple+import GHC.Base+import GHC.CString+import GHC.Classes+import GHC.Exts+import GHC.Int+import GHC.List+import GHC.Num+import GHC.Real+import GHC.Types+import GHC.Word++-- Liquid \"extra\" modules+import Liquid.Prelude.Totality+import Liquid.Prelude.Real++import "base" Prelude as Exports
+ src/Prelude.spec view
@@ -0,0 +1,68 @@+module spec Prelude where++import GHC.Base+import GHC.Int+import GHC.List+import GHC.Num+import GHC.Real+import GHC.Word++import Data.Foldable+import Data.Maybe+import Data.Tuple+import GHC.Exts+import GHC.Err +++// 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) }++embed Integer           as int++predicate Max V X Y = if X > Y then V = X else V = Y+predicate Min V X Y = if X < Y then V = X else V = Y++type IncrListD a  = [a]<{\x y -> (x+D) <= y}>++//BOT: Do not delete EVER!++qualif Bot(v:@(0))    : (0 = 1)+qualif Bot(v:obj)     : (0 = 1)+qualif Bot(v:a)       : (0 = 1)+qualif Bot(v:bool)    : (0 = 1)+qualif Bot(v:int)     : (0 = 1)++qualif CmpZ(v:a)      : (v <  0)+qualif CmpZ(v:a)      : (v <= 0)+qualif CmpZ(v:a)      : (v >  0)+qualif CmpZ(v:a)      : (v >= 0)+qualif CmpZ(v:a)      : (v  = 0)+qualif CmpZ(v:a)      : (v != 0)++qualif Cmp(v:a, x:a)  : (v <  x)+qualif Cmp(v:a, x:a)  : (v <= x)+qualif Cmp(v:a, x:a)  : (v >  x)+qualif Cmp(v:a, x:a)  : (v >= x)+qualif Cmp(v:a, x:a)  : (v  = x)+qualif Cmp(v:a, x:a)  : (v != x)++qualif One(v:int)     : v = 1+qualif True1(v:GHC.Types.Bool)   : (v)+qualif False1(v:GHC.Types.Bool)  : (~ v)++// 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])+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])+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])++// REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
+ src/System/CPUTime.hs view
@@ -0,0 +1,3 @@+module System.CPUTime (module Exports) where++import "base" System.CPUTime as Exports
+ src/System/Console/GetOpt.hs view
@@ -0,0 +1,3 @@+module System.Console.GetOpt (module Exports) where++import "base" System.Console.GetOpt as Exports
+ src/System/Environment.hs view
@@ -0,0 +1,3 @@+module System.Environment (module Exports) where++import "base" System.Environment as Exports
+ src/System/Environment/Blank.hs view
@@ -0,0 +1,3 @@+module System.Environment.Blank (module Exports) where++import "base" System.Environment.Blank as Exports
+ src/System/Exit.hs view
@@ -0,0 +1,3 @@+module System.Exit (module Exports) where++import "base" System.Exit as Exports
+ src/System/IO.hs view
@@ -0,0 +1,4 @@+module System.IO ( module Exports ) where++import GHC.IO.Handle as Exports+import "base" System.IO as Exports
+ src/System/IO.spec view
@@ -0,0 +1,3 @@+module spec System.IO where++import GHC.IO.Handle
+ src/System/IO/Error.hs view
@@ -0,0 +1,3 @@+module System.IO.Error (module Exports) where++import "base" System.IO.Error as Exports
+ src/System/IO/Unsafe.hs view
@@ -0,0 +1,3 @@+module System.IO.Unsafe (module Exports) where++import "base" System.IO.Unsafe as Exports
+ src/System/Info.hs view
@@ -0,0 +1,3 @@+module System.Info (module Exports) where++import "base" System.Info as Exports
+ src/System/Mem.hs view
@@ -0,0 +1,3 @@+module System.Mem (module Exports) where++import "base" System.Mem as Exports
+ src/System/Mem/StableName.hs view
@@ -0,0 +1,3 @@+module System.Mem.StableName (module Exports) where++import "base" System.Mem.StableName as Exports
+ src/System/Mem/Weak.hs view
@@ -0,0 +1,3 @@+module System.Mem.Weak (module Exports) where++import "base" System.Mem.Weak as Exports
+ src/System/Posix/Internals.hs view
@@ -0,0 +1,3 @@+module System.Posix.Internals (module Exports) where++import "base" System.Posix.Internals as Exports
+ src/System/Posix/Types.hs view
@@ -0,0 +1,3 @@+module System.Posix.Types (module Exports) where++import "base" System.Posix.Types as Exports
+ src/System/Timeout.hs view
@@ -0,0 +1,3 @@+module System.Timeout (module Exports) where++import "base" System.Timeout as Exports
+ src/Text/ParserCombinators/ReadP.hs view
@@ -0,0 +1,3 @@+module Text.ParserCombinators.ReadP (module Exports) where++import "base" Text.ParserCombinators.ReadP as Exports
+ src/Text/ParserCombinators/ReadPrec.hs view
@@ -0,0 +1,3 @@+module Text.ParserCombinators.ReadPrec (module Exports) where++import "base" Text.ParserCombinators.ReadPrec as Exports
+ src/Text/Printf.hs view
@@ -0,0 +1,3 @@+module Text.Printf (module Exports) where++import "base" Text.Printf as Exports
+ src/Text/Read.hs view
@@ -0,0 +1,3 @@+module Text.Read (module Exports) where++import "base" Text.Read as Exports
+ src/Text/Read/Lex.hs view
@@ -0,0 +1,3 @@+module Text.Read.Lex (module Exports) where++import "base" Text.Read.Lex as Exports
+ src/Text/Show.hs view
@@ -0,0 +1,3 @@+module Text.Show (module Exports) where++import "base" Text.Show as Exports
+ src/Text/Show/Functions.hs view
@@ -0,0 +1,3 @@+module Text.Show.Functions (module Exports) where++import "base" Text.Show.Functions as Exports
+ src/Type/Reflection.hs view
@@ -0,0 +1,3 @@+module Type.Reflection (module Exports) where++import "base" Type.Reflection as Exports
+ src/Type/Reflection/Unsafe.hs view
@@ -0,0 +1,3 @@+module Type.Reflection.Unsafe (module Exports) where++import "base" Type.Reflection.Unsafe as Exports
+ src/Unsafe/Coerce.hs view
@@ -0,0 +1,3 @@+module Unsafe.Coerce (module Exports) where++import "base" Unsafe.Coerce as Exports