October 2026 main drop: mirror from GitHub

a10b189 verified about 1 month ago

9.21 kB

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

{-|
Module      : Assertica.Backend.CodeGen
Description : Main code generation engine for Assertica → Haskell compilation
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL-1.0
This module is the primary interface for translating verified Assertica Core AST
to executable Haskell code. It orchestrates the compilation pipeline:
1. **TermCompiler**: Translates computational terms to Haskell expressions
2. **TypeCompiler**: Maps type universe to Haskell type signatures
3. **ProofCompiler**: Converts proof terms to Haskell evidence
4. **Emit**: Renders the result as syntactically valid Haskell source
DESIGN PRINCIPLES:
1. **Deterministic Generation**: Same AST input always produces identical output
2. **Type Safety**: Generated code must typecheck under GHC 9.2+
3. **No Unsafe Code**: Forbidden to use unsafeCoerce or similar
4. **Fail-Closed**: Malformed input generates an error, not silent code
5. **Module-Aware**: Qualified names preserve module structure
INTERFACE CONTRACT:
- compileModule: Module → Either String HaskellModule
  Takes a Module (from Core.Module), returns Haskell source or error
- compileDefinition: Definition → Either String HaskellDefinition
  Compiles a single definition (term, type, assertion, etc.)
- compileExpression: Term → Either String HaskellExpr
  Compiles a single term expression to Haskell
ASSUMPTIONS:
- All input has been verified by Agent 3B (TypeChecker)
- All proofs are valid (checked by Agent 2B)
- All module dependencies are resolved
- No circular references in type definitions
-}

module Assertica.Backend.CodeGen
  ( -- * Main compilation interface
    compileModule
  , compileDefinition
  , compileExpression
  , compileType
  , compileProof

    -- * Compiled output types
  , HaskellModule(..)
  , HaskellDefinition(..)
  , HaskellExpr(..)

    -- * Error handling
  , CodeGenError(..)
  , formatCodeGenError

    -- * Configuration
  , CodeGenConfig(..)
  , defaultConfig
  ) where

import Data.Text (Text)
import qualified Data.Text as T
import Data.List (intercalate)
import Data.Maybe (mapMaybe, catMaybes)
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)

import Assertica.Core.AST
import Assertica.Core.Module (Module(..), Definition(..), ModuleMetadata(..))
import qualified Assertica.Backend.TermCompiler as TC
import qualified Assertica.Backend.TypeCompiler as TyC
import qualified Assertica.Backend.ProofCompiler as PC
import qualified Assertica.Backend.Emit as Emit

-- ============================================================================
-- TYPES
-- ============================================================================

{-| Configuration for code generation -}
data CodeGenConfig = CodeGenConfig
  { cgcAddComments :: Bool        -- ^ Include source location comments
  , cgcAddTypeSignatures :: Bool  -- ^ Include type signatures for all definitions
  , cgcModulePrefix :: [Text]    -- ^ Module path prefix for qualification
  , cgcTargetVersion :: (Int, Int)  -- ^ GHC version target (e.g., (9, 2))
  }
  deriving (Show, Generic)

{-| Default code generation configuration -}
defaultConfig :: CodeGenConfig
defaultConfig = CodeGenConfig
  { cgcAddComments = True
  , cgcAddTypeSignatures = True
  , cgcModulePrefix = []
  , cgcTargetVersion = (9, 2)
  }

{-| A compiled Haskell module (abstract representation) -}
data HaskellModule = HaskellModule
  { hmName :: [Text]                    -- ^ Module name path
  , hmImports :: [Text]                 -- ^ Import statements (one per line)
  , hmDefinitions :: [HaskellDefinition] -- ^ All definitions in module
  , hmComments :: [Text]                -- ^ Header comments
  }
  deriving (Show, Generic)

{-| A single compiled Haskell definition -}
data HaskellDefinition = HaskellDefinition
  { hdName :: Text                      -- ^ Definition name
  , hdTypeSignature :: Maybe Text       -- ^ Type signature (e.g., "x :: Int")
  , hdBody :: Text                      -- ^ Definition body
  , hdSourceLocation :: Maybe Text      -- ^ Source location comment
  }
  deriving (Show, Generic)

{-| A compiled Haskell expression -}
data HaskellExpr = HaskellExpr
  { heExpr :: Text                      -- ^ The Haskell expression
  , heType :: Maybe Text                -- ^ Inferred type annotation
  }
  deriving (Show, Generic)

{-| Code generation errors -}
data CodeGenError
  = UnhandledConstruct String
  | InvalidQName QName
  | TypeCompilationFailed String
  | ProofCompilationFailed String
  | TermCompilationFailed String
  | ModuleCompilationFailed String
  | UnsupportedFeature String
  deriving (Show, Generic)

