Add export to Lean

doc/options.rst

@@ -100,14 +100,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:
 
@@ -136,11 +138,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

@@ -165,7 +165,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)
@@ -174,8 +175,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)
@@ -186,16 +187,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. *)
@@ -300,6 +312,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 =
@@ -311,14 +325,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)
 
@@ -328,7 +344,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 =
@@ -337,7 +353,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 =
@@ -346,7 +362,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 =
@@ -355,7 +371,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)
 
@@ -364,7 +380,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. *)

src/export/coq.ml

@@ -18,191 +18,10 @@ The renaming map can be specified through a lambdapi file (option --renaming).
 open Lplib open Extra
 open Common open Pos open Error
 open Parsing open Syntax
-open Core
-
-let log = Logger.make 'x' "xprt" "export"
-let log = log.pp
-
-(** Symbols necessary to encode STT. *)
-
-type builtin =
-  Set | Prop | Arr | El | Imp | All | Prf | Eq | Or | And | Ex | Not
-
-let index_of_builtin = function
-  | Set -> 0 | Prop -> 1 | Arr -> 2 | El -> 3 | Imp -> 4 | All -> 5
-  | Prf -> 6 | Eq -> 7 | Or -> 8 | And -> 9 | Ex -> 10 | Not -> 11
-
-let nb_builtins = 12
-
-let builtin_of_index = function
-  | 0 -> Set | 1 -> Prop | 2 -> Arr | 3 -> El | 4 -> Imp | 5 -> All
-  | 6 -> Prf | 7 -> Eq | 8 -> Or | 9 -> And | 10 -> Ex | 11 -> Not
-  | _ -> assert false
-
-let _ = (* sanity check *)
-  for i = 0 to nb_builtins - 1 do
-    assert (index_of_builtin (builtin_of_index i) = i)
-  done
-
-let index_of_name = function
-  | "Set" -> Some 0 | "prop" -> Some 1 | "arr" -> Some 2 | "El" -> Some 3
-  | "imp" -> Some 4 | "all" -> Some 5 | "Prf" -> Some 6 | "eq" -> Some 7
-  | "or" -> Some 8 | "and" -> Some 9 | "ex" -> Some 10 | "not" -> Some 11
-  | _ -> None
-
-let name_of_index = function
-  | 0 -> "Set" | 1 -> "prop" | 2 -> "arr" | 3 -> "El" | 4 -> "imp"| 5 -> "all"
-  | 6 -> "Prf" | 7 -> "eq" | 8 -> "or" | 9 -> "and" | 10 -> "ex" | 11 -> "not"
-  | _ -> assert false
-
-let _ = (* sanity check *)
-  for i = 0 to nb_builtins - 1 do
-    assert (index_of_name (name_of_index i) = Some i)
-  done
-
-let builtin : Term.qident array =
-  let path = ["STTfa"] in
-  Array.init nb_builtins (fun i -> path, name_of_index i)
-
-let sym b = builtin.(index_of_builtin b)
-
-(** Set renaming map from file. *)
-
-let rmap = ref StrMap.empty
-
-let set_renaming : string -> unit = fun f ->
-  let consume = function
-    | {elt=P_builtin(coq_id,{elt=([],lp_id);_});_} ->
-        if Logger.log_enabled() then log "rename %s into %s" lp_id coq_id;
-        rmap := StrMap.add lp_id coq_id !rmap
-    | {pos;_} -> fatal pos "Invalid command."
-  in
-  Stream.iter consume (Parser.parse_file f)
-
-(** Set symbols whose declarations have to be erased. *)
-
-let erase = ref StrSet.empty
-
-module Qid = struct type t = Term.qident let compare = Stdlib.compare end
-module QidMap = Map.Make(Qid)
-
-let map_erased_qid_coq = ref QidMap.empty
-
-let set_mapping : string -> unit = fun f ->
-  let consume = function
-    | {elt=P_builtin(coq_id,lp_qid);_} ->
-        if Logger.log_enabled() then
-          log "rename %a into %s" Pretty.qident lp_qid coq_id;
-        let id = snd lp_qid.elt in
-        if Logger.log_enabled() then log "erase %s" id;
-        erase := StrSet.add id !erase;
-        map_erased_qid_coq :=
-          QidMap.add lp_qid.elt coq_id !map_erased_qid_coq;
-        if fst lp_qid.elt = [] && id <> coq_id then
-          rmap := StrMap.add id coq_id !rmap
-    | {pos;_} -> fatal pos "Invalid command."
-  in
-  Stream.iter consume (Parser.parse_file f)
-
-(** Set encoding. *)
-
-let map_qid_builtin = ref QidMap.empty
-
-let set_encoding : string -> unit = fun f ->
-  let found = Array.make nb_builtins false in
-  let consume = function
-    | {elt=P_builtin(n,lp_qid);pos} ->
-        begin match index_of_name n with
-        | Some i ->
-            if Logger.log_enabled() then
-              log "builtin \"%s\" = %a" n Pretty.qident lp_qid;
-            builtin.(i) <- lp_qid.elt;
-            found.(i) <- true;
-            let b = builtin_of_index i in
-            map_qid_builtin := QidMap.add lp_qid.elt b !map_qid_builtin;
-            if b = El || b = Prf then
-              (if Logger.log_enabled() then log "erase %s" (snd lp_qid.elt);
-               erase := StrSet.add (snd lp_qid.elt) !erase)
-        | None -> fatal pos "Unknown builtin."
-        end
-    | {pos;_} -> fatal pos "Invalid command."
-  in
-  Stream.iter consume (Parser.parse_file f);
-  Array.iteri
-    (fun i b ->
-      if not b then
-        let pos =
-          Some {fname=Some f;start_line=0;start_col=0;start_offset=0;
-                end_line=0;end_col=0;end_offset=0}
-        in fatal pos "Builtin %s undefined." (name_of_index i))
-    found
-
-(** Basic printing functions. We use Printf for efficiency reasons. *)
-let out = Printf.printf
-
-let char = output_char
-let string = output_string
-
-let prefix pre elt oc x = string oc pre; elt oc x
-let suffix elt suf oc x = elt oc x; string oc suf
-
-let list elt sep oc xs =
-  match xs with
-  | [] -> ()
-  | x::xs -> elt oc x; List.iter (prefix sep elt oc) xs
-
-(** Translation of identifiers. *)
-
-let translate_ident : string -> string = fun s ->
-  try StrMap.find s !rmap with Not_found -> s
-
-let raw_ident oc s = string oc (translate_ident s)
-
-let ident oc {elt;_} = raw_ident oc elt
-
-let param_id oc idopt =
-  match idopt with
-  | Some id -> ident oc id
-  | None    -> char oc '_'
-
-let param_ids = list param_id " "
-
-let raw_path = list string "."
-
-let path oc {elt;_} = raw_path oc elt
-
-let qident oc {elt=(mp,s);_} =
-  match mp with
-  | [] -> raw_ident oc s
-  | _::_ -> raw_path oc mp; char oc '.'; raw_ident oc s
+open Stt
 
 (** Translation of terms. *)
 
