{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module : ./Comorphisms/Maude2CASL.hs
Description : Coding of Maude with preorder semantics into CASL
Copyright : (c) Adrian Riesco and Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : ariesco@fdi.ucm.es
Stability : experimental
Portability : non-portable (imports Logic.Logic)
The translating comorphism from Maude with preorder semantics to CASL.
-}
module Comorphisms.Maude2CASL
(
Maude2CASL (..)
, mapMaudeFreeness
)
where
import Logic.Logic
import Logic.Comorphism
-- Maude
import qualified Maude.Logic_Maude as MLogic
import qualified Maude.AS_Maude as MAS
import qualified Maude.Sign as MSign
import qualified Maude.Morphism as MMor
import qualified Maude.Symbol as MSymbol
import qualified Maude.Sentence as MSentence
import Maude.PreComorphism
-- CASL
import qualified CASL.Logic_CASL as CLogic
import qualified CASL.AS_Basic_CASL as CBasic
import qualified CASL.Sublogic as CSL
import qualified CASL.Sign as CSign
import qualified CASL.Morphism as CMor
import Common.Id ()
import Common.ProofTree
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
import qualified Data.Map as Map
import qualified Data.Set as Set
-- | lid of the morphism
data Maude2CASL = Maude2CASL deriving Show
instance Language Maude2CASL
instance Comorphism Maude2CASL
MLogic.Maude
()
MAS.MaudeText
MSentence.Sentence
()
()
MSign.Sign
MMor.Morphism
MSymbol.Symbol
MSymbol.Symbol
()
CLogic.CASL
CSL.CASL_Sublogics
CLogic.CASLBasicSpec
CBasic.CASLFORMULA
CBasic.SYMB_ITEMS
CBasic.SYMB_MAP_ITEMS
CSign.CASLSign
CMor.CASLMor
CSign.Symbol
CMor.RawSymbol
ProofTree
where
sourceLogic Maude2CASL = MLogic.Maude
sourceSublogic Maude2CASL = ()
targetLogic Maude2CASL = CLogic.CASL
mapSublogic Maude2CASL _ = Just CSL.caslTop
{ CSL.cons_features = CSL.emptyMapConsFeature
, CSL.sub_features = CSL.NoSub }
map_theory Maude2CASL = mapTheory
is_model_transportable Maude2CASL = True
map_symbol Maude2CASL = mapSymbol
map_sentence Maude2CASL = mapSentence
map_morphism Maude2CASL = mapMorphism
has_model_expansion Maude2CASL = True
is_weakly_amalgamable Maude2CASL = True
isInclusionComorphism Maude2CASL = True
mapMaudeFreeness :: MMor.Morphism
-> Result (CSign.CASLSign, CMor.CASLMor, CMor.CASLMor)
mapMaudeFreeness morph = do
let sMaude = MMor.source morph
tMaude = MMor.target morph
(sCASL, _) <- map_theory Maude2CASL (sMaude, [])
(tCASL, _) <- map_theory Maude2CASL (tMaude, [])
let tExt = signExtension tMaude tCASL
(f1, f2) = morExtension morph tExt sCASL tCASL
return (tExt, f1, f2)
signExtension :: MSign.Sign -> CSign.CASLSign -> CSign.CASLSign
signExtension sigma sigmaC =
let
sorts = Set.map MSymbol.toId $ MSign.sorts sigma
subsorts = Rel.map MSymbol.toId $ MSign.subsorts sigma
kindR = MSign.kindRel sigma
funs = (\ (x, _, _) -> x) $ translateOps (kindMapId kindR) $ MSign.ops sigma
funSorts = atLeastOneSort $ MSign.ops sigma
funs' = (\ (x, _, _) -> x) $ translateOps' (kindMapId kindR) funSorts
{- opTypeKind (CSign.OpType oK oArgs oRes) =
CSign.OpType oK (map kindId oArgs) (kindId oRes) -}
in sigmaC
{CSign.sortRel = Rel.union
(Rel.fromKeysSet $ Set.union sorts $ Set.map kindId sorts)
$ Rel.union subsorts $ Rel.union
(Rel.map kindId subsorts)
$ Rel.fromSet
$ Set.map (\ x -> (x, kindId x)) sorts,
CSign.opMap = CSign.addOpMapSet funs funs',
-- Map.map (\s -> Set.union s $ Set.map opTypeKind s) funs,
CSign.predMap = rewPredicates $ Set.union sorts
$ Set.map kindId sorts
}
morExtension :: MMor.Morphism -> -- sigma:\Sigma -> \Sigma'
CSign.CASLSign -> -- phi(\Sigma)
CSign.CASLSign -> -- phi(\Sigma')
CSign.CASLSign -> -- \Sigma'#
(CMor.CASLMor, CMor.CASLMor)
morExtension phi tExt sCASL tCASL =
let
changeMap f mapF = Map.mapKeys f $
Map.map f mapF
sortF = changeMap MSymbol.toId $ MMor.sortMap phi
iotaN = CMor.embedMorphism () tCASL tExt
genOps f = let
f' = MSymbol.toId f
profiles = MapSet.lookup f' $ CSign.opMap sCASL
ff = Map.findWithDefault (error "morExtension")
f $ MMor.opMap phi
in Set.toList $ Set.map (\ x -> ((f', x),
(MSymbol.toId ff, CBasic.Partial)))
profiles
phi' = CMor.Morphism {
CMor.msource = sCASL,
CMor.mtarget = tExt,
CMor.sort_map = Map.union sortF $
changeMap kindId sortF,
CMor.op_map = Map.fromList $ concatMap genOps $ Map.keys $
MMor.opMap phi ,
CMor.pred_map = Map.empty,
-- because rew is mapped identically!
CMor.extended_map = ()
}
in (iotaN, phi')