From 220f80dde287663375c81148b2129260cc36ee15 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Wed, 14 Aug 2024 10:57:11 +0200
Subject: [PATCH] feat(coq): Split attempt into submodules
---
rr_frontend/Cargo.toml | 2 +-
.../src/coq/command_new/compiled_files.rs | 53 ++++++++++
rr_frontend/radium/src/coq/command_new/mod.rs | 58 +++++++++++
rr_frontend/radium/src/coq/mod.rs | 97 +++++--------------
rr_frontend/radium/src/coq/module.rs | 4 +-
rr_frontend/radium/src/coq/section.rs | 26 +++++
rr_frontend/radium/src/coq/settings.rs | 19 ++++
7 files changed, 181 insertions(+), 78 deletions(-)
create mode 100644 rr_frontend/radium/src/coq/command_new/compiled_files.rs
create mode 100644 rr_frontend/radium/src/coq/command_new/mod.rs
create mode 100644 rr_frontend/radium/src/coq/section.rs
create mode 100644 rr_frontend/radium/src/coq/settings.rs
diff --git a/rr_frontend/Cargo.toml b/rr_frontend/Cargo.toml
index fe19035..f4de0a2 100644
--- a/rr_frontend/Cargo.toml
+++ b/rr_frontend/Cargo.toml
@@ -22,7 +22,7 @@ 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"] }
+derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "deref_mut", "display", "from"] }
env_logger = { version = "0.11" }
from_variants = "1"
glob = "0.3"
diff --git a/rr_frontend/radium/src/coq/command_new/compiled_files.rs b/rr_frontend/radium/src/coq/command_new/compiled_files.rs
new file mode 100644
index 0000000..34432f3
--- /dev/null
+++ b/rr_frontend/radium/src/coq/command_new/compiled_files.rs
@@ -0,0 +1,53 @@
+// © 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
new file mode 100644
index 0000000..c0d4006
--- /dev/null
+++ b/rr_frontend/radium/src/coq/command_new/mod.rs
@@ -0,0 +1,58 @@
+// © 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/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index 6bc9590..d27f6fc 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -295,24 +295,25 @@
//! [sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
pub mod command;
+pub mod command_new;
pub mod module;
+pub mod settings;
pub mod term;
use std::fmt;
-use derive_more::{Deref, DerefMut, Display};
+use derive_more::{Deref, DerefMut, Display, From};
use derive_new::new;
use from_variants::FromVariants;
use indoc::writedoc;
-use crate::write_list;
+use crate::display_list;
-/// A [document] is the entry-point to create a script, composed of [sentences].
+/// A [document].
///
-/// [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)]
+#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
+#[display("{}", display_list!(_0, "\n"))]
pub struct Document(pub Vec<Sentence>);
impl Document {
@@ -326,88 +327,34 @@ impl Document {
}
}
-/// 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.
+/// A [sentence].
///
-/// [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 }
- }
+/// [sentence]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-sentence
+#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
+pub enum Sentence {
+ #[display("{}", _0)]
+ CommandAttrs(command_new::CommandAttrs),
}
#[cfg(test)]
mod tests {
+ use command_new::compiled_files::*;
+ use command_new::*;
+
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::FromRequire(
+ FromRequire::new(vec!["nat", "bool"], Kind::Import).from("Coq.Init.Datatypes"),
+ ),
Command::Proof,
]);
- doc.push(Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")));
+ 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"));
}
diff --git a/rr_frontend/radium/src/coq/module.rs b/rr_frontend/radium/src/coq/module.rs
index d448321..ed9cc5a 100644
--- a/rr_frontend/radium/src/coq/module.rs
+++ b/rr_frontend/radium/src/coq/module.rs
@@ -18,8 +18,8 @@ pub struct Path(String);
impl Path {
#[must_use]
- pub fn new(path: &str) -> Self {
- Self(path.to_owned())
+ pub fn new(path: impl Into<String>) -> Self {
+ Self(path.into())
}
#[must_use]
diff --git a/rr_frontend/radium/src/coq/section.rs b/rr_frontend/radium/src/coq/section.rs
new file mode 100644
index 0000000..e2d76bf
--- /dev/null
+++ b/rr_frontend/radium/src/coq/section.rs
@@ -0,0 +1,26 @@
+// © 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/.
+
+/// [Sections].
+///
+/// [Sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
+use derive_more::Display;
+
+#[derive(Clone, Eq, PartialEq, Hash, Debug, Display)]
+#[display("Section {}", name)]
+pub struct Section {
+ name: String,
+}
+
+impl Section {
+ pub fn new(name: String) -> Self {
+ Self { name }
+ }
+
+ pub fn name(&self) -> &str {
+ &self.name
+ }
+}
diff --git a/rr_frontend/radium/src/coq/settings.rs b/rr_frontend/radium/src/coq/settings.rs
new file mode 100644
index 0000000..4418527
--- /dev/null
+++ b/rr_frontend/radium/src/coq/settings.rs
@@ -0,0 +1,19 @@
+// © 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);
--
GitLab