use crate::engine::grammar::SPG;
use crate::typing::{Context, Type, TypingSynth};
use crate::validation::parseable::check_all_prefixes_parseable;
use proptest::prelude::*;
fn ctx_of(pairs: &[(&str, &str)]) -> Context {
let mut ctx = Context::new();
for (name, ty) in pairs {
ctx.add(name.to_string(), Type::raw(ty));
}
ctx
}
fn stlc_chain_context(arg_count: usize) -> Vec<(String, String)> {
let type_names: Vec<String> = (0..=arg_count).map(|i| format!("T{}", i)).collect();
let mut f_ty = type_names[arg_count].clone();
for i in (0..arg_count).rev() {
f_ty = format!("{}->{}", type_names[i], f_ty);
}
let mut pairs = vec![("f".to_string(), f_ty)];
for (i, name) in (0..arg_count).map(|i| {
let name = match i {
0 => "x".to_string(),
1 => "y".to_string(),
2 => "z".to_string(),
3 => "u".to_string(),
4 => "v".to_string(),
_ => format!("a{}", i),
};
(i, name)
}) {
pairs.push((name, type_names[i].clone()));
}
pairs
}
fn stlc_chain_input(arg_count: usize) -> String {
let names: Vec<String> = stlc_chain_context(arg_count)
.into_iter()
.map(|(name, _)| name)
.collect();
names.join(" ")
}
fn ctx_from_owned(g: &SPG, pairs: &[(String, String)]) -> Context {
let mut ctx = Context::new();
for (name, ty) in pairs {
ctx.add(name.clone(), Type::parse(g, ty).unwrap());
}
ctx
}
fn unifies(a: &Type, b: &Type) -> bool {
let mut s = crate::typing::Subst::new();
crate::typing::term::unify(a, b, &mut s, true)
}
#[test]
fn top_unifies_with_concrete() {
assert!(unifies(&Type::top(), &Type::raw("number")));
}
#[test]
fn equal_raw_types() {
assert!(unifies(&Type::raw("Int"), &Type::raw("Int")));
assert!(!unifies(&Type::raw("Int"), &Type::raw("Bool")));
}
#[test]
fn untyped_closed_child_does_not_satisfy_concrete_ascription() {
let grammar = SPG::load(
r#"
Untyped ::= 'u'
Use(use) ::= Untyped[value]
Start ::= Use
Γ ⊢ value : 'number'
-------------------- (use)
'number'
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "u");
assert!(synth.parse_with(&Context::new()).is_err());
}
#[test]
fn context_membership_rejects_open_prefix_with_no_possible_binding() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Start ::= Variable
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "z");
assert!(synth.parse_with(&ctx_of(&[("foo", "number")])).is_err());
}
#[test]
fn context_membership_accepts_open_prefix_with_possible_binding() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Start ::= Variable
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "fo");
assert!(synth.parse_with(&ctx_of(&[("foo", "number")])).is_ok());
}
#[test]
fn ruleless_multichild_root_is_structural_tree() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Pair ::= Variable Variable
Start ::= Pair
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "x y");
let ast = synth
.parse_with(&ctx_of(&[("x", "'X'"), ("y", "'Y'")]))
.unwrap();
let arena = ast.arena();
assert!(
ast.root_ids().iter().any(|&id| {
matches!(
arena
.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence)),
Some(Type::Con(_, kids)) if kids.len() == 2
)
}),
"expected a structural Con tree over the two children"
);
}
#[test]
fn transparent_unary_ruleless_root_inherits_child_type() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Wrap ::= Variable
Start ::= Wrap
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "x");
let ast = synth.parse_with(&ctx_of(&[("x", "'X'")])).unwrap();
let arena = ast.arena();
eprintln!("DEBUG: {} root ids", ast.root_ids().len());
let root_types: Vec<_> = ast
.root_ids()
.iter()
.filter_map(|&id| {
arena.node(id).map(|node| {
let ev = synth.runtime().evidence_of(node.evidence);
eprintln!(
"DEBUG: root id={} nt={} evidence={:?} status={:?} children={:?}",
id, node.nt, ev, node.status, node.alts
);
(id, node.nt, ev)
})
})
.collect();
assert!(
ast.root_ids().iter().any(|&id| {
arena
.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence))
== Some(Type::raw("X"))
}),
"root types: {:?}",
root_types
);
}
#[test]
fn mixed_nonterminal_unary_alt_inherits_child_type() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Atom ::= Variable | '(' Variable ')'
Start ::= Atom
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "x");
let ast = synth.parse_with(&ctx_of(&[("x", "'X'")])).unwrap();
let arena = ast.arena();
assert!(ast.root_ids().iter().any(|&id| {
arena
.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence))
== Some(Type::raw("X"))
}));
}
#[test]
fn transparent_delimited_wrapper_inherits_child_type() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Group ::= '(' Variable ')'
Start ::= Group
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "(x)");
let ast = synth.parse_with(&ctx_of(&[("x", "'X'")])).unwrap();
let arena = ast.arena();
assert!(ast.root_ids().iter().any(|&id| {
arena
.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence))
== Some(Type::raw("X"))
}));
}
#[test]
fn unresolved_meta_is_not_exported_as_final_chain_type() {
let grammar = SPG::load(include_str!("../../../examples/stlc.auf")).unwrap();
let ctx = ctx_from_owned(
&grammar,
&[
("f".into(), "A->B->C".into()),
("x".into(), "A".into()),
("y".into(), "B".into()),
],
);
let expected = Type::parse(&grammar, "C").unwrap();
let mut synth = TypingSynth::new(grammar, "f x y");
let ast = synth.parse_with(&ctx).unwrap();
let arena = ast.arena();
assert!(ast.root_ids().iter().any(|&id| {
arena
.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence))
== Some(expected.clone())
}));
}
#[test]
fn empty_variable_prefix_is_accepted_as_unknown_not_contradiction() {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Start ::= Variable
x ∈ Γ
----------- (var)
Γ(x)
"#,
)
.unwrap();
let mut synth = TypingSynth::new(grammar, "");
let ast = synth.parse_with(&ctx_of(&[("x", "'X'")])).unwrap();
assert!(ast.is_complete() || !ast.root_ids().is_empty());
}
#[test]
fn closed_int_left_operand_does_not_reopen_for_float_operator() {
let grammar = SPG::load(include_str!("../../../examples/fun.auf")).unwrap();
let mut synth = TypingSynth::new(grammar, "10 /. 2.0");
assert!(synth.parse_with(&Context::new()).is_err());
}
#[test]
fn closed_parenthesized_int_expr_does_not_reopen_for_float_operator() {
let grammar = SPG::load(include_str!("../../../examples/fun.auf")).unwrap();
let mut synth = TypingSynth::new(grammar, "((1 + 2) * (3 + 4)) /. 2.0");
assert!(synth.parse_with(&Context::new()).is_err());
}
proptest! {
#[test]
fn prop_transparent_wrapper_inherits_child_type(name in "[a-z]{1,6}") {
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Wrap ::= Variable
Start ::= Wrap
x ∈ Γ
----------- (var)
Γ(x)
"#,
).unwrap();
let mut synth = TypingSynth::new(grammar, &name);
let ast = synth.parse_with(&ctx_of(&[(&name, "'X'")])).unwrap();
let arena = ast.arena();
let ok = ast.root_ids().iter().any(|&id| {
arena.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence))
== Some(Type::raw("X"))
});
prop_assert!(ok);
}
#[test]
fn prop_ruleless_multichild_stays_structural(a in "[a-z]{1,4}", b in "[a-z]{1,4}") {
prop_assume!(a != b);
let grammar = SPG::load(
r#"
Identifier ::= /[a-z]+/
Variable(var) ::= Identifier[x]
Pair ::= Variable Variable
Start ::= Pair
x ∈ Γ
----------- (var)
Γ(x)
"#,
).unwrap();
let mut synth = TypingSynth::new(grammar, format!("{} {}", a, b));
let ast = synth.parse_with(&ctx_of(&[(&a, "'L'"), (&b, "'R'")])).unwrap();
let arena = ast.arena();
let ok = ast.root_ids().iter().any(|&id| {
matches!(
arena.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence)),
Some(Type::Con(_, kids)) if kids.len() == 2
)
});
prop_assert!(ok);
}
}
#[test]
fn generated_stlc_chains_parse_and_resolve() {
let grammar = SPG::load(include_str!("../../../examples/stlc.auf")).unwrap();
let mut synth = TypingSynth::new(grammar.clone(), "");
for arg_count in 1..=5 {
let input = stlc_chain_input(arg_count);
let ctx = ctx_from_owned(&grammar, &stlc_chain_context(arg_count));
let expected = Type::parse(&grammar, &format!("T{}", arg_count)).unwrap();
synth.set_input(input.as_str());
let ast = synth.parse_with(&ctx).unwrap();
let arena = ast.arena();
let final_ok = ast.root_ids().iter().any(|&id| {
arena
.node(id)
.and_then(|node| synth.runtime().evidence_of(node.evidence))
== Some(expected.clone())
});
assert!(
final_ok,
"a {arg_count}-arg chain should resolve to T{arg_count}"
);
}
}
#[test]
fn generated_stlc_chain_prefixes_parse() {
let mut grammar = SPG::load(include_str!("../../../examples/stlc.auf")).unwrap();
for arg_count in 1..=5 {
let input = stlc_chain_input(arg_count);
let ctx = ctx_from_owned(&grammar, &stlc_chain_context(arg_count));
let result = check_all_prefixes_parseable(&mut grammar, &input, &ctx);
assert!(
matches!(
result,
crate::validation::parseable::ParseResult::Pass { .. }
),
"all prefixes of a {arg_count}-arg chain should parse"
);
}
}