GenerateDriver.hs

-- | Coq code generator driver: a thin host-side wrapper over the DSL-ported
-- `Hydra.Coq.Generate`. Only the `generateSources` adapter and the
-- `_CoqProject` writer live here; everything else has been promoted to DSL.

module Hydra.Coq.GenerateDriver where

import qualified Hydra.Packaging as Pkg
import qualified Hydra.Coq.Generate as CoqGenerate
import qualified Hydra.Context as Context
import qualified Hydra.Graph as Graph
import qualified Hydra.Errors as Errors
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Monad (forM_)
import Data.List (sort)
import System.Directory (copyFile, createDirectoryIfMissing, listDirectory)
import System.FilePath ((</>), takeDirectory)

-- | Standard coder interface: takes an adapted Module and Definitions,
-- returns a map from file paths to file contents.
-- Thin wrapper over the DSL-ported `Hydra.Coq.Generate.moduleToCoq` that
-- adapts the generateSources signature (accepting unused Context/Graph
-- parameters and wrapping the result in Either).
moduleToCoq :: Map.Map (String, String) String -> Map.Map String Int -> Set.Set String -> Set.Set String -> Pkg.Module -> [Pkg.Definition] -> Context.Context -> Graph.Graph
  -> Either Errors.Error (Map.Map FilePath String)
moduleToCoq fieldMap constrCounts ambiguousNames globalSanitizedAcc mod defs _cx _g =
  Right (CoqGenerate.moduleToCoq fieldMap constrCounts ambiguousNames globalSanitizedAcc mod defs)

-- | Generate a _CoqProject file for the output directory.
-- Maps the physical directory to the empty logical path so that
-- e.g. hydra/Core.v becomes module "hydra.Core".
writeCoqProject :: FilePath -> IO ()
writeCoqProject baseDir = do
  createDirectoryIfMissing True baseDir
  let content = unlines
        [ "# Generated by Hydra's Coq code generator"
        , "-Q . \"\""
        ]
  writeFile (baseDir </> "_CoqProject") content
  putStrLn "  _CoqProject"

-- | Copy the hand-written hydra.lib.* axiom-stub modules into the output tree.
-- These files declare Coq axioms for Hydra primitive functions whose bodies
-- are implemented natively in each host language. They have no DSL sources
-- (unlike hydra.lib.names, which is DSL-generated), so they are maintained
-- by hand under heads/haskell/src/main/coq/hydra/lib/ and copied into dist/
-- at generation time. The source path is resolved relative to the current
-- working directory, which is heads/haskell/ when generate-coq runs.
copyCoqLibFiles :: FilePath -> IO ()
copyCoqLibFiles baseDir = do
  let srcDir = "src/main/coq" </> "hydra" </> "lib"
      dstDir = baseDir </> "hydra" </> "lib"
  createDirectoryIfMissing True dstDir
  files <- sort <$> listDirectory srcDir
  forM_ files $ \f -> do
    copyFile (srcDir </> f) (dstDir </> f)
    putStrLn ("  hydra/lib/" ++ f)