{- |
Module      :  ./CASL/MapSentence.hs
Description :  rename symbols of sentences according to a signature morphisms
Copyright   :  (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Rename symbols of sentences according to a signature morphisms
-}

module CASL.MapSentence where

import CASL.Sign
import CASL.Morphism
import CASL.AS_Basic_CASL
import CASL.Fold

mapSrt :: Morphism f e m -> SORT -> SORT
mapSrt :: Morphism f e m -> SORT -> SORT
mapSrt = Sort_map -> SORT -> SORT
mapSort (Sort_map -> SORT -> SORT)
-> (Morphism f e m -> Sort_map) -> Morphism f e m -> SORT -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map

type MapSen f e m = Morphism f e m -> f -> f

mapMorphism :: MapSen f e m -> Morphism f e m
          -> Record f (FORMULA f) (TERM f)
mapMorphism :: MapSen f e m -> Morphism f e m -> Record f (FORMULA f) (TERM f)
mapMorphism mf :: MapSen f e m
mf m :: Morphism f e m
m = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f) -> Record f (FORMULA f) (TERM f)
forall a b. (a -> b) -> a -> b
$ MapSen f e m
mf Morphism f e m
m)
     { foldQual_var :: TERM f -> VAR -> SORT -> Range -> TERM f
foldQual_var = \ _ v :: VAR
v -> VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v (SORT -> Range -> TERM f)
-> (SORT -> SORT) -> SORT -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f e m
m
     , foldApplication :: TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f
foldApplication = \ _ -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (OP_SYMB -> [TERM f] -> Range -> TERM f)
-> (OP_SYMB -> OP_SYMB) -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> OP_SYMB -> OP_SYMB
forall f e m. Morphism f e m -> OP_SYMB -> OP_SYMB
mapOpSymb Morphism f e m
m
     , foldSorted_term :: TERM f -> TERM f -> SORT -> Range -> TERM f
foldSorted_term = \ _ st :: TERM f
st -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
st (SORT -> Range -> TERM f)
-> (SORT -> SORT) -> SORT -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f e m
m
     , foldCast :: TERM f -> TERM f -> SORT -> Range -> TERM f
foldCast = \ _ st :: TERM f
st -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Cast TERM f
st (SORT -> Range -> TERM f)
-> (SORT -> SORT) -> SORT -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f e m
m
     , foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ _ q :: QUANTIFIER
q ->
           QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q ([VAR_DECL] -> FORMULA f -> Range -> FORMULA f)
-> ([VAR_DECL] -> [VAR_DECL])
-> [VAR_DECL]
-> FORMULA f
-> Range
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism f e m -> VAR_DECL -> VAR_DECL
forall f e m. Morphism f e m -> VAR_DECL -> VAR_DECL
mapVars Morphism f e m
m)
     , foldPredication :: FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPredication = \ _ -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (PRED_SYMB -> [TERM f] -> Range -> FORMULA f)
-> (PRED_SYMB -> PRED_SYMB)
-> PRED_SYMB
-> [TERM f]
-> Range
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> PRED_SYMB -> PRED_SYMB
forall f e m. Morphism f e m -> PRED_SYMB -> PRED_SYMB
mapPrSymb Morphism f e m
m
     , foldMembership :: FORMULA f -> TERM f -> SORT -> Range -> FORMULA f
foldMembership = \ _ t :: TERM f
t -> TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
t (SORT -> Range -> FORMULA f)
-> (SORT -> SORT) -> SORT -> Range -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f e m
m
     , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> FORMULA f
foldSort_gen_ax = \ _ constrs :: [Constraint]
constrs isFree :: Bool
isFree -> let
       newConstrs :: [Constraint]
newConstrs = (Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism f e m -> Constraint -> Constraint
forall f e m. Morphism f e m -> Constraint -> Constraint
mapConstr Morphism f e m
m) [Constraint]
constrs in
       [Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax [Constraint]
newConstrs Bool
isFree
     }

mapTerm :: MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm :: MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm mf :: MapSen f e m
mf = Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f)
-> (Morphism f e m -> Record f (FORMULA f) (TERM f))
-> Morphism f e m
-> TERM f
-> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen f e m -> Morphism f e m -> Record f (FORMULA f) (TERM f)
forall f e m.
MapSen f e m -> Morphism f e m -> Record f (FORMULA f) (TERM f)
mapMorphism MapSen f e m
mf

mapMorphForm :: MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapMorphForm :: MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapMorphForm mf :: MapSen f e m
mf = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> (Morphism f e m -> Record f (FORMULA f) (TERM f))
-> Morphism f e m
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen f e m -> Morphism f e m -> Record f (FORMULA f) (TERM f)
forall f e m.
MapSen f e m -> Morphism f e m -> Record f (FORMULA f) (TERM f)
mapMorphism MapSen f e m
mf

