diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,6 @@ +module Main where + +import Language.Haskell.Liquid.Cabal (liquidHaskellMain) + +main :: IO () +main = liquidHaskellMain diff --git a/liquid-base.cabal b/liquid-base.cabal new file mode 100644 --- /dev/null +++ b/liquid-base.cabal @@ -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 +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 diff --git a/src/Control/Applicative.hs b/src/Control/Applicative.hs new file mode 100644 --- /dev/null +++ b/src/Control/Applicative.hs @@ -0,0 +1,4 @@ +module Control.Applicative ( module Exports ) where + +import GHC.Base +import "base" Control.Applicative as Exports diff --git a/src/Control/Arrow.hs b/src/Control/Arrow.hs new file mode 100644 --- /dev/null +++ b/src/Control/Arrow.hs @@ -0,0 +1,3 @@ +module Control.Arrow (module Exports) where + +import "base" Control.Arrow as Exports diff --git a/src/Control/Category.hs b/src/Control/Category.hs new file mode 100644 --- /dev/null +++ b/src/Control/Category.hs @@ -0,0 +1,3 @@ +module Control.Category (module Exports) where + +import "base" Control.Category as Exports diff --git a/src/Control/Concurrent.hs b/src/Control/Concurrent.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent.hs @@ -0,0 +1,3 @@ +module Control.Concurrent (module Exports) where + +import "base" Control.Concurrent as Exports diff --git a/src/Control/Concurrent/Chan.hs b/src/Control/Concurrent/Chan.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/Chan.hs @@ -0,0 +1,3 @@ +module Control.Concurrent.Chan (module Exports) where + +import "base" Control.Concurrent.Chan as Exports diff --git a/src/Control/Concurrent/MVar.hs b/src/Control/Concurrent/MVar.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/MVar.hs @@ -0,0 +1,3 @@ +module Control.Concurrent.MVar (module Exports) where + +import "base" Control.Concurrent.MVar as Exports diff --git a/src/Control/Concurrent/QSem.hs b/src/Control/Concurrent/QSem.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/QSem.hs @@ -0,0 +1,3 @@ +module Control.Concurrent.QSem (module Exports) where + +import "base" Control.Concurrent.QSem as Exports diff --git a/src/Control/Concurrent/QSemN.hs b/src/Control/Concurrent/QSemN.hs new file mode 100644 --- /dev/null +++ b/src/Control/Concurrent/QSemN.hs @@ -0,0 +1,3 @@ +module Control.Concurrent.QSemN (module Exports) where + +import "base" Control.Concurrent.QSemN as Exports diff --git a/src/Control/Exception.hs b/src/Control/Exception.hs new file mode 100644 --- /dev/null +++ b/src/Control/Exception.hs @@ -0,0 +1,6 @@ +module Control.Exception ( module Exports ) where + +import GHC.Base +import Control.Exception.Base + +import "base" Control.Exception as Exports diff --git a/src/Control/Exception.spec b/src/Control/Exception.spec new file mode 100644 --- /dev/null +++ b/src/Control/Exception.spec @@ -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 + diff --git a/src/Control/Exception/Base.hs b/src/Control/Exception/Base.hs new file mode 100644 --- /dev/null +++ b/src/Control/Exception/Base.hs @@ -0,0 +1,4 @@ +module Control.Exception.Base (module Exports) where + +import GHC.Base +import "base" Control.Exception.Base as Exports diff --git a/src/Control/Monad.hs b/src/Control/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad.hs @@ -0,0 +1,4 @@ +module Control.Monad ( module Exports ) where + +import GHC.Base +import "base" Control.Monad as Exports diff --git a/src/Control/Monad/Fail.hs b/src/Control/Monad/Fail.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Fail.hs @@ -0,0 +1,3 @@ +module Control.Monad.Fail (module Exports) where + +import "base" Control.Monad.Fail as Exports diff --git a/src/Control/Monad/Fix.hs b/src/Control/Monad/Fix.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Fix.hs @@ -0,0 +1,3 @@ +module Control.Monad.Fix (module Exports) where + +import "base" Control.Monad.Fix as Exports diff --git a/src/Control/Monad/IO/Class.hs b/src/Control/Monad/IO/Class.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/IO/Class.hs @@ -0,0 +1,3 @@ +module Control.Monad.IO.Class (module Exports) where + +import "base" Control.Monad.IO.Class as Exports diff --git a/src/Control/Monad/Instances.hs b/src/Control/Monad/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Instances.hs @@ -0,0 +1,3 @@ +module Control.Monad.Instances (module Exports) where + +import "base" Control.Monad.Instances as Exports diff --git a/src/Control/Monad/ST.hs b/src/Control/Monad/ST.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST (module Exports) where + +import "base" Control.Monad.ST as Exports diff --git a/src/Control/Monad/ST/Lazy.hs b/src/Control/Monad/ST/Lazy.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST/Lazy.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST.Lazy (module Exports) where + +import "base" Control.Monad.ST.Lazy as Exports diff --git a/src/Control/Monad/ST/Lazy/Safe.hs b/src/Control/Monad/ST/Lazy/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST/Lazy/Safe.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST.Lazy.Safe (module Exports) where + +import "base" Control.Monad.ST.Lazy.Safe as Exports diff --git a/src/Control/Monad/ST/Lazy/Unsafe.hs b/src/Control/Monad/ST/Lazy/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST/Lazy/Unsafe.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST.Lazy.Unsafe (module Exports) where + +import "base" Control.Monad.ST.Lazy.Unsafe as Exports diff --git a/src/Control/Monad/ST/Safe.hs b/src/Control/Monad/ST/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST/Safe.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST.Safe (module Exports) where + +import "base" Control.Monad.ST.Safe as Exports diff --git a/src/Control/Monad/ST/Strict.hs b/src/Control/Monad/ST/Strict.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST/Strict.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST.Strict (module Exports) where + +import "base" Control.Monad.ST.Strict as Exports diff --git a/src/Control/Monad/ST/Unsafe.hs b/src/Control/Monad/ST/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/ST/Unsafe.hs @@ -0,0 +1,3 @@ +module Control.Monad.ST.Unsafe (module Exports) where + +import "base" Control.Monad.ST.Unsafe as Exports diff --git a/src/Control/Monad/Zip.hs b/src/Control/Monad/Zip.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Zip.hs @@ -0,0 +1,3 @@ +module Control.Monad.Zip (module Exports) where + +import "base" Control.Monad.Zip as Exports diff --git a/src/Data/Bifoldable.hs b/src/Data/Bifoldable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bifoldable.hs @@ -0,0 +1,3 @@ +module Data.Bifoldable (module Exports) where + +import "base" Data.Bifoldable as Exports diff --git a/src/Data/Bifunctor.hs b/src/Data/Bifunctor.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bifunctor.hs @@ -0,0 +1,3 @@ +module Data.Bifunctor (module Exports) where + +import "base" Data.Bifunctor as Exports diff --git a/src/Data/Bitraversable.hs b/src/Data/Bitraversable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bitraversable.hs @@ -0,0 +1,3 @@ +module Data.Bitraversable (module Exports) where + +import "base" Data.Bitraversable as Exports diff --git a/src/Data/Bits.hs b/src/Data/Bits.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bits.hs @@ -0,0 +1,3 @@ +module Data.Bits ( module Exports ) where + +import "base" Data.Bits as Exports diff --git a/src/Data/Bits.spec b/src/Data/Bits.spec new file mode 100644 --- /dev/null +++ b/src/Data/Bits.spec @@ -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)) } + diff --git a/src/Data/Bool.hs b/src/Data/Bool.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bool.hs @@ -0,0 +1,3 @@ +module Data.Bool (module Exports) where + +import "base" Data.Bool as Exports diff --git a/src/Data/Char.hs b/src/Data/Char.hs new file mode 100644 --- /dev/null +++ b/src/Data/Char.hs @@ -0,0 +1,4 @@ +module Data.Char ( module Exports ) where + +import GHC.Base +import "base" Data.Char as Exports diff --git a/src/Data/Coerce.hs b/src/Data/Coerce.hs new file mode 100644 --- /dev/null +++ b/src/Data/Coerce.hs @@ -0,0 +1,3 @@ +module Data.Coerce (module Exports) where + +import "base" Data.Coerce as Exports diff --git a/src/Data/Complex.hs b/src/Data/Complex.hs new file mode 100644 --- /dev/null +++ b/src/Data/Complex.hs @@ -0,0 +1,3 @@ +module Data.Complex (module Exports) where + +import "base" Data.Complex as Exports diff --git a/src/Data/Data.hs b/src/Data/Data.hs new file mode 100644 --- /dev/null +++ b/src/Data/Data.hs @@ -0,0 +1,3 @@ +module Data.Data (module Exports) where + +import "base" Data.Data as Exports diff --git a/src/Data/Dynamic.hs b/src/Data/Dynamic.hs new file mode 100644 --- /dev/null +++ b/src/Data/Dynamic.hs @@ -0,0 +1,3 @@ +module Data.Dynamic (module Exports) where + +import "base" Data.Dynamic as Exports diff --git a/src/Data/Either.hs b/src/Data/Either.hs new file mode 100644 --- /dev/null +++ b/src/Data/Either.hs @@ -0,0 +1,5 @@ +module Data.Either ( module Exports ) where + +import GHC.Base + +import "base" Data.Either as Exports diff --git a/src/Data/Either.spec b/src/Data/Either.spec new file mode 100644 --- /dev/null +++ b/src/Data/Either.spec @@ -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 diff --git a/src/Data/Eq.hs b/src/Data/Eq.hs new file mode 100644 --- /dev/null +++ b/src/Data/Eq.hs @@ -0,0 +1,3 @@ +module Data.Eq (module Exports) where + +import "base" Data.Eq as Exports diff --git a/src/Data/Fixed.hs b/src/Data/Fixed.hs new file mode 100644 --- /dev/null +++ b/src/Data/Fixed.hs @@ -0,0 +1,3 @@ +module Data.Fixed (module Exports) where + +import "base" Data.Fixed as Exports diff --git a/src/Data/Foldable.hs b/src/Data/Foldable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Foldable.hs @@ -0,0 +1,4 @@ +module Data.Foldable (module Exports) where + +import GHC.Types +import "base" Data.Foldable as Exports diff --git a/src/Data/Foldable.spec b/src/Data/Foldable.spec new file mode 100644 --- /dev/null +++ b/src/Data/Foldable.spec @@ -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} diff --git a/src/Data/Function.hs b/src/Data/Function.hs new file mode 100644 --- /dev/null +++ b/src/Data/Function.hs @@ -0,0 +1,3 @@ +module Data.Function ( module Exports) where + +import "base" Data.Function as Exports diff --git a/src/Data/Functor.hs b/src/Data/Functor.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor.hs @@ -0,0 +1,3 @@ +module Data.Functor ( module Exports ) where + +import "base" Data.Functor as Exports diff --git a/src/Data/Functor/Classes.hs b/src/Data/Functor/Classes.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Classes.hs @@ -0,0 +1,3 @@ +module Data.Functor.Classes (module Exports) where + +import "base" Data.Functor.Classes as Exports diff --git a/src/Data/Functor/Compose.hs b/src/Data/Functor/Compose.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Compose.hs @@ -0,0 +1,3 @@ +module Data.Functor.Compose (module Exports) where + +import "base" Data.Functor.Compose as Exports diff --git a/src/Data/Functor/Const.hs b/src/Data/Functor/Const.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Const.hs @@ -0,0 +1,3 @@ +module Data.Functor.Const (module Exports) where + +import "base" Data.Functor.Const as Exports diff --git a/src/Data/Functor/Contravariant.hs b/src/Data/Functor/Contravariant.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Contravariant.hs @@ -0,0 +1,3 @@ +module Data.Functor.Contravariant (module Exports) where + +import "base" Data.Functor.Contravariant as Exports diff --git a/src/Data/Functor/Identity.hs b/src/Data/Functor/Identity.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Identity.hs @@ -0,0 +1,3 @@ +module Data.Functor.Identity (module Exports) where + +import "base" Data.Functor.Identity as Exports diff --git a/src/Data/Functor/Product.hs b/src/Data/Functor/Product.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Product.hs @@ -0,0 +1,3 @@ +module Data.Functor.Product (module Exports) where + +import "base" Data.Functor.Product as Exports diff --git a/src/Data/Functor/Sum.hs b/src/Data/Functor/Sum.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Sum.hs @@ -0,0 +1,3 @@ +module Data.Functor.Sum (module Exports) where + +import "base" Data.Functor.Sum as Exports diff --git a/src/Data/IORef.hs b/src/Data/IORef.hs new file mode 100644 --- /dev/null +++ b/src/Data/IORef.hs @@ -0,0 +1,5 @@ +module Data.IORef (module Exports ) where + +import GHC.Base +import "base" Data.IORef as Exports + diff --git a/src/Data/Int.hs b/src/Data/Int.hs new file mode 100644 --- /dev/null +++ b/src/Data/Int.hs @@ -0,0 +1,4 @@ +module Data.Int ( module Exports ) where + +import GHC.Int +import "base" Data.Int as Exports diff --git a/src/Data/Int.spec b/src/Data/Int.spec new file mode 100644 --- /dev/null +++ b/src/Data/Int.spec @@ -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} diff --git a/src/Data/Ix.hs b/src/Data/Ix.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ix.hs @@ -0,0 +1,3 @@ +module Data.Ix (module Exports) where + +import "base" Data.Ix as Exports diff --git a/src/Data/Kind.hs b/src/Data/Kind.hs new file mode 100644 --- /dev/null +++ b/src/Data/Kind.hs @@ -0,0 +1,3 @@ +module Data.Kind (module Exports) where + +import "base" Data.Kind as Exports diff --git a/src/Data/List.hs b/src/Data/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/List.hs @@ -0,0 +1,4 @@ +module Data.List ( module Exports) where + +import Data.Char +import "base" Data.List as Exports diff --git a/src/Data/List/NonEmpty.hs b/src/Data/List/NonEmpty.hs new file mode 100644 --- /dev/null +++ b/src/Data/List/NonEmpty.hs @@ -0,0 +1,4 @@ +module Data.List.NonEmpty ( module Exports ) where + +import Data.List +import "base" Data.List.NonEmpty as Exports diff --git a/src/Data/Maybe.hs b/src/Data/Maybe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Maybe.hs @@ -0,0 +1,4 @@ +module Data.Maybe ( module Exports ) where + +import GHC.Base +import "base" Data.Maybe as Exports diff --git a/src/Data/Monoid.hs b/src/Data/Monoid.hs new file mode 100644 --- /dev/null +++ b/src/Data/Monoid.hs @@ -0,0 +1,3 @@ +module Data.Monoid (module Exports) where + +import "base" Data.Monoid as Exports diff --git a/src/Data/Ord.hs b/src/Data/Ord.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ord.hs @@ -0,0 +1,3 @@ +module Data.Ord ( module Exports) where + +import "base" Data.Ord as Exports diff --git a/src/Data/Proxy.hs b/src/Data/Proxy.hs new file mode 100644 --- /dev/null +++ b/src/Data/Proxy.hs @@ -0,0 +1,3 @@ +module Data.Proxy (module Exports) where + +import "base" Data.Proxy as Exports diff --git a/src/Data/Ratio.hs b/src/Data/Ratio.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ratio.hs @@ -0,0 +1,4 @@ +module Data.Ratio ( module Exports ) where + +import GHC.Base +import "base" Data.Ratio as Exports diff --git a/src/Data/STRef.hs b/src/Data/STRef.hs new file mode 100644 --- /dev/null +++ b/src/Data/STRef.hs @@ -0,0 +1,3 @@ +module Data.STRef (module Exports) where + +import "base" Data.STRef as Exports diff --git a/src/Data/STRef/Lazy.hs b/src/Data/STRef/Lazy.hs new file mode 100644 --- /dev/null +++ b/src/Data/STRef/Lazy.hs @@ -0,0 +1,3 @@ +module Data.STRef.Lazy (module Exports) where + +import "base" Data.STRef.Lazy as Exports diff --git a/src/Data/STRef/Strict.hs b/src/Data/STRef/Strict.hs new file mode 100644 --- /dev/null +++ b/src/Data/STRef/Strict.hs @@ -0,0 +1,3 @@ +module Data.STRef.Strict (module Exports) where + +import "base" Data.STRef.Strict as Exports diff --git a/src/Data/Semigroup.hs b/src/Data/Semigroup.hs new file mode 100644 --- /dev/null +++ b/src/Data/Semigroup.hs @@ -0,0 +1,3 @@ +module Data.Semigroup (module Exports) where + +import "base" Data.Semigroup as Exports diff --git a/src/Data/String.hs b/src/Data/String.hs new file mode 100644 --- /dev/null +++ b/src/Data/String.hs @@ -0,0 +1,5 @@ +module Data.String ( module Exports ) where + +import GHC.Base +import "base" Data.String as Exports + diff --git a/src/Data/String.spec b/src/Data/String.spec new file mode 100644 --- /dev/null +++ b/src/Data/String.spec @@ -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 } diff --git a/src/Data/Traversable.hs b/src/Data/Traversable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Traversable.hs @@ -0,0 +1,3 @@ +module Data.Traversable (module Exports) where + +import "base" Data.Traversable as Exports diff --git a/src/Data/Tuple.hs b/src/Data/Tuple.hs new file mode 100644 --- /dev/null +++ b/src/Data/Tuple.hs @@ -0,0 +1,5 @@ +module Data.Tuple (module Exports) where + +import GHC.Base + +import "base" Data.Tuple as Exports diff --git a/src/Data/Tuple.spec b/src/Data/Tuple.spec new file mode 100644 --- /dev/null +++ b/src/Data/Tuple.spec @@ -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 } diff --git a/src/Data/Type/Bool.hs b/src/Data/Type/Bool.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Bool.hs @@ -0,0 +1,3 @@ +module Data.Type.Bool (module Exports) where + +import "base" Data.Type.Bool as Exports diff --git a/src/Data/Type/Coercion.hs b/src/Data/Type/Coercion.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Coercion.hs @@ -0,0 +1,3 @@ +module Data.Type.Coercion (module Exports) where + +import "base" Data.Type.Coercion as Exports diff --git a/src/Data/Type/Equality.hs b/src/Data/Type/Equality.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Equality.hs @@ -0,0 +1,3 @@ +module Data.Type.Equality (module Exports) where + +import "base" Data.Type.Equality as Exports diff --git a/src/Data/Typeable.hs b/src/Data/Typeable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Typeable.hs @@ -0,0 +1,3 @@ +module Data.Typeable (module Exports) where + +import "base" Data.Typeable as Exports diff --git a/src/Data/Unique.hs b/src/Data/Unique.hs new file mode 100644 --- /dev/null +++ b/src/Data/Unique.hs @@ -0,0 +1,3 @@ +module Data.Unique (module Exports) where + +import "base" Data.Unique as Exports diff --git a/src/Data/Version.hs b/src/Data/Version.hs new file mode 100644 --- /dev/null +++ b/src/Data/Version.hs @@ -0,0 +1,3 @@ +module Data.Version (module Exports) where + +import "base" Data.Version as Exports diff --git a/src/Data/Void.hs b/src/Data/Void.hs new file mode 100644 --- /dev/null +++ b/src/Data/Void.hs @@ -0,0 +1,3 @@ +module Data.Void (module Exports) where + +import "base" Data.Void as Exports diff --git a/src/Data/Word.hs b/src/Data/Word.hs new file mode 100644 --- /dev/null +++ b/src/Data/Word.hs @@ -0,0 +1,3 @@ +module Data.Word ( module Exports) where + +import "base" Data.Word as Exports diff --git a/src/Data/Word.spec b/src/Data/Word.spec new file mode 100644 --- /dev/null +++ b/src/Data/Word.spec @@ -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 } diff --git a/src/Debug/Trace.hs b/src/Debug/Trace.hs new file mode 100644 --- /dev/null +++ b/src/Debug/Trace.hs @@ -0,0 +1,3 @@ +module Debug.Trace (module Exports) where + +import "base" Debug.Trace as Exports diff --git a/src/Foreign.hs b/src/Foreign.hs new file mode 100644 --- /dev/null +++ b/src/Foreign.hs @@ -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 diff --git a/src/Foreign/C.hs b/src/Foreign/C.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/C.hs @@ -0,0 +1,3 @@ +module Foreign.C (module Exports) where + +import "base" Foreign.C as Exports diff --git a/src/Foreign/C/Error.hs b/src/Foreign/C/Error.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/C/Error.hs @@ -0,0 +1,3 @@ +module Foreign.C.Error (module Exports) where + +import "base" Foreign.C.Error as Exports diff --git a/src/Foreign/C/String.hs b/src/Foreign/C/String.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/C/String.hs @@ -0,0 +1,4 @@ +module Foreign.C.String (module Exports) where + +import Foreign.Ptr +import "base" Foreign.C.String as Exports diff --git a/src/Foreign/C/String.spec b/src/Foreign/C/String.spec new file mode 100644 --- /dev/null +++ b/src/Foreign/C/String.spec @@ -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 diff --git a/src/Foreign/C/Types.hs b/src/Foreign/C/Types.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/C/Types.hs @@ -0,0 +1,5 @@ +module Foreign.C.Types (module Exports) where + +import GHC.Base +import GHC.Word +import "base" Foreign.C.Types as Exports diff --git a/src/Foreign/C/Types.spec b/src/Foreign/C/Types.spec new file mode 100644 --- /dev/null +++ b/src/Foreign/C/Types.spec @@ -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 diff --git a/src/Foreign/Concurrent.hs b/src/Foreign/Concurrent.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Concurrent.hs @@ -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 diff --git a/src/Foreign/Concurrent.spec b/src/Foreign/Concurrent.spec new file mode 100644 --- /dev/null +++ b/src/Foreign/Concurrent.spec @@ -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))) diff --git a/src/Foreign/ForeignPtr.hs b/src/Foreign/ForeignPtr.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/ForeignPtr.hs @@ -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 diff --git a/src/Foreign/ForeignPtr.spec b/src/Foreign/ForeignPtr.spec new file mode 100644 --- /dev/null +++ b/src/Foreign/ForeignPtr.spec @@ -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) diff --git a/src/Foreign/ForeignPtr/Safe.hs b/src/Foreign/ForeignPtr/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/ForeignPtr/Safe.hs @@ -0,0 +1,3 @@ +module Foreign.ForeignPtr.Safe (module Exports) where + +import "base" Foreign.ForeignPtr.Safe as Exports diff --git a/src/Foreign/ForeignPtr/Unsafe.hs b/src/Foreign/ForeignPtr/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/ForeignPtr/Unsafe.hs @@ -0,0 +1,3 @@ +module Foreign.ForeignPtr.Unsafe (module Exports) where + +import "base" Foreign.ForeignPtr.Unsafe as Exports diff --git a/src/Foreign/Marshal.hs b/src/Foreign/Marshal.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal (module Exports) where + +import "base" Foreign.Marshal as Exports diff --git a/src/Foreign/Marshal/Alloc.hs b/src/Foreign/Marshal/Alloc.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Alloc.hs @@ -0,0 +1,7 @@ +module Foreign.Marshal.Alloc (module Exports) where + +import GHC.Types +import GHC.Ptr + +import "base" Foreign.Marshal.Alloc as Exports + diff --git a/src/Foreign/Marshal/Array.hs b/src/Foreign/Marshal/Array.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Array.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal.Array (module Exports) where + +import "base" Foreign.Marshal.Array as Exports diff --git a/src/Foreign/Marshal/Error.hs b/src/Foreign/Marshal/Error.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Error.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal.Error (module Exports) where + +import "base" Foreign.Marshal.Error as Exports diff --git a/src/Foreign/Marshal/Pool.hs b/src/Foreign/Marshal/Pool.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Pool.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal.Pool (module Exports) where + +import "base" Foreign.Marshal.Pool as Exports diff --git a/src/Foreign/Marshal/Safe.hs b/src/Foreign/Marshal/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Safe.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal.Safe (module Exports) where + +import "base" Foreign.Marshal.Safe as Exports diff --git a/src/Foreign/Marshal/Unsafe.hs b/src/Foreign/Marshal/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Unsafe.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal.Unsafe (module Exports) where + +import "base" Foreign.Marshal.Unsafe as Exports diff --git a/src/Foreign/Marshal/Utils.hs b/src/Foreign/Marshal/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Marshal/Utils.hs @@ -0,0 +1,3 @@ +module Foreign.Marshal.Utils (module Exports) where + +import "base" Foreign.Marshal.Utils as Exports diff --git a/src/Foreign/Ptr.hs b/src/Foreign/Ptr.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Ptr.hs @@ -0,0 +1,4 @@ +module Foreign.Ptr (module Exports) where + +import GHC.Ptr +import "base" Foreign.Ptr as Exports diff --git a/src/Foreign/Ptr.spec b/src/Foreign/Ptr.spec new file mode 100644 --- /dev/null +++ b/src/Foreign/Ptr.spec @@ -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 } + diff --git a/src/Foreign/Safe.hs b/src/Foreign/Safe.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Safe.hs @@ -0,0 +1,3 @@ +module Foreign.Safe (module Exports) where + +import "base" Foreign.Safe as Exports diff --git a/src/Foreign/StablePtr.hs b/src/Foreign/StablePtr.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/StablePtr.hs @@ -0,0 +1,3 @@ +module Foreign.StablePtr (module Exports) where + +import "base" Foreign.StablePtr as Exports diff --git a/src/Foreign/Storable.hs b/src/Foreign/Storable.hs new file mode 100644 --- /dev/null +++ b/src/Foreign/Storable.hs @@ -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 diff --git a/src/Foreign/Storable.spec b/src/Foreign/Storable.spec new file mode 100644 --- /dev/null +++ b/src/Foreign/Storable.spec @@ -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 () diff --git a/src/GHC/Arr.hs b/src/GHC/Arr.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Arr.hs @@ -0,0 +1,3 @@ +module GHC.Arr (module Exports) where + +import "base" GHC.Arr as Exports diff --git a/src/GHC/Base.hs b/src/GHC/Base.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Base.hs @@ -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 diff --git a/src/GHC/Base.spec b/src/GHC/Base.spec new file mode 100644 --- /dev/null +++ b/src/GHC/Base.spec @@ -0,0 +1,61 @@ +module spec GHC.Base where + +import GHC.CString +import GHC.Classes +import GHC.Types +import GHC.Tuple + +GHC.Base.. :: forall

