diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 17 |
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 |