sig
  type env
  type tau = Wp.Lang.F.tau
  type var = Wp.Lang.F.var
  type field = Wp.Lang.field
  type lfun = Wp.Lang.lfun
  type term = Wp.Lang.F.term
  type pred = Wp.Lang.F.pred
  val env : Wp.Lang.F.Vars.t -> Wp.Repr.env
  type repr =
      True
    | False
    | And of Wp.Repr.term list
    | Or of Wp.Repr.term list
    | Not of Wp.Repr.term
    | Imply of Wp.Repr.term list * Wp.Repr.term
    | If of Wp.Repr.term * Wp.Repr.term * Wp.Repr.term
    | Forall of Wp.Repr.tau * (Wp.Repr.env -> Wp.Repr.var * Wp.Repr.term)
    | Exists of Wp.Repr.tau * (Wp.Repr.env -> Wp.Repr.var * Wp.Repr.term)
    | Var of Wp.Repr.var
    | Int of Z.t
    | Real of Q.t
    | Add of Wp.Repr.term list
    | Mul of Wp.Repr.term list
    | Div of Wp.Repr.term * Wp.Repr.term
    | Mod of Wp.Repr.term * Wp.Repr.term
    | Eq of Wp.Repr.term * Wp.Repr.term
    | Neq of Wp.Repr.term * Wp.Repr.term
    | Lt of Wp.Repr.term * Wp.Repr.term
    | Leq of Wp.Repr.term * Wp.Repr.term
    | Times of Z.t * Wp.Repr.term
    | Call of Wp.Repr.lfun * Wp.Repr.term list
    | Field of Wp.Repr.term * Wp.Repr.field
    | Record of (Wp.Repr.field * Wp.Repr.term) list
    | Cst of Wp.Repr.tau * Wp.Repr.term
    | Get of Wp.Repr.term * Wp.Repr.term
    | Set of Wp.Repr.term * Wp.Repr.term * Wp.Repr.term
    | Abstract
  val term : Wp.Repr.term -> Wp.Repr.repr
  val pred : Wp.Repr.pred -> Wp.Repr.repr
  val lfun : Wp.Repr.lfun -> string
  val field : Wp.Repr.field -> string
end