Copyright	(c) Christian Maeder and Uni Bremen 2003-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

HasCASL.As

Contents

abstract syntax entities with small utility functions
symbol data types symbols
equality instances ignoring positions
compute better position

Description

abstract syntax for HasCASL, more liberal than Concrete-Syntax.txt, annotations are almost as for CASL

Synopsis

data BasicSpec = BasicSpec [Annoted BasicItem]
data BasicItem
- = SigItems SigItems
- | ProgItems [Annoted ProgEq] Range
- | ClassItems Instance [Annoted ClassItem] Range
- | GenVarItems [GenVarDecl] Range
- | FreeDatatype [Annoted DatatypeDecl] Range
- | GenItems [Annoted SigItems] Range
- | AxiomItems [GenVarDecl] [Annoted Term] Range
- | Internal [Annoted BasicItem] Range
data SigItems
- = TypeItems Instance [Annoted TypeItem] Range
- | OpItems OpBrand [Annoted OpItem] Range
data OpBrand
- = Pred
- | Op
- | Fun
isPred :: OpBrand -> Bool
data Instance
- = Instance
- | Plain
data ClassItem = ClassItem ClassDecl [Annoted BasicItem] Range
data ClassDecl = ClassDecl [Id] Kind Range
data Variance
- = InVar
- | CoVar
- | ContraVar
- | NonVar
data AnyKind a
- = ClassKind a
- | FunKind Variance (AnyKind a) (AnyKind a) Range
type Kind = AnyKind Id
type RawKind = AnyKind ()
data TypeItem
- = TypeDecl [TypePattern] Kind Range
- | SubtypeDecl [TypePattern] Type Range
- | IsoDecl [TypePattern] Range
- | SubtypeDefn TypePattern Vars Type (Annoted Term) Range
- | AliasType TypePattern (Maybe Kind) TypeScheme Range
- | Datatype DatatypeDecl
data Vars
- = Var Id
- | VarTuple [Vars] Range
data TypePattern
- = TypePattern Id [TypeArg] Range
- | TypePatternToken Token
- | MixfixTypePattern [TypePattern]
- | BracketTypePattern BracketKind [TypePattern] Range
- | TypePatternArg TypeArg Range
data Type
- = TypeName Id RawKind Int
- | TypeAppl Type Type
- | ExpandedType Type Type
- | TypeAbs TypeArg Type Range
- | KindedType Type (Set Kind) Range
- | TypeToken Token
- | BracketType BracketKind [Type] Range
- | MixfixType [Type]
mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme
data TypeScheme = TypeScheme [TypeArg] Type Range
data Partiality
- = Partial
- | Total
data OpItem
- = OpDecl [PolyId] TypeScheme [OpAttr] Range
- | OpDefn PolyId [[VarDecl]] TypeScheme Term Range
data BinOpAttr
- = Assoc
- | Comm
- | Idem
data OpAttr
- = BinOpAttr BinOpAttr Range
- | UnitOpAttr Term Range
data DatatypeDecl = DatatypeDecl TypePattern Kind [Annoted Alternative] [Id] Range
data Alternative
- = Constructor Id [[Component]] Partiality Range
- | Subtype [Type] Range
data Component
- = Selector Id Partiality Type SeparatorKind Range
- | NoSelector Type
data Quantifier
- = Universal
- | Existential
- | Unique
data TypeQual
- = OfType
- | AsType
- | InType
- | Inferred
data LetBrand
- = Let
- | Where
- | Program
data BracketKind
- = Parens
- | Squares
- | Braces
- | NoBrackets
getBrackets :: BracketKind -> (String, String)
data InstKind
- = UserGiven
- | Infer
data Term
- = QualVar VarDecl
- | QualOp OpBrand PolyId TypeScheme [Type] InstKind Range
- | ApplTerm Term Term Range
- | TupleTerm [Term] Range
- | TypedTerm Term TypeQual Type Range
- | AsPattern VarDecl Term Range
- | QuantifiedTerm Quantifier [GenVarDecl] Term Range
- | LambdaTerm [Term] Partiality Term Range
- | CaseTerm Term [ProgEq] Range
- | LetTerm LetBrand [ProgEq] Term Range
- | ResolvedMixTerm Id [Type] [Term] Range
- | TermToken Token
- | MixTypeTerm TypeQual Type Range
- | MixfixTerm [Term]
- | BracketTerm BracketKind [Term] Range
data ProgEq = ProgEq Term Term Range
data PolyId = PolyId Id [TypeArg] Range
data SeparatorKind
- = Comma
- | Other
data VarDecl = VarDecl Id Type SeparatorKind Range
data VarKind
- = VarKind Kind
- | Downset Type
- | MissingKind
data TypeArg = TypeArg Id Variance VarKind RawKind Int SeparatorKind Range
data GenVarDecl
- = GenVarDecl VarDecl
- | GenTypeVarDecl TypeArg
data SymbItems = SymbItems SymbKind [Symb] [Annotation] Range
data SymbMapItems = SymbMapItems SymbKind [SymbOrMap] [Annotation] Range
data SymbKind
- = Implicit
- | SyKtype
- | SyKsort
- | SyKfun
- | SyKop
- | SyKpred
- | SyKclass
data Symb = Symb Id (Maybe SymbType) Range
data SymbType = SymbType TypeScheme
data SymbOrMap = SymbOrMap Symb (Maybe Symb) Range
bestRange :: GetRange a => [a] -> Range -> Range

abstract syntax entities with small utility functions

data BasicSpec Source #

annotated basic items

Constructors

BasicSpec [Annoted BasicItem]

Instances

Instances details

