| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE GADTs, TypeSynonymInstances #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Galculator.Rule | ||
| 9 | Description : | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | <description of the module> | ||
| 17 | |||
| 18 | -} | ||
| 19 | |||
| 20 | ------------------------------------------------------------------------------- | ||
| 21 | |||
| 22 | module Galculator.Rule ( | ||
| 23 | Rule, | ||
| 24 | RewriteStep, | ||
| 25 | rewrite, | ||
| 26 | successEquiv, | ||
| 27 | successImpl | ||
| 28 | ) where | ||
| 29 | |||
| 30 | import Control.MonadOr | ||
| 31 | import Control.MonadPosition | ||
| 32 | import Control.Monad.RWS | ||
| 33 | import Data.Maybe | ||
| 34 | import Language.Law.Syntax | ||
| 35 | import Language.R.Rewrite | ||
| 36 | import Language.R.Syntax | ||
| 37 | import Language.Type.Syntax | ||
| 38 | |||
| 39 | ------------------------------------------------------------------------------- | ||
| 40 | |||
| 41 | type Rule = GenericM Rewrite | ||
| 42 | type Hyp = [String] | ||
| 43 | |||
| 44 | type RewriteSt = Pos | ||
| 45 | type Rewrite = RWST Hyp [RewriteStep] RewriteSt [] | ||
| 46 | |||
| 47 | instance MonadOr Rewrite where | ||
| 48 | morelse (RWST f) (RWST g) = RWST $ \r s -> f r s `morelse` g r s | ||
| 49 | |||
| 50 | instance MonadPosition Rewrite where | ||
| 51 | branchLeft = do | ||
| 52 | st <- get | ||
| 53 | put (0:st) | ||
| 54 | branchRight = do | ||
| 55 | st <- get | ||
| 56 | put (0:st) | ||
| 57 | getPosition = get | ||
| 58 | |||
| 59 | ------------------------------------------------------------------------------- | ||
| 60 | type RewriteStep = (Law, Pos) | ||
| 61 | type Pos = [Int] | ||
| 62 | |||
| 63 | ------------------------------------------------------------------------------- | ||
| 64 | initialState :: [Int] | ||
| 65 | initialState = [] | ||
| 66 | ------------------------------------------------------------------------------- | ||
| 67 | |||
| 68 | rewrite :: Rule -> Type a -> R a -> Maybe ((R a), [RewriteStep]) | ||
| 69 | rewrite r t expr = listToMaybe $ evalRWST (r t expr) [] initialState | ||
| 70 | |||
| 71 | ------------------------------------------------------------------------------- | ||
| 72 | |||
| 73 | successEquiv :: Meta -> Type a -> R a -> R a -> Rewrite (R a) | ||
| 74 | successEquiv m t r r' = do | ||
| 75 | pos <- getPosition | ||
| 76 | tell [(EQUIV m t r r',pos)] | ||
| 77 | return r' | ||
| 78 | |||
| 79 | ------------------------------------------------------------------------------- | ||
| 80 | |||
| 81 | successImpl :: Meta -> Type a -> R a -> R a -> Rewrite (R a) | ||
| 82 | successImpl m t r r' = do | ||
| 83 | pos <- getPosition | ||
| 84 | tell [(IMPL m t r r',pos)] | ||
| 85 | return r' | ||
| 86 | |||
| 87 | ------------------------------------------------------------------------------- | ||
| 88 |