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