{-# 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 (Int -> Sentence -> ShowS
[Sentence] -> ShowS
Sentence -> String
(Int -> Sentence -> ShowS)
-> (Sentence -> String) -> ([Sentence] -> ShowS) -> Show Sentence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sentence] -> ShowS
$cshowList :: [Sentence] -> ShowS
show :: Sentence -> String
$cshow :: Sentence -> String
showsPrec :: Int -> Sentence -> ShowS
$cshowsPrec :: Int -> Sentence -> ShowS
Show, ReadPrec [Sentence]
ReadPrec Sentence
Int -> ReadS Sentence
ReadS [Sentence]
(Int -> ReadS Sentence)
-> ReadS [Sentence]
-> ReadPrec Sentence
-> ReadPrec [Sentence]
-> Read Sentence
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Sentence]
$creadListPrec :: ReadPrec [Sentence]
readPrec :: ReadPrec Sentence
$creadPrec :: ReadPrec Sentence
readList :: ReadS [Sentence]
$creadList :: ReadS [Sentence]
readsPrec :: Int -> ReadS Sentence
$creadsPrec :: Int -> ReadS Sentence
Read, Eq Sentence
Eq Sentence =>
(Sentence -> Sentence -> Ordering)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Sentence)
-> (Sentence -> Sentence -> Sentence)
-> Ord Sentence
Sentence -> Sentence -> Bool
Sentence -> Sentence -> Ordering
Sentence -> Sentence -> Sentence
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Sentence -> Sentence -> Sentence
$cmin :: Sentence -> Sentence -> Sentence
max :: Sentence -> Sentence -> Sentence
$cmax :: Sentence -> Sentence -> Sentence
>= :: Sentence -> Sentence -> Bool
$c>= :: Sentence -> Sentence -> Bool
> :: Sentence -> Sentence -> Bool
$c> :: Sentence -> Sentence -> Bool
<= :: Sentence -> Sentence -> Bool
$c<= :: Sentence -> Sentence -> Bool
< :: Sentence -> Sentence -> Bool
$c< :: Sentence -> Sentence -> Bool
compare :: Sentence -> Sentence -> Ordering
$ccompare :: Sentence -> Sentence -> Ordering
$cp1Ord :: Eq Sentence
Ord, Sentence -> Sentence -> Bool
(Sentence -> Sentence -> Bool)
-> (Sentence -> Sentence -> Bool) -> Eq Sentence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sentence -> Sentence -> Bool
$c/= :: Sentence -> Sentence -> Bool
== :: Sentence -> Sentence -> Bool
$c== :: Sentence -> Sentence -> Bool
Eq, Typeable, Typeable Sentence
Constr
DataType
Typeable Sentence =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sentence -> c Sentence)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sentence)
-> (Sentence -> Constr)
-> (Sentence -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sentence))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence))
-> ((forall b. Data b => b -> b) -> Sentence -> Sentence)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Sentence -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Sentence -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sentence -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sentence -> m Sentence)
-> Data Sentence
Sentence -> Constr
Sentence -> DataType
(forall b. Data b => b -> b) -> Sentence -> Sentence
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u
forall u. (forall d. Data d => d -> u) -> Sentence -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sentence)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
$cRule :: Constr
$cEquation :: Constr
$cMembership :: Constr
$tSentence :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapMp :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapM :: (forall d. Data d => d -> m d) -> Sentence -> m Sentence
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sentence -> m Sentence
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sentence -> u
gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sentence -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Sentence -> r
gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence
$cgmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sentence)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sentence)
dataTypeOf :: Sentence -> DataType
$cdataTypeOf :: Sentence -> DataType
toConstr :: Sentence -> Constr
$ctoConstr :: Sentence -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sentence
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sentence -> c Sentence
$cp1Data :: Typeable Sentence
Data)

-- ** Sentence Instances

instance GetRange Sentence

instance Pretty Sentence where
    pretty :: Sentence -> Doc
pretty sent :: Sentence
sent = case Sentence
sent of
        Membership mb :: Membership
mb -> Membership -> Doc
forall a. Pretty a => a -> Doc
pretty Membership
mb
        Equation eq :: Equation
eq -> Equation -> Doc
forall a. Pretty a => a -> Doc
pretty Equation
eq
        Rule rl :: Rule
rl -> Rule -> Doc
forall a. Pretty a => a -> Doc
pretty Rule
rl
    pretties :: [Sentence] -> Doc
