Copyright	(c) Daniel Calegari Universidad de la Republica Uruguay 2013
License	GPLv2 or higher, see LICENSE.txt
Maintainer	dcalegar@fing.edu.uy
Stability	provisional
Portability	portable
Safe Haskell	Safe

QVTR.Sign

Description

Documentation

data RuleDef Source #

Constructors

RuleDef
Fields name :: String top :: Bool parameters :: [TypeClass]

Instances

Instances details

Eq RuleDef Source #
Instance details Defined in QVTR.Sign Methods (==) :: RuleDef -> RuleDef -> Bool (/=) :: RuleDef -> RuleDef -> Bool
Data RuleDef Source #
Instance details Defined in QVTR.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RuleDef -> c RuleDef gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RuleDef toConstr :: RuleDef -> Constr dataTypeOf :: RuleDef -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RuleDef) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RuleDef) gmapT :: (forall b. Data b => b -> b) -> RuleDef -> RuleDef gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RuleDef -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RuleDef -> r gmapQ :: (forall d. Data d => d -> u) -> RuleDef -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RuleDef -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RuleDef -> m RuleDef gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RuleDef -> m RuleDef gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RuleDef -> m RuleDef
Ord RuleDef Source #
Instance details Defined in QVTR.Sign Methods compare :: RuleDef -> RuleDef -> Ordering (<) :: RuleDef -> RuleDef -> Bool (<=) :: RuleDef -> RuleDef -> Bool (>) :: RuleDef -> RuleDef -> Bool (>=) :: RuleDef -> RuleDef -> Bool max :: RuleDef -> RuleDef -> RuleDef min :: RuleDef -> RuleDef -> RuleDef
Show RuleDef Source #
Instance details Defined in QVTR.Sign Methods showsPrec :: Int -> RuleDef -> ShowS show :: RuleDef -> String showList :: [RuleDef] -> ShowS
Generic RuleDef
Instance details Defined in QVTR.ATC_QVTR Associated Types type Rep RuleDef :: Type -> Type Methods from :: RuleDef -> Rep RuleDef x to :: Rep RuleDef x -> RuleDef
FromJSON RuleDef
Instance details Defined in QVTR.ATC_QVTR Methods parseJSON :: Value -> Parser RuleDef parseJSONList :: Value -> Parser [RuleDef]
ToJSON RuleDef
Instance details Defined in QVTR.ATC_QVTR Methods toJSON :: RuleDef -> Value toEncoding :: RuleDef -> Encoding toJSONList :: [RuleDef] -> Value toEncodingList :: [RuleDef] -> Encoding
ShATermConvertible RuleDef
Instance details Defined in QVTR.ATC_QVTR Methods toShATermAux :: ATermTable -> RuleDef -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RuleDef] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RuleDef) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RuleDef])
Pretty RuleDef Source #
Instance details Defined in QVTR.Sign Methods pretty :: RuleDef -> Doc Source # pretties :: [RuleDef] -> Doc Source #
type Rep RuleDef
Instance details Defined in QVTR.ATC_QVTR type Rep RuleDef = D1 ('MetaData "RuleDef" "QVTR.Sign" "main" 'False) (C1 ('MetaCons "RuleDef" 'PrefixI 'True) (S1 ('MetaSel ('Just "name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: (S1 ('MetaSel ('Just "top") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "parameters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypeClass]))))

data Sign Source #

Constructors

Sign
Fields sourceSign :: Sign targetSign :: Sign nonTopRelations :: Map String RuleDef topRelations :: Map String RuleDef keyDefs :: [(String, String)]

Instances

Instances details

Eq Sign Source #
Instance details Defined in QVTR.Sign Methods (==) :: Sign -> Sign -> Bool (/=) :: Sign -> Sign -> Bool
Data Sign Source #
Instance details Defined in QVTR.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign toConstr :: Sign -> Constr dataTypeOf :: Sign -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sign) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign) gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign
Ord Sign Source #
Instance details Defined in QVTR.Sign Methods compare :: Sign -> Sign -> Ordering (<) :: Sign -> Sign -> Bool (<=) :: Sign -> Sign -> Bool (>) :: Sign -> Sign -> Bool (>=) :: Sign -> Sign -> Bool max :: Sign -> Sign -> Sign min :: Sign -> Sign -> Sign
Show Sign Source #
Instance details Defined in QVTR.Sign Methods showsPrec :: Int -> Sign -> ShowS show :: Sign -> String showList :: [Sign] -> ShowS
Generic Sign
Instance details Defined in QVTR.ATC_QVTR Associated Types type Rep Sign :: Type -> Type Methods from :: Sign -> Rep Sign x to :: Rep Sign x -> Sign
GetRange Sign Source #
Instance details Defined in QVTR.Sign Methods getRange :: Sign -> Range Source # rangeSpan :: Sign -> [Pos] Source #
FromJSON Sign
Instance details Defined in QVTR.ATC_QVTR Methods parseJSON :: Value -> Parser Sign parseJSONList :: Value -> Parser [Sign]
ToJSON Sign
Instance details Defined in QVTR.ATC_QVTR Methods toJSON :: Sign -> Value toEncoding :: Sign -> Encoding toJSONList :: [Sign] -> Value toEncodingList :: [Sign] -> Encoding
ShATermConvertible Sign
Instance details Defined in QVTR.ATC_QVTR Methods toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])
Pretty Sign Source #
Instance details Defined in QVTR.Sign Methods pretty :: Sign -> Doc Source # pretties :: [Sign] -> Doc Source #
Sentences QVTR Sen Sign Morphism () Source #
Instance details Defined in QVTR.Logic_QVTR Methods map_sen :: QVTR -> Morphism -> Sen -> Result Sen Source # simplify_sen :: QVTR -> Sign -> Sen -> Sen Source # negation :: QVTR -> Sen -> Maybe Sen Source # print_sign :: QVTR -> Sign -> Doc Source # print_named :: QVTR -> Named Sen -> Doc Source # sym_of :: QVTR -> Sign -> [Set ()] Source # mostSymsOf :: QVTR -> Sign -> [()] Source # symmap_of :: QVTR -> Morphism -> EndoMap () Source # sym_name :: QVTR -> () -> Id Source # sym_label :: QVTR -> () -> Maybe String Source # fullSymName :: QVTR -> () -> String Source # symKind :: QVTR -> () -> String Source # symsOfSen :: QVTR -> Sign -> Sen -> [()] Source # pair_symbols :: QVTR -> () -> () -> Result () Source #
StaticAnalysis QVTR Transformation Sen () () Sign Morphism () () Source #
Instance details Defined in QVTR.Logic_QVTR Methods basic_analysis :: QVTR -> Maybe ((Transformation, Sign, GlobalAnnos) -> Result (Transformation, ExtSign Sign (), [Named Sen])) Source # sen_analysis :: QVTR -> Maybe ((Transformation, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: QVTR -> IRI -> LibName -> Transformation -> Sign -> GlobalAnnos -> Result (Transformation, ExtSign Sign (), [Named Sen]) Source # stat_symb_map_items :: QVTR -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: QVTR -> Sign -> [()] -> Result [()] Source # convertTheory :: QVTR -> Maybe ((Sign, [Named Sen]) -> Transformation) Source # ensures_amalgamability :: QVTR -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QVTR -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: QVTR -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QVTR -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: QVTR -> () -> () Source # id_to_raw :: QVTR -> Id -> () Source # matches :: QVTR -> () -> () -> Bool Source # empty_signature :: QVTR -> Sign Source # add_symb_to_sign :: QVTR -> Sign -> () -> Result Sign Source # signature_union :: QVTR -> Sign -> Sign -> Result Sign Source # signatureDiff :: QVTR -> Sign -> Sign -> Result Sign Source # intersection :: QVTR -> Sign -> Sign -> Result Sign Source # final_union :: QVTR -> Sign -> Sign -> Result Sign Source # morphism_union :: QVTR -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QVTR -> Sign -> Sign -> Bool Source # subsig_inclusion :: QVTR -> Sign -> Sign -> Result Morphism Source # generated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source # cogenerated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source # induced_from_morphism :: QVTR -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: QVTR -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result Morphism Source # is_transportable :: QVTR -> Morphism -> Bool Source # is_injective :: QVTR -> Morphism -> Bool Source # theory_to_taxonomy :: QVTR -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: QVTR -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: QVTR -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: QVTR -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #
Logic QVTR () Transformation Sen () () Sign Morphism () () () Source #
Instance details Defined in QVTR.Logic_QVTR Methods parse_basic_sen :: QVTR -> Maybe (Transformation -> AParser st Sen) Source # stability :: QVTR -> Stability Source # data_logic :: QVTR -> Maybe AnyLogic Source # top_sublogic :: QVTR -> () Source # all_sublogics :: QVTR -> [()] Source # bottomSublogic :: QVTR -> Maybe () Source # sublogicDimensions :: QVTR -> [[()]] Source # parseSublogic :: QVTR -> String -> Maybe () Source # proj_sublogic_epsilon :: QVTR -> () -> Sign -> Morphism Source # provers :: QVTR -> [Prover Sign Sen Morphism () ()] Source # default_prover :: QVTR -> String Source # cons_checkers :: QVTR -> [ConsChecker Sign Sen () Morphism ()] Source # conservativityCheck :: QVTR -> [ConservativityChecker Sign Sen Morphism] Source # empty_proof_tree :: QVTR -> () Source # syntaxTable :: QVTR -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QVTR -> Maybe OMCD Source # export_symToOmdoc :: QVTR -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: QVTR -> NameMap () -> Sen -> Result TCorOMElement Source # export_theoryToOmdoc :: QVTR -> SigMap () -> Sign -> [Named Sen] -> Result [TCElement] Source # omdocToSym :: QVTR -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: QVTR -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sen)) Source # addOMadtToTheory :: QVTR -> SigMapI () -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source # addOmdocToTheory :: QVTR -> SigMapI () -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source # sublogicOfTheo :: QVTR -> (Sign, [Sen]) -> () Source #
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.QVTR2CASL Methods sourceLogic :: QVTR2CASL -> QVTR Source # sourceSublogic :: QVTR2CASL -> () Source # sourceSublogicLossy :: QVTR2CASL -> () Source # minSourceTheory :: QVTR2CASL -> Maybe (LibName, String) Source # targetLogic :: QVTR2CASL -> CASL Source # mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source # map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source # extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: QVTR2CASL -> Bool Source # has_model_expansion :: QVTR2CASL -> Bool Source # is_weakly_amalgamable :: QVTR2CASL -> Bool Source # constituents :: QVTR2CASL -> [String] Source # isInclusionComorphism :: QVTR2CASL -> Bool Source # rps :: QVTR2CASL -> Bool Source # eps :: QVTR2CASL -> Bool Source # isGTC :: QVTR2CASL -> Bool Source #
type Rep Sign
Instance details Defined in QVTR.ATC_QVTR type Rep Sign = D1 ('MetaData "Sign" "QVTR.Sign" "main" 'False) (C1 ('MetaCons "Sign" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sourceSign") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sign) :: S1 ('MetaSel ('Just "targetSign") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sign)) :: (S1 ('MetaSel ('Just "nonTopRelations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map String RuleDef)) :: (S1 ('MetaSel ('Just "topRelations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map String RuleDef)) :: S1 ('MetaSel ('Just "keyDefs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, String)])))))

emptySign :: Sign Source #

data Sen Source #

Constructors

KeyConstr
Fields keyConst :: Key
QVTSen
Fields rule :: RelationSen

Instances

Instances details

Eq Sen Source #
Instance details Defined in QVTR.Sign Methods (==) :: Sen -> Sen -> Bool (/=) :: Sen -> Sen -> Bool
Data Sen Source #
Instance details Defined in QVTR.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sen -> c Sen gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sen toConstr :: Sen -> Constr dataTypeOf :: Sen -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sen) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sen) gmapT :: (forall b. Data b => b -> b) -> Sen -> Sen gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sen -> r gmapQ :: (forall d. Data d => d -> u) -> Sen -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sen -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sen -> m Sen gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sen -> m Sen gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sen -> m Sen
Ord Sen Source #
Instance details Defined in QVTR.Sign Methods compare :: Sen -> Sen -> Ordering (<) :: Sen -> Sen -> Bool (<=) :: Sen -> Sen -> Bool (>) :: Sen -> Sen -> Bool (>=) :: Sen -> Sen -> Bool max :: Sen -> Sen -> Sen min :: Sen -> Sen -> Sen
Show Sen Source #
Instance details Defined in QVTR.Sign Methods showsPrec :: Int -> Sen -> ShowS show :: Sen -> String showList :: [Sen] -> ShowS
Generic Sen
Instance details Defined in QVTR.ATC_QVTR Associated Types type Rep Sen :: Type -> Type Methods from :: Sen -> Rep Sen x to :: Rep Sen x -> Sen
GetRange Sen Source #
Instance details Defined in QVTR.Sign Methods getRange :: Sen -> Range Source # rangeSpan :: Sen -> [Pos] Source #
FromJSON Sen
Instance details Defined in QVTR.ATC_QVTR Methods parseJSON :: Value -> Parser Sen parseJSONList :: Value -> Parser [Sen]
ToJSON Sen
Instance details Defined in QVTR.ATC_QVTR Methods toJSON :: Sen -> Value toEncoding :: Sen -> Encoding toJSONList :: [Sen] -> Value toEncodingList :: [Sen] -> Encoding
ShATermConvertible Sen
Instance details Defined in QVTR.ATC_QVTR Methods toShATermAux :: ATermTable -> Sen -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sen] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sen) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sen])
Pretty Sen Source #
Instance details Defined in QVTR.Sign Methods pretty :: Sen -> Doc Source # pretties :: [Sen] -> Doc Source #
Sentences QVTR Sen Sign Morphism () Source #
Instance details Defined in QVTR.Logic_QVTR Methods map_sen :: QVTR -> Morphism -> Sen -> Result Sen Source # simplify_sen :: QVTR -> Sign -> Sen -> Sen Source # negation :: QVTR -> Sen -> Maybe Sen Source # print_sign :: QVTR -> Sign -> Doc Source # print_named :: QVTR -> Named Sen -> Doc Source # sym_of :: QVTR -> Sign -> [Set ()] Source # mostSymsOf :: QVTR -> Sign -> [()] Source # symmap_of :: QVTR -> Morphism -> EndoMap () Source # sym_name :: QVTR -> () -> Id Source # sym_label :: QVTR -> () -> Maybe String Source # fullSymName :: QVTR -> () -> String Source # symKind :: QVTR -> () -> String Source # symsOfSen :: QVTR -> Sign -> Sen -> [()] Source # pair_symbols :: QVTR -> () -> () -> Result () Source #
StaticAnalysis QVTR Transformation Sen () () Sign Morphism () () Source #
Instance details Defined in QVTR.Logic_QVTR Methods basic_analysis :: QVTR -> Maybe ((Transformation, Sign, GlobalAnnos) -> Result (Transformation, ExtSign Sign (), [Named Sen])) Source # sen_analysis :: QVTR -> Maybe ((Transformation, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: QVTR -> IRI -> LibName -> Transformation -> Sign -> GlobalAnnos -> Result (Transformation, ExtSign Sign (), [Named Sen]) Source # stat_symb_map_items :: QVTR -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: QVTR -> Sign -> [()] -> Result [()] Source # convertTheory :: QVTR -> Maybe ((Sign, [Named Sen]) -> Transformation) Source # ensures_amalgamability :: QVTR -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QVTR -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: QVTR -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QVTR -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: QVTR -> () -> () Source # id_to_raw :: QVTR -> Id -> () Source # matches :: QVTR -> () -> () -> Bool Source # empty_signature :: QVTR -> Sign Source # add_symb_to_sign :: QVTR -> Sign -> () -> Result Sign Source # signature_union :: QVTR -> Sign -> Sign -> Result Sign Source # signatureDiff :: QVTR -> Sign -> Sign -> Result Sign Source # intersection :: QVTR -> Sign -> Sign -> Result Sign Source # final_union :: QVTR -> Sign -> Sign -> Result Sign Source # morphism_union :: QVTR -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QVTR -> Sign -> Sign -> Bool Source # subsig_inclusion :: QVTR -> Sign -> Sign -> Result Morphism Source # generated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source # cogenerated_sign :: QVTR -> Set () -> Sign -> Result Morphism Source # induced_from_morphism :: QVTR -> EndoMap () -> Sign -> Result Morphism Source # induced_from_to_morphism :: QVTR -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result Morphism Source # is_transportable :: QVTR -> Morphism -> Bool Source # is_injective :: QVTR -> Morphism -> Bool Source # theory_to_taxonomy :: QVTR -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: QVTR -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap (), EndoMap ()) Source # equiv2cospan :: QVTR -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source # extract_module :: QVTR -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #
Logic QVTR () Transformation Sen () () Sign Morphism () () () Source #
Instance details Defined in QVTR.Logic_QVTR Methods parse_basic_sen :: QVTR -> Maybe (Transformation -> AParser st Sen) Source # stability :: QVTR -> Stability Source # data_logic :: QVTR -> Maybe AnyLogic Source # top_sublogic :: QVTR -> () Source # all_sublogics :: QVTR -> [()] Source # bottomSublogic :: QVTR -> Maybe () Source # sublogicDimensions :: QVTR -> [[()]] Source # parseSublogic :: QVTR -> String -> Maybe () Source # proj_sublogic_epsilon :: QVTR -> () -> Sign -> Morphism Source # provers :: QVTR -> [Prover Sign Sen Morphism () ()] Source # default_prover :: QVTR -> String Source # cons_checkers :: QVTR -> [ConsChecker Sign Sen () Morphism ()] Source # conservativityCheck :: QVTR -> [ConservativityChecker Sign Sen Morphism] Source # empty_proof_tree :: QVTR -> () Source # syntaxTable :: QVTR -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QVTR -> Maybe OMCD Source # export_symToOmdoc :: QVTR -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: QVTR -> NameMap () -> Sen -> Result TCorOMElement Source # export_theoryToOmdoc :: QVTR -> SigMap () -> Sign -> [Named Sen] -> Result [TCElement] Source # omdocToSym :: QVTR -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: QVTR -> SigMapI () -> TCElement -> String -> Result (Maybe (Named Sen)) Source # addOMadtToTheory :: QVTR -> SigMapI () -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source # addOmdocToTheory :: QVTR -> SigMapI () -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source # sublogicOfTheo :: QVTR -> (Sign, [Sen]) -> () Source #
Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.QVTR2CASL Methods sourceLogic :: QVTR2CASL -> QVTR Source # sourceSublogic :: QVTR2CASL -> () Source # sourceSublogicLossy :: QVTR2CASL -> () Source # minSourceTheory :: QVTR2CASL -> Maybe (LibName, String) Source # targetLogic :: QVTR2CASL -> CASL Source # mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: QVTR2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor Source # map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: QVTR2CASL -> Sign -> () -> Set Symbol Source # extractModel :: QVTR2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: QVTR2CASL -> Bool Source # has_model_expansion :: QVTR2CASL -> Bool Source # is_weakly_amalgamable :: QVTR2CASL -> Bool Source # constituents :: QVTR2CASL -> [String] Source # isInclusionComorphism :: QVTR2CASL -> Bool Source # rps :: QVTR2CASL -> Bool Source # eps :: QVTR2CASL -> Bool Source # isGTC :: QVTR2CASL -> Bool Source #
type Rep Sen
Instance details Defined in QVTR.ATC_QVTR type Rep Sen = D1 ('MetaData "Sen" "QVTR.Sign" "main" 'False) (C1 ('MetaCons "KeyConstr" 'PrefixI 'True) (S1 ('MetaSel ('Just "keyConst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Key)) :+: C1 ('MetaCons "QVTSen" 'PrefixI 'True) (S1 ('MetaSel ('Just "rule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RelationSen)))

data RelationSen Source #

Constructors

RelationSen
Fields ruleDef :: RuleDef varSet :: [RelVar] parSet :: [RelVar] sourcePattern :: Pattern targetPattern :: Pattern whenClause :: Maybe WhenWhere whereClause :: Maybe WhenWhere

Instances

Instances details

Eq RelationSen Source #
Instance details Defined in QVTR.Sign Methods (==) :: RelationSen -> RelationSen -> Bool (/=) :: RelationSen -> RelationSen -> Bool
Data RelationSen Source #
Instance details Defined in QVTR.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RelationSen -> c RelationSen gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RelationSen toConstr :: RelationSen -> Constr dataTypeOf :: RelationSen -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RelationSen) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelationSen) gmapT :: (forall b. Data b => b -> b) -> RelationSen -> RelationSen gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelationSen -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelationSen -> r gmapQ :: (forall d. Data d => d -> u) -> RelationSen -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RelationSen -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RelationSen -> m RelationSen gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RelationSen -> m RelationSen gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RelationSen -> m RelationSen
Ord RelationSen Source #
Instance details Defined in QVTR.Sign Methods compare :: RelationSen -> RelationSen -> Ordering (<) :: RelationSen -> RelationSen -> Bool (<=) :: RelationSen -> RelationSen -> Bool (>) :: RelationSen -> RelationSen -> Bool (>=) :: RelationSen -> RelationSen -> Bool max :: RelationSen -> RelationSen -> RelationSen min :: RelationSen -> RelationSen -> RelationSen
Show RelationSen Source #
Instance details Defined in QVTR.Sign Methods showsPrec :: Int -> RelationSen -> ShowS show :: RelationSen -> String showList :: [RelationSen] -> ShowS
Generic RelationSen
Instance details Defined in QVTR.ATC_QVTR Associated Types type Rep RelationSen :: Type -> Type Methods from :: RelationSen -> Rep RelationSen x to :: Rep RelationSen x -> RelationSen
GetRange RelationSen Source #
Instance details Defined in QVTR.Sign Methods getRange :: RelationSen -> Range Source # rangeSpan :: RelationSen -> [Pos] Source #
FromJSON RelationSen
Instance details Defined in QVTR.ATC_QVTR Methods parseJSON :: Value -> Parser RelationSen parseJSONList :: Value -> Parser [RelationSen]
ToJSON RelationSen
Instance details Defined in QVTR.ATC_QVTR Methods toJSON :: RelationSen -> Value toEncoding :: RelationSen -> Encoding toJSONList :: [RelationSen] -> Value toEncodingList :: [RelationSen] -> Encoding
ShATermConvertible RelationSen
Instance details Defined in QVTR.ATC_QVTR Methods toShATermAux :: ATermTable -> RelationSen -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RelationSen] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RelationSen) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RelationSen])
Pretty RelationSen Source #
Instance details Defined in QVTR.Sign Methods pretty :: RelationSen -> Doc Source # pretties :: [RelationSen] -> Doc Source #
type Rep RelationSen
Instance details Defined in QVTR.ATC_QVTR type Rep RelationSen = D1 ('MetaData "RelationSen" "QVTR.Sign" "main" 'False) (C1 ('MetaCons "RelationSen" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ruleDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RuleDef) :: (S1 ('MetaSel ('Just "varSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RelVar]) :: S1 ('MetaSel ('Just "parSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RelVar]))) :: ((S1 ('MetaSel ('Just "sourcePattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :: S1 ('MetaSel ('Just "targetPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern)) :: (S1 ('MetaSel ('Just "whenClause") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe WhenWhere)) :: S1 ('MetaSel ('Just "whereClause") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe WhenWhere))))))

data Pattern Source #

Constructors

Pattern
Fields patVarSet :: [RelVar] patRels :: [(PropertyT, RelVar, RelVar)] patPreds :: [(String, String, OCL)]

Instances

Instances details

Eq Pattern Source #
Instance details Defined in QVTR.Sign Methods (==) :: Pattern -> Pattern -> Bool (/=) :: Pattern -> Pattern -> Bool
Data Pattern Source #
Instance details Defined in QVTR.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern -> c Pattern gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pattern toConstr :: Pattern -> Constr dataTypeOf :: Pattern -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pattern) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pattern) gmapT :: (forall b. Data b => b -> b) -> Pattern -> Pattern gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern -> r gmapQ :: (forall d. Data d => d -> u) -> Pattern -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern -> m Pattern
Ord Pattern Source #
Instance details Defined in QVTR.Sign Methods compare :: Pattern -> Pattern -> Ordering (<) :: Pattern -> Pattern -> Bool (<=) :: Pattern -> Pattern -> Bool (>) :: Pattern -> Pattern -> Bool (>=) :: Pattern -> Pattern -> Bool max :: Pattern -> Pattern -> Pattern min :: Pattern -> Pattern -> Pattern
Show Pattern Source #
Instance details Defined in QVTR.Sign Methods showsPrec :: Int -> Pattern -> ShowS show :: Pattern -> String showList :: [Pattern] -> ShowS
Generic Pattern
Instance details Defined in QVTR.ATC_QVTR Associated Types type Rep Pattern :: Type -> Type Methods from :: Pattern -> Rep Pattern x to :: Rep Pattern x -> Pattern
GetRange Pattern Source #
Instance details Defined in QVTR.Sign Methods getRange :: Pattern -> Range Source # rangeSpan :: Pattern -> [Pos] Source #
FromJSON Pattern
Instance details Defined in QVTR.ATC_QVTR Methods parseJSON :: Value -> Parser Pattern parseJSONList :: Value -> Parser [Pattern]
ToJSON Pattern
Instance details Defined in QVTR.ATC_QVTR Methods toJSON :: Pattern -> Value toEncoding :: Pattern -> Encoding toJSONList :: [Pattern] -> Value toEncodingList :: [Pattern] -> Encoding
ShATermConvertible Pattern
Instance details Defined in QVTR.ATC_QVTR Methods toShATermAux :: ATermTable -> Pattern -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Pattern] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Pattern) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Pattern])
Pretty Pattern Source #
Instance details Defined in QVTR.Sign Methods pretty :: Pattern -> Doc Source # pretties :: [Pattern] -> Doc Source #
type Rep Pattern
Instance details Defined in QVTR.ATC_QVTR type Rep Pattern = D1 ('MetaData "Pattern" "QVTR.Sign" "main" 'False) (C1 ('MetaCons "Pattern" 'PrefixI 'True) (S1 ('MetaSel ('Just "patVarSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RelVar]) :: (S1 ('MetaSel ('Just "patRels") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(PropertyT, RelVar, RelVar)]) :: S1 ('MetaSel ('Just "patPreds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(String, String, OCL)]))))