{- |

Module : ./HasCASL/MapTerm.hs

Description : renaming according to signature morphisms

Copyright : (c) Christian Maeder and Uni Bremen 2004

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

rename symbols of terms according to a signature morphisms

-}

module HasCASL.MapTerm where

import HasCASL.As

import HasCASL.AsUtils

import HasCASL.Le

import HasCASL.FoldTerm

import Common.Id

import qualified Data.Set as Set

type Rename = ((Id, TypeScheme) -> (Id, TypeScheme), Type -> Type)

renameRec :: Rename -> MapRec

renameRec 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 }