| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# OPTIONS_GHC -Wall #-} | ||
| 3 | |||
| 4 | ------------------------------------------------------------------------------- | ||
| 5 | |||
| 6 | {- | | ||
| 7 | Module : Language.R.Equality | ||
| 8 | Description : Equality over the expression representations. | ||
| 9 | Copyright : (c) Paulo Silva | ||
| 10 | License : LGPL | ||
| 11 | |||
| 12 | Maintainer : paufil@di.uminho.pt | ||
| 13 | Stability : experimental | ||
| 14 | Portability : portable | ||
| 15 | |||
| 16 | -} | ||
| 17 | |||
| 18 | ------------------------------------------------------------------------------- | ||
| 19 | |||
| 20 | |||
| 21 | module Language.R.Equality ( | ||
| 22 | req | ||
| 23 | ) where | ||
| 24 | |||
| 25 | import {-# SOURCE #-} Language.R.Syntax | ||
| 26 | import Language.Type.Equality | ||
| 27 | |||
| 28 | ------------------------------------------------------------------------------- | ||
| 29 | req :: R a -> R b -> Bool | ||
| 30 | req BOT BOT = True | ||
| 31 | req TOP TOP = True | ||
| 32 | req (NEG r) (NEG r') = req r r' | ||
| 33 | req (MEET r s) (MEET r' s') = | ||
| 34 | req r r' && req s s' | ||
| 35 | req (JOIN r s) (JOIN r' s') = | ||
| 36 | req r r' && req s s' | ||
| 37 | req ID ID = True | ||
| 38 | req (CONV r) (CONV r') = req r r' | ||
| 39 | req (COMP b r s) (COMP b' r' s') = | ||
| 40 | beq b b' && req r r' && req s s' | ||
| 41 | req (SPLIT r s) (SPLIT r' s') = | ||
| 42 | req r r' && req s s' | ||
| 43 | req (ORD o) (ORD o') = req o o' | ||
| 44 | req (FUN f) (FUN f') = req f f' | ||
| 45 | req (LEFTSEC t f s) (LEFTSEC t' f' s') = | ||
| 46 | beq t t' && req f f' && req s s' | ||
| 47 | req (RIGHTSEC t f s) (RIGHTSEC t' f' s') = | ||
| 48 | beq t t' && req f f' && req s s' | ||
| 49 | req (APPLY t f v) (APPLY t' f' v') = | ||
| 50 | beq t t' && req f f' && req v v' | ||
| 51 | req (DEF n t) (DEF n' t') = | ||
| 52 | n == n' && beq t t' | ||
| 53 | req (Var n) (Var n') = n == n' | ||
| 54 | |||
| 55 | req (PROD r s) (PROD r' s') = | ||
| 56 | req r r' && req s s' | ||
| 57 | req (EITHER r s) (EITHER r' s') = | ||
| 58 | req r r' && req s s' | ||
| 59 | req (MAYBE r) (MAYBE r') = req r r' | ||
| 60 | req (LIST r) (LIST r') = req r r' | ||
| 61 | req (SET r) (SET r') = req r r' | ||
| 62 | req (MAP r) (MAP r') = req r r' | ||
| 63 | 5 | paulosilva | req (REYNOLDS r s) (REYNOLDS r' s') = |
| 64 | req r r' && req s s' | ||
| 65 | 1 | paulosilva | req FId FId = True |
| 66 | req (FComp t f g) (FComp t' f' g') = | ||
| 67 | beq t t' && req f f' && req g g' | ||
| 68 | |||
| 69 | req OId OId = True | ||
| 70 | req (OComp o1 o2) (OComp o1' o2') = | ||
| 71 | req o1 o1' && req o2 o2' | ||
| 72 | req (OConv o) (OConv o') = req o o' | ||
| 73 | req (OProd o) (OProd o') = req o o' | ||
| 74 | req (OJoin o) (OJoin o') = req o o' | ||
| 75 | req (OMeet o) (OMeet o') = req o o' | ||
| 76 | req (OMax o) (OMax o') = req o o' | ||
| 77 | req (OMin o) (OMin o') = req o o' | ||
| 78 | |||
| 79 | req (GDef n f g fo go) (GDef n' f' g' fo' go') = | ||
| 80 | n == n' && req f f' && req g g' && req fo fo' && req go go' | ||
| 81 | req GId GId = True | ||
| 82 | req (GComp t g1 g2) (GComp t' g1' g2') = | ||
| 83 | beq t t' && req g1 g1' && req g2 g2' | ||
| 84 | req (GConv g) (GConv g') = req g g' | ||
| 85 | req (GLAdj g) (GLAdj g') = req g g' | ||
| 86 | req (GUAdj g) (GUAdj g') = req g g' | ||
| 87 | req (GLOrd t g) (GLOrd t' g') = | ||
| 88 | beq t t' && req g g' | ||
| 89 | req (GUOrd t g) (GUOrd t' g') = | ||
| 90 | beq t t' && req g g' | ||
| 91 | req _ _ = False | ||
| 92 | |||
| 93 | ------------------------------------------------------------------------------- | ||
| 94 |