Module Ptree_helpers

module Ptree_helpers: sig .. end

Helpers for constructing program with the parse tree API

identifiers

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

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

val qualid : string list -> Ptree.qualid

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

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

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

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

terms and formulas

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

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

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

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

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

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

program expressions

val break_id : string

val continue_id : string

val return_id : string

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

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

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

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

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

val empty_spec : Ptree.spec

declarations

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

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

val global_var_decl : Ptree.pty -> string -> Ptree.ident * 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.