From 6bd791d7df311c4e3187c270a2730f7e22400739 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Fri, 16 Aug 2024 15:13:08 +0200
Subject: [PATCH] feat: Add 'Hello world' example
---
rr_frontend/Cargo.lock | 12 -
rr_frontend/Cargo.toml | 3 +-
rr_frontend/radium/Cargo.toml | 1 -
.../src/coq/command_new/compiled_files.rs | 53 ----
rr_frontend/radium/src/coq/command_new/mod.rs | 58 ----
rr_frontend/radium/src/coq/eval_new.rs | 20 ++
rr_frontend/radium/src/coq/mod.rs | 249 +++++++++++++++---
rr_frontend/radium/src/coq/module_new.rs | 108 ++++++++
rr_frontend/radium/src/coq/settings.rs | 19 --
rr_frontend/radium/src/coq/syntax_new.rs | 25 ++
rr_frontend/radium/src/coq/term_new.rs | 21 ++
11 files changed, 387 insertions(+), 182 deletions(-)
delete mode 100644 rr_frontend/radium/src/coq/command_new/compiled_files.rs
delete mode 100644 rr_frontend/radium/src/coq/command_new/mod.rs
create mode 100644 rr_frontend/radium/src/coq/eval_new.rs
create mode 100644 rr_frontend/radium/src/coq/module_new.rs
delete mode 100644 rr_frontend/radium/src/coq/settings.rs
create mode 100644 rr_frontend/radium/src/coq/syntax_new.rs
create mode 100644 rr_frontend/radium/src/coq/term_new.rs
diff --git a/rr_frontend/Cargo.lock b/rr_frontend/Cargo.lock
index f9e207b..b7a033b 100644
--- a/rr_frontend/Cargo.lock
+++ b/rr_frontend/Cargo.lock
@@ -174,17 +174,6 @@ 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"
@@ -473,7 +462,6 @@ dependencies = [
name = "radium"
version = "0.1.0"
dependencies = [
- "derive-new",
"derive_more 1.0.0-beta.6",
"from_variants",
"indent_write",
diff --git a/rr_frontend/Cargo.toml b/rr_frontend/Cargo.toml
index f4de0a2..0053981 100644
--- a/rr_frontend/Cargo.toml
+++ b/rr_frontend/Cargo.toml
@@ -21,8 +21,7 @@ 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-new = "0.5"
-derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "deref_mut", "display", "from"] }
+derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "deref_mut", "display", "from", "into"] }
env_logger = { version = "0.11" }
from_variants = "1"
glob = "0.3"
diff --git a/rr_frontend/radium/Cargo.toml b/rr_frontend/radium/Cargo.toml
index 67a7cf8..9939171 100644
--- a/rr_frontend/radium/Cargo.toml
+++ b/rr_frontend/radium/Cargo.toml
@@ -8,7 +8,6 @@ repository.workspace = true
version.workspace = true
[dependencies]
-derive-new.workspace = true
derive_more.workspace = true
from_variants.workspace = true
indent_write.workspace = true
diff --git a/rr_frontend/radium/src/coq/command_new/compiled_files.rs b/rr_frontend/radium/src/coq/command_new/compiled_files.rs
deleted file mode 100644
index 34432f3..0000000
--- a/rr_frontend/radium/src/coq/command_new/compiled_files.rs
+++ /dev/null
@@ -1,53 +0,0 @@
-// © 2023, The RefinedRust Developers and Contributors
-//
-// This Source Code Form is subject to the terms of the BSD-3-clause License.
-// 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/.
-
-use std::fmt;
-
-/// A [dirpath].
-///
-/// [dirpath]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-dirpath
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct DirPath(Vec<String>);
-
-/// Either an Import or an Export flag.
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub enum Kind {
- Import,
- Export,
-}
-
-/// A [`From ... Require`] command.
-///
-/// [`From ... Require`]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct FromRequire {
- pub from: Option<String>,
- pub import: Vec<String>,
- pub kind: Kind,
-}
-
-impl FromRequire {
- #[must_use]
- pub fn new(import: Vec<impl Into<String>>, kind: Kind) -> Self {
- let from = None;
- let import = import.into_iter().map(Into::into).collect();
-
- Self { from, kind, import }
- }
-
- #[must_use]
- pub fn from(self, from: impl Into<String>) -> Self {
- let from = Some(from.into());
-
- Self { from, ..self }
- }
-}
-
-impl fmt::Display for FromRequire {
- fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
- write!(f, "")
- }
-}
diff --git a/rr_frontend/radium/src/coq/command_new/mod.rs b/rr_frontend/radium/src/coq/command_new/mod.rs
deleted file mode 100644
index c0d4006..0000000
--- a/rr_frontend/radium/src/coq/command_new/mod.rs
+++ /dev/null
@@ -1,58 +0,0 @@
-// © 2023, The RefinedRust Developers and Contributors
-//
-// This Source Code Form is subject to the terms of the BSD-3-clause License.
-// 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/.
-
-pub mod compiled_files;
-
-use derive_more::Display;
-use from_variants::FromVariants;
-
-use crate::coq;
-use crate::coq::settings;
-
-/// A [command], with optional attributes.
-///
-/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{} {}.", command, attributes.as_ref().map_or(String::new(), |a| a.to_string()))]
-pub struct CommandAttrs {
- pub command: Command,
- pub attributes: Option<settings::Attribute>,
-}
-
-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<settings::Attribute>) -> Self {
- let attributes = Some(attributes.into());
-
- Self { attributes, ..self }
- }
-}
-
-/// A [command].
-///
-/// [command]: https://coq.inria.fr/doc/master/refman/coq-cmdindex.html#command-index
-#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
-pub enum Command {
- #[display("{}", _0)]
- FromRequire(compiled_files::FromRequire),
-
- #[display("Proof")]
- Proof,
-}
-
-impl From<Command> for coq::Sentence {
- fn from(command: Command) -> Self {
- Self::CommandAttrs(CommandAttrs::new(command))
- }
-}
diff --git a/rr_frontend/radium/src/coq/eval_new.rs b/rr_frontend/radium/src/coq/eval_new.rs
new file mode 100644
index 0000000..7c7a3c6
--- /dev/null
+++ b/rr_frontend/radium/src/coq/eval_new.rs
@@ -0,0 +1,20 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+//! The [eval] section. This module will be renamed `eval`.
+//!
+//! [eval]: https://coq.inria.fr/doc/master/refman/proofs/writing-proofs/equality.html#computing-in-a-term-eval-and-eval
+
+use derive_more::{Deref, DerefMut, Display};
+
+use crate::coq::term_new;
+
+/// The [`Compute`] command.
+///
+/// [`Compute`]: https://coq.inria.fr/doc/master/refman/proofs/writing-proofs/equality.html#coq:cmd.Compute
+#[derive(Clone, Eq, PartialEq, Debug, Display, Deref, DerefMut)]
+#[display("Compute {}", _0)]
+pub struct Compute(pub term_new::Term);
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index d27f6fc..04e0f7f 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -11,14 +11,15 @@
//!
//! ---
//!
-//! 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`.
+//! This crate defines structures in a similar way to the grammar defined in the [Rocq reference]
+//! documentation, but unstructured sentences have been reunited under a single structure, such as
+//! `Section`/`End`.
//!
//! The syntax used to create structures is designed to write as little code as possible, with choices
//! explained in the Notes section.
//!
+//! Moreover, the crate is divided into several modules but does generally not follow the [Rocq reference].
+//!
//! ---
//!
//! Following the [Rocq reference], most of the types can be structured as nested enumerations.
@@ -45,18 +46,36 @@
//!
//! This code can be generated with the following Rust code:
//! ```
-//! # use radium::coq::*;
-//! // Document(vec![
-//! // TODO
-//! // ]);
+//! # use radium::coq::{*, eval_new::*, module_new::*, syntax_new::*, term_new::*};
+//! Document(vec![
+//! Sentence::CommandAttrs(CommandAttrs {
+//! attributes: None,
+//! command: Command::FromRequire(FromRequire {
+//! from: Some("Coq.Strings".to_owned()),
+//! import: vec![DirPath(vec!["String".to_owned()])],
+//! kind: Kind::Import,
+//! }),
+//! }),
+//! Sentence::CommandAttrs(CommandAttrs {
+//! attributes: None,
+//! command: Command::OpenScope(OpenScope("string_scope".to_owned())),
+//! }),
+//! Sentence::QueryCommandAttrs(QueryCommandAttrs {
+//! attributes: None,
+//! command: QueryCommand::Compute(Compute(Term::String("Hello World".to_owned()))),
+//! natural: None,
+//! }),
+//! ]);
//! ```
//!
//! This code can be reduced using coercions in the following Rust code:
//! ```
-//! # use radium::coq::*;
-//! // Document::new(vec![
-//! // TODO
-//! // ]);
+//! # use radium::coq::{*, eval_new::*, module_new::*, syntax_new::*, term_new::*};
+//! let mut doc = Document::default();
+//!
+//! doc.push(Command::FromRequire(Import::new(vec![vec!["String"]]).from("Coq.Strings").into()));
+//! doc.push(Command::OpenScope(OpenScope::new("string_scope")));
+//! doc.push(QueryCommand::Compute(Compute(Term::String("Hello World".to_owned()))));
//! ```
//!
//! # Notes
@@ -119,10 +138,11 @@
//! }
//! }
//!
-//! FieldAttrs::new(Field::Foo).attributes("Hello".to_string());
+//! FieldAttrs::new(Field::Foo).attributes("Hello".to_owned());
//! ```
//!
-//! There are several builder patterns available, but owned (_aka consuming_) builder pattern has been chosen:
+//! There are several builder patterns available, but the 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
@@ -150,7 +170,7 @@
//!
//! Entries(vec![
//! Entry::FieldAttrs(FieldAttrs::new(Field::Foo)),
-//! Entry::FieldAttrs(FieldAttrs::new(Field::Bar).attributes("Hello".to_string())),
+//! Entry::FieldAttrs(FieldAttrs::new(Field::Bar).attributes("Hello".to_owned())),
//! ]);
//! ```
//!
@@ -181,7 +201,7 @@
//!
//! Entries(vec![
//! Field::Foo.into(),
-//! Entry::FieldAttrs(FieldAttrs::new(Field::Bar).attributes("Hello".to_string())),
+//! Entry::FieldAttrs(FieldAttrs::new(Field::Bar).attributes("Hello".to_owned())),
//! ]);
//! ```
//!
@@ -209,7 +229,7 @@
//!
//! Entries(vec![
//! Field::Foo.into(),
-//! FieldAttrs::new(Field::Bar).attributes("Hello".to_string()).into(),
+//! FieldAttrs::new(Field::Bar).attributes("Hello".to_owned()).into(),
//! ]);
//! ```
//!
@@ -260,7 +280,7 @@
//!
//! <section class="warning">
//!
-//! Heteregeneous does not exist in Rust, and coercion does not apply in the caller.
+//! Heterogeneous datatypes do not exist in Rust, and coercions 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:
@@ -295,17 +315,17 @@
//! [sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
pub mod command;
-pub mod command_new;
+pub mod eval_new;
pub mod module;
-pub mod settings;
+pub mod module_new;
+pub mod syntax_new;
pub mod term;
+pub mod term_new;
use std::fmt;
use derive_more::{Deref, DerefMut, Display, From};
-use derive_new::new;
use from_variants::FromVariants;
-use indoc::writedoc;
use crate::display_list;
@@ -313,7 +333,7 @@ use crate::display_list;
///
/// [document]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-document
#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
-#[display("{}", display_list!(_0, "\n"))]
+#[display("{}\n", display_list!(_0, "\n"))]
pub struct Document(pub Vec<Sentence>);
impl Document {
@@ -333,29 +353,184 @@ impl Document {
#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
pub enum Sentence {
#[display("{}", _0)]
- CommandAttrs(command_new::CommandAttrs),
+ CommandAttrs(CommandAttrs),
+
+ #[display("{}", _0)]
+ QueryCommandAttrs(QueryCommandAttrs),
+}
+
+/// A [command], with optional attributes.
+///
+/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct CommandAttrs {
+ pub command: Command,
+ pub attributes: Option<Attribute>,
+}
+
+impl Display for CommandAttrs {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ if let Some(attributes) = &self.attributes {
+ write!(f, "{} ", attributes)?;
+ }
+
+ write!(f, "{}.", self.command)
+ }
+}
+
+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<Attribute>) -> Self {
+ let attributes = Some(attributes.into());
+
+ Self { attributes, ..self }
+ }
+}
+
+/// A [command].
+///
+/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
+pub enum Command {
+ #[display("{}", _0)]
+ FromRequire(module_new::FromRequire),
+
+ #[display("{}", _0)]
+ OpenScope(syntax_new::OpenScope),
+
+ #[display("Proof")]
+ Proof,
+}
+
+impl From<Command> for Sentence {
+ fn from(command: Command) -> Self {
+ Self::CommandAttrs(CommandAttrs::new(command))
+ }
+}
+
+/// A [query command], with optional attributes.
+///
+/// [query command]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-query_command
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct QueryCommandAttrs {
+ pub command: QueryCommand,
+ pub natural: Option<i32>,
+ pub attributes: Option<Attribute>,
+}
+
+impl Display for QueryCommandAttrs {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ if let Some(attributes) = &self.attributes {
+ write!(f, "{} ", attributes)?;
+ }
+
+ if let Some(natural) = &self.natural {
+ write!(f, "{}: ", natural)?;
+ }
+
+ write!(f, "{}.", self.command)
+ }
+}
+
+impl QueryCommandAttrs {
+ #[must_use]
+ pub fn new(command: impl Into<QueryCommand>) -> Self {
+ Self {
+ attributes: None,
+ natural: None,
+ command: command.into(),
+ }
+ }
+
+ #[must_use]
+ pub fn attributes(self, attributes: impl Into<Attribute>) -> Self {
+ let attributes = Some(attributes.into());
+
+ Self { attributes, ..self }
+ }
+}
+
+/// A [query command].
+///
+/// [query command]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-query_command
+#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
+pub enum QueryCommand {
+ #[display("{}", _0)]
+ Compute(eval_new::Compute),
+}
+
+impl From<QueryCommand> for Sentence {
+ fn from(command: QueryCommand) -> Self {
+ Self::QueryCommandAttrs(QueryCommandAttrs::new(command))
+ }
}
+/// An [attribute].
+///
+/// [attribute]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-attribute
+#[derive(Clone, Eq, PartialEq, Debug, Display, From)]
+#[from(forward)]
+#[display("{}", _0)]
+pub struct Attribute(String);
+
#[cfg(test)]
mod tests {
- use command_new::compiled_files::*;
- use command_new::*;
+ use eval_new::Compute;
+ use module_new::{DirPath, FromRequire, Import, Kind};
+ use syntax_new::OpenScope;
+ use term_new::Term;
use super::*;
#[test]
- fn test_document() {
- let mut doc = Document::new(vec![
- Command::FromRequire(
- FromRequire::new(vec!["nat", "bool"], Kind::Import).from("Coq.Init.Datatypes"),
- ),
- Command::Proof,
+ fn hello_world_compact() {
+ let mut doc = Document::default();
+
+ doc.push(Command::FromRequire(Import::new(vec![vec!["String"]]).from("Coq.Strings").into()));
+ doc.push(Command::OpenScope(OpenScope::new("string_scope")));
+ doc.push(QueryCommand::Compute(Compute(Term::String("Hello World".to_owned()))));
+
+ assert_eq!(doc.to_string(), indoc::indoc! {r#"
+ From Coq.Strings Require Import String.
+ Open Scope string_scope.
+ Compute "Hello World".
+ "#});
+ }
+
+ #[test]
+ fn hello_world_extended() {
+ let doc = Document(vec![
+ Sentence::CommandAttrs(CommandAttrs {
+ attributes: None,
+ command: Command::FromRequire(FromRequire {
+ from: Some("Coq.Strings".to_owned()),
+ import: vec![DirPath(vec!["String".to_owned()])],
+ kind: Kind::Import,
+ }),
+ }),
+ Sentence::CommandAttrs(CommandAttrs {
+ attributes: None,
+ command: Command::OpenScope(OpenScope("string_scope".to_owned())),
+ }),
+ Sentence::QueryCommandAttrs(QueryCommandAttrs {
+ attributes: None,
+ command: QueryCommand::Compute(Compute(Term::String("Hello World".to_owned()))),
+ natural: None,
+ }),
]);
- doc.push(Command::FromRequire(
- FromRequire::new(vec!["nat", "bool"], Kind::Import).from("Coq.Init.Datatypes"),
- ));
- doc.push(Command::Proof);
- doc.push(CommandAttrs::new(Command::Proof).attributes("Some"));
+ assert_eq!(doc.to_string(), indoc::indoc! {r#"
+ From Coq.Strings Require Import String.
+ Open Scope string_scope.
+ Compute "Hello World".
+ "#});
}
}
diff --git a/rr_frontend/radium/src/coq/module_new.rs b/rr_frontend/radium/src/coq/module_new.rs
new file mode 100644
index 0000000..9794979
--- /dev/null
+++ b/rr_frontend/radium/src/coq/module_new.rs
@@ -0,0 +1,108 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+//! The [module] section. This module will be renamed `module`.
+//!
+//! [module]: https://coq.inria.fr/doc/master/refman/language/core/modules.html
+
+use std::fmt;
+
+use derive_more::{Deref, DerefMut, Display, From, Into};
+
+use crate::{display_list, write_list};
+
+/// A [dirpath].
+///
+/// [dirpath]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-dirpath
+#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
+#[display("{}", display_list!(_0, "."))]
+pub struct DirPath(pub Vec<String>);
+
+impl From<Vec<&str>> for DirPath {
+ fn from(v: Vec<&str>) -> Self {
+ Self(v.into_iter().map(ToString::to_string).collect())
+ }
+}
+
+/// Either an Import or an Export flag.
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub enum Kind {
+ Import,
+ Export,
+}
+
+/// The [`From ... Require`] command.
+///
+/// [`From ... Require`]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct FromRequire {
+ pub from: Option<String>,
+ pub import: Vec<DirPath>,
+ pub kind: Kind,
+}
+
+impl FromRequire {
+ #[must_use]
+ pub fn new(import: Vec<impl Into<DirPath>>, kind: Kind) -> Self {
+ let from = None;
+ let import = import.into_iter().map(Into::into).collect();
+
+ Self { from, import, kind }
+ }
+
+ #[allow(clippy::same_name_method)]
+ #[must_use]
+ pub fn from(self, from: impl Into<String>) -> Self {
+ let from = Some(from.into());
+
+ Self { from, ..self }
+ }
+}
+
+impl Display for FromRequire {
+ fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+ if let Some(from) = &self.from {
+ write!(f, "From {} ", from)?;
+ }
+
+ match self.kind {
+ Kind::Import => write!(f, "Require Import ")?,
+ Kind::Export => write!(f, "Require Export ")?,
+ };
+
+ write_list!(f, &self.import, " ")
+ }
+}
+
+/// A wrapper over [`FromRequire`] to represent an import list.
+#[derive(Clone, Eq, PartialEq, Debug, Deref, DerefMut, Into)]
+pub struct Import(pub FromRequire);
+
+impl Import {
+ pub fn new(import: Vec<impl Into<DirPath>>) -> Self {
+ Self(FromRequire::new(import, Kind::Import))
+ }
+
+ #[must_use]
+ pub fn from(self, from: impl Into<String>) -> Self {
+ Self(self.0.from(from))
+ }
+}
+
+/// A wrapper over [`FromRequire`] to represent an export list.
+#[derive(Clone, Eq, PartialEq, Debug, Deref, DerefMut, Into)]
+pub struct Export(pub FromRequire);
+
+impl Export {
+ pub fn new(import: Vec<impl Into<DirPath>>) -> Self {
+ Self(FromRequire::new(import, Kind::Export))
+ }
+
+ #[must_use]
+ pub fn from(self, from: impl Into<String>) -> Self {
+ Self(self.0.from(from))
+ }
+}
diff --git a/rr_frontend/radium/src/coq/settings.rs b/rr_frontend/radium/src/coq/settings.rs
deleted file mode 100644
index 4418527..0000000
--- a/rr_frontend/radium/src/coq/settings.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-// © 2023, The RefinedRust Developers and Contributors
-//
-// This Source Code Form is subject to the terms of the BSD-3-clause License.
-// 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/.
-
-//! Mechanisms, called [settings], for changing the behaviour of Rocq.
-//!
-//! [settings]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#settings
-
-use derive_more::{Display, From};
-
-/// An [attribute].
-///
-/// [attribute]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-attribute
-#[derive(Clone, Eq, PartialEq, Debug, Display, From)]
-#[from(forward)]
-#[display("{}", _0)]
-pub struct Attribute(String);
diff --git a/rr_frontend/radium/src/coq/syntax_new.rs b/rr_frontend/radium/src/coq/syntax_new.rs
new file mode 100644
index 0000000..008fff6
--- /dev/null
+++ b/rr_frontend/radium/src/coq/syntax_new.rs
@@ -0,0 +1,25 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+//! The [syntax and notations] section. This module will be renamed `syntax`.
+//!
+//! [syntax and notations]: https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html
+
+use derive_more::{Deref, DerefMut, Display, From};
+
+/// The [`Open Scope`] command.
+///
+/// [`Open Scope`]: https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Open-Scope
+#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut, From)]
+#[from(forward)]
+#[display("Open Scope {}", _0)]
+pub struct OpenScope(pub String);
+
+impl OpenScope {
+ pub fn new(scope: impl Into<String>) -> Self {
+ Self(scope.into())
+ }
+}
diff --git a/rr_frontend/radium/src/coq/term_new.rs b/rr_frontend/radium/src/coq/term_new.rs
new file mode 100644
index 0000000..1d05534
--- /dev/null
+++ b/rr_frontend/radium/src/coq/term_new.rs
@@ -0,0 +1,21 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+//! The [terms] section. This module will be renamed `term`.
+//!
+//! [terms]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#term-term
+
+use derive_more::Display;
+use from_variants::FromVariants;
+
+/// A [term].
+///
+/// [term]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-term
+#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
+pub enum Term {
+ #[display("\"{}\"", _0)]
+ String(String),
+}
--
GitLab