Data BasicSpec Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BasicSpec -> c BasicSpec gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BasicSpec toConstr :: BasicSpec -> Constr dataTypeOf :: BasicSpec -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BasicSpec) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BasicSpec) gmapT :: (forall b. Data b => b -> b) -> BasicSpec -> BasicSpec gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpec -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpec -> r gmapQ :: (forall d. Data d => d -> u) -> BasicSpec -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BasicSpec -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BasicSpec -> m BasicSpec gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpec -> m BasicSpec gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpec -> m BasicSpec
Show BasicSpec Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> BasicSpec -> ShowS show :: BasicSpec -> String showList :: [BasicSpec] -> ShowS
Generic BasicSpec
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep BasicSpec :: Type -> Type Methods from :: BasicSpec -> Rep BasicSpec x to :: Rep BasicSpec x -> BasicSpec
Semigroup BasicSpec
Instance details Defined in HasCASL.Logic_HasCASL Methods (<>) :: BasicSpec -> BasicSpec -> BasicSpec # sconcat :: NonEmpty BasicSpec -> BasicSpec stimes :: Integral b => b -> BasicSpec -> BasicSpec
Monoid BasicSpec
Instance details Defined in HasCASL.Logic_HasCASL Methods mempty :: BasicSpec mappend :: BasicSpec -> BasicSpec -> BasicSpec mconcat :: [BasicSpec] -> BasicSpec
GetRange BasicSpec Source #
Instance details Defined in HasCASL.As Methods getRange :: BasicSpec -> Range Source # rangeSpan :: BasicSpec -> [Pos] Source #
FromJSON BasicSpec
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser BasicSpec parseJSONList :: Value -> Parser [BasicSpec]
ToJSON BasicSpec
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: BasicSpec -> Value toEncoding :: BasicSpec -> Encoding toJSONList :: [BasicSpec] -> Value toEncodingList :: [BasicSpec] -> Encoding
ShATermConvertible BasicSpec
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> BasicSpec -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BasicSpec] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BasicSpec) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BasicSpec])
Pretty BasicSpec Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: BasicSpec -> Doc Source # pretties :: [BasicSpec] -> Doc Source #
ProjectSublogic Sublogic BasicSpec Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogic :: Sublogic -> BasicSpec -> BasicSpec Source #
MinSublogic Sublogic BasicSpec Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: BasicSpec -> Sublogic Source #
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parsersAndPrinters :: HasCASL -> Map String (PrefixMap -> AParser st BasicSpec, BasicSpec -> Doc) Source # parse_basic_spec :: HasCASL -> Maybe (PrefixMap -> AParser st BasicSpec) Source # parseSingleSymbItem :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_map_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbMapItems) Source # toItem :: HasCASL -> BasicSpec -> Item Source # symb_items_name :: HasCASL -> SymbItems -> [String] Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep BasicSpec
Instance details Defined in HasCASL.ATC_HasCASL type Rep BasicSpec = D1 ('MetaData "BasicSpec" "HasCASL.As" "main" 'False) (C1 ('MetaCons "BasicSpec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted BasicItem])))

data BasicItem Source #

the possible items

Instances

Instances details

Data BasicItem Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BasicItem -> c BasicItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BasicItem toConstr :: BasicItem -> Constr dataTypeOf :: BasicItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BasicItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BasicItem) gmapT :: (forall b. Data b => b -> b) -> BasicItem -> BasicItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BasicItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BasicItem -> r gmapQ :: (forall d. Data d => d -> u) -> BasicItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BasicItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BasicItem -> m BasicItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicItem -> m BasicItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicItem -> m BasicItem
Show BasicItem Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> BasicItem -> ShowS show :: BasicItem -> String showList :: [BasicItem] -> ShowS
Generic BasicItem
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep BasicItem :: Type -> Type Methods from :: BasicItem -> Rep BasicItem x to :: Rep BasicItem x -> BasicItem
FromJSON BasicItem
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser BasicItem parseJSONList :: Value -> Parser [BasicItem]
ToJSON BasicItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: BasicItem -> Value toEncoding :: BasicItem -> Encoding toJSONList :: [BasicItem] -> Value toEncodingList :: [BasicItem] -> Encoding
ShATermConvertible BasicItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> BasicItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BasicItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BasicItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BasicItem])
Pretty BasicItem Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: BasicItem -> Doc Source # pretties :: [BasicItem] -> Doc Source #
type Rep BasicItem
Instance details Defined in HasCASL.ATC_HasCASL type Rep BasicItem = D1 ('MetaData "BasicItem" "HasCASL.As" "main" 'False) (((C1 ('MetaCons "SigItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SigItems)) :+: C1 ('MetaCons "ProgItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted ProgEq]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "ClassItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Instance) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted ClassItem]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "GenVarItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GenVarDecl]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "FreeDatatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted DatatypeDecl]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "GenItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SigItems]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "AxiomItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GenVarDecl]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted Term]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Internal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted BasicItem]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data SigItems Source #

signature items are types or functions

Constructors

TypeItems Instance [Annoted TypeItem] Range
OpItems OpBrand [Annoted OpItem] Range

Instances

Instances details

