Add support for Negate rules

1 files changed, 41 insertions, 31 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 5e7d445..185752a 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -19,8 +19,8 @@ let kind_and_args_of_rule = function
     `ObjectRule (key, value)
   | { head = ((_, _), Function (_, args, term)); _ } ->
     `FunctionRule (args, term)
-  | { head = ((_, _), Assignment (_, _)); _ } ->
-    assert false (* TODO *)
+  | { head = ((_, _), Assignment (_, _)); _ } as rule ->
+    failwith (Printf.sprintf "unknown rule form: %s" (show_rule rule))
 
 let definition_kind_of_rule rule =
   match kind_and_args_of_rule rule with
@@ -33,6 +33,7 @@ type variable = { lean_id : string;
                   kind : definition_kind;
                   assigned : bool;
                 }
+[@@deriving eq, show]
 
 module Environ = Map.Make (String)
 type environ = variable Environ.t
@@ -115,7 +116,7 @@ let extract_variables (env : environ) (q : query) : analysis_result =
       if List.is_empty args then
         handle_term env target
       else
-        let terms = [] @ args in
+        let terms = [target] @ args in
         List.map terms ~f:(handle_term env) |> List.fold ~init:empty ~f:combine
     | Array xs | Set xs ->
       List.map xs ~f:(handle_term env) |> List.fold ~init:empty ~f:combine
@@ -191,7 +192,10 @@ let rec compile_term env : term -> lean_expression =
        -> Identifier lean_id
      | Some { assigned = false; _ } ->
        failwith (Printf.sprintf "identifier %s used before definition" id)
-     | Some _ -> assert false (* TODO *)
+     | Some var ->
+       failwith (Printf.sprintf
+                   "variable found in environment but of unknown form %s"
+                   (show_variable var))
      | None -> failwith (Printf.sprintf "unbound variable %s" id))
   | Ref (target, terms) ->
     let target' = compile_term env (term_of_ref_target target) in
@@ -272,14 +276,15 @@ and compile_literal env : literal -> (environ * lean_expression) = function
   | Exists (exprs, _) ->
     let (env', form) = compile_query env (List.map ~f:literal_of_expr exprs) in
     (env', form)
-  | Expr (expr, _) -> compile_expr env expr
-  | Negate (_expr, _) -> assert false (* TODO *)
+  | Expr (expr, _) ->
+    let (env', inner) = compile_expr env expr in
+    (env', Application (Identifier "Ne", [inner; Application (Identifier "Rego.Any.bool", [Bool false])]))
+  | Negate (expr, _) ->
+    let (env', form) = compile_literal env (Expr (expr, None)) in
+    (env', Application (Identifier "Not", [form]))
 
 and compile_query env literals : (environ * lean_expression) =
   let { free; bound; used } = extract_variables env literals in
-  print_endline (List.to_string ~f:String.to_string free);
-  print_endline (List.to_string ~f:String.to_string bound);
-  print_endline (List.to_string ~f:String.to_string used);
   let used = used
              |> List.filter ~f:(fun name -> match Map.find_exn env name with
                                             | { kind = Complete; _ } -> false
@@ -291,42 +296,47 @@ and compile_query env literals : (environ * lean_expression) =
        List.map bound ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = false }))]
     |> extend_environment env in
   let (env'', subterms) = map_with_environment_updates env' literals compile_literal in
-  let compiled_terms = List.map subterms
-      ~f:(fun x -> Application (Identifier "Ne", [x; Application (Identifier "Rego.Any.bool", [Bool false])])) in
 
   let lean_id_of_identifier k = (let { lean_id; _ } = Map.find_exn env'' k in lean_id) in
   let constraints =
-    List.map bound ~f:(fun name ->
+    List.filter_map used ~f:(fun name ->
         match Map.find env name with
         | Some { lean_id; kind = ScalarRule; _ } ->
-           Application (Identifier "scalar_specified_by",
-                        [Identifier lean_id;
-                         Identifier (lean_id_of_identifier name)])
+          Some
+            (Application (Identifier "scalar_specified_by",
+                          [Identifier lean_id;
+                           Identifier (lean_id_of_identifier name)]))
         | Some { lean_id; kind = SetRule; _ } ->
-           Application (Identifier "set_specified_by",
-                        [Identifier lean_id;
-                         Identifier (lean_id_of_identifier name)])
+          Some
+            (Application (Identifier "set_specified_by",
+                          [Identifier lean_id;
+                           Identifier (lean_id_of_identifier name)]))
         | Some { lean_id; kind = ObjectRule; _ } ->
-           Application (Identifier "object_specified_by",
-                        [Identifier lean_id;
-                         Identifier (lean_id_of_identifier name)])
+          Some
+            (Application (Identifier "object_specified_by",
+                          [Identifier lean_id;
+                           Identifier (lean_id_of_identifier name)]))
         | Some { lean_id; kind = FunctionRule; _ } ->
-           Application (Identifier "function_specified_by",
-                        [Identifier lean_id;
-                         Identifier (lean_id_of_identifier name)])
-        | None -> failwith (Printf.sprintf "unbound variable %s" name)
-        | _ -> assert false) in
-  let compiled_terms = constraints @ compiled_terms in
+          Some
+            (Application (Identifier "function_specified_by",
+                          [Identifier lean_id;
+                           Identifier (lean_id_of_identifier name)]))
+        | Some _ -> None
+        | None -> failwith (Printf.sprintf "unbound variable %s" name)) in
+  let compiled_terms = constraints @ subterms in
+
+  let form = match compiled_terms with
+     | [x] -> x
+     | xs -> Application (Identifier "And", xs)
+  in
 
   let quantified_names = free @ bound @ used in
   (env'',
    if List.is_empty quantified_names then
-     match compiled_terms with
-     | [x] -> x
-     | xs -> Application (Identifier "And", xs)
+     form
    else
      Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"),
-             Application (Identifier "And", compiled_terms)))
+             form))
 
 let compile_definition env (rules : rule list) =
   assert (not (List.is_empty rules));