Changeset 11843

Timestamp:

29.06.2009 18:01:38 (9 months ago)

Author:

maeder

Message:

added logic maude

Location:

trunk

Files:

• Comorphisms/LogicList.hs (modified) (2 diffs)
• Maude/AS_Maude.hs (modified) (5 diffs)
• Maude/Logic_Maude.hs (modified) (5 diffs)
• Maude/Meta/Qid.hs (modified) (1 diff)

trunk/Comorphisms/LogicList.hs

@@ -62 +62 @@
 import DFOL.Logic_DFOL
 import OMDoc.Logic_OMDoc ()
+import Maude.Logic_Maude
 #endif
 #ifndef NOOWLLOGIC
@@ -89 +90 @@
   , Logic Temporal
   , Logic DFOL
+  , Logic Maude
 #endif
 #ifndef NOOWLLOGIC

trunk/Maude/AS_Maude.hs

@@ -1 @@
-{-
-  Ref.
-  http://maude.cs.uiuc.edu/
+{-# OPTIONS -XDeriveDataTypeable #-}
+{- |
+Module      :  $Header$
+Description :  abstract maude syntax
+Copyright   :  (c) DFKI GmbH 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  ariesco@fdi.ucm.es
+Stability   :  experimental
+Portability :  portable
+
+The abstract syntax of maude. Basic specs are a list of statements excluding
+imports. Sentences are equations, membership axioms, and rules. Sort, subsort
+and operations should be converted to signature.
+
+Because maude parses and typechecks an input string in one go, basic specs for
+the logic instance are just a wrapped string that is created by a simple
+parser.
 -}
 
 module Maude.AS_Maude where
-  
-import qualified Common.Id as Id
-  
+
+import Common.ATerm.Lib
+import Common.Doc
+import Common.DocUtils
+import Common.Id
+import Data.Typeable
+
 data Spec = Spec ModId [Parameter] [Statement]
           deriving (Show, Read)
@@ -28 +47 @@
               | OpRenaming2 OpId [Type] Type ToPartRenaming
               deriving (Show, Read)
+
+newtype MaudeText = MaudeText String deriving (Show, Typeable)
+
+instance Pretty MaudeText where
+  pretty (MaudeText s) = text s
+
+instance ShATermConvertible MaudeText where
+  toShATermAux att0 (MaudeText a) = do
+        (att1, a') <- toShATerm' att0 a
+        return $ addATerm (ShAAppl "MaudeText" [a'] []) att1
+  fromShATermAux ix att0 =
+        case getShATerm ix att0 of
+            ShAAppl "MaudeText" [a] _ ->
+                    case fromShATerm' a att0 of { (att1, a') ->
+                    (att1, MaudeText a') }
+            u -> fromShATermError "MaudeText" u
 
 data Statement = ImportStmnt Import
@@ -80 +115 @@
           | Memo
           | Prec Int
-          | Gather [Id.Token]
-          | Format [Id.Token]
+          | Gather [Token]
+          | Format [Token]
           | Ctor
           | Config
@@ -90 +125 @@
           deriving (Show, Read)
 
-data StmntAttr = Label Id.Token
+data StmntAttr = Label Token
                | Metadata String
                | Owise
                | Nonexec
-               | Print [Id.Token]
+               | Print [Token]
                deriving (Show, Read)
 
-data Term = Const Id.Token Type
-          | Var Id.Token Type
-          | Apply Id.Token [Term]
+data Term = Const Token Type
+          | Var Token Type
+          | Apply Token [Term]
           deriving (Show, Read)
 
@@ -106 +141 @@
           deriving (Show, Read)
 
-newtype Sort = SortId Id.Token
+newtype Sort = SortId Token
              deriving (Show, Read)
 
-newtype Kind = KindId Id.Token
+newtype Kind = KindId Token
              deriving (Show, Read)
 
-newtype ParamId = ParamId Id.Token
+newtype ParamId = ParamId Token
                 deriving (Show, Read)
 
-newtype ModId = ModId Id.Token
+newtype ModId = ModId Token
               deriving (Show, Read)
 
-newtype LabelId = LabelId Id.Token
+newtype LabelId = LabelId Token
                 deriving (Show, Read)
 
-newtype OpId = OpId Id.Token
+newtype OpId = OpId Token
              deriving (Show, Read)

trunk/Maude/Logic_Maude.hs

@@ -9 +9 @@
 Portability :  non-portable (imports Logic.Logic)
 
-Instance of class Logic for Maude.
-    Also instances of Syntax and Category.
-    ... sometime in the future, that is.
--}
-{-
-  Ref.
-
-  ...
+Instance of class Logic for Maude. See <http://maude.cs.uiuc.edu/>
 -}
 
@@ -23 +16 @@
 import Logic.Logic
 
+import Maude.AS_Maude (MaudeText)
 import Maude.Sign     (Sign)
 import Maude.Morphism (Morphism)
@@ -77 +71 @@
 -- | Instance of Syntax for Maude
 -- TODO: Implement real instance of Syntax for Maude
-instance Syntax Maude () () () where
+instance Syntax Maude MaudeText () () where
     -- parse_basic_spec
     -- parse_symb_items
@@ -84 +78 @@
 -- | Instance of StaticAnalysis for Maude
 -- TODO: Implement real instance of StaticAnalysis for Maude
-instance StaticAnalysis Maude () Sentence () () Sign Morphism Symbol Symbol where
+instance StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol
+    Symbol where
     -- static analysis --
     -- basic_analysis
@@ -116 +111 @@
 -- | Instance of Logic for Maude
 -- TODO: Implement real instance of Logic for Maude
-instance Logic Maude () () Sentence () () Sign Morphism Symbol Symbol () where
+instance Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol
+    () where
     stability Maude = Experimental
     -- data_logic

trunk/Maude/Meta/Qid.hs

@@ -23 +23 @@
 -- A Quoted Identifier
 newtype Qid = Qid { qid :: Id.Id }
-    deriving (Show, Eq, Ord, Typeable, Pretty)
+    deriving (Show, Eq, Ord, Typeable, Pretty, Id.GetRange)
 
 -- TODO: Replace dummy implementation for ShATermConvertible Qid.