{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}

{-|
Module      : Assertica.Backend.TypeCompiler
Description : Compile Assertica types to Haskell type signatures
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL-1.0

Translates type expressions from the Core AST to Haskell type syntax:

MAPPINGS:

- TyVar v                   → v (type variable)
- TyConst C [T1, ..., Tn]   → C T1 ... Tn (type constructor application)
- TyFun A B                 → A -> B (function type)
- TyForall (x : A) . B      → forall x . A -> B (dependent function)
- TyUniverse Type0          → Type (type universe)
- TyUniverse (TypeN n)      → Type (all universes collapse to Type in Haskell)
- TyApp T1 T2               → T1 T2 (type application)
- TyEq a b                  → (a :~: b) (equality type using GADT)

UNIVERSE MAPPING:

Assertica's universe hierarchy (Type 0, Type 1, ...) is mapped to Haskell's
single-level kind system. All universes compile to "Type" or higher kinds
as appropriate for the context.

DEPENDENT TYPES:

Assertica supports full dependent types via TyForall. These are mapped to
Haskell functions or GADT syntax where possible. Complex dependent types
may require GADT encoding with indices.

PRINCIPLES:

1. **Type Safety**: Generated types are valid Haskell 2010 / GHC extensions
2. **Determinism**: Same type input produces same output
3. **Readability**: Generated types are human-readable
4. **No Generics**: Avoid needing exotic extensions where possible
-}

module Assertica.Backend.TypeCompiler
  ( -- * Main compilation function
    compileType
  , compileTypeWith
  ) where

import Data.Text (Text)
import qualified Data.Text as T
import Data.List (intercalate)
import qualified Data.Set as Set
import GHC.Generics (Generic)

import Assertica.Core.AST
import Assertica.Backend.CodeGen (CodeGenConfig)
import qualified Assertica.Backend.TermCompiler as TC

-- ============================================================================
-- MAIN COMPILATION FUNCTION
-- ============================================================================

{-| Compile a type to Haskell type syntax.

This is the primary entry point for type compilation.
Returns either a Haskell type expression string or an error.
-}
compileType :: CodeGenConfig -> Type -> Either String Text
compileType config ty = compileTypeWith config Set.empty ty

{-| Compile a type with a given bound variable context -}
compileTypeWith :: CodeGenConfig -> Set.Set Var -> Type -> Either String Text
compileTypeWith config bound = \case
  TyVar (Var name _) -> Right name

  TyConst (QName mod name) args -> do
    compiledArgs <- mapM (compileTypeWith config bound) args
    let qname = if null mod
                  then name
                  else T.intercalate "." mod <> "." <> name
    if null compiledArgs
      then Right qname
      else Right $ "(" <> qname <> " " <> T.intercalate " " compiledArgs <> ")"

  TyFun a b -> do
    ca <- compileTypeWith config bound a
    cb <- compileTypeWith config bound b
    Right $ "(" <> ca <> " -> " <> cb <> ")"

  TyForall (Binder (Var name _) _) body ->
    -- Dependent function type: forall x . body
    -- In Haskell, this becomes a higher-order function type
    let bound' = Set.insert (Var name 0) bound
    in do
      cb <- compileTypeWith config bound' body
      Right $ "(forall (" <> name <> ") . " <> cb <> ")"

  TyUniverse Type0 ->
    -- Type 0 → Haskell's Type kind
    Right "Type"

  TyUniverse (TypeN _n) ->
    -- Higher universes also map to Type in Haskell
    -- (Haskell doesn't have predicative universes)
    Right "Type"

  TyApp t1 t2 -> do
    ct1 <- compileTypeWith config bound t1
    ct2 <- compileTypeWith config bound t2
    -- Type application: just juxtapose
    Right $ "(" <> ct1 <> " " <> ct2 <> ")"

  TyEq e1 e2 -> do
    -- Equality type: compile using GADT syntax
    -- TyEq a b becomes (a :~: b) using GADT machinery
    _ce1 <- TC.compileTerm config e1
    _ce2 <- TC.compileTerm config e2
    -- For now, return a placeholder
    -- In a full implementation, would use GADT.Equality machinery
    Right "Equality"

-- ============================================================================
-- UNIVERSE HANDLING
-- ============================================================================

{-| Map Assertica universe levels to Haskell kinds -}
universeToKind :: TypeLevel -> Text
universeToKind = \case
  Type0 -> "Type"
  TypeN _ -> "Type"  -- All universes collapse to Type

{-| Check if a type is well-formed at a given universe level -}
-- This would be more complex in a production system
isWellFormedAtLevel :: TypeLevel -> Type -> Bool
isWellFormedAtLevel _level _ty =
  True  -- Simplified for now