From f4395c9955e2c6e082d10dcaf896bd82dfdc9023 Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Tue, 7 Nov 2023 19:09:36 -0500
Subject: Handle existential quantification over objects

---
 rego-proofs/compiler-rewrite/lib/compiler.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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
-- 
cgit v1.3