liquid-ghc-prim (empty) → 0.6.1
raw patch · 15 files changed
+192/−0 lines, 15 filesdep +ghc-primdep +liquidhaskellbuild-type:Customsetup-changed
Dependencies added: ghc-prim, liquidhaskell
Files
- LICENSE +30/−0
- Setup.hs +6/−0
- liquid-ghc-prim.cabal +46/−0
- src/GHC/CString.hs +5/−0
- src/GHC/CString.spec +9/−0
- src/GHC/Classes.hs +4/−0
- src/GHC/Classes.spec +29/−0
- src/GHC/Debug.hs +3/−0
- src/GHC/IntWord64.hs +3/−0
- src/GHC/Magic.hs +3/−0
- src/GHC/Prim/Ext.hs +3/−0
- src/GHC/PrimopWrappers.hs +3/−0
- src/GHC/Tuple.hs +3/−0
- src/GHC/Types.hs +10/−0
- src/GHC/Types.spec +35/−0
+ 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-ghc-prim.cabal view
@@ -0,0 +1,46 @@+cabal-version: 1.24+name: liquid-ghc-prim+version: 0.6.1+synopsis: Drop-in ghc-prim replacement for LiquidHaskell+description: Drop-in ghc-prim 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/GHC/*.spec+++custom-setup+ setup-depends: Cabal, base, liquidhaskell++library+ exposed-modules:+ -- We can't really export 'GHC.Prim' or this won't build on Windows,+ -- unfortunately. The issue is that 'GHC.Prim' is a special snowflake,+ -- treated specially by the GHC pipeline. In particular, GHC doesn't+ -- generate a '.hi' file for it, and this causes Windows' builds to choke.+ -- GHC.Prim+ GHC.CString+ GHC.Classes+ GHC.Debug+ GHC.IntWord64+ GHC.Magic+ GHC.Prim.Ext+ GHC.PrimopWrappers+ GHC.Tuple+ GHC.Types++ hs-source-dirs: src+ build-depends: ghc-prim == 0.6.1+ , liquidhaskell >= 0.8.10.1+ default-language: Haskell2010+ default-extensions: PackageImports+ NoImplicitPrelude+ MagicHash+ if impl(ghc >= 8.10)+ ghc-options: -fplugin=LiquidHaskell
+ src/GHC/CString.hs view
@@ -0,0 +1,5 @@+module GHC.CString (module Exports) where++import "this" GHC.Types++import "ghc-prim" GHC.CString as Exports
+ src/GHC/CString.spec view
@@ -0,0 +1,9 @@+module spec GHC.CString where++import GHC.Types++measure strLen :: Addr# -> GHC.Types.Int++GHC.CString.unpackCString#+ :: x:GHC.Prim.Addr#+ -> {v:[Char] | v ~~ x && len v == strLen x}
+ src/GHC/Classes.hs view
@@ -0,0 +1,4 @@+module GHC.Classes (module Exports) where++import GHC.Types+import "ghc-prim" GHC.Classes as Exports
+ src/GHC/Classes.spec view
@@ -0,0 +1,29 @@+module spec GHC.Classes where++import GHC.Types++not :: x:GHC.Types.Bool -> {v:GHC.Types.Bool | ((v) <=> ~(x))}+(&&) :: x:GHC.Types.Bool -> y:GHC.Types.Bool+ -> {v:GHC.Types.Bool | ((v) <=> ((x) && (y)))}+(||) :: x:GHC.Types.Bool -> y:GHC.Types.Bool+ -> {v:GHC.Types.Bool | ((v) <=> ((x) || (y)))}+(==) :: (GHC.Classes.Eq a) => x:a -> y:a+ -> {v:GHC.Types.Bool | ((v) <=> x = y)}+(/=) :: (GHC.Classes.Eq a) => x:a -> y:a+ -> {v:GHC.Types.Bool | ((v) <=> x != y)}+(>) :: (GHC.Classes.Ord a) => x:a -> y:a+ -> {v:GHC.Types.Bool | ((v) <=> x > y)}+(>=) :: (GHC.Classes.Ord a) => x:a -> y:a+ -> {v:GHC.Types.Bool | ((v) <=> x >= y)}+(<) :: (GHC.Classes.Ord a) => x:a -> y:a+ -> {v:GHC.Types.Bool | ((v) <=> x < y)}+(<=) :: (GHC.Classes.Ord a) => x:a -> y:a+ -> {v:GHC.Types.Bool | ((v) <=> x <= y)}++compare :: (GHC.Classes.Ord a) => x:a -> y:a+ -> {v:GHC.Types.Ordering | (((v = GHC.Types.EQ) <=> (x = y)) &&+ ((v = GHC.Types.LT) <=> (x < y)) &&+ ((v = GHC.Types.GT) <=> (x > y))) }++max :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) }+min :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) }
+ src/GHC/Debug.hs view
@@ -0,0 +1,3 @@+module GHC.Debug (module Exports) where++import "ghc-prim" GHC.Debug as Exports
+ src/GHC/IntWord64.hs view
@@ -0,0 +1,3 @@+module GHC.IntWord64 (module Exports) where++import "ghc-prim" GHC.IntWord64 as Exports
+ src/GHC/Magic.hs view
@@ -0,0 +1,3 @@+module GHC.Magic (module Exports) where++import "ghc-prim" GHC.Magic as Exports
+ src/GHC/Prim/Ext.hs view
@@ -0,0 +1,3 @@+module GHC.Prim.Ext (module Exports) where++import "ghc-prim" GHC.Prim.Ext as Exports
+ src/GHC/PrimopWrappers.hs view
@@ -0,0 +1,3 @@+module GHC.PrimopWrappers (module Exports) where++import "ghc-prim" GHC.PrimopWrappers as Exports
+ src/GHC/Tuple.hs view
@@ -0,0 +1,3 @@+module GHC.Tuple (module Exports) where++import "ghc-prim" GHC.Tuple as Exports
+ src/GHC/Types.hs view
@@ -0,0 +1,10 @@+module GHC.Types (module Exports) where++{-@ embed GHC.Prim.Int# as int @-}+{-@ embed GHC.Prim.Addr# as Str @-}+{-@ embed GHC.Prim.Char# as Char @-}+{-@ embed GHC.Prim.Double# as real @-}+{-@ embed GHC.Prim.Float# as real @-}+{-@ embed GHC.Prim.Word# as int @-}++import "ghc-prim" GHC.Types as Exports
+ src/GHC/Types.spec view
@@ -0,0 +1,35 @@+module spec GHC.Types where++// Boxed types+embed GHC.Types.Double as real+embed GHC.Types.Float as real+embed GHC.Types.Word as int+embed GHC.Types.Int as int+embed GHC.Types.Bool as bool+embed GHC.Types.Char as Char++embed GHC.Integer.Type.Integer as int++GHC.Types.True :: {v:GHC.Types.Bool | v }+GHC.Types.False :: {v:GHC.Types.Bool | (~ v) }+GHC.Types.isTrue# :: n:_ -> {v:GHC.Types.Bool | (n = 1 <=> v)}++GHC.Types.D# :: x:GHC.Prim.Double# -> {v: GHC.Types.Double | v = (x :: real) }+GHC.Types.F# :: x:GHC.Prim.Float# -> {v: GHC.Types.Float | v = (x :: real) }+GHC.Types.I# :: x:GHC.Prim.Int# -> {v: GHC.Types.Int | v = (x :: int) }+GHC.Types.C# :: x:GHC.Prim.Char# -> {v: GHC.Types.Char | v = (x :: Char) }+GHC.Types.W# :: w:_ -> {v:GHC.Types.Word | v == w }++measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int++type GeInt N = {v: GHC.Types.Int | v >= N }+type LeInt N = {v: GHC.Types.Int | v <= N }+type Nat = {v: GHC.Types.Int | v >= 0 }+type Even = {v: GHC.Types.Int | (v mod 2) = 0 }+type Odd = {v: GHC.Types.Int | (v mod 2) = 1 }+type BNat N = {v: Nat | v <= N }+type TT = {v: GHC.Types.Bool | v}+type FF = {v: GHC.Types.Bool | not v}+type String = [GHC.Types.Char]++class measure len :: forall f a. f a -> GHC.Types.Int