Normalize primitive and numeric constraints

This commit is contained in:
Keisuke Hirata 2026-06-16 11:22:09 +09:00
parent e23b31da46
commit 84680e2652
No known key found for this signature in database
4 changed files with 350 additions and 3 deletions

View File

@ -0,0 +1,284 @@
use alloc::{string::String, vec::Vec};
use crate::{
Diagnostic, DiagnosticKind, Span,
ast::CompareOp,
runtime::{Constraint, LiteralValue, PrimitiveType},
};
pub fn normalize_constraints(
constraints: Vec<Constraint>,
span: Span,
) -> crate::Result<Vec<Constraint>> {
let mut primitive = None;
let mut lower: Option<Bound> = None;
let mut upper: Option<Bound> = None;
let mut rest = Vec::new();
for constraint in constraints {
match constraint {
Constraint::Type(next) => match primitive {
Some(current) if current != next => {
return Err(Diagnostic::new(
DiagnosticKind::Conflict,
span,
"primitive type constraints conflict",
));
}
Some(_) => {}
None => primitive = Some(next),
},
Constraint::Compare(op, value) => {
let number = Number::from_literal(&value).ok_or_else(|| {
Diagnostic::new(
DiagnosticKind::TypeMismatch,
span,
"comparison constraints require numeric literals",
)
})?;
match op {
CompareOp::Gt => merge_lower(&mut lower, Bound::new(number, false)),
CompareOp::Gte => merge_lower(&mut lower, Bound::new(number, true)),
CompareOp::Lt => merge_upper(&mut upper, Bound::new(number, false)),
CompareOp::Lte => merge_upper(&mut upper, Bound::new(number, true)),
CompareOp::Eq => {
merge_lower(&mut lower, Bound::new(number, true));
merge_upper(&mut upper, Bound::new(number, true));
}
}
}
Constraint::Regex(pattern) => rest.push(Constraint::Regex(pattern)),
Constraint::BuiltinPredicate(name) => rest.push(Constraint::BuiltinPredicate(name)),
}
}
if matches!(primitive, Some(PrimitiveType::String | PrimitiveType::Bool))
&& (lower.is_some() || upper.is_some())
{
return Err(Diagnostic::new(
DiagnosticKind::Conflict,
span,
"numeric comparison constraints conflict with non-numeric primitive type",
));
}
if primitive == Some(PrimitiveType::Int)
&& lower
.iter()
.chain(upper.iter())
.any(|bound| !matches!(bound.number, Number::Int(_)))
{
return Err(Diagnostic::new(
DiagnosticKind::Conflict,
span,
"Int comparison constraints must use integer literals",
));
}
ensure_bounds_non_empty(primitive, lower, upper, span)?;
let mut normalized = Vec::new();
if let Some(primitive) = primitive {
normalized.push(Constraint::Type(primitive));
}
if let Some(lower) = lower {
normalized.push(Constraint::Compare(
if lower.inclusive {
CompareOp::Gte
} else {
CompareOp::Gt
},
lower.number.into_literal(),
));
}
if let Some(upper) = upper {
normalized.push(Constraint::Compare(
if upper.inclusive {
CompareOp::Lte
} else {
CompareOp::Lt
},
upper.number.into_literal(),
));
}
normalized.extend(rest);
Ok(normalized)
}
#[derive(Debug, Clone, Copy, PartialEq)]
struct Bound {
number: Number,
inclusive: bool,
}
impl Bound {
fn new(number: Number, inclusive: bool) -> Self {
Self { number, inclusive }
}
}
#[derive(Debug, Clone, Copy, PartialEq)]
enum Number {
Int(i64),
Float(f64),
}
impl Number {
fn from_literal(value: &LiteralValue) -> Option<Self> {
match value {
LiteralValue::Int(value) => Some(Self::Int(*value)),
LiteralValue::Float(value) => Some(Self::Float(*value)),
LiteralValue::String(_) | LiteralValue::Bool(_) => None,
}
}
fn into_literal(self) -> LiteralValue {
match self {
Self::Int(value) => LiteralValue::Int(value),
Self::Float(value) => LiteralValue::Float(value),
}
}
fn as_f64(self) -> f64 {
match self {
Self::Int(value) => value as f64,
Self::Float(value) => value,
}
}
}
fn merge_lower(current: &mut Option<Bound>, next: Bound) {
match current {
None => *current = Some(next),
Some(current_bound) if is_stricter_lower(next, *current_bound) => *current_bound = next,
Some(_) => {}
}
}
fn merge_upper(current: &mut Option<Bound>, next: Bound) {
match current {
None => *current = Some(next),
Some(current_bound) if is_stricter_upper(next, *current_bound) => *current_bound = next,
Some(_) => {}
}
}
fn is_stricter_lower(next: Bound, current: Bound) -> bool {
let next_value = next.number.as_f64();
let current_value = current.number.as_f64();
next_value > current_value
|| (next_value == current_value && !next.inclusive && current.inclusive)
}
fn is_stricter_upper(next: Bound, current: Bound) -> bool {
let next_value = next.number.as_f64();
let current_value = current.number.as_f64();
next_value < current_value
|| (next_value == current_value && !next.inclusive && current.inclusive)
}
fn ensure_bounds_non_empty(
primitive: Option<PrimitiveType>,
lower: Option<Bound>,
upper: Option<Bound>,
span: Span,
) -> crate::Result<()> {
if primitive == Some(PrimitiveType::Int) {
let min = lower.map(int_lower_bound).unwrap_or(i128::from(i64::MIN));
let max = upper.map(int_upper_bound).unwrap_or(i128::from(i64::MAX));
if min > max {
return Err(empty_numeric_bounds(span));
}
return Ok(());
}
if let (Some(lower), Some(upper)) = (lower, upper) {
let lower_value = lower.number.as_f64();
let upper_value = upper.number.as_f64();
if lower_value > upper_value {
return Err(empty_numeric_bounds(span));
}
if lower_value == upper_value && !(lower.inclusive && upper.inclusive) {
return Err(empty_numeric_bounds(span));
}
}
Ok(())
}
fn int_lower_bound(bound: Bound) -> i128 {
let Number::Int(value) = bound.number else {
unreachable!()
};
if bound.inclusive {
i128::from(value)
} else {
i128::from(value) + 1
}
}
fn int_upper_bound(bound: Bound) -> i128 {
let Number::Int(value) = bound.number else {
unreachable!()
};
if bound.inclusive {
i128::from(value)
} else {
i128::from(value) - 1
}
}
fn empty_numeric_bounds(span: Span) -> Diagnostic {
Diagnostic::new(
DiagnosticKind::Conflict,
span,
String::from("numeric comparison constraints have an empty intersection"),
)
}
#[cfg(test)]
mod tests {
use super::*;
use crate::runtime::LiteralValue;
#[test]
fn detects_primitive_conflict() {
assert!(
normalize_constraints(
alloc::vec![
Constraint::Type(PrimitiveType::Int),
Constraint::Type(PrimitiveType::String),
],
Span::default(),
)
.is_err()
);
}
#[test]
fn detects_empty_int_range() {
assert!(
normalize_constraints(
alloc::vec![
Constraint::Type(PrimitiveType::Int),
Constraint::Compare(CompareOp::Gt, LiteralValue::Int(10)),
Constraint::Compare(CompareOp::Lt, LiteralValue::Int(11)),
],
Span::default(),
)
.is_err()
);
}
#[test]
fn keeps_regex_constraints_without_intersection_check() {
let constraints = normalize_constraints(
alloc::vec![
Constraint::Regex(String::from("^a$")),
Constraint::Regex(String::from("^b$")),
],
Span::default(),
)
.unwrap();
assert_eq!(constraints.len(), 2);
}
}

