{- |
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 :: Rename -> MapRec
renameRec m :: Rename
m = MapRec
mapRec
   { foldQualVar :: Term -> VarDecl -> Term
foldQualVar = \ _ -> VarDecl -> Term
QualVar (VarDecl -> Term) -> (VarDecl -> VarDecl) -> VarDecl -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type) -> VarDecl -> VarDecl
mapVar (Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m)
   , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Term
foldQualOp = \ _ b :: OpBrand
b (PolyId i :: Id
i as :: [TypeArg]
as ps :: Range
ps) sc :: TypeScheme
sc tys :: [Type]
tys qs :: InstKind
qs ->
        let (i2 :: Id
i2, sc2 :: TypeScheme
sc2) = Rename -> (Id, TypeScheme) -> (Id, TypeScheme)
forall a b. (a, b) -> a
fst Rename
m (Id
i, TypeScheme
sc)
            in OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
b (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i2 [TypeArg]
as Range
ps) TypeScheme
sc2 ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m) [Type]
tys) InstKind
qs
   , foldTypedTerm :: Term -> Term -> TypeQual -> Type -> Range -> Term
foldTypedTerm = \ _ te :: Term
te q :: TypeQual
q -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
te TypeQual
q (Type -> Range -> Term) -> (Type -> Type) -> Type -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m
   , foldQuantifiedTerm :: Term -> Quantifier -> [GenVarDecl] -> Term -> Range -> Term
foldQuantifiedTerm = \ _ q :: Quantifier
q ->
       Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
q ([GenVarDecl] -> Term -> Range -> Term)
-> ([GenVarDecl] -> [GenVarDecl])
-> [GenVarDecl]
-> Term
-> Range
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenVarDecl -> GenVarDecl) -> [GenVarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> GenVarDecl -> GenVarDecl
mapGenVar ((Type -> Type) -> GenVarDecl -> GenVarDecl)
-> (Type -> Type) -> GenVarDecl -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m)
   , foldAsPattern :: Term -> VarDecl -> Term -> Range -> Term
foldAsPattern = \ _ -> VarDecl -> Term -> Range -> Term
AsPattern (VarDecl -> Term -> Range -> Term)
-> (VarDecl -> VarDecl) -> VarDecl -> Term -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type) -> VarDecl -> VarDecl
mapVar (Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m)
   , foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> Term
foldMixTypeTerm = \ _ q :: TypeQual
q -> TypeQual -> Type -> Range -> Term
MixTypeTerm TypeQual
q (Type -> Range -> Term) -> (Type -> Type) -> Type -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m }

mapTerm :: Rename -> Term -> Term
mapTerm :: Rename -> Term -> Term
mapTerm = MapRec -> Term -> Term
forall a b. FoldRec a b -> Term -> a
foldTerm (MapRec -> Term -> Term)
-> (Rename -> MapRec) -> Rename -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rename -> MapRec
renameRec

mapEq :: Rename -> ProgEq -> ProgEq
mapEq :: Rename -> ProgEq -> ProgEq
mapEq = MapRec -> ProgEq -> ProgEq
forall a b. FoldRec a b -> ProgEq -> b
foldEq (MapRec -> ProgEq -> ProgEq)
-> (Rename -> MapRec) -> Rename -> ProgEq -> ProgEq
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rename -> MapRec
renameRec

mapVar :: (Type -> Type) -> VarDecl -> VarDecl
mapVar :: (Type -> Type) -> VarDecl -> VarDecl
mapVar m :: Type -> Type
m (VarDecl v :: Id
v ty :: Type
ty q :: SeparatorKind
q ps :: Range
ps) = Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v (Type -> Type
m Type
ty) SeparatorKind
q Range
ps

mapGenVar :: (Type -> Type) -> GenVarDecl -> GenVarDecl
mapGenVar :: (Type -> Type) -> GenVarDecl -> GenVarDecl
mapGenVar m :: Type -> Type
m g :: GenVarDecl
g = case GenVarDecl
g of
    GenVarDecl vd :: VarDecl