c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>. + {xcmp::a, wcmp::b |- c

<: c} + (ycmp:b -> c

) + -> (zcmp:a -> b) + -> xcmp:a -> c + +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) diff --git a/src/GHC/ByteOrder.hs b/src/GHC/ByteOrder.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ByteOrder.hs @@ -0,0 +1,3 @@ +module GHC.ByteOrder (module Exports) where + +import "base" GHC.ByteOrder as Exports diff --git a/src/GHC/Char.hs b/src/GHC/Char.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Char.hs @@ -0,0 +1,3 @@ +module GHC.Char (module Exports) where + +import "base" GHC.Char as Exports diff --git a/src/GHC/Clock.hs b/src/GHC/Clock.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Clock.hs @@ -0,0 +1,3 @@ +module GHC.Clock (module Exports) where + +import "base" GHC.Clock as Exports diff --git a/src/GHC/Conc.hs b/src/GHC/Conc.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Conc.hs @@ -0,0 +1,3 @@ +module GHC.Conc (module Exports) where + +import "base" GHC.Conc as Exports diff --git a/src/GHC/Conc/IO.hs b/src/GHC/Conc/IO.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Conc/IO.hs @@ -0,0 +1,3 @@ +module GHC.Conc.IO (module Exports) where + +import "base" GHC.Conc.IO as Exports diff --git a/src/GHC/Conc/Signal.hs b/src/GHC/Conc/Signal.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Conc/Signal.hs @@ -0,0 +1,3 @@ +module GHC.Conc.Signal (module Exports) where + +import "base" GHC.Conc.Signal as Exports diff --git a/src/GHC/Conc/Sync.hs b/src/GHC/Conc/Sync.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Conc/Sync.hs @@ -0,0 +1,3 @@ +module GHC.Conc.Sync (module Exports) where + +import "base" GHC.Conc.Sync as Exports diff --git a/src/GHC/ConsoleHandler.hs b/src/GHC/ConsoleHandler.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ConsoleHandler.hs @@ -0,0 +1,3 @@ +module GHC.ConsoleHandler (module Exports) where + +import "base" GHC.ConsoleHandler as Exports diff --git a/src/GHC/Constants.hs b/src/GHC/Constants.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Constants.hs @@ -0,0 +1,3 @@ +module GHC.Constants (module Exports) where + +import "base" GHC.Constants as Exports diff --git a/src/GHC/Desugar.hs b/src/GHC/Desugar.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Desugar.hs @@ -0,0 +1,3 @@ +module GHC.Desugar (module Exports) where + +import "base" GHC.Desugar as Exports diff --git a/src/GHC/Enum.hs b/src/GHC/Enum.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Enum.hs @@ -0,0 +1,3 @@ +module GHC.Enum (module Exports) where + +import "base" GHC.Enum as Exports diff --git a/src/GHC/Environment.hs b/src/GHC/Environment.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Environment.hs @@ -0,0 +1,3 @@ +module GHC.Environment (module Exports) where + +import "base" GHC.Environment as Exports diff --git a/src/GHC/Err.hs b/src/GHC/Err.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Err.hs @@ -0,0 +1,3 @@ +module GHC.Err (module Exports) where + +import "base" GHC.Err as Exports diff --git a/src/GHC/Exception.hs b/src/GHC/Exception.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Exception.hs @@ -0,0 +1,3 @@ +module GHC.Exception (module Exports) where + +import "base" GHC.Exception as Exports diff --git a/src/GHC/Exception/Type.hs b/src/GHC/Exception/Type.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Exception/Type.hs @@ -0,0 +1,3 @@ +module GHC.Exception.Type (module Exports) where + +import "base" GHC.Exception.Type as Exports diff --git a/src/GHC/ExecutionStack.hs b/src/GHC/ExecutionStack.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ExecutionStack.hs @@ -0,0 +1,3 @@ +module GHC.ExecutionStack (module Exports) where + +import "base" GHC.ExecutionStack as Exports diff --git a/src/GHC/ExecutionStack/Internal.hs b/src/GHC/ExecutionStack/Internal.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ExecutionStack/Internal.hs @@ -0,0 +1,3 @@ +module GHC.ExecutionStack.Internal (module Exports) where + +import "base" GHC.ExecutionStack.Internal as Exports diff --git a/src/GHC/Exts.hs b/src/GHC/Exts.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Exts.hs @@ -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} @-} diff --git a/src/GHC/Fingerprint.hs b/src/GHC/Fingerprint.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Fingerprint.hs @@ -0,0 +1,3 @@ +module GHC.Fingerprint (module Exports) where + +import "base" GHC.Fingerprint as Exports diff --git a/src/GHC/Fingerprint/Type.hs b/src/GHC/Fingerprint/Type.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Fingerprint/Type.hs @@ -0,0 +1,3 @@ +module GHC.Fingerprint.Type (module Exports) where + +import "base" GHC.Fingerprint.Type as Exports diff --git a/src/GHC/Float.hs b/src/GHC/Float.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Float.hs @@ -0,0 +1,3 @@ +module GHC.Float (module Exports) where + +import "base" GHC.Float as Exports diff --git a/src/GHC/Float/ConversionUtils.hs b/src/GHC/Float/ConversionUtils.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Float/ConversionUtils.hs @@ -0,0 +1,3 @@ +module GHC.Float.ConversionUtils (module Exports) where + +import "base" GHC.Float.ConversionUtils as Exports diff --git a/src/GHC/Float/RealFracMethods.hs b/src/GHC/Float/RealFracMethods.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Float/RealFracMethods.hs @@ -0,0 +1,3 @@ +module GHC.Float.RealFracMethods (module Exports) where + +import "base" GHC.Float.RealFracMethods as Exports diff --git a/src/GHC/Foreign.hs b/src/GHC/Foreign.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Foreign.hs @@ -0,0 +1,3 @@ +module GHC.Foreign (module Exports) where + +import "base" GHC.Foreign as Exports diff --git a/src/GHC/ForeignPtr.hs b/src/GHC/ForeignPtr.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ForeignPtr.hs @@ -0,0 +1,4 @@ +module GHC.ForeignPtr ( module Exports ) where + +import GHC.Base +import "base" GHC.ForeignPtr as Exports diff --git a/src/GHC/ForeignPtr.spec b/src/GHC/ForeignPtr.spec new file mode 100644 --- /dev/null +++ b/src/GHC/ForeignPtr.spec @@ -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)) diff --git a/src/GHC/GHCi.hs b/src/GHC/GHCi.hs new file mode 100644 --- /dev/null +++ b/src/GHC/GHCi.hs @@ -0,0 +1,3 @@ +module GHC.GHCi (module Exports) where + +import "base" GHC.GHCi as Exports diff --git a/src/GHC/GHCi/Helpers.hs b/src/GHC/GHCi/Helpers.hs new file mode 100644 --- /dev/null +++ b/src/GHC/GHCi/Helpers.hs @@ -0,0 +1,3 @@ +module GHC.GHCi.Helpers (module Exports) where + +import "base" GHC.GHCi.Helpers as Exports diff --git a/src/GHC/Generics.hs b/src/GHC/Generics.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Generics.hs @@ -0,0 +1,4 @@ +module GHC.Generics ( module Exports ) where + +import GHC.Base +import "base" GHC.Generics as Exports diff --git a/src/GHC/IO.hs b/src/GHC/IO.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO.hs @@ -0,0 +1,4 @@ +module GHC.IO ( module Exports ) where + +import GHC.Base +import "base" GHC.IO as Exports diff --git a/src/GHC/IO/Buffer.hs b/src/GHC/IO/Buffer.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Buffer.hs @@ -0,0 +1,3 @@ +module GHC.IO.Buffer (module Exports) where + +import "base" GHC.IO.Buffer as Exports diff --git a/src/GHC/IO/BufferedIO.hs b/src/GHC/IO/BufferedIO.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/BufferedIO.hs @@ -0,0 +1,3 @@ +module GHC.IO.BufferedIO (module Exports) where + +import "base" GHC.IO.BufferedIO as Exports diff --git a/src/GHC/IO/Device.hs b/src/GHC/IO/Device.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Device.hs @@ -0,0 +1,3 @@ +module GHC.IO.Device (module Exports) where + +import "base" GHC.IO.Device as Exports diff --git a/src/GHC/IO/Encoding.hs b/src/GHC/IO/Encoding.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding (module Exports) where + +import "base" GHC.IO.Encoding as Exports diff --git a/src/GHC/IO/Encoding/CodePage.hs b/src/GHC/IO/Encoding/CodePage.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/CodePage.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.CodePage (module Exports) where + +import "base" GHC.IO.Encoding.CodePage as Exports diff --git a/src/GHC/IO/Encoding/Failure.hs b/src/GHC/IO/Encoding/Failure.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/Failure.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.Failure (module Exports) where + +import "base" GHC.IO.Encoding.Failure as Exports diff --git a/src/GHC/IO/Encoding/Iconv.hs b/src/GHC/IO/Encoding/Iconv.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/Iconv.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.Iconv (module Exports) where + +import "base" GHC.IO.Encoding.Iconv as Exports diff --git a/src/GHC/IO/Encoding/Latin1.hs b/src/GHC/IO/Encoding/Latin1.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/Latin1.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.Latin1 (module Exports) where + +import "base" GHC.IO.Encoding.Latin1 as Exports diff --git a/src/GHC/IO/Encoding/Types.hs b/src/GHC/IO/Encoding/Types.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/Types.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.Types (module Exports) where + +import "base" GHC.IO.Encoding.Types as Exports diff --git a/src/GHC/IO/Encoding/UTF16.hs b/src/GHC/IO/Encoding/UTF16.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/UTF16.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.UTF16 (module Exports) where + +import "base" GHC.IO.Encoding.UTF16 as Exports diff --git a/src/GHC/IO/Encoding/UTF32.hs b/src/GHC/IO/Encoding/UTF32.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/UTF32.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.UTF32 (module Exports) where + +import "base" GHC.IO.Encoding.UTF32 as Exports diff --git a/src/GHC/IO/Encoding/UTF8.hs b/src/GHC/IO/Encoding/UTF8.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Encoding/UTF8.hs @@ -0,0 +1,3 @@ +module GHC.IO.Encoding.UTF8 (module Exports) where + +import "base" GHC.IO.Encoding.UTF8 as Exports diff --git a/src/GHC/IO/Exception.hs b/src/GHC/IO/Exception.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Exception.hs @@ -0,0 +1,3 @@ +module GHC.IO.Exception (module Exports) where + +import "base" GHC.IO.Exception as Exports diff --git a/src/GHC/IO/FD.hs b/src/GHC/IO/FD.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/FD.hs @@ -0,0 +1,3 @@ +module GHC.IO.FD (module Exports) where + +import "base" GHC.IO.FD as Exports diff --git a/src/GHC/IO/Handle.hs b/src/GHC/IO/Handle.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle.hs @@ -0,0 +1,4 @@ +module GHC.IO.Handle ( module Exports ) where + +import GHC.Types +import "base" GHC.IO.Handle as Exports diff --git a/src/GHC/IO/Handle.spec b/src/GHC/IO/Handle.spec new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle.spec @@ -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}) diff --git a/src/GHC/IO/Handle/FD.hs b/src/GHC/IO/Handle/FD.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle/FD.hs @@ -0,0 +1,3 @@ +module GHC.IO.Handle.FD (module Exports) where + +import "base" GHC.IO.Handle.FD as Exports diff --git a/src/GHC/IO/Handle/Internals.hs b/src/GHC/IO/Handle/Internals.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle/Internals.hs @@ -0,0 +1,3 @@ +module GHC.IO.Handle.Internals (module Exports) where + +import "base" GHC.IO.Handle.Internals as Exports diff --git a/src/GHC/IO/Handle/Lock.hs b/src/GHC/IO/Handle/Lock.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle/Lock.hs @@ -0,0 +1,3 @@ +module GHC.IO.Handle.Lock (module Exports) where + +import "base" GHC.IO.Handle.Lock as Exports diff --git a/src/GHC/IO/Handle/Text.hs b/src/GHC/IO/Handle/Text.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle/Text.hs @@ -0,0 +1,3 @@ +module GHC.IO.Handle.Text (module Exports) where + +import "base" GHC.IO.Handle.Text as Exports diff --git a/src/GHC/IO/Handle/Types.hs b/src/GHC/IO/Handle/Types.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Handle/Types.hs @@ -0,0 +1,3 @@ +module GHC.IO.Handle.Types (module Exports) where + +import "base" GHC.IO.Handle.Types as Exports diff --git a/src/GHC/IO/IOMode.hs b/src/GHC/IO/IOMode.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/IOMode.hs @@ -0,0 +1,3 @@ +module GHC.IO.IOMode (module Exports) where + +import "base" GHC.IO.IOMode as Exports diff --git a/src/GHC/IO/Unsafe.hs b/src/GHC/IO/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IO/Unsafe.hs @@ -0,0 +1,3 @@ +module GHC.IO.Unsafe (module Exports) where + +import "base" GHC.IO.Unsafe as Exports diff --git a/src/GHC/IOArray.hs b/src/GHC/IOArray.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IOArray.hs @@ -0,0 +1,3 @@ +module GHC.IOArray (module Exports) where + +import "base" GHC.IOArray as Exports diff --git a/src/GHC/IORef.hs b/src/GHC/IORef.hs new file mode 100644 --- /dev/null +++ b/src/GHC/IORef.hs @@ -0,0 +1,3 @@ +module GHC.IORef (module Exports) where + +import "base" GHC.IORef as Exports diff --git a/src/GHC/Int.hs b/src/GHC/Int.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Int.hs @@ -0,0 +1,4 @@ +module GHC.Int (module Exports) where + +import GHC.Base +import "base" GHC.Int as Exports diff --git a/src/GHC/Int.spec b/src/GHC/Int.spec new file mode 100644 --- /dev/null +++ b/src/GHC/Int.spec @@ -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} diff --git a/src/GHC/Ix.hs b/src/GHC/Ix.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Ix.hs @@ -0,0 +1,3 @@ +module GHC.Ix (module Exports) where + +import "base" GHC.Ix as Exports diff --git a/src/GHC/List.hs b/src/GHC/List.hs new file mode 100644 --- /dev/null +++ b/src/GHC/List.hs @@ -0,0 +1,4 @@ +module GHC.List (module Exports) where + +import GHC.Base +import "base" GHC.List as Exports diff --git a/src/GHC/List.spec b/src/GHC/List.spec new file mode 100644 --- /dev/null +++ b/src/GHC/List.spec @@ -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 diff --git a/src/GHC/MVar.hs b/src/GHC/MVar.hs new file mode 100644 --- /dev/null +++ b/src/GHC/MVar.hs @@ -0,0 +1,3 @@ +module GHC.MVar (module Exports) where + +import "base" GHC.MVar as Exports diff --git a/src/GHC/Maybe.hs b/src/GHC/Maybe.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Maybe.hs @@ -0,0 +1,3 @@ +module GHC.Maybe (module Exports) where + +import "base" GHC.Maybe as Exports diff --git a/src/GHC/Natural.hs b/src/GHC/Natural.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Natural.hs @@ -0,0 +1,3 @@ +module GHC.Natural (module Exports) where + +import "base" GHC.Natural as Exports diff --git a/src/GHC/Num.hs b/src/GHC/Num.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Num.hs @@ -0,0 +1,4 @@ +module GHC.Num (module Exports) where + +import GHC.Base +import "base" GHC.Num as Exports diff --git a/src/GHC/Num.spec b/src/GHC/Num.spec new file mode 100644 --- /dev/null +++ b/src/GHC/Num.spec @@ -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 } diff --git a/src/GHC/OldList.hs b/src/GHC/OldList.hs new file mode 100644 --- /dev/null +++ b/src/GHC/OldList.hs @@ -0,0 +1,3 @@ +module GHC.OldList (module Exports) where + +import "base" GHC.OldList as Exports diff --git a/src/GHC/OverloadedLabels.hs b/src/GHC/OverloadedLabels.hs new file mode 100644 --- /dev/null +++ b/src/GHC/OverloadedLabels.hs @@ -0,0 +1,3 @@ +module GHC.OverloadedLabels (module Exports) where + +import "base" GHC.OverloadedLabels as Exports diff --git a/src/GHC/Pack.hs b/src/GHC/Pack.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Pack.hs @@ -0,0 +1,3 @@ +module GHC.Pack (module Exports) where + +import "base" GHC.Pack as Exports diff --git a/src/GHC/Profiling.hs b/src/GHC/Profiling.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Profiling.hs @@ -0,0 +1,3 @@ +module GHC.Profiling (module Exports) where + +import "base" GHC.Profiling as Exports diff --git a/src/GHC/Ptr.hs b/src/GHC/Ptr.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Ptr.hs @@ -0,0 +1,4 @@ +module GHC.Ptr ( module Exports ) where + +import GHC.Types +import "base" GHC.Ptr as Exports diff --git a/src/GHC/Ptr.spec b/src/GHC/Ptr.spec new file mode 100644 --- /dev/null +++ b/src/GHC/Ptr.spec @@ -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 + diff --git a/src/GHC/RTS/Flags.hs b/src/GHC/RTS/Flags.hs new file mode 100644 --- /dev/null +++ b/src/GHC/RTS/Flags.hs @@ -0,0 +1,3 @@ +module GHC.RTS.Flags (module Exports) where + +import "base" GHC.RTS.Flags as Exports diff --git a/src/GHC/Read.hs b/src/GHC/Read.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Read.hs @@ -0,0 +1,3 @@ +module GHC.Read (module Exports) where + +import "base" GHC.Read as Exports diff --git a/src/GHC/Real.hs b/src/GHC/Real.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Real.hs @@ -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 diff --git a/src/GHC/Real.spec b/src/GHC/Real.spec new file mode 100644 --- /dev/null +++ b/src/GHC/Real.spec @@ -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) } diff --git a/src/GHC/Records.hs b/src/GHC/Records.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Records.hs @@ -0,0 +1,3 @@ +module GHC.Records (module Exports) where + +import "base" GHC.Records as Exports diff --git a/src/GHC/ResponseFile.hs b/src/GHC/ResponseFile.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ResponseFile.hs @@ -0,0 +1,3 @@ +module GHC.ResponseFile (module Exports) where + +import "base" GHC.ResponseFile as Exports diff --git a/src/GHC/ST.hs b/src/GHC/ST.hs new file mode 100644 --- /dev/null +++ b/src/GHC/ST.hs @@ -0,0 +1,3 @@ +module GHC.ST (module Exports) where + +import "base" GHC.ST as Exports diff --git a/src/GHC/STRef.hs b/src/GHC/STRef.hs new file mode 100644 --- /dev/null +++ b/src/GHC/STRef.hs @@ -0,0 +1,3 @@ +module GHC.STRef (module Exports) where + +import "base" GHC.STRef as Exports diff --git a/src/GHC/Show.hs b/src/GHC/Show.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Show.hs @@ -0,0 +1,3 @@ +module GHC.Show (module Exports) where + +import "base" GHC.Show as Exports diff --git a/src/GHC/Stable.hs b/src/GHC/Stable.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Stable.hs @@ -0,0 +1,3 @@ +module GHC.Stable (module Exports) where + +import "base" GHC.Stable as Exports diff --git a/src/GHC/StableName.hs b/src/GHC/StableName.hs new file mode 100644 --- /dev/null +++ b/src/GHC/StableName.hs @@ -0,0 +1,3 @@ +module GHC.StableName (module Exports) where + +import "base" GHC.StableName as Exports diff --git a/src/GHC/Stack.hs b/src/GHC/Stack.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Stack.hs @@ -0,0 +1,3 @@ +module GHC.Stack (module Exports) where + +import "base" GHC.Stack as Exports diff --git a/src/GHC/Stack/CCS.hs b/src/GHC/Stack/CCS.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Stack/CCS.hs @@ -0,0 +1,3 @@ +module GHC.Stack.CCS (module Exports) where + +import "base" GHC.Stack.CCS as Exports diff --git a/src/GHC/Stack/Types.hs b/src/GHC/Stack/Types.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Stack/Types.hs @@ -0,0 +1,3 @@ +module GHC.Stack.Types (module Exports) where + +import "base" GHC.Stack.Types as Exports diff --git a/src/GHC/StaticPtr.hs b/src/GHC/StaticPtr.hs new file mode 100644 --- /dev/null +++ b/src/GHC/StaticPtr.hs @@ -0,0 +1,3 @@ +module GHC.StaticPtr (module Exports) where + +import "base" GHC.StaticPtr as Exports diff --git a/src/GHC/Stats.hs b/src/GHC/Stats.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Stats.hs @@ -0,0 +1,3 @@ +module GHC.Stats (module Exports) where + +import "base" GHC.Stats as Exports diff --git a/src/GHC/Storable.hs b/src/GHC/Storable.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Storable.hs @@ -0,0 +1,3 @@ +module GHC.Storable (module Exports) where + +import "base" GHC.Storable as Exports diff --git a/src/GHC/TopHandler.hs b/src/GHC/TopHandler.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TopHandler.hs @@ -0,0 +1,3 @@ +module GHC.TopHandler (module Exports) where + +import "base" GHC.TopHandler as Exports diff --git a/src/GHC/TypeLits.hs b/src/GHC/TypeLits.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits.hs @@ -0,0 +1,4 @@ +module GHC.TypeLits ( module Exports ) where + +import GHC.Base +import "base" GHC.TypeLits as Exports diff --git a/src/GHC/TypeNats.hs b/src/GHC/TypeNats.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeNats.hs @@ -0,0 +1,3 @@ +module GHC.TypeNats (module Exports) where + +import "base" GHC.TypeNats as Exports diff --git a/src/GHC/Unicode.hs b/src/GHC/Unicode.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Unicode.hs @@ -0,0 +1,3 @@ +module GHC.Unicode (module Exports) where + +import "base" GHC.Unicode as Exports diff --git a/src/GHC/Weak.hs b/src/GHC/Weak.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Weak.hs @@ -0,0 +1,3 @@ +module GHC.Weak (module Exports) where + +import "base" GHC.Weak as Exports diff --git a/src/GHC/Word.hs b/src/GHC/Word.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Word.hs @@ -0,0 +1,4 @@ +module GHC.Word (module Exports) where + +import GHC.Base +import "base" GHC.Word as Exports diff --git a/src/GHC/Word.spec b/src/GHC/Word.spec new file mode 100644 --- /dev/null +++ b/src/GHC/Word.spec @@ -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 diff --git a/src/Liquid/Prelude/NotReal.hs b/src/Liquid/Prelude/NotReal.hs new file mode 100644 --- /dev/null +++ b/src/Liquid/Prelude/NotReal.hs @@ -0,0 +1,4 @@ +module Liquid.Prelude.NotReal where + +import GHC.Num +import GHC.Real diff --git a/src/Liquid/Prelude/NotReal.spec b/src/Liquid/Prelude/NotReal.spec new file mode 100644 --- /dev/null +++ b/src/Liquid/Prelude/NotReal.spec @@ -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 diff --git a/src/Liquid/Prelude/Real.hs b/src/Liquid/Prelude/Real.hs new file mode 100644 --- /dev/null +++ b/src/Liquid/Prelude/Real.hs @@ -0,0 +1,3 @@ +module Liquid.Prelude.Real where + +import GHC.Num diff --git a/src/Liquid/Prelude/Real.spec b/src/Liquid/Prelude/Real.spec new file mode 100644 --- /dev/null +++ b/src/Liquid/Prelude/Real.spec @@ -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} diff --git a/src/Liquid/Prelude/Totality.hs b/src/Liquid/Prelude/Totality.hs new file mode 100644 --- /dev/null +++ b/src/Liquid/Prelude/Totality.hs @@ -0,0 +1,3 @@ +module Liquid.Prelude.Totality where + +import "base" Control.Exception.Base diff --git a/src/Liquid/Prelude/Totality.spec b/src/Liquid/Prelude/Totality.spec new file mode 100644 --- /dev/null +++ b/src/Liquid/Prelude/Totality.spec @@ -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 diff --git a/src/Numeric.hs b/src/Numeric.hs new file mode 100644 --- /dev/null +++ b/src/Numeric.hs @@ -0,0 +1,3 @@ +module Numeric (module Exports) where + +import "base" Numeric as Exports diff --git a/src/Numeric/Natural.hs b/src/Numeric/Natural.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/Natural.hs @@ -0,0 +1,3 @@ +module Numeric.Natural (module Exports) where + +import "base" Numeric.Natural as Exports diff --git a/src/Prelude.hs b/src/Prelude.hs new file mode 100644 --- /dev/null +++ b/src/Prelude.hs @@ -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 diff --git a/src/Prelude.spec b/src/Prelude.spec new file mode 100644 --- /dev/null +++ b/src/Prelude.spec @@ -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)]) diff --git a/src/System/CPUTime.hs b/src/System/CPUTime.hs new file mode 100644 --- /dev/null +++ b/src/System/CPUTime.hs @@ -0,0 +1,3 @@ +module System.CPUTime (module Exports) where + +import "base" System.CPUTime as Exports diff --git a/src/System/Console/GetOpt.hs b/src/System/Console/GetOpt.hs new file mode 100644 --- /dev/null +++ b/src/System/Console/GetOpt.hs @@ -0,0 +1,3 @@ +module System.Console.GetOpt (module Exports) where + +import "base" System.Console.GetOpt as Exports diff --git a/src/System/Environment.hs b/src/System/Environment.hs new file mode 100644 --- /dev/null +++ b/src/System/Environment.hs @@ -0,0 +1,3 @@ +module System.Environment (module Exports) where + +import "base" System.Environment as Exports diff --git a/src/System/Environment/Blank.hs b/src/System/Environment/Blank.hs new file mode 100644 --- /dev/null +++ b/src/System/Environment/Blank.hs @@ -0,0 +1,3 @@ +module System.Environment.Blank (module Exports) where + +import "base" System.Environment.Blank as Exports diff --git a/src/System/Exit.hs b/src/System/Exit.hs new file mode 100644 --- /dev/null +++ b/src/System/Exit.hs @@ -0,0 +1,3 @@ +module System.Exit (module Exports) where + +import "base" System.Exit as Exports diff --git a/src/System/IO.hs b/src/System/IO.hs new file mode 100644 --- /dev/null +++ b/src/System/IO.hs @@ -0,0 +1,4 @@ +module System.IO ( module Exports ) where + +import GHC.IO.Handle as Exports +import "base" System.IO as Exports diff --git a/src/System/IO.spec b/src/System/IO.spec new file mode 100644 --- /dev/null +++ b/src/System/IO.spec @@ -0,0 +1,3 @@ +module spec System.IO where + +import GHC.IO.Handle diff --git a/src/System/IO/Error.hs b/src/System/IO/Error.hs new file mode 100644 --- /dev/null +++ b/src/System/IO/Error.hs @@ -0,0 +1,3 @@ +module System.IO.Error (module Exports) where + +import "base" System.IO.Error as Exports diff --git a/src/System/IO/Unsafe.hs b/src/System/IO/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/System/IO/Unsafe.hs @@ -0,0 +1,3 @@ +module System.IO.Unsafe (module Exports) where + +import "base" System.IO.Unsafe as Exports diff --git a/src/System/Info.hs b/src/System/Info.hs new file mode 100644 --- /dev/null +++ b/src/System/Info.hs @@ -0,0 +1,3 @@ +module System.Info (module Exports) where + +import "base" System.Info as Exports diff --git a/src/System/Mem.hs b/src/System/Mem.hs new file mode 100644 --- /dev/null +++ b/src/System/Mem.hs @@ -0,0 +1,3 @@ +module System.Mem (module Exports) where + +import "base" System.Mem as Exports diff --git a/src/System/Mem/StableName.hs b/src/System/Mem/StableName.hs new file mode 100644 --- /dev/null +++ b/src/System/Mem/StableName.hs @@ -0,0 +1,3 @@ +module System.Mem.StableName (module Exports) where + +import "base" System.Mem.StableName as Exports diff --git a/src/System/Mem/Weak.hs b/src/System/Mem/Weak.hs new file mode 100644 --- /dev/null +++ b/src/System/Mem/Weak.hs @@ -0,0 +1,3 @@ +module System.Mem.Weak (module Exports) where + +import "base" System.Mem.Weak as Exports diff --git a/src/System/Posix/Internals.hs b/src/System/Posix/Internals.hs new file mode 100644 --- /dev/null +++ b/src/System/Posix/Internals.hs @@ -0,0 +1,3 @@ +module System.Posix.Internals (module Exports) where + +import "base" System.Posix.Internals as Exports diff --git a/src/System/Posix/Types.hs b/src/System/Posix/Types.hs new file mode 100644 --- /dev/null +++ b/src/System/Posix/Types.hs @@ -0,0 +1,3 @@ +module System.Posix.Types (module Exports) where + +import "base" System.Posix.Types as Exports diff --git a/src/System/Timeout.hs b/src/System/Timeout.hs new file mode 100644 --- /dev/null +++ b/src/System/Timeout.hs @@ -0,0 +1,3 @@ +module System.Timeout (module Exports) where + +import "base" System.Timeout as Exports diff --git a/src/Text/ParserCombinators/ReadP.hs b/src/Text/ParserCombinators/ReadP.hs new file mode 100644 --- /dev/null +++ b/src/Text/ParserCombinators/ReadP.hs @@ -0,0 +1,3 @@ +module Text.ParserCombinators.ReadP (module Exports) where + +import "base" Text.ParserCombinators.ReadP as Exports diff --git a/src/Text/ParserCombinators/ReadPrec.hs b/src/Text/ParserCombinators/ReadPrec.hs new file mode 100644 --- /dev/null +++ b/src/Text/ParserCombinators/ReadPrec.hs @@ -0,0 +1,3 @@ +module Text.ParserCombinators.ReadPrec (module Exports) where + +import "base" Text.ParserCombinators.ReadPrec as Exports diff --git a/src/Text/Printf.hs b/src/Text/Printf.hs new file mode 100644 --- /dev/null +++ b/src/Text/Printf.hs @@ -0,0 +1,3 @@ +module Text.Printf (module Exports) where + +import "base" Text.Printf as Exports diff --git a/src/Text/Read.hs b/src/Text/Read.hs new file mode 100644 --- /dev/null +++ b/src/Text/Read.hs @@ -0,0 +1,3 @@ +module Text.Read (module Exports) where + +import "base" Text.Read as Exports diff --git a/src/Text/Read/Lex.hs b/src/Text/Read/Lex.hs new file mode 100644 --- /dev/null +++ b/src/Text/Read/Lex.hs @@ -0,0 +1,3 @@ +module Text.Read.Lex (module Exports) where + +import "base" Text.Read.Lex as Exports diff --git a/src/Text/Show.hs b/src/Text/Show.hs new file mode 100644 --- /dev/null +++ b/src/Text/Show.hs @@ -0,0 +1,3 @@ +module Text.Show (module Exports) where + +import "base" Text.Show as Exports diff --git a/src/Text/Show/Functions.hs b/src/Text/Show/Functions.hs new file mode 100644 --- /dev/null +++ b/src/Text/Show/Functions.hs @@ -0,0 +1,3 @@ +module Text.Show.Functions (module Exports) where + +import "base" Text.Show.Functions as Exports diff --git a/src/Type/Reflection.hs b/src/Type/Reflection.hs new file mode 100644 --- /dev/null +++ b/src/Type/Reflection.hs @@ -0,0 +1,3 @@ +module Type.Reflection (module Exports) where + +import "base" Type.Reflection as Exports diff --git a/src/Type/Reflection/Unsafe.hs b/src/Type/Reflection/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Type/Reflection/Unsafe.hs @@ -0,0 +1,3 @@ +module Type.Reflection.Unsafe (module Exports) where + +import "base" Type.Reflection.Unsafe as Exports diff --git a/src/Unsafe/Coerce.hs b/src/Unsafe/Coerce.hs new file mode 100644 --- /dev/null +++ b/src/Unsafe/Coerce.hs @@ -0,0 +1,3 @@ +module Unsafe.Coerce (module Exports) where + +import "base" Unsafe.Coerce as Exports