Module `Kernel.Basic`Source

Basic Datatypes

Identifiers (hashconsed strings)

Internal representation of identifiers as hashconsed strings.

Sourcetype ident

Type of identifiers (hash-consing)

Sourceval mk_ident : string -> ident

mkd_ident str casts a string str to an identifier

Sourceval ident_eq : ident -> ident -> bool

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

Sourceval string_of_ident : ident -> string

string_of_ident id returns a string of the identifier id

Sourcetype mident

type of module identifers

Sourceval mk_mident : string -> mident

mk_ident str casts a string str to an module identifier

Sourceval mident_eq : mident -> mident -> bool

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

Sourceval string_of_mident : mident -> string

string_of_ident id returns a string of the identifier id

Sourcetype name

type for constant names such as foo.bar

Sourceval md : name -> mident

md foo.bar returns foo

Sourceval id : name -> ident

id foo.bar returns bar

Sourceval mk_name : mident -> ident -> name

mk_name foo bar returns the identifier foo.bar

Sourceval name_eq : name -> name -> bool

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

Sourceval dmark : ident

dmark is a special identifier for unification variables

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

Sourcemodule MidentSet : Set.S with type elt = mident

Sourcemodule IdentSet : Set.S with type elt = mident

Sourcemodule NameSet : Set.S with type elt = name

Lists with Length

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

Sourcemodule LList : sig ... end

Localization

Sourcetype loc

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

Sourceval dloc : loc

a dummy location

Sourceval 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

Sourceval of_loc : loc -> int * int

Debug

Sourcemodule Debug : sig ... end

Misc

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

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

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

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

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

Sourceval concat : 'a list -> 'a list -> 'a list

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

Printing functions

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

Functions printing objects on the given formatter.

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

Prints to a string

Sourceval pp_ident : ident printer

Sourceval pp_mident : mident printer

Sourceval pp_name : name printer

Sourceval pp_loc : loc printer

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

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

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

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

Printing object with printer or default string when None.

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

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

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dedukti.kernel/Kernel/Basic/index.html

Module `Kernel.Basic`Source

Identifiers (hashconsed strings)

Lists with Length

Localization

Debug

Misc

Printing functions

package dedukti

Install

Dune Dependency

Authors

Maintainers

Sources

doc/dedukti.kernel/Kernel/Basic/index.html

Module Kernel.BasicSource

Identifiers (hashconsed strings)

Lists with Length

Localization

Debug

Misc

Printing functions

Module `Kernel.Basic`Source