| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE GADTs, TypeOperators, TypeSynonymInstances #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.R.Syntax | ||
| 9 | Description : Representation of the expressions used by Galculator, namely | ||
| 10 | relations, functions, orders and Galois connections. | ||
| 11 | Copyright : (c) Paulo Silva | ||
| 12 | License : LGPL | ||
| 13 | |||
| 14 | Maintainer : paufil@di.uminho.pt | ||
| 15 | Stability : experimental | ||
| 16 | Portability : portable | ||
| 17 | |||
| 18 | -} | ||
| 19 | |||
| 20 | ------------------------------------------------------------------------------- | ||
| 21 | |||
| 22 | module Language.R.Syntax ( | ||
| 23 | R(..), | ||
| 24 | RType | ||
| 25 | ) where | ||
| 26 | |||
| 27 | import Data.Existential | ||
| 28 | import Data.Map(Map) | ||
| 29 | import Data.Set(Set) | ||
| 30 | import Language.R.Equality | ||
| 31 | import Language.R.Pretty | ||
| 32 | import Language.Type.Equality | ||
| 33 | import Language.Type.Syntax | ||
| 34 | |||
| 35 | ------------------------------------------------------------------------------- | ||
| 36 | |||
| 37 | -- | Relational representation | ||
| 38 | data R r where | ||
| 39 | BOT :: R (b :<->: a) | ||
| 40 | TOP :: R (b :<->: a) | ||
| 41 | NEG :: R (b :<->: a) -> R (b :<->: a) | ||
| 42 | MEET :: R (b :<->: a) -> R (b :<->: a) -> R (b :<->: a) | ||
| 43 | JOIN :: R (b :<->: a) -> R (b :<->: a) -> R (b :<->: a) | ||
| 44 | ID :: R (a :<->: a) | ||
| 45 | CONV :: R (b :<->: a) -> R (a :<->: b) | ||
| 46 | COMP :: Type b -> R (c :<->: b) -> R (b :<->: a) -> R (c :<->: a) | ||
| 47 | SPLIT :: R (b :<->: a) -> R (c :<->: a) -> R ((b,c) :<->: a) | ||
| 48 | |||
| 49 | ORD :: R (PO a) -> R (a :<->: a) | ||
| 50 | FUN :: R (b :<-: a) -> R (b :<->: a) | ||
| 51 | |||
| 52 | LEFTSEC :: Type b -> R (a :<-: (b,c)) -> R b -> R (a :<-: c) | ||
| 53 | RIGHTSEC :: Type c -> R (a :<-: (b,c)) -> R c -> R (a :<-: b) | ||
| 54 | |||
| 55 | APPLY :: Type b -> R (a :<-: b) -> R b -> R a | ||
| 56 | DEF :: Name -> Type a -> R a | ||
| 57 | Var :: Name -> R a | ||
| 58 | |||
| 59 | PROD :: R (b :<->: a) -> R (d :<->: c) -> R ((b,d) :<->: (a,c)) | ||
| 60 | EITHER :: R (b :<->: a) -> R (d :<->: c) -> R (Either b d :<->: Either a c) | ||
| 61 | MAYBE :: R (b :<->: a) -> R (Maybe b :<->: Maybe a) | ||
| 62 | LIST :: R (b :<->: a) -> R ([b] :<->: [a]) | ||
| 63 | SET :: R (b :<->: a) -> R (Set b :<->: Set a) | ||
| 64 | MAP :: R (b :<->: a) -> R (Map k b :<->: Map k a) | ||
| 65 | |||
| 66 | 5 | paulosilva | REYNOLDS :: R (b :<->: a) -> R (d :<->: c) -> R ((b :<-: d) :<->: (a :<-: c)) |
| 67 | |||
| 68 | 1 | paulosilva | FId :: R (a :<-: a) |
| 69 | FComp :: Type b -> R (c :<-: b) -> R (b :<-: a) -> R (c :<-: a) | ||
| 70 | |||
| 71 | OId :: R (PO a) | ||
| 72 | OComp :: R (PO a) -> R (PO a) -> R (PO a) | ||
| 73 | OConv :: R (PO a) -> R (PO a) | ||
| 74 | OProd :: R (PO a) -> R (PO (a,a)) | ||
| 75 | |||
| 76 | OJoin :: R (PO a) -> R (a :<-: (a,a)) | ||
| 77 | OMeet :: R (PO a) -> R (a :<-: (a,a)) | ||
| 78 | OMax :: R (PO a) -> R a | ||
| 79 | OMin :: R (PO a) -> R a | ||
| 80 | |||
| 81 | GDef :: Name | ||
| 82 | -> R (b :<-: a) -> R (a :<-: b) | ||
| 83 | -> R (PO b) -> R (PO a) | ||
| 84 | -> R (GC b a) | ||
| 85 | |||
| 86 | GId :: R (GC a a) | ||
| 87 | GComp :: Type b -> R (GC c b) -> R (GC b a) -> R (GC c a) | ||
| 88 | GConv :: R (GC b a) -> R (GC a b) | ||
| 89 | |||
| 90 | GLAdj :: R (GC b a) -> R (b :<-: a) | ||
| 91 | GUAdj :: R (GC b a) -> R (a :<-: b) | ||
| 92 | GLOrd :: Type a -> R (GC b a) -> R (PO b) | ||
| 93 | GUOrd :: Type b -> R (GC b a) -> R (PO a) | ||
| 94 | |||
| 95 | ------------------------------------------------------------------------------- | ||
| 96 | |||
| 97 | instance Show (R r) where | ||
| 98 | showsPrec _ = showR | ||
| 99 | |||
| 100 | ------------------------------------------------------------------------------- | ||
| 101 | |||
| 102 | instance Eq (R a) where | ||
| 103 | r1 == r2 = req r1 r2 | ||
| 104 | |||
| 105 | ------------------------------------------------------------------------------- | ||
| 106 | |||
| 107 | type RType = Exists Type R | ||
| 108 | |||
| 109 | ------------------------------------------------------------------------------- | ||
| 110 | |||
| 111 | instance Show RType where | ||
| 112 | show (Exists t a) = show a ++ " :: " ++ show t | ||
| 113 | |||
| 114 | ------------------------------------------------------------------------------- | ||
| 115 | |||
| 116 | instance Eq RType where | ||
| 117 | (Exists t r) == (Exists t' r') = beq t t' && req r r' | ||
| 118 | |||
| 119 | ------------------------------------------------------------------------------- | ||
| 120 |