Module Ptree_helpers

module Ptree_helpers: sig .. end

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 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

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

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
module I: sig .. end