ISLE: add a missing type check for whether terms used in expressions have a constructor
This commit is contained in:
@@ -338,6 +338,25 @@ impl Expr {
|
|||||||
| &Expr::Let { pos, .. } => pos,
|
| &Expr::Let { pos, .. } => pos,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Call `f` for each of the terms in this expression.
|
||||||
|
pub fn terms(&self, f: &mut dyn FnMut(Pos, &Ident)) {
|
||||||
|
match self {
|
||||||
|
Expr::Term { sym, args, pos } => {
|
||||||
|
f(*pos, sym);
|
||||||
|
for arg in args {
|
||||||
|
arg.terms(f);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Expr::Let { defs, body, .. } => {
|
||||||
|
for def in defs {
|
||||||
|
def.val.terms(f);
|
||||||
|
}
|
||||||
|
body.terms(f);
|
||||||
|
}
|
||||||
|
Expr::Var { .. } | Expr::ConstInt { .. } | Expr::ConstPrim { .. } => {}
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// One variable locally bound in a `(let ...)` expression.
|
/// One variable locally bound in a `(let ...)` expression.
|
||||||
|
|||||||
@@ -767,6 +767,7 @@ impl TermEnv {
|
|||||||
tyenv.return_errors()?;
|
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);
|
||||||
tyenv.return_errors()?;
|
tyenv.return_errors()?;
|
||||||
|
|
||||||
Ok(env)
|
Ok(env)
|
||||||
@@ -1283,6 +1284,28 @@ impl TermEnv {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn check_for_expr_terms_without_constructors(&self, tyenv: &mut TypeEnv, defs: &ast::Defs) {
|
||||||
|
for def in &defs.defs {
|
||||||
|
if let ast::Def::Rule(rule) = def {
|
||||||
|
rule.expr.terms(&mut |pos, ident| {
|
||||||
|
let sym = tyenv.intern_mut(ident);
|
||||||
|
let term = self.term_map[&sym];
|
||||||
|
let term = &self.terms[term.index()];
|
||||||
|
if !term.has_constructor() {
|
||||||
|
tyenv.report_error(
|
||||||
|
pos,
|
||||||
|
format!(
|
||||||
|
"term `{}` cannot be used in an expression because \
|
||||||
|
it does not have a constructor",
|
||||||
|
ident.0
|
||||||
|
),
|
||||||
|
)
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn translate_pattern(
|
fn translate_pattern(
|
||||||
&self,
|
&self,
|
||||||
tyenv: &mut TypeEnv,
|
tyenv: &mut TypeEnv,
|
||||||
|
|||||||
Reference in New Issue
Block a user