Skip to content

WIP: Ghc 8.4 #1330

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed

WIP: Ghc 8.4 #1330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0099c8b
Allow aeson-1.3
phadej Jun 9, 2018
d281dbc
all up to Liquid.Model
phadej Jun 9, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,12 @@

packages: .
./liquid-fixpoint
./text-format
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

haskell/text-format#21 local.

Let's see what Hackage Trustees can do with that.


package liquid-fixpoint
flags: devel

package liquidhaskell
flags: devel

with-compiler: ghc-8.4.3
2 changes: 1 addition & 1 deletion liquid-fixpoint
Open in desktop
Submodule liquid-fixpoint updated 23 files
+5 −3 liquid-fixpoint.cabal
+6 −3 src/Language/Fixpoint/Graph/Deps.hs
+8 −5 src/Language/Fixpoint/Graph/Partition.hs
+3 −3 src/Language/Fixpoint/Graph/Types.hs
+7 −1 src/Language/Fixpoint/Misc.hs
+0 −1 src/Language/Fixpoint/Smt/Interface.hs
+0 −1 src/Language/Fixpoint/Smt/Serialize.hs
+0 −1 src/Language/Fixpoint/Smt/Theories.hs
+6 −4 src/Language/Fixpoint/Solver/Solution.hs
+6 −3 src/Language/Fixpoint/SortCheck.hs
+49 −35 src/Language/Fixpoint/Types/Constraints.hs
+21 −10 src/Language/Fixpoint/Types/Environments.hs
+10 −7 src/Language/Fixpoint/Types/Errors.hs
+3 −0 src/Language/Fixpoint/Types/Graduals.hs
+15 −13 src/Language/Fixpoint/Types/PrettyPrint.hs
+7 −7 src/Language/Fixpoint/Types/Refinements.hs
+12 −9 src/Language/Fixpoint/Types/Solutions.hs
+13 −7 src/Language/Fixpoint/Types/Sorts.hs
+20 −8 src/Language/Fixpoint/Types/Substitutions.hs
+12 −9 src/Language/Fixpoint/Types/Theories.hs
+5 −2 src/Language/Fixpoint/Types/Visitor.hs
+13 −0 src/Text/PrettyPrint/HughesPJ/Compat.hs
+2 −0 stack.yaml
14 changes: 7 additions & 7 deletions liquidhaskell.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ Flag deterministic-profiling

Executable liquid
default-language: Haskell98
Build-Depends: base >=4.8.1.0 && <5
Build-Depends: base >=4.9.1.0 && <5
, ghc
, ghc-boot
, cmdargs
Expand Down Expand Up @@ -108,9 +108,9 @@ Executable liquid

Library
Default-Language: Haskell98
Build-Depends: base >=4.8.1.0 && <5
, ghc == 8.2.2
, ghc-boot == 8.2.2
Build-Depends: base >=4.11.1.0 && <5
, ghc == 8.4.3
, ghc-boot == 8.4.3
, template-haskell >= 2.9
, time >= 1.4
, array >= 0.5
Expand All @@ -134,9 +134,9 @@ Library
, vector >= 0.10
, hashable >= 1.2
, unordered-containers >= 0.2
, liquid-fixpoint >= 0.7.0.7
, liquid-fixpoint >= 0.7.0.5
, located-base
, aeson >= 1.2 && < 1.3
, aeson >= 1.2 && < 1.4
, bytestring >= 0.10
, fingertree >= 0.1
, Cabal >= 1.18
Expand Down Expand Up @@ -286,7 +286,7 @@ Library
if flag(include)
hs-source-dirs: devel
if flag(devel)
ghc-options: -Werror
-- ghc-options: -Werror
if flag(deterministic-profiling)
cpp-options: -DDETERMINISTIC_PROFILING
Default-Extensions: PatternGuards
Expand Down
18 changes: 9 additions & 9 deletions src/Language/Haskell/Liquid/Constraint/Generate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ import Name hiding (varName)
import FastString (fastStringToByteString)
import Unify
import UniqSet (mkUniqSet)
import Text.PrettyPrint.HughesPJ hiding (first)
import Text.PrettyPrint.HughesPJ.Compat
import Control.Monad.State
import Data.Maybe (fromMaybe, catMaybes, isJust)
import qualified Data.HashMap.Strict as M
Expand Down Expand Up @@ -75,7 +75,7 @@ import Language.Haskell.Liquid.Types.Literals
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Constraint.Constraint
import Language.Haskell.Liquid.Transforms.Rec
import Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult)
import Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult)
import Language.Haskell.Liquid.Bare.Misc (makeDataConChecker)

