HasSorts.hs revision c71a28752b8269572ba1de2e2230bb97a4dde6ea
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinmodule Maude.Meta.HasSorts (
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin HasSorts(..)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin) where
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport Maude.Meta.Qid
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport Maude.Meta.Term
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport Maude.Meta.Module
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport Data.Set (Set)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport qualified Data.Set as Set
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinimport Common.Lib.Rel (Rel)
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calinimport qualified Common.Lib.Rel as Rel
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinclass HasSorts a where
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin getSorts :: a -> SortSet
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin mapSorts :: QidMap -> a -> a
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance HasSorts Sort where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getSorts = Set.singleton
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin mapSorts = mapAsFunction
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maederinstance (HasSorts a) => HasSorts [a] where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getSorts = Set.unions . map getSorts
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin mapSorts = map . mapSorts
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance (HasSorts a, HasSorts b) => HasSorts (a, b) where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin getSorts (a, b) = Set.union (getSorts a) (getSorts b)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts mp (a, b) = (mapSorts mp a, mapSorts mp b)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance (HasSorts a, HasSorts b, HasSorts c) => HasSorts (a, b, c) where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin getSorts (a, b, c) = Set.union (getSorts a) (getSorts (b, c))
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin mapSorts mp (a, b, c) = (mapSorts mp a, mapSorts mp b, mapSorts mp c)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance (Ord a, HasSorts a) => HasSorts (Set a) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getSorts = Set.fold (Set.union . getSorts) Set.empty
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts = Set.map . mapSorts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance (Ord a, HasSorts a) => HasSorts (Rel a) where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin getSorts = getSorts . Rel.nodes
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin mapSorts = Rel.map . mapSorts
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance HasSorts Type where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin getSorts typ = case typ of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Sort s -> Set.singleton s
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Kind ss -> Set.fromList ss
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin mapSorts mp typ = case typ of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Sort s -> Sort (mapSorts mp s)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Kind ss -> Kind (mapSorts mp ss)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance HasSorts Term where
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin getSorts term = case term of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Constant _ t -> getSorts t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Variable _ t -> getSorts t
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin Term _ ts -> getSorts ts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapSorts mp term = case term of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Constant c t -> Constant c (mapSorts mp t)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Variable v t -> Variable v (mapSorts mp t)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Term t ts -> Term t (mapSorts mp ts)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance HasSorts OpDecl where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getSorts op = getSorts (op'domain op, op'range op)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin mapSorts mp op = op {
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin op'domain = mapSorts mp (op'domain op),
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin op'range = mapSorts mp (op'range op)
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder }
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calininstance HasSorts Condition where
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin getSorts cond = case cond of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Nil -> Set.empty
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Equal t1 t2 -> getSorts (t1, t2)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Member t s -> getSorts (s, t)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Match t1 t2 -> getSorts (t1, t2)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Implies t1 t2 -> getSorts (t1, t2)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin Conjunction c1 c2 -> getSorts (c1, c2)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin mapSorts mp cond = case cond of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Nil -> Nil
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin Equal t1 t2 -> Equal (mapSorts mp t1) (mapSorts mp t2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Member t s -> Member (mapSorts mp t) (mapSorts mp s)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin Match t1 t2 -> Match (mapSorts mp t1) (mapSorts mp t2)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin Implies t1 t2 -> Implies (mapSorts mp t1) (mapSorts mp t2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Conjunction c1 c2 -> Conjunction (mapSorts mp c1) (mapSorts mp c2)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance HasSorts MembAx where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getSorts mb = case mb of
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin Mb t s _ -> getSorts (s, t)
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin Cmb t s c _ -> getSorts (s, t, c)
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin mapSorts mp mb = case mb of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Mb t s as -> Mb (mapSorts mp t) (mapSorts mp s) as
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Cmb t s c as -> Cmb (mapSorts mp t) (mapSorts mp s) (mapSorts mp c) as
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calininstance HasSorts Equation where
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin 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)
mapSorts mp eq = case eq of
Eq t1 t2 as -> Eq (mapSorts mp t1) (mapSorts mp t2) as
Ceq t1 t2 c as -> Ceq (mapSorts mp t1) (mapSorts mp t2) (mapSorts mp c) as
instance HasSorts Rule where
getSorts rl = case rl of
Rl t1 t2 _ -> getSorts (t1, t2)
Crl t1 t2 c _ -> getSorts (t1, t2, c)
mapSorts mp rl = case rl of
Rl t1 t2 as -> Rl (mapSorts mp t1) (mapSorts mp t2) as
Crl t1 t2 c as -> Crl (mapSorts mp t1) (mapSorts mp t2) (mapSorts mp c) as