Add export to Lean

doc/options.rst

@@ -82,14 +82,16 @@ export
   - ``xtc``: `XTC <https://raw.githubusercontent.com/TermCOMP/TPDB/master/xml/xtc.xsd>`__ format of the termination competition
   - ``raw_coq``: `Coq <https://coq.inria.fr/>`__ format
   - ``stt_coq``: `Coq <https://coq.inria.fr/>`__ format assuming that the input file is in an encoding of simple type theory
+  - ``raw_lean``: `Lean <https://lean-lang.org/>`__ format
+  - ``stt_lean``: `Lean <https://lean-lang.org/>`__ format assuming that the input file is in an encoding of simple type theory
 
-**WARNING**: With the formats ``raw_coq``, ``stt_coq`` and ``raw_dk``, the translation is done just after parsing, thus before scoping and elaboration. So Lambdapi cannot translate any input file, and the output may be incomplete or fail to type-check.
+**WARNING**: With the formats ``raw_coq``, ``stt_coq``, ``raw_lean``, ``stt_lean`` and ``raw_dk``, the translation is done just after parsing, thus before scoping and elaboration. So Lambdapi cannot translate any input file, and the output may be incomplete or fail to type-check.
 
 The format ``raw_dk`` does not accept the commands ``notation`` and ``inductive``, and proofs and tactics, which require elaboration.
 
-The formats ``raw_coq`` and ``stt_coq`` only accept the commands ``require``, ``open``, ``symbol`` and ``rule``, but rules are simply ignored. The encoding of simple type theory can however be defined in Coq using `STTfa.v <https://github.com/Deducteam/lambdapi/blob/master/libraries/sttfa.v>`__.
+The formats ``raw_coq``, ``stt_coq``, ``raw_lean`` and ``stt_lean`` only accept the commands ``require``, ``open``, ``symbol`` and ``rule``, but rules are simply ignored. The encoding of simple type theory can however be defined in Coq using `STTfa.v <https://github.com/Deducteam/lambdapi/blob/master/libraries/sttfa.v>`__.
 
-For the format ``stt_coq``, several other options are available:
+For the formats ``stt_coq`` and ``stt_lean``, several other options are available:
 
 * ``--encoding <LP_FILE>`` (mandatory option) where ``<LP_FILE>`` contains the following sequence of builtin declarations:
 
@@ -118,11 +120,11 @@ In symbol declarations or definitions, parameters with no type are assumed to be
 
 ::
 
-   builtin "coq_expr" ≔ lp_id;
+   builtin "expr" ≔ lp_id;
 
-It instructs Lambdapi to replace any occurrence of the unqualified identifier ``lp_id`` by ``coq_expr``, which can be any Coq expression. Example: `renaming.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/renaming.lp>`__.
+It instructs Lambdapi to replace any occurrence of the unqualified identifier ``lp_id`` by ``expr``, which can be any expression. Example: `renaming.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/renaming.lp>`__.
 
-* ``--requiring <MODNAME>`` to add ``Require Import <MODNAME>`` at the beginning of the output. ``<MODNAME>.v`` usually needs to contain at least the following definitions:
+* ``--requiring <MODNAME>`` to add ``Require Import <MODNAME>`` at the beginning of the output. ``<MODNAME>.v`` (and similarly ``<MODNAME>.lean``) usually needs to contain at least the following definitions:
 
 ::
 

src/cli/lambdapi.ml

@@ -100,7 +100,8 @@ let parse_cmd : Config.t -> string list -> unit = fun cfg files ->
   Error.handle_exceptions run
 
 (** Possible outputs for the export command. *)
-type output = Lp | Dk | RawDk | Hrs | Xtc | RawCoq | SttCoq
+type output =
+  Lp | Dk | RawDk | Hrs | Xtc | RawCoq | SttCoq | RawLean | SttLean
 
 (** Running the export mode. *)
 let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
@@ -109,8 +110,8 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
       (file:string) : unit =
   let run _ =
     Config.init {cfg with verbose = Some 0};
-    Export.Coq.use_implicits := not no_implicits;
-    Export.Coq.use_notations := use_notations;
+    Export.Stt.use_implicits := not no_implicits;
+    Export.Stt.use_notations := use_notations;
     match output with
     | None
     | Some Lp -> Pretty.ast Format.std_formatter (Parser.parse_file file)
@@ -121,16 +122,27 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
     | Some Xtc ->
       Export.Xtc.sign Format.std_formatter (Compile.compile_file file)
     | Some RawCoq ->
-        Export.Coq.stt := false;
-        Option.iter Export.Coq.set_renaming renaming;
+        Export.Stt.stt := false;
+        Option.iter Export.Stt.set_renaming renaming;
         Export.Coq.print (Parser.parse_file file)
     | Some SttCoq ->
