| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE GADTs #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.Law.Syntax | ||
| 9 | Description : | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | <description of the module> | ||
| 18 | -} | ||
| 19 | |||
| 20 | ------------------------------------------------------------------------------- | ||
| 21 | |||
| 22 | module Language.Law.Syntax ( | ||
| 23 | Law(..), | ||
| 24 | RuleType(..), | ||
| 25 | Meta(..), | ||
| 26 | getName, | ||
| 27 | getLeft, | ||
| 28 | 7 | paulosilva | getRight |
| 29 | 1 | paulosilva | ) where |
| 30 | |||
| 31 | import Data.Existential | ||
| 32 | import Language.R.Syntax | ||
| 33 | import Language.Type.Syntax | ||
| 34 | |||
| 35 | ------------------------------------------------------------------------------- | ||
| 36 | |||
| 37 | data Law where | ||
| 38 | EQUIV :: Meta -> Type a -> R a -> R a -> Law | ||
| 39 | IMPL :: Meta -> Type a -> R a -> R a -> Law | ||
| 40 | |||
| 41 | ------------------------------------------------------------------------------- | ||
| 42 | |||
| 43 | instance Show Law where | ||
| 44 | 7 | paulosilva | show (EQUIV m _ r r') = |
| 45 | show r ++ " <=> " ++ show r' ++ " , " ++ show m | ||
| 46 | show (IMPL m _ r r') = | ||
| 47 | show r ++ " => " ++ show r' ++ " , " ++ show m | ||
| 48 | {- | ||
| 49 | 1 | paulosilva | show (EQUIV m _ r r') = |
| 50 | "EQUIV " ++ (name m) ++ " " ++ show r ++ " " ++ show r' | ||
| 51 | show (IMPL m _ r r') = | ||
| 52 | "IMPL " ++ (name m) ++ " " ++ show r ++ " " ++ show r' | ||
| 53 | 7 | paulosilva | -} |
| 54 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 55 | |||
| 56 | data RuleType = | ||
| 57 | ASSOC | ||
| 58 | | COMUT | ||
| 59 | | DISTR | ||
| 60 | | UNIV | ||
| 61 | | IDEMP | ||
| 62 | | INVOL | ||
| 63 | | UNIT | ||
| 64 | | CONTRAV | ||
| 65 | | GCSHUNT | ||
| 66 | | GCCANC | ||
| 67 | | GCMONOT | ||
| 68 | | GCDISTR | ||
| 69 | | GCTOP | ||
| 70 | | GCBOT | ||
| 71 | | DEFINITION | ||
| 72 | | FUSION | ||
| 73 | | ASSUMP | ||
| 74 | | RuleType String | ||
| 75 | |||
| 76 | ------------------------------------------------------------------------------- | ||
| 77 | |||
| 78 | instance Show RuleType where | ||
| 79 | show ASSOC = "Associativity" | ||
| 80 | show COMUT = "Comutativity" | ||
| 81 | show DISTR = "Distributivity" | ||
| 82 | show UNIV = "Universal Property" | ||
| 83 | show IDEMP = "Idempotence" | ||
| 84 | show INVOL = "Involution" | ||
| 85 | show UNIT = "Unit" | ||
| 86 | show CONTRAV = "Contravariance" | ||
| 87 | show GCSHUNT = "Shunting" | ||
| 88 | show GCCANC = "Cancellation" | ||
| 89 | show GCMONOT = "Monotonic" | ||
| 90 | show GCDISTR = "Distributivity" | ||
| 91 | show GCTOP = "Top-preserving" | ||
| 92 | show GCBOT = "Bottom-preserving" | ||
| 93 | show DEFINITION = "Definition" | ||
| 94 | show FUSION = "Fusion" | ||
| 95 | show ASSUMP = "Assumption" | ||
| 96 | show (RuleType nm) = nm | ||
| 97 | |||
| 98 | ------------------------------------------------------------------------------- | ||
| 99 | |||
| 100 | data Meta = Meta { | ||
| 101 | name :: String, | ||
| 102 | ruleType :: Maybe RuleType | ||
| 103 | } | ||
| 104 | |||
| 105 | ------------------------------------------------------------------------------- | ||
| 106 | |||
| 107 | instance Show Meta where | ||
| 108 | show (Meta n (Just tp)) = | ||
| 109 | 7 | paulosilva | "{[" ++ n ++ ": " ++ show tp ++ "]}" |
| 110 | 1 | paulosilva | show (Meta n Nothing) = |
| 111 | 7 | paulosilva | "{[" ++ n ++ "]}" |
| 112 | 1 | paulosilva | |
| 113 | ------------------------------------------------------------------------------- | ||
| 114 | |||
| 115 | getName :: Law -> String | ||
| 116 | getName (EQUIV m _ _ _) = name m | ||
| 117 | getName (IMPL m _ _ _) = name m | ||
| 118 | |||
| 119 | ------------------------------------------------------------------------------- | ||
| 120 | -- | Returns the left expression of a law. | ||
| 121 | -- Refactor? | ||
| 122 | getLeft :: Law -> RType | ||
| 123 | getLeft (EQUIV _ t r _) = Exists t r | ||
| 124 | getLeft (IMPL _ t r _) = Exists t r | ||
| 125 | |||
| 126 | ------------------------------------------------------------------------------- | ||
| 127 | -- | Returns the right expression of a law. | ||
| 128 | getRight :: Law -> RType | ||
| 129 | getRight (EQUIV _ t _ r) = Exists t r | ||
| 130 | getRight (IMPL _ t _ r) = Exists t r | ||
| 131 | |||
| 132 | ------------------------------------------------------------------------------- | ||
| 133 |