Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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
module type ENCODING = sig ... endThe signature which implements a reification function.
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
val add_rules : cfg -> Kernel.Rule.partially_typed_rule list -> unitadd_rules cfg rules add the rules to the meta configuration.
module MetaConfiguration :
Processor.S with type t = Kernel.Rule.partially_typed_rule listA processor which processes files containing the meta rewrite-rules. It is assumed that such file contains only rewrite rules.
The processor associated to MetaConfiguration.
val parse_meta_files : string list -> Kernel.Rule.partially_typed_rule listparse_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.
val mk_term : ?env:Env.t -> cfg -> Kernel.Term.term -> Kernel.Term.termmk_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).
val mk_entry : cfg -> Env.t -> Parsers.Entry.entry -> Parsers.Entry.entrymk_entry cfg env entry processes an entry according the meta configuration cfg and the current environment env
Debugging/Logging
val debug_flag : Kernel.Basic.Debug.flagA debug flag to register logs specific for dkmeta.
val log : ('a, Format.formatter, unit, unit) format4 -> 'aA logging function for dkmeta.