0N/A{- |

553N/AModule : ./HasCASL/MapTerm.hs

0N/ADescription : renaming according to signature morphisms

0N/ACopyright : (c) Christian Maeder and Uni Bremen 2004

0N/ALicense : GPLv2 or higher, see LICENSE.txt

0N/A

0N/AMaintainer : Christian.Maeder@dfki.de

0N/AStability : provisional

0N/APortability : portable

0N/A

0N/Arename symbols of terms according to a signature morphisms

0N/A-}

0N/A

0N/Amodule HasCASL.MapTerm where

0N/A

0N/Aimport HasCASL.As

0N/Aimport HasCASL.AsUtils

0N/Aimport HasCASL.Le

553N/Aimport HasCASL.FoldTerm

553N/Aimport Common.Id

553N/Aimport qualified Data.Set as Set

0N/A

0N/Atype Rename = ((Id, TypeScheme) -> (Id, TypeScheme), Type -> Type)

0N/A

0N/ArenameRec :: Rename -> MapRec

0N/ArenameRec m = mapRec

{ foldQualVar = \ _ -> QualVar . mapVar (snd m)

, foldQualOp = \ _ b (PolyId i as ps) sc tys qs ->

let (i2, sc2) = fst m (i, sc)

in QualOp b (PolyId i2 as ps) sc2 (map (snd m) tys) qs

, foldTypedTerm = \ _ te q -> TypedTerm te q . snd m

, foldQuantifiedTerm = \ _ q ->

QuantifiedTerm q . map (mapGenVar $ snd m)

, foldAsPattern = \ _ -> AsPattern . mapVar (snd m)

, foldMixTypeTerm = \ _ q -> MixTypeTerm q . snd m }

mapTerm :: Rename -> Term -> Term

mapTerm = foldTerm . renameRec

mapEq :: Rename -> ProgEq -> ProgEq

mapEq = foldEq . renameRec

mapVar :: (Type -> Type) -> VarDecl -> VarDecl

mapVar m (VarDecl v ty q ps) = VarDecl v (m ty) q ps

mapGenVar :: (Type -> Type) -> GenVarDecl -> GenVarDecl

mapGenVar m g = case g of

GenVarDecl vd -> GenVarDecl $ mapVar m vd

GenTypeVarDecl (TypeArg i v vk rk c s r) -> GenTypeVarDecl

$ TypeArg i v (case vk of

VarKind k -> -- extract kind renaming from type renaming

let KindedType _ nk _ =

m $ KindedType unitType (Set.singleton k) r

in VarKind $ Set.findMin nk

Downset t -> Downset $ m t

_ -> vk) rk c s r

mapOpInfo :: Rename -> OpInfo -> OpInfo

mapOpInfo m oi = oi

{ opType = mapTypeOfScheme (snd m) $ opType oi

, opAttrs = Set.map (mapOpAttr m) $ opAttrs oi

, opDefn = renameOpDefn m $ opDefn oi }

mapOpAttr :: Rename -> OpAttr -> OpAttr

mapOpAttr m o = case o of

UnitOpAttr t p -> UnitOpAttr (mapTerm m t) p

_ -> o

renameOpDefn :: Rename -> OpDefn -> OpDefn

renameOpDefn m d = case d of

SelectData cs i -> SelectData (Set.map (renameConstrInfo $ snd m) cs) i

Definition b t -> Definition b $ mapTerm m t

_ -> d

renameConstrInfo :: (Type -> Type) -> ConstrInfo -> ConstrInfo

renameConstrInfo m c = c { constrType = mapTypeOfScheme m $ constrType c }