diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 140bb0e2c74e77c44f50b39952745b3bc4fc6ec3..eca6402cb5091b59f07f1aa838e872f78d595baa 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -806,13 +806,7 @@ impl<'def> Function<'def> {
if has_params {
write!(f, "∀ ")?;
for param in &self.spec.coq_params {
- // TODO use CoqParam::format instead
- if param.implicit {
- write!(f, "`({})", param.ty)?;
- } else {
- write!(f, "({} : {})", param.name, param.ty)?;
- }
- write!(f, " ")?;
+ write!(f, "{} ", param)?;
}
// assume locations for other functions
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index bdadb866c344dbeda9ccf331ed5ae6352600196a..95ae1c40581568381ae9c146caa4c1b0ba3c7f3c 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -240,13 +240,70 @@ impl CoqType {
}
#[derive(Clone, Eq, PartialEq, Debug, Display)]
-#[display("{}", display_list!(_0, " ", |(name, ty)| format!("({} : {})", name, ty)))]
-pub struct CoqParamList(pub Vec<(CoqName, CoqType)>);
+#[display("{}", self.format(true))]
+pub struct CoqParam {
+ /// the name
+ pub(crate) name: CoqName,
+
+ /// the type
+ pub(crate) ty: CoqType,
+
+ /// implicit or not?
+ pub(crate) implicit: bool,
+
+ /// does this depend on Σ?
+ pub(crate) depends_on_sigma: bool,
+}
+
+impl CoqParam {
+ #[must_use]
+ pub fn new(name: CoqName, ty: CoqType, implicit: bool) -> Self {
+ let depends_on_sigma = if let CoqType::Literal(ref 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(CoqName::Named(name), self.ty.clone(), self.implicit)
+ }
+
+ #[allow(clippy::collapsible_else_if)]
+ #[must_use]
+ pub fn format(&self, make_implicits: bool) -> String {
+ if !self.implicit {
+ return format!("({} : {})", self.name, self.ty);
+ }
+
+ if make_implicits {
+ if let CoqName::Named(ref name) = self.name {
+ format!("`{{{} : !{}}}", name, self.ty)
+ } else {
+ format!("`{{!{}}}", self.ty)
+ }
+ } else {
+ if let CoqName::Named(ref name) = self.name {
+ format!("`({} : !{})", name, self.ty)
+ } else {
+ format!("`(!{})", self.ty)
+ }
+ }
+ }
+}
+
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{}", display_list!(_0, " "))]
+pub struct CoqParamList(Vec<CoqParam>);
impl CoqParamList {
#[must_use]
- pub const fn empty() -> Self {
- Self(vec![])
+ pub const fn new(params: Vec<CoqParam>) -> Self {
+ Self(params)
}
}
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index a6415e945723323acc4a46d8d5fabd688a8386fb..fc1c15852f98173e3f442de7120614aa0024ad4f 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -2177,7 +2177,7 @@ impl<'def> AbstractEnum<'def> {
let instance_decl = CoqInstanceDecl {
attrs: CoqAttributes::new(vec![CoqAttribute::Global]),
name: None,
- params: CoqParamList::empty(),
+ params: CoqParamList::new(vec![]),
ty: CoqType::Literal(format!("Inhabited {}", ind.name)),
body: CoqDefBody::Script(
CoqProofScript(vec![CoqProofItem::Literal(format!("solve_inhabited"))]),
@@ -2624,63 +2624,6 @@ pub struct LoopSpec {
pub func_predicate: IPropPredicate,
}
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct CoqParam {
- /// the name
- pub name: CoqName,
- /// the type
- pub ty: CoqType,
- /// implicit or not?
- pub implicit: bool,
- /// does this depend on Σ?
- pub depends_on_sigma: bool,
-}
-
-impl CoqParam {
- #[must_use]
- pub fn new(name: CoqName, ty: CoqType, implicit: bool) -> Self {
- let depends_on_sigma = if let CoqType::Literal(ref 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(CoqName::Named(name), self.ty.clone(), self.implicit)
- }
-
- #[allow(clippy::collapsible_else_if)]
- pub fn format(&self, f: &mut Formatter, make_implicits: bool) -> fmt::Result {
- if !self.implicit {
- return write!(f, "({} : {})", self.name, self.ty);
- }
-
- if make_implicits {
- if let CoqName::Named(ref name) = self.name {
- write!(f, "`{{{} : !{}}}", name, self.ty)
- } else {
- write!(f, "`{{!{}}}", self.ty)
- }
- } else {
- if let CoqName::Named(ref name) = self.name {
- write!(f, "`({} : !{})", name, self.ty)
- } else {
- write!(f, "`(!{})", self.ty)
- }
- }
- }
-}
-
-impl Display for CoqParam {
- fn fmt(&self, f: &mut Formatter) -> fmt::Result {
- self.format(f, true)
- }
-}
-
/**
* A Caesium function specification.
*/
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 18b002b14be3d6702bfecc0d62441b6dd5ca8b46..749e86c5ef6cd4070109095418a59b61893ce097 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -1100,13 +1100,18 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let (variant_args, variant_arg_binders, variant_rfn) = if variant_def.fields.is_empty() {
(vec![], vec![], "-[]".to_string())
} else {
- let args = vec![(radium::CoqName::Unnamed, radium::CoqType::Literal(refinement_type))];
+ let args = vec![radium::CoqParam::new(
+ radium::CoqName::Unnamed,
+ radium::CoqType::Literal(refinement_type),
+ false,
+ )];
+
(args, vec!["x".to_string()], "x".to_string())
};
let variant_def = radium::CoqVariant {
name: variant_name.to_string(),
- params: radium::CoqParamList(variant_args),
+ params: radium::CoqParamList::new(variant_args),
};
variants.push(variant_def);
@@ -1116,7 +1121,7 @@ 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 = radium::CoqInductive {
name: enum_name.to_string(),
- parameters: radium::CoqParamList(vec![]),
+ parameters: radium::CoqParamList::new(vec![]),
variants,
};