Hets - the Heterogeneous Tool Set
Copyright(c) Dominik Dietrich Ewaryst Schulz DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEwaryst.Schulz@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

CSL.AS_BASIC_CSL

Description

This module contains the abstract syntax types for EnCL as well as the predefined operator configuration.

Synopsis

Documentation

data EXPRESSION Source #

Datatype for expressions

Instances

Instances details
Eq EXPRESSION Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: EXPRESSION -> EXPRESSION -> Bool

(/=) :: EXPRESSION -> EXPRESSION -> Bool

Data EXPRESSION Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EXPRESSION -> c EXPRESSION

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EXPRESSION

toConstr :: EXPRESSION -> Constr

dataTypeOf :: EXPRESSION -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EXPRESSION)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXPRESSION)

gmapT :: (forall b. Data b => b -> b) -> EXPRESSION -> EXPRESSION

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXPRESSION -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXPRESSION -> r

gmapQ :: (forall d. Data d => d -> u) -> EXPRESSION -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EXPRESSION -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EXPRESSION -> m EXPRESSION

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EXPRESSION -> m EXPRESSION

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EXPRESSION -> m EXPRESSION

Ord EXPRESSION Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Show EXPRESSION Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> EXPRESSION -> ShowS

show :: EXPRESSION -> String

showList :: [EXPRESSION] -> ShowS

Generic EXPRESSION 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep EXPRESSION :: Type -> Type

Methods

from :: EXPRESSION -> Rep EXPRESSION x

to :: Rep EXPRESSION x -> EXPRESSION

GetRange EXPRESSION Source # 
Instance details

Defined in CSL.Print_AS

FromJSON EXPRESSION 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser EXPRESSION

parseJSONList :: Value -> Parser [EXPRESSION]

ToJSON EXPRESSION 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: EXPRESSION -> Value

toEncoding :: EXPRESSION -> Encoding

toJSONList :: [EXPRESSION] -> Value

toEncodingList :: [EXPRESSION] -> Encoding

ShATermConvertible EXPRESSION 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> EXPRESSION -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [EXPRESSION] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, EXPRESSION)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [EXPRESSION])

Pretty EXPRESSION Source # 
Instance details

Defined in CSL.Print_AS

Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #

Instance of Logic for reduce logc

Instance details

Defined in CSL.Logic_CSL

Methods

parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source #

stability :: CSL -> Stability Source #

data_logic :: CSL -> Maybe AnyLogic Source #

top_sublogic :: CSL -> () Source #

all_sublogics :: CSL -> [()] Source #

bottomSublogic :: CSL -> Maybe () Source #

sublogicDimensions :: CSL -> [[()]] Source #

parseSublogic :: CSL -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source #

provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source #

default_prover :: CSL -> String Source #

cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source #

conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source #

empty_proof_tree :: CSL -> [EXPRESSION] Source #

syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSL -> Maybe OMCD Source #

export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source #

omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source #

addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source #

addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source #

sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

type Rep EXPRESSION 
Instance details

Defined in CSL.ATC_CSL

type Rep EXPRESSION = D1 ('MetaData "EXPRESSION" "CSL.AS_BASIC_CSL" "main" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: (C1 ('MetaCons "Op" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OPID) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EXTPARAM])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EXPRESSION]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "List" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EXPRESSION]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Interval" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Double) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Double) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Int" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 APInt) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Rat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 APFloat) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data EXTPARAM Source #

Extended Parameter Datatype

Constructors

EP Token String APInt 

Instances

Instances details
Eq EXTPARAM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: EXTPARAM -> EXTPARAM -> Bool

(/=) :: EXTPARAM -> EXTPARAM -> Bool

Data EXTPARAM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EXTPARAM -> c EXTPARAM

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EXTPARAM

toConstr :: EXTPARAM -> Constr

dataTypeOf :: EXTPARAM -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EXTPARAM)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXTPARAM)

gmapT :: (forall b. Data b => b -> b) -> EXTPARAM -> EXTPARAM

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXTPARAM -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXTPARAM -> r

gmapQ :: (forall d. Data d => d -> u) -> EXTPARAM -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EXTPARAM -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EXTPARAM -> m EXTPARAM

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EXTPARAM -> m EXTPARAM

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EXTPARAM -> m EXTPARAM

Ord EXTPARAM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: EXTPARAM -> EXTPARAM -> Ordering

(<) :: EXTPARAM -> EXTPARAM -> Bool

(<=) :: EXTPARAM -> EXTPARAM -> Bool

(>) :: EXTPARAM -> EXTPARAM -> Bool

(>=) :: EXTPARAM -> EXTPARAM -> Bool

max :: EXTPARAM -> EXTPARAM -> EXTPARAM

min :: EXTPARAM -> EXTPARAM -> EXTPARAM

Show EXTPARAM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> EXTPARAM -> ShowS

show :: EXTPARAM -> String

showList :: [EXTPARAM] -> ShowS

Generic EXTPARAM 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep EXTPARAM :: Type -> Type

Methods

from :: EXTPARAM -> Rep EXTPARAM x

to :: Rep EXTPARAM x -> EXTPARAM

FromJSON EXTPARAM 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser EXTPARAM

parseJSONList :: Value -> Parser [EXTPARAM]

ToJSON EXTPARAM 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: EXTPARAM -> Value

toEncoding :: EXTPARAM -> Encoding

toJSONList :: [EXTPARAM] -> Value

toEncodingList :: [EXTPARAM] -> Encoding

ShATermConvertible EXTPARAM 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> EXTPARAM -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [EXTPARAM] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, EXTPARAM)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [EXTPARAM])

Pretty EXTPARAM Source # 
Instance details

Defined in CSL.Print_AS

type Rep EXTPARAM 
Instance details

Defined in CSL.ATC_CSL

type Rep EXTPARAM = D1 ('MetaData "EXTPARAM" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "EP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 APInt))))

data BASIC_ITEM Source #

basic items: an operator, extended parameter or variable declaration or an axiom

Instances

Instances details
Data BASIC_ITEM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_ITEM -> c BASIC_ITEM

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_ITEM

toConstr :: BASIC_ITEM -> Constr

dataTypeOf :: BASIC_ITEM -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BASIC_ITEM)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASIC_ITEM)

gmapT :: (forall b. Data b => b -> b) -> BASIC_ITEM -> BASIC_ITEM

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEM -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEM -> r

gmapQ :: (forall d. Data d => d -> u) -> BASIC_ITEM -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_ITEM -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_ITEM -> m BASIC_ITEM

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEM -> m BASIC_ITEM

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEM -> m BASIC_ITEM

Show BASIC_ITEM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> BASIC_ITEM -> ShowS

show :: BASIC_ITEM -> String

showList :: [BASIC_ITEM] -> ShowS

Generic BASIC_ITEM 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep BASIC_ITEM :: Type -> Type

Methods

from :: BASIC_ITEM -> Rep BASIC_ITEM x

to :: Rep BASIC_ITEM x -> BASIC_ITEM

GetRange BASIC_ITEM Source # 
Instance details

Defined in CSL.Print_AS

FromJSON BASIC_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser BASIC_ITEM

parseJSONList :: Value -> Parser [BASIC_ITEM]

ToJSON BASIC_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: BASIC_ITEM -> Value

toEncoding :: BASIC_ITEM -> Encoding

toJSONList :: [BASIC_ITEM] -> Value

toEncodingList :: [BASIC_ITEM] -> Encoding

