| Copyright | (c) Klaus Luettich Christian Maeder Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
CASL.AS_Basic_CASL
Description
Abstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.
Follows Sect. II:2.2 of the CASL Reference Manual.
Synopsis
- data BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
- data BASIC_ITEMS b s f
- = Sig_items (SIG_ITEMS s f)
- | Free_datatype SortsKind [Annoted DATATYPE_DECL] Range
- | Sort_gen [Annoted (SIG_ITEMS s f)] Range
- | Var_items [VAR_DECL] Range
- | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
- | Axiom_items [Annoted (FORMULA f)] Range
- | Ext_BASIC_ITEMS b
- data SortsKind
- data SIG_ITEMS s f
- = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
- | Op_items [Annoted (OP_ITEM f)] Range
- | Pred_items [Annoted (PRED_ITEM f)] Range
- | Datatype_items SortsKind [Annoted DATATYPE_DECL] Range
- | Ext_SIG_ITEMS s
- data SORT_ITEM f
- data OP_ITEM f
- data OpKind
- data OP_TYPE = Op_type OpKind [SORT] SORT Range
- args_OP_TYPE :: OP_TYPE -> [SORT]
- res_OP_TYPE :: OP_TYPE -> SORT
- data OP_HEAD = Op_head OpKind [VAR_DECL] (Maybe SORT) Range
- data OP_ATTR f
- data PRED_ITEM f
- data PRED_TYPE = Pred_type [SORT] Range
- data PRED_HEAD = Pred_head [VAR_DECL] Range
- data DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range
- data ALTERNATIVE
- data COMPONENTS
- data VAR_DECL = Var_decl [VAR] SORT Range
- varDeclRange :: VAR_DECL -> [Pos]
- data Junctor
- dualJunctor :: Junctor -> Junctor
- data Relation
- data Equality
- data FORMULA f
- = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range
- | Junction Junctor [FORMULA f] Range
- | Relation (FORMULA f) Relation (FORMULA f) Range
- | Negation (FORMULA f) Range
- | Atom Bool Range
- | Predication PRED_SYMB [TERM f] Range
- | Definedness (TERM f) Range
- | Equation (TERM f) Equality (TERM f) Range
- | Membership (TERM f) SORT Range
- | Mixfix_formula (TERM f)
- | Unparsed_formula String Range
- | Sort_gen_ax [Constraint] Bool
- | QuantOp OP_NAME OP_TYPE (FORMULA f)
- | QuantPred PRED_NAME PRED_TYPE (FORMULA f)
- | ExtFORMULA f
- mkSort_gen_ax :: [Constraint] -> Bool -> FORMULA f
- is_True_atom :: FORMULA f -> Bool
- is_False_atom :: FORMULA f -> Bool
- boolForm :: Bool -> FORMULA f
- trueForm :: FORMULA f
- falseForm :: FORMULA f
- data Constraint = Constraint {}
- sortConstraints :: [Constraint] -> [Constraint]
- isInjectiveList :: Ord a => [a] -> Bool
- recover_Sort_gen_ax :: [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
- recoverSortGen :: [Constraint] -> [(SORT, [OP_SYMB])]
- recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])]
- isSortGen :: FORMULA f -> Bool
- data QUANTIFIER
- data PRED_SYMB
- predSymbName :: PRED_SYMB -> PRED_NAME
- data TERM f
- = Qual_var VAR SORT Range
- | Application OP_SYMB [TERM f] Range
- | Sorted_term (TERM f) SORT Range
- | Cast (TERM f) SORT Range
- | Conditional (TERM f) (FORMULA f) (TERM f) Range
- | Unparsed_term String Range
- | Mixfix_qual_pred PRED_SYMB
- | Mixfix_term [TERM f]
- | Mixfix_token Token
- | Mixfix_sorted_term SORT Range
- | Mixfix_cast SORT Range
- | Mixfix_parenthesized [TERM f] Range
- | Mixfix_bracketed [TERM f] Range
- | Mixfix_braced [TERM f] Range
- | ExtTERM f
- varOrConst :: Token -> TERM f
- data OP_SYMB
- opSymbName :: OP_SYMB -> OP_NAME
- mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
- mkForall :: [VAR_DECL] -> FORMULA f -> FORMULA f
- mkExist :: [VAR_DECL] -> FORMULA f -> FORMULA f
- toQualVar :: VAR_DECL -> TERM f
- mkRel :: Relation -> FORMULA f -> FORMULA f -> FORMULA f
- mkImpl :: FORMULA f -> FORMULA f -> FORMULA f
- mkAnyEq :: Equality -> TERM f -> TERM f -> FORMULA f
- mkExEq :: TERM f -> TERM f -> FORMULA f
- mkStEq :: TERM f -> TERM f -> FORMULA f
- mkEqv :: FORMULA f -> FORMULA f -> FORMULA f
- mkAppl :: OP_SYMB -> [TERM f] -> TERM f
- mkPredication :: PRED_SYMB -> [TERM f] -> FORMULA f
- mkVarDecl :: VAR -> SORT -> VAR_DECL
- mkVarTerm :: VAR -> SORT -> TERM f
- conjunctRange :: [FORMULA f] -> Range -> FORMULA f
- conjunct :: [FORMULA f] -> FORMULA f
- disjunctRange :: [FORMULA f] -> Range -> FORMULA f
- disjunct :: [FORMULA f] -> FORMULA f
- mkQualOp :: OP_NAME -> OP_TYPE -> OP_SYMB
- mkQualPred :: PRED_NAME -> PRED_TYPE -> PRED_SYMB
- negateForm :: FORMULA f -> Range -> FORMULA f
- mkNeg :: FORMULA f -> FORMULA f
- mkVarDeclStr :: String -> SORT -> VAR_DECL
- type CASLFORMULA = FORMULA ()
- type CASLTERM = TERM ()
- type OP_NAME = Id
- type PRED_NAME = Id
- type SORT = Id
- type VAR = Token
- data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] Range
- symbItemsName :: SYMB_ITEMS -> [String]
- data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range
- data SYMB_KIND
- data SYMB
- data TYPE
- data SYMB_OR_MAP
Documentation
data BASIC_SPEC b s f Source #
Constructors
| Basic_spec [Annoted (BASIC_ITEMS b s f)] |
Instances
data BASIC_ITEMS b s f Source #
Constructors
| Sig_items (SIG_ITEMS s f) | |
| Free_datatype SortsKind [Annoted DATATYPE_DECL] Range | |
| Sort_gen [Annoted (SIG_ITEMS s f)] Range | |
| Var_items [VAR_DECL] Range | |
| Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range | |
| Axiom_items [Annoted (FORMULA f)] Range | |
| Ext_BASIC_ITEMS b |
Instances
| (Data b, Data s, Data f) => Data (BASIC_ITEMS b s f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> BASIC_ITEMS b s f -> c (BASIC_ITEMS b s f) gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BASIC_ITEMS b s f) toConstr :: BASIC_ITEMS b s f -> Constr dataTypeOf :: BASIC_ITEMS b s f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (BASIC_ITEMS b s f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BASIC_ITEMS b s f)) gmapT :: (forall b0. Data b0 => b0 -> b0) -> BASIC_ITEMS b s f -> BASIC_ITEMS b s f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS b s f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS b s f -> r gmapQ :: (forall d. Data d => d -> u) -> BASIC_ITEMS b s f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_ITEMS b s f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS b s f -> m (BASIC_ITEMS b s f) | |
| (Show s, Show f, Show b) => Show (BASIC_ITEMS b s f) Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> BASIC_ITEMS b s f -> ShowS show :: BASIC_ITEMS b s f -> String showList :: [BASIC_ITEMS b s f] -> ShowS | |
| Generic (BASIC_ITEMS b s f) | |
Defined in CASL.ATC_CASL Associated Types type Rep (BASIC_ITEMS b s f) :: Type -> Type Methods from :: BASIC_ITEMS b s f -> Rep (BASIC_ITEMS b s f) x to :: Rep (BASIC_ITEMS b s f) x -> BASIC_ITEMS b s f | |
| (GetRange b, GetRange s, GetRange f) => GetRange (BASIC_ITEMS b s f) Source # | |
Defined in CASL.AS_Basic_CASL Methods getRange :: BASIC_ITEMS b s f -> Range Source # rangeSpan :: BASIC_ITEMS b s f -> [Pos] Source # | |
| (FromJSON b, FromJSON s, FromJSON f) => FromJSON (BASIC_ITEMS b s f) | |
Defined in CASL.ATC_CASL Methods parseJSON :: Value -> Parser (BASIC_ITEMS b s f) parseJSONList :: Value -> Parser [BASIC_ITEMS b s f] | |
| (ToJSON b, ToJSON s, ToJSON f) => ToJSON (BASIC_ITEMS b s f) | |
Defined in CASL.ATC_CASL Methods toJSON :: BASIC_ITEMS b s f -> Value toEncoding :: BASIC_ITEMS b s f -> Encoding toJSONList :: [BASIC_ITEMS b s f] -> Value toEncodingList :: [BASIC_ITEMS b s f] -> Encoding | |
| (ShATermConvertible b, ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (BASIC_ITEMS b s f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> BASIC_ITEMS b s f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BASIC_ITEMS b s f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEMS b s f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_ITEMS b s f]) | |
| (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f) Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML (BASIC_ITEMS a b c) Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> BASIC_ITEMS a b c from_sml_ShATermList :: ATermTable -> [BASIC_ITEMS a b c] | |
| type Rep (BASIC_ITEMS b s f) | |
Defined in CASL.ATC_CASL type Rep (BASIC_ITEMS b s f) = D1 ('MetaData "BASIC_ITEMS" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Sig_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SIG_ITEMS s f))) :+: (C1 ('MetaCons "Free_datatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortsKind) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted DATATYPE_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Sort_gen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (SIG_ITEMS s f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "Var_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Local_var_axioms" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Axiom_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (FORMULA f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Ext_BASIC_ITEMS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b))))) | |
Constructors
| NonEmptySorts | |
| PossiblyEmptySorts |
Instances
| Data SortsKind Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SortsKind -> c SortsKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SortsKind toConstr :: SortsKind -> Constr dataTypeOf :: SortsKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SortsKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortsKind) gmapT :: (forall b. Data b => b -> b) -> SortsKind -> SortsKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SortsKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SortsKind -> r gmapQ :: (forall d. Data d => d -> u) -> SortsKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SortsKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SortsKind -> m SortsKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SortsKind -> m SortsKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SortsKind -> m SortsKind | |
| Show SortsKind Source # | |
| Generic SortsKind | |
| GetRange SortsKind Source # | |
| FromJSON SortsKind | |
Defined in CASL.ATC_CASL | |
| ToJSON SortsKind | |
Defined in CASL.ATC_CASL Methods toEncoding :: SortsKind -> Encoding toJSONList :: [SortsKind] -> Value toEncodingList :: [SortsKind] -> Encoding | |
| ShATermConvertible SortsKind | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> SortsKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SortsKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SortsKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SortsKind]) | |
| type Rep SortsKind | |
Defined in CASL.ATC_CASL type Rep SortsKind = D1 ('MetaData "SortsKind" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "NonEmptySorts" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PossiblyEmptySorts" 'PrefixI 'False) (U1 :: Type -> Type)) | |
Constructors
| Sort_items SortsKind [Annoted (SORT_ITEM f)] Range | |
| Op_items [Annoted (OP_ITEM f)] Range | |
| Pred_items [Annoted (PRED_ITEM f)] Range | |
| Datatype_items SortsKind [Annoted DATATYPE_DECL] Range | |
| Ext_SIG_ITEMS s |
Instances
| (Data s, Data f) => Data (SIG_ITEMS s f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SIG_ITEMS s f -> c (SIG_ITEMS s f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SIG_ITEMS s f) toConstr :: SIG_ITEMS s f -> Constr dataTypeOf :: SIG_ITEMS s f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SIG_ITEMS s f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SIG_ITEMS s f)) gmapT :: (forall b. Data b => b -> b) -> SIG_ITEMS s f -> SIG_ITEMS s f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SIG_ITEMS s f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SIG_ITEMS s f -> r gmapQ :: (forall d. Data d => d -> u) -> SIG_ITEMS s f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SIG_ITEMS s f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SIG_ITEMS s f -> m (SIG_ITEMS s f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SIG_ITEMS s f -> m (SIG_ITEMS s f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SIG_ITEMS s f -> m (SIG_ITEMS s f) | |
| (Show f, Show s) => Show (SIG_ITEMS s f) Source # | |
| Generic (SIG_ITEMS s f) | |
| (GetRange s, GetRange f) => GetRange (SIG_ITEMS s f) Source # | |
| (FromJSON s, FromJSON f) => FromJSON (SIG_ITEMS s f) | |
Defined in CASL.ATC_CASL | |
| (ToJSON s, ToJSON f) => ToJSON (SIG_ITEMS s f) | |
Defined in CASL.ATC_CASL Methods toJSON :: SIG_ITEMS s f -> Value toEncoding :: SIG_ITEMS s f -> Encoding toJSONList :: [SIG_ITEMS s f] -> Value toEncodingList :: [SIG_ITEMS s f] -> Encoding | |
| (ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (SIG_ITEMS s f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> SIG_ITEMS s f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SIG_ITEMS s f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SIG_ITEMS s f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SIG_ITEMS s f]) | |
| (Pretty s, FormExtension f) => Pretty (SIG_ITEMS s f) Source # | |
| ATermConvertibleSML (SIG_ITEMS a b) Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> SIG_ITEMS a b from_sml_ShATermList :: ATermTable -> [SIG_ITEMS a b] | |
| type Rep (SIG_ITEMS s f) | |
Defined in CASL.ATC_CASL type Rep (SIG_ITEMS s f) = D1 ('MetaData "SIG_ITEMS" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Sort_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortsKind) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (SORT_ITEM f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Op_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (OP_ITEM f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Pred_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (PRED_ITEM f)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "Datatype_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortsKind) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted DATATYPE_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Ext_SIG_ITEMS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s))))) | |
Constructors
| Sort_decl [SORT] Range | |
| Subsort_decl [SORT] SORT Range | |
| Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range | |
| Iso_decl [SORT] Range |
Instances
| Data f => Data (SORT_ITEM f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SORT_ITEM f -> c (SORT_ITEM f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SORT_ITEM f) toConstr :: SORT_ITEM f -> Constr dataTypeOf :: SORT_ITEM f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SORT_ITEM f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SORT_ITEM f)) gmapT :: (forall b. Data b => b -> b) -> SORT_ITEM f -> SORT_ITEM f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SORT_ITEM f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SORT_ITEM f -> r gmapQ :: (forall d. Data d => d -> u) -> SORT_ITEM f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SORT_ITEM f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SORT_ITEM f -> m (SORT_ITEM f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SORT_ITEM f -> m (SORT_ITEM f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SORT_ITEM f -> m (SORT_ITEM f) | |
| Show f => Show (SORT_ITEM f) Source # | |
| Generic (SORT_ITEM f) | |
| GetRange f => GetRange (SORT_ITEM f) Source # | |
| FromJSON f => FromJSON (SORT_ITEM f) | |
Defined in CASL.ATC_CASL | |
| ToJSON f => ToJSON (SORT_ITEM f) | |
Defined in CASL.ATC_CASL Methods toJSON :: SORT_ITEM f -> Value toEncoding :: SORT_ITEM f -> Encoding toJSONList :: [SORT_ITEM f] -> Value toEncodingList :: [SORT_ITEM f] -> Encoding | |
| ShATermConvertible f => ShATermConvertible (SORT_ITEM f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> SORT_ITEM f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SORT_ITEM f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SORT_ITEM f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SORT_ITEM f]) | |
| FormExtension f => Pretty (SORT_ITEM f) Source # | |
| ListCheck (SORT_ITEM f) Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML (SORT_ITEM a) Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> SORT_ITEM a from_sml_ShATermList :: ATermTable -> [SORT_ITEM a] | |
| type Rep (SORT_ITEM f) | |
Defined in CASL.ATC_CASL type Rep (SORT_ITEM f) = D1 ('MetaData "SORT_ITEM" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Sort_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Subsort_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Subsort_defn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VAR)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Annoted (FORMULA f))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: C1 ('MetaCons "Iso_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
Constructors
| Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range | |
| Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range |
Instances
| Data f => Data (OP_ITEM f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OP_ITEM f -> c (OP_ITEM f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OP_ITEM f) toConstr :: OP_ITEM f -> Constr dataTypeOf :: OP_ITEM f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OP_ITEM f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (OP_ITEM f)) gmapT :: (forall b. Data b => b -> b) -> OP_ITEM f -> OP_ITEM f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OP_ITEM f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OP_ITEM f -> r gmapQ :: (forall d. Data d => d -> u) -> OP_ITEM f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OP_ITEM f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OP_ITEM f -> m (OP_ITEM f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_ITEM f -> m (OP_ITEM f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_ITEM f -> m (OP_ITEM f) | |
| Show f => Show (OP_ITEM f) Source # | |
| Generic (OP_ITEM f) | |
| GetRange f => GetRange (OP_ITEM f) Source # | |
| FromJSON f => FromJSON (OP_ITEM f) | |
Defined in CASL.ATC_CASL | |
| ToJSON f => ToJSON (OP_ITEM f) | |
Defined in CASL.ATC_CASL Methods toEncoding :: OP_ITEM f -> Encoding toJSONList :: [OP_ITEM f] -> Value toEncodingList :: [OP_ITEM f] -> Encoding | |
| ShATermConvertible f => ShATermConvertible (OP_ITEM f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> OP_ITEM f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OP_ITEM f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_ITEM f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OP_ITEM f]) | |
| FormExtension f => Pretty (OP_ITEM f) Source # | |
| ListCheck (OP_ITEM f) Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML (OP_ITEM a) Source # | |
Defined in ATC.Sml_cats | |
| type Rep (OP_ITEM f) | |
Defined in CASL.ATC_CASL type Rep (OP_ITEM f) = D1 ('MetaData "OP_ITEM" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Op_decl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OP_NAME]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_TYPE)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OP_ATTR f]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Op_defn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_NAME) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_HEAD)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Annoted (TERM f))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
Instances
| Eq OpKind Source # | |
| Data OpKind Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpKind -> c OpKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpKind dataTypeOf :: OpKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpKind) gmapT :: (forall b. Data b => b -> b) -> OpKind -> OpKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpKind -> r gmapQ :: (forall d. Data d => d -> u) -> OpKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpKind -> m OpKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpKind -> m OpKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpKind -> m OpKind | |
| Ord OpKind Source # | |
| Show OpKind Source # | |
| Generic OpKind | |
| GetRange OpKind Source # | |
| FromJSON OpKind | |
Defined in CASL.ATC_CASL | |
| ToJSON OpKind | |
Defined in CASL.ATC_CASL Methods toEncoding :: OpKind -> Encoding toJSONList :: [OpKind] -> Value toEncodingList :: [OpKind] -> Encoding | |
| ShATermConvertible OpKind | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> OpKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OpKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OpKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpKind]) | |
| type Rep OpKind | |
Defined in CASL.ATC_CASL type Rep OpKind = D1 ('MetaData "OpKind" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Total" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Partial" 'PrefixI 'False) (U1 :: Type -> Type)) | |
Instances
| Eq OP_TYPE Source # | |
| Data OP_TYPE Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OP_TYPE -> c OP_TYPE gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OP_TYPE dataTypeOf :: OP_TYPE -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OP_TYPE) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OP_TYPE) gmapT :: (forall b. Data b => b -> b) -> OP_TYPE -> OP_TYPE gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OP_TYPE -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OP_TYPE -> r gmapQ :: (forall d. Data d => d -> u) -> OP_TYPE -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OP_TYPE -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OP_TYPE -> m OP_TYPE gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_TYPE -> m OP_TYPE gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_TYPE -> m OP_TYPE | |
| Ord OP_TYPE Source # | |
| Show OP_TYPE Source # | |
| Generic OP_TYPE | |
| GetRange OP_TYPE Source # | |
| FromJSON OP_TYPE | |
Defined in CASL.ATC_CASL | |
| ToJSON OP_TYPE | |
Defined in CASL.ATC_CASL Methods toEncoding :: OP_TYPE -> Encoding toJSONList :: [OP_TYPE] -> Value toEncodingList :: [OP_TYPE] -> Encoding | |
| ShATermConvertible OP_TYPE | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> OP_TYPE -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OP_TYPE] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_TYPE) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OP_TYPE]) | |
| Pretty OP_TYPE Source # | |
| ATermConvertibleSML OP_TYPE Source # | |
Defined in ATC.Sml_cats | |
| type Rep OP_TYPE | |
Defined in CASL.ATC_CASL type Rep OP_TYPE = D1 ('MetaData "OP_TYPE" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Op_type" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
args_OP_TYPE :: OP_TYPE -> [SORT] Source #
res_OP_TYPE :: OP_TYPE -> SORT Source #
Instances
| Eq OP_HEAD Source # | |
| Data OP_HEAD Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OP_HEAD -> c OP_HEAD gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OP_HEAD dataTypeOf :: OP_HEAD -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OP_HEAD) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OP_HEAD) gmapT :: (forall b. Data b => b -> b) -> OP_HEAD -> OP_HEAD gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OP_HEAD -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OP_HEAD -> r gmapQ :: (forall d. Data d => d -> u) -> OP_HEAD -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OP_HEAD -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OP_HEAD -> m OP_HEAD gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_HEAD -> m OP_HEAD gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_HEAD -> m OP_HEAD | |
| Ord OP_HEAD Source # | |
| Show OP_HEAD Source # | |
| Generic OP_HEAD | |
| GetRange OP_HEAD Source # | |
| FromJSON OP_HEAD | |
Defined in CASL.ATC_CASL | |
| ToJSON OP_HEAD | |
Defined in CASL.ATC_CASL Methods toEncoding :: OP_HEAD -> Encoding toJSONList :: [OP_HEAD] -> Value toEncodingList :: [OP_HEAD] -> Encoding | |
| ShATermConvertible OP_HEAD | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> OP_HEAD -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OP_HEAD] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_HEAD) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OP_HEAD]) | |
| Pretty OP_HEAD Source # | |
| ATermConvertibleSML OP_HEAD Source # | |
Defined in ATC.Sml_cats | |
| type Rep OP_HEAD | |
Defined in CASL.ATC_CASL type Rep OP_HEAD = D1 ('MetaData "OP_HEAD" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Op_head" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe SORT)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
Constructors
| Assoc_op_attr | |
| Comm_op_attr | |
| Idem_op_attr | |
| Unit_op_attr (TERM f) |
Instances
| Eq f => Eq (OP_ATTR f) Source # | |
| Data f => Data (OP_ATTR f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OP_ATTR f -> c (OP_ATTR f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (OP_ATTR f) toConstr :: OP_ATTR f -> Constr dataTypeOf :: OP_ATTR f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (OP_ATTR f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (OP_ATTR f)) gmapT :: (forall b. Data b => b -> b) -> OP_ATTR f -> OP_ATTR f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OP_ATTR f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OP_ATTR f -> r gmapQ :: (forall d. Data d => d -> u) -> OP_ATTR f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OP_ATTR f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OP_ATTR f -> m (OP_ATTR f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_ATTR f -> m (OP_ATTR f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_ATTR f -> m (OP_ATTR f) | |
| Ord f => Ord (OP_ATTR f) Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show f => Show (OP_ATTR f) Source # | |
| Generic (OP_ATTR f) | |
| GetRange f => GetRange (OP_ATTR f) Source # | |
| FromJSON f => FromJSON (OP_ATTR f) | |
Defined in CASL.ATC_CASL | |
| ToJSON f => ToJSON (OP_ATTR f) | |
Defined in CASL.ATC_CASL Methods toEncoding :: OP_ATTR f -> Encoding toJSONList :: [OP_ATTR f] -> Value toEncodingList :: [OP_ATTR f] -> Encoding | |
| ShATermConvertible f => ShATermConvertible (OP_ATTR f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> OP_ATTR f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OP_ATTR f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_ATTR f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OP_ATTR f]) | |
| FormExtension f => Pretty (OP_ATTR f) Source # | |
| ATermConvertibleSML (OP_ATTR a) Source # | |
Defined in ATC.Sml_cats | |
| type Rep (OP_ATTR f) | |
Defined in CASL.ATC_CASL type Rep (OP_ATTR f) = D1 ('MetaData "OP_ATTR" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Assoc_op_attr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Comm_op_attr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Idem_op_attr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unit_op_attr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM f))))) | |
Constructors
| Pred_decl [PRED_NAME] PRED_TYPE Range | |
| Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range |
Instances
| Data f => Data (PRED_ITEM f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PRED_ITEM f -> c (PRED_ITEM f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PRED_ITEM f) toConstr :: PRED_ITEM f -> Constr dataTypeOf :: PRED_ITEM f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (PRED_ITEM f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PRED_ITEM f)) gmapT :: (forall b. Data b => b -> b) -> PRED_ITEM f -> PRED_ITEM f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PRED_ITEM f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PRED_ITEM f -> r gmapQ :: (forall d. Data d => d -> u) -> PRED_ITEM f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PRED_ITEM f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PRED_ITEM f -> m (PRED_ITEM f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_ITEM f -> m (PRED_ITEM f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_ITEM f -> m (PRED_ITEM f) | |
| Show f => Show (PRED_ITEM f) Source # | |
| Generic (PRED_ITEM f) | |
| GetRange f => GetRange (PRED_ITEM f) Source # | |
| FromJSON f => FromJSON (PRED_ITEM f) | |
Defined in CASL.ATC_CASL | |
| ToJSON f => ToJSON (PRED_ITEM f) | |
Defined in CASL.ATC_CASL Methods toJSON :: PRED_ITEM f -> Value toEncoding :: PRED_ITEM f -> Encoding toJSONList :: [PRED_ITEM f] -> Value toEncodingList :: [PRED_ITEM f] -> Encoding | |
| ShATermConvertible f => ShATermConvertible (PRED_ITEM f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> PRED_ITEM f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PRED_ITEM f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_ITEM f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PRED_ITEM f]) | |
| FormExtension f => Pretty (PRED_ITEM f) Source # | |
| ListCheck (PRED_ITEM f) Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML (PRED_ITEM a) Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> PRED_ITEM a from_sml_ShATermList :: ATermTable -> [PRED_ITEM a] | |
| type Rep (PRED_ITEM f) | |
Defined in CASL.ATC_CASL type Rep (PRED_ITEM f) = D1 ('MetaData "PRED_ITEM" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Pred_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PRED_NAME]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_TYPE) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Pred_defn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_NAME) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_HEAD)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Annoted (FORMULA f))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
Instances
| Eq PRED_TYPE Source # | |
| Data PRED_TYPE Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PRED_TYPE -> c PRED_TYPE gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PRED_TYPE toConstr :: PRED_TYPE -> Constr dataTypeOf :: PRED_TYPE -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PRED_TYPE) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PRED_TYPE) gmapT :: (forall b. Data b => b -> b) -> PRED_TYPE -> PRED_TYPE gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PRED_TYPE -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PRED_TYPE -> r gmapQ :: (forall d. Data d => d -> u) -> PRED_TYPE -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PRED_TYPE -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PRED_TYPE -> m PRED_TYPE gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_TYPE -> m PRED_TYPE gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_TYPE -> m PRED_TYPE | |
| Ord PRED_TYPE Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show PRED_TYPE Source # | |
| Generic PRED_TYPE | |
| GetRange PRED_TYPE Source # | |
| FromJSON PRED_TYPE | |
Defined in CASL.ATC_CASL | |
| ToJSON PRED_TYPE | |
Defined in CASL.ATC_CASL Methods toEncoding :: PRED_TYPE -> Encoding toJSONList :: [PRED_TYPE] -> Value toEncodingList :: [PRED_TYPE] -> Encoding | |
| ShATermConvertible PRED_TYPE | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> PRED_TYPE -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PRED_TYPE] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_TYPE) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PRED_TYPE]) | |
| Pretty PRED_TYPE Source # | |
| ATermConvertibleSML PRED_TYPE Source # | |
Defined in ATC.Sml_cats | |
| type Rep PRED_TYPE | |
Defined in CASL.ATC_CASL type Rep PRED_TYPE = D1 ('MetaData "PRED_TYPE" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Pred_type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) | |
Instances
| Data PRED_HEAD Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PRED_HEAD -> c PRED_HEAD gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PRED_HEAD toConstr :: PRED_HEAD -> Constr dataTypeOf :: PRED_HEAD -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PRED_HEAD) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PRED_HEAD) gmapT :: (forall b. Data b => b -> b) -> PRED_HEAD -> PRED_HEAD gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PRED_HEAD -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PRED_HEAD -> r gmapQ :: (forall d. Data d => d -> u) -> PRED_HEAD -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PRED_HEAD -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PRED_HEAD -> m PRED_HEAD gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_HEAD -> m PRED_HEAD gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_HEAD -> m PRED_HEAD | |
| Show PRED_HEAD Source # | |
| Generic PRED_HEAD | |
| GetRange PRED_HEAD Source # | |
| FromJSON PRED_HEAD | |
Defined in CASL.ATC_CASL | |
| ToJSON PRED_HEAD | |
Defined in CASL.ATC_CASL Methods toEncoding :: PRED_HEAD -> Encoding toJSONList :: [PRED_HEAD] -> Value toEncodingList :: [PRED_HEAD] -> Encoding | |
| ShATermConvertible PRED_HEAD | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> PRED_HEAD -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PRED_HEAD] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_HEAD) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PRED_HEAD]) | |
| ATermConvertibleSML PRED_HEAD Source # | |
Defined in ATC.Sml_cats | |
| type Rep PRED_HEAD | |
Defined in CASL.ATC_CASL type Rep PRED_HEAD = D1 ('MetaData "PRED_HEAD" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Pred_head" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) | |
data DATATYPE_DECL Source #
Constructors
| Datatype_decl SORT [Annoted ALTERNATIVE] Range |
Instances
| Data DATATYPE_DECL Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DATATYPE_DECL -> c DATATYPE_DECL gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DATATYPE_DECL toConstr :: DATATYPE_DECL -> Constr dataTypeOf :: DATATYPE_DECL -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DATATYPE_DECL) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DATATYPE_DECL) gmapT :: (forall b. Data b => b -> b) -> DATATYPE_DECL -> DATATYPE_DECL gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DATATYPE_DECL -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DATATYPE_DECL -> r gmapQ :: (forall d. Data d => d -> u) -> DATATYPE_DECL -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DATATYPE_DECL -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DATATYPE_DECL -> m DATATYPE_DECL gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DATATYPE_DECL -> m DATATYPE_DECL gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DATATYPE_DECL -> m DATATYPE_DECL | |
| Show DATATYPE_DECL Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> DATATYPE_DECL -> ShowS show :: DATATYPE_DECL -> String showList :: [DATATYPE_DECL] -> ShowS | |
| Generic DATATYPE_DECL | |
Defined in CASL.ATC_CASL Associated Types type Rep DATATYPE_DECL :: Type -> Type | |
| GetRange DATATYPE_DECL Source # | |
Defined in CASL.AS_Basic_CASL | |
| FromJSON DATATYPE_DECL | |
Defined in CASL.ATC_CASL | |
| ToJSON DATATYPE_DECL | |
Defined in CASL.ATC_CASL Methods toJSON :: DATATYPE_DECL -> Value toEncoding :: DATATYPE_DECL -> Encoding toJSONList :: [DATATYPE_DECL] -> Value toEncodingList :: [DATATYPE_DECL] -> Encoding | |
| ShATermConvertible DATATYPE_DECL | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> DATATYPE_DECL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DATATYPE_DECL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DATATYPE_DECL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DATATYPE_DECL]) | |
| Pretty DATATYPE_DECL Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML DATATYPE_DECL Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> DATATYPE_DECL from_sml_ShATermList :: ATermTable -> [DATATYPE_DECL] | |
| type Rep DATATYPE_DECL | |
Defined in CASL.ATC_CASL type Rep DATATYPE_DECL = D1 ('MetaData "DATATYPE_DECL" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Datatype_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted ALTERNATIVE]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
data ALTERNATIVE Source #
Constructors
| Alt_construct OpKind OP_NAME [COMPONENTS] Range | |
| Subsorts [SORT] Range |
Instances
| Data ALTERNATIVE Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ALTERNATIVE -> c ALTERNATIVE gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ALTERNATIVE toConstr :: ALTERNATIVE -> Constr dataTypeOf :: ALTERNATIVE -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ALTERNATIVE) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ALTERNATIVE) gmapT :: (forall b. Data b => b -> b) -> ALTERNATIVE -> ALTERNATIVE gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ALTERNATIVE -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ALTERNATIVE -> r gmapQ :: (forall d. Data d => d -> u) -> ALTERNATIVE -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ALTERNATIVE -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ALTERNATIVE -> m ALTERNATIVE gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ALTERNATIVE -> m ALTERNATIVE gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ALTERNATIVE -> m ALTERNATIVE | |
| Show ALTERNATIVE Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> ALTERNATIVE -> ShowS show :: ALTERNATIVE -> String showList :: [ALTERNATIVE] -> ShowS | |
| Generic ALTERNATIVE | |
Defined in CASL.ATC_CASL Associated Types type Rep ALTERNATIVE :: Type -> Type | |
| GetRange ALTERNATIVE Source # | |
Defined in CASL.AS_Basic_CASL | |
| FromJSON ALTERNATIVE | |
Defined in CASL.ATC_CASL | |
| ToJSON ALTERNATIVE | |
Defined in CASL.ATC_CASL Methods toJSON :: ALTERNATIVE -> Value toEncoding :: ALTERNATIVE -> Encoding toJSONList :: [ALTERNATIVE] -> Value toEncodingList :: [ALTERNATIVE] -> Encoding | |
| ShATermConvertible ALTERNATIVE | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> ALTERNATIVE -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ALTERNATIVE] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ALTERNATIVE) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ALTERNATIVE]) | |
| Pretty ALTERNATIVE Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML ALTERNATIVE Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> ALTERNATIVE from_sml_ShATermList :: ATermTable -> [ALTERNATIVE] | |
| type Rep ALTERNATIVE | |
Defined in CASL.ATC_CASL type Rep ALTERNATIVE = D1 ('MetaData "ALTERNATIVE" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Alt_construct" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_NAME)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [COMPONENTS]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Subsorts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) | |
data COMPONENTS Source #
Instances
| Data COMPONENTS Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> COMPONENTS -> c COMPONENTS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c COMPONENTS toConstr :: COMPONENTS -> Constr dataTypeOf :: COMPONENTS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c COMPONENTS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COMPONENTS) gmapT :: (forall b. Data b => b -> b) -> COMPONENTS -> COMPONENTS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> COMPONENTS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> COMPONENTS -> r gmapQ :: (forall d. Data d => d -> u) -> COMPONENTS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> COMPONENTS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> COMPONENTS -> m COMPONENTS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> COMPONENTS -> m COMPONENTS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> COMPONENTS -> m COMPONENTS | |
| Show COMPONENTS Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> COMPONENTS -> ShowS show :: COMPONENTS -> String showList :: [COMPONENTS] -> ShowS | |
| Generic COMPONENTS | |
Defined in CASL.ATC_CASL Associated Types type Rep COMPONENTS :: Type -> Type | |
| GetRange COMPONENTS Source # | |
Defined in CASL.AS_Basic_CASL | |
| FromJSON COMPONENTS | |
Defined in CASL.ATC_CASL | |
| ToJSON COMPONENTS | |
Defined in CASL.ATC_CASL Methods toJSON :: COMPONENTS -> Value toEncoding :: COMPONENTS -> Encoding toJSONList :: [COMPONENTS] -> Value toEncodingList :: [COMPONENTS] -> Encoding | |
| ShATermConvertible COMPONENTS | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> COMPONENTS -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [COMPONENTS] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, COMPONENTS) fromShATermList' :: Int -> ATermTable -> (ATermTable, [COMPONENTS]) | |
| Pretty COMPONENTS Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML COMPONENTS Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> COMPONENTS from_sml_ShATermList :: ATermTable -> [COMPONENTS] | |
| type Rep COMPONENTS | |
Defined in CASL.ATC_CASL type Rep COMPONENTS = D1 ('MetaData "COMPONENTS" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Cons_select" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OP_NAME])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Sort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT))) | |
Instances
| Eq VAR_DECL Source # | |
| Data VAR_DECL Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VAR_DECL -> c VAR_DECL gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VAR_DECL toConstr :: VAR_DECL -> Constr dataTypeOf :: VAR_DECL -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VAR_DECL) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VAR_DECL) gmapT :: (forall b. Data b => b -> b) -> VAR_DECL -> VAR_DECL gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VAR_DECL -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VAR_DECL -> r gmapQ :: (forall d. Data d => d -> u) -> VAR_DECL -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> VAR_DECL -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> VAR_DECL -> m VAR_DECL gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VAR_DECL -> m VAR_DECL gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VAR_DECL -> m VAR_DECL | |
| Ord VAR_DECL Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show VAR_DECL Source # | |
| Generic VAR_DECL | |
| GetRange VAR_DECL Source # | |
| FromJSON VAR_DECL | |
Defined in CASL.ATC_CASL | |
| ToJSON VAR_DECL | |
Defined in CASL.ATC_CASL Methods toEncoding :: VAR_DECL -> Encoding toJSONList :: [VAR_DECL] -> Value toEncodingList :: [VAR_DECL] -> Encoding | |
| ShATermConvertible VAR_DECL | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> VAR_DECL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [VAR_DECL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, VAR_DECL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [VAR_DECL]) | |
| Pretty VAR_DECL Source # | |
| ListCheck VAR_DECL Source # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML VAR_DECL Source # | |
Defined in ATC.Sml_cats | |
| type Rep VAR_DECL | |
Defined in CASL.ATC_CASL type Rep VAR_DECL = D1 ('MetaData "VAR_DECL" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Var_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
varDeclRange :: VAR_DECL -> [Pos] Source #
Instances
| Eq Junctor Source # | |
| Data Junctor Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Junctor -> c Junctor gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Junctor dataTypeOf :: Junctor -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Junctor) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Junctor) gmapT :: (forall b. Data b => b -> b) -> Junctor -> Junctor gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Junctor -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Junctor -> r gmapQ :: (forall d. Data d => d -> u) -> Junctor -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Junctor -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Junctor -> m Junctor gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Junctor -> m Junctor gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Junctor -> m Junctor | |
| Ord Junctor Source # | |
| Show Junctor Source # | |
| Generic Junctor | |
| GetRange Junctor Source # | |
| FromJSON Junctor | |
Defined in CASL.ATC_CASL | |
| ToJSON Junctor | |
Defined in CASL.ATC_CASL Methods toEncoding :: Junctor -> Encoding toJSONList :: [Junctor] -> Value toEncodingList :: [Junctor] -> Encoding | |
| ShATermConvertible Junctor | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> Junctor -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Junctor] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Junctor) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Junctor]) | |
| type Rep Junctor | |
Defined in CASL.ATC_CASL type Rep Junctor = D1 ('MetaData "Junctor" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Con" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Dis" 'PrefixI 'False) (U1 :: Type -> Type)) | |
dualJunctor :: Junctor -> Junctor Source #
Constructors
| Implication | |
| RevImpl | |
| Equivalence |
Instances
| Eq Relation Source # | |
| Data Relation Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Relation -> c Relation gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Relation toConstr :: Relation -> Constr dataTypeOf :: Relation -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Relation) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Relation) gmapT :: (forall b. Data b => b -> b) -> Relation -> Relation gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Relation -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Relation -> r gmapQ :: (forall d. Data d => d -> u) -> Relation -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Relation -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Relation -> m Relation gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Relation -> m Relation gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Relation -> m Relation | |
| Ord Relation Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show Relation Source # | |
| Generic Relation | |
| GetRange Relation Source # | |
| FromJSON Relation | |
Defined in CASL.ATC_CASL | |
| ToJSON Relation | |
Defined in CASL.ATC_CASL Methods toEncoding :: Relation -> Encoding toJSONList :: [Relation] -> Value toEncodingList :: [Relation] -> Encoding | |
| ShATermConvertible Relation | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> Relation -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Relation] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Relation) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Relation]) | |
| type Rep Relation | |
Defined in CASL.ATC_CASL type Rep Relation = D1 ('MetaData "Relation" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Implication" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RevImpl" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Equivalence" 'PrefixI 'False) (U1 :: Type -> Type))) | |
Instances
| Eq Equality Source # | |
| Data Equality Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Equality -> c Equality gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Equality toConstr :: Equality -> Constr dataTypeOf :: Equality -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Equality) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equality) gmapT :: (forall b. Data b => b -> b) -> Equality -> Equality gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Equality -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Equality -> r gmapQ :: (forall d. Data d => d -> u) -> Equality -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Equality -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Equality -> m Equality gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Equality -> m Equality gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Equality -> m Equality | |
| Ord Equality Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show Equality Source # | |
| Generic Equality | |
| GetRange Equality Source # | |
| FromJSON Equality | |
Defined in CASL.ATC_CASL | |
| ToJSON Equality | |
Defined in CASL.ATC_CASL Methods toEncoding :: Equality -> Encoding toJSONList :: [Equality] -> Value toEncodingList :: [Equality] -> Encoding | |
| ShATermConvertible Equality | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> Equality -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Equality] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Equality) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Equality]) | |
| type Rep Equality | |
Defined in CASL.ATC_CASL type Rep Equality = D1 ('MetaData "Equality" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Strong" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Existl" 'PrefixI 'False) (U1 :: Type -> Type)) | |
Constructors
| Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range | |
| Junction Junctor [FORMULA f] Range | |
| Relation (FORMULA f) Relation (FORMULA f) Range | |
| Negation (FORMULA f) Range | |
| Atom Bool Range | |
| Predication PRED_SYMB [TERM f] Range | |
| Definedness (TERM f) Range | |
| Equation (TERM f) Equality (TERM f) Range | |
| Membership (TERM f) SORT Range | |
| Mixfix_formula (TERM f) | |
| Unparsed_formula String Range | |
| Sort_gen_ax [Constraint] Bool | |
| QuantOp OP_NAME OP_TYPE (FORMULA f) | |
| QuantPred PRED_NAME PRED_TYPE (FORMULA f) | |
| ExtFORMULA f |
Instances
mkSort_gen_ax :: [Constraint] -> Bool -> FORMULA f Source #
is_True_atom :: FORMULA f -> Bool Source #
is_False_atom :: FORMULA f -> Bool Source #
data Constraint Source #
Instances
| Eq Constraint Source # | |
Defined in CASL.AS_Basic_CASL | |
| Data Constraint Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constraint -> c Constraint gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constraint toConstr :: Constraint -> Constr dataTypeOf :: Constraint -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constraint) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint) gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint | |
| Ord Constraint Source # | |
Defined in CASL.AS_Basic_CASL Methods compare :: Constraint -> Constraint -> Ordering (<) :: Constraint -> Constraint -> Bool (<=) :: Constraint -> Constraint -> Bool (>) :: Constraint -> Constraint -> Bool (>=) :: Constraint -> Constraint -> Bool max :: Constraint -> Constraint -> Constraint min :: Constraint -> Constraint -> Constraint | |
| Show Constraint Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> Constraint -> ShowS show :: Constraint -> String showList :: [Constraint] -> ShowS | |
| Generic Constraint | |
Defined in CASL.ATC_CASL Associated Types type Rep Constraint :: Type -> Type | |
| GetRange Constraint Source # | |
Defined in CASL.AS_Basic_CASL | |
| FromJSON Constraint | |
Defined in CASL.ATC_CASL | |
| ToJSON Constraint | |
Defined in CASL.ATC_CASL Methods toJSON :: Constraint -> Value toEncoding :: Constraint -> Encoding toJSONList :: [Constraint] -> Value toEncodingList :: [Constraint] -> Encoding | |
| ShATermConvertible Constraint | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> Constraint -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Constraint] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Constraint) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Constraint]) | |
| type Rep Constraint | |
Defined in CASL.ATC_CASL type Rep Constraint = D1 ('MetaData "Constraint" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Constraint" 'PrefixI 'True) (S1 ('MetaSel ('Just "newSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: (S1 ('MetaSel ('Just "opSymbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(OP_SYMB, [Int])]) :*: S1 ('MetaSel ('Just "origSort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT)))) | |
sortConstraints :: [Constraint] -> [Constraint] Source #
isInjectiveList :: Ord a => [a] -> Bool Source #
no duplicate sorts, i.e. injective sort map?
recover_Sort_gen_ax :: [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)]) Source #
from a Sort_gex_ax, recover: a traditional sort generation constraint plus a sort mapping
recoverSortGen :: [Constraint] -> [(SORT, [OP_SYMB])] Source #
from a Sort_gen_ax, recover: the sorts, each paired with the constructors
recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])] Source #
from a free Sort_gen_ax, recover: the sorts, each paired with the constructors fails (i.e. delivers Nothing) if the sort map is not injective
data QUANTIFIER Source #
Constructors
| Universal | |
| Existential | |
| Unique_existential |
Instances
| Eq QUANTIFIER Source # | |
Defined in CASL.AS_Basic_CASL | |
| Data QUANTIFIER Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QUANTIFIER -> c QUANTIFIER gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QUANTIFIER toConstr :: QUANTIFIER -> Constr dataTypeOf :: QUANTIFIER -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QUANTIFIER) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QUANTIFIER) gmapT :: (forall b. Data b => b -> b) -> QUANTIFIER -> QUANTIFIER gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QUANTIFIER -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QUANTIFIER -> r gmapQ :: (forall d. Data d => d -> u) -> QUANTIFIER -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> QUANTIFIER -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> QUANTIFIER -> m QUANTIFIER gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QUANTIFIER -> m QUANTIFIER gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QUANTIFIER -> m QUANTIFIER | |
| Ord QUANTIFIER Source # | |
Defined in CASL.AS_Basic_CASL Methods compare :: QUANTIFIER -> QUANTIFIER -> Ordering (<) :: QUANTIFIER -> QUANTIFIER -> Bool (<=) :: QUANTIFIER -> QUANTIFIER -> Bool (>) :: QUANTIFIER -> QUANTIFIER -> Bool (>=) :: QUANTIFIER -> QUANTIFIER -> Bool max :: QUANTIFIER -> QUANTIFIER -> QUANTIFIER min :: QUANTIFIER -> QUANTIFIER -> QUANTIFIER | |
| Show QUANTIFIER Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> QUANTIFIER -> ShowS show :: QUANTIFIER -> String showList :: [QUANTIFIER] -> ShowS | |
| Generic QUANTIFIER | |
Defined in CASL.ATC_CASL Associated Types type Rep QUANTIFIER :: Type -> Type | |
| GetRange QUANTIFIER Source # | |
Defined in CASL.AS_Basic_CASL | |
| FromJSON QUANTIFIER | |
Defined in CASL.ATC_CASL | |
| ToJSON QUANTIFIER | |
Defined in CASL.ATC_CASL Methods toJSON :: QUANTIFIER -> Value toEncoding :: QUANTIFIER -> Encoding toJSONList :: [QUANTIFIER] -> Value toEncodingList :: [QUANTIFIER] -> Encoding | |
| ShATermConvertible QUANTIFIER | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> QUANTIFIER -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [QUANTIFIER] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, QUANTIFIER) fromShATermList' :: Int -> ATermTable -> (ATermTable, [QUANTIFIER]) | |
| ATermConvertibleSML QUANTIFIER Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> QUANTIFIER from_sml_ShATermList :: ATermTable -> [QUANTIFIER] | |
| type Rep QUANTIFIER | |
Defined in CASL.ATC_CASL type Rep QUANTIFIER = D1 ('MetaData "QUANTIFIER" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Universal" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Existential" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unique_existential" 'PrefixI 'False) (U1 :: Type -> Type))) | |
Instances
| Eq PRED_SYMB Source # | |
| Data PRED_SYMB Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PRED_SYMB -> c PRED_SYMB gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PRED_SYMB toConstr :: PRED_SYMB -> Constr dataTypeOf :: PRED_SYMB -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PRED_SYMB) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PRED_SYMB) gmapT :: (forall b. Data b => b -> b) -> PRED_SYMB -> PRED_SYMB gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PRED_SYMB -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PRED_SYMB -> r gmapQ :: (forall d. Data d => d -> u) -> PRED_SYMB -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PRED_SYMB -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PRED_SYMB -> m PRED_SYMB gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_SYMB -> m PRED_SYMB gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_SYMB -> m PRED_SYMB | |
| Ord PRED_SYMB Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show PRED_SYMB Source # | |
| Generic PRED_SYMB | |
| GetRange PRED_SYMB Source # | |
| FromJSON PRED_SYMB | |
Defined in CASL.ATC_CASL | |
| ToJSON PRED_SYMB | |
Defined in CASL.ATC_CASL Methods toEncoding :: PRED_SYMB -> Encoding toJSONList :: [PRED_SYMB] -> Value toEncodingList :: [PRED_SYMB] -> Encoding | |
| ShATermConvertible PRED_SYMB | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> PRED_SYMB -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PRED_SYMB] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_SYMB) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PRED_SYMB]) | |
| Pretty PRED_SYMB Source # | |
| ATermConvertibleSML PRED_SYMB Source # | |
Defined in ATC.Sml_cats | |
| type Rep PRED_SYMB | |
Defined in CASL.ATC_CASL type Rep PRED_SYMB = D1 ('MetaData "PRED_SYMB" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Pred_name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_NAME)) :+: C1 ('MetaCons "Qual_pred_name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_NAME) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_TYPE) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
predSymbName :: PRED_SYMB -> PRED_NAME Source #
Constructors
| Qual_var VAR SORT Range | |
| Application OP_SYMB [TERM f] Range | |
| Sorted_term (TERM f) SORT Range | |
| Cast (TERM f) SORT Range | |
| Conditional (TERM f) (FORMULA f) (TERM f) Range | |
| Unparsed_term String Range | |
| Mixfix_qual_pred PRED_SYMB | |
| Mixfix_term [TERM f] | |
| Mixfix_token Token | |
| Mixfix_sorted_term SORT Range | |
| Mixfix_cast SORT Range | |
| Mixfix_parenthesized [TERM f] Range | |
| Mixfix_bracketed [TERM f] Range | |
| Mixfix_braced [TERM f] Range | |
| ExtTERM f |
Instances
| Eq f => Eq (TERM f) Source # | |
| Data f => Data (TERM f) Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TERM f -> c (TERM f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TERM f) dataTypeOf :: TERM f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TERM f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TERM f)) gmapT :: (forall b. Data b => b -> b) -> TERM f -> TERM f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM f -> r gmapQ :: (forall d. Data d => d -> u) -> TERM f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TERM f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TERM f -> m (TERM f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM f -> m (TERM f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM f -> m (TERM f) | |
| Ord f => Ord (TERM f) Source # | |
| Show f => Show (TERM f) Source # | |
| Generic (TERM f) | |
| GetRange f => GetRange (TERM f) Source # | |
| FromJSON f => FromJSON (TERM f) | |
Defined in CASL.ATC_CASL | |
| ToJSON f => ToJSON (TERM f) | |
Defined in CASL.ATC_CASL Methods toEncoding :: TERM f -> Encoding toJSONList :: [TERM f] -> Value toEncodingList :: [TERM f] -> Encoding | |
| ShATermConvertible f => ShATermConvertible (TERM f) | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> TERM f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TERM f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TERM f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TERM f]) | |
| FormExtension f => Pretty (TERM f) Source # | |
| TermExtension f => TermExtension (TERM f) Source # | |
| ATermConvertibleSML (TERM a) Source # | |
Defined in ATC.Sml_cats | |
| type Rep (TERM f) | |
Defined in CASL.ATC_CASL type Rep (TERM f) = D1 ('MetaData "TERM" "CASL.AS_Basic_CASL" "main" 'False) (((C1 ('MetaCons "Qual_var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VAR) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Application" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_SYMB) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TERM f]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Sorted_term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM f)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: ((C1 ('MetaCons "Cast" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM f)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Conditional" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM f)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA f))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM f)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Unparsed_term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Mixfix_qual_pred" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_SYMB))))) :+: (((C1 ('MetaCons "Mixfix_term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TERM f])) :+: C1 ('MetaCons "Mixfix_token" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))) :+: (C1 ('MetaCons "Mixfix_sorted_term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Mixfix_cast" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "Mixfix_parenthesized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TERM f]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Mixfix_bracketed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TERM f]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Mixfix_braced" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TERM f]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "ExtTERM" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 f)))))) | |
varOrConst :: Token -> TERM f Source #
state after mixfix- but before overload resolution
Instances
| Eq OP_SYMB Source # | |
| Data OP_SYMB Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OP_SYMB -> c OP_SYMB gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OP_SYMB dataTypeOf :: OP_SYMB -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OP_SYMB) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OP_SYMB) gmapT :: (forall b. Data b => b -> b) -> OP_SYMB -> OP_SYMB gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OP_SYMB -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OP_SYMB -> r gmapQ :: (forall d. Data d => d -> u) -> OP_SYMB -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OP_SYMB -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OP_SYMB -> m OP_SYMB gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_SYMB -> m OP_SYMB gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OP_SYMB -> m OP_SYMB | |
| Ord OP_SYMB Source # | |
| Show OP_SYMB Source # | |
| Generic OP_SYMB | |
| GetRange OP_SYMB Source # | |
| FromJSON OP_SYMB | |
Defined in CASL.ATC_CASL | |
| ToJSON OP_SYMB | |
Defined in CASL.ATC_CASL Methods toEncoding :: OP_SYMB -> Encoding toJSONList :: [OP_SYMB] -> Value toEncodingList :: [OP_SYMB] -> Encoding | |
| ShATermConvertible OP_SYMB | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> OP_SYMB -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OP_SYMB] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OP_SYMB) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OP_SYMB]) | |
| Pretty OP_SYMB Source # | |
| ATermConvertibleSML OP_SYMB Source # | |
Defined in ATC.Sml_cats | |
| type Rep OP_SYMB | |
Defined in CASL.ATC_CASL type Rep OP_SYMB = D1 ('MetaData "OP_SYMB" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Op_name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_NAME)) :+: C1 ('MetaCons "Qual_op_name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_NAME) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_TYPE) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
opSymbName :: OP_SYMB -> OP_NAME Source #
short cuts for terms and formulas
mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f Source #
create binding if variables are non-null
toQualVar :: VAR_DECL -> TERM f Source #
convert a singleton variable declaration into a qualified variable
mkVarDeclStr :: String -> SORT -> VAR_DECL Source #
type synonyms
type CASLFORMULA = FORMULA () Source #
data SYMB_ITEMS Source #
Constructors
| Symb_items SYMB_KIND [SYMB] Range |
Instances
symbItemsName :: SYMB_ITEMS -> [String] Source #
data SYMB_MAP_ITEMS Source #
Constructors
| Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range |
Instances
Constructors
| Implicit | |
| Sorts_kind | |
| Ops_kind | |
| Preds_kind |
Instances
| Eq SYMB_KIND Source # | |
| Data SYMB_KIND Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_KIND -> c SYMB_KIND gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_KIND toConstr :: SYMB_KIND -> Constr dataTypeOf :: SYMB_KIND -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_KIND) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_KIND) gmapT :: (forall b. Data b => b -> b) -> SYMB_KIND -> SYMB_KIND gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_KIND -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_KIND -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB_KIND -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_KIND -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_KIND -> m SYMB_KIND gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_KIND -> m SYMB_KIND gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_KIND -> m SYMB_KIND | |
| Ord SYMB_KIND Source # | |
Defined in CASL.AS_Basic_CASL | |
| Show SYMB_KIND Source # | |
| Generic SYMB_KIND | |
| GetRange SYMB_KIND Source # | |
| FromJSON SYMB_KIND | |
Defined in CASL.ATC_CASL | |
| ToJSON SYMB_KIND | |
Defined in CASL.ATC_CASL Methods toEncoding :: SYMB_KIND -> Encoding toJSONList :: [SYMB_KIND] -> Value toEncodingList :: [SYMB_KIND] -> Encoding | |
| ShATermConvertible SYMB_KIND | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> SYMB_KIND -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SYMB_KIND] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_KIND) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_KIND]) | |
| Pretty SYMB_KIND Source # | |
| ATermConvertibleSML SYMB_KIND Source # | |
Defined in ATC.Sml_cats | |
| type Rep SYMB_KIND | |
Defined in CASL.ATC_CASL type Rep SYMB_KIND = D1 ('MetaData "SYMB_KIND" "CASL.AS_Basic_CASL" "main" 'False) ((C1 ('MetaCons "Implicit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sorts_kind" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Ops_kind" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Preds_kind" 'PrefixI 'False) (U1 :: Type -> Type))) | |
Instances
| Eq SYMB Source # | |
| Data SYMB Source # | |
Defined in CASL.AS_Basic_CASL 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 dataTypeOf :: SYMB -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB) gmapT :: (forall b. Data b => b -> b) -> SYMB -> SYMB gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB | |
| Ord SYMB Source # | |
| Show SYMB Source # | |
| Generic SYMB | |
| GetRange SYMB Source # | |
| FromJSON SYMB | |
Defined in CASL.ATC_CASL | |
| ToJSON SYMB | |
Defined in CASL.ATC_CASL Methods toEncoding :: SYMB -> Encoding toJSONList :: [SYMB] -> Value toEncodingList :: [SYMB] -> Encoding | |
| ShATermConvertible SYMB | |
Defined in CASL.ATC_CASL 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 # | |
| ATermConvertibleSML SYMB Source # | |
Defined in ATC.Sml_cats | |
| type Rep SYMB | |
Defined in CASL.ATC_CASL type Rep SYMB = D1 ('MetaData "SYMB" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "Symb_id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id)) :+: C1 ('MetaCons "Qual_id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TYPE) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) | |
Instances
| Eq TYPE Source # | |
| Data TYPE Source # | |
Defined in CASL.AS_Basic_CASL Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TYPE -> c TYPE gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TYPE dataTypeOf :: TYPE -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TYPE) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TYPE) gmapT :: (forall b. Data b => b -> b) -> TYPE -> TYPE gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r gmapQ :: (forall d. Data d => d -> u) -> TYPE -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TYPE -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TYPE -> m TYPE gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TYPE -> m TYPE gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TYPE -> m TYPE | |
| Ord TYPE Source # | |
| Show TYPE Source # | |
| Generic TYPE | |
| GetRange TYPE Source # | |
| FromJSON TYPE | |
Defined in CASL.ATC_CASL | |
| ToJSON TYPE | |
Defined in CASL.ATC_CASL Methods toEncoding :: TYPE -> Encoding toJSONList :: [TYPE] -> Value toEncodingList :: [TYPE] -> Encoding | |
| ShATermConvertible TYPE | |
Defined in CASL.ATC_CASL Methods toShATermAux :: ATermTable -> TYPE -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TYPE] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TYPE) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TYPE]) | |
| Pretty TYPE Source # | |
| ATermConvertibleSML TYPE Source # | |
Defined in ATC.Sml_cats | |
| type Rep TYPE | |
Defined in CASL.ATC_CASL type Rep TYPE = D1 ('MetaData "TYPE" "CASL.AS_Basic_CASL" "main" 'False) (C1 ('MetaCons "O_type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_TYPE)) :+: (C1 ('MetaCons "P_type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_TYPE)) :+: C1 ('MetaCons "A_type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT)))) | |
data SYMB_OR_MAP Source #
Instances
| Eq SYMB_OR_MAP Source # | |
Defined in CASL.AS_Basic_CASL | |
| Data SYMB_OR_MAP Source # | |
Defined in CASL.AS_Basic_CASL 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 | |
| Ord SYMB_OR_MAP Source # | |
Defined in CASL.AS_Basic_CASL Methods compare :: SYMB_OR_MAP -> SYMB_OR_MAP -> Ordering (<) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (<=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (>) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (>=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool max :: SYMB_OR_MAP -> SYMB_OR_MAP -> SYMB_OR_MAP min :: SYMB_OR_MAP -> SYMB_OR_MAP -> SYMB_OR_MAP | |
| Show SYMB_OR_MAP Source # | |
Defined in CASL.AS_Basic_CASL Methods showsPrec :: Int -> SYMB_OR_MAP -> ShowS show :: SYMB_OR_MAP -> String showList :: [SYMB_OR_MAP] -> ShowS | |
| Generic SYMB_OR_MAP | |
Defined in CASL.ATC_CASL Associated Types type Rep SYMB_OR_MAP :: Type -> Type | |
| GetRange SYMB_OR_MAP Source # | |
Defined in CASL.AS_Basic_CASL | |
| FromJSON SYMB_OR_MAP | |
Defined in CASL.ATC_CASL | |
| ToJSON SYMB_OR_MAP | |
Defined in CASL.ATC_CASL 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 | |
Defined in CASL.ATC_CASL 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 # | |
Defined in CASL.ToDoc | |
| ATermConvertibleSML SYMB_OR_MAP Source # | |
Defined in ATC.Sml_cats Methods from_sml_ShATerm :: ATermTable -> SYMB_OR_MAP from_sml_ShATermList :: ATermTable -> [SYMB_OR_MAP] | |
| type Rep SYMB_OR_MAP | |
Defined in CASL.ATC_CASL type Rep SYMB_OR_MAP = D1 ('MetaData "SYMB_OR_MAP" "CASL.AS_Basic_CASL" "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)))) | |