content: {- |
  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
  