ShATermConvertible BASIC_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> BASIC_ITEM -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BASIC_ITEM] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEM)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_ITEM])

Pretty BASIC_ITEM Source # 
Instance details

Defined in CSL.Print_AS

type Rep BASIC_ITEM 
Instance details

Defined in CSL.ATC_CSL

type Rep BASIC_ITEM = D1 ('MetaData "BASIC_ITEM" "CSL.AS_BASIC_CSL" "main" 'False) ((C1 ('MetaCons "Op_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_ITEM)) :+: (C1 ('MetaCons "EP_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Token, EPDomain)])) :+: C1 ('MetaCons "EP_domdecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Token, APInt)])))) :+: (C1 ('MetaCons "EP_defval" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Token, APInt)])) :+: (C1 ('MetaCons "Var_decls" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_ITEM])) :+: C1 ('MetaCons "Axiom_item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Annoted CMD))))))

newtype BASIC_SPEC Source #

Constructors

Basic_spec [Annoted BASIC_ITEM] 

Instances

Instances details
Data BASIC_SPEC Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_SPEC -> c BASIC_SPEC

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_SPEC

toConstr :: BASIC_SPEC -> Constr

dataTypeOf :: BASIC_SPEC -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BASIC_SPEC)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASIC_SPEC)

gmapT :: (forall b. Data b => b -> b) -> BASIC_SPEC -> BASIC_SPEC

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> r

gmapQ :: (forall d. Data d => d -> u) -> BASIC_SPEC -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_SPEC -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC

Show BASIC_SPEC Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> BASIC_SPEC -> ShowS

show :: BASIC_SPEC -> String

showList :: [BASIC_SPEC] -> ShowS

Generic BASIC_SPEC 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep BASIC_SPEC :: Type -> Type

Methods

from :: BASIC_SPEC -> Rep BASIC_SPEC x

to :: Rep BASIC_SPEC x -> BASIC_SPEC

Semigroup BASIC_SPEC 
Instance details

Defined in CSL.Logic_CSL

Methods

(<>) :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC #

sconcat :: NonEmpty BASIC_SPEC -> BASIC_SPEC

stimes :: Integral b => b -> BASIC_SPEC -> BASIC_SPEC

Monoid BASIC_SPEC 
Instance details

Defined in CSL.Logic_CSL

GetRange BASIC_SPEC Source # 
Instance details

Defined in CSL.Print_AS

FromJSON BASIC_SPEC 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser BASIC_SPEC

parseJSONList :: Value -> Parser [BASIC_SPEC]

ToJSON BASIC_SPEC 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: BASIC_SPEC -> Value

toEncoding :: BASIC_SPEC -> Encoding

toJSONList :: [BASIC_SPEC] -> Value

toEncodingList :: [BASIC_SPEC] -> Encoding

ShATermConvertible BASIC_SPEC 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BASIC_SPEC] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_SPEC])

Pretty BASIC_SPEC Source # 
Instance details

Defined in CSL.Print_AS

Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #

Syntax of CSL logic

Instance details

Defined in CSL.Logic_CSL

StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for reduce logic

Instance details

Defined in CSL.Logic_CSL

Methods

basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source #

sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source #

extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source #

stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source #

signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source #

symbol_to_raw :: CSL -> Symbol -> Symbol Source #

id_to_raw :: CSL -> Id -> Symbol Source #

matches :: CSL -> Symbol -> Symbol -> Bool Source #

empty_signature :: CSL -> Sign Source #

add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source #

signature_union :: CSL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source #

intersection :: CSL -> Sign -> Sign -> Result Sign Source #

final_union :: CSL -> Sign -> Sign -> Result Sign Source #

morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CSL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CSL -> Morphism -> Bool Source #

is_injective :: CSL -> Morphism -> Bool Source #

theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source #

corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #

Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #

Instance of Logic for reduce logc

Instance details

Defined in CSL.Logic_CSL

Methods

parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source #

stability :: CSL -> Stability Source #

data_logic :: CSL -> Maybe AnyLogic Source #

top_sublogic :: CSL -> () Source #

all_sublogics :: CSL -> [()] Source #

bottomSublogic :: CSL -> Maybe () Source #

sublogicDimensions :: CSL -> [[()]] Source #

parseSublogic :: CSL -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source #

provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source #

default_prover :: CSL -> String Source #

cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source #

conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source #

empty_proof_tree :: CSL -> [EXPRESSION] Source #

syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSL -> Maybe OMCD Source #

export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source #

omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source #

addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source #

addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source #

sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

type Rep BASIC_SPEC 
Instance details

Defined in CSL.ATC_CSL

type Rep BASIC_SPEC = D1 ('MetaData "BASIC_SPEC" "CSL.AS_BASIC_CSL" "main" 'True) (C1 ('MetaCons "Basic_spec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted BASIC_ITEM])))

data SYMB_ITEMS Source #

symbol lists for hiding

Constructors

Symb_items [SYMB] Range 

Instances

Instances details
Eq SYMB_ITEMS Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool

(/=) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool

Data SYMB_ITEMS Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS

toConstr :: SYMB_ITEMS -> Constr

dataTypeOf :: SYMB_ITEMS -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)

gmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r

gmapQ :: (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS

Show SYMB_ITEMS Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> SYMB_ITEMS -> ShowS

show :: SYMB_ITEMS -> String

showList :: [SYMB_ITEMS] -> ShowS

Generic SYMB_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep SYMB_ITEMS :: Type -> Type

Methods

from :: SYMB_ITEMS -> Rep SYMB_ITEMS x

to :: Rep SYMB_ITEMS x -> SYMB_ITEMS

GetRange SYMB_ITEMS Source # 
Instance details

Defined in CSL.Print_AS

FromJSON SYMB_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser SYMB_ITEMS

parseJSONList :: Value -> Parser [SYMB_ITEMS]

ToJSON SYMB_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: SYMB_ITEMS -> Value

toEncoding :: SYMB_ITEMS -> Encoding

toJSONList :: [SYMB_ITEMS] -> Value

toEncodingList :: [SYMB_ITEMS] -> Encoding

ShATermConvertible SYMB_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> SYMB_ITEMS -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SYMB_ITEMS] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_ITEMS)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_ITEMS])

Pretty SYMB_ITEMS Source # 
Instance details

Defined in CSL.Print_AS

Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #

Syntax of CSL logic

Instance details

Defined in CSL.Logic_CSL

StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for reduce logic

Instance details

Defined in CSL.Logic_CSL

Methods

basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source #

sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source #

extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source #

stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source #

signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source #

symbol_to_raw :: CSL -> Symbol -> Symbol Source #

id_to_raw :: CSL -> Id -> Symbol Source #

matches :: CSL -> Symbol -> Symbol -> Bool Source #

empty_signature :: CSL -> Sign Source #

add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source #

signature_union :: CSL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source #

intersection :: CSL -> Sign -> Sign -> Result Sign Source #

final_union :: CSL -> Sign -> Sign -> Result Sign Source #

morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CSL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CSL -> Morphism -> Bool Source #

is_injective :: CSL -> Morphism -> Bool Source #

theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source #

corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #

Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #

Instance of Logic for reduce logc

Instance details

Defined in CSL.Logic_CSL

Methods

parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source #

stability :: CSL -> Stability Source #

data_logic :: CSL -> Maybe AnyLogic Source #

top_sublogic :: CSL -> () Source #

all_sublogics :: CSL -> [()] Source #

bottomSublogic :: CSL -> Maybe () Source #

