aboutsummaryrefslogtreecommitdiff
path: root/rego-proofs/compiler/bin
diff options
context:
space:
mode:
Diffstat (limited to 'rego-proofs/compiler/bin')
-rw-r--r--rego-proofs/compiler/bin/dune5
-rw-r--r--rego-proofs/compiler/bin/main.ml12
2 files changed, 17 insertions, 0 deletions
diff --git a/rego-proofs/compiler/bin/dune b/rego-proofs/compiler/bin/dune
new file mode 100644
index 0000000..2676d29
--- /dev/null
+++ b/rego-proofs/compiler/bin/dune
@@ -0,0 +1,5 @@
+(executable
+ (public_name compiler)
+ (name main)
+ (libraries core compiler))
+
diff --git a/rego-proofs/compiler/bin/main.ml b/rego-proofs/compiler/bin/main.ml
new file mode 100644
index 0000000..f1b213c
--- /dev/null
+++ b/rego-proofs/compiler/bin/main.ml
@@ -0,0 +1,12 @@
+open Core
+open Compiler
+open Compiler__.Ast
+open Compiler__.Lean
+
+let () =
+ let file_name = Array.get (Sys.get_argv ()) 1 in
+ let policy_code = In_channel.read_all file_name in
+ ast_of_string policy_code
+ |> compile_package
+ |> List.map ~f:fmt_lean_expression
+ |> List.iter ~f:print_endline

© 2015 - 2026 Jakob L. Kreuze