-let stt = Stdlib.ref false
-let use_implicits = Stdlib.ref false
-let use_notations = Stdlib.ref false
-
-(* redefinition of p_get_args ignoring P_Wrap's. *)
-let p_get_args : p_term -> p_term * p_term list = fun t ->
-  let rec p_get_args t acc =
-    match t.elt with
-    | P_Appl(t, u) -> p_get_args t (u::acc)
-    | P_Wrap t -> p_get_args t acc
-    | _ -> t, acc
-  in p_get_args t []
-
-let app t default cases =
-  let h, ts = p_get_args t in
-  if !stt then
-    match h.elt with
-    | P_Iden({elt;_},expl) ->
-        begin match QidMap.find_opt elt !map_qid_builtin with
-        | None -> default h ts
-        | Some builtin -> cases h ts expl builtin
-        end
-    | _ -> default h ts
-  else default h ts
-
 let rec term oc t =
   (*if Logger.log_enabled() then
     log "pp %a" (*Pos.short t.pos*) Pretty.term t;*)
@@ -217,7 +36,7 @@ let rec term oc t =
   | P_Iden(qid,b) ->
       if b then char oc '@';
       if !stt then
-        match QidMap.find_opt qid.elt !map_erased_qid_coq with
+        match QidMap.find_opt qid.elt !map_erased_qid with
         | Some s -> string oc s
         | None -> qident oc qid
       else qident oc qid
@@ -288,8 +107,6 @@ and typopt oc t = Option.iter (prefix " : " term oc) t
 
 (** Translation of commands. *)
 
-let is_lem x = is_opaq x || is_priv x
-
 let command oc {elt; pos} =
   begin match elt with
   | P_open(true,ps) ->
@@ -345,18 +162,14 @@ let command oc {elt; pos} =
   | _ -> wrn pos "Command not translated."
   end
 
-let ast oc = Stream.iter (command oc)
+let commands oc = Stream.iter (command oc)
 
 (** Set Coq required file. *)
 
-let require = ref None
-
-let set_requiring : string -> unit = fun f -> require := Some f
-
 let print : ast -> unit = fun s ->
   let oc = stdout in
   begin match !require with
   | Some f -> string oc ("Require Import "^f^".\n")
   | None -> ()
   end;
-  ast oc s
+  commands oc s