hets/Maude/Sentence.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Maude/Sentence.hs
Description :  Maude Sentences
Copyright   :  (c) Martin Kuehl, Uni Bremen 2008-2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mkhl@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Definition of sentences for Maude.
-}

module Maude.Sentence (
    -- * The Sentence type
    Sentence (..),
    -- * Contruction
    fromSpec,
    fromStatements,
    -- * Testing
    isRule,
) where

import Maude.AS_Maude
import Maude.Meta
import Maude.Printing ()

import Common.Id (mkSimpleId, GetRange)
import Common.Doc (vcat)
import Common.DocUtils (Pretty (..))

import Data.Data

-- * The Sentence type

-- | A 'Membership', 'Equation' or 'Rule'.
data Sentence = Membership Membership
              | Equation Equation
              | Rule Rule
              deriving (Show, Read, Ord, Eq, Typeable, Data)

-- ** Sentence Instances

instance GetRange Sentence

instance Pretty Sentence where
    pretty sent = case sent of
        Membership mb -> pretty mb
        Equation eq -> pretty eq
        Rule rl -> pretty rl
    pretties = vcat . map pretty

instance HasSorts Sentence where
    getSorts sen = case sen of
        Membership mb -> getSorts mb
        Equation eq -> getSorts eq
        Rule rl -> getSorts rl
    mapSorts mp sen = case sen of
        Membership mb -> Membership $ mapSorts mp mb
        Equation eq -> Equation $ mapSorts mp eq
        Rule rl -> Rule $ mapSorts mp rl

instance HasOps Sentence where
    getOps sen = case sen of
        Membership mb -> getOps mb
        Equation eq -> getOps eq
        Rule rl -> getOps rl
    mapOps mp sen = case sen of
        Membership mb -> Membership $ mapOps mp mb
        Equation eq -> Equation $ mapOps mp eq
        Rule rl -> Rule $ mapOps mp rl

instance HasLabels Sentence where
    getLabels sen = case sen of
        Membership mb -> getLabels mb
        Equation eq -> getLabels eq
        Rule rl -> getLabels rl
    mapLabels mp sen = case sen of
        Membership mb -> Membership $ mapLabels mp mb
        Equation eq -> Equation $ mapLabels mp eq
        Rule rl -> Rule $ mapLabels mp rl

-- * Contruction

-- | Extract the 'Sentence's from the given 'Module'.
fromSpec :: Module -> [Sentence]
fromSpec (Module _ _ stmts) = fromStatements stmts

-- | Extract the 'Sentence's from the given 'Statement's.
fromStatements :: [Statement] -> [Sentence]
fromStatements stmts = let
    convert stmt = case stmt of
        -- SubsortStmnt sub -> [fromSubsort sub]
        OpStmnt op -> fromOperator op
        MbStmnt mb -> [Membership mb]
        EqStmnt eq -> [Equation eq]
        RlStmnt rl -> [Rule rl]
        _ -> []
    in concatMap convert stmts

{-
fromSubsort :: SubsortDecl -> Sentence
fromSubsort (Subsort s1 s2) = Membership mb
    where var = mkVar "V" (TypeSort s1)
          cond = MbCond var s1
          mb = Mb var s2 [cond] []
-}

fromOperator :: Operator -> [Sentence]
fromOperator (Op op dom cod attrs) = let
    name = getName op
    first : second : _ = dom
    convert attr = case attr of
        Assoc -> assocEq name first second cod
        Comm -> commEq name first second cod
        Idem -> idemEq name first cod
        Id term -> identityEq name first term cod
        LeftId term -> leftIdEq name first term cod
        RightId term -> rightIdEq name first term cod
        _ -> []
    in concatMap convert attrs

commEq :: Qid -> Type -> Type -> Type -> [Sentence]
commEq op ar1 ar2 co = [Equation $ Eq t1 t2 [] []]
    where v1 = mkVar "v1" $ type2Kind ar1
          v2 = mkVar "v2" $ type2Kind ar2
          t1 = Apply op [v1, v2] $ type2Kind co
          t2 = Apply op [v2, v1] $ type2Kind co

assocEq :: Qid -> Type -> Type -> Type -> [Sentence]
assocEq op ar1 ar2 co = [eq]
    where v1 = mkVar "v1" $ type2Kind ar1
          v2 = mkVar "v2" $ type2Kind ar2
          v3 = mkVar "v3" $ type2Kind ar2
          t1 = Apply op [v1, v2] $ type2Kind co
          t2 = Apply op [t1, v3] $ type2Kind co
          t3 = Apply op [v2, v3] $ type2Kind co
          t4 = Apply op [v1, t3] $ type2Kind co
          eq = Equation $ Eq t2 t4 [] []

idemEq :: Qid -> Type -> Type -> [Sentence]
idemEq op ar co = [Equation $ Eq t v [] []]
    where v = Apply (mkSimpleId "v") [] $ type2Kind ar
          t = Apply op [v, v] $ type2Kind co

identityEq :: Qid -> Type -> Term -> Type -> [Sentence]
identityEq op ar1 idt co = [eq1, eq2]
    where idt' = const2kind idt
          v = mkVar "v" $ type2Kind ar1
          t1 = Apply op [v, idt'] $ type2Kind co
          t2 = Apply op [idt', v] $ type2Kind co
          eq1 = Equation $ Eq t1 v [] []
          eq2 = Equation $ Eq t2 v [] []

leftIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
leftIdEq op ar1 idt co = [eq1, eq2]
    where idt' = const2kind idt
          v = mkVar "v" $ type2Kind ar1
          t = Apply op [idt', v] $ type2Kind co
          eq1 = Equation $ Eq t v [] []
          eq2 = Equation $ Eq v t [] []

rightIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
rightIdEq op ar1 idt co = [eq1, eq2]
    where idt' = const2kind idt
          v = mkVar "v" $ type2Kind ar1
          t = Apply op [v, idt'] $ type2Kind co
          eq1 = Equation $ Eq t v [] []
          eq2 = Equation $ Eq v t [] []

type2Kind :: Type -> Type
type2Kind (TypeSort (SortId s)) = TypeKind $ KindId s
type2Kind k = k

const2kind :: Term -> Term
const2kind (Const q ty) = Const q $ type2Kind ty
const2kind t = t

-- * Testing

-- | True iff the given 'Sentence' is a 'Rule'.
isRule :: Sentence -> Bool
isRule sent = case sent of
    Rule _ -> True
    _ -> False