sublogicDimensions :: CSL -> [[()]] Source #

parseSublogic :: CSL -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source #

provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source #

default_prover :: CSL -> String Source #

cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source #

conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source #

empty_proof_tree :: CSL -> [EXPRESSION] Source #

syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSL -> Maybe OMCD Source #

export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source #

omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source #

addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source #

addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source #

sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

type Rep SYMB_ITEMS 
Instance details

Defined in CSL.ATC_CSL

type Rep SYMB_ITEMS = D1 ('MetaData "SYMB_ITEMS" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "Symb_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SYMB]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

newtype SYMB Source #

symbol for identifiers

Constructors

Symb_id Token 

Instances

Instances details
Eq SYMB Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: SYMB -> SYMB -> Bool

(/=) :: SYMB -> SYMB -> Bool

Data SYMB Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

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

Show SYMB Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> SYMB -> ShowS

show :: SYMB -> String

showList :: [SYMB] -> ShowS

Generic SYMB 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep SYMB :: Type -> Type

Methods

from :: SYMB -> Rep SYMB x

to :: Rep SYMB x -> SYMB

GetRange SYMB Source # 
Instance details

Defined in CSL.Print_AS

FromJSON SYMB 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser SYMB

parseJSONList :: Value -> Parser [SYMB]

ToJSON SYMB 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: SYMB -> Value

toEncoding :: SYMB -> Encoding

toJSONList :: [SYMB] -> Value

toEncodingList :: [SYMB] -> Encoding

ShATermConvertible SYMB 
Instance details

Defined in CSL.ATC_CSL

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 CSL.Print_AS

Methods

pretty :: SYMB -> Doc Source #

pretties :: [SYMB] -> Doc Source #

type Rep SYMB 
Instance details

Defined in CSL.ATC_CSL

type Rep SYMB = D1 ('MetaData "SYMB" "CSL.AS_BASIC_CSL" "main" 'True) (C1 ('MetaCons "Symb_id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data SYMB_MAP_ITEMS Source #

symbol maps for renamings

Instances

Instances details
Eq SYMB_MAP_ITEMS Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Data SYMB_MAP_ITEMS Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS

toConstr :: SYMB_MAP_ITEMS -> Constr

dataTypeOf :: SYMB_MAP_ITEMS -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_MAP_ITEMS)

gmapT :: (forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r

gmapQ :: (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS

Show SYMB_MAP_ITEMS Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS

show :: SYMB_MAP_ITEMS -> String

showList :: [SYMB_MAP_ITEMS] -> ShowS

Generic SYMB_MAP_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep SYMB_MAP_ITEMS :: Type -> Type

GetRange SYMB_MAP_ITEMS Source # 
Instance details

Defined in CSL.Print_AS

FromJSON SYMB_MAP_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser SYMB_MAP_ITEMS

parseJSONList :: Value -> Parser [SYMB_MAP_ITEMS]

ToJSON SYMB_MAP_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: SYMB_MAP_ITEMS -> Value

toEncoding :: SYMB_MAP_ITEMS -> Encoding

toJSONList :: [SYMB_MAP_ITEMS] -> Value

toEncodingList :: [SYMB_MAP_ITEMS] -> Encoding

ShATermConvertible SYMB_MAP_ITEMS 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> SYMB_MAP_ITEMS -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SYMB_MAP_ITEMS] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_MAP_ITEMS)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_MAP_ITEMS])

Pretty SYMB_MAP_ITEMS Source # 
Instance details

Defined in CSL.Print_AS

Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #

Syntax of CSL logic

Instance details

Defined in CSL.Logic_CSL

StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for reduce logic

Instance details

Defined in CSL.Logic_CSL

Methods

basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source #

sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source #

extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source #

stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source #

signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source #

symbol_to_raw :: CSL -> Symbol -> Symbol Source #

id_to_raw :: CSL -> Id -> Symbol Source #

matches :: CSL -> Symbol -> Symbol -> Bool Source #

empty_signature :: CSL -> Sign Source #

add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source #

signature_union :: CSL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source #

intersection :: CSL -> Sign -> Sign -> Result Sign Source #

final_union :: CSL -> Sign -> Sign -> Result Sign Source #

morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CSL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CSL -> Morphism -> Bool Source #

is_injective :: CSL -> Morphism -> Bool Source #

theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source #

corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #

Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #

Instance of Logic for reduce logc

Instance details

Defined in CSL.Logic_CSL

Methods

parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source #

stability :: CSL -> Stability Source #

data_logic :: CSL -> Maybe AnyLogic Source #

top_sublogic :: CSL -> () Source #

all_sublogics :: CSL -> [()] Source #

bottomSublogic :: CSL -> Maybe () Source #

sublogicDimensions :: CSL -> [[()]] Source #

parseSublogic :: CSL -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source #

provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source #

default_prover :: CSL -> String Source #

cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source #

conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source #

empty_proof_tree :: CSL -> [EXPRESSION] Source #

syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSL -> Maybe OMCD Source #

export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source #

omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source #

addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source #

addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source #

sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

type Rep SYMB_MAP_ITEMS 
Instance details

Defined in CSL.ATC_CSL

type Rep SYMB_MAP_ITEMS = D1 ('MetaData "SYMB_MAP_ITEMS" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "Symb_map_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SYMB_OR_MAP]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data SYMB_OR_MAP Source #

symbol map or renaming (renaming then denotes the identity renaming)

Constructors

Symb SYMB 
Symb_map SYMB SYMB Range 

Instances

Instances details
Eq SYMB_OR_MAP Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool

(/=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool

Data SYMB_OR_MAP Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP

toConstr :: SYMB_OR_MAP -> Constr

dataTypeOf :: SYMB_OR_MAP -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_OR_MAP)

gmapT :: (forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r

gmapQ :: (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP

Show SYMB_OR_MAP Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> SYMB_OR_MAP -> ShowS

show :: SYMB_OR_MAP -> String

showList :: [SYMB_OR_MAP] -> ShowS

Generic SYMB_OR_MAP 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep SYMB_OR_MAP :: Type -> Type

Methods

from :: SYMB_OR_MAP -> Rep SYMB_OR_MAP x

to :: Rep SYMB_OR_MAP x -> SYMB_OR_MAP

GetRange SYMB_OR_MAP Source # 
Instance details

Defined in CSL.Print_AS

FromJSON SYMB_OR_MAP 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser SYMB_OR_MAP

parseJSONList :: Value -> Parser [SYMB_OR_MAP]

ToJSON SYMB_OR_MAP 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: SYMB_OR_MAP -> Value

toEncoding :: SYMB_OR_MAP -> Encoding

toJSONList :: [SYMB_OR_MAP] -> Value

toEncodingList :: [SYMB_OR_MAP] -> Encoding

ShATermConvertible SYMB_OR_MAP 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> SYMB_OR_MAP -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SYMB_OR_MAP] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_OR_MAP)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_OR_MAP])

Pretty SYMB_OR_MAP Source # 
Instance details

Defined in CSL.Print_AS

type Rep SYMB_OR_MAP 
Instance details

Defined in CSL.ATC_CSL

type Rep SYMB_OR_MAP = D1 ('MetaData "SYMB_OR_MAP" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "Symb" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB)) :+: C1 ('MetaCons "Symb_map" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data OPNAME Source #

Instances

Instances details
Eq OPNAME Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: OPNAME -> OPNAME -> Bool

(/=) :: OPNAME -> OPNAME -> Bool

Data OPNAME Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OPNAME -> c OPNAME

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OPNAME

toConstr :: OPNAME -> Constr

dataTypeOf :: OPNAME -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OPNAME)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OPNAME)

