From dee62ee036c2ff13e921186e5ab5e6556c049403 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Mon, 17 Jun 2024 10:25:50 +0200
Subject: [PATCH] chore(radium): Split coq crate (command, term)
---
rr_frontend/radium/src/code.rs | 38 +-
rr_frontend/radium/src/coq/command.rs | 277 ++++++++
rr_frontend/radium/src/coq/mod.rs | 646 +-----------------
rr_frontend/radium/src/coq/module.rs | 2 +-
rr_frontend/radium/src/coq/term.rs | 414 +++++++++++
rr_frontend/radium/src/specs.rs | 482 +++++++------
rr_frontend/translation/src/function_body.rs | 28 +-
rr_frontend/translation/src/lib.rs | 2 +-
.../src/spec_parsers/crate_attr_parser.rs | 10 +-
.../src/spec_parsers/enum_spec_parser.rs | 4 +-
.../src/spec_parsers/module_attr_parser.rs | 10 +-
.../src/spec_parsers/parse_utils.rs | 14 +-
.../src/spec_parsers/struct_spec_parser.rs | 20 +-
.../src/spec_parsers/trait_attr_parser.rs | 9 +-
.../spec_parsers/trait_impl_attr_parser.rs | 2 +-
.../verbose_function_spec_parser.rs | 22 +-
rr_frontend/translation/src/trait_registry.rs | 5 +-
.../translation/src/type_translator.rs | 21 +-
18 files changed, 1052 insertions(+), 954 deletions(-)
create mode 100644 rr_frontend/radium/src/coq/command.rs
create mode 100644 rr_frontend/radium/src/coq/term.rs
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index ff115ea..1ab1b7f 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -277,13 +277,13 @@ pub enum Expr {
#[display("StructInit {} [{}]", sls, display_list!(components, "; ", |(name, e)| format!("(\"{name}\", {e} : expr)")))]
StructInitE {
- sls: coq::AppTerm<String, String>,
+ sls: coq::term::App<String, String>,
components: Vec<(String, Expr)>,
},
#[display("EnumInit {} \"{}\" ({}) ({})", els, variant, ty, &initializer)]
EnumInitE {
- els: coq::AppTerm<String, String>,
+ els: coq::term::App<String, String>,
variant: String,
ty: RustType,
initializer: Box<Expr>,
@@ -651,7 +651,7 @@ pub struct FunctionCode {
basic_blocks: BTreeMap<usize, Stmt>,
/// Coq parameters that the function is parameterized over
- required_parameters: Vec<(coq::Name, coq::Type)>,
+ required_parameters: Vec<(coq::term::Name, coq::term::Type)>,
}
fn make_map_string(sep0: &str, sep: &str, els: &Vec<(String, String)>) -> String {
@@ -677,7 +677,7 @@ fn make_lft_map_string(els: &Vec<(String, String)>) -> String {
impl Display for FunctionCode {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- fn fmt_params((name, ty): &(coq::Name, coq::Type)) -> String {
+ fn fmt_params((name, ty): &(coq::term::Name, coq::term::Type)) -> String {
format!("({} : {})", name, ty)
}
@@ -1294,12 +1294,12 @@ impl<'def> FunctionBuilder<'def> {
}
/// Add a Coq-level param that comes before the type parameters.
- pub fn add_early_coq_param(&mut self, param: coq::Param) {
+ pub fn add_early_coq_param(&mut self, param: coq::term::Param) {
self.spec.early_coq_params.0.push(param);
}
/// Add a Coq-level param that comes after the type parameters.
- pub fn add_late_coq_param(&mut self, param: coq::Param) {
+ pub fn add_late_coq_param(&mut self, param: coq::term::Param) {
self.spec.late_coq_params.0.push(param);
}
@@ -1333,9 +1333,9 @@ impl<'def> FunctionBuilder<'def> {
let spec_type = format!("{} {spec_params_param_name}", trait_use.trait_ref.spec_record);
// add the spec params
- self.spec.late_coq_params.0.push(coq::Param::new(
- coq::Name::Named(spec_params_param_name),
- coq::Type::Literal(spec_params_type_name),
+ self.spec.late_coq_params.0.push(coq::term::Param::new(
+ coq::term::Name::Named(spec_params_param_name),
+ coq::term::Type::Literal(spec_params_type_name),
true,
));
@@ -1348,16 +1348,16 @@ impl<'def> FunctionBuilder<'def> {
.collect();
let mut attr_param = format!("{} ", trait_use.trait_ref.spec_attrs_record);
push_str_list!(attr_param, &all_args, " ");
- self.spec.late_coq_params.0.push(coq::Param::new(
- coq::Name::Named(spec_attrs_param_name),
- coq::Type::Literal(attr_param),
+ self.spec.late_coq_params.0.push(coq::term::Param::new(
+ coq::term::Name::Named(spec_attrs_param_name),
+ coq::term::Type::Literal(attr_param),
false,
));
// add the spec itself
- self.spec.late_coq_params.0.push(coq::Param::new(
- coq::Name::Named(spec_param_name),
- coq::Type::Literal(spec_type),
+ self.spec.late_coq_params.0.push(coq::term::Param::new(
+ coq::term::Name::Named(spec_param_name),
+ coq::term::Type::Literal(spec_type),
false,
));
@@ -1383,17 +1383,17 @@ impl<'def> FunctionBuilder<'def> {
// generate location parameters for other functions used by this one, as well as syntypes
// These are parameters that the code gets
- let mut parameters: Vec<(coq::Name, coq::Type)> = self
+ let mut parameters: Vec<(coq::term::Name, coq::term::Type)> = self
.other_functions
.iter()
- .map(|f_inst| (coq::Name::Named(f_inst.loc_name.clone()), coq::Type::Loc))
+ .map(|f_inst| (coq::term::Name::Named(f_inst.loc_name.clone()), coq::term::Type::Loc))
.collect();
// generate location parameters for statics used by this function
let mut statics_parameters = self
.used_statics
.iter()
- .map(|s| (coq::Name::Named(s.loc_name.clone()), coq::Type::Loc))
+ .map(|s| (coq::term::Name::Named(s.loc_name.clone()), coq::term::Type::Loc))
.collect();
parameters.append(&mut statics_parameters);
@@ -1403,7 +1403,7 @@ impl<'def> FunctionBuilder<'def> {
.generics
.get_ty_params()
.iter()
- .map(|names| (coq::Name::Named(names.syn_type.clone()), coq::Type::SynType))
+ .map(|names| (coq::term::Name::Named(names.syn_type.clone()), coq::term::Type::SynType))
.collect();
parameters.append(&mut gen_st_parameters);
diff --git a/rr_frontend/radium/src/coq/command.rs b/rr_frontend/radium/src/coq/command.rs
new file mode 100644
index 0000000..7e159ea
--- /dev/null
+++ b/rr_frontend/radium/src/coq/command.rs
@@ -0,0 +1,277 @@
+// © 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/.
+
+/// Rocq commands.
+use std::fmt;
+use std::fmt::Write as fmtWrite;
+
+use derive_more::Display;
+use indent_write::fmt::IndentWriter;
+
+use crate::coq::term;
+use crate::{display_list, BASE_INDENT};
+
+/// A single tactic call.
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum ProofItem {
+ #[display("{}.", _0)]
+ Literal(String),
+}
+
+/// A Coq proof script.
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}\n", display_list!(_0, "\n"))]
+pub struct ProofScript(pub Vec<ProofItem>);
+
+/// A terminator for a proof script
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum ProofScriptTerminator {
+ #[display("Qed")]
+ Qed,
+
+ #[display("Defined")]
+ Defined,
+
+ #[display("Admitted")]
+ Admitted,
+}
+
+/// A body of a Coq definition
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub enum DefBody {
+ /// a proof script invoking Ltac tactics
+ Script(ProofScript, ProofScriptTerminator),
+
+ /// a proof term
+ Term(term::Gallina),
+}
+
+impl Display for DefBody {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ match self {
+ Self::Script(script, terminator) => {
+ write!(f, ".\n")?;
+ write!(f, "Proof.\n")?;
+ let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
+ write!(f2, "{}", script)?;
+ write!(f, "{}.", terminator)?;
+ },
+ Self::Term(term) => {
+ write!(f, " := {}.", term)?;
+ },
+ }
+ Ok(())
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum Attribute {
+ #[display("global")]
+ Global,
+
+ #[display("local")]
+ Local,
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}",
+ if attrs.is_empty() { String::new() } else {
+ format!("#[ {} ]", display_list!(attrs, ", "))
+ }
+)]
+pub struct Attributes {
+ attrs: Vec<Attribute>,
+}
+
+impl Attributes {
+ #[must_use]
+ pub const fn empty() -> Self {
+ Self { attrs: vec![] }
+ }
+
+ #[must_use]
+ pub fn new(attrs: Vec<Attribute>) -> Self {
+ Self { attrs }
+ }
+
+ #[must_use]
+ pub fn singleton(attr: Attribute) -> Self {
+ Self { attrs: vec![attr] }
+ }
+}
+
+/// A Coq typeclass instance declaration
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("#[global] Instance : {}{}", ty, body)]
+pub struct InstanceDecl {
+ ty: term::Type,
+ body: DefBody,
+}
+
+impl InstanceDecl {
+ #[must_use]
+ pub const fn new(ty: term::Type, body: DefBody) -> Self {
+ Self { ty, body }
+ }
+}
+
+#[derive(Clone, Debug, Display, Eq, PartialEq)]
+#[display("{} {} : {}", name, params, ty)]
+pub struct RecordDeclItem {
+ pub name: String,
+ pub params: term::ParamList,
+ pub ty: term::Type,
+}
+
+/// A record declaration.
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Record {
+ pub name: String,
+ pub params: term::ParamList,
+ pub ty: term::Type,
+ pub constructor: Option<String>,
+ pub body: Vec<RecordDeclItem>,
+}
+
+impl Display for Record {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let constructor = self.constructor.clone().unwrap_or_default();
+ write!(f, "Record {} {} : {} := {constructor} {{\n", self.name, self.params, self.ty)?;
+ let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
+ for it in &self.body {
+ write!(f2, "{it};\n")?;
+ }
+ write!(f, "}}.")
+ }
+}
+
+/// A Context declaration.
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct ContextDecl {
+ pub items: term::ParamList,
+}
+
+impl ContextDecl {
+ #[must_use]
+ pub const fn new(items: term::ParamList) -> Self {
+ Self { items }
+ }
+
+ #[must_use]
+ pub fn refinedrust() -> Self {
+ Self {
+ items: term::ParamList::new(vec![term::Param::new(
+ term::Name::Named("RRGS".to_owned()),
+ term::Type::Literal("refinedrustGS Σ".to_owned()),
+ true,
+ )]),
+ }
+ }
+}
+
+impl Display for ContextDecl {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ if self.items.0.is_empty() { Ok(()) } else { write!(f, "Context {}.", self.items) }
+ }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Display)]
+pub enum DefinitionKind {
+ #[display("Definition")]
+ Definition,
+ #[display("Lemma")]
+ Lemma,
+}
+
+/// A Coq definition
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Definition {
+ pub name: String,
+ pub params: term::ParamList,
+ pub ty: Option<term::Type>,
+ pub body: DefBody,
+ pub kind: DefinitionKind,
+}
+
+impl Display for Definition {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ if let Some(ty) = &self.ty {
+ write!(f, "{} {} {} : {ty}{}", self.kind, self.name, self.params, self.body)
+ } else {
+ write!(f, "{} {} {}{}", self.kind, self.name, self.params, self.body)
+ }
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum TopLevelAssertion<'a> {
+ /// A declaration of a Coq Inductive
+ #[display("{}", _0)]
+ InductiveDecl(&'a term::Inductive),
+
+ /// A declaration of a Coq instance
+ #[display("{}", _0)]
+ InstanceDecl(&'a InstanceDecl),
+
+ /// A declaration of a Coq record
+ #[display("{}", _0)]
+ RecordDecl(Record),
+
+ /// A declaration of Coq context items
+ #[display("{}", _0)]
+ ContextDecl(ContextDecl),
+
+ /// A Coq Definition
+ #[display("{}", _0)]
+ Definition(Definition),
+
+ /// A Coq comment
+ #[display("(* {} *)", _0)]
+ Comment(&'a str),
+
+ /// A Coq section
+ #[display("Section {}.\n{}End{}.", _0, Indented::new(_1), _0)]
+ Section(String, TopLevelAssertions<'a>),
+
+ /// A Coq section start
+ #[display("Section {}.", _0)]
+ SectionStart(String),
+
+ /// A Coq section end
+ #[display("End {}.", _0)]
+ SectionEnd(String),
+}
+
+/// Type for writing contents indented via Display.
+struct Indented<T> {
+ x: T,
+}
+impl<T> Indented<T> {
+ pub const fn new(x: T) -> Self {
+ Self { x }
+ }
+}
+impl<T: Display> Display for Indented<T> {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut indent_writer = IndentWriter::new(BASE_INDENT, f);
+ write!(indent_writer, "{}", self.x)
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}", display_list!(_0, "\n"))]
+pub struct TopLevelAssertions<'a>(pub Vec<TopLevelAssertion<'a>>);
+
+impl<'a> TopLevelAssertions<'a> {
+ #[must_use]
+ pub(crate) const fn empty() -> Self {
+ Self(vec![])
+ }
+
+ pub(crate) fn push(&mut self, a: TopLevelAssertion<'a>) {
+ self.0.push(a);
+ }
+}
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index 5f69817..f24104c 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -4,648 +4,10 @@
// 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 module;
-
/// A collection of types to represent and generate Rocq code.
///
/// These types are intended to be used for the purposes of this project.
-use std::fmt;
-use std::fmt::Write as fmtWrite;
-
-use derive_more::Display;
-use indent_write::fmt::IndentWriter;
-use indent_write::indentable::Indentable;
-use itertools::Itertools;
-
-use crate::{display_list, make_indent, write_list, BASE_INDENT};
-
-/// Represents an application of a term to an rhs.
-/// (commonly used for layouts and instantiating them with generics).
-#[derive(Clone, Eq, PartialEq, Hash, Debug)]
-pub struct AppTerm<T, U> {
- pub(crate) lhs: T,
- pub(crate) rhs: Vec<U>,
-}
-
-impl<T: Display, U: Display> Display for AppTerm<T, U> {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- if self.rhs.is_empty() {
- return write!(f, "{}", self.lhs);
- }
-
- write_list!(f, &self.rhs, " ", "({})")
- }
-}
-
-impl<T, U> AppTerm<T, U> {
- pub fn new(lhs: T, rhs: Vec<U>) -> Self {
- Self { lhs, rhs }
- }
-
- pub fn new_lhs(lhs: T) -> Self {
- Self {
- lhs,
- rhs: Vec::new(),
- }
- }
-
- pub(crate) const fn get_lhs(&self) -> &T {
- &self.lhs
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Ord, PartialOrd, Debug, Display)]
-pub enum Name {
- #[display("{}", _0)]
- Named(String),
-
- #[display("_")]
- Unnamed,
-}
-
-/// A Coq pattern, e.g., "x" or "'(x, y)".
-pub type Pattern = String;
-
-fn fmt_prod(v: &Vec<Type>) -> String {
- match v.as_slice() {
- [] => "unit".to_owned(),
- [t] => t.to_string(),
- _ => format!("({})%type", display_list!(v, " * ")),
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-pub enum Type {
- /// literal types that are not contained in the grammar
- #[display("{}", _0)]
- Literal(String),
-
- /// function types; the argument vector should be non-empty
- #[display("{} → {}", display_list!(_0, " → ", "({})"), *_1)]
- Function(Vec<Type>, Box<Type>),
-
- /// Placeholder that should be inferred by Coq if possible
- #[display("_")]
- Infer,
-
- /// Coq type `lft`
- #[display("lft")]
- Lft,
-
- /// Coq type `loc`
- #[display("loc")]
- Loc,
-
- /// Coq type `layout`
- #[display("layout")]
- Layout,
-
- /// Coq type `syn_type`
- #[display("syn_type")]
- SynType,
-
- /// Coq type `struct_layout`
- #[display("struct_layout")]
- StructLayout,
-
- /// Coq type `Type`
- #[display("Type")]
- Type,
-
- /// Coq type `type rt`
- #[display("(type {})", &_0)]
- Ttype(Box<Type>),
-
- /// Coq type `rtype`
- #[display("rtype")]
- Rtype,
-
- /// the unit type
- #[display("unit")]
- Unit,
-
- /// the type of integers
- #[display("Z")]
- Z,
-
- /// the type of booleans
- #[display("bool")]
- Bool,
-
- /// product types
- #[display("{}", fmt_prod(_0))]
- Prod(Vec<Type>),
-
- /// place_rfn
- #[display("(place_rfn {})", &_0)]
- PlaceRfn(Box<Type>),
-
- /// gname
- #[display("gname")]
- Gname,
-
- /// a plist with a given type constructor over a list of types
- #[display("plist {} [{}]", _0, display_list!(_1, "; ", "{} : Type"))]
- PList(String, Vec<Type>),
-
- /// the semantic type of a function
- #[display("function_ty")]
- FunctionTy,
-
- /// the Coq type Prop of propositions
- #[display("Prop")]
- Prop,
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}", self.format(true))]
-pub struct Param {
- /// the name
- name: Name,
-
- /// the type
- ty: Type,
-
- /// implicit or not?
- implicit: bool,
-
- /// does this depend on Σ?
- depends_on_sigma: bool,
-}
-
-impl Param {
- #[must_use]
- pub fn new(name: Name, ty: Type, implicit: bool) -> Self {
- let depends_on_sigma = if let Type::Literal(lit) = &ty { lit.contains('Σ') } else { false };
-
- Self {
- name,
- ty,
- implicit,
- depends_on_sigma,
- }
- }
-
- #[must_use]
- pub fn with_name(&self, name: String) -> Self {
- Self::new(Name::Named(name), self.ty.clone(), self.implicit)
- }
-
- #[must_use]
- pub fn get_name_ref(&self) -> Option<&str> {
- match &self.name {
- Name::Named(s) => Some(s),
- Name::Unnamed => None,
- }
- }
-
- #[allow(clippy::collapsible_else_if)]
- #[must_use]
- fn format(&self, make_implicits: bool) -> String {
- if !self.implicit {
- return format!("({} : {})", self.name, self.ty);
- }
-
- if make_implicits {
- if let Name::Named(name) = &self.name {
- format!("`{{{} : !{}}}", name, self.ty)
- } else {
- format!("`{{!{}}}", self.ty)
- }
- } else {
- if let Name::Named(name) = &self.name {
- format!("`({} : !{})", name, self.ty)
- } else {
- format!("`(!{})", self.ty)
- }
- }
- }
-
- pub(crate) const fn get_name(&self) -> &Name {
- &self.name
- }
-
- pub(crate) const fn is_implicit(&self) -> bool {
- self.implicit
- }
-
- pub(crate) const fn is_dependent_on_sigma(&self) -> bool {
- self.depends_on_sigma
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}", display_list!(_0, " "))]
-pub struct ParamList(pub Vec<Param>);
-
-impl ParamList {
- #[must_use]
- pub const fn new(params: Vec<Param>) -> Self {
- Self(params)
- }
-
- #[must_use]
- pub const fn empty() -> Self {
- Self(vec![])
- }
-
- pub fn append(&mut self, params: Vec<Param>) {
- self.0.extend(params);
- }
-
- /// Make using terms for this list of binders
- #[must_use]
- pub fn make_using_terms(&self) -> Vec<GallinaTerm> {
- self.0.iter().map(|x| GallinaTerm::Literal(format!("{}", x.name))).collect()
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{} {}", name, params)]
-pub struct Variant {
- name: String,
- params: ParamList,
-}
-
-impl Variant {
- #[must_use]
- pub fn new(name: &str, params: Vec<Param>) -> Self {
- Self {
- name: name.to_owned(),
- params: ParamList::new(params),
- }
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("Inductive {} {} :=\n{}\n.", name, parameters,
- display_list!(variants, "\n| ").indented(&make_indent(1))
-)]
-pub struct Inductive {
- name: String,
- parameters: ParamList,
- variants: Vec<Variant>,
-}
-
-impl Inductive {
- #[must_use]
- pub fn new(name: &str, parameters: Vec<Param>, variants: Vec<Variant>) -> Self {
- Self {
- name: name.to_owned(),
- parameters: ParamList::new(parameters),
- variants,
- }
- }
-
- pub(crate) const fn get_name(&self) -> &String {
- &self.name
- }
-}
-
-/// A single tactic call.
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-pub enum ProofItem {
- #[display("{}.", _0)]
- Literal(String),
-}
-
-/// A Coq proof script.
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}\n", display_list!(_0, "\n"))]
-pub struct ProofScript(pub Vec<ProofItem>);
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct RecordBodyItem {
- pub name: String,
- pub params: ParamList,
- pub term: GallinaTerm,
-}
-
-impl Display for RecordBodyItem {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- let mut writer = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
- write!(writer, "{} {} :=\n{};", self.name, self.params, self.term)
- }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct RecordBodyTerm {
- pub items: Vec<RecordBodyItem>,
-}
-
-impl Display for RecordBodyTerm {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- write!(f, "{{|\n")?;
- let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
- for it in &self.items {
- write!(f2, "{}\n", it)?;
- }
- write!(f, "|}}\n")
- }
-}
-
-/// A Coq Gallina term.
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub enum GallinaTerm {
- /// a literal
- Literal(String),
- /// Application
- App(Box<AppTerm<GallinaTerm, GallinaTerm>>),
- /// a record body
- RecordBody(RecordBodyTerm),
- /// Projection a.(b) from a record
- RecordProj(Box<GallinaTerm>, String),
- /// Universal quantifiers
- All(ParamList, Box<GallinaTerm>),
- /// Existential quantifiers
- Exists(ParamList, Box<GallinaTerm>),
- /// Infix operators
- Infix(String, Vec<GallinaTerm>),
-}
-
-impl Display for GallinaTerm {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- match self {
- Self::Literal(lit) => {
- let mut f2 = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
- write!(f2, "{lit}")
- },
- Self::RecordBody(b) => {
- write!(f, "{b}")
- },
- Self::RecordProj(rec, component) => {
- write!(f, "{rec}.({component})")
- },
- Self::App(box a) => write!(f, "{a}"),
- Self::All(binders, box body) => {
- if !binders.0.is_empty() {
- write!(f, "∀ {binders}, ")?;
- }
- write!(f, "{body}")
- },
- Self::Exists(binders, box body) => {
- if !binders.0.is_empty() {
- write!(f, "∃ {binders}, ")?;
- }
- write!(f, "{body}")
- },
- Self::Infix(op, terms) => {
- if terms.is_empty() {
- write!(f, "True")
- } else {
- write!(f, "{}", terms.iter().format(&format!(" {op} ")))
- }
- },
- }
- }
-}
-
-/// A terminator for a proof script
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-pub enum ProofScriptTerminator {
- #[display("Qed")]
- Qed,
-
- #[display("Defined")]
- Defined,
-
- #[display("Admitted")]
- Admitted,
-}
-
-/// A body of a Coq definition
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub enum DefBody {
- /// a proof script invoking Ltac tactics
- Script(ProofScript, ProofScriptTerminator),
-
- /// a proof term
- Term(GallinaTerm),
-}
-
-impl Display for DefBody {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- match self {
- Self::Script(script, terminator) => {
- write!(f, ".\n")?;
- write!(f, "Proof.\n")?;
- let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
- write!(f2, "{}", script)?;
- write!(f, "{}.", terminator)?;
- },
- Self::Term(term) => {
- write!(f, " := {}.", term)?;
- },
- }
- Ok(())
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-pub enum Attribute {
- #[display("global")]
- Global,
-
- #[display("local")]
- Local,
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}",
- if attrs.is_empty() { String::new() } else {
- format!("#[ {} ]", display_list!(attrs, ", "))
- }
-)]
-pub struct Attributes {
- attrs: Vec<Attribute>,
-}
-
-impl Attributes {
- #[must_use]
- pub const fn empty() -> Self {
- Self { attrs: vec![] }
- }
-
- #[must_use]
- pub fn new(attrs: Vec<Attribute>) -> Self {
- Self { attrs }
- }
-
- #[must_use]
- pub fn singleton(attr: Attribute) -> Self {
- Self { attrs: vec![attr] }
- }
-}
-
-/// A Coq typeclass instance declaration
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("#[global] Instance : {}{}", ty, body)]
-pub struct InstanceDecl {
- ty: Type,
- body: DefBody,
-}
-
-impl InstanceDecl {
- #[must_use]
- pub const fn new(ty: Type, body: DefBody) -> Self {
- Self { ty, body }
- }
-}
-
-#[derive(Clone, Debug, Display, Eq, PartialEq)]
-#[display("{} {} : {}", name, params, ty)]
-pub struct RecordDeclItem {
- pub name: String,
- pub params: ParamList,
- pub ty: Type,
-}
-
-/// A record declaration.
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Record {
- pub name: String,
- pub params: ParamList,
- pub ty: Type,
- pub constructor: Option<String>,
- pub body: Vec<RecordDeclItem>,
-}
-
-impl Display for Record {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- let constructor = self.constructor.clone().unwrap_or_default();
- write!(f, "Record {} {} : {} := {constructor} {{\n", self.name, self.params, self.ty)?;
- let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
- for it in &self.body {
- write!(f2, "{it};\n")?;
- }
- write!(f, "}}.")
- }
-}
-
-/// A Context declaration.
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct ContextDecl {
- pub items: ParamList,
-}
-
-impl ContextDecl {
- #[must_use]
- pub const fn new(items: ParamList) -> Self {
- Self { items }
- }
-
- #[must_use]
- pub fn refinedrust() -> Self {
- Self {
- items: ParamList::new(vec![Param::new(
- Name::Named("RRGS".to_owned()),
- Type::Literal("refinedrustGS Σ".to_owned()),
- true,
- )]),
- }
- }
-}
-
-impl Display for ContextDecl {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- if self.items.0.is_empty() { Ok(()) } else { write!(f, "Context {}.", self.items) }
- }
-}
-
-#[derive(Clone, Debug, Eq, PartialEq, Display)]
-pub enum DefinitionKind {
- #[display("Definition")]
- Definition,
- #[display("Lemma")]
- Lemma,
-}
-
-/// A Coq definition
-#[derive(Clone, Debug, Eq, PartialEq)]
-pub struct Definition {
- pub name: String,
- pub params: ParamList,
- pub ty: Option<Type>,
- pub body: DefBody,
- pub kind: DefinitionKind,
-}
-
-impl Display for Definition {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- if let Some(ty) = &self.ty {
- write!(f, "{} {} {} : {ty}{}", self.kind, self.name, self.params, self.body)
- } else {
- write!(f, "{} {} {}{}", self.kind, self.name, self.params, self.body)
- }
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-pub enum TopLevelAssertion<'a> {
- /// A declaration of a Coq Inductive
- #[display("{}", _0)]
- InductiveDecl(&'a Inductive),
-
- /// A declaration of a Coq instance
- #[display("{}", _0)]
- InstanceDecl(&'a InstanceDecl),
-
- /// A declaration of a Coq record
- #[display("{}", _0)]
- RecordDecl(Record),
-
- /// A declaration of Coq context items
- #[display("{}", _0)]
- ContextDecl(ContextDecl),
-
- /// A Coq Definition
- #[display("{}", _0)]
- Definition(Definition),
-
- /// A Coq comment
- #[display("(* {} *)", _0)]
- Comment(&'a str),
-
- /// A Coq section
- #[display("Section {}.\n{}End{}.", _0, Indented::new(_1), _0)]
- Section(String, TopLevelAssertions<'a>),
-
- /// A Coq section start
- #[display("Section {}.", _0)]
- SectionStart(String),
-
- /// A Coq section end
- #[display("End {}.", _0)]
- SectionEnd(String),
-}
-
-/// Type for writing contents indented via Display.
-struct Indented<T> {
- x: T,
-}
-impl<T> Indented<T> {
- pub const fn new(x: T) -> Self {
- Self { x }
- }
-}
-impl<T: Display> Display for Indented<T> {
- fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- let mut indent_writer = IndentWriter::new(BASE_INDENT, f);
- write!(indent_writer, "{}", self.x)
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}", display_list!(_0, "\n"))]
-pub struct TopLevelAssertions<'a>(pub Vec<TopLevelAssertion<'a>>);
-
-impl<'a> TopLevelAssertions<'a> {
- #[must_use]
- pub(crate) const fn empty() -> Self {
- Self(vec![])
- }
-
- pub(crate) fn push(&mut self, a: TopLevelAssertion<'a>) {
- self.0.push(a);
- }
-}
+/// As such, they may not be suitable for general use.
+pub mod command;
+pub mod module;
+pub mod term;
diff --git a/rr_frontend/radium/src/coq/module.rs b/rr_frontend/radium/src/coq/module.rs
index 598af49..d986f80 100644
--- a/rr_frontend/radium/src/coq/module.rs
+++ b/rr_frontend/radium/src/coq/module.rs
@@ -4,7 +4,7 @@
// 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/.
-/// Rocq modules, which contains imports and exports.
+/// Rocq module system.
use std::fmt;
use std::ops::Deref;
diff --git a/rr_frontend/radium/src/coq/term.rs b/rr_frontend/radium/src/coq/term.rs
new file mode 100644
index 0000000..8c81804
--- /dev/null
+++ b/rr_frontend/radium/src/coq/term.rs
@@ -0,0 +1,414 @@
+// © 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/.
+
+/// Rocq terms.
+use std::fmt::{self, Write};
+
+use derive_more::Display;
+use indent_write::fmt::IndentWriter;
+use indent_write::indentable::Indentable;
+use itertools::Itertools;
+
+use crate::{display_list, make_indent, write_list, BASE_INDENT};
+
+/// Represents an application of a term to an rhs.
+/// (commonly used for layouts and instantiating them with generics).
+#[derive(Clone, Eq, PartialEq, Hash, Debug)]
+pub struct App<T, U> {
+ pub(crate) lhs: T,
+ pub(crate) rhs: Vec<U>,
+}
+
+impl<T: Display, U: Display> Display for App<T, U> {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ if self.rhs.is_empty() {
+ return write!(f, "{}", self.lhs);
+ }
+
+ write_list!(f, &self.rhs, " ", "({})")
+ }
+}
+
+impl<T, U> App<T, U> {
+ pub fn new(lhs: T, rhs: Vec<U>) -> Self {
+ Self { lhs, rhs }
+ }
+
+ pub fn new_lhs(lhs: T) -> Self {
+ Self {
+ lhs,
+ rhs: Vec::new(),
+ }
+ }
+
+ pub(crate) const fn get_lhs(&self) -> &T {
+ &self.lhs
+ }
+}
+
+/// A Coq Gallina term.
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub enum Gallina {
+ /// a literal
+ Literal(String),
+ /// Application
+ App(Box<App<Gallina, Gallina>>),
+ /// a record body
+ RecordBody(RecordBody),
+ /// Projection a.(b) from a record
+ RecordProj(Box<Gallina>, String),
+ /// Universal quantifiers
+ All(ParamList, Box<Gallina>),
+ /// Existential quantifiers
+ Exists(ParamList, Box<Gallina>),
+ /// Infix operators
+ Infix(String, Vec<Gallina>),
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct RecordBodyItem {
+ pub name: String,
+ pub params: ParamList,
+ pub term: Gallina,
+}
+
+impl Display for RecordBodyItem {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let mut writer = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
+ write!(writer, "{} {} :=\n{};", self.name, self.params, self.term)
+ }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct RecordBody {
+ pub items: Vec<RecordBodyItem>,
+}
+
+impl Display for RecordBody {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ write!(f, "{{|\n")?;
+ let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
+ for it in &self.items {
+ write!(f2, "{}\n", it)?;
+ }
+ write!(f, "|}}\n")
+ }
+}
+
+impl Display for Gallina {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ match self {
+ Self::Literal(lit) => {
+ let mut f2 = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
+ write!(f2, "{lit}")
+ },
+ Self::RecordBody(b) => {
+ write!(f, "{b}")
+ },
+ Self::RecordProj(rec, component) => {
+ write!(f, "{rec}.({component})")
+ },
+ Self::App(box a) => write!(f, "{a}"),
+ Self::All(binders, box body) => {
+ if !binders.0.is_empty() {
+ write!(f, "∀ {binders}, ")?;
+ }
+ write!(f, "{body}")
+ },
+ Self::Exists(binders, box body) => {
+ if !binders.0.is_empty() {
+ write!(f, "∃ {binders}, ")?;
+ }
+ write!(f, "{body}")
+ },
+ Self::Infix(op, terms) => {
+ if terms.is_empty() {
+ write!(f, "True")
+ } else {
+ write!(f, "{}", terms.iter().format(&format!(" {op} ")))
+ }
+ },
+ }
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Ord, PartialOrd, Debug, Display)]
+pub enum Name {
+ #[display("{}", _0)]
+ Named(String),
+
+ #[display("_")]
+ Unnamed,
+}
+
+/// A Coq pattern, e.g., "x" or "'(x, y)".
+pub type Pattern = String;
+
+fn fmt_prod(v: &Vec<Type>) -> String {
+ match v.as_slice() {
+ [] => "unit".to_owned(),
+ [t] => t.to_string(),
+ _ => format!("({})%type", display_list!(v, " * ")),
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum Type {
+ /// literal types that are not contained in the grammar
+ #[display("{}", _0)]
+ Literal(String),
+
+ /// function types; the argument vector should be non-empty
+ #[display("{} → {}", display_list!(_0, " → ", "({})"), *_1)]
+ Function(Vec<Type>, Box<Type>),
+
+ /// Placeholder that should be inferred by Coq if possible
+ #[display("_")]
+ Infer,
+
+ /// Coq type `lft`
+ #[display("lft")]
+ Lft,
+
+ /// Coq type `loc`
+ #[display("loc")]
+ Loc,
+
+ /// Coq type `layout`
+ #[display("layout")]
+ Layout,
+
+ /// Coq type `syn_type`
+ #[display("syn_type")]
+ SynType,
+
+ /// Coq type `struct_layout`
+ #[display("struct_layout")]
+ StructLayout,
+
+ /// Coq type `Type`
+ #[display("Type")]
+ Type,
+
+ /// Coq type `type rt`
+ #[display("(type {})", &_0)]
+ Ttype(Box<Type>),
+
+ /// Coq type `rtype`
+ #[display("rtype")]
+ Rtype,
+
+ /// the unit type
+ #[display("unit")]
+ Unit,
+
+ /// the type of integers
+ #[display("Z")]
+ Z,
+
+ /// the type of booleans
+ #[display("bool")]
+ Bool,
+
+ /// product types
+ #[display("{}", fmt_prod(_0))]
+ Prod(Vec<Type>),
+
+ /// place_rfn
+ #[display("(place_rfn {})", &_0)]
+ PlaceRfn(Box<Type>),
+
+ /// gname
+ #[display("gname")]
+ Gname,
+
+ /// a plist with a given type constructor over a list of types
+ #[display("plist {} [{}]", _0, display_list!(_1, "; ", "{} : Type"))]
+ PList(String, Vec<Type>),
+
+ /// the semantic type of a function
+ #[display("function_ty")]
+ FunctionTy,
+
+ /// the Coq type Prop of propositions
+ #[display("Prop")]
+ Prop,
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}", self.format(true))]
+pub struct Param {
+ /// the name
+ name: Name,
+
+ /// the type
+ ty: Type,
+
+ /// implicit or not?
+ implicit: bool,
+
+ /// does this depend on Σ?
+ depends_on_sigma: bool,
+}
+
+impl Param {
+ #[must_use]
+ pub fn new(name: Name, ty: Type, implicit: bool) -> Self {
+ let depends_on_sigma = if let Type::Literal(lit) = &ty { lit.contains('Σ') } else { false };
+
+ Self {
+ name,
+ ty,
+ implicit,
+ depends_on_sigma,
+ }
+ }
+
+ #[must_use]
+ pub fn with_name(&self, name: String) -> Self {
+ Self::new(Name::Named(name), self.ty.clone(), self.implicit)
+ }
+
+ #[must_use]
+ pub fn get_name_ref(&self) -> Option<&str> {
+ match &self.name {
+ Name::Named(s) => Some(s),
+ Name::Unnamed => None,
+ }
+ }
+
+ #[allow(clippy::collapsible_else_if)]
+ #[must_use]
+ fn format(&self, make_implicits: bool) -> String {
+ if !self.implicit {
+ return format!("({} : {})", self.name, self.ty);
+ }
+
+ if make_implicits {
+ if let Name::Named(name) = &self.name {
+ format!("`{{{} : !{}}}", name, self.ty)
+ } else {
+ format!("`{{!{}}}", self.ty)
+ }
+ } else {
+ if let Name::Named(name) = &self.name {
+ format!("`({} : !{})", name, self.ty)
+ } else {
+ format!("`(!{})", self.ty)
+ }
+ }
+ }
+
+ pub(crate) const fn get_name(&self) -> &Name {
+ &self.name
+ }
+
+ pub(crate) const fn is_implicit(&self) -> bool {
+ self.implicit
+ }
+
+ pub(crate) const fn is_dependent_on_sigma(&self) -> bool {
+ self.depends_on_sigma
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}", display_list!(_0, " "))]
+pub struct ParamList(pub Vec<Param>);
+
+impl ParamList {
+ #[must_use]
+ pub const fn new(params: Vec<Param>) -> Self {
+ Self(params)
+ }
+
+ #[must_use]
+ pub const fn empty() -> Self {
+ Self(vec![])
+ }
+
+ pub fn append(&mut self, params: Vec<Param>) {
+ self.0.extend(params);
+ }
+
+ /// Make using terms for this list of binders
+ #[must_use]
+ pub fn make_using_terms(&self) -> Vec<Gallina> {
+ self.0.iter().map(|x| Gallina::Literal(format!("{}", x.name))).collect()
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{} {}", name, params)]
+pub struct Variant {
+ name: String,
+ params: ParamList,
+}
+
+impl Variant {
+ #[must_use]
+ pub fn new(name: &str, params: Vec<Param>) -> Self {
+ Self {
+ name: name.to_owned(),
+ params: ParamList::new(params),
+ }
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("Inductive {} {} :=\n{}\n.", name, parameters,
+ display_list!(variants, "\n| ").indented(&make_indent(1))
+)]
+pub struct Inductive {
+ name: String,
+ parameters: ParamList,
+ variants: Vec<Variant>,
+}
+
+impl Inductive {
+ #[must_use]
+ pub fn new(name: &str, parameters: Vec<Param>, variants: Vec<Variant>) -> Self {
+ Self {
+ name: name.to_owned(),
+ parameters: ParamList::new(parameters),
+ variants,
+ }
+ }
+
+ pub(crate) const fn get_name(&self) -> &String {
+ &self.name
+ }
+}
+
+#[derive(Clone, Debug, Display, Eq, PartialEq)]
+#[display("{} {} : {}", name, params, ty)]
+pub struct RecordDeclItem {
+ pub name: String,
+ pub params: ParamList,
+ pub ty: Type,
+}
+
+/// A record declaration.
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub struct Record {
+ pub name: String,
+ pub params: ParamList,
+ pub ty: Type,
+ pub constructor: Option<String>,
+ pub body: Vec<RecordDeclItem>,
+}
+
+impl Display for Record {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ let constructor = self.constructor.clone().unwrap_or_default();
+ write!(f, "Record {} {} : {} := {constructor} {{\n", self.name, self.params, self.ty)?;
+ let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
+ for it in &self.body {
+ write!(f2, "{it};\n")?;
+ }
+ write!(f, "}}.")
+ }
+}
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 29410d8..92fef72 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -5,7 +5,6 @@
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
/// Provides the Spec AST and utilities for interfacing with it.
-use std::cell::{OnceCell, RefCell};
use std::collections::{HashMap, HashSet};
use std::fmt::{Formatter, Write};
use std::ops::{Add, Range};
@@ -145,9 +144,9 @@ pub enum OpType {
Char,
Ptr,
// a term for the struct_layout, and optypes for the individual fields
- Struct(coq::AppTerm<String, String>, Vec<OpType>),
+ Struct(coq::term::App<String, String>, Vec<OpType>),
Untyped(Layout),
- Literal(coq::AppTerm<String, String>),
+ Literal(coq::term::App<String, String>),
}
impl Display for OpType {
@@ -214,6 +213,7 @@ impl From<SynType> for Layout {
Self::from(&x)
}
}
+
impl From<&SynType> for Layout {
/// Get a Coq term for the layout of this syntactic type.
/// This may call the Coq-level layout algorithm that we assume.
@@ -230,7 +230,7 @@ impl From<&SynType> for Layout {
SynType::Literal(ca) => {
let rhs = ca.to_owned();
- Self::Literal(coq::AppTerm::new("use_layout_alg'".to_owned(), vec![rhs]))
+ Self::Literal(coq::term::App::new("use_layout_alg'".to_owned(), vec![rhs]))
},
}
}
@@ -254,12 +254,12 @@ impl From<&SynType> for OpType {
SynType::Ptr | SynType::FnPtr => Self::Ptr,
SynType::Untyped(ly) => Self::Untyped(ly.clone()),
- SynType::Unit => Self::Struct(coq::AppTerm::new_lhs("unit_sl".to_owned()), Vec::new()),
+ SynType::Unit => Self::Struct(coq::term::App::new_lhs("unit_sl".to_owned()), Vec::new()),
SynType::Never => Self::Untyped(Layout::Unit),
SynType::Literal(ca) => {
let rhs = ca.to_owned();
- Self::Literal(coq::AppTerm::new("use_op_alg'".to_owned(), vec![rhs]))
+ Self::Literal(coq::term::App::new("use_op_alg'".to_owned(), vec![rhs]))
},
}
}
@@ -318,7 +318,7 @@ pub struct LiteralType {
/// Coq name of the type
pub type_term: String,
/// the refinement type
- pub refinement_type: coq::Type,
+ pub refinement_type: coq::term::Type,
/// the syntactic type
pub syn_type: SynType,
}
@@ -374,7 +374,7 @@ impl<'def> LiteralTypeUse<'def> {
self.params.iter().map(|ty| ty.get_rfn_type().to_string()).collect();
let rfn_type = self.def.refinement_type.to_string();
- let applied = coq::AppTerm::new(rfn_type, rfn_instantiations);
+ let applied = coq::term::App::new(rfn_type, rfn_instantiations);
applied.to_string()
}
@@ -387,7 +387,7 @@ impl<'def> LiteralTypeUse<'def> {
let st: SynType = p.into();
param_sts.push(format!("({})", st));
}
- let specialized_spec = coq::AppTerm::new(self.def.syn_type.clone(), param_sts);
+ let specialized_spec = coq::term::App::new(self.def.syn_type.clone(), param_sts);
SynType::Literal(specialized_spec.to_string())
}
@@ -399,7 +399,7 @@ impl<'def> LiteralTypeUse<'def> {
let st: SynType = p.into();
param_sts.push(format!("({})", st));
}
- let specialized_spec = coq::AppTerm::new(self.def.syn_type.clone(), param_sts).to_string();
+ let specialized_spec = coq::term::App::new(self.def.syn_type.clone(), param_sts).to_string();
SynType::Literal(format!("({specialized_spec} : syn_type)"))
}
@@ -410,7 +410,7 @@ impl<'def> LiteralTypeUse<'def> {
for p in &self.params {
param_tys.push(format!("({})", p));
}
- let specialized_term = coq::AppTerm::new(self.def.type_term.clone(), param_tys);
+ let specialized_term = coq::term::App::new(self.def.type_term.clone(), param_tys);
specialized_term.to_string()
}
}
@@ -466,19 +466,23 @@ impl LiteralTyParam {
LiteralType {
rust_name: Some(self.rust_name.clone()),
type_term: self.type_term.clone(),
- refinement_type: coq::Type::Literal(self.refinement_type.clone()),
+ refinement_type: coq::term::Type::Literal(self.refinement_type.clone()),
syn_type: SynType::Literal(self.syn_type.clone()),
}
}
#[must_use]
- pub fn make_refinement_param(&self) -> coq::Param {
- coq::Param::new(coq::Name::Named(self.refinement_type.clone()), coq::Type::Type, false)
+ pub fn make_refinement_param(&self) -> coq::term::Param {
+ coq::term::Param::new(
+ coq::term::Name::Named(self.refinement_type.clone()),
+ coq::term::Type::Type,
+ false,
+ )
}
#[must_use]
- pub fn make_syntype_param(&self) -> coq::Param {
- coq::Param::new(coq::Name::Named(self.syn_type.clone()), coq::Type::SynType, false)
+ pub fn make_syntype_param(&self) -> coq::term::Param {
+ coq::term::Param::new(coq::term::Name::Named(self.syn_type.clone()), coq::term::Type::SynType, false)
}
}
@@ -578,28 +582,29 @@ impl<'def> Type<'def> {
/// Determines the type this type is refined by.
#[must_use]
- pub fn get_rfn_type(&self) -> coq::Type {
+ pub fn get_rfn_type(&self) -> coq::term::Type {
match self {
- Self::Bool => coq::Type::Bool,
- Self::Char | Self::Int(_) => coq::Type::Z,
+ Self::Bool => coq::term::Type::Bool,
+ Self::Char | Self::Int(_) => coq::term::Type::Z,
- Self::MutRef(box ty, _) => {
- coq::Type::Prod(vec![coq::Type::PlaceRfn(Box::new(ty.get_rfn_type())), coq::Type::Gname])
- },
+ Self::MutRef(box ty, _) => coq::term::Type::Prod(vec![
+ coq::term::Type::PlaceRfn(Box::new(ty.get_rfn_type())),
+ coq::term::Type::Gname,
+ ]),
Self::ShrRef(box ty, _) | Self::BoxType(box ty) => {
- coq::Type::PlaceRfn(Box::new(ty.get_rfn_type()))
+ coq::term::Type::PlaceRfn(Box::new(ty.get_rfn_type()))
},
- Self::RawPtr => coq::Type::Loc,
+ Self::RawPtr => coq::term::Type::Loc,
- Self::LiteralParam(lit) => coq::Type::Literal(lit.refinement_type.clone()),
- Self::Literal(lit) => coq::Type::Literal(lit.get_rfn_type()),
+ Self::LiteralParam(lit) => coq::term::Type::Literal(lit.refinement_type.clone()),
+ Self::Literal(lit) => coq::term::Type::Literal(lit.get_rfn_type()),
Self::Struct(su) => {
// NOTE: we don't need to subst, due to our invariant that the instantiations for
// struct uses are already fully substituted
- coq::Type::Literal(su.get_rfn_type())
+ coq::term::Type::Literal(su.get_rfn_type())
},
Self::Enum(su) => {
// similar to structs, we don't need to subst
@@ -608,7 +613,7 @@ impl<'def> Type<'def> {
Self::Unit | Self::Never | Self::Uninit(_) => {
// NOTE: could also choose to use an uninhabited type for Never
- coq::Type::Unit
+ coq::term::Type::Unit
},
}
}
@@ -735,12 +740,12 @@ pub struct InvariantSpec {
shr_lft_binder: String,
/// the refinement type of this struct
- rfn_type: coq::Type,
+ rfn_type: coq::term::Type,
/// the binding pattern for the refinement of this type
- rfn_pat: coq::Pattern,
+ rfn_pat: coq::term::Pattern,
/// existentials that are introduced in the invariant
- existentials: Vec<(coq::Name, coq::Type)>,
+ existentials: Vec<(coq::term::Name, coq::term::Type)>,
/// an optional invariant as a separating conjunction,
invariants: Vec<(IProp, InvariantMode)>,
@@ -748,10 +753,10 @@ pub struct InvariantSpec {
ty_own_invariants: Vec<TyOwnSpec>,
/// the specification of the abstracted refinement under a context where rfn_pat is bound
- abstracted_refinement: Option<coq::Pattern>,
+ abstracted_refinement: Option<coq::term::Pattern>,
// TODO add stuff for non-atomic/atomic invariants
/// name, type, implicit or not
- coq_params: Vec<coq::Param>,
+ coq_params: Vec<coq::term::Param>,
}
impl InvariantSpec {
@@ -760,13 +765,13 @@ impl InvariantSpec {
type_name: String,
flags: InvariantSpecFlags,
shr_lft_binder: String,
- rfn_type: coq::Type,
- rfn_pat: coq::Pattern,
- existentials: Vec<(coq::Name, coq::Type)>,
+ rfn_type: coq::term::Type,
+ rfn_pat: coq::term::Pattern,
+ existentials: Vec<(coq::term::Name, coq::term::Type)>,
invariants: Vec<(IProp, InvariantMode)>,
ty_own_invariants: Vec<TyOwnSpec>,
- abstracted_refinement: Option<coq::Pattern>,
- coq_params: Vec<coq::Param>,
+ abstracted_refinement: Option<coq::term::Pattern>,
+ coq_params: Vec<coq::term::Param>,
) -> Self {
if flags == InvariantSpecFlags::Persistent {
assert!(invariants.iter().all(|it| it.1 == InvariantMode::All) && ty_own_invariants.is_empty());
@@ -787,7 +792,7 @@ impl InvariantSpec {
}
/// Add the abstracted refinement, if it was not already provided.
- pub fn provide_abstracted_refinement(&mut self, abstracted_refinement: coq::Pattern) {
+ pub fn provide_abstracted_refinement(&mut self, abstracted_refinement: coq::term::Pattern) {
if self.abstracted_refinement.is_some() {
panic!("abstracted refinement for {} already provided", self.type_name);
}
@@ -1048,11 +1053,11 @@ impl InvariantSpec {
// get the applied base_rfn_type
let rfn_instantiations: Vec<String> =
generic_params.iter().map(|names| names.refinement_type.clone()).collect();
- let applied_base_rfn_type = coq::AppTerm::new(base_rfn_type, rfn_instantiations.clone());
+ let applied_base_rfn_type = coq::term::App::new(base_rfn_type, rfn_instantiations.clone());
// get the applied base type
let base_type_app: Vec<String> = generic_params.iter().map(|names| names.type_term.clone()).collect();
- let applied_base_type = coq::AppTerm::new(base_type_name, base_type_app);
+ let applied_base_type = coq::term::App::new(base_type_name, base_type_app);
write!(
out,
@@ -1157,7 +1162,7 @@ pub struct AbstractVariant<'def> {
/// the fields, closed under a surrounding scope
fields: Vec<(String, Type<'def>)>,
/// the refinement type of the plain struct
- rfn_type: coq::Type,
+ rfn_type: coq::term::Type,
/// the struct representation mode
repr: StructRepr,
/// the struct's name
@@ -1242,7 +1247,7 @@ impl<'def> AbstractVariant<'def> {
pub fn generate_coq_type_term(&self, sls_app: Vec<String>) -> String {
let mut out = String::with_capacity(200);
- out.push_str(&format!("struct_t {} +[", coq::AppTerm::new(&self.sls_def_name, sls_app)));
+ out.push_str(&format!("struct_t {} +[", coq::term::App::new(&self.sls_def_name, sls_app)));
push_str_list!(out, &self.fields, ";", |(_, ty)| ty.to_string());
out.push(']');
@@ -1303,7 +1308,7 @@ impl<'def> AbstractVariant<'def> {
pub fn generate_coq_type_def(
&self,
ty_params: &[LiteralTyParam],
- extra_context: &[coq::Param],
+ extra_context: &[coq::term::Param],
) -> String {
let mut out = String::with_capacity(200);
let indent = " ";
@@ -1351,7 +1356,10 @@ impl<'def> AbstractVariant<'def> {
}
}
-fn format_extra_context_items<F>(items: &[coq::Param], f: &mut F) -> Result<(Vec<String>, bool), fmt::Error>
+fn format_extra_context_items<F>(
+ items: &[coq::term::Param],
+ f: &mut F,
+) -> Result<(Vec<String>, bool), fmt::Error>
where
F: Write,
{
@@ -1492,7 +1500,7 @@ impl<'def> AbstractStruct<'def> {
LiteralType {
rust_name: Some(self.name().to_owned()),
type_term: self.public_type_name().to_owned(),
- refinement_type: coq::Type::Literal(self.public_rt_def_name()),
+ refinement_type: coq::term::Type::Literal(self.public_rt_def_name()),
syn_type: SynType::Literal(self.sls_def_name().to_owned()),
}
}
@@ -1516,7 +1524,7 @@ impl<'def> VariantBuilder<'def> {
let plain_ty_name: String = format!("{}_ty", &self.name);
let plain_rt_def_name: String = format!("{}_rt", &self.name);
- let rfn_type = coq::Type::PList(
+ let rfn_type = coq::term::Type::PList(
"place_rfn".to_owned(),
self.fields.iter().map(|(_, t)| t.get_rfn_type()).collect(),
);
@@ -1645,7 +1653,7 @@ impl<'def> AbstractStructUse<'def> {
#[must_use]
pub fn get_rfn_type(&self) -> String {
let Some(def) = self.def.as_ref() else {
- return coq::Type::Unit.to_string();
+ return coq::term::Type::Unit.to_string();
};
let rfn_instantiations: Vec<String> =
@@ -1655,11 +1663,11 @@ impl<'def> AbstractStructUse<'def> {
if self.is_raw() || inv.is_none() {
let rfn_type = def.plain_rt_def_name().to_owned();
- let applied = coq::AppTerm::new(rfn_type, rfn_instantiations);
+ let applied = coq::term::App::new(rfn_type, rfn_instantiations);
applied.to_string()
} else {
let rfn_type = inv.as_ref().unwrap().rt_def_name();
- let applied = coq::AppTerm::new(rfn_type, rfn_instantiations);
+ let applied = coq::term::App::new(rfn_type, rfn_instantiations);
applied.to_string()
}
}
@@ -1679,8 +1687,8 @@ impl<'def> AbstractStructUse<'def> {
}
// use_struct_layout_alg' ([my_spec] [params])
- let specialized_spec = format!("({})", coq::AppTerm::new(def.sls_def_name(), param_sts));
- coq::AppTerm::new("use_struct_layout_alg'".to_owned(), vec![specialized_spec]).to_string()
+ let specialized_spec = format!("({})", coq::term::App::new(def.sls_def_name(), param_sts));
+ coq::term::App::new("use_struct_layout_alg'".to_owned(), vec![specialized_spec]).to_string()
}
#[must_use]
@@ -1698,7 +1706,7 @@ impl<'def> AbstractStructUse<'def> {
// TODO generates too many apps
// use_struct_layout_alg' ([my_spec] [params])
- format!("({})", coq::AppTerm::new(def.sls_def_name(), param_sts))
+ format!("({})", coq::term::App::new(def.sls_def_name(), param_sts))
}
/// Get the `syn_type` term for this struct use.
@@ -1716,7 +1724,7 @@ impl<'def> AbstractStructUse<'def> {
}
// TODO generates too many apps
- let specialized_spec = coq::AppTerm::new(def.st_def_name().to_owned(), param_sts);
+ let specialized_spec = coq::term::App::new(def.st_def_name().to_owned(), param_sts);
SynType::Literal(specialized_spec.to_string())
}
@@ -1737,9 +1745,9 @@ impl<'def> AbstractStructUse<'def> {
unreachable!();
};
- coq::AppTerm::new(inv.type_name.clone(), param_tys).to_string()
+ coq::term::App::new(inv.type_name.clone(), param_tys).to_string()
} else {
- coq::AppTerm::new(def.plain_ty_name(), param_tys).to_string()
+ coq::term::App::new(def.plain_ty_name(), param_tys).to_string()
}
}
}
@@ -1748,7 +1756,7 @@ impl<'def> AbstractStructUse<'def> {
#[derive(Clone, Eq, PartialEq, Debug)]
pub struct EnumSpec {
/// the refinement type of the enum
- pub rfn_type: coq::Type,
+ pub rfn_type: coq::term::Type,
/// the refinement patterns for each of the variants
/// eg. for options:
/// - `(None, [], -[])`
@@ -1789,7 +1797,7 @@ pub struct AbstractEnum<'def> {
repr: EnumRepr,
/// an optional declaration of a Coq inductive for this enum
- optional_inductive_def: Option<coq::Inductive>,
+ optional_inductive_def: Option<coq::term::Inductive>,
/// name of the plain enum type (without additional invariants)
plain_ty_name: String,
@@ -1930,7 +1938,7 @@ impl<'def> AbstractEnum<'def> {
let spec = &self.spec;
write!(out, "λ rfn, match rfn with ").unwrap();
for ((name, _, _), (pat, apps, _)) in self.variants.iter().zip(spec.variant_patterns.iter()) {
- write!(out, "| {} => \"{name}\" ", coq::AppTerm::new(pat, apps.clone())).unwrap();
+ write!(out, "| {} => \"{name}\" ", coq::term::App::new(pat, apps.clone())).unwrap();
}
write!(out, "end").unwrap();
@@ -1951,7 +1959,7 @@ impl<'def> AbstractEnum<'def> {
// environment where all the type parametes are already instantiated.
let ty = v.public_type_name();
- write!(out, "| {} => existT _ ({ty}, {rfn})", coq::AppTerm::new(pat, apps.clone())).unwrap();
+ write!(out, "| {} => existT _ ({ty}, {rfn})", coq::term::App::new(pat, apps.clone())).unwrap();
}
write!(out, " end").unwrap();
@@ -2018,7 +2026,7 @@ impl<'def> AbstractEnum<'def> {
tag,
ty_def_term,
res,
- coq::AppTerm::new(pat, args.clone())
+ coq::term::App::new(pat, args.clone())
)
.unwrap();
write!(out, "{indent}Next Obligation. intros; unfold TCDone in *; naive_solver. Qed.\n").unwrap();
@@ -2082,21 +2090,26 @@ impl<'def> AbstractEnum<'def> {
writeln!(
out,
"{}",
- coq::TopLevelAssertion::Comment(&format!("auto-generated representation of {}", name))
+ coq::command::TopLevelAssertion::Comment(&format!(
+ "auto-generated representation of {}",
+ name
+ ))
)
.unwrap();
- writeln!(out, "{}", coq::TopLevelAssertion::InductiveDecl(ind)).unwrap();
+ writeln!(out, "{}", coq::command::TopLevelAssertion::InductiveDecl(ind)).unwrap();
// prove that it is inhabited
writeln!(
out,
"{}",
- coq::TopLevelAssertion::InstanceDecl(&coq::InstanceDecl::new(
- coq::Type::Literal(format!("Inhabited {}", name)),
- coq::DefBody::Script(
- coq::ProofScript(vec![coq::ProofItem::Literal("solve_inhabited".to_owned())]),
- coq::ProofScriptTerminator::Qed,
+ coq::command::TopLevelAssertion::InstanceDecl(&coq::command::InstanceDecl::new(
+ coq::term::Type::Literal(format!("Inhabited {}", name)),
+ coq::command::DefBody::Script(
+ coq::command::ProofScript(vec![coq::command::ProofItem::Literal(
+ "solve_inhabited".to_owned()
+ )]),
+ coq::command::ProofScriptTerminator::Qed,
),
))
)
@@ -2110,7 +2123,7 @@ impl<'def> AbstractEnum<'def> {
let term = format!("(ty_syn_type {})", names.type_term);
els_app.push(term);
}
- let els_app_term = coq::AppTerm::new(&self.els_def_name, els_app);
+ let els_app_term = coq::term::App::new(&self.els_def_name, els_app);
// main def
write!(
@@ -2169,7 +2182,7 @@ impl<'def> AbstractEnum<'def> {
LiteralType {
rust_name: Some(self.name().to_owned()),
type_term: self.public_type_name().to_owned(),
- refinement_type: coq::Type::Literal(self.public_rt_def_name().to_owned()),
+ refinement_type: coq::term::Type::Literal(self.public_rt_def_name().to_owned()),
syn_type: SynType::Literal(self.els_def_name().to_owned()),
}
}
@@ -2194,7 +2207,7 @@ impl<'def> EnumBuilder<'def> {
#[must_use]
pub fn finish(
self,
- optional_inductive_def: Option<coq::Inductive>,
+ optional_inductive_def: Option<coq::term::Inductive>,
spec: EnumSpec,
) -> AbstractEnum<'def> {
let els_def_name: String = format!("{}_els", &self.name);
@@ -2283,7 +2296,7 @@ impl<'def> AbstractEnumUse<'def> {
/// Get the refinement type of an enum usage.
/// This requires that all type parameters of the enum have been instantiated.
#[must_use]
- pub fn get_rfn_type(&self) -> coq::Type {
+ pub fn get_rfn_type(&self) -> coq::term::Type {
self.def.spec.rfn_type.clone()
}
@@ -2298,8 +2311,8 @@ impl<'def> AbstractEnumUse<'def> {
}
// use_struct_layout_alg' ([my_spec] [params])
- let specialized_spec = format!("({})", coq::AppTerm::new(self.def.els_def_name.clone(), param_sts));
- coq::AppTerm::new("use_enum_layout_alg'".to_owned(), vec![specialized_spec]).to_string()
+ let specialized_spec = format!("({})", coq::term::App::new(self.def.els_def_name.clone(), param_sts));
+ coq::term::App::new("use_enum_layout_alg'".to_owned(), vec![specialized_spec]).to_string()
}
/// Generate a term for the enum layout spec (of type `enum_layout_spec`).
@@ -2313,7 +2326,7 @@ impl<'def> AbstractEnumUse<'def> {
}
// use_struct_layout_alg' ([my_spec] [params])
- format!("({})", coq::AppTerm::new(self.def.els_def_name.clone(), param_sts))
+ format!("({})", coq::term::App::new(self.def.els_def_name.clone(), param_sts))
}
/// Get the `syn_type` term for this enum use.
@@ -2327,7 +2340,7 @@ impl<'def> AbstractEnumUse<'def> {
}
// [my_spec] [params]
- let specialized_spec = coq::AppTerm::new(self.def.st_def_name.clone(), param_sts);
+ let specialized_spec = coq::term::App::new(self.def.st_def_name.clone(), param_sts);
SynType::Literal(specialized_spec.to_string())
}
@@ -2338,7 +2351,7 @@ impl<'def> AbstractEnumUse<'def> {
for p in &self.ty_params {
param_tys.push(format!("({})", p));
}
- let term = coq::AppTerm::new(self.def.plain_ty_name.clone(), param_tys);
+ let term = coq::term::App::new(self.def.plain_ty_name.clone(), param_tys);
term.to_string()
}
}
@@ -2365,7 +2378,7 @@ pub enum Layout {
Unit,
/// used for variable layout terms, e.g. for struct layouts or generics
- Literal(coq::AppTerm<String, String>),
+ Literal(coq::term::App<String, String>),
/// padding of a given number of bytes
Pad(u32),
@@ -2429,10 +2442,10 @@ impl Layout {
// apart when generating them.
#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct CoqBinder(coq::Name, coq::Type);
+pub struct CoqBinder(coq::term::Name, coq::term::Type);
impl CoqBinder {
#[must_use]
- pub const fn new(n: coq::Name, t: coq::Type) -> Self {
+ pub const fn new(n: coq::term::Name, t: coq::term::Type) -> Self {
Self(n, t)
}
}
@@ -2548,7 +2561,7 @@ impl<'def> InnerFunctionSpec<'def> {
}
#[must_use]
- pub fn get_params(&self) -> Option<&[(coq::Name, coq::Type)]> {
+ pub fn get_params(&self) -> Option<&[(coq::term::Name, coq::term::Type)]> {
match self {
Self::Lit(lit) => Some(&lit.params),
Self::TraitDefault(_) => None,
@@ -2567,8 +2580,8 @@ pub struct FunctionSpec<T> {
pub generics: GenericScope,
/// Coq-level parameters the typing statement needs
- pub early_coq_params: coq::ParamList,
- pub late_coq_params: coq::ParamList,
+ pub early_coq_params: coq::term::ParamList,
+ pub late_coq_params: coq::term::ParamList,
pub spec: T,
}
@@ -2591,8 +2604,8 @@ impl<T> FunctionSpec<T> {
spec_name,
function_name,
generics: GenericScope::empty(),
- early_coq_params: coq::ParamList::empty(),
- late_coq_params: coq::ParamList::empty(),
+ early_coq_params: coq::term::ParamList::empty(),
+ late_coq_params: coq::term::ParamList::empty(),
spec,
}
}
@@ -2602,8 +2615,8 @@ impl<T> FunctionSpec<T> {
spec_name: String,
function_name: String,
generics: GenericScope,
- early_params: coq::ParamList,
- late_params: coq::ParamList,
+ early_params: coq::term::ParamList,
+ late_params: coq::term::ParamList,
spec: T,
) -> Self {
Self {
@@ -2622,7 +2635,7 @@ impl<T> FunctionSpec<T> {
}
#[must_use]
- pub fn get_all_coq_params(&self) -> coq::ParamList {
+ pub fn get_all_coq_params(&self) -> coq::term::ParamList {
// Important: early parameters should always be first, as they include trait specs.
// Important: the type parameters should be introduced before late parameters to ensure they are in
// scope.
@@ -2652,12 +2665,12 @@ impl<'def> Display for FunctionSpec<InnerFunctionSpec<'def>> {
let mut term = String::with_capacity(100);
self.spec.write_spec_term(&mut term, &self.generics)?;
- let coq_def = coq::Definition {
+ let coq_def = coq::command::Definition {
name: self.spec_name.clone(),
params,
ty: None,
- body: coq::DefBody::Term(coq::GallinaTerm::Literal(term)),
- kind: coq::DefinitionKind::Definition,
+ body: coq::command::DefBody::Term(coq::term::Gallina::Literal(term)),
+ kind: coq::command::DefinitionKind::Definition,
};
write!(f, "{coq_def}")
}
@@ -2668,7 +2681,7 @@ impl<'def> Display for FunctionSpec<InnerFunctionSpec<'def>> {
/// A function specification below generics.
#[derive(Clone, Debug)]
pub struct LiteralFunctionSpec<'def> {
- pub params: Vec<(coq::Name, coq::Type)>,
+ pub params: Vec<(coq::term::Name, coq::term::Type)>,
/// external lifetime context
pub elctx: Vec<ExtLftConstr>,
@@ -2680,7 +2693,7 @@ pub struct LiteralFunctionSpec<'def> {
/// argument types including refinements
pub args: Vec<TypeWithRef<'def>>,
/// existential quantifiers for the postcondition
- pub existentials: Vec<(coq::Name, coq::Type)>,
+ pub existentials: Vec<(coq::term::Name, coq::term::Type)>,
/// return type
pub ret: TypeWithRef<'def>,
/// postcondition as a separating conjunction
@@ -2719,14 +2732,14 @@ impl<'def> LiteralFunctionSpec<'def> {
out
}
- fn uncurry_typed_binders<'a, F>(v: F) -> (coq::Pattern, coq::Type)
+ fn uncurry_typed_binders<'a, F>(v: F) -> (coq::term::Pattern, coq::term::Type)
where
- F: IntoIterator<Item = &'a (coq::Name, coq::Type)>,
+ F: IntoIterator<Item = &'a (coq::term::Name, coq::term::Type)>,
{
let mut v = v.into_iter().peekable();
if v.peek().is_none() {
- return ("_".to_owned(), coq::Type::Literal("unit".to_owned()));
+ return ("_".to_owned(), coq::term::Type::Literal("unit".to_owned()));
}
let mut pattern = String::with_capacity(100);
@@ -2751,7 +2764,7 @@ impl<'def> LiteralFunctionSpec<'def> {
pattern.push(')');
types.push(')');
- (pattern, coq::Type::Literal(types))
+ (pattern, coq::term::Type::Literal(types))
}
/// Write the core spec term. Assumes that the coq parameters for the type parameters (as given by
@@ -2810,12 +2823,12 @@ impl<'def> LiteralFunctionSpec<'def> {
#[derive(Debug)]
pub struct LiteralFunctionSpecBuilder<'def> {
- params: Vec<(coq::Name, coq::Type)>,
+ params: Vec<(coq::term::Name, coq::term::Type)>,
elctx: Vec<ExtLftConstr>,
pre: IProp,
late_pre: IProp,
args: Vec<TypeWithRef<'def>>,
- existential: Vec<(coq::Name, coq::Type)>,
+ existential: Vec<(coq::term::Name, coq::term::Type)>,
ret: Option<TypeWithRef<'def>>,
post: IProp,
@@ -2842,14 +2855,14 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
}
}
- fn push_coq_name(&mut self, name: &coq::Name) {
- if let coq::Name::Named(name) = &name {
+ fn push_coq_name(&mut self, name: &coq::term::Name) {
+ if let coq::term::Name::Named(name) = &name {
self.coq_names.insert(name.to_owned());
}
}
/// Adds a (universally-quantified) parameter with a given Coq name for the spec.
- pub fn add_param(&mut self, name: coq::Name, t: coq::Type) -> Result<(), String> {
+ pub fn add_param(&mut self, name: coq::term::Name, t: coq::term::Type) -> Result<(), String> {
self.ensure_coq_not_bound(&name)?;
self.push_coq_name(&name);
self.params.push((name, t));
@@ -2858,10 +2871,10 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
/// Add a Coq type annotation for a parameter when no type is currently known.
/// This can e.g. be used to later on add knowledge about the type of a refinement.
- pub fn add_param_type_annot(&mut self, name: &coq::Name, t: coq::Type) -> Result<(), String> {
+ pub fn add_param_type_annot(&mut self, name: &coq::term::Name, t: coq::term::Type) -> Result<(), String> {
for (name0, t0) in &mut self.params {
if *name0 == *name {
- if *t0 == coq::Type::Infer {
+ if *t0 == coq::term::Type::Infer {
*t0 = t;
}
return Ok(());
@@ -2878,8 +2891,8 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
Ok(())
}
- fn ensure_coq_not_bound(&self, name: &coq::Name) -> Result<(), String> {
- if let coq::Name::Named(name) = &name {
+ fn ensure_coq_not_bound(&self, name: &coq::term::Name) -> Result<(), String> {
+ if let coq::term::Name::Named(name) = &name {
if self.coq_names.contains(name) {
return Err(format!("Coq name is already bound: {}", name));
}
@@ -2953,7 +2966,7 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
}
/// Add an existentially-quantified variable to the postcondition.
- pub fn add_existential(&mut self, name: coq::Name, t: coq::Type) -> Result<(), String> {
+ pub fn add_existential(&mut self, name: coq::term::Name, t: coq::term::Type) -> Result<(), String> {
self.ensure_coq_not_bound(&name)?;
self.existential.push((name, t));
// TODO: if we add some kind of name analysis to postcondition, we need to handle the
@@ -2999,14 +3012,14 @@ pub struct TraitInstanceSpec<'def> {
#[derive(Constructor, Clone, Debug)]
pub struct TraitSpecAttrsDecl {
/// a map of attributes and their types
- pub attrs: HashMap<String, coq::Type>,
+ pub attrs: HashMap<String, coq::term::Type>,
}
/// Implementation of the attributes of a trait
#[derive(Constructor, Clone, Debug)]
pub struct TraitSpecAttrsInst {
/// a map of attributes and their implementation
- pub attrs: HashMap<String, coq::GallinaTerm>,
+ pub attrs: HashMap<String, coq::term::Gallina>,
}
/// A using occurrence of a trait spec.
@@ -3388,60 +3401,60 @@ impl GenericScope {
/// Get the Coq parameters that need to be in scope for the type parameters of this function.
#[must_use]
- fn get_coq_ty_params(&self) -> coq::ParamList {
+ fn get_coq_ty_params(&self) -> coq::term::ParamList {
let mut ty_coq_params = Vec::new();
for names in &self.tys {
- ty_coq_params.push(coq::Param::new(
- coq::Name::Named(names.refinement_type.clone()),
- coq::Type::Type,
+ ty_coq_params.push(coq::term::Param::new(
+ coq::term::Name::Named(names.refinement_type.clone()),
+ coq::term::Type::Type,
false,
));
}
for names in &self.tys {
- ty_coq_params.push(coq::Param::new(
- coq::Name::Named(names.syn_type.clone()),
- coq::Type::SynType,
+ ty_coq_params.push(coq::term::Param::new(
+ coq::term::Name::Named(names.syn_type.clone()),
+ coq::term::Type::SynType,
false,
));
}
- coq::ParamList(ty_coq_params)
+ coq::term::ParamList(ty_coq_params)
}
/// Get the Coq parameters that need to be in scope for the type parameters of this function.
#[must_use]
- pub fn get_coq_ty_st_params(&self) -> coq::ParamList {
+ pub fn get_coq_ty_st_params(&self) -> coq::term::ParamList {
let mut ty_coq_params = Vec::new();
for names in &self.tys {
ty_coq_params.push(names.make_syntype_param());
}
- coq::ParamList::new(ty_coq_params)
+ coq::term::ParamList::new(ty_coq_params)
}
/// Get the direct Coq parameters that need to be in scope for the type parameters of this function.
#[must_use]
- pub fn get_direct_coq_ty_st_params(&self) -> coq::ParamList {
+ pub fn get_direct_coq_ty_st_params(&self) -> coq::term::ParamList {
let mut ty_coq_params = Vec::new();
for names in &self.tys {
if names.origin == TyParamOrigin::Direct {
ty_coq_params.push(names.make_syntype_param());
}
}
- coq::ParamList::new(ty_coq_params)
+ coq::term::ParamList::new(ty_coq_params)
}
#[must_use]
- pub fn get_direct_coq_ty_rt_params(&self) -> coq::ParamList {
+ pub fn get_direct_coq_ty_rt_params(&self) -> coq::term::ParamList {
let mut ty_coq_params = Vec::new();
for names in &self.tys {
if names.origin == TyParamOrigin::Direct {
ty_coq_params.push(names.make_refinement_param());
}
}
- coq::ParamList::new(ty_coq_params)
+ coq::term::ParamList::new(ty_coq_params)
}
#[must_use]
- pub fn get_direct_coq_ty_params(&self) -> coq::ParamList {
+ pub fn get_direct_coq_ty_params(&self) -> coq::term::ParamList {
let mut rt_params = self.get_direct_coq_ty_rt_params();
let st_params = self.get_direct_coq_ty_st_params();
rt_params.append(st_params.0);
@@ -3473,21 +3486,24 @@ fn make_trait_instance<'def>(
is_base_spec: bool,
spec_record_name: &str,
spec_record_params_name: &str,
-) -> Result<coq::TopLevelAssertions<'def>, fmt::Error> {
+) -> Result<coq::command::TopLevelAssertions<'def>, fmt::Error> {
let mut assertions = Vec::new();
// write the param record decl
let mut def_rts_params = Vec::new();
for param in scope.tys.iter().chain(assoc_types) {
- let rt_param =
- coq::Param::new(coq::Name::Named(param.refinement_type.clone()), coq::Type::Type, false);
+ let rt_param = coq::term::Param::new(
+ coq::term::Name::Named(param.refinement_type.clone()),
+ coq::term::Type::Type,
+ false,
+ );
def_rts_params.push(rt_param);
}
- let def_rts_params = coq::ParamList::new(def_rts_params);
+ let def_rts_params = coq::term::ParamList::new(def_rts_params);
let def_rts_params_uses = def_rts_params.make_using_terms();
let param_record_term = if spec.methods.is_empty() {
- coq::GallinaTerm::Literal(of_trait.spec_record_params_constructor_name())
+ coq::term::Gallina::Literal(of_trait.spec_record_params_constructor_name())
} else {
let mut components = Vec::new();
for (item_name, spec) in &spec.methods {
@@ -3508,56 +3524,67 @@ fn make_trait_instance<'def>(
// finally pass the associated types
write_list!(body, &assoc_types, " ", |x| { format!("{}", x.refinement_type) })?;
- let item = coq::RecordBodyItem {
+ let item = coq::term::RecordBodyItem {
name: record_item_name,
params,
- term: coq::GallinaTerm::Literal(body),
+ term: coq::term::Gallina::Literal(body),
};
components.push(item);
}
- let record_body = coq::RecordBodyTerm { items: components };
- coq::GallinaTerm::RecordBody(record_body)
+ let record_body = coq::term::RecordBody { items: components };
+ coq::term::Gallina::RecordBody(record_body)
};
- let param_record_definition = coq::Definition {
+ let param_record_definition = coq::command::Definition {
name: spec_record_params_name.to_owned(),
params: def_rts_params,
- ty: Some(coq::Type::Literal(of_trait.spec_params_record.clone())),
- body: coq::DefBody::Term(param_record_term),
- kind: coq::DefinitionKind::Definition,
+ ty: Some(coq::term::Type::Literal(of_trait.spec_params_record.clone())),
+ body: coq::command::DefBody::Term(param_record_term),
+ kind: coq::command::DefinitionKind::Definition,
};
- assertions.push(coq::TopLevelAssertion::Definition(param_record_definition));
+ assertions.push(coq::command::TopLevelAssertion::Definition(param_record_definition));
// write the attr record decl, if provided
let mut attrs_type_rts = Vec::new();
for param in param_inst.iter().chain(assoc_inst) {
attrs_type_rts.push(format!("{}", param.get_rfn_type()));
}
- let attrs_type = coq::AppTerm::new(of_trait.spec_attrs_record.clone(), attrs_type_rts);
- let attrs_type = coq::Type::Literal(format!("{attrs_type}"));
+ let attrs_type = coq::term::App::new(of_trait.spec_attrs_record.clone(), attrs_type_rts);
+ let attrs_type = coq::term::Type::Literal(format!("{attrs_type}"));
// write the spec record decl
let mut def_params = Vec::new();
// all rts
for param in scope.tys.iter().chain(assoc_types) {
- let rt_param =
- coq::Param::new(coq::Name::Named(param.refinement_type.clone()), coq::Type::Type, false);
+ let rt_param = coq::term::Param::new(
+ coq::term::Name::Named(param.refinement_type.clone()),
+ coq::term::Type::Type,
+ false,
+ );
def_params.push(rt_param);
}
// all sts
for param in scope.tys.iter().chain(assoc_types) {
- let st_param = coq::Param::new(coq::Name::Named(param.syn_type.clone()), coq::Type::SynType, false);
+ let st_param = coq::term::Param::new(
+ coq::term::Name::Named(param.syn_type.clone()),
+ coq::term::Type::SynType,
+ false,
+ );
def_params.push(st_param);
}
// then, the attrs. these also get the associated types
if is_base_spec {
- def_params.push(coq::Param::new(coq::Name::Named("_ATTRS".to_owned()), attrs_type, false));
+ def_params.push(coq::term::Param::new(
+ coq::term::Name::Named("_ATTRS".to_owned()),
+ attrs_type,
+ false,
+ ));
}
- let def_params = coq::ParamList::new(def_params);
+ let def_params = coq::term::ParamList::new(def_params);
// for this, we assume that the semantic type parameters are all in scope
let body_term = if spec.methods.is_empty() {
// special-case this, as we cannot use record constructor syntax for empty records
- coq::GallinaTerm::Literal(format!("@{} _", of_trait.spec_record_constructor_name()))
+ coq::term::Gallina::Literal(format!("@{} _", of_trait.spec_record_constructor_name()))
} else {
let mut components = Vec::new();
for (item_name, spec) in &spec.methods {
@@ -3611,15 +3638,15 @@ fn make_trait_instance<'def>(
)?;
write!(body, "→ _))")?;
- let item = coq::RecordBodyItem {
+ let item = coq::term::RecordBodyItem {
name: record_item_name,
params: direct_params,
- term: coq::GallinaTerm::Literal(body),
+ term: coq::term::Gallina::Literal(body),
};
components.push(item);
}
- let record_body = coq::RecordBodyTerm { items: components };
- coq::GallinaTerm::RecordBody(record_body)
+ let record_body = coq::term::RecordBody { items: components };
+ coq::term::Gallina::RecordBody(record_body)
};
// add the surrounding quantifiers over the semantic types
// TODO
@@ -3632,16 +3659,16 @@ fn make_trait_instance<'def>(
write_list!(ty_annot, &def_rts_params_uses, " ")?;
write!(ty_annot, "))")?;
- let definition = coq::Definition {
+ let definition = coq::command::Definition {
name: spec_record_name.to_owned(),
params: def_params,
- ty: Some(coq::Type::Literal(ty_annot)),
- body: coq::DefBody::Term(coq::GallinaTerm::Literal(term_with_specs)),
- kind: coq::DefinitionKind::Definition,
+ ty: Some(coq::term::Type::Literal(ty_annot)),
+ body: coq::command::DefBody::Term(coq::term::Gallina::Literal(term_with_specs)),
+ kind: coq::command::DefinitionKind::Definition,
};
- assertions.push(coq::TopLevelAssertion::Definition(definition));
+ assertions.push(coq::command::TopLevelAssertion::Definition(definition));
- Ok(coq::TopLevelAssertions(assertions))
+ Ok(coq::command::TopLevelAssertions(assertions))
}
/// When translating a trait declaration, we should generate this, bundling all the components of
@@ -3652,7 +3679,7 @@ pub struct TraitSpecDecl<'def> {
pub lit: LiteralTraitSpecRef<'def>,
/// a list of extra things we assume in the Coq context
- pub extra_coq_context: coq::ParamList,
+ pub extra_coq_context: coq::term::ParamList,
/// The generics this trait uses
pub generics: GenericScope,
@@ -3684,17 +3711,17 @@ impl<'def> Display for TraitSpecDecl<'def> {
// params are the rt of the direct type parameters
let params = item_spec.generics.get_direct_coq_ty_rt_params();
- let item = coq::RecordDeclItem {
+ let item = coq::term::RecordDeclItem {
name: record_item_name,
params,
- ty: coq::Type::Type,
+ ty: coq::term::Type::Type,
};
record_items.push(item);
}
- let spec_param_record = coq::Record {
+ let spec_param_record = coq::term::Record {
name: self.lit.spec_params_record.clone(),
- params: coq::ParamList::empty(),
- ty: coq::Type::Type,
+ params: coq::term::ParamList::empty(),
+ ty: coq::term::Type::Type,
constructor: Some(spec_param_record_constructor),
body: record_items,
};
@@ -3705,9 +3732,9 @@ impl<'def> Display for TraitSpecDecl<'def> {
for (item_name, item_ty) in &self.attrs.attrs {
let record_item_name = self.lit.make_spec_attr_name(item_name);
- let item = coq::RecordDeclItem {
+ let item = coq::term::RecordDeclItem {
name: record_item_name,
- params: coq::ParamList::empty(),
+ params: coq::term::ParamList::empty(),
ty: item_ty.to_owned(),
};
record_items.push(item);
@@ -3715,16 +3742,16 @@ impl<'def> Display for TraitSpecDecl<'def> {
// this is parametric in the params and associated types
let mut attr_params = Vec::new();
for param in self.generics.get_ty_params().iter().chain(self.assoc_types.iter()) {
- attr_params.push(coq::Param::new(
- coq::Name::Named(param.refinement_type.clone()),
- coq::Type::Type,
+ attr_params.push(coq::term::Param::new(
+ coq::term::Name::Named(param.refinement_type.clone()),
+ coq::term::Type::Type,
true,
));
}
- let spec_attr_record = coq::Record {
+ let spec_attr_record = coq::term::Record {
name: self.lit.spec_attrs_record.clone(),
- params: coq::ParamList::new(attr_params),
- ty: coq::Type::Type,
+ params: coq::term::ParamList::new(attr_params),
+ ty: coq::term::Type::Type,
constructor: Some(spec_attrs_record_constructor.clone()),
body: record_items,
};
@@ -3757,22 +3784,22 @@ impl<'def> Display for TraitSpecDecl<'def> {
write_list!(ty_term, &rt_param_uses, " ")?;
write!(ty_term, " → fn_params)")?;
- let item = coq::RecordDeclItem {
+ let item = coq::term::RecordDeclItem {
name: record_item_name,
params,
- ty: coq::Type::Literal(ty_term),
+ ty: coq::term::Type::Literal(ty_term),
};
record_items.push(item);
}
- let spec_params = vec![coq::Param::new(
- coq::Name::Named("_P".to_owned()),
- coq::Type::Literal(self.lit.spec_params_record.clone()),
+ let spec_params = vec![coq::term::Param::new(
+ coq::term::Name::Named("_P".to_owned()),
+ coq::term::Type::Literal(self.lit.spec_params_record.clone()),
true,
)];
- let spec_record = coq::Record {
+ let spec_record = coq::term::Record {
name: self.lit.spec_record.clone(),
- params: coq::ParamList::new(spec_params),
- ty: coq::Type::Type,
+ params: coq::term::ParamList::new(spec_params),
+ ty: coq::term::Type::Type,
constructor: Some(spec_record_constructor),
body: record_items,
};
@@ -3789,25 +3816,25 @@ impl<'def> Display for TraitSpecDecl<'def> {
let spec_param_type2 = format!("{} _P2", self.lit.spec_record);
let spec_incl_params = vec![
// the two spec params
- coq::Param::new(
- coq::Name::Named("_P1".to_owned()),
- coq::Type::Literal(self.lit.spec_params_record.clone()),
+ coq::term::Param::new(
+ coq::term::Name::Named("_P1".to_owned()),
+ coq::term::Type::Literal(self.lit.spec_params_record.clone()),
true,
),
- coq::Param::new(
- coq::Name::Named("_P2".to_owned()),
- coq::Type::Literal(self.lit.spec_params_record.clone()),
+ coq::term::Param::new(
+ coq::term::Name::Named("_P2".to_owned()),
+ coq::term::Type::Literal(self.lit.spec_params_record.clone()),
true,
),
// the two actual specs
- coq::Param::new(
- coq::Name::Named(spec_param_name1.clone()),
- coq::Type::Literal(spec_param_type1),
+ coq::term::Param::new(
+ coq::term::Name::Named(spec_param_name1.clone()),
+ coq::term::Type::Literal(spec_param_type1),
false,
),
- coq::Param::new(
- coq::Name::Named(spec_param_name2.clone()),
- coq::Type::Literal(spec_param_type2),
+ coq::term::Param::new(
+ coq::term::Name::Named(spec_param_name2.clone()),
+ coq::term::Type::Literal(spec_param_type2),
false,
),
];
@@ -3815,21 +3842,21 @@ impl<'def> Display for TraitSpecDecl<'def> {
for (name, decl) in &self.default_spec.methods {
let param_uses = decl.generics.get_direct_coq_ty_params().make_using_terms();
let record_item_name = self.lit.make_spec_method_name(name);
- let incl_term = coq::GallinaTerm::All(
+ let incl_term = coq::term::Gallina::All(
decl.generics.get_direct_coq_ty_params(),
- Box::new(coq::GallinaTerm::App(Box::new(coq::AppTerm::new(
- coq::GallinaTerm::Literal("function_subtype".to_owned()),
+ Box::new(coq::term::Gallina::App(Box::new(coq::term::App::new(
+ coq::term::Gallina::Literal("function_subtype".to_owned()),
vec![
- coq::GallinaTerm::App(Box::new(coq::AppTerm::new(
- coq::GallinaTerm::RecordProj(
- Box::new(coq::GallinaTerm::Literal(spec_param_name1.clone())),
+ coq::term::Gallina::App(Box::new(coq::term::App::new(
+ coq::term::Gallina::RecordProj(
+ Box::new(coq::term::Gallina::Literal(spec_param_name1.clone())),
record_item_name.clone(),
),
param_uses.clone(),
))),
- coq::GallinaTerm::App(Box::new(coq::AppTerm::new(
- coq::GallinaTerm::RecordProj(
- Box::new(coq::GallinaTerm::Literal(spec_param_name2.clone())),
+ coq::term::Gallina::App(Box::new(coq::term::App::new(
+ coq::term::Gallina::RecordProj(
+ Box::new(coq::term::Gallina::Literal(spec_param_name2.clone())),
record_item_name.clone(),
),
param_uses.clone(),
@@ -3839,14 +3866,14 @@ impl<'def> Display for TraitSpecDecl<'def> {
);
incls.push(incl_term);
}
- let body = coq::GallinaTerm::Infix("∧".to_owned(), incls);
+ let body = coq::term::Gallina::Infix("∧".to_owned(), incls);
- let spec_incl_def = coq::Definition {
+ let spec_incl_def = coq::command::Definition {
name: spec_incl_name,
- params: coq::ParamList::new(spec_incl_params),
- ty: Some(coq::Type::Prop),
- body: coq::DefBody::Term(body),
- kind: coq::DefinitionKind::Definition,
+ params: coq::term::ParamList::new(spec_incl_params),
+ ty: Some(coq::term::Type::Prop),
+ body: coq::command::DefBody::Term(body),
+ kind: coq::command::DefinitionKind::Definition,
};
write!(f, "{spec_incl_def}\n")?;
@@ -3935,7 +3962,7 @@ pub struct TraitImplSpec<'def> {
impl<'def> TraitImplSpec<'def> {
/// Generate the definition of the attribute record of this trait impl.
#[must_use]
- pub fn generate_attr_decl(&self) -> coq::TopLevelAssertion {
+ pub fn generate_attr_decl(&self) -> coq::command::TopLevelAssertion {
let attrs = &self.trait_ref.attrs;
let attrs_name = &self.names.spec_attrs_record;
let param_inst = &self.trait_ref.params_inst;
@@ -3944,11 +3971,14 @@ impl<'def> TraitImplSpec<'def> {
let mut def_rts_params = Vec::new();
for param in &self.trait_ref.generics.tys {
- let rt_param =
- coq::Param::new(coq::Name::Named(param.refinement_type.clone()), coq::Type::Type, false);
+ let rt_param = coq::term::Param::new(
+ coq::term::Name::Named(param.refinement_type.clone()),
+ coq::term::Type::Type,
+ false,
+ );
def_rts_params.push(rt_param);
}
- let def_rts_params = coq::ParamList::new(def_rts_params);
+ let def_rts_params = coq::term::ParamList::new(def_rts_params);
let def_rts_params_uses = def_rts_params.make_using_terms();
// write the attr record decl
@@ -3956,33 +3986,33 @@ impl<'def> TraitImplSpec<'def> {
for param in param_inst.iter().chain(assoc_inst) {
attrs_type_rts.push(format!("{}", param.get_rfn_type()));
}
- let attrs_type = coq::AppTerm::new(of_trait.spec_attrs_record.clone(), attrs_type_rts);
- let attrs_type = coq::Type::Literal(format!("{attrs_type}"));
+ let attrs_type = coq::term::App::new(of_trait.spec_attrs_record.clone(), attrs_type_rts);
+ let attrs_type = coq::term::Type::Literal(format!("{attrs_type}"));
let attr_record_term = if attrs.attrs.is_empty() {
- coq::GallinaTerm::Literal(of_trait.spec_record_attrs_constructor_name())
+ coq::term::Gallina::Literal(of_trait.spec_record_attrs_constructor_name())
} else {
let mut components = Vec::new();
for (attr_name, inst) in &attrs.attrs {
let record_item_name = of_trait.make_spec_attr_name(attr_name);
- let item = coq::RecordBodyItem {
+ let item = coq::term::RecordBodyItem {
name: record_item_name,
- params: coq::ParamList::empty(),
+ params: coq::term::ParamList::empty(),
term: inst.to_owned(),
};
components.push(item);
}
- let record_body = coq::RecordBodyTerm { items: components };
- coq::GallinaTerm::RecordBody(record_body)
+ let record_body = coq::term::RecordBody { items: components };
+ coq::term::Gallina::RecordBody(record_body)
};
- let attr_record_definition = coq::Definition {
+ let attr_record_definition = coq::command::Definition {
name: attrs_name.to_owned(),
params: def_rts_params,
ty: Some(attrs_type),
- body: coq::DefBody::Term(attr_record_term),
- kind: coq::DefinitionKind::Definition,
+ body: coq::command::DefBody::Term(attr_record_term),
+ kind: coq::command::DefinitionKind::Definition,
};
- coq::TopLevelAssertion::Definition(attr_record_definition)
+ coq::command::TopLevelAssertion::Definition(attr_record_definition)
}
/*
fn generate_proof(&self) -> coq::TopLevelAssertion {
@@ -4016,10 +4046,14 @@ impl<'def> TraitImplSpec<'def> {
impl<'def> Display for TraitImplSpec<'def> {
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
// This relies on all the impl's functions already having been printed
- write!(f, "{}\n", coq::TopLevelAssertion::SectionStart(self.names.spec_record.clone()))?;
+ write!(f, "{}\n", coq::command::TopLevelAssertion::SectionStart(self.names.spec_record.clone()))?;
{
let mut f = IndentWriter::new(BASE_INDENT, &mut *f);
- write!(f, "{}\n", coq::TopLevelAssertion::ContextDecl(coq::ContextDecl::refinedrust()))?;
+ write!(
+ f,
+ "{}\n",
+ coq::command::TopLevelAssertion::ContextDecl(coq::command::ContextDecl::refinedrust())
+ )?;
// write the bundled records
let base_decls = make_trait_instance(
@@ -4036,7 +4070,7 @@ impl<'def> Display for TraitImplSpec<'def> {
write!(f, "{base_decls}\n")?;
}
- write!(f, "{}\n", coq::TopLevelAssertion::SectionEnd(self.names.spec_record.clone()))
+ write!(f, "{}\n", coq::command::TopLevelAssertion::SectionEnd(self.names.spec_record.clone()))
}
}
@@ -4083,7 +4117,7 @@ impl<'def> InstantiatedTraitFunctionSpec<'def> {
params.push(self.trait_attr_term.clone());
let mut applied_base_spec = String::with_capacity(100);
- write!(applied_base_spec, "{}", coq::AppTerm::new(&self.trait_ref.of_trait.base_spec, params))?;
+ write!(applied_base_spec, "{}", coq::term::App::new(&self.trait_ref.of_trait.base_spec, params))?;
// instantiate semantic types
for ty in &self.trait_ref.params_inst {
write!(applied_base_spec, " <TY> {ty}")?;
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index 58813df..38a7d6a 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -1161,13 +1161,11 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
for ty in &assoc_tys {
param_ty_args.push(format!("{}", ty.get_rfn_type()));
}
- let param_ty = format!(
- "{}",
- radium::coq::AppTerm::new(trait_ref.spec_attrs_record.clone(), param_ty_args)
- );
- let param = radium::coq::Param::new(
- radium::coq::Name::Named(param_name.clone()),
- radium::coq::Type::Literal(param_ty),
+ let param_ty =
+ format!("{}", coq::term::App::new(trait_ref.spec_attrs_record.clone(), param_ty_args));
+ let param = coq::term::Param::new(
+ coq::term::Name::Named(param_name.clone()),
+ coq::term::Type::Literal(param_ty),
false,
);
@@ -1196,7 +1194,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
for ty in impl_ref.get_trait_param_inst().iter().chain(impl_ref.get_trait_assoc_inst()) {
param_ty_args.push(format!("{}", ty.get_rfn_type()));
}
- let param_ty = format!("{}", radium::coq::AppTerm::new(trait_ref.spec_attrs_record.clone(), param_ty_args));
+ let param_ty = format!("{}", radium::coq::App::new(trait_ref.spec_attrs_record.clone(), param_ty_args));
let param = radium::coq::Param::new(radium::coq::Name::Named(param_name.clone()), radium::coq::Type::Literal(param_ty), false);
// add it as parameter to the function after the generics
@@ -2127,13 +2125,13 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// get the refinement type
let mut rfn_ty = ty.get_rfn_type();
// wrap it in place_rfn, since we reason about places
- rfn_ty = coq::Type::PlaceRfn(Box::new(rfn_ty));
+ rfn_ty = coq::term::Type::PlaceRfn(Box::new(rfn_ty));
// determine their initialization status
//let initialized = true; // TODO
// determine the actual refinement type for the current initialization status.
- let rfn_name = coq::Name::Named(format!("r_{}", name));
+ let rfn_name = coq::term::Name::Named(format!("r_{}", name));
rfn_binders.push(radium::specs::CoqBinder::new(rfn_name, rfn_ty));
}
@@ -3798,7 +3796,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
translated_ops.into_iter().enumerate().map(|(i, o)| (i.to_string(), o)).collect();
Ok(radium::Expr::StructInitE {
- sls: coq::AppTerm::new_lhs(sl.to_string()),
+ sls: coq::term::App::new_lhs(sl.to_string()),
components: initializers,
})
},
@@ -3824,7 +3822,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
.collect();
return Ok(radium::Expr::StructInitE {
- sls: coq::AppTerm::new_lhs(sl.to_string()),
+ sls: coq::term::App::new_lhs(sl.to_string()),
components: initializers,
});
}
@@ -3843,7 +3841,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
.collect();
let variant_e = radium::Expr::StructInitE {
- sls: coq::AppTerm::new_lhs(sl.to_string()),
+ sls: coq::term::App::new_lhs(sl.to_string()),
components: initializers,
};
@@ -3855,7 +3853,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let variant_name = variant_def.name.to_string();
return Ok(radium::Expr::EnumInitE {
- els: coq::AppTerm::new_lhs(els.to_string()),
+ els: coq::term::App::new_lhs(els.to_string()),
variant: variant_name,
ty,
initializer: Box::new(variant_e),
@@ -3887,7 +3885,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
translated_ops.into_iter().enumerate().map(|(i, o)| (i.to_string(), o)).collect();
Ok(radium::Expr::StructInitE {
- sls: coq::AppTerm::new_lhs(sl.to_string()),
+ sls: coq::term::App::new_lhs(sl.to_string()),
components: initializers,
})
},
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 23d7ff6..440a47c 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -997,7 +997,7 @@ fn register_shims<'tcx>(vcx: &mut VerificationCtxt<'tcx, '_>) -> Result<(), base
rust_name: None,
type_term: shim.sem_type.clone(),
syn_type: radium::SynType::Literal(shim.syn_type.clone()),
- refinement_type: coq::Type::Literal(shim.refinement_type.clone()),
+ refinement_type: coq::term::Type::Literal(shim.refinement_type.clone()),
};
if let Err(e) = vcx.type_translator.register_adt_shim(did, &lit) {
diff --git a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
index 0e1ff2e..fb6dcf4 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -5,7 +5,7 @@
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
use attribute_parse::parse;
-use radium::{coq, specs};
+use radium::coq;
use rr_rustc_interface::ast::ast::AttrItem;
use crate::spec_parsers::parse_utils::{self, str_err};
@@ -23,7 +23,7 @@ pub struct CrateAttrs {
pub prefix: Option<String>,
pub includes: Vec<String>,
pub package: Option<String>,
- pub context_params: Vec<coq::Param>,
+ pub context_params: Vec<coq::term::Param>,
}
#[allow(clippy::module_name_repetitions)]
@@ -77,9 +77,9 @@ impl CrateAttrParser for VerboseCrateAttrParser {
},
"context" => {
let param: parse_utils::RRGlobalCoqContextItem = buffer.parse(&()).map_err(str_err)?;
- context_params.push(coq::Param::new(
- coq::Name::Unnamed,
- coq::Type::Literal(param.item),
+ context_params.push(coq::term::Param::new(
+ coq::term::Name::Unnamed,
+ coq::term::Type::Literal(param.item),
true,
));
},
diff --git a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
index 7a8eee1..e64f1ae 100644
--- a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
@@ -7,7 +7,7 @@
use std::collections::HashMap;
use attribute_parse::{parse, MToken};
-use parse::{Parse, Peek};
+use parse::Peek;
use radium::{coq, specs};
use rr_rustc_interface::ast::ast::{AttrArgs, AttrItem};
@@ -101,7 +101,7 @@ impl<'b, T: ParamLookup> EnumSpecParser for VerboseEnumSpecParser<'b, T> {
"refined_by" => {
let ty: parse::LitStr = buffer.parse(self.scope).map_err(str_err)?;
let (ty, _) = process_coq_literal(ty.value().as_str(), self.scope);
- rfn_type = Some(coq::Type::Literal(ty));
+ rfn_type = Some(coq::term::Type::Literal(ty));
},
"export_as" => {},
_ => {
diff --git a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
index 0850c50..ce6aae8 100644
--- a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
@@ -5,7 +5,7 @@
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
use attribute_parse::parse;
-use radium::{coq, specs};
+use radium::coq;
use rr_rustc_interface::ast::ast::AttrItem;
use rr_rustc_interface::hir::def_id::LocalDefId;
@@ -26,7 +26,7 @@ pub trait ModuleAttrParser {
pub struct ModuleAttrs {
pub exports: Vec<coq::module::Export>,
pub includes: Vec<String>,
- pub context_params: Vec<coq::Param>,
+ pub context_params: Vec<coq::term::Param>,
}
#[allow(clippy::module_name_repetitions)]
@@ -68,9 +68,9 @@ impl ModuleAttrParser for VerboseModuleAttrParser {
},
"context" => {
let param: parse_utils::RRGlobalCoqContextItem = buffer.parse(&()).map_err(str_err)?;
- context_params.push(coq::Param::new(
- coq::Name::Unnamed,
- coq::Type::Literal(param.item),
+ context_params.push(coq::term::Param::new(
+ coq::term::Name::Unnamed,
+ coq::term::Type::Literal(param.item),
true,
));
},
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 69a15fb..aca62c3 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -4,13 +4,13 @@
// 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/.
+/// This provides some general utilities for RefinedRust-specific attribute parsing.
use std::collections::{HashMap, HashSet};
use attribute_parse::{parse, MToken};
use lazy_static::lazy_static;
use log::info;
use parse::{Parse, Peek};
-/// This provides some general utilities for RefinedRust-specific attribute parsing.
use radium::{coq, specs};
use regex::{self, Captures, Regex};
@@ -132,13 +132,13 @@ impl<T: ParamLookup> parse::Parse<T> for IProp {
/// Parse a Coq type.
pub struct RRCoqType {
- pub ty: coq::Type,
+ pub ty: coq::term::Type,
}
impl<T: ParamLookup> parse::Parse<T> for RRCoqType {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
let ty: parse::LitStr = input.parse(meta)?;
let (ty, _) = process_coq_literal(&ty.value(), meta);
- let ty = coq::Type::Literal(ty);
+ let ty = coq::term::Type::Literal(ty);
Ok(Self { ty })
}
}
@@ -150,14 +150,14 @@ impl<T: ParamLookup> parse::Parse<T> for RRCoqType {
/// `w : "(Z * Z)%type"`
#[derive(Debug)]
pub struct RRParam {
- pub name: coq::Name,
- pub ty: coq::Type,
+ pub name: coq::term::Name,
+ pub ty: coq::term::Type,
}
impl<T: ParamLookup> parse::Parse<T> for RRParam {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
let name: IdentOrTerm = input.parse(meta)?;
- let name = coq::Name::Named(name.to_string());
+ let name = coq::term::Name::Named(name.to_string());
if parse::Colon::peek(input) {
input.parse::<_, MToken![:]>(meta)?;
@@ -166,7 +166,7 @@ impl<T: ParamLookup> parse::Parse<T> for RRParam {
} else {
Ok(Self {
name,
- ty: coq::Type::Infer,
+ ty: coq::term::Type::Infer,
})
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
index c1827ea..f662a3f 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -38,8 +38,8 @@ pub trait InvariantSpecParser {
/// Parse a binder pattern with an optional Coq type annotation, e.g.
/// `"(x, y)" : "(Z * Z)%type"`
struct RfnPattern {
- rfn_pat: coq::Pattern,
- rfn_type: Option<coq::Type>,
+ rfn_pat: coq::term::Pattern,
+ rfn_type: Option<coq::term::Type>,
}
impl<T: ParamLookup> parse::Parse<T> for RfnPattern {
@@ -54,7 +54,7 @@ impl<T: ParamLookup> parse::Parse<T> for RfnPattern {
let (ty, _) = process_coq_literal(ty.value().as_str(), meta);
Ok(Self {
rfn_pat: pat,
- rfn_type: Some(coq::Type::Literal(ty)),
+ rfn_type: Some(coq::term::Type::Literal(ty)),
})
} else {
Ok(Self {
@@ -196,14 +196,14 @@ impl<'b, T: ParamLookup> InvariantSpecParser for VerboseInvariantSpecParser<'b,
let mut abstracted_refinement = None;
let mut rfn_pat = "placeholder_pat".to_owned();
- let mut rfn_type = coq::Type::Infer;
+ let mut rfn_type = coq::term::Type::Infer;
let mut existentials: Vec<RRParam> = Vec::new();
// use Plain as the default
let mut inv_flags = specs::InvariantSpecFlags::Plain;
- let mut params: Vec<coq::Param> = Vec::new();
+ let mut params: Vec<coq::term::Param> = Vec::new();
for &it in attrs {
let path_segs = &it.path.segments;
@@ -270,7 +270,11 @@ impl<'b, T: ParamLookup> InvariantSpecParser for VerboseInvariantSpecParser<'b,
"context" => {
let param = RRCoqContextItem::parse(&buffer, self.scope).map_err(str_err)?;
- params.push(coq::Param::new(coq::Name::Unnamed, coq::Type::Literal(param.item), true));
+ params.push(coq::term::Param::new(
+ coq::term::Name::Unnamed,
+ coq::term::Type::Literal(param.item),
+ true,
+ ));
},
_ => {
//skip, this may be part of an enum spec
@@ -334,7 +338,7 @@ where
make_literal: F,
//ty_scope: &'a [Option<specs::Type<'def>>],
- //rfnty_scope: &'a [Option<coq::Type>],
+ //rfnty_scope: &'a [Option<coq::term::Type>],
}
impl<'a, 'def, T: ParamLookup, F> VerboseStructFieldSpecParser<'a, 'def, T, F>
@@ -367,7 +371,7 @@ where
let lit_ty = specs::LiteralType {
rust_name: None,
type_term: lit.ty.clone(),
- refinement_type: coq::Type::Infer,
+ refinement_type: coq::term::Type::Infer,
syn_type: ty.into(),
};
let lit_ref = (self.make_literal)(lit_ty);
diff --git a/rr_frontend/translation/src/spec_parsers/trait_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/trait_attr_parser.rs
index 33f0c73..8850176 100644
--- a/rr_frontend/translation/src/spec_parsers/trait_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/trait_attr_parser.rs
@@ -8,6 +8,7 @@ use std::collections::HashMap;
use attribute_parse::{parse, MToken};
use derive_more::Constructor;
+use radium::coq;
use rr_rustc_interface::ast::ast::AttrItem;
use rr_rustc_interface::hir::def_id::LocalDefId;
@@ -48,7 +49,7 @@ impl<'a, T: ParamLookup> ParamLookup for TraitAttrScope<'a, T> {
#[derive(Clone, Debug)]
pub struct TraitAttrs {
pub attrs: radium::TraitSpecAttrsDecl,
- pub context_items: Vec<radium::coq::Param>,
+ pub context_items: Vec<coq::term::Param>,
}
#[allow(clippy::module_name_repetitions)]
@@ -107,9 +108,9 @@ where
},
"context" => {
let context_item: RRCoqContextItem = buffer.parse(&self.scope).map_err(str_err)?;
- let param = radium::coq::Param::new(
- radium::coq::Name::Unnamed,
- radium::coq::Type::Literal(context_item.item),
+ let param = coq::term::Param::new(
+ coq::term::Name::Unnamed,
+ coq::term::Type::Literal(context_item.item),
true,
);
context_items.push(param);
diff --git a/rr_frontend/translation/src/spec_parsers/trait_impl_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/trait_impl_attr_parser.rs
index 5dfe604..35ad963 100644
--- a/rr_frontend/translation/src/spec_parsers/trait_impl_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/trait_impl_attr_parser.rs
@@ -58,7 +58,7 @@ impl<'b, T: ParamLookup> TraitImplAttrParser for VerboseTraitImplAttrParser<'b,
let parsed_term: parse::LitStr = buffer.parse(self.scope).map_err(str_err)?;
let (parsed_term, _) = process_coq_literal(&parsed_term.value(), self.scope);
if trait_attrs
- .insert(parsed_name.to_string(), radium::coq::GallinaTerm::Literal(parsed_term))
+ .insert(parsed_name.to_string(), radium::coq::term::Gallina::Literal(parsed_term))
.is_some()
{
return Err(format!(
diff --git a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
index cdd7cad..94c71b1 100644
--- a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
@@ -245,9 +245,9 @@ pub struct VerboseFunctionSpecParser<'a, 'def, F, T> {
#[derive(Default)]
pub struct FunctionRequirements {
/// additional late coq parameters
- pub late_coq_params: Vec<coq::Param>,
+ pub late_coq_params: Vec<coq::term::Param>,
/// additional early coq parameters
- pub early_coq_params: Vec<coq::Param>,
+ pub early_coq_params: Vec<coq::term::Param>,
/// proof information
pub proof_info: ProofInfo,
}
@@ -296,7 +296,7 @@ where
&mut self,
lit: &LiteralTypeWithRef,
ty: &specs::Type<'def>,
- ) -> (specs::TypeWithRef<'def>, Option<coq::Type>) {
+ ) -> (specs::TypeWithRef<'def>, Option<coq::term::Type>) {
if let Some(lit_ty) = &lit.ty {
// literal type given, we use this literal type as the RR semantic type
// TODO: get CoqType for refinement. maybe have it as an annotation? the Infer is currently a
@@ -305,7 +305,7 @@ where
let lit_ty = specs::LiteralType {
rust_name: None,
type_term: lit_ty.to_string(),
- refinement_type: coq::Type::Infer,
+ refinement_type: coq::term::Type::Infer,
syn_type: ty.into(),
};
let lit_ref = (self.make_literal)(lit_ty);
@@ -364,7 +364,7 @@ where
// potentially add a typing hint to the refinement
if let IdentOrTerm::Ident(i) = arg.rfn {
info!("Trying to add a typing hint for {}", i);
- builder.add_param_type_annot(&coq::Name::Named(i.clone()), cty)?;
+ builder.add_param_type_annot(&coq::term::Name::Named(i.clone()), cty)?;
}
}
}
@@ -413,7 +413,11 @@ where
},
"context" => {
let context_item = RRCoqContextItem::parse(buffer, scope).map_err(str_err)?;
- let param = coq::Param::new(coq::Name::Unnamed, coq::Type::Literal(context_item.item), true);
+ let param = coq::term::Param::new(
+ coq::term::Name::Unnamed,
+ coq::term::Type::Literal(context_item.item),
+ true,
+ );
if context_item.at_end {
self.fn_requirements.late_coq_params.push(param);
} else {
@@ -534,7 +538,7 @@ where
// push everything to the builder
for x in new_ghost_vars {
- builder.add_param(coq::Name::Named(x), coq::Type::Gname).unwrap();
+ builder.add_param(coq::term::Name::Named(x), coq::term::Type::Gname).unwrap();
}
// assemble a string for the closure arg
@@ -582,7 +586,9 @@ where
ty::ClosureKind::FnMut => {
// wrap the argument in a mutable reference
let post_name = "__γclos";
- builder.add_param(coq::Name::Named(post_name.to_owned()), coq::Type::Gname).unwrap();
+ builder
+ .add_param(coq::term::Name::Named(post_name.to_owned()), coq::term::Type::Gname)
+ .unwrap();
let lft = meta.closure_lifetime.unwrap();
let ref_ty = specs::Type::MutRef(Box::new(tuple), lft);
diff --git a/rr_frontend/translation/src/trait_registry.rs b/rr_frontend/translation/src/trait_registry.rs
index fc1fcca..34b8726 100644
--- a/rr_frontend/translation/src/trait_registry.rs
+++ b/rr_frontend/translation/src/trait_registry.rs
@@ -327,7 +327,7 @@ impl<'tcx, 'def> TraitRegistry<'tcx, 'def> {
let base_instance_spec = radium::TraitInstanceSpec::new(methods);
let decl = radium::TraitSpecDecl::new(
lit_trait_spec_ref,
- radium::coq::ParamList::new(trait_spec.context_items),
+ coq::term::ParamList::new(trait_spec.context_items),
param_scope.into(),
assoc_types,
base_instance_spec,
@@ -466,8 +466,7 @@ impl<'tcx, 'def> TraitRegistry<'tcx, 'def> {
for ty in &all_impl_args {
args.push(format!("{}", ty.get_rfn_type()));
}
- let attr_term =
- format!("{}", radium::coq::AppTerm::new(impl_spec.spec_attrs_record.clone(), args));
+ let attr_term = format!("{}", coq::term::App::new(impl_spec.spec_attrs_record.clone(), args));
radium::SpecializedTraitSpec::new_with_params(
impl_spec.spec_record.clone(),
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 9183874..2cd27b8 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -1549,7 +1549,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
/// Get the spec for a built-in enum like `std::option::Option`.
fn get_builtin_enum_spec(&self, did: DefId) -> Option<radium::EnumSpec> {
let option_spec = radium::EnumSpec {
- rfn_type: coq::Type::Literal("_".to_owned()),
+ rfn_type: coq::term::Type::Literal("_".to_owned()),
variant_patterns: vec![
("None".to_owned(), vec![], "-[]".to_owned()),
("Some".to_owned(), vec!["x".to_owned()], "-[x]".to_owned()),
@@ -1557,7 +1557,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
};
let enum_spec = radium::EnumSpec {
- rfn_type: coq::Type::Literal("_".to_owned()),
+ rfn_type: coq::term::Type::Literal("_".to_owned()),
variant_patterns: vec![
("inl".to_owned(), vec!["x".to_owned()], "-[x]".to_owned()),
("inr".to_owned(), vec!["x".to_owned()], "-[x]".to_owned()),
@@ -1586,10 +1586,10 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
&self,
def: ty::AdtDef<'tcx>,
inductive_name: String,
- ) -> (coq::Inductive, radium::EnumSpec) {
+ ) -> (coq::term::Inductive, radium::EnumSpec) {
trace!("Generating Inductive for enum {:?}", def);
- let mut variants: Vec<coq::Variant> = Vec::new();
+ let mut variants: Vec<coq::term::Variant> = Vec::new();
let mut variant_patterns = Vec::new();
for v in def.variants() {
@@ -1602,22 +1602,25 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let (variant_args, variant_arg_binders, variant_rfn) = if variant_def.fields.is_empty() {
(vec![], vec![], "-[]".to_owned())
} else {
- let args =
- vec![coq::Param::new(coq::Name::Unnamed, coq::Type::Literal(refinement_type), false)];
+ let args = vec![coq::term::Param::new(
+ coq::term::Name::Unnamed,
+ coq::term::Type::Literal(refinement_type),
+ false,
+ )];
(args, vec!["x".to_owned()], "x".to_owned())
};
- variants.push(coq::Variant::new(variant_name, variant_args));
+ variants.push(coq::term::Variant::new(variant_name, variant_args));
variant_patterns.push((variant_name.to_string(), variant_arg_binders, variant_rfn));
}
// We assume the generated Inductive def is placed in a context where the generic types are in scope.
- let inductive = coq::Inductive::new(&inductive_name, vec![], variants);
+ let inductive = coq::term::Inductive::new(&inductive_name, vec![], variants);
let enum_spec = radium::EnumSpec {
- rfn_type: coq::Type::Literal(inductive_name),
+ rfn_type: coq::term::Type::Literal(inductive_name),
variant_patterns,
};
--
GitLab