pretties = [Doc] -> Doc
vcat ([Doc] -> Doc) -> ([Sentence] -> [Doc]) -> [Sentence] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sentence -> Doc) -> [Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Sentence -> Doc
forall a. Pretty a => a -> Doc
pretty

instance HasSorts Sentence where
    getSorts :: Sentence -> SymbolSet
getSorts sen :: Sentence
sen = case Sentence
sen of
        Membership mb :: Membership
mb -> Membership -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Membership
mb
        Equation eq :: Equation
eq -> Equation -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Equation
eq
        Rule rl :: Rule
rl -> Rule -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts Rule
rl
    mapSorts :: SymbolMap -> Sentence -> Sentence
mapSorts mp :: SymbolMap
mp sen :: Sentence
sen = case Sentence
sen of
        Membership mb :: Membership
mb -> Membership -> Sentence
Membership (Membership -> Sentence) -> Membership -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Membership -> Membership
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Membership
mb
        Equation eq :: Equation
eq -> Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Equation -> Equation
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Equation
eq
        Rule rl :: Rule
rl -> Rule -> Sentence
Rule (Rule -> Sentence) -> Rule -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Rule -> Rule
forall a. HasSorts a => SymbolMap -> a -> a
mapSorts SymbolMap
mp Rule
rl

instance HasOps Sentence where
    getOps :: Sentence -> SymbolSet
getOps sen :: Sentence
sen = case Sentence
sen of
        Membership mb :: Membership
mb -> Membership -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Membership
mb
        Equation eq :: Equation
eq -> Equation -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Equation
eq
        Rule rl :: Rule
rl -> Rule -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps Rule
rl
    mapOps :: SymbolMap -> Sentence -> Sentence
mapOps mp :: SymbolMap
mp sen :: Sentence
sen = case Sentence
sen of
        Membership mb :: Membership
mb -> Membership -> Sentence
Membership (Membership -> Sentence) -> Membership -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Membership -> Membership
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Membership
mb
        Equation eq :: Equation
eq -> Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Equation -> Equation
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Equation
eq
        Rule rl :: Rule
rl -> Rule -> Sentence
Rule (Rule -> Sentence) -> Rule -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Rule -> Rule
forall a. HasOps a => SymbolMap -> a -> a
mapOps SymbolMap
mp Rule
rl

instance HasLabels Sentence where
    getLabels :: Sentence -> SymbolSet
getLabels sen :: Sentence
sen = case Sentence
sen of
        Membership mb :: Membership
mb -> Membership -> SymbolSet
forall a. HasLabels a => a -> SymbolSet
getLabels Membership
mb
        Equation eq :: Equation
eq -> Equation -> SymbolSet
forall a. HasLabels a => a -> SymbolSet
getLabels Equation
eq
        Rule rl :: Rule
rl -> Rule -> SymbolSet
forall a. HasLabels a => a -> SymbolSet
getLabels Rule
rl
    mapLabels :: SymbolMap -> Sentence -> Sentence
mapLabels mp :: SymbolMap
mp sen :: Sentence
sen = case Sentence
sen of
        Membership mb :: Membership
mb -> Membership -> Sentence
Membership (Membership -> Sentence) -> Membership -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Membership -> Membership
forall a. HasLabels a => SymbolMap -> a -> a
mapLabels SymbolMap
mp Membership
mb
        Equation eq :: Equation
eq -> Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Equation -> Equation
forall a. HasLabels a => SymbolMap -> a -> a
mapLabels SymbolMap
mp Equation
eq
        Rule rl :: Rule
rl -> Rule -> Sentence
Rule (Rule -> Sentence) -> Rule -> Sentence
forall a b. (a -> b) -> a -> b
$ SymbolMap -> Rule -> Rule
forall a. HasLabels a => SymbolMap -> a -> a
mapLabels SymbolMap
mp Rule
rl

-- * Contruction

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

-- | Extract the 'Sentence's from the given 'Statement's.
fromStatements :: [Statement] -> [Sentence]
fromStatements :: [Statement] -> [Sentence]
fromStatements stmts :: [Statement]
stmts = let
    convert :: Statement -> [Sentence]
convert stmt :: Statement
stmt = case Statement
stmt of
        -- SubsortStmnt sub -> [fromSubsort sub]
        OpStmnt op :: Operator
op -> Operator -> [Sentence]
fromOperator Operator
op
        MbStmnt mb :: Membership
mb -> [Membership -> Sentence
Membership Membership
mb]
        EqStmnt eq :: Equation
eq -> [Equation -> Sentence
Equation Equation
eq]
        RlStmnt rl :: Rule
rl -> [Rule -> Sentence
Rule Rule
rl]
        _ -> []
    in (Statement -> [Sentence]) -> [Statement] -> [Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Statement -> [Sentence]
convert [Statement]
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 :: Operator -> [Sentence]
fromOperator (Op op :: OpId
op dom :: [Type]
dom cod :: Type
cod attrs :: [Attr]
attrs) = let
    name :: Qid
name = OpId -> Qid
forall a. HasName a => a -> Qid
getName OpId
op
    first :: Type
first : second :: Type
second : _ = [Type]
dom
    convert :: Attr -> [Sentence]
convert attr :: Attr
attr = case Attr
attr of
        Assoc -> Qid -> Type -> Type -> Type -> [Sentence]
assocEq Qid
name Type
first Type
second Type
cod
        Comm -> Qid -> Type -> Type -> Type -> [Sentence]
commEq Qid
name Type
first Type
second Type
cod
        Idem -> Qid -> Type -> Type -> [Sentence]
idemEq Qid
name Type
first Type
cod
        Id term :: Term
term -> Qid -> Type -> Term -> Type -> [Sentence]
identityEq Qid
name Type
first Term
term Type
cod
        LeftId term :: Term
term -> Qid -> Type -> Term -> Type -> [Sentence]
leftIdEq Qid
name Type
first Term
term Type
cod
        RightId term :: Term
term -> Qid -> Type -> Term -> Type -> [Sentence]
rightIdEq Qid
name Type
first Term
term Type
cod
        _ -> []
    in (Attr -> [Sentence]) -> [Attr] -> [Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Attr -> [Sentence]
convert [Attr]
attrs

commEq :: Qid -> Type -> Type -> Type -> [Sentence]
commEq :: Qid -> Type -> Type -> Type -> [Sentence]
commEq op :: Qid
op ar1 :: Type
ar1 ar2 :: Type
ar2 co :: Type
co = [Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t1 Term
t2 [] []]
    where v1 :: Term
v1 = String -> Type -> Term
mkVar "v1" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar1
          v2 :: Term
v2 = String -> Type -> Term
mkVar "v2" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar2
          t1 :: Term
t1 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v1, Term
v2] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          t2 :: Term
t2 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v2, Term
v1] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co

assocEq :: Qid -> Type -> Type -> Type -> [Sentence]
assocEq :: Qid -> Type -> Type -> Type -> [Sentence]
assocEq op :: Qid
op ar1 :: Type
ar1 ar2 :: Type
ar2 co :: Type
co = [Sentence
eq]
    where v1 :: Term
v1 = String -> Type -> Term
mkVar "v1" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar1
          v2 :: Term
v2 = String -> Type -> Term
mkVar "v2" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar2
          v3 :: Term
v3 = String -> Type -> Term
mkVar "v3" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar2
          t1 :: Term
t1 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v1, Term
v2] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          t2 :: Term
t2 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
t1, Term
v3] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          t3 :: Term
t3 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v2, Term
v3] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          t4 :: Term
t4 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v1, Term
t3] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          eq :: Sentence
eq = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t2 Term
t4 [] []

