liquidhaskell 0.8.2.3 → 0.8.2.4
raw patch · 8 files changed
+3/−115 lines, 8 files
Files
- liquidhaskell.cabal +2/−2
- src/Language/Haskell/Liquid/Bare/Check.hs +1/−1
- tests/import/lib/Bools.hs +0/−16
- tests/pos/ExactGADT8a.hs +0/−24
- tests/pos/ExactGADT9a.hs +0/−13
- tests/pos/coerce1.hs +0/−17
- tests/pos/maps2.hs +0/−41
- tests/test.hs +0/−1
liquidhaskell.cabal view
@@ -1,5 +1,5 @@ Name: liquidhaskell-Version: 0.8.2.3+Version: 0.8.2.4 Copyright: 2010-17 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego. Synopsis: Liquid Types for Haskell Description: Liquid Types for Haskell.@@ -234,7 +234,7 @@ Language.Haskell.Liquid.Desugar.MatchLit, Language.Haskell.Liquid.Desugar.DsMonad, Language.Haskell.Liquid.Desugar.StaticPtrTable,- Language.Haskell.Liquid.Desugar.TmOracle+ Language.Haskell.Liquid.Desugar.TmOracle, Paths_liquidhaskell, -- FIXME: These shouldn't really be exposed, but the linker complains otherwise...
src/Language/Haskell/Liquid/Bare/Check.hs view
@@ -402,7 +402,7 @@ checkReft :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r))) => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc checkReft _ _ Nothing _ = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.-checkReft env emb (Just t) _ = (\z -> dr $+$ z {- $+$ text "In environment" $+$ nest 4 (pprint env) -}) <$> checkSortedReftFull env r+checkReft env emb (Just t) _ = (\z -> dr $+$ z) <$> checkSortedReftFull env r where r = rTypeSortedReft emb t dr = text "Sort Error in Refinement:" <+> pprint r
− tests/import/lib/Bools.hs
@@ -1,16 +0,0 @@-{-@ LIQUID "--exact-data-con" @-}--module Bools where --{-@ measure amTrue @-}-amTrue :: Bool -> Bool-amTrue True = True -amTrue False = False --{-@ reflect boo @-}-boo :: Bool -> Bool-boo True = True -boo False = False --data Bow = Pow Int-
− tests/pos/ExactGADT8a.hs
@@ -1,24 +0,0 @@-{-@ LIQUID "--exact-data-con" @-}--{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}--module ExactGADT8a where--{- data EntityField typ where- BlobXVal :: EntityField {v:_ | True }- | BlobYVal :: EntityField {v:_ | True }- @-}-data EntityField typ where- BlobXVal :: EntityField Int- BlobYVal :: EntityField Int-- -- TH-GEN- -- data EntityField Blob typ- -- = typ ~ Int => BlobXVal |- -- typ ~ Int => BlobYVal--{-@ reflect evalQBlob @-}-evalQBlob :: EntityField a -> Bool -evalQBlob BlobXVal = True -evalQBlob BlobYVal = False -
− tests/pos/ExactGADT9a.hs
@@ -1,13 +0,0 @@-{-@ LIQUID "--exact-data-con" @-}--{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}--module ExactGADT9a where--import ExactGADT8a--{-@ reflect zoo @-}-zoo :: EntityField a -> Bool -zoo BlobXVal = True -zoo BlobYVal = False -
− tests/pos/coerce1.hs
@@ -1,17 +0,0 @@--{-@ LIQUID "--exact-data-con" @-} -{-# LANGUAGE GADTs #-}--module Foo where --data Foo a where - FInt :: Foo Int - FBool :: Foo Bool--f :: Foo Int -> Int -f z = 10 --bar :: Foo a -> Int -bar z = case z of FInt -> f z- FBool -> 10 -
− tests/pos/maps2.hs
@@ -1,41 +0,0 @@-module Maps where---{-@ prop0 :: x:_ -> y:{_ | y == x} -> TT @-}-prop0 x y = (a == b)- where- a = get x emp - b = get y emp --{-@ prop1 :: x:_ -> y:{_ | y /= x} -> TT @-}-prop1 x y = (z == 10)- where- m1 = put x 10 emp - m2 = put y 20 m1- z = get x m2--{-@ prop2 :: x:_ -> y:{_ | y == x} -> TT @-}-prop2 x y = (z == 20)- where- m1 = put x 10 emp - m2 = put y 20 m1- z = get x m2---------------------------------------------------------------------------data Map k v = M--{-@ embed Map as Map_t @-}-{-@ measure Map_select :: Map k v -> k -> v @-}-{-@ measure Map_store :: Map k v -> k -> v -> Map k v @-}--emp :: Map Int Int-emp = undefined - -{-@ get :: k:k -> m:Map k v -> {v:v | v = Map_select m k} @-}-get :: k -> Map k v -> v-get = undefined --{-@ put :: k:k -> v:v -> m:Map k v -> {n:Map k v | n = Map_store m k v} @-}-put :: k -> v -> Map k v -> Map k v-put = undefined
tests/test.hs view
@@ -151,7 +151,6 @@ , errorTest "tests/errors/HoleCrash1.hs" 2 "Illegal type specification for `ListDemo.t`" , errorTest "tests/errors/HoleCrash2.hs" 2 "Malformed application of type alias `Geq`" , errorTest "tests/errors/HoleCrash3.hs" 2 "Specified type does not refine Haskell type for `ListDemo.countUp`"- , errorTest "tests/errors/HoleCrash3.hs" 2 "Specified type does not refine Haskell type for `ListDemo.countUp`" , errorTest "tests/errors/BadPredApp.hs" 2 "Malformed predicate application" , errorTest "tests/errors/LocalHole.hs" 2 "Illegal type specification for `go`" , errorTest "tests/errors/UnboundAbsRef.hs" 2 "Cannot apply unbound abstract refinement `p`"