ISLE: handle out-of-order extern converter decls. (#4079)
This fixes a bug where the ISLE compiler would refuse to accept out-of-order declarations in the order of: (i) use of an implicit conversion backed by an extern constructor; (ii) extern declaration for that constructor. The issue was one of phase separation: we were capturing and noting "extern constructor" status on terms in the same pass in which we were typechecking and resolving implicit conversions. Given this knowledge, the fix is straightforward: externs are picked up in a prior pass.
This commit is contained in:
@@ -0,0 +1,22 @@
|
|||||||
|
(type T (primitive T))
|
||||||
|
(type U (primitive U))
|
||||||
|
(type V (primitive V))
|
||||||
|
|
||||||
|
(convert T U t_to_u)
|
||||||
|
|
||||||
|
(type Result (enum (T (u U) (v V))))
|
||||||
|
|
||||||
|
;; Use the implicit converter before the underlying constructor is
|
||||||
|
;; declared (below). Also use one of the conversions before it is
|
||||||
|
;; declared (below).
|
||||||
|
(decl entry (T) Result)
|
||||||
|
(rule (entry t)
|
||||||
|
(Result.T t t))
|
||||||
|
|
||||||
|
(convert T V t_to_v)
|
||||||
|
|
||||||
|
(decl t_to_u (T) U)
|
||||||
|
(extern constructor t_to_u t_to_u)
|
||||||
|
|
||||||
|
(decl t_to_v (T) V)
|
||||||
|
(rule (t_to_v _) 0)
|
||||||
@@ -793,6 +793,8 @@ impl TermEnv {
|
|||||||
tyenv.return_errors()?;
|
tyenv.return_errors()?;
|
||||||
env.collect_converters(tyenv, defs);
|
env.collect_converters(tyenv, defs);
|
||||||
tyenv.return_errors()?;
|
tyenv.return_errors()?;
|
||||||
|
env.collect_externs(tyenv, defs);
|
||||||
|
tyenv.return_errors()?;
|
||||||
env.collect_rules(tyenv, defs);
|
env.collect_rules(tyenv, defs);
|
||||||
env.check_for_undefined_decls(tyenv, defs);
|
env.check_for_undefined_decls(tyenv, defs);
|
||||||
env.check_for_expr_terms_without_constructors(tyenv, defs);
|
env.check_for_expr_terms_without_constructors(tyenv, defs);
|
||||||
@@ -1164,64 +1166,9 @@ impl TermEnv {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn collect_rules(&mut self, tyenv: &mut TypeEnv, defs: &ast::Defs) {
|
fn collect_externs(&mut self, tyenv: &mut TypeEnv, defs: &ast::Defs) {
|
||||||
for def in &defs.defs {
|
for def in &defs.defs {
|
||||||
match def {
|
match def {
|
||||||
&ast::Def::Rule(ref rule) => {
|
|
||||||
let pos = rule.pos;
|
|
||||||
let mut bindings = Bindings {
|
|
||||||
next_var: 0,
|
|
||||||
vars: vec![],
|
|
||||||
};
|
|
||||||
|
|
||||||
let rule_term = match rule.pattern.root_term() {
|
|
||||||
Some(name) => {
|
|
||||||
let sym = tyenv.intern_mut(name);
|
|
||||||
match self.term_map.get(&sym) {
|
|
||||||
Some(term) => *term,
|
|
||||||
None => {
|
|
||||||
tyenv.report_error(
|
|
||||||
pos,
|
|
||||||
"Cannot define a rule for an unknown term".to_string(),
|
|
||||||
);
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
None => {
|
|
||||||
tyenv.report_error(
|
|
||||||
pos,
|
|
||||||
"Rule does not have a term at the root of its left-hand side"
|
|
||||||
.to_string(),
|
|
||||||
);
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let (lhs, ty) = unwrap_or_continue!(self.translate_pattern(
|
|
||||||
tyenv,
|
|
||||||
rule_term,
|
|
||||||
&rule.pattern,
|
|
||||||
None,
|
|
||||||
&mut bindings,
|
|
||||||
/* is_root = */ true,
|
|
||||||
));
|
|
||||||
let rhs = unwrap_or_continue!(self.translate_expr(
|
|
||||||
tyenv,
|
|
||||||
&rule.expr,
|
|
||||||
ty,
|
|
||||||
&mut bindings
|
|
||||||
));
|
|
||||||
|
|
||||||
let rid = RuleId(self.rules.len());
|
|
||||||
self.rules.push(Rule {
|
|
||||||
id: rid,
|
|
||||||
lhs,
|
|
||||||
rhs,
|
|
||||||
prio: rule.prio,
|
|
||||||
pos,
|
|
||||||
});
|
|
||||||
}
|
|
||||||
&ast::Def::Extern(ast::Extern::Constructor {
|
&ast::Def::Extern(ast::Extern::Constructor {
|
||||||
ref term,
|
ref term,
|
||||||
ref func,
|
ref func,
|
||||||
@@ -1356,6 +1303,69 @@ impl TermEnv {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn collect_rules(&mut self, tyenv: &mut TypeEnv, defs: &ast::Defs) {
|
||||||
|
for def in &defs.defs {
|
||||||
|
match def {
|
||||||
|
&ast::Def::Rule(ref rule) => {
|
||||||
|
let pos = rule.pos;
|
||||||
|
let mut bindings = Bindings {
|
||||||
|
next_var: 0,
|
||||||
|
vars: vec![],
|
||||||
|
};
|
||||||
|
|
||||||
|
let rule_term = match rule.pattern.root_term() {
|
||||||
|
Some(name) => {
|
||||||
|
let sym = tyenv.intern_mut(name);
|
||||||
|
match self.term_map.get(&sym) {
|
||||||
|
Some(term) => *term,
|
||||||
|
None => {
|
||||||
|
tyenv.report_error(
|
||||||
|
pos,
|
||||||
|
"Cannot define a rule for an unknown term".to_string(),
|
||||||
|
);
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
None => {
|
||||||
|
tyenv.report_error(
|
||||||
|
pos,
|
||||||
|
"Rule does not have a term at the root of its left-hand side"
|
||||||
|
.to_string(),
|
||||||
|
);
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
let (lhs, ty) = unwrap_or_continue!(self.translate_pattern(
|
||||||
|
tyenv,
|
||||||
|
rule_term,
|
||||||
|
&rule.pattern,
|
||||||
|
None,
|
||||||
|
&mut bindings,
|
||||||
|
/* is_root = */ true,
|
||||||
|
));
|
||||||
|
let rhs = unwrap_or_continue!(self.translate_expr(
|
||||||
|
tyenv,
|
||||||
|
&rule.expr,
|
||||||
|
ty,
|
||||||
|
&mut bindings
|
||||||
|
));
|
||||||
|
|
||||||
|
let rid = RuleId(self.rules.len());
|
||||||
|
self.rules.push(Rule {
|
||||||
|
id: rid,
|
||||||
|
lhs,
|
||||||
|
rhs,
|
||||||
|
prio: rule.prio,
|
||||||
|
pos,
|
||||||
|
});
|
||||||
|
}
|
||||||
|
_ => {}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn check_for_undefined_decls(&self, tyenv: &mut TypeEnv, defs: &ast::Defs) {
|
fn check_for_undefined_decls(&self, tyenv: &mut TypeEnv, defs: &ast::Defs) {
|
||||||
for def in &defs.defs {
|
for def in &defs.defs {
|
||||||
if let ast::Def::Decl(decl) = def {
|
if let ast::Def::Decl(decl) = def {
|
||||||
|
|||||||
Reference in New Issue
Block a user