lets CI

YoshikiTakashima · Sep 19, 2020 · 5fc099d · 5fc099d
1 parent 26fe1c3
commit 5fc099d
Show file tree

Hide file tree

Showing 28 changed files with 121 additions and 128 deletions.
diff --git a/include/Control/Exception.spec b/include/Control/Exception.spec
@@ -1,5 +1,5 @@
 module spec Control.Exception where
 
-// Useless as compiled into GHC primitive, which is ignored
+//  Useless as compiled into GHC primitive, which is ignored
 assume assert :: {v:Bool | v } -> a -> a
 
diff --git a/include/Data/Bits.spec b/include/Data/Bits.spec
@@ -1,6 +1,6 @@
 module spec Data.Bits where
 
-// TODO: cannot use this because `Bits` is not a `Num`
-// Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
-//                  -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
+//  TODO: cannot use this because `Bits` is not a `Num`
+//  Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
+//                   -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
 
diff --git a/include/Data/ByteString/Char8.spec b/include/Data/ByteString/Char8.spec
@@ -394,9 +394,9 @@ assume hGetNonBlocking
     -> n : { n : Int | 0 <= n }
     -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }
 
-// assume partition
-    // :: (Char -> GHC.Types.Bool)
-    // -> i : Data.ByteString.ByteString
-    // -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
-       // , { r : Data.ByteString.ByteString | bslen r <= bslen i }
-       // )
+//  assume partition
+    //  :: (Char -> GHC.Types.Bool)
+    //  -> i : Data.ByteString.ByteString
+    //  -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       //  , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       //  )
diff --git a/include/Data/Int.spec b/include/Data/Int.spec
@@ -5,4 +5,4 @@ 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}
+//  type Nat64 = {v:Data.Int.Int64 | v >= 0}
diff --git a/include/Data/Set.spec b/include/Data/Set.spec
@@ -2,38 +2,38 @@ module spec Data.Set where
 
 embed Data.Set.Internal.Set as Set_Set
 
-// ----------------------------------------------------------------------------------------------
-// -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------
-// ----------------------------------------------------------------------------------------------
+//  ----------------------------------------------------------------------------------------------
+//  -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------
+//  ----------------------------------------------------------------------------------------------
 
 
-// union
+//  union
 measure Set_cup  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
 
-// intersection
+//  intersection
 measure Set_cap  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
 
-// difference
+//  difference
 measure Set_dif   :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a)
 
-// singleton
+//  singleton
 measure Set_sng   :: a -> (Data.Set.Internal.Set a)
 
-// emptiness test
+//  emptiness test
 measure Set_emp   :: (Data.Set.Internal.Set a) -> GHC.Types.Bool
 
-// empty set
+//  empty set
 measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Internal.Set a)
 
-// membership test
+//  membership test
 measure Set_mem  :: a -> (Data.Set.Internal.Set a) -> GHC.Types.Bool
 
-// inclusion test
+//  inclusion test
 measure Set_sub  :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> GHC.Types.Bool
 
-// ---------------------------------------------------------------------------------------------
-// -- | Refined Types for Data.Set Operations --------------------------------------------------
-// ---------------------------------------------------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
+//  -- | Refined Types for Data.Set Operations --------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
 
 isSubsetOf    :: (GHC.Classes.Ord a) => x:(Data.Set.Internal.Set a) -> y:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_sub x y}
 member        :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_mem x xs}
@@ -50,9 +50,9 @@ difference    :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.S
 
 fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Internal.Set a | v = listElts xs}
 
-// ---------------------------------------------------------------------------------------------
-// -- | The set of elements in a list ----------------------------------------------------------
-// ---------------------------------------------------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
+//  -- | The set of elements in a list ----------------------------------------------------------
+//  ---------------------------------------------------------------------------------------------
 
 measure listElts :: [a] -> (Data.Set.Internal.Set a)
 listElts([])   = {v | (Set_emp v)}

diff --git a/include/Foreign/C/String.spec b/include/Foreign/C/String.spec
@@ -5,7 +5,7 @@ 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 :: Foreign.C.String.CStringLen -> 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/include/Foreign/ForeignPtr.spec b/include/Foreign/ForeignPtr.spec
@@ -12,5 +12,5 @@ Foreign.Concurrent.newForeignPtr  :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types
 Foreign.ForeignPtr.newForeignPtr ::  _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))
 
 
