assertica / src /Assertica /Backend /TermCompiler.hs

October 2026 main drop: mirror from GitHub

a10b189 verified about 1 month ago

7.44 kB

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

{-|
Module      : Assertica.Backend.TermCompiler
Description : Compile Assertica terms to Haskell expressions
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL-1.0
Translates computational terms from the Core AST to Haskell expressions:
MAPPINGS:
- Var v                     → v (variable reference)
- Const c                   → haskellLiteral c (constant)
- Lam (x : T) . e           → \x -> <compiled e> (lambda)
- App f x                   → (<compiled f>) (<compiled x>) (application)
- Constr C [e1, ..., en]    → C e1 ... en (constructor application)
- Case e [p1->b1, ...] def  → case e of { p1 -> b1; ... } (case expression)
- Let x = e1 in e2          → let x = <compiled e1> in <compiled e2>
- Ann e T                   → (<compiled e> :: <compiled T>) (type ascription)
- Forall (x : T) . body     → \(x :: <compiled T>) -> <compiled body> (dependent fn)
- ProofTerm p               → <compiled p> (proof evidence)
- Prop prop                 → proof-irrelevant <compiled p> (propositions as terms)
PRINCIPLES:
1. **Deterministic**: Always produces same output for same input
2. **Preserve Beta-Equivalence**: Compilation respects computational semantics
3. **Scope Preservation**: Free/bound variable distinction maintained
4. **No Code Simplification**: Generate direct translation (optimizer's job)
-}

module Assertica.Backend.TermCompiler
  ( -- * Main compilation function
    compileTerm
  , compilePattern
  , compileClause
  ) where

import Data.Text (Text)
import qualified Data.Text as T
import Data.List (intercalate, sortBy)
import Data.Ord (comparing)
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)

import Assertica.Core.AST
import Assertica.Backend.CodeGen (CodeGenConfig)

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

{-| Compile a term to Haskell source code.
This is the primary entry point for term compilation.
Returns either a Haskell expression string or an error.
-}
compileTerm :: CodeGenConfig -> Term -> Either String Text
compileTerm config term = compileTermWith config Set.empty term

