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
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. | Parametric of {
    1. arity : int;
    2. cst : E.Term.Const.t;
    3. ty_args : E.Ty.t list;
    4. eval_p : Value.t list -> Value.t;
    }
and t =
  1. | Partial of {
    1. func : value_function;
    2. args : E.term list;
    }
  2. | Ad_hoc of {
    1. cst : E.Term.Const.t;
    2. ty_args : E.Ty.t list;
    3. eval_a : E.Ty.t -> Value.t;
    }
val return : ('a, 'b, 'c, 'd, 'e, 'f) CamlinternalFormatBasics.format6 -> Stdlib.Format.formatter -> unit -> unit
val print : Stdlib.Format.formatter -> t -> unit
val compare : 'a -> 'b -> 'c
val ops : t Value.ops
val ad_hoc : cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (E.Ty.t -> Value.t) -> Value.t
val mk : env:'a -> eval:('b -> E.Term.t -> Value.t) -> E.Ty.Var.t list -> E.Term.Var.t list -> E.Term.t -> Value.t
val builtin : arity:int -> cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (Value.t list -> Value.t) -> Value.t
val fun_1 : cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (Value.t -> Value.t) -> Value.t
val fun_2 : cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (Value.t -> Value.t -> Value.t) -> Value.t
val fun_3 : cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (Value.t -> Value.t -> Value.t -> Value.t) -> Value.t
val fun_4 : cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (Value.t -> Value.t -> Value.t -> Value.t -> Value.t) -> Value.t
val fun_n : cst:E.Term.Const.t -> ?ty_args:E.Ty.t list -> (Value.t list -> Value.t) -> Value.t
val fun_lazy : cst:E.Term.Const.t -> (Env.t -> (Env.t -> E.term -> Value.t) -> E.term list -> Value.t) -> Value.t
val arity : value_function -> int
val reduce_val : eval:(Env.t -> E.Term.t -> Value.t) -> Env.t -> value_function -> Value.t list -> Value.t
val apply_val : eval:(Env.t -> E.Term.t -> Value.t) -> Env.t -> Value.t -> 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.term list -> Value.t
val apply : eval:(Env.t -> E.term -> Value.t) -> Env.t -> Value.t -> E.Ty.t list -> E.term list -> Value.t