dedukti 2.7 (latest) · OCaml Package

Basic Datatypes

Identifiers (hashconsed strings)

Internal representation of identifiers as hashconsed strings.

type ident

Type of identifiers (hash-consing)

val mk_ident : string -> ident

mkd_ident str casts a string str to an identifier

val ident_eq : ident -> ident -> bool

ident_eq id id' checks if the two identifiers id and id' are equals

val string_of_ident : ident -> string

string_of_ident id returns a string of the identifier id

type mident

type of module identifers

val mk_mident : string -> mident

mk_ident str casts a string str to an module identifier

val mident_eq : mident -> mident -> bool

mident_eq md md' checks if the two modules identifiers mid and mid' are equals

val string_of_mident : mident -> string

string_of_ident id returns a string of the identifier id

type name

type for constant names such as foo.bar

val md : name -> mident

md foo.bar returns foo

val id : name -> ident

id foo.bar returns bar

val mk_name : mident -> ident -> name

mk_name foo bar returns the identifier foo.bar

val name_eq : name -> name -> bool

name_eq n n' checks if the two names n and n' are equals

val dmark : ident

dmark is a special identifier for unification variables

The kernel may introduce such identifiers when creating new de Bruijn indices

module MidentSet : Set.S with type elt = mident

module IdentSet : Set.S with type elt = mident

module NameSet : Set.S with type elt = name

Lists with Length

A list where the method len is O(1). It is used by Matching.

module LList : sig ... end

Localization

type loc

Abstract type for a position (a line and a column) in a file

val dloc : loc

a dummy location

val mk_loc : int -> int -> loc

mk_loc l c builds the location where l is the line and c the column

of_loc l returns the line and the column associated to the position

val of_loc : loc -> int * int

Debug

module Debug : sig ... end

Misc

val fold_map : ('b -> 'a -> 'c * 'b) -> 'b -> 'a list -> 'c list * 'b

val bind_opt : ('a -> 'b option) -> 'a option -> 'b option

val map_opt : ('a -> 'b) -> 'a option -> 'b option

val split : int -> 'a list -> 'a list * 'a list

val rev_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list

val concat : 'a list -> 'a list -> 'a list

concat l1 l2 returns l1 @ l2 (testing on l2 empty first)

Printing functions

type 'a printer = Format.formatter -> 'a -> unit

Functions printing objects on the given formatter.

val string_of : 'a printer -> 'a -> string

Prints to a string

val pp_ident : ident printer

val pp_mident : mident printer

val pp_name : name printer

val pp_loc : loc printer

val pp_list : string -> 'a printer -> 'a list printer

val pp_llist : string -> 'a printer -> 'a LList.t printer

val pp_arr : string -> 'a printer -> 'a array printer

val pp_option : string -> 'a printer -> 'a option printer

Printing object with printer or default string when None.

val pp_lazy : 'a printer -> 'a Lazy.t printer

val pp_pair : 'a printer -> 'b printer -> ('a * 'b) printer

val pp_triple : 
  'a printer ->
  'b printer ->
  'c printer ->
  ('a * 'b * 'c) printer