1pub(crate) mod builtins;
6pub(crate) mod common;
7pub mod dafny;
8pub mod lean;
9pub mod rust;
10
11use std::collections::{HashMap, HashSet};
12
13use crate::ast::{FnDef, TopLevel, TypeDef};
14use crate::types::checker::TypeCheckResult;
15
16pub struct ModuleInfo {
18 pub prefix: String,
20 pub depends: Vec<String>,
22 pub type_defs: Vec<TypeDef>,
24 pub fn_defs: Vec<FnDef>,
26}
27
28pub struct CodegenContext {
30 pub items: Vec<TopLevel>,
32 pub fn_sigs: HashMap<String, (Vec<crate::types::Type>, crate::types::Type, Vec<String>)>,
34 pub memo_fns: HashSet<String>,
36 pub memo_safe_types: HashSet<String>,
38 pub type_defs: Vec<TypeDef>,
40 pub fn_defs: Vec<FnDef>,
42 pub project_name: String,
44 pub modules: Vec<ModuleInfo>,
46 pub module_prefixes: HashSet<String>,
48 pub policy: Option<crate::config::ProjectConfig>,
50 pub emit_replay_runtime: bool,
52 pub guest_entry: Option<String>,
54 pub emit_self_host_runtime: bool,
56}
57
58pub struct ProjectOutput {
60 pub files: Vec<(String, String)>,
62}
63
64pub fn build_context(
66 items: Vec<TopLevel>,
67 tc_result: &TypeCheckResult,
68 memo_fns: HashSet<String>,
69 project_name: String,
70 modules: Vec<ModuleInfo>,
71) -> CodegenContext {
72 let type_defs: Vec<TypeDef> = items
73 .iter()
74 .filter_map(|item| {
75 if let TopLevel::TypeDef(td) = item {
76 Some(td.clone())
77 } else {
78 None
79 }
80 })
81 .collect();
82
83 let fn_defs: Vec<FnDef> = items
84 .iter()
85 .filter_map(|item| {
86 if let TopLevel::FnDef(fd) = item {
87 Some(fd.clone())
88 } else {
89 None
90 }
91 })
92 .collect();
93
94 let module_prefixes: HashSet<String> = modules.iter().map(|m| m.prefix.clone()).collect();
95
96 CodegenContext {
97 items,
98 fn_sigs: tc_result.fn_sigs.clone(),
99 memo_fns,
100 memo_safe_types: tc_result.memo_safe_types.clone(),
101 type_defs,
102 fn_defs,
103 project_name,
104 modules,
105 module_prefixes,
106 policy: None,
107 emit_replay_runtime: false,
108 guest_entry: None,
109 emit_self_host_runtime: false,
110 }
111}