File size: 4,740 Bytes
a10b189 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 | {-# 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
|