1use crate::{Environment, Expr, Level, Name};
6
7use super::types::{
8 CoherenceResult, EtaCanonMap, EtaCategorizer, EtaCategory, EtaChangeKind, EtaChangeLog,
9 EtaDepthTracker, EtaEqualityOracle, EtaExpanded, EtaGraph, EtaLongChecker, EtaLongStatus,
10 EtaNormRunSummary, EtaNormalFormChecker, EtaNormalizationPass, EtaPassConfig, EtaRedex,
11 EtaRedexCollector, EtaReduction, EtaRewriteEngine, EtaStateMachine, EtaStats,
12 FieldBoundsChecker, FieldDescriptor, InjectivityChecker, KReductionTable, ProjectionRewrite,
13 ProjectionRewriteSet, RecordUpdate, RecordUpdateBatch, ShapeEquivalence, SingletonKReducer,
14 StructFlatteningPass, StructShape, StructureEta, StructureRegistry,
15};
16
17pub(super) fn head_const(expr: &Expr) -> Option<&Name> {
19 match expr {
20 Expr::Const(n, _) => Some(n),
21 Expr::App(f, _) => head_const(f),
22 _ => None,
23 }
24}
25#[cfg(test)]
26mod tests {
27 use super::*;
28 use crate::declaration::{ConstantInfo, ConstantVal, ConstructorVal, InductiveVal};
29 use crate::{BinderInfo, Environment, Expr, Level, Name};
30 fn env_with_mypair() -> Environment {
36 let mut env = Environment::new();
37 let ind_name = Name::str("MyPair");
38 let ctor_name = Name::str("MyPair.mk");
39 let ctor_ty = Expr::Pi(
40 BinderInfo::Default,
41 Name::str("fst"),
42 Box::new(Expr::Sort(Level::Zero)),
43 Box::new(Expr::Pi(
44 BinderInfo::Default,
45 Name::str("snd"),
46 Box::new(Expr::Sort(Level::Zero)),
47 Box::new(Expr::Const(ind_name.clone(), vec![])),
48 )),
49 );
50 let common_ctor = ConstantVal {
51 name: ctor_name.clone(),
52 level_params: vec![],
53 ty: ctor_ty,
54 };
55 let ctor_val = ConstructorVal {
56 common: common_ctor,
57 induct: ind_name.clone(),
58 cidx: 0,
59 num_params: 0,
60 num_fields: 2,
61 is_unsafe: false,
62 };
63 let ind_ty = Expr::Sort(Level::succ(Level::Zero));
64 let common_ind = ConstantVal {
65 name: ind_name.clone(),
66 level_params: vec![],
67 ty: ind_ty,
68 };
69 let ind_val = InductiveVal {
70 common: common_ind,
71 num_params: 0,
72 num_indices: 0,
73 all: vec![ind_name.clone()],
74 ctors: vec![ctor_name.clone()],
75 num_nested: 0,
76 is_rec: false,
77 is_unsafe: false,
78 is_reflexive: false,
79 is_prop: false,
80 };
81 env.add_constant(ConstantInfo::Inductive(ind_val))
82 .expect("value should be present");
83 env.add_constant(ConstantInfo::Constructor(ctor_val))
84 .expect("value should be present");
85 env
86 }
87 fn env_with_unit() -> Environment {
89 let mut env = Environment::new();
90 let ind_name = Name::str("Unit");
91 let ctor_name = Name::str("Unit.unit");
92 let ctor_ty = Expr::Const(ind_name.clone(), vec![]);
93 let common_ctor = ConstantVal {
94 name: ctor_name.clone(),
95 level_params: vec![],
96 ty: ctor_ty,
97 };
98 let ctor_val = ConstructorVal {
99 common: common_ctor,
100 induct: ind_name.clone(),
101 cidx: 0,
102 num_params: 0,
103 num_fields: 0,
104 is_unsafe: false,
105 };
106 let ind_ty = Expr::Sort(Level::succ(Level::Zero));
107 let common_ind = ConstantVal {
108 name: ind_name.clone(),
109 level_params: vec![],
110 ty: ind_ty,
111 };
112 let ind_val = InductiveVal {
113 common: common_ind,
114 num_params: 0,
115 num_indices: 0,
116 all: vec![ind_name.clone()],
117 ctors: vec![ctor_name.clone()],
118 num_nested: 0,
119 is_rec: false,
120 is_unsafe: false,
121 is_reflexive: false,
122 is_prop: false,
123 };
124 env.add_constant(ConstantInfo::Inductive(ind_val))
125 .expect("value should be present");
126 env.add_constant(ConstantInfo::Constructor(ctor_val))
127 .expect("value should be present");
128 env
129 }
130 #[test]
131 fn test_is_structure_type_recognizes_mypair() {
132 let env = env_with_mypair();
133 let se = StructureEta::new(&env);
134 let ty = Expr::Const(Name::str("MyPair"), vec![]);
135 assert!(se.is_structure_type(&ty));
136 }
137 #[test]
138 fn test_is_structure_type_rejects_unknown() {
139 let env = Environment::new();
140 let se = StructureEta::new(&env);
141 let ty = Expr::Const(Name::str("Foo"), vec![]);
142 assert!(!se.is_structure_type(&ty));
143 }
144 #[test]
145 fn test_collect_field_types_mypair() {
146 let env = env_with_mypair();
147 let se = StructureEta::new(&env);
148 let fields = se.collect_field_types(&Name::str("MyPair"));
149 assert_eq!(fields.len(), 2);
150 assert_eq!(fields[0].0, Name::str("fst"));
151 assert_eq!(fields[1].0, Name::str("snd"));
152 }
153 #[test]
154 fn test_make_proj_chain_length() {
155 let env = env_with_mypair();
156 let se = StructureEta::new(&env);
157 let base = Expr::Const(Name::str("e"), vec![]);
158 let projs = se.make_proj_chain(&base, &Name::str("MyPair"), 2);
159 assert_eq!(projs.len(), 2);
160 assert!(matches!(& projs[0], Expr::Proj(n, 0, _) if n == & Name::str("MyPair")));
161 assert!(matches!(& projs[1], Expr::Proj(n, 1, _) if n == & Name::str("MyPair")));
162 }
163 #[test]
164 fn test_eta_expand_struct_produces_app_tree() {
165 let env = env_with_mypair();
166 let se = StructureEta::new(&env);
167 let expr = Expr::Const(Name::str("e"), vec![]);
168 let ty = Expr::Const(Name::str("MyPair"), vec![]);
169 let expanded = se.eta_expand_struct(&expr, &ty);
170 assert!(expanded.is_some(), "should expand MyPair expression");
171 let result = expanded.expect("result should be present");
172 assert!(matches!(result, Expr::App(_, _)));
173 }
174 #[test]
175 fn test_is_singleton_unit() {
176 let env = env_with_unit();
177 let reducer = SingletonKReducer::new(&env);
178 let ty = Expr::Const(Name::str("Unit"), vec![]);
179 assert!(reducer.is_singleton_type(&ty));
180 }
181 #[test]
182 fn test_is_not_singleton_mypair() {
183 let env = env_with_mypair();
184 let reducer = SingletonKReducer::new(&env);
185 let ty = Expr::Const(Name::str("MyPair"), vec![]);
186 assert!(!reducer.is_singleton_type(&ty));
187 }
188 #[test]
189 fn test_k_reduce_unit_returns_ctor() {
190 let env = env_with_unit();
191 let reducer = SingletonKReducer::new(&env);
192 let expr = Expr::FVar(crate::FVarId::new(42));
193 let ty = Expr::Const(Name::str("Unit"), vec![]);
194 let result = reducer.k_reduce(&expr, &ty);
195 assert!(result.is_some());
196 let canonical = result.expect("canonical should be present");
197 assert!(
198 matches!(& canonical, Expr::Const(n, _) if n == & Name::str("Unit.unit")),
199 "expected Unit.unit constructor, got {:?}",
200 canonical
201 );
202 }
203}
204#[cfg(test)]
205mod tests_struct_eta_extended {
206 use super::*;
207 #[test]
208 fn test_field_descriptor() {
209 let f = FieldDescriptor::new("x", 0, false);
210 assert!(f.is_data());
211 assert!(!f.is_prop);
212 let fp = FieldDescriptor::new("proof", 1, true);
213 assert!(!fp.is_data());
214 }
215 #[test]
216 fn test_structure_registry() {
217 let mut reg = StructureRegistry::new();
218 reg.register(
219 "Point",
220 "Point.mk",
221 vec![
222 FieldDescriptor::new("x", 0, false),
223 FieldDescriptor::new("y", 1, false),
224 ],
225 );
226 reg.register(
227 "Sigma",
228 "Sigma.mk",
229 vec![
230 FieldDescriptor::new("fst", 0, false),
231 FieldDescriptor::new("snd", 1, true),
232 ],
233 );
234 assert_eq!(reg.len(), 2);
235 assert_eq!(reg.field_count("Point"), 2);
236 assert!(!reg.has_prop_fields("Point"));
237 assert!(reg.has_prop_fields("Sigma"));
238 assert_eq!(reg.field_count("Unknown"), 0);
239 let projs = reg.projectors("Point");
240 assert!(projs.contains(&"Point.x".to_string()));
241 assert!(projs.contains(&"Point.y".to_string()));
242 }
243 #[test]
244 fn test_eta_expanded() {
245 let exp = EtaExpanded::new("Point.mk", 42, vec![100, 101]);
246 assert_eq!(exp.arity(), 2);
247 assert_eq!(exp.expr_id, 42);
248 }
249 #[test]
250 fn test_eta_reduction() {
251 let r = EtaReduction::valid(99, "Point.mk");
252 assert!(r.is_valid);
253 let inv = EtaReduction::invalid("Unknown");
254 assert!(!inv.is_valid);
255 }
256 #[test]
257 fn test_eta_stats() {
258 let mut s = EtaStats::new();
259 s.record_expansion();
260 s.record_expansion();
261 s.record_failed_expansion();
262 s.record_reduction();
263 assert!((s.expansion_rate() - 2.0 / 3.0).abs() < 1e-9);
264 assert!((s.reduction_rate() - 1.0).abs() < 1e-9);
265 let summary = s.summary();
266 assert!(summary.contains("expansions=2"));
267 }
268 #[test]
269 fn test_eta_normal_form_checker() {
270 let mut reg = StructureRegistry::new();
271 reg.register(
272 "Prod",
273 "Prod.mk",
274 vec![
275 FieldDescriptor::new("fst", 0, false),
276 FieldDescriptor::new("snd", 1, false),
277 ],
278 );
279 let checker = EtaNormalFormChecker::new(reg);
280 assert!(checker.knows_structure("Prod"));
281 assert!(!checker.knows_structure("Sum"));
282 assert_eq!(checker.expected_arity("Prod"), Some(2));
283 let valid_exp = EtaExpanded::new("Prod", 1, vec![10, 20]);
284 let invalid_exp = EtaExpanded::new("Prod", 2, vec![10]);
285 assert!(checker.check_expansion(&valid_exp));
286 assert!(!checker.check_expansion(&invalid_exp));
287 }
288 #[test]
289 fn test_eta_normalization_pass() {
290 let mut pass = EtaNormalizationPass::new();
291 pass.schedule(1);
292 pass.schedule(2);
293 pass.schedule(1);
294 assert_eq!(pass.pending(), 2);
295 let first = pass.next();
296 assert_eq!(first, Some(1));
297 let _second = pass.next();
298 assert!(pass.is_done());
299 }
300 #[test]
301 fn test_k_reduction_table() {
302 let mut kt = KReductionTable::new();
303 kt.set("Subsingleton", true);
304 kt.set("Nonempty", true);
305 kt.set("Point", false);
306 assert!(kt.is_k_reducible("Subsingleton"));
307 assert!(!kt.is_k_reducible("Point"));
308 assert!(!kt.is_k_reducible("Unknown"));
309 let names = kt.k_reducible_names();
310 assert!(names.contains(&"Subsingleton"));
311 assert!(!names.contains(&"Point"));
312 }
313}
314#[cfg(test)]
315mod tests_struct_eta_extended2 {
316 use super::*;
317 #[test]
318 fn test_eta_depth_tracker() {
319 let mut t = EtaDepthTracker::new();
320 assert_eq!(t.depth(), 0);
321 assert!(!t.is_nested());
322 t.push("Prod");
323 t.push("Sigma");
324 assert_eq!(t.depth(), 2);
325 assert!(t.is_nested());
326 assert_eq!(t.current(), Some("Sigma"));
327 assert!(t.contains("Prod"));
328 assert!(!t.contains("Sum"));
329 assert_eq!(t.path(), "Prod.Sigma");
330 t.pop();
331 assert_eq!(t.depth(), 1);
332 }
333 #[test]
334 fn test_coherence_result() {
335 let ok = CoherenceResult::ok();
336 assert!(ok.is_coherent());
337 let fail = CoherenceResult::fail("mismatch in field 2");
338 assert!(!fail.is_coherent());
339 assert_eq!(
340 fail,
341 CoherenceResult::Incoherent {
342 reason: "mismatch in field 2".to_string()
343 }
344 );
345 }
346 #[test]
347 fn test_projection_rewrite_set() {
348 let mut set = ProjectionRewriteSet::new();
349 set.add(ProjectionRewrite::new("Point.mk", "Point.x", 0));
350 set.add(ProjectionRewrite::new("Point.mk", "Point.y", 1));
351 assert_eq!(set.len(), 2);
352 let r = set
353 .find_by_projector("Point.x")
354 .expect("r should be present");
355 assert_eq!(r.field_index, 0);
356 let rules = set.rules_for_ctor("Point.mk");
357 assert_eq!(rules.len(), 2);
358 }
359 #[test]
360 fn test_field_bounds_checker() {
361 assert!(FieldBoundsChecker::check(3, 0).is_ok());
362 assert!(FieldBoundsChecker::check(3, 2).is_ok());
363 assert!(FieldBoundsChecker::check(3, 3).is_err());
364 }
365 #[test]
366 fn test_field_bounds_checker_validate_set() {
367 let mut reg = StructureRegistry::new();
368 reg.register(
369 "Pair",
370 "Pair.mk",
371 vec![
372 FieldDescriptor::new("fst", 0, false),
373 FieldDescriptor::new("snd", 1, false),
374 ],
375 );
376 let mut set = ProjectionRewriteSet::new();
377 set.add(ProjectionRewrite::new("Pair", "Pair.fst", 0));
378 set.add(ProjectionRewrite::new("Pair", "Pair.snd", 1));
379 set.add(ProjectionRewrite::new("Pair", "Pair.bad", 5));
380 let errors = FieldBoundsChecker::validate_set(&set, ®);
381 assert_eq!(errors.len(), 1);
382 assert!(errors[0].contains("out of bounds"));
383 }
384 #[test]
385 fn test_eta_state_machine() {
386 let mut sm = EtaStateMachine::new();
387 assert!(!sm.is_expanding());
388 sm.start("Prod", 2);
389 assert!(sm.is_expanding());
390 assert_eq!(sm.remaining(), 2);
391 sm.process_field();
392 assert!(sm.is_expanding());
393 assert_eq!(sm.remaining(), 1);
394 sm.process_field();
395 assert!(sm.is_done());
396 assert_eq!(sm.remaining(), 0);
397 }
398 #[test]
399 fn test_projection_rewrite_as_rule() {
400 let r = ProjectionRewrite::new("Prod.mk", "Prod.fst", 0);
401 let rule = r.as_rule();
402 assert!(rule.contains("Prod.fst"));
403 assert!(rule.contains("Prod.mk"));
404 }
405}
406#[cfg(test)]
407mod tests_struct_eta_extended3 {
408 use super::*;
409 #[test]
410 fn test_struct_shape_basics() {
411 let ctor = StructShape::ctor("Prod.mk", 2);
412 let proj = StructShape::proj(0);
413 let other = StructShape::Other;
414 assert!(ctor.is_ctor());
415 assert!(!ctor.is_proj());
416 assert!(proj.is_proj());
417 assert!(!proj.is_ctor());
418 assert_eq!(ctor.arity(), Some(2));
419 assert_eq!(other.arity(), None);
420 }
421 #[test]
422 fn test_eta_redex_collector() {
423 let mut collector = EtaRedexCollector::new();
424 collector.add(EtaRedex::new(vec![], "Point.mk", 1));
425 collector.add(EtaRedex::new(vec![0, 1], "Sigma.mk", 2));
426 assert_eq!(collector.count(), 2);
427 assert!(collector.has_top_level());
428 let sorted = collector.sorted_by_depth();
429 assert_eq!(sorted[0].depth(), 0);
430 assert_eq!(sorted[1].depth(), 2);
431 }
432 #[test]
433 fn test_eta_redex_depth_limit() {
434 let mut collector = EtaRedexCollector::with_max_depth(1);
435 collector.add(EtaRedex::new(vec![0], "A.mk", 1));
436 collector.add(EtaRedex::new(vec![0, 1], "B.mk", 2));
437 assert_eq!(collector.count(), 1);
438 }
439 #[test]
440 fn test_struct_flattening_pass() {
441 let mut pass = StructFlatteningPass::new();
442 for _ in 0..100 {
443 pass.record_processed();
444 }
445 for _ in 0..42 {
446 pass.record_flattened();
447 }
448 assert!((pass.flatten_rate() - 0.42).abs() < 1e-9);
449 }
450 #[test]
451 fn test_shape_equivalence() {
452 let mut reg = StructureRegistry::new();
453 reg.register(
454 "Prod",
455 "Prod.mk",
456 vec![
457 FieldDescriptor::new("fst", 0, false),
458 FieldDescriptor::new("snd", 1, false),
459 ],
460 );
461 let oracle = ShapeEquivalence::new(reg);
462 let a = StructShape::ctor("Prod.mk", 2);
463 let b = StructShape::ctor("Prod.mk", 2);
464 let c = StructShape::ctor("Sum.mk", 2);
465 assert!(oracle.may_be_equal(&a, &b));
466 assert!(!oracle.may_be_equal(&a, &c));
467 let prod_shape = StructShape::ctor("Prod", 2);
468 assert!(oracle.is_expandable(&prod_shape));
469 let unknown = StructShape::ctor("Unknown", 1);
470 assert!(!oracle.is_expandable(&unknown));
471 }
472}
473#[cfg(test)]
474mod tests_struct_eta_extended4 {
475 use super::*;
476 #[test]
477 fn test_injectivity_checker() {
478 let mut ic = InjectivityChecker::new();
479 ic.mark_injective("Prod.mk");
480 ic.mark_injective("List.cons");
481 ic.mark_injective("Prod.mk");
482 assert_eq!(ic.count(), 2);
483 assert!(ic.is_injective("Prod.mk"));
484 assert!(!ic.is_injective("Nat.succ"));
485 }
486 #[test]
487 fn test_record_update() {
488 let u = RecordUpdate::new(10, "Point", 0, 20);
489 assert_eq!(u.expr_id, 10);
490 assert_eq!(u.field_index, 0);
491 assert!(u.describe().contains("Point.0"));
492 }
493 #[test]
494 fn test_record_update_batch() {
495 let mut batch = RecordUpdateBatch::new();
496 batch.add(RecordUpdate::new(1, "P", 0, 100));
497 batch.add(RecordUpdate::new(1, "P", 1, 200));
498 batch.add(RecordUpdate::new(2, "P", 0, 300));
499 assert_eq!(batch.len(), 3);
500 let for_expr1 = batch.updates_for_expr(1);
501 assert_eq!(for_expr1.len(), 2);
502 batch.clear();
503 assert!(batch.is_empty());
504 }
505 #[test]
506 fn test_eta_norm_run_summary() {
507 let mut s = EtaNormRunSummary::new();
508 s.total_expressions = 100;
509 s.eta_expansions = 30;
510 s.eta_reductions = 20;
511 s.unchanged = 50;
512 assert_eq!(s.total_changes(), 50);
513 assert!((s.change_rate() - 0.5).abs() < 1e-9);
514 let f = s.format();
515 assert!(f.contains("total=100"));
516 assert!(f.contains("unchanged=50"));
517 }
518}
519#[cfg(test)]
520mod tests_struct_eta_extended5 {
521 use super::*;
522 #[test]
523 fn test_eta_long_status() {
524 let s = EtaLongStatus::EtaLong;
525 assert!(s.is_eta_long());
526 let n = EtaLongStatus::NotEtaLong;
527 assert!(!n.is_eta_long());
528 }
529 #[test]
530 fn test_eta_long_checker() {
531 let mut chk = EtaLongChecker::new();
532 chk.record(1, EtaLongStatus::EtaLong);
533 chk.record(2, EtaLongStatus::NotEtaLong);
534 chk.record(3, EtaLongStatus::Unknown);
535 assert_eq!(chk.status(1), Some(EtaLongStatus::EtaLong));
536 assert_eq!(chk.status(99), None);
537 let (el, nel, unk) = chk.summary();
538 assert_eq!(el, 1);
539 assert_eq!(nel, 1);
540 assert_eq!(unk, 1);
541 }
542 #[test]
543 fn test_eta_category() {
544 assert!(EtaCategory::Record.needs_eta());
545 assert!(EtaCategory::Function.needs_eta());
546 assert!(!EtaCategory::Primitive.needs_eta());
547 assert_eq!(EtaCategory::Inductive.label(), "inductive");
548 }
549 #[test]
550 fn test_eta_categorizer() {
551 let mut cat = EtaCategorizer::new();
552 cat.assign(1, EtaCategory::Record);
553 cat.assign(2, EtaCategory::Primitive);
554 cat.assign(3, EtaCategory::Function);
555 let needs = cat.needs_eta_ids();
556 assert!(needs.contains(&1));
557 assert!(needs.contains(&3));
558 assert!(!needs.contains(&2));
559 let counts = cat.count_by_category();
560 let record_count = counts
561 .iter()
562 .find(|(c, _)| *c == EtaCategory::Record)
563 .map(|(_, n)| *n)
564 .unwrap_or(0);
565 assert_eq!(record_count, 1);
566 }
567}
568#[cfg(test)]
569mod tests_struct_eta_extended6 {
570 use super::*;
571 #[test]
572 fn test_eta_pass_config() {
573 let cfg = EtaPassConfig::default_config();
574 assert!(cfg.any_enabled());
575 assert!(cfg.do_expand && cfg.do_reduce);
576 let minimal = EtaPassConfig::proj_only();
577 assert!(minimal.any_enabled());
578 assert!(!minimal.do_expand);
579 assert_eq!(minimal.max_passes, 1);
580 }
581 #[test]
582 fn test_eta_change_log() {
583 let mut log = EtaChangeLog::new();
584 log.record(1, EtaChangeKind::Expanded, 0);
585 log.record(2, EtaChangeKind::Reduced, 0);
586 log.record(1, EtaChangeKind::ProjRewritten, 1);
587 assert_eq!(log.len(), 3);
588 let expansions = log.changes_of_kind(EtaChangeKind::Expanded);
589 assert_eq!(expansions.len(), 1);
590 let for_expr1 = log.changes_for_expr(1);
591 assert_eq!(for_expr1.len(), 2);
592 let pass0 = log.changes_in_pass(0);
593 assert_eq!(pass0.len(), 2);
594 }
595}
596#[cfg(test)]
597mod tests_struct_eta_extended7 {
598 use super::*;
599 #[test]
600 fn test_eta_graph() {
601 let mut g = EtaGraph::new();
602 g.add_edge(1, 2);
603 g.add_edge(1, 3);
604 g.add_edge(4, 2);
605 assert!(g.has_edge(1, 2));
606 assert!(!g.has_edge(2, 1));
607 let deps = g.dependencies_of(1);
608 assert!(deps.contains(&2) && deps.contains(&3));
609 let dependents = g.dependents_of(2);
610 assert!(dependents.contains(&1) && dependents.contains(&4));
611 g.remove_node(1);
612 assert!(!g.has_edge(1, 2));
613 assert_eq!(g.edge_count(), 1);
614 }
615 #[test]
616 fn test_eta_canon_map() {
617 let mut cm = EtaCanonMap::new();
618 cm.insert(10, 5);
619 cm.insert(11, 5);
620 cm.insert(12, 7);
621 assert_eq!(cm.canonical(10), 5);
622 assert_eq!(cm.canonical(99), 99);
623 let origs = cm.originals_of(5);
624 assert!(origs.contains(&10) && origs.contains(&11));
625 assert_eq!(origs.len(), 2);
626 }
627}
628#[cfg(test)]
629mod tests_struct_eta_engine {
630 use super::*;
631 #[test]
632 fn test_eta_rewrite_engine() {
633 let mut set = ProjectionRewriteSet::new();
634 set.add(ProjectionRewrite::new("Prod.mk", "Prod.fst", 0));
635 set.add(ProjectionRewrite::new("Prod.mk", "Prod.snd", 1));
636 let mut engine = EtaRewriteEngine::new(set, 5);
637 assert!(!engine.is_exhausted());
638 let r = engine.apply_proj("Prod.fst");
639 assert_eq!(r, Some(0));
640 assert_eq!(engine.steps_taken(), 1);
641 let r2 = engine.apply_proj("Prod.snd");
642 assert_eq!(r2, Some(1));
643 let r3 = engine.apply_proj("Unknown");
644 assert_eq!(r3, None);
645 engine.reset();
646 assert_eq!(engine.steps_taken(), 0);
647 }
648 #[test]
649 fn test_eta_equality_oracle() {
650 let mut cm = EtaCanonMap::new();
651 cm.insert(10, 5);
652 cm.insert(11, 5);
653 cm.insert(12, 7);
654 let oracle = EtaEqualityOracle::new(cm);
655 assert!(oracle.are_eta_equal(10, 11));
656 assert!(!oracle.are_eta_equal(10, 12));
657 assert!(oracle.are_eta_equal(99, 99));
658 assert_eq!(oracle.class_count(), 2);
659 }
660}