Import Lean representation from XACML compiler

3 files changed, 76 insertions, 1 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler-rewrite/lib/lean.ml
new file mode 100644
index 0000000..d670d5e
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/lib/lean.ml
@@ -0,0 +1,51 @@
+open Core
+
+type lean_expression =
+  | Identifier of string
+  | Bool of bool
+  | String of string
+  | Number of int
+  | List of lean_expression list
+  | Tuple of lean_expression list
+  | Application of lean_expression * lean_expression list
+  | Define of string * lean_expression
+  | Inductive of string * judgement list * (string * lean_expression) list
+  | ForAll of judgement * lean_expression
+  | Exists of judgement * lean_expression
+
+and judgement = string list * string
+
+let fmt_judgement : judgement -> string = function
+  | vars, t -> Printf.sprintf "(%s : %s)" (String.concat ~sep:" " vars) t
+
+let rec fmt_lean_expression : lean_expression -> string = function
+  | Identifier s -> s
+  | Bool b -> if b then "True" else "False"
+  | String s -> Printf.sprintf "\"%s\"" s
+  | Number n -> Int.to_string n
+  | List xs ->
+      Printf.sprintf "[%s]"
+        (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
+  | Tuple xs ->
+      Printf.sprintf "(%s)"
+        (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
+  | Application (head, args) ->
+      Printf.sprintf "(%s %s)" (fmt_lean_expression head)
+        (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args))
+  | Define (ident, expr) ->
+      Printf.sprintf "def %s := (%s)" ident (fmt_lean_expression expr)
+  | ForAll (j, expr) ->
+      Printf.sprintf "∀ %s, %s" (fmt_judgement j) (fmt_lean_expression expr)
+  | Exists (j, expr) ->
+      Printf.sprintf "∃ %s, %s" (fmt_judgement j) (fmt_lean_expression expr)
+  | Inductive (name, judgements, arms) ->
+      let fmt_arm (name, expr) =
+        let head =
+          Printf.sprintf "%s %s" name
+            (List.map ~f:fst judgements |> List.concat |> String.concat ~sep:" ")
+        in
+        Printf.sprintf "  | %s -> %s : %s" name (fmt_lean_expression expr) head
+      in
+      Printf.sprintf "inductive %s %s where\n%s" name
+        (List.map ~f:fmt_judgement judgements |> String.concat ~sep:" ")
+        (List.map ~f:fmt_arm arms |> String.concat ~sep:"\n")
diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler-rewrite/lib/lean.mli
new file mode 100644
index 0000000..c77cf81
--- /dev/null
+++ b/rego-proofs/compiler-rewrite/lib/lean.mli
@@ -0,0 +1,16 @@
+type lean_expression =
+  | Identifier of string
+  | Bool of bool
+  | String of string
+  | Number of int
+  | List of lean_expression list
+  | Tuple of lean_expression list
+  | Application of lean_expression * lean_expression list
+  | Define of string * lean_expression
+  | Inductive of string * judgement list * (string * lean_expression) list
+  | ForAll of judgement * lean_expression
+  | Exists of judgement * lean_expression
+
+and judgement = string list * string
+
+val fmt_lean_expression : lean_expression -> string
diff --git a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
index c21d157..3de5d7e 100644
--- a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
+++ b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml
@@ -2,7 +2,8 @@ open Core
 open Compiler_rewrite
 
 module To_test = struct
-  let extract_locals = Ast.extract_local_variables_wrapper
+  let extract_locals = Compiler.extract_local_variables_wrapper
+  let fmt = Lean.fmt_lean_expression
 end
 
 let strings =
@@ -67,6 +68,11 @@ q {
     "expected identifier list" [ "x" ]
     (To_test.extract_locals (extract_query policy_code))
 
+let test_identifier () =
+  let open Compiler_rewrite.Lean in
+  let ast = Identifier "test" in
+  Alcotest.(check string) "expected string" "test" (To_test.fmt ast)
+
 let () =
   let open Alcotest in
   run "Compiler"
@@ -86,4 +92,6 @@ let () =
              (2)"
             `Quick test_local_not_ground_because_of_ordering;
         ] );
+      ( "ast formatting ",
+        [ test_case "identifier compilation" `Quick test_identifier ] );
     ]