package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

An implementation of The Lambda-Pi Modulo Theory

Install

Dune Dependency

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

Authors

D

dedukti-dev@inria.fr

Maintainers

D

dedukti-dev@inria.fr

Sources

v2.7.tar.gz

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

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

Module `Kernel.Reduction`Source

Term reduction and conversion test.

Sourceval d_reduce : Basic.Debug.flag

Sourcetype red_target =

| Snf
| Whnf

Sourcetype red_strategy =

| ByName
| ByValue
| ByStrongValue

Sourcetype dtree_finder = Signature.t -> Basic.loc -> Basic.name -> Dtree.t

Sourcetype red_cfg = {

select : (Rule.rule_name -> bool) option;
nb_steps : int option;
target : red_target;
strat : red_strategy;
beta : bool;
logger : Term.position -> Rule.rule_name -> Term.term Lazy.t -> Term.term Lazy.t -> unit;
finder : dtree_finder;

}

Configuration for reduction. select = Some f restreins rules according to the given filter on names. select = None is the default behaviour (all rules allowed). nb_steps = Some n Allows only n reduction steps. nb_steps = None is the default behaviour. target is the normal form to compute. strat is the reduction strategy. beta flag enables/disables beta reductions. logger is the function to call upon applying a reduction rule. finder specifies where to find the decision tree.

Sourceval pp_red_cfg : red_cfg Basic.printer

Sourceval default_cfg : red_cfg

default configuration where:

select = None
nb_steps = None
strategy = ByName
target = Snf
beta = true
logger = fun _ _ _ -> ()
finder = Signature.get_dtree

Sourceval eta : bool ref

Set to true to allow eta expansion at conversion check

Sourceexception Not_convertible

Sourcetype convertibility_test = Signature.t -> Term.term -> Term.term -> bool

Sourceval selection : (Rule.rule_name -> bool) option ref

This predicate restrict the rules which can be used by the rewrite engine. Default is None meaning that every rules in Signature are used

Sourcemodule type ConvChecker = sig ... end

Sourcemodule type S = sig ... end

Sourcemodule Make (C : ConvChecker) (M : Matching.Matcher) : S

Sourcemodule Default : S