package electrod
Formal analysis for the Electrod formal pivot language
Install
dune-project
Dependency
Authors
Maintainers
Sources
electrod-0.8.0.tbz
sha256=dd47a6d755dc80a9a75fa21bda7a6507316ca2a33f7201d25ee9ba01d902a6a2
sha512=abc8bb1194df32bfe3c00f499dd989868c9ad208c8c7401085b9c18e87890eae1c087dbbb9bf128f95f4e759de27e1d7a6d6b2f7a5e6a9b000b469d72c77b87a
doc/electrod.libelectrod/Libelectrod/Raw/index.html
Module Libelectrod.RawSource
Type for "raw" ASTs yielded by the Electrod parser.
Source
type raw_problem = {file : string option;raw_univ : raw_urelements list;raw_decls : raw_declaration list;(*does not contain 'univ'
*)raw_goal : raw_goal;raw_invar : raw_block;(*may be empty
*)raw_inst : raw_assignment list;(*may be empty
*)raw_syms : raw_symmetry list;(*may be empty
*)
}Source
and raw_declaration = private | DConst of Raw_ident.t * int option * raw_scope| DVar of Raw_ident.t * int option * raw_scope * raw_scope option
The int option is the optionally-declared arity (compulsory for an empty scope).
Source
and raw_scope = private | SExact of raw_bound| SInexact of raw_bound * raw_multiplicity * raw_bound
Source
and raw_bound = private | BUniv| BRef of Raw_ident.t(*reference to a previously-defined set
*)| BProd of raw_bound * raw_multiplicity * raw_bound(*None/Some (lone/one)
*)| BUnion of raw_bound * raw_bound| BElts of raw_element list
A n-tuple (incl. n = 1). inv: nonempty list
asignemnt of tuples to a relation
may be empty
Source
type raw_paragraph = | ParGoal of raw_goal| ParInst of raw_assignment list| ParSym of raw_symmetry list| ParInv of raw_block
This definition is here just to be used in the parser ((to avoid cyclic dependencies). The puprose of paragraphs is to deal easily and efficiently with permutation of these (see Parse_main for more information).)
Constructors
Source
val problem :
string option ->
raw_urelements list ->
raw_declaration list ->
raw_goal ->
raw_block ->
raw_assignment list ->
raw_symmetry list ->
raw_problemAccessors
On This Page