logicaffeine-compile 0.9.0

LOGOS compilation pipeline - codegen and interpreter
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87

//! Dependency collection for program extraction.
//!
//! Collects all transitive dependencies needed to extract a definition.

use crate::kernel::{Context, Term};
use std::collections::HashSet;

/// Collect all dependencies of a definition.
///
/// Starting from an entry point, recursively collects all global names
/// that are referenced, including inductives, constructors, and definitions.
pub fn collect_dependencies(ctx: &Context, entry: &str) -> HashSet<String> {
    let mut visited = HashSet::new();
    let mut to_visit = vec![entry.to_string()];

    while let Some(name) = to_visit.pop() {
        if visited.contains(&name) {
            continue;
        }
        visited.insert(name.clone());

        // Get the term to analyze based on what kind of global it is
        if let Some(body) = ctx.get_definition_body(&name) {
            collect_globals(body, &mut to_visit);
            // Also collect from the type
            if let Some(ty) = ctx.get_definition_type(&name) {
                collect_globals(ty, &mut to_visit);
            }
        }

        if ctx.is_inductive(&name) {
            // Add constructors and their types
            for (ctor_name, ctor_ty) in ctx.get_constructors(&name) {
                collect_globals(ctor_ty, &mut to_visit);
                to_visit.push(ctor_name.to_string());
            }
        }

        if ctx.is_constructor(&name) {
            // Add the inductive type
            if let Some(ind) = ctx.constructor_inductive(&name) {
                to_visit.push(ind.to_string());
            }
        }
    }

    visited
}

/// Recursively collect all Global references from a term.
fn collect_globals(term: &Term, deps: &mut Vec<String>) {
    match term {
        Term::Global(name) => deps.push(name.clone()),
        Term::App(f, a) => {
            collect_globals(f, deps);
            collect_globals(a, deps);
        }
        Term::Lambda {
            param_type, body, ..
        } => {
            collect_globals(param_type, deps);
            collect_globals(body, deps);
        }
        Term::Pi {
            param_type,
            body_type,
            ..
        } => {
            collect_globals(param_type, deps);
            collect_globals(body_type, deps);
        }
        Term::Fix { body, .. } => collect_globals(body, deps),
        Term::Match {
            discriminant,
            motive,
            cases,
        } => {
            collect_globals(discriminant, deps);
            collect_globals(motive, deps);
            for case in cases {
                collect_globals(case, deps);
            }
        }
        // Base cases: no dependencies
        Term::Sort(_) | Term::Var(_) | Term::Lit(_) | Term::Hole => {}
    }
}