meta_language/translation/
surface.rs

1//! The surface AST the four frontends produce and the checker consumes.
2//!
3//! Its JSON form is the JavaScript runtime's (`{ "k": "binary", "op": "add", … }`),
4//! so the frontends of both runtimes can be compared node for node.
5
6use serde::{Deserialize, Deserializer, Serialize};
7
8use super::types::Type;
9use super::{Language, Span};
10
11#[allow(clippy::trivially_copy_pass_by_ref)] // serde passes fields by reference
12const fn is_false(value: &bool) -> bool {
13    !*value
14}
15
16/// Numeral text: the JavaScript frontends store some pattern numerals as
17/// numbers and others as decimal strings.
18fn numeral<'de, D: Deserializer<'de>>(deserializer: D) -> Result<String, D::Error> {
19    #[derive(Deserialize)]
20    #[serde(untagged)]
21    enum Numeral {
22        Text(String),
23        Number(serde_json::Number),
24    }
25    Ok(match Numeral::deserialize(deserializer)? {
26        Numeral::Text(text) => text,
27        Numeral::Number(number) => number.to_string(),
28    })
29}
30
31/// A surface expression.
32#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
33pub struct SExpr {
34    #[serde(flatten)]
35    pub node: SNode,
36    #[serde(default, skip_serializing_if = "Option::is_none")]
37    pub span: Option<Span>,
38    /// Set on a Rust block expression (`{ … }`) used as a value.
39    #[serde(default, skip_serializing_if = "is_false")]
40    pub block: bool,
41    /// Set on the match a JavaScript `x.$ === 'tag'` test reads as, so an
42    /// `if` on it can narrow `x`.
43    #[serde(rename = "tagTest", default, skip_serializing_if = "Option::is_none")]
44    pub tag_test: Option<Box<STagTest>>,
45}
46
47/// A JavaScript `x.$ === 'tag'` (or `!==`) test: the tested value, the tag
48/// and the data type that has it.
49#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
50pub struct STagTest {
51    pub object: SExpr,
52    pub tag: String,
53    pub data: SData,
54    pub negated: bool,
55}
56
57impl SExpr {
58    #[must_use]
59    pub const fn new(node: SNode, span: Option<Span>) -> Self {
60        Self {
61            node,
62            span,
63            block: false,
64            tag_test: None,
65        }
66    }
67
68    /// A name reference without a span, as the checker builds them.
69    #[must_use]
70    pub fn name(name: &str) -> Self {
71        Self::new(
72            SNode::Name {
73                path: vec![name.to_owned()],
74            },
75            None,
76        )
77    }
78
79    /// The single-segment name this expression refers to, if it is one.
80    #[must_use]
81    pub fn simple_name(&self) -> Option<&str> {
82        match &self.node {
83            SNode::Name { path } if path.len() == 1 => Some(&path[0]),
84            _ => None,
85        }
86    }
87}
88
89#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
90#[serde(rename_all = "camelCase")]
91pub enum UnaryOp {
92    Not,
93    Neg,
94}
95
96/// Surface binary operators: `plus` is JavaScript's overloaded `+`.
97#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
98#[serde(rename_all = "camelCase")]
99pub enum BinaryOp {
100    Add,
101    Sub,
102    Mul,
103    Div,
104    Rem,
105    Eq,
106    Ne,
107    Lt,
108    Le,
109    Gt,
110    Ge,
111    And,
112    Or,
113    Concat,
114    Plus,
115}
116
117impl BinaryOp {
118    /// The operator's name in the checked program's JSON, such as `add`.
119    #[must_use]
120    pub const fn name(self) -> &'static str {
121        match self {
122            Self::Add => "add",
123            Self::Sub => "sub",
124            Self::Mul => "mul",
125            Self::Div => "div",
126            Self::Rem => "rem",
127            Self::Eq => "eq",
128            Self::Ne => "ne",
129            Self::Lt => "lt",
130            Self::Le => "le",
131            Self::Gt => "gt",
132            Self::Ge => "ge",
133            Self::And => "and",
134            Self::Or => "or",
135            Self::Concat => "concat",
136            Self::Plus => "plus",
137        }
138    }
139}
140
141/// Division rounding a source operator asks for.
142#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
143#[serde(rename_all = "camelCase")]
144pub enum Rounding {
145    Trunc,
146    Euclid,
147    Floor,
148}
149
150/// How a value is printed: each source language's own rendering.
151#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
152pub enum ShowStyle {
153    #[serde(rename = "lean")]
154    Lean,
155    #[serde(rename = "rocq")]
156    Rocq,
157    #[serde(rename = "rust")]
158    Rust,
159    #[serde(rename = "js-console")]
160    JsConsole,
161    #[serde(rename = "js-template")]
162    JsTemplate,
163    /// The first of several `console.log` arguments, when it is not a literal string.
164    #[serde(rename = "js-format-first")]
165    JsFormatFirst,
166    /// The argument of a `%d` directive.
167    #[serde(rename = "js-format-number")]
168    JsFormatNumber,
169    /// The argument of a `%i` directive.
170    #[serde(rename = "js-format-integer")]
171    JsFormatInteger,
172}
173
174impl ShowStyle {
175    /// True for the values `console.log` shows: its argument, or those `util.format` reads.
176    #[must_use]
177    pub const fn is_console(self) -> bool {
178        matches!(
179            self,
180            Self::JsConsole | Self::JsFormatFirst | Self::JsFormatNumber | Self::JsFormatInteger
181        )
182    }
183}
184
185/// Conversion semantics: exact, checked (aborts when out of range) or clamped.
186#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
187#[serde(rename_all = "camelCase")]
188pub enum Flavor {
189    Exact,
190    Checked,
191    Clamp,
192}
193
194#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
195#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
196pub enum SNode {
197    Num {
198        value: String,
199        #[serde(rename = "type", default, skip_serializing_if = "Option::is_none")]
200        ty: Option<Type>,
201        #[serde(default, skip_serializing_if = "is_false")]
202        negative: bool,
203        /// The 1 of `x++`, which takes the type of `x`.
204        #[serde(default, skip_serializing_if = "is_false")]
205        unit: bool,
206    },
207    Bool {
208        value: bool,
209    },
210    Str {
211        value: String,
212    },
213    Unit,
214    Name {
215        path: Vec<String>,
216    },
217    /// Lean's `.ctor`, resolved against the expected type.
218    DotCtor {
219        name: String,
220    },
221    App {
222        #[serde(rename = "fn")]
223        func: Box<SExpr>,
224        args: Vec<SExpr>,
225    },
226    Field {
227        object: Box<SExpr>,
228        field: String,
229    },
230    Unary {
231        op: UnaryOp,
232        arg: Box<SExpr>,
233    },
234    Binary {
235        op: BinaryOp,
236        left: Box<SExpr>,
237        right: Box<SExpr>,
238        #[serde(default, skip_serializing_if = "Option::is_none")]
239        rounding: Option<Rounding>,
240    },
241    If {
242        cond: Box<SExpr>,
243        then: Box<SExpr>,
244        #[serde(rename = "else")]
245        otherwise: Box<SExpr>,
246    },
247    Let {
248        name: String,
249        #[serde(rename = "type", default, skip_serializing_if = "Option::is_none")]
250        ty: Option<Type>,
251        value: Box<SExpr>,
252        body: Box<SExpr>,
253    },
254    Match {
255        scrutinees: Vec<SExpr>,
256        rows: Vec<SRow>,
257    },
258    /// A single-level match, as pattern compilation produces it.
259    Match1 {
260        scrutinee: Box<SExpr>,
261        cases: Vec<SCase>,
262    },
263    ToString {
264        arg: Box<SExpr>,
265    },
266    Show {
267        arg: Box<SExpr>,
268        style: ShowStyle,
269    },
270    Cast {
271        arg: Box<SExpr>,
272        to: Type,
273        #[serde(default, skip_serializing_if = "Option::is_none")]
274        from: Option<Type>,
275        flavor: Flavor,
276    },
277    Abort {
278        message: String,
279    },
280    /// `console.log(expr)`, then `body`.
281    Print {
282        expr: Box<SExpr>,
283        style: ShowStyle,
284        body: Box<SExpr>,
285    },
286    /// A JavaScript `{ $: 'tag', field: value }` constructor object, fields in source order.
287    CtorObject {
288        tag: String,
289        #[serde(with = "ordered_fields")]
290        fields: Vec<(String, SExpr)>,
291    },
292    /// A JavaScript array literal `[a, ...xs, b]`.
293    Array {
294        items: Vec<SArrayItem>,
295        /// The element type inference fixed for a literal with no element of its own.
296        #[serde(default, skip_serializing_if = "Option::is_none")]
297        element: Option<Type>,
298    },
299    /// `xs[i]`, a read of an array element.
300    Index {
301        object: Box<SExpr>,
302        index: Box<SExpr>,
303    },
304    /// The length of an array: a Number, or for the counter of a for…of loop a `BigInt`.
305    Length {
306        object: Box<SExpr>,
307        integer: bool,
308    },
309    /// A call of a Math or Number function, `Math.max(a, ...xs)`: `op` is
310    /// the function and `name` the path the program called it by.
311    Math {
312        op: String,
313        name: String,
314        args: Vec<SArrayItem>,
315    },
316    // Frontend-internal forms; the checker rejects them if they reach it.
317    Cons {
318        head: Box<SExpr>,
319        tail: Box<SExpr>,
320    },
321    Nil,
322    List {
323        items: Vec<SExpr>,
324    },
325    Tag {
326        tag: String,
327    },
328    Default,
329}
330
331impl SNode {
332    /// The `k` discriminant.
333    #[must_use]
334    pub const fn kind(&self) -> &'static str {
335        match self {
336            Self::Num { .. } => "num",
337            Self::Bool { .. } => "bool",
338            Self::Str { .. } => "str",
339            Self::Unit => "unit",
340            Self::Name { .. } => "name",
341            Self::DotCtor { .. } => "dotCtor",
342            Self::App { .. } => "app",
343            Self::Field { .. } => "field",
344            Self::Unary { .. } => "unary",
345            Self::Binary { .. } => "binary",
346            Self::If { .. } => "if",
347            Self::Let { .. } => "let",
348            Self::Match { .. } => "match",
349            Self::Match1 { .. } => "match1",
350            Self::ToString { .. } => "toString",
351            Self::Show { .. } => "show",
352            Self::Cast { .. } => "cast",
353            Self::Abort { .. } => "abort",
354            Self::Print { .. } => "print",
355            Self::CtorObject { .. } => "ctorObject",
356            Self::Array { .. } => "array",
357            Self::Index { .. } => "index",
358            Self::Length { .. } => "length",
359            Self::Math { .. } => "math",
360            Self::Cons { .. } => "cons",
361            Self::Nil => "nil",
362            Self::List { .. } => "list",
363            Self::Tag { .. } => "tag",
364            Self::Default => "default",
365        }
366    }
367}
368
369/// An element of an array literal, or with `spread` the elements of an array.
370#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
371pub struct SArrayItem {
372    pub spread: bool,
373    pub value: SExpr,
374}
375
376/// An object whose keys keep their insertion order, as JavaScript objects do.
377mod ordered_fields {
378    use std::fmt;
379
380    use serde::de::{MapAccess, Visitor};
381    use serde::ser::SerializeMap;
382    use serde::{Deserializer, Serializer};
383
384    use super::SExpr;
385
386    #[allow(clippy::ptr_arg)]
387    pub fn serialize<S: Serializer>(
388        fields: &Vec<(String, SExpr)>,
389        serializer: S,
390    ) -> Result<S::Ok, S::Error> {
391        let mut map = serializer.serialize_map(Some(fields.len()))?;
392        for (name, value) in fields {
393            map.serialize_entry(name, value)?;
394        }
395        map.end()
396    }
397
398    pub fn deserialize<'de, D: Deserializer<'de>>(
399        deserializer: D,
400    ) -> Result<Vec<(String, SExpr)>, D::Error> {
401        struct Fields;
402        impl<'de> Visitor<'de> for Fields {
403            type Value = Vec<(String, SExpr)>;
404            fn expecting(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
405                formatter.write_str("an object of fields")
406            }
407            fn visit_map<A: MapAccess<'de>>(self, mut map: A) -> Result<Self::Value, A::Error> {
408                let mut fields = Vec::new();
409                while let Some(entry) = map.next_entry()? {
410                    fields.push(entry);
411                }
412                Ok(fields)
413            }
414        }
415        deserializer.deserialize_map(Fields)
416    }
417}
418
419/// One row of a multi-scrutinee surface match.
420#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
421pub struct SRow {
422    pub patterns: Vec<SPattern>,
423    pub body: SExpr,
424    #[serde(default, skip_serializing_if = "Option::is_none")]
425    pub span: Option<Span>,
426}
427
428/// One case of a single-level match.
429#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
430pub struct SCase {
431    pub pattern: SCasePattern,
432    pub body: SExpr,
433    #[serde(default, skip_serializing_if = "Option::is_none")]
434    pub span: Option<Span>,
435}
436
437/// Patterns of a single-level match: one constructor, fields bound to names.
438#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
439#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
440pub enum SCasePattern {
441    Wild,
442    Bind {
443        name: String,
444    },
445    NatZero,
446    NatSucc {
447        name: String,
448    },
449    Ctor {
450        path: Vec<String>,
451        binds: Vec<Option<String>>,
452    },
453}
454
455/// A surface pattern.
456#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
457pub struct SPattern {
458    #[serde(flatten)]
459    pub node: SPatternNode,
460    #[serde(default, skip_serializing_if = "Option::is_none")]
461    pub span: Option<Span>,
462}
463
464#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
465#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
466pub enum SPatternNode {
467    Wild,
468    /// A lone name: a nullary constructor when the scrutinee type has one, else a binder.
469    BindOrCtor {
470        name: String,
471    },
472    /// A binder, which the JavaScript frontend's generated matches use.
473    Bind {
474        name: String,
475    },
476    Ctor {
477        path: Vec<String>,
478        args: Vec<SPattern>,
479    },
480    NumLit {
481        #[serde(deserialize_with = "numeral")]
482        value: String,
483        #[serde(default, skip_serializing_if = "is_false")]
484        negative: bool,
485    },
486    BoolLit {
487        value: bool,
488        #[serde(default, skip_serializing_if = "is_false")]
489        negative: bool,
490    },
491    StrLit {
492        value: String,
493    },
494    /// Lean's `n + 2`; `add` holds the numeral's decimal digits.
495    NatAdd {
496        inner: Box<SPattern>,
497        add: String,
498    },
499}
500
501#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
502#[serde(rename_all = "camelCase")]
503pub struct SBinder {
504    pub name: String,
505    #[serde(rename = "type", default, skip_serializing_if = "Option::is_none")]
506    pub ty: Option<Type>,
507    /// The Rocq type as written (`N`, `nat`, `Z`), which proof steps consult.
508    #[serde(default, skip_serializing_if = "Option::is_none")]
509    pub rocq_type: Option<String>,
510    #[serde(default, skip_serializing_if = "Option::is_none")]
511    pub span: Option<Span>,
512}
513
514/// A surface proposition.
515#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
516pub struct SProp {
517    #[serde(flatten)]
518    pub node: SPropNode,
519    #[serde(default, skip_serializing_if = "Option::is_none")]
520    pub span: Option<Span>,
521}
522
523#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
524pub struct SComparison {
525    pub left: SExpr,
526    pub right: SExpr,
527    /// JavaScript's `assert.equal`, which compares objects by identity.
528    #[serde(default, skip_serializing_if = "is_false")]
529    pub reference: bool,
530    /// `assert.strictEqual` and its kin compare with `SameValue`
531    /// (`Object.is`): `NaN` equals `NaN`, and `0` differs from `-0`.
532    #[serde(default, rename = "sameValue", skip_serializing_if = "is_false")]
533    pub same_value: bool,
534}
535
536#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
537#[serde(tag = "p", rename_all = "camelCase", rename_all_fields = "camelCase")]
538pub enum SPropNode {
539    Forall {
540        binders: Vec<SBinder>,
541        body: Box<SProp>,
542    },
543    And {
544        left: Box<SProp>,
545        right: Box<SProp>,
546    },
547    Or {
548        left: Box<SProp>,
549        right: Box<SProp>,
550    },
551    Implies {
552        left: Box<SProp>,
553        right: Box<SProp>,
554    },
555    Not {
556        arg: Box<SProp>,
557    },
558    Bool {
559        expr: SExpr,
560    },
561    Eq(SComparison),
562    Ne(SComparison),
563    Lt(SComparison),
564    Le(SComparison),
565    Gt(SComparison),
566    Ge(SComparison),
567}
568
569#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
570pub struct SRule {
571    pub name: String,
572    pub reverse: bool,
573}
574
575/// A proof step: `t` names the tactic family.
576#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
577#[serde(tag = "t", rename_all = "camelCase", rename_all_fields = "camelCase")]
578pub enum SStep {
579    Compute {
580        #[serde(default, skip_serializing_if = "Option::is_none")]
581        tactic: Option<String>,
582    },
583    Arith {
584        #[serde(default, skip_serializing_if = "Option::is_none")]
585        tactic: Option<String>,
586    },
587    Intro {
588        names: Vec<String>,
589    },
590    Unfold {
591        names: Vec<String>,
592        #[serde(default, skip_serializing_if = "Option::is_none")]
593        tactic: Option<String>,
594    },
595    Simp {
596        rules: Vec<SRule>,
597        #[serde(default, skip_serializing_if = "Option::is_none")]
598        only: Option<bool>,
599        #[serde(default, skip_serializing_if = "Option::is_none")]
600        tactic: Option<String>,
601    },
602    Rewrite {
603        rules: Vec<SRule>,
604        #[serde(default, skip_serializing_if = "Option::is_none")]
605        only: Option<bool>,
606        #[serde(default, skip_serializing_if = "Option::is_none")]
607        tactic: Option<String>,
608    },
609    Induction(SSplit),
610    Cases(SSplit),
611}
612
613#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
614pub struct SSplit {
615    pub variable: String,
616    pub cases: Vec<SSplitCase>,
617    /// Rocq names cases by position; Lean by constructor.
618    #[serde(default, skip_serializing_if = "is_false")]
619    pub positional: bool,
620    #[serde(default, skip_serializing_if = "Option::is_none")]
621    pub blocks: Option<usize>,
622}
623
624#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
625pub struct SSplitCase {
626    #[serde(default, skip_serializing_if = "Option::is_none")]
627    pub ctor: Option<String>,
628    #[serde(default, skip_serializing_if = "Option::is_none")]
629    pub index: Option<usize>,
630    pub binds: Vec<Option<String>>,
631    pub steps: Vec<SStep>,
632}
633
634#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
635#[serde(rename_all = "camelCase")]
636pub struct SProof {
637    pub steps: Vec<SStep>,
638    #[serde(default, skip_serializing_if = "Option::is_none")]
639    pub source: Option<String>,
640    pub source_language: Language,
641}
642
643#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
644#[serde(rename_all = "camelCase")]
645pub struct SField {
646    #[serde(default, skip_serializing_if = "Option::is_none")]
647    pub name: Option<String>,
648    #[serde(rename = "type")]
649    pub ty: Type,
650    /// The type as written, on a Rocq constructor field declared as a binder `(x : N)`.
651    #[serde(default, skip_serializing_if = "Option::is_none")]
652    pub rocq_type: Option<String>,
653    #[serde(default, skip_serializing_if = "Option::is_none")]
654    pub span: Option<Span>,
655}
656
657#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
658pub struct SCtor {
659    pub name: String,
660    pub fields: Vec<SField>,
661}
662
663/// The leading `if (n < 0n) throw …` of a JavaScript parameter: a negative
664/// argument aborts with its message, the guards in their order.
665#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
666pub struct Guard {
667    pub message: String,
668    pub order: usize,
669}
670
671#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
672#[serde(rename_all = "camelCase")]
673pub struct SParam {
674    pub name: String,
675    #[serde(default, rename = "default", skip_serializing_if = "Option::is_none")]
676    pub default_value: Option<SExpr>,
677    #[serde(rename = "type", default, skip_serializing_if = "Option::is_none")]
678    pub ty: Option<Type>,
679    #[serde(default, skip_serializing_if = "Option::is_none")]
680    pub span: Option<Span>,
681    /// A JavaScript parameter restricted to the naturals by a leading guard.
682    #[serde(default, skip_serializing_if = "Option::is_none")]
683    pub guard: Option<Guard>,
684    #[serde(default, skip_serializing_if = "Option::is_none")]
685    pub rocq_type: Option<String>,
686}
687
688#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
689pub struct SData {
690    pub name: String,
691    pub ctors: Vec<SCtor>,
692    #[serde(default, skip_serializing_if = "Option::is_none")]
693    pub span: Option<Span>,
694    /// A data type the translator made up, whose name may use the reserved `ml_` prefix.
695    #[serde(default, skip_serializing_if = "is_false")]
696    pub generated: bool,
697}
698
699#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
700pub struct SFn {
701    pub name: String,
702    pub params: Vec<SParam>,
703    #[serde(default, skip_serializing_if = "Option::is_none")]
704    pub ret: Option<Type>,
705    pub body: SExpr,
706    #[serde(default, skip_serializing_if = "Option::is_none")]
707    pub span: Option<Span>,
708    /// A function the translator made up, such as a lifted loop.
709    #[serde(default, skip_serializing_if = "is_false")]
710    pub generated: bool,
711}
712
713#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
714pub struct STheorem {
715    pub name: String,
716    pub binders: Vec<SBinder>,
717    pub prop: SProp,
718    pub proof: SProof,
719    #[serde(default, skip_serializing_if = "Option::is_none")]
720    pub span: Option<Span>,
721}
722
723#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
724pub struct SModule {
725    pub name: String,
726    pub items: Vec<SItem>,
727    #[serde(default, skip_serializing_if = "Option::is_none")]
728    pub span: Option<Span>,
729}
730
731#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
732#[serde(tag = "k", rename_all = "camelCase")]
733pub enum SItem {
734    Data(SData),
735    Fn(SFn),
736    Theorem(STheorem),
737    Module(SModule),
738}
739
740impl SItem {
741    #[must_use]
742    pub fn name(&self) -> &str {
743        match self {
744            Self::Data(item) => &item.name,
745            Self::Fn(item) => &item.name,
746            Self::Theorem(item) => &item.name,
747            Self::Module(item) => &item.name,
748        }
749    }
750
751    #[must_use]
752    pub const fn span(&self) -> Option<Span> {
753        match self {
754            Self::Data(item) => item.span,
755            Self::Fn(item) => item.span,
756            Self::Theorem(item) => item.span,
757            Self::Module(item) => item.span,
758        }
759    }
760}
761
762#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
763#[serde(tag = "k", rename_all = "camelCase", rename_all_fields = "camelCase")]
764pub enum SEffect {
765    Print {
766        expr: SExpr,
767        style: ShowStyle,
768        #[serde(default, skip_serializing_if = "Option::is_none")]
769        span: Option<Span>,
770    },
771    Let {
772        name: String,
773        #[serde(rename = "type", default, skip_serializing_if = "Option::is_none")]
774        ty: Option<Type>,
775        value: SExpr,
776        #[serde(default, skip_serializing_if = "is_false")]
777        constant: bool,
778        #[serde(default, skip_serializing_if = "Option::is_none")]
779        span: Option<Span>,
780    },
781    Assert {
782        prop: SProp,
783        #[serde(default, skip_serializing_if = "Option::is_none")]
784        span: Option<Span>,
785    },
786}
787
788#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
789pub struct SMain {
790    pub effects: Vec<SEffect>,
791    #[serde(default, skip_serializing_if = "Option::is_none")]
792    pub span: Option<Span>,
793    /// Every call of an async function is awaited where it is made.
794    #[serde(rename = "sequentialAsync", default, skip_serializing_if = "is_false")]
795    pub sequential_async: bool,
796}
797
798/// A parsed source program.
799#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
800pub struct SProgram {
801    pub language: Language,
802    pub items: Vec<SItem>,
803    #[serde(default)]
804    pub main: Option<SMain>,
805}
meta_language/translation/surface.rs

meta_language/translation/
surface.rs
