package dedukti

  1. Overview
  2. Docs
An implementation of The Lambda-Pi Modulo Theory

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

  1. D
    dedukti-dev@inria.fr

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

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

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