idemEq :: Qid -> Type -> Type -> [Sentence]
idemEq :: Qid -> Type -> Type -> [Sentence]
idemEq op :: Qid
op ar :: Type
ar co :: Type
co = [Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t Term
v [] []]
    where v :: Term
v = Qid -> [Term] -> Type -> Term
Apply (String -> Qid
mkSimpleId "v") [] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar
          t :: Term
t = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v, Term
v] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co

identityEq :: Qid -> Type -> Term -> Type -> [Sentence]
identityEq :: Qid -> Type -> Term -> Type -> [Sentence]
identityEq op :: Qid
op ar1 :: Type
ar1 idt :: Term
idt co :: Type
co = [Sentence
eq1, Sentence
eq2]
    where idt' :: Term
idt' = Term -> Term
const2kind Term
idt
          v :: Term
v = String -> Type -> Term
mkVar "v" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar1
          t1 :: Term
t1 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v, Term
idt'] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          t2 :: Term
t2 = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
idt', Term
v] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          eq1 :: Sentence
eq1 = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t1 Term
v [] []
          eq2 :: Sentence
eq2 = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t2 Term
v [] []

leftIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
leftIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
leftIdEq op :: Qid
op ar1 :: Type
ar1 idt :: Term
idt co :: Type
co = [Sentence
eq1, Sentence
eq2]
    where idt' :: Term
idt' = Term -> Term
const2kind Term
idt
          v :: Term
v = String -> Type -> Term
mkVar "v" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar1
          t :: Term
t = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
idt', Term
v] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          eq1 :: Sentence
eq1 = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t Term
v [] []
          eq2 :: Sentence
eq2 = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
v Term
t [] []

rightIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
rightIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
rightIdEq op :: Qid
op ar1 :: Type
ar1 idt :: Term
idt co :: Type
co = [Sentence
eq1, Sentence
eq2]
    where idt' :: Term
idt' = Term -> Term
const2kind Term
idt
          v :: Term
v = String -> Type -> Term
mkVar "v" (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ar1
          t :: Term
t = Qid -> [Term] -> Type -> Term
Apply Qid
op [Term
v, Term
idt'] (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
co
          eq1 :: Sentence
eq1 = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
t Term
v [] []
          eq2 :: Sentence
eq2 = Equation -> Sentence
Equation (Equation -> Sentence) -> Equation -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term -> [Condition] -> [StmntAttr] -> Equation
Eq Term
v Term
t [] []

type2Kind :: Type -> Type
type2Kind :: Type -> Type
type2Kind (TypeSort (SortId s :: Qid
s)) = Kind -> Type
TypeKind (Kind -> Type) -> Kind -> Type
forall a b. (a -> b) -> a -> b
$ Qid -> Kind
KindId Qid
s
type2Kind k :: Type
k = Type
k

const2kind :: Term -> Term
const2kind :: Term -> Term
const2kind (Const q :: Qid
q ty :: Type
ty) = Qid -> Type -> Term
Const Qid
q (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type
type2Kind Type
ty
const2kind t :: Term
t = Term
t

-- * Testing

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