From 21ee7f3d5b5542906ffe1ddaefee147f41cdedc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 21 Jan 2025 14:35:34 +0100 Subject: [PATCH] rename option --erasing into --mapping (#1179) --- CHANGES.md | 1 + doc/options.rst | 2 +- libraries/dk2coq.mk | 2 +- libraries/dk2sttcoq.sh | 2 +- libraries/{erasing.lp => mapping.lp} | 0 src/cli/lambdapi.ml | 12 ++++++------ src/export/coq.ml | 2 +- 7 files changed, 11 insertions(+), 10 deletions(-) rename libraries/{erasing.lp => mapping.lp} (100%) diff --git a/CHANGES.md b/CHANGES.md index 6cf9ea168..bce9602d3 100644 --- a/CHANGES.md +++ b/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) diff --git a/doc/options.rst b/doc/options.rst index f614aa072..4a8c6acc3 100644 --- a/doc/options.rst +++ b/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 `__. -* ``--erasing `` where ```` 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 `__. +* ``--mapping `` where ```` 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 `__. * ``--use-notations`` instructs Lambdapi to use the usual Coq notations for the symbols corresponding to the builtins ``"eq"``, ``"not"``, ``"and"`` and ``"or"``. diff --git a/libraries/dk2coq.mk b/libraries/dk2coq.mk index 07fb21c16..887d67438 100644 --- a/libraries/dk2coq.mk +++ b/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) $< > $@ diff --git a/libraries/dk2sttcoq.sh b/libraries/dk2sttcoq.sh index c35cbca2f..f31fcece5 100755 --- a/libraries/dk2sttcoq.sh +++ b/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 diff --git a/libraries/erasing.lp b/libraries/mapping.lp similarity index 100% rename from libraries/erasing.lp rename to libraries/mapping.lp diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index 5557e6e15..7b8bb321a 100644 --- a/src/cli/lambdapi.ml +++ b/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 = diff --git a/src/export/coq.ml b/src/export/coq.ml index 395b15899..09627d892 100644 --- a/src/export/coq.ml +++ b/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