ghc/compiler/typecheck/TcTyClsDecls.lhs

   1 %
   2 % (c) The AQUA Project, Glasgow University, 1996-1998
   3 %
   4 \section[TcTyClsDecls]{Typecheck type and class declarations}
   5
   6 \begin{code}
   7 module TcTyClsDecls (
   8         tcTyAndClassDecls
   9     ) where
  10
  11 #include "HsVersions.h"
  12
  13 import HsSyn            ( HsDecl(..), TyClDecl(..),
  14                           HsType(..), HsTyVar,
  15                           ConDecl(..), ConDetails(..), BangType(..),
  16                           Sig(..),
  17                           tyClDeclName, isClassDecl, isSynDecl
  18                         )
  19 import RnHsSyn          ( RenamedHsDecl, RenamedTyClDecl, listTyCon_name, tupleTyCon_name )
  20 import BasicTypes       ( RecFlag(..), NewOrData(..), Arity )
  21
  22 import TcMonad
  23 import Inst             ( InstanceMapper )
  24 import TcClassDcl       ( kcClassDecl, tcClassDecl1 )
  25 import TcEnv            ( ValueEnv, TcTyThing(..),
  26                           tcExtendTypeEnv, getAllEnvTyCons
  27                         )
  28 import TcTyDecls        ( tcTyDecl, kcTyDecl )
  29 import TcMonoType       ( kcHsTyVar )
  30 import TcType           ( TcKind, newKindVar, newKindVars, kindToTcKind, zonkTcKindToKind )
  31
  32 import Type             ( mkArrowKind, boxedTypeKind, mkDictTy )
  33   -- next two imports for usage stuff only
  34 import TyCon            ( ArgVrcs, tyConKind, tyConArity, tyConDataCons, tyConTyVars,
  35                           tyConArgVrcs_maybe, getSynTyConDefn, isSynTyCon, isAlgTyCon )
  36 import DataCon          ( dataConRawArgTys, dataConSig )
  37
  38 import Class            ( Class, classBigSig )
  39 import Type             ( Type(..), TyNote(..), tyVarsOfTypes )
  40 import Var              ( TyVar, tyVarKind )
  41 import FiniteMap
  42 import Bag
  43 import VarSet
  44 import Digraph          ( stronglyConnComp, SCC(..) )
  45 import Name             ( Name, NamedThing(..), getSrcLoc, isTvOcc, nameOccName )
  46 import Outputable
  47 import Maybes           ( mapMaybe, expectJust )
  48 import UniqSet          ( UniqSet, emptyUniqSet,
  49                           unitUniqSet, unionUniqSets,
  50                           unionManyUniqSets, uniqSetToList )
  51 import ErrUtils         ( Message )
  52 import SrcLoc           ( SrcLoc )
  53 import TyCon            ( TyCon )
  54 import Unique           ( Unique, Uniquable(..) )
  55 import UniqFM           ( listToUFM, lookupUFM )
  56 \end{code}
  57
  58 The main function
  59 ~~~~~~~~~~~~~~~~~
  60 \begin{code}
  61 tcTyAndClassDecls :: ValueEnv -> InstanceMapper -- Knot tying stuff
  62                   -> [RenamedHsDecl]
  63                   -> TcM s TcEnv
  64
  65 tcTyAndClassDecls unf_env inst_mapper decls
  66   = sortByDependency decls              `thenTc` \ groups ->
  67     tcGroups unf_env inst_mapper groups
  68
  69 tcGroups unf_env inst_mapper []
  70   = tcGetEnv    `thenNF_Tc` \ env ->
  71     returnTc env
  72
  73 tcGroups unf_env inst_mapper (group:groups)
  74   = tcGroup unf_env inst_mapper group   `thenTc` \ env ->
  75     tcSetEnv env                        $
  76     tcGroups unf_env inst_mapper groups
  77 \end{code}
  78
  79 Dealing with a group
  80 ~~~~~~~~~~~~~~~~~~~~
  81
  82 The knot-tying parameters: @rec_tyclss@ is an alist mapping @Name@s to
  83 @TcTyThing@s.  @rec_vrcs@ is a finite map from @Name@s to @ArgVrcs@s.
  84
  85 \begin{code}
  86 tcGroup :: ValueEnv -> InstanceMapper -> SCC RenamedTyClDecl -> TcM s TcEnv
  87 tcGroup unf_env inst_mapper scc
  88   =     -- Do kind checking
  89     mapNF_Tc getTyBinding1 decls                        `thenNF_Tc` \ ty_env_stuff1 ->
  90     tcExtendTypeEnv ty_env_stuff1 (mapTc kcDecl decls)  `thenTc_`
  91
  92         -- Tie the knot
  93 --  traceTc (ppr (map fst ty_env_stuff1))               `thenTc_`
  94     fixTc ( \ ~(rec_tyclss, rec_vrcs, _) ->
  95         let
  96             rec_env = listToUFM rec_tyclss
  97         in
  98
  99                 -- Do type checking
 100         mapNF_Tc (getTyBinding2 rec_env) ty_env_stuff1  `thenNF_Tc` \ ty_env_stuff2 ->
 101         tcExtendTypeEnv ty_env_stuff2                           $
 102         mapTc (tcDecl is_rec_group unf_env inst_mapper rec_vrcs) decls
 103                                                                 `thenTc` \ tyclss ->
 104
 105         tcGetEnv                                                `thenTc` \ env ->
 106         let
 107             tycons = getAllEnvTyCons env
 108             vrcs   = calcTyConArgVrcs tycons
 109         in
 110
 111         returnTc (tyclss, vrcs, env)
 112     )                                                           `thenTc` \ (_, _, env) ->
 113 --  traceTc (text "done" <+> ppr (map fst ty_env_stuff1))       `thenTc_`
 114     returnTc env
 115   where
 116     is_rec_group = case scc of
 117                         AcyclicSCC _ -> NonRecursive
 118                         CyclicSCC _  -> Recursive
 119
 120     decls = case scc of
 121                 AcyclicSCC decl -> [decl]
 122                 CyclicSCC decls -> decls
 123 \end{code}
 124
 125 Dealing with one decl
 126 ~~~~~~~~~~~~~~~~~~~~~
 127 \begin{code}
 128 kcDecl decl
 129   = tcAddDeclCtxt decl          $
 130     if isClassDecl decl then
 131         kcClassDecl decl
 132     else
 133         kcTyDecl    decl
 134
 135 tcDecl  :: RecFlag                      -- True => recursive group
 136          -> ValueEnv -> InstanceMapper -> FiniteMap Name ArgVrcs
 137          -> RenamedTyClDecl -> TcM s (Name, TcTyThing)
 138
 139 tcDecl is_rec_group unf_env inst_mapper vrcs_env decl
 140   = tcAddDeclCtxt decl          $
 141 --  traceTc (text "Starting" <+> ppr name)      `thenTc_`
 142     if isClassDecl decl then
 143         tcClassDecl1 unf_env inst_mapper vrcs_env decl  `thenTc` \ clas ->
 144 --      traceTc (text "Finished" <+> ppr name)          `thenTc_`
 145         returnTc (getName clas, AClass clas)
 146     else
 147         tcTyDecl is_rec_group vrcs_env decl     `thenTc` \ tycon ->
 148 --      traceTc (text "Finished" <+> ppr name)  `thenTc_`
 149         returnTc (getName tycon, ATyCon tycon)
 150
 151   where
 152     name = tyClDeclName decl
 153
 154
 155 tcAddDeclCtxt decl thing_inside
 156   = tcAddSrcLoc loc     $
 157     tcAddErrCtxt ctxt   $
 158     thing_inside
 159   where
 160      (name, loc, thing)
 161         = case decl of
 162             (ClassDecl _ name _ _ _ _ _ _ loc)   -> (name, loc, "class")
 163             (TySynonym name _ _ loc)             -> (name, loc, "type synonym")
 164             (TyData NewType  _ name _ _ _ _ loc) -> (name, loc, "data type")
 165             (TyData DataType _ name _ _ _ _ loc) -> (name, loc, "newtype")
 166
 167      ctxt = hsep [ptext SLIT("In the"), text thing,
 168                   ptext SLIT("declaration for"), quotes (ppr name)]
 169 \end{code}
 170
 171
 172 getTyBinders
 173 ~~~~~~~~~~~
 174 Extract *binding* names from type and class decls.  Type variables are
 175 bound in type, data, newtype and class declarations,
 176         *and* the polytypes in the class op sigs.
 177         *and* the existentially quantified contexts in datacon decls
 178
 179 Why do we need to grab all these type variables at once, including
 180 those locally-quantified type variables in class op signatures?
 181
 182         [Incidentally, this only works because the names are all unique by now.]
 183
 184 Because we can only commit to the final kind of a type variable when
 185 we've completed the mutually recursive group. For example:
 186
 187 class C a where
 188    op :: D b => a -> b -> b
 189
 190 class D c where
 191    bop :: (Monad c) => ...
 192
 193 Here, the kind of the locally-polymorphic type variable "b"
 194 depends on *all the uses of class D*.  For example, the use of
 195 Monad c in bop's type signature means that D must have kind Type->Type.
 196
 197
 198 \begin{code}
 199 getTyBinding1 :: RenamedTyClDecl -> NF_TcM s (Name, (TcKind, Maybe Arity, TcTyThing))
 200 getTyBinding1 (TySynonym name tyvars _ _)
 201  = mapNF_Tc kcHsTyVar tyvars            `thenNF_Tc` \ arg_kinds ->
 202    newKindVar                           `thenNF_Tc` \ result_kind  ->
 203    returnNF_Tc (name, (foldr mkArrowKind result_kind arg_kinds,
 204                        Just (length tyvars),
 205                        ATyCon (pprPanic "ATyCon: syn" (ppr name))))
 206
 207 getTyBinding1 (TyData _ _ name tyvars _ _ _ _)
 208  = mapNF_Tc kcHsTyVar tyvars            `thenNF_Tc` \ arg_kinds ->
 209    returnNF_Tc (name, (foldr mkArrowKind boxedTypeKind arg_kinds,
 210                        Nothing,
 211                        ATyCon (error "ATyCon: data")))
 212
 213 getTyBinding1 (ClassDecl _ name tyvars _ _ _ _ _ _)
 214  = mapNF_Tc kcHsTyVar tyvars            `thenNF_Tc` \ arg_kinds ->
 215    returnNF_Tc (name, (foldr mkArrowKind boxedTypeKind arg_kinds,
 216                        Just (length tyvars),
 217                        AClass (error "AClass")))
 218
 219 -- Zonk the kind to its final form, and lookup the
 220 -- recursive tycon/class
 221 getTyBinding2 rec_env (name, (tc_kind, maybe_arity, thing))
 222   = zonkTcKindToKind tc_kind            `thenNF_Tc` \ kind ->
 223     returnNF_Tc (name, (kind, maybe_arity, mk_thing thing (lookupUFM rec_env name)))
 224   where
 225     mk_thing (ATyCon _) ~(Just (ATyCon tc))  = ATyCon tc
 226     mk_thing (AClass _) ~(Just (AClass cls)) = AClass cls
 227 \end{code}
 228
 229
 230 %************************************************************************
 231 %*                                                                      *
 232 \subsection{Dependency analysis}
 233 %*                                                                      *
 234 %************************************************************************
 235
 236 Dependency analysis
 237 ~~~~~~~~~~~~~~~~~~~
 238 \begin{code}
 239 sortByDependency :: [RenamedHsDecl] -> TcM s [SCC RenamedTyClDecl]
 240 sortByDependency decls
 241   = let         -- CHECK FOR CLASS CYCLES
 242         cls_sccs   = stronglyConnComp (mapMaybe mk_cls_edges tycl_decls)
 243         cls_cycles = [ decls | CyclicSCC decls <- cls_sccs]
 244     in
 245     checkTc (null cls_cycles) (classCycleErr cls_cycles)        `thenTc_`
 246
 247     let         -- CHECK FOR SYNONYM CYCLES
 248         syn_sccs   = stronglyConnComp (filter is_syn_decl edges)
 249         syn_cycles = [ decls | CyclicSCC decls <- syn_sccs]
 250
 251     in
 252     checkTc (null syn_cycles) (typeCycleErr syn_cycles)         `thenTc_`
 253
 254         -- DO THE MAIN DEPENDENCY ANALYSIS
 255     let
 256         decl_sccs  = stronglyConnComp edges
 257     in
 258     returnTc decl_sccs
 259   where
 260     tycl_decls = [d | TyClD d <- decls]
 261     edges      = map mk_edges tycl_decls
 262
 263     is_syn_decl (d, _, _) = isSynDecl d
 264     is_cls_decl (d, _, _) = isClassDecl d
 265 \end{code}
 266
 267 Edges in Type/Class decls
 268 ~~~~~~~~~~~~~~~~~~~~~~~~~
 269
 270 \begin{code}
 271 ----------------------------------------------------
 272 -- mk_cls_edges looks only at the context of class decls
 273 -- Its used when we are figuring out if there's a cycle in the
 274 -- superclass hierarchy
 275
 276 mk_cls_edges :: RenamedTyClDecl -> Maybe (RenamedTyClDecl, Unique, [Unique])
 277
 278 mk_cls_edges decl@(ClassDecl ctxt name _ _ _ _ _ _ _)
 279   = Just (decl, getUnique name, map (getUnique . fst) ctxt)
 280 mk_cls_edges other_decl
 281   = Nothing
 282
 283 ----------------------------------------------------
 284 mk_edges :: RenamedTyClDecl -> (RenamedTyClDecl, Unique, [Unique])
 285
 286 mk_edges decl@(TyData _ ctxt name _ condecls derivs _ _)
 287   = (decl, getUnique name, uniqSetToList (get_ctxt ctxt `unionUniqSets`
 288                                          get_cons condecls `unionUniqSets`
 289                                          get_deriv derivs))
 290
 291 mk_edges decl@(TySynonym name _ rhs _)
 292   = (decl, getUnique name, uniqSetToList (get_ty rhs))
 293
 294 mk_edges decl@(ClassDecl ctxt name _ sigs _ _ _ _ _)
 295   = (decl, getUnique name, uniqSetToList (get_ctxt ctxt `unionUniqSets`
 296                                          get_sigs sigs))
 297
 298
 299 ----------------------------------------------------
 300 get_ctxt ctxt = unionManyUniqSets (map (set_name.fst) ctxt)
 301
 302 ----------------------------------------------------
 303 get_deriv Nothing     = emptyUniqSet
 304 get_deriv (Just clss) = unionManyUniqSets (map set_name clss)
 305
 306 ----------------------------------------------------
 307 get_cons cons = unionManyUniqSets (map get_con cons)
 308
 309 ----------------------------------------------------
 310 get_con (ConDecl _ _ ctxt details _)
 311   = get_ctxt ctxt `unionUniqSets` get_con_details details
 312
 313 ----------------------------------------------------
 314 get_con_details (VanillaCon btys)    = unionManyUniqSets (map get_bty btys)
 315 get_con_details (InfixCon bty1 bty2) = unionUniqSets (get_bty bty1) (get_bty bty2)
 316 get_con_details (NewCon ty _)        = get_ty ty
 317 get_con_details (RecCon nbtys)       = unionManyUniqSets (map (get_bty.snd) nbtys)
 318
 319 ----------------------------------------------------
 320 get_bty (Banged ty)   = get_ty ty
 321 get_bty (Unbanged ty) = get_ty ty
 322 get_bty (Unpacked ty) = get_ty ty
 323
 324 ----------------------------------------------------
 325 get_ty (MonoTyVar name)
 326   = if isTvOcc (nameOccName name) then emptyUniqSet else set_name name
 327 get_ty (MonoTyApp ty1 ty2)
 328   = unionUniqSets (get_ty ty1) (get_ty ty2)
 329 get_ty (MonoFunTy ty1 ty2)
 330   = unionUniqSets (get_ty ty1) (get_ty ty2)
 331 get_ty (MonoListTy ty)
 332   = set_name listTyCon_name `unionUniqSets` get_ty ty
 333 get_ty (MonoTupleTy tys boxed)
 334   = set_name (tupleTyCon_name boxed (length tys)) `unionUniqSets` get_tys tys
 335 get_ty (MonoUsgTy _ ty)
 336   = get_ty ty
 337 get_ty (HsForAllTy _ ctxt mty)
 338   = get_ctxt ctxt `unionUniqSets` get_ty mty
 339 get_ty (MonoDictTy name _)
 340   = set_name name
 341
 342 ----------------------------------------------------
 343 get_tys tys
 344   = unionManyUniqSets (map get_ty tys)
 345
 346 ----------------------------------------------------
 347 get_sigs sigs
 348   = unionManyUniqSets (mapMaybe get_sig sigs)
 349   where
 350     get_sig (ClassOpSig _ _ ty _) = Just (get_ty ty)
 351     get_sig (FixSig _)            = Nothing
 352     get_sig other                 = panic "TcTyClsDecls:get_sig"
 353
 354 ----------------------------------------------------
 355 set_name name = unitUniqSet (getUnique name)
 356 set_to_bag set = listToBag (uniqSetToList set)
 357 \end{code}
 358
 359
 360 \begin{code}
 361 typeCycleErr, classCycleErr :: [[RenamedTyClDecl]] -> Message
 362
 363 typeCycleErr syn_cycles
 364   = vcat (map (pp_cycle "Cycle in type declarations:") syn_cycles)
 365
 366 classCycleErr cls_cycles
 367   = vcat (map (pp_cycle "Cycle in class declarations:") cls_cycles)
 368
 369 pp_cycle str decls
 370   = hang (text str)
 371          4 (vcat (map pp_decl decls))
 372   where
 373     pp_decl decl
 374       = hsep [quotes (ppr name), ptext SLIT("at"), ppr (getSrcLoc name)]
 375      where
 376         name = tyClDeclName decl
 377 \end{code}
 378
 379
 380 Computing the tyConArgVrcs info
 381 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 382
 383 @tyConArgVrcs@ gives a list of (occPos,occNeg) flags, one for each
 384 tyvar.  For @AlgTyCon@s and @SynTyCon@s, this info must be precomputed
 385 separately.  Note that this is information about occurrences of type
 386 variables, not usages of term variables.
 387
 388 The function @calcTyConArgVrcs@ must be passed a list of *algebraic or
 389 syntycons only* such that all tycons referred to (by mutual recursion)
 390 appear in the list.  The fixpointing will be done on this set of
 391 tycons as a whole.  It returns a list of @tyconVrcInfo@ data, ready to
 392 be (knot-tyingly?) stuck back into the appropriate fields.
 393
 394 \begin{code}
 395 calcTyConArgVrcs :: [TyCon]
 396                  -> FiniteMap Name ArgVrcs
 397
 398 calcTyConArgVrcs tycons
 399   = let oi           = foldl (\fm tc -> addToFM fm tc (initial tc)) emptyFM tycons
 400         initial tc   = if isAlgTyCon tc && null (tyConDataCons tc) then
 401                          -- make pessimistic assumption (and warn)
 402                          take (tyConArity tc) abstractVrcs
 403                        else
 404                          replicate (tyConArity tc) (False,False)
 405         oi''         = tcaoFix oi
 406         go (tc,vrcs) = (getName tc,vrcs)
 407     in  listToFM (map go (fmToList oi''))
 408
 409   where
 410
 411     tcaoFix :: FiniteMap TyCon ArgVrcs   -- initial ArgVrcs per tycon
 412             -> FiniteMap TyCon ArgVrcs   -- fixpointed ArgVrcs per tycon
 413
 414     tcaoFix oi = let (changed,oi') = foldFM (\ tc pms
 415                                                (changed,oi')
 416                                                -> let pms' = tcaoIter oi' tc  -- seq not simult
 417                                                   in  (changed || (pms /= pms'),
 418                                                        addToFM oi' tc pms'))
 419                                             (False,oi)  -- seq not simult for faster fixpting
 420                                             oi
 421                  in  if changed
 422                      then tcaoFix oi'
 423                      else oi'
 424
 425     tcaoIter :: FiniteMap TyCon ArgVrcs  -- reference ArgVrcs (initial)
 426              -> TyCon                    -- tycon to update
 427              -> ArgVrcs                  -- new ArgVrcs for tycon
 428
 429     tcaoIter oi tc | isAlgTyCon tc
 430       = let cs        = tyConDataCons tc
 431             vs        = tyConTyVars tc
 432             argtys    = concatMap dataConRawArgTys cs
 433             exdicttys = concatMap ((\ (_,_,_,exth,_,_) -> map (uncurry mkDictTy) exth)
 434                                    . dataConSig) cs
 435             myfao tc  = lookupWithDefaultFM oi (expectJust "tcaoIter(Alg)" $
 436                                                   tyConArgVrcs_maybe tc)
 437                                                tc
 438                         -- we use the already-computed result for tycons not in this SCC
 439         in  map (\v -> anyVrc (\ty -> vrcInTy myfao v ty) (exdicttys ++ argtys))
 440                 vs
 441
 442     tcaoIter oi tc | isSynTyCon tc
 443       = let (tyvs,ty) = getSynTyConDefn tc
 444             myfao tc  = lookupWithDefaultFM oi (expectJust "tcaoIter(Syn)" $
 445                                                   tyConArgVrcs_maybe tc)
 446                                                tc
 447                         -- we use the already-computed result for tycons not in this SCC
 448         in  map (\v -> vrcInTy myfao v ty) tyvs
 449
 450
 451 abstractVrcs :: ArgVrcs
 452 -- we pull this out as a CAF so the warning only appears *once*
 453 abstractVrcs = trace ("WARNING: tyConArgVrc info inaccurate due to unavailable constructors.\n"
 454                       ++ "\tUse -fno-prune-tydecls to fix.") $
 455                  repeat (True,True)
 456 \end{code}
 457
 458 And a general variance-check function.  We pass a function for
 459 determining the @ArgVrc@s of a tycon; when fixpointing this refers to
 460 the current value; otherwise this should be looked up from the tycon's
 461 own tyConArgVrcs.
 462
 463 \begin{code}
 464 vrcInTy :: (TyCon -> ArgVrcs)  -- function to get argVrcs of a tycon (break out of recursion)
 465         -> TyVar               -- tyvar to check Vrcs of
 466         -> Type                -- type to check for occ in
 467         -> (Bool,Bool)         -- (occurs positively, occurs negatively)
 468
 469 vrcInTy fao v (NoteTy (UsgNote _)   ty) = vrcInTy fao v ty
 470
 471 vrcInTy fao v (NoteTy (SynNote _)   ty) = vrcInTy fao v ty
 472                         -- SynTyCon doesn't neccessarily have vrcInfo at this point,
 473                         -- so don't try and use it
 474
 475 vrcInTy fao v (NoteTy (FTVNote ftv) ty) = if elemVarSet v ftv
 476                                           then vrcInTy fao v ty
 477                                           else (False,False)
 478                         -- note that ftv cannot be calculated as occPos||occNeg,
 479                         -- since if a tyvar occurs only as unused tyconarg,
 480                         -- occPos==occNeg==False, but ftv=True
 481
 482 vrcInTy fao v (TyVarTy v')              = if v==v'
 483                                           then (True,False)
 484                                           else (False,False)
 485
 486 vrcInTy fao v (AppTy ty1 ty2)           = if vrcInTy fao v ty2 /= (False,False)
 487                                           then (True,True)
 488                                           else vrcInTy fao v ty1
 489                         -- ty1 is probably unknown (or it would have been beta-reduced);
 490                         -- hence if v occurs in ty2 at all then it could occur with
 491                         -- either variance.  Otherwise it occurs as it does in ty1.
 492
 493 vrcInTy fao v (FunTy ty1 ty2)           = let (p1,m1) = vrcInTy fao v ty1
 494                                               (p2,m2) = vrcInTy fao v ty2
 495                                           in (m1||p2,p1||m2)
 496
 497 vrcInTy fao v (ForAllTy v' ty)          = if v==v'
 498                                           then (False,False)
 499                                           else vrcInTy fao v ty
 500
 501 vrcInTy fao v (TyConApp tc tys)         = let pms1 = map (vrcInTy fao v) tys
 502                                               pms2 = fao tc
 503                                           in  orVrcs (zipWith timesVrc pms1 pms2)
 504
 505 orVrc :: (Bool,Bool) -> (Bool,Bool) -> (Bool,Bool)
 506 orVrc (p1,m1) (p2,m2) = (p1||p2,m1||m2)
 507
 508 orVrcs :: [(Bool,Bool)] -> (Bool,Bool)
 509 orVrcs = foldl orVrc (False,False)
 510
 511 anyVrc :: (a -> (Bool,Bool)) -> [a] -> (Bool,Bool)
 512 anyVrc p as = foldl (\pm a -> pm `orVrc` p a) (False,False) as
 513
 514 timesVrc :: (Bool,Bool) -> (Bool,Bool) -> (Bool,Bool)
 515 timesVrc (p1,m1) (p2,m2) = (p1 && p2 || m1 && m2,
 516                             p1 && m2 || m1 && p2)
 517 \end{code}
 518
 519