1use std::collections::{HashMap, HashSet};
12
13use super::{Type, parse_type_str_strict};
14use crate::ast::{
15 BinOp, Expr, FnDef, Literal, Module, Pattern, Spanned, Stmt, TailCallData, TopLevel, TypeDef,
16};
17
18mod builtins;
19pub mod effect_classification;
20pub mod effect_lifting;
21mod exhaustiveness;
22mod flow;
23pub mod hostile_effects;
24pub mod hostile_values;
25mod infer;
26mod memo;
27mod modules;
28pub mod oracle_subtypes;
29pub mod proof_trust_header;
30
31#[cfg(test)]
32mod tests;
33
34#[derive(Debug, Clone)]
39pub struct TypeError {
40 pub message: String,
41 pub line: usize,
42 pub col: usize,
43 pub secondary: Option<TypeErrorSpan>,
45}
46
47#[derive(Debug, Clone)]
48pub struct TypeErrorSpan {
49 pub line: usize,
50 pub col: usize,
51 pub label: String,
52}
53
54#[derive(Debug)]
56pub struct TypeCheckResult {
57 pub errors: Vec<TypeError>,
58 pub fn_sigs: HashMap<String, (Vec<Type>, Type, Vec<String>)>,
61 pub memo_safe_types: HashSet<String>,
63 pub unused_bindings: Vec<(String, String, usize)>,
65}
66
67pub fn run_type_check(items: &[TopLevel]) -> Vec<TypeError> {
68 run_type_check_with_base(items, None)
69}
70
71pub fn run_type_check_with_base(items: &[TopLevel], base_dir: Option<&str>) -> Vec<TypeError> {
72 run_type_check_full(items, base_dir).errors
73}
74
75pub fn run_type_check_full(items: &[TopLevel], base_dir: Option<&str>) -> TypeCheckResult {
76 let mut checker = TypeChecker::new();
77 checker.check(items, base_dir);
78 finalize_check_result(checker, items)
79}
80
81pub fn run_type_check_with_loaded(
86 items: &[TopLevel],
87 loaded: &[crate::source::LoadedModule],
88) -> TypeCheckResult {
89 let mut checker = TypeChecker::new();
90 checker.check_with_loaded(items, loaded);
91 finalize_check_result(checker, items)
92}
93
94fn finalize_check_result(mut checker: TypeChecker, items: &[TopLevel]) -> TypeCheckResult {
95 let fn_sigs: HashMap<String, (Vec<Type>, Type, Vec<String>)> = checker
96 .fn_sigs
97 .iter()
98 .map(|(k, v)| {
99 (
100 k.clone(),
101 (v.params.clone(), v.ret.clone(), v.effects.clone()),
102 )
103 })
104 .collect();
105
106 let memo_safe_types = checker.compute_memo_safe_types(items);
107
108 check_module_effect_boundary(items, &mut checker.errors);
109
110 TypeCheckResult {
111 errors: checker.errors,
112 fn_sigs,
113 memo_safe_types,
114 unused_bindings: checker.unused_warnings,
115 }
116}
117
118fn check_module_effect_boundary(items: &[TopLevel], errors: &mut Vec<TypeError>) {
128 let Some(allowed) = items.iter().find_map(|i| match i {
129 TopLevel::Module(m) => m.effects.as_ref().map(|e| (e, m)),
130 _ => None,
131 }) else {
132 return;
133 };
134 let (allowed_list, module) = allowed;
135
136 let allowed_namespaces: HashSet<&str> = allowed_list
137 .iter()
138 .filter(|e| !e.contains('.'))
139 .map(|e| e.as_str())
140 .collect();
141 let allowed_methods: HashSet<&str> = allowed_list.iter().map(|e| e.as_str()).collect();
142
143 for item in items {
144 let TopLevel::FnDef(fd) = item else { continue };
145 for eff in &fd.effects {
146 let method = eff.node.as_str();
147 if allowed_methods.contains(method) {
148 continue;
149 }
150 if let Some((ns, _)) = method.split_once('.')
151 && allowed_namespaces.contains(ns)
152 {
153 continue;
154 }
155 errors.push(TypeError {
156 message: format!(
157 "module '{}' declared `effects [{}]` but '{}' uses '{}' which is not in the declared boundary",
158 module.name,
159 allowed_list.join(", "),
160 fd.name,
161 method
162 ),
163 line: eff.line,
164 col: 1,
165 secondary: module.effects_line.map(|l| TypeErrorSpan {
166 line: l,
167 col: 1,
168 label: "module effects declared here".to_string(),
169 }),
170 });
171 }
172 }
173}
174
175#[derive(Debug, Clone)]
180struct FnSig {
181 params: Vec<Type>,
182 ret: Type,
183 effects: Vec<String>,
184}
185
186struct TypeChecker {
187 fn_sigs: HashMap<String, FnSig>,
188 value_members: HashMap<String, Type>,
189 record_field_types: HashMap<String, Type>,
193 sig_aliases: HashMap<String, String>,
196 type_variants: HashMap<String, Vec<String>>,
199 globals: HashMap<String, Type>,
201 locals: HashMap<String, Type>,
203 errors: Vec<TypeError>,
204 current_fn_ret: Option<Type>,
206 current_fn_line: Option<usize>,
208 opaque_types: HashSet<String>,
210 used_names: HashSet<String>,
212 fn_bindings: Vec<(String, usize)>,
214 unused_warnings: Vec<(String, String, usize)>,
216 in_verify_trace_context: bool,
223}
224
225impl TypeChecker {
226 fn new() -> Self {
227 let mut type_variants = HashMap::new();
228 type_variants.insert(
229 "Result".to_string(),
230 vec!["Ok".to_string(), "Err".to_string()],
231 );
232 type_variants.insert(
233 "Option".to_string(),
234 vec!["Some".to_string(), "None".to_string()],
235 );
236
237 let mut tc = TypeChecker {
238 fn_sigs: HashMap::new(),
239 value_members: HashMap::new(),
240 record_field_types: HashMap::new(),
241 sig_aliases: HashMap::new(),
242 type_variants,
243 globals: HashMap::new(),
244 locals: HashMap::new(),
245 errors: Vec::new(),
246 current_fn_ret: None,
247 current_fn_line: None,
248 opaque_types: HashSet::new(),
249 used_names: HashSet::new(),
250 fn_bindings: Vec::new(),
251 unused_warnings: Vec::new(),
252 in_verify_trace_context: false,
253 };
254 tc.register_builtins();
255 tc
256 }
257
258 fn find_fn_sig(&self, key: &str) -> Option<&FnSig> {
261 self.fn_sigs
262 .get(key)
263 .or_else(|| self.sig_aliases.get(key).and_then(|c| self.fn_sigs.get(c)))
264 }
265
266 fn find_value_member(&self, key: &str) -> Option<&Type> {
267 self.value_members.get(key).or_else(|| {
268 self.sig_aliases
269 .get(key)
270 .and_then(|c| self.value_members.get(c))
271 })
272 }
273
274 fn find_record_field_type(&self, key: &str) -> Option<&Type> {
275 self.record_field_types.get(key).or_else(|| {
276 self.sig_aliases
277 .get(key)
278 .and_then(|c| self.record_field_types.get(c))
279 })
280 }
281
282 fn caller_has_effect(&self, caller_effects: &[String], required_effect: &str) -> bool {
286 caller_effects
287 .iter()
288 .any(|declared| crate::effects::effect_satisfies(declared, required_effect))
289 }
290
291 fn error(&mut self, msg: impl Into<String>) {
292 let line = self.current_fn_line.unwrap_or(1);
293 self.errors.push(TypeError {
294 message: msg.into(),
295 line,
296 col: 0,
297 secondary: None,
298 });
299 }
300
301 fn error_at_line(&mut self, line: usize, msg: impl Into<String>) {
302 self.errors.push(TypeError {
303 message: msg.into(),
304 line,
305 col: 0,
306 secondary: None,
307 });
308 }
309
310 fn insert_sig(&mut self, name: &str, params: &[Type], ret: Type, effects: &[&str]) {
311 self.fn_sigs.insert(
312 name.to_string(),
313 FnSig {
314 params: params.to_vec(),
315 ret,
316 effects: effects.iter().map(|s| s.to_string()).collect(),
317 },
318 );
319 }
320
321 fn fn_type_from_sig(sig: &FnSig) -> Type {
322 Type::Fn(
323 sig.params.clone(),
324 Box::new(sig.ret.clone()),
325 sig.effects.clone(),
326 )
327 }
328
329 fn sig_from_callable_type(ty: &Type) -> Option<FnSig> {
330 match ty {
331 Type::Fn(params, ret, effects) => Some(FnSig {
332 params: params.clone(),
333 ret: *ret.clone(),
334 effects: effects.clone(),
335 }),
336 _ => None,
337 }
338 }
339
340 fn binding_type(&self, name: &str) -> Option<Type> {
341 self.locals
342 .get(name)
343 .or_else(|| self.globals.get(name))
344 .cloned()
345 }
346
347 pub(super) fn constraint_compatible(actual: &Type, expected: &Type) -> bool {
354 if matches!(actual, Type::Unknown) && !matches!(expected, Type::Unknown) {
355 return false;
356 }
357 actual.compatible(expected)
358 }
359}