Module Parsetree

module Parsetree: sig .. end

Abstract syntax tree produced by the parser

type p_type = string

type p_read_memory_order =

type p_write_memory_order =

`\|`	`Pwmo_nonatomic`
`\|`	`Pwmo_relaxed of (string * string * a_expression list) option`
`\|`	`Pwmo_release of (string * string * a_expression list) option`
`\|`	`Pwmo_seq_cst of (string * string * a_expression list) option`

type p_cas_memory_order =

type p_expression = {

	`pexp_desc : p_expression_desc;`
	`pexp_loc : Location.t;`

}

type p_expression_desc =

`\|`	`Pexp_ident of string`
`\|`	`Pexp_num of int`
`\|`	`Pexp_bool of bool`
`\|`	`Pexp_prefix of string * p_expression`
`\|`	`Pexp_infix of string * p_expression * p_expression`
`\|`	`Pexp_cast of p_expression * p_type`	`(*`	impure	`*)`
`\|`	`Pexp_fld of p_expression * Misc.component * p_read_memory_order`	`(*`	impure	`*)`
`\|`	`Pexp_cas of p_expression * Misc.component * p_expression * p_expression * p_cas_memory_order * p_read_memory_order`	`(*`	impure	`*)`
`\|`	`Pexp_new of p_type * p_expression`	`(*`	impure	`*)`
`\|`	`Pexp_fun of string * p_expression list`
`\|`	`Pexp_fcall of string * actual_params`	`(*`	impure	`*)`

type actual_params = p_expression list * p_expression list

type a_expression = p_expression

without the impure cases

type dlink_kind =

`\|`	`DL`
`\|`	`XL`

type a_proposition =

`\|`	`Aprop_exp of a_expression`
`\|`	`Aprop_node of Misc.component * a_expression * (Misc.component * a_expression) list`
`\|`	`Aprop_indpred of string * (string * Location.t) list * a_expression list * Location.t`
`\|`	`Aprop_ifthenelse of a_expression * a_proposition * a_proposition`
`\|`	`Aprop_star of a_proposition * a_proposition`
`\|`	`Aprop_barbar of a_proposition * a_proposition`
`\|`	`Aprop_box of Misc.component * a_proposition`
`\|`	`Aprop_atomic_fld of a_expression * string * string * string * a_expression list`
`\|`	`Aprop_escrow of string * a_expression list`
`\|`	`Aprop_token of a_expression`

type a_invariant = a_proposition option

type p_statement = {

	`pstm_desc : p_statement_desc;`
	`pstm_loc : Location.t;`

}

type p_statement_desc =

`\|`	`Pstm_exp of p_expression`
`\|`	`Pstm_assign of string * p_expression option`
`\|`	`Pstm_fldassign of (p_expression * Misc.component * p_expression) list * p_write_memory_order`
`\|`	`Pstm_dispose of p_expression * p_expression`
`\|`	`Pstm_block of p_statement list`
`\|`	`Pstm_assume of p_expression`
`\|`	`Pstm_if of p_expression option * p_statement * p_statement`
`\|`	`Pstm_while of a_invariant * p_expression option * p_statement`
`\|`	`Pstm_atomic of p_expression * p_statement`
`\|`	`Pstm_withres of Misc.component * p_expression * p_statement * string * p_expression list`
`\|`	`Pstm_action of p_statement * Misc.component * string * p_expression list`
`\|`	`Pstm_parblock of (string option * string * actual_params) list`
`\|`	`Pstm_interfere of Misc.component * string`
`\|`	`Pstm_return of p_expression option`
`\|`	`Pstm_break`
`\|`	`Pstm_continue`
`\|`	`Pstm_comment of string`

type p_action = string * (string * Location.t) list * a_proposition *
       a_proposition * a_proposition *
       p_statement list * Location.t

type p_vars = (string * p_type * Location.t) list

type p_state_after = string * (string * Location.t) list * a_proposition * Location.t

type p_protocol_state = string * (string * Location.t) list * p_state_after list * 
       string * a_proposition * Location.t

type p_item =

`\|`	`Pdec_options of (string * string * Location.t) list`
`\|`	`Pdec_class of string * p_vars * Location.t`
`\|`	`Pdec_var of string * p_type * bool * Location.t`
`\|`	`Pdec_fun of string * p_type * (p_vars * p_vars) * (a_invariant * a_invariant) * (p_vars * p_statement list) * bool * Location.t`
`\|`	`Pdec_resource of Misc.component * (string * Location.t) list * a_invariant * (p_vars * p_statement list) * p_statement list option * p_action list * Location.t`
`\|`	`Pdec_indpred of string * (string * Location.t) list * a_proposition * Location.t`
`\|`	`Pdec_comment of string`
`\|`	`Pdec_protocol of string * p_protocol_state list * Location.t`
`\|`	`Pdec_escrow of string * (string * Location.t) list * a_proposition * a_proposition * Location.t`

type p_program = p_item list

val iter : (Location.t -> p_statement_desc -> unit) ->
       p_statement list -> unit

iter f s calls f on each statement in s

val a_prop_empty : a_proposition

val exp_is_pure : p_expression -> bool