Module Ptree (.ml)

module Ptree: sig .. end

type term =

`\|`	`TVar of Variable.t`
`\|`	`TTerm of Types.Term.t`

type atom =

`\|`	`AVar of Variable.t`
`\|`	`AAtom of Types.Atom.t`
`\|`	`AEq of term * term`
`\|`	`ANeq of term * term`
`\|`	`ALe of term * term`
`\|`	`ALt of term * term`

type formula =

`\|`	`PAtom of atom`
`\|`	`PNot of formula`
`\|`	`PAnd of formula list`
`\|`	`POr of formula list`
`\|`	`PImp of formula * formula`
`\|`	`PEquiv of formula * formula`
`\|`	`PIte of formula * formula * formula`
`\|`	`PForall of Variable.t list * formula`
`\|`	`PExists of Variable.t list * formula`
`\|`	`PForall_other of Variable.t list * formula`
`\|`	`PExists_other of Variable.t list * formula`

type term_or_formula =

`\|`	`PF of formula`
`\|`	`PT of term`

type cformula = formula

type pswts = (cformula * term) list

type pglob_update =

`\|`	`PUTerm of term`
`\|`	`PUCase of pswts`

type pupdate = {

	`pup_loc : Util.loc;`
	`pup_arr : Hstring.t;`
	`pup_arg : Variable.t list;`
	`pup_swts : pswts;`

}

type ptransition = {

	`ptr_lets : (Hstring.t * term) list;`
	`ptr_name : Hstring.t;`
	`ptr_args : Variable.t list;`
	`ptr_reqs : cformula;`
	`ptr_assigns : (Hstring.t * pglob_update) list;`
	`ptr_upds : pupdate list;`
	`ptr_nondets : Hstring.t list;`
	`ptr_loc : Util.loc;`

}

type psystem = {

	`pglobals : (Util.loc * Hstring.t * Smt.Type.t) list;`
	`pconsts : (Util.loc * Hstring.t * Smt.Type.t) list;`
	`parrays : (Util.loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list;`
	`ptype_defs : (Util.loc * Ast.type_constructors) list;`
	`pinit : Util.loc * Variable.t list * cformula;`
	`pinvs : (Util.loc * Variable.t list * cformula) list;`
	`punsafe : (Util.loc * Variable.t list * cformula) list;`
	`ptrans : ptransition list;`

}

type pdecl =

`\|`	`PInit of (Util.loc * Variable.t list * cformula)`
`\|`	`PInv of (Util.loc * Variable.t list * cformula)`
`\|`	`PUnsafe of (Util.loc * Variable.t list * cformula)`
`\|`	`PTrans of ptransition`
`\|`	`PFun`

val add_fun_def : Hstring.t -> Variable.t list -> formula -> unit

val app_fun : Hstring.t -> term_or_formula list -> formula

val encode_psystem : psystem -> Ast.system

val psystem_of_decls : pglobals:(Util.loc * Hstring.t * Smt.Type.t) list ->
       pconsts:(Util.loc * Hstring.t * Smt.Type.t) list ->
       parrays:(Util.loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list ->
       ptype_defs:(Util.loc * Ast.type_constructors) list ->
       pdecl list -> psystem

Pretty printing ASTs

val print_system : Format.formatter -> Ast.system -> unit