Last refactoring before sending out update

7 files changed, 68 insertions, 88 deletions

diff --git a/rego-proofs/compiler-rewrite/bin/main.ml b/rego-proofs/compiler-rewrite/bin/main.ml
index fb9f5e5..619527e 100644
--- a/rego-proofs/compiler-rewrite/bin/main.ml
+++ b/rego-proofs/compiler-rewrite/bin/main.ml
@@ -4,7 +4,4 @@ open Compiler_rewrite.Ast
 let () =
   let file_name = Array.get (Sys.get_argv ()) 1 in
   let policy_code = In_channel.read_all file_name in
-  match ast_of_string policy_code with
-  | { policy = [ { body; _ } ]; _ } ->
-      extract_local_variables_wrapper body |> List.iter ~f:print_endline
-  | _ -> print_endline "failed"
+  ast_of_string policy_code |> show_package |> print_endline
diff --git a/rego-proofs/compiler-rewrite/compiler_rewrite.opam b/rego-proofs/compiler-rewrite/compiler_rewrite.opam
index 7b13bb9..8dbe763 100644
--- a/rego-proofs/compiler-rewrite/compiler_rewrite.opam
+++ b/rego-proofs/compiler-rewrite/compiler_rewrite.opam
@@ -1,14 +1,8 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-synopsis: "A short synopsis"
-description: "A longer description"
-maintainer: ["Maintainer Name"]
-authors: ["Author Name"]
-license: "LICENSE"
-tags: ["topics" "to describe" "your" "project"]
-homepage: "https://github.com/username/reponame"
-doc: "https://url/to/documentation"
-bug-reports: "https://github.com/username/reponame/issues"
+synopsis: "Compiler from Rego to a Lean shallow embedding"
+maintainer: ["Jakob Kreuze"]
+authors: ["Jakob Kreuze"]
 depends: [
   "ocaml"
   "dune" {>= "3.11"}
@@ -28,4 +22,3 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/username/reponame.git"
diff --git a/rego-proofs/compiler-rewrite/dune-project b/rego-proofs/compiler-rewrite/dune-project
index 365d9da..e989552 100644
--- a/rego-proofs/compiler-rewrite/dune-project
+++ b/rego-proofs/compiler-rewrite/dune-project
@@ -4,23 +4,11 @@
 
 (generate_opam_files true)
 
-(source
- (github username/reponame))
+(authors "Jakob Kreuze")
 
-(authors "Author Name")
-
-(maintainers "Maintainer Name")
-
-(license LICENSE)
-
-(documentation https://url/to/documentation)
+(maintainers "Jakob Kreuze")
 
 (package
  (name compiler_rewrite)
- (synopsis "A short synopsis")
- (description "A longer description")
- (depends ocaml dune)
- (tags
-  (topics "to describe" your project)))
-
-; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
+ (synopsis "Compiler from Rego to a Lean shallow embedding")
+ (depends ocaml dune))
diff --git a/rego-proofs/compiler-rewrite/lib/ast.ml b/rego-proofs/compiler-rewrite/lib/ast.ml
index 884f2ff..3abf234 100644
--- a/rego-proofs/compiler-rewrite/lib/ast.ml
+++ b/rego-proofs/compiler-rewrite/lib/ast.ml
@@ -1,6 +1,8 @@
 open Core
 open Yojson.Basic.Util
 
+(* AST types. *)
+
 type expr = Term of term | Every of string option * string * term * query
 [@@deriving show]
 
@@ -70,54 +72,7 @@ type import = { alias : string option; path : reference } [@@deriving show]
 type package = { path : reference; imports : import list; policy : rule list }
 [@@deriving fields, show]
 
-module Environ = Map.Make (String)
-
-type environ = string Environ.t
-
-let rec term_ground (env : environ) (term : term) : bool =
-  match term with
-  | Var name -> Map.find env name |> Option.is_some
-  | Ref (Var name, _) -> Map.find env name |> Option.is_some
-  | Call (_, subterms) ->
-      List.reduce_exn ~f:( && ) (List.map ~f:(term_ground env) subterms)
-  | _ -> true
-
-let map_with_environment_updates env xs fn =
-  List.fold xs ~init:(env, []) ~f:(fun (env, ys) x ->
-      let env', y = fn env x in
-      (env', List.append ys [ y ]))
-
-let extract_local_variables (env : environ) (q : query) : string list =
-  let handle_term env = function
-    | Call ((Var func, []), [ Var name; rhs ])
-      when String.equal func "assign" || String.equal func "eq" ->
-        if Map.find env name |> Option.is_none && term_ground env rhs then
-          match Map.add env ~key:name ~data:name with
-          | `Duplicate -> failwith "should shadow?"
-          | `Ok env' -> (env', [ name ])
-        else (env, [])
-    | _ -> (env, [])
-  in
-  let handle_expr env = function
-    | Term t -> handle_term env t
-    | Every (Some _key, _value, _, _q) -> failwith "unimplemented"
-    | Every (None, _value, _, _q) -> failwith "unimplemented"
-  in
-  let handle_literal env = function
-    | Exists (exprs, _) ->
-        let env', ys = map_with_environment_updates env exprs handle_expr in
-        (env', ys |> List.concat)
-    | Expr (expr, _) -> handle_expr env expr
-    | Negate (expr, _) -> handle_expr env expr
-  in
-
-  let _env', identifiers = map_with_environment_updates env q handle_literal in
-  List.concat identifiers
-
-let extract_local_variables_wrapper (q : query) : string list =
-  extract_local_variables Environ.empty q
-
-(* --- *)
+(* Additional JSON utility functions. *)
 
 let is_null : Yojson.Basic.t -> bool = function `Null -> true | _ -> false
 
@@ -136,6 +91,8 @@ let object_key_of_term : term -> object_key = function
   | Var v -> Var v
   | _ -> failwith "failed to convert term to object_key"
 
+(* Code to parse the JSON output of `opa parse`. *)
+
 let rec parse_term (tree : Yojson.Basic.t) : term =
   let term_type = tree |> member "type" |> to_string in
   match term_type with
@@ -269,8 +226,6 @@ let rec parse_rule tree =
       | else_branch -> Some (parse_rule else_branch));
   }
 
-(* --- *)
-
 let parse_import_path tree =
   match tree |> member "type" |> to_string with
   | "ref" -> tree |> member "value" |> to_list |> parse_ref
@@ -282,12 +237,8 @@ let parse_import tree =
     path = tree |> member "path" |> parse_import_path;
   }
 
-(* --- *)
-
 let parse_package tree = tree |> member "path" |> to_list |> parse_ref
 
-(* --- *)
-
 let parse_tree tree =
   {
     path = tree |> member "package" |> parse_package;
@@ -296,7 +247,7 @@ let parse_tree tree =
     policy = List.map ~f:parse_rule (tree |> member "rules" |> to_list_or_empty);
   }
 
-(* --- *)
+(* OPA interaction. *)
 
 let invoke ?(stdin = "") ?(env = [||]) cmd =
   let ic, oc, ec = UnixLabels.open_process_full cmd ~env in
diff --git a/rego-proofs/compiler-rewrite/lib/ast.mli b/rego-proofs/compiler-rewrite/lib/ast.mli
index b373b0d..b2cae21 100644
--- a/rego-proofs/compiler-rewrite/lib/ast.mli
+++ b/rego-proofs/compiler-rewrite/lib/ast.mli
@@ -1,5 +1,3 @@
-type environ
-
 type expr = Term of term | Every of string option * string * term * query
 
 and literal =
@@ -57,5 +55,5 @@ type rule = {
 type import = { alias : string option; path : reference }
 type package = { path : reference; imports : import list; policy : rule list }
 
-val extract_local_variables_wrapper : query -> string list
 val ast_of_string : string -> package
+val show_package : package -> string
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
new file mode 100644
index 0000000..57b93e7
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -0,0 +1,48 @@
+open Ast
+open Core
+
+module Environ = Map.Make (String)
+type environ = string Environ.t
+
+let rec term_ground (env : environ) (term : term) : bool =
+  match term with
+  | Var name -> Map.find env name |> Option.is_some
+  | Ref (Var name, _) -> Map.find env name |> Option.is_some
+  | Call (_, subterms) ->
+      List.reduce_exn ~f:( && ) (List.map ~f:(term_ground env) subterms)
+  | _ -> true
+
+let map_with_environment_updates env xs fn =
+  List.fold xs ~init:(env, []) ~f:(fun (env, ys) x ->
+      let env', y = fn env x in
+      (env', List.append ys [ y ]))
+
+let extract_local_variables (env : environ) (q : query) : string list =
+  let handle_term env : term -> (environ * string list) = function
+    | Call ((Var func, []), [ Var name; rhs ])
+      when String.equal func "assign" || String.equal func "eq" ->
+        if Map.find env name |> Option.is_none && term_ground env rhs then
+          match Map.add env ~key:name ~data:name with
+          | `Duplicate -> failwith "should shadow?"
+          | `Ok env' -> (env', [ name ])
+        else (env, [])
+    | _ -> (env, [])
+  in
+  let handle_expr env = function
+    | Term t -> handle_term env t
+    | Every (Some _key, _value, _, _q) -> failwith "unimplemented"
+    | Every (None, _value, _, _q) -> failwith "unimplemented"
+  in
+  let handle_literal env = function
+    | Exists (exprs, _) ->
+        let env', ys = map_with_environment_updates env exprs handle_expr in
+        (env', ys |> List.concat)
+    | Expr (expr, _) -> handle_expr env expr
+    | Negate (expr, _) -> handle_expr env expr
+  in
+
+  let _env', identifiers = map_with_environment_updates env q handle_literal in
+  List.concat identifiers
+
+let extract_local_variables_wrapper (q : query) : string list =
+  extract_local_variables Environ.empty q
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.mli b/rego-proofs/compiler-rewrite/lib/compiler.mli
new file mode 100644
index 0000000..193376c
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/lib/compiler.mli
@@ -0,0 +1,5 @@
+open Ast
+
+type environ
+
+val extract_local_variables_wrapper : query -> string list