Skip to main content

cranelift_isle/
trie_again.rs

1//! A strongly-normalizing intermediate representation for ISLE rules. This representation is chosen
2//! to closely reflect the operations we can implement in Rust, to make code generation easy.
3use crate::disjointsets::DisjointSets;
4use crate::error::{Error, Span};
5use crate::lexer::Pos;
6use crate::sema::{self, RuleId, TermEnv, TermId, TypeEnv};
7use crate::stablemapset::StableSet;
8use std::collections::{HashMap, hash_map::Entry};
9
10/// A field index in a tuple or an enum variant.
11#[derive(Clone, Copy, Debug, Default, Eq, Hash, Ord, PartialEq, PartialOrd)]
12pub struct TupleIndex(u8);
13/// A hash-consed identifier for a binding, stored in a [RuleSet].
14#[derive(Clone, Copy, Debug, Default, Eq, Hash, Ord, PartialEq, PartialOrd)]
15pub struct BindingId(u16);
16
17impl std::convert::TryFrom<usize> for TupleIndex {
18    type Error = <u8 as std::convert::TryFrom<usize>>::Error;
19
20    fn try_from(value: usize) -> Result<Self, Self::Error> {
21        Ok(TupleIndex(value.try_into()?))
22    }
23}
24
25impl std::convert::TryFrom<usize> for BindingId {
26    type Error = <u16 as std::convert::TryFrom<usize>>::Error;
27
28    fn try_from(value: usize) -> Result<Self, Self::Error> {
29        Ok(BindingId(value.try_into()?))
30    }
31}
32
33impl std::convert::From<u16> for BindingId {
34    fn from(value: u16) -> Self {
35        BindingId(value)
36    }
37}
38
39impl TupleIndex {
40    /// Get the index of this field.
41    pub fn index(self) -> usize {
42        self.0.into()
43    }
44}
45
46impl BindingId {
47    /// Get the index of this id.
48    pub fn index(self) -> usize {
49        self.0.into()
50    }
51}
52
53/// Bindings are anything which can be bound to a variable name in Rust. This includes expressions,
54/// such as constants or function calls; but it also includes names bound in pattern matches.
55#[derive(Clone, Debug, Eq, Hash, PartialEq)]
56pub enum Binding {
57    /// Evaluates to the given boolean literal.
58    ConstBool {
59        /// The constant value.
60        val: bool,
61        /// The constant's type.
62        ty: sema::TypeId,
63    },
64    /// Evaluates to the given integer literal.
65    ConstInt {
66        /// The constant value.
67        val: i128,
68        /// The constant's type. Unsigned types preserve the representation of `val`, not its value.
69        ty: sema::TypeId,
70    },
71    /// Evaluates to the given primitive Rust value.
72    ConstPrim {
73        /// The constant value.
74        val: sema::Sym,
75    },
76    /// One of the arguments to the top-level function.
77    Argument {
78        /// Which of the function's arguments is this?
79        index: TupleIndex,
80    },
81    /// The result of calling an external extractor.
82    Extractor {
83        /// Which extractor should be called?
84        term: sema::TermId,
85        /// What expression should be passed to the extractor?
86        parameter: BindingId,
87    },
88    /// The result of calling an external constructor.
89    Constructor {
90        /// Which constructor should be called?
91        term: sema::TermId,
92        /// What expressions should be passed to the constructor?
93        parameters: Box<[BindingId]>,
94        /// For impure constructors, a unique number for each use of this term. Always 0 for pure
95        /// constructors.
96        instance: u32,
97    },
98    /// The result of getting one value from a multi-constructor or multi-extractor.
99    Iterator {
100        /// Which expression produced the iterator that this consumes?
101        source: BindingId,
102    },
103    /// The result of constructing an enum variant.
104    MakeVariant {
105        /// Which enum type should be constructed?
106        ty: sema::TypeId,
107        /// Which variant of that enum should be constructed?
108        variant: sema::VariantId,
109        /// What expressions should be provided for this variant's fields?
110        fields: Box<[BindingId]>,
111    },
112    /// Pattern-match one of the previous bindings against an enum variant and produce a new binding
113    /// from one of its fields. There must be a corresponding [Constraint::Variant] for each
114    /// `source`/`variant` pair that appears in some `MatchVariant` binding.
115    MatchVariant {
116        /// Which binding is being matched?
117        source: BindingId,
118        /// Which enum variant are we pulling binding sites from? This is somewhat redundant with
119        /// information in a corresponding [Constraint]. However, it must be here so that different
120        /// enum variants aren't hash-consed into the same binding site.
121        variant: sema::VariantId,
122        /// Which field of this enum variant are we projecting out? Although ISLE uses named fields,
123        /// we track them by index for constant-time comparisons. The [sema::TypeEnv] can be used to
124        /// get the field names.
125        field: TupleIndex,
126    },
127    /// The result of constructing a struct.
128    MakeStruct {
129        /// Which struct type should be constructed?
130        ty: sema::TypeId,
131        /// What expressions should be provided for this struct's fields?
132        fields: Box<[BindingId]>,
133    },
134    /// Extract the fields of the struct from one of the previous bindings to produce a new binding
135    /// from one of its fields. There must be a corresponding [Constraint::Struct] for each
136    /// `source`/`variant` pair that appears in some `ExtractStruct` binding.
137    ExtractStruct {
138        /// Which binding is being matched?
139        source: BindingId,
140        /// Which field of this struct are we projecting out? Although ISLE uses named fields,
141        /// we track them by index for constant-time comparisons. The [sema::TypeEnv] can be used to
142        /// get the field names.
143        field: TupleIndex,
144    },
145    /// The result of constructing an Option::Some variant.
146    MakeSome {
147        /// Contained expression.
148        inner: BindingId,
149    },
150    /// Pattern-match one of the previous bindings against `Option::Some` and produce a new binding
151    /// from its contents. There must be a corresponding [Constraint::Some] for each `source` that
152    /// appears in a `MatchSome` binding. (This currently only happens with external extractors.)
153    MatchSome {
154        /// Which binding is being matched?
155        source: BindingId,
156    },
157    /// Pattern-match one of the previous bindings against a tuple and produce a new binding from
158    /// one of its fields. This is an irrefutable pattern match so there is no corresponding
159    /// [Constraint]. (This currently only happens with external extractors.)
160    MatchTuple {
161        /// Which binding is being matched?
162        source: BindingId,
163        /// Which tuple field are we projecting out?
164        field: TupleIndex,
165    },
166}
167
168/// Pattern matches which can fail. Some binding sites are the result of successfully matching a
169/// constraint. A rule applies constraints to binding sites to determine whether the rule matches.
170#[derive(Clone, Copy, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)]
171pub enum Constraint {
172    /// The value must match this enum variant.
173    Variant {
174        /// Which enum type is being matched? This is implied by the binding where the constraint is
175        /// applied, but recorded here for convenience.
176        ty: sema::TypeId,
177        /// Which enum variant must this binding site match to satisfy the rule?
178        variant: sema::VariantId,
179        /// Number of fields in this variant of this enum. This is recorded in the constraint for
180        /// convenience, to avoid needing to look up the variant in a [sema::TypeEnv].
181        fields: TupleIndex,
182    },
183    /// The value must match this struct variant.
184    Struct {
185        /// Which struct type is being matched? This is implied by the binding where the constraint is
186        /// applied, but recorded here for convenience.
187        ty: sema::TypeId,
188        /// Number of fields in this variant of this enum. This is recorded in the constraint for
189        /// convenience, to avoid needing to look up the variant in a [sema::TypeEnv].
190        fields: TupleIndex,
191    },
192    /// The value must equal this boolean literal.
193    ConstBool {
194        /// The constant value.
195        val: bool,
196        /// The constant's type.
197        ty: sema::TypeId,
198    },
199    /// The value must equal this integer literal.
200    ConstInt {
201        /// The constant value.
202        val: i128,
203        /// The constant's type. Unsigned types preserve the representation of `val`, not its value.
204        ty: sema::TypeId,
205    },
206    /// The value must equal this Rust primitive value.
207    ConstPrim {
208        /// The constant value.
209        val: sema::Sym,
210    },
211    /// The value must be an `Option::Some`, from a fallible extractor.
212    Some,
213}
214
215/// A term-rewriting rule. All [BindingId]s are only meaningful in the context of the [RuleSet] that
216/// contains this rule.
217#[derive(Debug, Default)]
218pub struct Rule {
219    /// Identifier of the source rule.
220    pub id: RuleId,
221    /// Where was this rule defined?
222    pub pos: Pos,
223    /// All of these bindings must match the given constraints for this rule to apply. Note that
224    /// within a single rule, if a binding site must match two different constraints, then the rule
225    /// can never match.
226    constraints: HashMap<BindingId, Constraint>,
227    /// Sets of bindings which must be equal for this rule to match.
228    pub equals: DisjointSets<BindingId>,
229    /// These bindings are from multi-terms which need to be evaluated in this rule.
230    pub iterators: StableSet<BindingId>,
231    /// If other rules apply along with this one, the one with the highest numeric priority is
232    /// evaluated. If multiple applicable rules have the same priority, that's an overlap error.
233    pub prio: i64,
234    /// Rule name. Used for tracing.
235    pub name: Option<sema::Sym>,
236    /// If this rule applies, these side effects should be evaluated before returning.
237    pub impure: Vec<BindingId>,
238    /// If this rule applies, the top-level term should evaluate to this expression.
239    pub result: BindingId,
240}
241
242/// Records whether a given pair of rules can both match on some input.
243#[derive(Debug, Eq, PartialEq)]
244pub enum Overlap {
245    /// There is no input on which this pair of rules can both match.
246    No,
247    /// There is at least one input on which this pair of rules can both match.
248    Yes {
249        /// True if every input accepted by one rule is also accepted by the other. This does not
250        /// indicate which rule is more general and in fact the rules could match exactly the same
251        /// set of inputs. You can work out which by comparing `total_constraints()` in both rules:
252        /// The more general rule has fewer constraints.
253        subset: bool,
254    },
255}
256
257/// A collection of [Rule]s, along with hash-consed [Binding]s for all of them.
258#[derive(Debug, Default)]
259pub struct RuleSet {
260    /// The [Rule]s for a single [sema::Term].
261    pub rules: Vec<Rule>,
262    /// The bindings identified by [BindingId]s within rules.
263    pub bindings: Vec<Binding>,
264    /// Intern table for de-duplicating [Binding]s.
265    binding_map: HashMap<Binding, BindingId>,
266}
267
268/// Construct a [RuleSet] for each term in `termenv` that has rules.
269pub fn build(termenv: &sema::TermEnv) -> (Vec<(sema::TermId, RuleSet)>, Vec<Error>) {
270    let mut errors = Vec::new();
271    let mut term = HashMap::new();
272    for rule in termenv.rules.iter() {
273        term.entry(rule.root_term)
274            .or_insert_with(RuleSetBuilder::default)
275            .add_rule(rule, termenv, &mut errors);
276    }
277
278    // The `term` hash map may return terms in any order. Sort them to ensure that we produce the
279    // same output every time when given the same ISLE source. Rules are added to terms in `RuleId`
280    // order, so it's not necessary to sort within a `RuleSet`.
281    let mut result: Vec<_> = term
282        .into_iter()
283        .map(|(term, builder)| (term, builder.rules))
284        .collect();
285    result.sort_unstable_by_key(|(term, _)| *term);
286
287    (result, errors)
288}
289
290impl RuleSet {
291    /// Returns the [BindingId] corresponding to the given [Binding] within this rule-set, if any.
292    pub fn find_binding(&self, binding: &Binding) -> Option<BindingId> {
293        self.binding_map.get(binding).copied()
294    }
295}
296
297impl Binding {
298    /// Returns the binding sites which must be evaluated before this binding.
299    pub fn sources(&self) -> &[BindingId] {
300        match self {
301            Binding::ConstBool { .. } => &[][..],
302            Binding::ConstInt { .. } => &[][..],
303            Binding::ConstPrim { .. } => &[][..],
304            Binding::Argument { .. } => &[][..],
305            Binding::Extractor { parameter, .. } => std::slice::from_ref(parameter),
306            Binding::Constructor { parameters, .. } => &parameters[..],
307            Binding::Iterator { source } => std::slice::from_ref(source),
308            Binding::MakeVariant { fields, .. } => &fields[..],
309            Binding::MatchVariant { source, .. } => std::slice::from_ref(source),
310            Binding::MakeStruct { fields, .. } => &fields[..],
311            Binding::ExtractStruct { source, .. } => std::slice::from_ref(source),
312            Binding::MakeSome { inner } => std::slice::from_ref(inner),
313            Binding::MatchSome { source } => std::slice::from_ref(source),
314            Binding::MatchTuple { source, .. } => std::slice::from_ref(source),
315        }
316    }
317
318    /// Returns the term referenced by this binding.
319    pub fn term(&self, tyenv: &TypeEnv, termenv: &TermEnv) -> Option<TermId> {
320        match self {
321            Binding::ConstInt { .. } => None,
322            Binding::ConstBool { .. } => None,
323            Binding::ConstPrim { .. } => None,
324            Binding::Argument { .. } => None,
325            Binding::Extractor { term, .. } => Some(*term),
326            Binding::Constructor { term, .. } => Some(*term),
327            Binding::Iterator { .. } => None,
328            Binding::MakeVariant { ty, variant, .. } => {
329                Some(termenv.get_variant_term(tyenv, *ty, *variant))
330            }
331            Binding::MatchVariant { .. } => None,
332            Binding::MakeStruct { .. } => None,
333            Binding::ExtractStruct { .. } => None,
334            Binding::MakeSome { .. } => None,
335            Binding::MatchSome { .. } => None,
336            Binding::MatchTuple { .. } => None,
337        }
338    }
339}
340
341impl Constraint {
342    /// Return the nested [Binding]s from matching the given [Constraint] against the given [BindingId].
343    pub fn bindings_for(self, source: BindingId) -> Vec<Binding> {
344        match self {
345            // These constraints never introduce any bindings.
346            Constraint::ConstBool { .. }
347            | Constraint::ConstInt { .. }
348            | Constraint::ConstPrim { .. } => vec![],
349            Constraint::Some => vec![Binding::MatchSome { source }],
350            Constraint::Variant {
351                variant, fields, ..
352            } => (0..fields.0)
353                .map(TupleIndex)
354                .map(|field| Binding::MatchVariant {
355                    source,
356                    variant,
357                    field,
358                })
359                .collect(),
360            Constraint::Struct { fields, .. } => (0..fields.0)
361                .map(TupleIndex)
362                .map(|field| Binding::ExtractStruct { source, field })
363                .collect(),
364        }
365    }
366
367    /// Determine if this constraint could be compatible with a given binding.
368    pub fn compatible(&self, binding: &Binding) -> bool {
369        match (self, binding) {
370            (
371                Constraint::Variant {
372                    ty: tc,
373                    variant: vc,
374                    ..
375                },
376                Binding::MakeVariant {
377                    ty: tb,
378                    variant: vb,
379                    ..
380                },
381            ) => tb == tc && vb == vc,
382            (Constraint::ConstInt { val: vc, ty: tc }, Binding::ConstInt { val: vb, ty: tb }) => {
383                vc == vb && tc == tb
384            }
385            _ => true,
386        }
387    }
388}
389
390impl Rule {
391    /// Returns whether a given pair of rules can both match on some input, and if so, whether
392    /// either matches a subset of the other's inputs. If this function returns `No`, then the two
393    /// rules definitely do not overlap. However, it may return `Yes` in cases where the rules can't
394    /// overlap in practice, or where this analysis is not yet precise enough to decide.
395    pub fn may_overlap(&self, other: &Rule) -> Overlap {
396        // Two rules can't overlap if, for some binding site in the intersection of their
397        // constraints, the rules have different constraints: an input can't possibly match both
398        // rules then. If the rules do overlap, and one has a subset of the constraints of the
399        // other, then the less-constrained rule matches every input that the more-constrained rule
400        // matches, and possibly more. We test for both conditions at once, with the observation
401        // that if the intersection of two sets is equal to the smaller set, then it's a subset. So
402        // the outer loop needs to go over the rule with fewer constraints in order to correctly
403        // identify if it's a subset of the other rule. Also, that way around is faster.
404        let (small, big) = if self.constraints.len() <= other.constraints.len() {
405            (self, other)
406        } else {
407            (other, self)
408        };
409
410        // TODO: nonlinear constraints complicate the subset check
411        // For the purpose of overlap checking, equality constraints act like other constraints, in
412        // that they can cause rules to not overlap. However, because we don't have a concrete
413        // pattern to compare, the analysis to prove that is complicated. For now, we approximate
414        // the result. If either rule has nonlinear constraints, conservatively report that neither
415        // is a subset of the other. Note that this does not disagree with the doc comment for
416        // `Overlap::Yes { subset }` which says to use `total_constraints` to disambiguate, since if
417        // we return `subset: true` here, `equals` is empty for both rules, so `total_constraints()`
418        // equals `constraints.len()`.
419        let mut subset = small.equals.is_empty() && big.equals.is_empty();
420
421        for (binding, a) in small.constraints.iter() {
422            if let Some(b) = big.constraints.get(binding) {
423                if a != b {
424                    // If any binding site is constrained differently by both rules then there is
425                    // no input where both rules can match.
426                    return Overlap::No;
427                }
428                // Otherwise both are constrained in the same way at this binding site. That doesn't
429                // rule out any possibilities for what inputs the rules accept.
430            } else {
431                // The `big` rule's inputs are a subset of the `small` rule's inputs if every
432                // constraint in `small` is exactly matched in `big`. But we found a counterexample.
433                subset = false;
434            }
435        }
436        Overlap::Yes { subset }
437    }
438
439    /// Returns the total number of binding sites which this rule constrains, with either a concrete
440    /// pattern or an equality constraint.
441    pub fn total_constraints(&self) -> usize {
442        // Because of `normalize_equivalence_classes`, these two sets don't overlap, so the size of
443        // the union is the sum of their sizes.
444        self.constraints.len() + self.equals.len()
445    }
446
447    /// Returns the constraint that the given binding site must satisfy for this rule to match, if
448    /// there is one.
449    pub fn get_constraint(&self, source: BindingId) -> Option<Constraint> {
450        self.constraints.get(&source).copied()
451    }
452
453    fn set_constraint(
454        &mut self,
455        source: BindingId,
456        constraint: Constraint,
457    ) -> Result<(), UnreachableError> {
458        match self.constraints.entry(source) {
459            Entry::Occupied(entry) => {
460                if entry.get() != &constraint {
461                    return Err(UnreachableError {
462                        pos: self.pos,
463                        constraint_a: *entry.get(),
464                        constraint_b: constraint,
465                    });
466                }
467            }
468            Entry::Vacant(entry) => {
469                entry.insert(constraint);
470            }
471        }
472        Ok(())
473    }
474}
475
476#[derive(Debug)]
477struct UnreachableError {
478    pos: Pos,
479    constraint_a: Constraint,
480    constraint_b: Constraint,
481}
482
483#[derive(Debug, Default)]
484struct RuleSetBuilder {
485    current_rule: Rule,
486    impure_instance: u32,
487    unreachable: Vec<UnreachableError>,
488    rules: RuleSet,
489}
490
491impl RuleSetBuilder {
492    fn add_rule(&mut self, rule: &sema::Rule, termenv: &sema::TermEnv, errors: &mut Vec<Error>) {
493        self.impure_instance = 0;
494        self.current_rule.id = rule.id;
495        self.current_rule.pos = rule.pos;
496        self.current_rule.prio = rule.prio;
497        self.current_rule.name = rule.name;
498        self.current_rule.result = rule.visit(self, termenv);
499        if termenv.terms[rule.root_term.index()].is_partial() {
500            self.current_rule.result = self.dedup_binding(Binding::MakeSome {
501                inner: self.current_rule.result,
502            });
503        }
504        self.normalize_equivalence_classes();
505        let rule = std::mem::take(&mut self.current_rule);
506
507        if self.unreachable.is_empty() {
508            self.rules.rules.push(rule);
509        } else {
510            // If this rule can never match, drop it so it doesn't affect overlap checking.
511            errors.extend(
512                self.unreachable
513                    .drain(..)
514                    .map(|err| Error::UnreachableError {
515                        msg: format!(
516                            "rule requires binding to match both {:?} and {:?}",
517                            err.constraint_a, err.constraint_b
518                        ),
519                        span: Span::new_single(err.pos),
520                    }),
521            )
522        }
523    }
524
525    /// Establish the invariant that a binding site can have a concrete constraint in `constraints`,
526    /// or an equality constraint in `equals`, but not both. This is useful because overlap checking
527    /// is most effective on concrete constraints, and also because it exposes more rule structure
528    /// for codegen.
529    ///
530    /// If a binding site is constrained and also required to be equal to another binding site, then
531    /// copy the constraint and push the equality inside it. For example:
532    /// - `(term x @ 2 x)` is rewritten to `(term 2 2)`
533    /// - `(term x @ (T.A _ _) x)` is rewritten to `(term (T.A y z) (T.A y z))`
534    ///
535    /// In the latter case, note that every field of `T.A` has been replaced with a fresh variable
536    /// and each of the copies are set equal.
537    ///
538    /// If several binding sites are supposed to be equal but they each have conflicting constraints
539    /// then this rule is unreachable. For example, `(term x @ 2 (and x 3))` requires both arguments
540    /// to be equal but also requires them to match both 2 and 3, which can't happen for any input.
541    ///
542    /// We could do this incrementally, while building the rule. The implementation is nearly
543    /// identical but, having tried both ways, it's slightly easier to think about this as a
544    /// separate pass. Also, batching up this work should be slightly faster if there are multiple
545    /// binding sites set equal to each other.
546    fn normalize_equivalence_classes(&mut self) {
547        // First, find all the constraints that need to be copied to other binding sites in their
548        // respective equivalence classes. Note: do not remove these constraints here! Yes, we'll
549        // put them back later, but we rely on still having them around so that
550        // `set_constraint` can detect conflicting constraints.
551        let mut deferred_constraints = Vec::new();
552        for (&binding, &constraint) in self.current_rule.constraints.iter() {
553            if let Some(root) = self.current_rule.equals.find_mut(binding) {
554                deferred_constraints.push((root, constraint));
555            }
556        }
557
558        // Pick one constraint and propagate it through its equivalence class. If there are no
559        // errors then it doesn't matter what order we do this in, because that means that any
560        // redundant constraints on an equivalence class were equal. We can write equal values into
561        // the constraint map in any order and get the same result. If there were errors, we aren't
562        // going to generate code from this rule, so order only affects how conflicts are reported.
563        while let Some((current, constraint)) = deferred_constraints.pop() {
564            // Remove the entire equivalence class and instead add copies of this constraint to
565            // every binding site in the class. If there are constraints on other binding sites in
566            // this class, then when we try to copy this constraint to those binding sites,
567            // `set_constraint` will check that the constraints are equal and record an appropriate
568            // error otherwise.
569            //
570            // Later, we'll re-visit those other binding sites because they're still in
571            // `deferred_constraints`, but `set` will be empty because we already deleted the
572            // equivalence class the first time we encountered it.
573            let set = self.current_rule.equals.remove_set_of(current);
574            if let Some((&base, rest)) = set.split_first() {
575                let mut defer = |this: &Self, binding| {
576                    // We're adding equality constraints to binding sites that may not have had
577                    // one already. If that binding site already had a concrete constraint, then
578                    // we need to "recursively" propagate that constraint through the new
579                    // equivalence class too.
580                    if let Some(constraint) = this.current_rule.get_constraint(binding) {
581                        deferred_constraints.push((binding, constraint));
582                    }
583                };
584
585                // If this constraint introduces nested binding sites, make the fields of those
586                // binding sites equal instead. Arbitrarily pick one member of `set` to set all the
587                // others equal to. If there are existing constraints on the new binding sites, copy
588                // those around the new equivalence classes too.
589                let base_fields = self.set_constraint(base, constraint);
590                base_fields.iter().for_each(|&x| defer(self, x));
591                for &b in rest {
592                    for (&x, y) in base_fields.iter().zip(self.set_constraint(b, constraint)) {
593                        defer(self, y);
594                        self.current_rule.equals.merge(x, y);
595                    }
596                }
597            }
598        }
599    }
600
601    fn dedup_binding(&mut self, binding: Binding) -> BindingId {
602        if let Some(binding) = self.rules.binding_map.get(&binding) {
603            *binding
604        } else {
605            let id = BindingId(self.rules.bindings.len().try_into().unwrap());
606            self.rules.bindings.push(binding.clone());
607            self.rules.binding_map.insert(binding, id);
608            id
609        }
610    }
611
612    fn set_constraint(&mut self, input: BindingId, constraint: Constraint) -> Vec<BindingId> {
613        if let Err(e) = self.current_rule.set_constraint(input, constraint) {
614            self.unreachable.push(e);
615        }
616        constraint
617            .bindings_for(input)
618            .into_iter()
619            .map(|binding| self.dedup_binding(binding))
620            .collect()
621    }
622}
623
624impl sema::PatternVisitor for RuleSetBuilder {
625    type PatternId = BindingId;
626
627    fn add_match_equal(&mut self, a: BindingId, b: BindingId, _ty: sema::TypeId) {
628        // If both bindings represent the same binding site, they're implicitly equal.
629        if a != b {
630            self.current_rule.equals.merge(a, b);
631        }
632    }
633
634    fn add_match_bool(&mut self, input: BindingId, ty: sema::TypeId, val: bool) {
635        let bindings = self.set_constraint(input, Constraint::ConstBool { val, ty });
636        debug_assert_eq!(bindings, &[]);
637    }
638
639    fn add_match_int(&mut self, input: BindingId, ty: sema::TypeId, val: i128) {
640        let bindings = self.set_constraint(input, Constraint::ConstInt { val, ty });
641        debug_assert_eq!(bindings, &[]);
642    }
643
644    fn add_match_prim(&mut self, input: BindingId, _ty: sema::TypeId, val: sema::Sym) {
645        let bindings = self.set_constraint(input, Constraint::ConstPrim { val });
646        debug_assert_eq!(bindings, &[]);
647    }
648
649    fn add_match_variant(
650        &mut self,
651        input: BindingId,
652        input_ty: sema::TypeId,
653        arg_tys: &[sema::TypeId],
654        variant: sema::VariantId,
655    ) -> Vec<BindingId> {
656        let fields = TupleIndex(arg_tys.len().try_into().unwrap());
657        self.set_constraint(
658            input,
659            Constraint::Variant {
660                fields,
661                ty: input_ty,
662                variant,
663            },
664        )
665    }
666
667    fn add_extract_struct(
668        &mut self,
669        input: Self::PatternId,
670        input_ty: sema::TypeId,
671        arg_tys: &[sema::TypeId],
672    ) -> Vec<Self::PatternId> {
673        let fields = TupleIndex(arg_tys.len().try_into().unwrap());
674        self.set_constraint(
675            input,
676            Constraint::Struct {
677                fields,
678                ty: input_ty,
679            },
680        )
681    }
682
683    fn add_extract(
684        &mut self,
685        input: BindingId,
686        _input_ty: sema::TypeId,
687        output_tys: Vec<sema::TypeId>,
688        term: sema::TermId,
689        infallible: bool,
690        multi: bool,
691    ) -> Vec<BindingId> {
692        let source = self.dedup_binding(Binding::Extractor {
693            term,
694            parameter: input,
695        });
696
697        // If the extractor is fallible, build a pattern and constraint for `Some`
698        let source = if multi {
699            self.current_rule.iterators.insert(source);
700            self.dedup_binding(Binding::Iterator { source })
701        } else if infallible {
702            source
703        } else {
704            let bindings = self.set_constraint(source, Constraint::Some);
705            debug_assert_eq!(bindings.len(), 1);
706            bindings[0]
707        };
708
709        // If the extractor has multiple outputs, create a separate binding for each
710        match output_tys.len().try_into().unwrap() {
711            0 => vec![],
712            1 => vec![source],
713            outputs => (0..outputs)
714                .map(TupleIndex)
715                .map(|field| self.dedup_binding(Binding::MatchTuple { source, field }))
716                .collect(),
717        }
718    }
719}
720
721impl sema::ExprVisitor for RuleSetBuilder {
722    type ExprId = BindingId;
723
724    fn add_const_bool(&mut self, ty: sema::TypeId, val: bool) -> BindingId {
725        self.dedup_binding(Binding::ConstBool { val, ty })
726    }
727
728    fn add_const_int(&mut self, ty: sema::TypeId, val: i128) -> BindingId {
729        self.dedup_binding(Binding::ConstInt { val, ty })
730    }
731
732    fn add_const_prim(&mut self, _ty: sema::TypeId, val: sema::Sym) -> BindingId {
733        self.dedup_binding(Binding::ConstPrim { val })
734    }
735
736    fn add_create_variant(
737        &mut self,
738        inputs: Vec<(BindingId, sema::TypeId)>,
739        ty: sema::TypeId,
740        variant: sema::VariantId,
741    ) -> BindingId {
742        self.dedup_binding(Binding::MakeVariant {
743            ty,
744            variant,
745            fields: inputs.into_iter().map(|(expr, _)| expr).collect(),
746        })
747    }
748
749    fn add_create_struct(
750        &mut self,
751        inputs: Vec<(Self::ExprId, sema::TypeId)>,
752        ty: sema::TypeId,
753    ) -> Self::ExprId {
754        self.dedup_binding(Binding::MakeStruct {
755            ty,
756            fields: inputs.into_iter().map(|(expr, _)| expr).collect(),
757        })
758    }
759
760    fn add_construct(
761        &mut self,
762        inputs: Vec<(BindingId, sema::TypeId)>,
763        _ty: sema::TypeId,
764        term: sema::TermId,
765        pure: bool,
766        infallible: bool,
767        multi: bool,
768        _rec: bool,
769    ) -> BindingId {
770        let instance = if pure {
771            0
772        } else {
773            self.impure_instance += 1;
774            self.impure_instance
775        };
776        let source = self.dedup_binding(Binding::Constructor {
777            term,
778            parameters: inputs.into_iter().map(|(expr, _)| expr).collect(),
779            instance,
780        });
781
782        // If the constructor is fallible, build a pattern for `Some`, but not a constraint. If the
783        // constructor is on the right-hand side of a rule then its failure is not considered when
784        // deciding which rule to evaluate. Corresponding constraints are only added if this
785        // expression is subsequently used as a pattern; see `expr_as_pattern`.
786        let source = if multi {
787            self.current_rule.iterators.insert(source);
788            self.dedup_binding(Binding::Iterator { source })
789        } else if infallible {
790            source
791        } else {
792            self.dedup_binding(Binding::MatchSome { source })
793        };
794
795        if !pure {
796            self.current_rule.impure.push(source);
797        }
798
799        source
800    }
801}
802
803impl sema::RuleVisitor for RuleSetBuilder {
804    type PatternVisitor = Self;
805    type ExprVisitor = Self;
806    type Expr = BindingId;
807
808    fn add_arg(&mut self, index: usize, _ty: sema::TypeId) -> BindingId {
809        let index = TupleIndex(index.try_into().unwrap());
810        self.dedup_binding(Binding::Argument { index })
811    }
812
813    fn add_pattern<F: FnOnce(&mut Self)>(&mut self, visitor: F) {
814        visitor(self)
815    }
816
817    fn add_expr<F>(&mut self, visitor: F) -> BindingId
818    where
819        F: FnOnce(&mut Self) -> sema::VisitedExpr<Self>,
820    {
821        visitor(self).value
822    }
823
824    fn expr_as_pattern(&mut self, expr: BindingId) -> BindingId {
825        let mut todo = vec![expr];
826        while let Some(expr) = todo.pop() {
827            let expr = &self.rules.bindings[expr.index()];
828            todo.extend_from_slice(expr.sources());
829            if let &Binding::MatchSome { source } = expr {
830                let _ = self.set_constraint(source, Constraint::Some);
831            }
832        }
833        expr
834    }
835
836    fn pattern_as_expr(&mut self, pattern: BindingId) -> BindingId {
837        pattern
838    }
839}