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/Signature/index.html

Module Kernel.SignatureSource

Global Environment

Sourceval d_module : Basic.Debug.flag
Sourcetype file = string
Sourcetype signature_error =
  1. | UnmarshalBadVersionNumber of Basic.loc * file
  2. | UnmarshalSysError of Basic.loc * file * string
  3. | UnmarshalUnknown of Basic.loc * file
  4. | SymbolNotFound of Basic.loc * Basic.name
  5. | AlreadyDefinedSymbol of Basic.loc * Basic.name
  6. | CannotMakeRuleInfos of Rule.rule_error
  7. | CannotBuildDtree of Dtree.dtree_error
  8. | CannotAddRewriteRules of Basic.loc * Basic.name
  9. | ConfluenceErrorImport of Basic.loc * Basic.mident * Confluence.confluence_error
  10. | ConfluenceErrorRules of Basic.loc * Rule.rule_infos list * Confluence.confluence_error
  11. | GuardNotSatisfied of Basic.loc * Term.term * Term.term
  12. | CannotExportModule of Basic.mident * exn
  13. | PrivateSymbol of Basic.loc * Basic.name
  14. | ExpectedACUSymbol of Basic.loc * Basic.name
Sourceexception Signature_error of signature_error

Wrapper exception for errors occuring while handling a signature.

Sourcetype staticity =
  1. | Static
  2. | Definable of Term.algebra
  3. | Injective
    (*

    Is the symbol allowed to have rewrite rules or not ? And if it has, can it be considered injective by the type-checker ?

    *)
Sourcetype scope =
  1. | Public
  2. | Private
    (*

    Should the symbol be accessible from outside its definition file ?

    *)
Sourcetype t

A collection of well-typed symbols and rewrite rules.

make file creates a new signature corresponding to the file file.

Sourceval get_name : t -> Basic.mident

get_name sg returns the name of the signature sg.

Sourceval export : t -> out_channel -> unit

export sg oc saves the current environment in oc file.

Sourceval get_id_comparator : t -> Basic.name Term.comparator
Sourceval import_signature : t -> t -> unit

import sg sg_ext imports the signature sg_ext into the signature sg.

Sourceval is_static : t -> Basic.loc -> Basic.name -> bool

is_static sg l cst is true when cst is a static symbol.

Sourceval is_injective : t -> Basic.loc -> Basic.name -> bool

is_injective sg l cst is true when cst is either static or declared as injective.

Sourceval get_type : t -> Basic.loc -> Basic.name -> Term.term

get_type sg l md id returns the type of the constant md.id inside the environement sg.

Sourceval get_staticity : t -> Basic.loc -> Basic.name -> staticity

get_staticity sg l md id returns the staticity of the symbol md.id

Sourceval get_algebra : t -> Basic.loc -> Basic.name -> Term.algebra

get_algebra sg l md id returns the algebra of the symbol md.id.

Sourceval get_neutral : t -> Basic.loc -> Basic.name -> Term.term

get_neutral sg l md id returns the neutral element of the ACU symbol md.id.

Sourceval is_AC : t -> Basic.loc -> Basic.name -> bool

is_AC sg l na returns true when na is declared as AC symbol

Sourceval import : t -> Basic.loc -> Basic.mident -> unit

import sg md the module md in the signature sg.

Sourceval get_dtree : t -> Basic.loc -> Basic.name -> Dtree.t

get_dtree sg filter l cst returns the decision/matching tree associated with cst inside the environment sg.

Sourceval get_rules : t -> Basic.loc -> Basic.name -> Rule.rule_infos list

get_rules sg lc cst returns a list of rules that defines the symbol.

Sourceval add_external_declaration : t -> Basic.loc -> Basic.name -> scope -> staticity -> Term.term -> unit

add_external_declaration sg l cst sc st ty declares the symbol id of type ty, scope sc and staticity st in the environment sg.

Sourceval add_declaration : t -> Basic.loc -> Basic.ident -> scope -> staticity -> Term.term -> unit

add_declaration sg l id sc st ty declares the symbol id of type ty and staticity st in the environment sg. If sc is Private then the symbol cannot be used in other modules

Sourceval add_rules : t -> Rule.rule_infos list -> unit

add_rules sg rule_lst adds a list of rule to a symbol in the environement sg. All rules must be on the same symbol.

Sourcetype rw_infos = {
  1. stat : staticity;
    (*

    Whether a symbol is definable

    *)
  2. ty : Term.term;
    (*

    The type of a symbol

    *)
  3. scope : scope;
    (*

    The scope of the symbol (Public/Private)

    *)
  4. rules : Rule.rule_infos list;
    (*

    The stack pile of rules associated to a symbol. They are imported in the signature in the order by they are declared within the file

    *)
  5. decision_tree : Dtree.t option;
    (*

    The decision tree computed for the set of rules declared above

    *)
}
Sourceval get_rw_infos : t -> Basic.mident -> Basic.ident -> rw_infos option
Sourceval fold_symbols : (Basic.mident -> Basic.ident -> rw_infos -> 'a -> 'a) -> t -> 'a -> 'a

fold_symbols f sg t folds the function f on all symbol_infos in the signature starting from t.

Sourceval iter_symbols : (Basic.mident -> Basic.ident -> rw_infos -> unit) -> t -> unit

iter_symbols f sg iters the function f on all symbol_infos in the signature.