{-# 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.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 (Int -> Maude -> ShowS
[Maude] -> ShowS
Maude -> String
(Int -> Maude -> ShowS)
-> (Maude -> String) -> ([Maude] -> ShowS) -> Show Maude
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Maude] -> ShowS
$cshowList :: [Maude] -> ShowS
show :: Maude -> String
$cshow :: Maude -> String
showsPrec :: Int -> Maude -> ShowS
$cshowsPrec :: Int -> Maude -> ShowS
Show, Maude -> Maude -> Bool
(Maude -> Maude -> Bool) -> (Maude -> Maude -> Bool) -> Eq Maude
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Maude -> Maude -> Bool
$c/= :: Maude -> Maude -> Bool
== :: Maude -> Maude -> Bool
$c== :: Maude -> Maude -> Bool
Eq)


-- | Instance of Language for Maude
instance Language Maude where
    description :: Maude -> String
description _ = [String] -> String
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" String -> ShowS
forall a. [a] -> [a] -> [a]
++
          " <http://maude.cs.uiuc.edu/overview.html>."
        , "For information about rewriting logic see" String -> ShowS
forall a. [a] -> [a] -> [a]
++
          " <http://maude.cs.uiuc.edu/rwl.html>."
        , "For information about the Maude project see" String -> ShowS
forall a. [a] -> [a] -> [a]
++
          " <http://maude.cs.uiuc.edu/>." ]


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

-- | Instance of Sentences for Maude
instance Sentences Maude Sentence Sign Morphism Symbol where
    -- sentences --
    map_sen :: Maude -> Morphism -> Sentence -> Result Sentence
map_sen Maude = Morphism -> Sentence -> Result Sentence
Morphism.translateSentence
    simplify_sen :: Maude -> Sign -> Sentence -> Sentence
simplify_sen Maude = Sign -> Sentence -> Sentence
Sign.simplifySentence
    -- symbols --
    sym_name :: Maude -> Symbol -> Id
sym_name Maude = Symbol -> Id
Symbol.toId
    symKind :: Maude -> Symbol -> String
symKind Maude = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolKind -> Doc
forall a. Pretty a => a -> Doc
pretty (SymbolKind -> Doc) -> (Symbol -> SymbolKind) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbolKind
Symbol.sym_kind
    sym_of :: Maude -> Sign -> [Set Symbol]
sym_of Maude = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
Sign.symbols
    symmap_of :: Maude -> Morphism -> EndoMap Symbol
symmap_of Maude = Morphism -> EndoMap Symbol
Morphism.symbolMap

instance Semigroup MaudeText where
    (MaudeText l1 :: String
l1) <> :: MaudeText -> MaudeText -> MaudeText
<> (MaudeText l2 :: String
l2) = String -> MaudeText
MaudeText
      (String -> MaudeText)
-> ([String] -> String) -> [String] -> MaudeText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> MaudeText) -> [String] -> MaudeText
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
l1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
lines String
l2
instance Monoid MaudeText where
    mempty :: MaudeText
mempty = String -> MaudeText
MaudeText ""

-- | Instance of Syntax for Maude
instance Syntax Maude MaudeText Symbol () () where
    parse_basic_spec :: Maude -> Maybe (PrefixMap -> AParser st MaudeText)
parse_basic_spec Maude = (PrefixMap -> AParser st MaudeText)
-> Maybe (PrefixMap -> AParser st MaudeText)
forall a. a -> Maybe a
Just (\ _ -> (String -> MaudeText)
-> ParsecT String (AnnoState st) Identity String
-> AParser st MaudeText
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> MaudeText
MaudeText ParsecT String (AnnoState st) Identity String
forall st. CharParser st String
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
-> Maybe
     ((MaudeText, Sign, GlobalAnnos)
      -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence]))
basic_analysis Maude = let
        analyze :: (MaudeText, Sign, c)
-> m (MaudeText, ExtSign Sign symbol, [Named Sentence])
analyze (spec :: MaudeText
spec, sign :: Sign
sign, _) = let
            (rsig :: Sign
rsig, sens :: [Sentence]
sens) = IO (Sign, [Sentence]) -> (Sign, [Sentence])
forall a. IO a -> a
unsafePerformIO (IO (Sign, [Sentence]) -> (Sign, [Sentence]))
-> IO (Sign, [Sentence]) -> (Sign, [Sentence])
forall a b. (a -> b) -> a -> b
$ Sign -> MaudeText -> IO (Sign, [Sentence])
basicAnalysis Sign
sign MaudeText
spec
            in (MaudeText, ExtSign Sign symbol, [Named Sentence])
-> m (MaudeText, ExtSign Sign symbol, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (MaudeText
spec, Sign -> ExtSign Sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign Sign
rsig, (Sentence -> Named Sentence) -> [Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "") [Sentence]
sens)
        in ((MaudeText, Sign, GlobalAnnos)
 -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence]))
-> Maybe
     ((MaudeText, Sign, GlobalAnnos)
      -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence]))
forall a. a -> Maybe a
Just (MaudeText, Sign, GlobalAnnos)
-> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence])
forall (m :: * -> *) c symbol.
Monad m =>
(MaudeText, Sign, c)
-> m (MaudeText, ExtSign Sign symbol, [Named Sentence])
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 -> Sign -> Bool
is_subsig Maude = Sign -> Sign -> Bool
Sign.isSubsign
    empty_signature :: Maude -> Sign
empty_signature Maude = Sign
Sign.empty
    signature_union :: Maude -> Sign -> Sign -> Result Sign
signature_union Maude sign1 :: Sign
sign1 sign2 :: Sign
sign2 = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Sign
Sign.union Sign
sign1 Sign
sign2
    intersection :: Maude -> Sign -> Sign -> Result Sign
intersection Maude sign1 :: Sign
sign1 sign2 :: Sign
sign2 = Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Sign
Sign.intersection Sign
sign1 Sign
sign2
    -- final_union
    morphism_union :: Maude -> Morphism -> Morphism -> Result Morphism
morphism_union Maude mor1 :: Morphism
mor1 mor2 :: Morphism
mor2 = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism -> Morphism
Morphism.union Morphism
mor1 Morphism
mor2
    subsig_inclusion :: Maude -> Sign -> Sign -> Result Morphism
subsig_inclusion Maude src :: Sign
src tgt :: Sign
tgt = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Morphism
Morphism.inclusion Sign
src Sign
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 -> Stability
stability Maude = Stability
Experimental
    {- data_logic
    top_sublogic
    all_sublogics
    proj_sublogic_epsilon
    provers --
    provers
    cons_checkers
    conservativityCheck -}
    empty_proof_tree :: Maude -> ()
empty_proof_tree Maude = ()

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