Kernel.ReductionSourceTerm reduction and conversion test.
type 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.
default configuration where:
select = Nonenb_steps = Nonestrategy = ByNametarget = Snfbeta = truelogger = fun _ _ _ -> ()finder = Signature.get_dtreeThis predicate restrict the rules which can be used by the rewrite engine. Default is None meaning that every rules in Signature are used