package dedukti
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c
doc/dedukti.kernel/Kernel/Signature/index.html
Module Kernel.SignatureSource
Global Environment
type signature_error = | UnmarshalBadVersionNumber of Basic.loc * file| UnmarshalSysError of Basic.loc * file * string| UnmarshalUnknown of Basic.loc * file| SymbolNotFound of Basic.loc * Basic.name| AlreadyDefinedSymbol of Basic.loc * Basic.name| CannotMakeRuleInfos of Rule.rule_error| CannotBuildDtree of Dtree.dtree_error| CannotAddRewriteRules of Basic.loc * Basic.name| ConfluenceErrorImport of Basic.loc * Basic.mident * Confluence.confluence_error| ConfluenceErrorRules of Basic.loc * Rule.rule_infos list * Confluence.confluence_error| GuardNotSatisfied of Basic.loc * Term.term * Term.term| CannotExportModule of Basic.mident * exn| PrivateSymbol of Basic.loc * Basic.name| ExpectedACUSymbol of Basic.loc * Basic.name
Wrapper exception for errors occuring while handling a signature.
type staticity = | Static| Definable of Term.algebra| Injective(*Is the symbol allowed to have rewrite rules or not ? And if it has, can it be considered injective by the type-checker ?
*)
A collection of well-typed symbols and rewrite rules.
make file creates a new signature corresponding to the file file.
get_name sg returns the name of the signature sg.
export sg oc saves the current environment in oc file.
import sg sg_ext imports the signature sg_ext into the signature sg.
is_static sg l cst is true when cst is a static symbol.
is_injective sg l cst is true when cst is either static or declared as injective.
get_type sg l md id returns the type of the constant md.id inside the environement sg.
get_staticity sg l md id returns the staticity of the symbol md.id
get_algebra sg l md id returns the algebra of the symbol md.id.
get_neutral sg l md id returns the neutral element of the ACU symbol md.id.
is_AC sg l na returns true when na is declared as AC symbol
import sg md the module md in the signature sg.
get_dtree sg filter l cst returns the decision/matching tree associated with cst inside the environment sg.
get_rules sg lc cst returns a list of rules that defines the symbol.
val add_external_declaration :
t ->
Basic.loc ->
Basic.name ->
scope ->
staticity ->
Term.term ->
unitadd_external_declaration sg l cst sc st ty declares the symbol id of type ty, scope sc and staticity st in the environment sg.
val add_declaration :
t ->
Basic.loc ->
Basic.ident ->
scope ->
staticity ->
Term.term ->
unitadd_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
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.
type rw_infos = {stat : staticity;(*Whether a symbol is definable
*)ty : Term.term;(*The type of a symbol
*)scope : scope;(*The scope of the symbol (
*)Public/Private)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
*)decision_tree : Dtree.t option;(*The decision tree computed for the set of rules declared above
*)
}fold_symbols f sg t folds the function f on all symbol_infos in the signature starting from t.
iter_symbols f sg iters the function f on all symbol_infos in the signature.