1a38107941725211e7c3f051f7a8f5e12199f03acmaedermodule Maude.Meta.HasSorts (

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder HasSorts(..)

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder) where

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariimport Maude.Meta.Qid

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport Maude.Meta.Term

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariimport Maude.Meta.Module

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport qualified Data.Set as Set

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport qualified Data.Map as Map

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport qualified Common.Lib.Rel as Rel

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederclass HasSorts a where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari getSorts :: a -> SortSet

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts :: QidMap -> a -> a

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance HasSorts Sort where

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari getSorts = Set.singleton

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts = mapToFunction

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegariinstance (HasSorts a) => HasSorts [a] where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder getSorts = Set.unions . map getSorts

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts = map . mapSorts

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance (HasSorts a, HasSorts b) => HasSorts (a, b) where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari getSorts (a, b) = Set.union (getSorts a) (getSorts b)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts mp (a, b) = (mapSorts mp a, mapSorts mp b)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederinstance (HasSorts a, HasSorts b, HasSorts c) => HasSorts (a, b, c) where

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari getSorts (a, b, c) = Set.union (getSorts a) (getSorts (b, c))

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari mapSorts mp (a, b, c) = (mapSorts mp a, mapSorts mp b, mapSorts mp c)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

1a38107941725211e7c3f051f7a8f5e12199f03acmaederinstance (Ord a, HasSorts a) => HasSorts (Set.Set a) where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getSorts = Set.fold (Set.union . getSorts) Set.empty

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts = Set.map . mapSorts

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance (Ord a, HasSorts a) => HasSorts (Rel.Rel a) where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari getSorts = getSorts . Rel.nodes

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts = Rel.map . mapSorts

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

1a38107941725211e7c3f051f7a8f5e12199f03acmaederinstance HasSorts Type where

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari getSorts typ = case typ of

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Sort s -> Set.singleton s

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Kind ss -> Set.fromList ss

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts mp typ = case typ of

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Sort s -> Sort (mapSorts mp s)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Kind ss -> Kind (mapSorts mp ss)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance HasSorts Term where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder getSorts term = case term of

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Constant _ t -> getSorts t

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Variable _ t -> getSorts t

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Term _ ts -> getSorts ts

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts mp term = case term of

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Constant c t -> Constant c (mapSorts mp t)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Variable v t -> Variable v (mapSorts mp t)

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Term t ts -> Term t (mapSorts mp ts)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance HasSorts OpDecl where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari getSorts op = getSorts (op'domain op, op'range op)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts mp op = op {

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder op'domain = mapSorts mp (op'domain op),

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari op'range = mapSorts mp (op'range op)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance HasSorts Condition where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder getSorts cond = case cond of

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Nil -> Set.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Equal t1 t2 -> getSorts (t1, t2)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Member t s -> getSorts (s, t)

f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari Match t1 t2 -> getSorts (t1, t2)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Implies t1 t2 -> getSorts (t1, t2)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Conjunction c1 c2 -> getSorts (c1, c2)

f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari mapSorts mp cond = case cond of

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Nil -> Nil

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari Equal t1 t2 -> Equal (mapSorts mp t1) (mapSorts mp t2)

ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari Member t s -> Member (mapSorts mp t) (mapSorts mp s)

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Match t1 t2 -> Match (mapSorts mp t1) (mapSorts mp t2)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Implies t1 t2 -> Implies (mapSorts mp t1) (mapSorts mp t2)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Conjunction c1 c2 -> Conjunction (mapSorts mp c1) (mapSorts mp c2)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance HasSorts MembAx where

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari getSorts mb = case mb of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Mb t s _ -> getSorts (s, t)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Cmb t s c _ -> getSorts (s, t, c)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts mp mb = case mb of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Mb t s as -> Mb (mapSorts mp t) (mapSorts mp s) as

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Cmb t s c as -> Cmb (mapSorts mp t) (mapSorts mp s) (mapSorts mp c) as

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance HasSorts Equation where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari getSorts eq = case eq of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Eq t1 t2 _ -> getSorts (t1, t2)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Ceq t1 t2 c _ -> getSorts (t1, t2, c)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts mp eq = case eq of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Eq t1 t2 as -> Eq (mapSorts mp t1) (mapSorts mp t2) as

d658c27a8e2e75f11e83548631f759ced4ab7e74Daniel Calegari Ceq t1 t2 c as -> Ceq (mapSorts mp t1) (mapSorts mp t2) (mapSorts mp c) as

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance HasSorts Rule where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder getSorts rl = case rl of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Rl t1 t2 _ -> getSorts (t1, t2)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Crl t1 t2 c _ -> getSorts (t1, t2, c)

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari mapSorts mp rl = case rl of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Rl t1 t2 as -> Rl (mapSorts mp t1) (mapSorts mp t2) as

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Crl t1 t2 c as -> Crl (mapSorts mp t1) (mapSorts mp t2) (mapSorts mp c) as

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel CalegarimapToFunction :: (Ord a) => Map.Map a a -> (a -> a)

7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel CalegarimapToFunction mp name = Map.findWithDefault name name mp