AS_Maude.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Maude/AS_Maude.hs
Description :  Abstract Maude Syntax
Copyright   :  (c) DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.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 Common.Id hiding (Id)
import Common.Doc (specBraces, text)
import Common.DocUtils (Pretty (..))

import Data.Data

-- * Types

newtype MaudeText = MaudeText String deriving (Show, Typeable)

instance Pretty MaudeText where
    pretty (MaudeText s) = specBraces $ text s

instance GetRange MaudeText

type Qid = Token

data Spec = SpecMod Module
          | SpecTh Module
          | SpecView View
          deriving (Show, Read, Ord, Eq, Typeable, Data)

data Module = Module ModId [Parameter] [Statement]
            deriving (Show, Read, Ord, Eq, Typeable, Data)

data View = View ModId ModExp ModExp [Renaming]
            deriving (Show, Read, Ord, Eq, Typeable, Data)

data Parameter = Parameter Sort ModExp
               deriving (Show, Read, Ord, Eq, Typeable, Data)

data ModExp = ModExp ModId
            | SummationModExp ModExp ModExp
            | RenamingModExp ModExp [Renaming]
            | InstantiationModExp ModExp [ViewId]
            deriving (Show, Read, Ord, Eq, Typeable, Data)

data Renaming = SortRenaming Sort Sort
              | LabelRenaming LabelId LabelId
              | OpRenaming1 OpId ToPartRenaming
              | OpRenaming2 OpId [Type] Type ToPartRenaming
              | TermMap Term Term
              deriving (Show, Read, Ord, Eq, Typeable, Data)

data ToPartRenaming = To OpId [Attr]
                    deriving (Show, Read, Ord, Eq, Typeable, Data)

data Statement = ImportStmnt Import
               | SortStmnt Sort
               | SubsortStmnt SubsortDecl
               | OpStmnt Operator
               | EqStmnt Equation
               | MbStmnt Membership
               | RlStmnt Rule
               deriving (Show, Read, Ord, Eq, Typeable, Data)

data Import = Including ModExp
            | Extending ModExp
            | Protecting ModExp
            deriving (Show, Read, Ord, Eq, Typeable, Data)

data SubsortDecl = Subsort Sort Sort
                 deriving (Show, Read, Ord, Eq, Typeable, Data)

data Operator = Op OpId [Type] Type [Attr]
              deriving (Show, Read, Ord, Eq, Typeable, Data)

data Membership = Mb Term Sort [Condition] [StmntAttr]
                deriving (Show, Read, Ord, Eq, Typeable, Data)

data Equation = Eq Term Term [Condition] [StmntAttr]
              deriving (Show, Read, Ord, Eq, Typeable, Data)

data Rule = Rl Term Term [Condition] [StmntAttr]
          deriving (Show, Read, Ord, Eq, Typeable, Data)

data Condition = EqCond Term Term
               | MbCond Term Sort
               | MatchCond Term Term
               | RwCond Term Term
               deriving (Show, Read, Ord, Eq, Typeable, Data)

data Attr = Assoc
          | Comm
          | Idem
          | Iter
          | Id Term
          | LeftId Term
          | RightId Term
          | Strat [Int]
          | Memo
          | Prec Int
          | Gather [Qid]
          | Format [Qid]
          | Ctor
          | Config
          | Object
          | Msg
          | Frozen [Int]
          | Poly [Int]
          | Special [Hook]
          deriving (Show, Read, Ord, Eq, Typeable, Data)

data StmntAttr = Label Qid
               | Metadata String
               | Owise
               | Nonexec
               | Print [Qid]
               deriving (Show, Read, Ord, Eq, Typeable, Data)

data Hook = IdHook Qid [Qid]
          | OpHook Qid Qid [Qid] Qid
          | TermHook Qid Term
          deriving (Show, Read, Ord, Eq, Typeable, Data)

data Term = Const Qid Type
          | Var Qid Type
          | Apply Qid [Term] Type
          deriving (Show, Read, Ord, Eq, Typeable, Data)

data Type = TypeSort Sort
          | TypeKind Kind
          deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype Sort = SortId Qid
          deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype Kind = KindId Qid
             deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype ParamId = ParamId Qid
                deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype ViewId = ViewId Qid
               deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype ModId = ModId Qid
              deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype LabelId = LabelId Qid
                deriving (Show, Read, Ord, Eq, Typeable, Data)

newtype OpId = OpId Qid
             deriving (Show, Read, Ord, Eq, Typeable, Data)

-- * Construction

-- | Create a 'Var' 'Term' from the given arguments.
mkVar :: String -> Type -> Term
mkVar = Var . mkSimpleId

-- * Information Extraction

-- | Extract the 'Type' from the given 'Term'.
getTermType :: Term -> Type
getTermType term = case term of
    Const _ typ -> typ
    Var _ typ -> typ
    Apply _ _ typ -> typ

-- * Attribute Classification

-- | True iff the argument is the @assoc@ attribute.
assoc :: Attr -> Bool
assoc attr = case attr of
    Assoc -> True
    _ -> False

-- | True iff the argument is the @comm@ attribute.
comm :: Attr -> Bool
comm attr = case attr of
    Comm -> True
    _ -> False

-- | True iff the argument is the @idem@ attribute.
idem :: Attr -> Bool
idem attr = case attr of
    Idem -> True
    _ -> False

-- | True iff the argument is the identity attribute.
idtty :: Attr -> Bool
idtty attr = case attr of
    Id _ -> True
    _ -> False

-- | True iff the argument is the left identity attribute.
leftId :: Attr -> Bool
leftId attr = case attr of
    LeftId _ -> True
    _ -> False

-- | True iff the argument is the right identity attribute.
rightId :: Attr -> Bool
rightId attr = case attr of
    RightId _ -> True
    _ -> False

-- | True iff the argument is the @ctor@ attribute.
ctor :: Attr -> Bool
ctor attr = case attr of
    Ctor -> True
    _ -> False

-- | True iff the argument is the @owise@ attribute.
owise :: StmntAttr -> Bool
owise attr = case attr of
    Owise -> True
    _ -> False