meta_language/program_representation/
project.rs

1//! Project-aware semantics: resolves an entry program's module requests to the
2//! project's source files, reads the project manifests, and links the entry's
3//! imports, references, attributes, macros, notations and tactics to the
4//! declarations they name in other files. Every symbol is identified as
5//! `<file>#<qualified name>`. The JavaScript runtime implements the same
6//! analysis in js/src/program-project.js.
7
8mod javascript;
9mod lean;
10mod rocq;
11mod rust_lang;
12mod tree;
13
14use std::collections::BTreeMap;
15use std::rc::Rc;
16
17use super::analysis::syntax_facts;
18use super::{ProgramBinding, ProgramDiagnostic, ProgramFact, ProgramRange};
19use crate::{LinkNetwork, ParseConfiguration};
20use tree::{SyntaxTree, Target};
21
22const TYPE_KINDS: [&str; 9] = [
23    "class",
24    "struct",
25    "enum",
26    "trait",
27    "type",
28    "structure",
29    "inductive",
30    "constructor",
31    "universe",
32];
33const EFFECT_TRAITS: [&str; 4] = ["async", "generator", "io", "proof-state"];
34const PROOF_KINDS: [&str; 3] = ["theorem", "lemma", "tactic"];
35// Tactic steps, and the checked assertions of languages without proof terms.
36const PROOF_ROLES: [&str; 3] = ["tactic", "assertion", "const-assertion"];
37
38/// One project file by project-relative path.
39#[derive(Clone, Debug, PartialEq, Eq)]
40pub struct ProgramProjectSource {
41    path: String,
42    source: String,
43}
44
45impl ProgramProjectSource {
46    /// Creates a project file.
47    #[must_use]
48    pub fn new(path: impl Into<String>, source: impl Into<String>) -> Self {
49        Self {
50            path: path.into(),
51            source: source.into(),
52        }
53    }
54
55    /// Project-relative path.
56    #[must_use]
57    pub fn path(&self) -> &str {
58        &self.path
59    }
60
61    /// File contents.
62    #[must_use]
63    pub fn source(&self) -> &str {
64        &self.source
65    }
66}
67
68/// Project files and dependency names available during analysis.
69#[derive(Clone, Debug, Default, PartialEq, Eq)]
70pub struct ProgramProjectContext {
71    root: String,
72    files: Vec<String>,
73    dependencies: Vec<String>,
74    extensions: Vec<String>,
75    entry: Option<String>,
76    sources: Vec<ProgramProjectSource>,
77}
78
79impl ProgramProjectContext {
80    /// Creates a project context.
81    #[must_use]
82    pub fn new(root: impl Into<String>, files: Vec<String>, dependencies: Vec<String>) -> Self {
83        Self {
84            root: root.into(),
85            files,
86            dependencies,
87            extensions: Vec::new(),
88            entry: None,
89            sources: Vec::new(),
90        }
91    }
92
93    /// Adds project-defined syntax extensions.
94    #[must_use]
95    pub fn with_extensions(mut self, extensions: Vec<String>) -> Self {
96        self.extensions = extensions;
97        self
98    }
99
100    /// Names the analyzed program's path within the project and the project's
101    /// files (manifests and modules), enabling project-aware semantics.
102    #[must_use]
103    pub fn with_entry(
104        mut self,
105        entry: impl Into<String>,
106        sources: Vec<ProgramProjectSource>,
107    ) -> Self {
108        self.entry = Some(entry.into());
109        self.sources = sources;
110        self
111    }
112
113    /// Project root.
114    #[must_use]
115    pub fn root(&self) -> &str {
116        &self.root
117    }
118
119    /// Project files.
120    #[must_use]
121    pub fn files(&self) -> &[String] {
122        &self.files
123    }
124
125    /// Declared dependencies.
126    #[must_use]
127    pub fn dependencies(&self) -> &[String] {
128        &self.dependencies
129    }
130
131    /// Project-defined syntax extensions.
132    #[must_use]
133    pub fn extensions(&self) -> &[String] {
134        &self.extensions
135    }
136
137    /// The analyzed program's path within the project.
138    #[must_use]
139    pub fn entry(&self) -> Option<&str> {
140        self.entry.as_deref()
141    }
142
143    /// The project's files by project-relative path.
144    #[must_use]
145    pub fn sources(&self) -> &[ProgramProjectSource] {
146        &self.sources
147    }
148}
149
150/// An entry module request resolved to a project file.
151#[derive(Clone, Debug, PartialEq, Eq)]
152pub struct ProgramProjectModule {
153    request: String,
154    module: String,
155    file: String,
156    range: ProgramRange,
157}
158
159impl ProgramProjectModule {
160    /// The request as written.
161    #[must_use]
162    pub fn request(&self) -> &str {
163        &self.request
164    }
165
166    /// The resolved module.
167    #[must_use]
168    pub fn module(&self) -> &str {
169        &self.module
170    }
171
172    /// The project file defining the module.
173    #[must_use]
174    pub fn file(&self) -> &str {
175        &self.file
176    }
177
178    /// Entry range of the request.
179    #[must_use]
180    pub const fn range(&self) -> ProgramRange {
181        self.range
182    }
183}
184
185/// An entry range linked to the declaration it names, identified as
186/// `<file>#<qualified name>`.
187#[derive(Clone, Debug, PartialEq, Eq)]
188pub struct ProgramProjectReference {
189    role: &'static str,
190    name: String,
191    range: ProgramRange,
192    symbol: String,
193    target_kind: String,
194    traits: Vec<String>,
195    file: String,
196    declaration: ProgramRange,
197}
198
199impl ProgramProjectReference {
200    /// How the entry uses the declaration: `import`, `reference`, `attribute`,
201    /// `macro`, `notation`, `template-tag`, `tactic`, `assertion` or
202    /// `const-assertion`.
203    #[must_use]
204    pub const fn role(&self) -> &'static str {
205        self.role
206    }
207
208    /// The name as written.
209    #[must_use]
210    pub fn name(&self) -> &str {
211        &self.name
212    }
213
214    /// Entry range of the use.
215    #[must_use]
216    pub const fn range(&self) -> ProgramRange {
217        self.range
218    }
219
220    /// Declaration identity.
221    #[must_use]
222    pub fn symbol(&self) -> &str {
223        &self.symbol
224    }
225
226    /// Declaration kind.
227    #[must_use]
228    pub fn target_kind(&self) -> &str {
229        &self.target_kind
230    }
231
232    /// Declaration traits (`recursive`, `async`, `const`, `io`, ...).
233    #[must_use]
234    pub fn traits(&self) -> &[String] {
235        &self.traits
236    }
237
238    /// The project file declaring the target.
239    #[must_use]
240    pub fn file(&self) -> &str {
241        &self.file
242    }
243
244    /// Declaration range within its file.
245    #[must_use]
246    pub const fn declaration(&self) -> ProgramRange {
247        self.declaration
248    }
249}
250
251/// A macro, notation or tagged template use with the source it expands to.
252#[derive(Clone, Debug, PartialEq, Eq)]
253pub struct ProgramExpansion {
254    name: String,
255    kind: &'static str,
256    range: ProgramRange,
257    expansion: String,
258    target: String,
259}
260
261impl ProgramExpansion {
262    /// The macro, notation or tag name.
263    #[must_use]
264    pub fn name(&self) -> &str {
265        &self.name
266    }
267
268    /// `macro-rules`, `notation` or `tagged-template`.
269    #[must_use]
270    pub const fn kind(&self) -> &'static str {
271        self.kind
272    }
273
274    /// Entry range of the use.
275    #[must_use]
276    pub const fn range(&self) -> ProgramRange {
277        self.range
278    }
279
280    /// Expanded source.
281    #[must_use]
282    pub fn expansion(&self) -> &str {
283        &self.expansion
284    }
285
286    /// Symbol of the expanded definition.
287    #[must_use]
288    pub fn target(&self) -> &str {
289        &self.target
290    }
291}
292
293/// Results of the project-aware analysis.
294#[derive(Clone, Debug, Default)]
295pub(super) struct ProjectResult {
296    pub(super) modules: Vec<ProgramProjectModule>,
297    pub(super) facts: Vec<ProgramFact>,
298    pub(super) references: Vec<ProgramProjectReference>,
299    pub(super) expansions: Vec<ProgramExpansion>,
300    pub(super) diagnostics: Vec<ProgramDiagnostic>,
301    /// Module requests the language-neutral request scan does not see.
302    pub(super) requests: Vec<ProgramFact>,
303    /// Requests resolved to project files, as (name, start).
304    pub(super) resolved_requests: Vec<(String, usize)>,
305}
306
307/// Analyzes an entry program within its project. Returns empty results
308/// unless the project names an entry file.
309pub(super) fn project_semantics(
310    language: &'static str,
311    source: &str,
312    mappings: &[super::ProgramSourceMapping],
313    bindings: &[ProgramBinding],
314    unresolved: &[ProgramFact],
315    project: &ProgramProjectContext,
316) -> ProjectResult {
317    let Some(entry) = project.entry().filter(|entry| !entry.is_empty()) else {
318        return ProjectResult::default();
319    };
320    let mut context = ProjectContext::new(language, entry, source, mappings, project);
321    context.bindings = bindings;
322    context.unresolved = unresolved;
323    match language {
324        "JavaScript" => javascript::analyze(&mut context),
325        "Rust" => rust_lang::analyze(&mut context),
326        "Lean" => lean::analyze(&mut context),
327        "Rocq" => rocq::analyze(&mut context),
328        _ => {}
329    }
330    for file in &project.sources {
331        if context
332            .parsed
333            .get(&file.path)
334            .is_some_and(|parsed| !parsed.clean)
335        {
336            context.result.diagnostics.push(ProgramDiagnostic {
337                kind: "project-parse-error",
338                term: file.path.clone(),
339                range: ProgramRange::default(),
340            });
341        }
342    }
343    context.result
344}
345
346/// A parsed project file.
347#[derive(Debug)]
348struct ParsedFile {
349    path: String,
350    source: String,
351    tree: SyntaxTree,
352    clean: bool,
353}
354
355struct ProjectContext<'a> {
356    language: &'static str,
357    bindings: &'a [ProgramBinding],
358    unresolved: &'a [ProgramFact],
359    entry: Rc<ParsedFile>,
360    sources: BTreeMap<&'a str, &'a str>,
361    parsed: BTreeMap<String, Rc<ParsedFile>>,
362    result: ProjectResult,
363}
364
365impl<'a> ProjectContext<'a> {
366    fn new(
367        language: &'static str,
368        entry: &str,
369        source: &str,
370        mappings: &[super::ProgramSourceMapping],
371        project: &'a ProgramProjectContext,
372    ) -> Self {
373        let mut context = Self {
374            language,
375            bindings: &[],
376            unresolved: &[],
377            entry: Rc::new(ParsedFile {
378                path: entry.to_string(),
379                source: source.to_string(),
380                tree: SyntaxTree::build(mappings, source),
381                clean: true,
382            }),
383            sources: project
384                .sources
385                .iter()
386                .map(|file| (file.path.as_str(), file.source.as_str()))
387                .collect(),
388            parsed: BTreeMap::new(),
389            result: ProjectResult::default(),
390        };
391        for file in &project.sources {
392            context.fact(
393                "project-file",
394                &file.path,
395                &file.path,
396                (0, file.source.len()),
397            );
398        }
399        context
400    }
401
402    fn has(&self, path: &str) -> bool {
403        path == self.entry.path || self.sources.contains_key(path)
404    }
405
406    fn text(&self, path: &str) -> Option<&str> {
407        if path == self.entry.path {
408            return Some(&self.entry.source);
409        }
410        self.sources.get(path).copied()
411    }
412
413    /// Parses a project file once; `None` when the project has no such file.
414    fn load(&mut self, path: &str) -> Option<Rc<ParsedFile>> {
415        self.load_as(path, self.language)
416    }
417
418    fn load_as(&mut self, path: &str, language: &str) -> Option<Rc<ParsedFile>> {
419        if path == self.entry.path {
420            return Some(Rc::clone(&self.entry));
421        }
422        let source = *self.sources.get(path)?;
423        let parsed = self.parsed.entry(path.to_string()).or_insert_with(|| {
424            let network = LinkNetwork::parse(source, language, ParseConfiguration::default());
425            Rc::new(ParsedFile {
426                path: path.to_string(),
427                source: source.to_string(),
428                tree: SyntaxTree::build(&syntax_facts(&network), source),
429                clean: network.verify_full_match(None).is_clean(),
430            })
431        });
432        Some(Rc::clone(parsed))
433    }
434
435    fn fact(&mut self, kind: &str, name: &str, file: &str, range: (usize, usize)) {
436        let mut fact = ProgramFact::new(kind, name, ProgramRange::new(range.0, range.1));
437        fact.file = Some(file.to_string());
438        self.result.facts.push(fact);
439    }
440
441    fn module(&mut self, request: &str, module: &str, file: &str, range: (usize, usize)) {
442        self.result.modules.push(ProgramProjectModule {
443            request: request.to_string(),
444            module: module.to_string(),
445            file: file.to_string(),
446            range: ProgramRange::new(range.0, range.1),
447        });
448        self.result
449            .resolved_requests
450            .push((request.to_string(), range.0));
451    }
452
453    /// A module request the language-neutral request scan does not see.
454    fn request(&mut self, name: &str, range: (usize, usize)) {
455        self.result.requests.push(ProgramFact::new(
456            "module-import",
457            name,
458            ProgramRange::new(range.0, range.1),
459        ));
460    }
461
462    /// Links an entry range to a declaration.
463    fn reference(
464        &mut self,
465        role: &'static str,
466        name: &str,
467        range: (usize, usize),
468        target: &Target,
469    ) {
470        self.result.references.push(ProgramProjectReference {
471            role,
472            name: name.to_string(),
473            range: ProgramRange::new(range.0, range.1),
474            symbol: target.symbol.clone(),
475            target_kind: target.kind.clone(),
476            traits: target.traits.clone(),
477            file: target.file.clone(),
478            declaration: ProgramRange::new(target.start, target.end),
479        });
480    }
481
482    fn expansion(
483        &mut self,
484        name: &str,
485        kind: &'static str,
486        range: (usize, usize),
487        expansion: String,
488        target: &str,
489    ) {
490        self.result.expansions.push(ProgramExpansion {
491            name: name.to_string(),
492            kind,
493            range: ProgramRange::new(range.0, range.1),
494            expansion,
495            target: target.to_string(),
496        });
497    }
498
499    fn diagnose(&mut self, kind: &'static str, term: String, range: (usize, usize)) {
500        self.result.diagnostics.push(ProgramDiagnostic {
501            kind,
502            term,
503            range: ProgramRange::new(range.0, range.1),
504        });
505    }
506}
507
508/// Construct evidence contributed by the project analysis.
509pub(super) fn project_evidence(
510    project: &ProgramProjectContext,
511    result: &ProjectResult,
512    construct: &str,
513) -> Vec<ProgramFact> {
514    let entry = project.entry().unwrap_or_default();
515    let located = |kind: String, name: &str, range: ProgramRange, file: &str| {
516        let mut fact = ProgramFact::new(kind, name, range);
517        fact.file = Some(file.to_string());
518        fact
519    };
520    let references = |predicate: &dyn Fn(&ProgramProjectReference) -> bool| {
521        result
522            .references
523            .iter()
524            .filter(|reference| predicate(reference))
525            .map(|reference| {
526                located(
527                    format!(
528                        "project-reference:{}:{}",
529                        reference.role, reference.target_kind
530                    ),
531                    &reference.symbol,
532                    reference.range,
533                    entry,
534                )
535            })
536            .collect::<Vec<_>>()
537    };
538    let has_trait = |reference: &ProgramProjectReference, traits: &[&str]| {
539        reference
540            .traits
541            .iter()
542            .any(|value| traits.contains(&value.as_str()))
543    };
544    match construct {
545        "modules-and-imports" => result
546            .modules
547            .iter()
548            .map(|module| {
549                located(
550                    "project-module".to_string(),
551                    &module.module,
552                    module.range,
553                    entry,
554                )
555            })
556            .chain(references(&|reference| reference.role == "import"))
557            .collect(),
558        "scopes-and-bindings" => references(&|reference| reference.role == "reference"),
559        "recursive-definitions" => references(&|reference| has_trait(reference, &["recursive"])),
560        "types-and-universes" => references(&|reference| {
561            TYPE_KINDS.contains(&reference.target_kind.as_str())
562                || has_trait(reference, &["universe-polymorphic"])
563        }),
564        "effects" => references(&|reference| has_trait(reference, &EFFECT_TRAITS)),
565        "attributes" => references(&|reference| reference.role == "attribute"),
566        "macros-and-notation" => {
567            references(&|reference| matches!(reference.role, "macro" | "notation" | "template-tag"))
568        }
569        "proof-terms-and-tactics" => references(&|reference| {
570            PROOF_ROLES.contains(&reference.role)
571                || PROOF_KINDS.contains(&reference.target_kind.as_str())
572        }),
573        "surface-expansion-elaboration-traces" => result
574            .expansions
575            .iter()
576            .map(|expansion| {
577                located(
578                    format!("expansion:{}", expansion.kind),
579                    &expansion.target,
580                    expansion.range,
581                    entry,
582                )
583            })
584            .collect(),
585        "project-context-and-dependencies" => result.facts.clone(),
586        _ => Vec::new(),
587    }
588}
meta_language/program_representation/project.rs

meta_language/program_representation/
project.rs