{-| Human-readable error formatting -}
formatCodeGenError :: CodeGenError -> String
formatCodeGenError = \case
  UnhandledConstruct desc ->
    "Code generation: unhandled construct: " ++ desc
  InvalidQName (QName mod name) ->
    "Code generation: invalid qualified name: " ++ intercalate "." (map T.unpack mod) ++ "." ++ T.unpack name
  TypeCompilationFailed desc ->
    "Code generation: type compilation failed: " ++ desc
  ProofCompilationFailed desc ->
    "Code generation: proof compilation failed: " ++ desc
  TermCompilationFailed desc ->
    "Code generation: term compilation failed: " ++ desc
  ModuleCompilationFailed desc ->
    "Code generation: module compilation failed: " ++ desc
  UnsupportedFeature desc ->
    "Code generation: unsupported feature: " ++ desc

-- ============================================================================
-- MAIN COMPILATION INTERFACE
-- ============================================================================

{-| Compile an entire Assertica module to Haskell code.
The module must be fully elaborated and type-checked before reaching this stage.
This is the primary entry point for the backend.
-}
compileModule :: CodeGenConfig -> Module -> Either String HaskellModule
compileModule config (Module _modQName _imports _exports defMap _metadata) = do
  -- Compile all definitions from the definition map
  compiledDefs <- mapM (compileDefinitionValue config) (Map.elems defMap)

  -- Generate module header
  let imports = generateImports config
  let comments = ["-- Generated by Assertica Backend", "-- Do not edit manually"]

  return $ HaskellModule
    { hmName = []  -- Could extract from modQName if needed
    , hmImports = imports
    , hmDefinitions = compiledDefs
    , hmComments = comments
    }

