Add syntactic export to dk

CHANGES.md

@@ -3,6 +3,12 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## Unreleased
+
+### Added
+
+- add export format `raw_dk`
+
 ## 2.5.0 (2024-02-25)
 
 ### Added

Makefile

@@ -31,6 +31,7 @@ tests: lambdapi
 	@dune exec --only-packages lambdapi -- tests/dtrees.sh
 	@dune exec --only-packages lambdapi -- tests/export_dk.sh
 	@dune exec --only-packages lambdapi -- tests/export_lp.sh
+	@dune exec --only-packages lambdapi -- tests/export_raw_dk.sh
 
 .PHONY: tests_alt_ergo
 tests_alt_ergo: lambdapi
@@ -169,4 +170,3 @@ uninstall_vim_mode:
 .PHONY: build-vscode-extension
 build-vscode-extension:
 	cd editors/vscode && make && mkdir extensionFolder && vsce package -o extensionFolder
-

doc/about.rst

@@ -10,15 +10,23 @@ This allows to simplify some proofs, and formalize complex
 mathematical objects that are otherwise impossible or difficult to
 formalize in more traditional proof systems.
 
-Lambdapi can also take as input `Dedukti`_ files, and can thus be used
-as an interoperability tool.
+Lambdapi is mostly compatible with `Dedukti`_ in the sense that it can
+take Dedukti files as input and output Dedukti files as well.
 
-Lambdapi is a logical framework and does not come with a pre-defined
-logic. However, it is easy to define a logic by a few symbols and
-rules. See for instance, the file `FOL.lp
+Definitions and proofs written in Lambdapi can be exported to Coq as
+well, to some extent. Lambdapi can thus be used as an interoperability
+tool.
+
+Finally, Lambdapi is a logical framework, that is, it does not come
+with a pre-defined logic. Instead, one has to start defining its own
+logic. It is usually not too difficult to define a logic with a few
+symbols and rewrite rules, and Lambdapi comes with a `repository of
+pre-defined logics
+<https://github.com/Deducteam/lambdapi-logics>`__. See for instance,
+the file `FOL.lp
 <https://github.com/fblanqui/lib/blob/master/FOL.lp>`__ which defines
 (polymorphic) first-order logic. There also exist definitions for the
-logics of HOL, Coq or Agda.
+logics of HOL-Light, Coq or Agda.
 
 Here are some of the features of Lambdapi:
 

doc/dedukti.rst

@@ -19,13 +19,11 @@ accept the same class of identifiers and module/file names), we try to
 rename them instead of failing:
 
 - ``lp`` identifiers that are not valid ``dk`` identifiers or that are
-  ``dk`` keywords are enclosed between ``{|`` and ``|}`` and, in
-  escaped identifiers, spaces and newlines are replaced by
-  underscores.
+  ``dk`` keywords are enclosed between ``{|`` and ``|}``.
 
 - In module names, dots are replaced by underscores and, if a ``lp``
   file requires the module ``mylib.logic.untyped.fol``, its
   translation will require the file
   ``mylib_logic_untyped_fol.dk``. Therefore, in a package whose
-  ``root_path`` is ``mylib.logic``, the file ``untyped/fol.lp`` should
-  be translated into ``mylib_logic_untyped_fol.dk``.
+  ``root_path`` is ``mylib.logic``, the file ``untyped/fol.lp`` is
+  translated into ``mylib_logic_untyped_fol.dk``.

doc/options.rst

@@ -38,11 +38,11 @@ handled independently in the order they are given. The program
 immediately stops on the first failure, without going to the next file
 (if any).
 
-**index:**
+**Remark on index:**
 
 The ``index`` command generates the file ``~/.LPSearch.db``. This file contains an indexation of all the symbols and rules occurring in the dk/lp files given in argument. By default, the file ``~/.LPSearch.db`` is erased first. To append new symbols and rules, use the option ``--add``. It is also possile to normalize terms wrt some rules before indexation by using ``--rules`` options.
 
-**search:**
+**Remark on search:**
 
 The command ``search`` takes as argument a query and runs it against the index file ``~/.LPSearch.db``. See :doc:`query_language` for the specification of the query language.
 