mapSen :: MorphismExtension e m => MapSen f e m -> Morphism f e m -> FORMULA f
  -> FORMULA f
mapSen :: MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen mf :: MapSen f e m
mf m :: Morphism f e m
m = if (m -> Bool) -> Morphism f e m -> Bool
forall m f e. (m -> Bool) -> Morphism f e m -> Bool
isInclusionMorphism m -> Bool
forall e m. MorphismExtension e m => m -> Bool
isInclusionMorphismExtension Morphism f e m
m then FORMULA f -> FORMULA f
forall a. a -> a
id
  else MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
forall f e m.
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapMorphForm MapSen f e m
mf Morphism f e m
m

mapOpSymb :: Morphism f e m -> OP_SYMB -> OP_SYMB
mapOpSymb :: Morphism f e m -> OP_SYMB -> OP_SYMB
mapOpSymb m :: Morphism f e m
m (Qual_op_name i :: SORT
i t :: OP_TYPE
t ps :: Range
ps) =
   let (j :: SORT
j, ty :: OpType
ty) = Sort_map -> Op_map -> (SORT, OpType) -> (SORT, OpType)
mapOpSym (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m) (Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m) (SORT
i, OP_TYPE -> OpType
toOpType OP_TYPE
t)
   in SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
j (OpType -> OP_TYPE
toOP_TYPE OpType
ty) Range
ps
mapOpSymb _ (Op_name os :: SORT
os) =
    [Char] -> OP_SYMB
forall a. HasCallStack => [Char] -> a
error ([Char] -> OP_SYMB) -> [Char] -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ "mapOpSymb: unexpected op symb: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
os

mapVars :: Morphism f e m -> VAR_DECL -> VAR_DECL
mapVars :: Morphism f e m -> VAR_DECL -> VAR_DECL
mapVars m :: Morphism f e m
m (Var_decl vs :: [VAR]
vs s :: SORT
s ps :: Range
ps) = [VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR]
vs (Morphism f e m -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f e m
m SORT
s) Range
ps

mapDecoratedOpSymb :: Morphism f e m -> (OP_SYMB, [Int]) -> (OP_SYMB, [Int])
mapDecoratedOpSymb :: Morphism f e m -> (OP_SYMB, [Int]) -> (OP_SYMB, [Int])
mapDecoratedOpSymb m :: Morphism f e m
m (os :: OP_SYMB
os, indices :: [Int]
indices) = let
   newOs :: OP_SYMB
newOs = Morphism f e m -> OP_SYMB -> OP_SYMB
forall f e m. Morphism f e m -> OP_SYMB -> OP_SYMB
mapOpSymb Morphism f e m
m OP_SYMB
os
   in (OP_SYMB
newOs, [Int]
indices)

mapConstr :: Morphism f e m -> Constraint -> Constraint
mapConstr :: Morphism f e m -> Constraint -> Constraint
mapConstr m :: Morphism f e m
m constr :: Constraint
constr =
   let newS :: SORT
newS = Morphism f e m -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f e m
m (Constraint -> SORT
newSort Constraint
constr)
       newOps :: [(OP_SYMB, [Int])]
newOps = ((OP_SYMB, [Int]) -> (OP_SYMB, [Int]))
-> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism f e m -> (OP_SYMB, [Int]) -> (OP_SYMB, [Int])
forall f e m.
Morphism f e m -> (OP_SYMB, [Int]) -> (OP_SYMB, [Int])
mapDecoratedOpSymb Morphism f e m
m) (Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
constr)
   in (Constraint
constr {newSort :: SORT
newSort = SORT
newS, opSymbs :: [(OP_SYMB, [Int])]
opSymbs = [(OP_SYMB, [Int])]
newOps})

mapPrSymb :: Morphism f e m -> PRED_SYMB -> PRED_SYMB
mapPrSymb :: Morphism f e m -> PRED_SYMB -> PRED_SYMB
mapPrSymb m :: Morphism f e m
m (Qual_pred_name i :: SORT
i t :: PRED_TYPE
t ps :: Range
ps) =
   let (j :: SORT
j, ty :: PredType
ty) = Sort_map -> Pred_map -> (SORT, PredType) -> (SORT, PredType)
mapPredSym (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m) (Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m) (SORT
i, PRED_TYPE -> PredType
toPredType PRED_TYPE
t)
   in SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
j (PredType -> PRED_TYPE
toPRED_TYPE PredType
ty) Range
ps
mapPrSymb _ (Pred_name p :: SORT
p) =
    [Char] -> PRED_SYMB
forall a. HasCallStack => [Char] -> a
error ([Char] -> PRED_SYMB) -> [Char] -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ "mapPrSymb: unexpected pred symb: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
p