Ensure identifiers produced by gensym are legal Lean variable names

1 files changed, 9 insertions, 8 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 185752a..9b0e4ff 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -38,6 +38,15 @@ type variable = { lean_id : string;
 module Environ = Map.Make (String)
 type environ = variable Environ.t
 
+let gensym : string -> string =
+  let is_alphanum = function  'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' -> true | _ -> false in
+  let counter = ref 0 in
+  fun (base : string) ->
+    let base = String.filter base ~f:is_alphanum in
+    let number = !counter in
+    counter := !counter + 1 ;
+    Printf.sprintf "v%s__%d" base number
+
 let extend_environment (env : environ) (vars : (string * variable) list) =
   Environ.of_alist_exn vars
   |> Map.merge env ~f:(fun ~key:_key -> function
@@ -155,14 +164,6 @@ let extract_variables_wrapper (q : query) : analysis_result =
 
 (* --- *)
 
-let gensym : string -> string =
-  let counter = ref 0 in
-  fun (base : string) ->
-    let base = String.filter base ~f:(fun c -> not (Char.equal c '$')) in
-    let number = !counter in
-    counter := !counter + 1 ;
-    Printf.sprintf "%s__%d" base number
-
 (* This breaks a nested rule, such as one defining `w.x.y.z`, into as many as
    needed such that every rule is of the form `x["y"] := _`. *)
 let rec transform_rule_with_ref_head : rule -> rule list = function