{-# 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