1#[cfg(test)]
6mod tests {
7 use super::*;
8 use crate::ast_impl::BinderKind;
9 use crate::command::*;
10 use crate::tokens::{Span, Token, TokenKind};
11 fn make_token(kind: TokenKind) -> Token {
12 Token {
13 kind,
14 span: Span::new(0, 0, 1, 1),
15 }
16 }
17 fn make_ident(s: &str) -> Token {
18 make_token(TokenKind::Ident(s.to_string()))
19 }
20 fn make_eof() -> Token {
21 make_token(TokenKind::Eof)
22 }
23 #[test]
24 fn test_parser_create() {
25 let parser = CommandParser::new();
26 assert_eq!(parser.position(), 0);
27 }
28 #[test]
29 fn test_is_command_keyword() {
30 assert!(CommandParser::is_command_keyword(&TokenKind::Axiom));
31 assert!(CommandParser::is_command_keyword(&TokenKind::Definition));
32 assert!(CommandParser::is_command_keyword(&TokenKind::Theorem));
33 assert!(CommandParser::is_command_keyword(&TokenKind::Inductive));
34 assert!(CommandParser::is_command_keyword(&TokenKind::Structure));
35 assert!(CommandParser::is_command_keyword(&TokenKind::Class));
36 assert!(CommandParser::is_command_keyword(&TokenKind::Instance));
37 assert!(CommandParser::is_command_keyword(&TokenKind::Namespace));
38 assert!(CommandParser::is_command_keyword(&TokenKind::Section));
39 assert!(CommandParser::is_command_keyword(&TokenKind::Variable));
40 assert!(CommandParser::is_command_keyword(&TokenKind::Variables));
41 assert!(CommandParser::is_command_keyword(&TokenKind::End));
42 assert!(CommandParser::is_command_keyword(&TokenKind::Import));
43 assert!(CommandParser::is_command_keyword(&TokenKind::Export));
44 assert!(CommandParser::is_command_keyword(&TokenKind::Open));
45 assert!(CommandParser::is_command_keyword(&TokenKind::Attribute));
46 assert!(CommandParser::is_command_keyword(&TokenKind::Hash));
47 assert!(CommandParser::is_command_keyword(&TokenKind::Ident(
48 "set_option".to_string()
49 )));
50 assert!(CommandParser::is_command_keyword(&TokenKind::Ident(
51 "universe".to_string()
52 )));
53 assert!(CommandParser::is_command_keyword(&TokenKind::Ident(
54 "notation".to_string()
55 )));
56 assert!(CommandParser::is_command_keyword(&TokenKind::Ident(
57 "derive".to_string()
58 )));
59 assert!(!CommandParser::is_command_keyword(&TokenKind::LParen));
60 assert!(!CommandParser::is_command_keyword(&TokenKind::Ident(
61 "foo".to_string()
62 )));
63 }
64 #[test]
65 fn test_parser_reset() {
66 let mut parser = CommandParser::new();
67 parser.pos = 10;
68 parser.reset();
69 assert_eq!(parser.position(), 0);
70 }
71 #[test]
72 fn test_parse_import() {
73 let tokens = vec![
74 make_token(TokenKind::Import),
75 make_ident("Mathlib"),
76 make_eof(),
77 ];
78 let mut parser = CommandParser::new();
79 let cmd = parser
80 .parse_command(&tokens)
81 .expect("parse_decl should succeed");
82 match cmd {
83 Command::Import { module, .. } => assert_eq!(module, "Mathlib"),
84 _ => panic!("expected Import command"),
85 }
86 }
87 #[test]
88 fn test_parse_import_dotted() {
89 let tokens = vec![
90 make_token(TokenKind::Import),
91 make_ident("Mathlib"),
92 make_token(TokenKind::Dot),
93 make_ident("Data"),
94 make_token(TokenKind::Dot),
95 make_ident("Nat"),
96 make_eof(),
97 ];
98 let mut parser = CommandParser::new();
99 let cmd = parser
100 .parse_command(&tokens)
101 .expect("parse_decl should succeed");
102 match cmd {
103 Command::Import { module, .. } => assert_eq!(module, "Mathlib.Data.Nat"),
104 _ => panic!("expected Import command"),
105 }
106 }
107 #[test]
108 fn test_parse_export() {
109 let tokens = vec![
110 make_token(TokenKind::Export),
111 make_ident("foo"),
112 make_ident("bar"),
113 make_eof(),
114 ];
115 let mut parser = CommandParser::new();
116 let cmd = parser
117 .parse_command(&tokens)
118 .expect("parse_decl should succeed");
119 match cmd {
120 Command::Export { names, .. } => {
121 assert_eq!(names, vec!["foo".to_string(), "bar".to_string()]);
122 }
123 _ => panic!("expected Export command"),
124 }
125 }
126 #[test]
127 fn test_parse_namespace() {
128 let tokens = vec![
129 make_token(TokenKind::Namespace),
130 make_ident("MyNamespace"),
131 make_eof(),
132 ];
133 let mut parser = CommandParser::new();
134 let cmd = parser
135 .parse_command(&tokens)
136 .expect("parse_decl should succeed");
137 match cmd {
138 Command::Namespace { name, .. } => assert_eq!(name, "MyNamespace"),
139 _ => panic!("expected Namespace command"),
140 }
141 }
142 #[test]
143 fn test_parse_end() {
144 let tokens = vec![make_token(TokenKind::End), make_eof()];
145 let mut parser = CommandParser::new();
146 let cmd = parser
147 .parse_command(&tokens)
148 .expect("parse_decl should succeed");
149 assert!(matches!(cmd, Command::End { .. }));
150 }
151 #[test]
152 fn test_parse_open_all() {
153 let tokens = vec![make_token(TokenKind::Open), make_ident("Nat"), make_eof()];
154 let mut parser = CommandParser::new();
155 let cmd = parser
156 .parse_command(&tokens)
157 .expect("parse_decl should succeed");
158 match cmd {
159 Command::Open { path, items, .. } => {
160 assert_eq!(path, vec!["Nat".to_string()]);
161 assert_eq!(items.len(), 1);
162 assert!(matches!(items[0], OpenItem::All));
163 }
164 _ => panic!("expected Open command"),
165 }
166 }
167 #[test]
168 fn test_parse_open_only() {
169 let tokens = vec![
170 make_token(TokenKind::Open),
171 make_ident("Nat"),
172 make_ident("only"),
173 make_token(TokenKind::LBracket),
174 make_ident("add"),
175 make_token(TokenKind::Comma),
176 make_ident("mul"),
177 make_token(TokenKind::RBracket),
178 make_eof(),
179 ];
180 let mut parser = CommandParser::new();
181 let cmd = parser
182 .parse_command(&tokens)
183 .expect("parse_decl should succeed");
184 match cmd {
185 Command::Open { path, items, .. } => {
186 assert_eq!(path, vec!["Nat".to_string()]);
187 match &items[0] {
188 OpenItem::Only(names) => {
189 assert_eq!(names, &["add".to_string(), "mul".to_string()]);
190 }
191 _ => panic!("expected Only"),
192 }
193 }
194 _ => panic!("expected Open command"),
195 }
196 }
197 #[test]
198 fn test_parse_open_hiding() {
199 let tokens = vec![
200 make_token(TokenKind::Open),
201 make_ident("Nat"),
202 make_ident("hiding"),
203 make_token(TokenKind::LBracket),
204 make_ident("sub"),
205 make_token(TokenKind::RBracket),
206 make_eof(),
207 ];
208 let mut parser = CommandParser::new();
209 let cmd = parser
210 .parse_command(&tokens)
211 .expect("parse_decl should succeed");
212 match cmd {
213 Command::Open { items, .. } => {
214 assert!(
215 matches!(& items[0], OpenItem::Hiding(names) if names == & ["sub"
216 .to_string()])
217 );
218 }
219 _ => panic!("expected Open command"),
220 }
221 }
222 #[test]
223 fn test_parse_open_renaming() {
224 let tokens = vec![
225 make_token(TokenKind::Open),
226 make_ident("Nat"),
227 make_ident("renaming"),
228 make_ident("add"),
229 make_token(TokenKind::Arrow),
230 make_ident("plus"),
231 make_eof(),
232 ];
233 let mut parser = CommandParser::new();
234 let cmd = parser
235 .parse_command(&tokens)
236 .expect("parse_decl should succeed");
237 match cmd {
238 Command::Open { items, .. } => {
239 assert!(
240 matches!(& items[0], OpenItem::Renaming(old, new) if old == "add" &&
241 new == "plus")
242 );
243 }
244 _ => panic!("expected Open command"),
245 }
246 }
247 #[test]
248 fn test_parse_section() {
249 let tokens = vec![
250 make_token(TokenKind::Section),
251 make_ident("MySection"),
252 make_eof(),
253 ];
254 let mut parser = CommandParser::new();
255 let cmd = parser
256 .parse_command(&tokens)
257 .expect("parse_decl should succeed");
258 match cmd {
259 Command::Section { name, .. } => assert_eq!(name, "MySection"),
260 _ => panic!("expected Section command"),
261 }
262 }
263 #[test]
264 fn test_parse_variable_explicit() {
265 let tokens = vec![
266 make_token(TokenKind::Variable),
267 make_token(TokenKind::LParen),
268 make_ident("x"),
269 make_token(TokenKind::Colon),
270 make_ident("Nat"),
271 make_token(TokenKind::RParen),
272 make_eof(),
273 ];
274 let mut parser = CommandParser::new();
275 let cmd = parser
276 .parse_command(&tokens)
277 .expect("parse_decl should succeed");
278 match cmd {
279 Command::Variable { binders, .. } => {
280 assert_eq!(binders.len(), 1);
281 assert_eq!(binders[0].name, "x");
282 assert_eq!(binders[0].info, BinderKind::Default);
283 }
284 _ => panic!("expected Variable command"),
285 }
286 }
287 #[test]
288 fn test_parse_variable_implicit() {
289 let tokens = vec![
290 make_token(TokenKind::Variable),
291 make_token(TokenKind::LBrace),
292 make_ident("a"),
293 make_token(TokenKind::Colon),
294 make_ident("Type"),
295 make_token(TokenKind::RBrace),
296 make_eof(),
297 ];
298 let mut parser = CommandParser::new();
299 let cmd = parser
300 .parse_command(&tokens)
301 .expect("parse_decl should succeed");
302 match cmd {
303 Command::Variable { binders, .. } => {
304 assert_eq!(binders.len(), 1);
305 assert_eq!(binders[0].name, "a");
306 assert_eq!(binders[0].info, BinderKind::Implicit);
307 }
308 _ => panic!("expected Variable command"),
309 }
310 }
311 #[test]
312 fn test_parse_variable_instance() {
313 let tokens = vec![
314 make_token(TokenKind::Variable),
315 make_token(TokenKind::LBracket),
316 make_ident("inst"),
317 make_token(TokenKind::Colon),
318 make_ident("Add"),
319 make_token(TokenKind::RBracket),
320 make_eof(),
321 ];
322 let mut parser = CommandParser::new();
323 let cmd = parser
324 .parse_command(&tokens)
325 .expect("parse_decl should succeed");
326 match cmd {
327 Command::Variable { binders, .. } => {
328 assert_eq!(binders.len(), 1);
329 assert_eq!(binders[0].name, "inst");
330 assert_eq!(binders[0].info, BinderKind::Instance);
331 }
332 _ => panic!("expected Variable command"),
333 }
334 }
335 #[test]
336 fn test_parse_variable_multiple() {
337 let tokens = vec![
338 make_token(TokenKind::Variable),
339 make_token(TokenKind::LParen),
340 make_ident("x"),
341 make_ident("y"),
342 make_token(TokenKind::Colon),
343 make_ident("Nat"),
344 make_token(TokenKind::RParen),
345 make_eof(),
346 ];
347 let mut parser = CommandParser::new();
348 let cmd = parser
349 .parse_command(&tokens)
350 .expect("parse_decl should succeed");
351 match cmd {
352 Command::Variable { binders, .. } => {
353 assert_eq!(binders.len(), 2);
354 assert_eq!(binders[0].name, "x");
355 assert_eq!(binders[1].name, "y");
356 }
357 _ => panic!("expected Variable command"),
358 }
359 }
360 #[test]
361 fn test_parse_attribute() {
362 let tokens = vec![
363 make_token(TokenKind::Attribute),
364 make_token(TokenKind::LBracket),
365 make_ident("simp"),
366 make_token(TokenKind::Comma),
367 make_ident("ext"),
368 make_token(TokenKind::RBracket),
369 make_ident("myLemma"),
370 make_eof(),
371 ];
372 let mut parser = CommandParser::new();
373 let cmd = parser
374 .parse_command(&tokens)
375 .expect("parse_decl should succeed");
376 match cmd {
377 Command::Attribute { attrs, name, .. } => {
378 assert_eq!(attrs, vec!["simp".to_string(), "ext".to_string()]);
379 assert_eq!(name, "myLemma");
380 }
381 _ => panic!("expected Attribute command"),
382 }
383 }
384 #[test]
385 fn test_parse_check() {
386 let tokens = vec![
387 make_token(TokenKind::Hash),
388 make_ident("check"),
389 make_ident("Nat"),
390 make_token(TokenKind::Dot),
391 make_ident("add"),
392 make_eof(),
393 ];
394 let mut parser = CommandParser::new();
395 let cmd = parser
396 .parse_command(&tokens)
397 .expect("parse_decl should succeed");
398 match cmd {
399 Command::Check { expr_str, .. } => {
400 assert_eq!(expr_str, "Nat . add");
401 }
402 _ => panic!("expected Check command"),
403 }
404 }
405 #[test]
406 fn test_parse_eval() {
407 let tokens = vec![
408 make_token(TokenKind::Hash),
409 make_ident("eval"),
410 make_token(TokenKind::Nat(42)),
411 make_eof(),
412 ];
413 let mut parser = CommandParser::new();
414 let cmd = parser
415 .parse_command(&tokens)
416 .expect("parse_decl should succeed");
417 match cmd {
418 Command::Eval { expr_str, .. } => {
419 assert_eq!(expr_str, "42");
420 }
421 _ => panic!("expected Eval command"),
422 }
423 }
424 #[test]
425 fn test_parse_print() {
426 let tokens = vec![
427 make_token(TokenKind::Hash),
428 make_ident("print"),
429 make_ident("Nat"),
430 make_eof(),
431 ];
432 let mut parser = CommandParser::new();
433 let cmd = parser
434 .parse_command(&tokens)
435 .expect("parse_decl should succeed");
436 match cmd {
437 Command::Print { name, .. } => {
438 assert_eq!(name, "Nat");
439 }
440 _ => panic!("expected Print command"),
441 }
442 }
443 #[test]
444 fn test_parse_set_option() {
445 let tokens = vec![
446 make_ident("set_option"),
447 make_ident("pp"),
448 make_token(TokenKind::Dot),
449 make_ident("all"),
450 make_ident("true"),
451 make_eof(),
452 ];
453 let mut parser = CommandParser::new();
454 let cmd = parser
455 .parse_command(&tokens)
456 .expect("parse_decl should succeed");
457 match cmd {
458 Command::SetOption { name, value, .. } => {
459 assert_eq!(name, "pp.all");
460 assert_eq!(value, "true");
461 }
462 _ => panic!("expected SetOption command"),
463 }
464 }
465 #[test]
466 fn test_parse_universe_single() {
467 let tokens = vec![make_ident("universe"), make_ident("u"), make_eof()];
468 let mut parser = CommandParser::new();
469 let cmd = parser
470 .parse_command(&tokens)
471 .expect("parse_decl should succeed");
472 match cmd {
473 Command::Universe { names, .. } => {
474 assert_eq!(names, vec!["u".to_string()]);
475 }
476 _ => panic!("expected Universe command"),
477 }
478 }
479 #[test]
480 fn test_parse_universe_multiple() {
481 let tokens = vec![
482 make_ident("universe"),
483 make_ident("u"),
484 make_ident("v"),
485 make_ident("w"),
486 make_eof(),
487 ];
488 let mut parser = CommandParser::new();
489 let cmd = parser
490 .parse_command(&tokens)
491 .expect("parse_decl should succeed");
492 match cmd {
493 Command::Universe { names, .. } => {
494 assert_eq!(
495 names,
496 vec!["u".to_string(), "v".to_string(), "w".to_string()]
497 );
498 }
499 _ => panic!("expected Universe command"),
500 }
501 }
502 #[test]
503 fn test_parse_notation_infix() {
504 let tokens = vec![
505 make_ident("infix"),
506 make_token(TokenKind::Nat(65)),
507 make_token(TokenKind::String("+".to_string())),
508 make_token(TokenKind::Assign),
509 make_ident("HAdd"),
510 make_token(TokenKind::Dot),
511 make_ident("hAdd"),
512 make_eof(),
513 ];
514 let mut parser = CommandParser::new();
515 let cmd = parser
516 .parse_command(&tokens)
517 .expect("parse_decl should succeed");
518 match cmd {
519 Command::Notation {
520 kind,
521 name,
522 prec,
523 body,
524 ..
525 } => {
526 assert_eq!(kind, NotationKind::Infix);
527 assert_eq!(name, "+");
528 assert_eq!(prec, Some(65));
529 assert!(body.contains("HAdd"));
530 }
531 _ => panic!("expected Notation command"),
532 }
533 }
534 #[test]
535 fn test_parse_notation_prefix() {
536 let tokens = vec![
537 make_ident("prefix"),
538 make_token(TokenKind::Nat(100)),
539 make_token(TokenKind::String("-".to_string())),
540 make_token(TokenKind::Assign),
541 make_ident("Neg"),
542 make_token(TokenKind::Dot),
543 make_ident("neg"),
544 make_eof(),
545 ];
546 let mut parser = CommandParser::new();
547 let cmd = parser
548 .parse_command(&tokens)
549 .expect("parse_decl should succeed");
550 match cmd {
551 Command::Notation { kind, prec, .. } => {
552 assert_eq!(kind, NotationKind::Prefix);
553 assert_eq!(prec, Some(100));
554 }
555 _ => panic!("expected Notation command"),
556 }
557 }
558 #[test]
559 fn test_parse_derive() {
560 let tokens = vec![
561 make_ident("derive"),
562 make_ident("DecidableEq"),
563 make_token(TokenKind::Comma),
564 make_ident("Repr"),
565 make_ident("for"),
566 make_ident("MyType"),
567 make_eof(),
568 ];
569 let mut parser = CommandParser::new();
570 let cmd = parser
571 .parse_command(&tokens)
572 .expect("parse_decl should succeed");
573 match cmd {
574 Command::Derive {
575 strategies,
576 type_name,
577 ..
578 } => {
579 assert_eq!(
580 strategies,
581 vec!["DecidableEq".to_string(), "Repr".to_string()]
582 );
583 assert_eq!(type_name, "MyType");
584 }
585 _ => panic!("expected Derive command"),
586 }
587 }
588 #[test]
589 fn test_parse_empty_tokens() {
590 let tokens: Vec<Token> = vec![];
591 let mut parser = CommandParser::new();
592 assert!(parser.parse_command(&tokens).is_err());
593 }
594 #[test]
595 fn test_parse_unknown_command() {
596 let tokens = vec![make_ident("foobar"), make_eof()];
597 let mut parser = CommandParser::new();
598 assert!(parser.parse_command(&tokens).is_err());
599 }
600 #[test]
601 fn test_open_dotted_path() {
602 let tokens = vec![
603 make_token(TokenKind::Open),
604 make_ident("Std"),
605 make_token(TokenKind::Dot),
606 make_ident("Data"),
607 make_token(TokenKind::Dot),
608 make_ident("List"),
609 make_eof(),
610 ];
611 let mut parser = CommandParser::new();
612 let cmd = parser
613 .parse_command(&tokens)
614 .expect("parse_decl should succeed");
615 match cmd {
616 Command::Open { path, .. } => {
617 assert_eq!(
618 path,
619 vec!["Std".to_string(), "Data".to_string(), "List".to_string()]
620 );
621 }
622 _ => panic!("expected Open command"),
623 }
624 }
625 #[test]
626 fn test_notation_kind_display() {
627 assert_eq!(format!("{}", NotationKind::Prefix), "prefix");
628 assert_eq!(format!("{}", NotationKind::Infix), "infix");
629 assert_eq!(format!("{}", NotationKind::Postfix), "postfix");
630 assert_eq!(format!("{}", NotationKind::Notation), "notation");
631 }
632 #[test]
633 fn test_open_item_display() {
634 assert_eq!(format!("{}", OpenItem::All), "*");
635 assert_eq!(
636 format!("{}", OpenItem::Only(vec!["a".to_string(), "b".to_string()])),
637 "only [a, b]"
638 );
639 assert_eq!(
640 format!("{}", OpenItem::Hiding(vec!["c".to_string()])),
641 "hiding [c]"
642 );
643 assert_eq!(
644 format!(
645 "{}",
646 OpenItem::Renaming("old".to_string(), "new".to_string())
647 ),
648 "old -> new"
649 );
650 }
651 #[test]
652 fn test_parse_variable_strict_implicit() {
653 let tokens = vec![
654 make_token(TokenKind::Variable),
655 make_token(TokenKind::LBrace),
656 make_token(TokenKind::LBrace),
657 make_ident("a"),
658 make_token(TokenKind::Colon),
659 make_ident("Type"),
660 make_token(TokenKind::RBrace),
661 make_token(TokenKind::RBrace),
662 make_eof(),
663 ];
664 let mut parser = CommandParser::new();
665 let cmd = parser
666 .parse_command(&tokens)
667 .expect("parse_decl should succeed");
668 match cmd {
669 Command::Variable { binders, .. } => {
670 assert_eq!(binders.len(), 1);
671 assert_eq!(binders[0].name, "a");
672 assert_eq!(binders[0].info, BinderKind::StrictImplicit);
673 }
674 _ => panic!("expected Variable command"),
675 }
676 }
677 #[test]
678 fn test_parse_declaration_keyword_delegates() {
679 let tokens = vec![make_token(TokenKind::Axiom), make_eof()];
680 let mut parser = CommandParser::new();
681 let result = parser.parse_command(&tokens);
682 assert!(result.is_err());
683 }
684 #[test]
685 fn test_parse_export_empty() {
686 let tokens = vec![make_token(TokenKind::Export), make_eof()];
687 let mut parser = CommandParser::new();
688 assert!(parser.parse_command(&tokens).is_err());
689 }
690 #[test]
691 fn test_parse_universe_empty() {
692 let tokens = vec![make_ident("universe"), make_eof()];
693 let mut parser = CommandParser::new();
694 assert!(parser.parse_command(&tokens).is_err());
695 }
696 #[test]
697 fn test_parse_structure_simple() {
698 let tokens = vec![
699 make_token(TokenKind::Structure),
700 make_ident("Point"),
701 make_eof(),
702 ];
703 let mut parser = CommandParser::new();
704 let cmd = parser
705 .parse_command(&tokens)
706 .expect("parse_decl should succeed");
707 match cmd {
708 Command::Structure {
709 name,
710 extends,
711 fields,
712 derives,
713 ..
714 } => {
715 assert_eq!(name, "Point");
716 assert!(extends.is_empty());
717 assert!(fields.is_empty());
718 assert!(derives.is_empty());
719 }
720 _ => panic!("expected Structure command"),
721 }
722 }
723 #[test]
724 fn test_parse_structure_with_fields() {
725 let tokens = vec![
726 make_token(TokenKind::Structure),
727 make_ident("Point"),
728 make_ident("where"),
729 make_ident("x"),
730 make_token(TokenKind::Colon),
731 make_ident("Real"),
732 make_eof(),
733 ];
734 let mut parser = CommandParser::new();
735 let cmd = parser
736 .parse_command(&tokens)
737 .expect("parse_decl should succeed");
738 match cmd {
739 Command::Structure { name, fields, .. } => {
740 assert_eq!(name, "Point");
741 assert!(!fields.is_empty());
742 }
743 _ => panic!("expected Structure command"),
744 }
745 }
746 #[test]
747 fn test_parse_class_simple() {
748 let tokens = vec![
749 make_token(TokenKind::Class),
750 make_ident("Monoid"),
751 make_eof(),
752 ];
753 let mut parser = CommandParser::new();
754 let cmd = parser
755 .parse_command(&tokens)
756 .expect("parse_decl should succeed");
757 match cmd {
758 Command::Class {
759 name,
760 params,
761 extends,
762 ..
763 } => {
764 assert_eq!(name, "Monoid");
765 assert!(params.is_empty());
766 assert!(extends.is_empty());
767 }
768 _ => panic!("expected Class command"),
769 }
770 }
771 #[test]
772 fn test_parse_class_with_extends() {
773 let tokens = vec![
774 make_token(TokenKind::Class),
775 make_ident("Group"),
776 make_ident("extends"),
777 make_ident("Monoid"),
778 make_eof(),
779 ];
780 let mut parser = CommandParser::new();
781 let cmd = parser
782 .parse_command(&tokens)
783 .expect("parse_decl should succeed");
784 match cmd {
785 Command::Class { name, extends, .. } => {
786 assert_eq!(name, "Group");
787 assert_eq!(extends, vec!["Monoid".to_string()]);
788 }
789 _ => panic!("expected Class command"),
790 }
791 }
792 #[test]
793 fn test_parse_instance_simple() {
794 let tokens = vec![
795 make_token(TokenKind::Instance),
796 make_ident("myInst"),
797 make_token(TokenKind::Colon),
798 make_ident("Nat"),
799 make_token(TokenKind::Assign),
800 make_ident("42"),
801 make_eof(),
802 ];
803 let mut parser = CommandParser::new();
804 let cmd = parser
805 .parse_command(&tokens)
806 .expect("parse_decl should succeed");
807 match cmd {
808 Command::Instance {
809 name, ty, priority, ..
810 } => {
811 assert_eq!(name, "myInst");
812 assert_eq!(ty, "Nat");
813 assert!(priority.is_none());
814 }
815 _ => panic!("expected Instance command"),
816 }
817 }
818 #[test]
819 fn test_parse_instance_with_priority() {
820 let tokens = vec![
821 make_token(TokenKind::Instance),
822 make_ident("inst"),
823 make_token(TokenKind::Colon),
824 make_ident("Type"),
825 make_ident("priority"),
826 make_token(TokenKind::Nat(100)),
827 make_token(TokenKind::Assign),
828 make_ident("by"),
829 make_ident("rfl"),
830 make_eof(),
831 ];
832 let mut parser = CommandParser::new();
833 let cmd = parser
834 .parse_command(&tokens)
835 .expect("parse_decl should succeed");
836 match cmd {
837 Command::Instance { priority, .. } => {
838 assert_eq!(priority, Some(100));
839 }
840 _ => panic!("expected Instance command"),
841 }
842 }
843 #[test]
844 fn test_parse_reduce_command() {
845 let tokens = vec![
846 make_token(TokenKind::Hash),
847 make_ident("reduce"),
848 make_ident("1"),
849 make_token(TokenKind::Plus),
850 make_ident("1"),
851 make_eof(),
852 ];
853 let mut parser = CommandParser::new();
854 let cmd = parser
855 .parse_command(&tokens)
856 .expect("parse_decl should succeed");
857 match cmd {
858 Command::Reduce { expr_str, .. } => {
859 assert!(!expr_str.is_empty());
860 }
861 _ => panic!("expected Reduce command"),
862 }
863 }
864 #[test]
865 fn test_parse_attribute_decl_simple() {
866 let tokens = vec![
867 make_token(TokenKind::Attribute),
868 make_token(TokenKind::LBracket),
869 make_ident("simp"),
870 make_token(TokenKind::RBracket),
871 make_eof(),
872 ];
873 let mut parser = CommandParser::new();
874 let cmd = parser
875 .parse_command(&tokens)
876 .expect("parse_decl should succeed");
877 match cmd {
878 Command::AttributeDecl { name, kind, .. } => {
879 assert_eq!(name, "simp");
880 assert_eq!(kind, AttributeDeclKind::Simple);
881 }
882 _ => panic!("expected AttributeDecl command"),
883 }
884 }
885 #[test]
886 fn test_parse_syntax_command() {
887 let tokens = vec![
888 make_ident("syntax"),
889 make_ident("arrow"),
890 make_token(TokenKind::Nat(50)),
891 make_token(TokenKind::Assign),
892 make_ident("fun"),
893 make_eof(),
894 ];
895 let mut parser = CommandParser::new();
896 let cmd = parser
897 .parse_command(&tokens)
898 .expect("parse_decl should succeed");
899 match cmd {
900 Command::Syntax {
901 name,
902 prec,
903 pattern,
904 ..
905 } => {
906 assert_eq!(name, "arrow");
907 assert_eq!(prec, Some(50));
908 assert!(!pattern.is_empty());
909 }
910 _ => panic!("expected Syntax command"),
911 }
912 }
913 #[test]
914 fn test_structure_field_creation() {
915 let field = StructureField {
916 name: "x".to_string(),
917 ty: "Real".to_string(),
918 is_explicit: true,
919 default: Some("0".to_string()),
920 };
921 assert_eq!(field.name, "x");
922 assert_eq!(field.ty, "Real");
923 assert!(field.is_explicit);
924 assert_eq!(field.default, Some("0".to_string()));
925 }
926 #[test]
927 fn test_attribute_decl_kind_macro() {
928 let field = StructureField {
929 name: "test".to_string(),
930 ty: "T".to_string(),
931 is_explicit: false,
932 default: None,
933 };
934 assert!(!field.is_explicit);
935 }
936 #[test]
937 fn test_parse_structure_with_multiple_extends() {
938 let tokens = vec![
939 make_token(TokenKind::Structure),
940 make_ident("Diamond"),
941 make_ident("extends"),
942 make_ident("A"),
943 make_token(TokenKind::Comma),
944 make_ident("B"),
945 make_eof(),
946 ];
947 let mut parser = CommandParser::new();
948 let cmd = parser
949 .parse_command(&tokens)
950 .expect("parse_decl should succeed");
951 match cmd {
952 Command::Structure { extends, .. } => {
953 assert_eq!(extends.len(), 2);
954 assert_eq!(extends[0], "A");
955 assert_eq!(extends[1], "B");
956 }
957 _ => panic!("expected Structure command"),
958 }
959 }
960 #[test]
961 fn test_parse_class_with_multiple_extends() {
962 let tokens = vec![
963 make_token(TokenKind::Class),
964 make_ident("Ring"),
965 make_ident("extends"),
966 make_ident("Semiring"),
967 make_token(TokenKind::Comma),
968 make_ident("Neg"),
969 make_eof(),
970 ];
971 let mut parser = CommandParser::new();
972 let cmd = parser
973 .parse_command(&tokens)
974 .expect("parse_decl should succeed");
975 match cmd {
976 Command::Class { extends, .. } => {
977 assert_eq!(extends.len(), 2);
978 }
979 _ => panic!("expected Class command"),
980 }
981 }
982 #[test]
983 fn test_structure_field_implicit() {
984 let field = StructureField {
985 name: "implicit_field".to_string(),
986 ty: "Alpha".to_string(),
987 is_explicit: false,
988 default: None,
989 };
990 assert!(!field.is_explicit);
991 assert_eq!(field.name, "implicit_field");
992 }
993 #[test]
994 fn test_attribute_decl_builtin() {
995 let tokens = vec![
996 make_token(TokenKind::Attribute),
997 make_token(TokenKind::LBracket),
998 make_ident("builtin"),
999 make_token(TokenKind::RBracket),
1000 make_eof(),
1001 ];
1002 let mut parser = CommandParser::new();
1003 let cmd = parser
1004 .parse_command(&tokens)
1005 .expect("parse_decl should succeed");
1006 match cmd {
1007 Command::AttributeDecl { kind, .. } => {
1008 assert_eq!(kind, AttributeDeclKind::Builtin);
1009 }
1010 _ => panic!("expected AttributeDecl with Builtin kind"),
1011 }
1012 }
1013 #[test]
1014 fn test_parse_class_params() {
1015 let tokens = vec![
1016 make_token(TokenKind::Class),
1017 make_ident("Eq"),
1018 make_token(TokenKind::LParen),
1019 make_ident("α"),
1020 make_token(TokenKind::Colon),
1021 make_ident("Type"),
1022 make_token(TokenKind::RParen),
1023 make_eof(),
1024 ];
1025 let mut parser = CommandParser::new();
1026 let cmd = parser
1027 .parse_command(&tokens)
1028 .expect("parse_decl should succeed");
1029 match cmd {
1030 Command::Class { params, .. } => {
1031 assert_eq!(params.len(), 1);
1032 }
1033 _ => panic!("expected Class command with params"),
1034 }
1035 }
1036 #[test]
1037 fn test_parse_instance_underscore_name() {
1038 let tokens = vec![
1039 make_token(TokenKind::Instance),
1040 make_ident("_"),
1041 make_token(TokenKind::Colon),
1042 make_ident("Monad"),
1043 make_token(TokenKind::Assign),
1044 make_ident("trivial"),
1045 make_eof(),
1046 ];
1047 let mut parser = CommandParser::new();
1048 let cmd = parser
1049 .parse_command(&tokens)
1050 .expect("parse_decl should succeed");
1051 match cmd {
1052 Command::Instance { name, .. } => {
1053 assert_eq!(name, "_");
1054 }
1055 _ => panic!("expected Instance with underscore name"),
1056 }
1057 }
1058 #[test]
1059 fn test_syntax_without_prec() {
1060 let tokens = vec![
1061 make_ident("syntax"),
1062 make_ident("letbinding"),
1063 make_token(TokenKind::Assign),
1064 make_ident("let"),
1065 make_eof(),
1066 ];
1067 let mut parser = CommandParser::new();
1068 let cmd = parser
1069 .parse_command(&tokens)
1070 .expect("parse_decl should succeed");
1071 match cmd {
1072 Command::Syntax { prec, .. } => {
1073 assert!(prec.is_none());
1074 }
1075 _ => panic!("expected Syntax without precedence"),
1076 }
1077 }
1078 #[test]
1079 fn test_parse_structure_with_deriving() {
1080 let tokens = vec![
1081 make_token(TokenKind::Structure),
1082 make_ident("Data"),
1083 make_ident("deriving"),
1084 make_ident("Repr"),
1085 make_token(TokenKind::Comma),
1086 make_ident("BEq"),
1087 make_eof(),
1088 ];
1089 let mut parser = CommandParser::new();
1090 let cmd = parser
1091 .parse_command(&tokens)
1092 .expect("parse_decl should succeed");
1093 match cmd {
1094 Command::Structure { derives, .. } => {
1095 assert_eq!(derives.len(), 2);
1096 assert_eq!(derives[0], "Repr");
1097 assert_eq!(derives[1], "BEq");
1098 }
1099 _ => panic!("expected Structure with derives"),
1100 }
1101 }
1102 #[test]
1103 fn test_attribute_decl_macro_kind() {
1104 let tokens = vec![
1105 make_token(TokenKind::Attribute),
1106 make_token(TokenKind::LBracket),
1107 make_ident("my_macro"),
1108 make_token(TokenKind::RBracket),
1109 make_eof(),
1110 ];
1111 let mut parser = CommandParser::new();
1112 let cmd = parser
1113 .parse_command(&tokens)
1114 .expect("parse_decl should succeed");
1115 match cmd {
1116 Command::AttributeDecl { kind, .. } => {
1117 assert_eq!(kind, AttributeDeclKind::Macro);
1118 }
1119 _ => panic!("expected AttributeDecl with Macro kind"),
1120 }
1121 }
1122 #[test]
1123 fn test_apply_attribute_command() {
1124 let tokens = vec![
1125 make_token(TokenKind::Attribute),
1126 make_token(TokenKind::LBracket),
1127 make_ident("simp"),
1128 make_token(TokenKind::RBracket),
1129 make_ident("myLemma"),
1130 make_eof(),
1131 ];
1132 let mut parser = CommandParser::new();
1133 let cmd = parser
1134 .parse_command(&tokens)
1135 .expect("parse_decl should succeed");
1136 match cmd {
1137 Command::ApplyAttribute {
1138 attr_name, target, ..
1139 } => {
1140 assert_eq!(attr_name, "simp");
1141 assert_eq!(target, "myLemma");
1142 }
1143 _ => panic!("expected ApplyAttribute command"),
1144 }
1145 }
1146 #[test]
1147 fn test_parse_instance_body_complete() {
1148 let tokens = vec![
1149 make_token(TokenKind::Instance),
1150 make_ident("inst"),
1151 make_token(TokenKind::Colon),
1152 make_ident("Functor"),
1153 make_token(TokenKind::Assign),
1154 make_ident("{"),
1155 make_ident("map"),
1156 make_token(TokenKind::Assign),
1157 make_ident("fun"),
1158 make_ident("}"),
1159 make_eof(),
1160 ];
1161 let mut parser = CommandParser::new();
1162 let cmd = parser
1163 .parse_command(&tokens)
1164 .expect("parse_decl should succeed");
1165 match cmd {
1166 Command::Instance { body, .. } => {
1167 assert!(!body.is_empty());
1168 }
1169 _ => panic!("expected Instance with body"),
1170 }
1171 }
1172 #[test]
1173 fn test_structure_field_default_value() {
1174 let field = StructureField {
1175 name: "value".to_string(),
1176 ty: "Int".to_string(),
1177 is_explicit: true,
1178 default: Some("default_val".to_string()),
1179 };
1180 assert_eq!(field.default, Some("default_val".to_string()));
1181 }
1182 #[test]
1183 fn test_parse_notation_precedence_fifty() {
1184 let tokens = vec![
1185 make_ident("infix"),
1186 make_token(TokenKind::Nat(50)),
1187 make_token(TokenKind::String(",".to_string())),
1188 make_token(TokenKind::Assign),
1189 make_ident("Prod"),
1190 make_eof(),
1191 ];
1192 let mut parser = CommandParser::new();
1193 let cmd = parser
1194 .parse_command(&tokens)
1195 .expect("parse_decl should succeed");
1196 match cmd {
1197 Command::Notation { prec, .. } => {
1198 assert_eq!(prec, Some(50));
1199 }
1200 _ => panic!("expected Notation command"),
1201 }
1202 }
1203 #[test]
1204 fn test_check_keyword_helper() {
1205 let mut parser = CommandParser::new();
1206 let tokens = vec![make_ident("where")];
1207 parser.tokens = tokens;
1208 parser.pos = 0;
1209 assert!(parser.check_keyword("where"));
1210 }
1211 #[test]
1212 fn test_at_end_helper() {
1213 let mut parser = CommandParser::new();
1214 parser.tokens = vec![make_eof()];
1215 parser.pos = 1;
1216 assert!(parser.at_end());
1217 }
1218 #[test]
1219 fn test_attribute_decl_simple_kind() {
1220 let tokens = vec![
1221 make_token(TokenKind::Attribute),
1222 make_token(TokenKind::LBracket),
1223 make_ident("custom_attr"),
1224 make_token(TokenKind::RBracket),
1225 make_eof(),
1226 ];
1227 let mut parser = CommandParser::new();
1228 let cmd = parser
1229 .parse_command(&tokens)
1230 .expect("parse_decl should succeed");
1231 match cmd {
1232 Command::AttributeDecl { kind, .. } => {
1233 assert_eq!(kind, AttributeDeclKind::Simple);
1234 }
1235 _ => panic!("expected AttributeDecl with Simple kind"),
1236 }
1237 }
1238 #[test]
1239 fn test_multiple_structure_extends_syntax() {
1240 let token_list = ["A", "B", "C"];
1241 assert_eq!(token_list.len(), 3);
1242 }
1243 #[test]
1244 fn test_class_empty_fields() {
1245 let tokens = vec![
1246 make_token(TokenKind::Class),
1247 make_ident("EmptyClass"),
1248 make_eof(),
1249 ];
1250 let mut parser = CommandParser::new();
1251 let cmd = parser
1252 .parse_command(&tokens)
1253 .expect("parse_decl should succeed");
1254 match cmd {
1255 Command::Class { fields, .. } => {
1256 assert!(fields.is_empty());
1257 }
1258 _ => panic!("expected Class with empty fields"),
1259 }
1260 }
1261}