rename option --erasing into --mapping (#1179)

CHANGES.md

@@ -15,6 +15,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Changed
 
+- Option '--erasing' renamed into '--mapping'.
 - The export option `--requiring` does not require as argument a file with extension `.v` anymore: the argument must be a module name.
 
 ## 2.5.1 (2024-07-22)

doc/options.rst

@@ -132,7 +132,7 @@ It instructs Lambdapi to replace any occurrence of the unqualified identifier ``
 
 if the symbols corresponding to the builtins ``"arr"``, ``"imp"`` and ``"all"`` occurs partially applied in the input file. Example: `coq.v <https://github.com/Deducteam/lambdapi/blob/master/libraries/coq.v>`__.
 
-* ``--erasing <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations like for the option ``--renaming`` except that, this time, ``lp_id`` can be a qualified identifier. It has the same effect as the option ``--renaming`` plus it removes any declaration of the renamed symbols. ``coq_expr`` therefore needs to be defined in Coq standard library or in the Coq file specified with the option ``--requiring``. It is not necessary to have entries for the symbols corresponding to the builtins ``"El"`` and ``"Prf"`` declared with the option ``--encoding`` since they are erased automatically. Example: `erasing.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/erasing.lp>`__.
+* ``--mapping <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations like for the option ``--renaming`` except that, this time, ``lp_id`` can be a qualified identifier. It has the same effect as the option ``--renaming`` plus it removes any declaration of the renamed symbols. ``coq_expr`` therefore needs to be defined in Coq standard library or in the Coq file specified with the option ``--requiring``. It is not necessary to have entries for the symbols corresponding to the builtins ``"El"`` and ``"Prf"`` declared with the option ``--encoding`` since they are erased automatically. Example: `mapping.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/mapping.lp>`__.
 
 * ``--use-notations`` instructs Lambdapi to use the usual Coq notations for the symbols corresponding to the builtins ``"eq"``, ``"not"``, ``"and"`` and ``"or"``.
 

libraries/dk2coq.mk

@@ -2,7 +2,7 @@ SRC := $(wildcard *.dk)
 
 default: $(SRC:%.dk=%.v)
 
-LAMBDAPI = lambdapi export -o stt_coq --encoding ../encoding.lp --erasing ../erasing.lp --renaming ../renaming.lp --requiring coq.v --no-implicits
+LAMBDAPI = lambdapi export -o stt_coq --encoding ../encoding.lp --mapping ../mapping.lp --renaming ../renaming.lp --requiring coq.v --no-implicits
 
 %.v: %.dk
 	$(LAMBDAPI) $< > $@

libraries/dk2sttcoq.sh

@@ -15,7 +15,7 @@ do
 done
 sed -i -e 's/^hol.//' -e 's/def hol./def /' -e 's/thm hol./thm /' hol.dk
 
-# because "type" is not accepted in erasing.lp
+# because "type" is not accepted in mapping.lp
 echo replace \"hol.type\" by \"hol.typ\" in all dk files ...
 sed -i -e 's/^type /typ /' hol.dk
 sed -i -e 's/hol.type/hol.typ/g' *.dk

src/cli/lambdapi.ml

@@ -104,7 +104,7 @@ type output = Lp | Dk | RawDk | Hrs | Xtc | RawCoq | SttCoq
 
 (** Running the export mode. *)
 let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
-      (erasing:string option) (renaming:string option)
+      (mapping:string option) (renaming:string option)
       (requiring:string option) (no_implicits:bool) (use_notations:bool)
       (file:string) : unit =
   let run _ =
@@ -128,7 +128,7 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
         Export.Coq.stt := true;
         Option.iter Export.Coq.set_renaming renaming;
         Option.iter Export.Coq.set_encoding encoding;
-        Option.iter Export.Coq.set_erasing erasing;
+        Option.iter Export.Coq.set_mapping mapping;
         Option.iter Export.Coq.set_requiring requiring;
         Export.Coq.print (Parser.parse_file file)
   in Error.handle_exceptions run
@@ -275,14 +275,14 @@ let renaming : string option CLT.t =
   let doc = "Set config file for the command export -o stt_coq." in
   Arg.(value & opt (some renaming) None & info ["renaming"] ~docv:"FILE" ~doc)
 
-let erasing : string option CLT.t =
-  let erasing : string Arg.conv =
+let mapping : string option CLT.t =
+  let mapping : string Arg.conv =
     let parse (s: string) : (string, [>`Msg of string]) result = Ok s in
     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
-  Arg.(value & opt (some erasing) None & info ["erasing"] ~docv:"FILE" ~doc)
+  Arg.(value & opt (some mapping) None & info ["mapping"] ~docv:"FILE" ~doc)
 
 let requiring : string option CLT.t =
   let requiring : string Arg.conv =
@@ -372,7 +372,7 @@ let parse_cmd =
 let export_cmd =
   let doc = "Translate the given files to other formats." in
   Cmd.v (Cmd.info "export" ~doc ~man:man_pkg_file)
-    CLT.(const export_cmd $ Config.full $ output $ encoding $ erasing
+    CLT.(const export_cmd $ Config.full $ output $ encoding $ mapping
          $ renaming $ requiring $ no_implicits $ use_notations $ file)
 
 let lsp_server_cmd =

src/export/coq.ml

@@ -88,7 +88,7 @@ module QidMap = Map.Make(Qid)
 
 let map_erased_qid_coq = ref QidMap.empty
 
-let set_erasing : string -> unit = fun f ->
+let set_mapping : string -> unit = fun f ->
   let consume = function
     | {elt=P_builtin(coq_id,lp_qid);_} ->
         if Logger.log_enabled() then