Fix parse errors on existing examples

1 files changed, 23 insertions, 27 deletions

diff --git a/rego-proofs/compiler-rewrite/bin/main.ml b/rego-proofs/compiler-rewrite/bin/main.ml
index 11ecc44..8d91a2e 100644
--- a/rego-proofs/compiler-rewrite/bin/main.ml
+++ b/rego-proofs/compiler-rewrite/bin/main.ml
@@ -4,7 +4,9 @@ open Yojson.Basic.Util
 type expr = Term of term
           | Every of (string option) * string * term * query
 [@@deriving show]
-and literal = expr * (with_modifier option)
+and literal = Exists of (expr list) * (with_modifier option)
+            | Expr of expr * (with_modifier option)
+            | Negate of expr * (with_modifier option)
 [@@deriving show]
 and query = literal list
 [@@deriving show]
@@ -49,7 +51,7 @@ type rule_head_lhs = reference
 [@@deriving show]
 type rule_head_rhs = Assignment of assign_operator * term
                    | Function of assign_operator * (string list) * term
-                   | Set of string * term
+                   | Set of term
 [@@deriving show]
 type rule_head = rule_head_lhs * rule_head_rhs
 [@@deriving show]
@@ -94,7 +96,6 @@ let object_key_of_term : term -> object_key = function
   | _ -> failwith "failed to convert term to object_key"
 
 let rec parse_term (tree : Yojson.Basic.t) : term =
-  Printf.printf "%s: %s\n" "parse_term" (Yojson.Basic.to_string tree);
   let term_type = tree |> member "type" |> to_string in
   match term_type with
   | "var" -> Var (tree |> member "value" |> to_string)
@@ -135,7 +136,6 @@ let rec parse_term (tree : Yojson.Basic.t) : term =
   | _ -> failwith ("unsupported term type " ^ term_type)
 
 and parse_literal tree : literal =
-  Printf.printf "%s: %s\n" "parse_literal" (Yojson.Basic.to_string tree);
   let with_expr = tree |> member "with" in
   let with_expr = match with_expr with
     | `Null -> None
@@ -147,25 +147,29 @@ and parse_literal tree : literal =
   in
   match tree |> member "terms" with
   | `List (func :: args) ->
-     (Term (Call (func |> member "value" |> to_list |> parse_ref,
-                  List.map ~f:parse_term args)),
-      with_expr)
+     Expr (Term (Call (func |> member "value" |> to_list |> parse_ref,
+                       List.map ~f:parse_term args)),
+           with_expr)
   | `List _ -> failwith "ill-formed call"
   | x ->
-     if x |> member "domain" |> is_null then
-       (Term (parse_term x), with_expr)
+     if not (x |> member "symbols" |> is_null) then
+       Exists (x |> member "symbols"
+                 |> to_list
+                 |> List.map ~f:(fun x -> Term (parse_term x)),
+               with_expr)
+     else if x |> member "domain" |> is_null then
+       Expr (Term (parse_term x), with_expr)
      else
-       (Every ((if x |> member "key" |> is_null then
-                  None
-                else
-                  Some (x |> member "key" |> member "value" |> to_string)),
-               x |> member "value" |> member "value" |> to_string,
-               x |> member "domain" |> parse_term,
-               (List.map ~f:parse_literal (x |> member "body" |> to_list))),
-        with_expr)
+       Expr (Every ((if x |> member "key" |> is_null then
+                       None
+                     else
+                       Some (x |> member "key" |> member "value" |> to_string)),
+                    x |> member "value" |> member "value" |> to_string,
+                    x |> member "domain" |> parse_term,
+                    (List.map ~f:parse_literal (x |> member "body" |> to_list))),
+             with_expr)
 
 and parse_ref_target tree : ref_target =
-  Printf.printf "%s: %s\n" "parse_ref_target" (Yojson.Basic.to_string tree);
   let term = parse_term tree in
   match term with
   | Var term -> Var term
@@ -179,13 +183,11 @@ and parse_ref_target tree : ref_target =
   | _ -> failwith ("unsupported ref_target " ^ (show_term term))
 
 and parse_ref tree =
-  Printf.printf "%s: %s\n" "parse_ref" (String.concat (List.map ~f:Yojson.Basic.to_string tree));
   match tree with
   | target :: args -> (parse_ref_target target, List.map ~f:parse_term args)
   | _ -> failwith "empty reference"
 
 let parse_head tree =
-  Printf.printf "%s: %s\n" "parse_head" (Yojson.Basic.to_string tree);
   (* Variables are desugared to empty references. *)
   let lhs = tree |> member "ref" |> to_list |> parse_ref in
   let assign_operator = if tree |> member "assign" |> to_bool_or_false then
@@ -194,8 +196,7 @@ let parse_head tree =
                           Unify in
   let rhs =
     if not (tree |> member "key" |> is_null) then
-      Set (tree |> member "key" |> to_string,
-           (tree |> member "value" |> parse_term))
+      Set (tree |> member "key" |> parse_term)
     else if tree |> member "args" |> to_bool_or_false then
       Function (assign_operator,
                 (tree |> member "args" |> to_list |> List.map ~f:(fun x -> (x |> member "value" |> to_string))),
@@ -205,7 +206,6 @@ let parse_head tree =
   in (lhs, rhs)
 
 let rec parse_rule tree =
-  Printf.printf "%s: %s\n" "rec parse_rule tree" (Yojson.Basic.to_string tree);
   { default = tree |> member "default" |> to_bool_or_false;
     head = tree |> member "head" |> parse_head;
     body = List.map ~f:parse_literal (tree |> member "body" |> to_list_or_empty);
@@ -218,13 +218,11 @@ let rec parse_rule tree =
 (* --- *)
 
 let parse_import_path tree =
-  Printf.printf "%s: %s\n" "parse_import_path" (Yojson.Basic.to_string tree);
   match (tree |> member "type" |> to_string) with
   | "ref" -> tree |> member "value" |> to_list |> parse_ref
   | _ -> failwith "unimplemented"
 
 let parse_import tree =
-  Printf.printf "%s: %s\n" "parse_import" (Yojson.Basic.to_string tree);
   { alias = tree |> member "alias" |> to_string_option;
     path = tree |> member "path" |> parse_import_path
   }
@@ -232,13 +230,11 @@ let parse_import tree =
 (* --- *)
 
 let parse_package tree =
-  Printf.printf "%s: %s\n" "parse_package" (Yojson.Basic.to_string tree);
   tree |> member "path" |> to_list |> parse_ref
 
 (* --- *)
 
 let parse_tree tree =
-  Printf.printf "%s: %s\n" "parse_tree" (Yojson.Basic.to_string tree);
   { path = tree |> member "package" |> parse_package;
     imports = List.map ~f:parse_import (tree |> member "imports" |> to_list_or_empty);
     policy = List.map ~f:parse_rule (tree |> member "rules" |> to_list_or_empty)