--------------------------------------------------------------------------------
Expand Down Expand Up @@ -170,7 +170,7 @@ checkIndex (x, vs, t, index)
where
loc = getSrcSpan x
ts = ty_args $ toRTypeRep $ unOCons $ unTemplate t
msg1 = ErrTermin loc [xd] ("No decreasing" <+> F.pprint index <> "-th argument on" <+> xd <+> "with" <+> (F.pprint vs))
msg1 = ErrTermin loc [xd] ("No decreasing" <+> F.pprint index <-> "-th argument on" <+> xd <+> "with" <+> (F.pprint vs))
msg2 = ErrTermin loc [xd] "No decreasing parameter"
xd = F.pprint x

Expand Down Expand Up @@ -494,7 +494,7 @@ consBind isRec γ (x, e, Internal spect)
-- have to add the wf constraint here for HOLEs so we have the proper env
addW $ WfC γπ $ fmap killSubst spect
addIdA x (defAnn isRec spect)
return $ F.tracepp "consBind 2" $ Internal spect
return $ F.tracepp "consBind 2" $ Internal spect
where
explanation = "Cannot give singleton type to the function definition."

Expand Down Expand Up @@ -543,7 +543,7 @@ extender γ (x, Assumed t)
extender γ _
= return γ

data Template a
data Template a
= Asserted a
| Assumed a
| Internal a
Expand All @@ -552,11 +552,11 @@ data Template a

deriving instance (Show a) => (Show (Template a))

instance PPrint a => PPrint (Template a) where
instance PPrint a => PPrint (Template a) where
pprintTidy k (Asserted t) = "Asserted" <+> pprintTidy k t
pprintTidy k (Assumed t) = "Assumed" <+> pprintTidy k t
pprintTidy k (Internal t) = "Internal" <+> pprintTidy k t
pprintTidy _ Unknown = "Unknown"
pprintTidy _ Unknown = "Unknown"

unTemplate :: Template t -> t
unTemplate (Asserted t) = t
Expand Down Expand Up @@ -1171,9 +1171,9 @@ projectTypes (Just is) ts = mapM (projT is) (zip [0..] ts)
altReft :: CGEnv -> [AltCon] -> AltCon -> F.Reft
altReft _ _ (LitAlt l) = literalFReft l
altReft γ acs DEFAULT = mconcat ([notLiteralReft l | LitAlt l <- acs] ++ [notDataConReft d | DataAlt d <- acs])
where
where
notLiteralReft = maybe mempty F.notExprReft . snd . literalConst (emb γ)
notDataConReft d | exactDC (getConfig γ)
notDataConReft d | exactDC (getConfig γ)
= F.Reft (F.vv_, F.PNot (F.EApp (F.EVar $ makeDataConChecker d) (F.EVar F.vv_)))
| otherwise = mempty
altReft _ _ _ = panic Nothing "Constraint : altReft"
Expand Down
7 changes: 5 additions & 2 deletions src/Language/Haskell/Liquid/Constraint/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ import SrcLoc
import Unify (tcUnifyTy)
import qualified TyCon as TC
import qualified DataCon as DC
import Text.PrettyPrint.HughesPJ hiding (first)
import Text.PrettyPrint.HughesPJ.Compat
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.List as L
Expand Down Expand Up @@ -117,7 +117,10 @@ data LConstraint = LC [[(F.Symbol, SpecType)]]

instance Monoid LConstraint where
mempty = LC []
mappend (LC cs1) (LC cs2) = LC (cs1 ++ cs2)
mappend = (<>)

instance Semigroup LConstraint where
LC cs1 <> LC cs2 = LC (cs1 ++ cs2)

instance PPrint CGEnv where
pprintTidy k = pprintTidy k . renv
Expand Down
Loading