Module Ptree_helpers

module Ptree_helpers: sig .. end

Helpers for constructing program with the parse tree API

identifiers

val ident : ?attrs:Why3.Ptree.attr list ->
       ?loc:Why3.Loc.position -> string -> Why3.Ptree.ident

ident ?attr ?loc s produce the identifier named s optionally with the given attributes and source location

val qualid : string list -> Why3.Ptree.qualid

qualid l produces the qualified identifier given by the path l, a list in the style of ["int";"Int"]

val const : ?kind:Why3.Number.int_literal_kind -> int -> Why3.Constant.constant

val unit_binder : ?loc:Why3.Loc.position -> unit -> Why3.Ptree.binder list

val one_binder : ?loc:Why3.Loc.position ->
       ?ghost:bool -> ?pty:Why3.Ptree.pty -> string -> Why3.Ptree.binder list

terms and formulas

val term : ?loc:Why3.Loc.position -> Why3.Ptree.term_desc -> Why3.Ptree.term

val tconst : ?loc:Why3.Loc.position -> int -> Why3.Ptree.term

val tvar : ?loc:Why3.Loc.position -> Why3.Ptree.qualid -> Why3.Ptree.term

val tapp : ?loc:Why3.Loc.position ->
       Why3.Ptree.qualid -> Why3.Ptree.term list -> Why3.Ptree.term

val pat : ?loc:Why3.Loc.position -> Why3.Ptree.pat_desc -> Why3.Ptree.pattern

val pat_var : ?loc:Why3.Loc.position -> Why3.Ptree.ident -> Why3.Ptree.pattern

program expressions

val break_id : string

val continue_id : string

val return_id : string

val expr : ?loc:Why3.Loc.position -> Why3.Ptree.expr_desc -> Why3.Ptree.expr

val econst : ?loc:Why3.Loc.position -> int -> Why3.Ptree.expr

val eapp : ?loc:Why3.Loc.position ->
       Why3.Ptree.qualid -> Why3.Ptree.expr list -> Why3.Ptree.expr

val eapply : ?loc:Why3.Loc.position ->
       Why3.Ptree.expr -> Why3.Ptree.expr -> Why3.Ptree.expr

val evar : ?loc:Why3.Loc.position -> Why3.Ptree.qualid -> Why3.Ptree.expr

val empty_spec : Why3.Ptree.spec

declarations

val use : ?loc:Why3.Loc.position -> import:bool -> string list -> Why3.Ptree.decl

use l produces the equivalent of "use (import) path" where path is denoted by l

val global_var_decl : Why3.Ptree.pty -> string -> Why3.Ptree.ident * Why3.Ptree.decl

global_var_decl ty id declares a global mutable variable `id` of type `ty`. It returns both the variable identifier and the declaration itself

Declarations in top-down style

The following helpers allows one to create modules, declarations inside modules, and program functions in a top-down style, instead of the bottom-up style above

This extra layer commes into two flavors, a functional one, or say a monadic style, with an explicit state of declarations under constructions ; and an imperative style.

module F: sig .. end

Extra helpers for creating declarations in top-down style, functional interface

module I: sig .. end

Extra helpers for creating declarations in top-down style, imperative interface.