dolmen_model 0.8 · OCaml Package

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 {
1. ty_params : E.Ty.Var.t list;
2. term_params : E.Term.Var.t list;
3. body : E.Term.t;
}
| 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;
}
| 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 =

| Partial of {
1. func : value_function;
2. args : E.term list;
}
| 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, 'd, 'a) CamlinternalFormatBasics.format6 ->
  Format.formatter ->
  unit ->
  unit

val print : 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:('a -> 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

package dolmen_model