View File

@ -3,6 +3,7 @@ use alloc::{format, string::String, vec, vec::Vec};
use crate::{
ExprId, SourceForm, SourceId, Span,
ast::{Ast, BinaryOp, CompareOp, Expr, Field, Literal},
constraints::normalize_constraints,
diagnostic::{Diagnostic, DiagnosticKind, Result},
embedding::HostValue,
module::{EmptyLoader, LoadedSource, Module, SourceLoader},
@ -589,6 +590,7 @@ impl<L: SourceLoader> Engine<L> {
match (lhs, rhs) {
(RuntimeValue::Abstract(mut lhs), RuntimeValue::Abstract(rhs)) => {
lhs.constraints.extend(rhs.constraints);
lhs.constraints = normalize_constraints(lhs.constraints, span)?;
lhs.default = merge_default(lhs.default, rhs.default, span)?;
Ok(RuntimeValue::Abstract(lhs))
}
@ -765,6 +767,7 @@ impl<L: SourceLoader> Engine<L> {
} else {
None
};
let constraints = normalize_constraints(constraints, Span::default())?;
Ok(RuntimeValue::Abstract(AbstractValue {
constraints,
default,

View File

@ -3,6 +3,7 @@
extern crate alloc;
pub mod ast;
pub mod constraints;
pub mod diagnostic;
pub mod embedding;
pub mod eval;
@ -13,6 +14,7 @@ pub mod runtime;
pub mod span;
pub use ast::{Ast, BinaryOp, CompareOp, Expr, ExprId, Field, Literal, Param};
pub use constraints::normalize_constraints;
pub use diagnostic::{Diagnostic, DiagnosticKind, Result};
pub use embedding::{HostField, HostValue};
pub use eval::Engine;

View File

@ -31,9 +31,52 @@ A & B = A と B の両方を満たす値または制約
```dcdl
Int & String # エラー
>= 10 & <= 5 # エラーになりうる
> 10 & < 5 # エラー
Int & > 10 & < 11 # エラー整数値の候補が存在しない
```
## 制約の正規化
`&` によって abstract value 同士を合成した場合、処理系は軽量に判定できる制約を正規化する。
正規化対象:
- primitive type 制約。
- 数値比較制約。
primitive type 制約は、異なる型が同時に要求された場合 conflict になる。
```dcdl
Int & Float
Int & String
```
数値比較制約は上下限として正規化される。
```dcdl
Int & >= 1 & <= 65535 & > 443
```
これは概念的に以下へ正規化される。
```text
Type(Int)
> 443
<= 65535
```
上下限の交差が空であれば conflict になる。
`Int` 制約がある場合は、整数候補が存在するかも判定する。
```dcdl
> 10 & < 5 # conflict
Int & > 10 & < 11 # conflict
Int & >= 10 & <= 10 # OK
```
`Int` の比較制約は整数リテラルを使う。
`Float` の比較制約は整数リテラルまたは浮動小数リテラルを使える。
## 組み込み制約
最小の組み込み制約は以下である。
@ -53,13 +96,28 @@ IPv4Address
## 正規表現制約
正規表現リテラルは文字列制約として使える候補である
正規表現リテラルは文字列制約として使える。
```dcdl
Host = /^\d{1,3}\.\d{1,3}\.\d{1,3}\.\d{1,3}$/;
```
ただし、組み込み向け実装では正規表現エンジンを optional feature にできる。
正規表現制約は積み重ね可能である。
複数の正規表現制約が同じ abstract value に付与された場合、具体文字列はすべての正規表現制約に一致しなければならない。
```dcdl
String & /^a/ & /z$/
```
処理系は、正規表現制約同士の交差が空であるかを合成時に判定する必要はない。
つまり、以下は合成時には conflict にならず、具体値検証時に失敗する。
```dcdl
String & /^a$/ & /^b$/
```
正規表現エンジンは optional feature にできる。
正規表現 feature が無効な処理系では、正規表現制約の検証は unsupported feature diagnostic になる。
軽量実装では代表的な制約を組み込み述語として提供してもよい。
```dcdl