dolmen_model 0.9 · 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

exception Incomplete_ad_hoc_function of E.Term.Const.t

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;
}
| Poly of {
1. arity : int;
2. cst : E.Term.Const.t;
3. eval_p : E.Ty.t list -> Value.t list -> Value.t;
}
| 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 =

| 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 ->
  Format.formatter ->
  unit ->
  unit

val print_ad_hoc_case : Format.formatter -> (E.Ty.t list * 'a) -> unit

val print : 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

package dolmen_model