@@ -418,6 +418,33 @@ impl Term {
418
418
}
419
419
}
420
420
}
421
+
422
+ /// Returns `true` if `self` is structurally isomorphic to `other`.
423
+ ///
424
+ /// # Example
425
+ /// ```
426
+ /// use lambda_calculus::*;
427
+ ///
428
+ /// let term1 = abs(Var(1)); // λ 1
429
+ /// let term2 = abs(Var(2)); // λ 2
430
+ /// let term3 = abs(Var(1)); // λ 1
431
+ ///
432
+ /// assert_eq!(term1.is_isomorphic_to(&term2), false);
433
+ /// assert_eq!(term1.is_isomorphic_to(&term3), true);
434
+ ///
435
+ /// ```
436
+ pub fn is_isomorphic_to ( & self , other : & Term ) -> bool {
437
+ match ( self , other) {
438
+ ( Var ( x) , Var ( y) ) => x == y,
439
+ ( Abs ( p) , Abs ( q) ) => p. is_isomorphic_to ( q) ,
440
+ ( App ( p_boxed) , App ( q_boxed) ) => {
441
+ let ( ref fp, ref ap) = * * p_boxed;
442
+ let ( ref fq, ref aq) = * * q_boxed;
443
+ fp. is_isomorphic_to ( fq) && ap. is_isomorphic_to ( aq)
444
+ }
445
+ _ => false ,
446
+ }
447
+ }
421
448
}
422
449
423
450
/// Wraps a `Term` in an `Abs`traction. Consumes its argument.
@@ -677,4 +704,13 @@ mod tests {
677
704
9
678
705
) ;
679
706
}
707
+
708
+ #[ test]
709
+ fn is_isomorphic_to ( ) {
710
+ assert ! ( abs( Var ( 1 ) ) . is_isomorphic_to( & abs( Var ( 1 ) ) ) ) ;
711
+ assert ! ( !abs( Var ( 1 ) ) . is_isomorphic_to( & abs( Var ( 2 ) ) ) ) ;
712
+ assert ! ( !app( abs( Var ( 1 ) ) , Var ( 1 ) ) . is_isomorphic_to( & app( abs( Var ( 1 ) ) , Var ( 2 ) ) ) ) ;
713
+ assert ! ( app( abs( Var ( 1 ) ) , Var ( 1 ) ) . is_isomorphic_to( & app( abs( Var ( 1 ) ) , Var ( 1 ) ) ) ) ;
714
+ assert ! ( !app( abs( Var ( 1 ) ) , Var ( 1 ) ) . is_isomorphic_to( & app( Var ( 2 ) , abs( Var ( 1 ) ) ) ) ) ;
715
+ }
680
716
}
0 commit comments