fix dk export

src/core/env.ml

@@ -127,7 +127,7 @@ let of_prod_nth : ctxt -> int -> term -> env * term = fun c n t ->
     if i >= n then env, t
     else match_prod c t (fun a b ->
              let x, b = unbind b in
-             build_env (i+1) (add (name_of x) x a None env) b)
+             build_env (i+1) (add (base_name x) x a None env) b)
   in build_env 0 [] t
 
 (** [of_prod_using c xs t] is similar to [of_prod s c n t] where [n =
@@ -141,7 +141,7 @@ let of_prod_using : ctxt -> var array -> term -> env * term = fun c xs t ->
     if i >= n then env, t
     else match_prod c t (fun a b ->
              let xi = xs.(i) in
-             let name = name_of xi in
+             let name = base_name xi in
              let env = add name xi a None env in
              build_env (i+1) env (subst b (mk_Vari xi)))
   in build_env 0 [] t

src/core/print.ml

@@ -92,7 +92,7 @@ let sym : sym pp = fun ppf s ->
         else out ppf "%a.%a" path p uid n
     | Some alias -> out ppf "%a.%a" uid alias uid n
 
-let var : var pp = fun ppf x -> uid ppf (name_of x)
+let var : var pp = fun ppf x -> uid ppf (base_name x)
 
 (** Exception raised when trying to convert a term into a nat. *)
 exception Not_a_nat

src/core/term.ml

@@ -45,6 +45,41 @@ type mbinder_info = {mbinder_name : string array; mbinder_bound : bool array}
 
 let binder_name : binder_info -> string = fun bi -> bi.binder_name
 
+(** Type for free variables. *)
+type var = int * string
+
+(** [compare_vars x y] safely compares [x] and [y]. Note that it is unsafe to
+    compare variables using [Pervasive.compare]. *)
+let compare_vars : var -> var -> int = fun (i,_) (j,_) -> Stdlib.compare i j
+
+(** [eq_vars x y] safely computes the equality of [x] and [y]. Note that it is
+    unsafe to compare variables with the polymorphic equality function. *)
+let eq_vars : var -> var -> bool = fun x y -> compare_vars x y = 0
+
+(** [new_var name] creates a new unique variable of name [name]. *)
+let new_var : string -> var =
+  let open Stdlib in let n = ref 0 in fun name -> incr n; !n, name
+
+(** [new_var_ind s i] creates a new [var] of name [s ^ string_of_int i]. *)
+let new_var_ind : string -> int -> var = fun s i ->
+  new_var (Escape.add_prefix s (string_of_int i))
+
+(** [base_name x] returns the base name of variable [x]. Note that this name
+    is not unique: two distinct variables may have the same name. *)
+let base_name : var -> string = fun (_i,n) -> n
+
+(** [uniq_name x] returns a string uniquely identifying the variable [x]. *)
+let uniq_name : var -> string = fun (i,_) -> "v" ^ string_of_int i
+
+(** Sets and maps of variables. *)
+module Var = struct
+  type t = var
+  let compare = compare_vars
+end
+
+module VarSet = Set.Make(Var)
+module VarMap = Map.Make(Var)
+
 (** Representation of a term (or types) in a general sense. Values of the type
     are also used, for example, in the representation of patterns or rewriting
     rules. Specific constructors are included for such applications,  and they
@@ -67,9 +102,6 @@ type term =
   | LLet of term * term * binder
   (** [LLet(a, t, u)] is [let x : a ≔ t in u] (with [x] bound in [u]). *)
 
-(** Type for free variables. *)
-and var = int * string
-
 (** Type for binders. *)
 and binder = binder_info * term
 and mbinder = mbinder_info * term
@@ -237,34 +269,6 @@ end
 module MetaSet = Set.Make(Meta)
 module MetaMap = Map.Make(Meta)
 
-(** [compare_vars x y] safely compares [x] and [y].  Note that it is unsafe to
-    compare variables using [Pervasive.compare]. *)
-let compare_vars : var -> var -> int = fun (i,_) (j,_) -> Stdlib.compare i j
-
-(** [eq_vars x y] safely computes the equality of [x] and [y]. Note that it is
-    unsafe to compare variables with the polymorphic equality function. *)
-let eq_vars : var -> var -> bool = fun x y -> compare_vars x y = 0
-
-(** [new_var name] creates a new unique variable of name [name]. *)
-let new_var : string -> var =
-  let open Stdlib in let n = ref 0 in fun name -> incr n; !n, name
-
-(** [new_var_ind s i] creates a new [var] of name [s ^ string_of_int i]. *)
-let new_var_ind : string -> int -> var = fun s i ->
-  new_var (Escape.add_prefix s (string_of_int i))
-
-(** [name_of x] returns the name of variable [x]. *)
-let name_of : var -> string = fun (_i,n) -> n (*^ string_of_int i*)
-
-(** Sets and maps of variables. *)
-module Var = struct
-  type t = var
-  let compare = compare_vars
-end
-
-module VarSet = Set.Make(Var)
-module VarMap = Map.Make(Var)
-
 let mk_bin s t1 t2 = Appl(Appl(Symb s, t1), t2)
 
 (** [mk_left_comb s t ts] builds a left comb of applications of [s] from
@@ -617,7 +621,7 @@ let bind_mvar : var array -> term -> mbinder =
   let b = bind 1 t in
   if Logger.log_enabled() then
     log_term "bind_mvar %a %a = %a" (D.array var) xs term t term b;
-  let bi = { mbinder_name = Array.map name_of xs; mbinder_bound } in
+  let bi = { mbinder_name = Array.map base_name xs; mbinder_bound } in
   bi, b
 
 (** [binder_occur b] tests whether the bound variable occurs in [b]. *)

src/core/term.mli

@@ -249,8 +249,12 @@ val new_var : string -> var
 (** [new_var_ind s i] creates a new [var] of name [s ^ string_of_int i]. *)
 val new_var_ind : string -> int -> var
 
-(** [name_of x] returns the name of the variable [x]. *)
-val name_of : var -> string
+(** [base_name x] returns the base name of the variable [x]. Note that this
+    base name is not unique: two distinct variables may have the same name. *)
+val base_name : var -> string
+
+(** [uniq_name x] returns a string uniquely identifying the variable [x]. *)
+val uniq_name : var -> string
 
 (** Sets and maps of term variables. *)
 module Var : Map.OrderedType with type t = var

src/export/dk.ml

@@ -116,7 +116,9 @@ let cmp : decl cmp = cmp_map (Lplib.Option.cmp Pos.cmp) pos_of_decl
 
 (** Translation of terms. *)
 
-let var : var pp = fun ppf v -> ident ppf (name_of v)
+let var : var pp = fun ppf v -> string ppf (uniq_name v)
+
+let patt : int pp = fun ppf i -> out ppf "x%d" i
 
 (** [term b ppf t] prints term [t]. Print abstraction domains if [b]. *)
 let rec term : bool -> term pp = fun b ppf t ->
@@ -141,9 +143,9 @@ let rec term : bool -> term pp = fun b ppf t ->
     let x,u = unbind u in
     out ppf "((%a : %a := %a) => %a)" var x (term b) a (term b) t (term b) u
   | Patt(None,_,_) -> assert false
-  | Patt(Some i,_,[||]) -> int ppf i
+  | Patt(Some i,_,[||]) -> patt ppf i
   | Patt(Some i,_,ts) ->
-    out ppf "(%d%a)" i (Array.pp (prefix " " (term b)) "") ts
+    out ppf "(%a%a)" patt i (Array.pp (prefix " " (term b)) "") ts
   | Db _ -> assert false
   | TRef _ -> assert false
   | Wild -> assert false
@@ -197,8 +199,8 @@ let sym_decl : sym pp = fun ppf s ->
 let rule_decl : (Path.t * string * rule) pp = fun ppf (p, n, r) ->
   let rec var ppf i =
     if i < 0 then ()
-    else if i = 0 then out ppf "0"
-    else out ppf "%a,%d" var (i-1) i
+    else if i = 0 then patt ppf 0
+    else out ppf "%a,%a" var (i-1) patt i
   in
   out ppf "[%a] %a%a --> %a.@." var (r.vars_nb - 1) qid (p, n)
     (List.pp (prefix " " (term false)) "") r.lhs (term true) r.rhs

src/export/hrs.ml

@@ -73,10 +73,10 @@ let sym : sym pp = fun ppf s -> string ppf (SymMap.find s !syms)
 
 (** [add_bvar v] declares an abstracted Lambdapi variable. *)
 let add_bvar : var -> unit = fun v ->
-  bvars := StrSet.add (name_of v) !bvars
+  bvars := StrSet.add (base_name v) !bvars
 
 (** [bvar v] translates the Lambdapi variable [v]. *)
-let bvar : var pp = fun ppf v -> string ppf (name_of v)
+let bvar : var pp = fun ppf v -> string ppf (base_name v)
 
 (** [pvar i] translates the pattern variable index [i]. *)
 let pvar : int pp = fun ppf i -> out ppf "$%d_%d" !nb_rules i

src/export/xtc.ml

@@ -52,10 +52,10 @@ let sym : sym pp = fun ppf s ->
 
 (** [add_bvar v] declares an abstracted Lambdapi variable. *)
 let add_bvar : var -> unit = fun v ->
-  bvars := StrSet.add (name_of v) !bvars
+  bvars := StrSet.add (base_name v) !bvars
 
 (** [bvar v] translates the Lambdapi bound variable [v]. *)
-let bvar : var pp = fun ppf v -> out ppf "<var>%s</var>" (name_of v)
+let bvar : var pp = fun ppf v -> out ppf "<var>%s</var>" (base_name v)
 
 (** [pvar i] translates the Lambdapi pattern variable [i]. *)
 let pvar : int pp = fun ppf i -> out ppf "<var>%d_%d</var>" !nb_rules i

src/handle/inductive.ml

@@ -49,7 +49,7 @@ let gen_safe_prefixes : inductive -> string * string * string =
       match unfold t with
       | Prod(_,b) ->
         let x,b = unbind b in
-        add_name_from_type (StrSet.add (name_of x) set) b
+        add_name_from_type (StrSet.add (base_name x) set) b
       | _ -> set
     in
     let add_name_from_sym set sym =
@@ -318,7 +318,7 @@ let iter_rec_rules :
     let head = P.appl_wild head n in
     (* add a predicate variable for each inductive type *)
     let head =
-      let apred (_,d) t = apatt t (name_of d.ind_var) in
+      let apred (_,d) t = apatt t (base_name d.ind_var) in
       List.fold_right apred ind_pred_map head
     in
     (* add a case variable for each constructor *)
@@ -343,7 +343,7 @@ let iter_rec_rules :
       let env_appl t env =
         List.fold_right (fun (_,(x,_,_)) t -> P.appl t (P.var x)) env t in
       let add_abst t (_,(x,_,_)) =
-        P.abst (Some (Pos.none (name_of x))) t in
+        P.abst (Some (Pos.none (base_name x))) t in
       List.fold_left add_abst (arec s ts (env_appl x env)) env
     in
     let acc_rec_dom acc x aux = P.appl (P.appl acc x) aux in

src/handle/why3_tactic.ml

@@ -82,7 +82,7 @@ end = struct
           let sym = Why3.(Ty.create_tysymbol id [] Ty.NoDef) in
           ((te,TySym sym)::tbl, Why3.Ty.ty_app sym [])
         | Vari x, [] ->
-          let sym = Why3.Ty.tv_of_string (name_of x) in
+          let sym = Why3.Ty.tv_of_string (base_name x) in
           ((te,TyVar sym)::tbl, Why3.Ty.ty_var sym)
         | _ ->
           let id = Why3.Ident.id_fresh "ty" in
@@ -130,7 +130,7 @@ let translate_term : config -> cnst_table -> TyTable.t -> term ->
         let x, t = unbind t in
         let (tbl, ty_tbl ,t) = translate_prop tbl ty_tbl t in
         let tquant =
-          let id = Why3.Ident.id_fresh (name_of x) in
+          let id = Why3.Ident.id_fresh (base_name x) in
           let vid = Why3.(Term.create_vsymbol id) ty in
           let close =
             if s == cfg.symb_ex then Why3.Term.t_exists_close

src/parsing/syntax.ml

@@ -107,8 +107,8 @@ module P  = struct
   (** [iden s] builds a [P_Iden] "@s". *)
   let iden : string -> p_term = qiden []
 
-  (** [var v] builds a [P_Iden] from [name_of v]. *)
-  let var : Term.var -> p_term = fun v -> iden (Term.name_of v)
+  (** [var v] builds a [P_Iden] from [base_name v]. *)
+  let var : Term.var -> p_term = fun v -> iden (Term.base_name v)
 
   (** [patt s ts] builds a [P_Patt] "$s[ts]". *)
   let patt : string -> p_term array option -> p_term = fun s ts ->