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
Term reduction and conversion test.
val d_reduce : Basic.Debug.flagtype dtree_finder = Signature.t -> Basic.loc -> Basic.name -> Dtree.ttype 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.
val pp_red_cfg : red_cfg Basic.printerval default_cfg : red_cfgdefault configuration where:
select=Nonenb_steps=Nonestrategy=ByNametarget=Snfbeta=truelogger=fun _ _ _ -> ()finder=Signature.get_dtree
val eta : bool refSet to true to allow eta expansion at conversion check
type convertibility_test = Signature.t -> Term.term -> Term.term -> boolval selection : (Rule.rule_name -> bool) option refThis predicate restrict the rules which can be used by the rewrite engine. Default is None meaning that every rules in Signature are used
module type ConvChecker = sig ... endmodule type S = sig ... endmodule Make (C : ConvChecker) (M : Matching.Matcher) : S