feat(exhaustiveness): algorithm U borrowed from elm

This commit is contained in:
rvcas 2023-07-21 15:30:52 -04:00 committed by Lucas
parent 55887d3a45
commit 03efb46e6f
2 changed files with 551 additions and 10 deletions

View File

@ -1,15 +1,15 @@
use crate::ast::TypedPattern;
use std::{cmp::Ordering, collections::HashMap, sync::Arc}; use std::{cmp::Ordering, collections::HashMap, sync::Arc};
use vec1::Vec1; use vec1::Vec1;
mod usefulness;
use crate::{ use crate::{
ast::{ ast::{
Annotation, Arg, ArgName, AssignmentKind, BinOp, ByteArrayFormatPreference, CallArg, Annotation, Arg, ArgName, AssignmentKind, BinOp, ByteArrayFormatPreference, CallArg,
ClauseGuard, Constant, IfBranch, RecordUpdateSpread, Span, TraceKind, Tracing, TypedArg, ClauseGuard, Constant, IfBranch, RecordUpdateSpread, Span, TraceKind, Tracing, TypedArg,
TypedCallArg, TypedClause, TypedClauseGuard, TypedIfBranch, TypedRecordUpdateArg, UnOp, TypedCallArg, TypedClause, TypedClauseGuard, TypedIfBranch, TypedPattern,
UntypedArg, UntypedClause, UntypedClauseGuard, UntypedIfBranch, UntypedPattern, TypedRecordUpdateArg, UnOp, UntypedArg, UntypedClause, UntypedClauseGuard, UntypedIfBranch,
UntypedRecordUpdateArg, UntypedPattern, UntypedRecordUpdateArg,
}, },
builtins::{bool, byte_array, function, int, list, string, tuple}, builtins::{bool, byte_array, function, int, list, string, tuple},
expr::{FnStyle, TypedExpr, UntypedExpr}, expr::{FnStyle, TypedExpr, UntypedExpr},
@ -17,6 +17,8 @@ use crate::{
tipo::fields::FieldMap, tipo::fields::FieldMap,
}; };
use self::usefulness::compute_match_usefulness;
use super::{ use super::{
environment::{assert_no_labeled_arguments, collapse_links, EntityKind, Environment}, environment::{assert_no_labeled_arguments, collapse_links, EntityKind, Environment},
error::{Error, Warning}, error::{Error, Warning},
@ -48,9 +50,9 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
&mut self, &mut self,
subject: &Type, subject: &Type,
typed_clauses: &[TypedClause], typed_clauses: &[TypedClause],
location: Span, _location: Span,
) -> Result<(), Vec<String>> { ) -> Result<(), Vec<String>> {
let value_typ = collapse_links(Arc::new(subject.clone())); let _value_typ = collapse_links(Arc::new(subject.clone()));
// Currently guards in exhaustiveness checking are assumed that they can fail, // Currently guards in exhaustiveness checking are assumed that they can fail,
// so we go through all clauses and pluck out only the patterns // so we go through all clauses and pluck out only the patterns
@ -63,12 +65,16 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
.. ..
} = clause } = clause
{ {
patterns.push(pattern.clone()) patterns.push(pattern)
} }
} }
self.environment let _ = dbg!(compute_match_usefulness(self.environment, &patterns));
.check_exhaustiveness(patterns, value_typ, location)
// self.environment
// .check_exhaustiveness(patterns, value_typ, location)
Ok(())
} }
pub fn do_infer_call( pub fn do_infer_call(

View File

@ -0,0 +1,535 @@
use std::{collections::BTreeMap, iter, ops::Deref};
use crate::{
ast::{self, Span, TypedPattern},
tipo::{self, environment::Environment, error::Error},
};
#[derive(Debug, Clone)]
pub(crate) struct PatternStack {
pub(crate) patterns: Vec<Pattern>,
}
impl From<Pattern> for PatternStack {
fn from(value: Pattern) -> Self {
Self {
patterns: vec![value],
}
}
}
impl From<Vec<Pattern>> for PatternStack {
fn from(value: Vec<Pattern>) -> Self {
Self { patterns: value }
}
}
impl PatternStack {
fn is_empty(&self) -> bool {
self.patterns.is_empty()
}
fn head(&self) -> &Pattern {
&self.patterns[0]
}
fn tail(&self) -> PatternStack {
PatternStack {
patterns: self.patterns.iter().skip(1).cloned().collect(),
}
}
fn iter(&self) -> impl Iterator<Item = &Pattern> {
self.patterns.iter()
}
fn chain_tail_to_iter<'a>(&'a self, front: impl Iterator<Item = &'a Pattern>) -> PatternStack {
PatternStack {
patterns: front.chain(self.iter().skip(1)).cloned().collect(),
}
}
fn chain_tail_into_iter(&self, front: impl Iterator<Item = Pattern>) -> PatternStack {
PatternStack {
patterns: front.chain(self.iter().skip(1).cloned()).collect(),
}
}
// INVARIANT: (length row == N) ==> (length result == arity + N - 1)
fn specialize_row_by_ctor(&self, name: &String, arity: usize) -> Option<PatternStack> {
match self.head() {
Pattern::Constructor(p_name, _, p_args) => {
if p_name == name && p_args.len() == arity {
Some(self.chain_tail_to_iter(p_args.iter()))
} else {
None
}
}
Pattern::Wildcard => {
Some(self.chain_tail_into_iter(vec![Pattern::Wildcard; arity].into_iter()))
}
Pattern::Literal(_) => unreachable!(
"constructors and literals should never align in pattern match exhaustiveness checks."
),
}
}
// INVARIANT: (length row == N) ==> (length result == N-1)
fn specialize_row_by_wildcard(&self) -> Option<PatternStack> {
if self.is_empty() {
return None;
}
match self.head() {
Pattern::Constructor(_, _, _) => None,
Pattern::Literal(_) => None,
Pattern::Wildcard => Some(self.tail()),
}
}
// INVARIANT: (length row == N) ==> (length result == N-1)
fn specialize_row_by_literal(&self, literal: &Literal) -> Option<PatternStack> {
match self.head() {
Pattern::Literal(p_literal) => {
if p_literal == literal {
Some(self.tail())
} else {
None
}
}
Pattern::Wildcard => Some(self.tail()),
Pattern::Constructor(_, _, _) => unreachable!(
"constructors and literals should never align in pattern match exhaustiveness checks."
),
}
}
}
#[derive(Debug)]
pub(super) struct Matrix {
pub patterns: Vec<PatternStack>,
}
impl Matrix {
fn new() -> Self {
Matrix { patterns: vec![] }
}
pub(crate) fn is_empty(&self) -> bool {
self.patterns.is_empty()
}
pub(crate) fn push(&mut self, pattern_stack: PatternStack) {
self.patterns.push(pattern_stack);
}
/// Iterate over the first component of each row
pub(super) fn iter(&self) -> impl Iterator<Item = &PatternStack> {
self.patterns.iter()
}
/// Iterate over the first component of each row, mutably
pub(super) fn into_iter(self) -> impl Iterator<Item = PatternStack> {
self.patterns.into_iter()
}
pub(super) fn concat(self, other: Matrix) -> Matrix {
let mut patterns = self.patterns;
patterns.extend(other.patterns);
Matrix { patterns }
}
pub(crate) fn is_complete(&self) -> Complete {
let ctors = self.collect_ctors();
let num_seen = ctors.len();
if num_seen == 0 {
Complete::No
} else {
let (_, alts) = ctors.first_key_value().to_owned().unwrap();
if num_seen == alts.len() {
Complete::Yes(alts.to_vec())
} else {
Complete::No
}
}
}
pub(crate) fn collect_ctors(&self) -> BTreeMap<String, Vec<tipo::ValueConstructor>> {
let mut ctors = BTreeMap::new();
for pattern_stack in self.iter() {
match pattern_stack.head() {
Pattern::Constructor(name, alts, _) => {
ctors.insert(name.clone(), alts.clone());
}
Pattern::Wildcard | Pattern::Literal(_) => {}
}
}
ctors
}
fn specialize_rows_by_ctor(&self, name: &String, arity: usize) -> Matrix {
self.iter()
.filter_map(|p_stack| p_stack.specialize_row_by_ctor(name, arity))
.collect()
}
fn specialize_rows_by_wildcard(&self) -> Matrix {
self.iter()
.filter_map(|p_stack| p_stack.specialize_row_by_wildcard())
.collect()
}
fn specialize_rows_by_literal(&self, literal: &Literal) -> Matrix {
self.iter()
.filter_map(|p_stack| p_stack.specialize_row_by_literal(literal))
.collect()
}
}
#[derive(Debug)]
pub(crate) enum Complete {
Yes(Vec<tipo::ValueConstructor>),
No,
}
#[derive(Debug)]
pub(crate) struct Witness(Vec<TypedPattern>);
#[derive(Debug)]
enum Usefulness {
/// If we don't care about witnesses, simply remember if the pattern was useful.
NoWitnesses { useful: bool },
/// Carries a list of witnesses of non-exhaustiveness. If empty, indicates that the whole
/// pattern is unreachable.
WithWitnesses(Vec<Witness>),
}
#[derive(Copy, Clone, Debug)]
enum ArmType {
FakeExtraWildcard,
RealArm,
}
#[derive(Clone, Debug)]
pub(crate) enum Reachability {
/// The arm is reachable. This additionally carries a set of or-pattern branches that have been
/// found to be unreachable despite the overall arm being reachable. Used only in the presence
/// of or-patterns, otherwise it stays empty.
Reachable(Vec<Span>),
/// The arm is unreachable.
Unreachable,
}
#[derive(Debug)]
pub(crate) struct UsefulnessReport {
/// For each arm of the input, whether that arm is reachable after the arms above it.
pub(crate) arm_usefulness: Vec<(ast::TypedClause, Reachability)>,
/// If the match is exhaustive, this is empty. If not, this contains witnesses for the lack of
/// exhaustiveness.
pub(crate) non_exhaustiveness_witnesses: Vec<TypedPattern>,
}
#[derive(Debug, Clone)]
pub(crate) enum Pattern {
Wildcard,
Literal(Literal),
Constructor(String, Vec<tipo::ValueConstructor>, Vec<Pattern>),
}
#[derive(Debug, Clone, PartialEq)]
pub(crate) enum Literal {
Int(String),
}
fn simplify(environment: &mut Environment, value: &ast::TypedPattern) -> Result<Pattern, Error> {
match value {
ast::Pattern::Int { value, .. } => Ok(Pattern::Literal(Literal::Int(value.clone()))),
ast::Pattern::Assign { pattern, .. } => simplify(environment, pattern.as_ref()),
ast::Pattern::List { .. } => todo!(),
ast::Pattern::Constructor {
name,
arguments,
module,
location,
tipo,
..
} => {
let type_name = match tipo.deref() {
tipo::Type::App {
name: type_name, ..
} => type_name,
tipo::Type::Fn { ret, .. } => {
let tipo::Type::App {
name: type_name, ..
} = ret.deref() else {unreachable!("ret should be a Type::App")};
type_name
}
_ => unreachable!("tipo should be a Type::App"),
};
let constructors = environment
.get_constructors_for_type(module, type_name, *location)?
.clone();
let mut alts = Vec::new();
for constructor in constructors {
let value_constructor =
environment.get_value_constructor(module.as_ref(), &constructor, *location)?;
alts.push(value_constructor.clone());
}
let mut args = Vec::new();
for argument in arguments {
args.push(simplify(environment, &argument.value)?);
}
Ok(Pattern::Constructor(name.to_string(), alts, args))
}
ast::Pattern::Tuple { .. } => todo!(),
ast::Pattern::Var { .. } | ast::Pattern::Discard { .. } => Ok(Pattern::Wildcard),
}
}
impl iter::FromIterator<PatternStack> for Matrix {
fn from_iter<T: IntoIterator<Item = PatternStack>>(iter: T) -> Self {
Matrix {
patterns: iter.into_iter().collect(),
}
}
}
pub(crate) fn compute_match_usefulness(
environment: &mut Environment,
unchecked_patterns: &[&ast::TypedPattern],
) -> Result<UsefulnessReport, Error> {
let mut matrix = Matrix::new();
for unchecked_pattern in unchecked_patterns {
let pattern = simplify(environment, unchecked_pattern)?;
let pattern_stack = PatternStack::from(pattern);
if is_useful(&matrix, &pattern_stack) {
matrix.push(pattern_stack);
} else {
todo!("redudant")
}
}
dbg!(&matrix);
let bad_patterns = is_exhaustive(matrix, 1);
dbg!(bad_patterns);
Ok(UsefulnessReport {
arm_usefulness: vec![],
non_exhaustiveness_witnesses: vec![],
})
}
// INVARIANTS:
//
// The initial rows "matrix" are all of length 1
// The initial count of items per row "n" is also 1
// The resulting rows are examples of missing patterns
//
fn is_exhaustive(matrix: Matrix, n: usize) -> Matrix {
if matrix.is_empty() {
return Matrix {
patterns: vec![PatternStack {
patterns: vec![Pattern::Wildcard; n],
}],
};
}
if n == 0 {
return Matrix::new();
}
let ctors = matrix.collect_ctors();
let num_seen = ctors.len();
if num_seen == 0 {
let new_matrix = matrix.specialize_rows_by_wildcard();
let new_matrix = is_exhaustive(new_matrix, n - 1);
let new_matrix = new_matrix
.iter()
.map(|p_stack| {
let mut new_p_stack = p_stack.clone();
new_p_stack.patterns.insert(0, Pattern::Wildcard);
new_p_stack
})
.collect::<Matrix>();
return new_matrix;
}
let (_, alts) = ctors.first_key_value().unwrap();
if num_seen < alts.len() {
let new_matrix = matrix.specialize_rows_by_wildcard();
let new_matrix = is_exhaustive(new_matrix, n - 1);
let prefix = alts.iter().filter_map(|alt| is_missing(alts, &ctors, alt));
let mut m = Matrix::new();
for p_stack in new_matrix.into_iter() {
for p in prefix.clone() {
let mut p_stack = p_stack.clone();
p_stack.patterns.insert(0, p);
m.push(p_stack);
}
}
// (:)
// <$> Maybe.mapMaybe (isMissing alts ctors) altList
// <*> isExhaustive (Maybe.mapMaybe specializeRowByAnything matrix) (n - 1)
return m;
}
// let
// isAltExhaustive (Can.Ctor name _ arity _) =
// recoverCtor alts name arity <$>
// isExhaustive
// (Maybe.mapMaybe (specializeRowByCtor name arity) matrix)
// (arity + n - 1)
// in
// concatMap isAltExhaustive altList
//
alts.iter()
.map(|ctor| {
let tipo::ValueConstructor { variant, .. } = ctor;
let tipo::ValueConstructorVariant::Record {
name,
arity,
..
} = variant else {unreachable!("variant should be a ValueConstructorVariant")};
let new_matrix = matrix.specialize_rows_by_ctor(name, *arity);
let new_matrix = is_exhaustive(new_matrix, *arity + n - 1);
new_matrix
.into_iter()
.map(|p_stack| recover_ctor(alts.clone(), name, *arity, p_stack))
.collect()
})
.fold(Matrix::new(), |acc, m| acc.concat(m))
}
fn recover_ctor(
alts: Vec<tipo::ValueConstructor>,
name: &str,
arity: usize,
patterns: PatternStack,
) -> PatternStack {
let mut rest = patterns.patterns;
let mut args = rest.split_off(arity);
std::mem::swap(&mut rest, &mut args);
rest.insert(0, Pattern::Constructor(name.to_string(), alts, args));
rest.into()
}
fn is_missing(
alts: &[tipo::ValueConstructor],
ctors: &BTreeMap<String, Vec<tipo::ValueConstructor>>,
ctor: &tipo::ValueConstructor,
) -> Option<Pattern> {
let tipo::ValueConstructor { variant, .. } = ctor;
let tipo::ValueConstructorVariant::Record {
name,
arity,
..
} = variant else {unreachable!("variant should be a ValueConstructorVariant")};
if ctors.contains_key(name) {
None
} else {
Some(Pattern::Constructor(
name.clone(),
alts.to_vec(),
vec![Pattern::Wildcard; *arity],
))
}
}
fn is_useful(matrix: &Matrix, vector: &PatternStack) -> bool {
// No rows are the same as the new vector! The vector is useful!
if matrix.is_empty() {
return true;
}
// There is nothing left in the new vector, but we still have
// rows that match the same things. This is not a useful vector!
if vector.is_empty() {
return false;
}
let first_pattern = vector.head();
match first_pattern {
Pattern::Constructor(name, _, args) => {
let arity = args.len();
let new_matrix = matrix.specialize_rows_by_ctor(name, arity);
let new_vector: PatternStack = vector.chain_tail_to_iter(args.iter());
is_useful(&new_matrix, &new_vector)
}
Pattern::Wildcard => {
// check if all alts appear in matrix
match matrix.is_complete() {
Complete::No => {
// This Wildcard is useful because some Ctors are missing.
// But what if a previous row has a Wildcard?
// If so, this one is not useful.
let new_matrix = matrix.specialize_rows_by_wildcard();
let new_vector = vector.tail();
is_useful(&new_matrix, &new_vector)
}
Complete::Yes(alts) => alts.into_iter().any(|alt| {
let tipo::ValueConstructor { variant, .. } = alt;
let tipo::ValueConstructorVariant::Record {
name,
arity,
..
} = variant else {unreachable!("variant should be a ValueConstructorVariant")};
let new_matrix = matrix.specialize_rows_by_ctor(&name, arity);
let new_vector =
vector.chain_tail_into_iter(vec![Pattern::Wildcard; arity].into_iter());
is_useful(&new_matrix, &new_vector)
}),
}
}
Pattern::Literal(literal) => {
let new_matrix: Matrix = matrix.specialize_rows_by_literal(literal);
let new_vector = vector.tail();
is_useful(&new_matrix, &new_vector)
}
}
}