meta_language/translation/
ir.rs

1//! The checked portable core: every expression carries its type and every
2//! operator its source semantics. Emitters consume it; the renaming passes
3//! give each target unique, legal local names.
4//!
5//! The JSON form is the JavaScript runtime's checked program, except that
6//! `declarations` is an array and `items` refer to declarations by name.
7
8use std::collections::{BTreeSet, HashMap, HashSet};
9
10use serde::{Deserialize, Serialize};
11
12use super::surface::{BinaryOp, Flavor, Guard, Rounding, UnaryOp};
13use super::types::Type;
14use super::{Language, Span};
15
16mod rename;
17#[allow(clippy::trivially_copy_pass_by_ref)] // serde passes fields by reference
18const fn is_false(value: &bool) -> bool {
19    !*value
20}
21
22pub use self::rename::*;
23
24/// Arithmetic semantics: exact on unbounded integers, checked (aborting)
25/// machine arithmetic, truncated natural subtraction, or IEEE-754 binary64
26/// arithmetic on JavaScript Numbers.
27#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
28#[serde(rename_all = "camelCase")]
29pub enum Semantics {
30    Exact,
31    Checked,
32    Truncated,
33    /// Round to nearest, even on a tie; `%` is the exact truncated remainder
34    /// (C `fmod`); nothing aborts.
35    Ieee,
36}
37
38/// What division by zero does: abort (JavaScript, Rust) or yield a total value (Lean, Rocq).
39#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
40#[serde(rename_all = "camelCase")]
41pub enum ByZero {
42    Abort,
43    Total,
44}
45
46/// A literal's value: numerals and strings are text, booleans are booleans.
47#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
48#[serde(untagged)]
49pub enum LitValue {
50    Bool(bool),
51    Text(String),
52}
53
54impl LitValue {
55    /// The value as JavaScript's `String(value)` renders it.
56    #[must_use]
57    pub fn text(&self) -> String {
58        match self {
59            Self::Bool(value) => value.to_string(),
60            Self::Text(text) => text.clone(),
61        }
62    }
63}
64
65#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
66pub struct Expr {
67    #[serde(flatten)]
68    pub node: Node,
69    #[serde(rename = "type")]
70    pub ty: Type,
71    #[serde(default, skip_serializing_if = "Option::is_none")]
72    pub span: Option<Span>,
73}
74
75impl Expr {
76    #[must_use]
77    pub const fn new(node: Node, ty: Type) -> Self {
78        Self {
79            node,
80            ty,
81            span: None,
82        }
83    }
84
85    #[must_use]
86    pub fn var(name: impl Into<String>, ty: Type) -> Self {
87        Self::new(Node::Var { name: name.into() }, ty)
88    }
89
90    #[must_use]
91    pub const fn lit(ty: Type, value: LitValue) -> Self {
92        Self::new(Node::Lit { value }, ty)
93    }
94
95    #[must_use]
96    pub const fn with_span(mut self, span: Option<Span>) -> Self {
97        self.span = span;
98        self
99    }
100
101    /// The name of the variable this expression is, if it is one.
102    #[must_use]
103    pub fn var_name(&self) -> Option<&str> {
104        match &self.node {
105            Node::Var { name } => Some(name),
106            _ => None,
107        }
108    }
109
110    /// The `k` discriminant.
111    #[must_use]
112    pub const fn kind(&self) -> &'static str {
113        self.node.kind()
114    }
115
116    /// Direct subexpressions in the JavaScript runtime's key order.
117    #[must_use]
118    pub fn children(&self) -> Vec<&Self> {
119        match &self.node {
120            Node::Lit { .. }
121            | Node::Unit
122            | Node::Var { .. }
123            | Node::Abort { .. }
124            | Node::OutNil => Vec::new(),
125            Node::Call { args, .. }
126            | Node::Ctor { args, .. }
127            | Node::Array { items: args }
128            | Node::Math { args, .. } => args.iter().collect(),
129            Node::Unary { arg, .. }
130            | Node::ToString { arg, .. }
131            | Node::Cast { arg, .. }
132            | Node::Length { array: arg } => vec![arg],
133            Node::Binary { left, right, .. }
134            | Node::Append { left, right }
135            | Node::Index {
136                array: left,
137                index: right,
138            } => vec![left, right],
139            Node::If {
140                cond,
141                then,
142                otherwise,
143            } => vec![cond, then, otherwise],
144            Node::Let { value, body, .. } => vec![value, body],
145            Node::Print { text, body } => vec![text, body],
146            Node::OutCons { head, tail } => vec![head, tail],
147            Node::Match { scrutinee, cases } => {
148                let mut children = vec![&**scrutinee];
149                children.extend(cases.iter().map(|kase| &kase.body));
150                children
151            }
152        }
153    }
154
155    /// Rebuilds the node with every direct subexpression mapped, in key order.
156    #[must_use]
157    pub fn map_children(&self, visit: &mut impl FnMut(&Self) -> Self) -> Self {
158        let node = match &self.node {
159            Node::Lit { .. }
160            | Node::Unit
161            | Node::Var { .. }
162            | Node::Abort { .. }
163            | Node::OutNil => self.node.clone(),
164            Node::Print { text, body } => {
165                let text = Box::new(visit(text));
166                let body = Box::new(visit(body));
167                Node::Print { text, body }
168            }
169            Node::OutCons { head, tail } => {
170                let head = Box::new(visit(head));
171                let tail = Box::new(visit(tail));
172                Node::OutCons { head, tail }
173            }
174            Node::Array { items } => Node::Array {
175                items: items.iter().map(&mut *visit).collect(),
176            },
177            Node::Append { left, right } => {
178                let left = Box::new(visit(left));
179                let right = Box::new(visit(right));
180                Node::Append { left, right }
181            }
182            Node::Index { array, index } => {
183                let array = Box::new(visit(array));
184                let index = Box::new(visit(index));
185                Node::Index { array, index }
186            }
187            Node::Length { array } => Node::Length {
188                array: Box::new(visit(array)),
189            },
190            Node::Math { op, args } => Node::Math {
191                op: op.clone(),
192                args: args.iter().map(&mut *visit).collect(),
193            },
194            Node::Call { func, args } => Node::Call {
195                func: func.clone(),
196                args: args.iter().map(&mut *visit).collect(),
197            },
198            Node::Ctor { data, ctor, args } => Node::Ctor {
199                data: data.clone(),
200                ctor: ctor.clone(),
201                args: args.iter().map(&mut *visit).collect(),
202            },
203            Node::Unary { op, arg, semantics } => Node::Unary {
204                op: *op,
205                arg: Box::new(visit(arg)),
206                semantics: *semantics,
207            },
208            Node::ToString { arg, console } => Node::ToString {
209                arg: Box::new(visit(arg)),
210                console: *console,
211            },
212            Node::Cast {
213                arg,
214                from,
215                to,
216                flavor,
217                message,
218                order,
219            } => Node::Cast {
220                arg: Box::new(visit(arg)),
221                from: from.clone(),
222                to: to.clone(),
223                flavor: *flavor,
224                message: message.clone(),
225                order: *order,
226            },
227            Node::Binary {
228                op,
229                left,
230                right,
231                domain,
232                semantics,
233                rounding,
234                by_zero,
235            } => {
236                let left = Box::new(visit(left));
237                let right = Box::new(visit(right));
238                Node::Binary {
239                    op: *op,
240                    left,
241                    right,
242                    domain: domain.clone(),
243                    semantics: *semantics,
244                    rounding: *rounding,
245                    by_zero: *by_zero,
246                }
247            }
248            Node::If {
249                cond,
250                then,
251                otherwise,
252            } => {
253                let cond = Box::new(visit(cond));
254                let then = Box::new(visit(then));
255                let otherwise = Box::new(visit(otherwise));
256                Node::If {
257                    cond,
258                    then,
259                    otherwise,
260                }
261            }
262            Node::Let { name, value, body } => {
263                let value = Box::new(visit(value));
264                let body = Box::new(visit(body));
265                Node::Let {
266                    name: name.clone(),
267                    value,
268                    body,
269                }
270            }
271            Node::Match { scrutinee, cases } => {
272                let scrutinee = Box::new(visit(scrutinee));
273                let cases = cases
274                    .iter()
275                    .map(|kase| Case {
276                        pattern: kase.pattern.clone(),
277                        body: visit(&kase.body),
278                    })
279                    .collect();
280                Node::Match { scrutinee, cases }
281            }
282        };
283        Self {
284            node,
285            ty: self.ty.clone(),
286            span: self.span,
287        }
288    }
289}
290
291#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
292#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
293pub enum Node {
294    Lit {
295        value: LitValue,
296    },
297    Unit,
298    Var {
299        name: String,
300    },
301    Call {
302        #[serde(rename = "fn")]
303        func: String,
304        args: Vec<Expr>,
305    },
306    Ctor {
307        data: String,
308        ctor: String,
309        args: Vec<Expr>,
310    },
311    Unary {
312        op: UnaryOp,
313        arg: Box<Expr>,
314        #[serde(default, skip_serializing_if = "Option::is_none")]
315        semantics: Option<Semantics>,
316    },
317    Binary {
318        op: BinaryOp,
319        left: Box<Expr>,
320        right: Box<Expr>,
321        /// The operand type of comparisons and arithmetic.
322        #[serde(default, skip_serializing_if = "Option::is_none")]
323        domain: Option<Type>,
324        #[serde(default, skip_serializing_if = "Option::is_none")]
325        semantics: Option<Semantics>,
326        #[serde(default, skip_serializing_if = "Option::is_none")]
327        rounding: Option<Rounding>,
328        #[serde(default, skip_serializing_if = "Option::is_none")]
329        by_zero: Option<ByZero>,
330    },
331    If {
332        cond: Box<Expr>,
333        then: Box<Expr>,
334        #[serde(rename = "else")]
335        otherwise: Box<Expr>,
336    },
337    Let {
338        name: String,
339        value: Box<Expr>,
340        body: Box<Expr>,
341    },
342    Match {
343        scrutinee: Box<Expr>,
344        cases: Vec<Case>,
345    },
346    ToString {
347        arg: Box<Expr>,
348        /// `console.log` of a Number, which prints -0 as "-0" where `String(-0)` is "0".
349        #[serde(default, skip_serializing_if = "is_false")]
350        console: bool,
351    },
352    Cast {
353        arg: Box<Expr>,
354        from: Type,
355        to: Type,
356        flavor: Flavor,
357        /// The message of the guard a checked conversion to a parameter is.
358        #[serde(default, skip_serializing_if = "Option::is_none")]
359        message: Option<String>,
360        /// The place of that guard among the callee's guards.
361        #[serde(default, skip_serializing_if = "Option::is_none")]
362        order: Option<usize>,
363    },
364    Abort {
365        message: String,
366    },
367    /// Prints `text`, then is `body`.
368    Print {
369        text: Box<Expr>,
370        body: Box<Expr>,
371    },
372    /// A JavaScript array of `items`.
373    Array {
374        items: Vec<Expr>,
375    },
376    /// The elements of `left`, then those of `right`.
377    Append {
378        left: Box<Expr>,
379        right: Box<Expr>,
380    },
381    /// The element of `array` at `index`, a Number or an integer; a read
382    /// outside the array aborts.
383    Index {
384        array: Box<Expr>,
385        index: Box<Expr>,
386    },
387    /// The number of elements of `array`, as a Number or an integer.
388    Length {
389        array: Box<Expr>,
390    },
391    /// A `Math` or `Number` function of Numbers; `maxOf` and `minOf` fold
392    /// `max` and `min` over one array.
393    Math {
394        op: String,
395        args: Vec<Expr>,
396    },
397    /// No lines printed (see `output`).
398    OutNil,
399    /// The lines `tail` with `head` printed after them.
400    OutCons {
401        head: Box<Expr>,
402        tail: Box<Expr>,
403    },
404}
405
406impl Node {
407    #[must_use]
408    pub const fn kind(&self) -> &'static str {
409        match self {
410            Self::Lit { .. } => "lit",
411            Self::Unit => "unit",
412            Self::Var { .. } => "var",
413            Self::Call { .. } => "call",
414            Self::Ctor { .. } => "ctor",
415            Self::Unary { .. } => "unary",
416            Self::Binary { .. } => "binary",
417            Self::If { .. } => "if",
418            Self::Let { .. } => "let",
419            Self::Match { .. } => "match",
420            Self::ToString { .. } => "toString",
421            Self::Cast { .. } => "cast",
422            Self::Abort { .. } => "abort",
423            Self::Print { .. } => "print",
424            Self::Array { .. } => "array",
425            Self::Append { .. } => "append",
426            Self::Index { .. } => "index",
427            Self::Length { .. } => "length",
428            Self::Math { .. } => "math",
429            Self::OutNil => "outNil",
430            Self::OutCons { .. } => "outCons",
431        }
432    }
433}
434
435#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
436pub struct Case {
437    pub pattern: Pattern,
438    pub body: Expr,
439}
440
441/// A single-level match pattern.
442#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
443#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
444pub enum Pattern {
445    Wild,
446    Bind {
447        name: String,
448    },
449    NatZero,
450    NatSucc {
451        name: String,
452    },
453    Ctor {
454        data: String,
455        ctor: String,
456        binds: Vec<Option<String>>,
457    },
458}
459
460impl Pattern {
461    /// Locals the pattern binds.
462    #[must_use]
463    pub fn bound(&self) -> Vec<&str> {
464        match self {
465            Self::Bind { name } | Self::NatSucc { name } => vec![name],
466            Self::Ctor { binds, .. } => binds.iter().flatten().map(String::as_str).collect(),
467            Self::Wild | Self::NatZero => Vec::new(),
468        }
469    }
470}
471
472#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
473pub struct Binder {
474    pub name: String,
475    #[serde(rename = "type")]
476    pub ty: Type,
477}
478
479#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
480pub struct Comparison {
481    pub left: Expr,
482    pub right: Expr,
483    pub domain: Type,
484    /// Over Numbers, `assert.strictEqual` compares with `SameValue`, not
485    /// `===`: `NaN` equals `NaN`, and `0` differs from `-0`.
486    #[serde(default, rename = "sameValue", skip_serializing_if = "is_false")]
487    pub same_value: bool,
488}
489
490#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
491#[serde(tag = "p", rename_all = "camelCase", rename_all_fields = "camelCase")]
492pub enum Prop {
493    Forall {
494        binders: Vec<Binder>,
495        body: Box<Self>,
496    },
497    And {
498        left: Box<Self>,
499        right: Box<Self>,
500    },
501    Or {
502        left: Box<Self>,
503        right: Box<Self>,
504    },
505    Implies {
506        left: Box<Self>,
507        right: Box<Self>,
508    },
509    Not {
510        arg: Box<Self>,
511    },
512    Bool {
513        expr: Expr,
514    },
515    Eq(Comparison),
516    Ne(Comparison),
517    Lt(Comparison),
518    Le(Comparison),
519    Gt(Comparison),
520    Ge(Comparison),
521}
522
523impl Prop {
524    /// The comparison operator and operands of an `eq` … `ge` proposition.
525    #[must_use]
526    pub const fn comparison(&self) -> Option<(BinaryOp, &Comparison)> {
527        match self {
528            Self::Eq(comparison) => Some((BinaryOp::Eq, comparison)),
529            Self::Ne(comparison) => Some((BinaryOp::Ne, comparison)),
530            Self::Lt(comparison) => Some((BinaryOp::Lt, comparison)),
531            Self::Le(comparison) => Some((BinaryOp::Le, comparison)),
532            Self::Gt(comparison) => Some((BinaryOp::Gt, comparison)),
533            Self::Ge(comparison) => Some((BinaryOp::Ge, comparison)),
534            _ => None,
535        }
536    }
537
538    /// Builds the comparison proposition for `op`.
539    ///
540    /// # Panics
541    /// When `op` is not a comparison.
542    #[must_use]
543    pub fn compare(op: BinaryOp, comparison: Comparison) -> Self {
544        match op {
545            BinaryOp::Eq => Self::Eq(comparison),
546            BinaryOp::Ne => Self::Ne(comparison),
547            BinaryOp::Lt => Self::Lt(comparison),
548            BinaryOp::Le => Self::Le(comparison),
549            BinaryOp::Gt => Self::Gt(comparison),
550            BinaryOp::Ge => Self::Ge(comparison),
551            other => panic!("{other:?} is not a comparison"),
552        }
553    }
554}
555
556#[derive(Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
557pub struct Hints {
558    pub unfold: Vec<String>,
559    pub lemmas: Vec<String>,
560    pub hyps: Vec<String>,
561    pub library: Vec<String>,
562    pub arith: bool,
563    pub compute: bool,
564}
565
566#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
567#[serde(tag = "k", rename_all = "camelCase")]
568pub enum Plan {
569    Close { hints: Hints },
570    Induction(Split),
571    Cases(Split),
572}
573
574#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
575pub struct Split {
576    pub variable: String,
577    #[serde(rename = "type")]
578    pub ty: Type,
579    pub cases: Vec<PlanCase>,
580}
581
582#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
583pub struct PlanCase {
584    pub ctor: String,
585    pub fields: Vec<String>,
586    pub ihs: Vec<String>,
587    pub recursive: Vec<bool>,
588    pub plan: Plan,
589}
590
591#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
592#[serde(rename_all = "camelCase")]
593pub struct Proof {
594    pub plan: Plan,
595    pub source: String,
596    pub source_language: Language,
597}
598
599#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
600pub struct Field {
601    pub name: String,
602    #[serde(rename = "type")]
603    pub ty: Type,
604}
605
606#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
607pub struct Ctor {
608    pub name: String,
609    pub fields: Vec<Field>,
610}
611
612#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
613pub struct Param {
614    pub name: String,
615    #[serde(rename = "type")]
616    pub ty: Type,
617    /// A JavaScript parameter guarded to the naturals.
618    #[serde(default)]
619    pub guard: Option<Guard>,
620    #[serde(default, rename = "default")]
621    pub default_value: Option<super::surface::SExpr>,
622}
623
624#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
625#[serde(rename_all = "camelCase")]
626pub struct DataDecl {
627    pub name: String,
628    pub ctors: Vec<Ctor>,
629    #[serde(default)]
630    pub span: Option<Span>,
631    pub full_name: String,
632    pub module_path: Vec<String>,
633    #[serde(default, skip_serializing_if = "std::ops::Not::not")]
634    pub generated: bool,
635    /// A pair of printed lines and a value (see `output`).
636    #[serde(default, skip_serializing_if = "std::ops::Not::not")]
637    pub output: bool,
638}
639
640#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
641#[serde(rename_all = "camelCase")]
642pub struct FnDecl {
643    pub name: String,
644    pub params: Vec<Param>,
645    pub ret: Type,
646    pub body: Expr,
647    #[serde(default)]
648    pub span: Option<Span>,
649    pub full_name: String,
650    pub module_path: Vec<String>,
651    pub recursive: bool,
652    /// The structurally decreasing parameter of a recursive function.
653    pub decreasing: Option<usize>,
654    #[serde(default, skip_serializing_if = "std::ops::Not::not")]
655    pub mutual: bool,
656    /// A function the translator made up, such as a lifted loop.
657    #[serde(default, skip_serializing_if = "std::ops::Not::not")]
658    pub generated: bool,
659}
660
661#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
662#[serde(rename_all = "camelCase")]
663pub struct TheoremDecl {
664    pub name: String,
665    pub binders: Vec<Binder>,
666    pub prop: Prop,
667    pub proof: Proof,
668    #[serde(default)]
669    pub span: Option<Span>,
670    pub full_name: String,
671    pub module_path: Vec<String>,
672}
673
674#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
675#[serde(tag = "k", rename_all = "camelCase")]
676#[allow(clippy::large_enum_variant)] // programs hold a handful of declarations
677pub enum Decl {
678    Data(DataDecl),
679    Fn(FnDecl),
680    Theorem(TheoremDecl),
681}
682
683impl Decl {
684    #[must_use]
685    pub fn name(&self) -> &str {
686        match self {
687            Self::Data(decl) => &decl.name,
688            Self::Fn(decl) => &decl.name,
689            Self::Theorem(decl) => &decl.name,
690        }
691    }
692
693    #[must_use]
694    pub fn full_name(&self) -> &str {
695        match self {
696            Self::Data(decl) => &decl.full_name,
697            Self::Fn(decl) => &decl.full_name,
698            Self::Theorem(decl) => &decl.full_name,
699        }
700    }
701
702    #[must_use]
703    pub fn module_path(&self) -> &[String] {
704        match self {
705            Self::Data(decl) => &decl.module_path,
706            Self::Fn(decl) => &decl.module_path,
707            Self::Theorem(decl) => &decl.module_path,
708        }
709    }
710
711    #[must_use]
712    pub const fn span(&self) -> Option<Span> {
713        match self {
714            Self::Data(decl) => decl.span,
715            Self::Fn(decl) => decl.span,
716            Self::Theorem(decl) => decl.span,
717        }
718    }
719
720    /// `data`, `fn` or `theorem`.
721    #[must_use]
722    pub const fn kind(&self) -> &'static str {
723        match self {
724            Self::Data(_) => "data",
725            Self::Fn(_) => "fn",
726            Self::Theorem(_) => "theorem",
727        }
728    }
729}
730
731/// A program item: a declaration, named by its full name, or a module.
732#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
733#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
734pub enum Item {
735    Decl {
736        full_name: String,
737    },
738    Module {
739        name: String,
740        full_name: String,
741        items: Vec<Self>,
742        #[serde(default)]
743        span: Option<Span>,
744    },
745}
746
747#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
748#[serde(tag = "k", rename_all = "camelCase")]
749#[allow(clippy::large_enum_variant)]
750pub enum Effect {
751    Print {
752        expr: Expr,
753        #[serde(default)]
754        span: Option<Span>,
755    },
756    Let {
757        name: String,
758        value: Expr,
759        #[serde(default, skip_serializing_if = "is_false")]
760        constant: bool,
761        #[serde(default)]
762        span: Option<Span>,
763    },
764    Assert {
765        prop: Prop,
766        #[serde(default)]
767        span: Option<Span>,
768    },
769    /// Prints the lines `expr` holds, oldest first (see `output`).
770    Output {
771        expr: Expr,
772        #[serde(default)]
773        span: Option<Span>,
774    },
775    /// Binds `name` to the value of `pair`, made by the first of `ctors`, or
776    /// stops main with the message of its abort, made by the second (see `output`).
777    Unwrap {
778        name: String,
779        pair: Expr,
780        data: String,
781        ctors: Vec<String>,
782        #[serde(rename = "type")]
783        ty: Type,
784        #[serde(default)]
785        span: Option<Span>,
786    },
787}
788
789#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
790pub struct Main {
791    pub effects: Vec<Effect>,
792    #[serde(default)]
793    pub span: Option<Span>,
794    /// Every call of an async function is awaited where it is made.
795    #[serde(rename = "sequentialAsync", default, skip_serializing_if = "is_false")]
796    pub sequential_async: bool,
797}
798
799/// A checked portable-core program.
800#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
801#[serde(rename_all = "camelCase")]
802pub struct Program {
803    pub schema_version: u32,
804    pub source_language: Language,
805    pub items: Vec<Item>,
806    pub main: Option<Main>,
807    /// Every declaration in source order.
808    pub declarations: Vec<Decl>,
809    /// Functions that print take and return the lines printed (see `output`).
810    #[serde(default, skip_serializing_if = "is_false")]
811    pub output_threaded: bool,
812    /// Functions that may abort return the abort's message instead of a value (see `output`).
813    #[serde(default, skip_serializing_if = "is_false")]
814    pub aborts_threaded: bool,
815}
816
817impl Program {
818    #[must_use]
819    pub fn declaration(&self, full_name: &str) -> Option<&Decl> {
820        self.declarations
821            .iter()
822            .find(|decl| decl.full_name() == full_name)
823    }
824
825    /// The data declaration named `full_name`.
826    ///
827    /// # Panics
828    /// When there is none; the checker resolves every data type it records.
829    #[must_use]
830    pub fn data(&self, full_name: &str) -> &DataDecl {
831        match self.declaration(full_name) {
832            Some(Decl::Data(decl)) => decl,
833            _ => panic!("no data declaration {full_name}"),
834        }
835    }
836
837    /// Declarations in item order, modules flattened.
838    #[must_use]
839    pub fn flat_items(&self) -> Vec<&Decl> {
840        fn walk<'a>(program: &'a Program, items: &[Item], into: &mut Vec<&'a Decl>) {
841            for item in items {
842                match item {
843                    Item::Decl { full_name } => into.extend(program.declaration(full_name)),
844                    Item::Module { items, .. } => walk(program, items, into),
845                }
846            }
847        }
848        let mut into = Vec::new();
849        walk(self, &self.items, &mut into);
850        into
851    }
852}
853
854/// A per-declaration name supply: target-legal, unique, deterministic.
855#[derive(Clone)]
856pub struct Scope<'a> {
857    ident: &'a dyn Fn(&str) -> String,
858    used: HashSet<String>,
859}
860
861impl<'a> Scope<'a> {
862    pub fn new(ident: &'a dyn Fn(&str) -> String, reserved: &BTreeSet<String>) -> Self {
863        Self {
864            ident,
865            used: reserved.iter().cloned().collect(),
866        }
867    }
868
869    pub fn fresh(&mut self, name: &str) -> String {
870        // A suffixed name is legal on its own: `end_2` needs none of the quoting of Lean's `«end»`.
871        let mut candidate = (self.ident)(name);
872        let mut index = 2;
873        while self.used.contains(&candidate) {
874            candidate = (self.ident)(&format!("{name}_{index}"));
875            index += 1;
876        }
877        self.used.insert(candidate.clone());
878        candidate
879    }
880
881    #[must_use]
882    pub fn child(&self) -> Self {
883        self.clone()
884    }
885}
886
887type Env = HashMap<String, String>;
meta_language/translation/ir.rs

meta_language/translation/
ir.rs