gmapT :: (forall b. Data b => b -> b) -> OPNAME -> OPNAME

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OPNAME -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OPNAME -> r

gmapQ :: (forall d. Data d => d -> u) -> OPNAME -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OPNAME -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OPNAME -> m OPNAME

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OPNAME -> m OPNAME

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OPNAME -> m OPNAME

Ord OPNAME Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: OPNAME -> OPNAME -> Ordering

(<) :: OPNAME -> OPNAME -> Bool

(<=) :: OPNAME -> OPNAME -> Bool

(>) :: OPNAME -> OPNAME -> Bool

(>=) :: OPNAME -> OPNAME -> Bool

max :: OPNAME -> OPNAME -> OPNAME

min :: OPNAME -> OPNAME -> OPNAME

Show OPNAME Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> OPNAME -> ShowS

show :: OPNAME -> String

showList :: [OPNAME] -> ShowS

Generic OPNAME 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep OPNAME :: Type -> Type

Methods

from :: OPNAME -> Rep OPNAME x

to :: Rep OPNAME x -> OPNAME

FromJSON OPNAME 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser OPNAME

parseJSONList :: Value -> Parser [OPNAME]

ToJSON OPNAME 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: OPNAME -> Value

toEncoding :: OPNAME -> Encoding

toJSONList :: [OPNAME] -> Value

toEncodingList :: [OPNAME] -> Encoding

ShATermConvertible OPNAME 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> OPNAME -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [OPNAME] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, OPNAME)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [OPNAME])

ExpressionPrinter (Reader OpInfoNameMap) Source #

An OpInfoNameMap can be interpreted as an ExpressionPrinter

Instance details

Defined in CSL.Print_AS

type Rep OPNAME 
Instance details

Defined in CSL.ATC_CSL

type Rep OPNAME = D1 ('MetaData "OPNAME" "CSL.AS_BASIC_CSL" "main" 'False) (((((C1 ('MetaCons "OP_mult" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_div" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_plus" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "OP_minus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_neg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_pow" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OP_fthrt" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_sqrt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_abs" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "OP_max" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_min" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_sign" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "OP_cos" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_sin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_tan" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "OP_cot" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_Pi" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_reldist" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OP_minimize" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_minloc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_maximize" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "OP_maxloc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_factor" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OP_approx" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_divide" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "OP_factorize" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_int" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_rlqe" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "OP_simplify" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_solve" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_neq" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OP_lt" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_leq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_eq" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "OP_gt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_geq" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OP_convergence" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_reldistLe" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "OP_in" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_undef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_failure" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "OP_false" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_true" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_not" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OP_and" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OP_or" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_impl" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "OP_ex" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_all" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OP_hastype" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OP_real" 'PrefixI 'False) (U1 :: Type -> Type)))))))

data OPID Source #

Instances

Instances details
Eq OPID Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: OPID -> OPID -> Bool

(/=) :: OPID -> OPID -> Bool

Data OPID Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OPID -> c OPID

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OPID

toConstr :: OPID -> Constr

dataTypeOf :: OPID -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OPID)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OPID)

gmapT :: (forall b. Data b => b -> b) -> OPID -> OPID

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OPID -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OPID -> r

gmapQ :: (forall d. Data d => d -> u) -> OPID -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OPID -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OPID -> m OPID

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OPID -> m OPID

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OPID -> m OPID

Ord OPID Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: OPID -> OPID -> Ordering

(<) :: OPID -> OPID -> Bool

(<=) :: OPID -> OPID -> Bool

(>) :: OPID -> OPID -> Bool

(>=) :: OPID -> OPID -> Bool

max :: OPID -> OPID -> OPID

min :: OPID -> OPID -> OPID

Show OPID Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> OPID -> ShowS

show :: OPID -> String

showList :: [OPID] -> ShowS

Generic OPID 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep OPID :: Type -> Type

Methods

from :: OPID -> Rep OPID x

to :: Rep OPID x -> OPID

FromJSON OPID 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser OPID

parseJSONList :: Value -> Parser [OPID]

ToJSON OPID 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: OPID -> Value

toEncoding :: OPID -> Encoding

toJSONList :: [OPID] -> Value

toEncodingList :: [OPID] -> Encoding

ShATermConvertible OPID 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> OPID -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [OPID] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, OPID)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [OPID])

Pretty OPID Source # 
Instance details

Defined in CSL.Print_AS

Methods

pretty :: OPID -> Doc Source #

pretties :: [OPID] -> Doc Source #

type Rep OPID 
Instance details

Defined in CSL.ATC_CSL

type Rep OPID = D1 ('MetaData "OPID" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "OpId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OPNAME)) :+: C1 ('MetaCons "OpUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstantName)))

data ConstantName Source #

We differentiate between simple constant names and indexed constant names resulting from the extended parameter elimination.

Constructors

SimpleConstant String 
ElimConstant String Int 

Instances

Instances details
Eq ConstantName Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: ConstantName -> ConstantName -> Bool

(/=) :: ConstantName -> ConstantName -> Bool

Data ConstantName Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConstantName -> c ConstantName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConstantName

toConstr :: ConstantName -> Constr

dataTypeOf :: ConstantName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConstantName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstantName)

gmapT :: (forall b. Data b => b -> b) -> ConstantName -> ConstantName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConstantName -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConstantName -> r

gmapQ :: (forall d. Data d => d -> u) -> ConstantName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConstantName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConstantName -> m ConstantName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstantName -> m ConstantName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstantName -> m ConstantName

Ord ConstantName Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Show ConstantName Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> ConstantName -> ShowS

show :: ConstantName -> String

showList :: [ConstantName] -> ShowS

Generic ConstantName 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep ConstantName :: Type -> Type

FromJSON ConstantName 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser ConstantName

parseJSONList :: Value -> Parser [ConstantName]

ToJSON ConstantName 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: ConstantName -> Value

toEncoding :: ConstantName -> Encoding

toJSONList :: [ConstantName] -> Value

toEncodingList :: [ConstantName] -> Encoding

ShATermConvertible ConstantName 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> ConstantName -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ConstantName] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ConstantName)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ConstantName])

Pretty ConstantName Source # 
Instance details

Defined in CSL.Print_AS

type Rep ConstantName 
Instance details

Defined in CSL.ATC_CSL

type Rep ConstantName = D1 ('MetaData "ConstantName" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "SimpleConstant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "ElimConstant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

data OP_ITEM Source #

operator symbol declaration

Constructors

Op_item [Token] Range 

Instances

Instances details
Data OP_ITEM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OP_ITEM -> c OP_ITEM

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OP_ITEM

toConstr :: OP_ITEM -> Constr

dataTypeOf :: OP_ITEM -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OP_ITEM)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OP_ITEM)

gmapT :: (forall b. Data b => b -> b) -> OP_ITEM -> OP_ITEM

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OP_ITEM -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OP_ITEM -> r

gmapQ :: (forall d. Data d => d -> u) -> OP_ITEM -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OP_ITEM -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OP_ITEM -> m OP_ITEM

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_ITEM -> m OP_ITEM

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_ITEM -> m OP_ITEM

Show OP_ITEM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> OP_ITEM -> ShowS

show :: OP_ITEM -> String

showList :: [OP_ITEM] -> ShowS

Generic OP_ITEM 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep OP_ITEM :: Type -> Type

