From b7125100c1396c00ab6f67146f846b51f0f1280c Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Fri, 1 Nov 2024 02:20:25 +0100
Subject: [PATCH] feat(coq::radium): Add binders
---
rr_frontend/radium/src/code.rs | 30 ++--
rr_frontend/radium/src/coq/binder.rs | 142 +++++++++++++++
rr_frontend/radium/src/coq/command.rs | 17 +-
rr_frontend/radium/src/coq/inductive.rs | 8 +-
rr_frontend/radium/src/coq/mod.rs | 1 +
rr_frontend/radium/src/coq/term.rs | 136 ++-------------
rr_frontend/radium/src/coq/typeclasses.rs | 2 +-
rr_frontend/radium/src/specs.rs | 164 +++++++++---------
rr_frontend/translation/src/function_body.rs | 4 +-
.../src/spec_parsers/crate_attr_parser.rs | 10 +-
.../src/spec_parsers/module_attr_parser.rs | 10 +-
.../src/spec_parsers/parse_utils.rs | 8 +-
.../src/spec_parsers/struct_spec_parser.rs | 14 +-
.../src/spec_parsers/trait_attr_parser.rs | 9 +-
.../verbose_function_spec_parser.rs | 15 +-
rr_frontend/translation/src/trait_registry.rs | 2 +-
.../translation/src/type_translator.rs | 9 +-
17 files changed, 316 insertions(+), 265 deletions(-)
create mode 100644 rr_frontend/radium/src/coq/binder.rs
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index e0f4316..6d62514 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -651,7 +651,7 @@ pub struct FunctionCode {
basic_blocks: BTreeMap<usize, Stmt>,
/// Coq parameters that the function is parameterized over
- required_parameters: Vec<coq::term::Binder>,
+ required_parameters: Vec<coq::binder::Binder>,
}
fn make_map_string(sep: &str, els: &Vec<(String, String)>) -> String {
@@ -1289,12 +1289,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::term::Binder) {
+ pub fn add_early_coq_param(&mut self, param: coq::binder::Binder) {
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::term::Binder) {
+ pub fn add_late_coq_param(&mut self, param: coq::binder::Binder) {
self.spec.late_coq_params.0.push(param);
}
@@ -1328,13 +1328,11 @@ 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::term::Binder::new(
- Some(spec_params_param_name),
- coq::term::Type::Literal(spec_params_type_name),
- )
- .set_implicit(true),
- );
+ self.spec.late_coq_params.0.push(coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ Some(spec_params_param_name),
+ coq::term::Type::Literal(spec_params_type_name),
+ ));
// add the attr params
let all_args: Vec<_> = trait_use
@@ -1345,7 +1343,7 @@ 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::term::Binder::new(
+ self.spec.late_coq_params.0.push(coq::binder::Binder::new(
Some(spec_attrs_param_name),
coq::term::Type::Literal(attr_param),
));
@@ -1354,7 +1352,7 @@ impl<'def> FunctionBuilder<'def> {
self.spec
.late_coq_params
.0
- .push(coq::term::Binder::new(Some(spec_param_name), coq::term::Type::Literal(spec_type)));
+ .push(coq::binder::Binder::new(Some(spec_param_name), coq::term::Type::Literal(spec_type)));
let spec_precond = trait_use.make_spec_param_precond();
// this should be proved after typarams are instantiated
@@ -1378,17 +1376,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::term::Binder> = self
+ let mut parameters: Vec<coq::binder::Binder> = self
.other_functions
.iter()
- .map(|f_inst| (coq::term::Binder::new(Some(f_inst.loc_name.clone()), coq::term::Type::Loc)))
+ .map(|f_inst| (coq::binder::Binder::new(Some(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::term::Binder::new(Some(s.loc_name.clone()), coq::term::Type::Loc))
+ .map(|s| coq::binder::Binder::new(Some(s.loc_name.clone()), coq::term::Type::Loc))
.collect();
parameters.append(&mut statics_parameters);
@@ -1399,7 +1397,7 @@ impl<'def> FunctionBuilder<'def> {
.generics
.get_ty_params()
.iter()
- .map(|names| coq::term::Binder::new(Some(names.syn_type.clone()), coq::term::Type::SynType))
+ .map(|names| coq::binder::Binder::new(Some(names.syn_type.clone()), coq::term::Type::SynType))
.collect();
parameters.append(&mut gen_st_parameters);
diff --git a/rr_frontend/radium/src/coq/binder.rs b/rr_frontend/radium/src/coq/binder.rs
new file mode 100644
index 0000000..ce3d5e6
--- /dev/null
+++ b/rr_frontend/radium/src/coq/binder.rs
@@ -0,0 +1,142 @@
+//! The [implicit arguments], and [binders].
+//!
+//! [implicit arguments]: https://coq.inria.fr/doc/v8.20/refman/language/extensions/implicit-arguments.html#implicit-arguments
+//! [binders]: https://coq.inria.fr/doc/v8.20/refman/language/core/assumptions.html#binders
+
+use std::fmt;
+
+use derive_more::Display;
+
+use crate::coq::term;
+use crate::display_list;
+
+/// A [binder].
+///
+/// [binder]: https://coq.inria.fr/doc/v8.20/refman/language/core/assumptions.html#grammar-token-binder
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+pub enum Binder {
+ #[display("({}: {})", self.get_name(), _1)]
+ Default(Option<String>, term::Type),
+
+ #[display("{}", _0)]
+ Generalizing(Generalizing),
+}
+
+impl Binder {
+ #[must_use]
+ pub const fn new(name: Option<String>, ty: term::Type) -> Self {
+ Self::Default(name, ty)
+ }
+
+ #[must_use]
+ pub const fn new_generalized(kind: Kind, name: Option<String>, ty: term::Type) -> Self {
+ Self::Generalizing(Generalizing { kind, name, ty })
+ }
+
+ #[must_use]
+ pub(crate) fn get_name(&self) -> String {
+ match self {
+ Self::Default(name, _) => name.clone().unwrap_or_else(|| "_".to_owned()),
+ Self::Generalizing(g) => g.name.clone().unwrap_or_else(|| "_".to_owned()),
+ }
+ }
+
+ pub(crate) const fn get_name_ref(&self) -> &Option<String> {
+ match self {
+ Self::Default(name, _) => name,
+ Self::Generalizing(g) => &g.name,
+ }
+ }
+
+ pub(crate) const fn get_type(&self) -> &term::Type {
+ match self {
+ Self::Default(_, ty) => ty,
+ Self::Generalizing(g) => &g.ty,
+ }
+ }
+
+ #[must_use]
+ pub(crate) const fn is_implicit(&self) -> bool {
+ matches!(self, Self::Generalizing(_))
+ }
+
+ #[must_use]
+ pub(crate) fn is_dependent_on_sigma(&self) -> bool {
+ let term::Type::Literal(lit) = self.get_type() else {
+ return false;
+ };
+
+ lit.contains('Σ')
+ }
+
+ #[must_use]
+ pub fn set_name(self, name: String) -> Self {
+ match self {
+ Self::Default(_, ty) => Self::Default(Some(name), ty),
+ Self::Generalizing(g) => Self::Generalizing(Generalizing {
+ name: Some(name),
+ ..g
+ }),
+ }
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub enum Kind {
+ /// `()
+ Implicit,
+
+ /// `{}
+ MaxImplicit,
+}
+
+/// [Implicit generalization] binders.
+///
+/// [Implicit generalization]: https://coq.inria.fr/doc/v8.20/refman/language/extensions/implicit-arguments.html#grammar-token-generalizing_binder
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct Generalizing {
+ kind: Kind,
+ name: Option<String>,
+ ty: term::Type,
+}
+
+impl fmt::Display for Generalizing {
+ fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ match (&self.kind, &self.name) {
+ (Kind::Implicit, Some(name)) => write!(f, "`({} : !{})", name, self.ty),
+ (Kind::Implicit, None) => write!(f, "`(!{})", self.ty),
+ (Kind::MaxImplicit, Some(name)) => write!(f, "`{{{} : !{}}}", name, self.ty),
+ (Kind::MaxImplicit, None) => write!(f, "`{{!{}}}", self.ty),
+ }
+ }
+}
+
+/// A Rocq pattern, e.g., "x" or "'(x, y)".
+pub type Pattern = String;
+
+#[allow(clippy::module_name_repetitions)]
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}", display_list!(_0, " "))]
+pub struct BinderList(pub Vec<Binder>);
+
+impl BinderList {
+ #[must_use]
+ pub const fn new(params: Vec<Binder>) -> Self {
+ Self(params)
+ }
+
+ #[must_use]
+ pub const fn empty() -> Self {
+ Self(vec![])
+ }
+
+ pub fn append(&mut self, params: Vec<Binder>) {
+ self.0.extend(params);
+ }
+
+ /// Make using terms for this list of binders
+ #[must_use]
+ pub fn make_using_terms(&self) -> Vec<term::Gallina> {
+ self.0.iter().map(|x| term::Gallina::Literal(format!("{}", x.get_name()))).collect()
+ }
+}
diff --git a/rr_frontend/radium/src/coq/command.rs b/rr_frontend/radium/src/coq/command.rs
index c2bee15..7fe5716 100644
--- a/rr_frontend/radium/src/coq/command.rs
+++ b/rr_frontend/radium/src/coq/command.rs
@@ -14,7 +14,7 @@ use derive_more::Display;
use from_variants::FromVariants;
use indent_write::indentable::Indentable;
-use crate::coq::{eval, inductive, module, syntax, term, typeclasses, Attribute, Document, Sentence};
+use crate::coq::{binder, eval, inductive, module, syntax, term, typeclasses, Attribute, Document, Sentence};
use crate::make_indent;
/// A [command], with optional attributes.
@@ -176,22 +176,23 @@ impl From<QueryCommand> for Sentence {
/// A Context declaration.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ContextDecl {
- pub items: term::BinderList,
+ pub items: binder::BinderList,
}
impl ContextDecl {
#[must_use]
- pub const fn new(items: term::BinderList) -> Self {
+ pub const fn new(items: binder::BinderList) -> Self {
Self { items }
}
#[must_use]
pub fn refinedrust() -> Self {
Self {
- items: term::BinderList::new(vec![
- term::Binder::new(Some("RRGS".to_owned()), term::Type::Literal("refinedrustGS Σ".to_owned()))
- .set_implicit(true),
- ]),
+ items: binder::BinderList::new(vec![binder::Binder::new_generalized(
+ binder::Kind::MaxImplicit,
+ Some("RRGS".to_owned()),
+ term::Type::Literal("refinedrustGS Σ".to_owned()),
+ )]),
}
}
}
@@ -206,7 +207,7 @@ impl Display for ContextDecl {
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct Definition {
pub name: String,
- pub params: term::BinderList,
+ pub params: binder::BinderList,
pub ty: Option<term::Type>,
pub body: term::Gallina,
}
diff --git a/rr_frontend/radium/src/coq/inductive.rs b/rr_frontend/radium/src/coq/inductive.rs
index abd56db..31015d9 100644
--- a/rr_frontend/radium/src/coq/inductive.rs
+++ b/rr_frontend/radium/src/coq/inductive.rs
@@ -11,7 +11,7 @@
use derive_more::{Constructor, Display};
use indent_write::indentable::Indentable;
-use crate::coq::term;
+use crate::coq::binder;
use crate::{display_list, make_indent};
/// An [Inductive] type.
@@ -25,7 +25,7 @@ use crate::{display_list, make_indent};
)]
pub struct Inductive {
name: String,
- parameters: term::BinderList,
+ parameters: binder::BinderList,
variants: Vec<Variant>,
}
@@ -40,12 +40,12 @@ impl Inductive {
#[display("{} {}", name, display_list!(params, " "))]
pub struct Variant {
name: String,
- params: Vec<term::Binder>,
+ params: Vec<binder::Binder>,
}
impl Variant {
#[must_use]
- pub fn new(name: String, params: Vec<term::Binder>) -> Self {
+ pub fn new(name: String, params: Vec<binder::Binder>) -> Self {
Self { name, params }
}
}
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index d59cc2b..8897add 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -320,6 +320,7 @@
//! [Rocq reference]: https://coq.inria.fr/doc/v8.20/refman/index.html
//! [sections]: https://coq.inria.fr/doc/v8.20/refman/language/core/sections.html
+pub mod binder;
pub mod command;
pub mod eval;
pub mod inductive;
diff --git a/rr_frontend/radium/src/coq/term.rs b/rr_frontend/radium/src/coq/term.rs
index 66d09c7..3888be8 100644
--- a/rr_frontend/radium/src/coq/term.rs
+++ b/rr_frontend/radium/src/coq/term.rs
@@ -8,13 +8,14 @@
//!
//! [terms]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#term-term
-use std::fmt::{self, Write};
+use std::fmt;
use derive_more::Display;
use indent_write::fmt::IndentWriter;
use indent_write::indentable::Indentable;
use itertools::Itertools;
+use crate::coq::binder;
use crate::{display_list, make_indent, BASE_INDENT};
/// A [term].
@@ -35,10 +36,10 @@ pub enum Gallina {
RecordProj(Box<Gallina>, String),
/// Universal quantifiers
- All(BinderList, Box<Gallina>),
+ All(binder::BinderList, Box<Gallina>),
/// Existential quantifiers
- Exists(BinderList, Box<Gallina>),
+ Exists(binder::BinderList, Box<Gallina>),
/// Infix operators
Infix(String, Vec<Gallina>),
@@ -82,12 +83,14 @@ impl<T, U> App<T, U> {
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct RecordBodyItem {
pub name: String,
- pub params: BinderList,
+ pub params: binder::BinderList,
pub term: Gallina,
}
impl Display for RecordBodyItem {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ use fmt::Write;
+
let mut writer = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
write!(writer, "{} {} :=\n{};", self.name, self.params, self.term)
}
@@ -100,6 +103,8 @@ pub struct RecordBody {
impl Display for RecordBody {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ use fmt::Write;
+
write!(f, "{{|\n")?;
let mut f2 = IndentWriter::new(BASE_INDENT, &mut *f);
for it in &self.items {
@@ -111,6 +116,8 @@ impl Display for RecordBody {
impl Display for Gallina {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ use fmt::Write;
+
match self {
Self::Literal(lit) => {
let mut f2 = IndentWriter::new_skip_initial(BASE_INDENT, &mut *f);
@@ -240,127 +247,12 @@ pub enum Type {
Prop,
}
-/// A Coq pattern, e.g., "x" or "'(x, y)".
-pub type Pattern = String;
-
-/// A [binder].
-///
-/// [binder]: https://coq.inria.fr/doc/v8.20/refman/language/core/assumptions.html#grammar-token-binder
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}", self.format(true))]
-pub struct Binder {
- name: Option<String>,
- ty: Type,
- is_implicit: bool,
- depends_on_sigma: bool,
-}
-
-impl Binder {
- #[must_use]
- pub fn new(name: Option<String>, ty: Type) -> Self {
- let depends_on_sigma = if let Type::Literal(lit) = &ty { lit.contains('Σ') } else { false };
-
- Self {
- name,
- ty,
- is_implicit: false,
- depends_on_sigma,
- }
- }
-
- #[must_use]
- pub fn set_implicit(self, is_implicit: bool) -> Self {
- Self {
- is_implicit,
- ..self
- }
- }
-
- #[must_use]
- pub fn set_name(self, name: String) -> Self {
- Self {
- name: Some(name),
- ..self
- }
- }
-
- #[must_use]
- pub(crate) fn get_name(&self) -> String {
- let Some(name) = &self.name else { return "_".to_owned() };
- name.clone()
- }
-
- pub(crate) const fn get_name_ref(&self) -> &Option<String> {
- &self.name
- }
-
- pub(crate) const fn get_type(&self) -> &Type {
- &self.ty
- }
-
- pub(crate) const fn is_implicit(&self) -> bool {
- self.is_implicit
- }
-
- pub(crate) const fn is_dependent_on_sigma(&self) -> bool {
- self.depends_on_sigma
- }
-
- #[allow(clippy::collapsible_else_if)]
- #[must_use]
- fn format(&self, make_implicits: bool) -> String {
- if !self.is_implicit {
- return format!("({} : {})", self.get_name(), self.ty);
- }
-
- if make_implicits {
- if let Some(name) = &self.name {
- format!("`{{{} : !{}}}", name, self.ty)
- } else {
- format!("`{{!{}}}", self.ty)
- }
- } else {
- if let Some(name) = &self.name {
- format!("`({} : !{})", name, self.ty)
- } else {
- format!("`(!{})", self.ty)
- }
- }
- }
-}
-
-#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}", display_list!(_0, " "))]
-pub struct BinderList(pub Vec<Binder>);
-
-impl BinderList {
- #[must_use]
- pub const fn new(params: Vec<Binder>) -> Self {
- Self(params)
- }
-
- #[must_use]
- pub const fn empty() -> Self {
- Self(vec![])
- }
-
- pub fn append(&mut self, params: Vec<Binder>) {
- 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.get_name()))).collect()
- }
-}
-
/* TODO */
#[derive(Clone, Debug, Display, Eq, PartialEq)]
#[display("{} {} : {}", name, params, ty)]
pub struct RecordDeclItem {
pub name: String,
- pub params: BinderList,
+ pub params: binder::BinderList,
pub ty: Type,
}
@@ -368,7 +260,7 @@ pub struct RecordDeclItem {
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct Record {
pub name: String,
- pub params: BinderList,
+ pub params: binder::BinderList,
pub ty: Type,
pub constructor: Option<String>,
pub body: Vec<RecordDeclItem>,
@@ -376,6 +268,8 @@ pub struct Record {
impl Display for Record {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+ use fmt::Write;
+
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);
diff --git a/rr_frontend/radium/src/coq/typeclasses.rs b/rr_frontend/radium/src/coq/typeclasses.rs
index 3a511c7..9c35dcd 100644
--- a/rr_frontend/radium/src/coq/typeclasses.rs
+++ b/rr_frontend/radium/src/coq/typeclasses.rs
@@ -16,5 +16,5 @@ use crate::coq::term;
///
/// [`Instance`]: https://coq.inria.fr/doc/v8.20/refman/addendum/type-classes.html#coq:cmd.Instance
#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("Instance {}", _0)]
+#[display("Instance: {}", _0)]
pub struct Instance(pub term::Type);
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 2a91b2d..831063f 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -472,13 +472,13 @@ impl LiteralTyParam {
}
#[must_use]
- pub fn make_refinement_param(&self) -> coq::term::Binder {
- coq::term::Binder::new(Some(self.refinement_type.clone()), coq::term::Type::Type)
+ pub fn make_refinement_param(&self) -> coq::binder::Binder {
+ coq::binder::Binder::new(Some(self.refinement_type.clone()), coq::term::Type::Type)
}
#[must_use]
- pub fn make_syntype_param(&self) -> coq::term::Binder {
- coq::term::Binder::new(Some(self.syn_type.clone()), coq::term::Type::SynType)
+ pub fn make_syntype_param(&self) -> coq::binder::Binder {
+ coq::binder::Binder::new(Some(self.syn_type.clone()), coq::term::Type::SynType)
}
}
@@ -738,10 +738,10 @@ pub struct InvariantSpec {
/// the refinement type of this struct
rfn_type: coq::term::Type,
/// the binding pattern for the refinement of this type
- rfn_pat: coq::term::Pattern,
+ rfn_pat: coq::binder::Pattern,
/// existentials that are introduced in the invariant
- existentials: Vec<coq::term::Binder>,
+ existentials: Vec<coq::binder::Binder>,
/// an optional invariant as a separating conjunction,
invariants: Vec<(IProp, InvariantMode)>,
@@ -749,11 +749,11 @@ 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::term::Pattern>,
+ abstracted_refinement: Option<coq::binder::Pattern>,
// TODO add stuff for non-atomic/atomic invariants
/// name, type, implicit or not
- coq_params: Vec<coq::term::Binder>,
+ coq_params: Vec<coq::binder::Binder>,
}
impl InvariantSpec {
@@ -763,12 +763,12 @@ impl InvariantSpec {
flags: InvariantSpecFlags,
shr_lft_binder: String,
rfn_type: coq::term::Type,
- rfn_pat: coq::term::Pattern,
- existentials: Vec<coq::term::Binder>,
+ rfn_pat: coq::binder::Pattern,
+ existentials: Vec<coq::binder::Binder>,
invariants: Vec<(IProp, InvariantMode)>,
ty_own_invariants: Vec<TyOwnSpec>,
- abstracted_refinement: Option<coq::term::Pattern>,
- coq_params: Vec<coq::term::Binder>,
+ abstracted_refinement: Option<coq::binder::Pattern>,
+ coq_params: Vec<coq::binder::Binder>,
) -> Self {
if flags == InvariantSpecFlags::Persistent {
assert!(invariants.iter().all(|it| it.1 == InvariantMode::All) && ty_own_invariants.is_empty());
@@ -789,7 +789,7 @@ impl InvariantSpec {
}
/// Add the abstracted refinement, if it was not already provided.
- pub fn provide_abstracted_refinement(&mut self, abstracted_refinement: coq::term::Pattern) {
+ pub fn provide_abstracted_refinement(&mut self, abstracted_refinement: coq::binder::Pattern) {
if self.abstracted_refinement.is_some() {
panic!("abstracted refinement for {} already provided", self.type_name);
}
@@ -1299,7 +1299,7 @@ impl<'def> AbstractVariant<'def> {
pub fn generate_coq_type_def(
&self,
ty_params: &[LiteralTyParam],
- extra_context: &[coq::term::Binder],
+ extra_context: &[coq::binder::Binder],
) -> String {
let mut out = String::with_capacity(200);
let indent = " ";
@@ -1348,7 +1348,7 @@ impl<'def> AbstractVariant<'def> {
}
fn format_extra_context_items<F>(
- items: &[coq::term::Binder],
+ items: &[coq::binder::Binder],
f: &mut F,
) -> Result<(Vec<String>, bool), fmt::Error>
where
@@ -2434,8 +2434,8 @@ pub enum IProp {
Disj(Vec<IProp>),
Conj(Vec<IProp>),
Wand(Box<IProp>, Box<IProp>),
- Exists(Vec<coq::term::Binder>, Box<IProp>),
- All(Vec<coq::term::Binder>, Box<IProp>),
+ Exists(Vec<coq::binder::Binder>, Box<IProp>),
+ All(Vec<coq::binder::Binder>, Box<IProp>),
}
fn fmt_with_op<T>(v: &[T], op: &str, f: &mut Formatter<'_>) -> Result<(), fmt::Error>
@@ -2449,7 +2449,7 @@ where
write_list!(f, v, &format!(" {op} "), "({})")
}
-fn fmt_binders(binders: &[coq::term::Binder], op: &str, f: &mut Formatter<'_>) -> Result<(), fmt::Error> {
+fn fmt_binders(binders: &[coq::binder::Binder], op: &str, f: &mut Formatter<'_>) -> Result<(), fmt::Error> {
write!(f, "{} ", op)?;
write_list!(f, binders, " ")
}
@@ -2480,13 +2480,13 @@ impl Display for IProp {
/// Representation of an Iris predicate
#[derive(Clone, Debug)]
pub struct IPropPredicate {
- binders: Vec<coq::term::Binder>,
+ binders: Vec<coq::binder::Binder>,
prop: IProp,
}
impl IPropPredicate {
#[must_use]
- pub fn new(binders: Vec<coq::term::Binder>, prop: IProp) -> Self {
+ pub fn new(binders: Vec<coq::binder::Binder>, prop: IProp) -> Self {
Self { binders, prop }
}
}
@@ -2524,7 +2524,7 @@ impl<'def> InnerFunctionSpec<'def> {
}
#[must_use]
- pub fn get_params(&self) -> Option<&[coq::term::Binder]> {
+ pub fn get_params(&self) -> Option<&[coq::binder::Binder]> {
match self {
Self::Lit(lit) => Some(&lit.params),
Self::TraitDefault(_) => None,
@@ -2543,8 +2543,8 @@ pub struct FunctionSpec<T> {
pub generics: GenericScope,
/// Coq-level parameters the typing statement needs
- pub early_coq_params: coq::term::BinderList,
- pub late_coq_params: coq::term::BinderList,
+ pub early_coq_params: coq::binder::BinderList,
+ pub late_coq_params: coq::binder::BinderList,
pub spec: T,
}
@@ -2567,8 +2567,8 @@ impl<T> FunctionSpec<T> {
spec_name,
function_name,
generics: GenericScope::empty(),
- early_coq_params: coq::term::BinderList::empty(),
- late_coq_params: coq::term::BinderList::empty(),
+ early_coq_params: coq::binder::BinderList::empty(),
+ late_coq_params: coq::binder::BinderList::empty(),
spec,
}
}
@@ -2578,8 +2578,8 @@ impl<T> FunctionSpec<T> {
spec_name: String,
function_name: String,
generics: GenericScope,
- early_params: coq::term::BinderList,
- late_params: coq::term::BinderList,
+ early_params: coq::binder::BinderList,
+ late_params: coq::binder::BinderList,
spec: T,
) -> Self {
Self {
@@ -2598,7 +2598,7 @@ impl<T> FunctionSpec<T> {
}
#[must_use]
- pub fn get_all_coq_params(&self) -> coq::term::BinderList {
+ pub fn get_all_coq_params(&self) -> coq::binder::BinderList {
// 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.
@@ -2645,7 +2645,7 @@ impl<'def> Display for FunctionSpec<InnerFunctionSpec<'def>> {
/// A function specification below generics.
#[derive(Clone, Debug)]
pub struct LiteralFunctionSpec<'def> {
- pub params: Vec<coq::term::Binder>,
+ pub params: Vec<coq::binder::Binder>,
/// external lifetime context
pub elctx: Vec<ExtLftConstr>,
@@ -2657,7 +2657,7 @@ pub struct LiteralFunctionSpec<'def> {
/// argument types including refinements
pub args: Vec<TypeWithRef<'def>>,
/// existential quantifiers for the postcondition
- pub existentials: Vec<coq::term::Binder>,
+ pub existentials: Vec<coq::binder::Binder>,
/// return type
pub ret: TypeWithRef<'def>,
/// postcondition as a separating conjunction
@@ -2696,9 +2696,9 @@ impl<'def> LiteralFunctionSpec<'def> {
out
}
- fn uncurry_typed_binders<'a, F>(v: F) -> (coq::term::Pattern, coq::term::Type)
+ fn uncurry_typed_binders<'a, F>(v: F) -> (coq::binder::Pattern, coq::term::Type)
where
- F: IntoIterator<Item = &'a coq::term::Binder>,
+ F: IntoIterator<Item = &'a coq::binder::Binder>,
{
let mut v = v.into_iter().peekable();
@@ -2787,12 +2787,12 @@ impl<'def> LiteralFunctionSpec<'def> {
#[derive(Debug)]
pub struct LiteralFunctionSpecBuilder<'def> {
- params: Vec<coq::term::Binder>,
+ params: Vec<coq::binder::Binder>,
elctx: Vec<ExtLftConstr>,
pre: IProp,
late_pre: IProp,
args: Vec<TypeWithRef<'def>>,
- existential: Vec<coq::term::Binder>,
+ existential: Vec<coq::binder::Binder>,
ret: Option<TypeWithRef<'def>>,
post: IProp,
@@ -2826,7 +2826,7 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
}
/// Adds a (universally-quantified) parameter with a given Coq name for the spec.
- pub fn add_param(&mut self, binder: coq::term::Binder) -> Result<(), String> {
+ pub fn add_param(&mut self, binder: coq::binder::Binder) -> Result<(), String> {
self.ensure_coq_not_bound(binder.get_name_ref())?;
self.push_coq_name(binder.get_name_ref());
self.params.push(binder);
@@ -2843,7 +2843,7 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
if param_name == name {
if *param.get_type() == coq::term::Type::Infer {
- *param = coq::term::Binder::new(Some(name.clone()), ty);
+ *param = coq::binder::Binder::new(Some(name.clone()), ty);
}
return Ok(());
}
@@ -2935,7 +2935,7 @@ impl<'def> LiteralFunctionSpecBuilder<'def> {
}
/// Add an existentially-quantified variable to the postcondition.
- pub fn add_existential(&mut self, binder: coq::term::Binder) -> Result<(), String> {
+ pub fn add_existential(&mut self, binder: coq::binder::Binder) -> Result<(), String> {
self.ensure_coq_not_bound(binder.get_name_ref())?;
self.existential.push(binder);
// TODO: if we add some kind of name analysis to postcondition, we need to handle the
@@ -3370,54 +3370,54 @@ 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::term::BinderList {
+ fn get_coq_ty_params(&self) -> coq::binder::BinderList {
let mut ty_coq_params = Vec::new();
for names in &self.tys {
ty_coq_params
- .push(coq::term::Binder::new(Some(names.refinement_type.clone()), coq::term::Type::Type));
+ .push(coq::binder::Binder::new(Some(names.refinement_type.clone()), coq::term::Type::Type));
}
for names in &self.tys {
ty_coq_params
- .push(coq::term::Binder::new(Some(names.syn_type.clone()), coq::term::Type::SynType));
+ .push(coq::binder::Binder::new(Some(names.syn_type.clone()), coq::term::Type::SynType));
}
- coq::term::BinderList(ty_coq_params)
+ coq::binder::BinderList(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::term::BinderList {
+ pub fn get_coq_ty_st_params(&self) -> coq::binder::BinderList {
let mut ty_coq_params = Vec::new();
for names in &self.tys {
ty_coq_params.push(names.make_syntype_param());
}
- coq::term::BinderList::new(ty_coq_params)
+ coq::binder::BinderList::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::term::BinderList {
+ pub fn get_direct_coq_ty_st_params(&self) -> coq::binder::BinderList {
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::term::BinderList::new(ty_coq_params)
+ coq::binder::BinderList::new(ty_coq_params)
}
#[must_use]
- pub fn get_direct_coq_ty_rt_params(&self) -> coq::term::BinderList {
+ pub fn get_direct_coq_ty_rt_params(&self) -> coq::binder::BinderList {
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::term::BinderList::new(ty_coq_params)
+ coq::binder::BinderList::new(ty_coq_params)
}
#[must_use]
- pub fn get_direct_coq_ty_params(&self) -> coq::term::BinderList {
+ pub fn get_direct_coq_ty_params(&self) -> coq::binder::BinderList {
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);
@@ -3455,10 +3455,10 @@ fn make_trait_instance<'def>(
// 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::term::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type);
+ let rt_param = coq::binder::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type);
def_rts_params.push(rt_param);
}
- let def_rts_params = coq::term::BinderList::new(def_rts_params);
+ let def_rts_params = coq::binder::BinderList::new(def_rts_params);
let def_rts_params_uses = def_rts_params.make_using_terms();
let param_record_term = if spec.methods.is_empty() {
@@ -3515,19 +3515,19 @@ fn make_trait_instance<'def>(
let mut def_params = Vec::new();
// all rts
for param in scope.tys.iter().chain(assoc_types) {
- let rt_param = coq::term::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type);
+ let rt_param = coq::binder::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type);
def_params.push(rt_param);
}
// all sts
for param in scope.tys.iter().chain(assoc_types) {
- let st_param = coq::term::Binder::new(Some(param.syn_type.clone()), coq::term::Type::SynType);
+ let st_param = coq::binder::Binder::new(Some(param.syn_type.clone()), coq::term::Type::SynType);
def_params.push(st_param);
}
// then, the attrs. these also get the associated types
if is_base_spec {
- def_params.push(coq::term::Binder::new(Some("_ATTRS".to_owned()), attrs_type));
+ def_params.push(coq::binder::Binder::new(Some("_ATTRS".to_owned()), attrs_type));
}
- let def_params = coq::term::BinderList::new(def_params);
+ let def_params = coq::binder::BinderList::new(def_params);
// for this, we assume that the semantic type parameters are all in scope
let body_term = if spec.methods.is_empty() {
@@ -3625,7 +3625,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::term::BinderList,
+ pub extra_coq_context: coq::binder::BinderList,
/// The generics this trait uses
pub generics: GenericScope,
@@ -3667,7 +3667,7 @@ impl<'def> Display for TraitSpecDecl<'def> {
}
let spec_param_record = coq::term::Record {
name: self.lit.spec_params_record.clone(),
- params: coq::term::BinderList::empty(),
+ params: coq::binder::BinderList::empty(),
ty: coq::term::Type::Type,
constructor: Some(spec_param_record_constructor),
body: record_items,
@@ -3681,7 +3681,7 @@ impl<'def> Display for TraitSpecDecl<'def> {
let item = coq::term::RecordDeclItem {
name: record_item_name,
- params: coq::term::BinderList::empty(),
+ params: coq::binder::BinderList::empty(),
ty: item_ty.to_owned(),
};
record_items.push(item);
@@ -3689,14 +3689,15 @@ 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::term::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type)
- .set_implicit(true),
- );
+ attr_params.push(coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ Some(param.refinement_type.clone()),
+ coq::term::Type::Type,
+ ));
}
let spec_attr_record = coq::term::Record {
name: self.lit.spec_attrs_record.clone(),
- params: coq::term::BinderList::new(attr_params),
+ params: coq::binder::BinderList::new(attr_params),
ty: coq::term::Type::Type,
constructor: Some(spec_attrs_record_constructor.clone()),
body: record_items,
@@ -3737,16 +3738,14 @@ impl<'def> Display for TraitSpecDecl<'def> {
};
record_items.push(item);
}
- let spec_params = vec![
- coq::term::Binder::new(
- Some("_P".to_owned()),
- coq::term::Type::Literal(self.lit.spec_params_record.clone()),
- )
- .set_implicit(true),
- ];
+ let spec_params = vec![coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ Some("_P".to_owned()),
+ coq::term::Type::Literal(self.lit.spec_params_record.clone()),
+ )];
let spec_record = coq::term::Record {
name: self.lit.spec_record.clone(),
- params: coq::term::BinderList::new(spec_params),
+ params: coq::binder::BinderList::new(spec_params),
ty: coq::term::Type::Type,
constructor: Some(spec_record_constructor),
body: record_items,
@@ -3764,22 +3763,22 @@ 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::term::Binder::new(
+ coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
Some("_P1".to_owned()),
coq::term::Type::Literal(self.lit.spec_params_record.clone()),
- )
- .set_implicit(true),
- coq::term::Binder::new(
+ ),
+ coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
Some("_P2".to_owned()),
coq::term::Type::Literal(self.lit.spec_params_record.clone()),
- )
- .set_implicit(true),
+ ),
// the two actual specs
- coq::term::Binder::new(
+ coq::binder::Binder::new(
Some(spec_param_name1.clone()),
coq::term::Type::Literal(spec_param_type1),
),
- coq::term::Binder::new(
+ coq::binder::Binder::new(
Some(spec_param_name2.clone()),
coq::term::Type::Literal(spec_param_type2),
),
@@ -3816,7 +3815,7 @@ impl<'def> Display for TraitSpecDecl<'def> {
let spec_incl_def = coq::command::Definition {
name: spec_incl_name,
- params: coq::term::BinderList::new(spec_incl_params),
+ params: coq::binder::BinderList::new(spec_incl_params),
ty: Some(coq::term::Type::Prop),
body,
};
@@ -3916,10 +3915,11 @@ impl<'def> TraitImplSpec<'def> {
let mut def_rts_params = Vec::new();
for param in &self.trait_ref.generics.tys {
- let rt_param = coq::term::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type);
+ let rt_param =
+ coq::binder::Binder::new(Some(param.refinement_type.clone()), coq::term::Type::Type);
def_rts_params.push(rt_param);
}
- let def_rts_params = coq::term::BinderList::new(def_rts_params);
+ let def_rts_params = coq::binder::BinderList::new(def_rts_params);
let def_rts_params_uses = def_rts_params.make_using_terms();
// write the attr record decl
@@ -3938,7 +3938,7 @@ impl<'def> TraitImplSpec<'def> {
let item = coq::term::RecordBodyItem {
name: record_item_name,
- params: coq::term::BinderList::empty(),
+ params: coq::binder::BinderList::empty(),
term: inst.to_owned(),
};
components.push(item);
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index d76e50f..cc70850 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -1164,7 +1164,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
let param_ty =
format!("{}", coq::term::App::new(trait_ref.spec_attrs_record.clone(), param_ty_args));
let param =
- coq::term::Binder::new(Some(param_name.clone()), coq::term::Type::Literal(param_ty));
+ coq::binder::Binder::new(Some(param_name.clone()), coq::term::Type::Literal(param_ty));
// add it as a parameter to the function after the generics
translated_fn.add_late_coq_param(param);
@@ -2129,7 +2129,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// determine the actual refinement type for the current initialization status.
let rfn_name = format!("r_{}", name);
- rfn_binders.push(coq::term::Binder::new(Some(rfn_name), rfn_ty));
+ rfn_binders.push(coq::binder::Binder::new(Some(rfn_name), rfn_ty));
}
// TODO what do we do about stuff connecting borrows?
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 a4435c5..0488d50 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -23,7 +23,7 @@ pub struct CrateAttrs {
pub prefix: Option<String>,
pub includes: Vec<String>,
pub package: Option<String>,
- pub context_params: Vec<coq::term::Binder>,
+ pub context_params: Vec<coq::binder::Binder>,
}
#[allow(clippy::module_name_repetitions)]
@@ -77,9 +77,11 @@ impl CrateAttrParser for VerboseCrateAttrParser {
},
"context" => {
let param: parse_utils::RRGlobalCoqContextItem = buffer.parse(&()).map_err(str_err)?;
- context_params.push(
- coq::term::Binder::new(None, coq::term::Type::Literal(param.item)).set_implicit(true),
- );
+ context_params.push(coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ None,
+ coq::term::Type::Literal(param.item),
+ ));
},
_ => {
return Err(format!("unknown attribute for crate specification: {:?}", args));
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 6a7010a..8db1d3a 100644
--- a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
@@ -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::term::Binder>,
+ pub context_params: Vec<coq::binder::Binder>,
}
#[allow(clippy::module_name_repetitions)]
@@ -68,9 +68,11 @@ impl ModuleAttrParser for VerboseModuleAttrParser {
},
"context" => {
let param: parse_utils::RRGlobalCoqContextItem = buffer.parse(&()).map_err(str_err)?;
- context_params.push(
- coq::term::Binder::new(None, coq::term::Type::Literal(param.item)).set_implicit(true),
- );
+ context_params.push(coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ None,
+ coq::term::Type::Literal(param.item),
+ ));
},
_ => {
return Err(format!("unknown attribute for module specification: {:?}", args));
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 6f384c0..158ad51 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -149,9 +149,9 @@ impl<T: ParamLookup> parse::Parse<T> for RRCoqType {
/// `z`,
/// `w : "(Z * Z)%type"`
#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct RRParam(coq::term::Binder);
+pub struct RRParam(coq::binder::Binder);
-impl From<RRParam> for coq::term::Binder {
+impl From<RRParam> for coq::binder::Binder {
fn from(param: RRParam) -> Self {
param.0
}
@@ -165,9 +165,9 @@ impl<T: ParamLookup> parse::Parse<T> for RRParam {
if parse::Colon::peek(input) {
input.parse::<_, MToken![:]>(meta)?;
let ty: RRCoqType = input.parse(meta)?;
- Ok(Self(coq::term::Binder::new(Some(name), ty.ty)))
+ Ok(Self(coq::binder::Binder::new(Some(name), ty.ty)))
} else {
- Ok(Self(coq::term::Binder::new(Some(name), coq::term::Type::Infer)))
+ Ok(Self(coq::binder::Binder::new(Some(name), 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 ca79612..bf48d78 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -39,7 +39,7 @@ 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::term::Pattern,
+ rfn_pat: coq::binder::Pattern,
rfn_type: Option<coq::term::Type>,
}
@@ -199,12 +199,12 @@ impl<'b, T: ParamLookup> InvariantSpecParser for VerboseInvariantSpecParser<'b,
let mut rfn_pat = "placeholder_pat".to_owned();
let mut rfn_type = coq::term::Type::Infer;
- let mut existentials: Vec<coq::term::Binder> = Vec::new();
+ let mut existentials: Vec<coq::binder::Binder> = Vec::new();
// use Plain as the default
let mut inv_flags = specs::InvariantSpecFlags::Plain;
- let mut params: Vec<coq::term::Binder> = Vec::new();
+ let mut params: Vec<coq::binder::Binder> = Vec::new();
for &it in attrs {
let path_segs = &it.path.segments;
@@ -270,9 +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::term::Binder::new(None, coq::term::Type::Literal(param.item)).set_implicit(true),
- );
+ params.push(coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ None,
+ coq::term::Type::Literal(param.item),
+ ));
},
_ => {
//skip, this may be part of an enum spec
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 6e704ad..6cc5160 100644
--- a/rr_frontend/translation/src/spec_parsers/trait_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/trait_attr_parser.rs
@@ -49,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<coq::term::Binder>,
+ pub context_items: Vec<coq::binder::Binder>,
}
#[allow(clippy::module_name_repetitions)]
@@ -108,8 +108,11 @@ where
},
"context" => {
let context_item: RRCoqContextItem = buffer.parse(&self.scope).map_err(str_err)?;
- let param = coq::term::Binder::new(None, coq::term::Type::Literal(context_item.item))
- .set_implicit(true);
+ let param = coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ None,
+ coq::term::Type::Literal(context_item.item),
+ );
context_items.push(param);
},
"export_as" => (),
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 70181b3..88e0c9a 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::term::Binder>,
+ pub late_coq_params: Vec<coq::binder::Binder>,
/// additional early coq parameters
- pub early_coq_params: Vec<coq::term::Binder>,
+ pub early_coq_params: Vec<coq::binder::Binder>,
/// proof information
pub proof_info: ProofInfo,
}
@@ -413,8 +413,11 @@ where
},
"context" => {
let context_item = RRCoqContextItem::parse(buffer, scope).map_err(str_err)?;
- let param = coq::term::Binder::new(None, coq::term::Type::Literal(context_item.item))
- .set_implicit(true);
+ let param = coq::binder::Binder::new_generalized(
+ coq::binder::Kind::MaxImplicit,
+ None,
+ coq::term::Type::Literal(context_item.item),
+ );
if context_item.at_end {
self.fn_requirements.late_coq_params.push(param);
} else {
@@ -535,7 +538,7 @@ where
// push everything to the builder
for x in new_ghost_vars {
- builder.add_param(coq::term::Binder::new(Some(x), coq::term::Type::Gname)).unwrap();
+ builder.add_param(coq::binder::Binder::new(Some(x), coq::term::Type::Gname)).unwrap();
}
// assemble a string for the closure arg
@@ -584,7 +587,7 @@ where
// wrap the argument in a mutable reference
let post_name = "__γclos";
builder
- .add_param(coq::term::Binder::new(Some(post_name.to_owned()), coq::term::Type::Gname))
+ .add_param(coq::binder::Binder::new(Some(post_name.to_owned()), coq::term::Type::Gname))
.unwrap();
let lft = meta.closure_lifetime.unwrap();
diff --git a/rr_frontend/translation/src/trait_registry.rs b/rr_frontend/translation/src/trait_registry.rs
index 936d642..7d0c22e 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,
- coq::term::BinderList::new(trait_spec.context_items),
+ coq::binder::BinderList::new(trait_spec.context_items),
param_scope.into(),
assoc_types,
base_instance_spec,
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 9f85dca..6684001 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -1602,7 +1602,7 @@ 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::term::Binder::new(None, coq::term::Type::Literal(refinement_type))];
+ let args = vec![coq::binder::Binder::new(None, coq::term::Type::Literal(refinement_type))];
(args, vec!["x".to_owned()], "x".to_owned())
};
@@ -1612,8 +1612,11 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
}
// We assume the generated Inductive def is placed in a context where the generic types are in scope.
- let inductive =
- coq::inductive::Inductive::new(inductive_name.clone(), coq::term::BinderList::empty(), variants);
+ let inductive = coq::inductive::Inductive::new(
+ inductive_name.clone(),
+ coq::binder::BinderList::empty(),
+ variants,
+ );
let enum_spec = radium::EnumSpec {
rfn_type: coq::term::Type::Literal(inductive_name),
--
GitLab