ftml_solver/rules/fixity/
mod.rs

1mod bin;
2mod conj;
3mod pre;
4mod reorder;
5
6pub use bin::*;
7pub use conj::*;
8pub use pre::*;
9pub use reorder::*;
10
11use ftml_ontology::{
12    domain::declarations::symbols::Symbol,
13    narrative::elements::VariableDeclaration,
14    terms::{ApplicationTerm, Argument, ArgumentMode, MaybeSequence, Term, Variable},
15};
16use ftml_uris::SymbolUri;
17
18fn is_sequence_binary<'t>(
19    uri: &SymbolUri,
20    t: &'t Term,
21    head: either::Either<&Symbol, &VariableDeclaration>,
22) -> Option<(&'t ApplicationTerm, &'t MaybeSequence<Term>, usize)> {
23    let either::Left(sym) = head else {
24        return None;
25    };
26    if sym.uri != *uri {
27        return None;
28    }
29    let Term::Application(a) = t else {
30        tracing::trace!("Not an application");
31        return None;
32    };
33    let Some(mut seq_index) = sym
34        .data
35        .arity
36        .iter()
37        .position(|m| matches!(m, ArgumentMode::Sequence))
38    else {
39        tracing::trace!("No sequence index");
40        return None;
41    };
42    if let Some(perm) = sym.data.reordering.as_ref()
43        && let Some(new) = perm.of(seq_index as u8)
44    {
45        seq_index = new as _;
46    }
47    match a.arguments.get(seq_index) {
48        Some(Argument::Sequence(s)) => Some((a, s, seq_index)),
49        _ => None,
50    }
51}
52
53fn was_sequence_binary<'t>(
54    uri: &SymbolUri,
55    t: &'t Term,
56    head: either::Either<&Symbol, &VariableDeclaration>,
57) -> Option<(&'t ApplicationTerm, &'t Term, &'t Term, usize)> {
58    let either::Left(sym) = head else {
59        return None;
60    };
61    if sym.uri != *uri {
62        return None;
63    }
64    let Term::Application(a) = t else {
65        return None;
66    };
67    let mut seq_index = sym
68        .data
69        .arity
70        .iter()
71        .position(|m| matches!(m, ArgumentMode::Sequence))?;
72    if let Some(perm) = sym.data.reordering.as_ref()
73        && let Some(new) = perm.of(seq_index as u8)
74    {
75        seq_index = new as _;
76    }
77    let num_args = sym.data.arity.num() as usize;
78    let actual_args = a.arguments.len();
79    if actual_args < num_args {
80        return None;
81    }
82    let num_later = num_args - 1 - seq_index;
83    let range_end = actual_args - num_later;
84    if range_end != seq_index + 2 {
85        return None;
86    }
87    let Some(Argument::Simple(first)) = a.arguments.get(seq_index) else {
88        return None;
89    };
90    let Some(Argument::Simple(second)) = a.arguments.get(seq_index + 1) else {
91        return None;
92    };
93    Some((a, first, second, seq_index))
94}
95
96fn match_head(
97    lhs: either::Either<&Symbol, &VariableDeclaration>,
98    rhs: Option<either::Either<&SymbolUri, &Variable>>,
99) -> bool {
100    match (lhs, rhs) {
101        (either::Either::Left(s), Some(either::Either::Left(uri))) => *uri == s.uri,
102        (either::Either::Right(vd), Some(either::Either::Right(v))) => {
103            v.name() == vd.uri.name().last()
104        }
105        _ => false,
106    }
107}
ftml_solver/rules/fixity/mod.rs

ftml_solver/rules/fixity/
mod.rs
