[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / AG / FP / AG / ComSubsElim / CoreCmpModAlpha
Printer-friendly

Comparison of Core expressions and types modulo alpha equivalence

Comparison of Core expressions and types modulo alpha equivalence

Olaf Chitil

Exports and Imports


#include "HsVersions.h"


module CoreCmpModAlpha (
         GenCoreBinding(..), GenCoreExpr(..),
         GenCoreArg(..), GenCoreBinder(..), GenCoreCaseAlts(..),
         GenCoreCaseDefault(..),
         Coercion,
         Alpha, emptyAlpha,
         cmpModAlphaBinding, cmpModAlphaExpr, cmpModAlphaArg,
         cmpModAlphaBinder, cmpModAlphaCaseAlts, cmpModAlphaCaseDefault
       ) where

import Pretty(PrettyRep)
import PprStyle(PprStyle)

import Bag(Bag)
import Util(Ord3(..))  -- class Ord3 
       -- class needed for Id's, TyVar's, Literal's, Unique's,..
import Outputable(Outputable(..)) 
       -- class needed for Id's, BinderInfo's, ...
import Name(NamedThing(..), Name, OrigName, RdrName) 
       -- class needed for Id's and TyVar's,.. and types
import UniqFM(Uniquable(..), UniqFM) 
       -- class needed for Id's, TyVar's, ...
import Literal(Literal)
import Unique(Unique)
import CostCentre(CostCentre)
import BinderInfo(BinderInfo)
import TyVar(SYN_IE(TyVar), GenTyVar)
import Id(SYN_IE(Id), GenId)
import TyCon(TyCon)
import Class(GenClass)

-- what is actually needed:
import PrimOp(PrimOp, tagOf_PrimOp) -- for comparison
import CoreSyn
--import FiniteMap (FiniteMap, emtpyFM, addToFM, lookupFM)
import FiniteMap 
import TyCon(TyCon, mkFunTyCon)
import Type(SYN_IE(Type), GenType(..)) 
       -- need internals for comparision
import Usage(SYN_IE(Usage), GenUsage(..)) -- need internals for comparison

Assisting functions for _CMP_TAG


thenCmp :: _CMP_TAG -> _CMP_TAG -> _CMP_TAG
thenCmp _EQ   other = other
thenCmp first _     = first

lexicalCmp :: (a -> a -> _CMP_TAG) -> [a] -> [a] -> _CMP_TAG
lexicalCmp cmp []     []     = _EQ
lexicalCmp cmp []     (x:xs) = _LT
lexicalCmp cmp (x:xs) []     = _GT
lexicalCmp cmp (x:xs) (y:ys) = cmp x y `thenCmp` lexicalCmp cmp xs ys

Equality and ordering for coercions

Inside of coercions there are just id's of constructors. Hence equality modula alpha conversion is not necessary, just simple instances of Eq and Ord.


compareCoercion :: Coercion -> Coercion -> _CMP_TAG

compareCoercion (CoerceIn id1)  (CoerceIn id2)  = _tagCmp id1 id2
compareCoercion (CoerceIn id1)  _               = _LT
compareCoercion (CoerceOut id1) (CoerceOut id2) = _tagCmp id1 id2
compareCoercion _               _               = _GT


instance Eq Coercion where
  x == y = case (compareCoercion x y) of { _EQ -> True; _ -> False }    

instance Ord Coercion where
  x <= y = case (compareCoercion x y) of { _GT -> False; _ -> True }
  _tagCmp = compareCoercion
                        

The data type Alpha for keeping track of equal variables

Danger: implementation of instances depends on the two compared arguments never being swapped in recursive calls.


data (Ord valVar, Ord tyVar, Ord uVar) => Alpha valVar tyVar uVar 
     = Alpha (FiniteMap valVar valVar) (FiniteMap tyVar tyVar) 
         (FiniteMap uVar uVar)

emptyAlpha :: Alpha valVar tyVar uVar
emptyAlpha = Alpha emptyFM emptyFM emptyFM


addToAlphaValVar :: Ord valVar 
                 => Alpha valVar tyVar uVar -> valVar -> valVar 
                 -> Alpha valVar tyVar uVar

addToAlphaValVar (Alpha valVars tyVars uVars) valVar1 valVar2
  = Alpha (addToFM valVars valVar1 valVar2) tyVars uVars


addToAlphaTyVar :: Ord tyVar 
                => Alpha valVar tyVar uVar -> tyVar -> tyVar 
                -> Alpha valVar tyVar uVar

addToAlphaTyVar (Alpha valVars tyVars uVars) tyVar1 tyVar2
  = Alpha valVars (addToFM tyVars tyVar1 tyVar2) uVars

                                                          
addToAlphaUVar :: Ord uVar 
                 => Alpha valVar tyVar uVar -> uVar -> uVar 
                 -> Alpha valVar tyVar uVar

addToAlphaUVar (Alpha valVars tyVars uVars) uVar1 uVar2
  = Alpha valVars tyVars (addToFM uVars uVar1 uVar2)

Binder and Binding


cmpModAlphaBinder :: (Ord valVar, Ord tyVar, Ord uVar)
                  => Alpha valVar tyVar uVar
                  -> GenCoreBinder valVar tyVar uVar 
                  -> GenCoreBinder valVar tyVar uVar 
                  -> (_CMP_TAG, Alpha valVar tyVar uVar)

cmpModAlphaBinder alpha  (ValBinder valBdr1) (ValBinder valBdr2)
  = (_EQ, addToAlphaValVar alpha valBdr1 valBdr2)
cmpModAlphaBinder alpha  (TyBinder tyVar1) (TyBinder tyVar2)
  = (_EQ, addToAlphaTyVar alpha tyVar1 tyVar2)
cmpModAlphaBinder alpha  (UsageBinder uVar1) (UsageBinder uVar2)
  = (_EQ, addToAlphaUVar alpha uVar1 uVar2)
cmpModAlphaBinder alpha _ _ = (_LT, alpha)



cmpModAlphaBinding :: (Ord valVar, Ord tyVar, Ord uVar)
                   => Alpha valVar tyVar uVar
                   -> GenCoreBinding valVar valVar tyVar uVar
                   -> GenCoreBinding valVar valVar tyVar uVar
                   -> (_CMP_TAG, Alpha valVar tyVar uVar)

cmpModAlphaBinding alpha binding1 binding2
  = ( lexicalCmp (cmpModAlphaExpr alpha') 
        (rhssOfBind binding1) (rhssOfBind binding2)
    , alpha' 
    )
    where
    alpha' = foldl add alpha (zip (bindersOf binding1) (bindersOf binding2))
    add :: (Ord valVar, Ord tyVar, Ord uVar) 
        => Alpha valVar tyVar uVar 
        -> (valVar, valVar) 
        -> Alpha valVar tyVar uVar
    add alpha (valVar1, valVar2) = addToAlphaValVar alpha valVar1 valVar2

Problem with classes

Would like to have something like that:


class CmpModAlpha term uVar tyVar valVar where
  cmpModAlpha :: Alpha valVar tyVar uVar  
              -> term 
              -> term
              -> _CMP_TAG 

instance Ord valVar => CmpModAlpha (valVar)  valVar tyVar uVar where ...
instance Ord tyVar  => CmpModAlpha (tyVar)   valVar tyVar uVar where ...
instance Ord uVar   => CmpModAlpha (uVar)    valVar tyVar uVar where ...

instance CmpModAlpha term uVar tyVar valVar 
      => CmpModAlpha [term] uVar tyVar valVar where ...
  
instance ( CmpModAlpha (valVar) valVar tyVar uVar
         , CmpModAlpha (GenCoreArg valVar tyVar uVar) valVar tyVar uVar
         , CmpModAlpha (GenCoreBinder valVar tyVar uVar) valVar tyVar uVar
         , CmpModAlpha (GenCoreCaseAlts valVar valVar tyVar uVar) valVar tyVar uVar
         , CmpModAlpha (GenType tyVar uVar) valVar tyVar uVar)
      => CmpModAlpha (GenCoreExpr valVar valVar tyVar uVar) valVar tyVar uVar
   where
   ...

instance ( CmpModAlpha (valVar) valVar tyVar uVar
         , CmpModAlpha (tyVar)  valVar tyVar uVar
         , CmpModAlpha (uVar)   valVar tyVar uVar)
      => CmpModAlpha (GenCoreBinder valVar tyVar uVar) valVar tyVar uVar

...

Various kinds of variables


cmpModAlphaValVar :: Ord valVar 
                   => Alpha valVar tyVar uVar -> valVar -> valVar -> _CMP_TAG

cmpModAlphaValVar (Alpha valVars tyVars uVars) valVar1 valVar2
  = case lookupFM valVars valVar1 of
      Nothing     -> _tagCmp valVar1 valVar2 -- valVar1 is global variable
      Just valVar -> _tagCmp valVar valVar2  -- valVar1 is local variable


cmpModAlphaTyVar :: Ord tyVar 
                  => Alpha valVar tyVar uVar -> tyVar -> tyVar -> _CMP_TAG

cmpModAlphaTyVar (Alpha valVars tyVars uVars) tyVar1 tyVar2
  = case lookupFM tyVars tyVar1 of
      Nothing    -> _tagCmp tyVar1 tyVar2 -- tyVar1 is global variable
      Just tyVar -> _tagCmp tyVar tyVar2  -- tyVar1 is local variable


cmpModAlphaUVar :: Ord uVar 
                 => Alpha valVar tyVar uVar -> uVar -> uVar -> _CMP_TAG
cmpModAlphaUVar (Alpha valVars tyVars uVars) uVar1 uVar2
  = case lookupFM uVars uVar1 of
      Nothing   -> _tagCmp uVar1 uVar2 -- uVar1 is global variable
      Just uVar -> _tagCmp uVar uVar2  -- uVar1 is local variable

Expressions

Unfortunately there don't yet exist instances of Ord. It would make defining the following function much easier and shorter


cmpModAlphaExpr :: (Ord valVar, Ord tyVar, Ord uVar)
                 => Alpha valVar tyVar uVar
                 -> GenCoreExpr valVar valVar tyVar uVar
                 -> GenCoreExpr valVar valVar tyVar uVar
                 -> _CMP_TAG            

cmpModAlphaExpr alpha (Var var1) (Var var2) 
  = cmpModAlphaValVar alpha var1 var2
cmpModAlphaExpr alpha (Var _) _ = _LT

cmpModAlphaExpr alpha (Lit lit1) (Lit lit2) = _tagCmp lit1 lit2
cmpModAlphaExpr alpha (Lit _) (Var _) = _GT
cmpModAlphaExpr alpha (Lit _) _       = _LT

cmpModAlphaExpr alpha (Con conId1 args1) (Con conId2 args2)
  = _tagCmp conId1 conId2 `thenCmp` -- constructors are directly compared
   lexicalCmp (cmpModAlphaArg alpha) args1 args2
cmpModAlphaExpr alpha (Con _ _) (Var _) = _GT
cmpModAlphaExpr alpha (Con _ _) (Lit _) = _GT
cmpModAlphaExpr alpha (Con _ _) _       = _LT  

cmpModAlphaExpr alpha (Prim primOp1 args1) (Prim primOp2 args2)
  | (tagOf_PrimOp primOp1) _EQ_ (tagOf_PrimOp primOp2) 
    = lexicalCmp (cmpModAlphaArg alpha) args1 args2
  | (tagOf_PrimOp primOp1) _LT_ (tagOf_PrimOp primOp2)
    = _LT
  | otherwise
    = _GT
cmpModAlphaExpr alpha (Prim _ _) (Var _)   = _GT
cmpModAlphaExpr alpha (Prim _ _) (Lit _)   = _GT
cmpModAlphaExpr alpha (Prim _ _) (Con _ _) = _GT
cmpModAlphaExpr alpha (Prim _ _) _         = _LT
  
cmpModAlphaExpr alpha (Lam binder1 expr1) (Lam binder2 expr2)
  = cmp `thenCmp` cmpModAlphaExpr alpha' expr1 expr2
    where
    (cmp, alpha') = cmpModAlphaBinder alpha binder1 binder2
cmpModAlphaExpr alpha (Lam _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Lam _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Lam _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Lam _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Lam _ _) _          = _LT

cmpModAlphaExpr alpha (App fun1 arg1) (App fun2 arg2)
  = cmpModAlphaExpr alpha fun1 fun2 `thenCmp` cmpModAlphaArg alpha arg1 arg2
cmpModAlphaExpr alpha (App _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (App _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (App _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (App _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (App _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (App _ _) _          = _LT

cmpModAlphaExpr alpha (Case expr1 alts1) (Case expr2 alts2)
  = cmpModAlphaExpr alpha expr1 expr2 `thenCmp` 
    cmpModAlphaCaseAlts alpha alts1 alts2
cmpModAlphaExpr alpha (Case _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Case _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Case _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Case _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Case _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (Case _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (Case _ _) _          = _LT

cmpModAlphaExpr alpha (Let binder1 expr1) (Let binder2 expr2)
  = cmp `thenCmp` cmpModAlphaExpr alpha' expr1 expr2
    where
    (cmp, alpha') = cmpModAlphaBinding alpha binder1 binder2
cmpModAlphaExpr alpha (Let _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Let _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Let _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Let _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Let _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (Let _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (Let _ _) (Case _ _) = _GT
cmpModAlphaExpr alpha (Let _ _) _          = _LT

-- does comparing cost centres make sense? should possibly be always unequal!
-- danger: order is not antisymmetric: x _GT y and y _GT x
cmpModAlphaExpr alpha (SCC costCentre1 expr1) (SCC costCentre2 expr2) = _GT
cmpModAlphaExpr alpha (SCC _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (SCC _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (SCC _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (SCC _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) (Case _ _) = _GT
cmpModAlphaExpr alpha (SCC _ _) (Let _ _)  = _GT
cmpModAlphaExpr alpha (SCC _ _) _          = _LT

cmpModAlphaExpr alpha (Coerce coercion1 typeExpr1 expr1) 
                       (Coerce coercion2 typeExpr2 expr2)
  = _tagCmp coercion1 coercion2 `thenCmp`
    cmpModAlphaType alpha typeExpr1 typeExpr2 `thenCmp`
    cmpModAlphaExpr alpha expr1 expr2 
cmpModAlphaExpr alpha (Coerce _ _ _) (Var _)    = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Lit _)    = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Con _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Prim _ _) = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Lam _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (App _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Case _ _) = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (Let _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) (SCC _ _)  = _GT
cmpModAlphaExpr alpha (Coerce _ _ _) _          = _LT

Case expressions


cmpModAlphaCaseAlts :: (Ord valVar, Ord tyVar, Ord uVar)
                     => Alpha valVar tyVar uVar
                     -> GenCoreCaseAlts valVar valVar tyVar uVar
                     -> GenCoreCaseAlts valVar valVar tyVar uVar
                     -> _CMP_TAG
-- alternatives have to be in the same order

cmpModAlphaCaseAlts alpha (AlgAlts alts1 deflt1) (AlgAlts alts2 deflt2)
  = lexicalCmp (cmpModAlphaArgTriple alpha) alts1 alts2 `thenCmp`
    cmpModAlphaCaseDefault alpha deflt1 deflt2        
cmpModAlphaCaseAlts alpha (AlgAlts alts1 deflt1) _ = _LT
cmpModAlphaCaseAlts alpha (PrimAlts alts1 deflt1) (PrimAlts alts2 deflt2)
  = lexicalCmp (cmpModAlphaArgPair alpha) alts1 alts2 `thenCmp`
    cmpModAlphaCaseDefault alpha deflt1 deflt2
cmpModAlphaCaseAlts alpha (PrimAlts _ _) (AlgAlts _ _) = _GT
cmpModAlphaCaseAlts alpha (PrimAlts _ _) _             = _LT


cmpModAlphaArgTriple :: (Ord valVar, Ord tyVar, Ord uVar)
                     => Alpha valVar tyVar uVar
                     -> (Id, [valVar], GenCoreExpr valVar valVar tyVar uVar)
                     -> (Id, [valVar], GenCoreExpr valVar valVar tyVar uVar)
                     -> _CMP_TAG

cmpModAlphaArgTriple alpha (id1, valVars1, expr1) (id2, valVars2, expr2)
  = _tagCmp id1 id2 `thenCmp`
    cmpModAlphaExpr alpha' expr1 expr2
  where
  alpha' = foldl add alpha (zip valVars1 valVars2)
  add :: (Ord valVar, Ord tyVar, Ord uVar) 
      => Alpha valVar tyVar uVar 
      -> (valVar, valVar) 
      -> Alpha valVar tyVar uVar
  add alpha (valVar1, valVar2) = addToAlphaValVar alpha valVar1 valVar2


cmpModAlphaArgPair :: (Ord valVar, Ord tyVar, Ord uVar)
                   => Alpha valVar tyVar uVar
                   -> (Literal, GenCoreExpr valVar valVar tyVar uVar)
                   -> (Literal, GenCoreExpr valVar valVar tyVar uVar)
                   -> _CMP_TAG

cmpModAlphaArgPair alpha (lit1, expr1) (lit2, expr2)
  = _tagCmp lit1 lit2 `thenCmp`
    cmpModAlphaExpr alpha expr1 expr2



cmpModAlphaCaseDefault :: (Ord valVar, Ord tyVar, Ord uVar)
                        => Alpha valVar tyVar uVar
                        -> GenCoreCaseDefault valVar valVar tyVar uVar
                        -> GenCoreCaseDefault valVar valVar tyVar uVar
                        -> _CMP_TAG

cmpModAlphaCaseDefault alpha NoDefault NoDefault = _EQ
cmpModAlphaCaseDefault alpha NoDefault _         = _LT
cmpModAlphaCaseDefault alpha (BindDefault valBdr1 expr1) 
                             (BindDefault valBdr2 expr2)
  = cmpModAlphaExpr (addToAlphaValVar alpha valBdr1 valBdr2) expr1 expr2
cmpModAlphaCaseDefault alpha (BindDefault _ _) NoDefault = _GT

Arguments


cmpModAlphaArg :: (Ord valVar, Ord tyVar, Ord uVar)
               => Alpha valVar tyVar uVar
               -> GenCoreArg valVar tyVar uVar
               -> GenCoreArg valVar tyVar uVar
               -> _CMP_TAG

cmpModAlphaArg alpha (LitArg lit1) (LitArg lit2)
  = _tagCmp lit1 lit2 
cmpModAlphaArg alpha (LitArg _) _ = _LT
cmpModAlphaArg alpha (VarArg valVar1) (VarArg valVar2)
  = cmpModAlphaValVar alpha valVar1 valVar2
cmpModAlphaArg alpha (VarArg _) (LitArg _) = _GT
cmpModAlphaArg alpha (VarArg _) _          = _LT
cmpModAlphaArg alpha (TyArg type1) (TyArg type2)
  = cmpModAlphaType alpha type1 type2
cmpModAlphaArg alpha (TyArg _) (VarArg _) = _GT
cmpModAlphaArg alpha (TyArg _) (LitArg _) = _GT
cmpModAlphaArg alpha (TyArg _) _          = _LT
cmpModAlphaArg alpha (UsageArg usage1) (UsageArg usage2)
  = cmpModAlphaUsage alpha usage1 usage2
cmpModAlphaArg alpha (UsageArg _) (VarArg _) = _GT
cmpModAlphaArg alpha (UsageArg _) (LitArg _) = _GT
cmpModAlphaArg alpha (UsageArg _) (TyArg _)  = _GT
cmpModAlphaArg alpha (UsageArg _) _          = _LT

Types

Compare for definition of eqTy in module Type.


cmpModAlphaType :: (Ord tyVar, Ord uVar)
                => Alpha valVar tyVar uVar
                -> GenType tyVar uVar
                -> GenType tyVar uVar
                -> _CMP_TAG

cmpModAlphaType alpha (TyVarTy tyVar1) (TyVarTy tyVar2)
  = cmpModAlphaTyVar alpha tyVar1 tyVar2
cmpModAlphaType alpha (TyVarTy tyVar1) _ = _LT

cmpModAlphaType alpha (AppTy type11 type12) (AppTy type21 type22)
  = cmpModAlphaType alpha type11 type21 `thenCmp`
    cmpModAlphaType alpha type12 type22 
cmpModAlphaType alpha type1@(AppTy _ _) (FunTy type21 type22 usage2)
  -- expand function type just in case that version matches
  = cmpModAlphaType alpha type1 
      (AppTy (AppTy (TyConTy mkFunTyCon usage2) type21) type22)
cmpModAlphaType alpha (AppTy _ _) (TyVarTy _) = _GT
cmpModAlphaType alpha (AppTy _ _) _           = _LT
 
cmpModAlphaType alpha (TyConTy tyCon1 usage1) (TyConTy tyCon2 usage2)
  = _tagCmp tyCon1 tyCon2 `thenCmp`
    cmpModAlphaUsage alpha usage1 usage2
cmpModAlphaType alpha (TyConTy _ _) (TyVarTy _) = _GT
cmpModAlphaType alpha (TyConTy _ _) (AppTy _ _) = _GT
cmpModAlphaType alpha (TyConTy _ _) _           = _LT

cmpModAlphaType alpha (SynTy tyCon1 args1 expType1) 
                      (SynTy tyCon2 args2 expType2)
  = case _tagCmp tyCon1 tyCon2 `thenCmp` 
         lexicalCmp (cmpModAlphaType alpha) args1 args2 of
      _EQ -> _EQ
      _   -> cmpModAlphaType alpha expType1 expType2
cmpModAlphaType alpha (SynTy _ _ _) (TyVarTy _)   = _GT
cmpModAlphaType alpha (SynTy _ _ _) (AppTy _ _)   = _GT
cmpModAlphaType alpha (SynTy _ _ _) (TyConTy _ _) = _GT
cmpModAlphaType alpha (SynTy _ _ _) _             = _LT

cmpModAlphaType alpha (ForAllTy tyVar1 type1) (ForAllTy tyVar2 type2)
  = cmpModAlphaType (addToAlphaTyVar alpha tyVar1 tyVar2) type1 type2
cmpModAlphaType alpha (ForAllTy _ _) (TyVarTy _)   = _GT
cmpModAlphaType alpha (ForAllTy _ _) (AppTy _ _)   = _GT
cmpModAlphaType alpha (ForAllTy _ _) (TyConTy _ _) = _GT
cmpModAlphaType alpha (ForAllTy _ _) (SynTy _ _ _) = _GT
cmpModAlphaType alpha (ForAllTy _ _) _             = _LT

cmpModAlphaType alpha (ForAllUsageTy uVar1 bUsages1 type1)
                      (ForAllUsageTy uVar2 bUsages2 type2)
  = lexicalCmp (cmpModAlphaUVar alpha) bUsages1 bUsages2 `thenCmp`
    cmpModAlphaType (addToAlphaUVar alpha uVar1 uVar2) type1 type2
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (TyVarTy _)    = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (AppTy _ _)    = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (TyConTy _ _)  = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (SynTy _ _ _)  = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) (ForAllTy _ _) = _GT
cmpModAlphaType alpha (ForAllUsageTy _ _ _) _              = _LT

cmpModAlphaType alpha (FunTy type11 type12 usage1)
                      (FunTy type21 type22 usage2)
  = cmpModAlphaType alpha type11 type21 `thenCmp`
    cmpModAlphaType alpha type12 type22 `thenCmp`
    cmpModAlphaUsage alpha usage1 usage2
cmpModAlphaType alpha (FunTy type11 type12 usage1) type2@(AppTy _ _)
  -- expand function type just in case that version matches
  = cmpModAlphaType alpha 
      (AppTy (AppTy (TyConTy mkFunTyCon usage1) type11) type12) type2
cmpModAlphaType alpha (FunTy _ _ _) (TyVarTy _)           = _GT
cmpModAlphaType alpha (FunTy _ _ _) (TyConTy _ _)         = _GT
cmpModAlphaType alpha (FunTy _ _ _) (SynTy _ _ _)         = _GT
cmpModAlphaType alpha (FunTy _ _ _) (ForAllTy _ _)        = _GT
cmpModAlphaType alpha (FunTy _ _ _) (ForAllUsageTy _ _ _) = _GT
cmpModAlphaType alpha (FunTy _ _ _) _                     = _LT

cmpModAlphaType alpha (DictTy class1 type1 usage1)      
                      (DictTy class2 type2 usage2)
  = _tagCmp class1 class2 `thenCmp` 
    cmpModAlphaType alpha type1 type2 `thenCmp`
    cmpModAlphaUsage alpha usage1 usage2
  -- expansion too complicated
{-
  -- NB we use a guard for c1==c2 so that if they aren't equal we
  -- fall through into expanding the type. 
cmpModAlphaType alpha type1@(DictTy _ _ _) type2
  = cmpModAlphaType alpha (expandTy type1) type2
cmpModAlphaType alpha type1 type2@(DictTy _ _ _)
  = cmpModAlphaType alpha type1 (expandTy type2)
-}
cmpModAlphaType alpha (DictTy _ _ _) (TyVarTy _)           = _GT
cmpModAlphaType alpha (DictTy _ _ _) (AppTy _ _)           = _GT
cmpModAlphaType alpha (DictTy _ _ _) (TyConTy _ _)         = _GT
cmpModAlphaType alpha (DictTy _ _ _) (SynTy _ _ _)         = _GT
cmpModAlphaType alpha (DictTy _ _ _) (ForAllTy _ _)        = _GT
cmpModAlphaType alpha (DictTy _ _ _) (ForAllUsageTy _ _ _) = _GT
cmpModAlphaType alpha (DictTy _ _ _) (FunTy _ _ _)         = _GT
cmpModAlphaType alpha (DictTy _ _ _) _                     = _LT

Usages


cmpModAlphaUsage :: Ord uVar
                 => Alpha valVar tyVar uVar
                 -> GenUsage uVar
                 -> GenUsage uVar
                 -> _CMP_TAG

cmpModAlphaUsage alpha (UsageVar uVar1) (UsageVar uVar2)
  = cmpModAlphaUVar alpha uVar1 uVar2
cmpModAlphaUsage alpha (UsageVar _) _ = _LT
cmpModAlphaUsage alpha UsageOne UsageOne     = _EQ
cmpModAlphaUsage alpha UsageOne (UsageVar _) = _GT
cmpModAlphaUsage alpha UsageOne _            = _LT
cmpModAlphaUsage alpha UsageOmega UsageOmega   = _EQ
cmpModAlphaUsage alpha UsageOmega (UsageVar _) = _GT
cmpModAlphaUsage alpha UsageOmega UsageOne     = _GT
cmpModAlphaUsage alpha UsageOmega _            = _LT

Generated by Olaf Chitil using lit2html
Valid HTML 4.01 Strict! Valid CSS!