From 8dc823f5cc8a5ee7660d9fe813d213500dd07f57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 25 Oct 2023 17:11:14 +0200 Subject: [PATCH] coq export: treat P_NLit as P_Iden (#1015) --- doc/options.rst | 2 +- src/export/coq.ml | 12 +++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/doc/options.rst b/doc/options.rst index 5e5ed40d7..8cc25bbf3 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -129,7 +129,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 `__. +* ``--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 `__. * ``--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/src/export/coq.ml b/src/export/coq.ml index b870572c7..7b0e10ce9 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -94,8 +94,9 @@ let set_erasing : string -> unit = fun f -> | {elt=P_builtin(coq_id,lp_qid);_} -> if Logger.log_enabled() then log "rename %a into %s" Pretty.qident lp_qid coq_id; - if Logger.log_enabled() then log "erase %s" (snd lp_qid.elt); - erase := StrSet.add (snd lp_qid.elt) !erase; + 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 | {pos;_} -> fatal pos "Invalid command." in @@ -194,7 +195,12 @@ let rec term : p_term pp = fun ppf t -> | P_Expl _ -> wrn t.pos "TODO"; assert false | P_Type -> out ppf "Type" | P_Wild -> out ppf "_" - | P_NLit i -> raw_ident ppf i + | P_NLit i -> + if !stt then + match QidMap.find_opt ([],i) !map_erased_qid_coq with + | Some s -> string ppf s + | None -> raw_ident ppf i + else raw_ident ppf i | P_Iden(qid,b) -> if b then out ppf "@@"; if !stt then