Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

3 changed files:

Changes:

  • compiler/GHC/HsToCore/Pmc/Solver/Types.hs
    ... ... @@ -2,6 +2,7 @@
    2 2 
     {-# LANGUAGE ScopedTypeVariables #-}
    3 3 
     {-# LANGUAGE ViewPatterns        #-}
    4 4 
     {-# LANGUAGE MultiWayIf          #-}
    5 
    +{-# LANGUAGE TypeFamilies        #-}
    5 6
    6 7 
     -- | Domain types used in "GHC.HsToCore.Pmc.Solver".
    7 8 
     -- The ultimate goal is to define 'Nabla', which models normalised refinement
    ... ... @@ -32,7 +33,7 @@ module GHC.HsToCore.Pmc.Solver.Types (
    32 33 
             PmEquality(..), eqPmAltCon,
    33 34
    34 35 
             -- *** Operations on 'PmLit'
    35 
    -        literalToPmLit, negatePmLit, overloadPmLit,
    36 
    +        literalToPmLit, negatePmLit,
    36 37 
             pmLitAsStringLit, coreExprAsPmLit
    37 38
    38 39 
         ) where
    ... ... @@ -51,13 +52,12 @@ import GHC.Core.ConLike
    51 52 
     import GHC.Utils.Outputable
    52 53 
     import GHC.Utils.Panic.Plain
    53 54 
     import GHC.Utils.Misc (lastMaybe)
    54 
    -import GHC.Data.List.SetOps (unionLists)
    55 55 
     import GHC.Data.Maybe
    56 56 
     import GHC.Core.Type
    57 57 
     import GHC.Core.TyCon
    58 58 
     import GHC.Types.Literal
    59 59 
     import GHC.Core
    60 
    -import GHC.Core.TyCo.Compare( eqType )
    60 
    +import GHC.Core.TyCo.Compare( eqType, nonDetCmpType )
    61 61 
     import GHC.Core.Map.Expr
    62 62 
     import GHC.Core.Utils (exprType)
    63 63 
     import GHC.Builtin.Names
    ... ... @@ -69,15 +69,14 @@ import GHC.Types.CompleteMatch
    69 69 
     import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
    70 70 
                                 , fractionalLitFromRational
    71 71 
                                 , FractionalExponentBase(..))
    72 
    +
    72 73 
     import Numeric (fromRat)
    73 
    -import Data.Foldable (find)
    74 74 
     import Data.Ratio
    75 
    +import Data.List( find )
    76 
    +import qualified Data.Map as FM
    75 77 
     import GHC.Real (Ratio(..))
    76 
    -import qualified Data.Semigroup as Semi
    77 
    -
    78 
    --- import GHC.Driver.Ppr
    78 
    +import qualified Data.Semigroup as S
    79 79
    80 
    ---
    81 80 
     -- * Normalised refinement types
    82 81 
     --
    83 82
    ... ... @@ -358,6 +357,13 @@ lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of
    358 357 
         | Just sol <- find isDataConSolution pos -> Just sol
    359 358 
         | otherwise                              -> Just x
    360 359
    360 
    +
    361 
    +{- *********************************************************************
    362 
    +*                                                                      *
    363 
    +                 PmLit and PmLitValue
    364 
    +*                                                                      *
    365 
    +********************************************************************* -}
    366 
    +
    361 367 
     --------------------------------------------------------------------------------
    362 368 
     -- The rest is just providing an IR for (overloaded!) literals and AltCons that
    363 369 
     -- sits between Hs and Core. We need a reliable way to detect and determine
    ... ... @@ -376,13 +382,64 @@ data PmLitValue
    376 382 
       = PmLitInt Integer
    377 383 
       | PmLitRat Rational
    378 384 
       | PmLitChar Char
    379 
    -  -- We won't actually see PmLitString in the oracle since we desugar strings to
    380 
    -  -- lists
    381 385 
       | PmLitString FastString
    386 
    +       -- We won't actually see PmLitString in the oracle
    387 
    +       -- since we desugar strings to lists
    388 
    +
    389 
    +  -- Overloaded literals
    382 390 
       | PmLitOverInt Int {- How often Negated? -} Integer
    383 391 
       | PmLitOverRat Int {- How often Negated? -} FractionalLit
    384 392 
       | PmLitOverString FastString
    385 393
    394 
    +-- | Syntactic equality.
    395 
    +-- We want (Ord PmLit) so that we can use (Map PmLit x) in `PmAltConSet`
    396 
    +instance Eq PmLit where
    397 
    +  a == b = (a `compare` b) == EQ
    398 
    +instance Ord PmLit where
    399 
    +  compare = cmpPmLit
    400 
    +
    401 
    +cmpPmLit :: PmLit -> PmLit -> Ordering
    402 
    +-- This function does "syntactic comparison":
    403 
    +--   For overloaded literals, compare the type and value
    404 
    +--   For non-overloaded literals, just compare the values
    405 
    +-- But it treats (say)
    406 
    +--    (PmLit Bool (PmLitOverInt 1))
    407 
    +--    (PmLit Bool (PmLitOverInt 2))
    408 
    +-- as un-equal, even through (fromInteger @Bool 1)
    409 
    +-- could be the same as (fromInteger @Bool 2)
    410 
    +cmpPmLit (PmLit { pm_lit_ty = t1, pm_lit_val = val1 })
    411 
    +         (PmLit { pm_lit_ty = t2, pm_lit_val = val2 })
    412 
    +  = case (val1,val2) of
    413 
    +      (PmLitInt i1, PmLitInt i2) -> i1 `compare` i2
    414 
    +      (PmLitRat r1, PmLitRat r2) -> r1 `compare` r2
    415 
    +      (PmLitChar c1, PmLitChar c2) -> c1 `compare` c2
    416 
    +      (PmLitString s1, PmLitString s2) -> s1 `uniqCompareFS` s2
    417 
    +      (PmLitOverInt n1 i1, PmLitOverInt n2 i2) -> (n1 `compare` n2) S.<>
    418 
    +                                                  (i1 `compare` i2) S.<>
    419 
    +                                                  (t1 `nonDetCmpType` t2)
    420 
    +      (PmLitOverRat n1 r1, PmLitOverRat n2 r2) -> (n1 `compare` n2) S.<>
    421 
    +                                                  (r1 `compare` r2) S.<>
    422 
    +                                                  (t1 `nonDetCmpType` t2)
    423 
    +      (PmLitOverString s1, PmLitOverString s2) -> (s1 `uniqCompareFS` s2) S.<>
    424 
    +                                                  (t1 `nonDetCmpType` t2)
    425 
    +      (PmLitInt {},    _) -> LT
    426 
    +      (PmLitRat {},    PmLitInt {})  -> GT
    427 
    +      (PmLitRat {},    _)            -> LT
    428 
    +      (PmLitChar {},   PmLitInt {})  -> GT
    429 
    +      (PmLitChar {},   PmLitRat {})  -> GT
    430 
    +      (PmLitChar {},   _)            -> LT
    431 
    +      (PmLitString {}, PmLitInt {})  -> GT
    432 
    +      (PmLitString {}, PmLitRat {})  -> GT
    433 
    +      (PmLitString {}, PmLitChar {}) -> GT
    434 
    +      (PmLitString {}, _)            -> LT
    435 
    +
    436 
    +      (PmLitOverString {}, _)                 -> GT
    437 
    +      (PmLitOverRat {},    PmLitOverString{}) -> LT
    438 
    +      (PmLitOverRat {},    _)                 -> GT
    439 
    +      (PmLitOverInt {},    PmLitOverString{}) -> LT
    440 
    +      (PmLitOverInt {},    PmLitOverRat{})    -> LT
    441 
    +      (PmLitOverInt {},    _)                 -> GT
    442 
    +
    386 443 
     -- | Undecidable semantic equality result.
    387 444 
     -- See Note [Undecidable Equality for PmAltCons]
    388 445 
     data PmEquality
    ... ... @@ -406,7 +463,10 @@ eqPmLit :: PmLit -> PmLit -> PmEquality
    406 463 
     eqPmLit (PmLit t1 v1) (PmLit t2 v2)
    407 464 
       -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
    408 465 
       | not (t1 `eqType` t2) = Disjoint
    409 
    -  | otherwise            = go v1 v2
    466 
    +  | otherwise            = eqPmLitValue v1 v2
    467 
    +
    468 
    +eqPmLitValue :: PmLitValue -> PmLitValue -> PmEquality
    469 
    +eqPmLitValue v1 v2 = go v1 v2
    410 470 
       where
    411 471 
         go (PmLitInt i1)        (PmLitInt i2)        = decEquality (i1 == i2)
    412 472 
         go (PmLitRat r1)        (PmLitRat r2)        = decEquality (r1 == r2)
    ... ... @@ -420,10 +480,6 @@ eqPmLit (PmLit t1 v1) (PmLit t2 v2)
    420 480 
           | s1 == s2                                 = Equal
    421 481 
         go _                    _                    = PossiblyOverlap
    422 482
    423 
    --- | Syntactic equality.
    424 
    -instance Eq PmLit where
    425 
    -  a == b = eqPmLit a b == Equal
    426 
    -
    427 483 
     -- | Type of a 'PmLit'
    428 484 
     pmLitType :: PmLit -> Type
    429 485 
     pmLitType (PmLit ty _) = ty
    ... ... @@ -445,34 +501,47 @@ eqConLike (PatSynCon psc1) (PatSynCon psc2)
    445 501 
       = Equal
    446 502 
     eqConLike _                 _                 = PossiblyOverlap
    447 503
    504 
    +
    505 
    +{- *********************************************************************
    506 
    +*                                                                      *
    507 
    +                 PmAltCon and PmAltConSet
    508 
    +*                                                                      *
    509 
    +********************************************************************* -}
    510 
    +
    448 511 
     -- | Represents the head of a match against a 'ConLike' or literal.
    449 512 
     -- Really similar to 'GHC.Core.AltCon'.
    450 513 
     data PmAltCon = PmAltConLike ConLike
    451 514 
                   | PmAltLit     PmLit
    452 515
    453 
    -data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit]
    516 
    +data PmAltConSet = PACS !(UniqDSet ConLike)
    517 
    +                        !(FM.Map PmLit PmLit)
    518 
    +-- We use a (FM.Map PmLit PmLit) here, at the cost of requiring an Ord
    519 
    +-- instance for PmLit, because in extreme cases the set of PmLits can be
    520 
    +-- very large.  See #26514.
    454 521
    455 522 
     emptyPmAltConSet :: PmAltConSet
    456 
    -emptyPmAltConSet = PACS emptyUniqDSet []
    523 
    +emptyPmAltConSet = PACS emptyUniqDSet FM.empty
    457 524
    458 525 
     isEmptyPmAltConSet :: PmAltConSet -> Bool
    459 
    -isEmptyPmAltConSet (PACS cls lits) = isEmptyUniqDSet cls && null lits
    526 
    +isEmptyPmAltConSet (PACS cls lits)
    527 
    +  = isEmptyUniqDSet cls && FM.null lits
    460 528
    461 529 
     -- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
    462 530 
     -- the given 'PmAltCon' according to 'eqPmAltCon'.
    463 531 
     elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
    464 532 
     elemPmAltConSet (PmAltConLike cl) (PACS cls _   ) = elementOfUniqDSet cl cls
    465 
    -elemPmAltConSet (PmAltLit lit)    (PACS _   lits) = elem lit lits
    533 
    +elemPmAltConSet (PmAltLit lit)    (PACS _   lits) = isJust (FM.lookup lit lits)
    466 534
    467 535 
     extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
    468 536 
     extendPmAltConSet (PACS cls lits) (PmAltConLike cl)
    469 537 
       = PACS (addOneToUniqDSet cls cl) lits
    470 538 
     extendPmAltConSet (PACS cls lits) (PmAltLit lit)
    471 
    -  = PACS cls (unionLists lits [lit])
    539 
    +  = PACS cls (FM.insert lit lit lits)
    472 540
    473 541 
     pmAltConSetElems :: PmAltConSet -> [PmAltCon]
    474 542 
     pmAltConSetElems (PACS cls lits)
    475 
    -  = map PmAltConLike (uniqDSetToList cls) ++ map PmAltLit lits
    543 
    +  = map PmAltConLike (uniqDSetToList cls) ++
    544 
    +    FM.foldr ((:) . PmAltLit) [] lits
    476 545
    477 546 
     instance Outputable PmAltConSet where
    478 547 
       ppr = ppr . pmAltConSetElems

  • compiler/GHC/Types/SourceText.hs
    ... ... @@ -188,6 +188,7 @@ data FractionalLit = FL
    188 188 
         }
    189 189 
         deriving (Data, Show)
    190 190 
       -- The Show instance is required for the derived GHC.Parser.Lexer.Token instance when DEBUG is on
    191 
    +  -- Eq and Ord instances are done explicitly
    191 192
    192 193 
     -- See Note [FractionalLit representation] in GHC.HsToCore.Match.Literal
    193 194 
     data FractionalExponentBase

  • testsuite/tests/pmcheck/should_compile/pmcOrPats.stderr
    1 
    -
    2 1 
     pmcOrPats.hs:10:1: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    3 2 
         Pattern match(es) are non-exhaustive
    4 3 
         In an equation for ‘g’: Patterns of type ‘T’, ‘U’ not matched: A W
    ... ... @@ -18,7 +17,7 @@ pmcOrPats.hs:15:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)]
    18 17 
     pmcOrPats.hs:17:1: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)]
    19 18 
         Pattern match(es) are non-exhaustive
    20 19 
         In an equation for ‘z’:
    21 
    -        Patterns of type ‘a’ not matched: p where p is not one of {3, 1, 2}
    20 
    +        Patterns of type ‘a’ not matched: p where p is not one of {1, 2, 3}
    22 21
    23 22 
     pmcOrPats.hs:19:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)]
    24 23 
         Pattern match is redundant
    ... ... @@ -43,3 +42,4 @@ pmcOrPats.hs:21:1: warning: [GHC-61505]
    43 42 
           • Patterns reported as unmatched might actually be matched
    44 43 
         Suggested fix:
    45 44 
           Increase the limit or resolve the warnings to suppress this message.
    45 
    +

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help