{-| Compile a term with a given bound variable context.
The bound context tracks variables that are bound by enclosing lambdas,
let-bindings, or other binders, to ensure proper scoping.
-}
compileTermWith :: CodeGenConfig -> Set.Set Var -> Term -> Either String Text
compileTermWith config bound = \case
  Var (Var name _) ->
    Right $ name

  Const c -> Right $ compileConstant c

  Lam (Binder (Var name _) _mty) body ->
    let bound' = Set.insert (Var name 0) bound  -- Simplified: just track name
    in do
      compiledBody <- compileTermWith config bound' body
      Right $ "(\\(" <> name <> ") -> " <> compiledBody <> ")"

  App f x -> do
    cf <- compileTermWith config bound f
    cx <- compileTermWith config bound x
    Right $ "(" <> cf <> " " <> cx <> ")"

  Constr (QName mod name) args -> do
    compiledArgs <- mapM (compileTermWith 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 <> ")"

  Case scrutinee clauses defaultClause -> do
    cs <- compileTermWith config bound scrutinee
    compiledClauses <- mapM (compileClause config bound) clauses

    let caseClauses = T.intercalate "; " compiledClauses
    let defaultPart = case defaultClause of
          Nothing -> ""
          Just d -> do
            cd <- compileTermWith config bound d
            "; _ -> " <> cd

    Right $ "(case " <> cs <> " of { " <> caseClauses <> defaultPart <> " })"

  Let (Binder (Var name _) _) bindExpr bodyExpr -> do
    cb <- compileTermWith config bound bindExpr
    let bound' = Set.insert (Var name 0) bound
    ce <- compileTermWith config bound' bodyExpr
    Right $ "(let " <> name <> " = " <> cb <> " in " <> ce <> ")"

  Ann term _ty -> do
    -- For now, ignore the type annotation in code gen
    -- In a full implementation, could preserve as Haskell type ascription
    compileTermWith config bound term

  Forall (Binder (Var name _) _) body -> do
    -- Dependent function: treat as lambda abstraction
    let bound' = Set.insert (Var name 0) bound
    cb <- compileTermWith config bound' body
    Right $ "(\\(" <> name <> ") -> " <> cb <> ")"

  ProofTerm p -> do
    -- Proofs compile to evidence terms
    compileProofTerm config bound p

  Prop prop -> do
    -- Propositions as terms become proof-irrelevant ()
    -- The proposition itself is erased (proof irrelevance)
    Right "()"

-- ============================================================================
-- PATTERN COMPILATION
-- ============================================================================

{-| Compile a pattern to Haskell pattern syntax -}
compilePattern :: Pattern -> Either String Text
compilePattern = \case
  PatVar (Var name _) -> Right name

  PatConstr (QName mod name) pats -> do
    compiledPats <- mapM compilePattern pats
    let qname = if null mod
                  then name
                  else T.intercalate "." mod <> "." <> name
    if null compiledPats
      then Right qname
      else Right $ "(" <> qname <> " " <> T.intercalate " " compiledPats <> ")"

  PatWildcard -> Right "_"

  PatLit lit -> Right $ T.pack lit

{-| Compile a single case clause -}
compileClause :: CodeGenConfig -> Set.Set Var -> Clause -> Either String Text
compileClause config bound (Clause pat body) = do
  cp <- compilePattern pat
  cb <- compileTermWith config bound body
  Right $ cp <> " -> " <> cb

-- ============================================================================
-- CONSTANT COMPILATION
-- ============================================================================

{-| Compile a constant value -}
compileConstant :: Constant -> Text
compileConstant = \case
  PrimOp op -> compilePrimOp op
  IntLit n -> T.pack $ show n
  BoolLit b -> T.pack $ show b
  StringLit s -> T.pack $ show s
  UnitConst -> "()"
  ProofConst (QName mod name) ->
    if null mod
      then name
      else T.intercalate "." mod <> "." <> name

{-| Compile a primitive operation to Haskell -}
compilePrimOp :: PrimitiveOp -> Text
compilePrimOp = \case
  OpAdd -> "(+)"
  OpSub -> "(-)"
  OpMul -> "(*)"
  OpDiv -> "div"
  OpEq -> "(==)"
  OpNeq -> "(/=)"
  OpLt -> "(<)"
  OpLe -> "(<=)"
  OpGt -> "(>)"
  OpGe -> "(>=)"
  OpAnd -> "(&&)"
  OpOr -> "(||)"
  OpNot -> "not"
  OpIfThenElse -> "if"  -- Special handling in caller

-- ============================================================================
-- PROOF TERM COMPILATION (provisional)
-- ============================================================================

{-| Compile a proof term to Haskell evidence.
This is a simplified version that handles basic proof terms.
Full proof term handling is delegated to ProofCompiler.
-}
compileProofTerm :: CodeGenConfig -> Set.Set Var -> Proof -> Either String Text
compileProofTerm _config _bound = \case
  Refl e -> Right "Refl"
  Symm _ -> Right "Symm"
  Trans _ _ -> Right "Trans"
  ProofVar (Var name _) -> Right name
  _ -> Right "()"  -- Default: unit for unhandled proofs

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

	{-\|
	Module : Assertica.Backend.TermCompiler
	Description : Compile Assertica terms to Haskell expressions
	Copyright : (c) 2026 Ahmad Ali Parr
	License : BSL-1.0

	Translates computational terms from the Core AST to Haskell expressions:

	MAPPINGS:

	- Var v → v (variable reference)
	- Const c → haskellLiteral c (constant)
	- Lam (x : T) . e → \x -> <compiled e> (lambda)
	- App f x → (<compiled f>) (<compiled x>) (application)
	- Constr C [e1, ..., en] → C e1 ... en (constructor application)
	- Case e [p1->b1, ...] def → case e of { p1 -> b1; ... } (case expression)
	- Let x = e1 in e2 → let x = <compiled e1> in <compiled e2>
	- Ann e T → (<compiled e> :: <compiled T>) (type ascription)
	- Forall (x : T) . body → \(x :: <compiled T>) -> <compiled body> (dependent fn)
	- ProofTerm p → <compiled p> (proof evidence)
	- Prop prop → proof-irrelevant <compiled p> (propositions as terms)

	PRINCIPLES:

	1. Deterministic: Always produces same output for same input
	2. Preserve Beta-Equivalence: Compilation respects computational semantics
	3. Scope Preservation: Free/bound variable distinction maintained
	4. No Code Simplification: Generate direct translation (optimizer's job)
	-}

	module Assertica.Backend.TermCompiler
	( -- * Main compilation function
	compileTerm
	, compilePattern
	, compileClause
	) where

	import Data.Text (Text)
	import qualified Data.Text as T
	import Data.List (intercalate, sortBy)
	import Data.Ord (comparing)
	import qualified Data.Set as Set
	import qualified Data.Map.Strict as Map
	import GHC.Generics (Generic)

	import Assertica.Core.AST
	import Assertica.Backend.CodeGen (CodeGenConfig)

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

	{-\| Compile a term to Haskell source code.

	This is the primary entry point for term compilation.
	Returns either a Haskell expression string or an error.
	-}
	compileTerm :: CodeGenConfig -> Term -> Either String Text
	compileTerm config term = compileTermWith config Set.empty term

	{-\| Compile a term with a given bound variable context.

	The bound context tracks variables that are bound by enclosing lambdas,
	let-bindings, or other binders, to ensure proper scoping.
	-}
	compileTermWith :: CodeGenConfig -> Set.Set Var -> Term -> Either String Text
	compileTermWith config bound = \case
	Var (Var name _) ->
	Right $ name

	Const c -> Right $ compileConstant c

	Lam (Binder (Var name _) _mty) body ->
	let bound' = Set.insert (Var name 0) bound -- Simplified: just track name
	in do
	compiledBody <- compileTermWith config bound' body
	Right $ "(\\(" <> name <> ") -> " <> compiledBody <> ")"

	App f x -> do
	cf <- compileTermWith config bound f
	cx <- compileTermWith config bound x
	Right $ "(" <> cf <> " " <> cx <> ")"

	Constr (QName mod name) args -> do
	compiledArgs <- mapM (compileTermWith 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 <> ")"

	Case scrutinee clauses defaultClause -> do
	cs <- compileTermWith config bound scrutinee
	compiledClauses <- mapM (compileClause config bound) clauses

	let caseClauses = T.intercalate "; " compiledClauses
	let defaultPart = case defaultClause of
	Nothing -> ""
	Just d -> do
	cd <- compileTermWith config bound d
	"; _ -> " <> cd

	Right $ "(case " <> cs <> " of { " <> caseClauses <> defaultPart <> " })"

	Let (Binder (Var name _) _) bindExpr bodyExpr -> do
	cb <- compileTermWith config bound bindExpr
	let bound' = Set.insert (Var name 0) bound
	ce <- compileTermWith config bound' bodyExpr
	Right $ "(let " <> name <> " = " <> cb <> " in " <> ce <> ")"

	Ann term _ty -> do
	-- For now, ignore the type annotation in code gen
	-- In a full implementation, could preserve as Haskell type ascription
	compileTermWith config bound term

	Forall (Binder (Var name _) _) body -> do
	-- Dependent function: treat as lambda abstraction
	let bound' = Set.insert (Var name 0) bound
	cb <- compileTermWith config bound' body
	Right $ "(\\(" <> name <> ") -> " <> cb <> ")"

	ProofTerm p -> do
	-- Proofs compile to evidence terms
	compileProofTerm config bound p

	Prop prop -> do
	-- Propositions as terms become proof-irrelevant ()
	-- The proposition itself is erased (proof irrelevance)
	Right "()"

	-- ============================================================================
	-- PATTERN COMPILATION
	-- ============================================================================

	{-\| Compile a pattern to Haskell pattern syntax -}
	compilePattern :: Pattern -> Either String Text
	compilePattern = \case
	PatVar (Var name _) -> Right name

	PatConstr (QName mod name) pats -> do
	compiledPats <- mapM compilePattern pats
	let qname = if null mod
	then name
	else T.intercalate "." mod <> "." <> name
	if null compiledPats
	then Right qname
	else Right $ "(" <> qname <> " " <> T.intercalate " " compiledPats <> ")"

	PatWildcard -> Right "_"

	PatLit lit -> Right $ T.pack lit

	{-\| Compile a single case clause -}
	compileClause :: CodeGenConfig -> Set.Set Var -> Clause -> Either String Text
	compileClause config bound (Clause pat body) = do
	cp <- compilePattern pat
	cb <- compileTermWith config bound body
	Right $ cp <> " -> " <> cb

	-- ============================================================================
	-- CONSTANT COMPILATION
	-- ============================================================================

	{-\| Compile a constant value -}
	compileConstant :: Constant -> Text
	compileConstant = \case
	PrimOp op -> compilePrimOp op
	IntLit n -> T.pack $ show n
	BoolLit b -> T.pack $ show b
	StringLit s -> T.pack $ show s
	UnitConst -> "()"
	ProofConst (QName mod name) ->
	if null mod
	then name
	else T.intercalate "." mod <> "." <> name

	{-\| Compile a primitive operation to Haskell -}
	compilePrimOp :: PrimitiveOp -> Text
	compilePrimOp = \case
	OpAdd -> "(+)"
	OpSub -> "(-)"
	OpMul -> "(*)"
	OpDiv -> "div"
	OpEq -> "(==)"
	OpNeq -> "(/=)"
	OpLt -> "(<)"
	OpLe -> "(<=)"
	OpGt -> "(>)"
	OpGe -> "(>=)"
	OpAnd -> "(&&)"
	OpOr -> "(\|\|)"
	OpNot -> "not"
	OpIfThenElse -> "if" -- Special handling in caller

	-- ============================================================================
	-- PROOF TERM COMPILATION (provisional)
	-- ============================================================================

	{-\| Compile a proof term to Haskell evidence.

	This is a simplified version that handles basic proof terms.
	Full proof term handling is delegated to ProofCompiler.
	-}
	compileProofTerm :: CodeGenConfig -> Set.Set Var -> Proof -> Either String Text
	compileProofTerm _config _bound = \case
	Refl e -> Right "Refl"
	Symm _ -> Right "Symm"
	Trans _ _ -> Right "Trans"
	ProofVar (Var name _) -> Right name
	_ -> Right "()" -- Default: unit for unhandled proofs