| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.Law.Refresh | ||
| 9 | Description : Operations for refreshing the variable names. | ||
| 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.Law.Refresh ( | ||
| 22 | refresh | ||
| 23 | ) where | ||
| 24 | |||
| 25 | import Control.Monad.Fresh | ||
| 26 | import Control.Monad.Reader | ||
| 27 | import Data.List | ||
| 28 | import Language.Law.SyntaxADT | ||
| 29 | import qualified Language.R.Refresh as R | ||
| 30 | import Language.R.SyntaxADT | ||
| 31 | |||
| 32 | ------------------------------------------------------------------------------- | ||
| 33 | |||
| 34 | refresh :: MonadFresh [String] String m => LawS -> m LawS | ||
| 35 | refresh (EquivS p n s1 s2) = aux (EquivS p n) s1 s2 | ||
| 36 | refresh (ImplS p n s1 s2) = aux (ImplS p n) s1 s2 | ||
| 37 | |||
| 38 | ------------------------------------------------------------------------------- | ||
| 39 | |||
| 40 | aux :: MonadFresh [String] String m => (S -> S -> LawS) -> S -> S -> m LawS | ||
| 41 | aux constr s1 s2 = let | ||
| 42 | (rvar1,tvar1) = R.collect s1 | ||
| 43 | (rvar2,tvar2) = R.collect s2 | ||
| 44 | rvar = nub $ rvar1 ++ rvar2 | ||
| 45 | tvar = nub $ tvar1 ++ tvar2 | ||
| 46 | in do | ||
| 47 | newVars <- R.refreshVar rvar | ||
| 48 | newTypes <- R.refreshType tvar | ||
| 49 | let s1' = runReader (R.replace s1) $ R.St {R.rvars = newVars, | ||
| 50 | R.tvars = newTypes} | ||
| 51 | s2' = runReader (R.replace s2) $ R.St {R.rvars = newVars, | ||
| 52 | R.tvars = newTypes} | ||
| 53 | return $ constr s1' s2' | ||
| 54 | |||
| 55 | ------------------------------------------------------------------------------- | ||
| 56 |