Module `Libelectrod.Raw`Source

Type for "raw" ASTs yielded by the Electrod parser.

Sourcetype raw_goal = (Raw_ident.t, Raw_ident.t) Gen_goal.t

Sourcetype raw_block = (Raw_ident.t, Raw_ident.t) Gen_goal.block

Sourcetype 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
*)

}

Sourceand raw_urelements = private

| UIntvl of raw_interval
| UPlain of Raw_ident.t

Sourceand 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).

Sourceand raw_multiplicity = [ `Lone | `One ] option

Sourceand raw_scope = private

| SExact of raw_bound
| SInexact of raw_bound * raw_multiplicity * raw_bound

Sourceand 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

Sourceand raw_element = private

| EIntvl of raw_interval
(*
1-tuples
*)
| ETuple of raw_tuple

Sourceand raw_tuple = Raw_ident.t list

A n-tuple (incl. n = 1). inv: nonempty list

Sourceand raw_interval = Raw_ident.t * Raw_ident.t

Sourceand raw_assignment = Raw_ident.t * raw_tuple list

asignemnt of tuples to a relation

may be empty

Source

and raw_symmetry =
  (Raw_ident.t * raw_tuple) list * (Raw_ident.t * raw_tuple) list

Sourcetype 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

Sourceval interval : Raw_ident.t -> Raw_ident.t -> raw_interval

Sourceval etuple : Raw_ident.t list -> raw_element

Sourceval eintvl : raw_interval -> raw_element

Sourceval buniv : raw_bound

Sourceval bref : Raw_ident.t -> raw_bound

Sourceval bprod : raw_bound -> raw_multiplicity -> raw_bound -> raw_bound

Sourceval bunion : raw_bound -> raw_bound -> raw_bound

Sourceval belts : raw_element list -> raw_bound

Sourceval sexact : raw_bound -> raw_scope

Sourceval sinexact : raw_bound -> raw_multiplicity -> raw_bound -> raw_scope

Sourceval dconst : Raw_ident.t -> int option -> raw_scope -> raw_declaration

Source

val dvar : 
  Raw_ident.t ->
  int option ->
  raw_scope ->
  raw_scope option ->
  raw_declaration

Sourceval uintvl : raw_interval -> raw_urelements

Sourceval uplain : Raw_ident.t -> raw_urelements

Source

val problem : 
  string option ->
  raw_urelements list ->
  raw_declaration list ->
  raw_goal ->
  raw_block ->
  raw_assignment list ->
  raw_symmetry list ->
  raw_problem

Accessors

Sourceval decl_id : raw_declaration -> Raw_ident.t

package electrod

Module Libelectrod.RawSource

Constructors

Accessors

Module `Libelectrod.Raw`Source