content: {-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
  module TestACompare where
  
  import Data.Typeable
  import GHC.Generics
  import Unbound.Generics.LocallyNameless
  
  import Test.Tasty
  import Test.Tasty.HUnit
  
  import AlphaAssertions
  
  data Expr
    = V (Name Expr)
    | Add Expr Expr
    | L (Bind (Name Expr) Expr)
    deriving (Show,Generic,Typeable)
  
  instance Alpha Expr
  
  nameA, nameB, nameC :: Name Expr
  nameA = s2n "a"
  nameB = s2n "b"
  nameC = s2n "c"
  
  test_acompare :: TestTree
  test_acompare = testGroup "acompare"
     -- Names compare in the obvious way.
     [ testGroup "obvious"
        [testCase "ac1 (a < b)"  $ assertAcompare nameA nameB LT
        ,testCase "ac2 (b = b)" $ assertAcompare nameB nameB EQ
        ,testCase "ac3 (b > a)"  $ assertAcompare nameB nameA GT
        ]
     -- structured date compares lexicographically
     , testGroup "lexicographically"
        [testCase "ac4 (a + a = a + a)" $
          assertAcompare (Add (V nameA) (V nameA)) (Add (V nameA) (V nameA)) EQ
        ,testCase "ac5 (a + a < a + b)" $
          assertAcompare (Add (V nameA) (V nameA)) (Add (V nameA) (V nameB)) LT
        ,testCase "ac6 (a + b > a + a)" $
          assertAcompare (Add (V nameA) (V nameB)) (Add (V nameA) (V nameA)) GT
        ,testCase "ac7 (a + a < b + a)" $
          assertAcompare (Add (V nameA) (V nameA)) (Add (V nameB) (V nameA)) LT
        ,testCase "ac8 (b + a > a + a)" $
          assertAcompare (Add (V nameB) (V nameA)) (Add (V nameA) (V nameA)) GT
        ,testCase "ac9 (b + a > a + b)" $
          assertAcompare (Add (V nameB) (V nameA)) (Add (V nameA) (V nameB)) GT
        ]
     -- comparison goes under binders, alpha-respectingly.
     , testGroup "binders"
        [testCase "ac10 (\\a.a+a = \\b.b+b)" $
          assertAcompare (bind nameA (Add (V nameA) (V nameA)))
                         (bind nameB (Add (V nameB) (V nameB)))
                         EQ
        ,testCase "ac11 (\\a.a+a > \\a.a+b)" $
          assertAcompare (bind nameA (Add (V nameA) (V nameA)))
                         (bind nameA (Add (V nameA) (V nameB)))
                         GT
        ,testCase "ac12 (\\c.c+a < \\a.a+b)" $
          assertAcompare (bind nameC (Add (V nameC) (V nameA)))
                         (bind nameA (Add (V nameA) (V nameB)))
                         LT
        ]
     -- non-matching binders handled alpha-respectingly.
     , testGroup "non-matching binders"
        [testCase "ac13 ((\\a.a `ac` \\a b.a) = (\\c.c `ac` \\a b.a))" $
          assertAcompare (bind [nameA] nameA)
                         (bind [nameA,nameB] nameA)
                         (acompare (bind [nameC] nameC) (bind [nameA,nameB] nameA))
        ,testCase "ac14 ((\\a b.a `ac` \\a.a) = (\\c b.c `ac` \\a.a))" $
          assertAcompare (bind [nameA,nameB] nameA)
                         (bind [nameA] nameA)
                         (acompare (bind [nameC,nameB] nameC) (bind [nameA] nameA))
        ]
     -- non-binding stuff in patterns gets compared
     , testGroup "non-binding stuff"
        [testCase "ac15 (<a> < <b>)" $
            assertAcompare (Embed nameA) (Embed nameB) LT
        ,testCase "ac16 (\\c<a>.c+c < \\c<b>.c+c)" $
          assertAcompare
            (bind (nameC, Embed nameA) (Add (V nameC) (V nameC)))
            (bind (nameC, Embed nameB) (Add (V nameC) (V nameC)))
            LT
        ,testCase "ac17 (\\c<a>.b+b < \\c<b>.a+a)" $
          assertAcompare
            (bind (nameC, Embed nameA) (Add (V nameB) (V nameB)))
            (bind (nameC, Embed nameB) (Add (V nameA) (V nameA)))
            LT
        ]
     ]
  