Data SigItems Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SigItems -> c SigItems gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SigItems toConstr :: SigItems -> Constr dataTypeOf :: SigItems -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SigItems) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SigItems) gmapT :: (forall b. Data b => b -> b) -> SigItems -> SigItems gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SigItems -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SigItems -> r gmapQ :: (forall d. Data d => d -> u) -> SigItems -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SigItems -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SigItems -> m SigItems gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SigItems -> m SigItems gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SigItems -> m SigItems
Show SigItems Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> SigItems -> ShowS show :: SigItems -> String showList :: [SigItems] -> ShowS
Generic SigItems
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep SigItems :: Type -> Type Methods from :: SigItems -> Rep SigItems x to :: Rep SigItems x -> SigItems
FromJSON SigItems
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser SigItems parseJSONList :: Value -> Parser [SigItems]
ToJSON SigItems
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: SigItems -> Value toEncoding :: SigItems -> Encoding toJSONList :: [SigItems] -> Value toEncodingList :: [SigItems] -> Encoding
ShATermConvertible SigItems
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> SigItems -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SigItems] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SigItems) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SigItems])
Pretty SigItems Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: SigItems -> Doc Source # pretties :: [SigItems] -> Doc Source #
type Rep SigItems
Instance details Defined in HasCASL.ATC_HasCASL type Rep SigItems = D1 ('MetaData "SigItems" "HasCASL.As" "main" 'False) (C1 ('MetaCons "TypeItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Instance) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted TypeItem]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "OpItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpBrand) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted OpItem]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data OpBrand Source #

indicator for predicate, operation or function

Constructors

Pred
Op
Fun

Instances

Instances details

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

isPred :: OpBrand -> Bool Source #

test if the function was declared as predicate

data Instance Source #

indicator in ClassItems and TypeItems

Constructors

Instance
Plain

Instances

Instances details

Eq Instance Source #
Instance details Defined in HasCASL.As Methods (==) :: Instance -> Instance -> Bool (/=) :: Instance -> Instance -> Bool
Data Instance Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Instance -> c Instance gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Instance toConstr :: Instance -> Constr dataTypeOf :: Instance -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Instance) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Instance) gmapT :: (forall b. Data b => b -> b) -> Instance -> Instance gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Instance -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Instance -> r gmapQ :: (forall d. Data d => d -> u) -> Instance -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Instance -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Instance -> m Instance gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Instance -> m Instance gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Instance -> m Instance
Ord Instance Source #
Instance details Defined in HasCASL.As Methods compare :: Instance -> Instance -> Ordering (<) :: Instance -> Instance -> Bool (<=) :: Instance -> Instance -> Bool (>) :: Instance -> Instance -> Bool (>=) :: Instance -> Instance -> Bool max :: Instance -> Instance -> Instance min :: Instance -> Instance -> Instance
Show Instance Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> Instance -> ShowS show :: Instance -> String showList :: [Instance] -> ShowS
Generic Instance
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Instance :: Type -> Type Methods from :: Instance -> Rep Instance x to :: Rep Instance x -> Instance
FromJSON Instance
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Instance parseJSONList :: Value -> Parser [Instance]
ToJSON Instance
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Instance -> Value toEncoding :: Instance -> Encoding toJSONList :: [Instance] -> Value toEncodingList :: [Instance] -> Encoding
ShATermConvertible Instance
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Instance -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Instance] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Instance) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Instance])
type Rep Instance
Instance details Defined in HasCASL.ATC_HasCASL type Rep Instance = D1 ('MetaData "Instance" "HasCASL.As" "main" 'False) (C1 ('MetaCons "Instance" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Plain" 'PrefixI 'False) (U1 :: Type -> Type))

data ClassItem Source #

a class item

Constructors

ClassItem ClassDecl [Annoted BasicItem] Range

Instances

Instances details

Data ClassItem Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassItem -> c ClassItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassItem toConstr :: ClassItem -> Constr dataTypeOf :: ClassItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ClassItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassItem) gmapT :: (forall b. Data b => b -> b) -> ClassItem -> ClassItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassItem -> r gmapQ :: (forall d. Data d => d -> u) -> ClassItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassItem -> m ClassItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassItem -> m ClassItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassItem -> m ClassItem
Show ClassItem Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> ClassItem -> ShowS show :: ClassItem -> String showList :: [ClassItem] -> ShowS
Generic ClassItem
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep ClassItem :: Type -> Type Methods from :: ClassItem -> Rep ClassItem x to :: Rep ClassItem x -> ClassItem
FromJSON ClassItem
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser ClassItem parseJSONList :: Value -> Parser [ClassItem]
ToJSON ClassItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: ClassItem -> Value toEncoding :: ClassItem -> Encoding toJSONList :: [ClassItem] -> Value toEncodingList :: [ClassItem] -> Encoding
ShATermConvertible ClassItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> ClassItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ClassItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ClassItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ClassItem])
Pretty ClassItem Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: ClassItem -> Doc Source # pretties :: [ClassItem] -> Doc Source #
type Rep ClassItem
Instance details Defined in HasCASL.ATC_HasCASL type Rep ClassItem = D1 ('MetaData "ClassItem" "HasCASL.As" "main" 'False) (C1 ('MetaCons "ClassItem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ClassDecl) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted BasicItem]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data ClassDecl Source #

declaring class identifiers

Constructors

ClassDecl [Id] Kind Range

Instances

Instances details

Data ClassDecl Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassDecl -> c ClassDecl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassDecl toConstr :: ClassDecl -> Constr dataTypeOf :: ClassDecl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ClassDecl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassDecl) gmapT :: (forall b. Data b => b -> b) -> ClassDecl -> ClassDecl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassDecl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassDecl -> r gmapQ :: (forall d. Data d => d -> u) -> ClassDecl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassDecl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassDecl -> m ClassDecl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassDecl -> m ClassDecl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassDecl -> m ClassDecl
Show ClassDecl Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> ClassDecl -> ShowS show :: ClassDecl -> String showList :: [ClassDecl] -> ShowS
Generic ClassDecl
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep ClassDecl :: Type -> Type Methods from :: ClassDecl -> Rep ClassDecl x to :: Rep ClassDecl x -> ClassDecl
FromJSON ClassDecl
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser ClassDecl parseJSONList :: Value -> Parser [ClassDecl]
ToJSON ClassDecl
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: ClassDecl -> Value toEncoding :: ClassDecl -> Encoding toJSONList :: [ClassDecl] -> Value toEncodingList :: [ClassDecl] -> Encoding
ShATermConvertible ClassDecl
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> ClassDecl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ClassDecl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ClassDecl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ClassDecl])
Pretty ClassDecl Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: ClassDecl -> Doc Source # pretties :: [ClassDecl] -> Doc Source #
type Rep ClassDecl
Instance details Defined in HasCASL.ATC_HasCASL type Rep ClassDecl = D1 ('MetaData "ClassDecl" "HasCASL.As" "main" 'False) (C1 ('MetaCons "ClassDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Id]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data Variance Source #

co- or contra- variance indicator

Constructors

InVar
CoVar
ContraVar
NonVar

Instances

Instances details

Eq Variance Source #
Instance details Defined in HasCASL.As Methods (==) :: Variance -> Variance -> Bool (/=) :: Variance -> Variance -> Bool
Data Variance Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Variance -> c Variance gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Variance toConstr :: Variance -> Constr dataTypeOf :: Variance -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Variance) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Variance) gmapT :: (forall b. Data b => b -> b) -> Variance -> Variance gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Variance -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Variance -> r gmapQ :: (forall d. Data d => d -> u) -> Variance -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Variance -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Variance -> m Variance gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Variance -> m Variance gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Variance -> m Variance
Ord Variance Source #
Instance details Defined in HasCASL.As Methods compare :: Variance -> Variance -> Ordering (<) :: Variance -> Variance -> Bool (<=) :: Variance -> Variance -> Bool (>) :: Variance -> Variance -> Bool (>=) :: Variance -> Variance -> Bool max :: Variance -> Variance -> Variance min :: Variance -> Variance -> Variance
Show Variance Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> Variance -> ShowS show :: Variance -> String showList :: [Variance] -> ShowS
Generic Variance
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Variance :: Type -> Type Methods from :: Variance -> Rep Variance x to :: Rep Variance x -> Variance
FromJSON Variance
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Variance parseJSONList :: Value -> Parser [Variance]
ToJSON Variance
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Variance -> Value toEncoding :: Variance -> Encoding toJSONList :: [Variance] -> Value toEncodingList :: [Variance] -> Encoding
ShATermConvertible Variance
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Variance -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Variance] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Variance) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Variance])
Pretty Variance Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: Variance -> Doc Source # pretties :: [Variance] -> Doc Source #
type Rep Variance
Instance details Defined in HasCASL.ATC_HasCASL type Rep Variance = D1 ('MetaData "Variance" "HasCASL.As" "main" 'False) ((C1 ('MetaCons "InVar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoVar" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ContraVar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonVar" 'PrefixI 'False) (U1 :: Type -> Type)))

data AnyKind a Source #

(higher) kinds

Constructors

ClassKind a
FunKind Variance (AnyKind a) (AnyKind a) Range

Instances

Instances details

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

type Kind = AnyKind Id Source #

type RawKind = AnyKind () Source #

data TypeItem Source #

the possible type items

Constructors

TypeDecl [TypePattern] Kind Range
SubtypeDecl [TypePattern] Type Range
IsoDecl [TypePattern] Range
SubtypeDefn TypePattern Vars Type (Annoted Term) Range
AliasType TypePattern (Maybe Kind) TypeScheme Range
Datatype DatatypeDecl

Instances

Instances details

Data TypeItem Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeItem -> c TypeItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeItem toConstr :: TypeItem -> Constr dataTypeOf :: TypeItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeItem) gmapT :: (forall b. Data b => b -> b) -> TypeItem -> TypeItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeItem -> r gmapQ :: (forall d. Data d => d -> u) -> TypeItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeItem -> m TypeItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeItem -> m TypeItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeItem -> m TypeItem
Show TypeItem Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> TypeItem -> ShowS show :: TypeItem -> String showList :: [TypeItem] -> ShowS
Generic TypeItem
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep TypeItem :: Type -> Type Methods from :: TypeItem -> Rep TypeItem x to :: Rep TypeItem x -> TypeItem
FromJSON TypeItem
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser TypeItem parseJSONList :: Value -> Parser [TypeItem]
ToJSON TypeItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: TypeItem -> Value toEncoding :: TypeItem -> Encoding toJSONList :: [TypeItem] -> Value toEncodingList :: [TypeItem] -> Encoding
ShATermConvertible TypeItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> TypeItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypeItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeItem])
Pretty TypeItem Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: TypeItem -> Doc Source # pretties :: [TypeItem] -> Doc Source #
type Rep TypeItem
Instance details Defined in HasCASL.ATC_HasCASL type Rep TypeItem = D1 ('MetaData "TypeItem" "HasCASL.As" "main" 'False) ((C1 ('MetaCons "TypeDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypePattern]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "SubtypeDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypePattern]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "IsoDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypePattern]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "SubtypeDefn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypePattern) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Vars)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Annoted Term)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "AliasType" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypePattern) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Kind))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Datatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DatatypeDecl)))))

data Vars Source #

a tuple pattern for SubtypeDefn

Constructors

Var Id
VarTuple [Vars] Range

Instances

Instances details

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

data TypePattern Source #

the lhs of most type items

Constructors

TypePattern Id [TypeArg] Range
TypePatternToken Token
MixfixTypePattern [TypePattern]
BracketTypePattern BracketKind [TypePattern] Range
TypePatternArg TypeArg Range

Instances

Instances details

Data TypePattern Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypePattern -> c TypePattern gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypePattern toConstr :: TypePattern -> Constr dataTypeOf :: TypePattern -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypePattern) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypePattern) gmapT :: (forall b. Data b => b -> b) -> TypePattern -> TypePattern gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypePattern -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypePattern -> r gmapQ :: (forall d. Data d => d -> u) -> TypePattern -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypePattern -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypePattern -> m TypePattern gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypePattern -> m TypePattern gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypePattern -> m TypePattern
Show TypePattern Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> TypePattern -> ShowS show :: TypePattern -> String showList :: [TypePattern] -> ShowS
Generic TypePattern
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep TypePattern :: Type -> Type Methods from :: TypePattern -> Rep TypePattern x to :: Rep TypePattern x -> TypePattern
GetRange TypePattern Source #
Instance details Defined in HasCASL.As Methods getRange :: TypePattern -> Range Source # rangeSpan :: TypePattern -> [Pos] Source #
FromJSON TypePattern
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser TypePattern parseJSONList :: Value -> Parser [TypePattern]
ToJSON TypePattern
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: TypePattern -> Value toEncoding :: TypePattern -> Encoding toJSONList :: [TypePattern] -> Value toEncodingList :: [TypePattern] -> Encoding
ShATermConvertible TypePattern
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> TypePattern -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypePattern] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypePattern) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypePattern])
Pretty TypePattern Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: TypePattern -> Doc Source # pretties :: [TypePattern] -> Doc Source #
type Rep TypePattern
Instance details Defined in HasCASL.ATC_HasCASL type Rep TypePattern = D1 ('MetaData "TypePattern" "HasCASL.As" "main" 'False) ((C1 ('MetaCons "TypePattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypeArg]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "TypePatternToken" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))) :+: (C1 ('MetaCons "MixfixTypePattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypePattern])) :+: (C1 ('MetaCons "BracketTypePattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BracketKind) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypePattern]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "TypePatternArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeArg) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data Type Source #

types based on variable or constructor names and applications

Constructors

TypeName Id RawKind Int
TypeAppl Type Type
ExpandedType Type Type
TypeAbs TypeArg Type Range
KindedType Type (Set Kind) Range
TypeToken Token
BracketType BracketKind [Type] Range
MixfixType [Type]

Instances

Instances details

Eq Type Source #
Instance details Defined in HasCASL.As Methods (==) :: Type -> Type -> Bool (/=) :: Type -> Type -> Bool
Data Type Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type toConstr :: Type -> Constr dataTypeOf :: Type -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) gmapT :: (forall b. Data b => b -> b) -> Type -> Type gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type
Ord Type Source #
Instance details Defined in HasCASL.As Methods compare :: Type -> Type -> Ordering (<) :: Type -> Type -> Bool (<=) :: Type -> Type -> Bool (>) :: Type -> Type -> Bool (>=) :: Type -> Type -> Bool max :: Type -> Type -> Type min :: Type -> Type -> Type
Show Type Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> Type -> ShowS show :: Type -> String showList :: [Type] -> ShowS
Generic Type
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Type :: Type -> Type Methods from :: Type -> Rep Type x to :: Rep Type x -> Type
GetRange Type Source #
Instance details Defined in HasCASL.As Methods getRange :: Type -> Range Source # rangeSpan :: Type -> [Pos] Source #
FromJSON Type
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Type parseJSONList :: Value -> Parser [Type]
ToJSON Type
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Type -> Value toEncoding :: Type -> Encoding toJSONList :: [Type] -> Value toEncodingList :: [Type] -> Encoding
ShATermConvertible Type
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Type -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Type] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Type) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Type])
Pretty Type Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: Type -> Doc Source # pretties :: [Type] -> Doc Source #
type Rep Type
Instance details Defined in HasCASL.ATC_HasCASL type Rep Type = D1 ('MetaData "Type" "HasCASL.As" "main" 'False) (((C1 ('MetaCons "TypeName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: C1 ('MetaCons "TypeAppl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "ExpandedType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "TypeAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeArg) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "KindedType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Kind)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "TypeToken" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))) :+: (C1 ('MetaCons "BracketType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BracketKind) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "MixfixType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type])))))

mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme Source #

change the type within a scheme

data TypeScheme Source #

a type with bound type variables. The bound variables within the scheme should have negative numbers in the order given by the type argument list. The type arguments store proper kinds (including downsets) whereas the kind within the type names are only raw kinds.

Constructors

TypeScheme [TypeArg] Type Range

Instances

Instances details

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

data Partiality Source #

indicator for partial or total functions

Constructors

Partial
Total

Instances

Instances details

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

data OpItem Source #

function declarations or definitions

Constructors

OpDecl [PolyId] TypeScheme [OpAttr] Range
OpDefn PolyId [[VarDecl]] TypeScheme Term Range

Instances

Instances details

Data OpItem Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpItem -> c OpItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpItem toConstr :: OpItem -> Constr dataTypeOf :: OpItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpItem) gmapT :: (forall b. Data b => b -> b) -> OpItem -> OpItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpItem -> r gmapQ :: (forall d. Data d => d -> u) -> OpItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpItem -> m OpItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpItem -> m OpItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpItem -> m OpItem
Show OpItem Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> OpItem -> ShowS show :: OpItem -> String showList :: [OpItem] -> ShowS
Generic OpItem
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep OpItem :: Type -> Type Methods from :: OpItem -> Rep OpItem x to :: Rep OpItem x -> OpItem
FromJSON OpItem
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser OpItem parseJSONList :: Value -> Parser [OpItem]
ToJSON OpItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: OpItem -> Value toEncoding :: OpItem -> Encoding toJSONList :: [OpItem] -> Value toEncodingList :: [OpItem] -> Encoding
ShATermConvertible OpItem
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> OpItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OpItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OpItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpItem])
type Rep OpItem
Instance details Defined in HasCASL.ATC_HasCASL type Rep OpItem = D1 ('MetaData "OpItem" "HasCASL.As" "main" 'False) (C1 ('MetaCons "OpDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PolyId]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OpAttr]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "OpDefn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PolyId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[VarDecl]])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data BinOpAttr Source #

attributes without arguments for binary functions

Constructors

Assoc
Comm
Idem

Instances

Instances details

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

data OpAttr Source #

possible function attributes (including a term as a unit element)

Constructors

BinOpAttr BinOpAttr Range
UnitOpAttr Term Range

Instances

Instances details

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

data DatatypeDecl Source #

a polymorphic data type declaration with a deriving clause

Constructors

DatatypeDecl TypePattern Kind [Annoted Alternative] [Id] Range

Instances

Instances details

Data DatatypeDecl Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DatatypeDecl -> c DatatypeDecl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DatatypeDecl toConstr :: DatatypeDecl -> Constr dataTypeOf :: DatatypeDecl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DatatypeDecl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DatatypeDecl) gmapT :: (forall b. Data b => b -> b) -> DatatypeDecl -> DatatypeDecl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeDecl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeDecl -> r gmapQ :: (forall d. Data d => d -> u) -> DatatypeDecl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DatatypeDecl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DatatypeDecl -> m DatatypeDecl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeDecl -> m DatatypeDecl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeDecl -> m DatatypeDecl
Show DatatypeDecl Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> DatatypeDecl -> ShowS show :: DatatypeDecl -> String showList :: [DatatypeDecl] -> ShowS
Generic DatatypeDecl
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep DatatypeDecl :: Type -> Type Methods from :: DatatypeDecl -> Rep DatatypeDecl x to :: Rep DatatypeDecl x -> DatatypeDecl
FromJSON DatatypeDecl
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser DatatypeDecl parseJSONList :: Value -> Parser [DatatypeDecl]
ToJSON DatatypeDecl
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: DatatypeDecl -> Value toEncoding :: DatatypeDecl -> Encoding toJSONList :: [DatatypeDecl] -> Value toEncodingList :: [DatatypeDecl] -> Encoding
ShATermConvertible DatatypeDecl
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> DatatypeDecl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DatatypeDecl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DatatypeDecl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DatatypeDecl])
Pretty DatatypeDecl Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: DatatypeDecl -> Doc Source # pretties :: [DatatypeDecl] -> Doc Source #
type Rep DatatypeDecl
Instance details Defined in HasCASL.ATC_HasCASL type Rep DatatypeDecl = D1 ('MetaData "DatatypeDecl" "HasCASL.As" "main" 'False) (C1 ('MetaCons "DatatypeDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypePattern) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted Alternative]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Id]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data Alternative Source #

Alternatives are subtypes or a constructor with a list of (curried) tuples as arguments. Only the components of the first tuple can be addressed by the places of the mixfix constructor.

Constructors

Constructor Id [[Component]] Partiality Range
Subtype [Type] Range

Instances

Instances details

Data Alternative Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Alternative -> c Alternative gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Alternative toConstr :: Alternative -> Constr dataTypeOf :: Alternative -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Alternative) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Alternative) gmapT :: (forall b. Data b => b -> b) -> Alternative -> Alternative gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Alternative -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Alternative -> r gmapQ :: (forall d. Data d => d -> u) -> Alternative -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Alternative -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Alternative -> m Alternative gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Alternative -> m Alternative gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Alternative -> m Alternative
Show Alternative Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> Alternative -> ShowS show :: Alternative -> String showList :: [Alternative] -> ShowS
Generic Alternative
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Alternative :: Type -> Type Methods from :: Alternative -> Rep Alternative x to :: Rep Alternative x -> Alternative
FromJSON Alternative
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Alternative parseJSONList :: Value -> Parser [Alternative]
ToJSON Alternative
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Alternative -> Value toEncoding :: Alternative -> Encoding toJSONList :: [Alternative] -> Value toEncodingList :: [Alternative] -> Encoding
ShATermConvertible Alternative
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Alternative -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Alternative] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Alternative) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Alternative])
Pretty Alternative Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: Alternative -> Doc Source # pretties :: [Alternative] -> Doc Source #
type Rep Alternative
Instance details Defined in HasCASL.ATC_HasCASL type Rep Alternative = D1 ('MetaData "Alternative" "HasCASL.As" "main" 'False) (C1 ('MetaCons "Constructor" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Component]])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Partiality) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Subtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data Component Source #

A component is a type with on optional (only pre- or postfix) selector function.

Constructors

Selector Id Partiality Type SeparatorKind Range
NoSelector Type

Instances

Instances details

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

data Quantifier Source #

the possible quantifiers

Constructors

Universal
Existential
Unique

Instances

Instances details

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

data TypeQual Source #

the possibly type annotations of terms

Constructors

OfType
AsType
InType
Inferred

Instances

Instances details

Eq TypeQual Source #
Instance details Defined in HasCASL.As Methods (==) :: TypeQual -> TypeQual -> Bool (/=) :: TypeQual -> TypeQual -> Bool
Data TypeQual Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeQual -> c TypeQual gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeQual toConstr :: TypeQual -> Constr dataTypeOf :: TypeQual -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeQual) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeQual) gmapT :: (forall b. Data b => b -> b) -> TypeQual -> TypeQual gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeQual -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeQual -> r gmapQ :: (forall d. Data d => d -> u) -> TypeQual -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeQual -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeQual -> m TypeQual gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeQual -> m TypeQual gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeQual -> m TypeQual
Ord TypeQual Source #
Instance details Defined in HasCASL.As Methods compare :: TypeQual -> TypeQual -> Ordering (<) :: TypeQual -> TypeQual -> Bool (<=) :: TypeQual -> TypeQual -> Bool (>) :: TypeQual -> TypeQual -> Bool (>=) :: TypeQual -> TypeQual -> Bool max :: TypeQual -> TypeQual -> TypeQual min :: TypeQual -> TypeQual -> TypeQual
Show TypeQual Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> TypeQual -> ShowS show :: TypeQual -> String showList :: [TypeQual] -> ShowS
Generic TypeQual
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep TypeQual :: Type -> Type Methods from :: TypeQual -> Rep TypeQual x to :: Rep TypeQual x -> TypeQual
FromJSON TypeQual
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser TypeQual parseJSONList :: Value -> Parser [TypeQual]
ToJSON TypeQual
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: TypeQual -> Value toEncoding :: TypeQual -> Encoding toJSONList :: [TypeQual] -> Value toEncodingList :: [TypeQual] -> Encoding
ShATermConvertible TypeQual
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> TypeQual -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypeQual] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeQual) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeQual])
Pretty TypeQual Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: TypeQual -> Doc Source # pretties :: [TypeQual] -> Doc Source #
type Rep TypeQual
Instance details Defined in HasCASL.ATC_HasCASL type Rep TypeQual = D1 ('MetaData "TypeQual" "HasCASL.As" "main" 'False) ((C1 ('MetaCons "OfType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsType" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "InType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Inferred" 'PrefixI 'False) (U1 :: Type -> Type)))

data LetBrand Source #

an indicator of (otherwise equivalent) let or where equations

Constructors

Let
Where
Program

Instances

Instances details

Eq LetBrand Source #
Instance details Defined in HasCASL.As Methods (==) :: LetBrand -> LetBrand -> Bool (/=) :: LetBrand -> LetBrand -> Bool
Data LetBrand Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetBrand -> c LetBrand gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBrand toConstr :: LetBrand -> Constr dataTypeOf :: LetBrand -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetBrand) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetBrand) gmapT :: (forall b. Data b => b -> b) -> LetBrand -> LetBrand gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBrand -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBrand -> r gmapQ :: (forall d. Data d => d -> u) -> LetBrand -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBrand -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBrand -> m LetBrand gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBrand -> m LetBrand gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBrand -> m LetBrand
Ord LetBrand Source #
Instance details Defined in HasCASL.As Methods compare :: LetBrand -> LetBrand -> Ordering (<) :: LetBrand -> LetBrand -> Bool (<=) :: LetBrand -> LetBrand -> Bool (>) :: LetBrand -> LetBrand -> Bool (>=) :: LetBrand -> LetBrand -> Bool max :: LetBrand -> LetBrand -> LetBrand min :: LetBrand -> LetBrand -> LetBrand
Show LetBrand Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> LetBrand -> ShowS show :: LetBrand -> String showList :: [LetBrand] -> ShowS
Generic LetBrand
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep LetBrand :: Type -> Type Methods from :: LetBrand -> Rep LetBrand x to :: Rep LetBrand x -> LetBrand
FromJSON LetBrand
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser LetBrand parseJSONList :: Value -> Parser [LetBrand]
ToJSON LetBrand
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: LetBrand -> Value toEncoding :: LetBrand -> Encoding toJSONList :: [LetBrand] -> Value toEncodingList :: [LetBrand] -> Encoding
ShATermConvertible LetBrand
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> LetBrand -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [LetBrand] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, LetBrand) fromShATermList' :: Int -> ATermTable -> (ATermTable, [LetBrand])
type Rep LetBrand
Instance details Defined in HasCASL.ATC_HasCASL type Rep LetBrand = D1 ('MetaData "LetBrand" "HasCASL.As" "main" 'False) (C1 ('MetaCons "Let" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Where" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Program" 'PrefixI 'False) (U1 :: Type -> Type)))

data BracketKind Source #

the possible kinds of brackets (that should match when parsed)

Constructors

Parens
Squares
Braces
NoBrackets

Instances

Instances details

Eq BracketKind Source #
Instance details Defined in HasCASL.As Methods (==) :: BracketKind -> BracketKind -> Bool (/=) :: BracketKind -> BracketKind -> Bool
Data BracketKind Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BracketKind -> c BracketKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BracketKind toConstr :: BracketKind -> Constr dataTypeOf :: BracketKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BracketKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BracketKind) gmapT :: (forall b. Data b => b -> b) -> BracketKind -> BracketKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BracketKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BracketKind -> r gmapQ :: (forall d. Data d => d -> u) -> BracketKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BracketKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BracketKind -> m BracketKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BracketKind -> m BracketKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BracketKind -> m BracketKind
Ord BracketKind Source #
Instance details Defined in HasCASL.As Methods compare :: BracketKind -> BracketKind -> Ordering (<) :: BracketKind -> BracketKind -> Bool (<=) :: BracketKind -> BracketKind -> Bool (>) :: BracketKind -> BracketKind -> Bool (>=) :: BracketKind -> BracketKind -> Bool max :: BracketKind -> BracketKind -> BracketKind min :: BracketKind -> BracketKind -> BracketKind
Show BracketKind Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> BracketKind -> ShowS show :: BracketKind -> String showList :: [BracketKind] -> ShowS
Generic BracketKind
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep BracketKind :: Type -> Type Methods from :: BracketKind -> Rep BracketKind x to :: Rep BracketKind x -> BracketKind
FromJSON BracketKind
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser BracketKind parseJSONList :: Value -> Parser [BracketKind]
ToJSON BracketKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: BracketKind -> Value toEncoding :: BracketKind -> Encoding toJSONList :: [BracketKind] -> Value toEncodingList :: [BracketKind] -> Encoding
ShATermConvertible BracketKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> BracketKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BracketKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BracketKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BracketKind])
type Rep BracketKind
Instance details Defined in HasCASL.ATC_HasCASL type Rep BracketKind = D1 ('MetaData "BracketKind" "HasCASL.As" "main" 'False) ((C1 ('MetaCons "Parens" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Squares" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Braces" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoBrackets" 'PrefixI 'False) (U1 :: Type -> Type)))

getBrackets :: BracketKind -> (String, String) Source #

the brackets as strings for printing

data InstKind Source #

Constructors

UserGiven
Infer

Instances

Instances details

Eq InstKind Source #
Instance details Defined in HasCASL.As Methods (==) :: InstKind -> InstKind -> Bool (/=) :: InstKind -> InstKind -> Bool
Data InstKind Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InstKind -> c InstKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InstKind toConstr :: InstKind -> Constr dataTypeOf :: InstKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InstKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InstKind) gmapT :: (forall b. Data b => b -> b) -> InstKind -> InstKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InstKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InstKind -> r gmapQ :: (forall d. Data d => d -> u) -> InstKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> InstKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> InstKind -> m InstKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InstKind -> m InstKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InstKind -> m InstKind
Ord InstKind Source #
Instance details Defined in HasCASL.As Methods compare :: InstKind -> InstKind -> Ordering (<) :: InstKind -> InstKind -> Bool (<=) :: InstKind -> InstKind -> Bool (>) :: InstKind -> InstKind -> Bool (>=) :: InstKind -> InstKind -> Bool max :: InstKind -> InstKind -> InstKind min :: InstKind -> InstKind -> InstKind
Show InstKind Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> InstKind -> ShowS show :: InstKind -> String showList :: [InstKind] -> ShowS
Generic InstKind
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep InstKind :: Type -> Type Methods from :: InstKind -> Rep InstKind x to :: Rep InstKind x -> InstKind
FromJSON InstKind
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser InstKind parseJSONList :: Value -> Parser [InstKind]
ToJSON InstKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: InstKind -> Value toEncoding :: InstKind -> Encoding toJSONList :: [InstKind] -> Value toEncodingList :: [InstKind] -> Encoding
ShATermConvertible InstKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> InstKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [InstKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, InstKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [InstKind])
type Rep InstKind
Instance details Defined in HasCASL.ATC_HasCASL type Rep InstKind = D1 ('MetaData "InstKind" "HasCASL.As" "main" 'False) (C1 ('MetaCons "UserGiven" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Infer" 'PrefixI 'False) (U1 :: Type -> Type))

data Term Source #

The possible terms and patterns. Formulas are also kept as terms. Local variables and constants are kept separatetly. The variant ResolvedMixTerm is an intermediate representation for type checking only.

Instances

Instances details

Eq Term Source #
Instance details Defined in HasCASL.As Methods (==) :: Term -> Term -> Bool (/=) :: Term -> Term -> Bool
Data Term Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term toConstr :: Term -> Constr dataTypeOf :: Term -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) gmapT :: (forall b. Data b => b -> b) -> Term -> Term gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term
Ord Term Source #
Instance details Defined in HasCASL.As Methods compare :: Term -> Term -> Ordering (<) :: Term -> Term -> Bool (<=) :: Term -> Term -> Bool (>) :: Term -> Term -> Bool (>=) :: Term -> Term -> Bool max :: Term -> Term -> Term min :: Term -> Term -> Term
Show Term Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> Term -> ShowS show :: Term -> String showList :: [Term] -> ShowS
Generic Term
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Term :: Type -> Type Methods from :: Term -> Rep Term x to :: Rep Term x -> Term
GetRange Term Source #
Instance details Defined in HasCASL.As Methods getRange :: Term -> Range Source # rangeSpan :: Term -> [Pos] Source #
FromJSON Term
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Term parseJSONList :: Value -> Parser [Term]
ToJSON Term
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Term -> Value toEncoding :: Term -> Encoding toJSONList :: [Term] -> Value toEncodingList :: [Term] -> Encoding
ShATermConvertible Term
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Term] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Term) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Term])
Pretty Term Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: Term -> Doc Source # pretties :: [Term] -> Doc Source #
type Rep Term
Instance details Defined in HasCASL.ATC_HasCASL type Rep Term = D1 ('MetaData "Term" "HasCASL.As" "main" 'False) (((C1 ('MetaCons "QualVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarDecl)) :+: (C1 ('MetaCons "QualOp" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpBrand) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PolyId) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InstKind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: C1 ('MetaCons "ApplTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "TupleTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "TypedTerm" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeQual)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "AsPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarDecl) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "QuantifiedTerm" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantifier) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GenVarDecl])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))) :+: (((C1 ('MetaCons "LambdaTerm" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Partiality)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "CaseTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProgEq]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "LetTerm" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetBrand) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProgEq])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "ResolvedMixTerm" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "TermToken" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "MixTypeTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeQual) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "MixfixTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term])) :+: C1 ('MetaCons "BracketTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BracketKind) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))))

