1pub mod ctx;
2pub mod error;
3mod mono_type;
4mod occurs_in;
5mod polymorphic_function;
6mod substitute;
7mod substitute_from_ctx;
8mod ty;
9mod utils;
10mod well_formed;
11mod with_effects;
12
13use std::{cell::RefCell, rc::Rc};
14
15use ctx::Ctx;
16use error::{ExprTypeError, TypeError};
17use hir::{expr::Expr, meta::WithMeta};
18use ty::Type;
19use types::IdGen;
20use with_effects::WithEffects;
21
22pub fn synth(next_id: usize, expr: &WithMeta<Expr>) -> Result<(Ctx, Type), ExprTypeError> {
23 Ctx {
24 id_gen: Rc::new(RefCell::new(IdGen { next_id })),
25 ..Default::default()
26 }
27 .synth(expr)
28 .map(|WithEffects((ctx, ty), effects)| {
29 assert!(ctx.continue_input.borrow().is_empty());
30 assert!(ctx.continue_output.borrow().is_empty());
31 let ty = ctx.substitute_from_ctx(&ty);
32 let with_effects = ctx.with_effects(ty, effects);
33 (ctx, with_effects)
34 })
35}
36
37fn to_expr_type_error(expr: &WithMeta<Expr>, error: TypeError) -> ExprTypeError {
38 ExprTypeError {
39 meta: expr.meta.clone(),
40 error,
41 }
42}
43
44#[cfg(test)]
45mod tests {
46 use ariadne::{Label, Report, ReportKind, Source};
47 use file::FileId;
48 use hir::{expr::Literal, meta::dummy_meta};
49 use hirgen::HirGen;
50 use pretty_assertions::assert_eq;
51 use textual_diagnostics::TextualDiagnostics;
52
53 use crate::{
54 ctx::Ctx,
55 ty::{effect_expr::EffectExpr, Effect},
56 };
57
58 use super::*;
59
60 fn synth(expr: WithMeta<Expr>) -> Result<Type, ExprTypeError> {
61 crate::synth(100, &expr).map(|(_, ty)| ty)
62 }
63
64 fn parse(input: &str) -> WithMeta<Expr> {
65 parse_inner(input).1
66 }
67
68 fn parse_inner(input: &str) -> (HirGen, WithMeta<Expr>) {
69 let tokens = lexer::scan(input).unwrap();
70 let ast = parser::parse(tokens).unwrap();
71 hirgen::gen_hir(FileId(0), &ast, Default::default()).unwrap()
72 }
73
74 fn get_types(hirgen: &HirGen, ctx: &Ctx) -> Vec<(usize, Type)> {
75 let mut vec: Vec<_> = hirgen
76 .attrs
77 .borrow()
78 .iter()
79 .flat_map(|(id, attrs)| {
80 attrs.iter().map(|attr| match attr {
81 Expr::Literal(Literal::Int(attr)) => (*attr as usize, *id),
82 _ => todo!(),
83 })
84 })
85 .map(|(attr, id)| (attr, ctx.get_type(&id)))
86 .collect();
87
88 vec.sort_by_key(|(attr, _)| *attr);
89 vec
90 }
91
92 fn print_error<T>(input: &str, error: ExprTypeError) -> T {
93 let diagnostics: TextualDiagnostics = error.into();
94 let report = Report::build(ReportKind::Error, (), 0).with_message(diagnostics.title);
95 diagnostics
96 .reports
97 .into_iter()
98 .fold(
99 report,
100 |report, textual_diagnostics::Report { span, text }| {
101 report.with_label(Label::new(span).with_message(text))
102 },
103 )
104 .finish()
105 .print(Source::from(input))
106 .unwrap();
107 panic!()
108 }
109
110 #[test]
111 fn number() {
112 assert_eq!(
113 synth(dummy_meta(Expr::Literal(Literal::Int(1)))),
114 Ok(Type::Number)
115 );
116 }
117
118 #[test]
119 fn function() {
120 assert_eq!(
121 synth(dummy_meta(Expr::Apply {
122 function: dummy_meta(hir::ty::Type::Function {
123 parameter: Box::new(dummy_meta(hir::ty::Type::Number)),
124 body: Box::new(dummy_meta(hir::ty::Type::String)),
125 }),
126 link_name: Default::default(),
127 arguments: vec![dummy_meta(Expr::Literal(Literal::Int(1))),]
128 })),
129 Ok(Type::String)
130 );
131 }
132
133 #[test]
134 fn let_() {
135 assert_eq!(
136 synth(parse(
137 r#"
138 $ 1 ~ &'number
139 "#
140 )),
141 Ok(Type::Number)
142 );
143 }
144
145 #[test]
146 fn let_with_type() {
147 assert_eq!(
148 synth(parse(
149 r#"
150 $ 1: 'a x ~ &'a x
151 "#
152 )),
153 Ok(Type::Number)
154 );
155 }
156
157 #[test]
158 fn generic_function() {
159 assert_eq!(
160 synth(parse(
161 r#"
162 \ 'a x -> &'a x
163 "#
164 )),
165 Ok(Type::Function {
166 parameter: Box::new(Type::Existential(101)),
167 body: Box::new(Type::Existential(101)),
168 })
169 );
170 }
171
172 #[test]
173 fn let_function() {
174 assert_eq!(
175 synth(parse(
176 r#"
177 $ \ 'a x -> &'a x: 'a id ~
178 >'a id 1
179 "#
180 )),
181 Ok(Type::Number)
182 );
183 }
184
185 #[test]
186 fn typing_expressions() {
187 let input = &r#"
188 #1 $ #2 \ 'a x -> #3 &'a x: 'a id ~
189 $ #4 >'a id #5 1 ~
190 #6 >'a id #7 "a"
191 "#;
192 let (hirgen, expr) = parse_inner(input);
193 let (ctx, _ty) = crate::synth(100, &expr).unwrap_or_else(|error| print_error(input, error));
194
195 assert_eq!(
196 get_types(&hirgen, &ctx),
197 vec![
198 (1, Type::String),
199 (
200 2,
201 Type::Function {
202 parameter: Box::new(Type::Existential(102)),
203 body: Box::new(Type::Existential(102)),
204 },
205 ),
206 (3, Type::Existential(102)),
207 (4, Type::Number),
208 (5, Type::Number),
209 (6, Type::String),
210 (7, Type::String),
211 ],
212 );
213 }
214
215 #[test]
216 fn subtyping_sum_in_product() {
217 let (hirgen, expr) = parse_inner(
218 r#"
219 $ #1 \ + 'number, * -> 1: 'a fun ~
220 #3 >'a fun #2 * 1, "a"
221 "#,
222 );
223 let (ctx, _ty) = crate::synth(100, &expr).unwrap();
224
225 assert_eq!(
226 get_types(&hirgen, &ctx),
227 vec![
228 (
229 1,
230 Type::Function {
231 parameter: Box::new(Type::Sum(vec![Type::Number, Type::Product(vec![])])),
232 body: Box::new(Type::Number),
233 },
234 ),
235 (2, Type::Product(vec![Type::Number, Type::String])),
236 (3, Type::Number),
237 ],
238 );
239 }
240
241 #[test]
242 fn perform() {
243 let (hirgen, expr) = parse_inner(
244 r#"
245 $ #3 \ x -> #2 > \ 'number -> 'string ~ #1 ! &x => 'number: fun ~
246 #4 >fun "a"
247 "#,
248 );
249 let (ctx, _ty) = crate::synth(100, &expr).unwrap();
250
251 assert_eq!(
252 get_types(&hirgen, &ctx),
253 vec![
254 (
255 1,
256 Type::Effectful {
257 ty: Box::new(Type::Number),
258 effects: EffectExpr::Effects(vec![Effect {
259 input: Type::Existential(102),
260 output: Type::Number,
261 }]),
262 },
263 ),
264 (
265 2,
266 Type::Effectful {
267 ty: Box::new(Type::String),
268 effects: EffectExpr::Effects(vec![Effect {
269 input: Type::Existential(102),
270 output: Type::Number,
271 }]),
272 },
273 ),
274 (
275 3,
276 Type::Function {
277 parameter: Box::new(Type::Existential(102)),
278 body: Box::new(Type::Effectful {
279 ty: Box::new(Type::String),
280 effects: EffectExpr::Effects(vec![Effect {
281 input: Type::Existential(102),
282 output: Type::Number,
283 }]),
284 }),
285 },
286 ),
287 (
288 4,
289 Type::Effectful {
290 ty: Box::new(Type::String),
291 effects: EffectExpr::Effects(vec![Effect {
292 input: Type::String,
293 output: Type::Number,
294 }]),
295 }
296 ),
297 ],
298 );
299 }
300
301 #[test]
302 fn handle() {
303 let (hirgen, expr) = parse_inner(
304 r#"
305 \ x, y, z ->
306 #3 'handle #2 > \y -> z ! &x => y ~
307 x => y ->
308 $ ! 1 => 'string ~
309 #1 ! &y => z
310 "#,
311 );
312 let (ctx, _ty) = crate::synth(100, &expr).unwrap();
313
314 assert_eq!(
316 get_types(&hirgen, &ctx),
317 vec![
318 (
319 1,
320 Type::Effectful {
321 ty: Box::new(Type::Existential(109)),
322 effects: EffectExpr::Effects(vec![Effect {
323 input: Type::Existential(105),
324 output: Type::Existential(109),
325 }]),
326 },
327 ),
328 (
329 2,
330 Type::Effectful {
331 ty: Box::new(Type::Existential(109)),
332 effects: EffectExpr::Effects(vec![Effect {
333 input: Type::Existential(101),
334 output: Type::Existential(105),
335 }]),
336 },
337 ),
338 (
339 3,
340 Type::Effectful {
341 ty: Box::new(Type::Existential(109)),
342 effects: EffectExpr::Effects(vec![Effect {
343 input: Type::Number,
344 output: Type::String,
345 }]),
346 },
347 ),
348 ],
349 );
350 }
351
352 #[test]
353 fn test_continue() {
354 let (hirgen, expr) = parse_inner(
355 r#"
356 \x, y ->
357 #3 'handle #2 > \'number -> 'string ! &x => 'number ~
358 x => 'number ->
359 #1 <! &y
360 "#,
361 );
362 let (ctx, _ty) = crate::synth(100, &expr).unwrap();
363
364 assert_eq!(
365 get_types(&hirgen, &ctx),
366 vec![
367 (
368 1,
369 Type::Effectful {
370 ty: Box::new(Type::String),
371 effects: EffectExpr::Effects(vec![Effect {
372 input: Type::Number,
373 output: Type::String,
374 }]),
375 },
376 ),
377 (
378 2,
379 Type::Effectful {
380 ty: Box::new(Type::String),
381 effects: EffectExpr::Effects(vec![Effect {
382 input: Type::Existential(101),
383 output: Type::Number,
384 }]),
385 },
386 ),
387 (3, Type::String),
388 ]
389 );
390 }
391
392 #[test]
393 fn test_continue_with_output() {
394 let (hirgen, expr) = parse_inner(
395 r#"
396 \x, y ->
397 #3 'handle #2 > \'number -> y ! &x => 'number ~
398 x => 'number ->
399 #1 <! 1 => 'string
400 "#,
401 );
402 let (ctx, _ty) = crate::synth(100, &expr).unwrap();
403
404 assert_eq!(
405 get_types(&hirgen, &ctx),
406 vec![
407 (
408 1,
409 Type::Effectful {
410 ty: Box::new(Type::String),
411 effects: EffectExpr::Effects(vec![Effect {
412 input: Type::Number,
413 output: Type::String,
414 }]),
415 },
416 ),
417 (
418 2,
419 Type::Effectful {
420 ty: Box::new(Type::Existential(105)),
421 effects: EffectExpr::Effects(vec![Effect {
422 input: Type::Existential(101),
423 output: Type::Number,
424 }]),
425 },
426 ),
427 (3, Type::String),
428 ]
429 );
430 }
431
432 #[test]
433 #[ignore = "not yet implemented"]
434 fn test_polymorphic_effectful() {
435 let input = r#"
436 $ #1 \x, y ->
437 ^#2 'handle > x 1 ~
438 'number => 'string ->
439 > y 2
440 : 'number
441 : fun ~
442 #3 >fun
443 \ @x 'number ->
444 $ ! 1 => 'string ~
445 ! @a * => 'number,
446 \ @y 'number ->
447 $ ! "a" => 'number ~
448 ! @b * => 'number
449 "#;
450 let (hirgen, expr) = parse_inner(input);
451 let (ctx, _ty) = crate::synth(100, &expr).unwrap_or_else(|error| print_error(input, error));
452
453 assert_eq!(
454 get_types(&hirgen, &ctx),
455 vec![
456 (
457 1,
458 Type::Function {
459 parameter: Box::new(Type::Existential(2)),
460 body: Box::new(Type::Function {
461 parameter: Box::new(Type::Function {
462 parameter: Box::new(Type::Existential(23)),
463 body: Box::new(Type::Number)
464 }),
465 body: Box::new(Type::Effectful {
466 ty: Box::new(Type::Number),
467 effects: EffectExpr::Add(vec![])
468 })
469 })
470 }
471 ),
472 (
473 2,
474 Type::Effectful {
475 ty: Box::new(Type::Number),
476 effects: EffectExpr::Effects(vec![
477 Effect {
478 input: Type::Label {
479 label: "a".into(),
480 item: Box::new(Type::Product(vec![]))
481 },
482 output: Type::Number,
483 },
484 Effect {
485 input: Type::Label {
486 label: "b".into(),
487 item: Box::new(Type::Product(vec![]))
488 },
489 output: Type::Number,
490 }
491 ]),
492 },
493 ),
494 ]
495 );
496 }
497
498 #[test]
499 fn label() {
500 let expr = parse(
501 r#"
502 ^^^1: @labeled 'number: 'number: @labeled 'number
503 "#,
504 );
505 assert_eq!(
506 synth(expr),
507 Ok(Type::Label {
508 label: "labeled".into(),
509 item: Box::new(Type::Number),
510 })
511 );
512 }
513
514 #[test]
515 fn instantiate_label() {
516 let expr = parse(
517 r#"
518 \ 'a x -> ^&'a x: @labeled 'number
519 "#,
520 );
521 assert_eq!(
522 synth(expr),
523 Ok(Type::Function {
524 parameter: Box::new(Type::Label {
525 label: "labeled".into(),
526 item: Box::new(Type::Number),
527 }),
528 body: Box::new(Type::Label {
529 label: "labeled".into(),
530 item: Box::new(Type::Number),
531 })
532 })
533 );
534 }
535
536 #[test]
537 fn brand_supertype() {
538 let expr = parse(
539 r#"
540 'brand brand
541 ^1: @brand 'number
542 "#,
543 );
544 assert_eq!(
545 synth(expr).map_err(|e| e.error),
546 Err(TypeError::NotSubtype {
547 sub: Type::Number,
548 ty: Type::Brand {
549 brand: "brand".into(),
550 item: Box::new(Type::Number),
551 },
552 })
553 );
554 }
555
556 #[test]
557 fn brand_subtype() {
558 let expr = parse(
559 r#"
560 'brand brand
561 ^&@brand 'number: 'number
562 "#,
563 );
564 assert_eq!(synth(expr), Ok(Type::Number));
565 }
566
567 #[test]
568 fn infer() {
569 let (_hirgen, expr) = parse_inner(
570 r#"
571 ^> \ _ -> 'number "a": _
572 "#,
573 );
574 let (_ctx, ty) = crate::synth(100, &expr).unwrap();
575
576 assert_eq!(ty, Type::Number);
577 }
578
579 #[test]
580 fn test_match() {
581 let (hirgen, expr) = parse_inner(
582 r#"
583 \ 'a x ->
584 #2 + #1 &'a x ~
585 'number -> ^1: @a 'number,
586 'string -> ^2: @b 'number.
587 "#,
588 );
589 let (ctx, _ty) = crate::synth(100, &expr).unwrap();
590
591 assert_eq!(
592 get_types(&hirgen, &ctx),
593 vec![
594 (1, Type::Sum(vec![Type::Number, Type::String])),
595 (
596 2,
597 Type::Sum(vec![
598 Type::Label {
599 label: "a".into(),
600 item: Box::new(Type::Number)
601 },
602 Type::Label {
603 label: "b".into(),
604 item: Box::new(Type::Number)
605 }
606 ])
607 )
608 ]
609 );
610 }
611
612 }