vd -> VarDecl -> GenVarDecl
GenVarDecl (VarDecl -> GenVarDecl) -> VarDecl -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> VarDecl -> VarDecl
mapVar Type -> Type
m VarDecl
vd
    GenTypeVarDecl (TypeArg i :: Id
i v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk c :: Int
c s :: SeparatorKind
s r :: Range
r) -> TypeArg -> GenVarDecl
GenTypeVarDecl
      (TypeArg -> GenVarDecl) -> TypeArg -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v (case VarKind
vk of
          VarKind k :: Kind
k -> -- extract kind renaming from type renaming
              let KindedType _ nk :: Set Kind
nk _ =
                      Type -> Type
m (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Set Kind -> Range -> Type
KindedType Type
unitType (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k) Range
r
              in Kind -> VarKind
VarKind (Kind -> VarKind) -> Kind -> VarKind
forall a b. (a -> b) -> a -> b
$ Set Kind -> Kind
forall a. Set a -> a
Set.findMin Set Kind
nk
          Downset t :: Type
t -> Type -> VarKind
Downset (Type -> VarKind) -> Type -> VarKind
forall a b. (a -> b) -> a -> b
$ Type -> Type
m Type
t
          _ -> VarKind
vk) RawKind
rk Int
c SeparatorKind
s Range
r

mapOpInfo :: Rename -> OpInfo -> OpInfo
mapOpInfo :: Rename -> OpInfo -> OpInfo
mapOpInfo m :: Rename
m oi :: OpInfo
oi = OpInfo
oi
    { opType :: TypeScheme
opType = (Type -> Type) -> TypeScheme -> TypeScheme
mapTypeOfScheme (Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m) (TypeScheme -> TypeScheme) -> TypeScheme -> TypeScheme
forall a b. (a -> b) -> a -> b
$ OpInfo -> TypeScheme
opType OpInfo
oi
    , opAttrs :: Set OpAttr
opAttrs = (OpAttr -> OpAttr) -> Set OpAttr -> Set OpAttr
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Rename -> OpAttr -> OpAttr
mapOpAttr Rename
m) (Set OpAttr -> Set OpAttr) -> Set OpAttr -> Set OpAttr
forall a b. (a -> b) -> a -> b
$ OpInfo -> Set OpAttr
opAttrs OpInfo
oi
    , opDefn :: OpDefn
opDefn = Rename -> OpDefn -> OpDefn
renameOpDefn Rename
m (OpDefn -> OpDefn) -> OpDefn -> OpDefn
forall a b. (a -> b) -> a -> b
$ OpInfo -> OpDefn
opDefn OpInfo
oi }

mapOpAttr :: Rename -> OpAttr -> OpAttr
mapOpAttr :: Rename -> OpAttr -> OpAttr
mapOpAttr m :: Rename
m o :: OpAttr
o = case OpAttr
o of
    UnitOpAttr t :: Term
t p :: Range
p -> Term -> Range -> OpAttr
UnitOpAttr (Rename -> Term -> Term
mapTerm Rename
m Term
t) Range
p
    _ -> OpAttr
o

renameOpDefn :: Rename -> OpDefn -> OpDefn
renameOpDefn :: Rename -> OpDefn -> OpDefn
renameOpDefn m :: Rename
m d :: OpDefn
d = case OpDefn
d of
    SelectData cs :: Set ConstrInfo
cs i :: Id
i -> Set ConstrInfo -> Id -> OpDefn
SelectData ((ConstrInfo -> ConstrInfo) -> Set ConstrInfo -> Set ConstrInfo
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((Type -> Type) -> ConstrInfo -> ConstrInfo
renameConstrInfo ((Type -> Type) -> ConstrInfo -> ConstrInfo)
-> (Type -> Type) -> ConstrInfo -> ConstrInfo
forall a b. (a -> b) -> a -> b
$ Rename -> Type -> Type
forall a b. (a, b) -> b
snd Rename
m) Set ConstrInfo
cs) Id
i
    Definition b :: OpBrand
b t :: Term
t -> OpBrand -> Term -> OpDefn
Definition OpBrand
b (Term -> OpDefn) -> Term -> OpDefn
forall a b. (a -> b) -> a -> b
$ Rename -> Term -> Term
mapTerm Rename
m Term
t
    _ -> OpDefn
d

renameConstrInfo :: (Type -> Type) -> ConstrInfo -> ConstrInfo
renameConstrInfo :: (Type -> Type) -> ConstrInfo -> ConstrInfo
renameConstrInfo m :: Type -> Type
m c :: ConstrInfo
c = ConstrInfo
c { constrType :: TypeScheme
constrType = (Type -> Type) -> TypeScheme -> TypeScheme
mapTypeOfScheme Type -> Type
m (TypeScheme -> TypeScheme) -> TypeScheme -> TypeScheme
forall a b. (a -> b) -> a -> b
$ ConstrInfo -> TypeScheme
constrType ConstrInfo
c }