cranelift_isle/
ast.rs

1//! Abstract syntax tree (AST) created from parsed ISLE.
2
3#![expect(missing_docs, reason = "fields mostly self-describing")]
4
5use crate::lexer::Pos;
6use crate::log;
7
8/// One toplevel form in an ISLE file.
9#[derive(Clone, PartialEq, Eq, Debug)]
10pub enum Def {
11    Pragma(Pragma),
12    Type(Type),
13    Rule(Rule),
14    Extractor(Extractor),
15    Decl(Decl),
16    Attr(Attr),
17    Spec(Spec),
18    SpecMacro(SpecMacro),
19    Model(Model),
20    State(State),
21    Form(Form),
22    Instantiation(Instantiation),
23    Extern(Extern),
24    Converter(Converter),
25}
26
27/// An identifier -- a variable, term symbol, or type.
28#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
29pub struct Ident(pub String, pub Pos);
30
31/// Pragmas parsed with the `(pragma <ident>)` syntax.
32#[derive(Clone, PartialEq, Eq, Debug)]
33pub enum Pragma {
34    // currently, no pragmas are defined, but the infrastructure is useful to keep around
35}
36
37/// A declaration of a type.
38#[derive(Clone, PartialEq, Eq, Debug)]
39pub struct Type {
40    pub name: Ident,
41    pub is_extern: bool,
42    pub is_nodebug: bool,
43    pub ty: TypeValue,
44    pub pos: Pos,
45}
46
47/// The actual type-value: a primitive or an enum with variants.
48#[derive(Clone, PartialEq, Eq, Debug)]
49pub enum TypeValue {
50    Primitive(Ident, Pos),
51    Enum(Vec<Variant>, Pos),
52    Struct(Fields, Pos),
53}
54
55/// One variant of an enum type.
56#[derive(Clone, PartialEq, Eq, Debug)]
57pub struct Variant {
58    pub name: Ident,
59    pub fields: Fields,
60    pub pos: Pos,
61}
62
63impl Variant {
64    pub fn full_name(enum_name: &Ident, variant_name: &Ident) -> Ident {
65        Ident(
66            format!("{}.{}", enum_name.0, variant_name.0),
67            variant_name.1,
68        )
69    }
70}
71
72/// The fields of a struct or enum variant, formatted as a struct or tuple.
73#[derive(Clone, PartialEq, Eq, Debug)]
74pub enum Fields {
75    Unit,
76    Struct(StructFields),
77    Tuple(TupleFields),
78}
79
80/// A List of named fields of a struct.
81#[derive(Clone, PartialEq, Eq, Debug)]
82pub struct StructFields {
83    pub fields: Vec<StructField>,
84    pub pos: Pos,
85}
86
87/// One named field of a struct or enum variant.
88#[derive(Clone, PartialEq, Eq, Debug)]
89pub struct StructField {
90    pub name: Ident,
91    pub ty: Ident,
92    pub pos: Pos,
93}
94
95/// A List of unnamed fields of a tuple.
96#[derive(Clone, PartialEq, Eq, Debug)]
97pub struct TupleFields {
98    pub fields: Vec<TupleField>,
99    pub pos: Pos,
100}
101
102/// One unnamed field of a tuple.
103#[derive(Clone, PartialEq, Eq, Debug)]
104pub struct TupleField {
105    pub index: usize,
106    pub ty: Ident,
107    pub pos: Pos,
108}
109
110/// A declaration of a term with its argument and return types.
111#[derive(Clone, PartialEq, Eq, Debug)]
112pub struct Decl {
113    pub term: Ident,
114    pub arg_tys: Vec<Ident>,
115    pub ret_ty: Ident,
116    /// Whether this term's constructor is pure.
117    pub pure: bool,
118    /// Whether this term can exist with some multiplicity: an
119    /// extractor or a constructor that matches multiple times, or
120    /// produces multiple values.
121    pub multi: bool,
122    /// Whether this term's constructor can fail to match.
123    pub partial: bool,
124    /// Whether this term is permitted to be recursive.
125    pub rec: bool,
126    pub pos: Pos,
127}
128
129#[derive(Clone, PartialEq, Eq, Debug)]
130pub struct Instantiation {
131    pub term: Ident,
132    pub form: Option<Ident>,
133    pub signatures: Vec<Signature>,
134    /// An untagged instantiation always applies; a tagged one contributes its
135    /// signatures only when the run does not exclude the tag.
136    pub tags: Vec<Ident>,
137    pub pos: Pos,
138}
139
140/// An attribute applied to a declaration.
141#[derive(Clone, PartialEq, Eq, Debug)]
142pub struct Attr {
143    pub target: AttrTarget,
144    pub kinds: Vec<AttrKind>,
145    pub pos: Pos,
146}
147
148/// Object an attribute applies to.
149#[derive(Clone, PartialEq, Eq, Debug)]
150pub enum AttrTarget {
151    Term(Ident),
152    Rule(Ident),
153}
154
155/// A kind of attribute that can be applied to a term declaration or rule.
156#[derive(Clone, PartialEq, Eq, Debug)]
157pub enum AttrKind {
158    /// In verification, apply rule chaining to this term.
159    ///
160    /// A term marked for chaining may omit a specification. Instead, all
161    /// possible applications of rules to this term will be generated and
162    /// verified.
163    Chain,
164
165    /// In verification, declare that the correctness of lower priority rules
166    /// depends on this rule not matching.
167    ///
168    /// During rule expansion, any higher-priority overlapping rules that have
169    /// the priority tag will have their match conditions negated and added to
170    /// the verification conditions.
171    ///
172    /// Note that care must be taken when using this tag: if the specification
173    /// for the match conditions of the higher priority rule are an
174    /// over-approximation of reality, then the assumptions made by lower
175    /// priority rules will be an under-approximation. In an extreme case this
176    /// may cause the verifier to determine the lower priority rule never
177    /// applies. In a more subtle case, it could cause bugs to be missed.
178    Priority,
179
180    /// Tag allows for categorizing terms and rules.
181    Tag(Ident),
182}
183
184/// An expression used to specify term semantics, similar to SMT-LIB syntax.
185#[derive(Clone, PartialEq, Eq, Debug)]
186pub enum SpecExpr {
187    /// An operator that matches a constant integer value.
188    ConstInt {
189        val: i128,
190        pos: Pos,
191    },
192    /// An operator that matches a constant bitvector value.
193    ConstBitVec {
194        val: u128,
195        width: usize,
196        pos: Pos,
197    },
198    /// An operator that matches a constant boolean value.
199    ConstBool {
200        val: bool,
201        pos: Pos,
202    },
203    // A variable
204    Var {
205        var: Ident,
206        pos: Pos,
207    },
208    // As expression specifies the intended type of the expression. Functionally
209    // it is the identity. Analogous to qualified identifiers in SMT-LIB.
210    As {
211        x: Box<SpecExpr>,
212        ty: ModelType,
213        pos: Pos,
214    },
215    /// Struct field access.
216    Field {
217        field: Ident,
218        x: Box<SpecExpr>,
219        pos: Pos,
220    },
221    /// Discriminator is a predicate that tests the variant of an enum value.
222    Discriminator {
223        variant: Ident,
224        x: Box<SpecExpr>,
225        pos: Pos,
226    },
227    /// An application of a type variant or term.
228    Op {
229        op: SpecOp,
230        args: Vec<SpecExpr>,
231        pos: Pos,
232    },
233    /// Enum pattern matching.
234    Match {
235        x: Box<SpecExpr>,
236        arms: Vec<Arm>,
237        pos: Pos,
238    },
239    /// Let bindings.
240    Let {
241        defs: Vec<(Ident, SpecExpr)>,
242        body: Box<SpecExpr>,
243        pos: Pos,
244    },
245    /// Introduce new uninitialized variables.
246    With {
247        decls: Vec<Ident>,
248        body: Box<SpecExpr>,
249        pos: Pos,
250    },
251    /// Inline macro definition, or lambda.
252    Macro {
253        /// Parameter names.
254        params: Vec<Ident>,
255        /// Macro expansion.
256        body: Box<SpecExpr>,
257        pos: Pos,
258    },
259    /// Macro expansion.
260    Expand {
261        name: Ident,
262        args: Vec<SpecExpr>,
263        pos: Pos,
264    },
265    /// Pairs, currently used for switch statements.
266    Pair {
267        l: Box<SpecExpr>,
268        r: Box<SpecExpr>,
269        pos: Pos,
270    },
271    /// Construct enum variant.
272    Enum {
273        name: Ident,
274        variant: Ident,
275        args: Vec<SpecExpr>,
276        pos: Pos,
277    },
278    /// Construct struct value.
279    Struct {
280        fields: Vec<FieldInit>,
281        pos: Pos,
282    },
283}
284
285impl SpecExpr {
286    pub fn pos(&self) -> Pos {
287        match self {
288            &Self::ConstInt { pos, .. }
289            | &Self::ConstBitVec { pos, .. }
290            | &Self::ConstBool { pos, .. }
291            | &Self::Var { pos, .. }
292            | &Self::As { pos, .. }
293            | &Self::Field { pos, .. }
294            | &Self::Discriminator { pos, .. }
295            | &Self::Op { pos, .. }
296            | &Self::Match { pos, .. }
297            | &Self::Let { pos, .. }
298            | &Self::With { pos, .. }
299            | &Self::Macro { pos, .. }
300            | &Self::Expand { pos, .. }
301            | &Self::Pair { pos, .. }
302            | &Self::Enum { pos, .. }
303            | &Self::Struct { pos, .. } => pos,
304        }
305    }
306}
307
308/// An operation used to specify term semantics, similar to SMT-LIB syntax.
309#[derive(Clone, PartialEq, Eq, Debug)]
310pub enum SpecOp {
311    // Boolean operations
312    Eq,
313    And,
314    Or,
315    Not,
316    Imp,
317
318    // Integer arithmetic operations
319    Add,
320    Sub,
321    Mul,
322
323    // Integer comparisons
324    Lt,
325    Lte,
326    Gt,
327    Gte,
328
329    // Bitwise bitvector operations (directly SMT-LIB)
330    BVNot,
331    BVAnd,
332    BVOr,
333    BVXor,
334
335    // Bitvector arithmetic operations  (directly SMT-LIB)
336    BVNeg,
337    BVAdd,
338    BVSub,
339    BVMul,
340    BVUdiv,
341    BVUrem,
342    BVSdiv,
343    BVSrem,
344    BVShl,
345    BVLshr,
346    BVAshr,
347
348    // Bitvector comparison operations  (directly SMT-LIB)
349    BVUle,
350    BVUlt,
351    BVUgt,
352    BVUge,
353    BVSlt,
354    BVSle,
355    BVSgt,
356    BVSge,
357
358    // Bitvector overflow checks (SMT-LIB pending standardization)
359    BVSaddo,
360
361    // Desugared bitvector arithmetic operations
362    Rotr,
363    Rotl,
364    Extract,
365    ZeroExt,
366    SignExt,
367    Concat,
368    Replicate,
369
370    // Floating point (IEEE 754-2008)
371    FPEq,
372    FPNe,
373    FPLt,
374    FPGt,
375    FPLe,
376    FPGe,
377    FPPositiveInfinity,
378    FPNegativeInfinity,
379    FPPositiveZero,
380    FPNegativeZero,
381    FPNaN,
382    FPAdd,
383    FPSub,
384    FPMul,
385    FPDiv,
386    FPMin,
387    FPMax,
388    FPNeg,
389    FPCeil,
390    FPFloor,
391    FPSqrt,
392    FPTrunc,
393    FPNearest,
394    FPIsZero,
395    FPIsInfinite,
396    FPIsNaN,
397    FPIsNegative,
398    FPIsPositive,
399
400    // Custom encodings
401    Popcnt,
402    Clz,
403    Cls,
404    Rev,
405
406    // Conversion operations
407    ConvTo,
408    Int2BV,
409    BV2Nat,
410    ToFP,
411    ToFPUnsigned,
412    ToFPFromFP,
413    FPToUBV,
414    FPToSBV,
415    WidthOf,
416
417    // Control operations
418    If,
419    Switch,
420}
421
422/// Arm of a spec match expression.
423#[derive(Clone, PartialEq, Eq, Debug)]
424pub struct Arm {
425    pub variant: Ident,
426    pub args: Vec<Ident>,
427    pub body: SpecExpr,
428    pub pos: Pos,
429}
430
431/// Field initializer in a struct constructor.
432#[derive(Clone, PartialEq, Eq, Debug)]
433pub struct FieldInit {
434    pub name: Ident,
435    pub value: Box<SpecExpr>,
436    pub pos: Pos,
437}
438
439#[derive(Clone, PartialEq, Eq, Debug)]
440pub struct SpecMacro {
441    /// Macro name.
442    pub name: Ident,
443    /// Parameter names.
444    pub params: Vec<Ident>,
445    /// Macro expansion.
446    pub body: SpecExpr,
447    pub pos: Pos,
448}
449
450/// State modification clause.
451#[derive(Clone, PartialEq, Eq, Debug)]
452pub struct Modifies {
453    pub state: Ident,
454    pub cond: Option<Ident>,
455}
456
457/// A specification of the semantics of a term.
458#[derive(Clone, PartialEq, Eq, Debug)]
459pub struct Spec {
460    /// The term name (must match a (decl ...))
461    pub term: Ident,
462    /// Argument names
463    pub args: Vec<Ident>,
464    /// Provide statements, which give the semantics of the produces value
465    pub provides: Vec<SpecExpr>,
466    /// Require statements, which express preconditions on the term
467    pub requires: Vec<SpecExpr>,
468    /// Match conditions, which specify when a partial term returns a value.
469    pub matches: Vec<SpecExpr>,
470    /// State variables modified by the term.
471    pub modifies: Vec<Modifies>,
472    pub pos: Pos,
473}
474
475/// A model of an SMT-LIB type.
476#[derive(Clone, PartialEq, Eq, Debug)]
477pub enum ModelType {
478    /// Unspecified type.
479    ///
480    /// Unlike an auto-derived type, unspecified is a concrete type. However,
481    /// values of this type cannot be used for anything non-trivial. It is
482    /// intended to be used as a placeholder for a type that is not yet known,
483    /// but only appears in rules that are not yet covered by verification.
484    Unspecified,
485    /// Automatically deduced primitive type, left to type-inference to determine.
486    Auto,
487    /// SMT-LIB Int
488    Int,
489    /// SMT-LIB Bool
490    Bool,
491    /// Unit type.
492    Unit,
493    /// SMT-LIB bitvector, but with a potentially-polymorphic width
494    BitVec(Option<usize>),
495    /// Structured type.
496    Struct(Vec<ModelField>),
497    /// Same model as the named type.
498    Named(Ident),
499}
500
501#[derive(Clone, PartialEq, Eq, Debug)]
502pub struct ModelField {
503    pub name: Ident,
504    pub ty: ModelType,
505}
506
507/// A construct's value in SMT-LIB
508#[derive(Clone, PartialEq, Eq, Debug)]
509pub enum ModelValue {
510    /// Correspond to ISLE types
511    TypeValue(ModelType),
512    /// Corresponds to ISLE external constants.
513    ConstValue(SpecExpr),
514}
515
516/// A model of a construct into SMT-LIB (currently, types or enums)
517#[derive(Clone, PartialEq, Eq, Debug)]
518pub struct Model {
519    /// The name of the type or enum
520    pub name: Ident,
521    /// The value of the type or enum (potentially multiple values)
522    pub val: ModelValue,
523}
524
525/// Declare an element of global state accessible by verification specs.
526#[derive(Clone, PartialEq, Eq, Debug)]
527pub struct State {
528    /// Name of the state element.
529    pub name: Ident,
530    /// Type of the state element.
531    pub ty: ModelType,
532    /// Default specification, applied if the state is not modified.
533    pub default: SpecExpr,
534    pub pos: Pos,
535}
536
537#[derive(Clone, PartialEq, Eq, Debug)]
538pub struct Signature {
539    pub args: Vec<ModelType>,
540    pub ret: ModelType,
541    pub pos: Pos,
542}
543
544#[derive(Clone, PartialEq, Eq, Debug)]
545pub struct Form {
546    pub name: Ident,
547    pub signatures: Vec<Signature>,
548    pub pos: Pos,
549}
550
551#[derive(Clone, PartialEq, Eq, Debug)]
552pub struct Rule {
553    pub pattern: Pattern,
554    pub iflets: Vec<IfLet>,
555    pub expr: Expr,
556    pub pos: Pos,
557    pub prio: Option<i64>,
558    pub name: Option<Ident>,
559}
560
561#[derive(Clone, PartialEq, Eq, Debug)]
562pub struct IfLet {
563    pub pattern: Pattern,
564    pub expr: Expr,
565    pub pos: Pos,
566}
567
568/// An extractor macro: (A x y) becomes (B x _ y ...). Expanded during
569/// ast-to-sema pass.
570#[derive(Clone, PartialEq, Eq, Debug)]
571pub struct Extractor {
572    pub term: Ident,
573    pub args: Vec<Ident>,
574    pub template: Pattern,
575    pub pos: Pos,
576}
577
578/// A pattern: the left-hand side of a rule.
579#[derive(Clone, PartialEq, Eq, Debug)]
580pub enum Pattern {
581    /// A mention of a variable.
582    ///
583    /// Equivalent either to a binding (which can be emulated with
584    /// `BindPattern` with a `Pattern::Wildcard` subpattern), if this
585    /// is the first mention of the variable, in order to capture its
586    /// value; or else a match of the already-captured value. This
587    /// disambiguation happens when we lower `ast` nodes to `sema`
588    /// nodes as we resolve bound variable names.
589    Var { var: Ident, pos: Pos },
590    /// An operator that binds a variable to a subterm and matches the
591    /// subpattern.
592    BindPattern {
593        var: Ident,
594        subpat: Box<Pattern>,
595        pos: Pos,
596    },
597    /// An operator that matches a constant boolean value.
598    ConstBool { val: bool, pos: Pos },
599    /// An operator that matches a constant integer value.
600    ConstInt { val: i128, pos: Pos },
601    /// An operator that matches an external constant value.
602    ConstPrim { val: Ident, pos: Pos },
603    /// An application of a type variant or term.
604    Term {
605        sym: Ident,
606        args: Vec<Pattern>,
607        pos: Pos,
608    },
609    /// An operator that matches anything.
610    Wildcard { pos: Pos },
611    /// N sub-patterns that must all match.
612    And { subpats: Vec<Pattern>, pos: Pos },
613    /// Internal use only: macro argument in a template.
614    MacroArg { index: usize, pos: Pos },
615}
616
617impl Pattern {
618    pub fn root_term(&self) -> Option<&Ident> {
619        match self {
620            &Pattern::Term { ref sym, .. } => Some(sym),
621            _ => None,
622        }
623    }
624
625    /// Call `f` for each of the terms in this pattern.
626    pub fn terms(&self, f: &mut dyn FnMut(Pos, &Ident)) {
627        match self {
628            Pattern::Term { sym, args, pos } => {
629                f(*pos, sym);
630                for arg in args {
631                    arg.terms(f);
632                }
633            }
634            Pattern::And { subpats, .. } => {
635                for p in subpats {
636                    p.terms(f);
637                }
638            }
639            Pattern::BindPattern { subpat, .. } => {
640                subpat.terms(f);
641            }
642            Pattern::Var { .. }
643            | Pattern::ConstBool { .. }
644            | Pattern::ConstInt { .. }
645            | Pattern::ConstPrim { .. }
646            | Pattern::Wildcard { .. }
647            | Pattern::MacroArg { .. } => {}
648        }
649    }
650
651    pub fn make_macro_template(&self, macro_args: &[Ident]) -> Pattern {
652        log!("make_macro_template: {:?} with {:?}", self, macro_args);
653        match self {
654            &Pattern::BindPattern {
655                ref var,
656                ref subpat,
657                pos,
658                ..
659            } if matches!(&**subpat, &Pattern::Wildcard { .. }) => {
660                if let Some(i) = macro_args.iter().position(|arg| arg.0 == var.0) {
661                    Pattern::MacroArg { index: i, pos }
662                } else {
663                    self.clone()
664                }
665            }
666            &Pattern::BindPattern {
667                ref var,
668                ref subpat,
669                pos,
670            } => Pattern::BindPattern {
671                var: var.clone(),
672                subpat: Box::new(subpat.make_macro_template(macro_args)),
673                pos,
674            },
675            &Pattern::Var { ref var, pos } => {
676                if let Some(i) = macro_args.iter().position(|arg| arg.0 == var.0) {
677                    Pattern::MacroArg { index: i, pos }
678                } else {
679                    self.clone()
680                }
681            }
682            &Pattern::And { ref subpats, pos } => {
683                let subpats = subpats
684                    .iter()
685                    .map(|subpat| subpat.make_macro_template(macro_args))
686                    .collect::<Vec<_>>();
687                Pattern::And { subpats, pos }
688            }
689            &Pattern::Term {
690                ref sym,
691                ref args,
692                pos,
693            } => {
694                let args = args
695                    .iter()
696                    .map(|arg| arg.make_macro_template(macro_args))
697                    .collect::<Vec<_>>();
698                Pattern::Term {
699                    sym: sym.clone(),
700                    args,
701                    pos,
702                }
703            }
704
705            &Pattern::Wildcard { .. }
706            | &Pattern::ConstBool { .. }
707            | &Pattern::ConstInt { .. }
708            | &Pattern::ConstPrim { .. } => self.clone(),
709            &Pattern::MacroArg { .. } => unreachable!(),
710        }
711    }
712
713    pub fn subst_macro_args(&self, macro_args: &[Pattern]) -> Option<Pattern> {
714        log!("subst_macro_args: {:?} with {:?}", self, macro_args);
715        match self {
716            &Pattern::BindPattern {
717                ref var,
718                ref subpat,
719                pos,
720            } => Some(Pattern::BindPattern {
721                var: var.clone(),
722                subpat: Box::new(subpat.subst_macro_args(macro_args)?),
723                pos,
724            }),
725            &Pattern::And { ref subpats, pos } => {
726                let subpats = subpats
727                    .iter()
728                    .map(|subpat| subpat.subst_macro_args(macro_args))
729                    .collect::<Option<Vec<_>>>()?;
730                Some(Pattern::And { subpats, pos })
731            }
732            &Pattern::Term {
733                ref sym,
734                ref args,
735                pos,
736            } => {
737                let args = args
738                    .iter()
739                    .map(|arg| arg.subst_macro_args(macro_args))
740                    .collect::<Option<Vec<_>>>()?;
741                Some(Pattern::Term {
742                    sym: sym.clone(),
743                    args,
744                    pos,
745                })
746            }
747
748            &Pattern::Var { .. }
749            | &Pattern::Wildcard { .. }
750            | &Pattern::ConstBool { .. }
751            | &Pattern::ConstInt { .. }
752            | &Pattern::ConstPrim { .. } => Some(self.clone()),
753            &Pattern::MacroArg { index, .. } => macro_args.get(index).cloned(),
754        }
755    }
756
757    pub fn pos(&self) -> Pos {
758        match self {
759            &Pattern::ConstBool { pos, .. }
760            | &Pattern::ConstInt { pos, .. }
761            | &Pattern::ConstPrim { pos, .. }
762            | &Pattern::And { pos, .. }
763            | &Pattern::Term { pos, .. }
764            | &Pattern::BindPattern { pos, .. }
765            | &Pattern::Var { pos, .. }
766            | &Pattern::Wildcard { pos, .. }
767            | &Pattern::MacroArg { pos, .. } => pos,
768        }
769    }
770}
771
772/// An expression: the right-hand side of a rule.
773///
774/// Note that this *almost* looks like a core Lisp or lambda calculus,
775/// except that there is no abstraction (lambda). This first-order
776/// limit is what makes it analyzable.
777#[derive(Clone, PartialEq, Eq, Debug)]
778pub enum Expr {
779    /// A term: `(sym args...)`.
780    Term {
781        sym: Ident,
782        args: Vec<Expr>,
783        pos: Pos,
784    },
785    /// A variable use.
786    Var { name: Ident, pos: Pos },
787    /// A constant boolean.
788    ConstBool { val: bool, pos: Pos },
789    /// A constant integer.
790    ConstInt { val: i128, pos: Pos },
791    /// A constant of some other primitive type.
792    ConstPrim { val: Ident, pos: Pos },
793    /// The `(let ((var ty val)*) body)` form.
794    Let {
795        defs: Vec<LetDef>,
796        body: Box<Expr>,
797        pos: Pos,
798    },
799}
800
801impl Expr {
802    pub fn pos(&self) -> Pos {
803        match self {
804            &Expr::Term { pos, .. }
805            | &Expr::Var { pos, .. }
806            | &Expr::ConstBool { pos, .. }
807            | &Expr::ConstInt { pos, .. }
808            | &Expr::ConstPrim { pos, .. }
809            | &Expr::Let { pos, .. } => pos,
810        }
811    }
812
813    /// Call `f` for each of the terms in this expression.
814    pub fn terms(&self, f: &mut dyn FnMut(Pos, &Ident)) {
815        match self {
816            Expr::Term { sym, args, pos } => {
817                f(*pos, sym);
818                for arg in args {
819                    arg.terms(f);
820                }
821            }
822            Expr::Let { defs, body, .. } => {
823                for def in defs {
824                    def.val.terms(f);
825                }
826                body.terms(f);
827            }
828            Expr::Var { .. }
829            | Expr::ConstBool { .. }
830            | Expr::ConstInt { .. }
831            | Expr::ConstPrim { .. } => {}
832        }
833    }
834}
835
836/// One variable locally bound in a `(let ...)` expression.
837#[derive(Clone, PartialEq, Eq, Debug)]
838pub struct LetDef {
839    pub var: Ident,
840    pub ty: Ident,
841    pub val: Box<Expr>,
842    pub pos: Pos,
843}
844
845/// An external binding: an extractor or constructor function attached
846/// to a term.
847#[derive(Clone, PartialEq, Eq, Debug)]
848pub enum Extern {
849    /// An external extractor: `(extractor Term rustfunc)` form.
850    Extractor {
851        /// The term to which this external extractor is attached.
852        term: Ident,
853        /// The Rust function name.
854        func: Ident,
855        /// The position of this decl.
856        pos: Pos,
857        /// Infallibility: if an external extractor returns `(T1, T2,
858        /// ...)` rather than `Option<(T1, T2, ...)>`, and hence can
859        /// never fail, it is declared as such and allows for slightly
860        /// better code to be generated.
861        infallible: bool,
862    },
863    /// An external constructor: `(constructor Term rustfunc)` form.
864    Constructor {
865        /// The term to which this external constructor is attached.
866        term: Ident,
867        /// The Rust function name.
868        func: Ident,
869        /// The position of this decl.
870        pos: Pos,
871    },
872    /// An external constant: `(const $IDENT type)` form.
873    Const { name: Ident, ty: Ident, pos: Pos },
874}
875
876/// An implicit converter: the given term, which must have type
877/// (inner_ty) -> outer_ty, is used either in extractor or constructor
878/// position as appropriate when a type mismatch with the given pair
879/// of types would otherwise occur.
880#[derive(Clone, Debug, PartialEq, Eq)]
881pub struct Converter {
882    /// The term name.
883    pub term: Ident,
884    /// The "inner type": the type to convert *from*, on the
885    /// right-hand side, or *to*, on the left-hand side. Must match
886    /// the singular argument type of the term.
887    pub inner_ty: Ident,
888    /// The "outer type": the type to convert *to*, on the right-hand
889    /// side, or *from*, on the left-hand side. Must match the ret_ty
890    /// of the term.
891    pub outer_ty: Ident,
892    /// The position of this converter decl.
893    pub pos: Pos,
894}
cranelift_isle/ast.rs

cranelift_isle/
ast.rs
