1 files changed, 63 insertions, 0 deletions
diff --git a/rego-proofs/compiler/lib/lean.ml b/rego-proofs/compiler/lib/lean.ml
new file mode 100644
index 0000000..6bb4265
--- /dev/null
+++ b/rego-proofs/compiler/lib/lean.ml
@@ -0,0 +1,63 @@
+open Core
+
+type lean_expression =
+  | Comment of string
+  | Identifier of string
+  | Bool of bool
+  | String of string
+  | Number of float
+  | 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 * lean_expression list) list
+  | ForAll of judgement * lean_expression
+  | Exists of judgement * lean_expression
+  | ExistsUnique of judgement * lean_expression
+[@@deriving eq, show]
+
+and judgement = string list * string [@@deriving eq, show]
+
+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
+  | Comment s -> Printf.sprintf "\n-- %s\n" s
+  | Identifier s -> s
+  | Bool b -> if b then "True" else "False"
+  | String s -> Printf.sprintf "\"%s\"" s
+  | Number n -> Float.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)
+  | ExistsUnique (j, expr) ->
+      Printf.sprintf "∃! %s, %s" (fmt_judgement j) (fmt_lean_expression expr)
+  | Inductive (name, judgements, arms) ->
+    let fmt_arm (arm_name, exprs, values) =
+      let head =
+        Printf.sprintf
+          "%s %s"
+          name
+          (List.map ~f:fmt_lean_expression values |> String.concat ~sep:" ")
+      in
+      let body =
+        List.map ~f:fmt_lean_expression exprs
+        |> String.concat ~sep:" → "
+      in
+      Printf.sprintf "  | %s : %s → %s" arm_name body 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")