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 =
| Lambda of {
ty_params : E.Ty.Var.t list;
term_params : E.Term.Var.t list;
body : E.Term.t;
}
| Lazy of {
arity : int;
cst : E.Term.Const.t;
eval_lazy : Env.t -> ( Env.t -> E.term -> Value.t ) -> E.term list -> Value.t;
}
| Parametric of {
arity : int;
cst : E.Term.Const.t;
ty_args : E.Ty.t list;
eval_p : Value.t list -> Value.t;
}
and t =
| Partial of {
func : value_function;
args : E.term list;
}
| Ad_hoc of {
cst : E.Term.Const.t;
ty_args : E.Ty.t list;
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