-// this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
-// Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
+//  this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
+//  Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
diff --git a/include/Foreign/Storable.spec b/include/Foreign/Storable.spec
@@ -2,8 +2,8 @@ module spec Foreign.Storable where
 
 import Foreign.Ptr
 
-// DON'T do this, we can't import HS files from SPEC files
-// import Language.Haskell.Liquid.Foreign
+//  DON'T do this, we can't import HS files from SPEC files
+//  import Language.Haskell.Liquid.Foreign
 
 predicate PValid P N         = ((0 <= N) && (N < (plen P)))   
 

diff --git a/include/GHC/Base.spec b/include/GHC/Base.spec
@@ -14,9 +14,9 @@ instance measure len :: forall a. [a] -> GHC.Types.Int
   len []     = 0
   len (y:ys) = 1 + len ys
 
-// measure null :: [a] -> Bool
-// null []     = true 
-// null (y:ys) = false
+//  measure null :: [a] -> Bool
+//  null []     = true 
+//  null (y:ys) = false
 
 measure fst :: (a, b) -> a
   fst (a, b) = a
@@ -42,19 +42,19 @@ map       :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}
 ($)       :: (a -> b) -> a -> b
 id        :: x:a -> {v:a | v = x}
 
-// data variance Text.ParserCombinators.ReadPrec.ReadPrec contravariant
+//  data variance Text.ParserCombinators.ReadPrec.ReadPrec contravariant
 
-//qualif NonNull(v: [a])        : (? (nonnull v ))
-//qualif Null(v: [a])           : (~ (? (nonnull v )))
-//qualif EqNull(v:Bool, ~A: [a]): (v <=> (? (nonnull([~A]))))
+// qualif NonNull(v: [a])        : (? (nonnull v ))
+// qualif Null(v: [a])           : (~ (? (nonnull v )))
+// qualif EqNull(v:Bool, ~A: [a]): (v <=> (? (nonnull([~A]))))
 
-// qualif IsEmp(v:GHC.Types.Bool, ~A: [a]) : ((v) <=> len([~A]) [ > ;  = ] 0)
-// qualif ListZ(v: [a])          : len v  [ = ; >= ; > ] 0 
-// qualif CmpLen(v:[a], ~A:[b])  : len v  [= ; >=; >; <=; <] len([~A]) 
-// qualif EqLen(v:int, ~A: [a])  : v = len([~A]) 
-// qualif LenEq(v:[a], ~A: int)  : ~A = len v  
-// qualif LenAcc(v:int, ~A:[a], ~B: int): v = len([~A]) + ~B
-// qualif LenDiff(v:[a], ~A:int): len v  = (~A [ +; - ] 1)
+//  qualif IsEmp(v:GHC.Types.Bool, ~A: [a]) : ((v) <=> len([~A]) [ > ;  = ] 0)
+//  qualif ListZ(v: [a])          : len v  [ = ; >= ; > ] 0 
+//  qualif CmpLen(v:[a], ~A:[b])  : len v  [= ; >=; >; <=; <] len([~A]) 
+//  qualif EqLen(v:int, ~A: [a])  : v = len([~A]) 
+//  qualif LenEq(v:[a], ~A: int)  : ~A = len v  
+//  qualif LenAcc(v:int, ~A:[a], ~B: int): v = len([~A]) + ~B
+//  qualif LenDiff(v:[a], ~A:int): len v  = (~A [ +; - ] 1)
 
 qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0))
 qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0))

diff --git a/include/GHC/Exts.spec b/include/GHC/Exts.spec
@@ -1,10 +1,10 @@
 module spec GHC.Exts where
 
-// embed GHC.Exts.Int#     as int
-// embed GHC.Exts.Word#    as int
-// embed GHC.Exts.Addr#    as Str
-// embed GHC.Exts.Double#  as real
-// embed GHC.Exts.Char#    as Char
+//  embed GHC.Exts.Int#     as int
+//  embed GHC.Exts.Word#    as int
+//  embed GHC.Exts.Addr#    as Str
+//  embed GHC.Exts.Double#  as real
+//  embed GHC.Exts.Char#    as Char
 
 
 
diff --git a/include/GHC/Real.spec b/include/GHC/Real.spec
@@ -33,5 +33,5 @@ class (GHC.Real.Real a, GHC.Enum.Enum a) => GHC.Real.Integral a where
                                                 )
   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) }