@@ -63,13 +63,11 @@ The commands ``check``, ``decision-tree``, ``export``, ``parse``,
 
 * ``-v <NUM>``, ``--verbose=<NUM>`` sets the verbosity level to the given natural number (the default value is 1). A value of 0 should not print anything, and the higher values print more and more information.
 
-
 check
 -----
 
 * ``-c``, ``--gen-obj`` instructs Lambdapi to generate object files for every checked module (including dependencies). Object files have the extension ``.lpo`` and they are automatically read back when necessary if they exist and are up to date (they are regenerated otherwise).
 
-
 * ``--too-long=<FLOAT>`` gives a warning for each interpreted source file command taking more than the given number of seconds to be checked. The parameter ``FLOAT`` is expected to be a floating point number.
 
 export
@@ -79,14 +77,17 @@ export
 
   - ``lp``: Lambdapi format
   - ``dk``:  `Dedukti <https://github.com/Deducteam/dedukti>`__ format
+  - ``raw_dk``:  `Dedukti <https://github.com/Deducteam/dedukti>`__ format
   - ``hrs``: `HRS <http://project-coco.uibk.ac.at/problems/hrs.php>`__ format of the confluence competition
   - ``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
 
-**WARNING**: The options ``raw_coq`` and ``stt_coq`` are still experimental.
+**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.
+
+The format ``raw_dk`` does not accept the commands ``notation`` and ``inductive``, and proofs and tactics, which require elaboration.
 
-With the options ``raw_coq`` and ``stt_coq``, rules are 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`` 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>`__.
 
 For the format ``stt_coq``, several other options are available:
 

doc/vim.rst

@@ -1,5 +1,5 @@
-`Vim <https://www.vim.org/>`__
-==============================
+`Vim <https://www.vim.org/>`__ (not maintained anymore)
+=======================================================
 
 A minimal Vim mode is provided to edit Lambdapi files. It provides
 syntax highlighting and abbreviations to enter unicode characters.

src/cli/lambdapi.ml

@@ -100,7 +100,7 @@ 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 | Hrs | Xtc | RawCoq | SttCoq
+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)
@@ -115,6 +115,7 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
     | None
     | Some Lp -> Pretty.ast Format.std_formatter (Parser.parse_file file)
     | Some Dk -> Export.Dk.sign (Compile.compile_file file)
+    | Some RawDk -> Export.Rawdk.print (Parser.parse_file file)
     | Some Hrs ->
       Export.Hrs.sign Format.std_formatter (Compile.compile_file file)
     | Some Xtc ->
@@ -229,6 +230,7 @@ let output : output option CLT.t =
       match s with
       | "lp" -> Ok Lp
       | "dk" -> Ok Dk
+      | "raw_dk" -> Ok RawDk
       | "hrs" -> Ok Hrs
       | "xtc" -> Ok Xtc
       | "raw_coq" -> Ok RawCoq
