AlphaConvert.hs revision ad270004874ce1d0697fb30d7309f180553bb315
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : alpha-conversion (renaming of bound variables) for CASL formulas
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2005
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : maeder@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederuniquely rename variables in quantified formulas to allow for
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian Maedera formula equality modulo alpha conversion
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedermodule CASL.AlphaConvert (alphaEquiv, convertFormula) where
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowskiimport qualified Data.Map as Map
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till MossakowskiconvertRecord :: Int -> (f -> f) -> Record f (FORMULA f) (TERM f)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederconvertRecord n mf = (mapRecord mf)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder { foldQuantification = \ (Quantification q vs qf ps) _ _ _ _ ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let nvs = flatVAR_DECLs vs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mkVar i = mkSimpleId $ "v" ++ show i
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder rvs = map mkVar [n .. ]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder nf = replace_varsF (Map.fromList $ zipWith ( \ (v, s) i ->
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder (v, Qual_var i s ps)) nvs rvs) mf
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder $ convertFormula (n + length nvs) mf qf
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder in foldr ( \ (v, s) cf ->
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder Quantification q [Var_decl [v] s ps] cf ps)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder nf $ zip rvs $ map snd nvs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | uniquely rename variables in quantified formulas and always
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder quantify only over a single variable -}
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichconvertFormula :: Int -> (f -> f) -> FORMULA f -> FORMULA f
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederconvertFormula n = foldFormula . convertRecord n
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder-- | formula equality modulo alpha conversion
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederalphaEquiv :: Eq f => (f -> f) -> FORMULA f -> FORMULA f -> Bool
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederalphaEquiv mf f1 f2 =
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder convertFormula 1 mf f1 == convertFormula 1 mf f2