?prevdifflink? - Blame
|
{-# LANGUAGE FlexibleContexts #-} {-# OPTIONS_GHC -Wall #-} ------------------------------------------------------------------------------- {- | Module : Language.Law.Refresh Description : Operations for refreshing the variable names. Copyright : (c) Paulo Silva License : LGPL Maintainer : paufil@di.uminho.pt Stability : experimental Portability : portable -} ------------------------------------------------------------------------------- module Language.Law.Refresh ( refresh ) where import Control.Monad.Fresh import Control.Monad.Reader import Data.List import Language.Law.SyntaxADT import qualified Language.R.Refresh as R import Language.R.SyntaxADT ------------------------------------------------------------------------------- refresh :: MonadFresh [String] String m => LawS -> m LawS refresh (EquivS p n s1 s2) = aux (EquivS p n) s1 s2 refresh (ImplS p n s1 s2) = aux (ImplS p n) s1 s2 ------------------------------------------------------------------------------- aux :: MonadFresh [String] String m => (S -> S -> LawS) -> S -> S -> m LawS aux constr s1 s2 = let (rvar1,tvar1) = R.collect s1 (rvar2,tvar2) = R.collect s2 rvar = nub $ rvar1 ++ rvar2 tvar = nub $ tvar1 ++ tvar2 in do newVars <- R.refreshVar rvar newTypes <- R.refreshType tvar let s1' = runReader (R.replace s1) $ R.St {R.rvars = newVars, R.tvars = newTypes} s2' = runReader (R.replace s2) $ R.St {R.rvars = newVars, R.tvars = newTypes} return $ constr s1' s2' ------------------------------------------------------------------------------- |