diff --git a/src/core/Env.ml b/src/core/Env.ml index 6405faeb..ac630cf6 100644 --- a/src/core/Env.ml +++ b/src/core/Env.ml @@ -29,6 +29,8 @@ let empty () = let create ~anchor = {anchor; next = first_var} +let pp ppf env = Format.fprintf ppf "ENV(%d)" env.anchor + let fresh ~scope e = let v = Obj.magic (Term.Var.make ~env:e.anchor ~scope e.next) in e.next <- 1 + e.next; @@ -37,7 +39,8 @@ let fresh ~scope e = let check env v = (v.Term.Var.env = env.anchor) let check_exn env v = - if check env v then () else failwith "OCanren fatal (Env.check): wrong environment" + if check env v then () + else failwith "OCanren fatal (Env.check): wrong environment" let var env x = match Term.var x with diff --git a/src/core/Env.mli b/src/core/Env.mli index fe849a02..ae7d1f6f 100644 --- a/src/core/Env.mli +++ b/src/core/Env.mli @@ -28,6 +28,8 @@ type t the variable index introduced last. That's why {!empty} has extra unit argument. *) val empty : unit -> t +val pp : Format.formatter -> t -> unit + val create : anchor:Term.Var.env -> t (** Creating a fresh variable takes an extra argument [scope] to decide if