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 6e303e39e694bacd7beb2fa8bfc9f6ee0cb27f7a..f31f149a1a952a573e7feafcb726c4377b08f9fe 100644
--- a/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
@@ -40,7 +40,7 @@ impl<T: ParamLookup> parse::Parse<T> for EnumPattern {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
// parse the pattern
let pat: parse::LitStr = input.parse(meta)?;
- let (pat, _) = process_coq_literal(&pat.value(), meta);
+ let (pat, _) = meta.process_coq_literal(&pat.value());
let args: Vec<String> = if parse::Dollar::peek(input) {
// optionally parse args
@@ -53,7 +53,7 @@ impl<T: ParamLookup> parse::Parse<T> for EnumPattern {
parsed_args
.into_iter()
.map(|s| {
- let (arg, _) = process_coq_literal(&s.value(), meta);
+ let (arg, _) = meta.process_coq_literal(&s.value());
arg
})
.collect()
@@ -98,7 +98,7 @@ impl<'b, T: ParamLookup> EnumSpecParser for VerboseEnumSpecParser<'b, T> {
match seg.ident.name.as_str() {
"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);
+ let (ty, _) = self.scope.process_coq_literal(ty.value().as_str());
rfn_type = Some(coq::term::Type::Literal(ty));
},
"export_as" => {},
@@ -127,7 +127,7 @@ impl<'b, T: ParamLookup> EnumSpecParser for VerboseEnumSpecParser<'b, T> {
},
"refinement" => {
let rfn: parse::LitStr = buffer.parse(self.scope).map_err(str_err)?;
- let (rfn, _) = process_coq_literal(rfn.value().as_str(), self.scope);
+ let (rfn, _) = self.scope.process_coq_literal(rfn.value().as_str());
refinement = Some(rfn);
},
_ => {
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 74bb004643bf9afcd300310e57970c058d39a926..661ba0607aa0e7b29d4c920c5545d31a80b1c973 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -77,7 +77,7 @@ impl<T: ParamLookup> parse::Parse<T> for LiteralTypeWithRef {
if parse::At::peek(input) {
input.parse::<_, MToken![@]>(meta)?;
let ty: parse::LitStr = input.parse(meta)?;
- let (ty, meta) = process_coq_literal(&ty.value(), meta);
+ let (ty, meta) = meta.process_coq_literal(&ty.value());
Ok(Self {
rfn,
@@ -106,7 +106,7 @@ pub struct LiteralType {
impl<T: ParamLookup> parse::Parse<T> for LiteralType {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
let ty: parse::LitStr = input.parse(meta)?;
- let (ty, meta) = process_coq_literal(&ty.value(), meta);
+ let (ty, meta) = meta.process_coq_literal(&ty.value());
Ok(Self { ty, meta })
}
@@ -124,7 +124,7 @@ impl From<IProp> for specs::IProp {
impl<T: ParamLookup> parse::Parse<T> for IProp {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
let lit: parse::LitStr = input.parse(meta)?;
- let (lit, _) = process_coq_literal(&lit.value(), meta);
+ let (lit, _) = meta.process_coq_literal(&lit.value());
Ok(Self(specs::IProp::Atom(lit)))
}
@@ -137,7 +137,7 @@ pub struct RRCoqType {
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, _) = meta.process_coq_literal(&ty.value());
let ty = coq::term::Type::Literal(ty);
Ok(Self { ty })
}
@@ -226,7 +226,7 @@ pub struct RRCoqContextItem {
impl<T: ParamLookup> parse::Parse<T> for RRCoqContextItem {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
let item: parse::LitStr = input.parse(meta)?;
- let (item_str, annot_meta) = process_coq_literal(&item.value(), meta);
+ let (item_str, annot_meta) = meta.process_coq_literal(&item.value());
let at_end = !annot_meta.is_empty();
@@ -257,174 +257,174 @@ pub fn str_err(e: parse::Error) -> String {
format!("{:?}", e)
}
+/// Handle escape sequences in the given string.
+fn handle_escapes(s: &str) -> String {
+ String::from(s).replace("\\\"", "\"")
+}
+
/// Lookup of lifetime and type parameters given their Rust source names.
pub trait ParamLookup {
fn lookup_ty_param(&self, path: &[&str]) -> Option<&specs::LiteralTyParam>;
fn lookup_lft(&self, lft: &str) -> Option<&specs::Lft>;
fn lookup_literal(&self, path: &[&str]) -> Option<&str>;
-}
-
-/// Handle escape sequences in the given string.
-pub fn handle_escapes(s: &str) -> String {
- String::from(s).replace("\\\"", "\"")
-}
-/// Processes a literal Coq term annotated via an attribute.
-/// In particular, processes escapes `{...}` and replaces them via their interpretation, see
-/// below for supported escape sequences.
-///
-/// Supported interpretations:
-/// - `{{...}}` is replaced by `{...}`
-/// - `{ty_of T}` is replaced by the type for the type parameter `T`
-/// - `{rt_of T}` is replaced by the refinement type of the type parameter `T`
-/// - `{st_of T}` is replaced by the syntactic type of the type parameter `T`
-/// - `{ly_of T}` is replaced by a term giving the layout of the type parameter `T`'s syntactic type
-/// - `{'a}` is replaced by a term corresponding to the lifetime parameter 'a
-pub fn process_coq_literal<T: ParamLookup>(s: &str, meta: &T) -> (String, specs::TypeAnnotMeta) {
- let mut literal_lfts: HashSet<String> = HashSet::new();
- let mut literal_tyvars: HashSet<specs::LiteralTyParam> = HashSet::new();
-
- // TODOs:
- // - associated types, we should split them here already. We need to adjust the matching to accept :: and
- // then split
- // - lookup other literals in ParamLookup
-
- let s = handle_escapes(s);
-
- /* regexes:
- * - '{\s*rt_of\s+([[:alpha:]])\s*}' replace by lookup of the refinement type name
- * - '{\s*st_of\s+([[:alpha:]])\s*}' replace by lookup of the syntype name
- * - '{\s*ly_of\s+([[:alpha:]])\s*}' replace by "use_layout_alg' st"
- * - '{\s*ty_of\s+([[:alpha:]])\s*}' replace by the type name
- * - '{\s*'([[:alpha:]])\s*}' replace by lookup of the lifetime name
- * - '{{(.*)}}' replace by the contents
- *
- * Note: the leading regex ([^{]|^) is supposed to rule out leading {, for the RE_LIT rule.
- */
- // compile these just once, not for every invocation of the method
- lazy_static! {
- //(::[[:alpha:]]*)?
- static ref RE_RT_OF: Regex = Regex::new(r"([^{]|^)\{\s*rt_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
- static ref RE_ST_OF: Regex = Regex::new(r"([^{]|^)\{\s*st_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
- static ref RE_LY_OF: Regex = Regex::new(r"([^{]|^)\{\s*ly_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
- static ref RE_TY_OF: Regex = Regex::new(r"([^{]|^)\{\s*ty_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
- static ref RE_LFT_OF: Regex = Regex::new(r"([^{]|^)\{\s*'([[:alpha:]]+)\s*\}").unwrap();
-
- static ref RE_LIT: Regex = Regex::new(r"([^{]|^)\{\s*([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
-
- static ref RE_DIRECT: Regex = Regex::new(r"\{(\{.*\})\}").unwrap();
- }
+ /// Processes a literal Coq term annotated via an attribute.
+ /// In particular, processes escapes `{...}` and replaces them via their interpretation, see
+ /// below for supported escape sequences.
+ ///
+ /// Supported interpretations:
+ /// - `{{...}}` is replaced by `{...}`
+ /// - `{ty_of T}` is replaced by the type for the type parameter `T`
+ /// - `{rt_of T}` is replaced by the refinement type of the type parameter `T`
+ /// - `{st_of T}` is replaced by the syntactic type of the type parameter `T`
+ /// - `{ly_of T}` is replaced by a term giving the layout of the type parameter `T`'s syntactic type
+ /// - `{'a}` is replaced by a term corresponding to the lifetime parameter 'a
+ fn process_coq_literal(&self, s: &str) -> (String, specs::TypeAnnotMeta) {
+ let mut literal_lfts: HashSet<String> = HashSet::new();
+ let mut literal_tyvars: HashSet<specs::LiteralTyParam> = HashSet::new();
+
+ // TODOs:
+ // - associated types, we should split them here already. We need to adjust the matching to accept ::
+ // and then split
+ // - lookup other literals in ParamLookup
+
+ let s = handle_escapes(s);
+
+ /* regexes:
+ * - '{\s*rt_of\s+([[:alpha:]])\s*}' replace by lookup of the refinement type name
+ * - '{\s*st_of\s+([[:alpha:]])\s*}' replace by lookup of the syntype name
+ * - '{\s*ly_of\s+([[:alpha:]])\s*}' replace by "use_layout_alg' st"
+ * - '{\s*ty_of\s+([[:alpha:]])\s*}' replace by the type name
+ * - '{\s*'([[:alpha:]])\s*}' replace by lookup of the lifetime name
+ * - '{{(.*)}}' replace by the contents
+ *
+ * Note: the leading regex ([^{]|^) is supposed to rule out leading {, for the RE_LIT rule.
+ */
+ // compile these just once, not for every invocation of the method
+ lazy_static! {
+ //(::[[:alpha:]]*)?
+ static ref RE_RT_OF: Regex = Regex::new(r"([^{]|^)\{\s*rt_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
+ static ref RE_ST_OF: Regex = Regex::new(r"([^{]|^)\{\s*st_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
+ static ref RE_LY_OF: Regex = Regex::new(r"([^{]|^)\{\s*ly_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
+ static ref RE_TY_OF: Regex = Regex::new(r"([^{]|^)\{\s*ty_of\s+([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
+ static ref RE_LFT_OF: Regex = Regex::new(r"([^{]|^)\{\s*'([[:alpha:]]+)\s*\}").unwrap();
+
+ static ref RE_LIT: Regex = Regex::new(r"([^{]|^)\{\s*([[:alpha:]]+)(::([[:alpha:]]+))?\s*\}").unwrap();
+
+ static ref RE_DIRECT: Regex = Regex::new(r"\{(\{.*\})\}").unwrap();
+ }
- let cs = &s;
- let cs = RE_RT_OF.replace_all(cs, |c: &Captures<'_>| {
- let mut path = Vec::new();
- path.push(&c[2]);
+ let cs = &s;
+ let cs = RE_RT_OF.replace_all(cs, |c: &Captures<'_>| {
+ let mut path = Vec::new();
+ path.push(&c[2]);
- if let Some(t2) = c.get(4) {
- path.push(t2.as_str());
- }
+ if let Some(t2) = c.get(4) {
+ path.push(t2.as_str());
+ }
- let param = meta.lookup_ty_param(&path);
+ let param = self.lookup_ty_param(&path);
- let Some(param) = param else {
- return "ERR".to_owned();
- };
+ let Some(param) = param else {
+ return "ERR".to_owned();
+ };
- literal_tyvars.insert(param.clone());
- format!("{}{}", &c[1], ¶m.refinement_type)
- });
+ literal_tyvars.insert(param.clone());
+ format!("{}{}", &c[1], ¶m.refinement_type)
+ });
- let cs = RE_ST_OF.replace_all(&cs, |c: &Captures<'_>| {
- let mut path = Vec::new();
- path.push(&c[2]);
+ let cs = RE_ST_OF.replace_all(&cs, |c: &Captures<'_>| {
+ let mut path = Vec::new();
+ path.push(&c[2]);
- if let Some(t2) = c.get(4) {
- path.push(t2.as_str());
- }
- let param = meta.lookup_ty_param(&path);
+ if let Some(t2) = c.get(4) {
+ path.push(t2.as_str());
+ }
+ let param = self.lookup_ty_param(&path);
- let Some(param) = param else {
- return "ERR".to_owned();
- };
+ let Some(param) = param else {
+ return "ERR".to_owned();
+ };
- literal_tyvars.insert(param.clone());
- format!("{}(ty_syn_type {})", &c[1], ¶m.type_term)
- });
+ literal_tyvars.insert(param.clone());
+ format!("{}(ty_syn_type {})", &c[1], ¶m.type_term)
+ });
- let cs = RE_LY_OF.replace_all(&cs, |c: &Captures<'_>| {
- let mut path = Vec::new();
- path.push(&c[2]);
+ let cs = RE_LY_OF.replace_all(&cs, |c: &Captures<'_>| {
+ let mut path = Vec::new();
+ path.push(&c[2]);
- if let Some(t2) = c.get(4) {
- path.push(t2.as_str());
- }
- let param = meta.lookup_ty_param(&path);
+ if let Some(t2) = c.get(4) {
+ path.push(t2.as_str());
+ }
+ let param = self.lookup_ty_param(&path);
- let Some(param) = param else {
- return "ERR".to_owned();
- };
+ let Some(param) = param else {
+ return "ERR".to_owned();
+ };
- literal_tyvars.insert(param.clone());
- format!("{}(use_layout_alg' (ty_syn_type {}))", &c[1], ¶m.type_term)
- });
+ literal_tyvars.insert(param.clone());
+ format!("{}(use_layout_alg' (ty_syn_type {}))", &c[1], ¶m.type_term)
+ });
- let cs = RE_TY_OF.replace_all(&cs, |c: &Captures<'_>| {
- let mut path = Vec::new();
- path.push(&c[2]);
+ let cs = RE_TY_OF.replace_all(&cs, |c: &Captures<'_>| {
+ let mut path = Vec::new();
+ path.push(&c[2]);
- if let Some(t2) = c.get(4) {
- path.push(t2.as_str());
- }
- let param = meta.lookup_ty_param(&path);
+ if let Some(t2) = c.get(4) {
+ path.push(t2.as_str());
+ }
+ let param = self.lookup_ty_param(&path);
- let Some(param) = param else {
- return "ERR".to_owned();
- };
+ let Some(param) = param else {
+ return "ERR".to_owned();
+ };
- literal_tyvars.insert(param.clone());
- format!("{}{}", &c[1], ¶m.type_term)
- });
+ literal_tyvars.insert(param.clone());
+ format!("{}{}", &c[1], ¶m.type_term)
+ });
- let cs = RE_LFT_OF.replace_all(&cs, |c: &Captures<'_>| {
- let t = &c[2];
- let lft = meta.lookup_lft(t);
+ let cs = RE_LFT_OF.replace_all(&cs, |c: &Captures<'_>| {
+ let t = &c[2];
+ let lft = self.lookup_lft(t);
- let Some(lft) = lft else {
- return "ERR".to_owned();
- };
+ let Some(lft) = lft else {
+ return "ERR".to_owned();
+ };
- literal_lfts.insert(lft.clone());
- format!("{}{}", &c[1], lft)
- });
+ literal_lfts.insert(lft.clone());
+ format!("{}{}", &c[1], lft)
+ });
- let cs = RE_LIT.replace_all(&cs, |c: &Captures<'_>| {
- let mut path = Vec::new();
- path.push(&c[2]);
- if let Some(t2) = c.get(4) {
- path.push(t2.as_str());
- }
+ let cs = RE_LIT.replace_all(&cs, |c: &Captures<'_>| {
+ let mut path = Vec::new();
+ path.push(&c[2]);
+ if let Some(t2) = c.get(4) {
+ path.push(t2.as_str());
+ }
- // first lookup literals
- let lit = meta.lookup_literal(&path);
+ // first lookup literals
+ let lit = self.lookup_literal(&path);
- if let Some(lit) = lit {
- return format!("{}{}", &c[1], lit);
- }
+ if let Some(lit) = lit {
+ return format!("{}{}", &c[1], lit);
+ }
- // else interpret it as ty_of
- let ty = meta.lookup_ty_param(&path);
+ // else interpret it as ty_of
+ let ty = self.lookup_ty_param(&path);
- let Some(ty) = ty else {
- return "ERR".to_owned();
- };
+ let Some(ty) = ty else {
+ return "ERR".to_owned();
+ };
- literal_tyvars.insert(ty.clone());
- format!("{}{}", &c[1], &ty.type_term)
- });
+ literal_tyvars.insert(ty.clone());
+ format!("{}{}", &c[1], &ty.type_term)
+ });
- let cs = RE_DIRECT.replace_all(&cs, |c: &Captures<'_>| c[1].to_string());
+ let cs = RE_DIRECT.replace_all(&cs, |c: &Captures<'_>| c[1].to_string());
- (cs.to_string(), specs::TypeAnnotMeta::new(literal_tyvars, literal_lfts))
+ (cs.to_string(), specs::TypeAnnotMeta::new(literal_tyvars, literal_lfts))
+ }
}
#[cfg(test)]
@@ -472,7 +472,7 @@ mod tests {
let mut scope = TestScope::default();
scope.ty_names.insert("T".to_owned(), radium::LiteralTyParam::new("T", "T"));
- let (res, _) = super::process_coq_literal(lit, &scope);
+ let (res, _) = scope.process_coq_literal(lit);
assert_eq!(res, "T_rt * T_rt");
}
@@ -482,7 +482,7 @@ mod tests {
let mut scope = TestScope::default();
scope.ty_names.insert("T".to_owned(), radium::LiteralTyParam::new("T", "T"));
- let (res, _) = super::process_coq_literal(lit, &scope);
+ let (res, _) = scope.process_coq_literal(lit);
assert_eq!(res, "T_ty * T_ty");
}
@@ -492,7 +492,7 @@ mod tests {
let mut scope = TestScope::default();
scope.ty_names.insert("Self".to_owned(), radium::LiteralTyParam::new("Self", "Self"));
- let (res, _) = super::process_coq_literal(lit, &scope);
+ let (res, _) = scope.process_coq_literal(lit);
assert_eq!(res, "Self_rt * Self_rt");
}
@@ -502,7 +502,7 @@ mod tests {
let mut scope = TestScope::default();
scope.ty_names.insert("Self".to_owned(), radium::LiteralTyParam::new("Self", "Self"));
- let (res, _) = super::process_coq_literal(lit, &scope);
+ let (res, _) = scope.process_coq_literal(lit);
assert_eq!(res, "{rt_of Bla}");
}
@@ -516,7 +516,7 @@ mod tests {
radium::LiteralTyParam::new("Bla_Blub", "Bla_Blub"),
);
- let (res, _) = super::process_coq_literal(lit, &scope);
+ let (res, _) = scope.process_coq_literal(lit);
assert_eq!(res, "Bla_Blub_rt");
}
@@ -526,7 +526,7 @@ mod tests {
let mut scope = TestScope::default();
scope.literals.insert(vec!["Size".to_owned()], "(trait_attrs).(size)".to_owned());
- let (res, _) = super::process_coq_literal(lit, &scope);
+ let (res, _) = scope.process_coq_literal(lit);
assert_eq!(res, "(trait_attrs).(size) 4");
}
}
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 a7622a512f97b92e1daa125485102535c09989b3..7c80c88a6b8d39e8a78047480595599fb7cb5da0 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -45,13 +45,13 @@ struct RfnPattern {
impl<T: ParamLookup> parse::Parse<T> for RfnPattern {
fn parse(input: parse::Stream, meta: &T) -> parse::Result<Self> {
let pat = parse::LitStr::parse(input, meta)?;
- let (pat, _) = process_coq_literal(pat.value().as_str(), meta);
+ let (pat, _) = meta.process_coq_literal(pat.value().as_str());
// optionally, parse a type annotation (otherwise, let Coq inference do its thing)
if parse::Colon::peek(input) {
input.parse::<_, MToken![:]>(meta)?;
let ty: parse::LitStr = input.parse(meta)?;
- let (ty, _) = process_coq_literal(ty.value().as_str(), meta);
+ let (ty, _) = meta.process_coq_literal(ty.value().as_str());
Ok(Self {
rfn_pat: pat,
rfn_type: Some(coq::term::Type::Literal(ty)),
@@ -102,19 +102,19 @@ impl<T: ParamLookup> parse::Parse<T> for MetaIProp {
"type" => {
let loc_str: parse::LitStr = input.parse(meta)?;
- let (loc_str, mut annot_meta) = process_coq_literal(&loc_str.value(), meta);
+ let (loc_str, mut annot_meta) = meta.process_coq_literal(&loc_str.value());
input.parse::<_, MToken![:]>(meta)?;
let rfn_str: parse::LitStr = input.parse(meta)?;
- let (rfn_str, annot_meta2) = process_coq_literal(&rfn_str.value(), meta);
+ let (rfn_str, annot_meta2) = meta.process_coq_literal(&rfn_str.value());
annot_meta.join(&annot_meta2);
input.parse::<_, MToken![@]>(meta)?;
let type_str: parse::LitStr = input.parse(meta)?;
- let (type_str, annot_meta3) = process_coq_literal(&type_str.value(), meta);
+ let (type_str, annot_meta3) = meta.process_coq_literal(&type_str.value());
annot_meta.join(&annot_meta3);
@@ -136,13 +136,13 @@ impl<T: ParamLookup> parse::Parse<T> for MetaIProp {
input.parse::<_, MToken![:]>(meta)?;
let pure_prop: parse::LitStr = input.parse(meta)?;
- let (pure_str, _annot_meta) = process_coq_literal(&pure_prop.value(), meta);
+ let (pure_str, _annot_meta) = meta.process_coq_literal(&pure_prop.value());
// TODO: should we use annot_meta?
Ok(Self::Pure(pure_str, Some(name_str)))
} else {
// this is a
- let (lit, _) = process_coq_literal(&name_or_prop_str.value(), meta);
+ let (lit, _) = meta.process_coq_literal(&name_or_prop_str.value());
Ok(Self::Pure(lit, None))
}
}
@@ -410,7 +410,7 @@ where
if self.expect_rfn {
let rfn: parse::LitStr = buffer.parse(self.scope).map_err(str_err)?;
- let (rfn, _) = process_coq_literal(rfn.value().as_str(), self.scope);
+ let (rfn, _) = self.scope.process_coq_literal(rfn.value().as_str());
parsed_rfn = Some(rfn);
if parse::At::peek(&buffer) {
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 d6afa9d0657fade8410ffab92aa8978f61e13e1a..ce8d2909d47d53f121741c81d134d4244777b233 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
@@ -55,7 +55,7 @@ impl<'b, T: ParamLookup> TraitImplAttrParser for VerboseTraitImplAttrParser<'b,
buffer.parse::<_, MToken![:]>(&()).map_err(str_err)?;
buffer.parse::<_, MToken![=]>(&()).map_err(str_err)?;
let parsed_term: parse::LitStr = buffer.parse(self.scope).map_err(str_err)?;
- let (parsed_term, _) = process_coq_literal(&parsed_term.value(), self.scope);
+ let (parsed_term, _) = self.scope.process_coq_literal(&parsed_term.value());
if trait_attrs
.insert(parsed_name.to_string(), radium::coq::term::Gallina::Literal(parsed_term))
.is_some()
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 76226758a0cdf266302e7774b521fc61e331a9e2..a631873aa8d8781c77242ca85d81b79472d53e90 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
@@ -141,19 +141,19 @@ impl<T: ParamLookup> parse::Parse<T> for MetaIProp {
match macro_cmd.value().as_str() {
"type" => {
let loc_str: parse::LitStr = input.parse(meta)?;
- let (loc_str, mut annot_meta) = process_coq_literal(&loc_str.value(), meta);
+ let (loc_str, mut annot_meta) = meta.process_coq_literal(&loc_str.value());
input.parse::<_, MToken![:]>(meta)?;
let rfn_str: parse::LitStr = input.parse(meta)?;
- let (rfn_str, annot_meta2) = process_coq_literal(&rfn_str.value(), meta);
+ let (rfn_str, annot_meta2) = meta.process_coq_literal(&rfn_str.value());
annot_meta.join(&annot_meta2);
input.parse::<_, MToken![@]>(meta)?;
let type_str: parse::LitStr = input.parse(meta)?;
- let (type_str, annot_meta3) = process_coq_literal(&type_str.value(), meta);
+ let (type_str, annot_meta3) = meta.process_coq_literal(&type_str.value());
annot_meta.join(&annot_meta3);
let spec = specs::TyOwnSpec::new(loc_str, rfn_str, type_str, false, annot_meta);
@@ -168,13 +168,13 @@ impl<T: ParamLookup> parse::Parse<T> for MetaIProp {
input.parse::<_, MToken![:]>(meta)?;
let term: parse::LitStr = input.parse(meta)?;
- let (term, _meta) = process_coq_literal(&term.value(), meta);
+ let (term, _meta) = meta.process_coq_literal(&term.value());
Ok(Self::Observe(gname.value(), term))
},
"linktime" => {
let term: parse::LitStr = input.parse(meta)?;
- let (term, _meta) = process_coq_literal(&term.value(), meta);
+ let (term, _meta) = meta.process_coq_literal(&term.value());
Ok(Self::Linktime(term))
},
_ => Err(parse::Error::OtherErr(
@@ -191,13 +191,13 @@ impl<T: ParamLookup> parse::Parse<T> for MetaIProp {
input.parse::<_, MToken![:]>(meta)?;
let pure_prop: parse::LitStr = input.parse(meta)?;
- let (pure_str, _annot_meta) = process_coq_literal(&pure_prop.value(), meta);
+ let (pure_str, _annot_meta) = meta.process_coq_literal(&pure_prop.value());
// TODO: should we use annot_meta?
Ok(Self::Pure(pure_str, Some(name_str)))
} else {
// this is a
- let (lit, _) = process_coq_literal(&name_or_prop_str.value(), meta);
+ let (lit, _) = meta.process_coq_literal(&name_or_prop_str.value());
Ok(Self::Pure(lit, None))
}
}
@@ -388,7 +388,7 @@ where
buffer.parse::<_, MToken![:]>(scope)?;
let term: parse::LitStr = buffer.parse(scope)?;
- let (term, _) = process_coq_literal(&term.value(), scope);
+ let (term, _) = scope.process_coq_literal(&term.value());
Ok(MetaIProp::Observe(gname.value(), term))
};
let m = m().map_err(str_err)?;