1#[cfg(test)]
6mod tests {
7 use super::*;
8 use crate::tactic_parser::*;
9 use crate::tokens::{Span, Token, TokenKind};
10 fn make_token(kind: TokenKind) -> Token {
11 Token {
12 kind,
13 span: Span::new(0, 0, 0, 0),
14 }
15 }
16 fn ident(s: &str) -> Token {
17 make_token(TokenKind::Ident(s.to_string()))
18 }
19 #[test]
20 fn test_parse_basic_tactic() {
21 let tokens = vec![make_token(TokenKind::Ident("intro".to_string()))];
22 let mut parser = TacticParser::new(&tokens);
23 let result = parser.parse().expect("parsing should succeed");
24 assert_eq!(result, TacticExpr::Intro(Vec::new()));
25 }
26 #[test]
27 fn test_parse_tactic_with_args() {
28 let tokens = vec![
29 make_token(TokenKind::Ident("custom".to_string())),
30 make_token(TokenKind::LParen),
31 make_token(TokenKind::Ident("foo".to_string())),
32 make_token(TokenKind::RParen),
33 ];
34 let mut parser = TacticParser::new(&tokens);
35 let result = parser.parse().expect("parsing should succeed");
36 assert!(matches!(result, TacticExpr::WithArgs(..)));
37 }
38 #[test]
39 fn test_parse_repeat() {
40 let tokens = vec![
41 make_token(TokenKind::Ident("repeat".to_string())),
42 make_token(TokenKind::Ident("assumption".to_string())),
43 ];
44 let mut parser = TacticParser::new(&tokens);
45 let result = parser.parse().expect("parsing should succeed");
46 match result {
47 TacticExpr::Repeat(inner) => {
48 assert_eq!(*inner, TacticExpr::Assumption);
49 }
50 _ => panic!("expected Repeat"),
51 }
52 }
53 #[test]
54 fn test_parse_try() {
55 let tokens = vec![
56 make_token(TokenKind::Ident("try".to_string())),
57 make_token(TokenKind::Ident("trivial".to_string())),
58 ];
59 let mut parser = TacticParser::new(&tokens);
60 let result = parser.parse().expect("parsing should succeed");
61 match result {
62 TacticExpr::Try(inner) => {
63 assert_eq!(*inner, TacticExpr::Trivial);
64 }
65 _ => panic!("expected Try"),
66 }
67 }
68 #[test]
69 fn test_parse_seq() {
70 let tokens = vec![
71 ident("omega"),
72 make_token(TokenKind::Semicolon),
73 ident("ring"),
74 ];
75 let mut parser = TacticParser::new(&tokens);
76 let result = parser.parse().expect("parsing should succeed");
77 match result {
78 TacticExpr::Seq(left, right) => {
79 assert_eq!(*left, TacticExpr::Omega);
80 assert_eq!(*right, TacticExpr::Ring);
81 }
82 _ => panic!("expected Seq"),
83 }
84 }
85 #[test]
86 fn test_parse_intro_with_names() {
87 let tokens = vec![ident("intro"), ident("x"), ident("y"), ident("z")];
88 let mut parser = TacticParser::new(&tokens);
89 let result = parser.parse().expect("parsing should succeed");
90 assert_eq!(
91 result,
92 TacticExpr::Intro(vec!["x".to_string(), "y".to_string(), "z".to_string()])
93 );
94 }
95 #[test]
96 fn test_parse_intro_no_names() {
97 let tokens = vec![ident("intro")];
98 let mut parser = TacticParser::new(&tokens);
99 let result = parser.parse().expect("parsing should succeed");
100 assert_eq!(result, TacticExpr::Intro(vec![]));
101 }
102 #[test]
103 fn test_parse_apply() {
104 let tokens = vec![ident("apply"), ident("Nat.add_comm")];
105 let mut parser = TacticParser::new(&tokens);
106 let result = parser.parse().expect("parsing should succeed");
107 assert_eq!(result, TacticExpr::Apply("Nat.add_comm".to_string()));
108 }
109 #[test]
110 fn test_parse_exact() {
111 let tokens = vec![ident("exact"), ident("rfl")];
112 let mut parser = TacticParser::new(&tokens);
113 let result = parser.parse().expect("parsing should succeed");
114 assert_eq!(result, TacticExpr::Exact("rfl".to_string()));
115 }
116 #[test]
117 fn test_parse_rewrite_single() {
118 let tokens = vec![
119 ident("rewrite"),
120 make_token(TokenKind::LBracket),
121 ident("add_comm"),
122 make_token(TokenKind::RBracket),
123 ];
124 let mut parser = TacticParser::new(&tokens);
125 let result = parser.parse().expect("parsing should succeed");
126 match result {
127 TacticExpr::Rewrite(rules) => {
128 assert_eq!(rules.len(), 1);
129 assert_eq!(rules[0].lemma, "add_comm");
130 assert!(!rules[0].reverse);
131 }
132 _ => panic!("expected Rewrite"),
133 }
134 }
135 #[test]
136 fn test_parse_rewrite_reverse() {
137 let tokens = vec![
138 ident("rw"),
139 make_token(TokenKind::LBracket),
140 ident("<-"),
141 ident("mul_comm"),
142 make_token(TokenKind::RBracket),
143 ];
144 let mut parser = TacticParser::new(&tokens);
145 let result = parser.parse().expect("parsing should succeed");
146 match result {
147 TacticExpr::Rewrite(rules) => {
148 assert_eq!(rules.len(), 1);
149 assert_eq!(rules[0].lemma, "mul_comm");
150 assert!(rules[0].reverse);
151 }
152 _ => panic!("expected Rewrite"),
153 }
154 }
155 #[test]
156 fn test_parse_rewrite_multiple() {
157 let tokens = vec![
158 ident("rw"),
159 make_token(TokenKind::LBracket),
160 ident("add_comm"),
161 make_token(TokenKind::Comma),
162 ident("<-"),
163 ident("mul_assoc"),
164 make_token(TokenKind::RBracket),
165 ];
166 let mut parser = TacticParser::new(&tokens);
167 let result = parser.parse().expect("parsing should succeed");
168 match result {
169 TacticExpr::Rewrite(rules) => {
170 assert_eq!(rules.len(), 2);
171 assert_eq!(rules[0].lemma, "add_comm");
172 assert!(!rules[0].reverse);
173 assert_eq!(rules[1].lemma, "mul_assoc");
174 assert!(rules[1].reverse);
175 }
176 _ => panic!("expected Rewrite"),
177 }
178 }
179 #[test]
180 fn test_parse_simp_basic() {
181 let tokens = vec![ident("simp")];
182 let mut parser = TacticParser::new(&tokens);
183 let result = parser.parse().expect("parsing should succeed");
184 assert_eq!(
185 result,
186 TacticExpr::Simp(SimpArgs {
187 only: false,
188 lemmas: vec![],
189 config: vec![],
190 })
191 );
192 }
193 #[test]
194 fn test_parse_simp_only_with_lemmas() {
195 let tokens = vec![
196 ident("simp"),
197 ident("only"),
198 make_token(TokenKind::LBracket),
199 ident("add_zero"),
200 make_token(TokenKind::Comma),
201 ident("mul_one"),
202 make_token(TokenKind::RBracket),
203 ];
204 let mut parser = TacticParser::new(&tokens);
205 let result = parser.parse().expect("parsing should succeed");
206 match result {
207 TacticExpr::Simp(args) => {
208 assert!(args.only);
209 assert_eq!(
210 args.lemmas,
211 vec!["add_zero".to_string(), "mul_one".to_string()]
212 );
213 }
214 _ => panic!("expected Simp"),
215 }
216 }
217 #[test]
218 fn test_parse_simp_star() {
219 let tokens = vec![
220 ident("simp"),
221 make_token(TokenKind::LBracket),
222 make_token(TokenKind::Star),
223 make_token(TokenKind::RBracket),
224 ];
225 let mut parser = TacticParser::new(&tokens);
226 let result = parser.parse().expect("parsing should succeed");
227 match result {
228 TacticExpr::Simp(args) => {
229 assert!(!args.only);
230 assert_eq!(args.lemmas, vec!["*".to_string()]);
231 }
232 _ => panic!("expected Simp"),
233 }
234 }
235 #[test]
236 fn test_parse_cases_no_arms() {
237 let tokens = vec![ident("cases"), ident("h")];
238 let mut parser = TacticParser::new(&tokens);
239 let result = parser.parse().expect("parsing should succeed");
240 assert_eq!(result, TacticExpr::Cases("h".to_string(), vec![]));
241 }
242 #[test]
243 fn test_parse_cases_with_arms() {
244 let tokens = vec![
245 ident("cases"),
246 ident("h"),
247 ident("with"),
248 make_token(TokenKind::Bar),
249 ident("zero"),
250 make_token(TokenKind::Arrow),
251 ident("rfl"),
252 make_token(TokenKind::Bar),
253 ident("succ"),
254 ident("n"),
255 make_token(TokenKind::Arrow),
256 ident("omega"),
257 ];
258 let mut parser = TacticParser::new(&tokens);
259 let result = parser.parse().expect("parsing should succeed");
260 match result {
261 TacticExpr::Cases(target, arms) => {
262 assert_eq!(target, "h");
263 assert_eq!(arms.len(), 2);
264 assert_eq!(arms[0].name, "zero");
265 assert!(arms[0].bindings.is_empty());
266 assert_eq!(arms[0].tactic, TacticExpr::Rfl);
267 assert_eq!(arms[1].name, "succ");
268 assert_eq!(arms[1].bindings, vec!["n".to_string()]);
269 assert_eq!(arms[1].tactic, TacticExpr::Omega);
270 }
271 _ => panic!("expected Cases"),
272 }
273 }
274 #[test]
275 fn test_parse_induction_with_arms() {
276 let tokens = vec![
277 ident("induction"),
278 ident("n"),
279 ident("with"),
280 make_token(TokenKind::Bar),
281 ident("zero"),
282 make_token(TokenKind::Arrow),
283 ident("rfl"),
284 make_token(TokenKind::Bar),
285 ident("succ"),
286 ident("k"),
287 ident("ih"),
288 make_token(TokenKind::Arrow),
289 ident("assumption"),
290 ];
291 let mut parser = TacticParser::new(&tokens);
292 let result = parser.parse().expect("parsing should succeed");
293 match result {
294 TacticExpr::Induction(target, arms) => {
295 assert_eq!(target, "n");
296 assert_eq!(arms.len(), 2);
297 assert_eq!(arms[1].name, "succ");
298 assert_eq!(arms[1].bindings, vec!["k".to_string(), "ih".to_string()]);
299 assert_eq!(arms[1].tactic, TacticExpr::Assumption);
300 }
301 _ => panic!("expected Induction"),
302 }
303 }
304 #[test]
305 fn test_parse_have() {
306 let tokens = vec![
307 ident("have"),
308 ident("h"),
309 make_token(TokenKind::Colon),
310 ident("Nat"),
311 make_token(TokenKind::Assign),
312 ident("trivial"),
313 ];
314 let mut parser = TacticParser::new(&tokens);
315 let result = parser.parse().expect("parsing should succeed");
316 match result {
317 TacticExpr::Have(name, ty, body) => {
318 assert_eq!(name, "h");
319 assert_eq!(ty, Some("Nat".to_string()));
320 assert_eq!(*body, TacticExpr::Trivial);
321 }
322 _ => panic!("expected Have"),
323 }
324 }
325 #[test]
326 fn test_parse_let() {
327 let tokens = vec![
328 ident("let"),
329 ident("x"),
330 make_token(TokenKind::Assign),
331 ident("foo"),
332 ];
333 let mut parser = TacticParser::new(&tokens);
334 let result = parser.parse().expect("parsing should succeed");
335 assert_eq!(result, TacticExpr::Let("x".to_string(), "foo".to_string()));
336 }
337 #[test]
338 fn test_parse_show() {
339 let tokens = vec![ident("show"), ident("Nat")];
340 let mut parser = TacticParser::new(&tokens);
341 let result = parser.parse().expect("parsing should succeed");
342 assert_eq!(result, TacticExpr::Show("Nat".to_string()));
343 }
344 #[test]
345 fn test_parse_omega() {
346 let tokens = vec![ident("omega")];
347 let mut parser = TacticParser::new(&tokens);
348 assert_eq!(
349 parser.parse().expect("parsing should succeed"),
350 TacticExpr::Omega
351 );
352 }
353 #[test]
354 fn test_parse_ring() {
355 let tokens = vec![ident("ring")];
356 let mut parser = TacticParser::new(&tokens);
357 assert_eq!(
358 parser.parse().expect("parsing should succeed"),
359 TacticExpr::Ring
360 );
361 }
362 #[test]
363 fn test_parse_decide() {
364 let tokens = vec![ident("decide")];
365 let mut parser = TacticParser::new(&tokens);
366 assert_eq!(
367 parser.parse().expect("parsing should succeed"),
368 TacticExpr::Decide
369 );
370 }
371 #[test]
372 fn test_parse_norm_num() {
373 let tokens = vec![ident("norm_num")];
374 let mut parser = TacticParser::new(&tokens);
375 assert_eq!(
376 parser.parse().expect("parsing should succeed"),
377 TacticExpr::NormNum
378 );
379 }
380 #[test]
381 fn test_parse_constructor() {
382 let tokens = vec![ident("constructor")];
383 let mut parser = TacticParser::new(&tokens);
384 assert_eq!(
385 parser.parse().expect("parsing should succeed"),
386 TacticExpr::Constructor
387 );
388 }
389 #[test]
390 fn test_parse_left_right() {
391 let tokens_l = vec![ident("left")];
392 let tokens_r = vec![ident("right")];
393 let mut parser_l = TacticParser::new(&tokens_l);
394 let mut parser_r = TacticParser::new(&tokens_r);
395 assert_eq!(
396 parser_l.parse().expect("parsing should succeed"),
397 TacticExpr::Left
398 );
399 assert_eq!(
400 parser_r.parse().expect("parsing should succeed"),
401 TacticExpr::Right
402 );
403 }
404 #[test]
405 fn test_parse_existsi() {
406 let tokens = vec![ident("existsi"), ident("42")];
407 let mut parser = TacticParser::new(&tokens);
408 assert_eq!(
409 parser.parse().expect("parsing should succeed"),
410 TacticExpr::Existsi("42".to_string())
411 );
412 }
413 #[test]
414 fn test_parse_clear() {
415 let tokens = vec![ident("clear"), ident("h1"), ident("h2")];
416 let mut parser = TacticParser::new(&tokens);
417 assert_eq!(
418 parser.parse().expect("parsing should succeed"),
419 TacticExpr::Clear(vec!["h1".to_string(), "h2".to_string()])
420 );
421 }
422 #[test]
423 fn test_parse_revert() {
424 let tokens = vec![ident("revert"), ident("x"), ident("y")];
425 let mut parser = TacticParser::new(&tokens);
426 assert_eq!(
427 parser.parse().expect("parsing should succeed"),
428 TacticExpr::Revert(vec!["x".to_string(), "y".to_string()])
429 );
430 }
431 #[test]
432 fn test_parse_subst() {
433 let tokens = vec![ident("subst"), ident("h")];
434 let mut parser = TacticParser::new(&tokens);
435 assert_eq!(
436 parser.parse().expect("parsing should succeed"),
437 TacticExpr::Subst("h".to_string())
438 );
439 }
440 #[test]
441 fn test_parse_contradiction() {
442 let tokens = vec![ident("contradiction")];
443 let mut parser = TacticParser::new(&tokens);
444 assert_eq!(
445 parser.parse().expect("parsing should succeed"),
446 TacticExpr::Contradiction
447 );
448 }
449 #[test]
450 fn test_parse_exfalso() {
451 let tokens = vec![ident("exfalso")];
452 let mut parser = TacticParser::new(&tokens);
453 assert_eq!(
454 parser.parse().expect("parsing should succeed"),
455 TacticExpr::Exfalso
456 );
457 }
458 #[test]
459 fn test_parse_by_contra_with_name() {
460 let tokens = vec![ident("by_contra"), ident("h")];
461 let mut parser = TacticParser::new(&tokens);
462 assert_eq!(
463 parser.parse().expect("parsing should succeed"),
464 TacticExpr::ByContra(Some("h".to_string()))
465 );
466 }
467 #[test]
468 fn test_parse_by_contra_no_name() {
469 let tokens = vec![ident("by_contra")];
470 let mut parser = TacticParser::new(&tokens);
471 assert_eq!(
472 parser.parse().expect("parsing should succeed"),
473 TacticExpr::ByContra(None)
474 );
475 }
476 #[test]
477 fn test_parse_assumption() {
478 let tokens = vec![ident("assumption")];
479 let mut parser = TacticParser::new(&tokens);
480 assert_eq!(
481 parser.parse().expect("parsing should succeed"),
482 TacticExpr::Assumption
483 );
484 }
485 #[test]
486 fn test_parse_trivial() {
487 let tokens = vec![ident("trivial")];
488 let mut parser = TacticParser::new(&tokens);
489 assert_eq!(
490 parser.parse().expect("parsing should succeed"),
491 TacticExpr::Trivial
492 );
493 }
494 #[test]
495 fn test_parse_rfl() {
496 let tokens = vec![ident("rfl")];
497 let mut parser = TacticParser::new(&tokens);
498 assert_eq!(
499 parser.parse().expect("parsing should succeed"),
500 TacticExpr::Rfl
501 );
502 }
503 #[test]
504 fn test_parse_block() {
505 let tokens = vec![
506 make_token(TokenKind::LBrace),
507 ident("omega"),
508 make_token(TokenKind::Semicolon),
509 ident("ring"),
510 make_token(TokenKind::RBrace),
511 ];
512 let mut parser = TacticParser::new(&tokens);
513 let result = parser.parse().expect("parsing should succeed");
514 match result {
515 TacticExpr::Block(tactics) => {
516 assert_eq!(tactics.len(), 1);
517 assert!(matches!(tactics[0], TacticExpr::Seq(..)));
518 }
519 _ => panic!("expected Block"),
520 }
521 }
522 #[test]
523 fn test_parse_by_block() {
524 let tokens = vec![
525 ident("by"),
526 make_token(TokenKind::LBrace),
527 ident("rfl"),
528 make_token(TokenKind::RBrace),
529 ];
530 let mut parser = TacticParser::new(&tokens);
531 let result = parser
532 .parse_by_block()
533 .expect("mutex should not be poisoned");
534 match result {
535 TacticExpr::Block(tactics) => {
536 assert_eq!(tactics.len(), 1);
537 assert_eq!(tactics[0], TacticExpr::Rfl);
538 }
539 _ => panic!("expected Block"),
540 }
541 }
542 #[test]
543 fn test_parse_by_single() {
544 let tokens = vec![ident("by"), ident("rfl")];
545 let mut parser = TacticParser::new(&tokens);
546 let result = parser
547 .parse_by_block()
548 .expect("mutex should not be poisoned");
549 assert_eq!(result, TacticExpr::Rfl);
550 }
551 #[test]
552 fn test_parse_conv_lhs() {
553 let tokens = vec![
554 ident("conv_lhs"),
555 make_token(TokenKind::Arrow),
556 ident("ring"),
557 ];
558 let mut parser = TacticParser::new(&tokens);
559 let result = parser.parse().expect("parsing should succeed");
560 match result {
561 TacticExpr::Conv(side, inner) => {
562 assert_eq!(side, ConvSide::Lhs);
563 assert_eq!(*inner, TacticExpr::Ring);
564 }
565 _ => panic!("expected Conv"),
566 }
567 }
568 #[test]
569 fn test_parse_conv_rhs() {
570 let tokens = vec![
571 ident("conv_rhs"),
572 make_token(TokenKind::Arrow),
573 ident("ring"),
574 ];
575 let mut parser = TacticParser::new(&tokens);
576 let result = parser.parse().expect("parsing should succeed");
577 match result {
578 TacticExpr::Conv(side, inner) => {
579 assert_eq!(side, ConvSide::Rhs);
580 assert_eq!(*inner, TacticExpr::Ring);
581 }
582 _ => panic!("expected Conv"),
583 }
584 }
585 #[test]
586 fn test_parse_conv_with_side() {
587 let tokens = vec![
588 ident("conv"),
589 ident("lhs"),
590 make_token(TokenKind::Arrow),
591 ident("ring"),
592 ];
593 let mut parser = TacticParser::new(&tokens);
594 let result = parser.parse().expect("parsing should succeed");
595 match result {
596 TacticExpr::Conv(side, inner) => {
597 assert_eq!(side, ConvSide::Lhs);
598 assert_eq!(*inner, TacticExpr::Ring);
599 }
600 _ => panic!("expected Conv"),
601 }
602 }
603 #[test]
604 fn test_parse_seq_of_structured() {
605 let tokens = vec![
606 ident("intro"),
607 ident("x"),
608 make_token(TokenKind::Semicolon),
609 ident("apply"),
610 ident("foo"),
611 make_token(TokenKind::Semicolon),
612 ident("rfl"),
613 ];
614 let mut parser = TacticParser::new(&tokens);
615 let result = parser.parse().expect("parsing should succeed");
616 match result {
617 TacticExpr::Seq(left, right) => {
618 assert_eq!(*right, TacticExpr::Rfl);
619 match *left {
620 TacticExpr::Seq(left2, right2) => {
621 assert_eq!(*left2, TacticExpr::Intro(vec!["x".to_string()]));
622 assert_eq!(*right2, TacticExpr::Apply("foo".to_string()));
623 }
624 _ => panic!("expected inner Seq"),
625 }
626 }
627 _ => panic!("expected Seq"),
628 }
629 }
630 #[test]
631 fn test_parse_try_structured() {
632 let tokens = vec![ident("try"), ident("omega")];
633 let mut parser = TacticParser::new(&tokens);
634 let result = parser.parse().expect("parsing should succeed");
635 match result {
636 TacticExpr::Try(inner) => assert_eq!(*inner, TacticExpr::Omega),
637 _ => panic!("expected Try"),
638 }
639 }
640 #[test]
641 fn test_parse_repeat_structured() {
642 let tokens = vec![ident("repeat"), ident("constructor")];
643 let mut parser = TacticParser::new(&tokens);
644 let result = parser.parse().expect("parsing should succeed");
645 match result {
646 TacticExpr::Repeat(inner) => assert_eq!(*inner, TacticExpr::Constructor),
647 _ => panic!("expected Repeat"),
648 }
649 }
650 #[test]
651 fn test_parse_focus() {
652 let tokens = vec![ident("focus"), make_token(TokenKind::Nat(2)), ident("ring")];
653 let mut parser = TacticParser::new(&tokens);
654 let result = parser.parse().expect("parsing should succeed");
655 match result {
656 TacticExpr::Focus(n, inner) => {
657 assert_eq!(n, 2);
658 assert_eq!(*inner, TacticExpr::Ring);
659 }
660 _ => panic!("expected Focus"),
661 }
662 }
663 #[test]
664 fn test_parse_suffices() {
665 let tokens = vec![
666 ident("suffices"),
667 ident("h"),
668 ident("by"),
669 ident("assumption"),
670 ];
671 let mut parser = TacticParser::new(&tokens);
672 let result = parser.parse().expect("parsing should succeed");
673 match result {
674 TacticExpr::Suffices(name, body) => {
675 assert_eq!(name, "h");
676 assert_eq!(*body, TacticExpr::Assumption);
677 }
678 _ => panic!("expected Suffices"),
679 }
680 }
681 #[test]
682 fn test_parse_empty_rewrite() {
683 let tokens = vec![
684 ident("rw"),
685 make_token(TokenKind::LBracket),
686 make_token(TokenKind::RBracket),
687 ];
688 let mut parser = TacticParser::new(&tokens);
689 let result = parser.parse().expect("parsing should succeed");
690 match result {
691 TacticExpr::Rewrite(rules) => assert!(rules.is_empty()),
692 _ => panic!("expected Rewrite"),
693 }
694 }
695 #[test]
696 fn test_parse_use_alias() {
697 let tokens = vec![ident("use"), ident("witness")];
698 let mut parser = TacticParser::new(&tokens);
699 let result = parser.parse().expect("parsing should succeed");
700 assert_eq!(result, TacticExpr::Existsi("witness".to_string()));
701 }
702 #[test]
703 fn test_rewrite_rule_equality() {
704 let r1 = RewriteRule {
705 lemma: "foo".to_string(),
706 reverse: false,
707 };
708 let r2 = RewriteRule {
709 lemma: "foo".to_string(),
710 reverse: true,
711 };
712 assert_ne!(r1, r2);
713 }
714 #[test]
715 fn test_simp_args_equality() {
716 let a1 = SimpArgs {
717 only: true,
718 lemmas: vec!["a".to_string()],
719 config: vec![],
720 };
721 let a2 = SimpArgs {
722 only: false,
723 lemmas: vec!["a".to_string()],
724 config: vec![],
725 };
726 assert_ne!(a1, a2);
727 }
728 #[test]
729 fn test_case_arm_equality() {
730 let arm = CaseArm {
731 name: "zero".to_string(),
732 bindings: vec![],
733 tactic: TacticExpr::Rfl,
734 };
735 let arm2 = CaseArm {
736 name: "zero".to_string(),
737 bindings: vec![],
738 tactic: TacticExpr::Rfl,
739 };
740 assert_eq!(arm, arm2);
741 }
742 #[test]
743 fn test_conv_side_equality() {
744 assert_ne!(ConvSide::Lhs, ConvSide::Rhs);
745 assert_eq!(ConvSide::Lhs, ConvSide::Lhs);
746 }
747 #[test]
748 fn test_parse_all_goals_combinator() {
749 let tokens = vec![
750 ident("intro"),
751 make_token(TokenKind::Ident("<;>".to_string())),
752 ident("rfl"),
753 ];
754 let mut parser = TacticParser::new(&tokens);
755 let result = parser.parse().expect("parsing should succeed");
756 assert!(!matches!(result, TacticExpr::Rfl));
757 }
758 #[test]
759 fn test_parse_intros() {
760 let tokens = vec![ident("intros"), ident("x"), ident("y"), ident("z")];
761 let mut parser = TacticParser::new(&tokens);
762 let result = parser.parse().expect("parsing should succeed");
763 assert_eq!(
764 result,
765 TacticExpr::Intros(vec!["x".to_string(), "y".to_string(), "z".to_string()])
766 );
767 }
768 #[test]
769 fn test_parse_intros_empty() {
770 let tokens = vec![ident("intros")];
771 let mut parser = TacticParser::new(&tokens);
772 let result = parser.parse().expect("parsing should succeed");
773 assert_eq!(result, TacticExpr::Intros(vec![]));
774 }
775 #[test]
776 fn test_parse_generalize() {
777 let tokens = vec![
778 ident("generalize"),
779 ident("h"),
780 make_token(TokenKind::Colon),
781 ident("n"),
782 ];
783 let mut parser = TacticParser::new(&tokens);
784 let result = parser.parse().expect("parsing should succeed");
785 assert_eq!(
786 result,
787 TacticExpr::Generalize("h".to_string(), "n".to_string())
788 );
789 }
790 #[test]
791 fn test_parse_obtain() {
792 let tokens = vec![
793 ident("obtain"),
794 ident("h"),
795 make_token(TokenKind::Comma),
796 ident("rfl"),
797 ];
798 let mut parser = TacticParser::new(&tokens);
799 let result = parser.parse().expect("parsing should succeed");
800 match result {
801 TacticExpr::Obtain(name, body) => {
802 assert_eq!(name, "h");
803 assert_eq!(*body, TacticExpr::Rfl);
804 }
805 _ => panic!("expected Obtain"),
806 }
807 }
808 #[test]
809 fn test_parse_rcases() {
810 let tokens = vec![
811 ident("rcases"),
812 ident("h"),
813 ident("with"),
814 make_token(TokenKind::Bar),
815 ident("zero"),
816 make_token(TokenKind::Arrow),
817 ident("rfl"),
818 ];
819 let mut parser = TacticParser::new(&tokens);
820 let result = parser.parse().expect("parsing should succeed");
821 match result {
822 TacticExpr::Rcases(target, patterns) => {
823 assert_eq!(target, "h");
824 assert_eq!(patterns.len(), 1);
825 assert_eq!(patterns[0], "zero");
826 }
827 _ => panic!("expected Rcases"),
828 }
829 }
830 #[test]
831 fn test_parse_tauto() {
832 let tokens = vec![ident("tauto")];
833 let mut parser = TacticParser::new(&tokens);
834 assert_eq!(
835 parser.parse().expect("parsing should succeed"),
836 TacticExpr::Tauto
837 );
838 }
839 #[test]
840 fn test_parse_ac_rfl() {
841 let tokens = vec![ident("ac_rfl")];
842 let mut parser = TacticParser::new(&tokens);
843 assert_eq!(
844 parser.parse().expect("parsing should succeed"),
845 TacticExpr::AcRfl
846 );
847 }
848 #[test]
849 fn test_first_tactic_single() {
850 let tokens = vec![ident("first"), make_token(TokenKind::Bar), ident("omega")];
851 let mut parser = TacticParser::new(&tokens);
852 let result = parser.parse().expect("parsing should succeed");
853 match result {
854 TacticExpr::First(tactics) => {
855 assert!(!tactics.is_empty());
856 }
857 _ => panic!("expected First"),
858 }
859 }
860 #[test]
861 fn test_custom_tactic_structure() {
862 let custom = CustomTactic {
863 name: "my_tactic".to_string(),
864 params: vec!["x".to_string(), "y".to_string()],
865 body: "simp".to_string(),
866 };
867 assert_eq!(custom.name, "my_tactic");
868 assert_eq!(custom.params.len(), 2);
869 }
870 #[test]
871 fn test_tactic_location_structure() {
872 let loc = TacticLocation {
873 line: 42,
874 column: 10,
875 name: "omega".to_string(),
876 };
877 assert_eq!(loc.line, 42);
878 assert_eq!(loc.column, 10);
879 assert_eq!(loc.name, "omega");
880 }
881 #[test]
882 fn test_parse_seq_with_all_goals() {
883 let tokens = vec![
884 ident("omega"),
885 make_token(TokenKind::Semicolon),
886 ident("ring"),
887 ];
888 let mut parser = TacticParser::new(&tokens);
889 let result = parser.parse().expect("parsing should succeed");
890 match result {
891 TacticExpr::Seq(_, _) => {}
892 _ => panic!("expected Seq"),
893 }
894 }
895 #[test]
896 fn test_parse_apply_with_multiple_names() {
897 let tokens = vec![ident("apply"), ident("Nat"), ident("add_comm")];
898 let mut parser = TacticParser::new(&tokens);
899 let result = parser.parse().expect("parsing should succeed");
900 match result {
901 TacticExpr::Apply(name) => {
902 assert_eq!(name, "Nat");
903 }
904 _ => panic!("expected Apply"),
905 }
906 }
907 #[test]
908 fn test_parse_repeat_with_apply() {
909 let tokens = vec![ident("repeat"), ident("apply"), ident("Nat.succ")];
910 let mut parser = TacticParser::new(&tokens);
911 let result = parser.parse().expect("parsing should succeed");
912 match result {
913 TacticExpr::Repeat(inner) => {
914 assert!(matches!(*inner, TacticExpr::Apply(_)));
915 }
916 _ => panic!("expected Repeat"),
917 }
918 }
919 #[test]
920 fn test_parse_try_with_omega() {
921 let tokens = vec![ident("try"), ident("omega")];
922 let mut parser = TacticParser::new(&tokens);
923 let result = parser.parse().expect("parsing should succeed");
924 match result {
925 TacticExpr::Try(inner) => {
926 assert_eq!(*inner, TacticExpr::Omega);
927 }
928 _ => panic!("expected Try"),
929 }
930 }
931 #[test]
932 fn test_parse_rewrite_with_multiple_lemmas() {
933 let tokens = vec![
934 ident("rw"),
935 make_token(TokenKind::LBracket),
936 ident("lem1"),
937 make_token(TokenKind::Comma),
938 ident("lem2"),
939 make_token(TokenKind::Comma),
940 ident("lem3"),
941 make_token(TokenKind::RBracket),
942 ];
943 let mut parser = TacticParser::new(&tokens);
944 let result = parser.parse().expect("parsing should succeed");
945 match result {
946 TacticExpr::Rewrite(rules) => {
947 assert_eq!(rules.len(), 3);
948 }
949 _ => panic!("expected Rewrite"),
950 }
951 }
952 #[test]
953 fn test_parse_simp_with_negation() {
954 let tokens = vec![
955 ident("simp"),
956 make_token(TokenKind::LBracket),
957 make_token(TokenKind::Minus),
958 ident("lemma"),
959 make_token(TokenKind::RBracket),
960 ];
961 let mut parser = TacticParser::new(&tokens);
962 let result = parser.parse().expect("parsing should succeed");
963 match result {
964 TacticExpr::Simp(args) => {
965 assert_eq!(args.lemmas.len(), 1);
966 assert_eq!(args.lemmas[0], "-lemma");
967 }
968 _ => panic!("expected Simp"),
969 }
970 }
971 #[test]
972 fn test_parse_cases_multiple_arms() {
973 let tokens = vec![
974 ident("cases"),
975 ident("n"),
976 ident("with"),
977 make_token(TokenKind::Bar),
978 ident("zero"),
979 make_token(TokenKind::Arrow),
980 ident("rfl"),
981 make_token(TokenKind::Bar),
982 ident("succ"),
983 ident("k"),
984 make_token(TokenKind::Arrow),
985 ident("assumption"),
986 make_token(TokenKind::Bar),
987 ident("other"),
988 make_token(TokenKind::Arrow),
989 ident("trivial"),
990 ];
991 let mut parser = TacticParser::new(&tokens);
992 let result = parser.parse().expect("parsing should succeed");
993 match result {
994 TacticExpr::Cases(_, arms) => {
995 assert_eq!(arms.len(), 3);
996 }
997 _ => panic!("expected Cases"),
998 }
999 }
1000 #[test]
1001 fn test_parse_induction_base_and_step() {
1002 let tokens = vec![
1003 ident("induction"),
1004 ident("n"),
1005 ident("with"),
1006 make_token(TokenKind::Bar),
1007 ident("zero"),
1008 make_token(TokenKind::Arrow),
1009 ident("rfl"),
1010 make_token(TokenKind::Bar),
1011 ident("succ"),
1012 ident("k"),
1013 ident("ih"),
1014 make_token(TokenKind::Arrow),
1015 ident("simp"),
1016 ];
1017 let mut parser = TacticParser::new(&tokens);
1018 let result = parser.parse().expect("parsing should succeed");
1019 match result {
1020 TacticExpr::Induction(target, arms) => {
1021 assert_eq!(target, "n");
1022 assert_eq!(arms.len(), 2);
1023 assert_eq!(arms[1].bindings.len(), 2);
1024 }
1025 _ => panic!("expected Induction"),
1026 }
1027 }
1028 #[test]
1029 fn test_parse_have_with_by() {
1030 let tokens = vec![
1031 ident("have"),
1032 ident("h"),
1033 make_token(TokenKind::Colon),
1034 ident("P"),
1035 make_token(TokenKind::Assign),
1036 ident("by"),
1037 ident("assumption"),
1038 ];
1039 let mut parser = TacticParser::new(&tokens);
1040 let result = parser.parse().expect("parsing should succeed");
1041 match result {
1042 TacticExpr::Have(name, ty, body) => {
1043 assert_eq!(name, "h");
1044 assert_eq!(ty, Some("P".to_string()));
1045 assert_eq!(*body, TacticExpr::Assumption);
1046 }
1047 _ => panic!("expected Have"),
1048 }
1049 }
1050 #[test]
1051 fn test_parse_calc_multiple_steps() {
1052 let tokens = vec![
1053 ident("calc"),
1054 make_token(TokenKind::Underscore),
1055 ident("="),
1056 ident("e1"),
1057 make_token(TokenKind::Assign),
1058 ident("by"),
1059 ident("rfl"),
1060 make_token(TokenKind::Underscore),
1061 ident("="),
1062 ident("e2"),
1063 make_token(TokenKind::Assign),
1064 ident("by"),
1065 ident("simp"),
1066 ];
1067 let mut parser = TacticParser::new(&tokens);
1068 let result = parser.parse().expect("parsing should succeed");
1069 match result {
1070 TacticExpr::Calc(steps) => {
1071 assert_eq!(steps.len(), 2);
1072 }
1073 _ => panic!("expected Calc"),
1074 }
1075 }
1076 #[test]
1077 fn test_parse_conv_complex() {
1078 let tokens = vec![
1079 ident("conv"),
1080 ident("lhs"),
1081 make_token(TokenKind::Arrow),
1082 ident("simp"),
1083 make_token(TokenKind::Semicolon),
1084 ident("ring"),
1085 ];
1086 let mut parser = TacticParser::new(&tokens);
1087 let result = parser.parse().expect("parsing should succeed");
1088 match result {
1089 TacticExpr::Seq(left, right) => {
1090 match *left {
1091 TacticExpr::Conv(side, ref inner) => {
1092 assert_eq!(side, ConvSide::Lhs);
1093 assert!(matches!(**inner, TacticExpr::Simp(_)));
1094 }
1095 _ => panic!("expected Conv in left of Seq"),
1096 }
1097 assert_eq!(*right, TacticExpr::Ring);
1098 }
1099 _ => panic!("expected Seq(Conv(...), Ring)"),
1100 }
1101 }
1102 #[test]
1103 fn test_parse_clear_multiple() {
1104 let tokens = vec![ident("clear"), ident("h1"), ident("h2"), ident("h3")];
1105 let mut parser = TacticParser::new(&tokens);
1106 let result = parser.parse().expect("parsing should succeed");
1107 match result {
1108 TacticExpr::Clear(names) => {
1109 assert_eq!(names.len(), 3);
1110 }
1111 _ => panic!("expected Clear"),
1112 }
1113 }
1114 #[test]
1115 fn test_parse_revert_multiple() {
1116 let tokens = vec![ident("revert"), ident("x"), ident("y"), ident("z")];
1117 let mut parser = TacticParser::new(&tokens);
1118 let result = parser.parse().expect("parsing should succeed");
1119 match result {
1120 TacticExpr::Revert(names) => {
1121 assert_eq!(names.len(), 3);
1122 }
1123 _ => panic!("expected Revert"),
1124 }
1125 }
1126 #[test]
1127 fn test_parse_by_contra_full() {
1128 let tokens = vec![ident("by_contra"), ident("h")];
1129 let mut parser = TacticParser::new(&tokens);
1130 let result = parser.parse().expect("parsing should succeed");
1131 match result {
1132 TacticExpr::ByContra(Some(name)) => {
1133 assert_eq!(name, "h");
1134 }
1135 _ => panic!("expected ByContra with name"),
1136 }
1137 }
1138 #[test]
1139 fn test_parse_block_nested() {
1140 let tokens = vec![
1141 make_token(TokenKind::LBrace),
1142 ident("intro"),
1143 ident("x"),
1144 make_token(TokenKind::Semicolon),
1145 make_token(TokenKind::LBrace),
1146 ident("apply"),
1147 ident("foo"),
1148 make_token(TokenKind::Semicolon),
1149 ident("rfl"),
1150 make_token(TokenKind::RBrace),
1151 make_token(TokenKind::RBrace),
1152 ];
1153 let mut parser = TacticParser::new(&tokens);
1154 let result = parser.parse().expect("parsing should succeed");
1155 assert!(matches!(result, TacticExpr::Block(_)));
1156 }
1157 #[test]
1158 fn test_parse_intros_with_underscore() {
1159 let tokens = vec![
1160 ident("intros"),
1161 ident("x"),
1162 make_token(TokenKind::Underscore),
1163 ident("y"),
1164 ];
1165 let mut parser = TacticParser::new(&tokens);
1166 let result = parser.parse().expect("parsing should succeed");
1167 match result {
1168 TacticExpr::Intros(names) => {
1169 assert_eq!(names.len(), 3);
1170 assert_eq!(names[1], "_");
1171 }
1172 _ => panic!("expected Intros"),
1173 }
1174 }
1175 #[test]
1176 fn test_parse_constructor_nullary() {
1177 let tokens = vec![ident("constructor")];
1178 let mut parser = TacticParser::new(&tokens);
1179 assert_eq!(
1180 parser.parse().expect("parsing should succeed"),
1181 TacticExpr::Constructor
1182 );
1183 }
1184 #[test]
1185 fn test_parse_left_right_pair() {
1186 let left_tokens = vec![ident("left")];
1187 let right_tokens = vec![ident("right")];
1188 let mut left_parser = TacticParser::new(&left_tokens);
1189 let mut right_parser = TacticParser::new(&right_tokens);
1190 assert_eq!(
1191 left_parser.parse().expect("parsing should succeed"),
1192 TacticExpr::Left
1193 );
1194 assert_eq!(
1195 right_parser.parse().expect("parsing should succeed"),
1196 TacticExpr::Right
1197 );
1198 }
1199 #[test]
1200 fn test_rewrite_rule_reverse_flag() {
1201 let rule_fwd = RewriteRule {
1202 lemma: "add_comm".to_string(),
1203 reverse: false,
1204 };
1205 let rule_rev = RewriteRule {
1206 lemma: "add_comm".to_string(),
1207 reverse: true,
1208 };
1209 assert_ne!(rule_fwd, rule_rev);
1210 }
1211 #[test]
1212 fn test_simp_args_only_flag() {
1213 let simp1 = SimpArgs {
1214 only: true,
1215 lemmas: vec![],
1216 config: vec![],
1217 };
1218 let simp2 = SimpArgs {
1219 only: false,
1220 lemmas: vec![],
1221 config: vec![],
1222 };
1223 assert_ne!(simp1, simp2);
1224 }
1225 #[test]
1226 fn test_case_arm_with_bindings() {
1227 let arm = CaseArm {
1228 name: "succ".to_string(),
1229 bindings: vec!["n".to_string(), "ih".to_string()],
1230 tactic: TacticExpr::Assumption,
1231 };
1232 assert_eq!(arm.bindings.len(), 2);
1233 }
1234 #[test]
1235 fn test_calc_step_relation_symbols() {
1236 let step_eq = CalcStep {
1237 relation: "=".to_string(),
1238 rhs: "e2".to_string(),
1239 justification: TacticExpr::Rfl,
1240 };
1241 let step_lt = CalcStep {
1242 relation: "<".to_string(),
1243 rhs: "n".to_string(),
1244 justification: TacticExpr::Omega,
1245 };
1246 assert_eq!(step_eq.relation, "=");
1247 assert_eq!(step_lt.relation, "<");
1248 }
1249 #[test]
1250 fn test_parse_focus_with_goal_number() {
1251 let tokens = vec![
1252 ident("focus"),
1253 make_token(TokenKind::Nat(3)),
1254 ident("assumption"),
1255 ];
1256 let mut parser = TacticParser::new(&tokens);
1257 let result = parser.parse().expect("parsing should succeed");
1258 match result {
1259 TacticExpr::Focus(n, inner) => {
1260 assert_eq!(n, 3);
1261 assert_eq!(*inner, TacticExpr::Assumption);
1262 }
1263 _ => panic!("expected Focus"),
1264 }
1265 }
1266 #[test]
1267 fn test_parse_all_combinator() {
1268 let tokens = vec![ident("all"), ident("rfl")];
1269 let mut parser = TacticParser::new(&tokens);
1270 let result = parser.parse().expect("parsing should succeed");
1271 match result {
1272 TacticExpr::All(inner) => {
1273 assert_eq!(*inner, TacticExpr::Rfl);
1274 }
1275 _ => panic!("expected All"),
1276 }
1277 }
1278 #[test]
1279 fn test_parse_any_combinator() {
1280 let tokens = vec![ident("any"), ident("trivial")];
1281 let mut parser = TacticParser::new(&tokens);
1282 let result = parser.parse().expect("parsing should succeed");
1283 match result {
1284 TacticExpr::Any(inner) => {
1285 assert_eq!(*inner, TacticExpr::Trivial);
1286 }
1287 _ => panic!("expected Any"),
1288 }
1289 }
1290 #[test]
1291 fn test_parse_suffices_with_type() {
1292 let tokens = vec![
1293 ident("suffices"),
1294 ident("h"),
1295 make_token(TokenKind::Colon),
1296 ident("Q"),
1297 ident("by"),
1298 ident("assumption"),
1299 ];
1300 let mut parser = TacticParser::new(&tokens);
1301 let result = parser.parse().expect("parsing should succeed");
1302 match result {
1303 TacticExpr::Suffices(name, body) => {
1304 assert_eq!(name, "h");
1305 assert_eq!(*body, TacticExpr::Assumption);
1306 }
1307 _ => panic!("expected Suffices"),
1308 }
1309 }
1310 #[test]
1311 fn test_parse_show_goal() {
1312 let tokens = vec![ident("show"), ident("Nat")];
1313 let mut parser = TacticParser::new(&tokens);
1314 let result = parser.parse().expect("parsing should succeed");
1315 match result {
1316 TacticExpr::Show(ty) => {
1317 assert_eq!(ty, "Nat");
1318 }
1319 _ => panic!("expected Show"),
1320 }
1321 }
1322 #[test]
1323 fn test_parse_decision_tactics() {
1324 let decide_tokens = vec![ident("decide")];
1325 let norm_tokens = vec![ident("norm_num")];
1326 let mut decide_parser = TacticParser::new(&decide_tokens);
1327 let mut norm_parser = TacticParser::new(&norm_tokens);
1328 assert_eq!(
1329 decide_parser.parse().expect("parsing should succeed"),
1330 TacticExpr::Decide
1331 );
1332 assert_eq!(
1333 norm_parser.parse().expect("parsing should succeed"),
1334 TacticExpr::NormNum
1335 );
1336 }
1337 #[test]
1338 fn test_parse_let_in_tactic() {
1339 let tokens = vec![
1340 ident("let"),
1341 ident("x"),
1342 make_token(TokenKind::Assign),
1343 ident("42"),
1344 ];
1345 let mut parser = TacticParser::new(&tokens);
1346 let result = parser.parse().expect("parsing should succeed");
1347 assert_eq!(result, TacticExpr::Let("x".to_string(), "42".to_string()));
1348 }
1349 #[test]
1350 fn test_parse_existsi_witness() {
1351 let tokens = vec![ident("existsi"), ident("witness_expr")];
1352 let mut parser = TacticParser::new(&tokens);
1353 let result = parser.parse().expect("parsing should succeed");
1354 match result {
1355 TacticExpr::Existsi(witness) => {
1356 assert_eq!(witness, "witness_expr");
1357 }
1358 _ => panic!("expected Existsi"),
1359 }
1360 }
1361 #[test]
1362 fn test_generalize_expr_simple() {
1363 let tokens = vec![
1364 ident("generalize"),
1365 ident("h"),
1366 make_token(TokenKind::Colon),
1367 ident("m"),
1368 ];
1369 let mut parser = TacticParser::new(&tokens);
1370 let result = parser.parse().expect("parsing should succeed");
1371 match result {
1372 TacticExpr::Generalize(name, expr) => {
1373 assert_eq!(name, "h");
1374 assert_eq!(expr, "m");
1375 }
1376 _ => panic!("expected Generalize"),
1377 }
1378 }
1379 #[test]
1380 fn test_obtain_simple_pattern() {
1381 let tokens = vec![
1382 ident("obtain"),
1383 ident("h"),
1384 make_token(TokenKind::Comma),
1385 ident("trivial"),
1386 ];
1387 let mut parser = TacticParser::new(&tokens);
1388 let result = parser.parse().expect("parsing should succeed");
1389 assert!(matches!(result, TacticExpr::Obtain(_, _)));
1390 }
1391 #[test]
1392 #[allow(dead_code)]
1393 fn test_rcases_pattern_destructuring() {
1394 let tokens = vec![
1395 ident("rcases"),
1396 ident("h"),
1397 ident("with"),
1398 make_token(TokenKind::Bar),
1399 ident("case"),
1400 ];
1401 let mut parser = TacticParser::new(&tokens);
1402 let result = parser.parse().expect("parsing should succeed");
1403 assert!(matches!(result, TacticExpr::Rcases(_, _)));
1404 }
1405 #[test]
1406 fn test_first_list_alternatives() {
1407 let tokens = vec![
1408 ident("first"),
1409 make_token(TokenKind::Bar),
1410 ident("omega"),
1411 make_token(TokenKind::Bar),
1412 ident("ring"),
1413 ];
1414 let mut parser = TacticParser::new(&tokens);
1415 let result = parser.parse().expect("parsing should succeed");
1416 match result {
1417 TacticExpr::First(tactics) => {
1418 assert!(!tactics.is_empty());
1419 }
1420 _ => panic!("expected First"),
1421 }
1422 }
1423 #[test]
1424 fn test_tauto_propositional_solver() {
1425 let tokens = vec![ident("tauto")];
1426 let mut parser = TacticParser::new(&tokens);
1427 assert_eq!(
1428 parser.parse().expect("parsing should succeed"),
1429 TacticExpr::Tauto
1430 );
1431 }
1432 #[test]
1433 fn test_ac_rfl_associative_commutative() {
1434 let tokens = vec![ident("ac_rfl")];
1435 let mut parser = TacticParser::new(&tokens);
1436 assert_eq!(
1437 parser.parse().expect("parsing should succeed"),
1438 TacticExpr::AcRfl
1439 );
1440 }
1441 #[test]
1442 fn test_custom_tactic_parameters() {
1443 let custom = CustomTactic {
1444 name: "my_solver".to_string(),
1445 params: vec!["strategy".to_string(), "depth".to_string()],
1446 body: "omega".to_string(),
1447 };
1448 assert_eq!(custom.params.len(), 2);
1449 assert_eq!(custom.params[0], "strategy");
1450 }
1451 #[test]
1452 fn test_tactic_location_line_column() {
1453 let loc = TacticLocation {
1454 line: 100,
1455 column: 15,
1456 name: "simp".to_string(),
1457 };
1458 assert_eq!(loc.line, 100);
1459 assert_eq!(loc.column, 15);
1460 }
1461 #[test]
1462 fn test_parse_alternative_combinator() {
1463 let tokens = vec![
1464 ident("omega"),
1465 make_token(TokenKind::Ident("<|>".to_string())),
1466 ident("ring"),
1467 ];
1468 let mut parser = TacticParser::new(&tokens);
1469 let result = parser.parse().expect("parsing should succeed");
1470 match result {
1471 TacticExpr::Alt(_, _) => {}
1472 _ => panic!("expected Alt"),
1473 }
1474 }
1475 #[test]
1476 fn test_parse_simp_with_config() {
1477 let tokens = vec![
1478 ident("simp"),
1479 make_token(TokenKind::LBracket),
1480 ident("lem"),
1481 make_token(TokenKind::RBracket),
1482 make_token(TokenKind::LBrace),
1483 ident("arith"),
1484 make_token(TokenKind::Assign),
1485 ident("true"),
1486 make_token(TokenKind::RBrace),
1487 ];
1488 let mut parser = TacticParser::new(&tokens);
1489 let result = parser.parse().expect("parsing should succeed");
1490 match result {
1491 TacticExpr::Simp(args) => {
1492 assert!(!args.config.is_empty());
1493 }
1494 _ => panic!("expected Simp"),
1495 }
1496 }
1497}