Copyright	(c) Dominik Dietrich Ewaryst Schulz DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Ewaryst.Schulz@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

CSL.AS_BASIC_CSL

Description

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

Synopsis

data EXPRESSION
- = Var Token
- | Op OPID [EXTPARAM] [EXPRESSION] Range
- | List [EXPRESSION] Range
- | Interval Double Double Range
- | Int APInt Range
- | Rat APFloat Range
data EXTPARAM = EP Token String APInt
data BASIC_ITEM
- = Op_decl OP_ITEM
- | EP_decl [(Token, EPDomain)]
- | EP_domdecl [(Token, APInt)]
- | EP_defval [(Token, APInt)]
- | Var_decls [VAR_ITEM]
- | Axiom_item (Annoted CMD)
newtype BASIC_SPEC = Basic_spec [Annoted BASIC_ITEM]
data SYMB_ITEMS = Symb_items [SYMB] Range
newtype SYMB = Symb_id Token
data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Range
data SYMB_OR_MAP
- = Symb SYMB
- | Symb_map SYMB SYMB Range
data OPNAME
- = OP_mult
- | OP_div
- | OP_plus
- | OP_minus
- | OP_neg
- | OP_pow
- | OP_fthrt
- | OP_sqrt
- | OP_abs
- | OP_max
- | OP_min
- | OP_sign
- | OP_cos
- | OP_sin
- | OP_tan
- | OP_cot
- | OP_Pi
- | OP_reldist
- | OP_minimize
- | OP_minloc
- | OP_maximize
- | OP_maxloc
- | OP_factor
- | OP_approx
- | OP_divide
- | OP_factorize
- | OP_int
- | OP_rlqe
- | OP_simplify
- | OP_solve
- | OP_neq
- | OP_lt
- | OP_leq
- | OP_eq
- | OP_gt
- | OP_geq
- | OP_convergence
- | OP_reldistLe
- | OP_in
- | OP_undef
- | OP_failure
- | OP_false
- | OP_true
- | OP_not
- | OP_and
- | OP_or
- | OP_impl
- | OP_ex
- | OP_all
- | OP_hastype
- | OP_real
data OPID
- = OpId OPNAME
- | OpUser ConstantName
data ConstantName
- = SimpleConstant String
- | ElimConstant String Int
data OP_ITEM = Op_item [Token] Range
data VAR_ITEM = Var_item [Token] Domain Range
data VarDecl = VarDecl Token (Maybe Domain)
data OpDecl = OpDecl ConstantName [EXTPARAM] [VarDecl] Range
data EPDecl = EPDecl Token EPDomain (Maybe APInt)
data EPVal
- = EPVal APInt
- | EPConstRef Token
getEPVarRef :: EPVal -> Maybe Token
type Domain = SetOrInterval GroundConstant
type EPDomain = ClosedInterval EPVal
data GroundConstant
- = GCI APInt
- | GCR APFloat
cmpFloatToInt :: APFloat -> APInt -> Ordering
data AssDefinition
- = ConstDef EXPRESSION
- | FunDef [String] EXPRESSION
data InstantiatedConstant = InstantiatedConstant {
- constName :: ConstantName
- instantiation :: [EXPRESSION]
}
data CMD
- = Ass OpDecl EXPRESSION
- | Cmd String [EXPRESSION]
- | Sequence [CMD]
- | Cond [(EXPRESSION, [CMD])]
- | Repeat EXPRESSION [CMD]
class OperatorState a where
- addVar :: a -> String -> a
- isVar :: a -> String -> Bool
- lookupOperator :: a -> String -> Int -> Either Bool OpInfo
- lookupBinder :: a -> String -> Maybe OpInfo
data OpInfo = OpInfo {
- prec :: Int
- infx :: Bool
- arity :: Int
- foldNAry :: Bool
- opname :: OPNAME
- bind :: Maybe BindInfo
}
data BindInfo = BindInfo {
- bindingVarPos :: [Int]
- boundBodyPos :: [Int]
}
operatorInfo :: [OpInfo]
operatorInfoMap :: OpInfoMap
operatorInfoNameMap :: OpInfoNameMap
operatorBindInfoMap :: BindInfoMap
mergeOpArityMap :: Ord a => OpInfoArityMap a -> OpInfoArityMap a -> OpInfoArityMap a
getOpInfoMap :: (OpInfo -> String) -> [OpInfo] -> OpInfoMap
getOpInfoNameMap :: [OpInfo] -> OpInfoNameMap
getBindInfoMap :: [OpInfo] -> BindInfoMap
lookupOpInfo :: OpInfoNameMap -> OPID -> Int -> Either Bool OpInfo
lookupOpInfoForParsing :: OpInfoMap -> String -> Int -> Either Bool OpInfo
lookupBindInfo :: OpInfoNameMap -> OPID -> Int -> Maybe BindInfo
type APInt = Integer
type APFloat = Rational
toFraction :: APFloat -> (Integer, Integer)
fromFraction :: Integer -> Integer -> APFloat
type OpInfoMap = OpInfoArityMap String
type OpInfoNameMap = OpInfoArityMap OPNAME
type BindInfoMap = Map String OpInfo
showOPNAME :: OPNAME -> String
maxPrecedence :: Int