Methods

from :: OP_ITEM -> Rep OP_ITEM x

to :: Rep OP_ITEM x -> OP_ITEM

GetRange OP_ITEM Source # 
Instance details

Defined in CSL.Print_AS

FromJSON OP_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser OP_ITEM

parseJSONList :: Value -> Parser [OP_ITEM]

ToJSON OP_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: OP_ITEM -> Value

toEncoding :: OP_ITEM -> Encoding

toJSONList :: [OP_ITEM] -> Value

toEncodingList :: [OP_ITEM] -> Encoding

ShATermConvertible OP_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> OP_ITEM -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [OP_ITEM] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_ITEM)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [OP_ITEM])

Pretty OP_ITEM Source # 
Instance details

Defined in CSL.Print_AS

type Rep OP_ITEM 
Instance details

Defined in CSL.ATC_CSL

type Rep OP_ITEM = D1 ('MetaData "OP_ITEM" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "Op_item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Token]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data VAR_ITEM Source #

variable symbol declaration

Constructors

Var_item [Token] Domain Range 

Instances

Instances details
Data VAR_ITEM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VAR_ITEM -> c VAR_ITEM

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VAR_ITEM

toConstr :: VAR_ITEM -> Constr

dataTypeOf :: VAR_ITEM -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VAR_ITEM)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VAR_ITEM)

gmapT :: (forall b. Data b => b -> b) -> VAR_ITEM -> VAR_ITEM

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VAR_ITEM -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VAR_ITEM -> r

gmapQ :: (forall d. Data d => d -> u) -> VAR_ITEM -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> VAR_ITEM -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VAR_ITEM -> m VAR_ITEM

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VAR_ITEM -> m VAR_ITEM

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VAR_ITEM -> m VAR_ITEM

Show VAR_ITEM Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> VAR_ITEM -> ShowS

show :: VAR_ITEM -> String

showList :: [VAR_ITEM] -> ShowS

Generic VAR_ITEM 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep VAR_ITEM :: Type -> Type

Methods

from :: VAR_ITEM -> Rep VAR_ITEM x

to :: Rep VAR_ITEM x -> VAR_ITEM

GetRange VAR_ITEM Source # 
Instance details

Defined in CSL.Print_AS

FromJSON VAR_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser VAR_ITEM

parseJSONList :: Value -> Parser [VAR_ITEM]

ToJSON VAR_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: VAR_ITEM -> Value

toEncoding :: VAR_ITEM -> Encoding

toJSONList :: [VAR_ITEM] -> Value

toEncodingList :: [VAR_ITEM] -> Encoding

ShATermConvertible VAR_ITEM 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> VAR_ITEM -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [VAR_ITEM] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, VAR_ITEM)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [VAR_ITEM])

Pretty VAR_ITEM Source # 
Instance details

Defined in CSL.Print_AS

type Rep VAR_ITEM 
Instance details

Defined in CSL.ATC_CSL

type Rep VAR_ITEM = D1 ('MetaData "VAR_ITEM" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "Var_item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Token]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Domain) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data VarDecl Source #

Constructors

VarDecl Token (Maybe Domain) 

Instances

Instances details
Eq VarDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: VarDecl -> VarDecl -> Bool

(/=) :: VarDecl -> VarDecl -> Bool

Data VarDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

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 CSL.AS_BASIC_CSL

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 CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> VarDecl -> ShowS

show :: VarDecl -> String

showList :: [VarDecl] -> ShowS

Generic VarDecl 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep VarDecl :: Type -> Type

Methods

from :: VarDecl -> Rep VarDecl x

to :: Rep VarDecl x -> VarDecl

FromJSON VarDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser VarDecl

parseJSONList :: Value -> Parser [VarDecl]

ToJSON VarDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: VarDecl -> Value

toEncoding :: VarDecl -> Encoding

toJSONList :: [VarDecl] -> Value

toEncodingList :: [VarDecl] -> Encoding

ShATermConvertible VarDecl 
Instance details

Defined in CSL.ATC_CSL

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 CSL.Print_AS

type Rep VarDecl 
Instance details

Defined in CSL.ATC_CSL

type Rep VarDecl = D1 ('MetaData "VarDecl" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "VarDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Domain))))

data OpDecl Source #

Instances

Instances details
Eq OpDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: OpDecl -> OpDecl -> Bool

(/=) :: OpDecl -> OpDecl -> Bool

Data OpDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpDecl -> c OpDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpDecl

toConstr :: OpDecl -> Constr

dataTypeOf :: OpDecl -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpDecl)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDecl)

gmapT :: (forall b. Data b => b -> b) -> OpDecl -> OpDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpDecl -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> OpDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpDecl -> m OpDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpDecl -> m OpDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpDecl -> m OpDecl

Ord OpDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: OpDecl -> OpDecl -> Ordering

(<) :: OpDecl -> OpDecl -> Bool

(<=) :: OpDecl -> OpDecl -> Bool

(>) :: OpDecl -> OpDecl -> Bool

(>=) :: OpDecl -> OpDecl -> Bool

max :: OpDecl -> OpDecl -> OpDecl

min :: OpDecl -> OpDecl -> OpDecl

Show OpDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> OpDecl -> ShowS

show :: OpDecl -> String

showList :: [OpDecl] -> ShowS

Generic OpDecl 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep OpDecl :: Type -> Type

Methods

from :: OpDecl -> Rep OpDecl x

to :: Rep OpDecl x -> OpDecl

FromJSON OpDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser OpDecl

parseJSONList :: Value -> Parser [OpDecl]

ToJSON OpDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: OpDecl -> Value

toEncoding :: OpDecl -> Encoding

toJSONList :: [OpDecl] -> Value

toEncodingList :: [OpDecl] -> Encoding

ShATermConvertible OpDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> OpDecl -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [OpDecl] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, OpDecl)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpDecl])

Pretty OpDecl Source # 
Instance details

Defined in CSL.Print_AS

type Rep OpDecl 
Instance details

Defined in CSL.ATC_CSL

type Rep OpDecl = D1 ('MetaData "OpDecl" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "OpDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstantName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EXTPARAM])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VarDecl]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data EPDecl Source #

Constructors

EPDecl Token EPDomain (Maybe APInt) 

Instances

Instances details
Eq EPDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: EPDecl -> EPDecl -> Bool

(/=) :: EPDecl -> EPDecl -> Bool

Data EPDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EPDecl -> c EPDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EPDecl

toConstr :: EPDecl -> Constr

dataTypeOf :: EPDecl -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EPDecl)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EPDecl)

gmapT :: (forall b. Data b => b -> b) -> EPDecl -> EPDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EPDecl -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EPDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> EPDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EPDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EPDecl -> m EPDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EPDecl -> m EPDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EPDecl -> m EPDecl

Ord EPDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: EPDecl -> EPDecl -> Ordering

(<) :: EPDecl -> EPDecl -> Bool

(<=) :: EPDecl -> EPDecl -> Bool

(>) :: EPDecl -> EPDecl -> Bool

(>=) :: EPDecl -> EPDecl -> Bool

max :: EPDecl -> EPDecl -> EPDecl

min :: EPDecl -> EPDecl -> EPDecl

Show EPDecl Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> EPDecl -> ShowS

show :: EPDecl -> String

showList :: [EPDecl] -> ShowS

Generic EPDecl 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep EPDecl :: Type -> Type

Methods

from :: EPDecl -> Rep EPDecl x

