Module Dolmen_model.Eval

module E = Dolmen.Std.Expr
module Term = Dolmen.Std.Expr.Term
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 : ( 'a -> Cst.t -> 'b option ) list -> 'c -> Cst.t -> 'd
val eval : Env.t -> Fun.E.Term.t -> Value.t
val eval_var : Env.t -> Dolmen_std__Expr.ty Dolmen_std__Expr.id -> Value.t
val eval_cst : Env.t -> Dolmen_std__Expr.ty Dolmen_std__Expr.id -> Value.t
val eval_apply : Env.t -> Fun.E.term -> Fun.E.Ty.t list -> Fun.E.term list -> Value.t
val eval_binder : Env.t -> E.binder -> Fun.E.term -> Value.t
val eval_match_aux : Env.t -> Value.t -> (Adt.T.t * Fun.E.Term.t) list -> Value.t
val eval_match : Env.t -> Fun.E.Term.t -> (Adt.T.t * Fun.E.Term.t) list -> Value.t