{-| Compile a single definition from Module's Definition type -}
compileDefinitionValue :: CodeGenConfig -> Definition -> Either String HaskellDefinition
compileDefinitionValue config defn = case defn of
  DefTerm term -> do
    compiled <- compileExpression config term
    return $ HaskellDefinition
      { hdName = "value"  -- Anonymous term
      , hdTypeSignature = Nothing
      , hdBody = heExpr compiled
      , hdSourceLocation = if cgcAddComments config then Just "term" else Nothing
      }

  DefType ty -> do
    compiled <- compileType config ty
    return $ HaskellDefinition
      { hdName = "type_def"  -- Anonymous type
      , hdTypeSignature = Just "Type"
      , hdBody = heExpr compiled
      , hdSourceLocation = if cgcAddComments config then Just "type" else Nothing
      }

  DefAssertion _assertion -> do
    -- For now, compile assertion as a unit
    return $ HaskellDefinition
      { hdName = "assertion"
      , hdTypeSignature = Nothing
      , hdBody = "()"
      , hdSourceLocation = if cgcAddComments config then Just "assertion" else Nothing
      }

  DefOpaque desc ->
    return $ HaskellDefinition
      { hdName = "opaque"
      , hdTypeSignature = Nothing
      , hdBody = T.pack desc
      , hdSourceLocation = if cgcAddComments config then Just "opaque" else Nothing
      }

{-| Compile a single definition (can be a term, type, assertion, etc.) -}
compileDefinition :: CodeGenConfig -> Definition -> Either String HaskellDefinition
compileDefinition = compileDefinitionValue

{-| Compile a single term expression to Haskell -}
compileExpression :: CodeGenConfig -> Term -> Either String HaskellExpr
compileExpression config term = do
  expr <- TC.compileTerm config term
  return $ HaskellExpr
    { heExpr = expr
    , heType = Nothing
    }

{-| Compile a type to Haskell -}
compileType :: CodeGenConfig -> Type -> Either String HaskellExpr
compileType config ty = do
  expr <- TyC.compileType config ty
  return $ HaskellExpr
    { heExpr = expr
    , heType = Just "Type"  -- All types have kind Type
    }

{-| Compile a proof to Haskell -}
compileProof :: CodeGenConfig -> Proof -> Either String HaskellExpr
compileProof config proof = do
  expr <- PC.compileProof config proof
  return $ HaskellExpr
    { heExpr = expr
    , heType = Nothing
    }

-- ============================================================================
-- HELPER FUNCTIONS
-- ============================================================================

{-| Generate standard Haskell imports for a module -}
generateImports :: CodeGenConfig -> [Text]
generateImports _config =
  [ "import Prelude"
  , "import qualified Data.Typeable as Typeable"
  , "import GHC.Generics (Generic)"
  ]

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

	{-\|
	Module : Assertica.Backend.CodeGen
	Description : Main code generation engine for Assertica → Haskell compilation
	Copyright : (c) 2026 Ahmad Ali Parr
	License : BSL-1.0

	This module is the primary interface for translating verified Assertica Core AST
	to executable Haskell code. It orchestrates the compilation pipeline:

	1. TermCompiler: Translates computational terms to Haskell expressions
	2. TypeCompiler: Maps type universe to Haskell type signatures
	3. ProofCompiler: Converts proof terms to Haskell evidence
	4. Emit: Renders the result as syntactically valid Haskell source

	DESIGN PRINCIPLES:

	1. Deterministic Generation: Same AST input always produces identical output
	2. Type Safety: Generated code must typecheck under GHC 9.2+
	3. No Unsafe Code: Forbidden to use unsafeCoerce or similar
	4. Fail-Closed: Malformed input generates an error, not silent code
	5. Module-Aware: Qualified names preserve module structure

	INTERFACE CONTRACT:

	- compileModule: Module → Either String HaskellModule
	Takes a Module (from Core.Module), returns Haskell source or error

	- compileDefinition: Definition → Either String HaskellDefinition
	Compiles a single definition (term, type, assertion, etc.)

	- compileExpression: Term → Either String HaskellExpr
	Compiles a single term expression to Haskell

	ASSUMPTIONS:

	- All input has been verified by Agent 3B (TypeChecker)
	- All proofs are valid (checked by Agent 2B)
	- All module dependencies are resolved
	- No circular references in type definitions
	-}

	module Assertica.Backend.CodeGen
	( -- * Main compilation interface
	compileModule
	, compileDefinition
	, compileExpression
	, compileType
	, compileProof

	-- * Compiled output types
	, HaskellModule(..)
	, HaskellDefinition(..)
	, HaskellExpr(..)

	-- * Error handling
	, CodeGenError(..)
	, formatCodeGenError

	-- * Configuration
	, CodeGenConfig(..)
	, defaultConfig
	) where

	import Data.Text (Text)
	import qualified Data.Text as T
	import Data.List (intercalate)
	import Data.Maybe (mapMaybe, catMaybes)
	import qualified Data.Set as Set
	import qualified Data.Map.Strict as Map
	import GHC.Generics (Generic)

	import Assertica.Core.AST
	import Assertica.Core.Module (Module(..), Definition(..), ModuleMetadata(..))
	import qualified Assertica.Backend.TermCompiler as TC
	import qualified Assertica.Backend.TypeCompiler as TyC
	import qualified Assertica.Backend.ProofCompiler as PC
	import qualified Assertica.Backend.Emit as Emit

	-- ============================================================================
	-- TYPES
	-- ============================================================================

	{-\| Configuration for code generation -}
	data CodeGenConfig = CodeGenConfig
	{ cgcAddComments :: Bool -- ^ Include source location comments
	, cgcAddTypeSignatures :: Bool -- ^ Include type signatures for all definitions
	, cgcModulePrefix :: [Text] -- ^ Module path prefix for qualification
	, cgcTargetVersion :: (Int, Int) -- ^ GHC version target (e.g., (9, 2))
	}
	deriving (Show, Generic)

	{-\| Default code generation configuration -}
	defaultConfig :: CodeGenConfig
	defaultConfig = CodeGenConfig
	{ cgcAddComments = True
	, cgcAddTypeSignatures = True
	, cgcModulePrefix = []
	, cgcTargetVersion = (9, 2)
	}

	{-\| A compiled Haskell module (abstract representation) -}
	data HaskellModule = HaskellModule
	{ hmName :: [Text] -- ^ Module name path
	, hmImports :: [Text] -- ^ Import statements (one per line)
	, hmDefinitions :: [HaskellDefinition] -- ^ All definitions in module
	, hmComments :: [Text] -- ^ Header comments
	}
	deriving (Show, Generic)

	{-\| A single compiled Haskell definition -}
	data HaskellDefinition = HaskellDefinition
	{ hdName :: Text -- ^ Definition name
	, hdTypeSignature :: Maybe Text -- ^ Type signature (e.g., "x :: Int")
	, hdBody :: Text -- ^ Definition body
	, hdSourceLocation :: Maybe Text -- ^ Source location comment
	}
	deriving (Show, Generic)

	{-\| A compiled Haskell expression -}
	data HaskellExpr = HaskellExpr
	{ heExpr :: Text -- ^ The Haskell expression
	, heType :: Maybe Text -- ^ Inferred type annotation
	}
	deriving (Show, Generic)

	{-\| Code generation errors -}
	data CodeGenError
	= UnhandledConstruct String
	\| InvalidQName QName
	\| TypeCompilationFailed String
	\| ProofCompilationFailed String
	\| TermCompilationFailed String
	\| ModuleCompilationFailed String
	\| UnsupportedFeature String
	deriving (Show, Generic)

	{-\| Human-readable error formatting -}
	formatCodeGenError :: CodeGenError -> String
	formatCodeGenError = \case
	UnhandledConstruct desc ->
	"Code generation: unhandled construct: " ++ desc
	InvalidQName (QName mod name) ->
	"Code generation: invalid qualified name: " ++ intercalate "." (map T.unpack mod) ++ "." ++ T.unpack name
	TypeCompilationFailed desc ->
	"Code generation: type compilation failed: " ++ desc
	ProofCompilationFailed desc ->
	"Code generation: proof compilation failed: " ++ desc
	TermCompilationFailed desc ->
	"Code generation: term compilation failed: " ++ desc
	ModuleCompilationFailed desc ->
	"Code generation: module compilation failed: " ++ desc
	UnsupportedFeature desc ->
	"Code generation: unsupported feature: " ++ desc

	-- ============================================================================
	-- MAIN COMPILATION INTERFACE
	-- ============================================================================

	{-\| Compile an entire Assertica module to Haskell code.

	The module must be fully elaborated and type-checked before reaching this stage.
	This is the primary entry point for the backend.
	-}
	compileModule :: CodeGenConfig -> Module -> Either String HaskellModule
	compileModule config (Module _modQName _imports _exports defMap _metadata) = do
	-- Compile all definitions from the definition map
	compiledDefs <- mapM (compileDefinitionValue config) (Map.elems defMap)

	-- Generate module header
	let imports = generateImports config
	let comments = ["-- Generated by Assertica Backend", "-- Do not edit manually"]

	return $ HaskellModule
	{ hmName = [] -- Could extract from modQName if needed
	, hmImports = imports
	, hmDefinitions = compiledDefs
	, hmComments = comments
	}

	{-\| Compile a single definition from Module's Definition type -}
	compileDefinitionValue :: CodeGenConfig -> Definition -> Either String HaskellDefinition
	compileDefinitionValue config defn = case defn of
	DefTerm term -> do
	compiled <- compileExpression config term
	return $ HaskellDefinition
	{ hdName = "value" -- Anonymous term
	, hdTypeSignature = Nothing
	, hdBody = heExpr compiled
	, hdSourceLocation = if cgcAddComments config then Just "term" else Nothing
	}

	DefType ty -> do
	compiled <- compileType config ty
	return $ HaskellDefinition
	{ hdName = "type_def" -- Anonymous type
	, hdTypeSignature = Just "Type"
	, hdBody = heExpr compiled
	, hdSourceLocation = if cgcAddComments config then Just "type" else Nothing
	}

	DefAssertion _assertion -> do
	-- For now, compile assertion as a unit
	return $ HaskellDefinition
	{ hdName = "assertion"
	, hdTypeSignature = Nothing
	, hdBody = "()"
	, hdSourceLocation = if cgcAddComments config then Just "assertion" else Nothing
	}

	DefOpaque desc ->
	return $ HaskellDefinition
	{ hdName = "opaque"
	, hdTypeSignature = Nothing
	, hdBody = T.pack desc
	, hdSourceLocation = if cgcAddComments config then Just "opaque" else Nothing
	}

	{-\| Compile a single definition (can be a term, type, assertion, etc.) -}
	compileDefinition :: CodeGenConfig -> Definition -> Either String HaskellDefinition
	compileDefinition = compileDefinitionValue

	{-\| Compile a single term expression to Haskell -}
	compileExpression :: CodeGenConfig -> Term -> Either String HaskellExpr
	compileExpression config term = do
	expr <- TC.compileTerm config term
	return $ HaskellExpr
	{ heExpr = expr
	, heType = Nothing
	}

	{-\| Compile a type to Haskell -}
	compileType :: CodeGenConfig -> Type -> Either String HaskellExpr
	compileType config ty = do
	expr <- TyC.compileType config ty
	return $ HaskellExpr
	{ heExpr = expr
	, heType = Just "Type" -- All types have kind Type
	}

	{-\| Compile a proof to Haskell -}
	compileProof :: CodeGenConfig -> Proof -> Either String HaskellExpr
	compileProof config proof = do
	expr <- PC.compileProof config proof
	return $ HaskellExpr
	{ heExpr = expr
	, heType = Nothing
	}

	-- ============================================================================
	-- HELPER FUNCTIONS
	-- ============================================================================

	{-\| Generate standard Haskell imports for a module -}
	generateImports :: CodeGenConfig -> [Text]
	generateImports _config =
	[ "import Prelude"
	, "import qualified Data.Typeable as Typeable"
	, "import GHC.Generics (Generic)"
	]