Use gensym for generated identifiers

1 files changed, 7 insertions, 6 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 83fa856..ecc7162 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -180,8 +180,8 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
   | Every (Some key, value, domain, query) ->
     let domain' = compile_term env domain in
     (* Extend the environment with the key and value. *)
-    let env' = Map.set env ~key:key ~data:{ lean_id = key; complete = true; assigned = true }
-               |> Map.set ~key:value ~data:{ lean_id = value; complete = true; assigned = true } in
+    let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; complete = true; assigned = true }
+               |> Map.set ~key:value ~data:{ lean_id = gensym value; complete = true; assigned = true } in
     let (env'', query') = compile_query env' query in
     (env'',
      ForAll
@@ -195,7 +195,7 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
   | Every (None, value, domain, query) ->
     let domain' = compile_term env domain in
     (* Extend the environment with the value. *)
-    let env' = Map.set env ~key:value ~data:{ lean_id = value; complete = true; assigned = true } in
+    let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; complete = true; assigned = true } in
     let (env'', query') = compile_query env' query in
     (env'',
      ForAll
@@ -216,9 +216,9 @@ and compile_literal env : literal -> (environ * lean_expression) = function
 
 and compile_query env literals : (environ * lean_expression) =
   let { free; bound; _ } = extract_variables env literals in
-  let env' = List.map free ~f:(fun name -> (name, { lean_id = name; complete = true; assigned = true }))
+  let env' = List.map free ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = true }))
              |> List.append
-               (List.map bound ~f:(fun name -> (name, { lean_id = name; complete = true; assigned = false })))
+               (List.map bound ~f:(fun name -> (name, { lean_id = gensym name; complete = true; assigned = false })))
              |> Environ.of_alist_exn
              |> Map.merge env ~f:(fun ~key:_key -> function
                  | `Right v -> Some v
@@ -234,7 +234,8 @@ and compile_query env literals : (environ * lean_expression) =
      | [x] -> x
      | xs -> Application (Identifier "And", xs)
    else
-     Exists ((free @ bound, "Rego.Any"),
+     let lean_id_of_identifier k = (let { lean_id; _ } = Map.find_exn env'' k in lean_id) in
+     Exists ((List.map (free @ bound) ~f:lean_id_of_identifier , "Rego.Any"),
              Application (Identifier "And", compiled_terms)))
 
 (* TODO: Probably get rid of this once we deal with nested definitions. *)