| Copyright | (c) Artem Mavrin 2021 |
|---|---|
| License | BSD3 |
| Maintainer | artemvmavrin@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
AutoProof.Internal.AST
Description
Defines an abstract syntax tree class and related functions.
Synopsis
- class AST t where
- data ASTMetadata = ASTMetadata {}
- subtrees :: (AST t, Ord t) => t -> Set t
- properSubtrees :: (AST t, Ord t) => t -> Set t
- atomicASTConstructor :: (ASTMetadata -> a -> t) -> a -> t
- unaryASTConstructor :: AST t => (ASTMetadata -> t -> t) -> t -> t
- binaryASTConstructor :: AST t => (ASTMetadata -> t -> t -> t) -> t -> t -> t
- unaryRootedASTConstructor :: AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t
- binaryRootedASTConstructor :: AST t => (ASTMetadata -> a -> t -> t -> t) -> a -> t -> t -> t
- ternaryRootedASTConstructor :: AST t => (ASTMetadata -> a -> t -> t -> t -> t) -> a -> t -> t -> t -> t
Abstract syntax tree class and metadata type
Abstract syntax tree class.
Methods
The value at the AST's root node.
The AST's child ASTs.
metadata :: t -> ASTMetadata Source #
The AST's metadata
Number of edges on the longest path from the root of the AST to a leaf.
Number of nodes in the AST.
data ASTMetadata Source #
Container type for AST properties, intended for constant-time access.
Constructors
| ASTMetadata | |
Instances
| Eq ASTMetadata Source # | |
Defined in AutoProof.Internal.AST | |
| Ord ASTMetadata Source # | |
Defined in AutoProof.Internal.AST Methods compare :: ASTMetadata -> ASTMetadata -> Ordering # (<) :: ASTMetadata -> ASTMetadata -> Bool # (<=) :: ASTMetadata -> ASTMetadata -> Bool # (>) :: ASTMetadata -> ASTMetadata -> Bool # (>=) :: ASTMetadata -> ASTMetadata -> Bool # max :: ASTMetadata -> ASTMetadata -> ASTMetadata # min :: ASTMetadata -> ASTMetadata -> ASTMetadata # | |
AST functions
subtrees :: (AST t, Ord t) => t -> Set t Source #
( is the set of all subtrees of an AST subtrees t)t (including t
itself).
properSubtrees :: (AST t, Ord t) => t -> Set t Source #
( is the the set of all proper subtrees of an AST
properSubtrees t)t (i.e., not including t itself).
Helper functions for creating AST constructors
atomicASTConstructor :: (ASTMetadata -> a -> t) -> a -> t Source #
Helper function for creating metadata-aware ASTs.
unaryASTConstructor :: AST t => (ASTMetadata -> t -> t) -> t -> t Source #
Helper function for creating metadata-aware ASTs.
binaryASTConstructor :: AST t => (ASTMetadata -> t -> t -> t) -> t -> t -> t Source #
Helper function for creating metadata-aware ASTs.
unaryRootedASTConstructor :: AST t => (ASTMetadata -> a -> t -> t) -> a -> t -> t Source #
Helper function for creating metadata-aware rooted ASTs.
binaryRootedASTConstructor :: AST t => (ASTMetadata -> a -> t -> t -> t) -> a -> t -> t -> t Source #
Helper function for creating metadata-aware rooted ASTs.
ternaryRootedASTConstructor :: AST t => (ASTMetadata -> a -> t -> t -> t -> t) -> a -> t -> t -> t -> t Source #
Helper function for creating metadata-aware rooted ASTs.