Skip to main content

meta_language/translation/
emit_common.rs

1//! State shared by the emitters.
2//!
3//! The state holds target names for every declaration, the source-to-target
4//! mapping, and the encodings and assumptions a translation relies on. Every
5//! emitter records what it did here, so the translation contract lists exactly
6//! the choices that were made for this program.
7//!
8//! Mirrors `js/src/translation/emit-common.js`.
9
10use std::collections::{BTreeSet, HashMap, HashSet};
11
12use serde::{Deserialize, Serialize};
13
14use super::diagnostics::{Result, unsupported};
15use super::ir::{Decl, Effect, Expr, Node, Pattern, Plan, Program, Prop};
16use super::types::Type;
17use super::{Language, Span};
18
19/// A fixed assumption text, so that contracts compare across runtimes.
20#[derive(Clone, Copy, Debug)]
21pub struct AssumptionText {
22    pub id: &'static str,
23    pub statement: &'static str,
24}
25
26pub const IN_BOUNDS_READS: AssumptionText = AssumptionText {
27    id: "in-bounds-array-reads",
28    statement: "the translation agrees with the source on executions whose array reads are in bounds; JavaScript reads undefined at an index outside an array, where the target aborts",
29};
30
31/// Where a source declaration went in the target.
32#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
33#[serde(rename_all = "camelCase")]
34pub struct Mapping {
35    pub kind: String,
36    pub source: String,
37    pub target: String,
38    pub source_span: Option<Span>,
39}
40
41/// An assumption the translation relies on, with the program-specific details.
42#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
43pub struct Assumption {
44    pub id: String,
45    pub statement: String,
46    pub details: Vec<String>,
47}
48
49/// A representation choice the translation made.
50#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
51pub struct Encoding {
52    pub id: String,
53    pub statement: String,
54}
55
56/// A theorem or assertion the target states, and how it is discharged.
57#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
58#[serde(rename_all = "camelCase")]
59pub struct TheoremRecord {
60    pub source: String,
61    pub target: String,
62    pub kind: String,
63    pub closed_goal: bool,
64    #[serde(default, skip_serializing_if = "Option::is_none")]
65    pub discharge: Option<String>,
66    #[serde(default, skip_serializing_if = "Option::is_none")]
67    pub check: Option<String>,
68}
69
70/// An emitted target program together with its translation contract.
71#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
72pub struct Emitted {
73    pub language: Language,
74    pub text: String,
75    /// The helper definitions `text` starts with, in order. Not part of the
76    /// serialised contract.
77    #[serde(skip)]
78    pub preludes: Vec<String>,
79    /// The translated top-level definitions of `text`, in order, without the
80    /// header, the preludes and the entry point. Not part of the serialised
81    /// contract.
82    #[serde(skip)]
83    pub definitions: Vec<String>,
84    pub mappings: Vec<Mapping>,
85    pub assumptions: Vec<Assumption>,
86    pub encodings: Vec<Encoding>,
87    pub theorems: Vec<TheoremRecord>,
88    pub entry: Option<String>,
89}
90
91/// How constructors are named: inside a module next to their type (Rocq), or under the type.
92#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
93pub enum CtorStyle {
94    Module,
95    #[default]
96    Data,
97}
98
99/// Target naming rules for [`EmitState`].
100#[derive(Clone, Copy, Default)]
101#[allow(clippy::struct_excessive_bools)] // the flags mirror independent target namespaces
102pub struct EmitOptions {
103    pub ctor_style: CtorStyle,
104    pub type_name: Option<fn(&str) -> String>,
105    pub value_name: Option<fn(&str) -> String>,
106    pub ctor_name: Option<fn(&str) -> String>,
107    pub module_segment: Option<fn(&str) -> String>,
108    /// Names the target itself derives from a declaration (Rocq's `f_equation`, `T_ind`).
109    pub generated: Option<fn(&str) -> Vec<String>>,
110    pub type_space: bool,
111    pub modules_share_term_space: bool,
112    pub modules_share_type_space: bool,
113    /// Names root declarations may not take because the target's prelude has them.
114    pub root_reserved: &'static [&'static str],
115}
116
117struct Target {
118    local: String,
119    path: Vec<String>,
120}
121
122pub struct EmitState<'p> {
123    pub program: &'p Program,
124    pub language: Language,
125    pub ident: fn(&str) -> String,
126    reserved: BTreeSet<String>,
127    options: EmitOptions,
128    names: HashMap<String, Target>,
129    ctor_names: HashMap<String, String>,
130    module_names: HashMap<String, String>,
131    taken: HashMap<String, HashSet<String>>,
132    claimed: BTreeSet<String>,
133    pub mappings: Vec<Mapping>,
134    assumptions: Vec<Assumption>,
135    encodings: Vec<Encoding>,
136    pub theorems: Vec<TheoremRecord>,
137}
138
139impl<'p> EmitState<'p> {
140    #[must_use]
141    pub fn new(
142        program: &'p Program,
143        language: Language,
144        ident: fn(&str) -> String,
145        reserved: &[&str],
146        options: EmitOptions,
147    ) -> Self {
148        let mut state = Self {
149            program,
150            language,
151            ident,
152            reserved: reserved.iter().map(|name| (*name).to_owned()).collect(),
153            options,
154            names: HashMap::new(),
155            ctor_names: HashMap::new(),
156            module_names: HashMap::new(),
157            taken: HashMap::new(),
158            claimed: BTreeSet::new(),
159            mappings: Vec::new(),
160            assumptions: Vec::new(),
161            encodings: Vec::new(),
162            theorems: Vec::new(),
163        };
164        state.assign();
165        state
166    }
167
168    /// Target names are fixed up front, so references never depend on emission order.
169    fn assign(&mut self) {
170        let module_name = self.options.module_segment.unwrap_or(self.ident);
171        // JavaScript modules are values; Rust modules share the type namespace.
172        let module_space = if self.options.modules_share_term_space {
173            "term"
174        } else if self.options.modules_share_type_space {
175            "type"
176        } else {
177            "module"
178        };
179        let program = self.program;
180        for entry in &program.declarations {
181            let module_path = entry.module_path();
182            let mut segments = Vec::new();
183            for (index, segment) in module_path.iter().enumerate() {
184                let key = module_path[..=index].join(".");
185                if !self.module_names.contains_key(&key) {
186                    let parent = module_path[..index].join(".");
187                    let name =
188                        self.claim(&format!("{module_space}:{parent}"), &module_name(segment));
189                    self.module_names.insert(key.clone(), name);
190                }
191                segments.push(self.module_names[&key].clone());
192            }
193            let space = format!("term:{}", module_path.join("."));
194            let base = match entry {
195                Decl::Data(_) => self.options.type_name.unwrap_or(self.ident)(entry.name()),
196                _ => self.options.value_name.unwrap_or(self.ident)(entry.name()),
197            };
198            let local_space = if matches!(entry, Decl::Data(_)) && self.options.type_space {
199                format!("type:{}", module_path.join("."))
200            } else {
201                space.clone()
202            };
203            let local = self.claim(&local_space, &base);
204            self.names.insert(
205                entry.full_name().to_owned(),
206                Target {
207                    local,
208                    path: segments,
209                },
210            );
211            if let Decl::Data(data) = entry {
212                for ctor in &data.ctors {
213                    let ctor_base = self.options.ctor_name.unwrap_or(self.ident)(&ctor.name);
214                    let ctor_space = if self.options.ctor_style == CtorStyle::Module {
215                        space.clone()
216                    } else {
217                        format!("ctor:{}", data.full_name)
218                    };
219                    let name = self.claim(&ctor_space, &ctor_base);
220                    self.ctor_names
221                        .insert(format!("{}#{}", data.full_name, ctor.name), name);
222                }
223            }
224        }
225    }
226
227    fn claim(&mut self, space: &str, name: &str) -> String {
228        if !self.taken.contains_key(space) {
229            // Root declarations may not redeclare the target's prelude (`root_reserved`).
230            let mut used: HashSet<String> = self.reserved.iter().cloned().collect();
231            if space.ends_with(':') {
232                used.extend(
233                    self.options
234                        .root_reserved
235                        .iter()
236                        .map(|name| (*name).to_owned()),
237                );
238            }
239            self.taken.insert(space.to_owned(), used);
240        }
241        let generated = self.options.generated;
242        let used = self
243            .taken
244            .get_mut(space)
245            .expect("namespace was just created");
246        let is_generated = |candidate: &str, used: &HashSet<String>| {
247            generated.is_some_and(|generated| {
248                generated(candidate).iter().any(|name| used.contains(name))
249            })
250        };
251        let mut candidate = name.to_owned();
252        let mut index = 2;
253        while used.contains(&candidate) || is_generated(&candidate, used) {
254            candidate = format!("{name}_{index}");
255            index += 1;
256        }
257        let mut names = vec![candidate.clone()];
258        if let Some(generated) = generated {
259            names.extend(generated(&candidate));
260        }
261        for name in names {
262            used.insert(name.clone());
263            self.claimed.insert(name);
264        }
265        candidate
266    }
267
268    /// Names a local binder may not take: a local named like a module, a
269    /// top-level function or a constructor would shadow it in the target.
270    #[must_use]
271    pub fn local_reserved(&self) -> BTreeSet<String> {
272        self.reserved.union(&self.claimed).cloned().collect()
273    }
274
275    /// The target name of a declaration within its module.
276    ///
277    /// # Panics
278    /// When `full_name` is not a declaration of the program.
279    #[must_use]
280    pub fn local_name(&self, full_name: &str) -> &str {
281        &self.names[full_name].local
282    }
283
284    /// The target module path of a declaration.
285    ///
286    /// # Panics
287    /// When `full_name` is not a declaration of the program.
288    #[must_use]
289    pub fn module_path(&self, full_name: &str) -> &[String] {
290        &self.names[full_name].path
291    }
292
293    /// The target name of a source module.
294    #[must_use]
295    pub fn module_name(&self, source_path: &[String]) -> Option<&str> {
296        self.module_names
297            .get(&source_path.join("."))
298            .map(String::as_str)
299    }
300
301    /// Fully qualified reference from the top level.
302    #[must_use]
303    pub fn reference(&self, full_name: &str, separator: &str) -> String {
304        let target = &self.names[full_name];
305        let mut parts = target.path.clone();
306        parts.push(target.local.clone());
307        parts.join(separator)
308    }
309
310    /// The target name of a constructor within its namespace.
311    ///
312    /// # Panics
313    /// When the constructor is not declared.
314    #[must_use]
315    pub fn ctor_local(&self, data_name: &str, ctor: &str) -> &str {
316        &self.ctor_names[&format!("{data_name}#{ctor}")]
317    }
318
319    /// Fully qualified constructor reference from the top level.
320    #[must_use]
321    pub fn ctor_ref(&self, data_name: &str, ctor: &str, separator: &str) -> String {
322        let local = self.ctor_local(data_name, ctor);
323        if self.options.ctor_style == CtorStyle::Module {
324            let mut parts = self.module_path(data_name).to_vec();
325            parts.push(local.to_owned());
326            return parts.join(separator);
327        }
328        format!("{}{separator}{local}", self.reference(data_name, separator))
329    }
330
331    /// Records where a declaration (and a data type's constructors) went.
332    pub fn map(&mut self, entry: &Decl, target: &str) {
333        // A generated ml_io pair (output.rs) has no source declaration to map.
334        if matches!(entry, Decl::Data(data) if data.output) {
335            return;
336        }
337        let source_span = entry.span();
338        let mut path = self.module_path(entry.full_name()).to_vec();
339        path.push(target.to_owned());
340        self.mappings.push(Mapping {
341            kind: match entry {
342                Decl::Fn(_) => "function",
343                other => other.kind(),
344            }
345            .to_owned(),
346            source: entry.full_name().to_owned(),
347            target: path.join("."),
348            source_span,
349        });
350        if let Decl::Data(data) = entry {
351            for ctor in &data.ctors {
352                self.mappings.push(Mapping {
353                    kind: "constructor".to_owned(),
354                    source: format!("{}.{}", data.full_name, ctor.name),
355                    target: self.ctor_ref(&data.full_name, &ctor.name, "."),
356                    source_span,
357                });
358            }
359        }
360    }
361
362    pub fn assume(&mut self, assumption: AssumptionText, detail: Option<&str>) {
363        let index = if let Some(index) = self
364            .assumptions
365            .iter()
366            .position(|record| record.id == assumption.id)
367        {
368            index
369        } else {
370            self.assumptions.push(Assumption {
371                id: assumption.id.to_owned(),
372                statement: assumption.statement.to_owned(),
373                details: Vec::new(),
374            });
375            self.assumptions.len() - 1
376        };
377        let record = &mut self.assumptions[index];
378        if let Some(detail) = detail
379            && !record.details.iter().any(|known| known == detail)
380        {
381            record.details.push(detail.to_owned());
382        }
383    }
384
385    /// A machine integer of a pure target: its unbounded representation, with Rust's aborts threaded as values (`output`).
386    pub fn machine_integer(&mut self, ty: &Type, representation: &str) {
387        let key = ty.key();
388        self.encode(
389            &format!("machine-integer:{key}"),
390            &format!("{key} values are {representation} values; every {key} operation tests where Rust panics, overflow or a zero divisor, and aborts there with Rust's panic message, and otherwise computes the in-range result exactly"),
391        );
392    }
393
394    /// An array read: in bounds it is the element, outside it JavaScript's undefined, which the targets do not model.
395    pub fn array_read(&mut self) {
396        self.assume(IN_BOUNDS_READS, None);
397    }
398
399    pub fn encode(&mut self, id: &str, statement: &str) {
400        if !self.encodings.iter().any(|encoding| encoding.id == id) {
401            self.encodings.push(Encoding {
402                id: id.to_owned(),
403                statement: statement.to_owned(),
404            });
405        }
406    }
407
408    /// Records a theorem; `bounded` theorems are checked by the source
409    /// kernel and tested on bounded inputs in the target.
410    pub fn theorem(&mut self, full_name: &str, name: &str, closed_goal: bool, bounded: bool) {
411        let mut path = self.module_path(full_name).to_vec();
412        path.push(name.to_owned());
413        self.theorems.push(TheoremRecord {
414            source: full_name.to_owned(),
415            target: path.join("."),
416            kind: "theorem".to_owned(),
417            closed_goal,
418            discharge: bounded.then(|| "source-kernel".to_owned()),
419            check: bounded.then(|| "bounded".to_owned()),
420        });
421    }
422
423    pub fn assertion_theorem(&mut self, name: &str, effect: &Effect) {
424        self.assertion_theorem_with(name, effect, None);
425    }
426
427    /// An assertion with how it is discharged, such as `runtime-assertion`.
428    pub fn assertion_theorem_with(&mut self, name: &str, effect: &Effect, discharge: Option<&str>) {
429        let span = match effect {
430            Effect::Print { span, .. }
431            | Effect::Let { span, .. }
432            | Effect::Assert { span, .. }
433            | Effect::Output { span, .. }
434            | Effect::Unwrap { span, .. } => *span,
435        };
436        self.theorems.push(TheoremRecord {
437            source: format!(
438                "main:assert@{}",
439                span.map_or_else(|| "?".to_owned(), |span| span.start.to_string())
440            ),
441            target: name.to_owned(),
442            kind: "assertion".to_owned(),
443            closed_goal: true,
444            discharge: discharge.map(str::to_owned),
445            check: None,
446        });
447    }
448
449    #[must_use]
450    pub fn assumption_list(&self) -> Vec<Assumption> {
451        self.assumptions.clone()
452    }
453
454    #[must_use]
455    pub fn encoding_list(&self) -> Vec<Encoding> {
456        self.encodings.clone()
457    }
458
459    /// The emitted result with this state's contract.
460    #[must_use]
461    pub fn finish(&self, text: String, entry: Option<String>) -> Emitted {
462        Emitted {
463            language: self.language,
464            text,
465            preludes: Vec::new(),
466            definitions: Vec::new(),
467            mappings: self.mappings.clone(),
468            assumptions: self.assumption_list(),
469            encodings: self.encoding_list(),
470            theorems: self.theorems.clone(),
471            entry,
472        }
473    }
474}
475
476fn type_dependencies(ty: &Type, found: &mut HashSet<String>) {
477    match ty {
478        Type::Data { name } => {
479            found.insert(name.clone());
480        }
481        Type::Array { element } => type_dependencies(element, found),
482        _ => {}
483    }
484}
485
486fn expr_dependencies(expr: &Expr, found: &mut HashSet<String>) {
487    type_dependencies(&expr.ty, found);
488    match &expr.node {
489        Node::Call { func, .. } => {
490            found.insert(func.clone());
491        }
492        Node::Ctor { data, .. } => {
493            found.insert(data.clone());
494        }
495        Node::Binary {
496            domain: Some(domain),
497            ..
498        } => type_dependencies(domain, found),
499        Node::Cast { from, to, .. } => {
500            type_dependencies(from, found);
501            type_dependencies(to, found);
502        }
503        Node::Match { cases, .. } => {
504            for kase in cases {
505                if let Pattern::Ctor { data, .. } = &kase.pattern {
506                    found.insert(data.clone());
507                }
508            }
509        }
510        _ => {}
511    }
512    for child in expr.children() {
513        expr_dependencies(child, found);
514    }
515}
516
517fn prop_dependencies(prop: &Prop, found: &mut HashSet<String>) {
518    match prop {
519        Prop::Forall { binders, body } => {
520            for binder in binders {
521                type_dependencies(&binder.ty, found);
522            }
523            prop_dependencies(body, found);
524        }
525        Prop::And { left, right } | Prop::Or { left, right } | Prop::Implies { left, right } => {
526            prop_dependencies(left, found);
527            prop_dependencies(right, found);
528        }
529        Prop::Not { arg } => prop_dependencies(arg, found),
530        Prop::Bool { expr } => expr_dependencies(expr, found),
531        other => {
532            if let Some((_, comparison)) = other.comparison() {
533                expr_dependencies(&comparison.left, found);
534                expr_dependencies(&comparison.right, found);
535                type_dependencies(&comparison.domain, found);
536            }
537        }
538    }
539}
540
541/// An operation that may abort, which `output` threads as a value before a pure target sees it.
542///
543/// # Panics
544/// Always: the emitter met a node the threading should have rewritten.
545pub fn unthreaded(what: &str) -> ! {
546    panic!("{what} reaches a pure target's emitter without its abort threaded")
547}
548
549/// Declarations every declaration refers to (types, functions, constructors, lemmas).
550#[must_use]
551pub fn dependencies(entry: &Decl) -> HashSet<String> {
552    fn lemmas(plan: &Plan, found: &mut HashSet<String>) {
553        match plan {
554            Plan::Close { hints } => {
555                found.extend(hints.lemmas.iter().cloned());
556                found.extend(hints.unfold.iter().cloned());
557            }
558            Plan::Induction(split) | Plan::Cases(split) => {
559                for kase in &split.cases {
560                    lemmas(&kase.plan, found);
561                }
562            }
563        }
564    }
565    let mut found = HashSet::new();
566    match entry {
567        Decl::Data(data) => {
568            for ctor in &data.ctors {
569                for field in &ctor.fields {
570                    type_dependencies(&field.ty, &mut found);
571                }
572            }
573        }
574        Decl::Fn(function) => {
575            for param in &function.params {
576                type_dependencies(&param.ty, &mut found);
577            }
578            type_dependencies(&function.ret, &mut found);
579            expr_dependencies(&function.body, &mut found);
580        }
581        Decl::Theorem(theorem) => {
582            for binder in &theorem.binders {
583                type_dependencies(&binder.ty, &mut found);
584            }
585            prop_dependencies(&theorem.prop, &mut found);
586            lemmas(&theorem.proof.plan, &mut found);
587        }
588    }
589    found.remove(entry.full_name());
590    found
591}
592
593/// Whether a node depends on declarations of a kind, directly or not.
594pub struct Dependence {
595    marked: HashSet<String>,
596    /// Whether a node with a Number-typed part depends by itself.
597    floats: bool,
598}
599
600impl Dependence {
601    /// Whether a node computes with JavaScript Numbers: it has a
602    /// Number-typed part, or uses a declaration that does.
603    #[must_use]
604    pub fn numbers(program: &Program) -> Self {
605        let marked = program
606            .declarations
607            .iter()
608            .filter(|entry| !matches!(entry, Decl::Theorem(_)) && mentions_float(entry))
609            .map(|entry| entry.full_name().to_owned())
610            .collect();
611        Self::closed(program, marked, true)
612    }
613
614    /// Whether a node calls a recursive function with no decreasing
615    /// argument: Lean defines those as partial defs, whose equations the
616    /// kernel cannot unfold.
617    #[must_use]
618    pub fn partial(program: &Program) -> Self {
619        let marked = program
620            .declarations
621            .iter()
622            .filter(|entry| {
623                matches!(entry, Decl::Fn(function)
624                    if function.mutual || (function.recursive && function.decreasing.is_none()))
625            })
626            .map(|entry| entry.full_name().to_owned())
627            .collect();
628        Self::closed(program, marked, false)
629    }
630
631    fn closed(program: &Program, mut numeric: HashSet<String>, floats: bool) -> Self {
632        let uses: Vec<(String, HashSet<String>)> = program
633            .declarations
634            .iter()
635            .map(|entry| (entry.full_name().to_owned(), dependencies(entry)))
636            .collect();
637        let mut grew = true;
638        while grew {
639            grew = false;
640            for (name, used) in &uses {
641                if !numeric.contains(name) && used.iter().any(|name| numeric.contains(name)) {
642                    numeric.insert(name.clone());
643                    grew = true;
644                }
645            }
646        }
647        Self {
648            marked: numeric,
649            floats,
650        }
651    }
652
653    #[must_use]
654    pub fn prop(&self, prop: &Prop) -> bool {
655        let mut found = HashSet::new();
656        prop_dependencies(prop, &mut found);
657        (self.floats && mentions_float(prop)) || found.iter().any(|name| self.marked.contains(name))
658    }
659
660    #[must_use]
661    pub fn expr(&self, expr: &Expr) -> bool {
662        let mut found = HashSet::new();
663        expr_dependencies(expr, &mut found);
664        (self.floats && mentions_float(expr)) || found.iter().any(|name| self.marked.contains(name))
665    }
666}
667
668/// True when a node has a part of type `float`.
669fn mentions_float(node: &impl Serialize) -> bool {
670    fn visit(value: &serde_json::Value) -> bool {
671        match value {
672            serde_json::Value::Array(items) => items.iter().any(visit),
673            serde_json::Value::Object(fields) => {
674                fields.get("kind").and_then(serde_json::Value::as_str) == Some("float")
675                    || fields.values().any(visit)
676            }
677            _ => false,
678        }
679    }
680    serde_json::to_value(node).is_ok_and(|value| visit(&value))
681}
682
683/// Each function the checker marked mutual, mapped to its group.
684///
685/// A group is the functions it calls that call it back, directly or not,
686/// itself included, in source order. A function on a cycle of calls is itself
687/// mutual, so the cycles run through mutual functions only.
688#[must_use]
689pub fn mutual_groups(program: &Program) -> HashMap<String, Vec<&Decl>> {
690    let members: Vec<&Decl> = program
691        .declarations
692        .iter()
693        .filter(|entry| matches!(entry, Decl::Fn(function) if function.mutual))
694        .collect();
695    let calls: HashMap<&str, HashSet<String>> = members
696        .iter()
697        .map(|entry| (entry.full_name(), dependencies(entry)))
698        .collect();
699    let reached = |from: &str| {
700        let mut seen: HashSet<String> = HashSet::from([from.to_owned()]);
701        let mut stack = vec![from.to_owned()];
702        while let Some(name) = stack.pop() {
703            for next in calls.get(name.as_str()).into_iter().flatten() {
704                if calls.contains_key(next.as_str()) && seen.insert(next.clone()) {
705                    stack.push(next.clone());
706                }
707            }
708        }
709        seen
710    };
711    let reach: HashMap<&str, HashSet<String>> = members
712        .iter()
713        .map(|entry| (entry.full_name(), reached(entry.full_name())))
714        .collect();
715    members
716        .iter()
717        .map(|entry| {
718            let group = members
719                .iter()
720                .copied()
721                .filter(|other| {
722                    reach[entry.full_name()].contains(other.full_name())
723                        && reach[other.full_name()].contains(entry.full_name())
724                })
725                .collect();
726            (entry.full_name().to_owned(), group)
727        })
728        .collect()
729}
730
731/// Declarations in an order where each follows everything it uses.
732///
733/// Source order is kept where possible and, among ready declarations, the
734/// ones in the module being emitted come first so modules stay contiguous.
735///
736/// # Errors
737/// On cyclic declarations, and on modules that would have to be reopened
738/// when `require_contiguous_modules` is set.
739pub fn order_declarations(
740    program: &Program,
741    require_contiguous_modules: bool,
742) -> Result<Vec<&Decl>> {
743    let entries = &program.declarations;
744    let position: HashMap<&str, usize> = entries
745        .iter()
746        .enumerate()
747        .map(|(index, entry)| (entry.full_name(), index))
748        .collect();
749    let pending: Vec<HashSet<String>> = entries.iter().map(dependencies).collect();
750    // A group of mutually recursive functions is ready, and placed, as one.
751    let groups = mutual_groups(program);
752    let unit = |index: usize| -> Vec<&Decl> {
753        groups
754            .get(entries[index].full_name())
755            .cloned()
756            .unwrap_or_else(|| vec![&entries[index]])
757    };
758    let mut done: HashSet<&str> = HashSet::new();
759    let mut order: Vec<&Decl> = Vec::new();
760    let mut current: &[String] = &[];
761    while order.len() < entries.len() {
762        let mut ready: Vec<usize> = (0..entries.len())
763            .filter(|&index| {
764                let members = unit(index);
765                !done.contains(entries[index].full_name())
766                    && members.iter().all(|member| {
767                        pending[position[member.full_name()]].iter().all(|name| {
768                            done.contains(name.as_str())
769                                || !position.contains_key(name.as_str())
770                                || members.iter().any(|other| other.full_name() == name)
771                        })
772                    })
773            })
774            .collect();
775        if ready.is_empty() {
776            let stuck = entries
777                .iter()
778                .find(|entry| !done.contains(entry.full_name()))
779                .expect("some declaration is pending");
780            return Err(unsupported(
781                "cyclic declarations",
782                &format!(
783                    "{} depends on declarations that depend on it, which needs mutual definitions",
784                    stuck.full_name()
785                ),
786                stuck.span(),
787            ));
788        }
789        let shared = |index: usize| {
790            let path = entries[index].module_path();
791            current
792                .iter()
793                .zip(path)
794                .take_while(|(left, right)| left == right)
795                .count()
796        };
797        ready.sort_by(|&left, &right| shared(right).cmp(&shared(left)).then(left.cmp(&right)));
798        let next = &entries[ready[0]];
799        for member in unit(ready[0]) {
800            if member.module_path() != next.module_path() {
801                return Err(unsupported(
802                    "mutual recursion across modules",
803                    &format!(
804                        "{} and {} are mutually recursive in different modules; the target defines them together in one module",
805                        next.full_name(),
806                        member.full_name()
807                    ),
808                    member.span(),
809                ));
810            }
811            order.push(member);
812            done.insert(member.full_name());
813        }
814        current = next.module_path();
815    }
816    if require_contiguous_modules {
817        let mut closed: HashSet<String> = HashSet::new();
818        let mut open: &[String] = &[];
819        for entry in &order {
820            let path = entry.module_path();
821            for depth in 0..open.len() {
822                if path.get(depth) != Some(&open[depth]) {
823                    for index in depth..open.len() {
824                        closed.insert(open[..=index].join("."));
825                    }
826                    break;
827                }
828            }
829            for depth in 1..=path.len() {
830                let key = path[..depth].join(".");
831                if closed.contains(&key) {
832                    return Err(unsupported(
833                        "interleaved modules",
834                        &format!(
835                            "module {key} would have to be reopened after its declarations depend on later ones; the target cannot reopen a module"
836                        ),
837                        entry.span(),
838                    ));
839                }
840            }
841            open = path;
842        }
843    }
844    Ok(order)
845}