Module Kernel.ReductionSource

Term reduction and conversion test.

Sourceval d_reduce : Basic.Debug.flag
Sourcetype red_target =
  1. | Snf
  2. | Whnf
Sourcetype red_strategy =
  1. | ByName
  2. | ByValue
  3. | ByStrongValue
Sourcetype dtree_finder = Signature.t -> Basic.loc -> Basic.name -> Dtree.t
Sourcetype red_cfg = {
  1. select : (Rule.rule_name -> bool) option;
  2. nb_steps : int option;
  3. target : red_target;
  4. strat : red_strategy;
  5. beta : bool;
  6. logger : Term.position -> Rule.rule_name -> Term.term Lazy.t -> Term.term Lazy.t -> unit;
  7. 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 Default : S