+//  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/include/GHC/Types.spec b/include/GHC/Types.spec
@@ -7,15 +7,15 @@ embed GHC.Types.Double# as real
 embed GHC.Types.Float# as real
 embed GHC.Types.Word    as int 
 
-// TODO: Drop prefix below
-// GHC.Types.EQ :: {v:GHC.Types.Ordering | v = (cmp v) }
-// GHC.Types.LT :: {v:GHC.Types.Ordering | v = (cmp v) }
-// GHC.Types.GT :: {v:GHC.Types.Ordering | v = (cmp v) }
-
-// measure cmp :: GHC.Types.Ordering -> GHC.Types.Ordering
-// cmp GHC.Types.EQ = { v | v = GHC.Types.EQ }
-// cmp GHC.Types.LT = { v | v = GHC.Types.LT }
-// cmp GHC.Types.GT = { v | v = GHC.Types.GT }
+//  TODO: Drop prefix below
+//  GHC.Types.EQ :: {v:GHC.Types.Ordering | v = (cmp v) }
+//  GHC.Types.LT :: {v:GHC.Types.Ordering | v = (cmp v) }
+//  GHC.Types.GT :: {v:GHC.Types.Ordering | v = (cmp v) }
+
+//  measure cmp :: GHC.Types.Ordering -> GHC.Types.Ordering
+//  cmp GHC.Types.EQ = { v | v = GHC.Types.EQ }
+//  cmp GHC.Types.LT = { v | v = GHC.Types.LT }
+//  cmp GHC.Types.GT = { v | v = GHC.Types.GT }
 
 
 GHC.Types.True  :: {v:GHC.Types.Bool | v     }

diff --git a/include/Prelude.spec b/include/Prelude.spec
@@ -14,7 +14,7 @@ import GHC.Exts
 import GHC.Err 
 
 
-// GHC.Types.D# :: x:_ -> {v:_ | v = x}
+//  GHC.Types.D# :: x:_ -> {v:_ | v = x}
 
 GHC.Err.error :: {v:_ | false} -> a 
 
@@ -47,7 +47,7 @@ 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!
+// BOT: Do not delete EVER!
 
 qualif Bot(v:@(0))    : (0 = 1)
 qualif Bot(v:obj)     : (0 = 1)
@@ -73,16 +73,16 @@ 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])
+//  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
 qualif Papp(v:a, p:Pred a) : (papp1 p v)
 
-// REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
+//  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
 qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x)
 
-// REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
+//  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
 qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y)
 
-// qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
-// REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
+//  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
+//  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
 
-// REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
+//  REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
diff --git a/include/Real.spec b/include/Real.spec
@@ -6,4 +6,4 @@ assume GHC.Num.* :: (GHC.Num.Num a) => x:a -> y:a -> {v:a | v = x * y}
 
 
 
-// GHC.Real./       :: forall a. (GHC.Real.Fractional a) => x:a -> y:{v:a | v != 0.0} -> {v: a | v = (x / y) }
+//  GHC.Real./       :: forall a. (GHC.Real.Fractional a) => x:a -> y:{v:a | v != 0.0} -> {v: a | v = (x / y) }
diff --git a/liquid-base/src/Control/Exception.spec b/liquid-base/src/Control/Exception.spec
@@ -1,5 +1,5 @@
 module spec Control.Exception where
 
-// Useless as compiled into GHC primitive, which is ignored
+//  Useless as compiled into GHC primitive, which is ignored
 assume assert :: {v:Bool | v } -> a -> a
 
diff --git a/liquid-base/src/Data/Bits.spec b/liquid-base/src/Data/Bits.spec
@@ -1,6 +1,6 @@
 module spec Data.Bits where
 
-// TODO: cannot use this because `Bits` is not a `Num`
-// Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
-//                  -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
+//  TODO: cannot use this because `Bits` is not a `Num`
+//  Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat 
+//                   -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) }
 
diff --git a/liquid-base/src/Data/Int.spec b/liquid-base/src/Data/Int.spec
@@ -5,4 +5,4 @@ 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}
+//  type Nat64 = {v:Data.Int.Int64 | v >= 0}
diff --git a/liquid-base/src/Foreign/C/String.spec b/liquid-base/src/Foreign/C/String.spec
@@ -5,8 +5,8 @@ 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 :: Foreign.C.String.CStringLen -> GHC.Types.Int
 measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int
 
