{-# 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)