Documentation

data EXPRESSION Source #

Datatype for expressions

Constructors

Var Token
Op OPID [EXTPARAM] [EXPRESSION] Range
List [EXPRESSION] Range
Interval Double Double Range
Int APInt Range
Rat APFloat Range

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 Methods compare :: EXPRESSION -> EXPRESSION -> Ordering (<) :: EXPRESSION -> EXPRESSION -> Bool (<=) :: EXPRESSION -> EXPRESSION -> Bool (>) :: EXPRESSION -> EXPRESSION -> Bool (>=) :: EXPRESSION -> EXPRESSION -> Bool max :: EXPRESSION -> EXPRESSION -> EXPRESSION min :: EXPRESSION -> EXPRESSION -> EXPRESSION
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 Methods getRange :: EXPRESSION -> Range Source # rangeSpan :: EXPRESSION -> [Pos] Source #
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 Methods pretty :: EXPRESSION -> Doc Source # pretties :: [EXPRESSION] -> Doc 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 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 Methods pretty :: EXTPARAM -> Doc Source # pretties :: [EXTPARAM] -> Doc Source #
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

Constructors

Op_decl OP_ITEM
EP_decl [(Token, EPDomain)]
EP_domdecl [(Token, APInt)]
EP_defval [(Token, APInt)]
Var_decls [VAR_ITEM]
Axiom_item (Annoted CMD)

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 Methods getRange :: BASIC_ITEM -> Range Source # rangeSpan :: BASIC_ITEM -> [Pos] Source #
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 Methods pretty :: BASIC_ITEM -> Doc Source # pretties :: [BASIC_ITEM] -> Doc Source #
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 Methods mempty :: BASIC_SPEC mappend :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC mconcat :: [BASIC_SPEC] -> BASIC_SPEC
GetRange BASIC_SPEC Source #
Instance details Defined in CSL.Print_AS Methods getRange :: BASIC_SPEC -> Range Source # rangeSpan :: BASIC_SPEC -> [Pos] Source #
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 Methods pretty :: BASIC_SPEC -> Doc Source # pretties :: [BASIC_SPEC] -> Doc Source #
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #	Syntax of CSL logic
Instance details Defined in CSL.Logic_CSL Methods parsersAndPrinters :: CSL -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CSL -> BASIC_SPEC -> Item Source # symb_items_name :: CSL -> SYMB_ITEMS -> [String] Source #
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 Methods getRange :: SYMB_ITEMS -> Range Source # rangeSpan :: SYMB_ITEMS -> [Pos] Source #
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 Methods pretty :: SYMB_ITEMS -> Doc Source # pretties :: [SYMB_ITEMS] -> Doc Source #
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #	Syntax of CSL logic
Instance details Defined in CSL.Logic_CSL Methods parsersAndPrinters :: CSL -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CSL -> BASIC_SPEC -> Item Source # symb_items_name :: CSL -> SYMB_ITEMS -> [String] Source #
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 Methods getRange :: SYMB -> Range Source # rangeSpan :: SYMB -> [Pos] Source #
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

Constructors

Symb_map_items [SYMB_OR_MAP] Range

Instances

Instances details

