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