Skip to content
Snippets Groups Projects
Verified Commit 8add0d16 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

make process_coq_literal a method

parent c2dd80f7
No related branches found
No related tags found
1 merge request!62Support trait attributes in more places + lifetime solver improvements
Hide whitespace changes
Inline Side-by-side
Showing
with 166 additions and 166 deletions
rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs
+ 4
− 4
View file @ 8add0d16
......@@ -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);
},
_ => {
......
rr_frontend/translation/src/spec_parsers/parse_utils.rs
+ 145
− 145
View file @ 8add0d16
......@@ -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], &param.refinement_type)
});
literal_tyvars.insert(param.clone());
format!("{}{}", &c[1], &param.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], &param.type_term)
});
literal_tyvars.insert(param.clone());
format!("{}(ty_syn_type {})", &c[1], &param.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], &param.type_term)
});
literal_tyvars.insert(param.clone());
format!("{}(use_layout_alg' (ty_syn_type {}))", &c[1], &param.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], &param.type_term)
});
literal_tyvars.insert(param.clone());
format!("{}{}", &c[1], &param.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");
}
}
rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+ 8
− 8
View file @ 8add0d16
......@@ -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) {
......
rr_frontend/translation/src/spec_parsers/trait_impl_attr_parser.rs
+ 1
− 1
View file @ 8add0d16
......@@ -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()
......
rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+ 8
− 8
View file @ 8add0d16
......@@ -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)?;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment