    {- Data/Singletons/Single/Eq.hs

    (c) Richard Eisenberg 2014
    rae@cs.brynmawr.edu

    Defines functions to generate SEq and SDecide instances.
    -}

    module Data.Singletons.Single.Eq where

    import Language.Haskell.TH.Syntax
    import Language.Haskell.TH.Desugar
    import Data.Singletons.Deriving.Infer
    import Data.Singletons.Util
    import Data.Singletons.Names
    import Control.Monad

    -- making the SEq instance and the SDecide instance are rather similar,
    -- so we generalize
    type EqualityClassDesc q = ((DCon, DCon) -> q DClause, q DClause, Name, Name)
    sEqClassDesc, sDecideClassDesc :: Quasi q => EqualityClassDesc q
    sEqClassDesc :: EqualityClassDesc q
    sEqClassDesc = ((DCon, DCon) -> q DClause
    forall (q :: * -> *). Quasi q => (DCon, DCon) -> q DClause
    mkEqMethClause, q DClause
    forall (q :: * -> *). Applicative q => q DClause
    mkEmptyEqMethClause, Name
    sEqClassName, Name
    sEqMethName)
    sDecideClassDesc :: EqualityClassDesc q
    sDecideClassDesc = ((DCon, DCon) -> q DClause
    forall (q :: * -> *). Quasi q => (DCon, DCon) -> q DClause
    mkDecideMethClause, q DClause
    forall (q :: * -> *). Quasi q => q DClause
    mkEmptyDecideMethClause, Name
    sDecideClassName, Name
    sDecideMethName)

    mkEqualityInstance :: DsMonad q => Maybe DCxt -> DKind
                       -> [DCon] -- ^ The /original/ constructors (for inferring the instance context)
                       -> [DCon] -- ^ The /singletons/ constructors
                       -> EqualityClassDesc q -> q DDec
    mkEqualityInstance :: Maybe DCxt
    -> DKind -> [DCon] -> [DCon] -> EqualityClassDesc q -> q DDec
    mkEqualityInstance mb_ctxt :: Maybe DCxt
    mb_ctxt k :: DKind
    k ctors :: [DCon]
    ctors sctors :: [DCon]
    sctors (mkMeth :: (DCon, DCon) -> q DClause
    mkMeth, mkEmpty :: q DClause
    mkEmpty, className :: Name
    className, methName :: Name
    methName) = do
      let sctorPairs :: [(DCon, DCon)]
    sctorPairs = [ (DCon
    sc1, DCon
    sc2) | DCon
    sc1 <- [DCon]
    sctors, DCon
    sc2 <- [DCon]
    sctors ]
      [DClause]
    methClauses <- if [DCon] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [DCon]
    sctors
                     then (DClause -> [DClause] -> [DClause]
    forall a. a -> [a] -> [a]
    :[]) (DClause -> [DClause]) -> q DClause -> q [DClause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> q DClause
    mkEmpty
                     else ((DCon, DCon) -> q DClause) -> [(DCon, DCon)] -> q [DClause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (DCon, DCon) -> q DClause
    mkMeth [(DCon, DCon)]
    sctorPairs
      DCxt
    constraints <- Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
    forall (q :: * -> *).
    DsMonad q =>
    Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
    inferConstraintsDef Maybe DCxt
    mb_ctxt (Name -> DKind
    DConT Name
    className) DKind
    k [DCon]
    ctors
      DDec -> q DDec
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DDec -> q DDec) -> DDec -> q DDec
    forall a b. (a -> b) -> a -> b
    $ Maybe Overlap
    -> Maybe [DTyVarBndr] -> DCxt -> DKind -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                         DCxt
    constraints
                         (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    className) DKind
    k)
                         [DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Name -> [DClause] -> DLetDec
    DFunD Name
    methName [DClause]
    methClauses]

    data TestInstance = TestEquality
                      | TestCoercion

    -- Make an instance of TestEquality or TestCoercion by leveraging SDecide.
    mkTestInstance :: DsMonad q => Maybe DCxt -> DKind
                   -> Name   -- ^ The name of the data type
                   -> [DCon] -- ^ The /original/ constructors (for inferring the instance context)
                   -> TestInstance -> q DDec
    mkTestInstance :: Maybe DCxt -> DKind -> Name -> [DCon] -> TestInstance -> q DDec
    mkTestInstance mb_ctxt :: Maybe DCxt
    mb_ctxt k :: DKind
    k data_name :: Name
    data_name ctors :: [DCon]
    ctors ti :: TestInstance
    ti = do
      DCxt
    constraints <- Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
    forall (q :: * -> *).
    DsMonad q =>
    Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
    inferConstraintsDef Maybe DCxt
    mb_ctxt (Name -> DKind
    DConT Name
    sDecideClassName) DKind
    k [DCon]
    ctors
      DDec -> q DDec
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DDec -> q DDec) -> DDec -> q DDec
    forall a b. (a -> b) -> a -> b
    $ Maybe Overlap
    -> Maybe [DTyVarBndr] -> DCxt -> DKind -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                        DCxt
    constraints
                        (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    tiClassName)
                               (Name -> DKind
    DConT (Name -> Name
    singTyConName Name
    data_name)
                                 DKind -> DKind -> DKind
    `DSigT` (DKind
    DArrowT DKind -> DKind -> DKind
    `DAppT` DKind
    k DKind -> DKind -> DKind
    `DAppT` Name -> DKind
    DConT Name
    typeKindName)))
                        [DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Name -> [DClause] -> DLetDec
    DFunD Name
    tiMethName
                                         [[DPat] -> DExp -> DClause
    DClause [] (Name -> DExp
    DVarE Name
    tiDefaultName)]]
      where
        (tiClassName :: Name
    tiClassName, tiMethName :: Name
    tiMethName, tiDefaultName :: Name
    tiDefaultName) =
          case TestInstance
    ti of
            TestEquality -> (Name
    testEqualityClassName, Name
    testEqualityMethName, Name
    decideEqualityName)
            TestCoercion -> (Name
    testCoercionClassName, Name
    testCoercionMethName, Name
    decideCoercionName)

    mkEqMethClause :: Quasi q => (DCon, DCon) -> q DClause
    mkEqMethClause :: (DCon, DCon) -> q DClause
    mkEqMethClause (c1 :: DCon
    c1, c2 :: DCon
    c2)
      | Name
    lname Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    rname = do
        [Name]
    lnames <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    lNumArgs (String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "a")
        [Name]
    rnames <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    lNumArgs (String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "b")
        let lpats :: [DPat]
    lpats = (Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    lnames
            rpats :: [DPat]
    rpats = (Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    rnames
            lvars :: [DExp]
    lvars = (Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    lnames
            rvars :: [DExp]
    rvars = (Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    rnames
        DClause -> q DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause
          [Name -> [DPat] -> DPat
    DConP Name
    lname [DPat]
    lpats, Name -> [DPat] -> DPat
    DConP Name
    rname [DPat]
    rpats]
          ([DExp] -> DExp
    allExp ((DExp -> DExp -> DExp) -> [DExp] -> [DExp] -> [DExp]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\l :: DExp
    l r :: DExp
    r -> DExp -> [DExp] -> DExp
    foldExp (Name -> DExp
    DVarE Name
    sEqMethName) [DExp
    l, DExp
    r])
                            [DExp]
    lvars [DExp]
    rvars))
      | Bool
    otherwise =
        DClause -> q DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause
          [Name -> [DPat] -> DPat
    DConP Name
    lname (Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate Int
    lNumArgs DPat
    DWildP),
           Name -> [DPat] -> DPat
    DConP Name
    rname (Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate Int
    rNumArgs DPat
    DWildP)]
          (Name -> DExp
    DConE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    singDataConName Name
    falseName)
      where allExp :: [DExp] -> DExp
            allExp :: [DExp] -> DExp
    allExp [] = Name -> DExp
    DConE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    singDataConName Name
    trueName
            allExp [one :: DExp
    one] = DExp
    one
            allExp (h :: DExp
    h:t :: [DExp]
    t) = DExp -> DExp -> DExp
    DAppE (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DVarE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    singValName Name
    andName) DExp
    h) ([DExp] -> DExp
    allExp [DExp]
    t)

            (lname :: Name
    lname, lNumArgs :: Int
    lNumArgs) = DCon -> (Name, Int)
    extractNameArgs DCon
    c1
            (rname :: Name
    rname, rNumArgs :: Int
    rNumArgs) = DCon -> (Name, Int)
    extractNameArgs DCon
    c2

    mkEmptyEqMethClause :: Applicative q => q DClause
    mkEmptyEqMethClause :: q DClause
    mkEmptyEqMethClause =
      DClause -> q DClause
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [DPat
    DWildP, DPat
    DWildP]
           (DExp -> DClause) -> DExp -> DClause
    forall a b. (a -> b) -> a -> b
    $ Name -> DExp
    DConE Name
    strueName

    mkDecideMethClause :: Quasi q => (DCon, DCon) -> q DClause
    mkDecideMethClause :: (DCon, DCon) -> q DClause
    mkDecideMethClause (c1 :: DCon
    c1, c2 :: DCon
    c2)
      | Name
    lname Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    rname =
        if Int
    lNumArgs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0
        then DClause -> q DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [Name -> [DPat] -> DPat
    DConP Name
    lname [], Name -> [DPat] -> DPat
    DConP Name
    rname []]
                              (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DConE Name
    provedName) (Name -> DExp
    DConE Name
    reflName))
        else do
          [Name]
    lnames <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    lNumArgs (String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "a")
          [Name]
    rnames <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    lNumArgs (String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "b")
          Name
    contra <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "contra"
          let lpats :: [DPat]
    lpats = (Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    lnames
              rpats :: [DPat]
    rpats = (Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    rnames
              lvars :: [DExp]
    lvars = (Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    lnames
              rvars :: [DExp]
    rvars = (Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    rnames
          Name
    refl <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "refl"
          DClause -> q DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause
            [Name -> [DPat] -> DPat
    DConP Name
    lname [DPat]
    lpats, Name -> [DPat] -> DPat
    DConP Name
    rname [DPat]
    rpats]
            (DExp -> [DMatch] -> DExp
    DCaseE ([DExp] -> DExp
    mkTupleDExp ([DExp] -> DExp) -> [DExp] -> DExp
    forall a b. (a -> b) -> a -> b
    $
                     (DExp -> DExp -> DExp) -> [DExp] -> [DExp] -> [DExp]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\l :: DExp
    l r :: DExp
    r -> DExp -> [DExp] -> DExp
    foldExp (Name -> DExp
    DVarE Name
    sDecideMethName) [DExp
    l, DExp
    r])
                             [DExp]
    lvars [DExp]
    rvars)
                    ((DPat -> DExp -> DMatch
    DMatch ([DPat] -> DPat
    mkTupleDPat (Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate Int
    lNumArgs
                                            (Name -> [DPat] -> DPat
    DConP Name
    provedName [Name -> [DPat] -> DPat
    DConP Name
    reflName []])))
                            (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DConE Name
    provedName) (Name -> DExp
    DConE Name
    reflName))) DMatch -> [DMatch] -> [DMatch]
    forall a. a -> [a] -> [a]
    :
                     [DPat -> DExp -> DMatch
    DMatch ([DPat] -> DPat
    mkTupleDPat (Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate Int
    i DPat
    DWildP [DPat] -> [DPat] -> [DPat]
    forall a. [a] -> [a] -> [a]
    ++
                                           Name -> [DPat] -> DPat
    DConP Name
    disprovedName [Name -> DPat
    DVarP Name
    contra] DPat -> [DPat] -> [DPat]
    forall a. a -> [a] -> [a]
    :
                                           Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate (Int
    lNumArgs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) DPat
    DWildP))
                             (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DConE Name
    disprovedName)
                                    ([Name] -> DExp -> DExp
    DLamE [Name
    refl] (DExp -> DExp) -> DExp -> DExp
    forall a b. (a -> b) -> a -> b
    $
                                     DExp -> [DMatch] -> DExp
    DCaseE (Name -> DExp
    DVarE Name
    refl)
                                            [DPat -> DExp -> DMatch
    DMatch (Name -> [DPat] -> DPat
    DConP Name
    reflName []) (DExp -> DMatch) -> DExp -> DMatch
    forall a b. (a -> b) -> a -> b
    $
                                             (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DVarE Name
    contra)
                                                    (Name -> DExp
    DConE Name
    reflName))]))
                     | Int
    i <- [0..Int
    lNumArgsInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1] ]))

      | Bool
    otherwise = do
        Name
    x <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "x"
        DClause -> q DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause
          [Name -> [DPat] -> DPat
    DConP Name
    lname (Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate Int
    lNumArgs DPat
    DWildP),
           Name -> [DPat] -> DPat
    DConP Name
    rname (Int -> DPat -> [DPat]
    forall a. Int -> a -> [a]
    replicate Int
    rNumArgs DPat
    DWildP)]
          (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DConE Name
    disprovedName) ([Name] -> DExp -> DExp
    DLamE [Name
    x] (DExp -> [DMatch] -> DExp
    DCaseE (Name -> DExp
    DVarE Name
    x) [])))

      where
        (lname :: Name
    lname, lNumArgs :: Int
    lNumArgs) = DCon -> (Name, Int)
    extractNameArgs DCon
    c1
        (rname :: Name
    rname, rNumArgs :: Int
    rNumArgs) = DCon -> (Name, Int)
    extractNameArgs DCon
    c2

    mkEmptyDecideMethClause :: Quasi q => q DClause
    mkEmptyDecideMethClause :: q DClause
    mkEmptyDecideMethClause = do
      Name
    x <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "x"
      DClause -> q DClause
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DClause -> q DClause) -> DClause -> q DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [Name -> DPat
    DVarP Name
    x, DPat
    DWildP]
           (DExp -> DClause) -> DExp -> DClause
    forall a b. (a -> b) -> a -> b
    $ Name -> DExp
    DConE Name
    provedName DExp -> DExp -> DExp
    `DAppE` DExp -> [DMatch] -> DExp
    DCaseE (Name -> DExp
    DVarE Name
    x) []