Eq SYMB_MAP_ITEMS Source #
Instance details Defined in CSL.AS_BASIC_CSL Methods (==) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool (/=) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
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 Methods from :: SYMB_MAP_ITEMS -> Rep SYMB_MAP_ITEMS x to :: Rep SYMB_MAP_ITEMS x -> SYMB_MAP_ITEMS
GetRange SYMB_MAP_ITEMS Source #
Instance details Defined in CSL.Print_AS Methods getRange :: SYMB_MAP_ITEMS -> Range Source # rangeSpan :: SYMB_MAP_ITEMS -> [Pos] Source #
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 Methods pretty :: SYMB_MAP_ITEMS -> Doc Source # pretties :: [SYMB_MAP_ITEMS] -> Doc Source #
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #	Syntax of CSL logic
Instance details Defined in CSL.Logic_CSL Methods parsersAndPrinters :: CSL -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CSL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: CSL -> BASIC_SPEC -> Item Source # symb_items_name :: CSL -> SYMB_ITEMS -> [String] Source #
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 Methods getRange :: SYMB_OR_MAP -> Range Source # rangeSpan :: SYMB_OR_MAP -> [Pos] Source #
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 Methods pretty :: SYMB_OR_MAP -> Doc Source # pretties :: [SYMB_OR_MAP] -> Doc Source #
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 Methods getOINM :: Reader OpInfoNameMap OpInfoNameMap Source # printConstant :: ConstantName -> Reader OpInfoNameMap Doc Source # printOpname :: OPNAME -> Reader OpInfoNameMap Doc Source # prefixMode :: Reader OpInfoNameMap Bool Source # printArgs :: [Doc] -> Reader OpInfoNameMap Doc Source # printArgPattern :: String -> Reader OpInfoNameMap Doc Source # printInterval :: Double -> Double -> Reader OpInfoNameMap Doc Source # printRational :: APFloat -> Reader OpInfoNameMap Doc Source #
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 #

Constructors

OpId OPNAME
OpUser ConstantName

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 Methods compare :: ConstantName -> ConstantName -> Ordering (<) :: ConstantName -> ConstantName -> Bool (<=) :: ConstantName -> ConstantName -> Bool (>) :: ConstantName -> ConstantName -> Bool (>=) :: ConstantName -> ConstantName -> Bool max :: ConstantName -> ConstantName -> ConstantName min :: ConstantName -> ConstantName -> ConstantName
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 Methods from :: ConstantName -> Rep ConstantName x to :: Rep ConstantName x -> ConstantName
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 Methods pretty :: ConstantName -> Doc Source # pretties :: [ConstantName] -> Doc Source #
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 Methods getRange :: OP_ITEM -> Range Source # rangeSpan :: OP_ITEM -> [Pos] Source #
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 Methods pretty :: OP_ITEM -> Doc Source # pretties :: [OP_ITEM] -> Doc Source #
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 Methods getRange :: VAR_ITEM -> Range Source # rangeSpan :: VAR_ITEM -> [Pos] Source #
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 Methods pretty :: VAR_ITEM -> Doc Source # pretties :: [VAR_ITEM] -> Doc Source #
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 Methods pretty :: VarDecl -> Doc Source # pretties :: [VarDecl] -> Doc Source #
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 #

Constructors

OpDecl ConstantName [EXTPARAM] [VarDecl] Range

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 Methods pretty :: OpDecl -> Doc Source # pretties :: [OpDecl] -> Doc Source #
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 Methods pretty :: EPDecl -> Doc Source # pretties :: [EPDecl] -> Doc Source #
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 Methods pretty :: EPVal -> Doc Source # pretties :: [EPVal] -> Doc Source #
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)))

getEPVarRef :: EPVal -> Maybe Token Source #

type Domain = SetOrInterval GroundConstant Source #

type EPDomain = ClosedInterval EPVal Source #

data GroundConstant Source #

Constructors

GCI APInt
GCR APFloat

Instances

Instances details

Eq GroundConstant Source #
Instance details Defined in CSL.AS_BASIC_CSL Methods (==) :: GroundConstant -> GroundConstant -> Bool (/=) :: GroundConstant -> GroundConstant -> Bool
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 Methods compare :: GroundConstant -> GroundConstant -> Ordering (<) :: GroundConstant -> GroundConstant -> Bool (<=) :: GroundConstant -> GroundConstant -> Bool (>) :: GroundConstant -> GroundConstant -> Bool (>=) :: GroundConstant -> GroundConstant -> Bool max :: GroundConstant -> GroundConstant -> GroundConstant min :: GroundConstant -> GroundConstant -> GroundConstant
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 Methods from :: GroundConstant -> Rep GroundConstant x to :: Rep GroundConstant x -> GroundConstant
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 Methods pretty :: GroundConstant -> Doc Source # pretties :: [GroundConstant] -> Doc Source #
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 Methods (==) :: AssDefinition -> AssDefinition -> Bool (/=) :: AssDefinition -> AssDefinition -> Bool
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 Methods compare :: AssDefinition -> AssDefinition -> Ordering (<) :: AssDefinition -> AssDefinition -> Bool (<=) :: AssDefinition -> AssDefinition -> Bool (>) :: AssDefinition -> AssDefinition -> Bool (>=) :: AssDefinition -> AssDefinition -> Bool max :: AssDefinition -> AssDefinition -> AssDefinition min :: AssDefinition -> AssDefinition -> AssDefinition
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 Methods from :: AssDefinition -> Rep AssDefinition x to :: Rep AssDefinition x -> AssDefinition
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 Methods pretty :: AssDefinition -> Doc Source # pretties :: [AssDefinition] -> Doc Source #
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 #

