Module Print

Ascii Printing

module String : sig ... end
type print_mode =
| TeX
| Gml
| Asc

control some differences when printing for LaTeX or GraphML

val sanitize_name : string -> string
val print_mode : print_mode Stdlib.ref
val show_occur : bool Stdlib.ref
val latex_mode : unit -> bool
val lts : unit -> string
val lt : Stdlib.Format.formatter -> unit
val print_redex_as_let : bool Stdlib.ref
val break_hint : int Stdlib.ref

break_hint allows line breaking for record, ... It gives the number of nested records whose lines are breaked

val ignore_witness : bool Stdlib.ref

ignore witness in subtyping proofs

val is_tuple : (string * 'a) list -> bool

test if a list of record fields is a tuple

val ordi_count : int Stdlib.ref

Managment of a table to name all choice constants (for ordinals, terms and type) when printing. terms and ordinals are named the first time they are printed. The table of all names and definition can be printer later.

val ordi_tbl : (Ast.ordi * (Ast.ordi * bool)) list Stdlib.ref
val epsilon_term_tbl : (Ast.term * (Ast.term' Pos.loc * string * int)) list Stdlib.ref
val epsilon_type_tbl : ((Ast.kind, Ast.kind) LibTools.Bindlib.binder * (string * int * Ast.term * bool)) list Stdlib.ref
val reset_epsilon_tbls : unit -> unit
val search_type_tbl : Ast.term -> (Ast.kind, Ast.kind) LibTools.Bindlib.binder -> bool -> string * int
val search_term_tbl : Ast.term -> ('a, 'b) LibTools.Bindlib.binder -> Ast.term' Pos.loc * string * int
val search_ordi_tbl : Ast.ordi -> Ast.ordi
val unsugar_pattern : string -> string -> Ast.sugar -> Ast.term' Pos.loc -> string * Ast.term' Pos.loc
val has_kvar : Ast.kind -> bool

A test to avoid capture in match_kind below

val match_kind : Ast.kuvar list -> Ast.ouvar list -> Ast.kind -> Ast.kind -> bool

Matching kind and ordinals, used for printing only, in order to factorise definittion.

val match_ordi : Ast.ouvar list -> Ast.ordi -> Ast.ordi -> bool
val try_fold_def : Ast.kind -> Ast.kind
val print_index_ordi : Stdlib.Format.formatter -> Ast.ordi -> unit
val print_occur : Stdlib.Format.formatter -> Ast.occur -> unit
val pkind_def : bool -> Stdlib.Format.formatter -> Ast.kdef -> unit
val term_to_string : bool -> Ast.term -> string
val ordi_to_string : bool -> Ast.ordi -> string
val kind_to_string : bool -> Ast.kind -> string
val sub_used_ind : (Ast.ordi list * Ast.term * Ast.kind * Ast.kind * Ast.sub_rule) -> Sct.index list
val typ_used_ind : (Ast.ordi list * Ast.term * Ast.kind * Ast.typ_rule) -> Sct.index list
val is_refl : Ast.sub_prf -> bool
val mkSchema : ?ord_name:string -> Ast.schema -> string
val print_schema : ?ord_name:string -> Stdlib.Format.formatter -> Ast.schema -> unit
val sub2proof : Ast.sub_prf -> string Proof.proof
val typ2proof : Ast.typ_prf -> string Proof.proof
val print_typing_proof : Stdlib.Format.formatter -> Ast.typ_prf -> unit
val print_subtyping_proof : Stdlib.Format.formatter -> Ast.sub_prf -> unit
val print_term : ?unfolded_Y:(Ast.term', Ast.term) LibTools.Bindlib.binder list option -> ?give_pos:bool -> bool -> Stdlib.Format.formatter -> Ast.term -> unit
val print_kind : bool -> Stdlib.Format.formatter -> Ast.kind -> unit
val kind : Stdlib.Format.formatter -> Ast.kind -> unit
val term : Stdlib.Format.formatter -> Ast.term -> unit
val print_kind_def : bool -> Stdlib.Format.formatter -> Ast.kdef -> unit
val print_ordi : bool -> Stdlib.Format.formatter -> Ast.ordi -> unit
val print_ordis : Stdlib.Format.formatter -> Ast.ordi list -> unit
val print_position : Stdlib.Format.formatter -> Pos.pos option -> unit
val print_epsilon_tbls : Stdlib.Format.formatter -> unit
exception Find_tdef of Ast.kdef
val find_tdef : Ast.kind -> Ast.kdef
val ordi_to_printer : ('a * Ast.ordi) -> Stdlib.Format.formatter -> unit