MiniAgda-0.2025.7.23: src/MainLib.hs

module MainLib where

import Prelude hiding (null, mapM_)

import Data.Foldable (mapM_)

import System.Exit
import System.IO (stdout, hSetBuffering, BufferMode(..))

import qualified Language.Haskell.Exts.Syntax as H
import qualified Language.Haskell.Exts.Pretty as H

import Lexer
import Parser
import Options

import qualified Concrete as C
import qualified Abstract as A
import Abstract (Name)
import ScopeChecker
import TCM
import TypeChecker
import Extract
import ToHaskell

import Util

main :: IO ()
main = do
  hSetBuffering stdout NoBuffering
  -- putStrLn "MiniAgda by Andreas Abel and Karl Mehltretter"
  opts <- options
  mapM_ mainFile $ optInputs opts

mainFile :: String -> IO ()
mainFile fileName = do
  putStrLn $ "--- opening " ++ show fileName ++ " ---"
  file <- readFile fileName
  let t = alexScanTokens file
  let cdecls =  parse t
  -- putStrLn "--- parsing ---"
  -- mapM (putStrLn . show) cdecls
  putStrLn "--- scope checking ---"
  adecls <- doScopeCheck cdecls
  -- mapM (putStrLn . show) adecls
  putStrLn "--- type checking ---"
  (edecls, sig) <- doTypeCheck adecls
  putStrLn "--- evaluating ---"
  showAll sig adecls
{-
  putStrLn "--- extracting ---"
  edecls <- doExtract sig edecls
  hsmodule <- doTranslate edecls
  putStrLn $ H.prettyPrint hsmodule
  -- printHsDecls hsdecls
-}
  putStrLn $ "--- closing " ++ show fileName ++ " ---"

-- print extracted program

ppHsMode :: H.PPHsMode
ppHsMode = H.PPHsMode  -- H.defaultMode
  { H.classIndent  = 2
  , H.doIndent     = 3
  , H.multiIfIndent = 3
  , H.caseIndent   = 3
  , H.letIndent    = 4
  , H.whereIndent  = 2
  , H.onsideIndent = 1
  , H.spacing      = False
  , H.layout       = H.PPOffsideRule
  , H.linePragmas  = False
  }

printHsDecls :: [H.Decl ()] -> IO ()
printHsDecls hs = mapM_ (putStrLn . H.prettyPrintWithMode ppHsMode) hs

-- all let declarations
allLet :: Signature -> [A.Declaration] -> [(Name,A.Expr)]
allLet sig [] = []
allLet sig (decl:xs) =
    case decl of
      (A.LetDecl True n tel _ e) | null tel ->
          (n,e):(allLet sig xs)
      _ -> allLet sig xs


showAll :: Signature -> [A.Declaration] -> IO ()
showAll sig decl = mapM_ (showLet sig) $ allLet sig decl

showLet :: Signature -> (Name,A.Expr) -> IO ()
showLet sig (n,e) = do
  r <- doWhnf sig e
  case r of
    Right (v,_) -> putStrLn $ show n ++ " has whnf " ++ show v
    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err
                      exitFailure
  r <- doNf sig e
  case r of
    Right (v,_) -> putStrLn $ show n ++ " evaluates to " ++ show v
    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err
                      exitFailure

doExtract :: Signature -> [A.EDeclaration] -> IO [A.EDeclaration]
doExtract sig decls = do
  k <- runExtract sig $ extractDecls decls
  case k of
    Left err -> do
      putStrLn $ "error during extraction:\n" ++ show err
      exitFailure
    Right (hs, _) ->
      return hs

doTranslate :: [A.EDeclaration] -> IO (H.Module ())
doTranslate decls = do
  k <- runTranslate $ translateModule decls
  case k of
    Left err -> do
      putStrLn $ "error during extraction:\n" ++ show err
      exitFailure
    Right hs ->
      return hs

doTypeCheck :: [A.Declaration] -> IO ([A.EDeclaration], Signature)
doTypeCheck decls = do
  k <- typeCheck decls
  case k of
    Left err -> do
      putStrLn $ "error during typechecking:\n" ++ show err
      exitFailure
    Right (edecls, st) ->
      return (edecls, signature st)

doScopeCheck :: [C.Declaration] -> IO [A.Declaration]
doScopeCheck decl = case scopeCheck decl of
     Left err -> do putStrLn $ "scope check error: " ++ show err
                    exitFailure
     Right (decl',_) -> return $ decl'