{-# 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 Int -> HasCASL2HasCASL -> ShowS
[HasCASL2HasCASL] -> ShowS
HasCASL2HasCASL -> String
(Int -> HasCASL2HasCASL -> ShowS)
-> (HasCASL2HasCASL -> String)
-> ([HasCASL2HasCASL] -> ShowS)
-> Show HasCASL2HasCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HasCASL2HasCASL] -> ShowS
$cshowList :: [HasCASL2HasCASL] -> ShowS
show :: HasCASL2HasCASL -> String
$cshow :: HasCASL2HasCASL -> String
showsPrec :: Int -> HasCASL2HasCASL -> ShowS
$cshowsPrec :: Int -> HasCASL2HasCASL -> ShowS
Show

instance Language HasCASL2HasCASL where
  language_name :: HasCASL2HasCASL -> String
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
sourceLogic HasCASL2HasCASL = HasCASL
HasCASL
    sourceSublogic :: HasCASL2HasCASL -> Sublogic
sourceSublogic HasCASL2HasCASL = Sublogic
forall l. SemiLatticeWithTop l => l
top
    targetLogic :: HasCASL2HasCASL -> HasCASL
targetLogic HasCASL2HasCASL = HasCASL
HasCASL
    mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic
mapSublogic HasCASL2HasCASL = Sublogic -> Maybe Sublogic
forall a. a -> Maybe a
Just (Sublogic -> Maybe Sublogic)
-> (Sublogic -> Sublogic) -> Sublogic -> Maybe Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sublogic -> Sublogic
forall a. a -> a
id
    map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism
map_morphism HasCASL2HasCASL = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return
    map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence
map_sentence HasCASL2HasCASL env :: Env
env = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (Sentence -> Sentence) -> Sentence -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Sentence -> Sentence
translateSen Env
env
    map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol
map_symbol HasCASL2HasCASL _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton
    map_theory :: HasCASL2HasCASL
-> (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
map_theory HasCASL2HasCASL (sig :: Env
sig, sen :: [Named Sentence]
sen) = (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return
      (Env
sig, (Named Sentence -> Named Sentence)
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((Sentence -> Sentence) -> Named Sentence -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (Env -> Sentence -> Sentence
translateSen Env
sig)) [Named Sentence]
sen)