data ProgEq Source #

an equation or a case as pair of a pattern and a term

Constructors

ProgEq Term Term Range

Instances

Instances details

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

data PolyId Source #

an identifier with an optional list of type declarations

Constructors

PolyId Id [TypeArg] Range

Instances

Instances details

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

data SeparatorKind Source #

an indicator if variables were separated by commas or by separate declarations

Constructors

Comma
Other

Instances

Instances details

Eq SeparatorKind Source #
Instance details Defined in HasCASL.As Methods (==) :: SeparatorKind -> SeparatorKind -> Bool (/=) :: SeparatorKind -> SeparatorKind -> Bool
Data SeparatorKind Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SeparatorKind -> c SeparatorKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SeparatorKind toConstr :: SeparatorKind -> Constr dataTypeOf :: SeparatorKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SeparatorKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SeparatorKind) gmapT :: (forall b. Data b => b -> b) -> SeparatorKind -> SeparatorKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SeparatorKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SeparatorKind -> r gmapQ :: (forall d. Data d => d -> u) -> SeparatorKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SeparatorKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SeparatorKind -> m SeparatorKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SeparatorKind -> m SeparatorKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SeparatorKind -> m SeparatorKind
Ord SeparatorKind Source #
Instance details Defined in HasCASL.As Methods compare :: SeparatorKind -> SeparatorKind -> Ordering (<) :: SeparatorKind -> SeparatorKind -> Bool (<=) :: SeparatorKind -> SeparatorKind -> Bool (>) :: SeparatorKind -> SeparatorKind -> Bool (>=) :: SeparatorKind -> SeparatorKind -> Bool max :: SeparatorKind -> SeparatorKind -> SeparatorKind min :: SeparatorKind -> SeparatorKind -> SeparatorKind
Show SeparatorKind Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> SeparatorKind -> ShowS show :: SeparatorKind -> String showList :: [SeparatorKind] -> ShowS
Generic SeparatorKind
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep SeparatorKind :: Type -> Type Methods from :: SeparatorKind -> Rep SeparatorKind x to :: Rep SeparatorKind x -> SeparatorKind
FromJSON SeparatorKind
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser SeparatorKind parseJSONList :: Value -> Parser [SeparatorKind]
ToJSON SeparatorKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: SeparatorKind -> Value toEncoding :: SeparatorKind -> Encoding toJSONList :: [SeparatorKind] -> Value toEncodingList :: [SeparatorKind] -> Encoding
ShATermConvertible SeparatorKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> SeparatorKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SeparatorKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SeparatorKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SeparatorKind])
type Rep SeparatorKind
Instance details Defined in HasCASL.ATC_HasCASL type Rep SeparatorKind = D1 ('MetaData "SeparatorKind" "HasCASL.As" "main" 'False) (C1 ('MetaCons "Comma" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Other" 'PrefixI 'False) (U1 :: Type -> Type))

data VarDecl Source #

a variable with its type

Constructors

VarDecl Id Type SeparatorKind Range

Instances

Instances details

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

data VarKind Source #

the kind of a type variable (or a type argument in schemes)

Constructors

VarKind Kind
Downset Type
MissingKind

Instances

Instances details

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

data TypeArg Source #

a (simple) type variable with its kind (or supertype)

Constructors

TypeArg Id Variance VarKind RawKind Int SeparatorKind Range

Instances

Instances details

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

data GenVarDecl Source #

a value or type variable

Constructors

GenVarDecl VarDecl
GenTypeVarDecl TypeArg

Instances

Instances details

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

symbol data types symbols

data SymbItems Source #

Constructors

SymbItems SymbKind [Symb] [Annotation] Range

Instances

Instances details

Eq SymbItems Source #
Instance details Defined in HasCASL.As Methods (==) :: SymbItems -> SymbItems -> Bool (/=) :: SymbItems -> SymbItems -> Bool
Data SymbItems Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbItems -> c SymbItems gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbItems toConstr :: SymbItems -> Constr dataTypeOf :: SymbItems -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbItems) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbItems) gmapT :: (forall b. Data b => b -> b) -> SymbItems -> SymbItems gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbItems -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbItems -> r gmapQ :: (forall d. Data d => d -> u) -> SymbItems -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbItems -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbItems -> m SymbItems gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbItems -> m SymbItems gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbItems -> m SymbItems
Ord SymbItems Source #
Instance details Defined in HasCASL.As Methods compare :: SymbItems -> SymbItems -> Ordering (<) :: SymbItems -> SymbItems -> Bool (<=) :: SymbItems -> SymbItems -> Bool (>) :: SymbItems -> SymbItems -> Bool (>=) :: SymbItems -> SymbItems -> Bool max :: SymbItems -> SymbItems -> SymbItems min :: SymbItems -> SymbItems -> SymbItems
Show SymbItems Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> SymbItems -> ShowS show :: SymbItems -> String showList :: [SymbItems] -> ShowS
Generic SymbItems
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep SymbItems :: Type -> Type Methods from :: SymbItems -> Rep SymbItems x to :: Rep SymbItems x -> SymbItems
FromJSON SymbItems
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser SymbItems parseJSONList :: Value -> Parser [SymbItems]
ToJSON SymbItems
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: SymbItems -> Value toEncoding :: SymbItems -> Encoding toJSONList :: [SymbItems] -> Value toEncodingList :: [SymbItems] -> Encoding
ShATermConvertible SymbItems
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> SymbItems -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SymbItems] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbItems) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbItems])
Pretty SymbItems Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: SymbItems -> Doc Source # pretties :: [SymbItems] -> Doc Source #
ProjectSublogicM Sublogic SymbItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogicM :: Sublogic -> SymbItems -> Maybe SymbItems Source #
MinSublogic Sublogic SymbItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: SymbItems -> Sublogic Source #
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parsersAndPrinters :: HasCASL -> Map String (PrefixMap -> AParser st BasicSpec, BasicSpec -> Doc) Source # parse_basic_spec :: HasCASL -> Maybe (PrefixMap -> AParser st BasicSpec) Source # parseSingleSymbItem :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_map_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbMapItems) Source # toItem :: HasCASL -> BasicSpec -> Item Source # symb_items_name :: HasCASL -> SymbItems -> [String] Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep SymbItems
Instance details Defined in HasCASL.ATC_HasCASL type Rep SymbItems = D1 ('MetaData "SymbItems" "HasCASL.As" "main" 'False) (C1 ('MetaCons "SymbItems" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymbKind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symb])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annotation]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data SymbMapItems Source #

mapped symbols

Constructors

SymbMapItems SymbKind [SymbOrMap] [Annotation] Range

Instances

Instances details

Eq SymbMapItems Source #
Instance details Defined in HasCASL.As Methods (==) :: SymbMapItems -> SymbMapItems -> Bool (/=) :: SymbMapItems -> SymbMapItems -> Bool
Data SymbMapItems Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbMapItems -> c SymbMapItems gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbMapItems toConstr :: SymbMapItems -> Constr dataTypeOf :: SymbMapItems -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbMapItems) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbMapItems) gmapT :: (forall b. Data b => b -> b) -> SymbMapItems -> SymbMapItems gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbMapItems -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbMapItems -> r gmapQ :: (forall d. Data d => d -> u) -> SymbMapItems -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbMapItems -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbMapItems -> m SymbMapItems gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbMapItems -> m SymbMapItems gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbMapItems -> m SymbMapItems
Ord SymbMapItems Source #
Instance details Defined in HasCASL.As Methods compare :: SymbMapItems -> SymbMapItems -> Ordering (<) :: SymbMapItems -> SymbMapItems -> Bool (<=) :: SymbMapItems -> SymbMapItems -> Bool (>) :: SymbMapItems -> SymbMapItems -> Bool (>=) :: SymbMapItems -> SymbMapItems -> Bool max :: SymbMapItems -> SymbMapItems -> SymbMapItems min :: SymbMapItems -> SymbMapItems -> SymbMapItems
Show SymbMapItems Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> SymbMapItems -> ShowS show :: SymbMapItems -> String showList :: [SymbMapItems] -> ShowS
Generic SymbMapItems
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep SymbMapItems :: Type -> Type Methods from :: SymbMapItems -> Rep SymbMapItems x to :: Rep SymbMapItems x -> SymbMapItems
FromJSON SymbMapItems
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser SymbMapItems parseJSONList :: Value -> Parser [SymbMapItems]
ToJSON SymbMapItems
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: SymbMapItems -> Value toEncoding :: SymbMapItems -> Encoding toJSONList :: [SymbMapItems] -> Value toEncodingList :: [SymbMapItems] -> Encoding
ShATermConvertible SymbMapItems
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> SymbMapItems -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SymbMapItems] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbMapItems) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbMapItems])
Pretty SymbMapItems Source #
Instance details Defined in HasCASL.PrintAs Methods pretty :: SymbMapItems -> Doc Source # pretties :: [SymbMapItems] -> Doc Source #
ProjectSublogicM Sublogic SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogicM :: Sublogic -> SymbMapItems -> Maybe SymbMapItems Source #
MinSublogic Sublogic SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: SymbMapItems -> Sublogic Source #
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parsersAndPrinters :: HasCASL -> Map String (PrefixMap -> AParser st BasicSpec, BasicSpec -> Doc) Source # parse_basic_spec :: HasCASL -> Maybe (PrefixMap -> AParser st BasicSpec) Source # parseSingleSymbItem :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_map_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbMapItems) Source # toItem :: HasCASL -> BasicSpec -> Item Source # symb_items_name :: HasCASL -> SymbItems -> [String] Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep SymbMapItems
Instance details Defined in HasCASL.ATC_HasCASL type Rep SymbMapItems = D1 ('MetaData "SymbMapItems" "HasCASL.As" "main" 'False) (C1 ('MetaCons "SymbMapItems" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymbKind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SymbOrMap])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annotation]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data SymbKind Source #

kind of symbols

Constructors

Implicit
SyKtype
SyKsort
SyKfun
SyKop
SyKpred
SyKclass

Instances

Instances details

Eq SymbKind Source #
Instance details Defined in HasCASL.As Methods (==) :: SymbKind -> SymbKind -> Bool (/=) :: SymbKind -> SymbKind -> Bool
Data SymbKind Source #
Instance details Defined in HasCASL.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbKind -> c SymbKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbKind toConstr :: SymbKind -> Constr dataTypeOf :: SymbKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbKind) gmapT :: (forall b. Data b => b -> b) -> SymbKind -> SymbKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbKind -> r gmapQ :: (forall d. Data d => d -> u) -> SymbKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbKind -> m SymbKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbKind -> m SymbKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbKind -> m SymbKind
Ord SymbKind Source #
Instance details Defined in HasCASL.As Methods compare :: SymbKind -> SymbKind -> Ordering (<) :: SymbKind -> SymbKind -> Bool (<=) :: SymbKind -> SymbKind -> Bool (>) :: SymbKind -> SymbKind -> Bool (>=) :: SymbKind -> SymbKind -> Bool max :: SymbKind -> SymbKind -> SymbKind min :: SymbKind -> SymbKind -> SymbKind
Show SymbKind Source #
Instance details Defined in HasCASL.As Methods showsPrec :: Int -> SymbKind -> ShowS show :: SymbKind -> String showList :: [SymbKind] -> ShowS
Generic SymbKind
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep SymbKind :: Type -> Type Methods from :: SymbKind -> Rep SymbKind x to :: Rep SymbKind x -> SymbKind
FromJSON SymbKind
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser SymbKind parseJSONList :: Value -> Parser [SymbKind]
ToJSON SymbKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: SymbKind -> Value toEncoding :: SymbKind -> Encoding toJSONList :: [SymbKind] -> Value toEncodingList :: [SymbKind] -> Encoding
ShATermConvertible SymbKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> SymbKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SymbKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbKind])
Pretty SymbKind Source #
Instance details Defined in HasCASL.As Methods pretty :: SymbKind -> Doc Source # pretties :: [SymbKind] -> Doc Source #
type Rep SymbKind
Instance details Defined in HasCASL.ATC_HasCASL type Rep SymbKind = D1 ('MetaData "SymbKind" "HasCASL.As" "main" 'False) ((C1 ('MetaCons "Implicit" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SyKtype" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SyKsort" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SyKfun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SyKop" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SyKpred" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SyKclass" 'PrefixI 'False) (U1 :: Type -> Type))))

data Symb Source #

type annotated symbols

Constructors

Symb Id (Maybe SymbType) Range

Instances

Instances details

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

data SymbType Source #

type for symbols

Constructors

SymbType TypeScheme

Instances

Instances details

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

data SymbOrMap Source #

mapped symbol

Constructors

SymbOrMap Symb (Maybe Symb) Range

Instances

Instances details

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

equality instances ignoring positions

compute better position

bestRange :: GetRange a => [a] -> Range -> Range Source #

get a reasonable position for a list with an additional position list

SigItems SigItems
ProgItems [Annoted ProgEq] Range
ClassItems Instance [Annoted ClassItem] Range
GenVarItems [GenVarDecl] Range
FreeDatatype [Annoted DatatypeDecl] Range
GenItems [Annoted SigItems] Range
AxiomItems [GenVarDecl] [Annoted Term] Range
Internal [Annoted BasicItem] Range

QualVar VarDecl
QualOp OpBrand PolyId TypeScheme [Type] InstKind Range
ApplTerm Term Term Range
TupleTerm [Term] Range
TypedTerm Term TypeQual Type Range
AsPattern VarDecl Term Range
QuantifiedTerm Quantifier [GenVarDecl] Term Range
LambdaTerm [Term] Partiality Term Range
CaseTerm Term [ProgEq] Range
LetTerm LetBrand [ProgEq] Term Range
ResolvedMixTerm Id [Type] [Term] Range
TermToken Token
MixTypeTerm TypeQual Type Range
MixfixTerm [Term]
BracketTerm BracketKind [Term] Range