content: {- |
  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 = mapSort . 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 mf m = (mapRecord $ mf m)
       { foldQual_var = \ _ v -> Qual_var v . mapSrt m
       , foldApplication = \ _ -> Application . mapOpSymb m
       , foldSorted_term = \ _ st -> Sorted_term st . mapSrt m
       , foldCast = \ _ st -> Cast st . mapSrt m
       , foldQuantification = \ _ q ->
             Quantification q . map (mapVars m)
       , foldPredication = \ _ -> Predication . mapPrSymb m
       , foldMembership = \ _ t -> Membership t . mapSrt m
       , foldSort_gen_ax = \ _ constrs isFree -> let
         newConstrs = map (mapConstr m) constrs in
         mkSort_gen_ax newConstrs isFree
       }
  
  mapTerm :: MapSen f e m -> Morphism f e m -> TERM f -> TERM f
  mapTerm mf = foldTerm . mapMorphism mf
  
  mapMorphForm :: MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
  mapMorphForm mf = foldFormula . mapMorphism mf
  
  mapSen :: MorphismExtension e m => MapSen f e m -> Morphism f e m -> FORMULA f
    -> FORMULA f
  mapSen mf m = if isInclusionMorphism isInclusionMorphismExtension m then id
    else mapMorphForm mf m
  
  mapOpSymb :: Morphism f e m -> OP_SYMB -> OP_SYMB
  mapOpSymb m (Qual_op_name i t ps) =
     let (j, ty) = mapOpSym (sort_map m) (op_map m) (i, toOpType t)
     in Qual_op_name j (toOP_TYPE ty) ps
  mapOpSymb _ (Op_name os) =
      error $ "mapOpSymb: unexpected op symb: " ++ show os
  
  mapVars :: Morphism f e m -> VAR_DECL -> VAR_DECL
  mapVars m (Var_decl vs s ps) = Var_decl vs (mapSrt m s) ps
  
  mapDecoratedOpSymb :: Morphism f e m -> (OP_SYMB, [Int]) -> (OP_SYMB, [Int])
  mapDecoratedOpSymb m (os, indices) = let
     newOs = mapOpSymb m os
     in (newOs, indices)
  
  mapConstr :: Morphism f e m -> Constraint -> Constraint
  mapConstr m constr =
     let newS = mapSrt m (newSort constr)
         newOps = map (mapDecoratedOpSymb m) (opSymbs constr)
     in (constr {newSort = newS, opSymbs = newOps})
  
  mapPrSymb :: Morphism f e m -> PRED_SYMB -> PRED_SYMB
  mapPrSymb m (Qual_pred_name i t ps) =
     let (j, ty) = mapPredSym (sort_map m) (pred_map m) (i, toPredType t)
     in Qual_pred_name j (toPRED_TYPE ty) ps
  mapPrSymb _ (Pred_name p) =
      error $ "mapPrSymb: unexpected pred symb: " ++ show p
  