Compile default rules

1 files changed, 55 insertions, 35 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 9044f50..c68dd8a 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -297,27 +297,57 @@ let string_of_reference : reference -> string = function
 let compile_definition env (rules : rule list) =
   assert (not (List.is_empty rules));
 
+  (* TODO: Assert that all rules are of the same kind. *)
+
   let variable_being_defined =
     match List.nth_exn rules 0 with
     | { head = (rf, _); _ } -> rf
   in
 
+  let (default_rules, conditional_rules) =
+    List.partition_tf rules ~f:(function | { default = true; _ } -> true | _ -> false)
+  in
+  assert (List.length default_rules <= 1); (* There can be only one default rule. *)
+
+  let fold_or props =
+    match List.reduce props ~f:(fun x y -> Application (Identifier "Or", [y; x])) with
+    | Some x -> x
+    | None -> Bool true
+  in
+
   let subject = gensym "x" in
+  let conditional_arms =
+    List.mapi conditional_rules ~f:(fun i ->
+        function
+        | { head = (_, Assignment (_, term)); body; _ } ->
+          let eq : term = Call ((Var "eq", []), [Var subject; term]) in
+          let env' = [(subject, { lean_id = subject; kind = Complete; assigned = true })]
+                     |> extend_environment env in
+          let (_, subject_constraint) = compile_query env' [Expr (Term eq, None)] in
+          let (_, body_form) = compile_query env body in
+          (body_form,
+           (Printf.sprintf "rule%d" i,
+            [subject_constraint; body_form],
+            [Identifier subject]))
+        | _ -> failwith "unimplemented") in
+  let default_arms =
+    List.map default_rules ~f:(function
+        | { head = (_, Assignment (_, term)); _ } ->
+          let eq : term = Call ((Var "eq", []), [Var subject; term]) in
+          let env' = [(subject, { lean_id = subject; kind = Complete; assigned = true })]
+                     |> extend_environment env in
+          let (_, subject_constraint) = compile_query env' [Expr (Term eq, None)] in
+          let other_rule_bodies = List.map ~f:fst conditional_arms in
+          let body_form = Application (Identifier "Not", [fold_or other_rule_bodies]) in
+          ("rule_default",
+           [subject_constraint; body_form],
+           [Identifier subject])
+        | _ -> failwith "unimplemented") in
   let form =
     Inductive
       (string_of_reference variable_being_defined,
        [([subject], "Rego.Any")],
-       List.mapi rules ~f:(fun i ->
-           function
-           | { head = (_, Assignment (_, term)); body; _ } ->
-              let eq : term = Call ((Var "eq", []), [Var subject; term]) in
-              let env' = [(subject, { lean_id = subject; kind = Complete; assigned = true })]
-                         |> extend_environment env in
-              let (_, form) = compile_query env' [Expr (Term eq, None)] in
-              (Printf.sprintf "rule%d" i,
-               [form; compile_query env body |> snd],
-               [Identifier subject])
-           | _ -> failwith "unimplemented"))
+       List.append (List.map ~f:snd conditional_arms) default_arms)
   in (env, form)
 
 let compile_policy env (rules : rule list) =
@@ -331,34 +361,24 @@ let compile_policy env (rules : rule list) =
     grouping [] l in
   let head_of_rule = function | {head = (rf, _); _ } -> rf in
   let by_reference = group head_of_rule rules in
-
-  (* let _scope = List.map by_reference *)
-  (*     ~f:(fun x -> *)
-  (*         let lean_id = List.nth_exn x 0 |> head_of_rule |> string_of_reference in *)
-  (*         lean_id *)
-  (*       ) *)
-  (* in *)
-
-  map_with_environment_updates env by_reference compile_definition
+  let env' =
+    List.map by_reference ~f:(function
+        | { head = ((Var name, []), Assignment _); _ } :: _ ->
+          (name, { lean_id = name ; kind = ScalarRule; assigned = true })
+        | { head = ((Var name, [_]), Assignment _); _ } :: _ ->
+          (name, { lean_id = name ; kind = ObjectRule; assigned = true })
+        | { head = ((Var name, []), Set _); _ } :: _ ->
+          (name, { lean_id = name ; kind = SetRule; assigned = true })
+        | { head = ((Var name, []), Function _); _ } :: _ ->
+          (name, { lean_id = name ; kind = FunctionRule; assigned = true })
+        | _ -> failwith "policy rule head is not a variable")
+    |> extend_environment env in
+  map_with_environment_updates env' by_reference compile_definition
 
 let compile_package = function
   | { path; imports; policy } ->
     let policy = List.map ~f:transform_rule_with_ref_head policy |> List.concat in
-
-    let env =
-      List.map policy ~f:(function
-          | { head = ((Var name, []), Assignment _); _ } ->
-             (name, { lean_id = name ; kind = ScalarRule; assigned = true })
-          | { head = ((Var name, [_]), Assignment _); _ } ->
-             (name, { lean_id = name ; kind = ObjectRule; assigned = true })
-          | { head = ((Var name, []), Set _); _ } ->
-             (name, { lean_id = name ; kind = SetRule; assigned = true })
-          | { head = ((Var name, []), Function _); _ } ->
-             (name, { lean_id = name ; kind = FunctionRule; assigned = true })
-          | _ -> failwith "policy rule head is not a variable")
-      |> extend_environment toplevel in
-
-    let (_env', forms) = compile_policy env policy in
+    let (_env', forms) = compile_policy toplevel policy in
     [Comment (show_reference path |> String.escaped);
      Comment (List.map ~f:show_import imports |> String.concat |> String.escaped)]
     @ forms