meta_language/translation/
check.rs

1//! The portable-core checker.
2//!
3//! Resolves names, checks types, and fixes the exact operator semantics of a
4//! surface program produced by one of the language frontends. The result is
5//! the portable-core program the emitters consume: every expression carries
6//! its type and every operator carries the source language's semantics, so a
7//! target can never silently substitute its own (for example, Lean's Euclidean
8//! `Int` division for JavaScript's truncating `BigInt` division).
9//!
10//! Mirrors `js/src/translation/check.js`, including the order in which fresh
11//! names are drawn, so both runtimes produce the same checked program.
12
13use std::collections::{HashMap, HashSet};
14
15use super::decimal::Decimal;
16use super::diagnostics::{Result, TranslationError, type_error, unsupported};
17use super::ir::{
18    Binder, ByZero, Case, Comparison, Ctor, DataDecl, Decl, Effect, Expr, Field, FnDecl, Hints,
19    Item, LitValue, Main, Node, Param, Pattern, Plan, Program, Proof, Prop, Semantics, TheoremDecl,
20};
21use super::proof::{ProofContext, ProofName, TheoremHead, normalise_proof};
22use super::surface::{
23    BinaryOp, Flavor, Rounding, SArrayItem, SCase, SCasePattern, SEffect, SExpr, SItem, SMain,
24    SNode, SPattern, SPatternNode, SProgram, SProp, SPropNode, SRow, ShowStyle, UnaryOp,
25};
26use super::types::{BOOL, FLOAT, INT, NAT, STRING, Type, UNIT, array, data, fixed, fixed_bounds};
27use super::{Language, Span};
28
29mod arrays;
30mod expressions;
31mod items;
32mod matches;
33mod math;
34mod recursion;
35pub use self::recursion::*;
36
37/// Checks a surface program into the portable core.
38///
39/// # Errors
40/// On name, type and exhaustiveness errors, and on constructs outside the portable core.
41pub fn check_program(surface: &SProgram) -> Result<Program> {
42    Checker::new(surface.language).program(surface)
43}
44
45/// Inserts the source language's implicit conversions, which only JavaScript has.
46///
47/// # Errors
48/// When the value cannot take the type.
49pub fn coerce(
50    value: Expr,
51    ty: &Type,
52    language: Language,
53    span: Option<Span>,
54    flavor: Option<Flavor>,
55) -> Result<Expr> {
56    if value.ty.is_literal() {
57        return Err(type_error("untyped literal", span));
58    }
59    if value.ty.same(ty) {
60        return Ok(value);
61    }
62    if matches!(value.node, Node::Abort { .. }) {
63        return Ok(Expr {
64            ty: ty.clone(),
65            ..value
66        });
67    }
68    if language == Language::JavaScript && value.ty == Type::Nat && *ty == Type::Int {
69        return cast_to(value, &INT, Flavor::Exact, span);
70    }
71    if language == Language::JavaScript && value.ty == Type::Int && *ty == Type::Nat {
72        return cast_to(value, &NAT, flavor.unwrap_or(Flavor::Checked), span);
73    }
74    Err(type_error(
75        format!("expected {} but found {}", ty.key(), value.ty.key()),
76        span,
77    ))
78}
79
80fn cast_to(arg: Expr, to: &Type, flavor: Flavor, span: Option<Span>) -> Result<Expr> {
81    if arg.ty.same(to) {
82        return Ok(arg);
83    }
84    let from = arg.ty.clone();
85    let cast = |arg: Expr, flavor: Flavor| {
86        Expr::new(
87            Node::Cast {
88                arg: Box::new(arg),
89                from: from.clone(),
90                to: to.clone(),
91                flavor,
92                message: None,
93                order: None,
94            },
95            to.clone(),
96        )
97    };
98    match (&from, to) {
99        (Type::Nat, Type::Int) => Ok(cast(arg, Flavor::Exact)),
100        (Type::Int, Type::Nat) => {
101            if !matches!(flavor, Flavor::Checked | Flavor::Clamp) {
102                return Err(type_error(
103                    "int to nat conversion needs checked or clamp semantics",
104                    span,
105                ));
106            }
107            Ok(cast(arg, flavor))
108        }
109        (
110            Type::Fixed {
111                bits: from_bits,
112                signed: from_signed,
113            },
114            Type::Fixed { bits, signed },
115        ) => {
116            let (source_min, source_max) = fixed_bounds(*from_bits, *from_signed);
117            let (target_min, target_max) = fixed_bounds(*bits, *signed);
118            if source_min >= target_min && source_max <= target_max {
119                return Ok(cast(arg, Flavor::Exact));
120            }
121            Err(unsupported(
122                "narrowing integer cast",
123                &format!(
124                    "{} as {} wraps in Rust and has no portable encoding yet",
125                    from.key(),
126                    to.key()
127                ),
128                span,
129            ))
130        }
131        _ => Err(type_error(
132            format!("cannot convert {} to {}", from.key(), to.key()),
133            span,
134        )),
135    }
136}
137
138/// A name in a module scope: a declaration or a data constructor.
139#[derive(Clone, Debug)]
140enum Entry {
141    Decl(String),
142    Ctor { data: String, name: String },
143}
144
145#[derive(Default)]
146struct Scope {
147    path: Vec<String>,
148    names: HashMap<String, Entry>,
149    /// Submodule name → full name.
150    modules: HashMap<String, String>,
151}
152
153/// For a local, the constructor it is known to have matched and the locals naming its fields.
154#[derive(Clone, Debug)]
155struct Fact {
156    ctor: String,
157    binds: Vec<String>,
158}
159
160#[derive(Clone, Debug, Default)]
161struct Env {
162    vars: HashMap<String, Type>,
163    known: HashMap<String, Fact>,
164}
165
166impl Env {
167    fn has(&self, name: &str) -> bool {
168        self.vars.contains_key(name)
169    }
170
171    /// Binds a local, forgetting constructor facts the new binding shadows.
172    fn bind_local(&mut self, name: &str, ty: Type) {
173        self.vars.insert(name.to_owned(), ty);
174        self.known.retain(|variable, fact| {
175            variable != name && !fact.binds.iter().any(|bind| bind == name)
176        });
177    }
178
179    /// The single-segment local a surface expression names, if it is one.
180    fn local<'a>(&self, expr: &'a SExpr) -> Option<&'a str> {
181        expr.simple_name().filter(|name| self.has(name))
182    }
183}
184
185#[derive(Clone, Debug)]
186struct Column {
187    name: String,
188    ty: Type,
189}
190
191/// Natural numeral patterns above this unfold to equality tests rather than successor chains.
192const NAT_PATTERN_UNFOLD: i128 = 16;
193
194/// A match-compilation pattern: surface patterns are normalised against their column type.
195#[derive(Clone, Debug)]
196enum NPat {
197    Surface(SPattern),
198    Wild,
199    Bind(String),
200    Nat { succ: bool, args: Vec<Self> },
201    Data { ctor: String, args: Vec<Self> },
202    Lit { value: SExpr, key: String },
203}
204
205impl NPat {
206    const fn irrefutable(&self) -> bool {
207        matches!(self, Self::Wild | Self::Bind(_))
208    }
209
210    fn ctor(&self) -> Option<&str> {
211        match self {
212            Self::Nat { succ, .. } => Some(if *succ { "succ" } else { "zero" }),
213            Self::Data { ctor, .. } => Some(ctor),
214            _ => None,
215        }
216    }
217
218    fn args(&self) -> &[Self] {
219        match self {
220            Self::Nat { args, .. } | Self::Data { args, .. } => args,
221            _ => &[],
222        }
223    }
224
225    /// A natural literal pattern's value.
226    fn nat_value(&self) -> Option<Decimal> {
227        match self {
228            Self::Lit {
229                value:
230                    SExpr {
231                        node: SNode::Num { value, .. },
232                        ..
233                    },
234                ..
235            } => Decimal::parse(value),
236            _ => None,
237        }
238    }
239
240    fn lit_key(&self) -> Option<&str> {
241        match self {
242            Self::Lit { key, .. } => Some(key),
243            _ => None,
244        }
245    }
246}
247
248#[derive(Clone, Debug)]
249struct Row {
250    patterns: Vec<NPat>,
251    body: SExpr,
252    binds: Vec<(String, String)>,
253}
254
255const fn comparison(op: BinaryOp) -> bool {
256    matches!(
257        op,
258        BinaryOp::Eq | BinaryOp::Ne | BinaryOp::Lt | BinaryOp::Le | BinaryOp::Gt | BinaryOp::Ge
259    )
260}
261
262#[allow(clippy::too_many_arguments)]
263const fn binary_node(
264    op: BinaryOp,
265    left: Box<Expr>,
266    right: Box<Expr>,
267    domain: Option<Type>,
268    semantics: Option<Semantics>,
269    rounding: Option<Rounding>,
270    by_zero: Option<ByZero>,
271) -> Node {
272    Node::Binary {
273        op,
274        left,
275        right,
276        domain,
277        semantics,
278        rounding,
279        by_zero,
280    }
281}
282
283fn plain_binary(op: BinaryOp, left: Expr, right: Expr, ty: Type) -> Expr {
284    Expr::new(
285        binary_node(op, Box::new(left), Box::new(right), None, None, None, None),
286        ty,
287    )
288}
289
290fn text_lit(ty: Type, value: impl Into<String>) -> Expr {
291    Expr::lit(ty, LitValue::Text(value.into()))
292}
293
294/// The canonical text of a negated Number: `-x`, and `NaN` for `NaN`.
295fn negate_number(text: &str) -> String {
296    if text == "NaN" {
297        return text.to_owned();
298    }
299    text.strip_prefix('-')
300        .map_or_else(|| format!("-{text}"), str::to_owned)
301}
302
303fn surface_let(name: &str, value: &str, body: SExpr, span: Option<Span>) -> SExpr {
304    SExpr::new(
305        SNode::Let {
306            name: name.to_owned(),
307            ty: None,
308            value: Box::new(SExpr::name(value)),
309            body: Box::new(body),
310        },
311        span,
312    )
313}
314
315struct Checker {
316    language: Language,
317    /// Declaration full names in declaration order.
318    order: Vec<String>,
319    decls: HashMap<String, Decl>,
320    /// Functions whose parameter and result types are resolved.
321    signatures: HashSet<String>,
322    fresh: usize,
323    modules: HashMap<String, Scope>,
324}
325
326impl Checker {
327    fn new(language: Language) -> Self {
328        let mut modules = HashMap::new();
329        modules.insert(String::new(), Scope::default());
330        Self {
331            language,
332            order: Vec::new(),
333            decls: HashMap::new(),
334            signatures: HashSet::new(),
335            fresh: 0,
336            modules,
337        }
338    }
339
340    fn program(mut self, surface: &SProgram) -> Result<Program> {
341        self.declare(&surface.items, &[])?;
342        let items = self.check_items(&surface.items)?;
343        let main = match &surface.main {
344            Some(main) => Some(self.check_main(main)?),
345            None => None,
346        };
347        for name in &self.order {
348            if let Some(Decl::Fn(entry)) = self.decls.get_mut(name) {
349                entry.body = reuse_successors(&entry.body, &HashMap::new());
350            }
351        }
352        let mut declarations: Vec<Decl> = self
353            .order
354            .iter()
355            .filter_map(|name| self.decls.remove(name))
356            .collect();
357        analyse_recursion(&mut declarations);
358        Ok(Program {
359            schema_version: 1,
360            source_language: self.language,
361            items,
362            main,
363            declarations,
364            output_threaded: false,
365            aborts_threaded: false,
366        })
367    }
368
369    fn scope_mut(&mut self, path: &[String]) -> &mut Scope {
370        self.modules
371            .get_mut(&path.join("."))
372            .unwrap_or_else(|| unreachable!("module {} is declared", path.join(".")))
373    }
374}
375
376/// Proof names resolve from the theorem's module.
377struct ProofScope<'a> {
378    checker: &'a Checker,
379    path: &'a [String],
380    span: Option<Span>,
381}
382
383impl ProofContext for ProofScope<'_> {
384    fn lookup(&self, name: &str) -> Result<Option<ProofName>> {
385        let segments: Vec<String> = name.split('.').map(str::to_owned).collect();
386        Ok(
387            match self.checker.lookup(&segments, self.path, self.span)? {
388                None => None,
389                Some(Entry::Ctor { .. }) => Some(ProofName::Other),
390                Some(Entry::Decl(full_name)) => Some(match self.checker.decls.get(&full_name) {
391                    Some(Decl::Fn(_)) => ProofName::Function(full_name),
392                    Some(Decl::Theorem(_)) => ProofName::Theorem(full_name),
393                    _ => ProofName::Other,
394                }),
395            },
396        )
397    }
398
399    fn ctors(&self, data: &str) -> Vec<Ctor> {
400        self.checker
401            .data_decl(data)
402            .map(|decl| decl.ctors.clone())
403            .unwrap_or_default()
404    }
405}
406
407fn full(path: &[String], name: &str) -> String {
408    let mut parts = path.to_vec();
409    parts.push(name.to_owned());
410    parts.join(".")
411}
412
413fn flatten<'a>(items: &'a [SItem], path: &[String], out: &mut Vec<(&'a SItem, Vec<String>)>) {
414    for item in items {
415        if let SItem::Module(module) = item {
416            let mut inner = path.to_vec();
417            inner.push(module.name.clone());
418            flatten(&module.items, &inner, out);
419        } else {
420            out.push((item, path.to_vec()));
421        }
422    }
423}
424
425fn build_items(items: &[SItem], path: &[String]) -> Vec<Item> {
426    items
427        .iter()
428        .map(|item| match item {
429            SItem::Module(module) => {
430                let mut inner = path.to_vec();
431                inner.push(module.name.clone());
432                Item::Module {
433                    name: module.name.clone(),
434                    full_name: inner.join("."),
435                    items: build_items(&module.items, &inner),
436                    span: module.span,
437                }
438            }
439            other => Item::Decl {
440                full_name: full(path, other.name()),
441            },
442        })
443        .collect()
444}
445
446const fn op_name(op: BinaryOp) -> &'static str {
447    match op {
448        BinaryOp::Add => "add",
449        BinaryOp::Sub => "sub",
450        BinaryOp::Mul => "mul",
451        BinaryOp::Div => "div",
452        BinaryOp::Rem => "rem",
453        BinaryOp::Eq => "eq",
454        BinaryOp::Ne => "ne",
455        BinaryOp::Lt => "lt",
456        BinaryOp::Le => "le",
457        BinaryOp::Gt => "gt",
458        BinaryOp::Ge => "ge",
459        BinaryOp::And => "and",
460        BinaryOp::Or => "or",
461        BinaryOp::Concat => "concat",
462        BinaryOp::Plus => "plus",
463    }
464}
465
466fn arithmetic_semantics(
467    language: Language,
468    op: BinaryOp,
469    ty: &Type,
470    rounding: Option<Rounding>,
471) -> (Semantics, Option<Rounding>, Option<ByZero>) {
472    // IEEE-754 binary64 arithmetic rounds to nearest, even on a tie; `%` is the
473    // exact truncated remainder (C fmod); nothing aborts.
474    if ty.is_float() {
475        return (Semantics::Ieee, None, None);
476    }
477    let division = matches!(op, BinaryOp::Div | BinaryOp::Rem);
478    if matches!(ty, Type::Fixed { .. }) {
479        // Rust integer arithmetic with overflow checks: `/` and `%` truncate,
480        // `div_euclid` and `rem_euclid` round Euclidean; all panic on zero.
481        return if division {
482            (
483                Semantics::Checked,
484                Some(rounding.unwrap_or(Rounding::Trunc)),
485                Some(ByZero::Abort),
486            )
487        } else {
488            (Semantics::Checked, None, None)
489        };
490    }
491    if op == BinaryOp::Sub {
492        let semantics = if *ty == Type::Nat {
493            Semantics::Truncated
494        } else {
495            Semantics::Exact
496        };
497        return (semantics, None, None);
498    }
499    if !division {
500        return (Semantics::Exact, None, None);
501    }
502    if language == Language::JavaScript {
503        return (Semantics::Exact, Some(Rounding::Trunc), Some(ByZero::Abort));
504    }
505    // Lean and Rocq division is total: x / 0 = 0 and x % 0 = x.
506    if *ty == Type::Nat {
507        return (Semantics::Exact, Some(Rounding::Trunc), Some(ByZero::Total));
508    }
509    let default = if language == Language::Lean {
510        Rounding::Euclid
511    } else {
512        Rounding::Floor
513    };
514    (
515        Semantics::Exact,
516        Some(rounding.unwrap_or(default)),
517        Some(ByZero::Total),
518    )
519}
meta_language/translation/check.rs

meta_language/translation/
check.rs
