package dedukti
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c
doc/dedukti.api/Api/Meta/index.html
Module Api.MetaSource
Meta Dedukti
This file declares utilities which allows to use the rewrite rules of dedukti as a language to transform dedukti terms.
dkmeta also offers a way to reify the syntax of dedukti in dedukti. This refication can be used to get around the limitations of the rewrite engine offers par dedukti. Using a reification, one can rewrite a product for example. The reification process is extensible in a way that any user of the library can write its own reification function.
Reification
A shallow encoding of products. This encoding allows to rewrite products.
Meta configuration
The cfg type parameterise how the meta rewrite rules will act on dedukti terms.
If meta_rules is None then there is no meta rewrite rule but the strong normal form of every term will be computed.
If meta-rules is Some rules then all the terms will be normalised according to this set of rewrite rules.
Beta-reduction can be deactivated by setting beta to false.
If encoding is Some (module E) then the term will be reified according the function E.encode_term before being normalised.
If decoding is false then after normalising terms, the term won't be unreified.
If register_before is set to false, terms will be registered in the signatured only after being normalised and reified if applicable. This aims to be used for terms which are not well-typed before normalisation but are after normalisation. This can be used to implement macros for example.
The environment contains the internal representation of all the meta rewrite rules. This module maintains an invariant that the environment is consistent with the set of rewrite rules.
val default_config :
?meta_rules:Kernel.Rule.partially_typed_rule list ->
?beta:bool ->
?encoding:(module ENCODING) ->
?decoding:bool ->
?register_before:bool ->
unit ->
cfgInitliaze a configuration with the following parameters: meta_rules = None beta = true encoding = None decoding = true register_before = true
add_rules cfg rules add the rules to the meta configuration.
A processor which processes files containing the meta rewrite-rules. It is assumed that such file contains only rewrite rules.
The processor associated to MetaConfiguration.
parse_meta_files files returns the list of rules declares in the files files.
Meta processing
val make_meta_processor :
cfg ->
post_processing:(Env.t -> Parsers.Entry.entry -> unit) ->
(module Processor.S
with type t = unit)make_meta_processor cfg ~post_processing returns a processor which will normalise every entry according to the configuration cfg.
The function post_processing is called on each entry after being processed.
mk_term ?env cfg term normalize a term according to the configuration cfg. env is the environment used for type checking the term.
The env argument is mandatory if a safe encoding is used or if the normalisation strategy is done via the type checking environment (i.e. no meta rules were provided).
mk_entry cfg env entry processes an entry according the meta configuration cfg and the current environment env
Debugging/Logging
A debug flag to register logs specific for dkmeta.
A logging function for dkmeta.