{-# LANGUAGE LambdaCase #-}
module NonBaseTH where

import Data.List (sort)
import Language.Haskell.TH


-- | Define a new GADT that is a base-functor-like version of a given existing
-- GADT AST.
--
-- Remember to use 'lookupTypeName' or 'lookupValueName' instead of normal
-- quotes in case of punning of data types and constructors.
defineBaseAST
  :: Name  -- ^ Name of the (base-functor-like) data type to define
  -> Name  -- ^ Name of the GADT to process
  -> [Name]  -- ^ Constructors to exclude (chiefly Var, Let, Lam)
  -> Q [Dec]
defineBaseAST basename astname excludes = do
  info <- reify astname
  (params, constrs) <- case info of
    TyConI (DataD [] _ params Nothing constrs _) -> return (params, constrs)
    _ -> fail $ "Unsupported datatype: " ++ pprint astname

  let recvar = mkName "r"

  let detectRec :: BangType -> Q (Maybe Type)
      detectRec (_, field) = _

  let processConstr con = do
        (vars, ctx, names, fields, retty) <- case con of
          ForallC vars ctx (GadtC names fields retty) -> return (vars, ctx, names, fields, retty)
          GadtC names fields retty -> return ([], [], names, fields, retty)
          _ -> fail "Unsupported constructors found"
        checkRetty astname (head names) vars retty
        _

  constrs' <- concat <$> traverse processConstr constrs
  _

checkRetty :: Name -> Name -> [TyVarBndr a] -> Type -> Q ()
checkRetty astname consname vars retty = do
  case splitApps retty of
    (ConT name, args)
      | name /= astname -> fail $ "Could not parse return type of constructor " ++ pprint consname
      | null args -> fail "Expected GADT to have type parameters"

      | Just varnames <- traverse (\case VarT varname -> Just varname ; _ -> Nothing) (init args)
      , allDistinct varnames
      , all (`elem` map bndrName vars) varnames ->
          return ()

      | otherwise -> fail $ "All type parameters but the last one must be uniform over all constructors. "
                            ++ "(Return type of constructor " ++ pprint consname ++ ")"
    _ -> fail $ "Could not parse return type of constructor " ++ pprint consname

splitApps :: Type -> (Type, [Type])
splitApps = flip go []
  where go (AppT t arg) tl = go t (arg : tl)
        go t tl = (t, tl)

allDistinct :: Ord a => [a] -> Bool
allDistinct l =
  let sorted = sort l
  in all (uncurry (/=)) (zip sorted (drop 1 sorted))

bndrName :: TyVarBndr a -> Name
bndrName (PlainTV n _) = n
bndrName (KindedTV n _ _) = n