Skip to content
Snippets Groups Projects
Verified Commit 6a83e504 authored by Vincent Lafeychine's avatar Vincent Lafeychine
Browse files

feat(coq): Define a permissive syntax with explanations

parent 3022365b
No related branches found
No related tags found
1 merge request!55Refactor `coq` crate
Hide whitespace changes
Inline Side-by-side
rr_frontend/Cargo.lock
+ 87
− 0
View file @ 6a83e504
......@@ -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"
......
rr_frontend/Cargo.toml
+ 3
− 1
View file @ 6a83e504
......@@ -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"
......
rr_frontend/radium/Cargo.toml
+ 3
− 1
View file @ 6a83e504
......@@ -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
rr_frontend/radium/src/coq/mod.rs
+ 405
− 10
View file @ 6a83e504
......@@ -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"));
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment