{- |
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 :: Int -> (f -> f) -> Record f (FORMULA f) (TERM f)
convertRecord n :: Int
n mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
    { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ orig :: FORMULA f
orig _ _ _ _ ->
      let Quantification q :: QUANTIFIER
q vs :: [VAR_DECL]
vs qf :: FORMULA f
qf ps :: Range
ps = FORMULA f
orig
          nvs :: [(VAR, SORT)]
nvs = [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs [VAR_DECL]
vs
          mkVar :: a -> VAR
mkVar i :: a
i = String -> VAR
mkSimpleId (String -> VAR) -> String -> VAR
forall a b. (a -> b) -> a -> b
$ 'v' Char -> String -> String
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
i
          rvs :: [VAR]
rvs = (Int -> VAR) -> [Int] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map Int -> VAR
forall a. Show a => a -> VAR
mkVar [Int
n .. ]
          nf :: FORMULA f
nf = Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF ([(VAR, TERM f)] -> Subst f
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(VAR, TERM f)] -> Subst f) -> [(VAR, TERM f)] -> Subst f
forall a b. (a -> b) -> a -> b
$ ((VAR, SORT) -> VAR -> (VAR, TERM f))
-> [(VAR, SORT)] -> [VAR] -> [(VAR, TERM f)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ( \ (v :: VAR
v, s :: SORT
s) i :: VAR
i ->
                             (VAR
v, VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
i SORT
s Range
ps)) [(VAR, SORT)]
nvs [VAR]
rvs) f -> f
mf
               (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Int -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(VAR, SORT)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(VAR, SORT)]
nvs) f -> f
mf FORMULA f
qf
      in ((VAR, SORT) -> FORMULA f -> FORMULA f)
-> FORMULA f -> [(VAR, SORT)] -> FORMULA f
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (v :: VAR
v, s :: SORT
s) cf :: FORMULA f
cf ->
           QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [[VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR
v] SORT
s Range
ps] FORMULA f
cf Range
ps)
             FORMULA f
nf ([(VAR, SORT)] -> FORMULA f) -> [(VAR, SORT)] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [VAR] -> [SORT] -> [(VAR, SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR]
rvs ([SORT] -> [(VAR, SORT)]) -> [SORT] -> [(VAR, SORT)]
forall a b. (a -> b) -> a -> b
$ ((VAR, SORT) -> SORT) -> [(VAR, SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd [(VAR, SORT)]
nvs
    }

{- | uniquely rename variables in quantified formulas and always
     quantify only over a single variable -}
convertFormula :: Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula :: Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula n :: Int
n = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. Int -> (f -> f) -> Record f (FORMULA f) (TERM f)
convertRecord Int
n

alphaConvert :: Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)
alphaConvert :: Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)
alphaConvert n :: Int
n mf :: f -> f
mf f :: FORMULA f
f = let f2 :: FORMULA f
f2 = Int -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula Int
n f -> f
mf FORMULA f
f in
  (FORMULA f
f2, Set (VAR, SORT) -> Int
forall a. Set a -> Int
Set.size (FORMULA f -> Set (VAR, SORT)
forall f. FORMULA f -> Set (VAR, SORT)
getQuantVars FORMULA f
f2) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2) -- leave a gap

-- | formula equality modulo alpha conversion
alphaEquiv :: Eq f => (f -> f) -> FORMULA f -> FORMULA f -> Bool
alphaEquiv :: (f -> f) -> FORMULA f -> FORMULA f -> Bool
alphaEquiv mf :: f -> f
mf f1 :: FORMULA f
f1 f2 :: FORMULA f
f2 =
    Int -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula 1 f -> f
mf FORMULA f
f1 FORMULA f -> FORMULA f -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula 1 f -> f
mf FORMULA f
f2