lambdapi 2.5.1 · OCaml Package

Pretty-printing for the core AST.

The functions of this module are used for printing terms and other objects defined in the Term module. This is mainly used for displaying log messages, and feedback in case of success or error while type-checking terms or testing convertibility.

val log_prnt : 'a Lplib.Base.outfmt -> 'a

val sig_state : Sig_state.sig_state Timed.ref

Current signature state.

val notation_of : Term.sym -> float Sign.notation option

notation_of s returns the notation of symbol s or None.

val print_domains : bool Timed.ref

Flag for printing the domains of λ-abstractions.

val print_implicits : bool Timed.ref

Flag for printing implicit arguments.

val print_meta_types : bool Timed.ref

Flag for printing the type of uninstanciated metavariables. Remark: this does not generate parsable terms; use for debug only.

val print_contexts : bool Timed.ref

Flag for printing contexts in unification problems.

val print_meta_args : bool Timed.ref

Flag for printing metavariable arguments.

val assoc : Pratter.associativity Lplib.Base.pp

val notation : 'a Lplib.Base.pp -> 'a Sign.notation Lplib.Base.pp

val uid : string Lplib.Base.pp

val path : Common.Path.t Lplib.Base.pp

val prop : Term.prop Lplib.Base.pp

val expo : Term.expo Lplib.Base.pp

val match_strat : Term.match_strat Lplib.Base.pp

val do_not_qualify : bool Timed.ref

val without_qualifying : (unit -> 'a) -> 'a

val sym : Term.sym Lplib.Base.pp

val var : 'a Bindlib.var Lplib.Base.pp

exception Not_a_nat

Exception raised when trying to convert a term into a nat.

val nat_of_term : Term.term -> int

nat_of_term t converts a term into a natural number.

raises Not_a_nat
if this is not possible.

val are_quant_args : Term.term list -> bool

are_quant_args args returns true iff args has only one argument that is an abstraction.

type priority = [

| `Func
| `Appl
| `Atom

]

The possible priority levels are `Func (top level, including abstraction and product), `Appl (application) and `Atom (smallest priority).

val meta : Term.meta Lplib.Base.pp

val typ : Term.term Lplib.Base.pp

val term : Term.term Lplib.Base.pp

val term_in : Bindlib.ctxt -> Term.term Lplib.Base.pp

val prod : (Term.term * bool list) Lplib.Base.pp

val sym_rule : Term.sym_rule Lplib.Base.pp

val rule_of : Term.sym -> Term.rule Lplib.Base.pp

val unif_rule : Term.rule Lplib.Base.pp

val rules_of : Term.sym Lplib.Base.pp

val ctxt : Term.ctxt Lplib.Base.pp

val typing : Term.constr Lplib.Base.pp

val constr : Term.constr Lplib.Base.pp

val constrs : Term.constr list Lplib.Base.pp

val metaset : Core.Term.MetaSet.t Lplib.Base.pp

val problem : Term.problem Lplib.Base.pp

package lambdapi