Module Model.DT_util

module DT_util: sig .. end

type term = TermInner.Default.t

type dt = (term, term) Model.DT.t

type subst = (term, term) Var.Subst.t

val ite : term Var.t ->
       then_:dt -> else_:dt -> dt

val eval_subst : subst:subst -> dt -> dt

Eval the tree with the given substitution (which does not capture the tree's variables)
Raises Assert_failure if the substitution binds some of dt's variables

val map_vars : subst:(term, term Var.t) Var.Subst.t ->
       dt -> dt

Apply the substitution to the tree's variables and terms

val rename_vars : dt -> dt

Rename all variables in dt

val apply : dt -> term -> dt

apply dt arg returns the sub-tree of dt for when dt's variable is equal to arg.
Raises Invalid_argument if the dt is not a function

val apply_l : dt -> term list -> dt

apply the dt to a list of arguments
Raises Invalid_argument if the dt is not a function with enough arguments

val join : dt -> dt -> dt

join a b applies b to every leaf of a, grafting the resulting sub-tree in place of the leaf, using Model.DT_util.apply.

assumes the return type of a is the same as the first argument of b.

val merge : dt -> dt -> dt

merge a b concatenates the cases of a and b, merging the common cases recursively, favoring a over b when needed. The new default/else is a.default.

not commutative.

val merge_l : dt list -> dt

n-ary version of Model.DT_util.merge
Raises Invalid_argument if the list is empty

val reorder : term Var.t list -> dt -> dt

reorder vars dt rebalances dt so it has the given order of variables. It is assumed that vars is a permutation of DT.vars dt
Raises Invalid_argument if vars is not a permutation of the variables of dt

val remove_vars : term Var.t list -> dt -> dt

Remove the given variables, using Model.DT_util.merge_l to merge their sub-cases. If those variables occur in tests in variables that come earlier in DT.vars dt, they will not be substituted properly

val remove_first_var : dt -> dt

remove the first variable, using Model.DT_util.remove_vars.
Raises Invalid_argument if the tree is constant

exception Case_not_found of term

val find_cases : ?subst:subst ->
       term ->
       (term, term) Model.DT.cases ->
       subst * dt

Raises Case_not_found if the term is not found

val to_term : dt -> term

Convert the decision tree to a term

val print : dt Model.printer