Module `Core.Print`Source

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.

Sourceval log : 'a Lplib.Base.outfmt -> 'a

Sourceval sig_state : Sig_state.sig_state Timed.ref

Current signature state.

Sourceval print_domains : bool Timed.ref

Flag for printing the domains of λ-abstractions.

Sourceval print_implicits : bool Timed.ref

Flag for printing implicit arguments.

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

Sourceval print_contexts : bool Timed.ref

Flag for printing contexts in unification problems.

Sourceval print_meta_args : bool Timed.ref

Flag for printing metavariable arguments.

Source

val safe_unbind_no_check : 
  int Lplib.Extra.StrMap.t ->
  Term.binder ->
  (Term.var * Term.term) * int Lplib.Extra.StrMap.t

Source

val safe_unbind : 
  int Lplib.Extra.StrMap.t ->
  Term.binder ->
  (Term.var * Term.term) * int Lplib.Extra.StrMap.t

Sourceval assoc : Pratter.associativity Lplib.Base.pp

Sourceval notation : 'a Lplib.Base.pp -> 'a Term.notation Lplib.Base.pp

Sourceval uid : string Lplib.Base.pp

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

Sourceval prop : Term.prop Lplib.Base.pp

Sourceval expo : Term.expo Lplib.Base.pp

Sourceval match_strat : Term.match_strat Lplib.Base.pp

Sourceval do_not_qualify : bool Timed.ref

Sourceval no_qualif : (unit -> 'a) -> 'a

Sourceval sym : Term.sym Lplib.Base.pp

Sourceval var : Term.var Lplib.Base.pp

Sourceval meta : Term.meta Lplib.Base.pp

Sourceexception Not_a_nat

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

Sourceval builtin : Lplib.Extra.StrMap.key -> Term.sym

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

Sourceval pos_of_term : Term.term -> int

pos_of_term t converts a term into a positive number.

raises Not_a_nat
if this is not possible.

Sourceval int_of_term : Term.term -> int

int_of_term t converts a term into a positive number.

raises Not_a_nat
if this is not possible.

Sourceval are_quant_args : Term.term list -> bool

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

Sourcetype priority = [

| `Func
| `Appl
| `Atom

]

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

Source

val pp : 
  [> `Appl | `Atom | `Func ] ->
  int Lplib.Extra.StrMap.t ->
  Format.formatter ->
  Term.term ->
  unit

Source

val quantifier : 
  int Lplib.Extra.StrMap.t ->
  Format.formatter ->
  Term.sym ->
  Term.term list ->
  unit

Source

val head : 
  int Lplib.Extra.StrMap.t ->
  bool ->
  Format.formatter ->
  Term.term ->
  unit

Source

val abstractions : 
  int Lplib.Extra.StrMap.t ->
  Format.formatter ->
  Term.term ->
  unit

Sourceval typ_in : int Lplib.Extra.StrMap.t -> Term.term Lplib.Base.pp

Sourceval atom : int Lplib.Extra.StrMap.t -> Format.formatter -> Term.term -> unit

Sourceval appl : int Lplib.Extra.StrMap.t -> Format.formatter -> Term.term -> unit

Sourceval func : int Lplib.Extra.StrMap.t -> Term.term Lplib.Base.pp

Sourceval term_in : int Lplib.Extra.StrMap.t -> Term.term Lplib.Base.pp

Sourceval term : Term.term Lplib.Base.pp

Sourceval env : Format.formatter -> Term.term array -> unit

Sourceval prod_in : int Lplib.Extra.StrMap.t -> (Term.term * bool list) Lplib.Base.pp

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

Sourceval sym_type : Format.formatter -> Term.sym -> unit

Sourceval sym_rule : Term.sym_rule Lplib.Base.pp

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

Sourceval unif_rule : Term.rule Lplib.Base.pp

Sourceval rules_of : Term.sym Lplib.Base.pp

Sourceval typ : Term.term Lplib.Base.pp

Sourceval ctxt : Term.ctxt Lplib.Base.pp

Sourceval typing : Term.constr Lplib.Base.pp

Sourceval constr : Term.constr Lplib.Base.pp

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

Sourceval metaset : Term.MetaSet.t Lplib.Base.pp

Sourceval problem : Term.problem Lplib.Base.pp

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/lambdapi.core/Core/Print/index.html

Module `Core.Print`Source

package lambdapi

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/lambdapi.core/Core/Print/index.html

Module Core.PrintSource

dune-project
Dependency

Module `Core.Print`Source