| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE GADTs #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.R.Spine | ||
| 9 | Description : Spine representation for the expression representation. | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | -} | ||
| 18 | |||
| 19 | ------------------------------------------------------------------------------- | ||
| 20 | |||
| 21 | module Language.R.Spine ( | ||
| 22 | Typed((:|)), | ||
| 23 | Spine(Constr,Ap), | ||
| 24 | fromSpine, | ||
| 25 | toSpine | ||
| 26 | ) where | ||
| 27 | |||
| 28 | import Language.R.Syntax | ||
| 29 | import Language.Type.Syntax | ||
| 30 | |||
| 31 | ------------------------------------------------------------------------------- | ||
| 32 | |||
| 33 | data Typed a where | ||
| 34 | (:|) :: Type a -> R a -> Typed (R a) | ||
| 35 | |||
| 36 | data Spine a where | ||
| 37 | Constr :: a -> Spine a | ||
| 38 | Ap :: Spine (a -> b) -> Typed a -> Spine b | ||
| 39 | |||
| 40 | ------------------------------------------------------------------------------- | ||
| 41 | |||
| 42 | fromSpine :: Spine a -> a | ||
| 43 | fromSpine (Constr c) = c | ||
| 44 | fromSpine (f `Ap` (_:| a)) = (fromSpine f) a | ||
| 45 | |||
| 46 | ------------------------------------------------------------------------------- | ||
| 47 | toSpine :: Type a -> R a -> Spine (R a) | ||
| 48 | toSpine (Rel _ _) BOT = Constr BOT | ||
| 49 | toSpine (Rel _ _) TOP = Constr TOP | ||
| 50 | toSpine (Rel b a) (NEG r) = | ||
| 51 | (Constr NEG) `Ap` (Rel b a :| r) | ||
| 52 | toSpine (Rel b a) (MEET r s) = | ||
| 53 | ((Constr MEET) `Ap` (Rel b a :| r)) `Ap` (Rel b a :| s) | ||
| 54 | toSpine (Rel b a) (JOIN r s) = | ||
| 55 | ((Constr JOIN) `Ap` (Rel b a :| r)) `Ap` (Rel b a :| s) | ||
| 56 | toSpine (Rel _ _) ID = Constr ID | ||
| 57 | toSpine (Rel b a) (CONV r) = | ||
| 58 | (Constr CONV) `Ap` (Rel a b :| r) | ||
| 59 | toSpine (Rel c a) (COMP b r s) = | ||
| 60 | ((Constr (COMP b)) `Ap` (Rel c b :| r)) `Ap` (Rel b a :| s) | ||
| 61 | toSpine (Rel (Prod c b) a) (SPLIT r s) = | ||
| 62 | ((Constr SPLIT) `Ap` (Rel c a :| r)) `Ap` (Rel b a :| s) | ||
| 63 | toSpine (Rel a _) (ORD p) = | ||
| 64 | (Constr ORD) `Ap` (Ord a :| p) | ||
| 65 | toSpine (Rel b a) (FUN f) = | ||
| 66 | (Constr FUN) `Ap` (Fun b a :| f) | ||
| 67 | toSpine (Fun a c) (LEFTSEC b f s) = | ||
| 68 | ((Constr (LEFTSEC b)) `Ap` (Fun a (Prod b c) :| f)) `Ap` (b :| s) | ||
| 69 | toSpine (Fun a b) (RIGHTSEC c f s) = | ||
| 70 | ((Constr (RIGHTSEC c)) `Ap` (Fun a (Prod b c) :| f)) `Ap` (c :| s) | ||
| 71 | toSpine a (APPLY b r v) = | ||
| 72 | ((Constr (APPLY b)) `Ap` (Fun a b :| r)) `Ap` (b :| v) | ||
| 73 | toSpine _ v@(DEF _ _) = Constr v | ||
| 74 | toSpine _ v@(Var _) = Constr v | ||
| 75 | toSpine (Rel (Prod d b) (Prod c a)) (PROD r s) = | ||
| 76 | ((Constr PROD) `Ap` (Rel d c :| r)) `Ap` (Rel b a :| s) | ||
| 77 | toSpine (Rel (Either d b) (Either c a)) (EITHER r s) = | ||
| 78 | ((Constr EITHER) `Ap` (Rel d c :| r)) `Ap` (Rel b a :| s) | ||
| 79 | toSpine (Rel (Maybe b) (Maybe a)) (MAYBE r) = | ||
| 80 | (Constr MAYBE) `Ap` (Rel b a :| r) | ||
| 81 | toSpine (Rel (List b) (List a)) (LIST r) = | ||
| 82 | (Constr LIST) `Ap` (Rel b a :| r) | ||
| 83 | toSpine (Rel (Set b) (Set a)) (SET r) = | ||
| 84 | (Constr SET) `Ap` (Rel b a :| r) | ||
| 85 | toSpine (Rel (Map _ b) (Map _ a)) (MAP r) = | ||
| 86 | (Constr MAP) `Ap` (Rel b a :| r) | ||
| 87 | 5 | paulosilva | toSpine (Rel (Fun b d) (Fun a c)) (REYNOLDS r s) = |
| 88 | ((Constr REYNOLDS) `Ap` (Rel b a :| r)) `Ap` (Rel d c :| s) | ||
| 89 | 1 | paulosilva | toSpine _ FId = Constr FId |
| 90 | toSpine (Fun c a) (FComp b f g) = | ||
| 91 | ((Constr (FComp b)) `Ap` (Fun c b :| f)) `Ap` (Fun b a :| g) | ||
| 92 | toSpine (Ord _) OId = Constr OId | ||
| 93 | toSpine (Ord a) (OComp o1 o2) = | ||
| 94 | ((Constr OComp) `Ap` (Ord a :| o1)) `Ap` (Ord a :| o2) | ||
| 95 | toSpine (Ord a) (OConv o) = | ||
| 96 | (Constr OConv) `Ap` (Ord a :| o) | ||
| 97 | toSpine (Ord (Prod a _)) (OProd o) = | ||
| 98 | (Constr OProd) `Ap` (Ord a :| o) | ||
| 99 | toSpine (Fun a (Prod _ _)) (OJoin o) = | ||
| 100 | (Constr OJoin) `Ap` (Ord a :| o) | ||
| 101 | toSpine (Fun a (Prod _ _)) (OMeet o) = | ||
| 102 | (Constr OMeet) `Ap` (Ord a :| o) | ||
| 103 | toSpine a (OMax o) = | ||
| 104 | (Constr OMax) `Ap` (Ord a :| o) | ||
| 105 | toSpine a (OMin o) = | ||
| 106 | (Constr OMin) `Ap` (Ord a :| o) | ||
| 107 | -- Galois connections | ||
| 108 | toSpine (GC b a) (GDef name f g fo go) = | ||
| 109 | ((((Constr (GDef name)) `Ap` | ||
| 110 | (Fun b a :| f)) `Ap` | ||
| 111 | (Fun a b :| g)) `Ap` | ||
| 112 | (Ord b :| fo)) `Ap` | ||
| 113 | (Ord a :| go) | ||
| 114 | toSpine (GC _ _) GId = Constr GId | ||
| 115 | toSpine (GC c a) (GComp b g1 g2) = | ||
| 116 | ((Constr (GComp b)) `Ap` (GC c b :| g1)) `Ap` (GC b a :| g2) | ||
| 117 | toSpine (GC a b) (GConv g) = | ||
| 118 | (Constr GConv) `Ap` (GC b a :| g) | ||
| 119 | toSpine (Fun b a) (GLAdj f) = | ||
| 120 | (Constr GLAdj) `Ap` (GC b a :| f) | ||
| 121 | toSpine (Fun a b) (GUAdj f) = | ||
| 122 | (Constr GUAdj) `Ap` (GC b a :| f) | ||
| 123 | toSpine (Ord b) (GLOrd a o) = | ||
| 124 | (Constr (GLOrd a)) `Ap` (GC b a :| o) | ||
| 125 | toSpine (Ord a) (GUOrd b o) = | ||
| 126 | (Constr (GUOrd b)) `Ap` (GC b a :| o) | ||
| 127 | -- Missing cases | ||
| 128 | toSpine t a = error $ "toSpine missing case for " ++ show t ++ " :| " ++ show a | ||
| 129 | ------------------------------------------------------------------------------- |