{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  ./Maude/Logic_Maude.hs
Description :  Instance of class Logic for Maude
Copyright   :  (c) Martin Kuehl, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mkhl@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for Maude. See <http://maude.cs.uiuc.edu/>
-}

module Maude.Logic_Maude where

import Logic.Logic

import Common.Doc
import Common.DocUtils

import Maude.AS_Maude (MaudeText (..))
import Maude.Parse (mStuff)
import Maude.Symbol (Symbol)
import Maude.Sentence (Sentence)
import Maude.Sign (Sign)
import Maude.Morphism (Morphism)
import qualified Maude.Symbol as Symbol
import qualified Maude.Sign as Sign
import qualified Maude.Morphism as Morphism

import Maude.ATC_Maude ()

import Maude.Shellout

import Common.AS_Annotation
import Common.ExtSign

import Data.Monoid

import System.IO.Unsafe

-- | Lid for Maude
data Maude = Maude
           deriving (Show, Eq)


-- | Instance of Language for Maude
instance Language Maude where
    description _ = unlines
        [ "Maude - A High-Performance Rewriting Logic Framework"
        , "This logic is rewriting logic, a logic of concurrent change that"
        , "can naturally deal with state and with concurrent computations."
        , "For an overview of Maude see" ++
          " <http://maude.cs.uiuc.edu/overview.html>."
        , "For information about rewriting logic see" ++
          " <http://maude.cs.uiuc.edu/rwl.html>."
        , "For information about the Maude project see" ++
          " <http://maude.cs.uiuc.edu/>." ]


-- | Instance of Category for Maude
instance Category Sign Morphism where
    ide = Morphism.identity
    dom = Morphism.source
    cod = Morphism.target
    composeMorphisms = Morphism.compose
    inverse = Morphism.inverse
    isInclusion = Morphism.isInclusion
    legal_mor = Morphism.isLegal

-- | Instance of Sentences for Maude
instance Sentences Maude Sentence Sign Morphism Symbol where
    -- sentences --
    map_sen Maude = Morphism.translateSentence
    simplify_sen Maude = Sign.simplifySentence
    -- symbols --
    sym_name Maude = Symbol.toId
    symKind Maude = show . pretty . Symbol.sym_kind
    sym_of Maude = singletonList . Sign.symbols
    symmap_of Maude = Morphism.symbolMap

instance Monoid MaudeText where
    mempty = MaudeText ""
    mappend (MaudeText l1) (MaudeText l2) = MaudeText
      . unlines $ lines l1 ++ lines l2

-- | Instance of Syntax for Maude
instance Syntax Maude MaudeText Symbol () () where
    parse_basic_spec Maude = Just (\ _ -> fmap MaudeText mStuff)
    {- parse_symb_items
    parse_symb_map_items -}

-- | Instance of StaticAnalysis for Maude
instance StaticAnalysis Maude
         MaudeText Sentence () () Sign Morphism Symbol Symbol
  where
    -- static analysis --
    basic_analysis Maude = let
        analyze (spec, sign, _) = let
            (rsig, sens) = unsafePerformIO $ basicAnalysis sign spec
            in return (spec, mkExtSign rsig, map (makeNamed "") sens)
        in Just analyze
    {- stat_symb_map_items
    stat_symb_items
    amalgamation --
    ensures_amalgamability
    signature_colimit
    qualify
    symbols and raw symbols --
    symbol_to_raw
    id_to_raw
    matches
    operations on signatures and morphisms -- -}
    is_subsig Maude = Sign.isSubsign
    empty_signature Maude = Sign.empty
    signature_union Maude sign1 sign2 = return $ Sign.union sign1 sign2
    intersection Maude sign1 sign2 = return $ Sign.intersection sign1 sign2
    -- final_union
    morphism_union Maude mor1 mor2 = return $ Morphism.union mor1 mor2
    subsig_inclusion Maude src tgt = return $ Morphism.inclusion src tgt
    {- generated_sign
    cogenerated_sign
    induced_from_morphism
    induced_from_to_morphism
    is_transportable
    is_injective
    theory_to_taxonomy -}

-- | Instance of Logic for Maude
instance Logic Maude
         () MaudeText Sentence () () Sign Morphism Symbol Symbol ()
  where
    stability Maude = Experimental
    {- data_logic
    top_sublogic
    all_sublogics
    proj_sublogic_epsilon
    provers --
    provers
    cons_checkers
    conservativityCheck -}
    empty_proof_tree Maude = ()

instance LogicalFramework Maude
         () MaudeText Sentence () () Sign Morphism Symbol Symbol ()
