Module Term.Model

type fi = {
fi_ty_args : Type.t list;
fi_ty_ret : Type.t;
fi_cases : (term list * term) list;
fi_else : term;
}

function interpretation

type t = {
tys : (Type.t * term list) list;

interpretation of types

consts : (Var.t * term) list;

interpretation of variables

funs : (Var.t * fi) list;

functions

}
val empty : t
val make_fi : Var.t -> (term list * term) list -> default:term -> fi

make_fi f cases ~default builds a ite-tree from cases and default

val make : ?⁠tys:(Type.t * term list) list -> ?⁠funs:(Var.t * fi) list -> consts:(Var.t * term) list -> unit -> t
val term_of_fi : fi -> term

Make a lambda term from the function interpretation

val find_const : Var.t -> t -> term
raises Not_found

if not present

val get_const : Var.t -> t -> term option
val find_fun : Var.t -> t -> fi
raises Not_found

if not present

val get_fun : Var.t -> t -> fi option
val consts_list : t -> (Var.t * term) list
type entry =
| C of term
| F of fi
val to_list : t -> (Var.t * term) list
val to_list_full : t -> (Var.t * entry) list
val print_fi : fi CCFormat.printer
val print : t CCFormat.printer
val to_ocaml_code : t -> string