add constraint validation code (currently unused)

This commit is contained in:
Folkert 2021-05-05 21:35:49 +02:00
parent 86ffd430d7
commit b5c655c84d
3 changed files with 118 additions and 2 deletions

View file

@ -1,9 +1,9 @@
use crate::expected::{Expected, PExpected}; use crate::expected::{Expected, PExpected};
use roc_collections::all::SendMap; use roc_collections::all::{MutSet, SendMap};
use roc_module::symbol::Symbol; use roc_module::symbol::Symbol;
use roc_region::all::{Located, Region}; use roc_region::all::{Located, Region};
use roc_types::subs::Variable;
use roc_types::types::{Category, PatternCategory, Type}; use roc_types::types::{Category, PatternCategory, Type};
use roc_types::{subs::Variable, types::VariableDetail};
#[derive(Debug, Clone, PartialEq)] #[derive(Debug, Clone, PartialEq)]
pub enum Constraint { pub enum Constraint {
@ -25,3 +25,107 @@ pub struct LetConstraint {
pub defs_constraint: Constraint, pub defs_constraint: Constraint,
pub ret_constraint: Constraint, pub ret_constraint: Constraint,
} }
// VALIDATE
#[derive(Default, Clone)]
struct Declared {
pub rigid_vars: MutSet<Variable>,
pub flex_vars: MutSet<Variable>,
}
impl Constraint {
pub fn validate(&self) -> bool {
let mut unbound = Default::default();
validate_help(self, &Declared::default(), &mut unbound);
if !unbound.type_variables.is_empty() {
panic!("found unbound type variables {:?}", &unbound.type_variables);
}
if !unbound.lambda_set_variables.is_empty() {
panic!(
"found unbound lambda set variables {:?}",
&unbound.lambda_set_variables
);
}
if !unbound.recursion_variables.is_empty() {
panic!(
"found unbound recursion variables {:?}",
&unbound.recursion_variables
);
}
true
}
}
fn subtract(declared: &Declared, detail: &VariableDetail, accum: &mut VariableDetail) {
for var in &detail.type_variables {
if !(declared.rigid_vars.contains(&var) || declared.flex_vars.contains(&var)) {
accum.type_variables.insert(*var);
}
}
// lambda set variables are always flex
for var in &detail.lambda_set_variables {
if declared.rigid_vars.contains(&var.into_inner()) {
panic!("lambda set variable {:?} is declared as rigid", var);
}
if !declared.flex_vars.contains(&var.into_inner()) {
accum.lambda_set_variables.insert(*var);
}
}
// recursion vars should be always rigid
for var in &detail.recursion_variables {
if declared.flex_vars.contains(&var) {
panic!("recursion variable {:?} is declared as flex", var);
}
if !declared.rigid_vars.contains(&var) {
accum.recursion_variables.insert(*var);
}
}
}
fn validate_help(constraint: &Constraint, declared: &Declared, accum: &mut VariableDetail) {
use Constraint::*;
match constraint {
True | SaveTheEnvironment | Lookup(_, _, _) => { /* nothing */ }
Store(typ, var, _, _) => {
subtract(declared, &typ.variables_detail(), accum);
if !declared.flex_vars.contains(var) {
accum.type_variables.insert(*var);
}
}
Constraint::Eq(typ, expected, _, _) => {
subtract(declared, &typ.variables_detail(), accum);
subtract(declared, &expected.get_type_ref().variables_detail(), accum);
}
Constraint::Pattern(_, _, typ, expected) => {
subtract(declared, &typ.variables_detail(), accum);
subtract(declared, &expected.get_type_ref().variables_detail(), accum);
}
Constraint::Let(letcon) => {
let mut declared = declared.clone();
declared
.rigid_vars
.extend(letcon.rigid_vars.iter().copied());
declared.flex_vars.extend(letcon.flex_vars.iter().copied());
validate_help(&letcon.defs_constraint, &declared, accum);
validate_help(&letcon.ret_constraint, &declared, accum);
}
Constraint::And(inner) => {
for c in inner {
validate_help(c, declared, accum);
}
}
}
}

View file

@ -3221,6 +3221,10 @@ fn run_solve<'a>(
.. ..
} = module; } = module;
if false {
debug_assert!(constraint.validate(), "{:?}", &constraint);
}
let (solved_subs, solved_env, problems) = let (solved_subs, solved_env, problems) =
roc_solve::module::run_solve(aliases, rigid_variables, constraint, var_store); roc_solve::module::run_solve(aliases, rigid_variables, constraint, var_store);

View file

@ -850,6 +850,14 @@ pub struct VariableDetail {
pub recursion_variables: MutSet<Variable>, pub recursion_variables: MutSet<Variable>,
} }
impl VariableDetail {
pub fn is_empty(&self) -> bool {
self.type_variables.is_empty()
&& self.lambda_set_variables.is_empty()
&& self.recursion_variables.is_empty()
}
}
fn variables_help_detailed(tipe: &Type, accum: &mut VariableDetail) { fn variables_help_detailed(tipe: &Type, accum: &mut VariableDetail) {
use Type::*; use Type::*;