{- |

Module : ./CASL/AlphaConvert.hs

Description : alpha-conversion (renaming of bound variables) for CASL formulas

Copyright : (c) Christian Maeder, Uni Bremen 2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

uniquely rename variables in quantified formulas to allow for

a formula equality modulo alpha conversion

-}

module CASL.AlphaConvert (alphaEquiv, convertFormula, alphaConvert) where

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.Utils

import CASL.Quantification

import Common.Id

import qualified Data.Map as Map

import qualified Data.Set as Set

convertRecord :: Int -> (f -> f) -> Record f (FORMULA f) (TERM f)

convertRecord n mf = (mapRecord mf)

{ foldQuantification = \ orig _ _ _ _ ->

let Quantification q vs qf ps = orig

nvs = flatVAR_DECLs vs

mkVar i = mkSimpleId $ 'v' : show i

rvs = map mkVar [n .. ]

nf = replaceVarsF (Map.fromList $ zipWith ( \ (v, s) i ->

(v, Qual_var i s ps)) nvs rvs) mf

$ convertFormula (n + length nvs) mf qf

in foldr ( \ (v, s) cf ->

Quantification q [Var_decl [v] s ps] cf ps)

nf $ zip rvs $ map snd nvs

}

{- | uniquely rename variables in quantified formulas and always

quantify only over a single variable -}

convertFormula :: Int -> (f -> f) -> FORMULA f -> FORMULA f

convertFormula n = foldFormula . convertRecord n

alphaConvert :: Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)

alphaConvert n mf f = let f2 = convertFormula n mf f in

(f2, Set.size (getQuantVars f2) + 2) -- leave a gap

-- | formula equality modulo alpha conversion

alphaEquiv :: Eq f => (f -> f) -> FORMULA f -> FORMULA f -> Bool

alphaEquiv mf f1 f2 =

convertFormula 1 mf f1 == convertFormula 1 mf f2