Module `Dolmen_model.Fun`Source

Sourcemodule E = Dolmen.Std.Expr

Sourceexception Comparison_of_functional_values

Sourceexception Function_value_expected of Value.t

Sourceexception Bad_arity of E.Term.Const.t * int * Value.t list

Sourceexception Incomplete_ad_hoc_function of E.Term.Const.t

Sourcetype 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;
}

Sourceand t =

| Closure of {
1. func : value_function;
2. tys : E.ty list;
3. args : E.term list;
}

Source

val return : 
  ('a, 'b, 'c, 'd, 'd, 'a) CamlinternalFormatBasics.format6 ->
  Format.formatter ->
  unit ->
  unit

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

Sourceval print : Format.formatter -> t -> unit

Sourceval compare : 'a -> 'b -> 'c

Sourceval ops : t Value.ops

Sourceval mk_clos : value_function -> Value.t

Source

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

Sourceval lambda : E.Ty.Var.t list -> E.Term.Var.t list -> E.Term.t -> value_function

Source

val fun_lazy : 
  cst:E.Term.Const.t ->
  (Env.t -> (Env.t -> E.term -> Value.t) -> E.term list -> Value.t) ->
  value_function

Source

val poly : 
  arity:int ->
  cst:E.Term.Const.t ->
  (E.Ty.t list -> Value.t list -> Value.t) ->
  value_function

Source

val builtin : 
  arity:int ->
  cst:E.Term.Const.t ->
  (Value.t list -> Value.t) ->
  value_function

Sourceval fun_1 : cst:E.Term.Const.t -> (Value.t -> Value.t) -> value_function

Source

val fun_2 : 
  cst:E.Term.Const.t ->
  (Value.t -> Value.t -> Value.t) ->
  value_function

Source

val fun_3 : 
  cst:E.Term.Const.t ->
  (Value.t -> Value.t -> Value.t -> Value.t) ->
  value_function

Source

val fun_4 : 
  cst:E.Term.Const.t ->
  (Value.t -> Value.t -> Value.t -> Value.t -> Value.t) ->
  value_function

Sourceval fun_n : cst:E.Term.Const.t -> (Value.t list -> Value.t) -> Value.t

Sourceval arity : value_function -> int

Sourceval add_ty_args : 'a list -> 'b list -> 'a list -> 'a list

Source

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

Source

val reduce_val : 
  eval:(Env.t -> E.Term.t -> Value.t) ->
  Env.t ->
  value_function ->
  E.Ty.t list ->
  Value.t list ->
  Value.t

Source

val apply_val : 
  eval:(Env.t -> E.Term.t -> Value.t) ->
  Env.t ->
  Value.t ->
  E.ty list ->
  Value.t list ->
  Value.t

Sourceval take_drop : int -> 'a list -> 'a list * 'a list

Source

val reduce : 
  eval:(Env.t -> E.term -> Value.t) ->
  Env.t ->
  value_function ->
  E.Ty.t list ->
  E.term list ->
  Value.t

Source

val apply : 
  eval:(Env.t -> E.term -> Value.t) ->
  Env.t ->
  Value.t ->
  E.ty list ->
  E.term list ->
  Value.t

Source

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

Source

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

Module Dolmen_model.FunSource

Module `Dolmen_model.Fun`Source