package dedukti

  1. Overview
  2. Docs
package dedukti
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Kernel.BasicSource

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
Sourceval pp_triple : 'a printer -> 'b printer -> 'c printer -> ('a * 'b * 'c) printer
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct