Eval (dolmen_model.Dolmen

module E = Dolmen.Std.Expr

module B = Dolmen.Std.Builtin

module Term = Dolmen.Std.Expr.Term

module Var = Dolmen.Std.Expr.Term.Var

module Cst = Dolmen.Std.Expr.Term.Const

exception Quantifier

exception Partial_model

exception Incomplete_match

exception Unhandled_builtin of Cst.t

exception Undefined_variable of Var.t

exception Undefined_constant of Cst.t

val builtins : Env.builtins list -> Env.builtins

val eval : Env.t -> Dolmen_model.Fun.E.term -> Value.t

val eval_var : Env.t -> Dolmen_std__Expr.ty Dolmen_std__Expr.id -> Value.t

val eval_cst : Env.t -> Cst.t -> Value.t

val eval_apply : 
  Env.t ->
  Dolmen_model.Fun.E.term ->
  Dolmen_model.Fun.E.ty list ->
  Dolmen_model.Fun.E.term list ->
  Value.t

val eval_binder : Env.t -> E.binder -> Dolmen_model.Fun.E.term -> Value.t

val eval_match_aux : 
  Env.t ->
  Value.t ->
  (Dolmen_model.Adt.T.t * Dolmen_model.Fun.E.term) list ->
  Value.t

val eval_match : 
  Env.t ->
  Dolmen_model.Fun.E.term ->
  (Dolmen_model.Adt.T.t * Dolmen_model.Fun.E.term) list ->
  Value.t