to :: Rep EPDecl x -> EPDecl

FromJSON EPDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser EPDecl

parseJSONList :: Value -> Parser [EPDecl]

ToJSON EPDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: EPDecl -> Value

toEncoding :: EPDecl -> Encoding

toJSONList :: [EPDecl] -> Value

toEncodingList :: [EPDecl] -> Encoding

ShATermConvertible EPDecl 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> EPDecl -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [EPDecl] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, EPDecl)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [EPDecl])

Pretty EPDecl Source # 
Instance details

Defined in CSL.Print_AS

type Rep EPDecl 
Instance details

Defined in CSL.ATC_CSL

type Rep EPDecl = D1 ('MetaData "EPDecl" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "EPDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EPDomain) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe APInt)))))

data EPVal Source #

Extended Parameter value may be an integer or a reference to an EPDomVal. This type is used for the domain specification of EPs (see EPDomain).

Constructors

EPVal APInt 
EPConstRef Token 

Instances

Instances details
Eq EPVal Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: EPVal -> EPVal -> Bool

(/=) :: EPVal -> EPVal -> Bool

Data EPVal Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EPVal -> c EPVal

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EPVal

toConstr :: EPVal -> Constr

dataTypeOf :: EPVal -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EPVal)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EPVal)

gmapT :: (forall b. Data b => b -> b) -> EPVal -> EPVal

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EPVal -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EPVal -> r

gmapQ :: (forall d. Data d => d -> u) -> EPVal -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EPVal -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EPVal -> m EPVal

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EPVal -> m EPVal

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EPVal -> m EPVal

Ord EPVal Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: EPVal -> EPVal -> Ordering

(<) :: EPVal -> EPVal -> Bool

(<=) :: EPVal -> EPVal -> Bool

(>) :: EPVal -> EPVal -> Bool

(>=) :: EPVal -> EPVal -> Bool

max :: EPVal -> EPVal -> EPVal

min :: EPVal -> EPVal -> EPVal

Show EPVal Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> EPVal -> ShowS

show :: EPVal -> String

showList :: [EPVal] -> ShowS

Generic EPVal 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep EPVal :: Type -> Type

Methods

from :: EPVal -> Rep EPVal x

to :: Rep EPVal x -> EPVal

FromJSON EPVal 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser EPVal

parseJSONList :: Value -> Parser [EPVal]

ToJSON EPVal 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: EPVal -> Value

toEncoding :: EPVal -> Encoding

toJSONList :: [EPVal] -> Value

toEncodingList :: [EPVal] -> Encoding

ShATermConvertible EPVal 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> EPVal -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [EPVal] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, EPVal)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [EPVal])

Pretty EPVal Source # 
Instance details

Defined in CSL.Print_AS

type Rep EPVal 
Instance details

Defined in CSL.ATC_CSL

type Rep EPVal = D1 ('MetaData "EPVal" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "EPVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 APInt)) :+: C1 ('MetaCons "EPConstRef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data GroundConstant Source #

Constructors

GCI APInt 
GCR APFloat 

Instances

Instances details
Eq GroundConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Data GroundConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GroundConstant -> c GroundConstant

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GroundConstant

toConstr :: GroundConstant -> Constr

dataTypeOf :: GroundConstant -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GroundConstant)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GroundConstant)

gmapT :: (forall b. Data b => b -> b) -> GroundConstant -> GroundConstant

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GroundConstant -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GroundConstant -> r

gmapQ :: (forall d. Data d => d -> u) -> GroundConstant -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> GroundConstant -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GroundConstant -> m GroundConstant

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GroundConstant -> m GroundConstant

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GroundConstant -> m GroundConstant

Ord GroundConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Show GroundConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> GroundConstant -> ShowS

show :: GroundConstant -> String

showList :: [GroundConstant] -> ShowS

Generic GroundConstant 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep GroundConstant :: Type -> Type

Continuous GroundConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

FromJSON GroundConstant 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser GroundConstant

parseJSONList :: Value -> Parser [GroundConstant]

ToJSON GroundConstant 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: GroundConstant -> Value

toEncoding :: GroundConstant -> Encoding

toJSONList :: [GroundConstant] -> Value

toEncodingList :: [GroundConstant] -> Encoding

ShATermConvertible GroundConstant 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> GroundConstant -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [GroundConstant] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, GroundConstant)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [GroundConstant])

Pretty GroundConstant Source # 
Instance details

Defined in CSL.Print_AS

type Rep GroundConstant 
Instance details

Defined in CSL.ATC_CSL

type Rep GroundConstant = D1 ('MetaData "GroundConstant" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "GCI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 APInt)) :+: C1 ('MetaCons "GCR" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 APFloat)))

cmpFloatToInt :: APFloat -> APInt -> Ordering Source #

data AssDefinition Source #

A constant or function definition

Constructors

ConstDef EXPRESSION 
FunDef [String] EXPRESSION 

Instances

Instances details
Eq AssDefinition Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Data AssDefinition Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AssDefinition -> c AssDefinition

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AssDefinition

toConstr :: AssDefinition -> Constr

dataTypeOf :: AssDefinition -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AssDefinition)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssDefinition)

gmapT :: (forall b. Data b => b -> b) -> AssDefinition -> AssDefinition

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AssDefinition -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AssDefinition -> r

gmapQ :: (forall d. Data d => d -> u) -> AssDefinition -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AssDefinition -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AssDefinition -> m AssDefinition

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AssDefinition -> m AssDefinition

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AssDefinition -> m AssDefinition

Ord AssDefinition Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Show AssDefinition Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> AssDefinition -> ShowS

show :: AssDefinition -> String

showList :: [AssDefinition] -> ShowS

Generic AssDefinition 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep AssDefinition :: Type -> Type

FromJSON AssDefinition 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser AssDefinition

parseJSONList :: Value -> Parser [AssDefinition]

ToJSON AssDefinition 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: AssDefinition -> Value

toEncoding :: AssDefinition -> Encoding

toJSONList :: [AssDefinition] -> Value

toEncodingList :: [AssDefinition] -> Encoding

ShATermConvertible AssDefinition 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> AssDefinition -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [AssDefinition] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, AssDefinition)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [AssDefinition])

Pretty AssDefinition Source # 
Instance details

Defined in CSL.Print_AS

type Rep AssDefinition 
Instance details

Defined in CSL.ATC_CSL

type Rep AssDefinition = D1 ('MetaData "AssDefinition" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "ConstDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EXPRESSION)) :+: C1 ('MetaCons "FunDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EXPRESSION)))

data InstantiatedConstant Source #

Instances

Instances details
Eq InstantiatedConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Data InstantiatedConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InstantiatedConstant -> c InstantiatedConstant

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InstantiatedConstant

toConstr :: InstantiatedConstant -> Constr

dataTypeOf :: InstantiatedConstant -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InstantiatedConstant)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InstantiatedConstant)

gmapT :: (forall b. Data b => b -> b) -> InstantiatedConstant -> InstantiatedConstant

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InstantiatedConstant -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InstantiatedConstant -> r

gmapQ :: (forall d. Data d => d -> u) -> InstantiatedConstant -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> InstantiatedConstant -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> InstantiatedConstant -> m InstantiatedConstant

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InstantiatedConstant -> m InstantiatedConstant

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InstantiatedConstant -> m InstantiatedConstant

Ord InstantiatedConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Show InstantiatedConstant Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> InstantiatedConstant -> ShowS

show :: InstantiatedConstant -> String

