Handle existential quantification over objects

1 files changed, 5 insertions, 1 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 2f9025d..65e139c 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -139,7 +139,11 @@ let extract_variables (env : environ) (q : query) : analysis_result =
     | _ -> empty
   and handle_expr env = function
     | Term t -> handle_term env t
-    | Every (Some _key, _value, _, _q) -> assert false (* TODO *)
+    | Every (Some key, value, _, q) ->
+      let env' = [(key,   { lean_id = "unimportant"; kind = Complete; assigned = true });
+                  (value, { lean_id = "unimportant"; kind = Complete; assigned = true })]
+                 |> extend_environment env in
+      List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine
     | Every (None, value, _, q) ->
       let var = ({ lean_id = "unimportant"; kind = Complete; assigned = true }) in
       let env' = Map.set env ~key:value ~data:var in