[Git][ghc/ghc][wip/ttg-booleanformula] moved as much as I can towards the correct places...
Hassan Al-Awwadi (@hassan.awwadi)
gitlab at gitlab.haskell.org
Wed Sep 18 16:13:54 UTC 2024
Hassan Al-Awwadi pushed to branch wip/ttg-booleanformula at Glasgow Haskell Compiler / GHC
Commits:
2ad76802 by Hassan Al-Awwadi at 2024-09-18T18:13:19+02:00
moved as much as I can towards the correct places...
- - - - -
3 changed files:
- compiler/GHC/Data/BooleanFormula.hs
- compiler/GHC/Hs/Decls.hs
- compiler/Language/Haskell/Syntax/BooleanFormula.hs
Changes:
=====================================
compiler/GHC/Data/BooleanFormula.hs
=====================================
@@ -1,10 +1,5 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE TypeFamilies #-}
--------------------------------------------------------------------------------
-- | Boolean formulas without quantifiers and without negation.
@@ -21,31 +16,39 @@ module GHC.Data.BooleanFormula (
pprBooleanFormula, pprBooleanFormulaNice
) where
-import Language.Haskell.Syntax.BooleanFormula
-
-import GHC.Prelude hiding ( init, last )
-
import Data.List ( intersperse )
import Data.List.NonEmpty ( NonEmpty (..), init, last )
-import Data.Data
-import GHC.Utils.Outputable
-import GHC.Parser.Annotation ( SrcSpanAnnL )
+import GHC.Prelude hiding ( init, last )
import GHC.Types.Unique
import GHC.Types.Unique.Set
-import Language.Haskell.Syntax.Extension (Anno)
import GHC.Types.SrcLoc (GenLocated(L), unLoc)
+import GHC.Utils.Outputable
+import GHC.Parser.Annotation ( SrcSpanAnnL )
import GHC.Hs.Extension (GhcPass)
+import Language.Haskell.Syntax.Extension (Anno)
+import Language.Haskell.Syntax.BooleanFormula
+
+
+
----------------------------------------------------------------------
-- Boolean formula type and smart constructors
----------------------------------------------------------------------
+-- Actually should this be moved to GHC.Hs.Decls?
+-- That's where most of the anno instances are, anyway.
+-- But I don't know how strictly that is just an implementation detail
+-- I'm allowed to ignore?
type instance Anno (BooleanFormula (GhcPass p) a) = SrcSpanAnnL
-deriving instance (Eq a, Eq (LBooleanFormula p a)) => Eq (BooleanFormula p a)
-deriving instance (Data a, Data p, Data (LBooleanFormula p a)) => Data (BooleanFormula p a)
-
+-- In a perfect world I could do something like
+-- instance (Functor (LBooleanFormula p) => Functor (BooleanFormula p)).
+-- But type synonyms need to be fully applied, and I could not figure out the
+-- correct way to hack my way around wrapping and unwrapping and ~ to make it work
+-- less cleanly. My last hope for using mapXRec also doe not work, because it has
+-- the Anno p a ~ Anno p b constraint which seems impossible to get in the class
+-- constraint header.
instance Functor (BooleanFormula (GhcPass p)) where
fmap :: (a -> b) -> BooleanFormula (GhcPass p) a -> BooleanFormula (GhcPass p) b
fmap f (Var a ) = Var (f a)
@@ -53,13 +56,7 @@ instance Functor (BooleanFormula (GhcPass p)) where
fmap f (Or bfs) = Or $ fmap (fmap (fmap f)) bfs
fmap f (Parens bf ) = Parens $ fmap (fmap f) bf
-instance Foldable (BooleanFormula (GhcPass p)) where
- foldMap :: Monoid m => (a -> m) -> BooleanFormula (GhcPass p) a -> m
- foldMap f (Var a ) = f a
- foldMap f (And bfs) = foldMap (foldMap f . unLoc) bfs
- foldMap f (Or bfs) = foldMap (foldMap f . unLoc) bfs
- foldMap f (Parens bf ) = foldMap f $ unLoc bf
-
+-- See comment above Functor instance.
instance Traversable (BooleanFormula (GhcPass p)) where
sequenceA :: Applicative f => BooleanFormula (GhcPass p) (f a) -> f (BooleanFormula (GhcPass p) a)
sequenceA (Var a) = Var <$> a
@@ -87,7 +84,6 @@ lbfSwitchPass :: forall p p' l a
lbfSwitchPass (L loc bf) = L loc (bfSwitchPass bf)
-
{-
Note [Simplification of BooleanFormulas]
~~~~~~~~~~~~~~~~~~~~~~
@@ -134,7 +130,7 @@ isTrue :: BooleanFormula (GhcPass p) a -> Bool
isTrue (And []) = True
isTrue _ = False
-eval :: forall p a. (a -> Bool) -> BooleanFormula (GhcPass p) a -> Bool
+eval :: (a -> Bool) -> BooleanFormula (GhcPass p) a -> Bool
eval f (Var x) = f x
eval f (And xs) = all (eval f . unLoc) xs
eval f (Or xs) = any (eval f . unLoc) xs
@@ -142,7 +138,7 @@ eval f (Parens x) = eval f (unLoc x)
-- Simplify a boolean formula.
-- The argument function should give the truth of the atoms, or Nothing if undecided.
-simplify :: forall p a. Eq a => (a -> Maybe Bool) -> BooleanFormula (GhcPass p) a -> BooleanFormula (GhcPass p) a
+simplify :: Eq a => (a -> Maybe Bool) -> BooleanFormula (GhcPass p) a -> BooleanFormula (GhcPass p) a
simplify f (Var a) = case f a of
Nothing -> Var a
Just b -> mkBool b
@@ -153,7 +149,7 @@ simplify f (Parens x) = simplify f (unLoc x)
-- Test if a boolean formula is satisfied when the given values are assigned to the atoms
-- if it is, returns Nothing
-- if it is not, return (Just remainder)
-isUnsatisfied :: forall p a. Eq a => (a -> Bool) -> BooleanFormula (GhcPass p) a -> Maybe (BooleanFormula (GhcPass p) a)
+isUnsatisfied :: Eq a => (a -> Bool) -> BooleanFormula (GhcPass p) a -> Maybe (BooleanFormula (GhcPass p) a)
isUnsatisfied f bf
| isTrue bf' = Nothing
| otherwise = Just bf'
@@ -166,14 +162,14 @@ isUnsatisfied f bf
-- eval f x == False <==> isFalse (simplify (Just . f) x)
-- If the boolean formula holds, does that mean that the given atom is always true?
-impliesAtom :: forall p a. Eq a => BooleanFormula (GhcPass p) a -> a -> Bool
+impliesAtom :: Eq a => BooleanFormula (GhcPass p) a -> a -> Bool
Var x `impliesAtom` y = x == y
And xs `impliesAtom` y = any (\x -> unLoc x `impliesAtom` y) xs
-- we have all of xs, so one of them implying y is enough
Or xs `impliesAtom` y = all (\x -> unLoc x `impliesAtom` y) xs
Parens x `impliesAtom` y = unLoc x `impliesAtom` y
-implies :: forall p a. Uniquable a => BooleanFormula (GhcPass p) a -> BooleanFormula (GhcPass p) a -> Bool
+implies :: Uniquable a => BooleanFormula (GhcPass p) a -> BooleanFormula (GhcPass p) a -> Bool
implies e1 e2 = go (Clause emptyUniqSet [e1]) (Clause emptyUniqSet [e2])
where
go :: Uniquable a => Clause (GhcPass p) a -> Clause (GhcPass p) a -> Bool
@@ -210,8 +206,7 @@ memberClauseAtoms x c = x `elementOfUniqSet` clauseAtoms c
-- Pretty print a BooleanFormula,
-- using the arguments as pretty printers for Var, And and Or respectively
-pprBooleanFormula' :: forall p a. ()
- => (Rational -> a -> SDoc)
+pprBooleanFormula' :: (Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational -> BooleanFormula (GhcPass p) a -> SDoc
@@ -245,8 +240,7 @@ pprBooleanFormulaNice = pprBooleanFormula' pprVar pprAnd pprOr 0
instance (OutputableBndr a) => Outputable (BooleanFormula (GhcPass p) a) where
ppr = pprBooleanFormulaNormal
-pprBooleanFormulaNormal :: forall p a. (OutputableBndr a)
- => BooleanFormula (GhcPass p) a -> SDoc
+pprBooleanFormulaNormal :: (OutputableBndr a) => BooleanFormula (GhcPass p) a -> SDoc
pprBooleanFormulaNormal = go
where
go (Var x) = pprPrefixOcc x
=====================================
compiler/GHC/Hs/Decls.hs
=====================================
@@ -103,6 +103,8 @@ module GHC.Hs.Decls (
import GHC.Prelude
import Language.Haskell.Syntax.Decls
+import Language.Haskell.Syntax.Extension
+import Language.Haskell.Syntax.BooleanFormula (BooleanFormula)
import {-# SOURCE #-} GHC.Hs.Expr ( pprExpr, pprUntypedSplice )
-- Because Expr imports Decls via HsBracket
@@ -112,7 +114,7 @@ import GHC.Hs.Type
import GHC.Hs.Doc
import GHC.Types.Basic
import GHC.Core.Coercion
-import Language.Haskell.Syntax.Extension
+
import GHC.Hs.Extension
import GHC.Parser.Annotation
import GHC.Types.Name
@@ -1395,3 +1397,4 @@ type instance Anno (Maybe Role) = EpAnnCO
type instance Anno CCallConv = EpaLocation
type instance Anno Safety = EpaLocation
type instance Anno CExportSpec = EpaLocation
+type instance Anno (BooleanFormula (GhcPass p) a) = SrcSpanAnnL
=====================================
compiler/Language/Haskell/Syntax/BooleanFormula.hs
=====================================
@@ -1,11 +1,14 @@
-{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
module Language.Haskell.Syntax.BooleanFormula(
BooleanFormula(..), LBooleanFormula,
mkVar, mkFalse, mkTrue, mkBool, mkAnd, mkOr) where
import Prelude hiding ( init, last )
import Data.List ( nub )
+import Data.Data (Data)
import Language.Haskell.Syntax.Extension (XRec, UnXRec (..))
@@ -14,16 +17,16 @@ type LBooleanFormula p a = XRec p (BooleanFormula p a)
--type role BooleanFormula phantom nominal
data BooleanFormula p a = Var a | And [LBooleanFormula p a] | Or [LBooleanFormula p a]
| Parens (LBooleanFormula p a)
- deriving () --, Functor, Foldable, Traversable)
--- | Monadic version of concatMap
-concatMapM :: (Monad m, Traversable f) => (a -> m [b]) -> f a -> m [b]
-concatMapM f xs = fmap concat (mapM f xs)
--- A dupe from GHC.Utils.Monad, until I figure out what to actually do with it.
-{-# INLINE concatMapM #-}
--- It's better to inline to inline this than to specialise
--- concatMapM :: (Monad m) => (a -> m [b]) -> [a] -> m [b]
--- Inlining cuts compiler allocation by around 1%
+-- instances
+deriving instance (Eq a, Eq (LBooleanFormula p a)) => Eq (BooleanFormula p a)
+deriving instance (Data a, Data p, Data (LBooleanFormula p a)) => Data (BooleanFormula p a)
+instance UnXRec p => Foldable (BooleanFormula p) where
+ foldMap :: Monoid m => (a -> m) -> BooleanFormula p a -> m
+ foldMap f (Var a ) = f a
+ foldMap f (And bfs) = foldMap (foldMap f . unXRec @p) bfs
+ foldMap f (Or bfs) = foldMap (foldMap f . unXRec @p) bfs
+ foldMap f (Parens bf ) = foldMap f $ unXRec @p bf
mkVar :: a -> BooleanFormula p a
@@ -40,7 +43,7 @@ mkBool True = mkTrue
-- Make a conjunction, and try to simplify
mkAnd :: forall p a. (UnXRec p, Eq a, Eq (LBooleanFormula p a)) => [LBooleanFormula p a] -> BooleanFormula p a
-mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
+mkAnd = maybe mkFalse (mkAnd' . nub . concat) . mapM fromAnd
where
-- See Note [Simplification of BooleanFormulas]
fromAnd :: LBooleanFormula p a -> Maybe [LBooleanFormula p a]
@@ -55,7 +58,7 @@ mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
mkAnd' xs = And xs
mkOr :: forall p a. (UnXRec p, Eq a, Eq (LBooleanFormula p a)) => [LBooleanFormula p a] -> BooleanFormula p a
-mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
+mkOr = maybe mkTrue (mkOr' . nub . concat) . mapM fromOr
where
-- See Note [Simplification of BooleanFormulas]
fromOr bf = case unXRec @p bf of
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2ad768025845f7a772047290c9c7a781bc5e6ab5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2ad768025845f7a772047290c9c7a781bc5e6ab5
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240918/7743c0eb/attachment-0001.html>
More information about the ghc-commits
mailing list