Constructors

InstantiatedConstant
Fields constName :: ConstantName instantiation :: [EXPRESSION]

Instances

Instances details

Eq InstantiatedConstant Source #
Instance details Defined in CSL.AS_BASIC_CSL Methods (==) :: InstantiatedConstant -> InstantiatedConstant -> Bool (/=) :: InstantiatedConstant -> InstantiatedConstant -> Bool
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 Methods compare :: InstantiatedConstant -> InstantiatedConstant -> Ordering (<) :: InstantiatedConstant -> InstantiatedConstant -> Bool (<=) :: InstantiatedConstant -> InstantiatedConstant -> Bool (>) :: InstantiatedConstant -> InstantiatedConstant -> Bool (>=) :: InstantiatedConstant -> InstantiatedConstant -> Bool max :: InstantiatedConstant -> InstantiatedConstant -> InstantiatedConstant min :: InstantiatedConstant -> InstantiatedConstant -> InstantiatedConstant
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 Methods from :: InstantiatedConstant -> Rep InstantiatedConstant x to :: Rep InstantiatedConstant x -> InstantiatedConstant
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 Methods toJSON :: InstantiatedConstant -> Value toEncoding :: InstantiatedConstant -> Encoding toJSONList :: [InstantiatedConstant] -> Value toEncodingList :: [InstantiatedConstant] -> Encoding
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 Methods pretty :: InstantiatedConstant -> Doc Source # pretties :: [InstantiatedConstant] -> Doc Source #
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 #

Constructors

Ass OpDecl EXPRESSION
Cmd String [EXPRESSION]
Sequence [CMD]
Cond [(EXPRESSION, [CMD])]
Repeat EXPRESSION [CMD]

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 Methods getRange :: CMD -> Range Source # rangeSpan :: CMD -> [Pos] Source #
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 Methods map_sen :: CSL -> Morphism -> CMD -> Result CMD Source # simplify_sen :: CSL -> Sign -> CMD -> CMD Source # negation :: CSL -> CMD -> Maybe CMD Source # print_sign :: CSL -> Sign -> Doc Source # print_named :: CSL -> Named CMD -> Doc Source # sym_of :: CSL -> Sign -> [Set Symbol] Source # mostSymsOf :: CSL -> Sign -> [Symbol] Source # symmap_of :: CSL -> Morphism -> EndoMap Symbol Source # sym_name :: CSL -> Symbol -> Id Source # sym_label :: CSL -> Symbol -> Maybe String Source # fullSymName :: CSL -> Symbol -> String Source # symKind :: CSL -> Symbol -> String Source # symsOfSen :: CSL -> Sign -> CMD -> [Symbol] Source # pair_symbols :: CSL -> Symbol -> Symbol -> Result Symbol Source #
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 Methods getOINM :: Reader OpInfoNameMap OpInfoNameMap Source # printConstant :: ConstantName -> Reader OpInfoNameMap Doc Source # printOpname :: OPNAME -> Reader OpInfoNameMap Doc Source # prefixMode :: Reader OpInfoNameMap Bool Source # printArgs :: [Doc] -> Reader OpInfoNameMap Doc Source # printArgPattern :: String -> Reader OpInfoNameMap Doc Source # printInterval :: Double -> Double -> Reader OpInfoNameMap Doc Source # printRational :: APFloat -> Reader OpInfoNameMap Doc 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 #
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 bindingVarPos :: [Int] argument positions of binding variables boundBodyPos :: [Int] argument positions of bound terms

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

operatorBindInfoMap :: BindInfoMap Source #

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 #

maxPrecedence :: Int Source #

OP_mult
OP_div
OP_plus
OP_minus
OP_neg
OP_pow
OP_fthrt
OP_sqrt
OP_abs
OP_max
OP_min
OP_sign
OP_cos
OP_sin
OP_tan
OP_cot
OP_Pi
OP_reldist
OP_minimize
OP_minloc
OP_maximize
OP_maxloc
OP_factor
OP_approx
OP_divide
OP_factorize
OP_int
OP_rlqe
OP_simplify
OP_solve
OP_neq
OP_lt
OP_leq
OP_eq
OP_gt
OP_geq
OP_convergence
OP_reldistLe
OP_in
OP_undef
OP_failure
OP_false
OP_true
OP_not
OP_and
OP_or
OP_impl
OP_ex
OP_all
OP_hastype
OP_real