{-# 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 Int -> Maude2CASL -> ShowS
[Maude2CASL] -> ShowS
Maude2CASL -> String
(Int -> Maude2CASL -> ShowS)
-> (Maude2CASL -> String)
-> ([Maude2CASL] -> ShowS)
-> Show Maude2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Maude2CASL] -> ShowS
$cshowList :: [Maude2CASL] -> ShowS
show :: Maude2CASL -> String
$cshow :: Maude2CASL -> String
showsPrec :: Int -> Maude2CASL -> ShowS
$cshowsPrec :: Int -> Maude2CASL -> ShowS
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 -> Maude
sourceLogic Maude2CASL = Maude
MLogic.Maude
      sourceSublogic :: Maude2CASL -> ()
sourceSublogic Maude2CASL = ()
      targetLogic :: Maude2CASL -> CASL
targetLogic Maude2CASL = CASL
CLogic.CASL
      mapSublogic :: Maude2CASL -> () -> Maybe CASL_Sublogics
mapSublogic Maude2CASL _ = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
forall a. Lattice a => CASL_SL a
CSL.caslTop
        { cons_features :: SortGenerationFeatures
CSL.cons_features = SortGenerationFeatures
CSL.emptyMapConsFeature
        , sub_features :: SubsortingFeatures
CSL.sub_features = SubsortingFeatures
CSL.NoSub }
      map_theory :: Maude2CASL
