0N/A{-# LANGUAGE MultiParamTypeClasses #-}

3909N/A{- |

0N/AModule : ./Maude/Logic_Maude.hs

0N/ADescription : Instance of class Logic for Maude

0N/ACopyright : (c) Martin Kuehl, Uni Bremen 2008

0N/ALicense : GPLv2 or higher, see LICENSE.txt

0N/A

0N/AMaintainer : mkhl@informatik.uni-bremen.de

0N/AStability : experimental

0N/APortability : non-portable (imports Logic.Logic)

0N/A

0N/AInstance of class Logic for Maude. See <http://maude.cs.uiuc.edu/>

0N/A-}

0N/A

0N/Amodule Maude.Logic_Maude where

0N/A

0N/Aimport Logic.Logic

0N/A

2362N/Aimport Maude.AS_Maude (MaudeText (..))

2362N/Aimport Maude.Parse (mStuff)

2362N/Aimport Maude.Symbol (Symbol)

0N/Aimport Maude.Sentence (Sentence)

0N/Aimport Maude.Sign (Sign)

0N/Aimport Maude.Morphism (Morphism)

0N/Aimport qualified Maude.Symbol as Symbol

496N/Aimport qualified Maude.Sign as Sign

0N/Aimport qualified Maude.Morphism as Morphism

0N/A

0N/Aimport Maude.ATC_Maude ()

0N/A

0N/Aimport Maude.Shellout

0N/A

0N/Aimport Common.AS_Annotation

0N/Aimport Common.ExtSign

3320N/A

3320N/Aimport Data.Monoid

0N/A

0N/Aimport System.IO.Unsafe

0N/A

496N/A-- | Lid for Maude

0N/Adata Maude = Maude

496N/A deriving (Show, Eq)

496N/A

0N/A

0N/A-- | Instance of Language for Maude

0N/Ainstance Language Maude where

0N/A description _ = unlines

0N/A [ "Maude - A High-Performance Rewriting Logic Framework"

0N/A , "This logic is rewriting logic, a logic of concurrent change that"

0N/A , "can naturally deal with state and with concurrent computations."

0N/A , "For an overview of Maude see" ++

0N/A " <http://maude.cs.uiuc.edu/overview.html>."

0N/A , "For information about rewriting logic see" ++

0N/A " <http://maude.cs.uiuc.edu/rwl.html>."

0N/A , "For information about the Maude project see" ++

0N/A " <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

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 ()