-//measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int 
-//cStringLen (c, n) = n
+// measure cStringLen :: ((GHC.Ptr.Ptr Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int 
+// cStringLen (c, n) = n
diff --git a/liquid-base/src/Foreign/ForeignPtr.spec b/liquid-base/src/Foreign/ForeignPtr.spec
@@ -12,5 +12,5 @@ Foreign.Concurrent.newForeignPtr  :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types
 Foreign.ForeignPtr.newForeignPtr ::  _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p)))
 
 
-// this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
-// Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
+//  this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n`
+//  Foreign.ForeignPtr.Imp.mallocForeignPtrArray :: (Foreign.Storable.Storable a) => n:Nat -> IO (ForeignPtrN a n)
diff --git a/liquid-base/src/GHC/List.spec b/liquid-base/src/GHC/List.spec
@@ -46,7 +46,7 @@ break :: (a -> GHC.Types.Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x
 
 reverse      :: xs:[a] -> {v: [a] | len(v) = len(xs)}
 
-// Copy-pasted from len.hquals
+//  Copy-pasted from len.hquals
 qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))
 qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))
 

diff --git a/liquid-base/src/GHC/Real.spec b/liquid-base/src/GHC/Real.spec
@@ -35,5 +35,5 @@ class (GHC.Real.Real a, GHC.Enum.Enum a) => GHC.Real.Integral a where
                                                 )
   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) }
+//  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/liquid-base/src/Prelude.spec b/liquid-base/src/Prelude.spec
@@ -14,11 +14,11 @@ import GHC.Exts
 import GHC.Err 
 
 
-// GHC.Types.D# :: x:_ -> {v:_ | v = x}
+//  GHC.Types.D# :: x:_ -> {v:_ | v = x}
 
 GHC.Err.error :: {v:_ | false} -> a 
 
-//assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) }
+// assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) }
 
 embed Integer           as int
 
@@ -27,7 +27,7 @@ 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!
+// BOT: Do not delete EVER!
 
 qualif Bot(v:@(0))    : (0 = 1)
 qualif Bot(v:obj)     : (0 = 1)
@@ -53,16 +53,16 @@ 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])
+//  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
 qualif Papp(v:a, p:Pred a) : (papp1 p v)
 
-// REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
+//  REBARE constant papp2 : func(4, [Pred @(0) @(1); @(2); @(3); bool])
 qualif Papp2(v:a, x:b, p:Pred a b) : (papp2 p v x)
 
-// REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
+//  REBARE constant papp3 : func(6, [Pred @(0) @(1) @(2); @(3); @(4); @(5); bool])
 qualif Papp3(v:a, x:b, y:c, p:Pred a b c) : (papp3 p v x y)
 
-// qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
-// REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
+//  qualif Papp4(v:a,x:b, y:c, z:d, p:Pred a b c d) : papp4(p, v, x, y, z)
+//  REBARE constant papp4 : func(8, [Pred @(0) @(1) @(2) @(6); @(3); @(4); @(5); @(7); bool])
 
-// REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
+//  REBARE constant runFun : func(2, [Arrow @(0) @(1); @(0); @(1)])
diff --git a/liquid-bytestring/src/Data/ByteString/Char8.spec b/liquid-bytestring/src/Data/ByteString/Char8.spec
@@ -394,9 +394,9 @@ assume hGetNonBlocking
     -> n : { n : Int | 0 <= n }
     -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }
 
-// assume partition
-    // :: (Char -> GHC.Types.Bool)
-    // -> i : Data.ByteString.ByteString
-    // -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
-       // , { r : Data.ByteString.ByteString | bslen r <= bslen i }
-       // )
+//  assume partition
+    //  :: (Char -> GHC.Types.Bool)
+    //  -> i : Data.ByteString.ByteString
+    //  -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       //  , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       //  )
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@ assume GHC.Num.* :: (GHC.Num.Num a) => x:a -> y:a -> {v:a \| v = x * y}



		// GHC.Real./ :: forall a. (GHC.Real.Fractional a) => x:a -> y:{v:a \| v != 0.0} -> {v: a \| v = (x / y) }
		// GHC.Real./ :: forall a. (GHC.Real.Fractional a) => x:a -> y:{v:a \| v != 0.0} -> {v: a \| v = (x / y) }