Module Dolmen_model.Fun

module E = Dolmen.Std.Expr
exception Comparison_of_functional_values
exception Function_value_expected of Value.t
exception Bad_arity of E.Term.Const.t * int * Value.t list
exception Incomplete_ad_hoc_function of E.Term.Const.t
type value_function =
  1. | Lambda of {
    1. ty_params : E.Ty.Var.t list;
    2. term_params : E.Term.Var.t list;
    3. body : E.Term.t;
    }
  2. | Lazy of {
    1. arity : int;
    2. cst : E.Term.Const.t;
    3. eval_lazy : Env.t -> (Env.t -> E.term -> Value.t) -> E.term list -> Value.t;
    }
  3. | Poly of {
    1. arity : int;
    2. cst : E.Term.Const.t;
    3. eval_p : E.Ty.t list -> Value.t list -> Value.t;
    }
  4. | Ad_hoc of {
    1. arity : int;
    2. ty_arity : int;
    3. cst : E.Term.Const.t;
    4. eval_l : (E.Ty.t list * (E.Ty.subst -> value_function)) list;
    }
and t =
  1. | Closure of {
    1. func : value_function;
    2. tys : E.ty list;
    3. args : E.term list;
    }
val return : ('a, 'b, 'c, 'd, 'd, 'a) CamlinternalFormatBasics.format6 -> Stdlib.Format.formatter -> unit -> unit
val print_ad_hoc_case : Stdlib.Format.formatter -> (E.Ty.t list * 'a) -> unit
val print : Stdlib.Format.formatter -> t -> unit
val compare : 'a -> 'b -> 'c
val ops : t Value.ops
val mk_clos : value_function -> Value.t
val ad_hoc : cst:E.Term.Const.t -> arity:int -> ty_arity:int -> (E.Ty.t list * (E.Ty.subst -> value_function)) list -> value_function
val lambda : E.Ty.Var.t list -> E.Term.Var.t list -> E.Term.t -> value_function
val fun_lazy : cst:E.Term.Const.t -> (Env.t -> (Env.t -> E.term -> Value.t) -> E.term list -> Value.t) -> value_function
val poly : arity:int -> cst:E.Term.Const.t -> (E.Ty.t list -> Value.t list -> Value.t) -> value_function
val builtin : arity:int -> cst:E.Term.Const.t -> (Value.t list -> Value.t) -> value_function
val fun_1 : cst:E.Term.Const.t -> (Value.t -> Value.t) -> value_function
val fun_2 : cst:E.Term.Const.t -> (Value.t -> Value.t -> Value.t) -> value_function
val fun_3 : cst:E.Term.Const.t -> (Value.t -> Value.t -> Value.t -> Value.t) -> value_function
val fun_4 : cst:E.Term.Const.t -> (Value.t -> Value.t -> Value.t -> Value.t -> Value.t) -> value_function
val fun_n : cst:E.Term.Const.t -> (Value.t list -> Value.t) -> Value.t
val arity : value_function -> int
val add_ty_args : 'a list -> 'b list -> 'a list -> 'a list
val reduce_ty : eval:'a -> cst:E.Term.Const.t -> 'b -> E.Ty.t list -> (E.Ty.t list * (E.Ty.subst -> 'c)) list -> 'c
val reduce_val : eval:(Env.t -> E.Term.t -> Value.t) -> Env.t -> value_function -> E.Ty.t list -> Value.t list -> Value.t
val apply_val : eval:(Env.t -> E.Term.t -> Value.t) -> Env.t -> Value.t -> E.ty list -> Value.t list -> Value.t
val take_drop : int -> 'a list -> 'a list * 'a list
val reduce : eval:(Env.t -> E.term -> Value.t) -> Env.t -> value_function -> E.Ty.t list -> E.term list -> Value.t
val apply : eval:(Env.t -> E.term -> Value.t) -> Env.t -> Value.t -> E.ty list -> E.term list -> Value.t
val corner_case : ?post_check:(Value.t -> unit) -> eval:(Env.t -> E.Term.t -> Value.t) -> Env.t -> Dolmen.Std.Expr.Term.Const.t -> E.ty list -> Value.t list -> Value.t
val add_ad_hoc_instance : Dolmen_model__Model.t -> cst:Dolmen.Std.Expr.Term.Const.t -> ty_args:E.Ty.t list -> term_params:E.Term.Var.t list -> body:E.Term.t -> Dolmen_model__Model.t