-        Export.Coq.stt := true;
-        Option.iter Export.Coq.set_renaming renaming;
-        Option.iter Export.Coq.set_encoding encoding;
-        Option.iter Export.Coq.set_mapping mapping;
-        Option.iter Export.Coq.set_requiring requiring;
+        Export.Stt.stt := true;
+        Option.iter Export.Stt.set_renaming renaming;
+        Option.iter Export.Stt.set_encoding encoding;
+        Option.iter Export.Stt.set_mapping mapping;
+        Option.iter Export.Stt.set_requiring requiring;
         Export.Coq.print (Parser.parse_file file)
+    | Some RawLean ->
+        Export.Stt.stt := false;
+        Option.iter Export.Stt.set_renaming renaming;
+        Export.Lean.print file (Parser.parse_file file)
+    | Some SttLean ->
+        Export.Stt.stt := true;
+        Option.iter Export.Stt.set_renaming renaming;
+        Option.iter Export.Stt.set_encoding encoding;
+        Option.iter Export.Stt.set_mapping mapping;
+        Option.iter Export.Stt.set_requiring requiring;
+        Export.Lean.print file (Parser.parse_file file)
   in Error.handle_exceptions run
 
 (** Running the LSP server. *)
@@ -235,6 +247,8 @@ let output : output option CLT.t =
       | "xtc" -> Ok Xtc
       | "raw_coq" -> Ok RawCoq
       | "stt_coq" -> Ok SttCoq
+      | "raw_lean" -> Ok RawLean
+      | "stt_lean" -> Ok SttLean
       | _ -> Error(`Msg "Invalid format")
     in
     let print fmt o =
@@ -246,14 +260,16 @@ let output : output option CLT.t =
          | Hrs -> "hrs"
          | Xtc -> "xtc"
          | RawCoq -> "raw_coq"
-         | SttCoq -> "stt_coq")
+         | SttCoq -> "stt_coq"
+         | RawLean -> "raw_lean"
+         | SttLean -> "stt_lean")
     in
     Arg.conv (parse, print)
   in
   let doc =
     "Set the output format of the export command. The value of $(docv) \
-     must be `lp' (default), `raw_dk`, `dk`, `hrs`, `xtc`, `raw_coq` or \
-     `stt_coq`."
+     must be `lp' (default), `raw_dk`, `dk`, `hrs`, `xtc`, `raw_coq`, \
+     `stt_coq`, `raw_lean` or `stt_lean`."
   in
   Arg.(value & opt (some output) None & info ["output";"o"] ~docv:"FMT" ~doc)
 
@@ -263,7 +279,7 @@ let encoding : string option CLT.t =
     let print fmt s = string fmt s in
     Arg.conv (parse, print)
   in
-  let doc = "Set config file for the command export -o stt_coq." in
+  let doc = "Set config file for the command export -o stt_[coq|lean]." in
   Arg.(value & opt (some encoding) None & info ["encoding"] ~docv:"FILE" ~doc)
 
 let renaming : string option CLT.t =
@@ -272,7 +288,7 @@ let renaming : string option CLT.t =
     let print fmt s = string fmt s in
     Arg.conv (parse, print)
   in
-  let doc = "Set config file for the command export -o stt_coq." in
+  let doc = "Set config file for the command export -o stt_[coq|lean]." in
   Arg.(value & opt (some renaming) None & info ["renaming"] ~docv:"FILE" ~doc)
 
 let mapping : string option CLT.t =
@@ -281,7 +297,7 @@ let mapping : string option CLT.t =
     let print fmt s = string fmt s in
     Arg.conv (parse, print)
   in
-  let doc = "Set config file for the command export -o stt_coq." in
+  let doc = "Set config file for the command export -o stt_[coq|lean]." in
   Arg.(value & opt (some mapping) None & info ["mapping"] ~docv:"FILE" ~doc)
 
 let requiring : string option CLT.t =
@@ -290,7 +306,7 @@ let requiring : string option CLT.t =
     let print fmt s = string fmt s in
     Arg.conv (parse, print)
   in
-  let doc = "Set config file for the command export -o stt_coq." in
+  let doc = "Set config file for the command export -o stt_[coq|lean]." in
   Arg.(value & opt (some requiring) None
        & info ["requiring"] ~docv:"FILE" ~doc)
 
@@ -299,7 +315,7 @@ let no_implicits : bool CLT.t =
   Arg.(value & flag & info ["no-implicits"] ~doc)
 
 let use_notations : bool CLT.t =
-  let doc = "Generate Coq code using notations." in
+  let doc = "Generate code using notations." in
   Arg.(value & flag & info ["use-notations"] ~doc)
 
 (** Remaining arguments: source files. *)