showList :: [InstantiatedConstant] -> ShowS

Generic InstantiatedConstant 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep InstantiatedConstant :: Type -> Type

FromJSON InstantiatedConstant 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser InstantiatedConstant

parseJSONList :: Value -> Parser [InstantiatedConstant]

ToJSON InstantiatedConstant 
Instance details

Defined in CSL.ATC_CSL

ShATermConvertible InstantiatedConstant 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> InstantiatedConstant -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [InstantiatedConstant] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, InstantiatedConstant)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [InstantiatedConstant])

Pretty InstantiatedConstant Source # 
Instance details

Defined in CSL.Print_AS

type Rep InstantiatedConstant 
Instance details

Defined in CSL.ATC_CSL

type Rep InstantiatedConstant = D1 ('MetaData "InstantiatedConstant" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "InstantiatedConstant" 'PrefixI 'True) (S1 ('MetaSel ('Just "constName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstantName) :*: S1 ('MetaSel ('Just "instantiation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EXPRESSION])))

data CMD Source #

Instances

Instances details
Eq CMD Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: CMD -> CMD -> Bool

(/=) :: CMD -> CMD -> Bool

Data CMD Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMD -> c CMD

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CMD

toConstr :: CMD -> Constr

dataTypeOf :: CMD -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CMD)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CMD)

gmapT :: (forall b. Data b => b -> b) -> CMD -> CMD

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMD -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMD -> r

gmapQ :: (forall d. Data d => d -> u) -> CMD -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CMD -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMD -> m CMD

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMD -> m CMD

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMD -> m CMD

Ord CMD Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: CMD -> CMD -> Ordering

(<) :: CMD -> CMD -> Bool

(<=) :: CMD -> CMD -> Bool

(>) :: CMD -> CMD -> Bool

(>=) :: CMD -> CMD -> Bool

max :: CMD -> CMD -> CMD

min :: CMD -> CMD -> CMD

Show CMD Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> CMD -> ShowS

show :: CMD -> String

showList :: [CMD] -> ShowS

Generic CMD 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep CMD :: Type -> Type

Methods

from :: CMD -> Rep CMD x

to :: Rep CMD x -> CMD

GetRange CMD Source # 
Instance details

Defined in CSL.Print_AS

FromJSON CMD 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser CMD

parseJSONList :: Value -> Parser [CMD]

ToJSON CMD 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: CMD -> Value

toEncoding :: CMD -> Encoding

toJSONList :: [CMD] -> Value

toEncodingList :: [CMD] -> Encoding

ShATermConvertible CMD 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> CMD -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CMD] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CMD)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CMD])

Pretty CMD Source # 
Instance details

Defined in CSL.Print_AS

Methods

pretty :: CMD -> Doc Source #

pretties :: [CMD] -> Doc Source #

Sentences CSL CMD Sign Morphism Symbol Source #

Instance of Sentences for reduce logic

Instance details

Defined in CSL.Logic_CSL

StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #

Static Analysis for reduce logic

Instance details

Defined in CSL.Logic_CSL

Methods

basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source #

sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source #

extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source #

stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source #

signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source #

symbol_to_raw :: CSL -> Symbol -> Symbol Source #

id_to_raw :: CSL -> Id -> Symbol Source #

matches :: CSL -> Symbol -> Symbol -> Bool Source #

empty_signature :: CSL -> Sign Source #

add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source #

signature_union :: CSL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source #

intersection :: CSL -> Sign -> Sign -> Result Sign Source #

final_union :: CSL -> Sign -> Sign -> Result Sign Source #

morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CSL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CSL -> Morphism -> Bool Source #

is_injective :: CSL -> Morphism -> Bool Source #

theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source #

corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #

Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #

Instance of Logic for reduce logc

Instance details

Defined in CSL.Logic_CSL

Methods

parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source #

stability :: CSL -> Stability Source #

data_logic :: CSL -> Maybe AnyLogic Source #

top_sublogic :: CSL -> () Source #

all_sublogics :: CSL -> [()] Source #

bottomSublogic :: CSL -> Maybe () Source #

sublogicDimensions :: CSL -> [[()]] Source #

parseSublogic :: CSL -> String -> Maybe () Source #

proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source #

provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source #

default_prover :: CSL -> String Source #

cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source #

conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source #

empty_proof_tree :: CSL -> [EXPRESSION] Source #

syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CSL -> Maybe OMCD Source #

export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source #

export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source #

omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source #

addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source #

addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source #

sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

type Rep CMD 
Instance details

Defined in CSL.ATC_CSL

type Rep CMD = D1 ('MetaData "CMD" "CSL.AS_BASIC_CSL" "main" 'False) ((C1 ('MetaCons "Ass" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpDecl) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EXPRESSION)) :+: C1 ('MetaCons "Cmd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EXPRESSION]))) :+: (C1 ('MetaCons "Sequence" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CMD])) :+: (C1 ('MetaCons "Cond" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(EXPRESSION, [CMD])])) :+: C1 ('MetaCons "Repeat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 EXPRESSION) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [CMD])))))

class OperatorState a where Source #

Minimal complete definition

lookupOperator, lookupBinder

Methods

addVar :: a -> String -> a Source #

isVar :: a -> String -> Bool Source #

lookupOperator Source #

Arguments

:: a 
-> String

operator name

-> Int

operator arity

-> Either Bool OpInfo 

lookupBinder Source #

Arguments

:: a 
-> String

binder name

-> Maybe OpInfo 

Instances

Instances details
OperatorState () Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

addVar :: () -> String -> () Source #

isVar :: () -> String -> Bool Source #

lookupOperator :: () -> String -> Int -> Either Bool OpInfo Source #

lookupBinder :: () -> String -> Maybe OpInfo Source #

OperatorState (AnnoState st) Source # 
Instance details

Defined in CSL.Parse_AS_Basic

Methods

addVar :: AnnoState st -> String -> AnnoState st Source #

isVar :: AnnoState st -> String -> Bool Source #

lookupOperator :: AnnoState st -> String -> Int -> Either Bool OpInfo Source #

lookupBinder :: AnnoState st -> String -> Maybe OpInfo Source #

OperatorState a => OperatorState (OpVarState a) Source # 
Instance details

Defined in CSL.Parse_AS_Basic

Methods

addVar :: OpVarState a -> String -> OpVarState a Source #

isVar :: OpVarState a -> String -> Bool Source #

lookupOperator :: OpVarState a -> String -> Int -> Either Bool OpInfo Source #

lookupBinder :: OpVarState a -> String -> Maybe OpInfo Source #

OperatorState (OpInfoMap, BindInfoMap) Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

addVar :: (OpInfoMap, BindInfoMap) -> String -> (OpInfoMap, BindInfoMap) Source #

isVar :: (OpInfoMap, BindInfoMap) -> String -> Bool Source #

lookupOperator :: (OpInfoMap, BindInfoMap) -> String -> Int -> Either Bool OpInfo Source #

lookupBinder :: (OpInfoMap, BindInfoMap) -> String -> Maybe OpInfo Source #

data OpInfo Source #

Constructors

OpInfo 

Fields

  • prec :: Int

    precedence between 0 and maxPrecedence

  • infx :: Bool

    True = infix

  • arity :: Int

    the operator arity

  • foldNAry :: Bool

    True = fold nary-applications during construction into binary ones

  • opname :: OPNAME

    The actual operator name

  • bind :: Maybe BindInfo

    More info for binders

Instances

Instances details
Eq OpInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: OpInfo -> OpInfo -> Bool

