diff --git a/rr_frontend/Cargo.lock b/rr_frontend/Cargo.lock
index dd573b9880d008a4ef9c7a5674c620272d2c145b..f9e207be4fb2c2aa54835c975d5aaf3cf6f2c632 100644
--- a/rr_frontend/Cargo.lock
+++ b/rr_frontend/Cargo.lock
@@ -133,12 +133,58 @@ dependencies = [
"memchr",
]
+[[package]]
+name = "darling"
+version = "0.14.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7b750cb3417fd1b327431a470f388520309479ab0bf5e323505daf0290cd3850"
+dependencies = [
+ "darling_core",
+ "darling_macro",
+]
+
+[[package]]
+name = "darling_core"
+version = "0.14.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "109c1ca6e6b7f82cc233a97004ea8ed7ca123a9af07a8230878fcfda9b158bf0"
+dependencies = [
+ "fnv",
+ "ident_case",
+ "proc-macro2",
+ "quote",
+ "strsim",
+ "syn 1.0.109",
+]
+
+[[package]]
+name = "darling_macro"
+version = "0.14.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a4aab4dbc9f7611d8b55048a3a16d2d010c2c8334e46304b40ac1cc14bf3b48e"
+dependencies = [
+ "darling_core",
+ "quote",
+ "syn 1.0.109",
+]
+
[[package]]
name = "datafrog"
version = "2.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a0afaad2b26fa326569eb264b1363e8ae3357618c43982b3f285f0774ce76b69"
+[[package]]
+name = "derive-new"
+version = "0.5.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3418329ca0ad70234b9735dc4ceed10af4df60eff9c8e7b06cb5e520d92c3535"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
[[package]]
name = "derive_more"
version = "0.99.17"
@@ -221,6 +267,33 @@ version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
+[[package]]
+name = "fnv"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
+
+[[package]]
+name = "from_variants"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4e859c8f2057687618905dbe99fc76e836e0a69738865ef90e46fc214a41bbf2"
+dependencies = [
+ "from_variants_impl",
+]
+
+[[package]]
+name = "from_variants_impl"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "55a5e644a80e6d96b2b4910fa7993301d7b7926c045b475b62202b20a36ce69e"
+dependencies = [
+ "darling",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
[[package]]
name = "hashbrown"
version = "0.14.3"
@@ -239,6 +312,12 @@ version = "2.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
+[[package]]
+name = "ident_case"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39"
+
[[package]]
name = "indent_write"
version = "2.2.0"
@@ -394,7 +473,9 @@ dependencies = [
name = "radium"
version = "0.1.0"
dependencies = [
+ "derive-new",
"derive_more 1.0.0-beta.6",
+ "from_variants",
"indent_write",
"indoc",
"itertools",
@@ -532,6 +613,12 @@ version = "1.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
+[[package]]
+name = "strsim"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
+
[[package]]
name = "syn"
version = "1.0.109"
diff --git a/rr_frontend/Cargo.toml b/rr_frontend/Cargo.toml
index ec8d9f9ef3c27a60c28706a6e911fe5a51bda4bf..fe1903586565a5c8eb8af2a7a60c4dd8b681dbd6 100644
--- a/rr_frontend/Cargo.toml
+++ b/rr_frontend/Cargo.toml
@@ -21,8 +21,10 @@ analysis = { git = "https://github.com/viperproject/prusti-dev.git", rev = "24bd
config = { version = "0.14", default-features = false, features = ["toml"] }
csv = "1"
datafrog = "2"
-derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "display"] }
+derive-new = "0.5"
+derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "deref_mut", "display"] }
env_logger = { version = "0.11" }
+from_variants = "1"
glob = "0.3"
indent_write = "2"
indoc = "2"
diff --git a/rr_frontend/radium/Cargo.toml b/rr_frontend/radium/Cargo.toml
index 2849d38c3259270ee2f8287dd1a19e8f66481eef..67a7cf8caf2d727408cd358282797ccd2ef15ce3 100644
--- a/rr_frontend/radium/Cargo.toml
+++ b/rr_frontend/radium/Cargo.toml
@@ -8,9 +8,11 @@ repository.workspace = true
version.workspace = true
[dependencies]
-typed-arena.workspace = true
+derive-new.workspace = true
derive_more.workspace = true
+from_variants.workspace = true
indent_write.workspace = true
indoc.workspace = true
log.workspace = true
itertools.workspace = true
+typed-arena.workspace = true
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index 4ada12f13703ce103361592702cfba3bf0b93563..6bc9590c55177761f5c4f46bbd48cc386a53a4db 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -4,16 +4,411 @@
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
-/// A collection of types to represent and generate [Rocq] code.
-///
-/// These types are intended to be used for the purposes of the [RefinedRust project].
-/// As such, they may not be suitable for general use.
-///
-/// This crate is split up in the same way as the [Rocq reference documentation].
-///
-/// [RefinedRust project]: https://plv.mpi-sws.org/refinedrust/
-/// [Rocq]: https://coq.inria.fr
-/// [Rocq reference]: https://coq.inria.fr/doc/master/refman/index.html
+//! A collection of types for representing and generating [Rocq] code.
+//!
+//! These types are intended to be used for the purposes of the [RefinedRust project].
+//! As such, they may not be suitable for general use.
+//!
+//! ---
+//!
+//! This crate is divided in a similar way to the grammar defined in the [Rocq reference] documentation, but
+//! is not followed strictly:
+//! - Unstructured sentences have been reunited under a single structure, such as `Section`/`End`.
+//! - Some cases are unified for simplicity, such as `command`/`control_command`/`query_command`.
+//!
+//! The syntax used to create structures is designed to write as little code as possible, with choices
+//! explained in the Notes section.
+//!
+//! ---
+//!
+//! Following the [Rocq reference], most of the types can be structured as nested enumerations.
+//! However, some types can take optional attributes that will be left empty most of the time:
+//! - Structures wrapping the element are required, suffixed with `Attrs`.
+//! - Consuming builder pattern, without any validation, is used to fill the attributes.
+//!
+//! ---
+//!
+//! Each enumeration derives the `From` trait for each variant, and each element wrapped in an `Attr`
+//! structure are coerced into the parent enumeration using the same `From` trait.
+//!
+//! This concept makes sense when each arguments expects a type that can be coerced into the final expected
+//! type, allowing the user not to explicitly write `.into()` everywhere.
+//!
+//! # Examples
+//!
+//! Let's write the following [Rocq] code:
+//! ```text
+//! From Coq.Strings Require Import String.
+//! Open Scope string_scope.
+//! Compute "Hello World".
+//! ```
+//!
+//! This code can be generated with the following Rust code:
+//! ```
+//! # use radium::coq::*;
+//! // Document(vec![
+//! // TODO
+//! // ]);
+//! ```
+//!
+//! This code can be reduced using coercions in the following Rust code:
+//! ```
+//! # use radium::coq::*;
+//! // Document::new(vec![
+//! // TODO
+//! // ]);
+//! ```
+//!
+//! # Notes
+//!
+//! This section explains the various design decisions that have been made.
+//! It also allows a developer to understand how to contribute to this crate.
+//!
+//! Throughout this section, let's take the following example:
+//! ```
+//! struct FieldAttrs {
+//! field: Field,
+//! attributes: Option<String>,
+//! };
+//!
+//! enum Field {
+//! Foo,
+//! Bar,
+//! };
+//! ```
+//!
+//! ## Filling the attributes
+//!
+//! The following idiomatic code could be used, but it is too verbose as each field must be filled.
+//! Also, this syntax is not resilient to future changes in the structure of types:
+//! ```
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! FieldAttrs {
+//! field: Field::Foo,
+//! attributes: None,
+//! };
+//! ```
+//!
+//! The following idiomatic syntax cannot be used because some types contain an enumeration:
+//! ``` compile_fail
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! FieldAttrs {
+//! field: Field::Foo,
+//! ..FieldAttrs::default() // Error: `Field` is an enumeration without a default value.
+//! };
+//! ```
+//!
+//! Instead, the following builder pattern is preferred where mandatory fields are filled on creation, and
+//! optional fields are filled with a method call:
+//! ```
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! impl FieldAttrs {
+//! fn new(field: Field) -> Self {
+//! let attributes = None;
+//!
+//! Self { field, attributes }
+//! }
+//!
+//! fn attributes(self, attributes: String) -> Self {
+//! let attributes = Some(attributes);
+//!
+//! Self { attributes, ..self }
+//! }
+//! }
+//!
+//! FieldAttrs::new(Field::Foo).attributes("Hello".to_string());
+//! ```
+//!
+//! There are several builder patterns available, but owned (_aka consuming_) builder pattern has been chosen:
+//! - It is possible to chain method calls to keep everything concise.
+//! - There is no need to `.copy()`/`.clone()` objects to build the final object.
+//! - No verification is performed, which would be unmaintainable and currently outside the scope of this
+//! crate.
+//! - Therefore, there is no need to `.build()?` the object, as it can be considered built after each step.
+//!
+//! ## Type coercions
+//!
+//! Let's take the following code, which is simple but already verbose:
+//! ```
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! # impl FieldAttrs {
+//! # fn new(field: Field) -> Self { Self { field, attributes: None } }
+//! # fn attributes(self, attributes: String) -> Self { Self { attributes: Some(attributes), ..self } }
+//! # }
+//! use derive_more::{Deref, DerefMut};
+//!
+//! #[derive(Deref, DerefMut)]
+//! struct Entries(Vec<Entry>);
+//!
+//! enum Entry {
+//! FieldAttrs(FieldAttrs),
+//! };
+//!
+//! Entries(vec![
+//! Entry::FieldAttrs(FieldAttrs::new(Field::Foo)),
+//! Entry::FieldAttrs(FieldAttrs::new(Field::Bar).attributes("Hello".to_string())),
+//! ]);
+//! ```
+//!
+//! Writing the attribute structure can be unnecessarily verbose if no attributes are given.
+//!
+//! To avoid this, the `From<Field>` trait is derived for `Entry`, resulting in the following syntax:
+//! ```
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! # impl FieldAttrs {
+//! # fn new(field: Field) -> Self { Self { field, attributes: None } }
+//! # fn attributes(self, attributes: String) -> Self { Self { attributes: Some(attributes), ..self } }
+//! # }
+//! use derive_more::{Deref, DerefMut};
+//!
+//! #[derive(Deref, DerefMut)]
+//! struct Entries(Vec<Entry>);
+//!
+//! enum Entry {
+//! FieldAttrs(FieldAttrs),
+//! };
+//!
+//! impl From<Field> for Entry {
+//! fn from(field: Field) -> Self {
+//! Self::FieldAttrs(FieldAttrs::new(field))
+//! }
+//! }
+//!
+//! Entries(vec![
+//! Field::Foo.into(),
+//! Entry::FieldAttrs(FieldAttrs::new(Field::Bar).attributes("Hello".to_string())),
+//! ]);
+//! ```
+//!
+//! Similarly, the `.into()` method can be derived for each enumeration variant using `FromVariant`:
+//! ```
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! # impl FieldAttrs {
+//! # fn new(field: Field) -> Self { Self { field, attributes: None } }
+//! # fn attributes(self, attributes: String) -> Self { Self { attributes: Some(attributes), ..self } }
+//! # }
+//! # impl From<Field> for Entry {
+//! # fn from(field: Field) -> Self { Self::FieldAttrs(FieldAttrs::new(field)) }
+//! # }
+//! use derive_more::{Deref, DerefMut};
+//! use from_variants::FromVariants;
+//!
+//! #[derive(Deref, DerefMut)]
+//! struct Entries(Vec<Entry>);
+//!
+//! #[derive(FromVariants)]
+//! enum Entry {
+//! FieldAttrs(FieldAttrs),
+//! };
+//!
+//! Entries(vec![
+//! Field::Foo.into(),
+//! FieldAttrs::new(Field::Bar).attributes("Hello".to_string()).into(),
+//! ]);
+//! ```
+//!
+//! ## Call-site into
+//!
+//! With this syntax, the caller will be filled with lots of `.into()`.
+//!
+//! This can be circumvented with function argument types. Instead of taking `T`, functions should take `impl
+//! Into<T>`.
+//!
+//! <section class="warning">
+//!
+//! Although concise for user writing, this approach can be seen as a bad practice as monomorphising for each
+//! `T` duplicates the function's body. In practice, the methods are tiny and easily inlineable by the
+//! compiler.
+//!
+//! </section>
+//!
+//! Then, the previous example can be written using this syntax:
+//! ```
+//! # use from_variants::FromVariants;
+//! # struct Entries(Vec<Entry>);
+//! # #[derive(FromVariants)] enum Entry { FieldAttrs(FieldAttrs) };
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # impl FieldAttrs {
+//! # fn new(field: Field) -> Self { Self { field, attributes: None } }
+//! # }
+//! # enum Field { Foo, Bar };
+//! # impl From<Field> for Entry {
+//! # fn from(field: Field) -> Self { Self::FieldAttrs(FieldAttrs::new(field)) }
+//! # }
+//! impl Entries {
+//! pub fn push(mut self, entry: impl Into<Entry>) -> Self {
+//! self.0.push(entry.into());
+//! self
+//! }
+//! }
+//!
+//! impl FieldAttrs {
+//! fn attributes(self, attributes: impl Into<String>) -> Self {
+//! let attributes = Some(attributes.into());
+//! Self { attributes, ..self }
+//! }
+//! }
+//!
+//! Entries(vec![]).push(Field::Foo).push(FieldAttrs::new(Field::Bar).attributes("Hello"));
+//! ```
+//!
+//! <section class="warning">
+//!
+//! Heteregeneous does not exist in Rust, and coercion does not apply in the caller.
+//! Therefore, the example cannot merge `Field` and `FieldAttrs`, and must use `.push()` instead.
+//!
+//! However, if there is a homogeneous list, an `impl Into` argument can be used:
+//! ```
+//! # use from_variants::FromVariants;
+//! # struct Entries(Vec<Entry>);
+//! # #[derive(FromVariants)] enum Entry { FieldAttrs(FieldAttrs) };
+//! # struct FieldAttrs { field: Field, attributes: Option<String> };
+//! # enum Field { Foo, Bar };
+//! # impl FieldAttrs {
+//! # fn new(field: Field) -> Self { Self { field, attributes: None } }
+//! # }
+//! # impl From<Field> for Entry {
+//! # fn from(field: Field) -> Self { Self::FieldAttrs(FieldAttrs::new(field)) }
+//! # }
+//! impl Entries {
+//! fn new(entries: Vec<impl Into<Entry>>) -> Self {
+//! Self(entries.into_iter().map(Into::into).collect())
+//! }
+//! }
+//!
+//! Entries::new(vec![Field::Foo, Field::Bar]);
+//! ```
+//!
+//! In practice, this case is not expected to happen very often.
+//!
+//! </section>
+//!
+//! [RefinedRust project]: https://plv.mpi-sws.org/refinedrust/
+//! [Rocq]: https://coq.inria.fr
+//! [Rocq reference]: https://coq.inria.fr/doc/master/refman/index.html
+//! [sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
+
pub mod command;
pub mod module;
pub mod term;
+
+use std::fmt;
+
+use derive_more::{Deref, DerefMut, Display};
+use derive_new::new;
+use from_variants::FromVariants;
+use indoc::writedoc;
+
+use crate::write_list;
+
+/// A [document] is the entry-point to create a script, composed of [sentences].
+///
+/// [commands]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+/// [document]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-document
+/// [sentences]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-sentence
+#[derive(Eq, PartialEq, Debug, Default, Deref, DerefMut)]
+pub struct Document(pub Vec<Sentence>);
+
+impl Document {
+ #[must_use]
+ pub fn new(sentences: Vec<impl Into<Sentence>>) -> Self {
+ Self(sentences.into_iter().map(Into::into).collect())
+ }
+
+ pub fn push(&mut self, sentence: impl Into<Sentence>) {
+ self.0.push(sentence.into());
+ }
+}
+
+/// Beware, imports and exports [Command] are gathered on top of the list.
+#[derive(Eq, PartialEq, Debug, FromVariants)]
+pub enum Sentence {
+ CommandAttrs(CommandAttrs),
+}
+
+#[derive(Eq, PartialEq, Debug)]
+pub struct CommandAttrs {
+ pub command: Command,
+ pub attributes: Option<String>,
+}
+
+impl CommandAttrs {
+ #[must_use]
+ pub fn new(command: impl Into<Command>) -> Self {
+ Self {
+ attributes: None,
+ command: command.into(),
+ }
+ }
+
+ #[must_use]
+ pub fn attributes(self, attributes: impl Into<String>) -> Self {
+ let attributes = Some(attributes.into());
+
+ Self { attributes, ..self }
+ }
+}
+
+/// A [command], the entrypoint of everything that can be written.
+///
+/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+#[derive(Eq, PartialEq, Debug, FromVariants)]
+pub enum Command {
+ Require(Require),
+
+ Proof,
+ // TODO: Add section, ...
+}
+
+impl From<Command> for Sentence {
+ fn from(command: Command) -> Self {
+ Self::CommandAttrs(CommandAttrs::new(command))
+ }
+}
+
+#[derive(Eq, PartialEq, Debug)]
+pub struct Require {
+ pub from: Option<String>,
+ pub import: Vec<String>,
+}
+
+impl Require {
+ #[must_use]
+ pub fn new(import: Vec<impl Into<String>>) -> Self {
+ Self {
+ from: None,
+ import: import.into_iter().map(Into::into).collect(),
+ }
+ }
+
+ #[must_use]
+ pub fn from(self, from: impl Into<String>) -> Self {
+ let from = Some(from.into());
+
+ Self { from, ..self }
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ #[test]
+ fn test_document() {
+ let mut doc = Document::new(vec![
+ Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")),
+ Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")),
+ Command::Proof,
+ ]);
+
+ doc.push(Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")));
+ doc.push(Command::Proof);
+ doc.push(CommandAttrs::new(Command::Proof).attributes("Some"));
+ }
+}