1#[cfg(test)]
6mod tests {
7 use super::*;
8 use crate::ast_impl::{
9 BinderKind, Decl, DoAction, Literal, Located, Pattern, SortKind, SurfaceExpr,
10 };
11 use crate::error_impl::ParseError;
12 use crate::lexer::Lexer;
13 use crate::parser_impl::*;
14 fn parse_expr_from_str(s: &str) -> Result<Located<SurfaceExpr>, ParseError> {
15 let mut lexer = Lexer::new(s);
16 let tokens = lexer.tokenize();
17 let mut parser = Parser::new(tokens);
18 parser.parse_expr()
19 }
20 fn parse_decl_from_str(s: &str) -> Result<Located<Decl>, ParseError> {
21 let mut lexer = Lexer::new(s);
22 let tokens = lexer.tokenize();
23 let mut parser = Parser::new(tokens);
24 parser.parse_decl()
25 }
26 #[test]
27 fn test_parse_var() {
28 let expr = parse_expr_from_str("x").expect("parse_expr should succeed");
29 assert!(matches!(expr.value, SurfaceExpr::Var(_)));
30 }
31 #[test]
32 fn test_parse_nat() {
33 let expr = parse_expr_from_str("42").expect("parse_expr should succeed");
34 assert_eq!(expr.value, SurfaceExpr::Lit(Literal::Nat(42)));
35 }
36 #[test]
37 fn test_parse_type() {
38 let expr = parse_expr_from_str("Type").expect("parse_expr should succeed");
39 assert_eq!(expr.value, SurfaceExpr::Sort(SortKind::Type));
40 }
41 #[test]
42 fn test_parse_app() {
43 let expr = parse_expr_from_str("f x").expect("parse_expr should succeed");
44 assert!(matches!(expr.value, SurfaceExpr::App(_, _)));
45 }
46 #[test]
47 fn test_parse_arrow() {
48 let expr = parse_expr_from_str("A -> B").expect("parse_expr should succeed");
49 assert!(matches!(expr.value, SurfaceExpr::Pi(_, _)));
50 }
51 #[test]
52 fn test_parse_lambda() {
53 let expr = parse_expr_from_str("fun (x : Nat) -> x").expect("parse_expr should succeed");
54 assert!(matches!(expr.value, SurfaceExpr::Lam(_, _)));
55 }
56 #[test]
57 fn test_parse_paren() {
58 let expr = parse_expr_from_str("(x)").expect("parse_expr should succeed");
59 assert!(matches!(expr.value, SurfaceExpr::Var(_)));
60 }
61 #[test]
62 fn test_parse_hole() {
63 let expr = parse_expr_from_str("_").expect("parse_expr should succeed");
64 assert_eq!(expr.value, SurfaceExpr::Hole);
65 }
66 #[test]
67 fn test_parse_if_then_else() {
68 let expr = parse_expr_from_str("if x then y else z").expect("parse_expr should succeed");
69 assert!(matches!(expr.value, SurfaceExpr::If(_, _, _)));
70 }
71 #[test]
72 fn test_parse_if_nested() {
73 let expr = parse_expr_from_str("if a then if b then c else d else e")
74 .expect("parse_expr should succeed");
75 assert!(matches!(expr.value, SurfaceExpr::If(_, _, _)));
76 }
77 #[test]
78 fn test_parse_match() {
79 let expr = parse_expr_from_str("match x with | y -> z").expect("parse_expr should succeed");
80 match &expr.value {
81 SurfaceExpr::Match(_, arms) => {
82 assert_eq!(arms.len(), 1);
83 }
84 other => panic!("Expected Match, got {:?}", other),
85 }
86 }
87 #[test]
88 fn test_parse_match_multi_arm() {
89 let expr = parse_expr_from_str("match x with | 0 -> a | n -> b")
90 .expect("parse_expr should succeed");
91 match &expr.value {
92 SurfaceExpr::Match(_, arms) => {
93 assert_eq!(arms.len(), 2);
94 }
95 other => panic!("Expected Match, got {:?}", other),
96 }
97 }
98 #[test]
99 fn test_parse_match_wildcard() {
100 let expr = parse_expr_from_str("match x with | _ -> y").expect("parse_expr should succeed");
101 match &expr.value {
102 SurfaceExpr::Match(_, arms) => {
103 assert!(matches!(arms[0].pattern.value, Pattern::Wild));
104 }
105 other => panic!("Expected Match, got {:?}", other),
106 }
107 }
108 #[test]
109 fn test_parse_match_ctor_pattern() {
110 let expr =
111 parse_expr_from_str("match x with | Cons h t -> h").expect("parse_expr should succeed");
112 match &expr.value {
113 SurfaceExpr::Match(_, arms) => {
114 assert!(matches!(arms[0].pattern.value, Pattern::Ctor(_, _)));
115 }
116 other => panic!("Expected Match, got {:?}", other),
117 }
118 }
119 #[test]
120 fn test_parse_match_with_guard() {
121 let expr = parse_expr_from_str("match x with | n if cond -> body")
122 .expect("parse_expr should succeed");
123 match &expr.value {
124 SurfaceExpr::Match(_, arms) => {
125 assert_eq!(arms.len(), 1);
126 assert!(arms[0].guard.is_some(), "guard should be Some");
127 if let Some(guard) = &arms[0].guard {
128 assert!(matches!(guard.value, SurfaceExpr::Var(_)));
129 }
130 }
131 other => panic!("Expected Match, got {:?}", other),
132 }
133 }
134 #[test]
135 fn test_parse_match_no_guard() {
136 let expr =
137 parse_expr_from_str("match x with | n -> body").expect("parse_expr should succeed");
138 match &expr.value {
139 SurfaceExpr::Match(_, arms) => {
140 assert_eq!(arms.len(), 1);
141 assert!(arms[0].guard.is_none(), "guard should be None");
142 }
143 other => panic!("Expected Match, got {:?}", other),
144 }
145 }
146 #[test]
147 fn test_parse_do() {
148 let expr = parse_expr_from_str("do { x }").expect("parse_expr should succeed");
149 assert!(matches!(expr.value, SurfaceExpr::Do(_)));
150 }
151 #[test]
152 fn test_parse_do_multi_action() {
153 let expr = parse_expr_from_str("do { let x := 1; x }").expect("parse_expr should succeed");
154 match &expr.value {
155 SurfaceExpr::Do(actions) => {
156 assert_eq!(actions.len(), 2);
157 assert!(matches!(actions[0], DoAction::Let(_, _)));
158 assert!(matches!(actions[1], DoAction::Expr(_)));
159 }
160 other => panic!("Expected Do, got {:?}", other),
161 }
162 }
163 #[test]
164 fn test_parse_do_bind() {
165 let expr =
166 parse_expr_from_str("do { x <- getLine; x }").expect("parse_expr should succeed");
167 match &expr.value {
168 SurfaceExpr::Do(actions) => {
169 assert_eq!(actions.len(), 2);
170 assert!(matches!(actions[0], DoAction::Bind(_, _)));
171 }
172 other => panic!("Expected Do, got {:?}", other),
173 }
174 }
175 #[test]
176 fn test_parse_have() {
177 let expr = parse_expr_from_str("have h : Nat := 42; h").expect("parse_expr should succeed");
178 match &expr.value {
179 SurfaceExpr::Have(name, _, _, _) => {
180 assert_eq!(name, "h");
181 }
182 other => panic!("Expected Have, got {:?}", other),
183 }
184 }
185 #[test]
186 fn test_parse_suffices() {
187 let expr =
188 parse_expr_from_str("suffices h : Nat by auto").expect("parse_expr should succeed");
189 match &expr.value {
190 SurfaceExpr::Suffices(name, _, _) => {
191 assert_eq!(name, "h");
192 }
193 other => panic!("Expected Suffices, got {:?}", other),
194 }
195 }
196 #[test]
197 fn test_parse_show() {
198 let expr = parse_expr_from_str("show Nat from 42").expect("parse_expr should succeed");
199 assert!(matches!(expr.value, SurfaceExpr::Show(_, _)));
200 }
201 #[test]
202 fn test_parse_tuple() {
203 let expr = parse_expr_from_str("(1, 2)").expect("parse_expr should succeed");
204 match &expr.value {
205 SurfaceExpr::Tuple(elems) => {
206 assert_eq!(elems.len(), 2);
207 }
208 other => panic!("Expected Tuple, got {:?}", other),
209 }
210 }
211 #[test]
212 fn test_parse_tuple_triple() {
213 let expr = parse_expr_from_str("(1, 2, 3)").expect("parse_expr should succeed");
214 match &expr.value {
215 SurfaceExpr::Tuple(elems) => {
216 assert_eq!(elems.len(), 3);
217 }
218 other => panic!("Expected Tuple, got {:?}", other),
219 }
220 }
221 #[test]
222 fn test_parse_list_empty() {
223 let expr = parse_expr_from_str("[]").expect("parse_expr should succeed");
224 match &expr.value {
225 SurfaceExpr::ListLit(elems) => {
226 assert!(elems.is_empty());
227 }
228 other => panic!("Expected ListLit, got {:?}", other),
229 }
230 }
231 #[test]
232 fn test_parse_list() {
233 let expr = parse_expr_from_str("[1, 2, 3]").expect("parse_expr should succeed");
234 match &expr.value {
235 SurfaceExpr::ListLit(elems) => {
236 assert_eq!(elems.len(), 3);
237 }
238 other => panic!("Expected ListLit, got {:?}", other),
239 }
240 }
241 #[test]
242 fn test_parse_type_annotation() {
243 let expr = parse_expr_from_str("(x : Nat)").expect("parse_expr should succeed");
244 assert!(matches!(expr.value, SurfaceExpr::Ann(_, _)));
245 }
246 #[test]
247 fn test_parse_proj() {
248 let expr = parse_expr_from_str("x.foo").expect("parse_expr should succeed");
249 match &expr.value {
250 SurfaceExpr::Proj(_, field) => {
251 assert_eq!(field, "foo");
252 }
253 other => panic!("Expected Proj, got {:?}", other),
254 }
255 }
256 #[test]
257 fn test_parse_proj_chain() {
258 let expr = parse_expr_from_str("x.foo.bar").expect("parse_expr should succeed");
259 match &expr.value {
260 SurfaceExpr::Proj(inner, field) => {
261 assert_eq!(field, "bar");
262 assert!(matches!(inner.value, SurfaceExpr::Proj(_, _)));
263 }
264 other => panic!("Expected Proj, got {:?}", other),
265 }
266 }
267 #[test]
268 fn test_parse_plus() {
269 let expr = parse_expr_from_str("a + b").expect("parse_expr should succeed");
270 match &expr.value {
271 SurfaceExpr::App(lhs, rhs) => {
272 assert!(matches!(rhs.value, SurfaceExpr::Var(_)));
273 match &lhs.value {
274 SurfaceExpr::App(op, _lhs_inner) => {
275 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "+"));
276 }
277 other => panic!("Expected App, got {:?}", other),
278 }
279 }
280 other => panic!("Expected App, got {:?}", other),
281 }
282 }
283 #[test]
284 fn test_parse_binop_precedence() {
285 let expr = parse_expr_from_str("a + b * c").expect("parse_expr should succeed");
286 match &expr.value {
287 SurfaceExpr::App(lhs, _rhs) => match &lhs.value {
288 SurfaceExpr::App(op, _) => {
289 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "+"));
290 }
291 other => panic!("Expected App(Var(+), ..), got {:?}", other),
292 },
293 other => panic!("Expected App, got {:?}", other),
294 }
295 }
296 #[test]
297 fn test_parse_comparison() {
298 let expr = parse_expr_from_str("a < b").expect("parse_expr should succeed");
299 match &expr.value {
300 SurfaceExpr::App(lhs, _) => match &lhs.value {
301 SurfaceExpr::App(op, _) => {
302 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "Lt"));
303 }
304 other => panic!("Expected App, got {:?}", other),
305 },
306 other => panic!("Expected App, got {:?}", other),
307 }
308 }
309 #[test]
310 fn test_parse_and_or() {
311 let expr = parse_expr_from_str("a && b").expect("parse_expr should succeed");
312 match &expr.value {
313 SurfaceExpr::App(lhs, _) => match &lhs.value {
314 SurfaceExpr::App(op, _) => {
315 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "&&"));
316 }
317 other => panic!("Expected App, got {:?}", other),
318 },
319 other => panic!("Expected App, got {:?}", other),
320 }
321 }
322 #[test]
323 fn test_parse_not() {
324 let expr = parse_expr_from_str("!x").expect("parse_expr should succeed");
325 match &expr.value {
326 SurfaceExpr::App(func, _) => {
327 assert!(matches!(& func.value, SurfaceExpr::Var(n) if n == "Not"));
328 }
329 other => panic!("Expected App(Not, x), got {:?}", other),
330 }
331 }
332 #[test]
333 fn test_parse_string_lit() {
334 let expr = parse_expr_from_str(r#""hello""#).expect("parse_expr should succeed");
335 assert_eq!(
336 expr.value,
337 SurfaceExpr::Lit(Literal::String("hello".to_string()))
338 );
339 }
340 #[test]
341 fn test_parse_question_mark_hole() {
342 let expr = parse_expr_from_str("?").expect("parse_expr should succeed");
343 assert_eq!(expr.value, SurfaceExpr::Hole);
344 }
345 #[test]
346 fn test_parse_prop() {
347 let expr = parse_expr_from_str("Prop").expect("parse_expr should succeed");
348 assert_eq!(expr.value, SurfaceExpr::Sort(SortKind::Prop));
349 }
350 #[test]
351 fn test_parse_forall() {
352 let expr = parse_expr_from_str("forall (x : Nat), x").expect("parse_expr should succeed");
353 assert!(matches!(expr.value, SurfaceExpr::Pi(_, _)));
354 }
355 #[test]
356 fn test_parse_let() {
357 let expr = parse_expr_from_str("let x := 1 in x").expect("parse_expr should succeed");
358 assert!(matches!(expr.value, SurfaceExpr::Let(_, _, _, _)));
359 }
360 #[test]
361 fn test_parse_let_typed() {
362 let expr = parse_expr_from_str("let x : Nat := 1 in x").expect("parse_expr should succeed");
363 match &expr.value {
364 SurfaceExpr::Let(name, ty, _, _) => {
365 assert_eq!(name, "x");
366 assert!(ty.is_some());
367 }
368 other => panic!("Expected Let, got {:?}", other),
369 }
370 }
371 #[test]
372 fn test_parse_implicit_binder() {
373 let expr = parse_expr_from_str("fun {x : Nat} -> x").expect("parse_expr should succeed");
374 match &expr.value {
375 SurfaceExpr::Lam(binders, _) => {
376 assert_eq!(binders.len(), 1);
377 assert_eq!(binders[0].info, BinderKind::Implicit);
378 }
379 other => panic!("Expected Lam, got {:?}", other),
380 }
381 }
382 #[test]
383 fn test_parse_instance_binder() {
384 let expr = parse_expr_from_str("fun [x : Monad] -> x").expect("parse_expr should succeed");
385 match &expr.value {
386 SurfaceExpr::Lam(binders, _) => {
387 assert_eq!(binders.len(), 1);
388 assert_eq!(binders[0].info, BinderKind::Instance);
389 }
390 other => panic!("Expected Lam, got {:?}", other),
391 }
392 }
393 #[test]
394 fn test_parse_strict_implicit_binder() {
395 let expr = parse_expr_from_str("fun {{x : Nat}} -> x").expect("parse_expr should succeed");
396 match &expr.value {
397 SurfaceExpr::Lam(binders, _) => {
398 assert_eq!(binders.len(), 1);
399 assert_eq!(binders[0].info, BinderKind::StrictImplicit);
400 }
401 other => panic!("Expected Lam, got {:?}", other),
402 }
403 }
404 #[test]
405 fn test_parse_mixed_binders() {
406 let expr = parse_expr_from_str("fun (a : Nat) {b : Nat} [c : Monad] -> a")
407 .expect("parse_expr should succeed");
408 match &expr.value {
409 SurfaceExpr::Lam(binders, _) => {
410 assert_eq!(binders.len(), 3);
411 assert_eq!(binders[0].info, BinderKind::Default);
412 assert_eq!(binders[1].info, BinderKind::Implicit);
413 assert_eq!(binders[2].info, BinderKind::Instance);
414 }
415 other => panic!("Expected Lam, got {:?}", other),
416 }
417 }
418 #[test]
419 fn test_parse_axiom_decl() {
420 let decl = parse_decl_from_str("axiom A : Prop").expect("parse_decl should succeed");
421 match &decl.value {
422 Decl::Axiom { name, .. } => assert_eq!(name, "A"),
423 other => panic!("Expected Axiom, got {:?}", other),
424 }
425 }
426 #[test]
427 fn test_parse_def_decl() {
428 let decl = parse_decl_from_str("def x := 42").expect("parse_decl should succeed");
429 match &decl.value {
430 Decl::Definition { name, ty, .. } => {
431 assert_eq!(name, "x");
432 assert!(ty.is_none());
433 }
434 other => panic!("Expected Definition, got {:?}", other),
435 }
436 }
437 #[test]
438 fn test_parse_def_typed() {
439 let decl = parse_decl_from_str("def x : Nat := 42").expect("parse_decl should succeed");
440 match &decl.value {
441 Decl::Definition { name, ty, .. } => {
442 assert_eq!(name, "x");
443 assert!(ty.is_some());
444 }
445 other => panic!("Expected Definition, got {:?}", other),
446 }
447 }
448 #[test]
449 fn test_parse_theorem_decl() {
450 let decl = parse_decl_from_str("theorem t : Prop := x").expect("parse_decl should succeed");
451 match &decl.value {
452 Decl::Theorem { name, .. } => assert_eq!(name, "t"),
453 other => panic!("Expected Theorem, got {:?}", other),
454 }
455 }
456 #[test]
457 fn test_parse_lemma_decl() {
458 let decl = parse_decl_from_str("lemma l : Prop := x").expect("parse_decl should succeed");
459 match &decl.value {
460 Decl::Theorem { name, .. } => assert_eq!(name, "l"),
461 other => panic!("Expected Theorem, got {:?}", other),
462 }
463 }
464 #[test]
465 fn test_parse_import_decl() {
466 let decl = parse_decl_from_str("import Foo.Bar").expect("parse_decl should succeed");
467 match &decl.value {
468 Decl::Import { path } => {
469 assert_eq!(path, &["Foo", "Bar"]);
470 }
471 other => panic!("Expected Import, got {:?}", other),
472 }
473 }
474 #[test]
475 fn test_parse_structure_decl() {
476 let decl = parse_decl_from_str("structure Point where x : Nat y : Nat")
477 .expect("parse_decl should succeed");
478 match &decl.value {
479 Decl::Structure { name, fields, .. } => {
480 assert_eq!(name, "Point");
481 assert_eq!(fields.len(), 2);
482 assert_eq!(fields[0].name, "x");
483 assert_eq!(fields[1].name, "y");
484 }
485 other => panic!("Expected Structure, got {:?}", other),
486 }
487 }
488 #[test]
489 fn test_parse_class_decl() {
490 let decl =
491 parse_decl_from_str("class Monoid where op : Nat").expect("parse_decl should succeed");
492 match &decl.value {
493 Decl::ClassDecl { name, fields, .. } => {
494 assert_eq!(name, "Monoid");
495 assert_eq!(fields.len(), 1);
496 }
497 other => panic!("Expected ClassDecl, got {:?}", other),
498 }
499 }
500 #[test]
501 fn test_parse_instance_decl() {
502 let decl = parse_decl_from_str("instance : Monoid Nat where op := 42")
503 .expect("parse_decl should succeed");
504 match &decl.value {
505 Decl::InstanceDecl {
506 name,
507 class_name,
508 defs,
509 ..
510 } => {
511 assert!(name.is_none());
512 assert_eq!(class_name, "Monoid");
513 assert_eq!(defs.len(), 1);
514 assert_eq!(defs[0].0, "op");
515 }
516 other => panic!("Expected InstanceDecl, got {:?}", other),
517 }
518 }
519 #[test]
520 fn test_parse_instance_named() {
521 let decl = parse_decl_from_str("instance myInst : Monoid Nat where op := 42")
522 .expect("parse_decl should succeed");
523 match &decl.value {
524 Decl::InstanceDecl { name, .. } => {
525 assert_eq!(name.as_deref(), Some("myInst"));
526 }
527 other => panic!("Expected InstanceDecl, got {:?}", other),
528 }
529 }
530 #[test]
531 fn test_parse_section_decl() {
532 let decl = parse_decl_from_str("section Foo axiom a : Prop end Foo")
533 .expect("parse_decl should succeed");
534 match &decl.value {
535 Decl::SectionDecl { name, decls } => {
536 assert_eq!(name, "Foo");
537 assert_eq!(decls.len(), 1);
538 }
539 other => panic!("Expected SectionDecl, got {:?}", other),
540 }
541 }
542 #[test]
543 fn test_parse_variable_decl() {
544 let decl = parse_decl_from_str("variable (n : Nat)").expect("parse_decl should succeed");
545 match &decl.value {
546 Decl::Variable { binders } => {
547 assert_eq!(binders.len(), 1);
548 assert_eq!(binders[0].name, "n");
549 }
550 other => panic!("Expected Variable, got {:?}", other),
551 }
552 }
553 #[test]
554 fn test_parse_variable_implicit() {
555 let decl = parse_decl_from_str("variable {a : Type}").expect("parse_decl should succeed");
556 match &decl.value {
557 Decl::Variable { binders } => {
558 assert_eq!(binders.len(), 1);
559 assert_eq!(binders[0].info, BinderKind::Implicit);
560 }
561 other => panic!("Expected Variable, got {:?}", other),
562 }
563 }
564 #[test]
565 fn test_parse_open_decl() {
566 let decl = parse_decl_from_str("open Foo.Bar").expect("parse_decl should succeed");
567 match &decl.value {
568 Decl::Open { path, names } => {
569 assert_eq!(path, &["Foo", "Bar"]);
570 assert!(names.is_empty());
571 }
572 other => panic!("Expected Open, got {:?}", other),
573 }
574 }
575 #[test]
576 fn test_parse_open_with_names() {
577 let decl = parse_decl_from_str("open Foo (bar baz)").expect("parse_decl should succeed");
578 match &decl.value {
579 Decl::Open { path, names } => {
580 assert_eq!(path, &["Foo"]);
581 assert_eq!(names, &["bar", "baz"]);
582 }
583 other => panic!("Expected Open, got {:?}", other),
584 }
585 }
586 #[test]
587 fn test_parse_attribute_decl() {
588 let decl =
589 parse_decl_from_str("@[simp] axiom a : Prop").expect("parse_decl should succeed");
590 match &decl.value {
591 Decl::Attribute { attrs, decl } => {
592 assert_eq!(attrs, &["simp"]);
593 assert!(matches!(decl.value, Decl::Axiom { .. }));
594 }
595 other => panic!("Expected Attribute, got {:?}", other),
596 }
597 }
598 #[test]
599 fn test_parse_attribute_multi() {
600 let decl = parse_decl_from_str("@[simp, ext] theorem t : Prop := x")
601 .expect("parse_decl should succeed");
602 match &decl.value {
603 Decl::Attribute { attrs, .. } => {
604 assert_eq!(attrs, &["simp", "ext"]);
605 }
606 other => panic!("Expected Attribute, got {:?}", other),
607 }
608 }
609 #[test]
610 fn test_parse_hash_check() {
611 let decl = parse_decl_from_str("#check Nat").expect("parse_decl should succeed");
612 match &decl.value {
613 Decl::HashCmd { cmd, .. } => {
614 assert_eq!(cmd, "check");
615 }
616 other => panic!("Expected HashCmd, got {:?}", other),
617 }
618 }
619 #[test]
620 fn test_parse_hash_eval() {
621 let decl = parse_decl_from_str("#eval 42").expect("parse_decl should succeed");
622 match &decl.value {
623 Decl::HashCmd { cmd, arg } => {
624 assert_eq!(cmd, "eval");
625 assert_eq!(arg.value, SurfaceExpr::Lit(Literal::Nat(42)));
626 }
627 other => panic!("Expected HashCmd, got {:?}", other),
628 }
629 }
630 #[test]
631 fn test_parse_hash_print() {
632 let decl = parse_decl_from_str("#print Nat").expect("parse_decl should succeed");
633 match &decl.value {
634 Decl::HashCmd { cmd, .. } => {
635 assert_eq!(cmd, "print");
636 }
637 other => panic!("Expected HashCmd, got {:?}", other),
638 }
639 }
640 #[test]
641 fn test_parse_namespace_decl() {
642 let decl = parse_decl_from_str("namespace Foo axiom a : Prop end Foo")
643 .expect("parse_decl should succeed");
644 match &decl.value {
645 Decl::Namespace { name, decls } => {
646 assert_eq!(name, "Foo");
647 assert_eq!(decls.len(), 1);
648 }
649 other => panic!("Expected Namespace, got {:?}", other),
650 }
651 }
652 #[test]
653 fn test_parse_inductive_decl() {
654 let decl = parse_decl_from_str("inductive Bool : Type | true : Bool | false : Bool")
655 .expect("parse_decl should succeed");
656 match &decl.value {
657 Decl::Inductive { name, ctors, .. } => {
658 assert_eq!(name, "Bool");
659 assert_eq!(ctors.len(), 2);
660 }
661 other => panic!("Expected Inductive, got {:?}", other),
662 }
663 }
664 #[test]
665 fn test_parse_arrow_chain() {
666 let expr = parse_expr_from_str("A -> B -> C").expect("parse_expr should succeed");
667 match &expr.value {
668 SurfaceExpr::Pi(_, body) => {
669 assert!(matches!(body.value, SurfaceExpr::Pi(_, _)));
670 }
671 other => panic!("Expected Pi, got {:?}", other),
672 }
673 }
674 #[test]
675 fn test_parse_app_chain() {
676 let expr = parse_expr_from_str("f x y").expect("parse_expr should succeed");
677 match &expr.value {
678 SurfaceExpr::App(lhs, _) => {
679 assert!(matches!(lhs.value, SurfaceExpr::App(_, _)));
680 }
681 other => panic!("Expected App, got {:?}", other),
682 }
683 }
684 #[test]
685 fn test_parse_minus_prefix() {
686 let expr = parse_expr_from_str("(- x)").expect("parse_expr should succeed");
687 match &expr.value {
688 SurfaceExpr::App(func, _) => {
689 assert!(matches!(& func.value, SurfaceExpr::Var(n) if n == "Neg"));
690 }
691 other => panic!("Expected App(Neg, x), got {:?}", other),
692 }
693 }
694 #[test]
695 fn test_parse_sort_with_universe() {
696 let expr = parse_expr_from_str("Type u").expect("parse_expr should succeed");
697 assert_eq!(
698 expr.value,
699 SurfaceExpr::Sort(SortKind::TypeU("u".to_string()))
700 );
701 }
702 #[test]
703 fn test_parse_empty_tuple() {
704 let expr = parse_expr_from_str("()").expect("parse_expr should succeed");
705 match &expr.value {
706 SurfaceExpr::Tuple(elems) => assert!(elems.is_empty()),
707 other => panic!("Expected empty Tuple, got {:?}", other),
708 }
709 }
710 #[test]
711 fn test_parse_do_let_typed() {
712 let expr =
713 parse_expr_from_str("do { let x : Nat := 1; x }").expect("parse_expr should succeed");
714 match &expr.value {
715 SurfaceExpr::Do(actions) => {
716 assert_eq!(actions.len(), 2);
717 assert!(matches!(actions[0], DoAction::LetTyped(_, _, _)));
718 }
719 other => panic!("Expected Do, got {:?}", other),
720 }
721 }
722 #[test]
723 fn test_parse_caret_right_assoc() {
724 let expr = parse_expr_from_str("a ^ b ^ c").expect("parse_expr should succeed");
725 match &expr.value {
726 SurfaceExpr::App(lhs, _rhs) => match &lhs.value {
727 SurfaceExpr::App(op, _) => {
728 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "^"));
729 }
730 other => panic!("Expected App(^, ...), got {:?}", other),
731 },
732 other => panic!("Expected App, got {:?}", other),
733 }
734 }
735 #[test]
736 fn test_parse_multi_binder_group() {
737 let expr =
738 parse_expr_from_str("fun (a : Nat) (b : Nat) -> a").expect("parse_expr should succeed");
739 match &expr.value {
740 SurfaceExpr::Lam(binders, _) => {
741 assert_eq!(binders.len(), 2);
742 assert_eq!(binders[0].name, "a");
743 assert_eq!(binders[1].name, "b");
744 }
745 other => panic!("Expected Lam, got {:?}", other),
746 }
747 }
748 #[test]
749 fn test_parse_structure_extends() {
750 let decl = parse_decl_from_str("structure ColorPoint extends Point where color : Nat")
751 .expect("parse_decl should succeed");
752 match &decl.value {
753 Decl::Structure { name, extends, .. } => {
754 assert_eq!(name, "ColorPoint");
755 assert_eq!(extends, &["Point"]);
756 }
757 other => panic!("Expected Structure, got {:?}", other),
758 }
759 }
760 #[test]
761 fn test_parse_univ_params() {
762 let decl = parse_decl_from_str("axiom A {u, v} : Prop").expect("parse_decl should succeed");
763 match &decl.value {
764 Decl::Axiom { univ_params, .. } => {
765 assert_eq!(univ_params, &["u", "v"]);
766 }
767 other => panic!("Expected Axiom, got {:?}", other),
768 }
769 }
770 #[test]
771 fn test_parse_eq_binop() {
772 let expr = parse_expr_from_str("a = b").expect("parse_expr should succeed");
773 match &expr.value {
774 SurfaceExpr::App(lhs, _) => match &lhs.value {
775 SurfaceExpr::App(op, _) => {
776 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "Eq"));
777 }
778 other => panic!("Expected App(Eq, ..), got {:?}", other),
779 },
780 other => panic!("Expected App, got {:?}", other),
781 }
782 }
783 #[test]
784 fn test_parse_percent_binop() {
785 let expr = parse_expr_from_str("a % b").expect("parse_expr should succeed");
786 match &expr.value {
787 SurfaceExpr::App(lhs, _) => match &lhs.value {
788 SurfaceExpr::App(op, _) => {
789 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "%"));
790 }
791 other => panic!("Expected App, got {:?}", other),
792 },
793 other => panic!("Expected App, got {:?}", other),
794 }
795 }
796 #[test]
797 fn test_parse_list_single() {
798 let expr = parse_expr_from_str("[42]").expect("parse_expr should succeed");
799 match &expr.value {
800 SurfaceExpr::ListLit(elems) => {
801 assert_eq!(elems.len(), 1);
802 assert_eq!(elems[0].value, SurfaceExpr::Lit(Literal::Nat(42)));
803 }
804 other => panic!("Expected ListLit, got {:?}", other),
805 }
806 }
807 #[test]
808 fn test_parse_or_binop() {
809 let expr = parse_expr_from_str("a || b").expect("parse_expr should succeed");
810 match &expr.value {
811 SurfaceExpr::App(lhs, _) => match &lhs.value {
812 SurfaceExpr::App(op, _) => {
813 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "||"));
814 }
815 other => panic!("Expected App, got {:?}", other),
816 },
817 other => panic!("Expected App, got {:?}", other),
818 }
819 }
820 #[test]
821 fn test_parse_variable_instance_binder() {
822 let decl = parse_decl_from_str("variable [m : Monad]").expect("parse_decl should succeed");
823 match &decl.value {
824 Decl::Variable { binders } => {
825 assert_eq!(binders.len(), 1);
826 assert_eq!(binders[0].info, BinderKind::Instance);
827 assert_eq!(binders[0].name, "m");
828 }
829 other => panic!("Expected Variable, got {:?}", other),
830 }
831 }
832 #[test]
833 fn test_parse_do_without_braces() {
834 let expr = parse_expr_from_str("do x <- getLine; x").expect("parse_expr should succeed");
835 match &expr.value {
836 SurfaceExpr::Do(actions) => {
837 assert_eq!(actions.len(), 2);
838 assert!(matches!(actions[0], DoAction::Bind(_, _)));
839 }
840 other => panic!("Expected Do, got {:?}", other),
841 }
842 }
843 #[test]
844 fn test_parse_structure_with_default() {
845 let decl = parse_decl_from_str("structure Config where verbose : Nat := 0")
846 .expect("parse_decl should succeed");
847 match &decl.value {
848 Decl::Structure { name, fields, .. } => {
849 assert_eq!(name, "Config");
850 assert_eq!(fields.len(), 1);
851 assert!(fields[0].default.is_some());
852 }
853 other => panic!("Expected Structure, got {:?}", other),
854 }
855 }
856 #[test]
857 fn test_parse_anonymous_ctor_single() {
858 let expr = parse_expr_from_str("⟨42⟩").expect("parse_expr should succeed");
859 match &expr.value {
860 SurfaceExpr::AnonymousCtor(elems) => {
861 assert_eq!(elems.len(), 1);
862 }
863 other => panic!("Expected AnonymousCtor, got {:?}", other),
864 }
865 }
866 #[test]
867 fn test_parse_anonymous_ctor_pair() {
868 let expr = parse_expr_from_str("⟨1, 2⟩").expect("parse_expr should succeed");
869 match &expr.value {
870 SurfaceExpr::AnonymousCtor(elems) => {
871 assert_eq!(elems.len(), 2);
872 }
873 other => panic!("Expected AnonymousCtor, got {:?}", other),
874 }
875 }
876 #[test]
877 fn test_parse_anonymous_ctor_triple() {
878 let expr = parse_expr_from_str("⟨1, 2, 3⟩").expect("parse_expr should succeed");
879 match &expr.value {
880 SurfaceExpr::AnonymousCtor(elems) => {
881 assert_eq!(elems.len(), 3);
882 }
883 other => panic!("Expected AnonymousCtor, got {:?}", other),
884 }
885 }
886 #[test]
887 fn test_parse_anonymous_ctor_nested() {
888 let expr = parse_expr_from_str("⟨⟨1, 2⟩, 3⟩").expect("parse_expr should succeed");
889 match &expr.value {
890 SurfaceExpr::AnonymousCtor(elems) => {
891 assert_eq!(elems.len(), 2);
892 assert!(matches!(elems[0].value, SurfaceExpr::AnonymousCtor(_)));
893 }
894 other => panic!("Expected AnonymousCtor, got {:?}", other),
895 }
896 }
897 #[test]
898 fn test_parse_anonymous_ctor_empty() {
899 let expr = parse_expr_from_str("⟨⟩").expect("parse_expr should succeed");
900 match &expr.value {
901 SurfaceExpr::AnonymousCtor(elems) => {
902 assert!(elems.is_empty());
903 }
904 other => panic!("Expected empty AnonymousCtor, got {:?}", other),
905 }
906 }
907 #[test]
908 fn test_parse_named_arg_single() {
909 let expr = parse_expr_from_str("f (x := 1)").expect("parse_expr should succeed");
910 match &expr.value {
911 SurfaceExpr::App(_, arg) => {
912 assert!(matches!(arg.value, SurfaceExpr::NamedArg(_, _, _)));
913 }
914 other => panic!("Expected App with NamedArg, got {:?}", other),
915 }
916 }
917 #[test]
918 fn test_parse_named_arg_extraction() {
919 let expr = parse_expr_from_str("f (x := 1)").expect("parse_expr should succeed");
920 match &expr.value {
921 SurfaceExpr::App(_, arg) => match &arg.value {
922 SurfaceExpr::NamedArg(_, name, val) => {
923 assert_eq!(name, "x");
924 assert_eq!(val.value, SurfaceExpr::Lit(Literal::Nat(1)));
925 }
926 other => panic!("Expected NamedArg, got {:?}", other),
927 },
928 other => panic!("Expected App, got {:?}", other),
929 }
930 }
931 #[test]
932 fn test_parse_named_arg_complex_value() {
933 let expr = parse_expr_from_str("f (name := x + y)").expect("parse_expr should succeed");
934 match &expr.value {
935 SurfaceExpr::App(_, arg) => {
936 assert!(matches!(arg.value, SurfaceExpr::NamedArg(_, _, _)));
937 }
938 other => panic!("Expected App with NamedArg, got {:?}", other),
939 }
940 }
941 #[test]
942 fn test_parse_do_let_bind_mixed() {
943 let expr = parse_expr_from_str("do { let x := 1; y <- f x; y }")
944 .expect("parse_expr should succeed");
945 match &expr.value {
946 SurfaceExpr::Do(actions) => {
947 assert_eq!(actions.len(), 3);
948 assert!(matches!(actions[0], DoAction::Let(_, _)));
949 assert!(matches!(actions[1], DoAction::Bind(_, _)));
950 assert!(matches!(actions[2], DoAction::Expr(_)));
951 }
952 other => panic!("Expected Do, got {:?}", other),
953 }
954 }
955 #[test]
956 fn test_parse_do_action_expr() {
957 let expr = parse_expr_from_str("do { x; y; z }").expect("parse_expr should succeed");
958 match &expr.value {
959 SurfaceExpr::Do(actions) => {
960 assert_eq!(actions.len(), 3);
961 for action in actions {
962 assert!(matches!(action, DoAction::Expr(_)));
963 }
964 }
965 other => panic!("Expected Do, got {:?}", other),
966 }
967 }
968 #[test]
969 fn test_parse_do_bind_simple() {
970 let expr = parse_expr_from_str("do { x <- getLine; putLine x }")
971 .expect("parse_expr should succeed");
972 match &expr.value {
973 SurfaceExpr::Do(actions) => {
974 assert_eq!(actions.len(), 2);
975 match &actions[0] {
976 DoAction::Bind(name, _) => {
977 assert_eq!(name, "x");
978 }
979 other => panic!("Expected Bind, got {:?}", other),
980 }
981 }
982 other => panic!("Expected Do, got {:?}", other),
983 }
984 }
985 #[test]
986 fn test_parse_have_simple() {
987 let expr =
988 parse_expr_from_str("have h : True := trivial; h").expect("parse_expr should succeed");
989 match &expr.value {
990 SurfaceExpr::Have(name, ty, proof, body) => {
991 assert_eq!(name, "h");
992 let _ = (ty, proof, body);
993 }
994 other => panic!("Expected Have, got {:?}", other),
995 }
996 }
997 #[test]
998 fn test_parse_have_body_chain() {
999 let expr = parse_expr_from_str("have h1 : True := trivial; have h2 : True := h1; h2")
1000 .expect("parse_expr should succeed");
1001 match &expr.value {
1002 SurfaceExpr::Have(_, _, _, body) => {
1003 assert!(matches!(body.value, SurfaceExpr::Have(_, _, _, _)));
1004 }
1005 other => panic!("Expected nested Have, got {:?}", other),
1006 }
1007 }
1008 #[test]
1009 fn test_parse_suffices_with_tactic() {
1010 let expr =
1011 parse_expr_from_str("suffices h : Nat by simp").expect("parse_expr should succeed");
1012 match &expr.value {
1013 SurfaceExpr::Suffices(name, ty, tactic) => {
1014 assert_eq!(name, "h");
1015 let _ = (ty, tactic);
1016 }
1017 other => panic!("Expected Suffices, got {:?}", other),
1018 }
1019 }
1020 #[test]
1021 fn test_parse_suffices_complex_type() {
1022 let expr = parse_expr_from_str("suffices h : forall x, x = x by simp")
1023 .expect("parse_expr should succeed");
1024 match &expr.value {
1025 SurfaceExpr::Suffices(name, _, _) => {
1026 assert_eq!(name, "h");
1027 }
1028 other => panic!("Expected Suffices, got {:?}", other),
1029 }
1030 }
1031 #[test]
1032 fn test_parse_show_simple() {
1033 let expr = parse_expr_from_str("show Nat from 42").expect("parse_expr should succeed");
1034 match &expr.value {
1035 SurfaceExpr::Show(ty, proof) => {
1036 let _ = (ty, proof);
1037 }
1038 other => panic!("Expected Show, got {:?}", other),
1039 }
1040 }
1041 #[test]
1042 fn test_parse_show_complex_type() {
1043 let expr = parse_expr_from_str("show (forall x, x = x) from (fun x -> rfl)")
1044 .expect("parse_expr should succeed");
1045 match &expr.value {
1046 SurfaceExpr::Show(_, _) => {}
1047 other => panic!("Expected Show, got {:?}", other),
1048 }
1049 }
1050 #[test]
1051 fn test_parse_show_nested() {
1052 let expr = parse_expr_from_str("show Nat from (show Nat from 0)")
1053 .expect("parse_expr should succeed");
1054 match &expr.value {
1055 SurfaceExpr::Show(_, proof) => {
1056 assert!(matches!(proof.value, SurfaceExpr::Show(_, _)));
1057 }
1058 other => panic!("Expected nested Show, got {:?}", other),
1059 }
1060 }
1061 #[test]
1062 fn test_parse_list_nested() {
1063 let expr = parse_expr_from_str("[[1, 2], [3, 4]]").expect("parse_expr should succeed");
1064 match &expr.value {
1065 SurfaceExpr::ListLit(elems) => {
1066 assert_eq!(elems.len(), 2);
1067 for elem in elems {
1068 assert!(matches!(elem.value, SurfaceExpr::ListLit(_)));
1069 }
1070 }
1071 other => panic!("Expected nested ListLit, got {:?}", other),
1072 }
1073 }
1074 #[test]
1075 fn test_parse_list_mixed_types() {
1076 let expr = parse_expr_from_str("[1, x, y + z]").expect("parse_expr should succeed");
1077 match &expr.value {
1078 SurfaceExpr::ListLit(elems) => {
1079 assert_eq!(elems.len(), 3);
1080 }
1081 other => panic!("Expected ListLit, got {:?}", other),
1082 }
1083 }
1084 #[test]
1085 fn test_parse_tuple_single() {
1086 let expr = parse_expr_from_str("(1, 1)").expect("parse_expr should succeed");
1087 match &expr.value {
1088 SurfaceExpr::Tuple(elems) => {
1089 assert_eq!(elems.len(), 2);
1090 }
1091 other => panic!("Expected Tuple with 2 elements, got {:?}", other),
1092 }
1093 }
1094 #[test]
1095 fn test_parse_tuple_nested() {
1096 let expr = parse_expr_from_str("((1, 2), (3, 4))").expect("parse_expr should succeed");
1097 match &expr.value {
1098 SurfaceExpr::Tuple(elems) => {
1099 assert_eq!(elems.len(), 2);
1100 for elem in elems {
1101 assert!(matches!(elem.value, SurfaceExpr::Tuple(_)));
1102 }
1103 }
1104 other => panic!("Expected nested Tuple, got {:?}", other),
1105 }
1106 }
1107 #[test]
1108 fn test_parse_tuple_large() {
1109 let expr = parse_expr_from_str("(1, 2, 3, 4, 5)").expect("parse_expr should succeed");
1110 match &expr.value {
1111 SurfaceExpr::Tuple(elems) => {
1112 assert_eq!(elems.len(), 5);
1113 }
1114 other => panic!("Expected Tuple with 5 elements, got {:?}", other),
1115 }
1116 }
1117 #[test]
1118 fn test_parse_proj_multi_level() {
1119 let expr = parse_expr_from_str("x.a.b.c").expect("parse_expr should succeed");
1120 match &expr.value {
1121 SurfaceExpr::Proj(inner, field) => {
1122 assert_eq!(field, "c");
1123 assert!(matches!(inner.value, SurfaceExpr::Proj(_, _)));
1124 }
1125 other => panic!("Expected Proj, got {:?}", other),
1126 }
1127 }
1128 #[test]
1129 fn test_parse_proj_on_app() {
1130 let expr = parse_expr_from_str("(f x).field").expect("parse_expr should succeed");
1131 match &expr.value {
1132 SurfaceExpr::Proj(inner, field) => {
1133 assert_eq!(field, "field");
1134 assert!(matches!(inner.value, SurfaceExpr::App(_, _)));
1135 }
1136 other => panic!("Expected Proj, got {:?}", other),
1137 }
1138 }
1139 #[test]
1140 fn test_parse_proj_on_tuple() {
1141 let expr = parse_expr_from_str("(1, 2, 3).foo").expect("parse_expr should succeed");
1142 match &expr.value {
1143 SurfaceExpr::Proj(inner, field) => {
1144 assert_eq!(field, "foo");
1145 assert!(matches!(inner.value, SurfaceExpr::Tuple(_)));
1146 }
1147 other => panic!("Expected Proj on Tuple, got {:?}", other),
1148 }
1149 }
1150 #[test]
1151 fn test_parse_mixed_precedence() {
1152 let expr = parse_expr_from_str("a + b * c - d").expect("parse_expr should succeed");
1153 assert!(matches!(expr.value, SurfaceExpr::App(_, _)));
1154 }
1155 #[test]
1156 fn test_parse_comparison_chain() {
1157 let expr = parse_expr_from_str("a < b").expect("parse_expr should succeed");
1158 match &expr.value {
1159 SurfaceExpr::App(lhs, _) => {
1160 assert!(matches!(lhs.value, SurfaceExpr::App(_, _)));
1161 }
1162 other => panic!("Expected App, got {:?}", other),
1163 }
1164 }
1165 #[test]
1166 fn test_parse_iff_operator() {
1167 let expr = parse_expr_from_str("Iff a b").expect("parse_expr should succeed");
1168 match &expr.value {
1169 SurfaceExpr::App(lhs, _) => match &lhs.value {
1170 SurfaceExpr::App(_, _) => {}
1171 other => panic!("Expected App, got {:?}", other),
1172 },
1173 other => panic!("Expected App, got {:?}", other),
1174 }
1175 }
1176 #[test]
1177 fn test_parse_logical_and() {
1178 let expr = parse_expr_from_str("a && b").expect("parse_expr should succeed");
1179 match &expr.value {
1180 SurfaceExpr::App(lhs, _) => match &lhs.value {
1181 SurfaceExpr::App(op, _) => {
1182 assert!(matches!(& op.value, SurfaceExpr::Var(n) if n == "&&"));
1183 }
1184 other => panic!("Expected App(&&, ...), got {:?}", other),
1185 },
1186 other => panic!("Expected App, got {:?}", other),
1187 }
1188 }
1189 #[test]
1190 fn test_parse_ann_in_app() {
1191 let expr = parse_expr_from_str("f (x : Nat)").expect("parse_expr should succeed");
1192 match &expr.value {
1193 SurfaceExpr::App(_, arg) => {
1194 assert!(matches!(arg.value, SurfaceExpr::Ann(_, _)));
1195 }
1196 other => panic!("Expected App with Ann, got {:?}", other),
1197 }
1198 }
1199 #[test]
1200 fn test_parse_ann_complex_type() {
1201 let expr =
1202 parse_expr_from_str("(x : forall a, a -> a)").expect("parse_expr should succeed");
1203 assert!(matches!(expr.value, SurfaceExpr::Ann(_, _)));
1204 }
1205 #[test]
1206 fn test_parse_if_associativity() {
1207 let expr = parse_expr_from_str("if a then if b then c else d else e")
1208 .expect("parse_expr should succeed");
1209 match &expr.value {
1210 SurfaceExpr::If(_, then_branch, _) => {
1211 assert!(matches!(then_branch.value, SurfaceExpr::If(_, _, _)));
1212 }
1213 other => panic!("Expected If with nested If in then branch, got {:?}", other),
1214 }
1215 }
1216 #[test]
1217 fn test_parse_if_complex_condition() {
1218 let expr =
1219 parse_expr_from_str("if x && y || z then a else b").expect("parse_expr should succeed");
1220 assert!(matches!(expr.value, SurfaceExpr::If(_, _, _)));
1221 }
1222 #[test]
1223 fn test_parse_match_multiple_arms() {
1224 let expr = parse_expr_from_str("match x with | 0 -> a | 1 -> b | _ -> c")
1225 .expect("parse_expr should succeed");
1226 match &expr.value {
1227 SurfaceExpr::Match(_, arms) => {
1228 assert_eq!(arms.len(), 3);
1229 }
1230 other => panic!("Expected Match with 3 arms, got {:?}", other),
1231 }
1232 }
1233 #[test]
1234 fn test_parse_match_constructor_patterns() {
1235 let expr = parse_expr_from_str("match x with | nil -> a | cons h t -> h")
1236 .expect("parse_expr should succeed");
1237 match &expr.value {
1238 SurfaceExpr::Match(_, arms) => {
1239 assert_eq!(arms.len(), 2);
1240 assert!(matches!(arms[0].pattern.value, Pattern::Var(_)));
1241 assert!(matches!(arms[1].pattern.value, Pattern::Ctor(_, _)));
1242 }
1243 other => panic!("Expected Match, got {:?}", other),
1244 }
1245 }
1246 #[test]
1247 fn test_parse_match_with_literals() {
1248 let expr = parse_expr_from_str("match x with | \"hello\" -> a | \"world\" -> b")
1249 .expect("parse_expr should succeed");
1250 match &expr.value {
1251 SurfaceExpr::Match(_, arms) => {
1252 assert_eq!(arms.len(), 2);
1253 }
1254 other => panic!("Expected Match, got {:?}", other),
1255 }
1256 }
1257 #[test]
1258 fn test_parse_let_chain() {
1259 let expr = parse_expr_from_str("let x := 1 in let y := 2 in x + y")
1260 .expect("parse_expr should succeed");
1261 match &expr.value {
1262 SurfaceExpr::Let(_, _, _, body) => {
1263 assert!(matches!(body.value, SurfaceExpr::Let(_, _, _, _)));
1264 }
1265 other => panic!("Expected chained Let, got {:?}", other),
1266 }
1267 }
1268 #[test]
1269 fn test_parse_let_no_type() {
1270 let expr = parse_expr_from_str("let x := 42 in x").expect("parse_expr should succeed");
1271 match &expr.value {
1272 SurfaceExpr::Let(_, ty, _, _) => {
1273 assert!(ty.is_none());
1274 }
1275 other => panic!("Expected Let, got {:?}", other),
1276 }
1277 }
1278 #[test]
1279 fn test_parse_let_with_app() {
1280 let expr = parse_expr_from_str("let x := f 1 2 in x").expect("parse_expr should succeed");
1281 match &expr.value {
1282 SurfaceExpr::Let(_, _, val, _) => {
1283 assert!(matches!(val.value, SurfaceExpr::App(_, _)));
1284 }
1285 other => panic!("Expected Let, got {:?}", other),
1286 }
1287 }
1288 #[test]
1289 fn test_parse_lambda_multi_arg() {
1290 let expr = parse_expr_from_str("fun (x : Nat) (y : Nat) -> x + y")
1291 .expect("parse_expr should succeed");
1292 match &expr.value {
1293 SurfaceExpr::Lam(binders, _) => {
1294 assert_eq!(binders.len(), 2);
1295 }
1296 other => panic!("Expected Lam with 2 binders, got {:?}", other),
1297 }
1298 }
1299 #[test]
1300 fn test_parse_lambda_no_type() {
1301 let expr = parse_expr_from_str("fun x -> x").expect("parse_expr should succeed");
1302 match &expr.value {
1303 SurfaceExpr::Lam(binders, _) => {
1304 assert_eq!(binders.len(), 1);
1305 assert!(binders[0].ty.is_none());
1306 }
1307 other => panic!("Expected Lam, got {:?}", other),
1308 }
1309 }
1310 #[test]
1311 fn test_parse_lambda_mixed_binders() {
1312 let expr = parse_expr_from_str("fun (x : Nat) {y} [z : Monad] -> x")
1313 .expect("parse_expr should succeed");
1314 match &expr.value {
1315 SurfaceExpr::Lam(binders, _) => {
1316 assert_eq!(binders.len(), 3);
1317 assert_eq!(binders[0].info, BinderKind::Default);
1318 assert_eq!(binders[1].info, BinderKind::Implicit);
1319 assert_eq!(binders[2].info, BinderKind::Instance);
1320 }
1321 other => panic!("Expected Lam with mixed binders, got {:?}", other),
1322 }
1323 }
1324 #[test]
1325 fn test_parse_pi_multi_arg() {
1326 let expr = parse_expr_from_str("forall (x : Nat) (y : Nat), x = y")
1327 .expect("parse_expr should succeed");
1328 match &expr.value {
1329 SurfaceExpr::Pi(binders, _) => {
1330 assert_eq!(binders.len(), 2);
1331 }
1332 other => panic!("Expected Pi with 2 binders, got {:?}", other),
1333 }
1334 }
1335 #[test]
1336 fn test_parse_pi_implicit() {
1337 let expr =
1338 parse_expr_from_str("forall {x : Nat}, x = x").expect("parse_expr should succeed");
1339 match &expr.value {
1340 SurfaceExpr::Pi(binders, _) => {
1341 assert_eq!(binders[0].info, BinderKind::Implicit);
1342 }
1343 other => panic!("Expected Pi with implicit, got {:?}", other),
1344 }
1345 }
1346 #[test]
1347 fn test_parse_def_with_univ_params() {
1348 let decl =
1349 parse_decl_from_str("def id {u} : Type := Type").expect("parse_decl should succeed");
1350 match &decl.value {
1351 Decl::Definition {
1352 name, univ_params, ..
1353 } => {
1354 assert_eq!(name, "id");
1355 assert_eq!(univ_params, &["u"]);
1356 }
1357 other => panic!("Expected Definition, got {:?}", other),
1358 }
1359 }
1360 #[test]
1361 fn test_parse_theorem_with_type() {
1362 let decl =
1363 parse_decl_from_str("theorem identity : Nat := 42").expect("parse_decl should succeed");
1364 match &decl.value {
1365 Decl::Theorem { name, ty, .. } => {
1366 assert_eq!(name, "identity");
1367 let _ = ty;
1368 }
1369 other => panic!("Expected Theorem, got {:?}", other),
1370 }
1371 }
1372 #[test]
1373 fn test_parse_inductive_multi_ctor() {
1374 let decl =
1375 parse_decl_from_str("inductive List : Type | nil : Type | cons : Nat → List → List")
1376 .expect("test operation should succeed");
1377 match &decl.value {
1378 Decl::Inductive { name, ctors, .. } => {
1379 assert_eq!(name, "List");
1380 assert_eq!(ctors.len(), 2);
1381 }
1382 other => panic!("Expected Inductive, got {:?}", other),
1383 }
1384 }
1385 #[test]
1386 fn test_parse_class_with_extends() {
1387 let decl = parse_decl_from_str("class Functor extends Inhabited where map : Nat")
1388 .expect("parse_decl should succeed");
1389 match &decl.value {
1390 Decl::ClassDecl { name, extends, .. } => {
1391 assert_eq!(name, "Functor");
1392 assert!(extends.contains(&"Inhabited".to_string()));
1393 }
1394 other => panic!("Expected ClassDecl, got {:?}", other),
1395 }
1396 }
1397 #[test]
1398 fn test_parse_instance_with_methods() {
1399 let decl = parse_decl_from_str("instance : Monoid Nat where op := Nat")
1400 .expect("parse_decl should succeed");
1401 match &decl.value {
1402 Decl::InstanceDecl { defs, .. } => {
1403 assert_eq!(defs.len(), 1);
1404 assert_eq!(defs[0].0, "op");
1405 }
1406 other => panic!("Expected InstanceDecl, got {:?}", other),
1407 }
1408 }
1409 #[test]
1410 fn test_parse_deeply_nested_expr() {
1411 let expr = parse_expr_from_str("(((((x)))))").expect("parse_expr should succeed");
1412 assert!(matches!(expr.value, SurfaceExpr::Var(_)));
1413 }
1414 #[test]
1415 fn test_parse_deeply_nested_app() {
1416 let expr = parse_expr_from_str("f (g (h (i (j x))))").expect("parse_expr should succeed");
1417 assert!(matches!(expr.value, SurfaceExpr::App(_, _)));
1418 }
1419 #[test]
1420 fn test_parse_complex_mixed_expr() {
1421 let expr =
1422 parse_expr_from_str("let x := 1 in match x with | 0 -> if y then z else w | n -> n")
1423 .expect("test operation should succeed");
1424 assert!(matches!(expr.value, SurfaceExpr::Let(_, _, _, _)));
1425 }
1426 #[test]
1427 fn test_parse_annotation_in_lambda() {
1428 let expr =
1429 parse_expr_from_str("fun (x : Nat) -> (x : Nat)").expect("parse_expr should succeed");
1430 match &expr.value {
1431 SurfaceExpr::Lam(_, body) => {
1432 assert!(matches!(body.value, SurfaceExpr::Ann(_, _)));
1433 }
1434 other => panic!("Expected Lam, got {:?}", other),
1435 }
1436 }
1437 #[test]
1438 fn test_parse_app_with_annotation() {
1439 let expr =
1440 parse_expr_from_str("f (x : Nat) (y : String)").expect("parse_expr should succeed");
1441 match &expr.value {
1442 SurfaceExpr::App(_, _) => {}
1443 other => panic!("Expected App, got {:?}", other),
1444 }
1445 }
1446 #[test]
1447 fn test_parse_single_char_ident() {
1448 let expr = parse_expr_from_str("x").expect("parse_expr should succeed");
1449 match &expr.value {
1450 SurfaceExpr::Var(name) => {
1451 assert_eq!(name, "x");
1452 }
1453 other => panic!("Expected Var, got {:?}", other),
1454 }
1455 }
1456 #[test]
1457 fn test_parse_long_ident() {
1458 let expr = parse_expr_from_str("veryLongIdentifierNameWithManyWords")
1459 .expect("parse_expr should succeed");
1460 match &expr.value {
1461 SurfaceExpr::Var(name) => {
1462 assert_eq!(name, "veryLongIdentifierNameWithManyWords");
1463 }
1464 other => panic!("Expected Var, got {:?}", other),
1465 }
1466 }
1467 #[test]
1468 fn test_parse_large_nat() {
1469 let expr = parse_expr_from_str("999999999999").expect("parse_expr should succeed");
1470 match &expr.value {
1471 SurfaceExpr::Lit(Literal::Nat(n)) => {
1472 assert_eq!(*n, 999999999999);
1473 }
1474 other => panic!("Expected Nat literal, got {:?}", other),
1475 }
1476 }
1477 #[test]
1478 fn test_parse_binder_underscore() {
1479 let expr = parse_expr_from_str("fun (_ : Nat) -> 42").expect("parse_expr should succeed");
1480 match &expr.value {
1481 SurfaceExpr::Lam(binders, _) => {
1482 assert_eq!(binders[0].name, "_");
1483 }
1484 other => panic!("Expected Lam, got {:?}", other),
1485 }
1486 }
1487 #[test]
1488 fn test_parse_multiple_projections() {
1489 let expr = parse_expr_from_str("x.a.b.c.d.e").expect("parse_expr should succeed");
1490 let mut depth = 0;
1491 let mut current = &expr.value;
1492 while let SurfaceExpr::Proj(inner, _) = current {
1493 depth += 1;
1494 current = &inner.value;
1495 }
1496 assert_eq!(depth, 5);
1497 }
1498}