(/=) :: OpInfo -> OpInfo -> Bool

Data OpInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpInfo -> c OpInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpInfo

toConstr :: OpInfo -> Constr

dataTypeOf :: OpInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo)

gmapT :: (forall b. Data b => b -> b) -> OpInfo -> OpInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> OpInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo

Ord OpInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: OpInfo -> OpInfo -> Ordering

(<) :: OpInfo -> OpInfo -> Bool

(<=) :: OpInfo -> OpInfo -> Bool

(>) :: OpInfo -> OpInfo -> Bool

(>=) :: OpInfo -> OpInfo -> Bool

max :: OpInfo -> OpInfo -> OpInfo

min :: OpInfo -> OpInfo -> OpInfo

Show OpInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> OpInfo -> ShowS

show :: OpInfo -> String

showList :: [OpInfo] -> ShowS

Generic OpInfo 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep OpInfo :: Type -> Type

Methods

from :: OpInfo -> Rep OpInfo x

to :: Rep OpInfo x -> OpInfo

FromJSON OpInfo 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser OpInfo

parseJSONList :: Value -> Parser [OpInfo]

ToJSON OpInfo 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: OpInfo -> Value

toEncoding :: OpInfo -> Encoding

toJSONList :: [OpInfo] -> Value

toEncodingList :: [OpInfo] -> Encoding

ShATermConvertible OpInfo 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> OpInfo -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [OpInfo] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, OpInfo)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpInfo])

ExpressionPrinter (Reader OpInfoNameMap) Source #

An OpInfoNameMap can be interpreted as an ExpressionPrinter

Instance details

Defined in CSL.Print_AS

OperatorState (OpInfoMap, BindInfoMap) Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

addVar :: (OpInfoMap, BindInfoMap) -> String -> (OpInfoMap, BindInfoMap) Source #

isVar :: (OpInfoMap, BindInfoMap) -> String -> Bool Source #

lookupOperator :: (OpInfoMap, BindInfoMap) -> String -> Int -> Either Bool OpInfo Source #

lookupBinder :: (OpInfoMap, BindInfoMap) -> String -> Maybe OpInfo Source #

type Rep OpInfo 
Instance details

Defined in CSL.ATC_CSL

type Rep OpInfo = D1 ('MetaData "OpInfo" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "OpInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "prec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: (S1 ('MetaSel ('Just "infx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :*: (S1 ('MetaSel ('Just "foldNAry") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "opname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OPNAME) :*: S1 ('MetaSel ('Just "bind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe BindInfo))))))

data BindInfo Source #

Constructors

BindInfo 

Fields

Instances

Instances details
Eq BindInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

(==) :: BindInfo -> BindInfo -> Bool

(/=) :: BindInfo -> BindInfo -> Bool

Data BindInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindInfo -> c BindInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindInfo

toConstr :: BindInfo -> Constr

dataTypeOf :: BindInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindInfo)

gmapT :: (forall b. Data b => b -> b) -> BindInfo -> BindInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> BindInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BindInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindInfo -> m BindInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindInfo -> m BindInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindInfo -> m BindInfo

Ord BindInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

compare :: BindInfo -> BindInfo -> Ordering

(<) :: BindInfo -> BindInfo -> Bool

(<=) :: BindInfo -> BindInfo -> Bool

(>) :: BindInfo -> BindInfo -> Bool

(>=) :: BindInfo -> BindInfo -> Bool

max :: BindInfo -> BindInfo -> BindInfo

min :: BindInfo -> BindInfo -> BindInfo

Show BindInfo Source # 
Instance details

Defined in CSL.AS_BASIC_CSL

Methods

showsPrec :: Int -> BindInfo -> ShowS

show :: BindInfo -> String

showList :: [BindInfo] -> ShowS

Generic BindInfo 
Instance details

Defined in CSL.ATC_CSL

Associated Types

type Rep BindInfo :: Type -> Type

Methods

from :: BindInfo -> Rep BindInfo x

to :: Rep BindInfo x -> BindInfo

FromJSON BindInfo 
Instance details

Defined in CSL.ATC_CSL

Methods

parseJSON :: Value -> Parser BindInfo

parseJSONList :: Value -> Parser [BindInfo]

ToJSON BindInfo 
Instance details

Defined in CSL.ATC_CSL

Methods

toJSON :: BindInfo -> Value

toEncoding :: BindInfo -> Encoding

toJSONList :: [BindInfo] -> Value

toEncodingList :: [BindInfo] -> Encoding

ShATermConvertible BindInfo 
Instance details

Defined in CSL.ATC_CSL

Methods

toShATermAux :: ATermTable -> BindInfo -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BindInfo] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BindInfo)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BindInfo])

type Rep BindInfo 
Instance details

Defined in CSL.ATC_CSL

type Rep BindInfo = D1 ('MetaData "BindInfo" "CSL.AS_BASIC_CSL" "main" 'False) (C1 ('MetaCons "BindInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "bindingVarPos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]) :*: S1 ('MetaSel ('Just "boundBodyPos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))

operatorInfo :: [OpInfo] Source #

Mapping of operator names to arity-OpInfo-maps (an operator may behave differently for different arities).

operatorInfoMap :: OpInfoMap Source #

opInfoMap for the predefined operatorInfo

operatorInfoNameMap :: OpInfoNameMap Source #

opInfoNameMap for the predefined operatorInfo

mergeOpArityMap :: Ord a => OpInfoArityMap a -> OpInfoArityMap a -> OpInfoArityMap a Source #

Merges two OpInfoArityMaps together with the first map as default map and the second overwriting the default values

getOpInfoMap :: (OpInfo -> String) -> [OpInfo] -> OpInfoMap Source #

Mapping of operator names to arity-OpInfo-maps (an operator may behave differently for different arities).

getOpInfoNameMap :: [OpInfo] -> OpInfoNameMap Source #

Same as operatorInfoMap but with keys of type OPNAME instead of String

getBindInfoMap :: [OpInfo] -> BindInfoMap Source #

a special map for binders which have to be unique for each name (no different arities).

lookupOpInfo Source #

Arguments

:: OpInfoNameMap 
-> OPID

operator id

-> Int

operator arity

-> Either Bool OpInfo 

For the given name and arity we lookup an OpInfo, where arity=-1 means flexible arity. If an operator is registered for the given string but not for the arity we return: Left True.

lookupOpInfoForParsing Source #

Arguments

:: OpInfoMap

map to be used for lookup

-> String

operator name

-> Int

operator arity

-> Either Bool OpInfo 

For the given name and arity we lookup an OpInfo, where arity=-1 means flexible arity. If an operator is registered for the given string but not for the arity we return: Left True. This function is designed for the lookup of operators in not statically analyzed terms. For statically analyzed terms use lookupOpInfo.

lookupBindInfo Source #

Arguments

:: OpInfoNameMap 
-> OPID

operator name

-> Int

operator arity

-> Maybe BindInfo 

For the given name and arity we lookup an BindInfo, where arity=-1 means flexible arity.

type APInt = Integer Source #

type APFloat = Rational Source #

toFraction :: APFloat -> (Integer, Integer) Source #

fromFraction :: Integer -> Integer -> APFloat Source #

type OpInfoMap = OpInfoArityMap String Source #

type OpInfoNameMap = OpInfoArityMap OPNAME Source #

type BindInfoMap = Map String OpInfo Source #

showOPNAME :: OPNAME -> String Source #