-> (Sign, [Named Sentence])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory Maude2CASL = (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory
      is_model_transportable :: Maude2CASL -> Bool
is_model_transportable Maude2CASL = Bool
True
      map_symbol :: Maude2CASL -> Sign -> Symbol -> Set Symbol
map_symbol Maude2CASL = Sign -> Symbol -> Set Symbol
mapSymbol
      map_sentence :: Maude2CASL -> Sign -> Sentence -> Result CASLFORMULA
map_sentence Maude2CASL = Sign -> Sentence -> Result CASLFORMULA
mapSentence
      map_morphism :: Maude2CASL -> Morphism -> Result CASLMor
map_morphism Maude2CASL = Morphism -> Result CASLMor
mapMorphism
      has_model_expansion :: Maude2CASL -> Bool
has_model_expansion Maude2CASL = Bool
True
      is_weakly_amalgamable :: Maude2CASL -> Bool
is_weakly_amalgamable Maude2CASL = Bool
True
      isInclusionComorphism :: Maude2CASL -> Bool
isInclusionComorphism Maude2CASL = Bool
True

mapMaudeFreeness :: MMor.Morphism
                 -> Result (CSign.CASLSign, CMor.CASLMor, CMor.CASLMor)
mapMaudeFreeness :: Morphism -> Result (CASLSign, CASLMor, CASLMor)
mapMaudeFreeness morph :: Morphism
morph = do
 let sMaude :: Sign
sMaude = Morphism -> Sign
MMor.source Morphism
morph
     tMaude :: Sign
tMaude = Morphism -> Sign
MMor.target Morphism
morph
 (sCASL :: CASLSign
sCASL, _) <- Maude2CASL
-> (Sign, [Named Sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
map_theory Maude2CASL
Maude2CASL (Sign
sMaude, [])
 (tCASL :: CASLSign
tCASL, _) <- Maude2CASL
-> (Sign, [Named Sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
map_theory Maude2CASL
Maude2CASL (Sign
tMaude, [])
 let tExt :: CASLSign
tExt = Sign -> CASLSign -> CASLSign
signExtension Sign
tMaude CASLSign
tCASL
     (f1 :: CASLMor
f1, f2 :: CASLMor
f2) = Morphism -> CASLSign -> CASLSign -> CASLSign -> (CASLMor, CASLMor)
morExtension Morphism
morph CASLSign
tExt CASLSign
sCASL CASLSign
tCASL
 (CASLSign, CASLMor, CASLMor) -> Result (CASLSign, CASLMor, CASLMor)
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
tExt, CASLMor
f1, CASLMor
f2)


signExtension :: MSign.Sign -> CSign.CASLSign -> CSign.CASLSign
signExtension :: Sign -> CASLSign -> CASLSign
signExtension sigma :: Sign
sigma sigmaC :: CASLSign
sigmaC =
 let
  sorts :: Set Id
sorts = (Symbol -> Id) -> Set Symbol -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> Id
MSymbol.toId (Set Symbol -> Set Id) -> Set Symbol -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
MSign.sorts Sign
sigma
  subsorts :: Rel Id
subsorts = (Symbol -> Id) -> Rel Symbol -> Rel Id
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map Symbol -> Id
MSymbol.toId (Rel Symbol -> Rel Id) -> Rel Symbol -> Rel Id
forall a b. (a -> b) -> a -> b
$ Sign -> Rel Symbol
MSign.subsorts Sign
sigma
  kindR :: KindRel
kindR = Sign -> KindRel
MSign.kindRel Sign
sigma
  funs :: OpMap
funs = (\ (x :: OpMap
x, _, _) -> OpMap
x) ((OpMap, OpMap, Set Component) -> OpMap)
-> (OpMap, OpMap, Set Component) -> OpMap
forall a b. (a -> b) -> a -> b
$ IdMap -> OpMap -> (OpMap, OpMap, Set Component)
translateOps (KindRel -> IdMap
kindMapId KindRel
kindR) (OpMap -> (OpMap, OpMap, Set Component))
-> OpMap -> (OpMap, OpMap, Set Component)
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
MSign.ops Sign
sigma
  funSorts :: OpMap
funSorts = OpMap -> OpMap
atLeastOneSort (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
MSign.ops Sign
sigma
  funs' :: OpMap
funs' = (\ (x :: OpMap
x, _, _) -> OpMap
x) ((OpMap, OpMap, Set Component) -> OpMap)
-> (OpMap, OpMap, Set Component) -> OpMap
forall a b. (a -> b) -> a -> b
$ IdMap -> OpMap -> (OpMap, OpMap, Set Component)
translateOps' (KindRel -> IdMap
kindMapId KindRel
kindR) OpMap
funSorts
  {- opTypeKind (CSign.OpType oK oArgs oRes) =
              CSign.OpType oK (map kindId oArgs) (kindId oRes) -}
 in CASLSign
sigmaC
         {sortRel :: Rel Id
CSign.sortRel = Rel Id -> Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union
             (Set Id -> Rel Id
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet (Set Id -> Rel Id) -> Set Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
sorts (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Id
kindId Set Id
sorts)
             (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Rel Id -> Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Rel Id
subsorts (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Rel Id -> Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union
                              ((Id -> Id) -> Rel Id -> Rel Id
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map Id -> Id
kindId Rel Id
subsorts)
                              (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Set (Id, Id) -> Rel Id
forall a. Ord a => Set (a, a) -> Rel a
Rel.fromSet
                              (Set (Id, Id) -> Rel Id) -> Set (Id, Id) -> Rel Id
forall a b. (a -> b) -> a -> b
$ (Id -> (Id, Id)) -> Set Id -> Set (Id, Id)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: Id
x -> (Id
x, Id -> Id
kindId Id
x)) Set Id
sorts,
          opMap :: OpMap
CSign.opMap = OpMap -> OpMap -> OpMap
CSign.addOpMapSet OpMap
funs OpMap
funs',
           -- Map.map (\s -> Set.union s $ Set.map opTypeKind s) funs,
          predMap :: PredMap
CSign.predMap = Set Id -> PredMap
rewPredicates (Set Id -> PredMap) -> Set Id -> PredMap
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
sorts
                          (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Id
kindId Set Id
sorts

          }

morExtension :: MMor.Morphism ->  -- sigma:\Sigma -> \Sigma'
                CSign.CASLSign ->  -- phi(\Sigma)
                CSign.CASLSign -> -- phi(\Sigma')
                CSign.CASLSign -> -- \Sigma'#
                (CMor.CASLMor, CMor.CASLMor)
morExtension :: Morphism -> CASLSign -> CASLSign -> CASLSign -> (CASLMor, CASLMor)
morExtension phi :: Morphism
phi tExt :: CASLSign
tExt sCASL :: CASLSign
sCASL tCASL :: CASLSign
tCASL =
 let
   changeMap :: (k1 -> a) -> Map k1 k1 -> Map a a
changeMap f :: k1 -> a
f mapF :: Map k1 k1
mapF = (k1 -> a) -> Map k1 a -> Map a a
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys k1 -> a
f (Map k1 a -> Map a a) -> Map k1 a -> Map a a
forall a b. (a -> b) -> a -> b
$
                       (k1 -> a) -> Map k1 k1 -> Map k1 a
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map k1 -> a
f Map k1 k1
mapF
   sortF :: IdMap
sortF = (Symbol -> Id) -> KindRel -> IdMap
forall a k1. Ord a => (k1 -> a) -> Map k1 k1 -> Map a a
changeMap Symbol -> Id
MSymbol.toId (KindRel -> IdMap) -> KindRel -> IdMap
forall a b. (a -> b) -> a -> b
$ Morphism -> KindRel
MMor.sortMap Morphism
phi
   iotaN :: CASLMor
iotaN = () -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
CMor.embedMorphism () CASLSign
tCASL CASLSign
tExt
   genOps :: Symbol -> [((Id, OpType), (Id, OpKind))]
genOps f :: Symbol
f = let
               f' :: Id
f' = Symbol -> Id
MSymbol.toId Symbol
f
               profiles :: Set OpType
profiles = Id -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
f' (OpMap -> Set OpType) -> OpMap -> Set OpType
forall a b. (a -> b) -> a -> b
$ CASLSign -> OpMap
forall f e. Sign f e -> OpMap
CSign.opMap CASLSign
sCASL
               ff :: Symbol
ff = Symbol -> Symbol -> KindRel -> Symbol
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Symbol
forall a. HasCallStack => String -> a
error "morExtension")
                     Symbol
f (KindRel -> Symbol) -> KindRel -> Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> KindRel
MMor.opMap Morphism
phi
              in Set ((Id, OpType), (Id, OpKind)) -> [((Id, OpType), (Id, OpKind))]
forall a. Set a -> [a]
Set.toList (Set ((Id, OpType), (Id, OpKind))
 -> [((Id, OpType), (Id, OpKind))])
-> Set ((Id, OpType), (Id, OpKind))
-> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> a -> b
$ (OpType -> ((Id, OpType), (Id, OpKind)))
-> Set OpType -> Set ((Id, OpType), (Id, OpKind))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ x :: OpType
x -> ((Id
f', OpType
x),
                            (Symbol -> Id
MSymbol.toId Symbol
ff, OpKind
CBasic.Partial)))
                 Set OpType
profiles
   phi' :: CASLMor
phi' = Morphism :: forall f e m.
Sign f e
-> Sign f e -> IdMap -> Op_map -> Pred_map -> m -> Morphism f e m
CMor.Morphism {
             msource :: CASLSign
CMor.msource = CASLSign
sCASL,
             mtarget :: CASLSign
CMor.mtarget = CASLSign
tExt,
             sort_map :: IdMap
CMor.sort_map = IdMap -> IdMap -> IdMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union IdMap
sortF (IdMap -> IdMap) -> IdMap -> IdMap
forall a b. (a -> b) -> a -> b
$
                              (Id -> Id) -> IdMap -> IdMap
forall a k1. Ord a => (k1 -> a) -> Map k1 k1 -> Map a a
changeMap Id -> Id
kindId IdMap
sortF,
             op_map :: Op_map
CMor.op_map = [((Id, OpType), (Id, OpKind))] -> Op_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Id, OpType), (Id, OpKind))] -> Op_map)
-> [((Id, OpType), (Id, OpKind))] -> Op_map
forall a b. (a -> b) -> a -> b
$ (Symbol -> [((Id, OpType), (Id, OpKind))])
-> [Symbol] -> [((Id, OpType), (Id, OpKind))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Symbol -> [((Id, OpType), (Id, OpKind))]
genOps ([Symbol] -> [((Id, OpType), (Id, OpKind))])
-> [Symbol] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> a -> b
$ KindRel -> [Symbol]
forall k a. Map k a -> [k]
Map.keys (KindRel -> [Symbol]) -> KindRel -> [Symbol]
forall a b. (a -> b) -> a -> b
$
                            Morphism -> KindRel
MMor.opMap Morphism
phi ,
             pred_map :: Pred_map
CMor.pred_map = Pred_map
forall k a. Map k a
Map.empty,
                -- because rew is mapped identically!
             extended_map :: ()
CMor.extended_map = ()
           }
 in (CASLMor
iotaN, CASLMor
phi')