@@ -240,6 +242,7 @@ let output : output option CLT.t =
         (match o with
          | Lp -> "lp"
          | Dk -> "dk"
+         | RawDk -> "raw_dk"
          | Hrs -> "hrs"
          | Xtc -> "xtc"
          | RawCoq -> "raw_coq"
@@ -249,7 +252,8 @@ let output : output option CLT.t =
   in
   let doc =
     "Set the output format of the export command. The value of $(docv) \
-     must be `lp' (default), `dk`, `hrs`, `xtc`, `raw_coq` or `stt_coq`."
+     must be `lp' (default), `raw_dk`, `dk`, `hrs`, `xtc`, `raw_coq` or \
+     `stt_coq`."
   in
   Arg.(value & opt (some output) None & info ["output";"o"] ~docv:"FMT" ~doc)
 

src/common/escape.ml

@@ -1,4 +1,5 @@
 (** Escaped identifiers ["{|...|}"]. *)
+let escape : string -> string = fun s -> "{|" ^ s ^ "|}"
 
 (** [is_escaped s] tells if [s] begins with ["{|"] and ends with ["|}"]
    without overlapping. For efficiency, we just test that it starts with
@@ -13,10 +14,10 @@ let unescape : string -> string = fun s ->
    too, then [add_prefix p n] is just [p ^ n]. Otherwise, it is ["{|" ^ p ^
    unescape n ^ "|}"]. *)
 let add_prefix : string -> string -> string = fun p n ->
-  if is_escaped n then "{|" ^ p ^ unescape n ^ "|}" else p ^ n
+  if is_escaped n then escape (p ^ unescape n) else p ^ n
 
 (** [s] is assumed to be a regular identifier. If [n] is a regular identifier
    too, then [add_suffix n s] is just [n ^ s]. Otherwise, it is ["{" ^
    unescape n ^ s ^ "|}"]. *)
 let add_suffix : string -> string -> string = fun n s ->
-  if is_escaped n then "{|" ^ unescape n ^ s ^ "|}"  else n ^ s
+  if is_escaped n then escape (unescape n ^ s)  else n ^ s

src/core/term.ml

@@ -365,7 +365,8 @@ let create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
     { elt = sym_name; pos = sym_pos } sym_decl_pos
     typ sym_impl ->
   {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None;
-   sym_opaq = ref sym_opaq; sym_rules = ref []; sym_dtree = ref Tree_type.empty_dtree;
+   sym_opaq = ref sym_opaq; sym_rules = ref [];
+   sym_dtree = ref Tree_type.empty_dtree;
    sym_mstrat; sym_prop; sym_expo; sym_pos ; sym_decl_pos }
 
 (** [is_constant s] tells whether [s] is a constant. *)

src/export/dk.ml

@@ -5,8 +5,6 @@ open Timed
 open Common
 open Core open Term
 
-let string = string
-
 (** Translation of identifiers. Lambdapi identifiers that are Dedukti keywords
    or invalid Dedukti identifiers are escaped, a feature offered by
    Dedukti. *)
@@ -56,33 +54,30 @@ let is_ident : string -> bool = fun s ->
 let is_mident : string -> bool = fun s ->
   Parsing.DkLexer.is_mident (Lexing.from_string s)
 
-let escape : string pp = fun ppf s -> out ppf "{|%s|}" s
-
-let replace_spaces : string -> string = fun s ->
+(*let replace_spaces : string -> string = fun s ->
   let open Bytes in
   let b = of_string s in
   for i=0 to length b - 1 do
     match get b i with
     | ' ' | '\n' -> set b i '_'
     | _ -> ()
   done;
-  to_string b
+  to_string b*)
 
 let ident : string pp = fun ppf s ->
-  if s = "" then escape ppf s
-  else if s.[0] = '{' then string ppf (replace_spaces s)
-  else if is_keyword s then escape ppf s
-  else if is_ident s then string ppf s
-  else escape ppf s
+  string ppf
+    (if s = "" then Escape.escape s
+     else if s.[0] = '{' then s
+     else if is_keyword s then Escape.escape s
+     else if is_ident s then s
+     else Escape.escape s)
 
 (** Translation of paths. Paths equal to the [!current_path] are not
    printed. Non-empty paths end with a dot. We assume that the module p1.p2.p3
    is in the file p1_p2_p3.dk. *)
 
 let path_elt : string pp = fun ppf s ->
-  if s <> "" && s.[0] = '{' then
-    string ppf (replace_spaces (Escape.unescape s))
-  else string ppf s
+  string ppf (if Escape.is_escaped s then Escape.unescape s else s)
 
 let current_path = Stdlib.ref []
 
@@ -91,11 +86,9 @@ let path : Path.t pp = fun ppf p ->
   match p with
   | [] -> ()
   | p ->
-      let joined_path = Format.asprintf "%a" (List.pp path_elt "_") p in
-      if List.for_all is_mident p then
-        out ppf "%s." joined_path
-      else
-        Format.fprintf ppf "%a." escape joined_path
+      let m = Format.asprintf "%a" (List.pp path_elt "_") p in
+      let m = if is_mident m then m else Escape.escape m in
+      out ppf "%s." m
 
 let qid : (Path.t * string) pp = fun ppf (p, i) ->
   out ppf "%a%a" path p ident i