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