content: {-# LANGUAGE MultiParamTypeClasses #-}
  {- |
  Module      :  ./Comorphisms/HasCASL2HasCASL.hs
  Description :  translating executable formulas to programs
  Copyright   :  (c) Christian Maeder, Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  translate HasCASL formulas to HasCASL program equations
  -}
  
  module Comorphisms.HasCASL2HasCASL where
  
  import Logic.Logic
  import Logic.Comorphism
  
  import HasCASL.Logic_HasCASL
  import HasCASL.Sublogic
  import HasCASL.As
  import HasCASL.Le
  import HasCASL.ProgEq
  
  import qualified Data.Set as Set
  import Common.AS_Annotation
  
  -- | The identity of the comorphism
  data HasCASL2HasCASL = HasCASL2HasCASL deriving Show
  
  instance Language HasCASL2HasCASL where
    language_name HasCASL2HasCASL = "HasCASL2HasCASLPrograms"
  
  instance Comorphism HasCASL2HasCASL
                 HasCASL Sublogic
                 BasicSpec Sentence SymbItems SymbMapItems
                 Env Morphism Symbol RawSymbol ()
                 HasCASL Sublogic
                 BasicSpec Sentence SymbItems SymbMapItems
                 Env Morphism Symbol RawSymbol () where
      sourceLogic HasCASL2HasCASL = HasCASL
      sourceSublogic HasCASL2HasCASL = top
      targetLogic HasCASL2HasCASL = HasCASL
      mapSublogic HasCASL2HasCASL = Just . id
      map_morphism HasCASL2HasCASL = return
      map_sentence HasCASL2HasCASL env = return . translateSen env
      map_symbol HasCASL2HasCASL _ = Set.singleton
      map_theory HasCASL2HasCASL (sig, sen) = return
        (sig, map (mapNamed (translateSen sig)) sen)
  